[pulse] emit formula of path conditions in json output

Summary: Needed for REDOCS.

Reviewed By: ngorogiannis

Differential Revision: D24568404

fbshipit-source-id: 30fed9879

infer/src/pulse/PulseAbstractValue.ml

@@ -34,7 +34,13 @@ module PPKey = struct
 end
 
 module Set = PrettyPrintable.MakePPSet (PPKey)
-module Map = PrettyPrintable.MakePPMap (PPKey)
+
+module Map = struct
+  include PrettyPrintable.MakePPMap (PPKey)
+
+  let yojson_of_t yojson_of_val m =
+    `List (List.map ~f:(fun (k, v) -> `List [yojson_of_t k; yojson_of_val v]) (bindings m))
+end
 
 module Constants = struct
   module M = Caml.Map.Make (IntLit)

infer/src/pulse/PulseAbstractValue.mli

@@ -28,7 +28,11 @@ end
 
 module Set : PrettyPrintable.PPSet with type elt = t
 
-module Map : PrettyPrintable.PPMap with type key = t
+module Map : sig
+  include PrettyPrintable.PPMap with type key = t
+
+  val yojson_of_t : ('a -> Yojson.Safe.t) -> 'a t -> Yojson.Safe.t
+end
 
 (** internal state of the module
 

infer/src/pulse/PulseFormula.ml

@@ -37,12 +37,20 @@ module Q = struct
   let to_int64 q = conv_protect Q.to_int64 q
 
   let to_bigint q = conv_protect Q.to_bigint q
+
+  type z = Z.t
+
+  let yojson_of_z z = `String (Z.to_string z)
+
+  type _q = t = {num: z; den: z} [@@deriving yojson_of]
+
+  let yojson_of_t = [%yojson_of: _q]
 end
 
 (** Linear Arithmetic *)
 module LinArith : sig
   (** linear combination of variables, eg [2·x + 3/4·y + 12] *)
-  type t [@@deriving compare]
+  type t [@@deriving compare, yojson_of]
 
   type subst_target = QSubst of Q.t | VarSubst of Var.t | LinSubst of t
 
@@ -85,6 +93,8 @@ end = struct
   (** invariant: the representation is always "canonical": coefficients cannot be [Q.zero] *)
   type t = Q.t Var.Map.t * Q.t [@@deriving compare]
 
+  let yojson_of_t (vs, c) = `List [Var.Map.yojson_of_t Q.yojson_of_t vs; Q.yojson_of_t c]
+
   type subst_target = QSubst of Q.t | VarSubst of Var.t | LinSubst of t
 
   let pp pp_var fmt (vs, c) =
@@ -231,7 +241,7 @@ module Term = struct
     | BitShiftLeft of t * t
     | BitShiftRight of t * t
     | BitXor of t * t
-  [@@deriving compare]
+  [@@deriving compare, yojson_of]
 
   let equal_syntax = [%compare.equal: t]
 
@@ -695,7 +705,7 @@ module Atom = struct
     | LessThan of Term.t * Term.t
     | Equal of Term.t * Term.t
     | NotEqual of Term.t * Term.t
-  [@@deriving compare]
+  [@@deriving compare, yojson_of]
 
   let pp_with_pp_var pp_var fmt atom =
     (* add parens around terms that look like atoms to disambiguate *)
@@ -937,6 +947,9 @@ module Atom = struct
           ~fold:(IContainer.fold_of_pervasives_set_fold fold)
           ~pp_item:(fun fmt atom -> F.fprintf fmt "{%a}" (pp_with_pp_var pp_var) atom)
           fmt atoms
+
+
+    let yojson_of_t atoms = `List (List.map (elements atoms) ~f:yojson_of_t)
   end
 end
 
@@ -968,11 +981,27 @@ module VarUF =
     (Var.Set)
 
 module Formula = struct
+  (* redefined for yojson output *)
+  type var_eqs = VarUF.t
+
+  let yojson_of_var_eqs var_eqs =
+    `List
+      (VarUF.fold_congruences var_eqs ~init:[] ~f:(fun jsons (repr, eqs) ->
+           `List
+             (Var.yojson_of_t (repr :> Var.t) :: List.map ~f:Var.yojson_of_t (Var.Set.elements eqs))
+           :: jsons ))
+
+
+  type linear_eqs = LinArith.t Var.Map.t
+
+  let yojson_of_linear_eqs linear_eqs = Var.Map.yojson_of_t LinArith.yojson_of_t linear_eqs
+
   type t =
-    { var_eqs: VarUF.t  (** equality relation between variables *)
+    { var_eqs: var_eqs  (** equality relation between variables *)
-    ; linear_eqs: LinArith.t Var.Map.t
+    ; linear_eqs: linear_eqs
           (** equalities of the form [x = l] where [l] is from linear arithmetic *)
     ; atoms: Atom.Set.t  (** not always normalized w.r.t. [var_eqs] and [linear_eqs] *) }
+  [@@deriving yojson_of]
 
   let ttrue = {var_eqs= VarUF.empty; linear_eqs= Var.Map.empty; atoms= Atom.Set.empty}
 
@@ -1234,6 +1263,7 @@ type t =
   { known: Formula.t  (** all the things we know to be true for sure *)
   ; pruned: Atom.Set.t  (** collection of conditions that have to be true along the path *)
   ; both: Formula.t  (** [both = known ∧ pruned], allows us to detect contradictions *) }
+[@@deriving yojson_of]
 
 let ttrue = {known= Formula.ttrue; pruned= Atom.Set.empty; both= Formula.ttrue}
 

infer/src/pulse/PulseFormula.mli

@@ -16,7 +16,7 @@ module Var = PulseAbstractValue
 
     Build formulas from SIL and tries to decide if they are (mostly un-)satisfiable. *)
 
-type t
+type t [@@deriving yojson_of]
 
 val pp : F.formatter -> t -> unit
 

infer/src/pulse/PulsePathCondition.ml

@@ -34,7 +34,7 @@ type t =
   ; citvs: CItvs.t
   ; formula: Formula.t }
 
-let yojson_of_t = [%yojson_of: _]
+let yojson_of_t {formula} = [%yojson_of: Formula.t] formula
 
 let pp fmt {is_unsat; bo_itvs; citvs; formula} =
   F.fprintf fmt "@[<hv>unsat:%b,@;bo: @[%a@],@;citv: @[%a@],@;formula: @[%a@]@]" is_unsat BoItvs.pp