[inferbo] Only callee formals are needed

Reviewed By: skcho

Differential Revision: D13865391

fbshipit-source-id: bfe3b4d13

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. *)

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 ) )

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

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