diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 5b6843862..29a7cce48 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -38,12 +38,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct type extras = Typ.Procname.t -> Procdesc.t option let declare_symbolic_val - : Typ.Procname.t -> Tenv.t -> CFG.node -> Location.t -> Loc.t -> Typ.typ -> inst_num:int + : Typ.Procname.t -> Tenv.t -> node_hash:int -> Location.t -> Loc.t -> Typ.typ -> inst_num:int -> new_sym_num:Itv.Counter.t -> Domain.t -> Domain.t = - fun pname tenv node location loc typ ~inst_num ~new_sym_num mem -> + fun pname tenv ~node_hash location loc typ ~inst_num ~new_sym_num mem -> let max_depth = 2 in let new_alloc_num = Itv.Counter.make 1 in - let rec decl_sym_val pname tenv node location ~depth ~may_last_field loc typ mem = + let rec decl_sym_val pname tenv ~node_hash location ~depth ~may_last_field loc typ mem = if depth > max_depth then mem else let depth = depth + 1 in @@ -62,8 +62,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct in Dom.Mem.add_heap loc v mem | Typ.Tptr (typ, _) -> - BoUtils.Exec.decl_sym_arr ~decl_sym_val:(decl_sym_val ~may_last_field) pname tenv node - location ~depth loc typ ~inst_num ~new_sym_num ~new_alloc_num mem + BoUtils.Exec.decl_sym_arr ~decl_sym_val:(decl_sym_val ~may_last_field) pname tenv + ~node_hash location ~depth loc typ ~inst_num ~new_sym_num ~new_alloc_num mem | Typ.Tarray {elt; length} -> let size = match length with @@ -75,18 +75,18 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let offset = Itv.zero in BoUtils.Exec.decl_sym_arr ~decl_sym_val:(decl_sym_val ~may_last_field:false) - pname tenv node location ~depth loc elt ~offset ?size ~inst_num ~new_sym_num + pname tenv ~node_hash location ~depth loc elt ~offset ?size ~inst_num ~new_sym_num ~new_alloc_num mem | Typ.Tstruct typename -> ( match Models.TypName.dispatch typename with | Some {Models.declare_symbolic} -> - let model_env = Models.mk_model_env pname node location tenv in + let model_env = Models.mk_model_env pname node_hash location tenv in declare_symbolic ~decl_sym_val:(decl_sym_val ~may_last_field) model_env ~depth loc ~inst_num ~new_sym_num ~new_alloc_num mem | None -> let decl_fld ~may_last_field mem (fn, typ, _) = let loc_fld = Loc.append_field loc ~fn in - decl_sym_val pname tenv node location ~depth loc_fld typ ~may_last_field mem + decl_sym_val pname tenv ~node_hash location ~depth loc_fld typ ~may_last_field mem in let decl_flds str = IList.fold_last ~f:(decl_fld ~may_last_field:false) @@ -98,20 +98,22 @@ module TransferFunctions (CFG : ProcCfg.S) = struct if Config.bo_debug >= 3 then L.(debug BufferOverrun Verbose) "/!\\ decl_fld of unhandled type: %a at %a@." (Typ.pp Pp.text) typ Location.pp - (CFG.loc node) ; + location ; mem in - decl_sym_val pname tenv node location ~depth:0 ~may_last_field:true loc typ mem + decl_sym_val pname tenv ~node_hash location ~depth:0 ~may_last_field:true loc typ mem let declare_symbolic_parameters - : Typ.Procname.t -> Tenv.t -> CFG.node -> Location.t -> inst_num:int -> (Pvar.t * Typ.t) list - -> Dom.Mem.astate -> Dom.Mem.astate = - fun pname tenv node location ~inst_num formals mem -> + : Typ.Procname.t -> Tenv.t -> node_hash:int -> Location.t -> inst_num:int + -> (Pvar.t * Typ.t) list -> Dom.Mem.astate -> Dom.Mem.astate = + fun pname tenv ~node_hash location ~inst_num formals mem -> let new_sym_num = Itv.Counter.make 0 in let add_formal (mem, inst_num) (pvar, typ) = let loc = Loc.of_pvar pvar in - let mem = declare_symbolic_val pname tenv node location loc typ ~inst_num ~new_sym_num mem in + let mem = + declare_symbolic_val pname tenv ~node_hash location loc typ ~inst_num ~new_sym_num mem + in (mem, inst_num + 1) in List.fold ~f:add_formal ~init:(mem, inst_num) formals |> fst @@ -249,7 +251,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Call (ret, Const Cfun callee_pname, params, location, _) -> ( match Models.Call.dispatch callee_pname params with | Some {Models.exec} -> - let model_env = Models.mk_model_env callee_pname node location tenv ?ret in + let node_hash = CFG.hash node in + let model_env = Models.mk_model_env callee_pname node_hash location tenv ?ret in exec model_env mem | None -> match Summary.read_summary pdesc callee_pname with @@ -265,16 +268,17 @@ module TransferFunctions (CFG : ProcCfg.S) = struct ) | Declare_locals (locals, location) -> (* array allocation in stack e.g., int arr[10] *) - let rec decl_local pname node location loc typ ~inst_num ~dimension mem = + let node_hash = CFG.hash node in + let rec decl_local pname ~node_hash location loc typ ~inst_num ~dimension mem = match typ.Typ.desc with | Typ.Tarray {elt= typ; length; stride} -> let stride = Option.map ~f:IntLit.to_int stride in - BoUtils.Exec.decl_local_array ~decl_local pname node location loc typ ~length + BoUtils.Exec.decl_local_array ~decl_local pname ~node_hash location loc typ ~length ?stride ~inst_num ~dimension mem | Typ.Tstruct typname -> ( match Models.TypName.dispatch typname with | Some {Models.declare_local} -> - let model_env = Models.mk_model_env pname node location tenv in + let model_env = Models.mk_model_env pname node_hash location tenv in declare_local ~decl_local model_env loc ~inst_num ~dimension mem | None -> (mem, inst_num) ) @@ -283,11 +287,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct in let try_decl_local (mem, inst_num) (pvar, typ) = let loc = Loc.of_pvar pvar in - decl_local pname node location loc typ ~inst_num ~dimension:1 mem + decl_local pname ~node_hash location loc typ ~inst_num ~dimension:1 mem in let mem, inst_num = List.fold ~f:try_decl_local ~init:(mem, 1) locals in let formals = Sem.get_formals pdesc in - declare_symbolic_parameters pname tenv node location ~inst_num formals mem + declare_symbolic_parameters pname tenv ~node_hash location ~inst_num formals mem | Call (_, fun_exp, _, location, _) -> let () = L.(debug BufferOverrun Verbose) @@ -455,7 +459,8 @@ module Report = struct | Sil.Call (_, Const Cfun callee_pname, params, location, _) -> ( match Models.Call.dispatch callee_pname params with | Some {Models.check} -> - check (Models.mk_model_env pname node location tenv) mem cond_set + let node_hash = CFG.hash node in + check (Models.mk_model_env pname node_hash location tenv) mem cond_set | None -> match Summary.read_summary pdesc callee_pname with | Some callee_summary -> diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 95e7124db..ada690666 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -22,12 +22,12 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct type model_env = { pname: Typ.Procname.t - ; node: CFG.node + ; node_hash: int ; location: Location.t ; tenv: Tenv.t ; ret: (Ident.t * Typ.t) option } - let mk_model_env pname node location ?ret tenv = {pname; node; location; tenv; ret} + let mk_model_env pname node_hash location ?ret tenv = {pname; node_hash; location; tenv; ret} type exec_fun = model_env -> Dom.Mem.astate -> Dom.Mem.astate @@ -73,19 +73,19 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct PO.ConditionSet.add_alloc_size pname location ~length traces cond_set - let set_uninitialized node (typ: Typ.t) ploc mem = + 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 | _ -> L.(debug BufferOverrun Verbose) "/!\\ Do not know how to uninitialize type %a at %a@\n" (Typ.pp Pp.text) typ Location.pp - (CFG.loc node) ; + location ; mem let malloc size_exp = - let exec {pname; ret; node; location; tenv} mem = + let exec {pname; ret; node_hash; location; tenv} mem = match ret with | Some (id, _) -> let size_exp = Prop.exp_normalize_noabs tenv Sil.sub_empty size_exp in @@ -93,16 +93,16 @@ 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 typ ?stride Itv.zero (Dom.Val.get_itv length) 0 1 + Sem.eval_array_alloc pname ~node_hash typ ?stride Itv.zero (Dom.Val.get_itv length) 0 1 |> Dom.Val.set_traces traces in mem |> Dom.Mem.add_stack (Loc.of_id id) v - |> set_uninitialized node typ (Dom.Val.get_array_locs v) - |> BoUtils.Exec.init_array_fields tenv pname node typ (Dom.Val.get_array_locs v) + |> set_uninitialized location typ (Dom.Val.get_array_locs v) + |> BoUtils.Exec.init_array_fields tenv pname ~node_hash typ (Dom.Val.get_array_locs v) ?dyn_length | _ -> L.(debug BufferOverrun Verbose) - "/!\\ Do not know where to model malloc at %a@\n" Location.pp (CFG.loc node) ; + "/!\\ Do not know where to model malloc at %a@\n" Location.pp location ; mem and check = check_alloc_size size_exp in {exec; check} @@ -197,14 +197,14 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct let set_array_length array length_exp = - let exec {pname; node} mem = + let exec {pname; node_hash; location} mem = match array with | 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 elt ?stride Itv.zero length 0 1 in + let v = Sem.eval_array_alloc pname ~node_hash elt ?stride Itv.zero length 0 1 in mem |> Dom.Mem.add_stack (Loc.of_pvar array_pvar) v - |> set_uninitialized node elt (Dom.Val.get_array_locs v) + |> set_uninitialized location elt (Dom.Val.get_array_locs v) | _ -> L.(die InternalError) "Unexpected type of first argument for __set_array_length()" and check = check_alloc_size length_exp in @@ -254,18 +254,18 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct module StdArray = struct let typ typ length = - let declare_local ~decl_local {pname; node; location} loc ~inst_num ~dimension mem = + let declare_local ~decl_local {pname; node_hash; location} loc ~inst_num ~dimension mem = (* should this be deferred to the constructor? *) let length = Some (IntLit.of_int64 length) in - BoUtils.Exec.decl_local_array ~decl_local pname node location loc typ ~length ~inst_num - ~dimension mem + BoUtils.Exec.decl_local_array ~decl_local pname ~node_hash location loc typ ~length + ~inst_num ~dimension mem in - let declare_symbolic ~decl_sym_val {pname; tenv; node; location} ~depth loc ~inst_num + let declare_symbolic ~decl_sym_val {pname; tenv; node_hash; location} ~depth loc ~inst_num ~new_sym_num ~new_alloc_num mem = let offset = Itv.zero in let size = Itv.of_int64 length in - BoUtils.Exec.decl_sym_arr ~decl_sym_val pname tenv node location ~depth loc typ ~offset - ~size ~inst_num ~new_sym_num ~new_alloc_num mem + BoUtils.Exec.decl_sym_arr ~decl_sym_val pname tenv ~node_hash location ~depth loc typ + ~offset ~size ~inst_num ~new_sym_num ~new_alloc_num mem in {declare_local; declare_symbolic} diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index fc990f9df..68aee279a 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -318,19 +318,20 @@ module Make (CFG : ProcCfg.S) = struct Val.bot - let get_allocsite : Typ.Procname.t -> CFG.node -> int -> int -> string = - fun proc_name node inst_num dimension -> + let get_allocsite : Typ.Procname.t -> node_hash:int -> int -> int -> string = + fun proc_name ~node_hash inst_num dimension -> let proc_name = Typ.Procname.to_string proc_name in - let node_num = CFG.hash node |> string_of_int 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 - : Typ.Procname.t -> CFG.node -> Typ.t -> ?stride:int -> Itv.t -> Itv.t -> int -> int -> Val.t = - fun pdesc node typ ?stride:stride0 offset size inst_num dimension -> - let allocsite = get_allocsite pdesc node inst_num dimension in + : 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 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 ba2b3a72d..0ad58d28b 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -25,26 +25,26 @@ module type S = sig val load_val : Ident.t -> Dom.Val.astate -> Dom.Mem.astate -> Dom.Mem.astate type decl_local = - Typ.Procname.t -> CFG.node -> Location.t -> Loc.t -> Typ.t -> inst_num:int -> dimension:int - -> Dom.Mem.astate -> Dom.Mem.astate * int + Typ.Procname.t -> node_hash:int -> Location.t -> Loc.t -> Typ.t -> inst_num:int + -> dimension:int -> Dom.Mem.astate -> Dom.Mem.astate * int val decl_local_array : - decl_local:decl_local -> Typ.Procname.t -> CFG.node -> Location.t -> Loc.t -> Typ.t + decl_local:decl_local -> Typ.Procname.t -> node_hash:int -> Location.t -> Loc.t -> Typ.t -> length:IntLit.t option -> ?stride:int -> inst_num:int -> dimension:int -> Dom.Mem.astate -> Dom.Mem.astate * int type decl_sym_val = - Typ.Procname.t -> Tenv.t -> CFG.node -> Location.t -> depth:int -> Loc.t -> Typ.t + Typ.Procname.t -> Tenv.t -> node_hash:int -> Location.t -> depth:int -> Loc.t -> Typ.t -> Dom.Mem.astate -> Dom.Mem.astate val decl_sym_arr : - decl_sym_val:decl_sym_val -> Typ.Procname.t -> Tenv.t -> CFG.node -> Location.t -> depth:int - -> Loc.t -> Typ.t -> ?offset:Itv.t -> ?size:Itv.t -> inst_num:int + decl_sym_val:decl_sym_val -> Typ.Procname.t -> Tenv.t -> node_hash:int -> Location.t + -> depth:int -> Loc.t -> Typ.t -> ?offset:Itv.t -> ?size:Itv.t -> inst_num:int -> new_sym_num:Itv.Counter.t -> new_alloc_num:Itv.Counter.t -> Dom.Mem.astate -> Dom.Mem.astate val init_array_fields : - Tenv.t -> Typ.Procname.t -> CFG.node -> Typ.t -> PowLoc.t -> ?dyn_length:Exp.t + Tenv.t -> Typ.Procname.t -> node_hash:int -> Typ.t -> PowLoc.t -> ?dyn_length:Exp.t -> Dom.Mem.astate -> Dom.Mem.astate val set_dyn_length : Tenv.t -> Typ.t -> PowLoc.t -> Itv.t -> Dom.Mem.astate -> Dom.Mem.astate @@ -71,41 +71,41 @@ module Make (CFG : ProcCfg.S) = struct type decl_local = - Typ.Procname.t -> CFG.node -> Location.t -> Loc.t -> Typ.t -> inst_num:int -> dimension:int - -> Dom.Mem.astate -> Dom.Mem.astate * int + Typ.Procname.t -> node_hash:int -> Location.t -> Loc.t -> Typ.t -> inst_num:int + -> dimension:int -> Dom.Mem.astate -> Dom.Mem.astate * int let decl_local_array - : decl_local:decl_local -> Typ.Procname.t -> CFG.node -> Location.t -> Loc.t -> Typ.t + : decl_local:decl_local -> Typ.Procname.t -> node_hash:int -> Location.t -> Loc.t -> Typ.t -> length:IntLit.t option -> ?stride:int -> inst_num:int -> dimension:int -> Dom.Mem.astate -> Dom.Mem.astate * int = - fun ~decl_local pname node location loc typ ~length ?stride ~inst_num ~dimension mem -> + 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 typ Itv.zero size ?stride inst_num dimension + Sem.eval_array_alloc pname ~node_hash typ Itv.zero size ?stride 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 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 location loc typ ~inst_num ~dimension:(dimension + 1) mem + decl_local pname ~node_hash location loc typ ~inst_num ~dimension:(dimension + 1) mem in (mem, inst_num + 1) type decl_sym_val = - Typ.Procname.t -> Tenv.t -> CFG.node -> Location.t -> depth:int -> Loc.t -> Typ.t + Typ.Procname.t -> Tenv.t -> node_hash:int -> Location.t -> depth:int -> Loc.t -> Typ.t -> Dom.Mem.astate -> Dom.Mem.astate let decl_sym_arr - : decl_sym_val:decl_sym_val -> Typ.Procname.t -> Tenv.t -> CFG.node -> Location.t + : decl_sym_val:decl_sym_val -> Typ.Procname.t -> Tenv.t -> node_hash:int -> Location.t -> depth:int -> Loc.t -> Typ.t -> ?offset:Itv.t -> ?size:Itv.t -> inst_num:int -> new_sym_num:Itv.Counter.t -> new_alloc_num:Itv.Counter.t -> Dom.Mem.astate -> Dom.Mem.astate = - fun ~decl_sym_val pname tenv node location ~depth loc typ ?offset ?size ~inst_num ~new_sym_num - ~new_alloc_num mem -> + fun ~decl_sym_val pname tenv ~node_hash location ~depth loc typ ?offset ?size ~inst_num + ~new_sym_num ~new_alloc_num mem -> let option_value opt_x default_f = match opt_x with Some x -> x | None -> default_f () in let itv_make_sym () = Itv.make_sym pname new_sym_num in let offset = option_value offset itv_make_sym in @@ -113,15 +113,15 @@ 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 typ offset size inst_num alloc_num + Sem.eval_array_alloc pname ~node_hash typ offset size inst_num 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 inst_num alloc_num) in - decl_sym_val pname tenv node location ~depth deref_loc typ mem + let deref_loc = Loc.of_allocsite (Sem.get_allocsite pname ~node_hash inst_num alloc_num) in + decl_sym_val pname tenv ~node_hash location ~depth deref_loc typ mem - let init_array_fields tenv pname node typ locs ?dyn_length mem = + let init_array_fields tenv pname ~node_hash typ locs ?dyn_length mem = let rec init_field locs dimension ?dyn_length (mem, inst_num) (field_name, field_typ, _) = let field_loc = PowLoc.append_field locs ~fn:field_name in let mem = @@ -135,7 +135,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 typ ?stride Itv.zero length inst_num dimension + Sem.eval_array_alloc pname ~node_hash typ ?stride Itv.zero length inst_num + dimension in Dom.Mem.strong_update_heap field_loc v mem | _ ->