From 0b7e2fb7c7142417a68352db8b17e24ae89e1483 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Fri, 2 Oct 2020 08:14:59 -0700 Subject: [PATCH] [pulse] more type-safety around summary and latent issues creation Summary: This makes sure we call `AbductiveDomain.summary_of_post` exactly once per post-condition. Notice in particular in the diff: - in Pulse.ml we remove a now-certified-useless "is_unsat_expensive" call - in PulseOperations.ml we add a previously-missing call to `summary_of_post` (it's needed to remove local variables from the symbolic state + normalize) The price to pay is ugly type annotations and down-casting peppered in a few places, in reasonable number. Reviewed By: da319 Differential Revision: D24078564 fbshipit-source-id: 3102cacf0 --- infer/src/checkers/impurity.ml | 12 +++-- infer/src/pulse/Pulse.ml | 48 ++++++++++---------- infer/src/pulse/PulseAbductiveDomain.ml | 4 +- infer/src/pulse/PulseAbductiveDomain.mli | 7 ++- infer/src/pulse/PulseExecutionDomain.ml | 57 ++++++++++++++---------- infer/src/pulse/PulseExecutionDomain.mli | 18 +++++--- infer/src/pulse/PulseLatentIssue.ml | 10 ++++- infer/src/pulse/PulseLatentIssue.mli | 5 ++- infer/src/pulse/PulseModels.ml | 4 +- infer/src/pulse/PulseOperations.ml | 36 +++++++++------ infer/src/pulse/PulseOperations.mli | 3 +- infer/src/pulse/PulseSummary.ml | 8 ++-- infer/src/pulse/PulseSummary.mli | 2 +- infer/src/topl/Topl.ml | 4 +- 14 files changed, 129 insertions(+), 89 deletions(-) diff --git a/infer/src/checkers/impurity.ml b/infer/src/checkers/impurity.ml index ffc3acbf4..a5e16ff3b 100644 --- a/infer/src/checkers/impurity.ml +++ b/infer/src/checkers/impurity.ml @@ -142,8 +142,10 @@ let extract_impurity tenv pdesc (exec_state : ExecutionDomain.t) : ImpurityDomai match exec_state with | ExitProgram astate -> (astate, true) - | AbortProgram astate | ContinueProgram astate | LatentAbortProgram {astate} -> + | ContinueProgram astate -> (astate, false) + | AbortProgram astate | LatentAbortProgram {astate} -> + ((astate :> AbductiveDomain.t), false) in let pre_heap = (AbductiveDomain.get_pre astate).BaseDomain.heap in let post = AbductiveDomain.get_post astate in @@ -162,7 +164,8 @@ let extract_impurity tenv pdesc (exec_state : ExecutionDomain.t) : ImpurityDomai {modified_globals; modified_params; skipped_calls; exited} -let checker {IntraproceduralAnalysis.proc_desc; tenv; err_log} pulse_summary_opt = +let checker {IntraproceduralAnalysis.proc_desc; tenv; err_log} + (pulse_summary_opt : PulseSummary.t option) = let proc_name = Procdesc.get_proc_name proc_desc in let pname_loc = Procdesc.get_loc proc_desc in match pulse_summary_opt with @@ -182,8 +185,9 @@ let checker {IntraproceduralAnalysis.proc_desc; tenv; err_log} pulse_summary_opt IssueType.impure_function impure_fun_desc | Some pre_posts -> let (ImpurityDomain.{modified_globals; modified_params; skipped_calls} as impurity_astate) = - List.fold pre_posts ~init:ImpurityDomain.pure ~f:(fun acc exec_state -> - let modified = extract_impurity tenv proc_desc exec_state in + List.fold pre_posts ~init:ImpurityDomain.pure + ~f:(fun acc (exec_state : ExecutionDomain.summary) -> + let modified = extract_impurity tenv proc_desc (exec_state :> ExecutionDomain.t) in ImpurityDomain.join acc modified ) in if PurityChecker.should_report proc_name && not (ImpurityDomain.is_pure impurity_astate) then diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index be78f3962..7c3200d17 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -23,29 +23,26 @@ let check_error_transform {InterproceduralAnalysis.proc_desc; err_log} ~f = func | Ok astate -> f astate | Error (diagnostic, astate) -> ( - let astate, is_unsat = PulseArithmetic.is_unsat_expensive astate in - if is_unsat then [] + let astate_summary = AbductiveDomain.summary_of_post proc_desc astate in + if PulseArithmetic.is_unsat_cheap (astate_summary :> AbductiveDomain.t) then [] else - let astate = AbductiveDomain.of_post proc_desc astate in - if PulseArithmetic.is_unsat_cheap astate then [] - else - match LatentIssue.should_report_diagnostic astate diagnostic with - | `ReportNow -> - report proc_desc err_log diagnostic ; - [ExecutionDomain.AbortProgram astate] - | `DelayReport latent_issue -> - ( if Config.pulse_report_latent_issues then - (* HACK: report latent issues with a prominent message to distinguish them from - non-latent. Useful for infer's own tests. *) - let diagnostic = LatentIssue.to_diagnostic latent_issue in - let extra_trace = - let depth = 0 in - let tags = [] in - let location = Diagnostic.get_location diagnostic in - [Errlog.make_trace_element depth location "*** LATENT ***" tags] - in - report ~extra_trace proc_desc err_log diagnostic ) ; - [ExecutionDomain.LatentAbortProgram {astate; latent_issue}] ) + match LatentIssue.should_report_diagnostic astate_summary diagnostic with + | `ReportNow -> + report proc_desc err_log diagnostic ; + [ExecutionDomain.AbortProgram astate_summary] + | `DelayReport latent_issue -> + ( if Config.pulse_report_latent_issues then + (* HACK: report latent issues with a prominent message to distinguish them from + non-latent. Useful for infer's own tests. *) + let diagnostic = LatentIssue.to_diagnostic latent_issue in + let extra_trace = + let depth = 0 in + let tags = [] in + let location = Diagnostic.get_location diagnostic in + [Errlog.make_trace_element depth location "*** LATENT ***" tags] + in + report ~extra_trace proc_desc err_log diagnostic ) ; + [ExecutionDomain.LatentAbortProgram {astate= astate_summary; latent_issue}] ) let check_error_continue analysis_data result = @@ -72,13 +69,14 @@ module PulseTransferFunctions = struct AnalysisCallbacks.proc_resolve_attributes pname |> Option.map ~f:ProcAttributes.get_pvar_formals - let interprocedural_call {InterproceduralAnalysis.analyze_dependency} ret call_exp actuals - call_loc astate = + let interprocedural_call {InterproceduralAnalysis.analyze_dependency; proc_desc} ret call_exp + actuals call_loc astate = match proc_name_of_call call_exp with | Some callee_pname when not Config.pulse_intraprocedural_only -> let formals_opt = get_pvar_formals callee_pname in let callee_data = analyze_dependency callee_pname in - PulseOperations.call ~callee_data call_loc callee_pname ~ret ~actuals ~formals_opt astate + PulseOperations.call ~caller_proc_desc:proc_desc ~callee_data call_loc callee_pname ~ret + ~actuals ~formals_opt astate | _ -> L.d_printfln "Skipping indirect call %a@\n" Exp.pp call_exp ; PulseOperations.unknown_call call_loc (SkippedUnknownCall call_exp) ~ret ~actuals diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index d78456db0..433cda285 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -432,7 +432,9 @@ let invalidate_locals pdesc astate : t = else {astate with post= PostDomain.update astate.post ~attrs:attrs'} -let of_post pdesc astate = +type summary = t + +let summary_of_post pdesc astate = let astate = filter_for_summary astate in let astate, live_addresses, _ = discard_unreachable astate in let astate = diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index eba41e6b1..e5fc32ddc 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -158,7 +158,12 @@ val add_skipped_calls : SkippedCalls.t -> t -> t val set_path_condition : PathCondition.t -> t -> t -val of_post : Procdesc.t -> t -> t +(** private type to make sure {!summary_of_post} is always called when creating summaries *) +type summary = private t + +val summary_of_post : Procdesc.t -> t -> summary +(** trim the state down to just the procedure's interface (formals and globals), and simplify and + normalize the state *) val set_post_edges : AbstractValue.t -> BaseMemory.Edges.t -> t -> t (** directly set the edges for the given address, bypassing abduction altogether *) diff --git a/infer/src/pulse/PulseExecutionDomain.ml b/infer/src/pulse/PulseExecutionDomain.ml index b09e6eb09..9d0a1e9ff 100644 --- a/infer/src/pulse/PulseExecutionDomain.ml +++ b/infer/src/pulse/PulseExecutionDomain.ml @@ -12,11 +12,17 @@ open PulseBasicInterface module AbductiveDomain = PulseAbductiveDomain module LatentIssue = PulseLatentIssue -type t = - | AbortProgram of AbductiveDomain.t - | ContinueProgram of AbductiveDomain.t - | ExitProgram of AbductiveDomain.t - | LatentAbortProgram of {astate: AbductiveDomain.t; latent_issue: LatentIssue.t} +(* The type variable is needed to distinguish summaries from plain states. + + Some of the variants have summary-typed states instead of plain states, to ensure we have + normalized them and don't need to normalize them again. *) +type 'abductive_domain_t base_t = + | ContinueProgram of 'abductive_domain_t + | ExitProgram of 'abductive_domain_t + | AbortProgram of AbductiveDomain.summary + | LatentAbortProgram of {astate: AbductiveDomain.summary; latent_issue: LatentIssue.t} + +type t = AbductiveDomain.t base_t let continue astate = ContinueProgram astate @@ -24,13 +30,14 @@ let mk_initial pdesc = ContinueProgram (AbductiveDomain.mk_initial pdesc) let leq ~lhs ~rhs = match (lhs, rhs) with - | AbortProgram astate1, AbortProgram astate2 - | ContinueProgram astate1, ContinueProgram astate2 - | ExitProgram astate1, ExitProgram astate2 -> - AbductiveDomain.leq ~lhs:astate1 ~rhs:astate2 + | AbortProgram astate1, AbortProgram astate2 -> + AbductiveDomain.leq ~lhs:(astate1 :> AbductiveDomain.t) ~rhs:(astate2 :> AbductiveDomain.t) + | ContinueProgram astate1, ContinueProgram astate2 | ExitProgram astate1, ExitProgram astate2 -> + AbductiveDomain.leq ~lhs:(astate1 :> AbductiveDomain.t) ~rhs:(astate2 :> AbductiveDomain.t) | ( LatentAbortProgram {astate= astate1; latent_issue= issue1} , LatentAbortProgram {astate= astate2; latent_issue= issue2} ) -> - LatentIssue.equal issue1 issue2 && AbductiveDomain.leq ~lhs:astate1 ~rhs:astate2 + LatentIssue.equal issue1 issue2 + && AbductiveDomain.leq ~lhs:(astate1 :> AbductiveDomain.t) ~rhs:(astate2 :> AbductiveDomain.t) | _ -> false @@ -39,36 +46,40 @@ let pp fmt = function | ContinueProgram astate -> AbductiveDomain.pp fmt astate | ExitProgram astate -> - F.fprintf fmt "{ExitProgram %a}" AbductiveDomain.pp astate + F.fprintf fmt "{ExitProgram %a}" AbductiveDomain.pp (astate :> AbductiveDomain.t) | AbortProgram astate -> - F.fprintf fmt "{AbortProgram %a}" AbductiveDomain.pp astate + F.fprintf fmt "{AbortProgram %a}" AbductiveDomain.pp (astate :> AbductiveDomain.t) | LatentAbortProgram {astate; latent_issue} -> let diagnostic = LatentIssue.to_diagnostic latent_issue in let message = Diagnostic.get_message diagnostic in let location = Diagnostic.get_location diagnostic in F.fprintf fmt "{LatentAbortProgram(%a: %s) %a}" Location.pp location message - AbductiveDomain.pp astate + AbductiveDomain.pp + (astate :> AbductiveDomain.t) let map ~f exec_state = match exec_state with - | AbortProgram astate -> - AbortProgram (f astate) | ContinueProgram astate -> ContinueProgram (f astate) | ExitProgram astate -> ExitProgram (f astate) + | AbortProgram astate -> + AbortProgram astate | LatentAbortProgram {astate; latent_issue} -> - LatentAbortProgram {astate= f astate; latent_issue} + LatentAbortProgram {astate; latent_issue} + +type summary = AbductiveDomain.summary base_t -let of_posts pdesc posts = +let summary_of_posts pdesc posts = List.filter_mapi posts ~f:(fun i exec_state -> - let ( AbortProgram astate - | ContinueProgram astate - | ExitProgram astate - | LatentAbortProgram {astate} ) = - exec_state + let astate = + match exec_state with + | AbortProgram astate | LatentAbortProgram {astate} -> + (astate :> AbductiveDomain.t) + | ContinueProgram astate | ExitProgram astate -> + astate in L.d_printfln "Creating spec out of state #%d:@\n%a" i pp exec_state ; let astate, is_unsat = PulseArithmetic.is_unsat_expensive astate in @@ -77,4 +88,4 @@ let of_posts pdesc posts = Some (map exec_state ~f:(fun _astate -> (* prefer [astate] since it is an equivalent state that has been normalized *) - AbductiveDomain.of_post pdesc astate )) ) + AbductiveDomain.summary_of_post pdesc astate )) ) diff --git a/infer/src/pulse/PulseExecutionDomain.mli b/infer/src/pulse/PulseExecutionDomain.mli index 9d4791db8..814fe90e3 100644 --- a/infer/src/pulse/PulseExecutionDomain.mli +++ b/infer/src/pulse/PulseExecutionDomain.mli @@ -9,18 +9,22 @@ open! IStd module AbductiveDomain = PulseAbductiveDomain module LatentIssue = PulseLatentIssue -type t = - | AbortProgram of AbductiveDomain.t +type 'abductive_domain_t base_t = + | ContinueProgram of 'abductive_domain_t (** represents the state at the program point *) + | ExitProgram of 'abductive_domain_t (** represents the state originating at exit/divergence. *) + | AbortProgram of AbductiveDomain.summary (** represents the state at the program point that caused an error *) - | ContinueProgram of AbductiveDomain.t (** represents the state at the program point *) - | ExitProgram of AbductiveDomain.t (** represents the state originating at exit/divergence. *) - | LatentAbortProgram of {astate: AbductiveDomain.t; latent_issue: LatentIssue.t} + | LatentAbortProgram of {astate: AbductiveDomain.summary; latent_issue: LatentIssue.t} (** this path leads to an error but we don't have conclusive enough data to report it yet *) +type t = AbductiveDomain.t base_t + include AbstractDomain.NoJoin with type t := t val continue : AbductiveDomain.t -> t -val of_posts : Procdesc.t -> t list -> t list - val mk_initial : Procdesc.t -> t + +type summary = AbductiveDomain.summary base_t + +val summary_of_posts : Procdesc.t -> t list -> summary list diff --git a/infer/src/pulse/PulseLatentIssue.ml b/infer/src/pulse/PulseLatentIssue.ml index 69f5d02da..584145e5b 100644 --- a/infer/src/pulse/PulseLatentIssue.ml +++ b/infer/src/pulse/PulseLatentIssue.ml @@ -7,6 +7,8 @@ open! IStd open PulseBasicInterface +module AbductiveDomain = PulseAbductiveDomain +module Arithmetic = PulseArithmetic type t = AccessToInvalidAddress of Diagnostic.access_to_invalid_address [@@deriving equal] @@ -20,9 +22,13 @@ let add_call call_and_loc = function AccessToInvalidAddress {access with calling_context= call_and_loc :: access.calling_context} -let should_report astate = PulseArithmetic.has_no_assumptions astate +let should_report (astate : AbductiveDomain.summary) = + Arithmetic.has_no_assumptions (astate :> AbductiveDomain.t) -let should_report_diagnostic astate (diagnostic : Diagnostic.t) = + +(* require a summary because we don't want to stop reporting because some non-abducible condition is + not true as calling context cannot possibly influence such conditions *) +let should_report_diagnostic (astate : AbductiveDomain.summary) (diagnostic : Diagnostic.t) = match diagnostic with | MemoryLeak _ | StackVariableAddressEscape _ -> (* these issues are reported regardless of the calling context, not sure if that's the right diff --git a/infer/src/pulse/PulseLatentIssue.mli b/infer/src/pulse/PulseLatentIssue.mli index ce9aa378b..44578a0d7 100644 --- a/infer/src/pulse/PulseLatentIssue.mli +++ b/infer/src/pulse/PulseLatentIssue.mli @@ -7,6 +7,7 @@ open! IStd open PulseBasicInterface +module AbductiveDomain = PulseAbductiveDomain (** A subset of [PulseDiagnostic] that can be "latent", i.e. there is a potential issue in the code but we want to delay reporting until we see the conditions for the bug manifest themselves in @@ -16,9 +17,9 @@ type t = AccessToInvalidAddress of Diagnostic.access_to_invalid_address [@@deriv val to_diagnostic : t -> Diagnostic.t -val should_report : PulseAbductiveDomain.t -> bool +val should_report : AbductiveDomain.summary -> bool val should_report_diagnostic : - PulseAbductiveDomain.t -> Diagnostic.t -> [`ReportNow | `DelayReport of t] + AbductiveDomain.summary -> Diagnostic.t -> [`ReportNow | `DelayReport of t] val add_call : CallEvent.t * Location.t -> t -> t diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 18ab3aa98..e1159e6b2 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -456,7 +456,7 @@ end module StdFunction = struct let operator_call ProcnameDispatcher.Call.FuncArg.{arg_payload= lambda_ptr_hist; typ} actuals : model = - fun {analyze_dependency} ~callee_procname:_ location ~ret astate -> + fun {analyze_dependency; proc_desc} ~callee_procname:_ location ~ret astate -> let havoc_ret (ret_id, _) astate = let event = ValueHistory.Call {f= Model "std::function::operator()"; location; in_call= []} in [PulseOperations.havoc_id ret_id [event] astate] @@ -475,7 +475,7 @@ module StdFunction = struct :: List.map actuals ~f:(fun ProcnameDispatcher.Call.FuncArg.{arg_payload; typ} -> (arg_payload, typ) ) in - PulseOperations.call + PulseOperations.call ~caller_proc_desc:proc_desc ~callee_data:(analyze_dependency callee_proc_name) location callee_proc_name ~ret ~actuals ~formals_opt:None astate diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 685fdf379..b1f64647a 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -437,8 +437,8 @@ let unknown_call call_loc reason ~ret ~actuals ~formals_opt astate = |> havoc_ret ret |> add_skipped_proc -let apply_callee callee_pname call_loc callee_exec_state ~ret ~captured_vars_with_actuals ~formals - ~actuals astate = +let apply_callee ~caller_proc_desc callee_pname call_loc callee_exec_state ~ret + ~captured_vars_with_actuals ~formals ~actuals astate = let apply callee_prepost ~f = PulseInterproc.apply_prepost callee_pname call_loc ~callee_prepost ~captured_vars_with_actuals ~formals ~actuals astate @@ -467,13 +467,18 @@ let apply_callee callee_pname call_loc callee_exec_state ~ret ~captured_vars_wit | ExitProgram astate -> apply astate ~f:(fun astate -> Ok (Some (ExitProgram astate))) | LatentAbortProgram {astate; latent_issue} -> - apply astate ~f:(fun astate -> - let latent_issue = - LatentIssue.add_call (CallEvent.Call callee_pname, call_loc) latent_issue - in - if LatentIssue.should_report astate then - Error (LatentIssue.to_diagnostic latent_issue, astate) - else Ok (Some (LatentAbortProgram {astate; latent_issue})) ) + apply + (astate :> AbductiveDomain.t) + ~f:(fun astate -> + let astate_summary = AbductiveDomain.summary_of_post caller_proc_desc astate in + if PulseArithmetic.is_unsat_cheap (astate_summary :> AbductiveDomain.t) then Ok None + else + let latent_issue = + LatentIssue.add_call (CallEvent.Call callee_pname, call_loc) latent_issue + in + if LatentIssue.should_report astate_summary then + Error (LatentIssue.to_diagnostic latent_issue, (astate_summary :> AbductiveDomain.t)) + else Ok (Some (LatentAbortProgram {astate= astate_summary; latent_issue})) ) let get_captured_actuals location ~captured_vars ~actual_closure astate = @@ -488,8 +493,9 @@ let get_captured_actuals location ~captured_vars ~actual_closure astate = (astate, captured_vars_with_actuals) -let call ~callee_data call_loc callee_pname ~ret ~actuals ~formals_opt (astate : AbductiveDomain.t) - : (ExecutionDomain.t list, Diagnostic.t * t) result = +let call ~caller_proc_desc ~(callee_data : (Procdesc.t * PulseSummary.t) option) call_loc + callee_pname ~ret ~actuals ~formals_opt (astate : AbductiveDomain.t) : + (ExecutionDomain.t list, Diagnostic.t * t) result = match callee_data with | Some (callee_proc_desc, exec_states) -> let formals = @@ -516,12 +522,14 @@ let call ~callee_data call_loc callee_pname ~ret ~actuals ~formals_opt (astate : Str.string_match regex (Procname.to_string callee_pname) 0 ) in (* call {!AbductiveDomain.PrePost.apply} on each pre/post pair in the summary. *) - IContainer.fold_result_until exec_states ~fold:List.fold ~init:[] + IContainer.fold_result_until + (exec_states :> ExecutionDomain.t list) + ~fold:List.fold ~init:[] ~f:(fun posts callee_exec_state -> (* apply all pre/post specs *) match - apply_callee callee_pname call_loc callee_exec_state ~captured_vars_with_actuals - ~formals ~actuals ~ret astate + apply_callee ~caller_proc_desc callee_pname call_loc callee_exec_state + ~captured_vars_with_actuals ~formals ~actuals ~ret astate with | Ok None -> (* couldn't apply pre/post pair *) diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index 58f69ed46..b45c66454 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -124,7 +124,8 @@ val check_address_escape : Location.t -> Procdesc.t -> AbstractValue.t -> ValueHistory.t -> t -> t access_result val call : - callee_data:(Procdesc.t * PulseSummary.t) option + caller_proc_desc:Procdesc.t + -> callee_data:(Procdesc.t * PulseSummary.t) option -> Location.t -> Procname.t -> ret:Ident.t * Typ.t diff --git a/infer/src/pulse/PulseSummary.ml b/infer/src/pulse/PulseSummary.ml index bfd6032a6..822bd6789 100644 --- a/infer/src/pulse/PulseSummary.ml +++ b/infer/src/pulse/PulseSummary.ml @@ -9,17 +9,17 @@ open! IStd module F = Format open PulseDomainInterface -type t = ExecutionDomain.t list +type t = ExecutionDomain.summary list let pp fmt summary = F.open_vbox 0 ; F.fprintf fmt "%d pre/post(s)@;" (List.length summary) ; - List.iteri summary ~f:(fun i pre_post -> - F.fprintf fmt "#%d: @[%a@]@;" i ExecutionDomain.pp pre_post ) ; + List.iteri summary ~f:(fun i (pre_post : ExecutionDomain.summary) -> + F.fprintf fmt "#%d: @[%a@]@;" i ExecutionDomain.pp (pre_post :> ExecutionDomain.t) ) ; F.close_box () let of_posts pdesc posts = AnalysisCallbacks.html_debug_new_node_session (Procdesc.get_exit_node pdesc) ~pp_name:(fun fmt -> F.pp_print_string fmt "pulse summary creation") - ~f:(fun () -> ExecutionDomain.of_posts pdesc posts) + ~f:(fun () -> ExecutionDomain.summary_of_posts pdesc posts) diff --git a/infer/src/pulse/PulseSummary.mli b/infer/src/pulse/PulseSummary.mli index 676759217..7fd0567a2 100644 --- a/infer/src/pulse/PulseSummary.mli +++ b/infer/src/pulse/PulseSummary.mli @@ -8,7 +8,7 @@ open! IStd open PulseDomainInterface -type t = ExecutionDomain.t list +type t = ExecutionDomain.summary list val of_posts : Procdesc.t -> ExecutionDomain.t list -> t diff --git a/infer/src/topl/Topl.ml b/infer/src/topl/Topl.ml index 336e7b4bb..a5d30c4ef 100644 --- a/infer/src/topl/Topl.ml +++ b/infer/src/topl/Topl.ml @@ -304,10 +304,10 @@ let add_errors_biabduction {InterproceduralAnalysis.proc_desc; tenv; err_log} bi List.iter ~f:handle_preposts preposts -let add_errors_pulse {InterproceduralAnalysis.proc_desc; err_log} pulse_summary = +let add_errors_pulse {InterproceduralAnalysis.proc_desc; err_log} (pulse_summary : PulseSummary.t) = let pulse_summary = let f = function PulseExecutionDomain.ContinueProgram s -> Some s | _ -> None in - List.filter_map ~f pulse_summary + List.filter_map ~f (pulse_summary :> PulseExecutionDomain.t list) in let proc_name = Procdesc.get_proc_name proc_desc in if not (ToplUtils.is_synthesized proc_name) then