diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index ada690666..5a7920236 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -93,7 +93,8 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct let length = Sem.eval length0 mem in let traces = TraceSet.add_elem (Trace.ArrDecl location) (Dom.Val.get_traces length) in let v = - Sem.eval_array_alloc pname ~node_hash typ ?stride Itv.zero (Dom.Val.get_itv length) 0 1 + 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 in mem |> Dom.Mem.add_stack (Loc.of_id id) v @@ -202,7 +203,10 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct | 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 Itv.zero length 0 1 in + let v = + Sem.eval_array_alloc pname ~node_hash elt ~stride ~offset:Itv.zero ~size:length + ~inst_num:0 ~dimension:1 + 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/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 68aee279a..cba14f6f0 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -318,8 +318,8 @@ module Make (CFG : ProcCfg.S) = struct Val.bot - let get_allocsite : Typ.Procname.t -> node_hash:int -> int -> int -> string = - fun proc_name ~node_hash inst_num dimension -> + let get_allocsite : Typ.Procname.t -> node_hash:int -> inst_num:int -> dimension:int -> string = + 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 @@ -328,11 +328,11 @@ module Make (CFG : ProcCfg.S) = struct let eval_array_alloc - : Typ.Procname.t -> node_hash:int -> Typ.t -> ?stride:int -> Itv.t -> Itv.t -> int -> int - -> Val.t = - fun pdesc ~node_hash typ ?stride:stride0 offset size inst_num dimension -> - let allocsite = get_allocsite pdesc ~node_hash inst_num dimension in - let int_stride = match stride0 with None -> sizeof typ | Some stride -> stride in + : 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 + 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 diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index a399da580..ef731f1ed 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -81,14 +81,15 @@ module Make (CFG : ProcCfg.S) = struct fun ~decl_local pname ~node_hash location loc typ ~length ?stride ~inst_num ~dimension mem -> let size = Option.value_map ~default:Itv.top ~f:Itv.of_int_lit length in let arr = - Sem.eval_array_alloc pname ~node_hash typ Itv.zero size ?stride inst_num dimension + Sem.eval_array_alloc pname ~node_hash typ ~stride ~offset:Itv.zero ~size ~inst_num + ~dimension |> 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 loc = Loc.of_allocsite (Sem.get_allocsite pname ~node_hash ~inst_num ~dimension) in let mem, _ = decl_local pname ~node_hash location loc typ ~inst_num ~dimension:(dimension + 1) mem in @@ -113,11 +114,14 @@ module Make (CFG : ProcCfg.S) = struct let alloc_num = Itv.Counter.next new_alloc_num in let elem = Trace.SymAssign (loc, location) in let arr = - Sem.eval_array_alloc pname ~node_hash typ offset size inst_num alloc_num + Sem.eval_array_alloc pname ~node_hash typ ~stride:None ~offset ~size ~inst_num + ~dimension:alloc_num |> Dom.Val.add_trace_elem elem 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 alloc_num) in + let deref_loc = + Loc.of_allocsite (Sem.get_allocsite pname ~node_hash ~inst_num ~dimension:alloc_num) + in decl_sym_val pname tenv ~node_hash location ~depth deref_loc typ mem @@ -135,8 +139,8 @@ module Make (CFG : ProcCfg.S) = struct in let stride = Option.map stride ~f:IntLit.to_int in let v = - Sem.eval_array_alloc pname ~node_hash typ ?stride Itv.zero length inst_num - dimension + 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 | _ ->