From 364099530e1bb6397d5633a58ca4c5b71a7376c8 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Tue, 21 Aug 2018 00:59:07 -0700 Subject: [PATCH] [inferbo] Retrieve callee_pdesc and payload at the same time Reviewed By: jvillard Differential Revision: D9378011 fbshipit-source-id: c67c46e12 --- infer/src/absint/SummaryPayload.ml | 2 + infer/src/absint/SummaryPayload.mli | 3 + .../src/bufferoverrun/bufferOverrunChecker.ml | 87 ++++++++++--------- .../src/bufferoverrun/bufferOverrunDomain.ml | 10 +++ 4 files changed, 59 insertions(+), 43 deletions(-) diff --git a/infer/src/absint/SummaryPayload.ml b/infer/src/absint/SummaryPayload.ml index c8d83337b..7589e3f28 100644 --- a/infer/src/absint/SummaryPayload.ml +++ b/infer/src/absint/SummaryPayload.ml @@ -20,6 +20,8 @@ module type S = sig val update_summary : t -> Summary.t -> Summary.t + val of_summary : Summary.t -> t option + val read : Procdesc.t -> Typ.Procname.t -> t option end diff --git a/infer/src/absint/SummaryPayload.mli b/infer/src/absint/SummaryPayload.mli index 3de9f5023..ba877195b 100644 --- a/infer/src/absint/SummaryPayload.mli +++ b/infer/src/absint/SummaryPayload.mli @@ -23,6 +23,9 @@ module type S = sig val update_summary : t -> Summary.t -> Summary.t (** Update the corresponding part of the payload in the procedure summary *) + val of_summary : Summary.t -> t option + (** Read the corresponding part of the payload from the procedure summary *) + val read : Procdesc.t -> Typ.Procname.t -> t option (** Return the payload for the given procedure. Runs the analysis on-demand if necessary. *) end diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 524866662..7dc772f69 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -103,25 +103,21 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let instantiate_mem - : Tenv.t -> Ident.t * Typ.t -> Procdesc.t option -> Typ.Procname.t -> (Exp.t * Typ.t) list + : Tenv.t -> Ident.t * Typ.t -> Procdesc.t -> Typ.Procname.t -> (Exp.t * Typ.t) list -> Dom.Mem.astate -> Dom.Summary.t -> Location.t -> Dom.Mem.astate = fun tenv ret callee_pdesc callee_pname params caller_mem summary location -> let callee_symbol_table = Dom.Summary.get_symbol_table summary in let callee_exit_mem = Dom.Summary.get_output summary in - match callee_pdesc with - | Some pdesc -> - let bound_subst_map, ret_alias, rel_subst_map = - Sem.get_subst_map tenv pdesc params caller_mem callee_symbol_table callee_exit_mem - in - let caller_mem = - instantiate_ret ret callee_pname ~callee_exit_mem bound_subst_map caller_mem ret_alias - location - |> instantiate_param tenv pdesc params callee_exit_mem bound_subst_map location - |> forget_ret_relation ret callee_pname - in - Dom.Mem.instantiate_relation rel_subst_map ~caller:caller_mem ~callee:callee_exit_mem - | None -> - caller_mem + let bound_subst_map, ret_alias, rel_subst_map = + Sem.get_subst_map tenv callee_pdesc params caller_mem callee_symbol_table callee_exit_mem + in + let caller_mem = + instantiate_ret ret callee_pname ~callee_exit_mem bound_subst_map caller_mem ret_alias + location + |> instantiate_param tenv callee_pdesc params callee_exit_mem bound_subst_map location + |> forget_ret_relation ret callee_pname + in + Dom.Mem.instantiate_relation rel_subst_map ~caller:caller_mem ~callee:callee_exit_mem let print_debug_info : Sil.instr -> Dom.Mem.astate -> Dom.Mem.astate -> unit = @@ -175,7 +171,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct mem | Prune (exp, _, _, _) -> Sem.Prune.prune exp mem - | Call (ret, Const (Cfun callee_pname), params, location, _) -> ( + | Call (((id, _) as ret), Const (Cfun callee_pname), params, location, _) -> ( match Models.Call.dispatch tenv callee_pname params with | Some {Models.exec} -> let node_hash = CFG.Node.hash node in @@ -184,18 +180,23 @@ module TransferFunctions (CFG : ProcCfg.S) = struct in exec model_env ~ret mem | None -> - match Payload.read pdesc callee_pname with - | Some summary -> - let callee = Ondemand.get_proc_desc callee_pname in - instantiate_mem tenv ret callee callee_pname params mem summary location + match Ondemand.analyze_proc_name ~caller_pdesc:pdesc callee_pname with + | Some callee_summary -> ( + match Payload.of_summary callee_summary with + | Some payload -> + let callee_pdesc = Summary.get_proc_desc callee_summary in + instantiate_mem tenv ret callee_pdesc callee_pname params mem payload location + | None -> + (* This may happen for procedures with a biabduction model. *) + L.(debug BufferOverrun Verbose) + "/!\\ Call to %a at %a has no inferbo payload@\n" Typ.Procname.pp callee_pname + Location.pp location ; + Dom.Mem.add_unknown_from id ~callee_pname ~location mem ) | None -> L.(debug BufferOverrun Verbose) "/!\\ Unknown call to %a at %a@\n" Typ.Procname.pp callee_pname Location.pp location ; - let id = fst ret in - let val_unknown = Dom.Val.unknown_from ~callee_pname ~location in - Dom.Mem.add_stack (Loc.of_id id) val_unknown mem - |> Dom.Mem.add_heap Loc.unknown val_unknown ) + Dom.Mem.add_unknown_from id ~callee_pname ~location mem ) | Call (_, fun_exp, _, location, _) -> let () = L.(debug BufferOverrun Verbose) @@ -449,23 +450,19 @@ module Report = struct let instantiate_cond - : Tenv.t -> Typ.Procname.t -> Procdesc.t option -> (Exp.t * Typ.t) list -> Dom.Mem.astate + : Tenv.t -> Typ.Procname.t -> Procdesc.t -> (Exp.t * Typ.t) list -> Dom.Mem.astate -> Payload.t -> Location.t -> PO.ConditionSet.t = fun tenv caller_pname callee_pdesc params caller_mem summary location -> let callee_symbol_table = Dom.Summary.get_symbol_table summary in let callee_exit_mem = Dom.Summary.get_output summary in let callee_cond = Dom.Summary.get_cond_set summary in - match callee_pdesc with - | Some pdesc -> - let bound_subst_map, _, rel_subst_map = - Sem.get_subst_map tenv pdesc params caller_mem callee_symbol_table callee_exit_mem - in - let pname = Procdesc.get_proc_name pdesc in - let caller_rel = Dom.Mem.get_relation caller_mem in - PO.ConditionSet.subst callee_cond bound_subst_map rel_subst_map caller_rel caller_pname - pname location - | _ -> - callee_cond + let bound_subst_map, _, rel_subst_map = + Sem.get_subst_map tenv callee_pdesc params caller_mem callee_symbol_table callee_exit_mem + in + let pname = Procdesc.get_proc_name callee_pdesc in + let caller_rel = Dom.Mem.get_relation caller_mem in + PO.ConditionSet.subst callee_cond bound_subst_map rel_subst_map caller_rel caller_pname pname + location let check_instr @@ -482,13 +479,17 @@ module Report = struct let node_hash = CFG.Node.hash node in check (Models.mk_model_env pname node_hash location tenv symbol_table) mem cond_set | None -> - match Payload.read pdesc callee_pname with - | Some callee_summary -> - let callee = Ondemand.get_proc_desc callee_pname in - instantiate_cond tenv pname callee params mem callee_summary location - |> PO.ConditionSet.join cond_set - | _ -> - cond_set ) + match Ondemand.analyze_proc_name ~caller_pdesc:pdesc callee_pname with + | Some callee_summary -> ( + match Payload.of_summary callee_summary with + | Some callee_payload -> + let callee_pdesc = Summary.get_proc_desc callee_summary in + instantiate_cond tenv pname callee_pdesc params mem callee_payload location + |> PO.ConditionSet.join cond_set + | None -> + (* no inferbo payload *) cond_set ) + | None -> + (* unknown call *) cond_set ) | _ -> cond_set diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index b396e99c2..be65aaf6a 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -741,6 +741,12 @@ module MemReach = struct let add_heap : Loc.t -> Val.t -> t -> t = fun k v m -> {m with heap= Heap.add k v m.heap} + let add_unknown_from : Ident.t -> callee_pname:Typ.Procname.t -> location:Location.t -> t -> t = + fun id ~callee_pname ~location m -> + let val_unknown = Val.unknown_from ~callee_pname ~location in + add_stack (Loc.of_id id) val_unknown m |> add_heap Loc.unknown val_unknown + + let strong_update_heap : PowLoc.t -> Val.t -> t -> t = fun p v m -> {m with heap= Heap.strong_update p v m.heap} @@ -931,6 +937,10 @@ module Mem = struct let add_heap : Loc.t -> Val.t -> t -> t = fun k v -> f_lift (MemReach.add_heap k v) + let add_unknown_from : Ident.t -> callee_pname:Typ.Procname.t -> location:Location.t -> t -> t = + fun id ~callee_pname ~location -> f_lift (MemReach.add_unknown_from id ~callee_pname ~location) + + let strong_update_heap : PowLoc.t -> Val.t -> t -> t = fun p v -> f_lift (MemReach.strong_update_heap p v)