diff --git a/infer/src/absint/AbstractDomain.ml b/infer/src/absint/AbstractDomain.ml index d6c2f1899a..aec93ce21f 100644 --- a/infer/src/absint/AbstractDomain.ml +++ b/infer/src/absint/AbstractDomain.ml @@ -126,7 +126,7 @@ module BottomLiftedUtils = struct let pp_bottom f = F.pp_print_string f SpecialChars.up_tack - let pp ~pp f = function Bottom -> pp_bottom f | NonBottom astate -> pp f astate + let pp pp f = function Bottom -> pp_bottom f | NonBottom astate -> pp f astate end module BottomLifted (Domain : S) = struct @@ -164,7 +164,7 @@ module BottomLifted (Domain : S) = struct let map = BottomLiftedUtils.map - let pp = BottomLiftedUtils.pp ~pp:Domain.pp + let pp = BottomLiftedUtils.pp Domain.pp end module TopLiftedUtils = struct diff --git a/infer/src/absint/AbstractDomain.mli b/infer/src/absint/AbstractDomain.mli index e25f6420b1..fdbaaedcf4 100644 --- a/infer/src/absint/AbstractDomain.mli +++ b/infer/src/absint/AbstractDomain.mli @@ -6,6 +6,7 @@ *) open! IStd +module F = Format (** {1 Abstract domains and domain combinators} *) @@ -108,7 +109,9 @@ module BottomLifted (Domain : S) : sig end module BottomLiftedUtils : sig - val pp_bottom : Format.formatter -> unit + val pp_bottom : F.formatter -> unit + + val pp : (F.formatter -> 't -> unit) -> F.formatter -> 't bottom_lifted -> unit end (** Create a domain with Top element from a pre-domain *) @@ -121,7 +124,7 @@ module TopLifted (Domain : S) : sig end module TopLiftedUtils : sig - val pp_top : Format.formatter -> unit + val pp_top : F.formatter -> unit end (** Create a domain with Bottom and Top elements from a pre-domain *) @@ -178,10 +181,10 @@ module StackedUtils : sig -> int val pp : - pp_below:(Format.formatter -> 'b -> unit) - -> pp:(Format.formatter -> 'v -> unit) - -> pp_above:(Format.formatter -> 'a -> unit) - -> Format.formatter + pp_below:(F.formatter -> 'b -> unit) + -> pp:(F.formatter -> 'v -> unit) + -> pp_above:(F.formatter -> 'a -> unit) + -> F.formatter -> ('b, 'v, 'a) below_above -> unit diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index caaa4180ea..2f4eaf1cd1 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/infer/src/absint/AbstractInterpreter.ml @@ -335,7 +335,7 @@ struct F.fprintf f "#%d: @[%a@]@;" i (T.pp_disjunct pp_kind) disjunct ) in F.fprintf f "@[%d disjuncts:@;%a%a@]" (List.length disjuncts) pp_disjuncts disjuncts - (Pp.html_collapsible_block ~name:"Non-disjunctive state" pp_kind T.NonDisjDomain.pp) + (Pp.html_collapsible_block ~name:"Non-disjunctive state" pp_kind (T.pp_non_disj pp_kind)) non_disj diff --git a/infer/src/absint/TransferFunctions.ml b/infer/src/absint/TransferFunctions.ml index 434922a6a4..173240dc7b 100644 --- a/infer/src/absint/TransferFunctions.ml +++ b/infer/src/absint/TransferFunctions.ml @@ -66,4 +66,6 @@ module type DisjReady = sig val pp_session_name : CFG.Node.t -> Format.formatter -> unit val pp_disjunct : Pp.print_kind -> Format.formatter -> DisjDomain.t -> unit + + val pp_non_disj : Pp.print_kind -> Format.formatter -> NonDisjDomain.t -> unit end diff --git a/infer/src/absint/TransferFunctions.mli b/infer/src/absint/TransferFunctions.mli index 4057d1751d..90889d0879 100644 --- a/infer/src/absint/TransferFunctions.mli +++ b/infer/src/absint/TransferFunctions.mli @@ -76,4 +76,6 @@ module type DisjReady = sig val pp_session_name : CFG.Node.t -> Format.formatter -> unit val pp_disjunct : Pp.print_kind -> Format.formatter -> DisjDomain.t -> unit + + val pp_non_disj : Pp.print_kind -> Format.formatter -> NonDisjDomain.t -> unit end diff --git a/infer/src/checkers/DisjunctiveDemo.ml b/infer/src/checkers/DisjunctiveDemo.ml index 99b3faf259..0791cfc05f 100644 --- a/infer/src/checkers/DisjunctiveDemo.ml +++ b/infer/src/checkers/DisjunctiveDemo.ml @@ -71,6 +71,8 @@ module DisjunctiveAnalyzerTransferFunctions = struct let pp_session_name _node fmt = F.pp_print_string fmt "Disjunctive Domain demo" let pp_disjunct _pp_kind = DisjDomain.pp + + let pp_non_disj _pp_kind = NonDisjDomain.pp end module DisjunctiveAnalyzer = diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index e4c9c1c8c0..a2c8484320 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -1526,6 +1526,9 @@ module PulseTransferFunctions = struct let pp_disjunct kind fmt (exec_astate, path) = ExecutionDomain.pp_with_kind kind (Some path) fmt exec_astate + + + let pp_non_disj kind fmt non_disj = NonDisjDomain.pp_with_kind kind fmt non_disj end let summary_count_channel = diff --git a/infer/src/pulse/PulseNonDisjunctiveDomain.ml b/infer/src/pulse/PulseNonDisjunctiveDomain.ml index 89ce245f0d..af7393c65e 100644 --- a/infer/src/pulse/PulseNonDisjunctiveDomain.ml +++ b/infer/src/pulse/PulseNonDisjunctiveDomain.ml @@ -699,6 +699,11 @@ module OverApproxDomain = struct let widen ~prev ~next ~num_iters = if Config.pulse_over_approximate_reasoning then widen ~prev ~next ~num_iters else bottom + + + let pp_with_kind pp_kind fmt astate_path = + let pp fmt (astate, path) = PulsePp.pp pp_kind (Some path) fmt astate in + AbstractDomain.BottomLiftedUtils.pp pp fmt astate_path end type t = @@ -708,12 +713,15 @@ type t = ; astate: OverApproxDomain.t } [@@deriving abstract_domain] -let pp fmt ({intra; inter; has_dropped_disjuncts; astate} [@warning "missing-record-field-pattern"]) - = +let pp_with_kind pp_kind fmt + ({intra; inter; has_dropped_disjuncts; astate} [@warning "missing-record-field-pattern"]) = F.fprintf fmt "@[%a,@ %a%s@\n @[%a@]@]" IntraDom.pp intra InterDom.pp inter (if has_dropped_disjuncts then " (some disjuncts dropped)" else "") - OverApproxDomain.pp astate + (OverApproxDomain.pp_with_kind pp_kind) + astate + +let pp fmt non_disj = pp_with_kind TEXT fmt non_disj let bottom = {intra= IntraDom.bottom; inter= InterDom.bottom; has_dropped_disjuncts= false; astate= Bottom} diff --git a/infer/src/pulse/PulseNonDisjunctiveDomain.mli b/infer/src/pulse/PulseNonDisjunctiveDomain.mli index 40b31a5a64..516326d1a0 100644 --- a/infer/src/pulse/PulseNonDisjunctiveDomain.mli +++ b/infer/src/pulse/PulseNonDisjunctiveDomain.mli @@ -6,6 +6,7 @@ *) open! IStd +module F = Format open PulseBasicInterface module BaseMemory = PulseBaseMemory module DecompilerExpr = PulseDecompilerExpr @@ -39,6 +40,8 @@ type parameter_spec_t = include AbstractDomain.WithBottomTop +val pp_with_kind : Pp.print_kind -> F.formatter -> t -> unit + type summary val make_summary : t -> summary