From 6273b1f445e4f22b70212d4d6f017606950b45a4 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 17 Mar 2021 03:51:44 -0700 Subject: [PATCH] [pulse] move summarisation and reporting functions around Summary: This is to avoid a circular dependency issue in the future when creating summaries might cause new reports: PulseReport depends on PulseExecuationDomain so the latter cannot emit reports. Move summary creation functions to PulseSummary instead, which sits above both of these modules. Also limit the responsabilities of PulseLatentIssues to just latent issues in preparation for another change. Reviewed By: skcho Differential Revision: D26915799 fbshipit-source-id: 3275cd514 --- infer/src/pulse/Pulse.ml | 25 ++++----- infer/src/pulse/PulseAccessResult.ml | 10 ---- infer/src/pulse/PulseAccessResult.mli | 21 -------- infer/src/pulse/PulseExecutionDomain.ml | 29 ---------- infer/src/pulse/PulseExecutionDomain.mli | 4 -- infer/src/pulse/PulseLatentIssue.ml | 26 ++++----- infer/src/pulse/PulseLatentIssue.mli | 6 +-- infer/src/pulse/PulseObjectiveCSummary.ml | 8 +-- infer/src/pulse/PulseOperations.ml | 23 ++++---- infer/src/pulse/PulseReport.ml | 65 ++++++++++++++++------- infer/src/pulse/PulseReport.mli | 12 +++-- infer/src/pulse/PulseSummary.ml | 33 +++++++++++- infer/src/pulse/PulseSummary.mli | 3 ++ 13 files changed, 127 insertions(+), 138 deletions(-) delete mode 100644 infer/src/pulse/PulseAccessResult.mli diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 2cee99739..f4318abcd 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -123,7 +123,7 @@ module PulseTransferFunctions = struct astate - let dispatch_call ({tenv; InterproceduralAnalysis.proc_desc} as analysis_data) ret call_exp + let dispatch_call ({InterproceduralAnalysis.tenv; proc_desc} as analysis_data) ret call_exp actuals call_loc flags astate = (* evaluate all actuals *) let<*> astate, rev_func_args = @@ -196,7 +196,7 @@ module PulseTransferFunctions = struct | Error _ as err -> Some err | Ok exec_state -> - ExecutionDomain.force_exit_program tenv proc_desc exec_state + PulseSummary.force_exit_program tenv proc_desc exec_state |> Option.map ~f:(fun exec_state -> Ok exec_state) ) else exec_states_res @@ -225,7 +225,8 @@ module PulseTransferFunctions = struct add and execute calls to dealloc. The main advantage of adding this calls is that some memory could be freed in dealloc, and we would be reporting a leak on it if we didn't call it. *) - let execute_injected_dealloc_calls analysis_data vars astate location = + let execute_injected_dealloc_calls + ({InterproceduralAnalysis.tenv; proc_desc; err_log} as analysis_data) vars astate location = let used_ids = Stack.keys astate |> List.filter_map ~f:(fun var -> Var.get_ident var) in Ident.update_name_generator used_ids ; let call_dealloc (astate_list : Domain.t list) (ret_id, id, typ, dealloc) = @@ -243,7 +244,7 @@ module PulseTransferFunctions = struct [astate] | ContinueProgram astate -> dispatch_call analysis_data ret call_exp actuals location call_flags astate - |> PulseReport.report_exec_results analysis_data ) + |> PulseReport.report_exec_results tenv proc_desc err_log ) in let dynamic_types_unreachable = PulseOperations.get_dynamic_type_unreachable_values vars astate @@ -258,8 +259,8 @@ module PulseTransferFunctions = struct let exec_instr_aux (astate : Domain.t) - ({tenv; InterproceduralAnalysis.proc_desc} as analysis_data) _cfg_node (instr : Sil.instr) : - Domain.t list = + ({InterproceduralAnalysis.tenv; proc_desc; err_log} as analysis_data) _cfg_node + (instr : Sil.instr) : Domain.t list = match astate with | ISLLatentMemoryError _ | AbortProgram _ | LatentAbortProgram _ -> (* We can also continue the analysis with the error state here @@ -282,7 +283,7 @@ module PulseTransferFunctions = struct [ (let+ astate, rhs_addr_hist = PulseOperations.eval_deref loc rhs_exp astate in PulseOperations.write_id lhs_id rhs_addr_hist astate) ] in - PulseReport.report_results analysis_data result + PulseReport.report_results tenv proc_desc err_log result | Store {e1= lhs_exp; e2= rhs_exp; loc} -> (* [*lhs_exp := rhs_exp] *) let event = ValueHistory.Assignment loc in @@ -326,7 +327,7 @@ module PulseTransferFunctions = struct | _ -> astates in - PulseReport.report_results analysis_data result + PulseReport.report_results tenv proc_desc err_log result | Prune (condition, loc, _is_then_branch, _if_kind) -> (let<*> astate = PulseOperations.prune loc ~condition astate in if PulseArithmetic.is_unsat_cheap astate then @@ -335,10 +336,10 @@ module PulseTransferFunctions = struct else (* [condition] is true or unknown value: go into the branch *) [Ok (ContinueProgram astate)]) - |> PulseReport.report_exec_results analysis_data + |> PulseReport.report_exec_results tenv proc_desc err_log | Call (ret, call_exp, actuals, loc, call_flags) -> dispatch_call analysis_data ret call_exp actuals loc call_flags astate - |> PulseReport.report_exec_results analysis_data + |> PulseReport.report_exec_results tenv proc_desc err_log | Metadata (ExitScope (vars, location)) -> let remove_vars vars astates = List.concat_map astates ~f:(fun (astate : Domain.t) -> @@ -347,7 +348,7 @@ module PulseTransferFunctions = struct [astate] | ContinueProgram astate -> PulseOperations.remove_vars tenv vars location astate - |> PulseReport.report_result analysis_data ) + |> PulseReport.report_result tenv proc_desc err_log ) in if Procname.is_java (Procdesc.get_proc_name proc_desc) then remove_vars vars [ContinueProgram astate] @@ -404,7 +405,7 @@ let with_debug_exit_node proc_desc ~f = ~f -let checker ({tenv; InterproceduralAnalysis.proc_desc; err_log} as analysis_data) = +let checker ({InterproceduralAnalysis.tenv; proc_desc; err_log} as analysis_data) = AbstractValue.State.reset () ; let initial_astate = ExecutionDomain.mk_initial tenv proc_desc in let initial = [initial_astate] in diff --git a/infer/src/pulse/PulseAccessResult.ml b/infer/src/pulse/PulseAccessResult.ml index 41f82d3aa..c5c804eb1 100644 --- a/infer/src/pulse/PulseAccessResult.ml +++ b/infer/src/pulse/PulseAccessResult.ml @@ -16,13 +16,3 @@ type 'astate error = type ('a, 'astate) base_t = ('a, 'astate error) result type 'a t = ('a, AbductiveDomain.t) base_t - -let to_summary tenv proc_desc error = - let open SatUnsat.Import in - match error with - | ReportableError {astate; diagnostic} -> - let+ astate = AbductiveDomain.summary_of_post tenv proc_desc astate in - ReportableError {astate; diagnostic} - | ISLError astate -> - let+ astate = AbductiveDomain.summary_of_post tenv proc_desc astate in - ISLError astate diff --git a/infer/src/pulse/PulseAccessResult.mli b/infer/src/pulse/PulseAccessResult.mli deleted file mode 100644 index 0719d34e6..000000000 --- a/infer/src/pulse/PulseAccessResult.mli +++ /dev/null @@ -1,21 +0,0 @@ -(* - * Copyright (c) Facebook, Inc. and its affiliates. - * - * This source code is licensed under the MIT license found in the - * LICENSE file in the root directory of this source tree. - *) - -open! IStd -open PulseBasicInterface -module AbductiveDomain = PulseAbductiveDomain - -type 'astate error = - | ReportableError of {astate: 'astate; diagnostic: Diagnostic.t} - | ISLError of 'astate - -type ('a, 'astate) base_t = ('a, 'astate error) result - -type 'a t = ('a, AbductiveDomain.t) base_t - -val to_summary : - Tenv.t -> Procdesc.t -> AbductiveDomain.t error -> AbductiveDomain.summary error SatUnsat.t diff --git a/infer/src/pulse/PulseExecutionDomain.ml b/infer/src/pulse/PulseExecutionDomain.ml index 86810e033..02ca1349e 100644 --- a/infer/src/pulse/PulseExecutionDomain.ml +++ b/infer/src/pulse/PulseExecutionDomain.ml @@ -7,7 +7,6 @@ open! IStd module F = Format -module L = Logging open PulseBasicInterface module AbductiveDomain = PulseAbductiveDomain module LatentIssue = PulseLatentIssue @@ -81,31 +80,3 @@ let get_astate : t -> AbductiveDomain.t = function let is_unsat_cheap exec_state = PathCondition.is_unsat_cheap (get_astate exec_state).path_condition type summary = AbductiveDomain.summary base_t [@@deriving compare, equal, yojson_of] - -let summary_of_post_common tenv ~continue_program proc_desc = function - | ContinueProgram astate -> ( - match AbductiveDomain.summary_of_post tenv proc_desc astate with - | Unsat -> - None - | Sat astate -> - Some (continue_program astate) ) - (* already a summary but need to reconstruct the variants to make the type system happy *) - | AbortProgram astate -> - Some (AbortProgram astate) - | ExitProgram astate -> - Some (ExitProgram astate) - | LatentAbortProgram {astate; latent_issue} -> - Some (LatentAbortProgram {astate; latent_issue}) - | ISLLatentMemoryError astate -> - Some (ISLLatentMemoryError astate) - - -let summary_of_posts tenv proc_desc posts = - List.filter_mapi posts ~f:(fun i exec_state -> - L.d_printfln "Creating spec out of state #%d:@\n%a" i pp exec_state ; - summary_of_post_common tenv proc_desc exec_state ~continue_program:(fun astate -> - ContinueProgram astate ) ) - - -let force_exit_program tenv proc_desc post = - summary_of_post_common tenv proc_desc post ~continue_program:(fun astate -> ExitProgram astate) diff --git a/infer/src/pulse/PulseExecutionDomain.mli b/infer/src/pulse/PulseExecutionDomain.mli index 8a642a794..e6fb02394 100644 --- a/infer/src/pulse/PulseExecutionDomain.mli +++ b/infer/src/pulse/PulseExecutionDomain.mli @@ -33,7 +33,3 @@ val is_unsat_cheap : t -> bool (** see {!PulsePathCondition.is_unsat_cheap} *) type summary = AbductiveDomain.summary base_t [@@deriving compare, equal, yojson_of] - -val summary_of_posts : Tenv.t -> Procdesc.t -> t list -> summary list - -val force_exit_program : Tenv.t -> Procdesc.t -> t -> t option diff --git a/infer/src/pulse/PulseLatentIssue.ml b/infer/src/pulse/PulseLatentIssue.ml index 04d3014ef..a12379cf6 100644 --- a/infer/src/pulse/PulseLatentIssue.ml +++ b/infer/src/pulse/PulseLatentIssue.ml @@ -35,19 +35,13 @@ let is_manifest (astate : AbductiveDomain.summary) = (* 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 (access_error : AbductiveDomain.summary PulseAccessResult.error) = - match access_error with - | ReportableError {astate; diagnostic} -> ( - match diagnostic with - | MemoryLeak _ | StackVariableAddressEscape _ -> - (* these issues are reported regardless of the calling context, not sure if that's the right - decision yet *) - `ReportNow (astate, diagnostic) - | AccessToInvalidAddress latent -> - if is_manifest astate then `ReportNow (astate, diagnostic) - else `DelayReport (astate, AccessToInvalidAddress latent) - | ReadUninitializedValue latent -> - if is_manifest astate then `ReportNow (astate, diagnostic) - else `DelayReport (astate, ReadUninitializedValue latent) ) - | ISLError astate -> - `ISLDelay astate +let should_report (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 + decision yet *) + `ReportNow + | AccessToInvalidAddress latent -> + if is_manifest astate then `ReportNow else `DelayReport (AccessToInvalidAddress latent) + | ReadUninitializedValue latent -> + if is_manifest astate then `ReportNow else `DelayReport (ReadUninitializedValue latent) diff --git a/infer/src/pulse/PulseLatentIssue.mli b/infer/src/pulse/PulseLatentIssue.mli index f76a086b8..99e4a95a6 100644 --- a/infer/src/pulse/PulseLatentIssue.mli +++ b/infer/src/pulse/PulseLatentIssue.mli @@ -20,10 +20,6 @@ type t = val to_diagnostic : t -> Diagnostic.t -val should_report : - AbductiveDomain.summary PulseAccessResult.error - -> [> `DelayReport of AbductiveDomain.summary * t - | `ReportNow of AbductiveDomain.summary * Diagnostic.t - | `ISLDelay of AbductiveDomain.summary ] +val should_report : AbductiveDomain.summary -> Diagnostic.t -> [> `DelayReport of t | `ReportNow] val add_call : CallEvent.t * Location.t -> t -> t diff --git a/infer/src/pulse/PulseObjectiveCSummary.ml b/infer/src/pulse/PulseObjectiveCSummary.ml index 0a50993a1..eab331f3e 100644 --- a/infer/src/pulse/PulseObjectiveCSummary.ml +++ b/infer/src/pulse/PulseObjectiveCSummary.ml @@ -25,7 +25,7 @@ let mk_objc_method_nil_summary_aux proc_desc astate = PulseOperations.write_deref location ~ref:ret_var_addr_hist ~obj:self_value astate -let mk_objc_method_nil_summary ({InterproceduralAnalysis.proc_desc} as analysis_data) initial = +let mk_objc_method_nil_summary {InterproceduralAnalysis.tenv; proc_desc; err_log} initial = let proc_name = Procdesc.get_proc_name proc_desc in match (initial, proc_name) with | ContinueProgram astate, Procname.ObjC_Cpp {kind= ObjCInstanceMethod} @@ -36,7 +36,7 @@ let mk_objc_method_nil_summary ({InterproceduralAnalysis.proc_desc} as analysis_ However, there is an exception in the case where the return type is non-POD. In that case it's UB and we want to report an error. *) let result = mk_objc_method_nil_summary_aux proc_desc astate in - Some (PulseReport.report_result analysis_data result) + Some (PulseReport.report_result tenv proc_desc err_log result) | ContinueProgram _, _ | ExitProgram _, _ | AbortProgram _, _ @@ -45,7 +45,7 @@ let mk_objc_method_nil_summary ({InterproceduralAnalysis.proc_desc} as analysis_ None -let append_objc_self_positive ({InterproceduralAnalysis.proc_desc} as analysis_data) astate = +let append_objc_self_positive {InterproceduralAnalysis.tenv; proc_desc; err_log} astate = let location = Procdesc.get_loc proc_desc in let self = mk_objc_self_pvar proc_desc in match astate with @@ -54,7 +54,7 @@ let append_objc_self_positive ({InterproceduralAnalysis.proc_desc} as analysis_d let+ astate, value = PulseOperations.eval_deref location (Lvar self) astate in PulseArithmetic.prune_positive (fst value) astate in - PulseReport.report_result analysis_data result + PulseReport.report_result tenv proc_desc err_log result | ExitProgram _ | AbortProgram _ | LatentAbortProgram _ | ISLLatentMemoryError _ -> [astate] diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 60d67871d..8d32252dd 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -643,7 +643,9 @@ let apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state map_call_result ~is_isl_error_prepost:false (astate :> AbductiveDomain.t) ~f:(fun astate -> - let+ astate_summary = AbductiveDomain.summary_of_post tenv caller_proc_desc astate in + let+ (astate_summary : AbductiveDomain.summary) = + AbductiveDomain.summary_of_post tenv caller_proc_desc astate + in match callee_exec_state with | ContinueProgram _ | ISLLatentMemoryError _ -> assert false @@ -655,17 +657,14 @@ let apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state let latent_issue = LatentIssue.add_call (CallEvent.Call callee_pname, call_loc) latent_issue in - let error = - ReportableError - {diagnostic= LatentIssue.to_diagnostic latent_issue; astate= astate_summary} - in - match LatentIssue.should_report error with - | `DelayReport (astate, latent_issue) -> - Ok (LatentAbortProgram {astate; latent_issue}) - | `ReportNow (astate, diagnostic) -> - Error (ReportableError {diagnostic; astate= (astate :> AbductiveDomain.t)}) - | `ISLDelay astate -> - Error (ISLError (astate :> AbductiveDomain.t)) ) ) + let diagnostic = LatentIssue.to_diagnostic latent_issue in + match LatentIssue.should_report astate_summary diagnostic with + | `DelayReport latent_issue -> + Ok (LatentAbortProgram {astate= astate_summary; latent_issue}) + | `ReportNow -> + Error + (ReportableError {diagnostic; astate= (astate_summary :> AbductiveDomain.t)}) ) + ) | ISLLatentMemoryError astate -> map_call_result ~is_isl_error_prepost:true (astate :> AbductiveDomain.t) diff --git a/infer/src/pulse/PulseReport.ml b/infer/src/pulse/PulseReport.ml index 60d2997f9..bb5157902 100644 --- a/infer/src/pulse/PulseReport.ml +++ b/infer/src/pulse/PulseReport.ml @@ -8,7 +8,6 @@ open! IStd open PulseBasicInterface open PulseDomainInterface -open PulseOperations.Import let report ?(extra_trace = []) proc_desc err_log diagnostic = let open Diagnostic in @@ -45,37 +44,65 @@ let is_suppressed tenv proc_desc diagnostic astate = false -let report_error tenv proc_desc err_log access_error = - match LatentIssue.should_report access_error with - | `ReportNow (astate_summary, diagnostic) -> - if not (is_suppressed tenv proc_desc diagnostic astate_summary) then - report proc_desc err_log diagnostic ; - AbortProgram astate_summary - | `DelayReport (astate, latent_issue) -> - if Config.pulse_report_latent_issues then report_latent_issue proc_desc err_log latent_issue ; - LatentAbortProgram {astate; latent_issue} - | `ISLDelay astate -> +let summary_of_error_post tenv proc_desc mk_error astate = + match AbductiveDomain.summary_of_post tenv proc_desc astate with + | Sat astate -> + Sat (mk_error astate) + | Unsat -> + Unsat + + +let summary_error_of_error tenv proc_desc (error : AbductiveDomain.t AccessResult.error) : + AbductiveDomain.summary AccessResult.error SatUnsat.t = + match error with + | ReportableError {astate; diagnostic} -> + summary_of_error_post tenv proc_desc + (fun astate -> AccessResult.ReportableError {astate; diagnostic}) + astate + | ISLError astate -> + summary_of_error_post tenv proc_desc (fun astate -> AccessResult.ISLError astate) astate + + +let report_summary_error tenv proc_desc err_log + (access_error : AbductiveDomain.summary AccessResult.error) : _ ExecutionDomain.base_t = + match access_error with + | ISLError astate -> ISLLatentMemoryError astate + | ReportableError {astate; diagnostic} -> ( + match LatentIssue.should_report astate diagnostic with + | `ReportNow -> + if not (is_suppressed tenv proc_desc diagnostic astate) then + report proc_desc err_log diagnostic ; + AbortProgram astate + | `DelayReport latent_issue -> + if Config.pulse_report_latent_issues then report_latent_issue proc_desc err_log latent_issue ; + LatentAbortProgram {astate; latent_issue} ) + + +let report_error tenv proc_desc err_log (access_error : AbductiveDomain.t AccessResult.error) = + let open SatUnsat.Import in + summary_error_of_error tenv proc_desc access_error >>| report_summary_error tenv proc_desc err_log -let report_exec_results {InterproceduralAnalysis.proc_desc; tenv; err_log} results = +let report_exec_results tenv proc_desc err_log results = List.filter_map results ~f:(fun exec_result -> match exec_result with | Ok post -> Some post | Error error -> ( - match AccessResult.to_summary tenv proc_desc error with + match report_error tenv proc_desc err_log error with | Unsat -> None - | Sat error -> - Some (report_error tenv proc_desc err_log error) ) ) + | Sat exec_state -> + Some exec_state ) ) -let report_results analysis_data results = +let report_results tenv proc_desc err_log results = + let open IResult.Let_syntax in List.map results ~f:(fun result -> let+ astate = result in - ContinueProgram astate ) - |> report_exec_results analysis_data + ExecutionDomain.ContinueProgram astate ) + |> report_exec_results tenv proc_desc err_log -let report_result analysis_data result = report_results analysis_data [result] +let report_result tenv proc_desc err_log result = report_results tenv proc_desc err_log [result] diff --git a/infer/src/pulse/PulseReport.mli b/infer/src/pulse/PulseReport.mli index bb0416a26..65fedb6ed 100644 --- a/infer/src/pulse/PulseReport.mli +++ b/infer/src/pulse/PulseReport.mli @@ -9,16 +9,18 @@ open! IStd open PulseDomainInterface val report_result : - PulseSummary.t InterproceduralAnalysis.t - -> AbductiveDomain.t AccessResult.t - -> ExecutionDomain.t list + Tenv.t -> Procdesc.t -> Errlog.t -> AbductiveDomain.t AccessResult.t -> ExecutionDomain.t list val report_results : - PulseSummary.t InterproceduralAnalysis.t + Tenv.t + -> Procdesc.t + -> Errlog.t -> AbductiveDomain.t AccessResult.t list -> ExecutionDomain.t list val report_exec_results : - PulseSummary.t InterproceduralAnalysis.t + Tenv.t + -> Procdesc.t + -> Errlog.t -> ExecutionDomain.t AccessResult.t list -> ExecutionDomain.t list diff --git a/infer/src/pulse/PulseSummary.ml b/infer/src/pulse/PulseSummary.ml index 65deaf692..bd3bbb863 100644 --- a/infer/src/pulse/PulseSummary.ml +++ b/infer/src/pulse/PulseSummary.ml @@ -7,6 +7,8 @@ open! IStd module F = Format +module L = Logging +open PulseBasicInterface open PulseDomainInterface type t = ExecutionDomain.summary list [@@deriving yojson_of] @@ -19,4 +21,33 @@ let pp fmt summary = F.close_box () -let of_posts tenv pdesc posts = ExecutionDomain.summary_of_posts tenv pdesc posts +let exec_summary_of_post_common tenv ~continue_program proc_desc (exec_astate : ExecutionDomain.t) : + _ ExecutionDomain.base_t option = + match exec_astate with + | ContinueProgram astate -> ( + match AbductiveDomain.summary_of_post tenv proc_desc astate with + | Unsat -> + None + | Sat astate -> + Some (continue_program astate) ) + (* already a summary but need to reconstruct the variants to make the type system happy :( *) + | AbortProgram astate -> + Some (AbortProgram astate) + | ExitProgram astate -> + Some (ExitProgram astate) + | LatentAbortProgram {astate; latent_issue} -> + Some (LatentAbortProgram {astate; latent_issue}) + | ISLLatentMemoryError astate -> + Some (ISLLatentMemoryError astate) + + +let force_exit_program tenv proc_desc post = + exec_summary_of_post_common tenv proc_desc post ~continue_program:(fun astate -> + ExitProgram astate ) + + +let of_posts tenv proc_desc posts = + List.filter_mapi posts ~f:(fun i exec_state -> + L.d_printfln "Creating spec out of state #%d:@\n%a" i ExecutionDomain.pp exec_state ; + exec_summary_of_post_common tenv proc_desc exec_state ~continue_program:(fun astate -> + ContinueProgram astate ) ) diff --git a/infer/src/pulse/PulseSummary.mli b/infer/src/pulse/PulseSummary.mli index 00733f818..de7fdcf6c 100644 --- a/infer/src/pulse/PulseSummary.mli +++ b/infer/src/pulse/PulseSummary.mli @@ -12,4 +12,7 @@ type t = ExecutionDomain.summary list [@@deriving yojson_of] val of_posts : Tenv.t -> Procdesc.t -> ExecutionDomain.t list -> t +val force_exit_program : + Tenv.t -> Procdesc.t -> ExecutionDomain.t -> _ ExecutionDomain.base_t option + val pp : Format.formatter -> t -> unit