diff --git a/Makefile.autoconf.in b/Makefile.autoconf.in index 4faf1d9dd..061a908ee 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@ @@ -79,5 +81,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..8a5aa0410 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.]) 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 03af48298..f8b118e5b 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -823,6 +823,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)] @@ -2445,6 +2452,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 4c4b38ee7..af5f9ae38 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -242,6 +242,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 b58716146..a96bd3177 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, _) -> BoUtils.Exec.decl_sym_arr ~decl_sym_val:(decl_sym_val ~may_last_field) pname path tenv ~node_hash location ~depth loc typ ~inst_num ~new_sym_num ~new_alloc_num mem @@ -182,6 +183,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 = @@ -191,12 +198,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 @@ -224,6 +236,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 @@ -364,7 +384,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 @@ -403,7 +425,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 | _ -> @@ -418,11 +443,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 @@ -558,6 +585,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 @@ -570,16 +600,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 defcf6ab0..45fe13a93 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} @@ -295,6 +344,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 @@ -396,10 +454,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 @@ -506,7 +563,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 @@ -593,11 +650,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 @@ -605,6 +672,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 = @@ -614,7 +682,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 = @@ -622,12 +690,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 = @@ -689,13 +760,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 @@ -768,6 +832,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 @@ -894,6 +993,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 @@ -921,5 +1056,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..fd7cdf0dd --- /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) -> ( + try Some (Texpr1.Cst (Coeff.s_of_int (IntLit.to_int i))) with _ -> None ) + | _ -> + 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 1c82979e9..58f1273f4 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 @@ -82,12 +83,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 @@ -178,10 +184,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 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 e0c0f1726..27a523dd1 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} = @@ -206,8 +219,15 @@ module ArrayAccessCondition = struct (* idx = [il, iu], size = [sl, su], we want to check that 0 <= idx < size *) let c' = set_size_pos c in (* if sl < 0, use sl' = 0 *) - let not_overrun = ItvPure.lt_sem c'.idx c'.size in - let not_underrun = ItvPure.le_sem ItvPure.zero c'.idx in + let not_overrun = + 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 (* 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 *) @@ -235,13 +255,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 @@ -258,11 +287,11 @@ 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 c -> - ArrayAccessCondition.subst bound_map c |> make_array_access + ArrayAccessCondition.subst bound_map rel_map caller_relation c |> make_array_access let have_similar_bounds c1 c2 = @@ -306,6 +335,14 @@ module Condition = struct AllocSizeCondition.check c | ArrayAccess c -> ArrayAccessCondition.check c + + + let forget_locs locs x = + match x with + | ArrayAccess c -> + ArrayAccess (ArrayAccessCondition.forget_locs locs c) + | AllocSize _ -> + x end module ConditionTrace = struct @@ -386,12 +423,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 -> @@ -425,6 +462,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 @@ -486,9 +526,10 @@ module ConditionSet = struct join [cwt] condset - let add_array_access pname location ~idx ~size val_traces condset = - ArrayAccessCondition.make ~idx ~size |> Condition.make_array_access - |> add_opt pname location val_traces condset + let add_array_access pname location ~idx ~size ~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 |> add_opt pname location val_traces condset let add_alloc_size pname location ~length val_traces condset = @@ -496,10 +537,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 @@ -523,12 +566,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 5f4d47bb2..e76be7dbe 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 79e259958..1aa48a176 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 @@ -33,15 +34,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 @@ -69,12 +73,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 @@ -95,11 +101,11 @@ module Exec = struct Itv.plus i length ) in let stride = Option.map stride ~f:IntLit.to_int 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 @@ -141,14 +147,21 @@ module Exec = struct end module Check = struct - 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 arr_traces = Dom.Val.get_traces 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 :@," ; L.(debug BufferOverrun Verbose) "array: %a@," ArrayBlk.pp arr_blk ; L.(debug BufferOverrun Verbose) " idx: %a@," Itv.pp idx_in_blk ; @@ -156,7 +169,8 @@ module Check = struct match (size, idx_in_blk) with | NonBottom size, NonBottom idx -> let traces = TraceSet.merge ~arr_traces ~idx_traces location in - PO.ConditionSet.add_array_access pname location ~size ~idx traces cond_set + PO.ConditionSet.add_array_access pname location ~size ~idx ~size_sym_exp ~idx_sym_exp + ~relation traces cond_set | _ -> cond_set @@ -164,5 +178,7 @@ module Check = struct let lindex ~array_exp ~index_exp mem pname location cond_set = let arr = Sem.eval_arr array_exp mem in let idx = Sem.eval index_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 0f04fb0bd..d674290c1 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 @@ -41,7 +42,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 f587d5733..ba43d4b2a 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 50437ad04..d72e418e0 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 242687f9c..572514fd7 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/deadcode/jbuild.in b/infer/src/deadcode/jbuild.in index e4be88c2c..f289f0cbb 100644 --- a/infer/src/deadcode/jbuild.in +++ b/infer/src/deadcode/jbuild.in @@ -1,6 +1,8 @@ (* -*- tuareg -*- *) (* NOTE: prepend jbuild.common to this file! *) +let deadcode_cflags = common_cflags @ ["-cclib -lparmap_stubs"] + ;; Format.sprintf {| (executable @@ -12,7 +14,7 @@ (preprocess (pps (ppx_compare ppx_sexp_conv -no-check))) )) |} - (String.concat " " common_cflags) + (String.concat " " deadcode_cflags) (String.concat " " common_optflags) (String.concat " " common_libraries) |> Jbuild_plugin.V1.send diff --git a/infer/src/jbuild.common.in b/infer/src/jbuild.common.in index f1579a19d..d325430db 100644 --- a/infer/src/jbuild.common.in +++ b/infer/src/jbuild.common.in @@ -55,6 +55,9 @@ 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" + ; "elina" ; "atdgen" ; "base" ; "base64" diff --git a/infer/src/jbuild.in b/infer/src/jbuild.in index 834a14050..b0adab22b 100644 --- a/infer/src/jbuild.in +++ b/infer/src/jbuild.in @@ -38,7 +38,8 @@ let infer_cflags = ; "-open" ; "InferIR" ; "-open" - ; "InferBase" ] + ; "InferBase" + ; "-cclib -lparmap_stubs" ] (** The build stanzas to be passed to jbuilder *) 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 355910ea2..d5819d6d8 100644 --- a/opam +++ b/opam @@ -27,14 +27,18 @@ 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"} + "elina" "extlib-compat" "javalib" {>="2.3.4"} "jbuilder" {build & >="1.0+beta14"} diff --git a/opam.lock b/opam.lock index f60868baf..7b538c00d 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 @@ -22,6 +27,7 @@ cppo = 1.6.4 cppo_ocamlbuild = 1.6.0 ctypes = 0.14.0 easy-format = 1.3.1 +elina = 1.0 extlib-compat = 1.7.2 fieldslib = v0.11.0 integers = 0.2.2 @@ -29,6 +35,7 @@ jane-street-headers = v0.11.0 javalib = 2.3.4 jbuilder = 1.0+beta20 menhir = 20171222 +mlgmpidl = 1.2.6-1 mtime = 1.1.0 num = 1.1 ocaml-compiler-libs = v0.11.0