From 1bf8ed95b8b38b3d6d559101e0071a04d143456d Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Sun, 26 Aug 2018 22:47:52 -0700 Subject: [PATCH] [inferbo] Simplify stack/heap memory domain Summary: In SIL, (1) some program variables (e.g., array parameter) are used as pointers to heap addresses and (2) the other program variables (e.g., local array) are used as addresses themselves. So, the values of (1) are retrieved by the `Load` command, while that of (2) are by `Exp.Lvar` expressions directly. To address them differently, we had managed two maps (`Mem.Stack` and `Mem.Heap`), but which introduced function duplications on abstract memory and increased complexity. This diff merges the two maps, and instead a location set is used for distinguishing two types of abstract locations during analysis. Reviewed By: mbouaziz Differential Revision: D9420388 fbshipit-source-id: 13f824850 --- .../src/bufferoverrun/bufferOverrunChecker.ml | 70 +++--- .../src/bufferoverrun/bufferOverrunDomain.ml | 207 ++++++++---------- .../src/bufferoverrun/bufferOverrunModels.ml | 4 +- .../bufferoverrun/bufferOverrunSemantics.ml | 29 ++- infer/src/bufferoverrun/bufferOverrunUtils.ml | 8 +- infer/src/checkers/cost.ml | 3 +- 6 files changed, 151 insertions(+), 170 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 661764e8b..55c20f15b 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -37,7 +37,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let instantiate_ret ret callee_pname ~callee_exit_mem subst_map mem ret_alias location = let copy_reachable_new_locs_from locs mem = let copy loc acc = - Option.value_map (Dom.Mem.find_heap_opt loc callee_exit_mem) ~default:acc ~f:(fun v -> + Option.value_map (Dom.Mem.find_opt loc callee_exit_mem) ~default:acc ~f:(fun v -> let v = Dom.Val.subst v subst_map location |> Dom.Val.add_trace_elem (Trace.Return location) in @@ -48,7 +48,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct in let id = fst ret in let ret_loc = Loc.of_pvar (Pvar.get_ret_pvar callee_pname) in - let ret_val = Dom.Mem.find_heap ret_loc callee_exit_mem in + let ret_val = Dom.Mem.find ret_loc callee_exit_mem in let ret_var = Loc.of_var (Var.of_id id) in let add_ret_alias l = Dom.Mem.load_alias id l mem in let mem = Option.value_map ret_alias ~default:mem ~f:add_ret_alias in @@ -68,28 +68,27 @@ module TransferFunctions (CFG : ProcCfg.S) = struct match Tenv.lookup tenv typename with | Some str -> let formal_locs = - Dom.Mem.find_heap (Loc.of_pvar (fst formal)) callee_exit_mem - |> Dom.Val.get_array_blk |> ArrayBlk.get_pow_loc + Dom.Mem.find (Loc.of_pvar (fst formal)) callee_exit_mem |> Dom.Val.get_array_blk + |> ArrayBlk.get_pow_loc in let instantiate_fld mem (fn, _, _) = let formal_fields = PowLoc.append_field formal_locs ~fn in - let v = Dom.Mem.find_heap_set formal_fields callee_exit_mem in + let v = Dom.Mem.find_set formal_fields callee_exit_mem in let actual_fields = PowLoc.append_field (Dom.Val.get_all_locs actual) ~fn in Dom.Val.subst v subst_map location - |> Fn.flip (Dom.Mem.strong_update_heap actual_fields) mem + |> Fn.flip (Dom.Mem.strong_update actual_fields) mem in List.fold ~f:instantiate_fld ~init:mem str.Typ.Struct.fields | _ -> mem ) | _ -> let formal_locs = - Dom.Mem.find_heap (Loc.of_pvar (fst formal)) callee_exit_mem |> Dom.Val.get_array_blk + Dom.Mem.find (Loc.of_pvar (fst formal)) callee_exit_mem |> Dom.Val.get_array_blk |> ArrayBlk.get_pow_loc in - let v = Dom.Mem.find_heap_set formal_locs callee_exit_mem in + let v = Dom.Mem.find_set formal_locs callee_exit_mem in let actual_locs = Dom.Val.get_all_locs actual in - Dom.Val.subst v subst_map location - |> Fn.flip (Dom.Mem.strong_update_heap actual_locs) mem ) + Dom.Val.subst v subst_map location |> Fn.flip (Dom.Mem.strong_update actual_locs) mem ) | _ -> mem in @@ -159,7 +158,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | "__inferbo_empty" when Loc.is_return loc_v -> ( match Sem.get_formals pdesc with | [(formal, _)] -> - let formal_v = Dom.Mem.find_heap (Loc.of_pvar formal) mem in + let formal_v = Dom.Mem.find (Loc.of_pvar formal) mem in Dom.Mem.store_empty_alias formal_v loc_v exp2 mem | _ -> assert false ) @@ -171,33 +170,36 @@ module TransferFunctions (CFG : ProcCfg.S) = struct mem | Prune (exp, _, _, _) -> Sem.Prune.prune exp mem - | Call (((id, _) as ret), Const (Cfun callee_pname), params, location, _) -> ( - match Models.Call.dispatch tenv callee_pname params with - | Some {Models.exec} -> - let node_hash = CFG.Node.hash node in - let model_env = - Models.mk_model_env callee_pname node_hash location tenv symbol_table - in - exec model_env ~ret mem - | None -> - match Ondemand.analyze_proc_name ~caller_pdesc:pdesc callee_pname with - | Some callee_summary -> ( - match Payload.of_summary callee_summary with - | Some payload -> - let callee_pdesc = Summary.get_proc_desc callee_summary in - instantiate_mem tenv ret callee_pdesc callee_pname params mem payload location + | Call (((id, _) as ret), Const (Cfun callee_pname), params, location, _) + -> ( + let mem = Dom.Mem.add_stack_loc (Loc.of_id id) mem in + match Models.Call.dispatch tenv callee_pname params with + | Some {Models.exec} -> + let node_hash = CFG.Node.hash node in + let model_env = + Models.mk_model_env callee_pname node_hash location tenv symbol_table + in + exec model_env ~ret mem + | None -> + match Ondemand.analyze_proc_name ~caller_pdesc:pdesc callee_pname with + | Some callee_summary -> ( + match Payload.of_summary callee_summary with + | Some payload -> + let callee_pdesc = Summary.get_proc_desc callee_summary in + instantiate_mem tenv ret callee_pdesc callee_pname params mem payload location + | None -> + (* This may happen for procedures with a biabduction model. *) + L.(debug BufferOverrun Verbose) + "/!\\ Call to %a at %a has no inferbo payload@\n" Typ.Procname.pp callee_pname + Location.pp location ; + Dom.Mem.add_unknown_from id ~callee_pname ~location mem ) | None -> - (* This may happen for procedures with a biabduction model. *) L.(debug BufferOverrun Verbose) - "/!\\ Call to %a at %a has no inferbo payload@\n" Typ.Procname.pp callee_pname - Location.pp location ; + "/!\\ Unknown call to %a at %a@\n" Typ.Procname.pp callee_pname Location.pp + location ; Dom.Mem.add_unknown_from id ~callee_pname ~location mem ) - | None -> - L.(debug BufferOverrun Verbose) - "/!\\ Unknown call to %a at %a@\n" Typ.Procname.pp callee_pname Location.pp - location ; - Dom.Mem.add_unknown_from id ~callee_pname ~location mem ) | Call ((id, _), fun_exp, _, location, _) -> + let mem = Dom.Mem.add_stack_loc (Loc.of_id id) mem in let () = L.(debug BufferOverrun Verbose) "/!\\ Call to non-const function %a at %a" Exp.pp fun_exp Location.pp location diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 6ed9c1964..c582bbac2 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -132,6 +132,8 @@ module Val = struct let of_int n = of_itv (Itv.of_int n) + let of_loc : Loc.t -> t = fun x -> {bot with powloc= PowLoc.singleton x} + let of_pow_loc : PowLoc.t -> t = fun x -> {bot with powloc= x} let of_array_alloc : Allocsite.t -> stride:int option -> offset:Itv.t -> size:Itv.t -> t = @@ -308,64 +310,17 @@ module Val = struct end end -module Stack = struct - include AbstractDomain.Map (Loc) (Val) +module StackLocs = struct + include AbstractDomain.FiniteSet (Loc) let bot = empty - - let find : Loc.t -> astate -> Val.t = fun l m -> try find l m with Caml.Not_found -> Val.bot - - let find_set : PowLoc.t -> astate -> Val.t = - fun locs mem -> - let find_join loc acc = Val.join acc (find loc mem) in - PowLoc.fold find_join locs Val.bot - - - let remove_temps : Ident.t list -> astate -> astate = - fun temps mem -> - let remove_temp mem temp = - let temp_loc = Loc.of_id temp in - remove temp_loc mem - in - List.fold temps ~init:mem ~f:remove_temp end -module Heap = struct +module MemPure = struct include AbstractDomain.Map (Loc) (Val) let bot = empty - let find : Loc.t -> astate -> Val.t = - fun l m -> try find l m with Caml.Not_found -> Val.Itv.top - - - let find_set : PowLoc.t -> astate -> Val.t = - fun locs mem -> - let find_join loc acc = Val.join acc (find loc mem) in - PowLoc.fold find_join locs Val.bot - - - let transform : f:(Val.t -> Val.t) -> PowLoc.t -> astate -> astate = - 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 - - - let weak_update : PowLoc.t -> Val.t -> astate -> astate = - fun locs v mem -> PowLoc.fold (fun x -> add x (Val.join v (find x mem))) locs mem - - let get_return : astate -> Val.t = fun mem -> let mem = filter (fun l _ -> Loc.is_return l) mem in @@ -464,10 +419,7 @@ module AliasMap = struct let find : Ident.t -> t -> AliasTarget.t option = fun k m -> M.find_opt k m - let remove_temps : Ident.t list -> t -> t = - fun temps m -> - let remove_temp m temp = M.remove temp m in - List.fold temps ~init:m ~f:remove_temp + let remove : Ident.t -> t -> t = M.remove end module AliasRet = struct @@ -554,8 +506,8 @@ module Alias = struct else a - let remove_temps : Ident.t list -> astate -> astate = - fun temps a -> (AliasMap.remove_temps temps (fst a), snd a) + let remove_temp : Ident.t -> astate -> astate = + fun temp (alias_map, alias_ret) -> (AliasMap.remove temp alias_map, alias_ret) let pp : F.formatter -> astate -> unit = @@ -647,8 +599,8 @@ end module MemReach = struct type astate = - { stack: Stack.astate - ; heap: Heap.astate + { stack_locs: StackLocs.astate + ; mem_pure: MemPure.astate ; alias: Alias.astate ; latest_prune: LatestPrune.astate ; relation: Relation.astate } @@ -656,8 +608,8 @@ module MemReach = struct type t = astate let init : t = - { stack= Stack.bot - ; heap= Heap.bot + { stack_locs= StackLocs.bot + ; mem_pure= MemPure.bot ; alias= Alias.bot ; latest_prune= LatestPrune.top ; relation= Relation.empty } @@ -666,7 +618,8 @@ module MemReach = struct let ( <= ) ~lhs ~rhs = if phys_equal lhs rhs then true else - Stack.( <= ) ~lhs:lhs.stack ~rhs:rhs.stack && Heap.( <= ) ~lhs:lhs.heap ~rhs:rhs.heap + StackLocs.( <= ) ~lhs:lhs.stack_locs ~rhs:rhs.stack_locs + && MemPure.( <= ) ~lhs:lhs.mem_pure ~rhs:rhs.mem_pure && Alias.( <= ) ~lhs:lhs.alias ~rhs:rhs.alias && LatestPrune.( <= ) ~lhs:lhs.latest_prune ~rhs:rhs.latest_prune && Relation.( <= ) ~lhs:lhs.relation ~rhs:rhs.relation @@ -675,8 +628,8 @@ module MemReach = struct let widen ~prev ~next ~num_iters = if phys_equal prev next then prev else - { stack= Stack.widen ~prev:prev.stack ~next:next.stack ~num_iters - ; heap= Heap.widen ~prev:prev.heap ~next:next.heap ~num_iters + { stack_locs= StackLocs.widen ~prev:prev.stack_locs ~next:next.stack_locs ~num_iters + ; mem_pure= MemPure.widen ~prev:prev.mem_pure ~next:next.mem_pure ~num_iters ; alias= Alias.widen ~prev:prev.alias ~next:next.alias ~num_iters ; latest_prune= LatestPrune.widen ~prev:prev.latest_prune ~next:next.latest_prune ~num_iters ; relation= Relation.widen ~prev:prev.relation ~next:next.relation ~num_iters } @@ -684,8 +637,8 @@ module MemReach = struct let join : t -> t -> t = fun x y -> - { stack= Stack.join x.stack y.stack - ; heap= Heap.join x.heap y.heap + { stack_locs= StackLocs.join x.stack_locs y.stack_locs + ; mem_pure= MemPure.join x.mem_pure y.mem_pure ; alias= Alias.join x.alias y.alias ; latest_prune= LatestPrune.join x.latest_prune y.latest_prune ; relation= Relation.join x.relation y.relation } @@ -693,23 +646,28 @@ module MemReach = struct 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" StackLocs.pp x.stack_locs MemPure.pp x.mem_pure + Alias.pp x.alias ; if Option.is_some Config.bo_relational_domain then F.fprintf fmt "@;Relation:@;%a" Relation.pp x.relation - let find_stack : Loc.t -> t -> Val.t = fun k m -> Stack.find k m.stack + let is_stack_loc : Loc.t -> t -> bool = fun l m -> StackLocs.mem l m.stack_locs - let find_stack_set : PowLoc.t -> t -> Val.t = fun k m -> Stack.find_set k m.stack + let find_opt : Loc.t -> t -> Val.t option = fun l m -> MemPure.find_opt l m.mem_pure - let find_heap : Loc.t -> t -> Val.t = fun k m -> Heap.find k m.heap + let find_stack : Loc.t -> t -> Val.t = fun l m -> Option.value (find_opt l m) ~default:Val.bot - let find_heap_opt : Loc.t -> t -> Val.t option = fun k m -> Heap.find_opt k m.heap + let find_heap : Loc.t -> t -> Val.t = fun l m -> Option.value (find_opt l m) ~default:Val.Itv.top + + let find : Loc.t -> t -> Val.t = + fun l m -> if is_stack_loc l m then find_stack l m else find_heap l m - let find_heap_set : PowLoc.t -> t -> Val.t = fun k m -> Heap.find_set k m.heap let find_set : PowLoc.t -> t -> Val.t = - fun k m -> Val.join (find_stack_set k m) (find_heap_set k m) + fun locs m -> + let find_join loc acc = Val.join acc (find loc m) in + PowLoc.fold find_join locs Val.bot let find_alias : Ident.t -> t -> AliasTarget.t option = fun k m -> Alias.find k m.alias @@ -737,9 +695,29 @@ module MemReach = struct fun formal loc e m -> {m with alias= Alias.store_empty formal loc e m.alias} - let add_stack : Loc.t -> Val.t -> t -> t = fun k v m -> {m with stack= Stack.add k v m.stack} + let add_stack_loc : Loc.t -> t -> t = fun k m -> {m with stack_locs= StackLocs.add k m.stack_locs} + + let add_stack : Loc.t -> Val.t -> t -> t = + fun k v m -> + {m with stack_locs= StackLocs.add k m.stack_locs; mem_pure= MemPure.add k v m.mem_pure} + + + let replace_stack : Loc.t -> Val.t -> t -> t = + fun k v m -> {m with mem_pure= MemPure.add k v m.mem_pure} + + + let add_heap : Loc.t -> Val.t -> t -> t = + fun x v m -> + let 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 + {v with Val.sym; Val.offset_sym; Val.size_sym} + in + {m with mem_pure= MemPure.add x v m.mem_pure} - let add_heap : Loc.t -> Val.t -> t -> t = fun k v m -> {m with heap= Heap.add k v m.heap} let add_unknown_from : Ident.t -> callee_pname:Typ.Procname.t option -> location:Location.t -> t -> t = @@ -748,37 +726,48 @@ module MemReach = struct add_stack (Loc.of_id id) val_unknown m |> add_heap Loc.unknown val_unknown - let strong_update_heap : PowLoc.t -> Val.t -> t -> t = - fun p v m -> {m with heap= Heap.strong_update p v m.heap} - + let strong_update : PowLoc.t -> Val.t -> t -> t = + fun locs v m -> + let strong_update1 l m = if is_stack_loc l m then replace_stack l v m else add_heap l v m in + PowLoc.fold strong_update1 locs m - let transform_heap : f:(Val.t -> Val.t) -> PowLoc.t -> t -> t = - fun ~f p m -> {m with heap= Heap.transform ~f p m.heap} + let transform_mem : f:(Val.t -> Val.t) -> PowLoc.t -> t -> t = + fun ~f locs m -> + let transform_mem1 l m = + let add, find = + if is_stack_loc l m then (replace_stack, find_stack) else (add_heap, find_heap) + in + add l (f (find l m)) m + in + PowLoc.fold transform_mem1 locs m - let weak_update_heap : PowLoc.t -> Val.t -> t -> t = - fun p v m -> {m with heap= Heap.weak_update p v m.heap} + let weak_update locs v m = transform_mem ~f:(fun v' -> Val.join v' v) locs m - let get_return : t -> Val.t = fun m -> Heap.get_return m.heap + let get_return : t -> Val.t = fun m -> MemPure.get_return m.mem_pure 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 + if can_strong_update ploc then strong_update ploc v s else let () = L.(debug BufferOverrun Verbose) "Weak update for %a <- %a@." PowLoc.pp ploc Val.pp v in - weak_update_heap ploc v s + weak_update ploc v s - let transform_mem : f:(Val.t -> Val.t) -> PowLoc.t -> t -> t = - fun ~f ploc s -> transform_heap ~f ploc s + let remove_temp : Ident.t -> t -> t = + fun temp m -> + let l = Loc.of_id temp in + { m with + stack_locs= StackLocs.remove l m.stack_locs + ; mem_pure= MemPure.remove l m.mem_pure + ; alias= Alias.remove_temp temp m.alias } let remove_temps : Ident.t list -> t -> t = - fun temps m -> - {m with stack= Stack.remove_temps temps m.stack; alias= Alias.remove_temps temps m.alias} + fun temps m -> List.fold temps ~init:m ~f:(fun acc temp -> remove_temp temp acc) let set_prune_pairs : PrunePairs.t -> t -> t = @@ -820,14 +809,14 @@ module MemReach = struct and add_from_loc heap loc acc = if PowLoc.mem loc acc then acc else - let reachable_locs = Heap.fold (add_reachable1 ~root:loc) heap PowLoc.empty in + let reachable_locs = MemPure.fold (add_reachable1 ~root:loc) heap PowLoc.empty in add_from_locs heap reachable_locs (PowLoc.add loc acc) in - fun locs m -> add_from_locs m.heap locs PowLoc.empty + fun locs m -> add_from_locs m.mem_pure locs PowLoc.empty - let heap_range : filter_loc:(Loc.t -> bool) -> t -> Itv.NonNegativePolynomial.astate = - fun ~filter_loc {heap} -> Heap.range ~filter_loc heap + let range : filter_loc:(Loc.t -> bool) -> t -> Itv.NonNegativePolynomial.astate = + fun ~filter_loc {mem_pure} -> MemPure.range ~filter_loc mem_pure let get_relation : t -> Relation.astate = fun m -> m.relation @@ -882,30 +871,24 @@ module Mem = struct fun f -> f_lift_default ~default:Bottom (fun m' -> NonBottom (f m')) - let find_stack : Loc.t -> t -> Val.t = - fun k -> f_lift_default ~default:Val.bot (MemReach.find_stack k) + let is_stack_loc : Loc.t -> t -> bool = + fun k -> f_lift_default ~default:false (MemReach.is_stack_loc k) - let find_stack_set : PowLoc.t -> t -> Val.t = - fun k -> f_lift_default ~default:Val.bot (MemReach.find_stack_set k) + let find : Loc.t -> t -> Val.t = fun k -> f_lift_default ~default:Val.bot (MemReach.find k) - - let find_heap : Loc.t -> t -> Val.t = - fun k -> f_lift_default ~default:Val.bot (MemReach.find_heap k) - - - let find_heap_opt : Loc.t -> t -> Val.t option = - fun k -> f_lift_default ~default:None (MemReach.find_heap_opt k) - - - let find_heap_set : PowLoc.t -> t -> Val.t = - fun k -> f_lift_default ~default:Val.bot (MemReach.find_heap_set k) + let find_stack : Loc.t -> t -> Val.t = + fun k -> f_lift_default ~default:Val.bot (MemReach.find_stack k) let find_set : PowLoc.t -> t -> Val.t = fun k -> f_lift_default ~default:Val.bot (MemReach.find_set k) + let find_opt : Loc.t -> t -> Val.t option = + fun k -> f_lift_default ~default:None (MemReach.find_opt k) + + let find_alias : Ident.t -> t -> AliasTarget.t option = fun k -> f_lift_default ~default:None (MemReach.find_alias k) @@ -934,6 +917,8 @@ module Mem = struct fun formal loc e -> f_lift (MemReach.store_empty_alias formal loc e) + let add_stack_loc : Loc.t -> t -> t = fun k -> f_lift (MemReach.add_stack_loc k) + let add_stack : Loc.t -> Val.t -> t -> t = fun k v -> f_lift (MemReach.add_stack k v) let add_heap : Loc.t -> Val.t -> t -> t = fun k v -> f_lift (MemReach.add_heap k v) @@ -947,13 +932,9 @@ module Mem = struct fun id ~location -> f_lift (MemReach.add_unknown_from id ~callee_pname:None ~location) - let strong_update_heap : PowLoc.t -> Val.t -> t -> t = - fun p v -> f_lift (MemReach.strong_update_heap p v) - - - let weak_update_heap : PowLoc.t -> Val.t -> t -> t = - fun p v -> f_lift (MemReach.weak_update_heap p v) + let strong_update : PowLoc.t -> Val.t -> t -> t = fun p v -> f_lift (MemReach.strong_update p v) + let weak_update : PowLoc.t -> Val.t -> t -> t = fun p v -> f_lift (MemReach.weak_update p v) let get_return : t -> Val.t = f_lift_default ~default:Val.bot MemReach.get_return diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 713a1660d..eaba97227 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -83,7 +83,7 @@ let check_alloc_size size_exp {location} mem cond_set = let set_uninitialized location (typ: Typ.t) ploc mem = match typ.desc with | Tint _ | Tfloat _ -> - Dom.Mem.weak_update_heap ploc Dom.Val.Itv.top mem + Dom.Mem.weak_update ploc Dom.Val.Itv.top mem | _ -> L.(debug BufferOverrun Verbose) "/!\\ Do not know how to uninitialize type %a at %a@\n" (Typ.pp Pp.text) typ Location.pp @@ -336,7 +336,7 @@ module Collection = struct let change_size_by ~size_f alist_id _ ~ret:_ mem = - let alist_v = Dom.Mem.find_stack (Loc.of_id alist_id) mem in + let alist_v = Dom.Mem.find (Loc.of_id alist_id) mem in let locs = Dom.Val.get_pow_loc alist_v in Dom.Mem.transform_mem ~f:size_f locs mem diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 033bbcddc..0cd61a0b1 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -140,9 +140,8 @@ let rec eval : Exp.t -> Mem.astate -> Val.t = | Exp.Var id -> Mem.find_stack (Var.of_id id |> Loc.of_var) mem | Exp.Lvar pvar -> - let ploc = pvar |> Loc.of_pvar |> PowLoc.singleton in - let arr = Mem.find_stack_set ploc mem in - ploc |> Val.of_pow_loc |> Val.join arr + let ploc = Loc.of_pvar pvar in + if Mem.is_stack_loc ploc mem then Mem.find ploc mem else Val.of_loc ploc | Exp.UnOp (uop, e, _) -> eval_unop uop e mem | Exp.BinOp (bop, e1, e2) -> @@ -249,7 +248,7 @@ let rec eval_arr : Exp.t -> Mem.astate -> Val.t = | Exp.Var id -> ( match Mem.find_alias id mem with | Some (AliasTarget.Simple loc) -> - Mem.find_heap loc mem + Mem.find loc mem | Some (AliasTarget.Empty _) | None -> Val.bot ) | Exp.Lvar pvar -> @@ -260,7 +259,7 @@ let rec eval_arr : Exp.t -> Mem.astate -> Val.t = eval_arr e mem | Exp.Lfield (e, fn, _) -> let locs = eval e mem |> Val.get_all_locs |> PowLoc.append_field ~fn in - Mem.find_heap_set locs mem + Mem.find_set locs mem | Exp.Lindex (e1, e2) -> let arr = eval e1 mem in let idx = eval e2 mem in @@ -290,11 +289,11 @@ module Prune = struct | Exp.Var x -> ( match Mem.find_alias x mem with | Some (AliasTarget.Simple lv) -> - let v = Mem.find_heap lv mem in + let v = Mem.find lv mem in let v' = Val.prune_ne_zero v in update_mem_in_prune lv v' astate | Some (AliasTarget.Empty lv) -> - let v = Mem.find_heap lv mem in + let v = Mem.find lv mem in let v' = Val.prune_eq_zero v in update_mem_in_prune lv v' astate | None -> @@ -302,11 +301,11 @@ module Prune = struct | Exp.UnOp (Unop.LNot, Exp.Var x, _) -> ( match Mem.find_alias x mem with | Some (AliasTarget.Simple lv) -> - let v = Mem.find_heap lv mem in + let v = Mem.find lv mem in let v' = Val.prune_eq_zero v in update_mem_in_prune lv v' astate | Some (AliasTarget.Empty lv) -> - let v = Mem.find_heap lv mem in + let v = Mem.find lv mem in let itv_v = Itv.prune_comp Binop.Ge (Val.get_itv v) Itv.one in let v' = Val.modify_itv itv_v v in update_mem_in_prune lv v' astate @@ -325,7 +324,7 @@ module Prune = struct | Exp.BinOp ((Binop.Ge as comp), Exp.Var x, e') -> ( match Mem.find_simple_alias x mem with | Some lv -> - let v = Mem.find_heap lv mem in + let v = Mem.find lv mem in let v' = Val.prune_comp comp v (eval e' mem) in update_mem_in_prune lv v' astate | None -> @@ -333,7 +332,7 @@ module Prune = struct | Exp.BinOp (Binop.Eq, Exp.Var x, e') -> ( match Mem.find_simple_alias x mem with | Some lv -> - let v = Mem.find_heap lv mem in + let v = Mem.find lv mem in let v' = Val.prune_eq v (eval e' mem) in update_mem_in_prune lv v' astate | None -> @@ -341,7 +340,7 @@ module Prune = struct | Exp.BinOp (Binop.Ne, Exp.Var x, e') -> ( match Mem.find_simple_alias x mem with | Some lv -> - let v = Mem.find_heap lv mem in + let v = Mem.find lv mem in let v' = Val.prune_ne v (eval e' mem) in update_mem_in_prune lv v' astate | None -> @@ -437,11 +436,11 @@ let get_matching_pairs 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 + let deref_field v fn mem = Mem.find_set (append_field v fn) mem in let deref_ptr v mem = let array_locs = Val.get_array_locs v in let locs = if PowLoc.is_empty array_locs then Val.get_pow_loc v else array_locs in - Mem.find_heap_set locs mem + Mem.find_set locs mem in let ret_alias = ref None in let add_ret_alias v1 v2 = @@ -563,7 +562,7 @@ let get_subst_map * Relation.SubstMap.t = fun tenv callee_pdesc params caller_mem callee_symbol_table callee_exit_mem -> let add_pair (formal, typ) (actual, actual_exp) (bound_l, ret_alias, rel_l) = - let callee_v = Mem.find_heap (Loc.of_pvar formal) callee_exit_mem in + let callee_v = Mem.find (Loc.of_pvar formal) callee_exit_mem in let new_bound_matching, ret_alias', new_rel_matching = get_matching_pairs tenv (Itv.SymbolPath.of_pvar formal) callee_v actual actual_exp typ caller_mem callee_symbol_table callee_exit_mem diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index a44efae87..664ea93dd 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -19,12 +19,12 @@ module TraceSet = Trace.Set module Exec = struct let get_alist_size alist mem = let size_powloc = Dom.Val.get_pow_loc alist in - Dom.Mem.find_heap_set size_powloc mem + Dom.Mem.find_set size_powloc mem let load_val id val_ mem = let locs = val_ |> Dom.Val.get_all_locs in - let v = Dom.Mem.find_heap_set locs mem in + let v = Dom.Mem.find_set locs mem in let mem = Dom.Mem.add_stack (Loc.of_id id) v mem in if PowLoc.is_singleton locs then Dom.Mem.load_simple_alias id (PowLoc.min_elt locs) mem else mem @@ -155,7 +155,7 @@ module Exec = struct let allocsite = Allocsite.make pname ~node_hash ~inst_num ~dimension in let offset, size = (Itv.zero, length) in let v = Dom.Val.of_array_alloc allocsite ~stride ~offset ~size in - mem |> Dom.Mem.strong_update_heap field_loc v + mem |> Dom.Mem.strong_update 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 @@ -188,7 +188,7 @@ module Exec = struct | Tarray {length= Some length} -> let length = Itv.plus (Itv.of_int_lit length) dyn_length in let v = Dom.Mem.find_set field_loc mem |> Dom.Val.set_array_size length in - Dom.Mem.strong_update_heap field_loc v mem + Dom.Mem.strong_update field_loc v mem | _ -> set_dyn_length tenv field_typ field_loc dyn_length mem ) | _ -> diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index b0e18b96f..e4a5aa3da 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -165,8 +165,7 @@ module BoundMap = struct unreachable returning cost 0 \n" ; BasicCost.zero | NonBottom mem -> - BufferOverrunDomain.MemReach.heap_range ~filter_loc:(filter_loc control_vars) - mem + BufferOverrunDomain.MemReach.range ~filter_loc:(filter_loc control_vars) mem in L.(debug Analysis Medium) "@\n>>>Setting bound for node = %a to %a@\n\n" Node.pp_id node_id BasicCost.pp