pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[inferbo] Simplify stack/heap memory domain

Browse Source 
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
master
Sungkeun Cho 6 years ago committed by Facebook Github Bot
parent 49e582fa49
commit 1bf8ed95b8
6 changed files with 151 additions and 170 deletions
Show Stats Download Patch File Download Diff File

70
infer/src/bufferoverrun/bufferOverrunChecker.ml
Unescape View File

@ -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

207
infer/src/bufferoverrun/bufferOverrunDomain.ml
Unescape View File

@ -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

4
infer/src/bufferoverrun/bufferOverrunModels.ml
Unescape View File

@ -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

29
infer/src/bufferoverrun/bufferOverrunSemantics.ml
Unescape View File

@ -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

8
infer/src/bufferoverrun/bufferOverrunUtils.ml
Unescape View File

@ -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 )
| _ ->

3
infer/src/checkers/cost.ml
Unescape View File

@ -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

Write Preview
Loading…
Cancel
Save