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"