From 5e7fd7c3265bf17b9469fc26811a3c32cac8bfc9 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Mon, 28 Jan 2019 06:15:10 -0800 Subject: [PATCH] [inferbo] Uncouple condition reporting and propagating Reviewed By: skcho Differential Revision: D13825862 fbshipit-source-id: 63ccce7ba --- .../src/bufferoverrun/bufferOverrunChecker.ml | 23 ++++----- .../bufferOverrunProofObligations.ml | 47 ++++++++++--------- .../bufferOverrunProofObligations.mli | 10 ++-- 3 files changed, 40 insertions(+), 40 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index a493c3bb7..a1cbc2149 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/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 diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index 1803d366e..d6e72cb88 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/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:@;@[{ %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 = diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli b/infer/src/bufferoverrun/bufferOverrunProofObligations.mli index 6b8a7b7b0..347a01b2a 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli +++ b/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