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

[inferbo] Move functions constructing array values

Browse Source 
Summary: It moves the functions that constructs array values from BufferOverrunSemantics to ArrayBlk and Val modules.

Reviewed By: mbouaziz

Differential Revision: D9194130

fbshipit-source-id: bf040a01a
master
Sungkeun Cho 7 years ago committed by Facebook Github Bot
parent 427bb440d6
commit fec87c8b95
5 changed files with 26 additions and 33 deletions
Show Stats Download Patch File Download Diff File

9
infer/src/bufferoverrun/absLoc.ml
Unescape View File

@ -16,7 +16,14 @@ module Allocsite = struct
let pp fmt s = Format.pp_print_string fmt s
let make x = x
let make : Typ.Procname.t -> node_hash:int -> inst_num:int -> dimension:int -> 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
let inst_num = string_of_int inst_num in
let dimension = string_of_int dimension in
proc_name ^ "-" ^ node_num ^ "-" ^ inst_num ^ "-" ^ dimension
let unknown = "Unknown"
end

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

@ -134,10 +134,11 @@ module Val = struct
let of_pow_loc : PowLoc.t -> t = fun x -> {bot with powloc= x}
let of_array_blk : allocsite:Allocsite.t -> ArrayBlk.astate -> t =
fun ~allocsite a ->
let of_array_alloc : Allocsite.t -> stride:int option -> offset:Itv.t -> size:Itv.t -> t =
fun allocsite ~stride ~offset ~size ->
let stride = Option.value_map stride ~default:Itv.nat ~f:Itv.of_int in
{ bot with
arrayblk= a
arrayblk= ArrayBlk.make allocsite ~offset ~size ~stride
; offset_sym= Relation.Sym.of_allocsite_offset allocsite
; size_sym= Relation.Sym.of_allocsite_size allocsite }

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

@ -94,13 +94,13 @@ 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 allocsite = Allocsite.make 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 allocsite ~stride ~offset ~size |> Dom.Val.set_traces traces in
let v = Dom.Val.of_array_alloc allocsite ~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)
@ -193,8 +193,8 @@ let set_array_length array length_exp =
| Exp.Lvar array_pvar, {Typ.desc= Typ.Tarray {elt; stride}} ->
let length = Sem.eval length_exp mem |> Dom.Val.get_itv in
let stride = Option.map ~f:IntLit.to_int_exn stride in
let allocsite = Sem.get_allocsite pname ~node_hash ~inst_num:0 ~dimension:1 in
let v = Sem.eval_array_alloc allocsite ~stride ~offset:Itv.zero ~size:length in
let allocsite = Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 in
let v = Dom.Val.of_array_alloc allocsite ~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)
| _ ->
@ -322,7 +322,7 @@ module ArrayList = struct
let new_list _ =
let exec {pname; node_hash; location} ~ret:(id, _) mem =
let loc = Loc.of_id id in
let allocsite = Sem.get_allocsite pname ~node_hash ~inst_num:0 ~dimension:1 in
let allocsite = Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 in
let alloc_loc = Loc.of_allocsite allocsite in
let init_size = Dom.Val.of_int 0 in
let traces = TraceSet.add_elem (Trace.ArrDecl location) (Dom.Val.get_traces init_size) in

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

@ -269,21 +269,6 @@ 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 -> 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
let inst_num = string_of_int inst_num in
let dimension = string_of_int dimension in
proc_name ^ "-" ^ node_num ^ "-" ^ inst_num ^ "-" ^ dimension |> Allocsite.make
let eval_array_alloc : Allocsite.t -> stride:int option -> offset:Itv.t -> size:Itv.t -> Val.t =
fun allocsite ~stride ~offset ~size ->
let stride = Option.value_map stride ~default:Itv.nat ~f:Itv.of_int in
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)

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

@ -41,9 +41,9 @@ module Exec = struct
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 allocsite = Allocsite.make pname ~node_hash ~inst_num ~dimension in
let arr =
Sem.eval_array_alloc allocsite ~stride ~offset ~size
Dom.Val.of_array_alloc allocsite ~stride ~offset ~size
|> Dom.Val.add_trace_elem (Trace.ArrDecl location)
in
let mem =
@ -61,7 +61,7 @@ module Exec = struct
: Typ.Procname.t -> node_hash:int -> Location.t -> Loc.t -> inst_num:int -> dimension:int
-> Dom.Mem.astate -> Dom.Mem.astate * int =
fun pname ~node_hash location loc ~inst_num ~dimension mem ->
let allocsite = Sem.get_allocsite pname ~node_hash ~inst_num ~dimension in
let allocsite = Allocsite.make pname ~node_hash ~inst_num ~dimension in
let alloc_loc = Loc.of_allocsite allocsite in
let alist =
Dom.Val.of_pow_loc (PowLoc.singleton alloc_loc)
@ -98,16 +98,16 @@ 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 allocsite = Allocsite.make pname ~node_hash ~inst_num ~dimension:alloc_num in
let arr =
Sem.eval_array_alloc allocsite ~stride:None ~offset ~size |> Dom.Val.add_trace_elem elem
Dom.Val.of_array_alloc allocsite ~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 deref_loc =
Loc.of_allocsite (Sem.get_allocsite pname ~node_hash ~inst_num ~dimension:alloc_num)
Loc.of_allocsite (Allocsite.make pname ~node_hash ~inst_num ~dimension:alloc_num)
in
let path = Itv.SymbolPath.index path in
decl_sym_val pname path tenv ~node_hash location ~depth deref_loc typ mem
@ -121,7 +121,7 @@ module Exec = struct
mem ->
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 allocsite = Allocsite.make pname ~node_hash ~inst_num ~dimension:alloc_num in
let alloc_loc = Loc.of_allocsite allocsite in
let v = Dom.Val.of_pow_loc (PowLoc.singleton alloc_loc) |> Dom.Val.add_trace_elem elem in
L.(debug BufferOverrun Verbose) "alloc_num:%d, depth:%d \n" alloc_num depth ;
@ -153,9 +153,9 @@ module Exec = struct
Itv.plus i length )
in
let stride = Option.map stride ~f:IntLit.to_int_exn in
let allocsite = Sem.get_allocsite pname ~node_hash ~inst_num ~dimension in
let allocsite = Allocsite.make pname ~node_hash ~inst_num ~dimension in
let offset, size = (Itv.zero, length) in
let v = Sem.eval_array_alloc allocsite ~stride ~offset ~size in
let v = Dom.Val.of_array_alloc allocsite ~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
| _ ->

Write Preview
Loading…
Cancel
Save