From 387ef518f995d7bd0254b3cf70c143eab891b10a Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Mon, 16 Dec 2019 00:59:14 -0800 Subject: [PATCH] [inferbo] Revert external relational domains (apron, elina) Summary: Inferbo does not use the external relational domains, apron and elina. At some point, the parts of inferbo using them were broken and they do not seem to be fixed easily in the near future. Let's remove them and keep the code base cleaner. Reviewed By: jvillard Differential Revision: D19022905 fbshipit-source-id: e0eafe79f --- INSTALL.md | 3 +- Makefile | 67 - Makefile.autoconf.in | 4 - configure.ac | 9 - infer/man/man1/infer-analyze.txt | 4 - infer/man/man1/infer-full.txt | 7 - infer/man/man1/infer.txt | 4 - infer/src/base/Config.ml | 9 - infer/src/base/Config.mli | 2 - infer/src/bufferoverrun/absLoc.ml | 4 - infer/src/bufferoverrun/absLoc.mli | 4 - .../bufferoverrun/bufferOverrunAnalysis.ml | 62 +- .../bufferoverrun/bufferOverrunAnalysis.mli | 6 - .../src/bufferoverrun/bufferOverrunChecker.ml | 57 +- .../src/bufferoverrun/bufferOverrunDomain.ml | 161 +- .../bufferOverrunDomainRelation.ml | 1601 ----------------- .../src/bufferoverrun/bufferOverrunModels.ml | 29 +- .../bufferOverrunProofObligations.ml | 94 +- .../bufferOverrunProofObligations.mli | 8 +- .../bufferoverrun/bufferOverrunSemantics.ml | 133 +- infer/src/bufferoverrun/bufferOverrunUtils.ml | 50 +- .../src/bufferoverrun/bufferOverrunUtils.mli | 3 - infer/src/dune.common.in | 3 - opam | 4 - opam.locked | 5 - scripts/create_binary_release.sh | 2 +- scripts/set_libso_path.sh | 30 - 27 files changed, 84 insertions(+), 2281 deletions(-) delete mode 100644 infer/src/bufferoverrun/bufferOverrunDomainRelation.ml delete mode 100755 scripts/set_libso_path.sh diff --git a/INSTALL.md b/INSTALL.md index fb202c09d..d438565cb 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -25,13 +25,12 @@ is required to compile everything from source. - Xcode >= 6.1 (only needed for the C/Objective-C analysis) - autoconf >= 2.63 and automake >= 1.11.1 (if building from git) - gmp -- mpfr You can install some of these dependencies using [Homebrew](http://brew.sh/): ```sh -brew install autoconf automake cmake opam pkg-config sqlite gmp mpfr +brew install autoconf automake cmake opam pkg-config sqlite gmp brew cask install java ``` diff --git a/Makefile b/Makefile index 542dc228b..ea0906a47 100644 --- a/Makefile +++ b/Makefile @@ -695,73 +695,6 @@ else endif endif -# install dynamic libraries -# use this if you want to distribute infer binaries -install-with-libs: install - test -d '$(DESTDIR)$(libdir)'/infer/infer/libso || \ - $(MKDIR_P) '$(DESTDIR)$(libdir)'/infer/infer/libso -ifneq ($(OPAM),no) - set -x; \ - OPAM_SHARE=$$($(OPAM) config var share); \ - APRON_LIB_PATHS="$$OPAM_SHARE/apron/lib/libapron.so $$OPAM_SHARE/apron/lib/liboctMPQ.so"; \ - ELINA_LIB_PATHS="$$OPAM_SHARE/elina/lib/libelinalinearize.so $$OPAM_SHARE/elina/lib/liboptpoly.so $$OPAM_SHARE/elina/lib/libpartitions.so"; \ - $(INSTALL_PROGRAM) -C $$APRON_LIB_PATHS '$(DESTDIR)$(libdir)'/infer/infer/libso/; \ - $(INSTALL_PROGRAM) -C $$ELINA_LIB_PATHS '$(DESTDIR)$(libdir)'/infer/infer/libso/ -ifneq ($(LDD),no) -ifneq ($(PATCHELF),no) -# this sort of assumes Linux -# figure out where libgmp and libmpfr are using ldd - set -x; \ - for lib in $$($(LDD) $(INFER_BIN) \ - | cut -d ' ' -f 3 \ - | grep -e 'lib\(gmp\|mpfr\)'); do \ - $(INSTALL_PROGRAM) -C "$$lib" '$(DESTDIR)$(libdir)'/infer/infer/libso/; \ - done -# update rpath of executables - for sofile in '$(DESTDIR)$(libdir)'/infer/infer/libso/*.so; do \ - $(PATCHELF) --set-rpath '$$ORIGIN' --force-rpath "$$sofile"; \ - done - $(PATCHELF) --set-rpath '$$ORIGIN/../libso' --force-rpath '$(DESTDIR)$(libdir)'/infer/infer/bin/infer -ifeq ($(IS_FACEBOOK_TREE),yes) - $(PATCHELF) --set-rpath '$$ORIGIN/../libso' --force-rpath '$(DESTDIR)$(libdir)'/infer/infer/bin/InferCreateTraceViewLinks -endif -else # ldd found but not patchelf - echo "ERROR: ldd (Linux?) found but not patchelf, please install patchelf" >&2; exit 1 -endif -else # ldd not found -ifneq ($(OTOOL),no) -ifneq ($(INSTALL_NAME_TOOL),no) -# this sort of assumes osx -# figure out where libgmp and libmpfr are using otool - set -e; \ - set -x; \ - for lib in $$($(OTOOL) -L $(INFER_BIN) \ - | cut -d ' ' -f 1 | tr -d '\t' \ - | grep -e 'lib\(gmp\|mpfr\)'); do \ - $(INSTALL_PROGRAM) -C "$$lib" '$(DESTDIR)$(libdir)'/infer/infer/libso/; \ - done - set -x; \ - for sofile in '$(DESTDIR)$(libdir)'/infer/infer/libso/*.{so,dylib}; do \ - $(INSTALL_NAME_TOOL) -add_rpath "@executable_path" "$$sofile" 2> /dev/null || true; \ - scripts/set_libso_path.sh '$(DESTDIR)$(libdir)'/infer/infer/libso "$$sofile"; \ - done - $(INSTALL_NAME_TOOL) -add_rpath '@executable_path/../libso' '$(DESTDIR)$(libdir)'/infer/infer/bin/infer 2> /dev/null || true - scripts/set_libso_path.sh '$(DESTDIR)$(libdir)'/infer/infer/libso '$(DESTDIR)$(libdir)'/infer/infer/bin/infer -ifeq ($(IS_FACEBOOK_TREE),yes) - $(INSTALL_NAME_TOOL) -add_rpath '@executable_path/../libso' '$(DESTDIR)$(libdir)'/infer/infer/bin/InferCreateTraceViewLinks 2> /dev/null || true - scripts/set_libso_path.sh '$(DESTDIR)$(libdir)'/infer/infer/libso '$(DESTDIR)$(libdir)'/infer/infer/bin/InferCreateTraceViewLinks -endif -else # install_name_tool not found - echo "ERROR: otool (OSX?) found but not install_name_tool, please install install_name_tool" >&2; exit 1 -endif -else # otool not found - echo "ERROR: need ldd + patchelf (Linux) or otool + install_name_tool (OSX) available" >&2; exit 1 -endif -endif # ldd -else # opam - echo "ERROR: need opam" >&2; exit 1 -endif - # Nuke objects built from OCaml. Useful when changing the OCaml compiler, for instance. .PHONY: ocaml_clean ocaml_clean: diff --git a/Makefile.autoconf.in b/Makefile.autoconf.in index 4b9dea773..8f9b445b8 100644 --- a/Makefile.autoconf.in +++ b/Makefile.autoconf.in @@ -36,13 +36,11 @@ INFER_MINOR = @INFER_MINOR@ INFER_PATCH = @INFER_PATCH@ INSTALL = @INSTALL@ INSTALL_DATA = @INSTALL_DATA@ -INSTALL_NAME_TOOL = @INSTALL_NAME_TOOL@ INSTALL_PROGRAM = @INSTALL_PROGRAM@ IS_FACEBOOK_TREE = @IS_FACEBOOK_TREE@ IS_RELEASE_TREE = @IS_RELEASE_TREE@ JAVA_MAJOR_VERSION = @JAVA_MAJOR_VERSION@ JAVAC = @JAVAC@ -LDD = @LDD@ LDFLAGS = @LDFLAGS@ libdir = @libdir@ # override in your `make` command to make the install relocatable @@ -68,8 +66,6 @@ OCAMLOPT = @OCAMLOPT@ OPAM = @OPAM@ OPAMROOT = @OPAMROOT@ OPAMSWITCH = @OPAMSWITCH@ -OTOOL = @OTOOL@ -PATCHELF = @PATCHELF@ PATH = @PATH@ prefix = @prefix@ PYTHON_lxml = @PYTHON_lxml@ diff --git a/configure.ac b/configure.ac index 44d37b639..176c32e58 100644 --- a/configure.ac +++ b/configure.ac @@ -400,15 +400,6 @@ AC_SUBST([GNU_SED]) AC_CHECK_TOOL([BREW], [brew], [no]) -AC_CHECK_TOOL([INSTALL_NAME_TOOL], [install_name_tool], [no]) -AC_SUBST([INSTALL_NAME_TOOL]) -AC_CHECK_TOOL([LDD], [ldd], [no]) -AC_SUBST([LDD]) -AC_CHECK_TOOL([OTOOL], [otool], [no]) -AC_SUBST([OTOOL]) -AC_CHECK_TOOL([PATCHELF], [patchelf], [no]) -AC_SUBST([PATCHELF]) - AC_CHECK_INFER_MAN_LAST_MODIFIED() AC_CONFIG_FILES([ diff --git a/infer/man/man1/infer-analyze.txt b/infer/man/man1/infer-analyze.txt index 2ac1d1add..e72316481 100644 --- a/infer/man/man1/infer-analyze.txt +++ b/infer/man/man1/infer-analyze.txt @@ -356,10 +356,6 @@ BUCK FLAVORS OPTIONS BUFFER OVERRUN OPTIONS --bo-debug int Debug level for buffer-overrun checker (0-4) - - --bo-relational-domain { oct | poly } - Select a relational domain being used in the bufferoverrun checker - (experimental) CLANG OPTIONS --annotation-reachability-cxx json Specify annotation reachability analyses to be performed on diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 18a770d8d..e109ea5f8 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -129,10 +129,6 @@ OPTIONS --bo-debug int Debug level for buffer-overrun checker (0-4) See also infer-analyze(1). - --bo-relational-domain { oct | poly } - Select a relational domain being used in the bufferoverrun checker - (experimental) See also infer-analyze(1). - --bootclasspath string Specify the Java bootclasspath See also infer-capture(1). @@ -1188,9 +1184,6 @@ INTERNAL OPTIONS Activates: Mode for analyzing the biabduction models (Conversely: --no-biabduction-models-mode) - --bo-relational-domain-reset - Cancel the effect of --bo-relational-domain. - --bootclasspath-reset Cancel the effect of --bootclasspath. diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index e2cd59d15..08fce1113 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -129,10 +129,6 @@ OPTIONS --bo-debug int Debug level for buffer-overrun checker (0-4) See also infer-analyze(1). - --bo-relational-domain { oct | poly } - Select a relational domain being used in the bufferoverrun checker - (experimental) See also infer-analyze(1). - --bootclasspath string Specify the Java bootclasspath See also infer-capture(1). diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 0096cc296..a7d181c42 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -851,13 +851,6 @@ and biabduction_model_free_pattern = "Regex of methods that should be modelled as free if definition is missing" -and bo_relational_domain = - CLOpt.mk_symbol_opt ~long:"bo-relational-domain" - ~in_help:InferCommand.[(Analyze, manual_buffer_overrun)] - ~symbols:[("oct", `Bo_relational_domain_oct); ("poly", `Bo_relational_domain_poly)] - "Select a relational domain being used in the bufferoverrun checker (experimental)" - - and bootclasspath = CLOpt.mk_string_opt ~long:"bootclasspath" ~in_help:InferCommand.[(Capture, manual_java)] @@ -2756,8 +2749,6 @@ and bootclasspath = !bootclasspath and bo_debug = !bo_debug -and bo_relational_domain = !bo_relational_domain - and buck = !buck and buck_blacklist = !buck_blacklist diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 4895dc4bb..e6e7010c4 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -233,8 +233,6 @@ val biabduction_models_mode : bool val bo_debug : int -val bo_relational_domain : [`Bo_relational_domain_oct | `Bo_relational_domain_poly] option - val bootclasspath : string option val buck : bool diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml index c9addeed8..fdc14c9ce 100644 --- a/infer/src/bufferoverrun/absLoc.ml +++ b/infer/src/bufferoverrun/absLoc.ml @@ -65,8 +65,6 @@ module Allocsite = struct let is_unknown = function Unknown -> true | Symbol _ | Known _ | LiteralString _ -> false - let to_string x = F.asprintf "%a" pp x - let make : Typ.Procname.t -> node_hash:int @@ -243,8 +241,6 @@ module Loc = struct let pp = pp_paren ~paren:false - let to_string x = F.asprintf "%a" pp x - let is_var = function Var _ -> true | _ -> false let is_c_strlen = function diff --git a/infer/src/bufferoverrun/absLoc.mli b/infer/src/bufferoverrun/absLoc.mli index a5eb4d955..25e8673e8 100644 --- a/infer/src/bufferoverrun/absLoc.mli +++ b/infer/src/bufferoverrun/absLoc.mli @@ -22,8 +22,6 @@ module Allocsite : sig include PrettyPrintable.PrintableOrderedType with type t := t - val to_string : t -> string - val unknown : t val make : @@ -59,8 +57,6 @@ module Loc : sig include PrettyPrintable.PrintableOrderedType with type t := t - val to_string : t -> string - val of_allocsite : Allocsite.t -> t val of_c_strlen : t -> t diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index b29176cf8..35a90fa85 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -137,12 +137,6 @@ module TransferFunctions = struct |> instantiate_latest_prune ~ret_id ~callee_exit_mem eval_sym_trace location - let forget_ret_relation ret callee_pname mem = - let ret_loc = Loc.of_pvar (Pvar.get_ret_pvar callee_pname) in - let ret_var = Loc.of_var (Var.of_id (fst ret)) in - Dom.Mem.relation_forget_locs (PowLoc.add ret_loc (PowLoc.singleton ret_var)) mem - - let is_external pname = match pname with | Typ.Procname.Java java_pname -> @@ -160,8 +154,7 @@ module TransferFunctions = struct let instantiate_mem : - Tenv.t - -> Typ.IntegerWidths.t + Typ.IntegerWidths.t -> Ident.t * Typ.t -> (Pvar.t * Typ.t) list -> Typ.Procname.t @@ -170,23 +163,14 @@ module TransferFunctions = struct -> BufferOverrunAnalysisSummary.t -> Location.t -> Dom.Mem.t = - fun tenv integer_type_widths ret callee_formals callee_pname params caller_mem callee_exit_mem + fun integer_type_widths ret callee_formals callee_pname params caller_mem callee_exit_mem location -> let eval_sym_trace = Sem.mk_eval_sym_trace integer_type_widths callee_formals params caller_mem ~mode:Sem.EvalNormal in - let caller_mem' = - instantiate_mem_reachable ret callee_formals callee_pname ~callee_exit_mem eval_sym_trace - caller_mem location - |> forget_ret_relation ret callee_pname - in - Option.value_map Config.bo_relational_domain ~default:caller_mem' ~f:(fun _ -> - let rel_subst_map = - Sem.get_subst_map tenv integer_type_widths callee_formals params caller_mem - callee_exit_mem - in - Dom.Mem.instantiate_relation rel_subst_map ~caller:caller_mem' ~callee:callee_exit_mem ) + instantiate_mem_reachable ret callee_formals callee_pname ~callee_exit_mem eval_sym_trace + caller_mem location let rec is_array_access_exp = function @@ -331,16 +315,6 @@ module TransferFunctions = struct let v = Sem.eval integer_type_widths exp2 mem |> Dom.Val.add_assign_trace_elem location locs in - let mem = - let sym_exps = - Dom.Relation.SymExp.of_exps - ~get_int_sym_f:(Sem.get_sym_f integer_type_widths mem) - ~get_offset_sym_f:(Sem.get_offset_sym_f integer_type_widths mem) - ~get_size_sym_f:(Sem.get_size_sym_f integer_type_widths mem) - exp2 - in - Dom.Mem.store_relation locs sym_exps mem - in let mem = Dom.Mem.update_mem locs v mem in let mem = if Language.curr_language_is Clang && Typ.is_char typ then @@ -378,7 +352,7 @@ module TransferFunctions = struct | None -> ( match get_proc_summary_and_formals callee_pname with | Some (callee_exit_mem, callee_formals) -> - instantiate_mem tenv integer_type_widths ret callee_formals callee_pname params mem + instantiate_mem integer_type_widths ret callee_formals callee_pname params mem callee_exit_mem location | None -> (* This may happen for procedures with a biabduction model too. *) @@ -417,8 +391,6 @@ module Analyzer = AbstractInterpreter.MakeWTO (TransferFunctions) type invariant_map = Analyzer.invariant_map -type local_decls = PowLoc.t - type memory_summary = BufferOverrunAnalysisSummary.t let extract_pre = Analyzer.extract_pre @@ -427,17 +399,6 @@ let extract_post = Analyzer.extract_post let extract_state = Analyzer.extract_state -let get_local_decls : Procdesc.t -> local_decls = - fun proc_desc -> - let proc_name = Procdesc.get_proc_name proc_desc in - let accum_local_decls acc {ProcAttributes.name} = - let pvar = Pvar.mk name proc_name in - let loc = Loc.of_pvar pvar in - PowLoc.add loc acc - in - Procdesc.get_locals proc_desc |> List.fold ~init:PowLoc.empty ~f:accum_local_decls - - let compute_invariant_map : Summary.t -> Tenv.t -> Typ.IntegerWidths.t -> get_proc_summary_and_formals -> invariant_map = fun summary tenv integer_type_widths get_proc_summary_and_formals -> @@ -484,16 +445,12 @@ let cached_compute_invariant_map = inv_map -let compute_summary : - local_decls -> (Pvar.t * Typ.t) list -> CFG.t -> invariant_map -> memory_summary = - fun locals formals cfg inv_map -> +let compute_summary : (Pvar.t * Typ.t) list -> CFG.t -> invariant_map -> memory_summary = + fun formals cfg inv_map -> let exit_node_id = CFG.exit_node cfg |> CFG.Node.id in match extract_post exit_node_id inv_map with | Some exit_mem -> - exit_mem - |> Dom.Mem.forget_unreachable_locs ~formals - |> Dom.Mem.relation_forget_locs locals - |> Dom.Mem.unset_oenv + exit_mem |> Dom.Mem.forget_unreachable_locs ~formals |> Dom.Mem.unset_oenv | None -> Bottom @@ -505,8 +462,7 @@ let do_analysis : Callbacks.proc_callback_args -> Summary.t = let tenv = Exe_env.get_tenv exe_env proc_name in let integer_type_widths = Exe_env.get_integer_type_widths exe_env proc_name in let inv_map = cached_compute_invariant_map summary tenv integer_type_widths in - let locals = get_local_decls proc_desc in let formals = Procdesc.get_pvar_formals proc_desc in let cfg = CFG.from_pdesc proc_desc in - let payload = compute_summary locals formals cfg inv_map in + let payload = compute_summary formals cfg inv_map in Payload.update_summary payload summary diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.mli b/infer/src/bufferoverrun/bufferOverrunAnalysis.mli index 7ccf5b0e4..d79cabf5f 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.mli +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.mli @@ -8,12 +8,8 @@ open! IStd module CFG = ProcCfg.NormalOneInstrPerNode -module Payload : SummaryPayload.S with type t = BufferOverrunAnalysisSummary.t - type invariant_map -type local_decls = AbsLoc.PowLoc.t - val cached_compute_invariant_map : Summary.t -> Tenv.t -> Typ.IntegerWidths.t -> invariant_map val extract_pre : CFG.Node.id -> invariant_map -> BufferOverrunDomain.Mem.t option @@ -23,6 +19,4 @@ val extract_post : CFG.Node.id -> invariant_map -> BufferOverrunDomain.Mem.t opt val extract_state : CFG.Node.id -> invariant_map -> BufferOverrunDomain.Mem.t AbstractInterpreter.State.t option -val get_local_decls : Procdesc.t -> local_decls - val do_analysis : Callbacks.proc_callback_t diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index e987ee0d3..ca9bb412a 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -16,7 +16,6 @@ module F = Format module L = Logging module Models = BufferOverrunModels module PO = BufferOverrunProofObligations -module Relation = BufferOverrunDomainRelation module Sem = BufferOverrunSemantics module Trace = BufferOverrunTrace @@ -133,11 +132,8 @@ let check_binop_array_access : fun integer_type_widths ~is_plus ~e1 ~e2 location mem cond_set -> let arr = Sem.eval integer_type_widths e1 mem in let idx = Sem.eval integer_type_widths e2 mem in - let idx_sym_exp = Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f integer_type_widths mem) e2 in - let relation = Dom.Mem.get_relation mem in let latest_prune = Dom.Mem.get_latest_prune mem in - BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus ~last_included:false - ~latest_prune location cond_set + BoUtils.Check.array_access ~arr ~idx ~is_plus ~last_included:false ~latest_prune location cond_set let check_binop : @@ -189,11 +185,10 @@ let check_expr_for_array_access : match exp with | Exp.Var _ -> let arr = Sem.eval integer_type_widths exp mem in - let idx, idx_sym_exp = (Dom.Val.Itv.zero, Some Relation.SymExp.zero) in - let relation = Dom.Mem.get_relation mem in + let idx = Dom.Val.Itv.zero in let latest_prune = Dom.Mem.get_latest_prune mem in - BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus:true ~last_included:false - ~latest_prune location cond_set + BoUtils.Check.array_access ~arr ~idx ~is_plus:true ~last_included:false ~latest_prune location + cond_set | Exp.BinOp (bop, e1, e2) -> check_binop integer_type_widths ~bop ~e1 ~e2 location mem cond_set | _ -> @@ -239,34 +234,23 @@ let rec check_expr_for_integer_overflow integer_type_widths exp location mem con let instantiate_cond : - Tenv.t - -> Typ.IntegerWidths.t + Typ.IntegerWidths.t -> Typ.Procname.t -> (Pvar.t * Typ.t) list -> (Exp.t * Typ.t) list -> Dom.Mem.t - -> BufferOverrunAnalysisSummary.t -> BufferOverrunCheckerSummary.t -> Location.t -> PO.ConditionSet.checked_t = - fun tenv integer_type_widths callee_pname callee_formals params caller_mem callee_exit_mem - callee_cond location -> - let rel_subst_map = - Option.value_map Config.bo_relational_domain ~default:Relation.SubstMap.empty ~f:(fun _ -> - Sem.get_subst_map tenv integer_type_widths callee_formals params caller_mem callee_exit_mem - ) - in - let caller_rel = Dom.Mem.get_relation caller_mem in + fun integer_type_widths callee_pname callee_formals params caller_mem callee_cond location -> let eval_sym_trace = Sem.mk_eval_sym_trace integer_type_widths callee_formals params caller_mem in let latest_prune = Dom.Mem.get_latest_prune caller_mem in - PO.ConditionSet.subst callee_cond eval_sym_trace rel_subst_map caller_rel callee_pname location - latest_prune + PO.ConditionSet.subst callee_cond eval_sym_trace callee_pname location latest_prune type checks_summary = BufferOverrunCheckerSummary.t -type get_proc_summary = - Typ.Procname.t -> (BufferOverrunAnalysisSummary.t * (Pvar.t * Typ.t) list * checks_summary) option +type get_proc_summary = Typ.Procname.t -> ((Pvar.t * Typ.t) list * checks_summary) option let check_instr : get_proc_summary @@ -308,9 +292,9 @@ let check_instr : check model_env mem cond_set | None -> ( match get_proc_summary callee_pname with - | Some (callee_mem, callee_formals, callee_condset) -> - instantiate_cond tenv integer_type_widths callee_pname callee_formals params mem - callee_mem callee_condset location + | Some (callee_formals, callee_condset) -> + instantiate_cond integer_type_widths callee_pname callee_formals params mem + callee_condset location |> PO.ConditionSet.join cond_set | None -> (* unknown call / no inferbo payload *) cond_set ) ) @@ -416,13 +400,12 @@ let report_errors : Tenv.t -> checks -> Summary.t -> unit = PO.ConditionSet.report_errors ~report cond_set -let get_checks_summary : BufferOverrunAnalysis.local_decls -> checks -> checks_summary = - fun locals - Checks. +let get_checks_summary : checks -> checks_summary = + fun Checks. { cond_set ; unused_branches= _ (* intra-procedural *) ; unreachable_statements= _ (* intra-procedural *) } -> - PO.ConditionSet.for_summary ~relation_forget_locs:locals cond_set + PO.ConditionSet.for_summary cond_set let checker : Callbacks.proc_callback_args -> Summary.t = @@ -442,17 +425,13 @@ let checker : Callbacks.proc_callback_args -> Summary.t = let get_proc_summary callee_pname = Ondemand.analyze_proc_name ~caller_summary:summary callee_pname |> Option.bind ~f:(fun summary -> - let analysis_payload = BufferOverrunAnalysis.Payload.of_summary summary in let checker_payload = Payload.of_summary summary in - Option.map2 analysis_payload checker_payload - ~f:(fun analysis_payload checker_payload -> - ( analysis_payload - , Summary.get_proc_desc summary |> Procdesc.get_pvar_formals - , checker_payload ) ) ) + Option.map checker_payload ~f:(fun checker_payload -> + (Summary.get_proc_desc summary |> Procdesc.get_pvar_formals, checker_payload) + ) ) in compute_checks get_proc_summary proc_desc tenv integer_type_widths cfg inv_map in report_errors tenv checks summary ; - let locals = BufferOverrunAnalysis.get_local_decls proc_desc in - let cond_set = get_checks_summary locals checks in + let cond_set = get_checks_summary checks in Payload.update_summary cond_set summary ) diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 786488dd1..50869fe84 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -13,7 +13,6 @@ open! AbstractDomain.Types module F = Format module L = Logging module OndemandEnv = BufferOverrunOndemandEnv -module Relation = BufferOverrunDomainRelation module SPath = Symb.SymbolPath module Trace = BufferOverrunTrace module TraceSet = Trace.Set @@ -93,11 +92,8 @@ module Val = struct ; itv_thresholds: ItvThresholds.t ; itv_updated_by: ItvUpdatedBy.t ; modeled_range: ModeledRange.t - ; sym: Relation.Sym.t ; powloc: PowLoc.t ; arrayblk: ArrayBlk.t - ; offset_sym: Relation.Sym.t - ; size_sym: Relation.Sym.t ; traces: TraceSet.t } let bot : t = @@ -105,11 +101,8 @@ module Val = struct ; itv_thresholds= ItvThresholds.empty ; itv_updated_by= ItvUpdatedBy.bottom ; modeled_range= ModeledRange.bottom - ; sym= Relation.Sym.bot ; powloc= PowLoc.bot ; arrayblk= ArrayBlk.bot - ; offset_sym= Relation.Sym.bot - ; size_sym= Relation.Sym.bot ; traces= TraceSet.bottom } @@ -121,9 +114,6 @@ module Val = struct let itv_updated_by_pp fmt itv_updated_by = if Config.bo_debug >= 3 then F.fprintf fmt "(updated by %a)" ItvUpdatedBy.pp itv_updated_by in - let relation_sym_pp fmt sym = - if Option.is_some Config.bo_relational_domain then F.fprintf fmt ", %a" Relation.Sym.pp sym - in let modeled_range_pp fmt range = if not (ModeledRange.is_bottom range) then F.fprintf fmt " (modeled_range:%a)" ModeledRange.pp range @@ -131,10 +121,9 @@ module Val = struct let trace_pp fmt traces = if Config.bo_debug >= 1 then F.fprintf fmt ", %a" TraceSet.pp traces in - F.fprintf fmt "(%a%a%a%a%a, %a, %a%a%a%a)" Itv.pp x.itv itv_thresholds_pp x.itv_thresholds - relation_sym_pp x.sym itv_updated_by_pp x.itv_updated_by modeled_range_pp x.modeled_range - PowLoc.pp x.powloc ArrayBlk.pp x.arrayblk relation_sym_pp x.offset_sym relation_sym_pp - x.size_sym trace_pp x.traces + F.fprintf fmt "(%a%a%a%a, %a, %a%a)" Itv.pp x.itv itv_thresholds_pp x.itv_thresholds + itv_updated_by_pp x.itv_updated_by modeled_range_pp x.modeled_range PowLoc.pp x.powloc + ArrayBlk.pp x.arrayblk trace_pp x.traces let unknown_from : callee_pname:_ -> location:_ -> t = @@ -144,11 +133,8 @@ module Val = struct ; itv_thresholds= ItvThresholds.empty ; itv_updated_by= ItvUpdatedBy.Top ; modeled_range= ModeledRange.bottom - ; sym= Relation.Sym.top ; powloc= PowLoc.unknown ; arrayblk= ArrayBlk.unknown - ; offset_sym= Relation.Sym.top - ; size_sym= Relation.Sym.top ; traces } @@ -159,11 +145,8 @@ module Val = struct && ItvThresholds.leq ~lhs:lhs.itv_thresholds ~rhs:rhs.itv_thresholds && ItvUpdatedBy.leq ~lhs:lhs.itv_updated_by ~rhs:rhs.itv_updated_by && ModeledRange.leq ~lhs:lhs.modeled_range ~rhs:rhs.modeled_range - && Relation.Sym.leq ~lhs:lhs.sym ~rhs:rhs.sym && PowLoc.leq ~lhs:lhs.powloc ~rhs:rhs.powloc && ArrayBlk.leq ~lhs:lhs.arrayblk ~rhs:rhs.arrayblk - && Relation.Sym.leq ~lhs:lhs.offset_sym ~rhs:rhs.offset_sym - && Relation.Sym.leq ~lhs:lhs.size_sym ~rhs:rhs.size_sym let widen ~prev ~next ~num_iters = @@ -179,11 +162,8 @@ module Val = struct ItvUpdatedBy.widen ~prev:prev.itv_updated_by ~next:next.itv_updated_by ~num_iters ; modeled_range= ModeledRange.widen ~prev:prev.modeled_range ~next:next.modeled_range ~num_iters - ; sym= Relation.Sym.widen ~prev:prev.sym ~next:next.sym ~num_iters ; powloc= PowLoc.widen ~prev:prev.powloc ~next:next.powloc ~num_iters ; arrayblk= ArrayBlk.widen ~prev:prev.arrayblk ~next:next.arrayblk ~num_iters - ; offset_sym= Relation.Sym.widen ~prev:prev.offset_sym ~next:next.offset_sym ~num_iters - ; size_sym= Relation.Sym.widen ~prev:prev.size_sym ~next:next.size_sym ~num_iters ; traces= TraceSet.join prev.traces next.traces } @@ -195,11 +175,8 @@ module Val = struct ; itv_thresholds= ItvThresholds.join x.itv_thresholds y.itv_thresholds ; itv_updated_by= ItvUpdatedBy.join x.itv_updated_by y.itv_updated_by ; modeled_range= ModeledRange.join x.modeled_range y.modeled_range - ; sym= Relation.Sym.join x.sym y.sym ; powloc= PowLoc.join x.powloc y.powloc ; arrayblk= ArrayBlk.join x.arrayblk y.arrayblk - ; offset_sym= Relation.Sym.join x.offset_sym y.offset_sym - ; size_sym= Relation.Sym.join x.size_sym y.size_sym ; traces= TraceSet.join x.traces y.traces } @@ -209,10 +186,6 @@ module Val = struct let get_modeled_range : t -> ModeledRange.t = fun x -> x.modeled_range - let get_sym : t -> Relation.Sym.t = fun x -> x.sym - - let get_sym_var : t -> Relation.Var.t option = fun x -> Relation.Sym.get_var x.sym - let get_pow_loc : t -> PowLoc.t = fun x -> x.powloc let get_array_blk : t -> ArrayBlk.t = fun x -> x.arrayblk @@ -221,10 +194,6 @@ module Val = struct let get_all_locs : t -> PowLoc.t = fun x -> PowLoc.join x.powloc (get_array_locs x) - let get_offset_sym : t -> Relation.Sym.t = fun x -> x.offset_sym - - let get_size_sym : t -> Relation.Sym.t = fun x -> x.size_sym - let get_traces : t -> TraceSet.t = fun x -> x.traces let of_itv ?(traces = TraceSet.bottom) itv = {bot with itv; traces} @@ -243,19 +212,11 @@ module Val = struct Allocsite.t -> stride:int option -> offset:Itv.t -> size:Itv.t -> traces:TraceSet.t -> t = fun allocsite ~stride ~offset ~size ~traces -> let stride = Option.value_map stride ~default:Itv.nat ~f:Itv.of_int in - { bot with - arrayblk= ArrayBlk.make_c allocsite ~offset ~size ~stride - ; offset_sym= Relation.Sym.of_allocsite_offset allocsite - ; size_sym= Relation.Sym.of_allocsite_size allocsite - ; traces } + {bot with arrayblk= ArrayBlk.make_c allocsite ~offset ~size ~stride; traces} let of_java_array_alloc : Allocsite.t -> length:Itv.t -> traces:TraceSet.t -> t = - fun allocsite ~length ~traces -> - { bot with - arrayblk= ArrayBlk.make_java allocsite ~length - ; size_sym= Relation.Sym.of_allocsite_size allocsite - ; traces } + fun allocsite ~length ~traces -> {bot with arrayblk= ArrayBlk.make_java allocsite ~length; traces} let of_literal_string : Typ.IntegerWidths.t -> string -> t = @@ -284,11 +245,11 @@ module Val = struct let set_modeled_range range x = {x with modeled_range= range} - let unknown_bit : t -> t = fun x -> {x with itv= Itv.top; sym= Relation.Sym.top} + let unknown_bit : t -> t = fun x -> {x with itv= Itv.top} - let neg : t -> t = fun x -> {x with itv= Itv.neg x.itv; sym= Relation.Sym.top} + let neg : t -> t = fun x -> {x with itv= Itv.neg x.itv} - let lnot : t -> t = fun x -> {x with itv= Itv.lnot x.itv |> Itv.of_bool; sym= Relation.Sym.top} + let lnot : t -> t = fun x -> {x with itv= Itv.lnot x.itv |> Itv.of_bool} let lift_itv : (Itv.t -> Itv.t -> Itv.t) -> ?f_trace:_ -> t -> t -> t = fun f ?f_trace x y -> @@ -1766,7 +1727,6 @@ module MemReach = struct ; mem_pure: MemPure.t ; alias: Alias.t ; latest_prune: LatestPrune.t - ; relation: Relation.t ; oenv: ('has_oenv, OndemandEnv.t) GOption.t } type no_oenv_t = GOption.none t0 @@ -1779,7 +1739,6 @@ module MemReach = struct ; mem_pure= MemPure.bot ; alias= Alias.init ; latest_prune= LatestPrune.top - ; relation= Relation.empty ; oenv= GOption.GSome oenv } @@ -1790,7 +1749,6 @@ module MemReach = struct && MemPure.leq ~lhs:lhs.mem_pure ~rhs:rhs.mem_pure && Alias.leq ~lhs:lhs.alias ~rhs:rhs.alias && LatestPrune.leq ~lhs:lhs.latest_prune ~rhs:rhs.latest_prune - && Relation.leq ~lhs:lhs.relation ~rhs:rhs.relation let widen ~prev ~next ~num_iters = @@ -1802,7 +1760,6 @@ module MemReach = struct ; mem_pure= MemPure.widen oenv ~prev:prev.mem_pure ~next:next.mem_pure ~num_iters ; alias= Alias.widen ~prev:prev.alias ~next:next.alias ~num_iters ; latest_prune= LatestPrune.widen ~prev:prev.latest_prune ~next:next.latest_prune ~num_iters - ; relation= Relation.widen ~prev:prev.relation ~next:next.relation ~num_iters ; oenv= prev.oenv } ) @@ -1814,16 +1771,13 @@ module MemReach = struct ; mem_pure= MemPure.join oenv x.mem_pure y.mem_pure ; alias= Alias.join x.alias y.alias ; latest_prune= LatestPrune.join x.latest_prune y.latest_prune - ; relation= Relation.join x.relation y.relation ; oenv= x.oenv } let pp : F.formatter -> _ t0 -> unit = fun fmt x -> F.fprintf fmt "StackLocs:@;%a@;MemPure:@;%a@;Alias:@;%a@;%a" StackLocs.pp x.stack_locs - MemPure.pp x.mem_pure Alias.pp x.alias LatestPrune.pp x.latest_prune ; - if Option.is_some Config.bo_relational_domain then - F.fprintf fmt "@;Relation:@;%a" Relation.pp x.relation + MemPure.pp x.mem_pure Alias.pp x.alias LatestPrune.pp x.latest_prune let unset_oenv : t -> no_oenv_t = function x -> {x with oenv= GOption.GNone} @@ -1940,14 +1894,6 @@ module MemReach = struct let add_heap : ?represents_multiple_values:bool -> Loc.t -> Val.t -> t -> t = fun ?represents_multiple_values x v m -> - let v = - let sym = if Itv.is_bottom (Val.get_itv v) then Relation.Sym.bot else Relation.Sym.of_loc x in - let offset_sym, size_sym = - if ArrayBlk.is_bot (Val.get_array_blk v) then (Relation.Sym.bot, Relation.Sym.bot) - else (Relation.Sym.of_loc_offset x, Relation.Sym.of_loc_size x) - in - {v with Val.sym; Val.offset_sym; Val.size_sym} - in {m with mem_pure= MemPure.add ?represents_multiple_values x v m.mem_pure} @@ -2106,30 +2052,6 @@ module MemReach = struct fun ~filter_loc ~node_id {mem_pure} -> MemPure.range ~filter_loc ~node_id mem_pure - let get_relation : t -> Relation.t = fun m -> m.relation - - let is_relation_unsat : t -> bool = fun m -> Relation.is_unsat m.relation - - let lift_relation : (Relation.t -> Relation.t) -> t -> t = - fun f m -> {m with relation= f m.relation} - - - let meet_constraints : Relation.Constraints.t -> t -> t = - fun constrs -> lift_relation (Relation.meet_constraints constrs) - - - let store_relation : - PowLoc.t - -> Relation.SymExp.t option * Relation.SymExp.t option * Relation.SymExp.t option - -> t - -> t = - fun locs symexp_opts -> lift_relation (Relation.store_relation locs symexp_opts) - - - let relation_forget_locs : PowLoc.t -> t -> t = - fun locs -> lift_relation (Relation.forget_locs locs) - - let forget_unreachable_locs : formals:(Pvar.t * Typ.t) list -> t -> t = fun ~formals m -> let is_reachable = @@ -2149,25 +2071,6 @@ module MemReach = struct let forget_size_alias arr_locs m = {m with alias= Alias.forget_size_alias arr_locs m.alias} - let init_param_relation : Loc.t -> t -> t = fun loc -> lift_relation (Relation.init_param loc) - - let init_array_relation : - Allocsite.t - -> offset_opt:Itv.t option - -> size:Itv.t - -> size_exp_opt:Relation.SymExp.t option - -> t - -> t = - fun allocsite ~offset_opt ~size ~size_exp_opt -> - lift_relation (Relation.init_array allocsite ~offset_opt ~size ~size_exp_opt) - - - let instantiate_relation : Relation.SubstMap.t -> caller:t -> callee:no_oenv_t -> t = - fun subst_map ~caller ~callee -> - { caller with - relation= Relation.instantiate subst_map ~caller:caller.relation ~callee:callee.relation } - - (* unsound *) let set_first_idx_of_null : Loc.t -> Val.t -> t -> t = fun loc idx m -> update_mem (PowLoc.singleton (Loc.of_c_strlen loc)) idx m @@ -2412,58 +2315,12 @@ module Mem = struct fun latest_prune m -> map ~f:(MemReach.set_latest_prune latest_prune) m - let get_relation : t -> Relation.t = - fun m -> f_lift_default ~default:Relation.bot MemReach.get_relation m - - - let meet_constraints : Relation.Constraints.t -> t -> t = - fun constrs -> map ~f:(MemReach.meet_constraints constrs) - - - let is_relation_unsat m = f_lift_default ~default:true MemReach.is_relation_unsat m - - let store_relation : - PowLoc.t - -> Relation.SymExp.t option * Relation.SymExp.t option * Relation.SymExp.t option - -> t - -> t = - fun locs symexp_opts -> map ~f:(MemReach.store_relation locs symexp_opts) - - - let relation_forget_locs : PowLoc.t -> t -> t = - fun locs -> map ~f:(MemReach.relation_forget_locs locs) - - let forget_unreachable_locs : formals:(Pvar.t * Typ.t) list -> t -> t = fun ~formals -> map ~f:(MemReach.forget_unreachable_locs ~formals) let forget_size_alias arr_locs = map ~f:(MemReach.forget_size_alias arr_locs) - let[@warning "-32"] init_param_relation : Loc.t -> t -> t = - fun loc -> map ~f:(MemReach.init_param_relation loc) - - - let init_array_relation : - Allocsite.t - -> offset_opt:Itv.t option - -> size:Itv.t - -> size_exp_opt:Relation.SymExp.t option - -> t - -> t = - fun allocsite ~offset_opt ~size ~size_exp_opt -> - map ~f:(MemReach.init_array_relation allocsite ~offset_opt ~size ~size_exp_opt) - - - let instantiate_relation : Relation.SubstMap.t -> caller:t -> callee:no_oenv_t -> t = - fun subst_map ~caller ~callee -> - match callee with - | Bottom | ExcRaised -> - caller - | NonBottom callee -> - map ~f:(fun caller -> MemReach.instantiate_relation subst_map ~caller ~callee) caller - - let unset_oenv = function | (Bottom | ExcRaised) as x -> x diff --git a/infer/src/bufferoverrun/bufferOverrunDomainRelation.ml b/infer/src/bufferoverrun/bufferOverrunDomainRelation.ml deleted file mode 100644 index 2cd85be49..000000000 --- a/infer/src/bufferoverrun/bufferOverrunDomainRelation.ml +++ /dev/null @@ -1,1601 +0,0 @@ -(* - * Copyright (c) Facebook, Inc. and its affiliates. - * - * This source code is licensed under the MIT license found in the - * LICENSE file in the root directory of this source tree. - *) - -open! IStd -open Core -open AbsLoc -open! AbstractDomain.Types -module F = Format -open Apron - -module type S = sig - module Var : sig - type t - end - - module Sym : sig - include AbstractDomain.S - - val bot : t - - val top : t - - val of_loc : Loc.t -> t - - val of_loc_offset : Loc.t -> t - - val of_loc_size : Loc.t -> t - - val of_allocsite_offset : Allocsite.t -> t - - val of_allocsite_size : Allocsite.t -> t - - val get_var : t -> Var.t option - end - - module SymExp : sig - type t [@@deriving compare] - - val pp_opt : F.formatter -> t option -> unit - - val zero : t - - val of_sym : Sym.t -> t option - - val of_exp : get_sym_f:(Exp.t -> Sym.t) -> Exp.t -> t option - - val of_exps : - get_int_sym_f:(Exp.t -> Sym.t) - -> get_offset_sym_f:(Exp.t -> Sym.t) - -> get_size_sym_f:(Exp.t -> Sym.t) - -> Exp.t - -> t option * t option * t option - - val of_exp_opt : get_sym_f:(Exp.t -> Sym.t) -> Exp.t option -> t option - - val plus : t -> t -> t - - val minus : t -> t -> t - end - - module Constraints : sig - type t - - val of_exp : get_sym_f:(Exp.t -> Sym.t) -> Exp.t -> t - end - - module SubstMap : sig - type t - - val empty : t - - val add : Var.t -> SymExp.t option -> t -> t - - val symexp_subst_opt : t -> SymExp.t option -> SymExp.t option - end - - include AbstractDomain.S - - val set_deserialize : unit -> unit - - val compare : t -> t -> int - - val empty : t - - val bot : t - - val is_unsat : t -> bool - - val lt_sat_opt : SymExp.t option -> SymExp.t option -> t -> bool - - val le_sat_opt : SymExp.t option -> SymExp.t option -> t -> bool - - val meet_constraints : Constraints.t -> t -> t - - val store_relation : PowLoc.t -> SymExp.t option * SymExp.t option * SymExp.t option -> t -> t - - val init_param : Loc.t -> t -> t - - val init_array : - Allocsite.t -> offset_opt:Itv.t option -> size:Itv.t -> size_exp_opt:SymExp.t option -> t -> t - - val forget_locs : PowLoc.t -> t -> t - - val instantiate : caller:t -> callee:t -> SubstMap.t -> t -end - -module NoRelation = struct - module UnitDom = struct - type t = unit [@@deriving compare] - - let f1 _ = () - - let f2 _ _ = () - - let f3 _ _ _ = () - - let f1_none _ = None - - let f2_none _ _ = None - - let f1_false _ = false - - let f3_false _ _ _ = false - - let leq ~lhs:() ~rhs:() = true - - let join = f2 - - let widen ~prev:() ~next:() ~num_iters:_ = () - - let pp = f2 - - let bot = () - - let top = () - end - - module Var = UnitDom - - module Sym = struct - include UnitDom - - let of_loc = f1 - - let of_loc_offset = f1 - - let of_loc_size = f1 - - let of_allocsite_offset = f1 - - let of_allocsite_size = f1 - - let get_var = f1_none - end - - module SymExp = struct - include UnitDom - - let pp_opt = f2 - - let zero = () - - let of_exp ~get_sym_f:_ = f1_none - - let of_exps ~get_int_sym_f:_ ~get_offset_sym_f:_ ~get_size_sym_f:_ _x = (None, None, None) - - let of_exp_opt ~get_sym_f:_ = f1_none - - let of_sym = f1_none - - let plus = f2 - - let minus = f2 - end - - module Constraints = struct - include UnitDom - - let of_exp ~get_sym_f:_ = f1 - end - - module SubstMap = struct - include UnitDom - - let empty = () - - let add = f3 - - let symexp_subst_opt = f2_none - end - - include UnitDom - - let set_deserialize = f1 - - let empty = () - - let is_unsat = f1_false - - let lt_sat_opt = f3_false - - let le_sat_opt = f3_false - - let meet_constraints = f2 - - let store_relation = f3 - - let init_param = f2 - - let init_array _allocsite ~offset_opt:_ ~size:_ ~size_exp_opt:_ = f1 - - let forget_locs = f2 - - let instantiate ~caller:_ ~callee:_ = f1 -end - -module type Manager_S = sig - type domain_t - - val alloc_man : unit -> domain_t Manager.t -end - -module Make (Manager : Manager_S) = struct - let man = Manager.alloc_man () - - let set_deserialize () = Apron.Manager.set_deserialize man - - module Compares = struct - let lift int_of x y = int_of x - int_of y - - let int_of_unop = function Texpr0.Neg -> 0 | Texpr0.Cast -> 1 | Texpr0.Sqrt -> 2 - - let int_of_binop = function - | Texpr0.Add -> - 0 - | Texpr0.Sub -> - 1 - | Texpr0.Mul -> - 2 - | Texpr0.Div -> - 3 - | Texpr0.Mod -> - 4 - | Texpr0.Pow -> - 5 - - - let int_of_typ = function - | Texpr0.Real -> - 0 - | Texpr0.Int -> - 1 - | Texpr0.Single -> - 2 - | Texpr0.Double -> - 3 - | Texpr0.Extended -> - 4 - | Texpr0.Quad -> - 5 - - - let int_of_round = function - | Texpr0.Near -> - 0 - | Texpr0.Zero -> - 1 - | Texpr0.Up -> - 2 - | Texpr0.Down -> - 3 - | Texpr0.Rnd -> - 4 - - - let compare_unop = lift int_of_unop - - let compare_binop = lift int_of_binop - - let compare_typ = lift int_of_typ - - let compare_round = lift int_of_round - - let ( ) n (cmp, x, y) = if n <> 0 then n else cmp x y - - let rec compare_texpr0_expr x y = - let int_of_texpr0_expr = function - | Texpr0.Cst _ -> - 0 - | Texpr0.Dim _ -> - 1 - | Texpr0.Unop _ -> - 2 - | Texpr0.Binop _ -> - 3 - in - match (x, y) with - | Texpr0.Cst c1, Texpr0.Cst c2 -> - Coeff.cmp c1 c2 - | Texpr0.Dim i1, Texpr0.Dim i2 -> - i1 - i2 - | Texpr0.Unop (uop1, e1, t1, r1), Texpr0.Unop (uop2, e2, t2, r2) -> - compare_unop uop1 uop2 (compare_texpr0_expr, e1, e2) (compare_typ, t1, t2) - (compare_round, r1, r2) - | Texpr0.Binop (bop1, le1, re1, t1, r1), Texpr0.Binop (bop2, le2, re2, t2, r2) -> - compare_binop bop1 bop2 (compare_texpr0_expr, le1, le2) - (compare_texpr0_expr, re1, re2) (compare_typ, t1, t2) (compare_round, r1, r2) - | _, _ -> - int_of_texpr0_expr x - int_of_texpr0_expr y - - - let compare_texpr0 x y = compare_texpr0_expr (Texpr0.to_expr x) (Texpr0.to_expr y) - - let compare_texpr1 x y = - compare_texpr0 (Texpr1.get_texpr0 x) (Texpr1.get_texpr0 y) - (Environment.compare, Texpr1.get_env x, Texpr1.get_env y) - - - let compare_abstract1 x y = Abstract1.hash man x - Abstract1.hash man y - end - - module TexprToLinexpr = struct - let scalar_op (float_op, mpqf_op, mpfrf_op) s1 s2 = - match (s1, s2) with - | Scalar.Float f1, Scalar.Float f2 -> - Scalar.Float (float_op f1 f2) - | Scalar.Float f1, Scalar.Mpqf m2 | Scalar.Mpqf m2, Scalar.Float f1 -> - Scalar.Mpqf (mpqf_op (Mpqf.of_float f1) m2) - | Scalar.Float f1, Scalar.Mpfrf m2 | Scalar.Mpfrf m2, Scalar.Float f1 -> - Scalar.Mpfrf (mpfrf_op (Mpfrf.of_float f1 Mpfr.Near) m2 Mpfr.Near) - | Scalar.Mpqf m1, Scalar.Mpqf m2 -> - Scalar.Mpqf (mpqf_op m1 m2) - | Scalar.Mpqf m1, Scalar.Mpfrf m2 | Scalar.Mpfrf m2, Scalar.Mpqf m1 -> - Scalar.Mpfrf (mpfrf_op (Mpfrf.of_mpq m1 Mpfr.Near) m2 Mpfr.Near) - | Scalar.Mpfrf m1, Scalar.Mpfrf m2 -> - Scalar.Mpfrf (mpfrf_op m1 m2 Mpfr.Near) - - - let scalar_add = scalar_op (( +. ), Mpqf.add, Mpfrf.add) - - let scalar_mult = scalar_op (( *. ), Mpqf.mul, Mpfrf.mul) - - let coeff_plus c1 c2 = - match (c1, c2) with - | Coeff.Scalar s1, Coeff.Scalar s2 -> - Coeff.Scalar (scalar_add s1 s2) - | _, _ -> - assert false - - - let coeff_minus c1 c2 = coeff_plus c1 (Coeff.neg c2) - - let coeff_mult c1 c2 = - match (c1, c2) with - | Coeff.Scalar s1, Coeff.Scalar s2 -> - Coeff.Scalar (scalar_mult s1 s2) - | _, _ -> - assert false - - - let rec is_constant = function - | Texpr1.Cst c -> - Some c - | Texpr1.Unop (Texpr1.Neg, re1, _, _) -> - Option.map (is_constant re1) ~f:Coeff.neg - | Texpr1.Binop (Texpr1.Add, re1, re2, _, _) -> - Option.map2 (is_constant re1) (is_constant re2) ~f:coeff_plus - | Texpr1.Binop (Texpr1.Sub, re1, re2, _, _) -> - Option.map2 (is_constant re1) (is_constant re2) ~f:coeff_minus - | Texpr1.Binop (Texpr1.Mul, re1, re2, _, _) -> - Option.map2 (is_constant re1) (is_constant re2) ~f:coeff_mult - | _ -> - None - - - let rec add_coeffs ~coeff re x = - match re with - | Texpr1.Cst c -> - let c' = Linexpr1.get_cst x in - Linexpr1.set_cst x (coeff_plus c' (coeff_mult c coeff)) ; - Some x - | Texpr1.Var var -> - let c' = Linexpr1.get_coeff x var in - Linexpr1.set_coeff x var (coeff_plus c' coeff) ; - Some x - | Texpr1.Unop (Texpr1.Neg, re1, _, _) -> - add_coeffs ~coeff:(Coeff.neg coeff) re1 x - | Texpr1.Binop (Texpr1.Add, re1, re2, _, _) -> - Option.bind (add_coeffs ~coeff re1 x) ~f:(add_coeffs ~coeff re2) - | Texpr1.Binop (Texpr1.Sub, re1, re2, _, _) -> - Option.bind (add_coeffs ~coeff re1 x) ~f:(add_coeffs ~coeff:(Coeff.neg coeff) re2) - | Texpr1.Binop (Texpr1.Mul, re1, re2, _, _) -> ( - match is_constant re1 with - | None -> - Option.value_map (is_constant re2) ~default:None ~f:(fun c -> - add_coeffs ~coeff:(coeff_mult coeff c) re1 x ) - | Some c -> - add_coeffs ~coeff:(coeff_mult coeff c) re2 x ) - | _ -> - assert false - - - let trans x = - let lin = Linexpr1.make (Texpr1.get_env x) in - add_coeffs ~coeff:(Coeff.s_of_int 1) (Texpr1.to_expr x) lin - end - - module Var = struct - include Apron.Var - - let equal = [%compare.equal: t] - - let pp = print - - let dummy = of_string "dummy" - - let return = of_string "return" - - let param_prefix = "__inferbo_param_" - - let temp_param_prefix = "__inferbo_temp_param_" - - let loc_offset_prefix = "__inferbo_loc_offset_" - - let loc_size_prefix = "__inferbo_loc_size_" - - let allocsite_offset_prefix = "__inferbo_allocsite_offset_" - - let allocsite_size_prefix = "__inferbo_allocsite_size_" - - let of_loc loc = of_string (Loc.to_string loc) - - let of_loc_offset loc = of_string (loc_offset_prefix ^ Loc.to_string loc) - - let of_loc_size loc = of_string (loc_size_prefix ^ Loc.to_string loc) - - let of_allocsite_offset allocsite = - of_string (allocsite_offset_prefix ^ Allocsite.to_string allocsite) - - - let of_allocsite_size allocsite = - of_string (allocsite_size_prefix ^ Allocsite.to_string allocsite) - - - let param_of var = of_string (param_prefix ^ to_string var) - - let temp_param_of var = of_string (temp_param_prefix ^ to_string var) - - let param_of_loc loc = of_string (param_prefix ^ Loc.to_string loc) - - let array_of_var var = Array.create ~len:1 var - - let array_of_powloc of_loc locs = - let len = PowLoc.cardinal locs in - let a = Array.create ~len dummy in - let i = ref 0 in - PowLoc.iter - (fun loc -> - a.(!i) <- of_loc loc ; - i := !i + 1 ) - locs ; - a - - - let int_array_of_powloc locs = array_of_powloc of_loc locs - - let offset_array_of_powloc locs = array_of_powloc of_loc_offset locs - - let size_array_of_powloc locs = array_of_powloc of_loc_size locs - end - - module VarSet = struct - include PrettyPrintable.MakePPSet (Var) - - let of_array var_array = Array.fold var_array ~init:empty ~f:(fun acc var -> add var acc) - - let to_array x = - let a = Array.create ~len:(cardinal x) Var.dummy in - let n = ref 0 in - iter - (fun var -> - a.(!n) <- var ; - n := !n + 1 ) - x ; - a - - - let of_powloc var_of_loc locs = PowLoc.fold (fun loc acc -> add (var_of_loc loc) acc) locs empty - - let int_of_powloc locs = of_powloc Var.of_loc locs - - let offset_of_powloc locs = of_powloc Var.of_loc_offset locs - - let size_of_powloc locs = of_powloc Var.of_loc_size locs - end - - module VarMap = struct - include PrettyPrintable.MakePPMap (Var) - - let iter x ~f = iter f x - - let fold x ~init ~f = fold f x init - - let fold2 x y ~init ~f = - let m = merge (fun _ v1 v2 -> Some (v1, v2)) x y in - fold m ~init ~f:(fun k (v1, v2) acc -> f k v1 v2 acc) - end - - module Sym = struct - include AbstractDomain.Flat (Var) - - let bot = bottom - - let lift f x = v (f x) - - let of_loc = lift Var.of_loc - - let of_loc_offset = lift Var.of_loc_offset - - let of_loc_size = lift Var.of_loc_size - - let of_allocsite_offset = lift Var.of_allocsite_offset - - let of_allocsite_size = lift Var.of_allocsite_size - - let get_var = get - end - - module Env = struct - type t = Environment.t - - let empty : t = Environment.make [||] [||] - - let join env1 env2 = - let vars, _ = Environment.vars env2 in - let vars = Array.filter vars ~f:(fun var -> not (Environment.mem_var env1 var)) in - Environment.add env1 vars [||] - - - let of_vars_array vars = Environment.make vars [||] - - let of_vars_set vars = of_vars_array (VarSet.to_array vars) - - let to_vars_set x = - let vars, _ = Environment.vars x in - VarSet.of_array vars - end - - module SymExp = struct - (* raw tree expression without environments *) - type raw = Texpr1.expr - - (* efficient tree expression with environments *) - type t = Texpr1.t - - let string_of_binop = function - | Texpr1.Add -> - "+" - | Texpr1.Sub -> - "-" - | Texpr1.Mul -> - "*" - | Texpr1.Div -> - "/" - | Texpr1.Mod -> - "%" - | Texpr1.Pow -> - "^" - - - let rec pp_raw ~need_paren fmt = function - | Texpr1.Cst coeff -> - Coeff.print fmt coeff - | Texpr1.Var x -> - Var.print fmt x - | Texpr1.Unop (Texpr1.Neg, e, _, _) -> - F.fprintf fmt "-%a" (pp_raw ~need_paren:true) e - | Texpr1.Unop (Texpr1.Cast, e, typ, _) -> - F.fprintf fmt "(%a)%a" Texpr1.print_typ typ (pp_raw ~need_paren:true) e - | Texpr1.Unop (Texpr1.Sqrt, e, _, _) -> - F.fprintf fmt "sqrt(%a)" (pp_raw ~need_paren:false) e - | Texpr1.Binop (bop, e1, e2, _, _) -> - (if need_paren then F.fprintf fmt "(%a%s%a)" else F.fprintf fmt "%a%s%a") - (pp_raw ~need_paren:true) e1 (string_of_binop bop) (pp_raw ~need_paren:true) e2 - - - let pp fmt x = pp_raw ~need_paren:false fmt (Texpr1.to_expr x) - - let pp_opt fmt = function None -> F.fprintf fmt "None" | Some x -> pp fmt x - - let compare = Compares.compare_texpr1 - - (* NOTE: We consider only integer values as of now. *) - let default_round = Texpr1.Near - - let raw_uop_make typ re = Texpr1.Unop (typ, re, Texpr1.Int, default_round) - - let raw_bop_make typ re1 re2 = Texpr1.Binop (typ, re1, re2, Texpr1.Int, default_round) - - let vars_array_of_raw re = - let rec vars_set_of = function - | Texpr1.Cst _ -> - VarSet.empty - | Texpr1.Var x -> - VarSet.singleton x - | Texpr1.Unop (_, re, _, _) -> - vars_set_of re - | Texpr1.Binop (_, re1, re2, _, _) -> - VarSet.union (vars_set_of re1) (vars_set_of re2) - in - VarSet.to_array (vars_set_of re) - - - let vars_set_of x = Env.to_vars_set (Texpr1.get_env x) - - let vars_set_of_opt x_opt = Option.value_map x_opt ~default:VarSet.empty ~f:vars_set_of - - let env_of_raw re = Env.of_vars_array (vars_array_of_raw re) - - let raw_of_exp ~get_sym_f e : raw option = - let try_get_sym_f e = get_sym_f e |> Sym.get_var |> Option.map ~f:(fun x -> Texpr1.Var x) in - let rec raw_of_exp' e = - match e with - | Exp.UnOp (Unop.Neg, e', _) -> ( - match raw_of_exp' e' with - | Some re -> - Some (raw_uop_make Texpr1.Neg re) - | None -> - try_get_sym_f e ) - | Exp.BinOp (bop, e1, e2) -> ( - match (raw_of_exp' e1, raw_of_exp' e2) with - | Some re1, Some re2 -> ( - match bop with - | Binop.PlusA _ -> - Some (raw_bop_make Texpr1.Add re1 re2) - | Binop.MinusA _ -> - Some (raw_bop_make Texpr1.Sub re1 re2) - | Binop.Mult _ -> - Some (raw_bop_make Texpr1.Mul re1 re2) - | _ -> - try_get_sym_f e ) - | _, _ -> - try_get_sym_f e ) - | Exp.Const (Const.Cint i) -> - Option.map (IntLit.to_int i) ~f:(fun n -> Texpr1.Cst (Coeff.s_of_int n)) - | _ -> - try_get_sym_f e - in - raw_of_exp' e - - - let raw_offset_of_exp ~get_int_sym_f ~get_offset_sym_f e = - let try_get_offset_sym_f e = - get_offset_sym_f e |> Sym.get_var |> Option.map ~f:(fun x -> Texpr1.Var x) - in - let rec raw_offset_of_exp' e = - match e with - | Exp.BinOp (bop, e1, e2) -> ( - match (raw_offset_of_exp' e1, raw_of_exp ~get_sym_f:get_int_sym_f e2) with - | Some re1, Some re2 -> ( - match bop with - | Binop.PlusPI -> - Some (raw_bop_make Texpr1.Add re1 re2) - | Binop.MinusPI -> - Some (raw_bop_make Texpr1.Sub re1 re2) - | _ -> - try_get_offset_sym_f e ) - | _, _ -> - try_get_offset_sym_f e ) - | _ -> - try_get_offset_sym_f e - in - raw_offset_of_exp' e - - - let raw_size_of_exp ~get_size_sym_f e = - let try_get_size_sym_f e = - get_size_sym_f e |> Sym.get_var |> Option.map ~f:(fun x -> Texpr1.Var x) - in - let rec raw_size_of_exp' e = - match e with - | Exp.BinOp (bop, e1, _e2) -> ( - match raw_size_of_exp' e1 with - | Some re1 -> ( - match bop with Binop.PlusPI | Binop.MinusPI -> Some re1 | _ -> try_get_size_sym_f e ) - | _ -> - try_get_size_sym_f e ) - | _ -> - try_get_size_sym_f e - in - raw_size_of_exp' e - - - let of_raw re = Texpr1.of_expr (env_of_raw re) re - - let of_exp ~get_sym_f e = Option.map (raw_of_exp ~get_sym_f e) ~f:of_raw - - let offset_of_exp ~get_int_sym_f ~get_offset_sym_f e : t option = - Option.map (raw_offset_of_exp ~get_int_sym_f ~get_offset_sym_f e) ~f:of_raw - - - let size_of_exp ~get_size_sym_f e : t option = - Option.map (raw_size_of_exp ~get_size_sym_f e) ~f:of_raw - - - let of_exps ~get_int_sym_f ~get_offset_sym_f ~get_size_sym_f e : t option * t option * t option - = - let int_sym = of_exp ~get_sym_f:get_int_sym_f e in - let offset_sym = offset_of_exp ~get_int_sym_f ~get_offset_sym_f e in - let size_sym = size_of_exp ~get_size_sym_f e in - (int_sym, offset_sym, size_sym) - - - let of_exp_opt ~get_sym_f opt_e : t option = Option.find_map opt_e ~f:(of_exp ~get_sym_f) - - let of_big_int i = - Texpr1.cst Env.empty (Coeff.s_of_mpq (Mpq.of_mpz (Mpz.of_string (Z.to_string i)))) - - - let zero = of_big_int Z.zero - - let one = of_big_int Z.one - - let of_sym s = Sym.get_var s |> Option.map ~f:(fun x -> of_raw (Texpr1.Var x)) - - let of_var var = of_raw (Texpr1.Var var) - - let dummy = of_var Var.dummy - - let linexpr_dummy = Linexpr1.make Env.empty - - let to_var x = match Texpr1.to_expr x with Texpr1.Var x' -> Some x' | _ -> None - - let is_var x = match to_var x with Some _ -> true | None -> false - - let bop_make typ x y = - let env = Env.join (Texpr1.get_env x) (Texpr1.get_env y) in - let re = raw_bop_make typ (Texpr1.to_expr x) (Texpr1.to_expr y) in - Texpr1.of_expr env re - - - let plus = bop_make Texpr1.Add - - let minus = bop_make Texpr1.Sub - - let to_linexpr = TexprToLinexpr.trans - end - - module SubstMap = struct - type t = SymExp.t option VarMap.t - - let add = VarMap.add - - let empty = VarMap.empty - - let fold = VarMap.fold - - let mem = VarMap.mem - - let singleton = VarMap.singleton - - let map_opt ~f x = VarMap.map (Option.value_map ~default:None ~f) x - - let to_arrays dummy x = - let x = - VarMap.fold x ~init:VarMap.empty ~f:(fun k v_opt acc -> - Option.value_map v_opt ~default:acc ~f:(fun v -> VarMap.add k v acc) ) - in - let keys = Array.create ~len:(VarMap.cardinal x) Var.dummy in - let values = Array.create ~len:(VarMap.cardinal x) dummy in - let n = ref 0 in - VarMap.iter x ~f:(fun key value -> - keys.(!n) <- key ; - values.(!n) <- value ; - n := !n + 1 ) ; - (keys, values) - - - let to_arrays_symexp = to_arrays SymExp.dummy - - let to_arrays_linexpr = to_arrays SymExp.linexpr_dummy - - let rec symexp_raw_subst subst_map x = - match x with - | Texpr1.Cst _ -> - Some x - | Texpr1.Var var -> - if mem var subst_map then Option.map (VarMap.find var subst_map) ~f:Texpr1.to_expr - else None - | Texpr1.Unop (uop, re, typ, round) -> - Option.map (symexp_raw_subst subst_map re) ~f:(fun re' -> - Texpr1.Unop (uop, re', typ, round) ) - | Texpr1.Binop (bop, re1, re2, typ, round) -> - Option.map2 (symexp_raw_subst subst_map re1) (symexp_raw_subst subst_map re2) - ~f:(fun re1' re2' -> Texpr1.Binop (bop, re1', re2', typ, round)) - - - let symexp_subst subst_map x = - let re_opt = symexp_raw_subst subst_map (Texpr1.to_expr x) in - Option.map re_opt ~f:SymExp.of_raw - - - let symexp_subst_opt subst_map x_opt = - Option.value_map x_opt ~default:None ~f:(symexp_subst subst_map) - end - - module Constraints = struct - type t = Tcons1.earray - - let empty = Tcons1.array_make Env.empty 0 - - let singleton e = - let tcons_array = Tcons1.array_make (Tcons1.get_env e) 1 in - Tcons1.array_set tcons_array 0 e ; tcons_array - - - let doubleton e1 e2 = - let env = Env.join (Tcons1.get_env e1) (Tcons1.get_env e2) in - let tcons_array = Tcons1.array_make env 2 in - Tcons1.array_set tcons_array 0 e1 ; Tcons1.array_set tcons_array 1 e2 ; tcons_array - - - let and_ x y = - let env = Env.join (Tcons1.array_get_env x) (Tcons1.array_get_env y) in - let x, y = (Tcons1.array_extend_environment x env, Tcons1.array_extend_environment y env) in - let len1, len2 = (Tcons1.array_length x, Tcons1.array_length y) in - let tcons_array = Tcons1.array_make env (len1 + len2) in - for i = 0 to len1 - 1 do - Tcons1.array_set tcons_array i (Tcons1.array_get x i) - done ; - for i = 0 to len2 - 1 do - Tcons1.array_set tcons_array (len1 + i) (Tcons1.array_get y i) - done ; - tcons_array - - - let eq_of var1 var2 = - let sym_exp1, sym_exp2 = (SymExp.of_var var1, SymExp.of_var var2) in - let sym_exp = SymExp.minus sym_exp1 sym_exp2 in - singleton (Tcons1.make sym_exp Tcons1.EQ) - - - let eq_of_sym sym1 sym_exp2 = - Option.map (SymExp.of_sym sym1) ~f:(fun sym_exp1 -> - let sym_exp = SymExp.minus sym_exp1 sym_exp2 in - singleton (Tcons1.make sym_exp Tcons1.EQ) ) - - - let itv_of sym itv = - match itv with - | Bottom -> - empty - | NonBottom itv_pure -> - let lb, ub = (Itv.ItvPure.lb itv_pure, Itv.ItvPure.ub itv_pure) in - Option.value_map (SymExp.of_sym sym) ~default:empty ~f:(fun sym_exp -> - let tcons_lb = - Option.map (Itv.Bound.get_const lb) ~f:(fun lb -> - let sym_minus_lb = SymExp.minus sym_exp (SymExp.of_big_int lb) in - Tcons1.make sym_minus_lb Tcons1.SUPEQ ) - in - let tcons_ub = - Option.map (Itv.Bound.get_const ub) ~f:(fun ub -> - let ub_minus_sym = SymExp.minus (SymExp.of_big_int ub) sym_exp in - Tcons1.make ub_minus_sym Tcons1.SUPEQ ) - in - match (tcons_lb, tcons_ub) with - | Some tcons_lb, Some tcons_ub -> - doubleton tcons_lb tcons_ub - | Some tcons, None | None, Some tcons -> - singleton tcons - | None, None -> - empty ) - - - let of_raw_symexp re typ = singleton (Tcons1.make (SymExp.of_raw re) typ) - - let of_exp ~get_sym_f e : t = - let of_bin_compare bop e1 e2 = - match (SymExp.raw_of_exp ~get_sym_f e1, SymExp.raw_of_exp ~get_sym_f e2) with - | Some re1, Some re2 -> - of_raw_symexp (SymExp.raw_bop_make Texpr1.Sub re1 re2) bop - | _, _ -> - empty - in - match e with - | Exp.Var _ | Exp.Lvar _ | Exp.Cast _ | Exp.Lfield _ | Exp.Lindex _ -> ( - match get_sym_f e |> Sym.get_var with - | Some x -> - of_raw_symexp (Texpr1.Var x) Tcons1.DISEQ - | None -> - empty ) - | Exp.BinOp (Binop.Eq, e1, e2) | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Ne, e1, e2), _) -> - of_bin_compare Tcons1.EQ e1 e2 - | Exp.BinOp (Binop.Ne, e1, e2) | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Eq, e1, e2), _) -> - of_bin_compare Tcons1.DISEQ e1 e2 - | Exp.BinOp (Binop.Gt, e1, e2) - | Exp.BinOp (Binop.Lt, e2, e1) - | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Le, e1, e2), _) - | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Ge, e2, e1), _) -> - of_bin_compare Tcons1.SUP e1 e2 - | Exp.BinOp (Binop.Ge, e1, e2) - | Exp.BinOp (Binop.Le, e2, e1) - | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Lt, e1, e2), _) - | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Gt, e2, e1), _) -> - of_bin_compare Tcons1.SUPEQ e1 e2 - | _ -> - empty - - - let vars_set_of x = - let vars = ref VarSet.empty in - for i = 0 to Tcons1.array_length x - 1 do - vars := VarSet.union !vars (SymExp.vars_set_of (Tcons1.get_texpr1 (Tcons1.array_get x i))) - done ; - !vars - - - let remove_strict_ineq_tcons1 x = - match Tcons1.get_typ x with - | Tcons1.SUP -> - let e_minus_one = SymExp.minus (Tcons1.get_texpr1 x) SymExp.one in - Tcons1.make e_minus_one Tcons1.SUPEQ - | _ -> - x - - - let remove_strict_ineq x = - let length = Tcons1.array_length x in - let x' = Tcons1.array_make (Tcons1.array_get_env x) length in - for i = 0 to length - 1 do - let tcons1 = Tcons1.array_get x i in - Tcons1.array_set x' i (remove_strict_ineq_tcons1 tcons1) - done ; - x' - end - - module Val = struct - type t = Manager.domain_t Abstract1.t - - let compare = Compares.compare_abstract1 - - let bot = Abstract1.bottom man Env.empty - - let top = Abstract1.top man Env.empty - - let is_bot x = Abstract1.is_bottom man x - - let is_top x = Abstract1.is_top man x - - let sync_env x y = - let x, y = (Abstract1.minimize_environment man x, Abstract1.minimize_environment man y) in - let env = Env.join (Abstract1.env x) (Abstract1.env y) in - let x = Abstract1.change_environment man x env false in - let y = Abstract1.change_environment man y env false in - (x, y) - - - let extend_env env x = - let x = Abstract1.minimize_environment man x in - let new_env = Env.join (Abstract1.env x) env in - Abstract1.change_environment man x new_env false - - - let sync_env_lift f x y = - let x, y = sync_env x y in - f x y - - - let join = sync_env_lift (Abstract1.join man) - - let meet = sync_env_lift (Abstract1.meet man) - - let widen ~prev ~next ~num_iters:_ = sync_env_lift (Abstract1.widening man) prev next - - let pp fmt x = Abstract1.print fmt x - - let leq ~lhs ~rhs = sync_env_lift (Abstract1.is_leq man) lhs rhs - - let sat_tcons tcons x = - let tcons = Constraints.remove_strict_ineq_tcons1 tcons in - let x = extend_env (Tcons1.get_env tcons) x in - Abstract1.sat_tcons man x tcons - - - let is_unsat_constraint constr x = - let symexp = Tcons1.get_texpr1 constr in - let typ = Tcons1.get_typ constr in - let neg_constr_opt = - match typ with - | Tcons1.EQ -> - Some (Tcons1.make symexp Tcons1.DISEQ) - | Tcons1.DISEQ -> - Some (Tcons1.make symexp Tcons1.EQ) - | Tcons1.SUPEQ | Tcons1.SUP -> ( - let env = Tcons1.get_env constr in - let neg_symexp = - Texpr1.of_expr env (SymExp.raw_uop_make Texpr1.Neg (Texpr1.to_expr symexp)) - in - match typ with - | Tcons1.SUPEQ -> - Some (Tcons1.make neg_symexp Tcons1.SUP) - | Tcons1.SUP -> - Some (Tcons1.make neg_symexp Tcons1.SUPEQ) - | _ -> - assert false ) - | _ -> - None - in - Option.value_map neg_constr_opt ~default:false ~f:(fun neg_constr -> sat_tcons neg_constr x) - - - let is_unsat_constraints constrs x = - let sat = ref true in - for i = 0 to Tcons1.array_length constrs - 1 do - let constr = Tcons1.array_get constrs i in - if is_unsat_constraint constr x then sat := false - done ; - not !sat - - - let meet_constraints constrs x = - let constrs = Constraints.remove_strict_ineq constrs in - let x = extend_env (Tcons1.array_get_env constrs) x in - if is_unsat_constraints constrs x then bot else Abstract1.meet_tcons_array man x constrs - - - let forget_vars_array vars x = - let x = extend_env (Env.of_vars_array vars) x in - Abstract1.forget_array man x vars false - - - let forget_vars_set vars x = forget_vars_array (VarSet.to_array vars) x - - let assign_vars vars texpr x = - let x = extend_env (Env.join (Texpr1.get_env texpr) (Env.of_vars_array vars)) x in - let texprs = Array.create ~len:(Array.length vars) texpr in - Abstract1.assign_texpr_array man x vars texprs None - - - let store_relation var_array_of_powloc locs texpr_opt x = - let vars = var_array_of_powloc locs in - if can_strong_update locs then - match texpr_opt with - | Some texpr -> - assign_vars vars texpr x - | None -> - forget_vars_array vars x - else forget_vars_array vars x - - - let store_relation_int locs texpr_opt x = - store_relation Var.int_array_of_powloc locs texpr_opt x - - - let store_relation_offset locs texpr_opt x = - store_relation Var.offset_array_of_powloc locs texpr_opt x - - - let store_relation_size locs texpr_opt x = - store_relation Var.size_array_of_powloc locs texpr_opt x - - - let forget_var var x = forget_vars_array (Var.array_of_var var) x - - let lt_sat e1 e2 x = sat_tcons (Tcons1.make (SymExp.minus e2 e1) Tcons1.SUP) x - - let le_sat e1 e2 x = sat_tcons (Tcons1.make (SymExp.minus e2 e1) Tcons1.SUPEQ) x - - let subst : forget_free:bool -> SubstMap.t -> t -> t = - let forget_free_vars vars_in_subst_map x = - let free_vars = VarSet.diff (Env.to_vars_set (Abstract1.env x)) vars_in_subst_map in - let free_vars = VarSet.remove Var.return free_vars in - forget_vars_set free_vars x - in - let filter_vars_to_none subst_map x = - let vars_to_none = - SubstMap.fold subst_map ~init:VarSet.empty ~f:(fun k v acc -> - match v with None -> VarSet.add k acc | Some _ -> acc ) - in - forget_vars_set vars_to_none x - in - let extend_and_substitute subst_map to_arrays new_env substitute x = - let x = filter_vars_to_none subst_map x in - let vars, exps = to_arrays subst_map in - let x = extend_env new_env x in - substitute man x vars exps None - in - fun ~forget_free subst_map x -> - let vars_in_subst_map = - SubstMap.fold subst_map ~init:VarSet.empty ~f:(fun var sym_exp_opt acc -> - acc |> VarSet.add var - |> VarSet.add (Var.param_of var) - |> VarSet.union (SymExp.vars_set_of_opt sym_exp_opt) ) - in - let new_env = Env.of_vars_set vars_in_subst_map in - let x = if forget_free then forget_free_vars vars_in_subst_map x else x in - match Config.bo_relational_domain with - | None -> - assert false - | Some `Bo_relational_domain_oct -> - extend_and_substitute subst_map SubstMap.to_arrays_symexp new_env - Abstract1.substitute_texpr_array x - | Some `Bo_relational_domain_poly -> - let subst_map = SubstMap.map_opt ~f:SymExp.to_linexpr subst_map in - extend_and_substitute subst_map SubstMap.to_arrays_linexpr new_env - Abstract1.substitute_linexpr_array x - end - - module Pack = struct - type t = int [@@deriving compare] - - let equal = Int.equal - - let pp fmt x = F.fprintf fmt "%d" x - - let subst ~from ~to_ x = if equal x from then to_ else x - end - - module PackSet = struct - include PrettyPrintable.MakePPSet (Pack) - - let subst ~from ~to_ x = if mem x from then to_ else x - end - - module PackMap = struct - include PrettyPrintable.MakePPMap (Pack) - - let remove_packs pack_ids x = PackSet.fold remove pack_ids x - end - - module PackedVal = struct - type t = {pack_ids: Pack.t VarMap.t; packs: Val.t PackMap.t} [@@deriving compare] - - let empty = {pack_ids= VarMap.empty; packs= PackMap.empty} - - let pp_packs = PackMap.pp ~pp_value:Val.pp - - let pp fmt x = pp_packs fmt x.packs - - let sync_pack x y = - let id_ref = ref 0 in - let get_new_id () : Pack.t = - id_ref := !id_ref + 1 ; - !id_ref - in - let add_subst_partial var id (pack_ids, subst) = - match PackMap.find id subst with - | id' -> - (VarMap.add var id' pack_ids, subst) - | exception Caml.Not_found -> - let id' = get_new_id () in - (VarMap.add var id' pack_ids, PackMap.add id id' subst) - in - let add_subst var id1_opt id2_opt ((pack_ids, subst1, subst2) as subst_res) = - match (id1_opt, id2_opt) with - | Some id1, Some id2 -> ( - match (PackMap.find_opt id1 subst1, PackMap.find_opt id2 subst2) with - | Some id1', Some id2' -> - if Pack.equal id1' id2' then (VarMap.add var id1' pack_ids, subst1, subst2) - else - let pack_ids = - pack_ids |> VarMap.add var id1' |> VarMap.map (Pack.subst ~from:id2' ~to_:id1') - in - let subst1 = PackMap.map (Pack.subst ~from:id2' ~to_:id1') subst1 in - let subst2 = PackMap.map (Pack.subst ~from:id2' ~to_:id1') subst2 in - (pack_ids, subst1, subst2) - | Some id1', None -> - (VarMap.add var id1' pack_ids, subst1, PackMap.add id2 id1' subst2) - | None, Some id2' -> - (VarMap.add var id2' pack_ids, PackMap.add id1 id2' subst1, subst2) - | None, None -> - let id' = get_new_id () in - (VarMap.add var id' pack_ids, PackMap.add id1 id' subst1, PackMap.add id2 id' subst2) - ) - | Some id1, None -> - let pack_ids, subst1 = add_subst_partial var id1 (pack_ids, subst1) in - (pack_ids, subst1, subst2) - | None, Some id2 -> - let pack_ids, subst2 = add_subst_partial var id2 (pack_ids, subst2) in - (pack_ids, subst1, subst2) - | None, None -> - subst_res - in - let get_subst_map pack_ids1 pack_ids2 = - VarMap.fold2 pack_ids1 pack_ids2 ~f:add_subst - ~init:(VarMap.empty, PackMap.empty, PackMap.empty) - in - let subst subst_map packs = - let subst_helper pack_id v acc = - match PackMap.find pack_id subst_map with - | pack_id' -> - let v = - Option.value_map (PackMap.find_opt pack_id' acc) ~default:v ~f:(fun v' -> - Val.meet v' v ) - in - PackMap.add pack_id' v acc - | exception Caml.Not_found -> - acc - in - PackMap.fold subst_helper packs PackMap.empty - in - let pack_ids, subst_map_x, subst_map_y = get_subst_map x.pack_ids y.pack_ids in - (pack_ids, subst subst_map_x x.packs, subst subst_map_y y.packs) - - - let le_synced_packs ~lhs ~rhs = - let ge_than_lhs pack_id rhs = - match PackMap.find pack_id lhs with - | lhs -> - Val.leq ~lhs ~rhs - | exception Caml.Not_found -> - Val.is_top rhs - in - PackMap.for_all ge_than_lhs rhs - - - let join_synced_packs x y = - let join_opt _ v1_opt v2_opt = Option.map2 v1_opt v2_opt ~f:Val.join in - PackMap.merge join_opt x y - - - let meet_synced_packs x y = - let exception BottomByMeet in - let meet_opt _ v1_opt v2_opt = - match (v1_opt, v2_opt) with - | Some v1, Some v2 -> - let v = Val.meet v1 v2 in - if Val.is_bot v then raise BottomByMeet else Some v - | Some v, None | None, Some v -> - Some v - | None, None -> - None - in - match PackMap.merge meet_opt x y with packs -> Some packs | exception BottomByMeet -> None - - - let widen_synced_packs ~prev ~next ~num_iters = - let widen_opt _ prev_opt next_opt = - Option.map2 prev_opt next_opt ~f:(fun prev next -> Val.widen ~prev ~next ~num_iters) - in - PackMap.merge widen_opt prev next - - - let leq ~lhs ~rhs = - let _, packs_lhs, packs_rhs = sync_pack lhs rhs in - le_synced_packs ~lhs:packs_lhs ~rhs:packs_rhs - - - let join x y = - let pack_ids, packs_x, packs_y = sync_pack x y in - if le_synced_packs ~lhs:packs_x ~rhs:packs_y then y - else if le_synced_packs ~lhs:packs_y ~rhs:packs_x then x - else {pack_ids; packs= join_synced_packs packs_x packs_y} - - - let meet x y = - let pack_ids, packs_x, packs_y = sync_pack x y in - if le_synced_packs ~lhs:packs_x ~rhs:packs_y then NonBottom x - else if le_synced_packs ~lhs:packs_y ~rhs:packs_x then NonBottom y - else - Option.value_map (meet_synced_packs packs_x packs_y) ~default:Bottom ~f:(fun packs -> - NonBottom {pack_ids; packs} ) - - - let widen ~prev ~next ~num_iters = - let pack_ids, packs_prev, packs_next = sync_pack prev next in - {pack_ids; packs= widen_synced_packs ~prev:packs_prev ~next:packs_next ~num_iters} - - - let pack_id_of_var var x = VarMap.find var x.pack_ids - - let pack_id_of_var_opt var x = VarMap.find_opt var x.pack_ids - - let pack_ids_of_vars vars x = - let add_id var acc = - Option.value_map (pack_id_of_var_opt var x) ~default:acc ~f:(fun id -> PackSet.add id acc) - in - VarSet.fold add_id vars PackSet.empty - - - let val_of_pack_id_opt pack_id x = PackMap.find_opt pack_id x.packs - - let val_of_pack_id pack_id x = Option.value (val_of_pack_id_opt pack_id x) ~default:Val.top - - let val_of_pack_ids ids x = - let meet_val id acc = - Option.value_map (val_of_pack_id_opt id x) ~default:acc ~f:(fun v -> Val.meet acc v) - in - PackSet.fold meet_val ids Val.top - - - let val_of_vars vars x = val_of_pack_ids (pack_ids_of_vars vars x) x - - let lt_sat e1 e2 x = - let vars = VarSet.union (SymExp.vars_set_of e1) (SymExp.vars_set_of e2) in - Val.lt_sat e1 e2 (val_of_vars vars x) - - - let le_sat e1 e2 x = - let vars = VarSet.union (SymExp.vars_set_of e1) (SymExp.vars_set_of e2) in - Val.le_sat e1 e2 (val_of_vars vars x) - - - let lift_sat_opt f e1_opt e2_opt x = - match (e1_opt, e2_opt) with Some e1, Some e2 -> f e1 e2 x | _, _ -> false - - - let lt_sat_opt = lift_sat_opt lt_sat - - let le_sat_opt = lift_sat_opt le_sat - - let repack_with_vars vars x = - let id_ref = - let max_pack_id = - VarMap.fold x.pack_ids ~init:0 ~f:(fun _ pack_id acc -> max acc pack_id) - in - ref max_pack_id - in - let get_new_id () : Pack.t = - id_ref := !id_ref + 1 ; - !id_ref - in - let set_pack_id_of_vars vars id pack_ids = - VarSet.fold (fun var acc -> VarMap.add var id acc) vars pack_ids - in - let vars_ids = pack_ids_of_vars vars x in - match PackSet.is_singleton_or_more vars_ids with - | IContainer.Empty -> - let id = get_new_id () in - {x with pack_ids= set_pack_id_of_vars vars id x.pack_ids} - | IContainer.Singleton id -> - {x with pack_ids= set_pack_id_of_vars vars id x.pack_ids} - | IContainer.More -> - let id = PackSet.min_elt vars_ids in - let other_ids = PackSet.remove id vars_ids in - let pack_ids = - x.pack_ids |> set_pack_id_of_vars vars id - |> VarMap.map (PackSet.subst ~from:other_ids ~to_:id) - in - let packs = - let v = val_of_pack_ids vars_ids x in - x.packs |> PackMap.remove_packs other_ids |> PackMap.add id v - in - {pack_ids; packs} - - - let subst ~forget_free subst_map x = - let exception BottomBySubst in - let repack_for_subst subst_map x = - SubstMap.fold subst_map ~init:x ~f:(fun var sym_exp_opt acc -> - let vars = VarSet.add var (SymExp.vars_set_of_opt sym_exp_opt) in - repack_with_vars vars acc ) - in - let pack_subst_map x subst_map = - let add_subst var exp acc = - let pack_id = pack_id_of_var var x in - match PackMap.find pack_id acc with - | subst_map -> - PackMap.add pack_id (SubstMap.add var exp subst_map) acc - | exception Caml.Not_found -> - PackMap.add pack_id (SubstMap.singleton var exp) acc - in - SubstMap.fold subst_map ~init:PackMap.empty ~f:add_subst - in - let do_subst packed_subst_map pack_id v acc = - let subst_map = - Option.value (PackMap.find_opt pack_id packed_subst_map) ~default:SubstMap.empty - in - let v = Val.subst ~forget_free subst_map v in - if Val.is_bot v then raise BottomBySubst else PackMap.add pack_id v acc - in - let x = repack_for_subst subst_map x in - let packed_subst_map = pack_subst_map x subst_map in - match PackMap.fold (do_subst packed_subst_map) x.packs PackMap.empty with - | packs -> - NonBottom {x with packs} - | exception BottomBySubst -> - Bottom - - - let meet_constraints constrs x = - let vars = Constraints.vars_set_of constrs in - if VarSet.is_empty vars then - if Val.is_unsat_constraints constrs Val.top then Bottom else NonBottom x - else - let x = repack_with_vars vars x in - let pack_id = pack_id_of_var (VarSet.choose vars) x in - let v = Val.meet_constraints constrs (val_of_pack_id pack_id x) in - if Val.is_bot v then Bottom else NonBottom {x with packs= PackMap.add pack_id v x.packs} - - - let store_relation locs (int_exp, offset_exp, size_exp) x = - let store_relation' varset_of_locs exp_opt val_store_relation x = - let vars_of_exp = VarSet.union (varset_of_locs locs) (SymExp.vars_set_of_opt exp_opt) in - let x = repack_with_vars vars_of_exp x in - let pack_id = pack_id_of_var (VarSet.choose vars_of_exp) x in - let v = val_store_relation locs exp_opt (val_of_pack_id pack_id x) in - if Val.is_bot v then Bottom else NonBottom {x with packs= PackMap.add pack_id v x.packs} - in - let ( ||> ) x f = match x with Bottom -> Bottom | NonBottom x -> f x in - if PowLoc.is_empty locs then NonBottom x - else - store_relation' VarSet.int_of_powloc int_exp Val.store_relation_int x - ||> store_relation' VarSet.offset_of_powloc offset_exp Val.store_relation_offset - ||> store_relation' VarSet.size_of_powloc size_exp Val.store_relation_size - - - let forget_var var x = - let forget_var_in pack_id = - let pack_ids = VarMap.remove var x.pack_ids in - let packs = - Option.value_map (val_of_pack_id_opt pack_id x) ~default:x.packs ~f:(fun v -> - PackMap.add pack_id (Val.forget_var var v) x.packs ) - in - {pack_ids; packs} - in - Option.value_map (pack_id_of_var_opt var x) ~default:x ~f:forget_var_in - - - let forget_loc loc x = forget_var (Var.of_loc loc) x - - let forget_locs locs x = PowLoc.fold forget_loc locs x - - let forget_vars vars x = VarSet.fold forget_var vars x - - let init_param loc x = - let param_var = Var.param_of_loc loc in - let var = Var.of_loc loc in - meet_constraints (Constraints.eq_of param_var var) x - - - let init_array allocsite ~offset_opt ~size ~size_exp_opt x = - let size_sym = Sym.of_allocsite_size allocsite in - let size_constrs = - match size_exp_opt with - | None -> - Constraints.itv_of size_sym size - | Some size_exp -> ( - match Constraints.eq_of_sym size_sym size_exp with - | None -> - Constraints.itv_of size_sym size - | Some constr -> - constr ) - in - let constraints = - match offset_opt with - | Some offset -> - let offset_sym = Sym.of_allocsite_offset allocsite in - let offset_constrs = Constraints.itv_of offset_sym offset in - Constraints.and_ offset_constrs size_constrs - | None -> - size_constrs - in - meet_constraints constraints x - - - let subst_param_caller subst_map caller = - let accum_rev_if_var k v acc = - Option.value_map (SymExp.to_var v) ~default:acc ~f:(fun k' -> - SubstMap.add k' (Some (SymExp.of_var (Var.temp_param_of k))) acc ) - in - let accum_rev k v_opt acc = - Option.value_map v_opt ~default:acc ~f:(fun v -> accum_rev_if_var k v acc) - in - let rev_subst_map = SubstMap.fold subst_map ~init:SubstMap.empty ~f:accum_rev in - subst ~forget_free:false rev_subst_map caller - - - let subst_callee subst_map callee = - let accum_param_subst k v acc = - let v = - match v with - | Some v' when SymExp.is_var v' -> - Some (SymExp.of_var (Var.temp_param_of k)) - | _ -> - v - in - SubstMap.add (Var.param_of k) v acc - in - let param_subst_map = SubstMap.fold subst_map ~init:SubstMap.empty ~f:accum_param_subst in - subst ~forget_free:true param_subst_map callee - - - let forget_temp_param subst_map x = - let temps = - SubstMap.fold subst_map ~init:VarSet.empty ~f:(fun k _ acc -> - VarSet.add (Var.temp_param_of k) acc ) - in - forget_vars temps x - - - let instantiate ~caller ~callee subst_map = - match subst_param_caller subst_map caller with - | Bottom -> - Bottom - | NonBottom caller -> ( - match subst_callee subst_map callee with - | Bottom -> - Bottom - | NonBottom callee -> ( - match meet caller callee with - | Bottom -> - Bottom - | NonBottom relation -> - NonBottom (forget_temp_param subst_map relation) ) ) - end - - include AbstractDomain.BottomLifted (PackedVal) - - let compare x y = - match (x, y) with - | Bottom, Bottom -> - 0 - | Bottom, _ -> - -1 - | _, Bottom -> - 1 - | NonBottom x', NonBottom y' -> - PackedVal.compare x' y' - - - let empty : t = NonBottom PackedVal.empty - - let bot : t = Bottom - - let is_unsat : t -> bool = function Bottom -> true | NonBottom _ -> false - - let lift_default : default:'a -> (PackedVal.t -> 'a) -> t -> 'a = - fun ~default f -> function Bottom -> default | NonBottom x -> f x - - - let lift : (PackedVal.t -> PackedVal.t) -> t -> t = - fun f -> function Bottom -> Bottom | NonBottom x -> NonBottom (f x) - - - let lift2 : (PackedVal.t -> PackedVal.t -> t) -> t -> t -> t = - fun f x y -> - match (x, y) with Bottom, _ | _, Bottom -> Bottom | NonBottom x', NonBottom y' -> f x' y' - - - let lt_sat_opt : SymExp.t option -> SymExp.t option -> t -> bool = - fun e1_opt e2_opt -> lift_default ~default:true (PackedVal.lt_sat_opt e1_opt e2_opt) - - - let le_sat_opt : SymExp.t option -> SymExp.t option -> t -> bool = - fun e1_opt e2_opt -> lift_default ~default:true (PackedVal.le_sat_opt e1_opt e2_opt) - - - let meet_constraints : Constraints.t -> t -> t = - fun constrs -> lift_default ~default:Bottom (PackedVal.meet_constraints constrs) - - - let store_relation : PowLoc.t -> SymExp.t option * SymExp.t option * SymExp.t option -> t -> t = - fun locs texpr_opts -> lift_default ~default:Bottom (PackedVal.store_relation locs texpr_opts) - - - let init_param : Loc.t -> t -> t = - fun loc -> lift_default ~default:Bottom (PackedVal.init_param loc) - - - let init_array : - Allocsite.t -> offset_opt:Itv.t option -> size:Itv.t -> size_exp_opt:SymExp.t option -> t -> t - = - fun allocsite ~offset_opt ~size ~size_exp_opt -> - lift_default ~default:Bottom (PackedVal.init_array allocsite ~offset_opt ~size ~size_exp_opt) - - - let forget_locs : PowLoc.t -> t -> t = fun locs -> lift (PackedVal.forget_locs locs) - - let instantiate : caller:t -> callee:t -> SubstMap.t -> t = - fun ~caller ~callee subst_map -> - lift2 (fun caller callee -> PackedVal.instantiate ~caller ~callee subst_map) caller callee -end - -module ApronOctagonManager = struct - type domain_t = Oct.t - - let alloc_man : unit -> domain_t Manager.t = Oct.manager_alloc -end - -module ElinaPolyManager = struct - type domain_t = Elina_poly.loose Elina_poly.t - - let alloc_man : unit -> domain_t Manager.t = Elina_poly.manager_alloc_loose -end - -include ( val match Config.bo_relational_domain with - | None -> - (module NoRelation : S) - | Some `Bo_relational_domain_oct -> - (module Make (ApronOctagonManager) : S) - | Some `Bo_relational_domain_poly -> - (module Make (ElinaPolyManager) : S) ) - -(* NOTE: Globally only one manager (of a relational domain depends on - Apron) can set deserialization functions. *) -let () = set_deserialize () diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 32f794775..380dab659 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -13,7 +13,6 @@ module BoUtils = BufferOverrunUtils module Dom = BufferOverrunDomain module PO = BufferOverrunProofObligations module Sem = BufferOverrunSemantics -module Relation = BufferOverrunDomainRelation module Trace = BufferOverrunTrace open BoUtils.ModelEnv open ProcnameDispatcher.Call.FuncArg @@ -128,10 +127,6 @@ let malloc ~can_be_zero size_exp = let allocsite = Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path ~represents_multiple_values in - let size_exp_opt = - let size_exp = Option.value dyn_length ~default:length0 in - Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f integer_type_widths mem) size_exp - in if Language.curr_language_is Java then let internal_arr = let allocsite = @@ -148,7 +143,6 @@ let malloc ~can_be_zero size_exp = let v = Dom.Val.of_c_array_alloc allocsite ~stride ~offset ~size ~traces in mem |> Dom.Mem.add_stack (Loc.of_id id) v - |> Dom.Mem.init_array_relation allocsite ~offset_opt:(Some offset) ~size ~size_exp_opt |> BoUtils.Exec.init_c_array_fields model_env path typ (Dom.Val.get_array_locs v) ?dyn_length and check = check_alloc_size ~can_be_zero size_exp in {exec; check} @@ -203,11 +197,10 @@ let strcpy dest_exp src_exp = and check {integer_type_widths; location} mem cond_set = let access_last_char = let idx = Dom.Mem.get_c_strlen (Sem.eval_locs src_exp mem) mem in - let relation = Dom.Mem.get_relation mem in let latest_prune = Dom.Mem.get_latest_prune mem in fun arr cond_set -> - BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp:None ~relation ~is_plus:true - ~last_included:false ~latest_prune location cond_set + BoUtils.Check.array_access ~arr ~idx ~is_plus:true ~last_included:false ~latest_prune + location cond_set in cond_set |> access_last_char (Sem.eval integer_type_widths dest_exp mem) @@ -246,10 +239,9 @@ let strcat dest_exp src_exp = |> Dom.Mem.add_stack (Loc.of_id id) (Sem.eval integer_type_widths dest_exp mem) and check {integer_type_widths; location} mem cond_set = let access_last_char arr idx cond_set = - let relation = Dom.Mem.get_relation mem in let latest_prune = Dom.Mem.get_latest_prune mem in - BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp:None ~relation ~is_plus:true - ~last_included:false ~latest_prune location cond_set + BoUtils.Check.array_access ~arr ~idx ~is_plus:true ~last_included:false ~latest_prune location + cond_set in let src_strlen = let str_loc = Sem.eval_locs src_exp mem in @@ -575,10 +567,9 @@ module ArrObjCommon = struct and check ({location; integer_type_widths} as model_env) mem cond_set = let idx = Sem.eval integer_type_widths index_exp mem in let arr = Dom.Mem.find_set (deref_of model_env arr_exp ~fn mem) mem in - let relation = Dom.Mem.get_relation mem in let latest_prune = Dom.Mem.get_latest_prune mem in - BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp:None ~relation ~is_plus:true - ~last_included:false ~latest_prune location cond_set + BoUtils.Check.array_access ~arr ~idx ~is_plus:true ~last_included:false ~latest_prune location + cond_set in {exec; check} @@ -978,13 +969,9 @@ module Collection = struct Dom.Mem.find_set arr_locs mem in let idx = Sem.eval integer_type_widths index_exp mem in - let idx_sym_exp = - Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f integer_type_widths mem) index_exp - in - let relation = Dom.Mem.get_relation mem in let latest_prune = Dom.Mem.get_latest_prune mem in - BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus:true ~last_included - ~latest_prune location cond_set + BoUtils.Check.array_access ~arr ~idx ~is_plus:true ~last_included ~latest_prune location + cond_set let add_at_index (coll_id : Ident.t) index_exp = diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index bb3fcd561..f821f0844 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml @@ -13,7 +13,6 @@ module Bound = Bounds.Bound module Dom = BufferOverrunDomain module ItvPure = Itv.ItvPure module MF = MarkupFormatter -module Relation = BufferOverrunDomainRelation module Sem = BufferOverrunSemantics module ValTrace = BufferOverrunTrace @@ -195,15 +194,7 @@ module AllocSizeCondition = struct end module ArrayAccessCondition = struct - type t = - { offset: ItvPure.t - ; idx: ItvPure.t - ; size: ItvPure.t - ; last_included: bool - ; idx_sym_exp: Relation.SymExp.t option - ; size_sym_exp: Relation.SymExp.t option - ; relation: Relation.t - ; void_ptr: bool } + type t = {offset: ItvPure.t; idx: ItvPure.t; size: ItvPure.t; last_included: bool; void_ptr: bool} [@@deriving compare] let get_symbols c = @@ -218,10 +209,7 @@ module ArrayAccessCondition = struct in let cmp = if c.last_included then "<=" else "<" in F.fprintf fmt "%t%a %s %a" pp_offset ItvPure.pp c.idx cmp ItvPure.pp - (ItvPure.make_positive c.size) ; - if Option.is_some Config.bo_relational_domain then - F.fprintf fmt "@,%a %s %a when %a" Relation.SymExp.pp_opt c.idx_sym_exp cmp - Relation.SymExp.pp_opt c.size_sym_exp Relation.pp c.relation + (ItvPure.make_positive c.size) let pp_description : markup:bool -> F.formatter -> t -> unit = @@ -239,20 +227,12 @@ module ArrayAccessCondition = struct pp_offset (ItvPure.pp_mark ~markup) (ItvPure.make_positive c.size) - let make : - offset:ItvPure.t - -> idx:ItvPure.t - -> size:ItvPure.t - -> last_included:bool - -> idx_sym_exp:Relation.SymExp.t option - -> size_sym_exp:Relation.SymExp.t option - -> relation:Relation.t - -> t option = - fun ~offset ~idx ~size ~last_included ~idx_sym_exp ~size_sym_exp ~relation -> + let make : offset:ItvPure.t -> idx:ItvPure.t -> size:ItvPure.t -> last_included:bool -> t option = + fun ~offset ~idx ~size ~last_included -> if ItvPure.is_invalid offset || ItvPure.is_invalid idx || ItvPure.is_invalid size then None else let void_ptr = ItvPure.has_void_ptr_symb offset || ItvPure.has_void_ptr_symb size in - Some {offset; idx; size; last_included; idx_sym_exp; size_sym_exp; relation; void_ptr} + Some {offset; idx; size; last_included; void_ptr} let have_similar_bounds {offset= loff; idx= lidx; size= lsiz; last_included= lcol} @@ -365,14 +345,8 @@ module ArrayAccessCondition = struct if c.last_included then ItvPure.succ size_pos else size_pos in (* if sl < 0, use sl' = 0 *) - let not_overrun = - if Relation.lt_sat_opt c.idx_sym_exp c.size_sym_exp c.relation then Boolean.True - else ItvPure.lt_sem real_idx size - in - let not_underrun = - if Relation.le_sat_opt (Some Relation.SymExp.zero) c.idx_sym_exp c.relation then Boolean.True - else ItvPure.le_sem ItvPure.zero real_idx - in + let not_overrun = ItvPure.lt_sem real_idx size in + let not_underrun = ItvPure.le_sem ItvPure.zero real_idx in (* il >= 0 and iu < sl, definitely not an error *) if Boolean.is_true not_overrun && Boolean.is_true not_underrun then {report_issue_type= NotIssue; propagate= false} (* iu < 0 or il >= su, definitely an error *) @@ -400,30 +374,19 @@ module ArrayAccessCondition = struct {report_issue_type; propagate= is_symbolic} - let subst : Bound.eval_sym -> Relation.SubstMap.t -> Relation.t -> t -> t option = - fun eval_sym rel_map caller_relation c -> + let subst : Bound.eval_sym -> t -> t option = + fun eval_sym c -> match (ItvPure.subst c.offset eval_sym, ItvPure.subst c.idx eval_sym, ItvPure.subst c.size eval_sym) with | NonBottom offset, NonBottom idx, NonBottom size -> - let idx_sym_exp, size_sym_exp, relation = - if Option.is_none Config.bo_relational_domain then (None, None, Relation.bot) - else - ( Relation.SubstMap.symexp_subst_opt rel_map c.idx_sym_exp - , Relation.SubstMap.symexp_subst_opt rel_map c.size_sym_exp - , Relation.instantiate rel_map ~caller:caller_relation ~callee:c.relation ) - in let void_ptr = c.void_ptr || ItvPure.has_void_ptr_symb offset || ItvPure.has_void_ptr_symb idx || ItvPure.has_void_ptr_symb size in - Some {c with offset; idx; size; idx_sym_exp; size_sym_exp; relation; void_ptr} + Some {c with offset; idx; size; void_ptr} | _ -> None - - - let relation_forget_locs : AbsLoc.PowLoc.t -> t -> t = - fun locs c -> {c with relation= Relation.forget_locs locs c.relation} end module BinaryOperationCondition = struct @@ -631,11 +594,11 @@ module Condition = struct BinaryOperationCondition.get_symbols c - let subst eval_sym rel_map caller_relation = function + let subst eval_sym = function | AllocSize c -> AllocSizeCondition.subst eval_sym c |> make_alloc_size | ArrayAccess c -> - ArrayAccessCondition.subst eval_sym rel_map caller_relation c |> make_array_access + ArrayAccessCondition.subst eval_sym c |> make_array_access | BinaryOperation c -> BinaryOperationCondition.subst eval_sym c |> make_binary_operation @@ -701,14 +664,6 @@ module Condition = struct BinaryOperationCondition.check c trace - let relation_forget_locs locs x = - match x with - | ArrayAccess c -> - ArrayAccess (ArrayAccessCondition.relation_forget_locs locs c) - | AllocSize _ | BinaryOperation _ -> - x - - let is_array_access_of_void_ptr = function ArrayAccess {void_ptr} -> void_ptr | _ -> false end @@ -756,7 +711,7 @@ module ConditionWithTrace = struct else `NotComparable - let subst eval_sym_trace rel_map caller_relation callee_pname call_site cwt = + let subst eval_sym_trace callee_pname call_site cwt = let symbols = Condition.get_symbols cwt.cond in if Symb.SymbolSet.is_empty symbols then L.(die InternalError) @@ -770,7 +725,7 @@ module ConditionWithTrace = struct with | `Reachable reachability -> ( let {Dom.eval_sym; trace_of_sym} = eval_sym_trace ~mode:Sem.EvalPOCond in - match Condition.subst eval_sym rel_map caller_relation cwt.cond with + match Condition.subst eval_sym cwt.cond with | None -> None | Some cond -> @@ -834,7 +789,7 @@ module ConditionWithTrace = struct report cwt.cond cwt.trace issue_type - let for_summary ~relation_forget_locs = function + let for_summary = function | _, {propagate= false} | _, {report_issue_type= NotIssue} -> None | {cond; trace; reported; reachability}, {report_issue_type} -> @@ -847,7 +802,6 @@ module ConditionWithTrace = struct | Issue issue_type -> Some (Reported.make issue_type) in - let cond = Condition.relation_forget_locs relation_forget_locs cond in let trace = ConditionTrace.for_summary trace in Some {cond; trace; reported; reachability} end @@ -926,9 +880,9 @@ module ConditionSet = struct join_one condset (check_one cwt) - let add_array_access location ~offset ~idx ~size ~last_included ~idx_sym_exp ~size_sym_exp - ~relation ~idx_traces ~arr_traces ~latest_prune condset = - ArrayAccessCondition.make ~offset ~idx ~size ~last_included ~idx_sym_exp ~size_sym_exp ~relation + let add_array_access location ~offset ~idx ~size ~last_included ~idx_traces ~arr_traces + ~latest_prune condset = + ArrayAccessCondition.make ~offset ~idx ~size ~last_included |> Condition.make_array_access |> add_opt location (ValTrace.Issue.(binary location ArrayAccess) idx_traces arr_traces) @@ -950,13 +904,9 @@ module ConditionSet = struct latest_prune condset - let subst condset eval_sym_trace rel_subst_map caller_relation callee_pname call_site latest_prune - = + let subst condset eval_sym_trace callee_pname call_site latest_prune = let subst_add_cwt condset cwt = - match - ConditionWithTrace.subst eval_sym_trace rel_subst_map caller_relation callee_pname call_site - cwt - with + match ConditionWithTrace.subst eval_sym_trace callee_pname call_site cwt with | None -> condset | Some cwt -> @@ -970,9 +920,7 @@ module ConditionSet = struct List.iter condset ~f:(ConditionWithTrace.report_errors ~report) - let for_summary ~relation_forget_locs condset = - List.filter_map condset ~f:(ConditionWithTrace.for_summary ~relation_forget_locs) - + let for_summary condset = List.filter_map condset ~f:ConditionWithTrace.for_summary let pp_summary : F.formatter -> _ t0 -> unit = fun fmt condset -> diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli b/infer/src/bufferoverrun/bufferOverrunProofObligations.mli index 6e59bc513..ba6cbce8f 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.mli @@ -8,7 +8,6 @@ open! IStd open! AbstractDomain.Types module ItvPure = Itv.ItvPure -module Relation = BufferOverrunDomainRelation module Condition : sig type t @@ -39,9 +38,6 @@ module ConditionSet : sig -> idx:ItvPure.t -> size:ItvPure.t -> last_included:bool - -> idx_sym_exp:Relation.SymExp.t option - -> size_sym_exp:Relation.SymExp.t option - -> relation:Relation.t -> idx_traces:BufferOverrunTrace.Set.t -> arr_traces:BufferOverrunTrace.Set.t -> latest_prune:BufferOverrunDomain.LatestPrune.t @@ -74,8 +70,6 @@ module ConditionSet : sig val subst : summary_t -> (mode:BufferOverrunSemantics.eval_mode -> BufferOverrunDomain.eval_sym_trace) - -> Relation.SubstMap.t - -> Relation.t -> Typ.Procname.t -> Location.t -> BufferOverrunDomain.LatestPrune.t @@ -84,7 +78,7 @@ module ConditionSet : sig val report_errors : report:(Condition.t -> ConditionTrace.t -> IssueType.t -> unit) -> checked_t -> unit - val for_summary : relation_forget_locs:AbsLoc.PowLoc.t -> checked_t -> summary_t + val for_summary : checked_t -> summary_t end val description : markup:bool -> Condition.t -> ConditionTrace.t -> string diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 6c3f8dde9..1cfe4b06a 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -475,12 +475,6 @@ let mk_eval_sym_mode ~mode integer_type_widths callee_formals actual_exps caller let mk_eval_sym_cost = mk_eval_sym_mode ~mode:EvalCost -let get_sym_f integer_type_widths mem e = Val.get_sym (eval integer_type_widths e mem) - -let get_offset_sym_f integer_type_widths mem e = Val.get_offset_sym (eval integer_type_widths e mem) - -let get_size_sym_f integer_type_widths mem e = Val.get_size_sym (eval integer_type_widths e mem) - (* This function evaluates the array length conservatively, which is useful when there are multiple array locations and their lengths are joined to top. For example, if the [arr_locs] points to two arrays [a] and [b] and if their lengths are [a.length] and [b.length], this function @@ -732,9 +726,7 @@ module Prune = struct let prune_unreachable : Typ.IntegerWidths.t -> Exp.t -> t -> t = fun integer_type_widths e ({mem} as astate) -> - if is_unreachable_constant integer_type_widths e mem || Mem.is_relation_unsat mem then - {astate with mem= Mem.bot} - else astate + if is_unreachable_constant integer_type_widths e mem then {astate with mem= Mem.bot} else astate let rec prune_helper integer_type_widths e astate = @@ -779,129 +771,6 @@ module Prune = struct let prune : Typ.IntegerWidths.t -> Exp.t -> Mem.t -> Mem.t = fun integer_type_widths e mem -> let mem, prune_pairs = Mem.apply_latest_prune e mem in - let mem = - let constrs = Relation.Constraints.of_exp e ~get_sym_f:(get_sym_f integer_type_widths mem) in - Mem.meet_constraints constrs mem - in let {mem; prune_pairs} = prune_helper integer_type_widths e {mem; prune_pairs} in if PrunePairs.is_reachable prune_pairs then Mem.set_prune_pairs prune_pairs mem else Mem.bot end - -let get_matching_pairs : - Tenv.t - -> Typ.IntegerWidths.t - -> Val.t - -> Val.t - -> Exp.t option - -> Typ.t - -> Mem.t - -> _ Mem.t0 - -> (Relation.Var.t * Relation.SymExp.t option) list = - fun tenv integer_type_widths callee_v actual actual_exp_opt typ caller_mem callee_exit_mem -> - let get_offset_sym v = Val.get_offset_sym v in - let get_size_sym v = Val.get_size_sym v in - let get_field_name (fn, _, _) = fn in - let append_field v fn = PowLoc.append_field (Val.get_all_locs v) ~fn in - let deref_field v fn mem = Mem.find_set (append_field v fn) mem in - let deref_ptr v mem = - let array_locs = Val.get_array_locs v in - let locs = if PowLoc.is_empty array_locs then Val.get_pow_loc v else array_locs in - Mem.find_set locs mem - in - let add_pair_sym_main_value v1 v2 ~e2_opt l = - Option.value_map (Val.get_sym_var v1) ~default:l ~f:(fun var -> - let sym_exp_opt = - Option.first_some - (Relation.SymExp.of_exp_opt - ~get_sym_f:(get_sym_f integer_type_widths caller_mem) - e2_opt) - (Relation.SymExp.of_sym (Val.get_sym v2)) - in - (var, sym_exp_opt) :: l ) - in - let add_pair_sym s1 s2 l = - Option.value_map (Relation.Sym.get_var s1) ~default:l ~f:(fun var -> - (var, Relation.SymExp.of_sym s2) :: l ) - in - let add_pair_val v1 v2 ~e2_opt rel_pairs = - rel_pairs - |> add_pair_sym_main_value v1 v2 ~e2_opt - |> add_pair_sym (get_offset_sym v1) (get_offset_sym v2) - |> add_pair_sym (get_size_sym v1) (get_size_sym v2) - in - let add_pair_field v1 v2 pairs fn = - let v1' = deref_field v1 fn callee_exit_mem in - let v2' = deref_field v2 fn caller_mem in - add_pair_val v1' v2' ~e2_opt:None pairs - in - let add_pair_ptr typ v1 v2 pairs = - match typ.Typ.desc with - | Typ.Tptr ({desc= Tstruct typename}, _) -> ( - match Tenv.lookup tenv typename with - | Some str -> - let fns = List.map ~f:get_field_name str.Typ.Struct.fields in - List.fold ~f:(add_pair_field v1 v2) ~init:pairs fns - | _ -> - pairs ) - | Typ.Tptr (_, _) -> - let v1' = deref_ptr v1 callee_exit_mem in - let v2' = deref_ptr v2 caller_mem in - add_pair_val v1' v2' ~e2_opt:None pairs - | _ -> - pairs - in - [] |> add_pair_val callee_v actual ~e2_opt:actual_exp_opt |> add_pair_ptr typ callee_v actual - - -let subst_map_of_rel_pairs : (Relation.Var.t * Relation.SymExp.t option) list -> Relation.SubstMap.t - = - fun pairs -> - let add_pair rel_map (x, e) = Relation.SubstMap.add x e rel_map in - List.fold pairs ~init:Relation.SubstMap.empty ~f:add_pair - - -let rec list_fold2_def : - default:Val.t * Exp.t option - -> f:('a -> Val.t * Exp.t option -> 'b -> 'b) - -> 'a list - -> (Val.t * Exp.t option) list - -> init:'b - -> 'b = - fun ~default ~f xs ys ~init:acc -> - match (xs, ys) with - | [], _ -> - acc - | x :: xs', [] -> - list_fold2_def ~default ~f xs' ys ~init:(f x default acc) - | [x], _ :: _ -> - let v = List.fold ys ~init:Val.bot ~f:(fun acc (y, _) -> Val.join y acc) in - let exp_opt = match ys with [(_, exp_opt)] -> exp_opt | _ -> None in - f x (v, exp_opt) acc - | x :: xs', y :: ys' -> - list_fold2_def ~default ~f xs' ys' ~init:(f x y acc) - - -let get_subst_map : - Tenv.t - -> Typ.IntegerWidths.t - -> (Pvar.t * Typ.t) list - -> (Exp.t * 'a) list - -> Mem.t - -> _ Mem.t0 - -> Relation.SubstMap.t = - fun tenv integer_type_widths callee_formals params caller_mem callee_exit_mem -> - let add_pair (formal, typ) (actual, actual_exp) rel_l = - let callee_v = Mem.find (Loc.of_pvar formal) callee_exit_mem in - let new_rel_matching = - get_matching_pairs tenv integer_type_widths callee_v actual actual_exp typ caller_mem - callee_exit_mem - in - List.rev_append new_rel_matching rel_l - in - let actuals = - List.map ~f:(fun (a, _) -> (eval integer_type_widths a caller_mem, Some a)) params - in - let rel_pairs = - list_fold2_def ~default:(Val.Itv.top, None) ~f:add_pair callee_formals actuals ~init:[] - in - subst_map_of_rel_pairs rel_pairs diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index 0930f7366..e6caa6349 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -10,7 +10,6 @@ open AbsLoc open! AbstractDomain.Types module L = Logging module Dom = BufferOverrunDomain -module Relation = BufferOverrunDomainRelation module PO = BufferOverrunProofObligations module Sem = BufferOverrunSemantics module Trace = BufferOverrunTrace @@ -77,16 +76,15 @@ module Exec = struct Allocsite.make pname ~node_hash ~inst_num ~dimension ~path ~represents_multiple_values in let mem = - let arr, offset_opt = + let arr = let traces = Trace.(Set.singleton location ArrayDeclaration) in match Typ.Procname.get_language pname with | Language.Clang -> let offset = Itv.zero in - (Dom.Val.of_c_array_alloc allocsite ~stride ~offset ~size ~traces, Some offset) + Dom.Val.of_c_array_alloc allocsite ~stride ~offset ~size ~traces | Language.Java -> - (Dom.Val.of_java_array_alloc allocsite ~length:size ~traces, None) + Dom.Val.of_java_array_alloc allocsite ~length:size ~traces in - let mem = Dom.Mem.init_array_relation allocsite ~offset_opt ~size ~size_exp_opt:None mem in if Int.equal dimension 1 then Dom.Mem.add_stack ~represents_multiple_values loc arr mem else Dom.Mem.add_heap ~represents_multiple_values loc arr mem in @@ -128,8 +126,6 @@ module Exec = struct Dom.Val.of_c_array_alloc allocsite ~stride ~offset ~size ~traces in mem |> Dom.Mem.strong_update field_loc v - |> Dom.Mem.init_array_relation allocsite ~offset_opt:(Some offset) ~size - ~size_exp_opt:None | _ -> init_fields field_path field_typ field_loc dimension ?dyn_length mem in @@ -239,12 +235,12 @@ module Exec = struct end module Check = struct - let check_access ~size ~idx ~offset ~size_sym_exp ~idx_sym_exp ~relation ~arr_traces ~idx_traces - ~last_included ~latest_prune location cond_set = + let check_access ~size ~idx ~offset ~arr_traces ~idx_traces ~last_included ~latest_prune location + cond_set = match (size, idx) with | NonBottom length, NonBottom idx -> - PO.ConditionSet.add_array_access location ~size:length ~offset ~idx ~size_sym_exp - ~idx_sym_exp ~relation ~last_included ~idx_traces ~arr_traces ~latest_prune cond_set + PO.ConditionSet.add_array_access location ~size:length ~offset ~idx ~last_included + ~idx_traces ~arr_traces ~latest_prune cond_set | _ -> cond_set @@ -264,27 +260,19 @@ module Check = struct offset - let array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus ~last_included ~latest_prune location - cond_set = + let array_access ~arr ~idx ~is_plus ~last_included ~latest_prune location cond_set = let idx_traces = Dom.Val.get_traces idx in let idx = let idx_itv = Dom.Val.get_itv idx in if is_plus then idx_itv else Itv.neg idx_itv in let arr_traces = Dom.Val.get_traces arr in - let size_sym_exp = Relation.SymExp.of_sym (Dom.Val.get_size_sym arr) in - let idx_sym_exp = - let offset_sym_exp = Relation.SymExp.of_sym (Dom.Val.get_offset_sym arr) in - Option.map2 offset_sym_exp idx_sym_exp ~f:(fun offset_sym_exp idx_sym_exp -> - let op = if is_plus then Relation.SymExp.plus else Relation.SymExp.minus in - op idx_sym_exp offset_sym_exp ) - in let array_access1 allocsite arr_info acc = let size = ArrayBlk.ArrInfo.get_size arr_info in let offset = offsetof arr_info in log_array_access allocsite size offset idx ; - check_access ~size ~idx ~offset ~size_sym_exp ~idx_sym_exp ~relation ~arr_traces ~idx_traces - ~last_included ~latest_prune location acc + check_access ~size ~idx ~offset ~arr_traces ~idx_traces ~last_included ~latest_prune location + acc in ArrayBlk.fold array_access1 (Dom.Val.get_array_blk arr) cond_set @@ -297,17 +285,11 @@ module Check = struct if PowLoc.is_empty arr_locs then Dom.Val.Itv.top else Dom.Mem.find_set arr_locs mem else Sem.eval_arr integer_type_widths array_exp mem in - let idx_sym_exp = - Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f integer_type_widths mem) index_exp - in - let relation = Dom.Mem.get_relation mem in let latest_prune = Dom.Mem.get_latest_prune mem in - array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus:true ~last_included ~latest_prune - location cond_set + array_access ~arr ~idx ~is_plus:true ~last_included ~latest_prune location cond_set - let array_access_byte ~arr ~idx ~relation ~is_plus ~last_included ~latest_prune location cond_set - = + let array_access_byte ~arr ~idx ~is_plus ~last_included ~latest_prune location cond_set = let idx_traces = Dom.Val.get_traces idx in let idx = let idx_itv = Dom.Val.get_itv idx in @@ -318,8 +300,8 @@ module Check = struct let size = ArrayBlk.ArrInfo.byte_size arr_info in let offset = offsetof arr_info in log_array_access allocsite size offset idx ; - check_access ~size ~idx ~offset ~size_sym_exp:None ~idx_sym_exp:None ~relation ~arr_traces - ~idx_traces ~last_included ~latest_prune location acc + check_access ~size ~idx ~offset ~arr_traces ~idx_traces ~last_included ~latest_prune location + acc in ArrayBlk.fold array_access_byte1 (Dom.Val.get_array_blk arr) cond_set @@ -328,10 +310,8 @@ module Check = struct cond_set = let idx = Sem.eval integer_type_widths byte_index_exp mem in let arr = Sem.eval_arr integer_type_widths array_exp mem in - let relation = Dom.Mem.get_relation mem in let latest_prune = Dom.Mem.get_latest_prune mem in - array_access_byte ~arr ~idx ~relation ~is_plus:true ~last_included ~latest_prune location - cond_set + array_access_byte ~arr ~idx ~is_plus:true ~last_included ~latest_prune location cond_set let binary_operation integer_type_widths bop ~lhs ~rhs ~latest_prune location cond_set = diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.mli b/infer/src/bufferoverrun/bufferOverrunUtils.mli index becf079e7..4dbce6ec7 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.mli +++ b/infer/src/bufferoverrun/bufferOverrunUtils.mli @@ -8,7 +8,6 @@ open! IStd open AbsLoc module Dom = BufferOverrunDomain -module Relation = BufferOverrunDomainRelation module PO = BufferOverrunProofObligations module ModelEnv : sig @@ -56,8 +55,6 @@ module Check : sig val array_access : arr:Dom.Val.t -> idx:Dom.Val.t - -> idx_sym_exp:Relation.SymExp.t option - -> relation:Relation.t -> is_plus:bool -> last_included:bool -> latest_prune:Dom.LatestPrune.t diff --git a/infer/src/dune.common.in b/infer/src/dune.common.in index 67c05c37d..4ab00a8cc 100644 --- a/infer/src/dune.common.in +++ b/infer/src/dune.common.in @@ -66,15 +66,12 @@ let common_optflags = match build_mode with Opt -> ["-O3"] | Default | Test -> [ let common_libraries = (if java then ["javalib"; "sawja"] else []) @ [ "ANSITerminal" - ; "apron" - ; "apron.octMPQ" ; "async" ; "atdgen" ; "base" ; "base64" ; "cmdliner" ; "core" - ; "elina" ; "mtime.clock.os" ; "ocamlgraph" ; "oUnit" diff --git a/opam b/opam index 25d4733cf..f375607cf 100644 --- a/opam +++ b/opam @@ -21,20 +21,16 @@ install: [ ] depends: [ "ANSITerminal" {>="0.7"} - "apron" {<"v0.9.12"} "async" {>="v0.12.0" & < "v0.13"} "atdgen" {>="2.0.0"} "base64" {>="3.0.0"} "cmdliner" {>="1.0.0"} "core" {>="v0.12.0" & < "v0.13"} "conf-autoconf" {build} - "conf-gmp" {build} - "conf-mpfr" {build} "conf-sqlite3" {build} "conf-zlib" {build} "ctypes" {>="0.9.2"} "dune" {build & >="1.0"} - "elina" {>="1.1"} "javalib" {>="3.1.1"} "mlgmpidl" {>="1.2.12"} "mtime" diff --git a/opam.locked b/opam.locked index 33b355bba..e45110954 100644 --- a/opam.locked +++ b/opam.locked @@ -21,7 +21,6 @@ install: [ ] depends: [ "ANSITerminal" {= "0.8.1"} - "apron" {= "20160125"} "async" {= "v0.12.0"} "async_extra" {= "v0.12.0"} "async_kernel" {= "v0.12.0"} @@ -40,13 +39,11 @@ depends: [ "base_quickcheck" {= "v0.12.1"} "bin_prot" {= "v0.12.0"} "biniou" {= "1.2.1"} - "camlidl" {= "1.07"} "camlzip" {= "1.09"} "cmdliner" {= "1.0.4"} "conf-autoconf" {= "0.1"} "conf-gmp" {= "1"} "conf-m4" {= "1"} - "conf-mpfr" {= "1"} "conf-perl" {= "1"} "conf-pkg-config" {= "1.1"} "conf-sqlite3" {= "1"} @@ -59,7 +56,6 @@ depends: [ "dune" {= "1.11.4"} "dune-configurator" {= "1.0.0"} "easy-format" {= "1.3.2"} - "elina" {= "1.1"} "extlib" {= "1.7.6"} "fieldslib" {= "v0.12.0"} "integers" {= "0.3.0"} @@ -68,7 +64,6 @@ depends: [ "jbuilder" {= "transition"} "jst-config" {= "v0.12.0"} "menhir" {= "20190924"} - "mlgmpidl" {= "1.2.12"} "mtime" {= "1.2.0"} "num" {= "1.3"} "ocaml" {= "4.08.1"} diff --git a/scripts/create_binary_release.sh b/scripts/create_binary_release.sh index d73ed762f..bf46114a9 100755 --- a/scripts/create_binary_release.sh +++ b/scripts/create_binary_release.sh @@ -46,7 +46,7 @@ touch .release --prefix="/$RELEASE_NAME" make -j "$JOBS" \ - install-with-libs \ + install \ BUILD_MODE=opt \ DESTDIR="$ROOT_DIR" \ libdir_relative_to_bindir=../lib diff --git a/scripts/set_libso_path.sh b/scripts/set_libso_path.sh deleted file mode 100755 index 04af8ce68..000000000 --- a/scripts/set_libso_path.sh +++ /dev/null @@ -1,30 +0,0 @@ -#!/bin/bash - -# Copyright (c) Facebook, Inc. and its affiliates. -# -# This source code is licensed under the MIT license found in the -# LICENSE file in the root directory of this source tree. - -# Usage: set_libso_path.sh [LIBSO_DIR] [TARGET] -# -# This changes MacOSX's executable [TARGET] to use shared libraries in -# [LIBSO_DIR] when rpath has been set to [LIBSO_DIR]. - -set -e -set -o pipefail -set -u - -LIBSO_DIR=$1 -TARGET=$2 - -TMP=$( mktemp ) -trap "rm $TMP" EXIT - -otool -L "$TARGET" | tail -n +2 > "$TMP" -while IFS='' read -r line || [[ -n "$line" ]]; do - LIB_PATH=$( echo $line | awk '{print $1}' ) - LIB_FILE=$( basename "${LIB_PATH}" ) - if [ -f "${LIBSO_DIR}/${LIB_FILE}" ]; then - install_name_tool -change "${LIB_PATH}" "@rpath/${LIB_FILE}" "$TARGET" - fi -done < "$TMP"