[inferbo] Refactoring: move get_formals type definition

Summary:
This diffs does: (1) move `get_formals` to `BufferOverrunUtils` (2) use separate `get_formals` in
`BufferOverrunChecker`, in order to simplify the following diff.

Reviewed By: jvillard

Differential Revision: D19432280

fbshipit-source-id: bfb4df118

infer/src/bufferoverrun/bufferOverrunAnalysis.ml

@@ -25,11 +25,9 @@ module Payload = SummaryPayload.Make (struct
   let field = Payloads.Fields.buffer_overrun_analysis
 end)
 
-type get_formals = Procname.t -> (Pvar.t * Typ.t) list option
-
 type extras =
   { get_summary: BufferOverrunAnalysisSummary.get_summary
-  ; get_formals: get_formals
+  ; get_formals: BoUtils.get_formals
   ; oenv: OndemandEnv.t }
 
 module CFG = ProcCfg.NormalOneInstrPerNode
@@ -449,7 +447,7 @@ let compute_invariant_map :
     -> Tenv.t
     -> Typ.IntegerWidths.t
     -> BufferOverrunAnalysisSummary.get_summary
-    -> get_formals
+    -> BoUtils.get_formals
     -> invariant_map =
  fun summary tenv integer_type_widths get_summary get_formals ->
   let pdesc = Summary.get_proc_desc summary in

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -250,10 +250,11 @@ let instantiate_cond :
 
 type checks_summary = BufferOverrunCheckerSummary.t
 
-type get_checks_summary = Procname.t -> ((Pvar.t * Typ.t) list * checks_summary) option
+type get_checks_summary = Procname.t -> checks_summary option
 
 let check_instr :
        get_checks_summary
+    -> BoUtils.get_formals
     -> Procdesc.t
     -> Tenv.t
     -> Typ.IntegerWidths.t
@@ -262,7 +263,7 @@ let check_instr :
     -> Dom.Mem.t
     -> PO.ConditionSet.checked_t
     -> PO.ConditionSet.checked_t =
- fun get_checks_summary pdesc tenv integer_type_widths node instr mem cond_set ->
+ fun get_checks_summary get_formals pdesc tenv integer_type_widths node instr mem cond_set ->
   match instr with
   | Sil.Load {e= exp; loc= location} ->
       cond_set
@@ -291,12 +292,12 @@ let check_instr :
           in
           check model_env mem cond_set
       | None -> (
-        match get_checks_summary callee_pname with
+        match (get_checks_summary callee_pname, get_formals callee_pname) with
-        | Some (callee_formals, callee_condset) ->
+        | Some callee_condset, Some callee_formals ->
             instantiate_cond integer_type_widths callee_pname callee_formals params mem
               callee_condset location
             |> PO.ConditionSet.join cond_set
-        | None ->
+        | _, _ ->
             (* unknown call / no inferbo payload *) cond_set ) )
   | Sil.Prune (exp, location, _, _) ->
       check_expr_for_integer_overflow integer_type_widths exp location mem cond_set
@@ -316,6 +317,7 @@ let print_debug_info : Sil.instr -> Dom.Mem.t -> PO.ConditionSet.checked_t -> un
 
 let check_instrs :
        get_checks_summary
+    -> BoUtils.get_formals
     -> Procdesc.t
     -> Tenv.t
     -> Typ.IntegerWidths.t
@@ -325,7 +327,7 @@ let check_instrs :
     -> Dom.Mem.t AbstractInterpreter.State.t
     -> Checks.t
     -> Checks.t =
- fun get_checks_summary pdesc tenv integer_type_widths cfg node instrs state checks ->
+ fun get_checks_summary get_formals pdesc tenv integer_type_widths cfg node instrs state checks ->
   match state with
   | _ when Instrs.is_empty instrs ->
       checks
@@ -342,7 +344,8 @@ let check_instrs :
             checks
       in
       let cond_set =
-        check_instr get_checks_summary pdesc tenv integer_type_widths node instr pre checks.cond_set
+        check_instr get_checks_summary get_formals pdesc tenv integer_type_widths node instr pre
+          checks.cond_set
       in
       print_debug_info instr pre cond_set ;
       {checks with cond_set}
@@ -350,6 +353,7 @@ let check_instrs :
 
 let check_node :
        get_checks_summary
+    -> BoUtils.get_formals
     -> Procdesc.t
     -> Tenv.t
     -> Typ.IntegerWidths.t
@@ -358,11 +362,12 @@ let check_node :
     -> Checks.t
     -> CFG.Node.t
     -> Checks.t =
- fun get_checks_summary pdesc tenv integer_type_widths cfg inv_map checks node ->
+ fun get_checks_summary get_formals pdesc tenv integer_type_widths cfg inv_map checks node ->
   match BufferOverrunAnalysis.extract_state (CFG.Node.id node) inv_map with
   | Some state ->
       let instrs = CFG.instrs node in
-      check_instrs get_checks_summary pdesc tenv integer_type_widths cfg node instrs state checks
+      check_instrs get_checks_summary get_formals pdesc tenv integer_type_widths cfg node instrs
+        state checks
   | _ ->
       checks
 
@@ -371,15 +376,16 @@ type checks = Checks.t
 
 let compute_checks :
        get_checks_summary
+    -> BoUtils.get_formals
     -> Procdesc.t
     -> Tenv.t
     -> Typ.IntegerWidths.t
     -> CFG.t
     -> BufferOverrunAnalysis.invariant_map
     -> checks =
- fun get_checks_summary pdesc tenv integer_type_widths cfg inv_map ->
+ fun get_checks_summary get_formals pdesc tenv integer_type_widths cfg inv_map ->
   CFG.fold_nodes cfg
-    ~f:(check_node get_checks_summary pdesc tenv integer_type_widths cfg inv_map)
+    ~f:(check_node get_checks_summary get_formals pdesc tenv integer_type_widths cfg inv_map)
     ~init:Checks.empty
 
 
@@ -422,12 +428,11 @@ let checker : Callbacks.proc_callback_args -> Summary.t =
   NodePrinter.with_session ~pp_name underlying_exit_node ~f:(fun () ->
       let cfg = CFG.from_pdesc proc_desc in
       let checks =
-        let get_checks_summary callee_pname =
+        let get_checks_summary callee_pname = Payload.read ~caller_summary:summary ~callee_pname in
-          Payload.read_full ~caller_summary:summary ~callee_pname
+        let get_formals callee_pname =
-          |> Option.map ~f:(fun (callee_pdesc, callee_summary) ->
+          Ondemand.get_proc_desc callee_pname |> Option.map ~f:Procdesc.get_pvar_formals
-                 (Procdesc.get_pvar_formals callee_pdesc, callee_summary) )
         in
-        compute_checks get_checks_summary proc_desc tenv integer_type_widths cfg inv_map
+        compute_checks get_checks_summary get_formals proc_desc tenv integer_type_widths cfg inv_map
       in
       report_errors tenv checks summary ;
       let cond_set = get_checks_summary checks in

infer/src/bufferoverrun/bufferOverrunUtils.ml

@@ -328,3 +328,5 @@ module Check = struct
     | _, _ ->
         cond_set
 end
+
+type get_formals = Procname.t -> (Pvar.t * Typ.t) list option

infer/src/bufferoverrun/bufferOverrunUtils.mli

@@ -92,3 +92,5 @@ module Check : sig
     -> PO.ConditionSet.checked_t
     -> PO.ConditionSet.checked_t
 end
+
+type get_formals = Procname.t -> (Pvar.t * Typ.t) list option