Migrate to Goblint CIL

.circleci/config.yml

@@ -13,9 +13,14 @@ jobs:
               build-essential libbsd-dev libelf-dev libdw-dev binutils-dev zlib1g-dev \
               autoconf automake libtool pkg-config autoconf-archive \
               g++-10 gcc-10 lib32gcc-10-dev \
-              ocaml ocamlbuild ocaml-findlib libnum-ocaml-dev \
+              ocaml ocamlbuild ocaml-findlib libnum-ocaml-dev cppo \
               default-jdk-headless python3 \
               make git gawk gdb wget libc6-dbg \
+              ocaml-dune libdune-ocaml-dev \
+              libyojson-ocaml libyojson-ocaml-dev libppx-deriving-yojson-ocaml-dev \
+              libzarith-ocaml libzarith-ocaml-dev \
+              libnum-ocaml libnum-ocaml-dev \
+              libcsexp-ocaml libcsexp-ocaml-dev \
               libunwind-dev libunwind-dev:i386 linux-libc-dev-i386-cross libc6-dev-i386 \
               libboost-iostreams-dev libboost-regex-dev \
               libboost-serialization-dev libboost-filesystem-dev libffi-dev \
@@ -65,6 +70,7 @@ jobs:
               ca-certificates make build-essential g++-10 autoconf automake libtool \
               libelf-dev python3 git gawk libunwind-dev \
               ocaml ocamlbuild ocaml-findlib \
+              libppx-deriving-yojson-ocaml-dev libyojson-ocaml libnum-ocaml libzarith-ocaml \
               clang \
               libdw-dev binutils-dev libffi-dev \
               libboost-iostreams-dev libboost-regex-dev \

.gitmodules

@@ -16,9 +16,12 @@
 [submodule "contrib/donald"]
 	path = contrib/donald
 	url = https://github.com/stephenrkell/donald.git
-[submodule "contrib/cil"]
-	path = contrib/cil
-	url = https://github.com/stephenrkell/cil.git
 [submodule "contrib/elftin"]
 	path = contrib/elftin
 	url = https://github.com/stephenrkell/elftin.git
+[submodule "contrib/dune"]
+	path = contrib/dune
+	url = https://github.com/probablytom/dune.git
+[submodule "contrib/cil"]
+	path = contrib/cil
+	url = https://github.com/mbyzhangAlt/cil.git

README.md

@@ -220,11 +220,16 @@ look something like the following.
 
     $ sudo apt-get install libelf-dev libdw-dev binutils-dev \
         autoconf automake libtool pkg-config autoconf-archive \
-        g++ ocaml ocamlbuild ocaml-findlib \
+        g++ ocaml ocamlbuild ocaml-dune ocaml-findlib cppo \
+        libppx-deriving-yojson-ocaml-dev \
         default-jre-headless python3 python \
         make git gawk gdb wget \
         libunwind-dev libc6-dev-i386 zlib1g-dev libc6-dbg \
-        libboost-{iostreams,regex,serialization,filesystem}-dev && \
+        libboost-{iostreams,regex,serialization,filesystem}-dev \
+        cppo libcsexp-ocaml libcsexp-ocaml-dev libyojson-ocaml \
+        libyojson-ocaml-dev libnum-ocaml libnum-ocaml-dev \
+        libzarith-ocaml libzarith-ocaml-dev \
+        linux-libc-dev-i386-cross libdune-ocaml-dev libfindlib-ocaml-dev && \
     git clone https://github.com/stephenrkell/liballocs.git && \
     cd liballocs && \
     git submodule update --init --recursive && \

contrib/Makefile

@@ -1,6 +1,18 @@
 THIS_MAKEFILE := $(realpath $(lastword $(MAKEFILE_LIST)))
 CONTRIB := $(realpath $(dir $(THIS_MAKEFILE)))
 
+export LIBALLOCS_OCAML_PREFIX := $(CONTRIB)/../lib/ocaml
+CONFIG_MK += \nLIBALLOCS_OCAML_PREFIX := ${LIBALLOCS_OCAML_PREFIX}\n
+varlist += LIBALLOCS_OCAML_PREFIX
+
+export OCAML_LIBDEST := ${LIBALLOCS_OCAML_PREFIX}/lib
+export OCAMLPATH = ${OCAML_LIBDEST}
+
+export PATH := ${PATH}:${LIBALLOCS_OCAML_PREFIX}/bin
+
+export CC := gcc
+export CIL_CC := ${CC}
+
 # NOTE all this env.sh amounts to just a different way to do
 # ./configure --with-blah=/path/to/blah ?
 # ... but we prefer it because it's more compositional:
@@ -121,29 +133,45 @@ clean::
 # ----------------------------cil
 
 .PHONY: build-cil
-build-cil: cil.stamp
+build-cil: cil.stamp mainFeature.cmx
+
+.PHONY: dune-configurator
+dune-configurator:
+	cd dune && dune build -p dune-configurator && dune install -p dune-configurator --prefix=${LIBALLOCS_OCAML_PREFIX}
 
 # PROBLEM: cil's ocamlbuild takes a significant time to re-run even in the
 # case where nothing's changed. So use a stamp to run around that.
-cil.stamp: cil/Makefile $(shell find cil -name '*.c' -o -name '*.ml' -o -name '*.mli' -o -name '*.in' -o -name '*.mly' )
-	$(MAKE) -C cil all install-local && touch $@
-cil/Makefile: cil/configure
-	cd cil && CC=$${ALLOCSCC_CC:-$${CC:-cc}} ./configure INSTALL="`which install` -p"
+cil.stamp: goblint-cil
+goblint-cil: dune-configurator
+	cd cil && dune build && dune build @install && dune install --prefix=${LIBALLOCS_OCAML_PREFIX}
+	touch cil.stamp
+
+CONFIG_MK += \nCIL_ROOT ?= $(CONTRIB)/cil/\n
+varlist += CIL_ROOT
+export CIL_ROOT
 
-CONFIG_MK += \nCIL_INSTALL ?= $(CONTRIB)/cil/lib\n
+CONFIG_MK += \nCIL_INSTALL ?= ${LIBALLOCS_OCAML_PREFIX}/lib/goblint-cil/\n
 varlist += CIL_INSTALL
 export CIL_INSTALL
 
+.PHONY: mainFeature.cmx
+mainFeature.cmx: cil.stamp
+	cd cil && cp ${CIL_ROOT}/src/mainFeature.ml ${CIL_ROOT}/src/mainFeature.mli ${CIL_INSTALL} && ocamlfind ocamlopt -c ${CIL_INSTALL}/mainFeature.mli && ocamlfind ocamlopt -linkpkg -package dynlink -package findlib -package str -package zarith -I ${CIL_INSTALL} ${CIL_INSTALL}goblintCil.cmxa ${CIL_INSTALL}mainFeature.ml
+
+.PHONY: goblint-cil-deps
+goblint-cil-deps: dune-configurator
+
 clean::
-	$(MAKE) -C cil clean
+	cd cil && dune clean
+	cd dune   && dune uninstall -p dune-configurator --prefix=/usr/lib/ocaml/
 	rm -f cil.stamp
 
 # ----------------------------toolsub
 
 .PHONY: build-toolsub
 build-toolsub: build-cil
 	$(MAKE) -C toolsub wrapper-recursive cilpp-recursive  # don't build clang-based cccppp
-	$(MAKE) -C toolsub/wrapper/example/constructor-priority-checker dumpconstr
+	#$(MAKE) -C toolsub/wrapper/example/constructor-priority-checker dumpconstr
 CONFIG_MK += \nTOOLSUB ?= $(CONTRIB)/toolsub\n
 varlist += TOOLSUB
 

include/liballocs_cil_inlines.h

@@ -85,15 +85,15 @@ CURRENT_ALLOC_VARS_QUALIFIERS void *__current_allocsite CURRENT_ALLOC_VARS_QUALI
 
 void __liballocs_unindex_stack_objects_counted_by(unsigned long *, void *frame_addr);
 
-extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_alloca_caller_frame_cleanup)(void *counter);
-extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_alloca_caller_frame_cleanup)(void *counter)
+extern inline void (__attribute__((always_inline,gnu_inline)) __liballocs_alloca_caller_frame_cleanup)(void *counter);
+extern inline void (__attribute__((always_inline,gnu_inline)) __liballocs_alloca_caller_frame_cleanup)(void *counter)
 {
 	__liballocs_unindex_stack_objects_counted_by((unsigned long *) counter, __builtin_frame_address(0));
 }
 
 /* alloca helpers */
-extern inline const void *(__attribute__((always_inline,gnu_inline,used)) __liballocs_get_sp)(void);
-extern inline const void *(__attribute__((always_inline,gnu_inline,used)) __liballocs_get_sp)(void)
+extern inline const void *(__attribute__((always_inline,gnu_inline)) __liballocs_get_sp)(void);
+extern inline const void *(__attribute__((always_inline,gnu_inline)) __liballocs_get_sp)(void)
 {
 	unsigned long our_sp;
 	#ifdef UNW_TARGET_X86
@@ -104,8 +104,8 @@ extern inline const void *(__attribute__((always_inline,gnu_inline,used)) __liba
 	return (const void*) our_sp;
 }
 
-extern inline const void *(__attribute__((always_inline,gnu_inline,used)) __liballocs_get_bp)(void);
-extern inline const void *(__attribute__((always_inline,gnu_inline,used)) __liballocs_get_bp)(void)
+extern inline const void *(__attribute__((always_inline,gnu_inline)) __liballocs_get_bp)(void);
+extern inline const void *(__attribute__((always_inline,gnu_inline)) __liballocs_get_bp)(void)
 {
 	return (const void *) __builtin_frame_address(0);
 }
@@ -118,8 +118,8 @@ extern inline const void *(__attribute__((always_inline,gnu_inline,used)) __liba
  * for the allocation site / type metadata. We call a helper to get
  * the *overall* size, and then the __liballocs_notify_and_adjust_alloca()
  * function will fill in both the header and the trailer. */
-extern inline unsigned long (__attribute__((always_inline,gnu_inline,used)) __liballocs_alloca_size)(unsigned long orig_size);
-extern inline unsigned long (__attribute__((always_inline,gnu_inline,used)) __liballocs_alloca_size)(unsigned long orig_size)
+extern inline unsigned long (__attribute__((always_inline,gnu_inline)) __liballocs_alloca_size)(unsigned long orig_size);
+extern inline unsigned long (__attribute__((always_inline,gnu_inline)) __liballocs_alloca_size)(unsigned long orig_size)
 {
 	/* Insert heap trailer etc..
 	 * Basically we have to do everything that our malloc hooks, allocator wrappers
@@ -138,8 +138,8 @@ extern inline unsigned long (__attribute__((always_inline,gnu_inline,used)) __li
 	 * we don't track them. */
 }
 
-extern inline void *(__attribute__((always_inline,gnu_inline,used)) __liballocs_notify_and_adjust_alloca)(void *allocated, unsigned long orig_size, unsigned long tweaked_size, unsigned long *frame_counter, void *caller);
-extern inline void *(__attribute__((always_inline,gnu_inline,used)) __liballocs_notify_and_adjust_alloca)(void *allocated, unsigned long orig_size, unsigned long tweaked_size, unsigned long *frame_counter, void *caller)
+extern inline void *(__attribute__((always_inline,gnu_inline)) __liballocs_notify_and_adjust_alloca)(void *allocated, unsigned long orig_size, unsigned long tweaked_size, unsigned long *frame_counter, void *caller);
+extern inline void *(__attribute__((always_inline,gnu_inline)) __liballocs_notify_and_adjust_alloca)(void *allocated, unsigned long orig_size, unsigned long tweaked_size, unsigned long *frame_counter, void *caller)
 {
 #ifndef LIBALLOCS_NO_ZERO
 	__builtin_memset(allocated, 0, tweaked_size);
@@ -213,8 +213,8 @@ struct __liballocs_memrange_cache
 };
 extern struct __liballocs_memrange_cache /* __thread */ __liballocs_ool_cache;
 
-extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_check_cache_sanity )(struct __liballocs_memrange_cache *cache __attribute__((unused)));
-extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_check_cache_sanity )(struct __liballocs_memrange_cache *cache __attribute__((unused)))
+extern inline void (__attribute__((always_inline,gnu_inline)) __liballocs_check_cache_sanity )(struct __liballocs_memrange_cache *cache __attribute__((unused)));
+extern inline void (__attribute__((always_inline,gnu_inline)) __liballocs_check_cache_sanity )(struct __liballocs_memrange_cache *cache __attribute__((unused)))
 {
 #ifdef DEBUG
 	unsigned visited_linear = 0u;
@@ -247,8 +247,8 @@ extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_c
 #endif
 }
 
-extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_cache_unlink )(struct __liballocs_memrange_cache *cache, unsigned i);
-extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_cache_unlink )(struct __liballocs_memrange_cache *cache, unsigned i)
+extern inline void (__attribute__((always_inline,gnu_inline)) __liballocs_cache_unlink )(struct __liballocs_memrange_cache *cache, unsigned i);
+extern inline void (__attribute__((always_inline,gnu_inline)) __liballocs_cache_unlink )(struct __liballocs_memrange_cache *cache, unsigned i)
 {
 	__liballocs_check_cache_sanity(cache);
 	/* unset validity and make this the next victim */
@@ -266,8 +266,8 @@ extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_c
 	__liballocs_check_cache_sanity(cache);
 }
 
-extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_cache_push_head_mru )(struct __liballocs_memrange_cache *cache, unsigned i);
-extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_cache_push_head_mru )(struct __liballocs_memrange_cache *cache, unsigned i)
+extern inline void (__attribute__((always_inline,gnu_inline)) __liballocs_cache_push_head_mru )(struct __liballocs_memrange_cache *cache, unsigned i);
+extern inline void (__attribute__((always_inline,gnu_inline)) __liballocs_cache_push_head_mru )(struct __liballocs_memrange_cache *cache, unsigned i)
 {
 	__liballocs_check_cache_sanity(cache);
 	/* Put us at the head of the LRU chain. */
@@ -284,8 +284,8 @@ extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_c
 	__liballocs_check_cache_sanity(cache);
 }	
 
-extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_cache_bump_victim )(struct __liballocs_memrange_cache *cache, unsigned i);
-extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_cache_bump_victim )(struct __liballocs_memrange_cache *cache, unsigned i)
+extern inline void (__attribute__((always_inline,gnu_inline)) __liballocs_cache_bump_victim )(struct __liballocs_memrange_cache *cache, unsigned i);
+extern inline void (__attribute__((always_inline,gnu_inline)) __liballocs_cache_bump_victim )(struct __liballocs_memrange_cache *cache, unsigned i)
 {
 	__liballocs_check_cache_sanity(cache);
 	/* make sure we're not the next victim */
@@ -299,8 +299,8 @@ extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_c
 	__liballocs_check_cache_sanity(cache);
 }
 
-extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_cache_bump_mru )(struct __liballocs_memrange_cache *cache, unsigned i);
-extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_cache_bump_mru )(struct __liballocs_memrange_cache *cache, unsigned i)
+extern inline void (__attribute__((always_inline,gnu_inline)) __liballocs_cache_bump_mru )(struct __liballocs_memrange_cache *cache, unsigned i);
+extern inline void (__attribute__((always_inline,gnu_inline)) __liballocs_cache_bump_mru )(struct __liballocs_memrange_cache *cache, unsigned i)
 {
 	__liballocs_check_cache_sanity(cache);
 	if (cache->head_mru != i)
@@ -312,10 +312,10 @@ extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_c
 }
 
 extern inline
-struct __liballocs_memrange_cache_entry_s *(__attribute__((always_inline,gnu_inline,used))
+struct __liballocs_memrange_cache_entry_s *(__attribute__((always_inline,gnu_inline))
 __liballocs_memrange_cache_lookup )(struct __liballocs_memrange_cache *cache, const void *obj, struct uniqtype *t, unsigned long require_period);
 extern inline
-struct __liballocs_memrange_cache_entry_s *(__attribute__((always_inline,gnu_inline,used))
+struct __liballocs_memrange_cache_entry_s *(__attribute__((always_inline,gnu_inline))
 __liballocs_memrange_cache_lookup )(struct __liballocs_memrange_cache *cache, const void *obj, struct uniqtype *t, unsigned long require_period)
 {
 #ifndef LIBALLOCS_NOOP_INLINES
@@ -352,10 +352,10 @@ __liballocs_memrange_cache_lookup )(struct __liballocs_memrange_cache *cache, co
 }
 
 extern inline
-struct __liballocs_memrange_cache_entry_s *(__attribute__((always_inline,gnu_inline,used))
+struct __liballocs_memrange_cache_entry_s *(__attribute__((always_inline,gnu_inline))
 __liballocs_memrange_cache_lookup_notype )(struct __liballocs_memrange_cache *cache, const void *obj, unsigned long require_period);
 extern inline
-struct __liballocs_memrange_cache_entry_s *(__attribute__((always_inline,gnu_inline,used))
+struct __liballocs_memrange_cache_entry_s *(__attribute__((always_inline,gnu_inline))
 __liballocs_memrange_cache_lookup_notype )(struct __liballocs_memrange_cache *cache, const void *obj, unsigned long require_period)
 {
 #ifndef LIBALLOCS_NOOP_INLINES
@@ -389,8 +389,8 @@ __liballocs_memrange_cache_lookup_notype )(struct __liballocs_memrange_cache *ca
 	return (struct __liballocs_memrange_cache_entry_s *)(void*)0;
 }
 
-extern inline struct uniqtype *(__attribute__((always_inline,gnu_inline,used)) __liballocs_get_cached_object_type)(const void *addr);
-extern inline struct uniqtype *(__attribute__((always_inline,gnu_inline,used)) __liballocs_get_cached_object_type)(const void *addr)
+extern inline struct uniqtype *(__attribute__((always_inline,gnu_inline)) __liballocs_get_cached_object_type)(const void *addr);
+extern inline struct uniqtype *(__attribute__((always_inline,gnu_inline)) __liballocs_get_cached_object_type)(const void *addr)
 {
 	struct __liballocs_memrange_cache_entry_s *found = __liballocs_memrange_cache_lookup_notype(
 		&__liballocs_ool_cache,

lib/ocaml/.gitignore

@@ -0,0 +1,8 @@
+# We want to ensure lib/ocaml _always_ exists, but we can't commit an empty dir
+# to a git repo. There has to be some content at this path. However, everything
+# that gets placed here is a build artifact that shouldn't be committed.
+
+# So: ignore everything in this directory _except_ this file, so that this file
+# ensures the path exists.
+*
+!.gitignore

tools/allocscompilerwrapper.py

@@ -676,7 +676,7 @@ def main(self):
                 linkItemsIncluded = []
                 linkItemsDeferred = []
                 for item in allLinkItems:
-                    if item.startswith("-L") or item.startswith("-l") or item.endswith(".so"):
+                    if item.startswith("-L") or item.startswith("-l") or re.match(".*\\.so(\\.[0-9]+)*$", item):
                         linkItemsDeferred += [item]
                     else:
                         linkItemsIncluded += [item]

tools/lang/c/Makefile

@@ -6,10 +6,17 @@ OCAMLFIND ?= ocamlfind
 ifeq ($(CIL_INSTALL),)
 $(error "Expected CIL_INSTALL to be set")
 endif
+ifeq ($(LIBALLOCS_OCAML_PREFIX),)
+$(error "Expected LIBALLOCS_OCAML_PREFIX to be set")
+endif
+
+export OCAMLPATH := $(LIBALLOCS_OCAML_PREFIX)/lib:$(OCAMLPATH)
+
 CILLY ?= $(CIL_INSTALL)/../bin/cilly
 CIL_TOOLS ?= cilallocs dumpallocs monalloca dumpmemacc trapptrwrites
-OCAMLFLAGS +=  -package findlib
-OCAMLFLAGS += -I $(CIL_INSTALL)/cil -I $(dir $(THIS_MAKEFILE))/cilallocs
+OCAMLFLAGS += -package findlib -package goblint-cil
+OCAMLFLAGS += -I $(dir $(THIS_MAKEFILE))/cilallocs
+OCAMLFLAGS += -open GoblintCil -open GoblintCil.Cilint
 
 CIL_TOOLS_SRC := $(shell find $(CIL_TOOLS) $(realpath $(dir $(THIS_MAKEFILE)))/lib -name '*.ml')
 
@@ -27,6 +34,7 @@ DEPS += $(OCAML_DEPS)
 	$(OCAMLFIND) ocamlopt -shared -o "$@" $(OCAMLOPTFLAGS) $(OCAMLFLAGS) $+
 %.cmx %.cmi: %.ml
 	$(OCAMLFIND) ocamlopt -o "$@" $(OCAMLOPTFLAGS) $(OCAMLFLAGS) -c "$<"
+goblintCil.cmo: goblintCil.ml ;
 %.cmo %.cmi: %.ml
 	$(OCAMLFIND) ocamlc -o "$@" $(OCAMLFLAGS) -c "$<"
 %.cma: %.cmo
@@ -46,4 +54,4 @@ monalloca/monalloca.cmo: cilallocs/cilallocs.cmo
 
 .PHONY: clean
 clean:
-	for dir in $(CIL_TOOLS); do (cd $$dir && rm -f *.o *.cmo *.cma *.cmi *.cmx *.cmxa *.cmxs *.cil.c *.i ); done
+	for dir in $(CIL_TOOLS); do (cd $$dir && rm -f *.o *.cmo *.cma *.cmi *.cmx *.cmxa *.cmxs *.cil.c *.i *.d ); done

tools/lang/c/bin/allocscc

@@ -12,21 +12,17 @@ import os, sys, re, subprocess, tempfile
 REAL_FILE = os.path.realpath(__file__)
 REAL_DIR = os.path.realpath(os.path.dirname(REAL_FILE))
 liballocs_base = os.path.realpath(REAL_DIR + "/../../../..")
+ocaml_prefix = os.environ.get("LIBALLOCS_OCAML_PREFIX", liballocs_base + "/lib/ocaml")
+cilly_cmd = ocaml_prefix + "/bin/cilly"
 sys.path.append(liballocs_base + "/tools")
 from allocscompilerwrapper import *
-existing_cil_install = os.environ.get("CIL_INSTALL")
-if existing_cil_install == None:
-    cilly_cmd = liballocs_base + "/contrib/cil/bin/cilly"
-    existing_cil_install = liballocs_base + "/contrib/cil/lib"
-else:
-    cilly_cmd = existing_cil_install + "/../bin/cilly"
 existing_elftin = os.environ.get("ELFTIN")
 if existing_elftin == None:
     os.putenv("ELFTIN", liballocs_base + "/contrib/elftin")
 existing_ocamlpath = os.environ.get("OCAMLPATH")
 if existing_ocamlpath == None:
     existing_ocamlpath = ""
-os.putenv("OCAMLPATH", existing_cil_install + ":" + existing_ocamlpath)
+os.putenv("OCAMLPATH", ocaml_prefix + "/lib:" + existing_ocamlpath)
 os.putenv("LANG", "C") # Allow allocscc to be called with non-english locales
 
 class AllocsCC(AllocsCompilerWrapper):
@@ -95,7 +91,7 @@ class AllocsCC(AllocsCompilerWrapper):
             return []
         return [
             "--decil",
-            "--native",
+            #"--native",
             "--load=%s" % (self.getLibAllocsBaseDir() + "/tools/lang/c/cilallocs/cilallocs.cmxs"),
             "--load=%s" % (self.getLibAllocsBaseDir() + "/tools/lang/c/dumpallocs/dumpallocs.cmxs"),
             "--dodumpallocs",