diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 1d985abe4..746524648 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -13,35 +13,6 @@ open PulseBasicInterface open PulseDomainInterface open PulseOperations.Import -let exec_list_of_list_result = function - | Ok posts -> - posts - | Error Unsat -> - [] - | Error (Sat post) -> - [post] - - -let report_on_error {InterproceduralAnalysis.proc_desc; tenv; err_log} result = - PulseReport.report_error proc_desc tenv err_log result - >>| List.map ~f:(fun post -> ContinueProgram post) - |> exec_list_of_list_result - - -let post_of_report_result = function - | Ok post -> - Some post - | Error Unsat -> - None - | Error (Sat post) -> - Some post - - -let report_on_error_list {InterproceduralAnalysis.proc_desc; tenv; err_log} results = - List.filter_map results ~f:(fun exec_result -> - PulseReport.report_error proc_desc tenv err_log exec_result |> post_of_report_result ) - - let report_topl_errors proc_desc err_log summary = let f = function | ContinueProgram astate -> @@ -272,7 +243,7 @@ module PulseTransferFunctions = struct | ContinueProgram astate -> let astate = dispatch_call analysis_data ret call_exp actuals location call_flags astate - |> report_on_error_list analysis_data + |> PulseReport.report_results analysis_data in List.rev_append astate astates ) ~init:[] astate_list @@ -322,7 +293,7 @@ module PulseTransferFunctions = struct List.map astate_rhs_addr_hists ~f:(fun (astate, rhs_addr_hist) -> PulseOperations.write_id lhs_id rhs_addr_hist astate ) in - report_on_error analysis_data result + PulseReport.report_list_result analysis_data result | Store {e1= lhs_exp; e2= rhs_exp; loc} -> (* [*lhs_exp := rhs_exp] *) let event = ValueHistory.Assignment loc in @@ -375,7 +346,7 @@ module PulseTransferFunctions = struct | _ -> Ok astates in - report_on_error analysis_data result + PulseReport.report_list_result analysis_data result | Prune (condition, loc, _is_then_branch, _if_kind) -> (let<*> astate = PulseOperations.prune loc ~condition astate in if PulseArithmetic.is_unsat_cheap astate then @@ -384,10 +355,10 @@ module PulseTransferFunctions = struct else (* [condition] is true or unknown value: go into the branch *) [Ok (ContinueProgram astate)]) - |> report_on_error_list analysis_data + |> PulseReport.report_results analysis_data | Call (ret, call_exp, actuals, loc, call_flags) -> dispatch_call analysis_data ret call_exp actuals loc call_flags astate - |> report_on_error_list analysis_data + |> PulseReport.report_results analysis_data | Metadata (ExitScope (vars, location)) -> let remove_vars vars astates = List.fold @@ -402,7 +373,7 @@ module PulseTransferFunctions = struct Ok [astate] | Error _ as error -> error ) - |> report_on_error analysis_data + |> PulseReport.report_list_result analysis_data in List.rev_append astate astates ) ~init:[] astates diff --git a/infer/src/pulse/PulseReport.ml b/infer/src/pulse/PulseReport.ml index 8c94a189b..4d1bd8f1b 100644 --- a/infer/src/pulse/PulseReport.ml +++ b/infer/src/pulse/PulseReport.ml @@ -55,3 +55,33 @@ let report_error proc_desc tenv err_log access_result = if Config.pulse_report_latent_issues && not is_suppressed then report_latent_issue proc_desc err_log latent_issue ; ExecutionDomain.LatentAbortProgram {astate= astate_summary; latent_issue} ) + + +let exec_list_of_list_result = function + | Ok posts -> + posts + | Error Unsat -> + [] + | Error (Sat post) -> + [post] + + +let report_list_result {InterproceduralAnalysis.proc_desc; tenv; err_log} result = + let open Result.Monad_infix in + report_error proc_desc tenv err_log result + >>| List.map ~f:(fun post -> ExecutionDomain.ContinueProgram post) + |> exec_list_of_list_result + + +let post_of_report_result = function + | Ok post -> + Some post + | Error Unsat -> + None + | Error (Sat post) -> + Some post + + +let report_results {InterproceduralAnalysis.proc_desc; tenv; err_log} results = + List.filter_map results ~f:(fun exec_result -> + report_error proc_desc tenv err_log exec_result |> post_of_report_result ) diff --git a/infer/src/pulse/PulseReport.mli b/infer/src/pulse/PulseReport.mli index bc8dc94cc..450d39c89 100644 --- a/infer/src/pulse/PulseReport.mli +++ b/infer/src/pulse/PulseReport.mli @@ -11,9 +11,12 @@ open PulseDomainInterface type 'a access_result = ('a, Diagnostic.t * AbductiveDomain.t) result -val report_error : - Procdesc.t - -> Tenv.t - -> Errlog.t - -> 'ok access_result - -> ('ok, _ ExecutionDomain.base_t SatUnsat.t) result +val report_list_result : + PulseSummary.t InterproceduralAnalysis.t + -> AbductiveDomain.t list access_result + -> ExecutionDomain.t list + +val report_results : + PulseSummary.t InterproceduralAnalysis.t + -> ExecutionDomain.t access_result list + -> ExecutionDomain.t list