[inferbo] Parametric in Ondemand

Reviewed By: skcho

Differential Revision: D13852045

fbshipit-source-id: eacd6485c

infer/src/bufferoverrun/bufferOverrunAnalysis.ml

@@ -26,7 +26,10 @@ module Payload = SummaryPayload.Make (struct
   let of_payloads (payloads : Payloads.t) = payloads.buffer_overrun_analysis
 end)
 
-type extras = {oenv: Dom.OndemandEnv.t}
+type extras =
+  { get_proc_summary:
+      Typ.Procname.t -> (BufferOverrunAnalysisSummary.t * (Pvar.t * Typ.t) list) option
+  ; oenv: Dom.OndemandEnv.t }
 
 module CFG = ProcCfg.NormalOneInstrPerNode
 
@@ -138,7 +141,7 @@ module TransferFunctions = struct
 
 
   let exec_instr : Dom.Mem.t -> extras ProcData.t -> CFG.Node.t -> Sil.instr -> Dom.Mem.t =
-   fun mem {pdesc; tenv; extras= {oenv= {integer_type_widths}}} node instr ->
+   fun mem {pdesc; tenv; extras= {get_proc_summary; oenv= {integer_type_widths}}} node instr ->
     match instr with
     | Load (id, _, _, _) when Ident.is_none id ->
         mem
@@ -146,11 +149,8 @@ module TransferFunctions = struct
       -> (
       match Pvar.get_initializer_pname pvar with
       | Some callee_pname -> (
-        match
-          Ondemand.analyze_proc_name ~caller_pdesc:pdesc callee_pname
-          |> Option.bind ~f:Payload.of_summary
-        with
-        | Some callee_mem ->
+        match get_proc_summary callee_pname with
+        | Some (callee_mem, _) ->
             let v = Dom.Mem.find (Loc.of_pvar pvar) callee_mem in
             Dom.Mem.add_stack (Loc.of_id id) v mem
         | None ->
@@ -227,15 +227,7 @@ module TransferFunctions = struct
             in
             exec model_env ~ret mem
         | None -> (
-          match
-            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 |> Procdesc.get_pvar_formals ) )
-               )
-          with
+          match get_proc_summary callee_pname with
           | Some (callee_exit_mem, callee_formals) ->
               instantiate_mem tenv integer_type_widths ret callee_formals callee_pname params mem
                 callee_exit_mem location
@@ -296,7 +288,14 @@ let cached_compute_invariant_map =
     let cfg = CFG.from_pdesc pdesc in
     let pdata =
       let oenv = Dom.OndemandEnv.mk pdesc tenv integer_type_widths in
-      ProcData.make pdesc tenv {oenv}
+      let get_proc_summary callee_pname =
+        Ondemand.analyze_proc_name ~caller_pdesc:pdesc callee_pname
+        |> Option.bind ~f:(fun summary ->
+               Payload.of_summary summary
+               |> Option.map ~f:(fun payload ->
+                      (payload, Summary.get_proc_desc summary |> Procdesc.get_pvar_formals) ) )
+      in
+      ProcData.make pdesc tenv {get_proc_summary; oenv}
     in
     let initial = Init.initial_state pdata (CFG.start_node cfg) in
     Analyzer.exec_pdesc ~do_narrowing:true ~initial pdata

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -265,8 +265,14 @@ let instantiate_cond :
     latest_prune
 
 
+type get_proc_summary =
+     Typ.Procname.t
+  -> (BufferOverrunAnalysisSummary.t * BufferOverrunCheckerSummary.t * (Pvar.t * Typ.t) list)
+     option
+
 let check_instr :
-       Procdesc.t
+       get_proc_summary
+    -> Procdesc.t
     -> Tenv.t
     -> Typ.IntegerWidths.t
     -> CFG.Node.t
@@ -274,7 +280,7 @@ let check_instr :
     -> Dom.Mem.t
     -> PO.ConditionSet.checked_t
     -> PO.ConditionSet.checked_t =
- fun pdesc tenv integer_type_widths node instr mem cond_set ->
+ fun get_proc_summary pdesc tenv integer_type_widths node instr mem cond_set ->
   match instr with
   | Sil.Load (_, exp, _, location) ->
       cond_set
@@ -299,17 +305,7 @@ let check_instr :
           in
           check model_env mem cond_set
       | None -> (
-        match
-          Ondemand.analyze_proc_name ~caller_pdesc:pdesc callee_pname
-          |> Option.bind ~f:(fun callee_summary ->
-                 let analysis_payload = BufferOverrunAnalysis.Payload.of_summary callee_summary in
-                 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 |> Procdesc.get_pvar_formals ) ) )
-        with
+        match get_proc_summary callee_pname with
         | Some (callee_mem, callee_condset, callee_formals) ->
             instantiate_cond tenv integer_type_widths callee_pname callee_formals params mem
               callee_mem callee_condset location
@@ -333,7 +329,8 @@ let print_debug_info : Sil.instr -> Dom.Mem.t -> PO.ConditionSet.checked_t -> un
 
 
 let check_instrs :
-       Procdesc.t
+       get_proc_summary
+    -> Procdesc.t
     -> Tenv.t
     -> Typ.IntegerWidths.t
     -> CFG.t
@@ -342,7 +339,7 @@ let check_instrs :
     -> Dom.Mem.t AbstractInterpreter.State.t
     -> Checks.t
     -> Checks.t =
- fun pdesc tenv integer_type_widths cfg node instrs state checks ->
+ fun get_proc_summary pdesc tenv integer_type_widths cfg node instrs state checks ->
   match state with
   | _ when Instrs.is_empty instrs ->
       checks
@@ -359,13 +356,16 @@ let check_instrs :
         | NonBottom _ ->
             checks
       in
-      let cond_set = check_instr pdesc tenv integer_type_widths node instr pre checks.cond_set in
+      let cond_set =
+        check_instr get_proc_summary pdesc tenv integer_type_widths node instr pre checks.cond_set
+      in
       print_debug_info instr pre cond_set ;
       {checks with cond_set}
 
 
 let check_node :
-       Procdesc.t
+       get_proc_summary
+    -> Procdesc.t
     -> Tenv.t
     -> Typ.IntegerWidths.t
     -> CFG.t
@@ -373,11 +373,11 @@ let check_node :
     -> Checks.t
     -> CFG.Node.t
     -> Checks.t =
- fun pdesc tenv integer_type_widths cfg inv_map checks node ->
+ fun get_proc_summary 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 pdesc tenv integer_type_widths cfg node instrs state checks
+      check_instrs get_proc_summary pdesc tenv integer_type_widths cfg node instrs state checks
   | _ ->
       checks
 
@@ -385,14 +385,17 @@ let check_node :
 type checks = Checks.t
 
 let compute_checks :
-       Procdesc.t
+       get_proc_summary
+    -> Procdesc.t
     -> Tenv.t
     -> Typ.IntegerWidths.t
     -> CFG.t
     -> BufferOverrunAnalysis.invariant_map
     -> checks =
- fun pdesc tenv integer_type_widths cfg inv_map ->
-  CFG.fold_nodes cfg ~f:(check_node pdesc tenv integer_type_widths cfg inv_map) ~init:Checks.empty
+ fun get_proc_summary pdesc tenv integer_type_widths cfg inv_map ->
+  CFG.fold_nodes cfg
+    ~f:(check_node get_proc_summary pdesc tenv integer_type_widths cfg inv_map)
+    ~init:Checks.empty
 
 
 type checks_summary = PO.ConditionSet.summary_t
@@ -432,7 +435,20 @@ let checker : Callbacks.proc_callback_args -> Summary.t =
   NodePrinter.start_session ~pp_name underlying_exit_node ;
   let summary =
     let cfg = CFG.from_pdesc proc_desc in
-    let checks = compute_checks proc_desc tenv integer_type_widths cfg inv_map in
+    let checks =
+      let get_proc_summary callee_pname =
+        Ondemand.analyze_proc_name ~caller_pdesc:proc_desc callee_pname
+        |> Option.bind ~f:(fun summary ->
+               let analysis_payload = BufferOverrunAnalysis.Payload.of_summary summary in
+               let checker_payload = Payload.of_summary summary in
+               Option.map2 analysis_payload checker_payload
+                 ~f:(fun analysis_payload checker_payload ->
+                   ( analysis_payload
+                   , checker_payload
+                   , Summary.get_proc_desc summary |> Procdesc.get_pvar_formals ) ) )
+      in
+      compute_checks get_proc_summary proc_desc tenv integer_type_widths cfg inv_map
+    in
     report_errors tenv summary checks ;
     let locals = BufferOverrunAnalysis.get_local_decls proc_desc in
     let cond_set = checks_summary locals checks in