From fec87c8b9542ab9887a2e85d0043bfb054c26d60 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Thu, 9 Aug 2018 03:38:25 -0700 Subject: [PATCH] [inferbo] Move functions constructing array values 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 --- infer/src/bufferoverrun/absLoc.ml | 9 ++++++++- infer/src/bufferoverrun/bufferOverrunDomain.ml | 7 ++++--- infer/src/bufferoverrun/bufferOverrunModels.ml | 10 +++++----- .../bufferoverrun/bufferOverrunSemantics.ml | 15 --------------- infer/src/bufferoverrun/bufferOverrunUtils.ml | 18 +++++++++--------- 5 files changed, 26 insertions(+), 33 deletions(-) diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml index 1b6f2023e..851810a1a 100644 --- a/infer/src/bufferoverrun/absLoc.ml +++ b/infer/src/bufferoverrun/absLoc.ml @@ -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 diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 879792a52..bf3068fb6 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -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 } diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 1c7657252..1e898d6aa 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -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 diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 46f571282..033bbcddc 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -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) diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index efa9b60a1..f5eb7757f 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -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 | _ ->