[inferbo] Uncouple condition reporting and propagating

Reviewed By: skcho

Differential Revision: D13825862

fbshipit-source-id: 63ccce7ba

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -622,7 +622,7 @@ module Report = struct
       -> Tenv.t
       -> Typ.IntegerWidths.t
       -> CFG.t
-      -> Analyzer.invariant_map
+      -> invariant_map
       -> Checks.t
       -> CFG.Node.t
       -> Checks.t =
@@ -636,14 +636,14 @@ module Report = struct
 
 
   let check_proc :
-      Procdesc.t -> Tenv.t -> Typ.IntegerWidths.t -> CFG.t -> Analyzer.invariant_map -> Checks.t =
+      Procdesc.t -> Tenv.t -> Typ.IntegerWidths.t -> CFG.t -> invariant_map -> Checks.t =
    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
 
 
-  let report_errors : Tenv.t -> Summary.t -> Checks.t -> PO.ConditionSet.t =
+  let report_errors : Tenv.t -> Summary.t -> Checks.t -> unit =
    fun tenv summary {cond_set; unused_branches; unreachable_statements} ->
     UnusedBranches.report tenv summary unused_branches ;
     UnreachableStatements.report summary unreachable_statements ;
@@ -657,12 +657,14 @@ module Report = struct
       in
       Reporting.log_error summary ~loc:location ~ltr:trace issue_type (description ~markup:true)
     in
-    PO.ConditionSet.check_all ~report cond_set
+    PO.ConditionSet.report_errors ~report cond_set
 
 
-  let forget_locs = PO.ConditionSet.forget_locs
-
-  let for_summary = PO.ConditionSet.for_summary
+  let for_summary ~forget_locs
+      Checks.({ cond_set
+              ; unused_branches= _ (* intra-procedural *)
+              ; unreachable_statements= _ (* intra-procedural *) }) =
+    PO.ConditionSet.for_summary ~forget_locs cond_set
 end
 
 let extract_pre = Analyzer.extract_pre
@@ -694,11 +696,10 @@ let compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_
   let pp_name f = F.pp_print_string f "bufferoverrun check" in
   NodePrinter.start_session ~pp_name underlying_exit_node ;
   let summary =
+    let checks = Report.check_proc proc_desc tenv integer_type_widths cfg inv_map in
+    Report.report_errors tenv summary checks ;
     let locals = get_local_decls proc_desc in
-    let cond_set =
-      Report.check_proc proc_desc tenv integer_type_widths cfg inv_map
-      |> Report.report_errors tenv summary |> Report.forget_locs locals |> Report.for_summary
-    in
+    let cond_set = Report.for_summary ~forget_locs:locals checks in
     let exit_mem =
       extract_post (CFG.Node.id exit_node) inv_map
       |> Option.value ~default:Bottom |> Dom.Mem.forget_locs locals |> Dom.Mem.unset_oenv

infer/src/bufferoverrun/bufferOverrunProofObligations.ml

@@ -794,26 +794,35 @@ module ConditionWithTrace = struct
         {report_issue_type; propagate}
 
 
-  let report ~report ((cwt, checked) as default) =
+  let report_errors ~report (cwt, checked) =
     match checked.report_issue_type with
     | NotIssue | SymbolicIssue ->
-        default
+        ()
     | Issue issue_type ->
-        report cwt.cond cwt.trace issue_type ;
-        if checked.propagate then ({cwt with reported= Some (Reported.make issue_type)}, checked)
-        else default
-
+        report cwt.cond cwt.trace issue_type
 
-  let forget_locs locs cwt = {cwt with cond= Condition.forget_locs locs cwt.cond}
 
-  let for_summary cwt = {cwt with trace= ConditionTrace.for_summary cwt.trace}
+  let for_summary ~forget_locs = function
+    | _, {propagate= false} | _, {report_issue_type= NotIssue} ->
+        None
+    | {cond; trace; reported; reachability}, {report_issue_type} ->
+        let reported =
+          match report_issue_type with
+          | NotIssue ->
+              assert false
+          | SymbolicIssue ->
+              reported
+          | Issue issue_type ->
+              Some (Reported.make issue_type)
+        in
+        let cond = Condition.forget_locs forget_locs cond in
+        let trace = ConditionTrace.for_summary trace in
+        Some {cond; trace; reported; reachability}
 end
 
 module ConditionSet = struct
   type 'cond_trace t0 = 'cond_trace ConditionWithTrace.t0 list
 
-  type t = ConditionTrace.intra_cond_trace t0
-
   type checked_t = (ConditionTrace.intra_cond_trace ConditionWithTrace.t0 * checked_condition) list
 
   type summary_t = unit t0
@@ -923,10 +932,12 @@ module ConditionSet = struct
     List.fold condset ~f:subst_add_cwt ~init:[]
 
 
-  let check_all ~report condset =
-    condset
-    |> List.map ~f:(ConditionWithTrace.report ~report)
-    |> List.filter_map ~f:(fun (cwt, {propagate}) -> Option.some_if propagate cwt)
+  let report_errors ~report condset =
+    List.iter condset ~f:(ConditionWithTrace.report_errors ~report)
+
+
+  let for_summary ~forget_locs condset =
+    List.filter_map condset ~f:(ConditionWithTrace.for_summary ~forget_locs)
 
 
   let pp_summary : F.formatter -> _ t0 -> unit =
@@ -946,14 +957,6 @@ module ConditionSet = struct
     F.fprintf fmt "Safety conditions:@;@[<hov 2>{ %a }@]"
       (IList.pp_print_list ~max:30 ~pp_sep pp_elem)
       condset
-
-
-  let forget_locs : AbsLoc.PowLoc.t -> 'a t0 -> 'a t0 =
-   fun locs x -> List.map x ~f:(ConditionWithTrace.forget_locs locs)
-
-
-  let for_summary : _ t0 -> summary_t =
-   fun condset -> List.map condset ~f:ConditionWithTrace.for_summary
 end
 
 let description ~markup cond trace =

infer/src/bufferoverrun/bufferOverrunProofObligations.mli

@@ -23,8 +23,6 @@ module ConditionTrace : sig
 end
 
 module ConditionSet : sig
-  type t
-
   type checked_t
 
   type summary_t
@@ -81,12 +79,10 @@ module ConditionSet : sig
     -> Location.t
     -> checked_t
 
-  val check_all : report:(Condition.t -> ConditionTrace.t -> IssueType.t -> unit) -> checked_t -> t
-  (** Check the conditions, call [report] on those that trigger an issue, returns those that needs to be propagated to callers. *)
-
-  val for_summary : t -> summary_t
+  val report_errors :
+    report:(Condition.t -> ConditionTrace.t -> IssueType.t -> unit) -> checked_t -> unit
 
-  val forget_locs : AbsLoc.PowLoc.t -> t -> t
+  val for_summary : forget_locs:AbsLoc.PowLoc.t -> checked_t -> summary_t
 end
 
 val description : markup:bool -> Condition.t -> ConditionTrace.t -> string