[pulse] fancy HTML printing for non-disj state too

Summary:
Now that non-disjunctive states include a pulse abstract state we want
to use the more concise state printing for them too.

Reviewed By: davidpichardie

Differential Revision:
D65942325

Privacy Context Container: L1208441

fbshipit-source-id: 5f3dcfdfb0dc39f87fe72a76f6cf24bd602ad103

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

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
 

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 "@[<v>%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
 
 

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

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

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 =

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 =

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}

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