From e1cadb12b0a96a8d422b83f89beb246e1044171f Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Tue, 27 Oct 2020 10:12:33 -0700 Subject: [PATCH] [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 | 8 +++++- infer/src/pulse/PulseAbstractValue.mli | 6 +++- infer/src/pulse/PulseFormula.ml | 40 ++++++++++++++++++++++---- infer/src/pulse/PulseFormula.mli | 2 +- infer/src/pulse/PulsePathCondition.ml | 2 +- 5 files changed, 49 insertions(+), 9 deletions(-) diff --git a/infer/src/pulse/PulseAbstractValue.ml b/infer/src/pulse/PulseAbstractValue.ml index 6f494a5f4..576c12dae 100644 --- a/infer/src/pulse/PulseAbstractValue.ml +++ b/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) diff --git a/infer/src/pulse/PulseAbstractValue.mli b/infer/src/pulse/PulseAbstractValue.mli index 5c79c71e4..97f2e7260 100644 --- a/infer/src/pulse/PulseAbstractValue.mli +++ b/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 diff --git a/infer/src/pulse/PulseFormula.ml b/infer/src/pulse/PulseFormula.ml index 4bac45ca4..fdd86df2c 100644 --- a/infer/src/pulse/PulseFormula.ml +++ b/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 *) - ; linear_eqs: LinArith.t Var.Map.t + { var_eqs: var_eqs (** equality relation between variables *) + ; 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} diff --git a/infer/src/pulse/PulseFormula.mli b/infer/src/pulse/PulseFormula.mli index 2e5d73c38..1fece38a5 100644 --- a/infer/src/pulse/PulseFormula.mli +++ b/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 diff --git a/infer/src/pulse/PulsePathCondition.ml b/infer/src/pulse/PulsePathCondition.ml index 3ee0defdf..4e0e4a50c 100644 --- a/infer/src/pulse/PulsePathCondition.ml +++ b/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 "@[unsat:%b,@;bo: @[%a@],@;citv: @[%a@],@;formula: @[%a@]@]" is_unsat BoItvs.pp