From 9eca72d4057e6f8fd093fb369be01a4b25fc89bb Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Tue, 31 Jul 2018 23:01:27 -0700 Subject: [PATCH] [Inferbo] Add relational domains Summary: It adds relational domains to Inferbo: octagon of Apron and polyhedra of Elina. - Each Mem domain value includes one relational value containing relations among symbols. The relational values are modified by the `Prune` and `Store` commands. - Each abstract value includes three symbols, which represent integer value, array offset, and array size of an abstract value. The relational domain is deactivated by default. Use the `--bo-relational-domain {oct, poly}` option for the activation, though Inferbo with the relational domains does not work at this point because some modifications of Apron and Elina we made has not been applied to their opam repositories yet. Reviewed By: jvillard Differential Revision: D8874102 fbshipit-source-id: 08e5883cb --- INSTALL.md | 4 +- Makefile.autoconf.in | 5 + configure.ac | 4 + infer/src/absint/AbstractInterpreter.ml | 2 +- infer/src/base/Config.ml | 9 + infer/src/base/Config.mli | 2 + infer/src/bufferoverrun/absLoc.ml | 11 + .../src/bufferoverrun/bufferOverrunChecker.ml | 76 +- .../src/bufferoverrun/bufferOverrunDomain.ml | 207 ++- .../bufferOverrunDomainRelation.ml | 1623 +++++++++++++++++ .../src/bufferoverrun/bufferOverrunModels.ml | 18 +- .../bufferOverrunProofObligations.ml | 95 +- .../bufferoverrun/bufferOverrunSemantics.ml | 115 +- infer/src/bufferoverrun/bufferOverrunUtils.ml | 55 +- .../src/bufferoverrun/bufferOverrunUtils.mli | 4 +- infer/src/bufferoverrun/itv.ml | 2 + infer/src/bufferoverrun/itv.mli | 2 + infer/src/checkers/cost.ml | 2 +- infer/src/dune.common.in | 3 + .../codetoanalyze/c/bufferoverrun/issues.exp | 4 + .../codetoanalyze/c/bufferoverrun/relation.c | 43 + opam | 4 + opam.lock | 7 + 23 files changed, 2162 insertions(+), 135 deletions(-) create mode 100644 infer/src/bufferoverrun/bufferOverrunDomainRelation.ml create mode 100644 infer/tests/codetoanalyze/c/bufferoverrun/relation.c diff --git a/INSTALL.md b/INSTALL.md index 5985e072d..8faeba4a8 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -24,12 +24,14 @@ is required to compile everything from source. `xcode-select --install` (only needed for the C/Objective-C analysis) - 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 +brew install autoconf automake cmake opam pkg-config sqlite gmp mpfr brew cask install java ``` diff --git a/Makefile.autoconf.in b/Makefile.autoconf.in index 4faf1d9dd..716ebff6c 100644 --- a/Makefile.autoconf.in +++ b/Makefile.autoconf.in @@ -18,6 +18,7 @@ CFLAGS = @CFLAGS@ CLANG_INCLUDES = @CLANG_INCLUDES@ CLANG_PREFIX = @CLANG_PREFIX@ CMAKE = @CMAKE@ +CPATH = @CPATH@ CPP = @CPP@ CXX = @CXX@ CXXFLAGS = @CXXFLAGS@ @@ -42,6 +43,7 @@ LDFLAGS = @LDFLAGS@ libdir = @libdir@ # override in your `make` command to make the install relocatable libdir_relative_to_bindir = $(libdir) +LIBRARY_PATH = @LIBRARY_PATH@ LIBS = @LIBS@ mandir = @mandir@ MENHIR = @MENHIR@ @@ -61,6 +63,7 @@ OCAMLOPT = @OCAMLOPT@ OPAM = @OPAM@ OPAMROOT = @OPAMROOT@ OPAMSWITCH = @OPAMSWITCH@ +PATCHELF = @PATCHELF@ PATH = @PATH@ prefix = @prefix@ PYTHON_lxml = @PYTHON_lxml@ @@ -79,5 +82,7 @@ endif # Export parts of the config relevant to running other programs export PATH := $(PATH) +export CPATH := $(CPATH) +export LIBRARY_PATH := $(LIBRARY_PATH) export CAML_LD_LIBRARY_PATH := $(CAML_LD_LIBRARY_PATH) export OPAMROOT := $(OPAMROOT) diff --git a/configure.ac b/configure.ac index 2b1b8cd2b..265c9b2a5 100644 --- a/configure.ac +++ b/configure.ac @@ -192,6 +192,8 @@ AC_ASSERT_OCAML_PKG([oUnit], [], [2.0.0]) AC_CHECK_TOOL([UTOP], [utop], [no]) AC_ASSERT_OCAML_PKG([yojson]) +AC_ARG_VAR([CPATH], [Additional directories to search for C headers.]) +AC_ARG_VAR([LIBRARY_PATH], [Additional directories to search for C shared objects.]) AC_ARG_VAR([CAML_LD_LIBRARY_PATH], [Additional directories to search for dynamically-loaded libraries.]) AC_ARG_VAR([OPAMROOT], [Root of the local opam installation.]) @@ -324,6 +326,8 @@ AC_SUBST([GNU_SED]) AC_CHECK_TOOL([BREW], [brew], [no]) +AC_CHECK_TOOL([PATCHELF], [patchelf], [no]) + # warn about broken pkg-config version for brew users if test "$BREW" != "no"; then if "$BREW" info pkg-config > /dev/null && \ diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index bfc9a27e5..7a0ff2acf 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/infer/src/absint/AbstractInterpreter.ml @@ -93,7 +93,7 @@ struct in if debug then ( L.d_strln - (Format.asprintf "PRE: %a@.INSTRS: %aPOST: %a@." Domain.pp pre + (Format.asprintf "@[PRE: %a@]@\n@[INSTRS: %a@]@[POST: %a@]@." Domain.pp pre (Instrs.pp Pp.(html Green)) instrs Domain.pp astate_post) ; NodePrinter.finish_session (Node.underlying_node node) ) ; diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 929f9dd2d..dc8bbc7a6 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -821,6 +821,13 @@ and blacklist = ~meta:"regex" "Skip analysis of files matched by the specified regular expression" +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)] @@ -2443,6 +2450,8 @@ and bootclasspath = !bootclasspath and bo_debug = !bo_debug +and bo_relational_domain = !bo_relational_domain + and buck = !buck and buck_build_args = !buck_build_args diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 8d44d129e..0f55c7c34 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -240,6 +240,8 @@ val bootclasspath : string option val bo_debug : int +val bo_relational_domain : [`Bo_relational_domain_oct | `Bo_relational_domain_poly] option + val buck : bool val buck_build_args : string list diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml index 5940c7e49..1b6f2023e 100644 --- a/infer/src/bufferoverrun/absLoc.ml +++ b/infer/src/bufferoverrun/absLoc.ml @@ -42,6 +42,8 @@ module Loc = struct F.fprintf fmt "%a.%a" pp l Typ.Fieldname.pp f + let to_string x = F.asprintf "%a" pp x + let is_var = function Var _ -> true | _ -> false let rec contains_allocsite = function @@ -89,3 +91,12 @@ module PowLoc = struct let is_singleton x = Int.equal (cardinal x) 1 end + +(** unsound but ok for bug catching *) +let always_strong_update = true + +let can_strong_update : PowLoc.t -> bool = + fun ploc -> + if always_strong_update then true + else if Int.equal (PowLoc.cardinal ploc) 1 then Loc.is_var (PowLoc.choose ploc) + else false diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index af2df4a13..212c8b42c 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -13,6 +13,7 @@ open AbsLoc open! AbstractDomain.Types module BoUtils = BufferOverrunUtils module Dom = BufferOverrunDomain +module Relation = BufferOverrunDomainRelation module L = Logging module Models = BufferOverrunModels module Sem = BufferOverrunSemantics @@ -47,16 +48,16 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Typ.Tint ikind -> let unsigned = Typ.ikind_is_unsigned ikind in let v = - Dom.Val.make_sym ~unsigned pname path new_sym_num + Dom.Val.make_sym ~unsigned loc pname path new_sym_num |> Dom.Val.add_trace_elem (Trace.SymAssign (loc, location)) in - Dom.Mem.add_heap loc v mem + mem |> Dom.Mem.add_heap loc v |> Dom.Mem.init_param_relation loc | Typ.Tfloat _ -> let v = - Dom.Val.make_sym pname path new_sym_num + Dom.Val.make_sym loc pname path new_sym_num |> Dom.Val.add_trace_elem (Trace.SymAssign (loc, location)) in - Dom.Mem.add_heap loc v mem + mem |> Dom.Mem.add_heap loc v |> Dom.Mem.init_param_relation loc | Typ.Tptr (typ, _) when Language.curr_language_is Java && not (Typ.is_array typ) -> BoUtils.Exec.decl_sym_java_ptr ~decl_sym_val:(decl_sym_val ~may_last_field:false) @@ -186,6 +187,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct try List.fold2_exn formals actuals ~init:mem ~f with Invalid_argument _ -> mem + 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.forget_locs (PowLoc.add ret_loc (PowLoc.singleton ret_var)) mem + + let instantiate_mem : Tenv.t -> Ident.t * Typ.t -> Procdesc.t option -> Typ.Procname.t -> (Exp.t * Typ.t) list -> Dom.Mem.astate -> Dom.Summary.t -> Location.t -> Dom.Mem.astate = @@ -195,12 +202,17 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let callee_ret_alias = Dom.Mem.find_ret_alias callee_exit_mem in match callee_pdesc with | Some pdesc -> - let subst_map, ret_alias = + let bound_subst_map, ret_alias, rel_subst_map = Sem.get_subst_map tenv pdesc params caller_mem callee_entry_mem ~callee_ret_alias in - instantiate_ret ret callee_pname ~callee_entry_mem ~callee_exit_mem subst_map caller_mem - ret_alias location - |> instantiate_param tenv pdesc params callee_entry_mem callee_exit_mem subst_map location + let caller_mem = + instantiate_ret ret callee_pname ~callee_entry_mem ~callee_exit_mem bound_subst_map + caller_mem ret_alias location + |> instantiate_param tenv pdesc params callee_entry_mem callee_exit_mem bound_subst_map + location + |> forget_ret_relation ret callee_pname + in + Dom.Mem.instantiate_relation rel_subst_map ~caller:caller_mem ~callee:callee_exit_mem | None -> caller_mem @@ -228,6 +240,14 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Store (exp1, _, exp2, location) -> let locs = Sem.eval exp1 mem |> Dom.Val.get_all_locs in let v = Sem.eval exp2 mem |> Dom.Val.add_trace_elem (Trace.Assign location) in + let mem = + let sym_exps = + Dom.Relation.SymExp.of_exps ~get_int_sym_f:(Sem.get_sym_f mem) + ~get_offset_sym_f:(Sem.get_offset_sym_f mem) + ~get_size_sym_f:(Sem.get_size_sym_f 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 PowLoc.is_singleton locs then @@ -368,7 +388,9 @@ module Report = struct fun pname ~is_plus ~e1 ~e2 location mem cond_set -> let arr = Sem.eval e1 mem in let idx = Sem.eval e2 mem in - BoUtils.Check.array_access ~arr ~idx ~is_plus pname location cond_set + let idx_sym_exp = Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f mem) e2 in + let relation = Dom.Mem.get_relation mem in + BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus pname location cond_set let check_binop @@ -407,7 +429,10 @@ module Report = struct match exp with | Exp.Var _ -> let arr = Sem.eval exp mem in - BoUtils.Check.array_access ~arr ~idx:Dom.Val.Itv.zero ~is_plus:true pname location cond_set + let idx, idx_sym_exp = (Dom.Val.Itv.zero, Some Relation.SymExp.zero) in + let relation = Dom.Mem.get_relation mem in + BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus:true pname location + cond_set | Exp.BinOp (bop, e1, e2) -> check_binop pname ~bop ~e1 ~e2 location mem cond_set | _ -> @@ -422,11 +447,13 @@ module Report = struct let callee_cond = Dom.Summary.get_cond_set summary in match callee_pdesc with | Some pdesc -> - let subst_map, _ = + let bound_subst_map, _, rel_subst_map = Sem.get_subst_map tenv pdesc params caller_mem callee_entry_mem ~callee_ret_alias:None in let pname = Procdesc.get_proc_name pdesc in - PO.ConditionSet.subst callee_cond subst_map caller_pname pname location + let caller_rel = Dom.Mem.get_relation caller_mem in + PO.ConditionSet.subst callee_cond bound_subst_map rel_subst_map caller_rel caller_pname + pname location | _ -> callee_cond @@ -562,6 +589,9 @@ module Report = struct Reporting.log_error summary ~loc:location ~ltr:trace exn in PO.ConditionSet.check_all ~report cond_set + + + let forget_locs = PO.ConditionSet.forget_locs end let extract_pre = Analyzer.extract_pre @@ -574,16 +604,34 @@ let print_summary : Typ.Procname.t -> Dom.Summary.t -> unit = "@\n@[Summary of %a:@,%a@]@." Typ.Procname.pp proc_name Dom.Summary.pp_summary s +let get_local_decls cfg = + let accum_pvar_list acc pvars = + List.fold pvars ~init:acc ~f:(fun acc (pvar, _) -> PowLoc.add (Loc.of_pvar pvar) acc) + in + let accum_decls_of_instr acc instr = + match instr with Sil.Declare_locals (vars, _) -> accum_pvar_list acc vars | _ -> acc + in + let accum_decls_of_node acc node = + Instrs.fold (CFG.instrs node) ~init:acc ~f:accum_decls_of_instr + in + let decls = CFG.fold_nodes cfg ~init:PowLoc.empty ~f:accum_decls_of_node in + let ret_loc = Loc.of_pvar (Pvar.get_ret_pvar (Procdesc.get_proc_name cfg)) in + PowLoc.remove ret_loc decls + + let compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_map * Summary.t = fun {proc_desc; tenv; summary} -> Preanal.do_preanalysis proc_desc tenv ; let pdata = ProcData.make_default proc_desc tenv in let inv_map = Analyzer.exec_pdesc ~initial:Dom.Mem.init pdata in let cfg = CFG.from_pdesc proc_desc in - let entry_mem = extract_post (CFG.start_node cfg |> CFG.Node.id) inv_map in - let exit_mem = extract_post (CFG.exit_node cfg |> CFG.Node.id) inv_map in + let locals = get_local_decls cfg in + let forget_locals mem = Option.map ~f:(Dom.Mem.forget_locs locals) mem in + let entry_mem = extract_post (CFG.start_node cfg |> CFG.Node.id) inv_map |> forget_locals in + let exit_mem = extract_post (CFG.exit_node cfg |> CFG.Node.id) inv_map |> forget_locals in let cond_set = Report.check_proc summary proc_desc tenv cfg inv_map |> Report.report_errors summary proc_desc + |> Report.forget_locs locals in let summary = match (entry_mem, exit_mem) with diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 57a07504c..c9bbde66e 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -13,31 +13,54 @@ open AbsLoc open! AbstractDomain.Types module F = Format module L = Logging +module Relation = BufferOverrunDomainRelation module PO = BufferOverrunProofObligations module Trace = BufferOverrunTrace module TraceSet = Trace.Set -(** unsound but ok for bug catching *) -let always_strong_update = true - module Val = struct type astate = - {itv: Itv.astate; powloc: PowLoc.astate; arrayblk: ArrayBlk.astate; traces: TraceSet.t} + { itv: Itv.astate + ; sym: Relation.Sym.astate + ; powloc: PowLoc.astate + ; arrayblk: ArrayBlk.astate + ; offset_sym: Relation.Sym.astate + ; size_sym: Relation.Sym.astate + ; traces: TraceSet.t } type t = astate - let bot : t = {itv= Itv.bot; powloc= PowLoc.bot; arrayblk= ArrayBlk.bot; traces= TraceSet.empty} + let bot : t = + { itv= Itv.bot + ; sym= Relation.Sym.bot + ; powloc= PowLoc.bot + ; arrayblk= ArrayBlk.bot + ; offset_sym= Relation.Sym.bot + ; size_sym= Relation.Sym.bot + ; traces= TraceSet.empty } + let pp fmt x = - if Config.bo_debug <= 1 then - F.fprintf fmt "(%a, %a, %a)" Itv.pp x.itv PowLoc.pp x.powloc ArrayBlk.pp x.arrayblk - else - F.fprintf fmt "(%a, %a, %a, %a)" Itv.pp x.itv PowLoc.pp x.powloc ArrayBlk.pp x.arrayblk - TraceSet.pp x.traces + 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 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)" Itv.pp x.itv relation_sym_pp x.sym PowLoc.pp x.powloc + ArrayBlk.pp x.arrayblk relation_sym_pp x.offset_sym relation_sym_pp x.size_sym trace_pp + x.traces let unknown : traces:TraceSet.t -> t = - fun ~traces -> {itv= Itv.top; powloc= PowLoc.unknown; arrayblk= ArrayBlk.unknown; traces} + fun ~traces -> + { itv= Itv.top + ; sym= Relation.Sym.top + ; powloc= PowLoc.unknown + ; arrayblk= ArrayBlk.unknown + ; offset_sym= Relation.Sym.top + ; size_sym= Relation.Sym.top + ; traces } let unknown_from : callee_pname:_ -> location:_ -> t = @@ -51,8 +74,11 @@ module Val = struct let ( <= ) ~lhs ~rhs = if phys_equal lhs rhs then true else - Itv.( <= ) ~lhs:lhs.itv ~rhs:rhs.itv && PowLoc.( <= ) ~lhs:lhs.powloc ~rhs:rhs.powloc + Itv.( <= ) ~lhs:lhs.itv ~rhs:rhs.itv && Relation.Sym.( <= ) ~lhs:lhs.sym ~rhs:rhs.sym + && PowLoc.( <= ) ~lhs:lhs.powloc ~rhs:rhs.powloc && ArrayBlk.( <= ) ~lhs:lhs.arrayblk ~rhs:rhs.arrayblk + && Relation.Sym.( <= ) ~lhs:lhs.offset_sym ~rhs:rhs.offset_sym + && Relation.Sym.( <= ) ~lhs:lhs.size_sym ~rhs:rhs.size_sym let equal x y = phys_equal x y || (( <= ) ~lhs:x ~rhs:y && ( <= ) ~lhs:y ~rhs:x) @@ -61,8 +87,11 @@ module Val = struct if phys_equal prev next then prev else { itv= Itv.widen ~prev:prev.itv ~next:next.itv ~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 } @@ -71,13 +100,20 @@ module Val = struct if phys_equal x y then x else { itv= Itv.join x.itv y.itv + ; 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 } let get_itv : t -> Itv.t = fun x -> x.itv + let get_sym : t -> Relation.Sym.astate = 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.astate = fun x -> x.arrayblk @@ -86,6 +122,10 @@ 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.astate = fun x -> x.offset_sym + + let get_size_sym : t -> Relation.Sym.astate = fun x -> x.size_sym + let get_traces : t -> TraceSet.t = fun x -> x.traces let set_traces : TraceSet.t -> t -> t = fun traces x -> {x with traces} @@ -96,20 +136,29 @@ module Val = struct let of_pow_loc : PowLoc.t -> t = fun x -> {bot with powloc= x} - let of_array_blk : ArrayBlk.astate -> t = fun a -> {bot with arrayblk= a} + let of_array_blk : allocsite:Allocsite.t -> ArrayBlk.astate -> t = + fun ~allocsite a -> + { bot with + arrayblk= a + ; offset_sym= Relation.Sym.of_allocsite_offset allocsite + ; size_sym= Relation.Sym.of_allocsite_size allocsite } + let modify_itv : Itv.t -> t -> t = fun i x -> {x with itv= i} - let make_sym : ?unsigned:bool -> Typ.Procname.t -> Itv.SymbolPath.partial -> Itv.Counter.t -> t = - fun ?(unsigned= false) pname path new_sym_num -> - {bot with itv= Itv.make_sym ~unsigned pname (Itv.SymbolPath.normal path) new_sym_num} + let make_sym + : ?unsigned:bool -> Loc.t -> Typ.Procname.t -> Itv.SymbolPath.partial -> Itv.Counter.t -> t = + fun ?(unsigned= false) loc pname path new_sym_num -> + { bot with + itv= Itv.make_sym ~unsigned pname (Itv.SymbolPath.normal path) new_sym_num + ; sym= Relation.Sym.of_loc loc } - let unknown_bit : t -> t = fun x -> {x with itv= Itv.top} + let unknown_bit : t -> t = fun x -> {x with itv= Itv.top; sym= Relation.Sym.top} - let neg : t -> t = fun x -> {x with itv= Itv.neg x.itv} + let neg : t -> t = fun x -> {x with itv= Itv.neg x.itv; sym= Relation.Sym.top} - let lnot : t -> t = fun x -> {x with itv= Itv.lnot x.itv |> Itv.of_bool} + let lnot : t -> t = fun x -> {x with itv= Itv.lnot x.itv |> Itv.of_bool; sym= Relation.Sym.top} let lift_itv : (Itv.t -> Itv.t -> Itv.t) -> t -> t -> t = fun f x y -> {bot with itv= f x.itv y.itv; traces= TraceSet.join x.traces y.traces} @@ -297,6 +346,15 @@ module Heap = struct fun ~f locs mem -> PowLoc.fold (fun loc -> find loc mem |> f |> add loc) locs mem + let add x v = + let sym = if Itv.is_empty (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 + add x {v with Val.sym; Val.offset_sym; Val.size_sym} + + let strong_update : PowLoc.t -> Val.t -> astate -> astate = fun locs v mem -> PowLoc.fold (fun x -> add x v) locs mem @@ -398,10 +456,9 @@ module AliasMap = struct let pp_sep fmt () = F.fprintf fmt ", @," in let pp1 fmt (k, v) = F.fprintf fmt "%a=%a" Ident.pp k AliasTarget.pp v in (* F.fprintf fmt "@[Logical Variables :@,"; *) - F.fprintf fmt "@[{ @," ; + F.fprintf fmt "@[{ " ; F.pp_print_list ~pp_sep pp1 fmt (M.bindings x) ; - F.fprintf fmt " }@]" ; - F.fprintf fmt "@]" + F.fprintf fmt " }@]" let load : Ident.t -> AliasTarget.t -> t -> t = fun id loc m -> M.add id loc m @@ -508,7 +565,7 @@ module Alias = struct let pp : F.formatter -> astate -> unit = fun fmt (aliasmap, aliasret) -> - F.fprintf fmt "AliasMap:@;%a@;AliasRet:@;%a@;" AliasMap.pp aliasmap AliasRet.pp aliasret + F.fprintf fmt "AliasMap:@;%a@;AliasRet:@;%a" AliasMap.pp aliasmap AliasRet.pp aliasret end module PrunePairs = struct @@ -595,11 +652,21 @@ end module MemReach = struct type astate = - {stack: Stack.astate; heap: Heap.astate; alias: Alias.astate; latest_prune: LatestPrune.astate} + { stack: Stack.astate + ; heap: Heap.astate + ; alias: Alias.astate + ; latest_prune: LatestPrune.astate + ; relation: Relation.astate } type t = astate - let init : t = {stack= Stack.bot; heap= Heap.bot; alias= Alias.bot; latest_prune= LatestPrune.top} + let init : t = + { stack= Stack.bot + ; heap= Heap.bot + ; alias= Alias.bot + ; latest_prune= LatestPrune.top + ; relation= Relation.empty } + let ( <= ) ~lhs ~rhs = if phys_equal lhs rhs then true @@ -607,6 +674,7 @@ module MemReach = struct Stack.( <= ) ~lhs:lhs.stack ~rhs:rhs.stack && Heap.( <= ) ~lhs:lhs.heap ~rhs:rhs.heap && Alias.( <= ) ~lhs:lhs.alias ~rhs:rhs.alias && LatestPrune.( <= ) ~lhs:lhs.latest_prune ~rhs:rhs.latest_prune + && Relation.( <= ) ~lhs:lhs.relation ~rhs:rhs.relation let widen ~prev ~next ~num_iters = @@ -616,7 +684,7 @@ module MemReach = struct ; heap= Heap.widen ~prev:prev.heap ~next:next.heap ~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 } let join : t -> t -> t = @@ -624,12 +692,15 @@ module MemReach = struct { stack= Stack.join x.stack y.stack ; heap= Heap.join x.heap y.heap ; alias= Alias.join x.alias y.alias - ; latest_prune= LatestPrune.join x.latest_prune y.latest_prune } + ; latest_prune= LatestPrune.join x.latest_prune y.latest_prune + ; relation= Relation.join x.relation y.relation } let pp : F.formatter -> t -> unit = fun fmt x -> - F.fprintf fmt "Stack:@;%a@;Heap:@;%a@;%a" Stack.pp x.stack Heap.pp x.heap Alias.pp x.alias + F.fprintf fmt "Stack:@;%a@;Heap:@;%a@;%a" Stack.pp x.stack Heap.pp x.heap Alias.pp x.alias ; + if Option.is_some Config.bo_relational_domain then + F.fprintf fmt "@;Relation:@;%a" Relation.pp x.relation let pp_summary : F.formatter -> t -> unit = @@ -691,13 +762,6 @@ module MemReach = struct let get_return : t -> Val.t = fun m -> Heap.get_return m.heap - let can_strong_update : PowLoc.t -> bool = - fun ploc -> - if always_strong_update then true - else if Int.equal (PowLoc.cardinal ploc) 1 then Loc.is_var (PowLoc.choose ploc) - else false - - let update_mem : PowLoc.t -> Val.t -> t -> t = fun ploc v s -> if can_strong_update ploc then strong_update_heap ploc v s @@ -770,6 +834,41 @@ module MemReach = struct let heap_range : filter_loc:(Loc.t -> bool) -> t -> Itv.NonNegativePolynomial.astate = fun ~filter_loc {heap} -> Heap.range ~filter_loc heap + + + let get_relation : t -> Relation.astate = fun m -> m.relation + + let is_relation_unsat : t -> bool = fun m -> Relation.is_unsat m.relation + + let lift_relation : (Relation.astate -> Relation.astate) -> 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 forget_locs : PowLoc.t -> t -> t = fun locs -> lift_relation (Relation.forget_locs locs) + + let init_param_relation : Loc.t -> t -> t = fun loc -> lift_relation (Relation.init_param loc) + + let init_array_relation + : Allocsite.t -> offset:Itv.t -> size:Itv.t -> size_exp_opt:Relation.SymExp.t option -> t + -> t = + fun allocsite ~offset ~size ~size_exp_opt -> + lift_relation (Relation.init_array allocsite ~offset ~size ~size_exp_opt) + + + let instantiate_relation : Relation.SubstMap.t -> caller:t -> callee:t -> t = + fun subst_map ~caller ~callee -> + { caller with + relation= Relation.instantiate subst_map ~caller:caller.relation ~callee:callee.relation } end module Mem = struct @@ -896,6 +995,42 @@ module Mem = struct let update_latest_prune : Exp.t -> Exp.t -> t -> t = fun e1 e2 -> f_lift (MemReach.update_latest_prune e1 e2) + + + let get_relation : t -> Relation.astate = + fun m -> f_lift_default ~default:Relation.bot MemReach.get_relation m + + + let meet_constraints : Relation.Constraints.t -> t -> t = + fun constrs -> f_lift (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 -> f_lift (MemReach.store_relation locs symexp_opts) + + + let forget_locs : PowLoc.t -> t -> t = fun locs -> f_lift (MemReach.forget_locs locs) + + let init_param_relation : Loc.t -> t -> t = fun loc -> f_lift (MemReach.init_param_relation loc) + + let init_array_relation + : Allocsite.t -> offset:Itv.t -> size:Itv.t -> size_exp_opt:Relation.SymExp.t option -> t + -> t = + fun allocsite ~offset ~size ~size_exp_opt -> + f_lift (MemReach.init_array_relation allocsite ~offset ~size ~size_exp_opt) + + + let instantiate_relation : Relation.SubstMap.t -> caller:t -> callee:t -> t = + fun subst_map ~caller ~callee -> + match callee with + | Bottom -> + caller + | NonBottom callee -> + f_lift (fun caller -> MemReach.instantiate_relation subst_map ~caller ~callee) caller end module Summary = struct @@ -923,5 +1058,5 @@ module Summary = struct let pp : F.formatter -> t -> unit = fun fmt (entry_mem, exit_mem, condition_set) -> - F.fprintf fmt "%a@,%a@,%a@," Mem.pp entry_mem Mem.pp exit_mem PO.ConditionSet.pp condition_set + F.fprintf fmt "%a@;%a@;%a" Mem.pp entry_mem Mem.pp exit_mem PO.ConditionSet.pp condition_set end diff --git a/infer/src/bufferoverrun/bufferOverrunDomainRelation.ml b/infer/src/bufferoverrun/bufferOverrunDomainRelation.ml new file mode 100644 index 000000000..cf6097359 --- /dev/null +++ b/infer/src/bufferoverrun/bufferOverrunDomainRelation.ml @@ -0,0 +1,1623 @@ +(* + * Copyright (c) 2018-present, Facebook, Inc. + * + * 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 : astate + + val top : astate + + val of_loc : Loc.t -> astate + + val of_loc_offset : Loc.t -> astate + + val of_loc_size : Loc.t -> astate + + val of_allocsite_offset : Allocsite.t -> astate + + val of_allocsite_size : Allocsite.t -> astate + + val get_var : astate -> 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.astate -> t option + + val of_exp : get_sym_f:(Exp.t -> Sym.astate) -> Exp.t -> t option + + val of_exps : + get_int_sym_f:(Exp.t -> Sym.astate) -> get_offset_sym_f:(Exp.t -> Sym.astate) + -> get_size_sym_f:(Exp.t -> Sym.astate) -> Exp.t -> t option * t option * t option + + val of_exp_opt : get_sym_f:(Exp.t -> Sym.astate) -> 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.astate) -> 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_astate : astate -> astate -> int + + val empty : astate + + val bot : astate + + val is_unsat : astate -> bool + + val lt_sat_opt : SymExp.t option -> SymExp.t option -> astate -> bool + + val le_sat_opt : SymExp.t option -> SymExp.t option -> astate -> bool + + val meet_constraints : Constraints.t -> astate -> astate + + val store_relation : + PowLoc.t -> SymExp.t option * SymExp.t option * SymExp.t option -> astate -> astate + + val init_param : Loc.t -> astate -> astate + + val init_array : + Allocsite.t -> offset:Itv.t -> size:Itv.t -> size_exp_opt:SymExp.t option -> astate -> astate + + val forget_locs : PowLoc.t -> astate -> astate + + val instantiate : caller:astate -> callee:astate -> SubstMap.t -> astate +end + +module NoRelation = struct + module UnitDom = struct + type astate = unit [@@deriving compare] + + type t = astate [@@deriving compare] + + let compare_astate _ _ = 0 + + let f1 _ = () + + let f2 _ _ = () + + let f3 _ _ _ = () + + let f1_none _ = None + + let f2_none _ _ = None + + let f1_false _ = false + + let f3_false _ _ _ = false + + let ( <= ) ~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:_ ~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 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 + type astate = Bot | V of Var.t | Top [@@deriving compare] + + let ( <= ) ~lhs ~rhs = + match (lhs, rhs) with + | Bot, _ -> + true + | _, Bot -> + false + | _, Top -> + true + | Top, _ -> + false + | V x, V y -> + Int.equal (Var.compare x y) 0 + + + let join x y = + match (x, y) with + | Bot, a | a, Bot -> + a + | _, Top | Top, _ -> + Top + | V x', V y' -> + if Int.equal (Var.compare x' y') 0 then x else Top + + + let widen ~prev ~next ~num_iters:_ = join prev next + + let pp fmt = function + | Bot -> + F.fprintf fmt "_|_" + | Top -> + F.fprintf fmt "T" + | V x -> + Var.pp fmt x + + + let bot = Bot + + let top = Top + + 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 = function V x -> Some x | Bot | Top -> None + 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 = match get_sym_f e with Sym.V x -> Some (Texpr1.Var x) | _ -> None 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 = + match get_offset_sym_f e with Sym.V x -> Some (Texpr1.Var x) | _ -> None + 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 = + match get_size_sym_f e with Sym.V x -> Some (Texpr1.Var x) | _ -> None + 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_int i = Texpr1.cst Env.empty (Coeff.s_of_int i) + + let zero = of_int 0 + + let one = of_int 1 + + let of_sym s = match s with Sym.V x -> Some (of_raw (Texpr1.Var x)) | _ -> None + + 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 = + if Itv.is_empty itv then empty + else + let lb, ub = (Itv.lb itv, Itv.ub itv) in + Option.value_map (SymExp.of_sym sym) ~default:empty ~f:(fun sym_exp -> + let tcons_lb = + Option.map (Itv.Bound.is_const lb) ~f:(fun lb -> + let sym_minus_lb = SymExp.minus sym_exp (SymExp.of_int lb) in + Tcons1.make sym_minus_lb Tcons1.SUPEQ ) + in + let tcons_ub = + Option.map (Itv.Bound.is_const ub) ~f:(fun ub -> + let ub_minus_sym = SymExp.minus (SymExp.of_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 with Sym.V x -> of_raw_symexp (Texpr1.Var x) Tcons1.DISEQ | _ -> 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 astate = Manager.domain_t Abstract1.t + + let compare_astate = 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 ( <= ) ~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 -> astate -> astate = + 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 astate = {pack_ids: Pack.t VarMap.t; packs: Val.astate 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.( <= ) ~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 ( <= ) ~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 + let num_vars_ids = PackSet.cardinal vars_ids in + if Int.equal num_vars_ids 0 then + let id = get_new_id () in + {x with pack_ids= set_pack_id_of_vars vars id x.pack_ids} + else if Int.equal num_vars_ids 1 then + let id = PackSet.choose vars_ids in + {x with pack_ids= set_pack_id_of_vars vars id x.pack_ids} + else + 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 ~size ~size_exp_opt x = + let offset_sym = Sym.of_allocsite_offset allocsite in + let size_sym = Sym.of_allocsite_size allocsite in + let offset_constrs = Constraints.itv_of offset_sym offset 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 + meet_constraints (Constraints.and_ offset_constrs size_constrs) 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_astate x y = + match (x, y) with + | Bottom, Bottom -> + 0 + | Bottom, _ -> + -1 + | _, Bottom -> + 1 + | NonBottom x', NonBottom y' -> + PackedVal.compare_astate x' y' + + + let empty : astate = NonBottom PackedVal.empty + + let bot : astate = Bottom + + let is_unsat : astate -> bool = function Bottom -> true | NonBottom _ -> false + + let lift_default : default:'a -> (PackedVal.astate -> 'a) -> astate -> 'a = + fun ~default f -> function Bottom -> default | NonBottom x -> f x + + + let lift : (PackedVal.astate -> PackedVal.astate) -> astate -> astate = + fun f -> function Bottom -> Bottom | NonBottom x -> NonBottom (f x) + + + let lift2 : (PackedVal.astate -> PackedVal.astate -> astate) -> astate -> astate -> astate = + 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 -> astate -> 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 -> astate -> bool = + fun e1_opt e2_opt -> lift_default ~default:true (PackedVal.le_sat_opt e1_opt e2_opt) + + + let meet_constraints : Constraints.t -> astate -> astate = + fun constrs -> lift_default ~default:Bottom (PackedVal.meet_constraints constrs) + + + let store_relation + : PowLoc.t -> SymExp.t option * SymExp.t option * SymExp.t option -> astate -> astate = + fun locs texpr_opts -> lift_default ~default:Bottom (PackedVal.store_relation locs texpr_opts) + + + let init_param : Loc.t -> astate -> astate = + fun loc -> lift_default ~default:Bottom (PackedVal.init_param loc) + + + let init_array + : Allocsite.t -> offset:Itv.t -> size:Itv.t -> size_exp_opt:SymExp.t option -> astate + -> astate = + fun allocsite ~offset ~size ~size_exp_opt -> + lift_default ~default:Bottom (PackedVal.init_array allocsite ~offset ~size ~size_exp_opt) + + + let forget_locs : PowLoc.t -> astate -> astate = fun locs -> lift (PackedVal.forget_locs locs) + + let instantiate : caller:astate -> callee:astate -> SubstMap.t -> astate = + 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 3640d7abe..e6aa2aaa8 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -13,6 +13,7 @@ module BoUtils = BufferOverrunUtils module Dom = BufferOverrunDomain module PO = BufferOverrunProofObligations module Sem = BufferOverrunSemantics +module Relation = BufferOverrunDomainRelation module Trace = BufferOverrunTrace module TraceSet = Trace.Set @@ -86,12 +87,17 @@ let malloc size_exp = let typ, stride, length0, dyn_length = get_malloc_info size_exp in let length = Sem.eval length0 mem in let traces = TraceSet.add_elem (Trace.ArrDecl location) (Dom.Val.get_traces length) in + let allocsite = Sem.get_allocsite pname ~node_hash ~inst_num:0 ~dimension:1 in + let offset, size = (Itv.zero, Dom.Val.get_itv length) 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 mem) size_exp + in let v = - Sem.eval_array_alloc pname ~node_hash typ ~stride ~offset:Itv.zero - ~size:(Dom.Val.get_itv length) ~inst_num:0 ~dimension:1 - |> Dom.Val.set_traces traces + Sem.eval_array_alloc allocsite typ ~stride ~offset ~size |> Dom.Val.set_traces traces in mem |> Dom.Mem.add_stack (Loc.of_id id) v + |> Dom.Mem.init_array_relation allocsite ~offset ~size ~size_exp_opt |> set_uninitialized location typ (Dom.Val.get_array_locs v) |> BoUtils.Exec.init_array_fields tenv pname ~node_hash typ (Dom.Val.get_array_locs v) ?dyn_length @@ -182,10 +188,8 @@ let set_array_length array length_exp = | Exp.Lvar array_pvar, {Typ.desc= Typ.Tarray {elt; stride}} -> let length = Sem.eval length_exp mem |> Dom.Val.get_itv in let stride = Option.map ~f:IntLit.to_int_exn stride in - let v = - Sem.eval_array_alloc pname ~node_hash elt ~stride ~offset:Itv.zero ~size:length - ~inst_num:0 ~dimension:1 - in + let allocsite = Sem.get_allocsite pname ~node_hash ~inst_num:0 ~dimension:1 in + let v = Sem.eval_array_alloc allocsite elt ~stride ~offset:Itv.zero ~size:length in mem |> Dom.Mem.add_stack (Loc.of_pvar array_pvar) v |> set_uninitialized location elt (Dom.Val.get_array_locs v) | _ -> diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index 50e3def8b..d7cde0b3c 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml @@ -10,6 +10,7 @@ open! AbstractDomain.Types module F = Format module L = Logging module ItvPure = Itv.ItvPure +module Relation = BufferOverrunDomainRelation module MF = MarkupFormatter module ValTraceSet = BufferOverrunTrace.Set @@ -93,7 +94,13 @@ module AllocSizeCondition = struct end module ArrayAccessCondition = struct - type t = {idx: ItvPure.astate; size: ItvPure.astate} [@@deriving compare] + type t = + { idx: ItvPure.astate + ; size: ItvPure.astate + ; idx_sym_exp: Relation.SymExp.t option + ; size_sym_exp: Relation.SymExp.t option + ; relation: Relation.astate } + [@@deriving compare] let get_symbols c = ItvPure.get_symbols c.idx @ ItvPure.get_symbols c.size @@ -106,7 +113,10 @@ module ArrayAccessCondition = struct let pp : F.formatter -> t -> unit = fun fmt c -> let c = set_size_pos c in - F.fprintf fmt "%a < %a" ItvPure.pp c.idx ItvPure.pp c.size + F.fprintf fmt "%a < %a" ItvPure.pp c.idx ItvPure.pp c.size ; + if Option.is_some Config.bo_relational_domain then + F.fprintf fmt "@,%a < %a when %a" Relation.SymExp.pp_opt c.idx_sym_exp Relation.SymExp.pp_opt + c.size_sym_exp Relation.pp c.relation let pp_description : F.formatter -> t -> unit = @@ -115,9 +125,12 @@ module ArrayAccessCondition = struct F.fprintf fmt "Offset: %a Size: %a" ItvPure.pp c.idx ItvPure.pp c.size - let make : idx:ItvPure.t -> size:ItvPure.t -> t option = - fun ~idx ~size -> - if ItvPure.is_invalid idx || ItvPure.is_invalid size then None else Some {idx; size} + let make + : idx:ItvPure.t -> size:ItvPure.t -> idx_sym_exp:Relation.SymExp.t option + -> size_sym_exp:Relation.SymExp.t option -> relation:Relation.astate -> t option = + fun ~idx ~size ~idx_sym_exp ~size_sym_exp ~relation -> + if ItvPure.is_invalid idx || ItvPure.is_invalid size then None + else Some {idx; size; idx_sym_exp; size_sym_exp; relation} let have_similar_bounds {idx= lidx; size= lsiz} {idx= ridx; size= rsiz} = @@ -209,9 +222,15 @@ module ArrayAccessCondition = struct let c' = set_size_pos c in (* if sl < 0, use sl' = 0 *) let not_overrun = - if is_arraylist_add then ItvPure.le_sem c'.idx c'.size else ItvPure.lt_sem c'.idx c'.size + if is_arraylist_add then ItvPure.le_sem c'.idx c'.size + else if Relation.lt_sat_opt c'.idx_sym_exp c'.size_sym_exp c'.relation then Itv.Boolean.true_ + else ItvPure.lt_sem c'.idx c'.size + in + let not_underrun = + if Relation.le_sat_opt (Some Relation.SymExp.zero) c'.idx_sym_exp c'.relation then + Itv.Boolean.true_ + else ItvPure.le_sem ItvPure.zero c'.idx in - let not_underrun = ItvPure.le_sem ItvPure.zero c'.idx in (* il >= 0 and iu < sl, definitely not an error *) if Itv.Boolean.is_true not_overrun && Itv.Boolean.is_true not_underrun then {report_issue_type= None; propagate= false} (* iu < 0 or il >= su, definitely an error *) @@ -239,13 +258,22 @@ module ArrayAccessCondition = struct {report_issue_type; propagate= is_symbolic} - let subst : Itv.Bound.t bottom_lifted Itv.SymbolMap.t -> t -> t option = - fun bound_map c -> + let subst + : Itv.Bound.t bottom_lifted Itv.SymbolMap.t -> Relation.SubstMap.t -> Relation.astate -> t + -> t option = + fun bound_map rel_map caller_relation c -> match (ItvPure.subst c.idx bound_map, ItvPure.subst c.size bound_map) with | NonBottom idx, NonBottom size -> - Some {idx; size} + let idx_sym_exp = Relation.SubstMap.symexp_subst_opt rel_map c.idx_sym_exp in + let size_sym_exp = Relation.SubstMap.symexp_subst_opt rel_map c.size_sym_exp in + let relation = Relation.instantiate rel_map ~caller:caller_relation ~callee:c.relation in + Some {idx; size; idx_sym_exp; size_sym_exp; relation} | _ -> None + + + let forget_locs : AbsLoc.PowLoc.t -> t -> t = + fun locs c -> {c with relation= Relation.forget_locs locs c.relation} end module Condition = struct @@ -266,11 +294,12 @@ module Condition = struct ArrayAccessCondition.get_symbols c - let subst bound_map = function + let subst bound_map rel_map caller_relation = function | AllocSize c -> AllocSizeCondition.subst bound_map c |> make_alloc_size | ArrayAccess {is_arraylist_add; c} -> - ArrayAccessCondition.subst bound_map c |> make_array_access ~is_arraylist_add + ArrayAccessCondition.subst bound_map rel_map caller_relation c + |> make_array_access ~is_arraylist_add let have_similar_bounds c1 c2 = @@ -315,6 +344,14 @@ module Condition = struct AllocSizeCondition.check c | ArrayAccess {is_arraylist_add; c} -> ArrayAccessCondition.check ~is_arraylist_add c + + + let forget_locs locs x = + match x with + | ArrayAccess {is_arraylist_add; c} -> + ArrayAccess {is_arraylist_add; c= ArrayAccessCondition.forget_locs locs c} + | AllocSize _ -> + x end module ConditionTrace = struct @@ -395,12 +432,12 @@ module ConditionWithTrace = struct cmp - let subst (bound_map, trace_map) caller_pname callee_pname location cwt = + let subst (bound_map, trace_map) rel_map caller_relation caller_pname callee_pname location cwt = match Condition.get_symbols cwt.cond with | [] -> Some cwt | symbols -> - match Condition.subst bound_map cwt.cond with + match Condition.subst bound_map rel_map caller_relation cwt.cond with | None -> None | Some cond -> @@ -434,6 +471,9 @@ module ConditionWithTrace = struct report_issue_type |> Option.map ~f:(set_buffer_overrun_u5 cwt) |> Option.iter ~f:(report cwt.cond cwt.trace) ; propagate + + + let forget_locs locs cwt = {cwt with cond= Condition.forget_locs locs cwt.cond} end module ConditionSet = struct @@ -495,9 +535,10 @@ module ConditionSet = struct join [cwt] condset - let add_array_access pname location ~idx ~size ~is_arraylist_add val_traces condset = - ArrayAccessCondition.make ~idx ~size |> Condition.make_array_access ~is_arraylist_add - |> add_opt pname location val_traces condset + let add_array_access pname location ~idx ~size ~is_arraylist_add ~idx_sym_exp ~size_sym_exp + ~relation val_traces condset = + ArrayAccessCondition.make ~idx ~size ~idx_sym_exp ~size_sym_exp ~relation + |> Condition.make_array_access ~is_arraylist_add |> add_opt pname location val_traces condset let add_alloc_size pname location ~length val_traces condset = @@ -505,10 +546,12 @@ module ConditionSet = struct |> add_opt pname location val_traces condset - let subst condset bound_map_trace_map caller_pname callee_pname location = + let subst condset bound_map_trace_map rel_subst_map caller_relation caller_pname callee_pname + location = let subst_add_cwt condset cwt = match - ConditionWithTrace.subst bound_map_trace_map caller_pname callee_pname location cwt + ConditionWithTrace.subst bound_map_trace_map rel_subst_map caller_relation caller_pname + callee_pname location cwt with | None -> condset @@ -532,12 +575,14 @@ module ConditionSet = struct let pp : Format.formatter -> t -> unit = fun fmt condset -> - let pp_sep fmt () = F.fprintf fmt ", @," in - F.fprintf fmt "@[Safety conditions :@," ; - F.fprintf fmt "@[{" ; - F.pp_print_list ~pp_sep ConditionWithTrace.pp fmt condset ; - F.fprintf fmt " }@]" ; - F.fprintf fmt "@]" + let pp_sep fmt () = F.fprintf fmt ",@," in + F.fprintf fmt "Safety conditions:@;@[{ %a }@]" + (F.pp_print_list ~pp_sep ConditionWithTrace.pp) + condset + + + let forget_locs : AbsLoc.PowLoc.t -> t -> t = + fun locs x -> List.map x ~f:(ConditionWithTrace.forget_locs locs) end let description cond trace = diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 9699146fe..dd897bc69 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -314,7 +314,7 @@ let rec eval_arr : Exp.t -> Mem.astate -> Val.t = Val.bot -let get_allocsite : Typ.Procname.t -> node_hash:int -> inst_num:int -> dimension:int -> string = +let get_allocsite : Typ.Procname.t -> node_hash:int -> inst_num:int -> dimension:int -> Allocsite.t = fun proc_name ~node_hash ~inst_num ~dimension -> let proc_name = Typ.Procname.to_string proc_name in let node_num = string_of_int node_hash in @@ -324,15 +324,19 @@ let get_allocsite : Typ.Procname.t -> node_hash:int -> inst_num:int -> dimension let eval_array_alloc - : Typ.Procname.t -> node_hash:int -> Typ.t -> stride:int option -> offset:Itv.t -> size:Itv.t - -> inst_num:int -> dimension:int -> Val.t = - fun pdesc ~node_hash typ ~stride ~offset ~size ~inst_num ~dimension -> - let allocsite = get_allocsite pdesc ~node_hash ~inst_num ~dimension in + : Allocsite.t -> Typ.t -> stride:int option -> offset:Itv.t -> size:Itv.t -> Val.t = + fun allocsite typ ~stride ~offset ~size -> let int_stride = match stride with None -> sizeof typ | Some stride -> stride in let stride = Itv.of_int int_stride in - ArrayBlk.make allocsite ~offset ~size ~stride |> Val.of_array_blk + ArrayBlk.make allocsite ~offset ~size ~stride |> Val.of_array_blk ~allocsite +let get_sym_f mem e = Val.get_sym (eval e mem) + +let get_offset_sym_f mem e = Val.get_offset_sym (eval e mem) + +let get_size_sym_f mem e = Val.get_size_sym (eval e mem) + module Prune = struct type astate = {prune_pairs: PrunePairs.t; mem: Mem.astate} @@ -423,12 +427,16 @@ module Prune = struct let is_unreachable_constant : Exp.t -> Mem.astate -> bool = - fun e m -> Val.( <= ) ~lhs:(eval e m) ~rhs:(Val.of_int 0) + fun e m -> + let v = eval e m in + Itv.( <= ) ~lhs:(Val.get_itv v) ~rhs:(Itv.of_int 0) && PowLoc.is_bot (Val.get_pow_loc v) + && ArrayBlk.is_bot (Val.get_array_blk v) let prune_unreachable : Exp.t -> astate -> astate = fun e ({mem} as astate) -> - if is_unreachable_constant e mem then {astate with mem= Mem.bot} else astate + if is_unreachable_constant e mem || Mem.is_relation_unsat mem then {astate with mem= Mem.bot} + else astate let rec prune_helper e astate = @@ -461,6 +469,10 @@ module Prune = struct let prune : Exp.t -> Mem.astate -> Mem.astate = fun e mem -> let mem = Mem.apply_latest_prune e mem in + let mem = + let constrs = Relation.Constraints.of_exp e ~get_sym_f:(get_sym_f mem) in + Mem.meet_constraints constrs mem + in let {mem; prune_pairs} = prune_helper e {mem; prune_pairs= PrunePairs.empty} in Mem.set_prune_pairs prune_pairs mem end @@ -472,13 +484,17 @@ let get_formals : Procdesc.t -> (Pvar.t * Typ.t) list = let get_matching_pairs - : Tenv.t -> Val.t -> Val.t -> Typ.t -> Mem.astate -> Mem.astate + : Tenv.t -> Val.t -> Val.t -> Exp.t option -> Typ.t -> Mem.astate -> Mem.astate -> callee_ret_alias:AliasTarget.t option - -> (Itv.Bound.t * Itv.Bound.t bottom_lifted * TraceSet.t) list * AliasTarget.t option = - fun tenv formal actual typ caller_mem callee_mem ~callee_ret_alias -> + -> (Itv.Bound.t * Itv.Bound.t bottom_lifted * TraceSet.t) list + * AliasTarget.t option + * (Relation.Var.t * Relation.SymExp.t option) list = + fun tenv formal actual actual_exp_opt typ caller_mem callee_mem ~callee_ret_alias -> let get_itv v = Val.get_itv v in let get_offset v = v |> Val.get_array_blk |> ArrayBlk.offsetof in let get_size v = v |> Val.get_array_blk |> ArrayBlk.sizeof in + 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_heap_set (append_field v fn) mem in @@ -506,17 +522,38 @@ let get_matching_pairs else (lb itv1, NonBottom (lb itv2), traces) :: (ub itv1, NonBottom (ub itv2), traces) :: l else l in - let add_pair_val v1 v2 pairs = + 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 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 (bound_pairs, rel_pairs) = add_ret_alias (Val.get_all_locs v1) (Val.get_all_locs v2) ; - pairs |> add_pair_itv (get_itv v1) (get_itv v2) (Val.get_traces v2) - |> add_pair_itv (get_offset v1) (get_offset v2) (Val.get_traces v2) - |> add_pair_itv (get_size v1) (get_size v2) (Val.get_traces v2) + let bound_pairs = + bound_pairs |> add_pair_itv (get_itv v1) (get_itv v2) (Val.get_traces v2) + |> add_pair_itv (get_offset v1) (get_offset v2) (Val.get_traces v2) + |> add_pair_itv (get_size v1) (get_size v2) (Val.get_traces v2) + in + let 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 + (bound_pairs, rel_pairs) in let add_pair_field v1 v2 pairs fn = add_ret_alias (append_field v1 fn) (append_field v2 fn) ; let v1' = deref_field v1 fn callee_mem in let v2' = deref_field v2 fn caller_mem in - add_pair_val v1' v2' pairs + add_pair_val v1' v2' ~e2_opt:None pairs in let add_pair_ptr typ v1 v2 pairs = add_ret_alias (Val.get_all_locs v1) (Val.get_all_locs v2) ; @@ -531,15 +568,17 @@ let get_matching_pairs | Typ.Tptr (_, _) -> let v1' = deref_ptr v1 callee_mem in let v2' = deref_ptr v2 caller_mem in - add_pair_val v1' v2' pairs + add_pair_val v1' v2' ~e2_opt:None pairs | _ -> pairs in - let pairs = [] |> add_pair_val formal actual |> add_pair_ptr typ formal actual in - (pairs, !ret_alias) + let bound_pairs, rel_pairs = + ([], []) |> add_pair_val formal actual ~e2_opt:actual_exp_opt |> add_pair_ptr typ formal actual + in + (bound_pairs, !ret_alias, rel_pairs) -let subst_map_of_pairs +let subst_map_of_bound_pairs : (Itv.Bound.t * Itv.Bound.t bottom_lifted * TraceSet.t) list -> Itv.Bound.t bottom_lifted Itv.SymbolMap.t * TraceSet.t Itv.SymbolMap.t = fun pairs -> @@ -552,8 +591,16 @@ let subst_map_of_pairs List.fold ~f:add_pair ~init:(Itv.SymbolMap.empty, Itv.SymbolMap.empty) pairs +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 -> f:('a -> Val.t -> 'b -> 'b) -> 'a list -> Val.t list -> init:'b -> 'b = + : 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 | [], _ -> @@ -561,7 +608,9 @@ let rec list_fold2_def | x :: xs', [] -> list_fold2_def ~default ~f xs' ys ~init:(f x default acc) | [x], _ :: _ -> - f x (List.fold ~f:Val.join ~init:Val.bot ys) acc + 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) @@ -570,18 +619,22 @@ let get_subst_map : Tenv.t -> Procdesc.t -> (Exp.t * 'a) list -> Mem.astate -> Mem.astate -> callee_ret_alias:AliasTarget.t option -> (Itv.Bound.t bottom_lifted Itv.SymbolMap.t * TraceSet.t Itv.SymbolMap.t) - * AliasTarget.t option = + * AliasTarget.t option + * Relation.SubstMap.t = fun tenv callee_pdesc params caller_mem callee_entry_mem ~callee_ret_alias -> - let add_pair (formal, typ) actual (l, ret_alias) = + let add_pair (formal, typ) (actual, actual_exp) (bound_l, ret_alias, rel_l) = let formal = Mem.find_heap (Loc.of_pvar formal) callee_entry_mem in - let new_matching, ret_alias' = - get_matching_pairs tenv formal actual typ caller_mem callee_entry_mem ~callee_ret_alias + let new_bound_matching, ret_alias', new_rel_matching = + get_matching_pairs tenv formal actual actual_exp typ caller_mem callee_entry_mem + ~callee_ret_alias in - (List.rev_append new_matching l, Option.first_some ret_alias ret_alias') + ( List.rev_append new_bound_matching bound_l + , Option.first_some ret_alias ret_alias' + , List.rev_append new_rel_matching rel_l ) in let formals = get_formals callee_pdesc in - let actuals = List.map ~f:(fun (a, _) -> eval a caller_mem) params in - let pairs, ret_alias = - list_fold2_def ~default:Val.Itv.top ~f:add_pair formals actuals ~init:([], None) + let actuals = List.map ~f:(fun (a, _) -> (eval a caller_mem, Some a)) params in + let bound_pairs, ret_alias, rel_pairs = + list_fold2_def ~default:(Val.Itv.top, None) ~f:add_pair formals actuals ~init:([], None, []) in - (subst_map_of_pairs pairs, ret_alias) + (subst_map_of_bound_pairs bound_pairs, ret_alias, subst_map_of_rel_pairs rel_pairs) diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index f4425c53e..a23af28bb 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -10,6 +10,7 @@ open AbsLoc open! AbstractDomain.Types module L = Logging module Dom = BufferOverrunDomain +module Relation = BufferOverrunDomainRelation module PO = BufferOverrunProofObligations module Sem = BufferOverrunSemantics module Trace = BufferOverrunTrace @@ -38,15 +39,18 @@ module Exec = struct -> length:IntLit.t option -> ?stride:int -> inst_num:int -> dimension:int -> Dom.Mem.astate -> Dom.Mem.astate * int = fun ~decl_local pname ~node_hash location loc typ ~length ?stride ~inst_num ~dimension mem -> + let offset = Itv.zero in let size = Option.value_map ~default:Itv.top ~f:Itv.of_int_lit length in + let allocsite = Sem.get_allocsite pname ~node_hash ~inst_num ~dimension in let arr = - Sem.eval_array_alloc pname ~node_hash typ ~stride ~offset:Itv.zero ~size ~inst_num ~dimension + Sem.eval_array_alloc allocsite typ ~stride ~offset ~size |> Dom.Val.add_trace_elem (Trace.ArrDecl location) in let mem = if Int.equal dimension 1 then Dom.Mem.add_stack loc arr mem else Dom.Mem.add_heap loc arr mem in - let loc = Loc.of_allocsite (Sem.get_allocsite pname ~node_hash ~inst_num ~dimension) in + let mem = Dom.Mem.init_array_relation allocsite ~offset ~size ~size_exp_opt:None mem in + let loc = Loc.of_allocsite allocsite in let mem, _ = decl_local pname ~node_hash location loc typ ~inst_num ~dimension:(dimension + 1) mem in @@ -92,12 +96,14 @@ module Exec = struct in let alloc_num = Itv.Counter.next new_alloc_num in let elem = Trace.SymAssign (loc, location) in + let allocsite = Sem.get_allocsite pname ~node_hash ~inst_num ~dimension:alloc_num in let arr = - Sem.eval_array_alloc pname ~node_hash typ ~stride:None ~offset ~size ~inst_num - ~dimension:alloc_num - |> Dom.Val.add_trace_elem elem + Sem.eval_array_alloc allocsite typ ~stride:None ~offset ~size |> Dom.Val.add_trace_elem elem + in + let mem = + mem |> Dom.Mem.add_heap loc arr |> Dom.Mem.init_param_relation loc + |> Dom.Mem.init_array_relation allocsite ~offset ~size ~size_exp_opt:None in - let mem = Dom.Mem.add_heap loc arr mem in let deref_loc = Loc.of_allocsite (Sem.get_allocsite pname ~node_hash ~inst_num ~dimension:alloc_num) in @@ -145,11 +151,11 @@ module Exec = struct Itv.plus i length ) in let stride = Option.map stride ~f:IntLit.to_int_exn in - let v = - Sem.eval_array_alloc pname ~node_hash typ ~stride ~offset:Itv.zero ~size:length - ~inst_num ~dimension - in - Dom.Mem.strong_update_heap field_loc v mem + let allocsite = Sem.get_allocsite pname ~node_hash ~inst_num ~dimension in + let offset, size = (Itv.zero, length) in + let v = Sem.eval_array_alloc allocsite typ ~stride ~offset ~size in + mem |> Dom.Mem.strong_update_heap field_loc v + |> Dom.Mem.init_array_relation allocsite ~offset ~size ~size_exp_opt:None | _ -> init_fields field_typ field_loc dimension ?dyn_length mem in @@ -191,27 +197,36 @@ module Exec = struct end module Check = struct - let check_access ~size ~idx ~arr ~idx_traces ?(is_arraylist_add= false) pname location cond_set = + let check_access ~size ~idx ~size_sym_exp ~idx_sym_exp ~relation ~arr ~idx_traces + ?(is_arraylist_add= false) pname location cond_set = let arr_traces = Dom.Val.get_traces arr in match (size, idx) with | NonBottom length, NonBottom idx -> let traces = TraceSet.merge ~arr_traces ~idx_traces location in - PO.ConditionSet.add_array_access pname location ~size:length ~idx ~is_arraylist_add traces - cond_set + PO.ConditionSet.add_array_access pname location ~size:length ~idx ~size_sym_exp + ~idx_sym_exp ~relation ~is_arraylist_add traces cond_set | _ -> cond_set - let array_access ~arr ~idx ~is_plus pname location cond_set = + let array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus pname location cond_set = let arr_blk = Dom.Val.get_array_blk arr in let size = ArrayBlk.sizeof arr_blk in + let size_sym_exp = Relation.SymExp.of_sym (Dom.Val.get_size_sym arr) in let offset = ArrayBlk.offsetof arr_blk in + let offset_sym_exp = Relation.SymExp.of_sym (Dom.Val.get_offset_sym arr) in let idx_itv = Dom.Val.get_itv idx in let idx_traces = Dom.Val.get_traces idx in let idx_in_blk = (if is_plus then Itv.plus else Itv.minus) offset idx_itv in + let idx_sym_exp = + 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 L.(debug BufferOverrun Verbose) "@[Add condition :@,array: %a@, idx: %a@,@]@." ArrayBlk.pp arr_blk Itv.pp idx_in_blk ; - check_access ~size ~idx:idx_in_blk ~arr ~idx_traces pname location cond_set + check_access ~size ~idx:idx_in_blk ~size_sym_exp ~idx_sym_exp ~relation ~arr ~idx_traces pname + location cond_set let arraylist_access ~array_exp ~index_exp ?(is_arraylist_add= false) mem pname location cond_set = @@ -220,11 +235,15 @@ module Check = struct let idx_traces = Dom.Val.get_traces idx in let size = Exec.get_alist_size arr mem |> Dom.Val.get_itv in let idx = Dom.Val.get_itv idx in - check_access ~size ~idx ~arr ~idx_traces ~is_arraylist_add pname location cond_set + let relation = Dom.Mem.get_relation mem in + check_access ~size ~idx ~size_sym_exp:None ~idx_sym_exp:None ~relation ~arr ~idx_traces + ~is_arraylist_add pname location cond_set let lindex ~array_exp ~index_exp mem pname location cond_set = let idx = Sem.eval index_exp mem in let arr = Sem.eval_arr array_exp mem in - array_access ~arr ~idx ~is_plus:true pname location cond_set + let idx_sym_exp = Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f mem) index_exp in + let relation = Dom.Mem.get_relation mem in + array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus:true pname location cond_set end diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.mli b/infer/src/bufferoverrun/bufferOverrunUtils.mli index 97b7f2a6e..546eaceb8 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.mli +++ b/infer/src/bufferoverrun/bufferOverrunUtils.mli @@ -8,6 +8,7 @@ open! IStd open AbsLoc module Dom = BufferOverrunDomain +module Relation = BufferOverrunDomainRelation module PO = BufferOverrunProofObligations module Exec : sig @@ -56,7 +57,8 @@ end module Check : sig val array_access : - arr:Dom.Val.t -> idx:Dom.Val.t -> is_plus:bool -> Typ.Procname.t -> Location.t + arr:Dom.Val.t -> idx:Dom.Val.t -> idx_sym_exp:Relation.SymExp.t option + -> relation:Relation.astate -> is_plus:bool -> Typ.Procname.t -> Location.t -> PO.ConditionSet.t -> PO.ConditionSet.t val lindex : diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 7d80a5a57..b11486c0a 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -35,6 +35,8 @@ module Boolean = struct let top = Top + let true_ = True + let equal = [%compare.equal : t] let is_false = function False -> true | _ -> false diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index d635b8584..be0b30747 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -22,6 +22,8 @@ module Boolean : sig val top : t + val true_ : t + val equal : t -> t -> bool val is_false : t -> bool diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index a65a1f740..246ef67e5 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -61,7 +61,7 @@ module TransferFunctionsNodesBasicCost = struct let callee_entry_mem = BufferOverrunDomain.Summary.get_input inferbo_summary in let callee_exit_mem = BufferOverrunDomain.Summary.get_output inferbo_summary in let callee_ret_alias = BufferOverrunDomain.Mem.find_ret_alias callee_exit_mem in - let (subst_map, _), _ = + let (subst_map, _), _, _ = BufferOverrunSemantics.get_subst_map tenv callee_pdesc params inferbo_caller_mem callee_entry_mem ~callee_ret_alias in diff --git a/infer/src/dune.common.in b/infer/src/dune.common.in index f1579a19d..4ffd89a25 100644 --- a/infer/src/dune.common.in +++ b/infer/src/dune.common.in @@ -55,11 +55,14 @@ let common_optflags = match build_mode with Opt -> ["-O3"] | Default | Test -> [ let common_libraries = (if java then ["javalib"; "ptrees"; "sawja"] else []) @ [ "ANSITerminal" + ; "apron" + ; "apron.octMPQ" ; "atdgen" ; "base" ; "base64" ; "cmdliner" ; "core" + ; "elina" ; "extlib" ; "mtime.clock.os" ; "oUnit" diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 89bc25e22..b1ae71592 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -86,6 +86,10 @@ codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_not_Bad, 3, CONDI codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_not_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [1, 1] Size: [1, 1]] codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_true_Ok, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_value_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] +codetoanalyze/c/bufferoverrun/relation.c, FP_array_access2_Ok, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [3, 3] Size: [1, 1]] +codetoanalyze/c/bufferoverrun/relation.c, FP_array_access3_Ok, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [3, 3] Size: [1, 1]] +codetoanalyze/c/bufferoverrun/relation.c, FP_array_access4_Ok, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [3, 3] Size: [1, 1]] +codetoanalyze/c/bufferoverrun/relation.c, FP_call_array_access_Ok, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: x,ArrayAccess: Offset: [-1, -1] Size: [1, 1] by call to `array_access_Ok()` ] codetoanalyze/c/bufferoverrun/sizeof.c, FN_static_stride_bad, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [1, 1] Size: [0, 0]] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/relation.c b/infer/tests/codetoanalyze/c/bufferoverrun/relation.c new file mode 100644 index 000000000..0b3d5af36 --- /dev/null +++ b/infer/tests/codetoanalyze/c/bufferoverrun/relation.c @@ -0,0 +1,43 @@ +/* + * Copyright (c) 2018-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +void array_access_Ok(int x, int y) { + int a[1]; + if (x + y == 1) { + a[x + y - 1] = 0; + } +} + +void FP_call_array_access_Ok() { array_access_Ok(0, 0); } + +void FP_array_access2_Ok(int x, int y) { + int a[1]; + if (x + y == 1) { + if (x + y != 1) { + a[3] = 0; + } + } +} + +void FP_array_access3_Ok(int x, int* y) { + int a[1]; + *y = x + 1; + if (x + 1 == 1) { + if (*y != 1) { + a[3] = 0; + } + } +} + +void FP_array_access4_Ok(int x, int* y) { + int a[1]; + *y = x * 3 + 1; + if (x * 3 + 1 == 1) { + if (*y != 1) { + a[3] = 0; + } + } +} diff --git a/opam b/opam index c32fb5e4b..dedce1696 100644 --- a/opam +++ b/opam @@ -27,15 +27,19 @@ remove: [ ocaml-version: [ >= "4.04.2" ] depends: [ "ANSITerminal" {>="0.7"} + "apron" "atdgen" {>="1.6.0"} "base64" "cmdliner" {>="1.0.0"} "core" "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"} "extlib-compat" "javalib" {>="2.3.4"} "mtime" diff --git a/opam.lock b/opam.lock index 15b6d4ff5..1990d799e 100644 --- a/opam.lock +++ b/opam.lock @@ -1,16 +1,21 @@ ANSITerminal = 0.8 +apron = 20160125 atd = 1.12.0 atdgen = 1.12.0 base = v0.11.0 base64 = 2.2.0 bin_prot = v0.11.0 biniou = 1.2.0 +camlidl = 1.05 camlp4 = 4.06+1 camlzip = 1.07 cmdliner = 1.0.2 conf-aclocal = 1.0.0 conf-autoconf = 0.1 +conf-gmp = 1 conf-m4 = 1 +conf-mpfr = 1 +conf-perl = 1 conf-pkg-config = 1.0 conf-sqlite3 = 1 conf-which = 1 @@ -23,6 +28,7 @@ cppo_ocamlbuild = 1.6.0 ctypes = 0.14.0 dune = 1.0.0 easy-format = 1.3.1 +elina = 1.1 extlib-compat = 1.7.2 fieldslib = v0.11.0 integers = 0.2.2 @@ -30,6 +36,7 @@ jane-street-headers = v0.11.0 javalib = 2.3.4 jbuilder = transition menhir = 20171222 +mlgmpidl = 1.2.6-1 mtime = 1.1.0 num = 1.1 ocaml-compiler-libs = v0.11.0