From 2287910968c946cf9e79d6f8c5b7f4e42ba7e4ae Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Sat, 18 Jan 2020 03:36:44 -0800 Subject: [PATCH] [inferbo] Precise unknown value depending on type Summary: This diff revises the generation of unknown value. If the type of the unknown value generating is int, it does not add the "Unknown" pointer/array value. Reviewed By: ngorogiannis Differential Revision: D19392696 fbshipit-source-id: e1b3c9a3a --- .../bufferoverrun/bufferOverrunAnalysis.ml | 20 ++++++------- .../src/bufferoverrun/bufferOverrunDomain.ml | 28 ++++++++++--------- .../src/bufferoverrun/bufferOverrunDomain.mli | 6 ++-- .../src/bufferoverrun/bufferOverrunModels.ml | 8 +++--- 4 files changed, 32 insertions(+), 30 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index efcc1b215..0e0fe48f8 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -274,7 +274,7 @@ module TransferFunctions = struct None - let load_global_constant get_summary id pvar location mem ~find_from_initializer = + let load_global_constant get_summary ((id, _) as ret) pvar location mem ~find_from_initializer = match Pvar.get_initializer_pname pvar with | Some callee_pname -> ( match get_summary callee_pname with @@ -284,11 +284,11 @@ module TransferFunctions = struct | None -> L.d_printfln_escaped "/!\\ Unknown initializer of global constant %a" (Pvar.pp Pp.text) pvar ; - Dom.Mem.add_unknown_from id ~callee_pname ~location mem ) + Dom.Mem.add_unknown_from ret ~callee_pname ~location mem ) | None -> L.d_printfln_escaped "/!\\ Failed to get initializer name of global constant %a" (Pvar.pp Pp.text) pvar ; - Dom.Mem.add_unknown id ~location mem + Dom.Mem.add_unknown ret ~location mem let exec_instr : Dom.Mem.t -> extras ProcData.t -> CFG.Node.t -> Sil.instr -> Dom.Mem.t = @@ -297,13 +297,13 @@ module TransferFunctions = struct match instr with | Load {id} when Ident.is_none id -> mem - | Load {id; e= Exp.Lvar pvar; loc= location} + | Load {id; e= Exp.Lvar pvar; typ; loc= location} when Pvar.is_compile_constant pvar || Pvar.is_ice pvar -> - load_global_constant get_summary id pvar location mem + load_global_constant get_summary (id, typ) pvar location mem ~find_from_initializer:(fun callee_mem -> Dom.Mem.find (Loc.of_pvar pvar) callee_mem) - | Load {id; e= Exp.Lindex (Exp.Lvar pvar, _); loc= location} + | Load {id; e= Exp.Lindex (Exp.Lvar pvar, _); typ; loc= location} when Pvar.is_compile_constant pvar || Pvar.is_ice pvar -> - load_global_constant get_summary id pvar location mem + load_global_constant get_summary (id, typ) pvar location mem ~find_from_initializer:(fun callee_mem -> let locs = Dom.Mem.find (Loc.of_pvar pvar) callee_mem |> Dom.Val.get_all_locs in Dom.Mem.find_set locs callee_mem ) @@ -408,11 +408,11 @@ module TransferFunctions = struct L.(debug BufferOverrun Verbose) "/!\\ Non-static call to unknown %a \n\n" Procname.pp callee_pname ; assign_symbolic_pname_value callee_pname params ret location mem ) - else Dom.Mem.add_unknown_from id ~callee_pname ~location mem ) ) - | Call ((id, _), fun_exp, _, location, _) -> + else Dom.Mem.add_unknown_from ret ~callee_pname ~location mem ) ) + | Call (((id, _) as ret), fun_exp, _, location, _) -> let mem = Dom.Mem.add_stack_loc (Loc.of_id id) mem in L.d_printfln_escaped "/!\\ Call to non-const function %a" Exp.pp fun_exp ; - Dom.Mem.add_unknown id ~location mem + Dom.Mem.add_unknown ret ~location mem | Metadata (VariableLifetimeBegins (pvar, typ, location)) when Pvar.is_global pvar -> let model_env = let pname = Summary.get_proc_name summary in diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index b7f836987..ca7bf9cee 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -126,15 +126,16 @@ module Val = struct ArrayBlk.pp x.arrayblk trace_pp x.traces - let unknown_from : callee_pname:_ -> location:_ -> t = - fun ~callee_pname ~location -> + let unknown_from : Typ.t -> callee_pname:_ -> location:_ -> t = + fun typ ~callee_pname ~location -> + let is_int = Typ.is_int typ in let traces = Trace.(Set.singleton_final location (UnknownFrom callee_pname)) in { itv= Itv.top ; itv_thresholds= ItvThresholds.empty ; itv_updated_by= ItvUpdatedBy.Top ; modeled_range= ModeledRange.bottom - ; powloc= PowLoc.unknown - ; arrayblk= ArrayBlk.unknown + ; powloc= (if is_int then PowLoc.bottom else PowLoc.unknown) + ; arrayblk= (if is_int then ArrayBlk.bottom else ArrayBlk.unknown) ; traces } @@ -1984,10 +1985,10 @@ module MemReach = struct PowLoc.fold (fun l acc -> add_heap ?represents_multiple_values l v acc) locs m - let add_unknown_from : Ident.t -> callee_pname:Procname.t option -> location:Location.t -> t -> t - = - fun id ~callee_pname ~location m -> - let val_unknown = Val.unknown_from ~callee_pname ~location in + let add_unknown_from : + Ident.t * Typ.t -> callee_pname:Procname.t option -> location:Location.t -> t -> t = + fun (id, typ) ~callee_pname ~location m -> + let val_unknown = Val.unknown_from typ ~callee_pname ~location in add_stack (Loc.of_id id) val_unknown m |> add_heap Loc.unknown val_unknown @@ -2356,13 +2357,14 @@ module Mem = struct map ~f:(MemReach.add_heap_set ?represents_multiple_values ploc v) - let add_unknown_from : Ident.t -> callee_pname:Procname.t -> location:Location.t -> t -> t = - fun id ~callee_pname ~location -> - map ~f:(MemReach.add_unknown_from id ~callee_pname:(Some callee_pname) ~location) + let add_unknown_from : Ident.t * Typ.t -> callee_pname:Procname.t -> location:Location.t -> t -> t + = + fun ret ~callee_pname ~location -> + map ~f:(MemReach.add_unknown_from ret ~callee_pname:(Some callee_pname) ~location) - let add_unknown : Ident.t -> location:Location.t -> t -> t = - fun id ~location -> map ~f:(MemReach.add_unknown_from id ~callee_pname:None ~location) + let add_unknown : Ident.t * Typ.t -> location:Location.t -> t -> t = + fun ret ~location -> map ~f:(MemReach.add_unknown_from ret ~callee_pname:None ~location) let strong_update : PowLoc.t -> Val.t -> t -> t = fun p v -> map ~f:(MemReach.strong_update p v) diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.mli b/infer/src/bufferoverrun/bufferOverrunDomain.mli index f4e6dd4cc..2349e7068 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.mli +++ b/infer/src/bufferoverrun/bufferOverrunDomain.mli @@ -83,7 +83,7 @@ module Val : sig val unknown_locs : t - val unknown_from : callee_pname:Procname.t option -> location:Location.t -> t + val unknown_from : Typ.t -> callee_pname:Procname.t option -> location:Location.t -> t (** Unknown return value of [callee_pname] *) val is_mone : t -> bool @@ -502,10 +502,10 @@ module Mem : sig val add_heap_set : ?represents_multiple_values:bool -> AbsLoc.PowLoc.t -> Val.t -> t -> t - val add_unknown : Ident.t -> location:Location.t -> t -> t + val add_unknown : Ident.t * Typ.t -> location:Location.t -> t -> t (** Add an unknown value for stack variables *) - val add_unknown_from : Ident.t -> callee_pname:Procname.t -> location:Location.t -> t -> t + val add_unknown_from : Ident.t * Typ.t -> callee_pname:Procname.t -> location:Location.t -> t -> t (** Add an unknown return value of [callee_pname] for stack variables *) val remove_temps : Ident.t list -> t -> t diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 08ac38c5a..5dabaf235 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -26,9 +26,9 @@ type model = {exec: exec_fun; check: check_fun} let no_check _model_env _mem cond_set = cond_set let no_model = - let exec {pname; location} ~ret:(id, _) mem = + let exec {pname; location} ~ret mem = L.d_printfln_escaped "No model for %a" Procname.pp pname ; - Dom.Mem.add_unknown_from id ~callee_pname:pname ~location mem + Dom.Mem.add_unknown_from ret ~callee_pname:pname ~location mem in {exec; check= no_check} @@ -565,10 +565,10 @@ module ArrObjCommon = struct let at arr_exp ~fn index_exp = - let exec ({pname; location} as model_env) ~ret:(id, _) mem = + let exec ({pname; location} as model_env) ~ret:(id, typ) mem = let array_v = let locs = deref_of model_env arr_exp ~fn mem in - if PowLoc.is_bot locs then Dom.Val.unknown_from ~callee_pname:(Some pname) ~location + if PowLoc.is_bot locs then Dom.Val.unknown_from typ ~callee_pname:(Some pname) ~location else Dom.Mem.find_set locs mem in Dom.Mem.add_stack (Loc.of_id id) array_v mem