diff --git a/.circleci/config.yml b/.circleci/config.yml index 3fbb4803c..d5f8a2982 100644 --- a/.circleci/config.yml +++ b/.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 \ diff --git a/.gitmodules b/.gitmodules index ccc214c85..0355a584f 100644 --- a/.gitmodules +++ b/.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 diff --git a/README.md b/README.md index 397b4b34d..ddfc04999 100644 --- a/README.md +++ b/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 && \ diff --git a/contrib/Makefile b/contrib/Makefile index 64f1969d2..14f01c12f 100644 --- a/contrib/Makefile +++ b/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,21 +133,37 @@ 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 @@ -143,7 +171,7 @@ clean:: .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 diff --git a/contrib/cil b/contrib/cil index cc5a6ce72..783788822 160000 --- a/contrib/cil +++ b/contrib/cil @@ -1 +1 @@ -Subproject commit cc5a6ce72e5adbcd1b1fe622a0316c6df7f22e44 +Subproject commit 783788822b09d1ebe15fb1ba7bdec76bdd2fb82b diff --git a/contrib/dune b/contrib/dune new file mode 160000 index 000000000..ef3b45c08 --- /dev/null +++ b/contrib/dune @@ -0,0 +1 @@ +Subproject commit ef3b45c08a4db30a2581f231ccc267ec4ce73c3c diff --git a/contrib/toolsub b/contrib/toolsub index 601bb2062..fa1b495dd 160000 --- a/contrib/toolsub +++ b/contrib/toolsub @@ -1 +1 @@ -Subproject commit 601bb2062337a981796c576e4884c8ca1c333192 +Subproject commit fa1b495ddd432cc9b378774ca78f1b99d46fd3e2 diff --git a/include/liballocs_cil_inlines.h b/include/liballocs_cil_inlines.h index dc60af1d6..b173bdf5f 100644 --- a/include/liballocs_cil_inlines.h +++ b/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, diff --git a/lib/ocaml/.gitignore b/lib/ocaml/.gitignore new file mode 100644 index 000000000..83f42c9bf --- /dev/null +++ b/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 diff --git a/tools/allocscompilerwrapper.py b/tools/allocscompilerwrapper.py index 9d27b81a0..f25c25690 100644 --- a/tools/allocscompilerwrapper.py +++ b/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] diff --git a/tools/lang/c/Makefile b/tools/lang/c/Makefile index b88f47093..f6c4f6fed 100644 --- a/tools/lang/c/Makefile +++ b/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 diff --git a/tools/lang/c/bin/allocscc b/tools/lang/c/bin/allocscc index 9caff7bb3..bf44a1a85 100755 --- a/tools/lang/c/bin/allocscc +++ b/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", diff --git a/tools/lang/c/cilallocs/cilallocs.ml b/tools/lang/c/cilallocs/cilallocs.ml index 5414059e3..3c2431c9e 100644 --- a/tools/lang/c/cilallocs/cilallocs.ml +++ b/tools/lang/c/cilallocs/cilallocs.ml @@ -43,7 +43,6 @@ open Unix open List open Str open Map -open Pretty open Cil open Hashtbl module NamedTypeMap = Map.Make(String) @@ -169,7 +168,7 @@ let unzip l = let foldConstants e = visitCilExpr (Cil.constFoldVisitor true) e -let makeIntegerConstant n = Const(CInt64(n, IInt, None)) +let makeIntegerConstant n = Const(CInt(n, IInt, None)) let isStaticallyZero e = isZero (foldConstants e) @@ -186,8 +185,8 @@ let rec isStaticallyNull e = isStaticallyZero e || isStaticallyNullPtr e let constInt64ValueOfExprNoChr (intExp: Cil.exp) : int64 option = match (foldConstants intExp) with - Const(CInt64(intValue, _, _)) -> - Some(intValue) + Const(CInt(intValue, _, _)) -> + Some(int64_of_cilint intValue) | _ -> None let constInt64ValueOfExpr (intExp: Cil.exp) : int64 option = @@ -196,9 +195,9 @@ let constInt64ValueOfExpr (intExp: Cil.exp) : int64 option = | _ -> constInt64ValueOfExprNoChr intExp let nullPtr = CastE( TPtr(TVoid([]), []) , zero ) -let one = Const(CInt64((Int64.of_int 1), IInt, None)) +let one = Const(CInt((cilint_of_int64 (Int64.of_int 1)), IInt, None)) let onePtr = CastE( TPtr(TVoid([]), []) , one ) -let negativeOne = Const(CInt64((Int64.of_int (0-1)), IInt, None)) +let negativeOne = Const(CInt(cilint_of_int64 (Int64.of_int (0-1)), IInt, None)) let negativeOnePtr = CastE( TPtr(TVoid([]), []) , negativeOne ) let debug_print lvl s = @@ -208,7 +207,7 @@ let debug_print lvl s = int_of_string levelString end with Not_found -> 0 | Failure(_) -> 0 in - if level >= lvl then (output_string Pervasives.stderr s; flush Pervasives.stderr) else () + if level >= lvl then (output_string Out_channel.stderr s; flush Out_channel.stderr) else () (* HACKed realpath for now: *) let abspath f = @@ -229,8 +228,8 @@ let trim str = in let len = String.length str in try - let left = search_pos 0 (fun i -> i >= len) (succ) - and right = search_pos (len - 1) (fun i -> i < 0) (pred) + let left = search_pos 0 (fun i -> i >= len) (Stdlib.succ) + and right = search_pos (len - 1) (fun i -> i < 0) (Stdlib.pred) in String.sub str left (right - left + 1) with Empty -> "" @@ -305,7 +304,7 @@ let rec barenameFromSig ts = "__ARG" ^ (string_of_int startAt) ^ "_" ^ (barenameFromSig t) ^ remainder in match ts with - TSArray(tNestedSig, optSz, attrs) -> "__ARR" ^ (match optSz with Some(s) -> (string_of_int (i64_to_int s)) | None -> "0") ^ "_" ^ (barenameFromSig tNestedSig) + TSArray(tNestedSig, optSz, attrs) -> "__ARR" ^ (match optSz with Some(s) -> (string_of_int (i64_to_int (int64_of_cilint s))) | None -> "0") ^ "_" ^ (barenameFromSig tNestedSig) | TSPtr(tNestedSig, attrs) -> "__PTR_" ^ (barenameFromSig tNestedSig) | TSComp(isSpecial, name, attrs) -> name | TSFun(returnTs, Some(argsTss), false, attrs) -> @@ -333,7 +332,7 @@ let rec dwarfidlFromSig ts = match ts with TSArray(tNestedSig, optSz, attrs) -> "(array_type [type = " ^ (dwarfidlFromSig tNestedSig) ^ "] {" - ^ (match optSz with Some(s) -> ("subrange_type [upper_bound = " ^ (string_of_int (i64_to_int s)) ^ "];") | None -> "") ^ " })" + ^ (match optSz with Some(s) -> ("subrange_type [upper_bound = " ^ (string_of_int (i64_to_int (int64_of_cilint s))) ^ "];") | None -> "") ^ " })" | TSPtr(tNestedSig, attrs) -> "(pointer_type [type = " ^ (dwarfidlFromSig tNestedSig) ^ "];)" | TSComp(isSpecial, name, attrs) -> name | TSFun(returnTs, Some(argsTss), false, attrs) -> @@ -384,7 +383,7 @@ let rec decayArrayInTypesig ts = match ts with let rec accumulateArrayDimensionsInTypesig ts = match ts with TSArray(tsig, Some(sz), attrs) -> (* recurse for multidim arrays *) (match accumulateArrayDimensionsInTypesig tsig with - (ts, Some(subN)) -> (ts, Some(Int64.mul sz subN)) + (ts, Some(subN)) -> (ts, Some(Int64.mul (int64_of_cilint sz) subN)) | (ts, None) -> (ts, None) ) | TSArray(tsig, None, attrs) -> (* recurse for multidim arrays *) @@ -398,7 +397,7 @@ let rec collapseArrayDimensionsInTypesig ts = match ts with -> (* tsig is also an array, so ... *) let ts, maybeSz = accumulateArrayDimensionsInTypesig ts in - TSArray(ts, maybeSz, attrs) + TSArray(ts, Option.map cilint_of_int64 maybeSz, attrs) | _ -> ts (* This will make a "pointer to array of X" typesig into a "pointer to X" typesig. @@ -481,7 +480,6 @@ let matchIgnoringLocation g1 g2 = match g1 with | GAsm(s, loc) -> begin match g2 with GAsm(s2, loc) -> s = s2 | _ -> false end | GPragma(a, loc) -> begin match g2 with GPragma(a2, loc) -> a = a2 | _ -> false end | GText(s) -> begin match g2 with GText(s2) -> s = s2 | _ -> false end - | GStaticAssert(e,s,l) -> begin match g2 with GStaticAssert(e2,s2,_)-> e=e2 && s=s2 | _ -> false end let isFunction g = match g with GFun(_, _) -> true @@ -576,7 +574,7 @@ let getOrCreateUniqtypeGlobal m concreteType globals = tempGlobal.vattr <- [Attr("weak", [])]; tempGlobal in - let newGlobalVarInfo = GVarDecl(newGlobal, {line = -1; file = "BLAH FIXME"; byte = 0}) + let newGlobalVarInfo = GVarDecl(newGlobal, {line = -1; file = "BLAH FIXME"; byte = 0; column = -1; endLine = -1; endByte = -1; endColumn = -1; synthetic = false }) in let newMap = (UniqtypeMap.add concreteType newGlobalVarInfo m) in @@ -671,7 +669,7 @@ let findOrCreateExternalFunctionInFile fl nm proto : fundec = (* findOrCreateFun Some(d) -> d | None -> let funDec = emptyFunction nm in funDec.svar.vtype <- proto; - fl.globals <- newGlobalsList fl.globals [GVarDecl(funDec.svar, {line = -1; file = "BLAH FIXME"; byte = 0})] isFunction; + let loc = {line = -1; file = "BLAH FIXME"; byte = 0; column = -1; endLine = -1; endByte = -1; endColumn = -1; synthetic = false } in funDec let findOrCreateNewFunctionInFile fl nm proto l createBeforePred : fundec = (* findOrCreateFunc fl nm proto *) (* NO! doesn't let us have the fundec *) @@ -696,7 +694,7 @@ let makeInlineFunctionInFile fl ourFun nm proto body referencedValues = begin let arglist = List.map (fun (ident, typ, attrs) -> makeFormalVar ourFun ident typ) protoArgs in let () = setFunctionType ourFun protoWithInlineAttrs in let nameFunc = (fun n t -> makeTempVar ourFun ~name:n t) in - let loc = {line = -1; file = "BLAH FIXME"; byte = 0} in + let loc = {line = -1; file = "BLAH FIXME"; byte = 0; column = -1; endLine = -1; endByte = -1; endColumn = -1; synthetic = false } in let argPatternBindings = List.map (fun ((ident, typ, attrs), arg) -> (ident, Fv arg)) (List.combine protoArgs arglist) in let extPatternBindings = (* List.map (fun (ident, v) -> (ident, Fv v)) *) referencedValues in let madeBody = mkBlock (Formatcil.cStmts body nameFunc loc (argPatternBindings @ extPatternBindings)) in @@ -845,7 +843,8 @@ let restructureInstrsStatement skind = Instr(group); sid = 0; succs = []; - preds = [] + preds = []; + fallthrough = None }] }) in @@ -854,7 +853,8 @@ let restructureInstrsStatement skind = skind; sid = 0; succs = []; - preds = [] + preds = []; + fallthrough = None } ) groupedInstrs) in let b = mkBlock stmts in diff --git a/tools/lang/c/dumpallocs/dumpallocs.ml b/tools/lang/c/dumpallocs/dumpallocs.ml index 520900c78..55043a8e0 100644 --- a/tools/lang/c/dumpallocs/dumpallocs.ml +++ b/tools/lang/c/dumpallocs/dumpallocs.ml @@ -87,7 +87,7 @@ let maybeDecayArrayTypesig maybeTs = match maybeTs with | _ -> Undet let rec getSizeExpr (ex: exp) (env : (int * sz) list) (gs : Cil.global list) : sz = - debug_print 2 ("Hello from getSizeExpr(" ^ (Pretty.sprint 80 (Pretty.dprintf "%a" d_exp ex)) ^ ") ... "); flush Pervasives.stderr; + debug_print 2 ("Hello from getSizeExpr(" ^ (Pretty.sprint 80 (Pretty.dprintf "%a" d_exp ex)) ^ ") ... "); flush Out_channel.stderr; let isTrailingField fi compinfo = let reverseFields = rev compinfo.cfields in @@ -112,17 +112,17 @@ let rec getSizeExpr (ex: exp) (env : (int * sz) list) (gs : Cil.global list) : s * &a.i[0] a.k.a. &a.i a.k.a. a.i * might be a trailing field, if i is the last field in the struct. *) let rec isTrailingFieldOffsetExpr ts off = - debug_print 2 ("Hello from isTrailingFieldOffsetExpr(" ^ (Pretty.sprint 80 (d_typsig () ts)) ^ (Pretty.sprint 80 (d_offset Pretty.nil () off)) ^ ") "); flush Pervasives.stderr; + debug_print 2 ("Hello from isTrailingFieldOffsetExpr(" ^ (Pretty.sprint 80 (d_typsig () ts)) ^ (Pretty.sprint 80 (d_offset Pretty.nil () off)) ^ ") "); flush Out_channel.stderr; match off with - NoOffset -> (debug_print 2 ("... no offset\n"); flush Pervasives.stderr; false) + NoOffset -> (debug_print 2 ("... no offset\n"); flush Out_channel.stderr; false) | Field(fi, NoOffset) when isTrailingField fi fi.fcomp - -> (debug_print 2 ("... trailing field + no offset\n"); flush Pervasives.stderr; true) + -> (debug_print 2 ("... trailing field + no offset\n"); flush Out_channel.stderr; true) | Field(fi, NoOffset) - -> (debug_print 2 ("... non-trailing no-offset\n"); flush Pervasives.stderr; false) + -> (debug_print 2 ("... non-trailing no-offset\n"); flush Out_channel.stderr; false) | Index(indexEx, maybeOffset) - -> (debug_print 2 ("... index\n"); flush Pervasives.stderr; isTrailingFieldOffsetExpr (arrayElementType ts) maybeOffset) + -> (debug_print 2 ("... index\n"); flush Out_channel.stderr; isTrailingFieldOffsetExpr (arrayElementType ts) maybeOffset) | Field(fi, someOffset) - -> (debug_print 2 ("... residual field case\n"); flush Pervasives.stderr; isTrailingFieldOffsetExpr (typeSig fi.ftype) someOffset) + -> (debug_print 2 ("... residual field case\n"); flush Out_channel.stderr; isTrailingFieldOffsetExpr (typeSig fi.ftype) someOffset) (* (getConcreteType (typeSig fi.ftype)) = (getConcreteType ts) -> @@ -138,7 +138,7 @@ let rec getSizeExpr (ex: exp) (env : (int * sz) list) (gs : Cil.global list) : s *) in let containingTypeSigInTrailingFieldOffsetFromNullPtrExpr lv = begin - debug_print 2 ("Hello from containingTypeSigInTrailingFieldOffsetFromNullPtrExpr(" ^ (Pretty.sprint 80 (Pretty.dprintf "%a" d_lval lv)) ^ ")\n"); flush Pervasives.stderr; + debug_print 2 ("Hello from containingTypeSigInTrailingFieldOffsetFromNullPtrExpr(" ^ (Pretty.sprint 80 (Pretty.dprintf "%a" d_lval lv)) ^ ")\n"); flush Out_channel.stderr; match lv with (* Does it make sense to have complex expressions when doing an offsetof-based size calculation? e.g. @@ -161,18 +161,18 @@ let rec getSizeExpr (ex: exp) (env : (int * sz) list) (gs : Cil.global list) : s Field(d-fieldinfo, NoOffset))))))) *) - (Mem(e), off) -> debug_print 2 ("Saw Mem case\n"); flush Pervasives.stderr; + (Mem(e), off) -> debug_print 2 ("Saw Mem case\n"); flush Out_channel.stderr; if isStaticallyNullPtr e then ( - debug_print 2 ("Saw statically-null case\n"); - flush Pervasives.stderr; + debug_print 2 ("Saw statically-null case\n"); + flush Out_channel.stderr; let targetTs = pointerTargetType (typeSig (typeOf e)) in if isTrailingFieldOffsetExpr targetTs off then Some(targetTs) else None ) - else (debug_print 2 ("Saw non-statically-null case\n"); flush Pervasives.stderr; None) + else (debug_print 2 ("Saw non-statically-null case\n"); flush Out_channel.stderr; None) | _ -> None end in @@ -268,14 +268,14 @@ let rec getSizeExpr (ex: exp) (env : (int * sz) list) (gs : Cil.global list) : s if ci.cstruct && List.length ci.cfields > 0 then let fi = List.nth ci.cfields (List.length ci.cfields - 1) in - let _ = (debug_print 2 ("Hello from field-subtracting (s - f) case in getSizeExpr (s is " ^ (typsigToString ts1) ^ ", f is " ^ (typToString fi.ftype) ^ " )\n"); flush Pervasives.stderr) in + let _ = (debug_print 2 ("Hello from field-subtracting (s - f) case in getSizeExpr (s is " ^ (typsigToString ts1) ^ ", f is " ^ (typToString fi.ftype) ^ " )\n"); flush Out_channel.stderr) in let subtractingLastField = if fi.fbitfield <> None then false else (let tsf = Cil.typeSig fi.ftype in tsMatchModuloSignedness tsf ts2 || (match tsf with - TSArray(tsa, Some(bound), _) when bound = Int64.one -> + TSArray(tsa, Some(bound), _) when bound = cilint_of_int64 Int64.one -> tsMatchModuloSignedness tsa ts2 | ts -> false) ) @@ -308,7 +308,7 @@ let rec getSizeExpr (ex: exp) (env : (int * sz) list) (gs : Cil.global list) : s end | CastE(t, e) -> (getSizeExpr e env gs) (* i.e. recurse down e *) | AddrOf(lv) -> begin - debug_print 2 ("Hello from AddrOf case in getSizeExpr\n"); flush Pervasives.stderr; + debug_print 2 ("Hello from AddrOf case in getSizeExpr\n"); flush Out_channel.stderr; let ts = containingTypeSigInTrailingFieldOffsetFromNullPtrExpr lv in match ts with None -> Undet @@ -329,7 +329,7 @@ let rec getSizeExpr (ex: exp) (env : (int * sz) list) (gs : Cil.global list) : s | Undet -> debug_print 2 "don't know\n" | TooComplex -> debug_print 2 "something too complex\n" ); - flush Pervasives.stderr; + flush Out_channel.stderr; res ) @@ -380,35 +380,35 @@ let matchUserAllocArgs i arglist signature env maybeFunNameToPrint (calledFuncti in let fragment = (* string_after *) (matched_string signature) (* nskip *) in - (debug_print 2 ("Info: signature " ^ signature ^ " did contain a function arg spec (" ^ fragment ^ " a.k.a. signature + "^ (string_of_int nskip) ^")\n"); flush Pervasives.stderr); + (debug_print 2 ("Info: signature " ^ signature ^ " did contain a function arg spec (" ^ fragment ^ " a.k.a. signature + "^ (string_of_int nskip) ^")\n"); flush Out_channel.stderr); fragment ) with Not_found -> ( - (debug_print 0 ("Warning: signature " ^ signature ^ " did not contain an arg spec\n"); flush Pervasives.stderr); + (debug_print 0 ("Warning: signature " ^ signature ^ " did not contain an arg spec\n"); flush Out_channel.stderr); "" ) in let sizeArgPos = if string_match (regexp "[^A-Z]*[A-Z]") signatureArgSpec 0 then Some((String.length (matched_string signatureArgSpec)) - 1 (* for the bracket*) - 1 (* because we want zero-based *)) - else (debug_print 0 ("Warning: signature " ^ signature ^ " did not contain a capitalized arg spec element\n"); flush Pervasives.stderr; None) + else (debug_print 0 ("Warning: signature " ^ signature ^ " did not contain a capitalized arg spec element\n"); flush Out_channel.stderr; None) in match sizeArgPos with Some(s) -> if (length arglist) > s then let szEx = - (debug_print 2 ("Looking at arg expression number " ^ (string_of_int s) ^ "\n"); flush Pervasives.stderr); + (debug_print 2 ("Looking at arg expression number " ^ (string_of_int s) ^ "\n"); flush Out_channel.stderr); getSizeExpr (nth arglist s) env gs in match szEx with - Existing(szType, _) -> (debug_print 2 ("Inferred that we are allocating some number of " ^ (Pretty.sprint 80 (Pretty.dprintf "\t%a\t" d_typsig szType)) ^ "\n"); flush Pervasives.stderr ); + Existing(szType, _) -> (debug_print 2 ("Inferred that we are allocating some number of " ^ (Pretty.sprint 80 (Pretty.dprintf "\t%a\t" d_typsig szType)) ^ "\n"); flush Out_channel.stderr ); szEx - | Undet | TooComplex -> debug_print 1 ("Could not infer what we are allocating\n"); flush Pervasives.stderr; szEx - | Synthetic(_) -> debug_print 1 ("We are allocating a composite: FIXME print this out\n"); flush Pervasives.stderr; szEx + | Undet | TooComplex -> debug_print 1 ("Could not infer what we are allocating\n"); flush Out_channel.stderr; szEx + | Synthetic(_) -> debug_print 1 ("We are allocating a composite: FIXME print this out\n"); flush Out_channel.stderr; szEx else (match maybeFunNameToPrint with Some(fnname) -> ((debug_print 0 ("Warning: signature " ^ signature ^ " wrongly predicts allocation function " ^ fnname ^ " will have at least " ^ (string_of_int s) ^ " arguments, where call site it has only " ^ (string_of_int (length arglist)) ^"\n"); - flush Pervasives.stderr); Undet) + flush Out_channel.stderr); Undet) | None -> (debug_print 0 ("Warning: spec argument count (" ^ (string_of_int s) ^ ") does not match call-site argument count (" ^ (string_of_int (length arglist)) ^ ")")); Undet) | None -> (* If we have no sizearg pos, use the return type of the function: @@ -455,11 +455,11 @@ let functionNameMatchesSignature fname signature = in match friendlyName with Some(s) -> - (debug_print 2 ("Info: signature " ^ signature ^ " did contain a function name: " ^ s ^ "\n"); - flush Pervasives.stderr; + (debug_print 2 ("Info: signature " ^ signature ^ " did contain a function name: " ^ s ^ "\n"); + flush Out_channel.stderr; fname = s ) | None -> (debug_print 2 ("Warning: signature " ^ signature ^ " did not contain a function name\n"); - flush Pervasives.stderr; false ) + flush Out_channel.stderr; false ) let functionArgCountMatchesSignature arglist signature = let (friendlyName, friendlyArgChars) = parseSignature signature @@ -471,7 +471,7 @@ let rec extractUserAllocMatchingSignature i maybeFunName arglist signature env ( (* destruct the signature string *) debug_print 2 ("Warning: matching against signature " ^ signature ^ " when argcount is " ^ (string_of_int (List.length arglist)) ^ "\n"); - flush Pervasives.stderr; + flush Out_channel.stderr; match maybeFunName with Some(fname) when functionNameMatchesSignature fname signature @@ -607,8 +607,8 @@ let rec accumulateOverStatements acc (stmts: Cil.stmt list) (gs : Cil.global lis Let's try this. *) let rec accumulateOverOneInstr acc i = (* debug_print 2 "hello from accumulateOverOneInstr\n"; flush Pervasives.stderr; *) match i with - Call(_, f, args, l) -> acc - | Set((host, off), e, l) -> begin + Call(_, f, args, l, _) -> acc + | Set((host, off), e, l, _) -> begin match host with Var(v) -> if v.vglob then acc else begin let szness = getSizeExpr e acc gs in @@ -616,12 +616,13 @@ let rec accumulateOverStatements acc (stmts: Cil.stmt list) (gs : Cil.global lis Undet -> acc | _ -> ( debug_print 2 ("found some sizeofness in assignment to: " ^ (Pretty.sprint 80 (Pretty.dprintf "\t%a\t" d_lval (host, off))) ^ " (vid " ^ (string_of_int v.vid) ^ ", sizeofness " ^ (sizeofnessToString szness) ^ ")\n"); - flush Pervasives.stderr; + flush Out_channel.stderr; (v.vid, szness) :: (remove_assoc v.vid acc)) end | Mem(e) -> acc end | Asm(_, _, _, _, _, l) -> acc + | VarDecl(_, l) -> acc in let rec accumulateOverInstrs acc instrs = (* debug_print 2 "hello from accumulateOverInstrs\n"; flush Pervasives.stderr; *) @@ -642,12 +643,9 @@ let rec accumulateOverStatements acc (stmts: Cil.stmt list) (gs : Cil.global lis | Continue (l : location) -> *) | Block(b) -> (* recurse over the block's stmts *) accumulateOverStatements acc b.bstmts gs - | If (e, b1, b2, l) -> accumulateOverStatements (accumulateOverStatements acc b2.bstmts gs) b1.bstmts gs - | Switch (e, b, ss, l) -> accumulateOverStatements (accumulateOverStatements acc ss gs) b.bstmts gs - | Loop (b, l, continueLabel, breakLabel) -> accumulateOverStatements acc b.bstmts gs - | TryFinally (tryBlock, finallyBlock, l) -> accumulateOverStatements (accumulateOverStatements acc tryBlock.bstmts gs) finallyBlock.bstmts gs - | TryExcept (tryBlock, _, exceptBlock, l) - -> accumulateOverStatements (accumulateOverStatements acc tryBlock.bstmts gs) exceptBlock.bstmts gs (* FIXME: instr list doesn't get handled*) + | If (e, b1, b2, l, _) -> accumulateOverStatements (accumulateOverStatements acc b2.bstmts gs) b1.bstmts gs + | Switch (e, b, ss, l, _) -> accumulateOverStatements (accumulateOverStatements acc ss gs) b.bstmts gs + | Loop (b, l, _, continueLabel, breakLabel) -> accumulateOverStatements acc b.bstmts gs | _ -> acc in match stmts with @@ -685,7 +683,7 @@ class dumpAllocsVisitor = fun (fl: Cil.file) -> object(self) (* debug_print 2 ("printing alloc for " ^ fileAndLine ^ ", funvar " ^ funvar.vname ^ "\n"); *) let chan = match !outChannel with | Some(s) -> s - | None -> Pervasives.stderr + | None -> Out_channel.stderr in let targetFunc = match maybeFunvar with Some(funvar) -> Pretty.sprint 80 (* I so do not understand Pretty.dprintf *) @@ -767,12 +765,13 @@ class dumpAllocsVisitor = fun (fl: Cil.file) -> object(self) method vinst (i: instr) : instr list visitAction = ( debug_print 2 ("considering instruction " ^ ( match i with - Call(_, _, _, l) -> "(call) at " ^ l.file ^ ", line: " ^ (string_of_int l.line) - | Set(_, _, l) -> "(assignment) at " ^ l.file ^ ", line: " ^ (string_of_int l.line) + Call(_, _, _, l, _) -> "(call) at " ^ l.file ^ ", line: " ^ (string_of_int l.line) + | Set(_, _, l, _) -> "(assignment) at " ^ l.file ^ ", line: " ^ (string_of_int l.line) | Asm(_, _, _, _, _, l) -> "(assembly) at " ^ l.file ^ ", line: " ^ (string_of_int l.line) - ) ^ "\n"); flush Pervasives.stderr); + | VarDecl(_, l) -> "(vardecl) at " ^ l.file ^ ", line: " ^ (string_of_int l.line) + ) ^ "\n"); flush Out_channel.stderr); match i with - Call(_, funExpr, args, l) -> begin + Call(_, funExpr, args, l, _) -> begin let handleCall maybeFunvar (functionT : Cil.typ) = begin let functionTs = typeSig functionT in match functionTs with @@ -849,8 +848,9 @@ class dumpAllocsVisitor = fun (fl: Cil.file) -> object(self) | _ (* match f *) -> (debug_print 2 ("skipping call to non-lvalue at " ^ l.file ^ ":" ^ (string_of_int l.line) ^ "\n"); flush Pervasives.stderr; SkipChildren) *) end - | Set(lv, e, l) -> (* (debug_print 2 ("skipping assignment at " ^ l.file ^ ":" ^ (string_of_int l.line) ^ "\n" ); flush Pervasives.stderr; *) SkipChildren (* ) *) + | Set(lv, e, l, _) -> (* (debug_print 2 ("skipping assignment at " ^ l.file ^ ":" ^ (string_of_int l.line) ^ "\n" ); flush Pervasives.stderr; *) SkipChildren (* ) *) | Asm(_, _, _, _, _, l) -> (* (debug_print 2 ("skipping assignment at " ^ l.file ^ ":" ^ (string_of_int l.line) ^ "\n" ); *) SkipChildren (* ) *) + | VarDecl(_, l) -> SkipChildren (* ) *) end (* class dumpAllocsVisitor *) diff --git a/tools/lang/c/dumpmemacc/dumpmemacc.ml b/tools/lang/c/dumpmemacc/dumpmemacc.ml index 5bceb49c8..e370f15fb 100644 --- a/tools/lang/c/dumpmemacc/dumpmemacc.ml +++ b/tools/lang/c/dumpmemacc/dumpmemacc.ml @@ -16,7 +16,7 @@ class dumpMemAccVisitor = fun (fl: Cil.file) -> object(self) method doReport (direction : string) (kind: string) (exprT : Cil.typ) (enclosingT : Cil.typ) : unit = let chan = match !outChannel with Some(c) -> c - | None -> Pervasives.stderr + | None -> Out_channel.stderr in let loc = match !currentLoc with Some(l) -> l @@ -117,7 +117,7 @@ class dumpMemAccVisitor = fun (fl: Cil.file) -> object(self) method vinst (outerI: instr) : instr list visitAction = ChangeDoChildrenPost([outerI], fun is -> match is with - [Call(maybeOut, funExpr, args, l)] -> ( + [Call(maybeOut, funExpr, args, l, _)] -> ( currentLoc := Some(l); (match maybeOut with Some(lv) -> self#reportWrite lv @@ -126,7 +126,7 @@ class dumpMemAccVisitor = fun (fl: Cil.file) -> object(self) let _ = List.mapi (fun idx -> (fun subE -> (self#reportVirtualWrite subE))) args in (); is ) - | [Set(lv, e, l)] -> + | [Set(lv, e, l, _)] -> currentLoc := Some(l); self#reportVirtualWrite e; self#reportWrite lv; diff --git a/tools/lang/c/monalloca/monalloca.ml b/tools/lang/c/monalloca/monalloca.ml index 65e7168f1..37fb2faf1 100644 --- a/tools/lang/c/monalloca/monalloca.ml +++ b/tools/lang/c/monalloca/monalloca.ml @@ -91,7 +91,7 @@ let ensureCleanupLocal (fn : fundec) = (* trying to initialize this right here, by adding to fn.sbody.bstmts, doesn't work -- likely because it gets clobbered by the visitor code. So we do it when visiting the function instead. *) - fn.sbody.bstmts <- (mkStmtOneInstr (Set((Var(v), NoOffset), zero, v.vdecl))) + fn.sbody.bstmts <- (mkStmtOneInstr (Set((Var(v), NoOffset), zero, v.vdecl, v.vdecl))) :: fn.sbody.bstmts; v @@ -114,7 +114,7 @@ class monAllocaExprVisitor = fun (fl: Cil.file) | _ -> false in match i with - Call(tgt, funExpr, [sizeArg], l) when isAllocaFun funExpr -> begin + Call(tgt, funExpr, [sizeArg], l, _) when isAllocaFun funExpr -> begin (* We need to * - ensure we have a local in the function for recording the fact that this frame does alloca @@ -156,7 +156,7 @@ class monAllocaExprVisitor = fun (fl: Cil.file) ChangeTo([ Call(Some(Var(fixedSizeVar), NoOffset), Lval(Var(liballocsAllocaSizeFun.svar), NoOffset), - [sizeArg], l); + [sizeArg], l, l); Asm([(* attrs *)], [(* template strings *) " call "^ labelString1 ^"_%=\n\ @@ -170,14 +170,14 @@ class monAllocaExprVisitor = fun (fl: Cil.file) [(* clobbers *)], (* location *) l ); Call(Some(Var(tempPtrVar), NoOffset), Lval(Var(builtinAllocaFunVar), NoOffset), - [Lval(Var(fixedSizeVar), NoOffset)], l); + [Lval(Var(fixedSizeVar), NoOffset)], l, l); Call(tgt, Lval(Var(liballocsNotifyAndAdjustAllocaFun.svar), NoOffset), [Lval(Var(tempPtrVar), NoOffset); sizeArg; Lval(Var(fixedSizeVar), NoOffset); mkAddrOf (Var(counterVar), NoOffset); Lval(Var(callSiteVar), NoOffset) - ], l) + ], l, l) ]) end | _ -> SkipChildren @@ -236,7 +236,7 @@ class monAllocaFunVisitor = fun (fl: Cil.file) -> object(self) None -> ChangeTo(modifiedFunDec) | Some(v) -> modifiedFunDec.sbody.bstmts <- - (mkStmtOneInstr (Set((Var(v), NoOffset), zero, v.vdecl))) :: modifiedFunDec.sbody.bstmts; + (mkStmtOneInstr (Set((Var(v), NoOffset), zero, v.vdecl, v.vdecl))) :: modifiedFunDec.sbody.bstmts; ChangeTo(modifiedFunDec) end (* class monAllocaFunVisitor *) diff --git a/tools/lang/c/trapptrwrites/trapptrwrites.ml b/tools/lang/c/trapptrwrites/trapptrwrites.ml index 05d901a34..8c882e414 100644 --- a/tools/lang/c/trapptrwrites/trapptrwrites.ml +++ b/tools/lang/c/trapptrwrites/trapptrwrites.ml @@ -89,7 +89,7 @@ let trapPtrWrites file = match unrollType (typeOfLval lv) with | TPtr _ | TFun _ -> Call (None, Lval (var notifyPtrWriteFun), - [ mkCast (mkAddrOf lv) constVoidPtrPtrType ; Lval rv ], loc) :: tail + [ mkCast (mkAddrOf lv) constVoidPtrPtrType ; Lval rv ], loc, loc) :: tail | TComp (c, _) -> (* treat unions as structs, might not be a good idea... *) List.fold_left (fun acc field -> let flv = addOffsetLval (Field(field, NoOffset)) lv in @@ -101,31 +101,31 @@ let trapPtrWrites file = Call (None, Lval (var notifyCopyFun), [ mkAddrOf lv ; StartOf rv ; BinOp (Mult, length_exp, SizeOf eltyp, !upointType) ], - loc) :: tail + loc, loc) :: tail | _ -> tail in match i with - | Set (lv, _, _) | Call (Some lv, _, _, _) when not (lvNeedTrapCalls lv) -> + | Set (lv, _, _, _) | Call (Some lv, _, _, _, _) when not (lvNeedTrapCalls lv) -> SkipChildren - | Set(lv, Lval rv, l) -> - ChangeTo (addTrapCallsForLval lv rv l [Set(lv, Lval rv, l)]) - | Set(lv, e, l) -> + | Set(lv, Lval rv, l, _) -> + ChangeTo (addTrapCallsForLval lv rv l [Set(lv, Lval rv, l, l)]) + | Set(lv, e, l, _) -> let curFunc = match curFunc with | Some f -> f | None -> assert false in let tmpvar = var (makeTempVar curFunc (typeOfLval lv)) in - ChangeTo (Set(tmpvar, e, l) :: - addTrapCallsForLval lv tmpvar l [Set(lv, Lval tmpvar, l)]) - | Call(Some lv, f, args, l) -> + ChangeTo (Set(tmpvar, e, l, l) :: + addTrapCallsForLval lv tmpvar l [Set(lv, Lval tmpvar, l, l)]) + | Call(Some lv, f, args, l, _) -> let curFunc = match curFunc with | Some f -> f | None -> assert false in let tmpvar = var (makeTempVar curFunc (typeOfLval lv)) in - ChangeTo (Call(Some tmpvar, f, args, l) :: - addTrapCallsForLval lv tmpvar l [Set(lv, Lval tmpvar, l)]) + ChangeTo (Call(Some tmpvar, f, args, l, l) :: + addTrapCallsForLval lv tmpvar l [Set(lv, Lval tmpvar, l, l)]) | _ -> SkipChildren end in