diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index daf493d68..7635567b3 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -17,7 +17,6 @@ module L = Logging module Models = BufferOverrunModels module Sem = BufferOverrunSemantics module Trace = BufferOverrunTrace -module TypModels = BufferOverrunTypModels module Payload = SummaryPayload.Make (struct type t = BufferOverrunSummary.t @@ -33,31 +32,17 @@ module CFG = ProcCfg.NormalOneInstrPerNode module Init = struct let initial_state {ProcData.pdesc; tenv; extras= oenv} start_node = - let node_hash = CFG.Node.hash start_node in - let location = CFG.Node.loc start_node in - let pname = Procdesc.get_proc_name pdesc in - let rec decl_local pname ~node_hash location loc typ ~inst_num ~represents_multiple_values - ~dimension mem = - match typ.Typ.desc with - | Typ.Tarray {elt= typ; length; stride} -> - let stride = Option.map ~f:IntLit.to_int_exn stride in - BoUtils.Exec.decl_local_array ~decl_local pname ~node_hash location loc typ ~length - ?stride ~inst_num ~represents_multiple_values ~dimension mem - | Typ.Tstruct typname -> ( - match TypModels.dispatch tenv typname with - | Some (CArray {element_typ; length}) -> - BoUtils.Exec.decl_local_array ~decl_local pname ~node_hash location loc element_typ - ~length:(Some length) ~inst_num ~represents_multiple_values ~dimension mem - | Some JavaCollection | None -> - (mem, inst_num) ) - | _ -> - (mem, inst_num) - in - let try_decl_local (mem, inst_num) {ProcAttributes.name; typ} = - let pvar = Pvar.mk name pname in - let loc = Loc.of_pvar pvar in - decl_local pname ~node_hash location loc typ ~inst_num ~represents_multiple_values:false - ~dimension:1 mem + let try_decl_local = + let pname = Procdesc.get_proc_name pdesc in + let model_env = + let node_hash = CFG.Node.hash start_node in + let location = CFG.Node.loc start_node in + let integer_type_widths = oenv.Dom.OndemandEnv.integer_type_widths in + BoUtils.ModelEnv.mk_model_env pname ~node_hash location tenv integer_type_widths + in + fun (mem, inst_num) {ProcAttributes.name; typ} -> + let loc = Loc.of_pvar (Pvar.mk name pname) in + BoUtils.Exec.decl_local model_env (mem, inst_num) (loc, typ) in let mem = Dom.Mem.init oenv in let mem, _ = List.fold ~f:try_decl_local ~init:(mem, 1) (Procdesc.get_locals pdesc) in @@ -185,10 +170,13 @@ module TransferFunctions = struct | Load (id, exp, _, _) -> BoUtils.Exec.load_locs id (Sem.eval_locs exp mem) mem | Store (exp1, _, Const (Const.Cstr s), location) -> - let pname = Procdesc.get_proc_name pdesc in - let node_hash = CFG.Node.hash node in let locs = Sem.eval_locs exp1 mem in - BoUtils.Exec.decl_string pname ~node_hash integer_type_widths location locs s mem + let model_env = + let pname = Procdesc.get_proc_name pdesc in + let node_hash = CFG.Node.hash node in + BoUtils.ModelEnv.mk_model_env pname ~node_hash location tenv integer_type_widths + in + BoUtils.Exec.decl_string model_env locs s mem | Store (exp1, _, exp2, location) -> let locs = Sem.eval_locs exp1 mem in let v = @@ -232,9 +220,10 @@ module TransferFunctions = struct 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 integer_type_widths + let node_hash = CFG.Node.hash node in + BoUtils.ModelEnv.mk_model_env callee_pname ~node_hash location tenv + integer_type_widths in exec model_env ~ret mem | None -> ( @@ -509,11 +498,12 @@ module Report = struct in match Models.Call.dispatch tenv callee_pname params with | Some {Models.check} -> - let node_hash = CFG.Node.hash node in - let pname = Procdesc.get_proc_name pdesc in - check - (Models.mk_model_env pname node_hash location tenv integer_type_widths) - mem cond_set + let model_env = + let node_hash = CFG.Node.hash node in + let pname = Procdesc.get_proc_name pdesc in + BoUtils.ModelEnv.mk_model_env pname ~node_hash location tenv integer_type_widths + in + check model_env mem cond_set | None -> ( match Ondemand.analyze_proc_name ~caller_pdesc:pdesc callee_pname with | Some callee_summary -> ( diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index b5a51563e..ba781fda0 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -15,17 +15,7 @@ module PO = BufferOverrunProofObligations module Sem = BufferOverrunSemantics module Relation = BufferOverrunDomainRelation module Trace = BufferOverrunTrace - -type model_env = - { pname: Typ.Procname.t - ; node_hash: int - ; location: Location.t - ; tenv: Tenv.t - ; integer_type_widths: Typ.IntegerWidths.t } - -let mk_model_env pname node_hash location tenv integer_type_widths = - {pname; node_hash; location; tenv; integer_type_widths} - +open BoUtils.ModelEnv type exec_fun = model_env -> ret:Ident.t * Typ.t -> Dom.Mem.t -> Dom.Mem.t @@ -77,7 +67,8 @@ let check_alloc_size size_exp {location; integer_type_widths} mem cond_set = let malloc size_exp = - let exec {pname; node_hash; location; tenv; integer_type_widths} ~ret:(id, _) mem = + let exec ({pname; node_hash; location; tenv; integer_type_widths} as model_env) ~ret:(id, _) mem + = let size_exp = Prop.exp_normalize_noabs tenv Sil.sub_empty size_exp in let typ, stride, length0, dyn_length = get_malloc_info size_exp in let length = Sem.eval integer_type_widths length0 mem in @@ -96,8 +87,7 @@ let malloc size_exp = mem |> Dom.Mem.add_stack (Loc.of_id id) v |> Dom.Mem.init_array_relation allocsite ~offset_opt:(Some offset) ~size ~size_exp_opt - |> BoUtils.Exec.init_c_array_fields tenv integer_type_widths pname path ~node_hash typ - (Dom.Val.get_array_locs v) ?dyn_length + |> BoUtils.Exec.init_c_array_fields model_env path typ (Dom.Val.get_array_locs v) ?dyn_length and check = check_alloc_size size_exp in {exec; check} @@ -128,7 +118,7 @@ let memset arr_exp size_exp = let realloc src_exp size_exp = - let exec {location; tenv; integer_type_widths} ~ret:(id, _) mem = + let exec ({location; tenv; integer_type_widths} as model_env) ~ret:(id, _) mem = let size_exp = Prop.exp_normalize_noabs tenv Sil.sub_empty size_exp in let typ, _, length0, dyn_length = get_malloc_info size_exp in let length = Sem.eval integer_type_widths length0 mem in @@ -138,7 +128,7 @@ let realloc src_exp size_exp = let mem = Dom.Mem.add_stack (Loc.of_id id) v mem in Option.value_map dyn_length ~default:mem ~f:(fun dyn_length -> let dyn_length = Dom.Val.get_itv (Sem.eval integer_type_widths dyn_length mem) in - BoUtils.Exec.set_dyn_length location tenv typ (Dom.Val.get_array_locs v) dyn_length mem ) + BoUtils.Exec.set_dyn_length model_env typ (Dom.Val.get_array_locs v) dyn_length mem ) and check = check_alloc_size size_exp in {exec; check} @@ -346,11 +336,11 @@ module StdBasicString = struct (* The (5) constructor in https://en.cppreference.com/w/cpp/string/basic_string/basic_string *) let constructor_from_char_ptr_without_len tgt src = - let exec {pname; node_hash; location; integer_type_widths} ~ret:_ mem = + let exec ({integer_type_widths} as model_env) ~ret:_ mem = match src with | Exp.Const (Const.Cstr s) -> let locs = Sem.eval_locs tgt mem in - BoUtils.Exec.decl_string pname ~node_hash integer_type_widths location locs s mem + BoUtils.Exec.decl_string model_env locs s mem | _ -> let tgt_locs = Sem.eval_locs tgt mem in let v = Sem.eval integer_type_widths src mem in diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index fddc20f62..85e7df5a7 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -15,8 +15,23 @@ module PO = BufferOverrunProofObligations module Sem = BufferOverrunSemantics module Trace = BufferOverrunTrace module TraceSet = Trace.Set +module TypModels = BufferOverrunTypModels + +module ModelEnv = struct + type model_env = + { pname: Typ.Procname.t + ; node_hash: int + ; location: Location.t + ; tenv: Tenv.t + ; integer_type_widths: Typ.IntegerWidths.t } + + let mk_model_env pname ~node_hash location tenv integer_type_widths = + {pname; node_hash; location; tenv; integer_type_widths} +end module Exec = struct + open ModelEnv + let load_locs id locs mem = let v = Dom.Mem.find_set locs mem in let mem = Dom.Mem.add_stack (Loc.of_id id) v mem in @@ -31,34 +46,26 @@ module Exec = struct let load_val id v mem = load_locs id (Dom.Val.get_all_locs v) mem - type decl_local = - Typ.Procname.t - -> node_hash:int - -> Location.t - -> Loc.t - -> Typ.t - -> inst_num:int - -> represents_multiple_values:bool - -> dimension:int - -> Dom.Mem.t - -> Dom.Mem.t * int + let rec decl_local_loc ({tenv} as model_env) loc typ ~inst_num ~represents_multiple_values + ~dimension mem = + match typ.Typ.desc with + | Typ.Tarray {elt= typ; length; stride} -> + let stride = Option.map ~f:IntLit.to_int_exn stride in + decl_local_array model_env loc typ ~length ?stride ~inst_num ~represents_multiple_values + ~dimension mem + | Typ.Tstruct typname -> ( + match TypModels.dispatch tenv typname with + | Some (CArray {element_typ; length}) -> + decl_local_array model_env loc element_typ ~length:(Some length) ~inst_num + ~represents_multiple_values ~dimension mem + | Some JavaCollection | None -> + (mem, inst_num) ) + | _ -> + (mem, inst_num) + - let decl_local_array : - 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 - -> represents_multiple_values:bool - -> dimension:int - -> Dom.Mem.t - -> Dom.Mem.t * int = - fun ~decl_local pname ~node_hash location loc typ ~length ?stride ~inst_num - ~represents_multiple_values ~dimension mem -> + and decl_local_array ({pname; node_hash; location} as model_env) loc typ ~length ?stride + ~inst_num ~represents_multiple_values ~dimension mem = let size = Option.value_map ~default:Itv.top ~f:Itv.of_int_lit length in let path = Loc.get_path loc in let allocsite = @@ -81,13 +88,18 @@ module Exec = struct in let loc = Loc.of_allocsite allocsite in let mem, _ = - decl_local pname ~node_hash location loc typ ~inst_num ~represents_multiple_values:true + decl_local_loc model_env loc typ ~inst_num ~represents_multiple_values:true ~dimension:(dimension + 1) mem in (mem, inst_num + 1) - let init_c_array_fields tenv integer_type_widths pname path ~node_hash typ locs ?dyn_length mem = + let decl_local model_env (mem, inst_num) (loc, typ) = + decl_local_loc model_env loc typ ~inst_num ~represents_multiple_values:false ~dimension:1 mem + + + let init_c_array_fields {pname; node_hash; tenv; integer_type_widths} path typ locs ?dyn_length + mem = let rec init_field path locs dimension ?dyn_length (mem, inst_num) (field_name, field_typ, _) = let field_path = Option.map path ~f:(fun path -> Symb.SymbolPath.field path field_name) in let field_loc = PowLoc.append_field locs ~fn:field_name in @@ -133,7 +145,7 @@ module Exec = struct init_fields path typ locs 1 ?dyn_length mem - let rec set_dyn_length location tenv typ locs dyn_length mem = + let rec set_dyn_length ({location; tenv} as model_env) typ locs dyn_length mem = match typ.Typ.desc with | Tstruct typename -> ( match Tenv.lookup tenv typename with @@ -148,7 +160,7 @@ module Exec = struct in Dom.Mem.strong_update field_loc v mem | _ -> - set_dyn_length location tenv field_typ field_loc dyn_length mem ) + set_dyn_length model_env field_typ field_loc dyn_length mem ) | _ -> mem ) | _ -> @@ -157,7 +169,7 @@ module Exec = struct let get_max_char s = String.fold s ~init:0 ~f:(fun acc c -> max acc (Char.to_int c)) - let decl_string pname ~node_hash integer_type_widths location locs s mem = + let decl_string {pname; node_hash; location; integer_type_widths} locs s mem = let stride = Some (Typ.width_of_ikind integer_type_widths IChar / 8) in let offset = Itv.zero in let size = Itv.of_int (String.length s + 1) in diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.mli b/infer/src/bufferoverrun/bufferOverrunUtils.mli index 96e92744b..89c1dd025 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.mli +++ b/infer/src/bufferoverrun/bufferOverrunUtils.mli @@ -11,61 +11,37 @@ module Dom = BufferOverrunDomain module Relation = BufferOverrunDomainRelation module PO = BufferOverrunProofObligations +module ModelEnv : sig + type model_env = + { pname: Typ.Procname.t + ; node_hash: int + ; location: Location.t + ; tenv: Tenv.t + ; integer_type_widths: Typ.IntegerWidths.t } + + val mk_model_env : + Typ.Procname.t -> node_hash:int -> Location.t -> Tenv.t -> Typ.IntegerWidths.t -> model_env +end + module Exec : sig val load_locs : Ident.t -> PowLoc.t -> Dom.Mem.t -> Dom.Mem.t val load_val : Ident.t -> Dom.Val.t -> Dom.Mem.t -> Dom.Mem.t - type decl_local = - Typ.Procname.t - -> node_hash:int - -> Location.t - -> Loc.t - -> Typ.t - -> inst_num:int - -> represents_multiple_values:bool - -> dimension:int - -> Dom.Mem.t - -> Dom.Mem.t * int - - val decl_local_array : - 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 - -> represents_multiple_values:bool - -> dimension:int - -> Dom.Mem.t - -> Dom.Mem.t * int + val decl_local : ModelEnv.model_env -> Dom.Mem.t * int -> Loc.t * Typ.t -> Dom.Mem.t * int val init_c_array_fields : - Tenv.t - -> Typ.IntegerWidths.t - -> Typ.Procname.t + ModelEnv.model_env -> Itv.SymbolPath.partial option - -> node_hash:int -> Typ.t -> PowLoc.t -> ?dyn_length:Exp.t -> Dom.Mem.t -> Dom.Mem.t - val set_dyn_length : Location.t -> Tenv.t -> Typ.t -> PowLoc.t -> Itv.t -> Dom.Mem.t -> Dom.Mem.t + val set_dyn_length : ModelEnv.model_env -> Typ.t -> PowLoc.t -> Itv.t -> Dom.Mem.t -> Dom.Mem.t - val decl_string : - Typ.Procname.t - -> node_hash:int - -> Typ.IntegerWidths.t - -> Location.t - -> PowLoc.t - -> string - -> Dom.Mem.t - -> Dom.Mem.t + val decl_string : ModelEnv.model_env -> PowLoc.t -> string -> Dom.Mem.t -> Dom.Mem.t end module Check : sig