From e4bb3c9d685d065c46d116c9d12e4ef7e816eb0e Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Wed, 30 Jan 2019 12:10:47 -0800 Subject: [PATCH] [inferbo] Only callee formals are needed Reviewed By: skcho Differential Revision: D13865391 fbshipit-source-id: bfe3b4d13 --- .../bufferoverrun/bufferOverrunAnalysis.ml | 25 ++++++++++--------- .../src/bufferoverrun/bufferOverrunChecker.ml | 25 +++++++++++-------- .../bufferoverrun/bufferOverrunSemantics.ml | 12 ++++----- infer/src/checkers/cost.ml | 3 ++- 4 files changed, 35 insertions(+), 30 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index ed39a57b5..09f728c8d 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -55,9 +55,8 @@ module TransferFunctions = struct type nonrec extras = extras - let instantiate_mem_reachable (ret_id, _) callee_pdesc callee_pname ~callee_exit_mem + let instantiate_mem_reachable (ret_id, _) callee_formals callee_pname ~callee_exit_mem ({Dom.eval_locpath} as eval_sym_trace) mem location = - let formals = Procdesc.get_pvar_formals callee_pdesc in let copy_reachable_locs_from locs mem = let copy loc acc = Option.value_map (Dom.Mem.find_opt loc callee_exit_mem) ~default:acc ~f:(fun v -> @@ -65,7 +64,7 @@ module TransferFunctions = struct let v = Dom.Val.subst v eval_sym_trace location in PowLoc.fold (fun loc acc -> Dom.Mem.add_heap loc v acc) locs acc ) in - let reachable_locs = Dom.Mem.get_reachable_locs_from formals locs callee_exit_mem in + let reachable_locs = Dom.Mem.get_reachable_locs_from callee_formals locs callee_exit_mem in PowLoc.fold copy reachable_locs mem in let instantiate_ret_alias mem = @@ -89,7 +88,7 @@ module TransferFunctions = struct let ret_var = Loc.of_var (Var.of_id ret_id) in let ret_val = Dom.Mem.find (Loc.of_pvar (Pvar.get_ret_pvar callee_pname)) callee_exit_mem in let formal_locs = - List.fold formals ~init:PowLoc.bot ~f:(fun acc (formal, _) -> + List.fold callee_formals ~init:PowLoc.bot ~f:(fun acc (formal, _) -> let v = Dom.Mem.find (Loc.of_pvar formal) callee_exit_mem in PowLoc.join acc (Dom.Val.get_all_locs v) ) in @@ -116,23 +115,23 @@ module TransferFunctions = struct Tenv.t -> Typ.IntegerWidths.t -> Ident.t * Typ.t - -> Procdesc.t + -> (Pvar.t * Typ.t) list -> Typ.Procname.t -> (Exp.t * Typ.t) list -> Dom.Mem.t -> BufferOverrunAnalysisSummary.t -> Location.t -> Dom.Mem.t = - fun tenv integer_type_widths ret callee_pdesc callee_pname params caller_mem callee_exit_mem + fun tenv integer_type_widths ret callee_formals callee_pname params caller_mem callee_exit_mem location -> let rel_subst_map = - Sem.get_subst_map tenv integer_type_widths callee_pdesc params caller_mem callee_exit_mem + Sem.get_subst_map tenv integer_type_widths callee_formals params caller_mem callee_exit_mem in let eval_sym_trace = - Sem.mk_eval_sym_trace integer_type_widths callee_pdesc params caller_mem ~strict:false + Sem.mk_eval_sym_trace integer_type_widths callee_formals params caller_mem ~strict:false in let caller_mem = - instantiate_mem_reachable ret callee_pdesc callee_pname ~callee_exit_mem eval_sym_trace + instantiate_mem_reachable ret callee_formals callee_pname ~callee_exit_mem eval_sym_trace caller_mem location |> forget_ret_relation ret callee_pname in @@ -233,11 +232,13 @@ module TransferFunctions = struct Ondemand.analyze_proc_name ~caller_pdesc:pdesc callee_pname |> Option.bind ~f:(fun callee_summary -> Payload.of_summary callee_summary - |> Option.map ~f:(fun payload -> (payload, Summary.get_proc_desc callee_summary)) + |> Option.map ~f:(fun payload -> + ( payload + , Summary.get_proc_desc callee_summary |> Procdesc.get_pvar_formals ) ) ) with - | Some (callee_exit_mem, callee_pdesc) -> - instantiate_mem tenv integer_type_widths ret callee_pdesc callee_pname params mem + | Some (callee_exit_mem, callee_formals) -> + instantiate_mem tenv integer_type_widths ret callee_formals callee_pname params mem callee_exit_mem location | None -> (* This may happen for procedures with a biabduction model too. *) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index fa6b2ac42..f605f1ed8 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -243,21 +243,24 @@ let rec check_expr_for_integer_overflow integer_type_widths exp location mem con let instantiate_cond : Tenv.t -> Typ.IntegerWidths.t - -> Procdesc.t + -> Typ.Procname.t + -> (Pvar.t * Typ.t) list -> (Exp.t * Typ.t) list -> Dom.Mem.t -> BufferOverrunAnalysisSummary.t -> BufferOverrunCheckerSummary.t -> Location.t -> PO.ConditionSet.checked_t = - fun tenv integer_type_widths callee_pdesc params caller_mem callee_exit_mem callee_cond location -> + fun tenv integer_type_widths callee_pname callee_formals params caller_mem callee_exit_mem + callee_cond location -> let rel_subst_map = - Sem.get_subst_map tenv integer_type_widths callee_pdesc params caller_mem callee_exit_mem + Sem.get_subst_map tenv integer_type_widths callee_formals params caller_mem callee_exit_mem in - let pname = Procdesc.get_proc_name callee_pdesc in let caller_rel = Dom.Mem.get_relation caller_mem in - let eval_sym_trace = Sem.mk_eval_sym_trace integer_type_widths callee_pdesc params caller_mem in - PO.ConditionSet.subst callee_cond eval_sym_trace rel_subst_map caller_rel pname location + let eval_sym_trace = + Sem.mk_eval_sym_trace integer_type_widths callee_formals params caller_mem + in + PO.ConditionSet.subst callee_cond eval_sym_trace rel_subst_map caller_rel callee_pname location let check_instr : @@ -301,11 +304,13 @@ let check_instr : let checker_payload = Payload.of_summary callee_summary in Option.map2 analysis_payload checker_payload ~f:(fun analysis_payload checker_payload -> - (analysis_payload, checker_payload, Summary.get_proc_desc callee_summary) ) ) + ( analysis_payload + , checker_payload + , Summary.get_proc_desc callee_summary |> Procdesc.get_pvar_formals ) ) ) with - | Some (callee_mem, callee_condset, callee_pdesc) -> - instantiate_cond tenv integer_type_widths callee_pdesc params mem callee_mem - callee_condset location + | Some (callee_mem, callee_condset, callee_formals) -> + instantiate_cond tenv integer_type_widths callee_pname callee_formals params mem + callee_mem callee_condset location |> PO.ConditionSet.join cond_set | None -> (* unknown call / no inferbo payload *) cond_set ) ) diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 138e05ca6..923158ed4 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -407,11 +407,10 @@ let eval_sympath ~strict params sympath mem = - non-strict mode (which is used by default): it returns the unknown location. - strict mode (which is used only in the substitution of condition of proof obligation): it returns the bottom location. *) -let mk_eval_sym_trace integer_type_widths callee_pdesc actual_exps caller_mem = +let mk_eval_sym_trace integer_type_widths callee_formals actual_exps caller_mem = let params = - let formals = Procdesc.get_pvar_formals callee_pdesc in let actuals = List.map ~f:(fun (a, _) -> eval integer_type_widths a caller_mem) actual_exps in - ParamBindings.make formals actuals + ParamBindings.make callee_formals actuals in let eval_sym s bound_end = let sympath = Symb.Symbol.path s in @@ -729,12 +728,12 @@ let rec list_fold2_def : let get_subst_map : Tenv.t -> Typ.IntegerWidths.t - -> Procdesc.t + -> (Pvar.t * Typ.t) list -> (Exp.t * 'a) list -> Mem.t -> _ Mem.t0 -> Relation.SubstMap.t = - fun tenv integer_type_widths callee_pdesc params caller_mem callee_exit_mem -> + fun tenv integer_type_widths callee_formals params caller_mem callee_exit_mem -> let add_pair (formal, typ) (actual, actual_exp) rel_l = let callee_v = Mem.find (Loc.of_pvar formal) callee_exit_mem in let new_rel_matching = @@ -743,11 +742,10 @@ let get_subst_map : in List.rev_append new_rel_matching rel_l in - let formals = Procdesc.get_pvar_formals callee_pdesc in let actuals = List.map ~f:(fun (a, _) -> (eval integer_type_widths a caller_mem, Some a)) params in let rel_pairs = - list_fold2_def ~default:(Val.Itv.top, None) ~f:add_pair formals actuals ~init:[] + list_fold2_def ~default:(Val.Itv.top, None) ~f:add_pair callee_formals actuals ~init:[] in subst_map_of_rel_pairs rel_pairs diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index 2147c2746..a01398a5c 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -41,8 +41,9 @@ let instantiate_cost integer_type_widths ~inferbo_caller_mem ~callee_pname ~para "Can't instantiate symbolic cost %a from call to %a (can't get procdesc)" BasicCost.pp callee_cost Typ.Procname.pp callee_pname | Some callee_pdesc -> + let callee_formals = Procdesc.get_pvar_formals callee_pdesc in let eval_sym = - BufferOverrunSemantics.mk_eval_sym integer_type_widths callee_pdesc params + BufferOverrunSemantics.mk_eval_sym integer_type_widths callee_formals params inferbo_caller_mem in BasicCost.subst callee_cost eval_sym