[cost] Report only after the analysis

Summary:
- Decouple analysis/reporting a little bit
- Avoids carrying the summary while computing stuff

Depends on D14028249

Reviewed By: ngorogiannis

Differential Revision: D14028673

fbshipit-source-id: 18e7298f8

infer/src/checkers/cost.ml

@@ -516,8 +516,7 @@ end
 type extras_WCET =
   { inferbo_invariant_map: BufferOverrunAnalysis.invariant_map
   ; integer_type_widths: Typ.IntegerWidths.t
-  ; get_node_nb_exec: Node.id -> BasicCost.t
+  ; get_node_nb_exec: Node.id -> BasicCost.t }
-  ; summary: Summary.t }
 
 let instantiate_cost integer_type_widths ~inferbo_caller_mem ~callee_pname ~params ~callee_cost =
   match Ondemand.get_proc_desc callee_pname with
@@ -614,7 +613,9 @@ let compute_errlog_extras cost =
   It is the dot product of basic_cost_map and get_node_nb_exec.
 *)
 module WCET = struct
-  type astate = {current_cost: BasicCost.t; report_on_threshold: bool}
+  type report = DontCheck | PleaseCheck | ReportOn of {location: Location.t; cost: BasicCost.t}
+
+  type astate = {current_cost: BasicCost.t; report_on_threshold: report}
 
   let do_report summary loc cost =
     let degree_str =
@@ -647,7 +648,7 @@ module WCET = struct
 
 
   let exec_node {current_cost; report_on_threshold} pdata instr_node =
-    let {ProcData.extras= {get_node_nb_exec; summary}} = pdata in
+    let {ProcData.extras= {get_node_nb_exec}} = pdata in
     let node_cost =
       let instr_cost_record = InstrBasicCost.get_instr_node_cost_record pdata instr_node in
       let instr_cost = CostDomain.get_operation_cost instr_cost_record in
@@ -657,10 +658,11 @@ module WCET = struct
     in
     let current_cost = BasicCost.plus current_cost node_cost in
     let report_on_threshold =
-      if report_on_threshold && should_report_cost current_cost then (
+      match report_on_threshold with
-        do_report summary (InstrCFG.Node.loc instr_node) current_cost ;
+      | PleaseCheck when should_report_cost current_cost ->
-        false )
+          ReportOn {location= InstrCFG.Node.loc instr_node; cost= current_cost}
-      else report_on_threshold
+      | _ ->
+          report_on_threshold
     in
     {current_cost; report_on_threshold}
 
@@ -676,7 +678,7 @@ module WCET = struct
     | Component {head; rest; next} ->
         let {current_cost; report_on_threshold} = astate in
         let {current_cost} =
-          exec_partition {current_cost; report_on_threshold= false} pdata rest
+          exec_partition {current_cost; report_on_threshold= DontCheck} pdata rest
         in
         (* Execute head after the loop body to always report at loop head *)
         let astate = exec_node {current_cost; report_on_threshold} pdata head in
@@ -685,10 +687,12 @@ module WCET = struct
 
   let compute pdata =
     let cfg = InstrCFG.from_pdesc pdata.ProcData.pdesc in
-    let initial = {current_cost= BasicCost.zero; report_on_threshold= Config.use_cost_threshold} in
+    let report_on_threshold = if Config.use_cost_threshold then PleaseCheck else DontCheck in
-    let {current_cost} = exec_partition initial pdata (InstrCFG.wto cfg) in
+    let initial = {current_cost= BasicCost.zero; report_on_threshold} in
-    CostDomain.mk_cost_record ~operation_cost:current_cost ~allocation_cost:BasicCost.zero
+    let {current_cost; report_on_threshold} = exec_partition initial pdata (InstrCFG.wto cfg) in
-      ~io_cost:BasicCost.zero
+    ( CostDomain.mk_cost_record ~operation_cost:current_cost ~allocation_cost:BasicCost.zero
+        ~io_cost:BasicCost.zero
+    , report_on_threshold )
 end
 
 let check_and_report_top_and_bottom cost_record proc_desc summary =
@@ -751,10 +755,9 @@ let checker {Callbacks.tenv; proc_desc; integer_type_widths; summary} : Summary.
     if Config.write_html then NodePrinter.finish_session start_node ;
     ConstraintSolver.get_node_nb_exec equalities
   in
-  let exit_cost_record =
+  let exit_cost_record, report =
     let pdata =
-      ProcData.make proc_desc tenv
+      ProcData.make proc_desc tenv {inferbo_invariant_map; integer_type_widths; get_node_nb_exec}
-        {inferbo_invariant_map; integer_type_widths; get_node_nb_exec; summary}
     in
     WCET.compute pdata
   in
@@ -763,5 +766,6 @@ let checker {Callbacks.tenv; proc_desc; integer_type_widths; summary} : Summary.
     (Procdesc.get_proc_name proc_desc)
     (Container.length ~fold:NodeCFG.fold_nodes node_cfg)
     CostDomain.VariantCostMap.pp exit_cost_record ;
+  (match report with ReportOn {location; cost} -> WCET.do_report summary location cost | _ -> ()) ;
   check_and_report_top_and_bottom exit_cost_record proc_desc summary ;
   Payload.update_summary {post= exit_cost_record} summary