From bf40a9119e4403efc949ca65c3a323c900d66a5e Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 13 Aug 2020 03:12:10 -0700 Subject: [PATCH] [pulse][formula] print readable variable names in unit tests Summary: Perhaps a bit overkill to introduce all this extra complexity but it makes the unit tests much more readable. In fact, this uncovered a bug in the dead variable elimination! Reviewed By: dulmarod Differential Revision: D22925548 fbshipit-source-id: d1f411683 --- infer/src/pulse/PulseFormula.ml | 81 +++++++++++++----------- infer/src/pulse/PulseFormula.mli | 4 ++ infer/src/pulse/unit/PulseFormulaTest.ml | 66 ++++++++++++------- 3 files changed, 93 insertions(+), 58 deletions(-) diff --git a/infer/src/pulse/PulseFormula.ml b/infer/src/pulse/PulseFormula.ml index 87745593c..946fb9657 100644 --- a/infer/src/pulse/PulseFormula.ml +++ b/infer/src/pulse/PulseFormula.ml @@ -66,56 +66,60 @@ module Term = struct true - let rec pp_paren ~needs_paren fmt t = - if needs_paren t then F.fprintf fmt "(%a)" pp_no_paren t else pp_no_paren fmt t + let rec pp_paren pp_var ~needs_paren fmt t = + if needs_paren t then F.fprintf fmt "(%a)" (pp_no_paren pp_var) t else pp_no_paren pp_var fmt t - and pp_no_paren fmt = function + and pp_no_paren pp_var fmt = function | Var v -> - AbstractValue.pp fmt v + pp_var fmt v | Const c -> Const.pp Pp.text fmt c | Minus t -> - F.fprintf fmt "-%a" (pp_paren ~needs_paren) t + F.fprintf fmt "-%a" (pp_paren pp_var ~needs_paren) t | BitNot t -> - F.fprintf fmt "BitNot%a" (pp_paren ~needs_paren) t + F.fprintf fmt "BitNot%a" (pp_paren pp_var ~needs_paren) t | Not t -> - F.fprintf fmt "¬%a" (pp_paren ~needs_paren) t + F.fprintf fmt "¬%a" (pp_paren pp_var ~needs_paren) t | Add (t1, Minus t2) -> - F.fprintf fmt "%a-%a" (pp_paren ~needs_paren) t1 (pp_paren ~needs_paren) t2 + F.fprintf fmt "%a-%a" (pp_paren pp_var ~needs_paren) t1 (pp_paren pp_var ~needs_paren) t2 | Add (t1, t2) -> - F.fprintf fmt "%a+%a" (pp_paren ~needs_paren) t1 (pp_paren ~needs_paren) t2 + F.fprintf fmt "%a+%a" (pp_paren pp_var ~needs_paren) t1 (pp_paren pp_var ~needs_paren) t2 | Mult (t1, t2) -> - F.fprintf fmt "%a×%a" (pp_paren ~needs_paren) t1 (pp_paren ~needs_paren) t2 + F.fprintf fmt "%a×%a" (pp_paren pp_var ~needs_paren) t1 (pp_paren pp_var ~needs_paren) t2 | Div (t1, t2) -> - F.fprintf fmt "%a÷%a" (pp_paren ~needs_paren) t1 (pp_paren ~needs_paren) t2 + F.fprintf fmt "%a÷%a" (pp_paren pp_var ~needs_paren) t1 (pp_paren pp_var ~needs_paren) t2 | Mod (t1, t2) -> - F.fprintf fmt "%a mod %a" (pp_paren ~needs_paren) t1 (pp_paren ~needs_paren) t2 + F.fprintf fmt "%a mod %a" (pp_paren pp_var ~needs_paren) t1 (pp_paren pp_var ~needs_paren) + t2 | BitAnd (t1, t2) -> - F.fprintf fmt "%a&%a" (pp_paren ~needs_paren) t1 (pp_paren ~needs_paren) t2 + F.fprintf fmt "%a&%a" (pp_paren pp_var ~needs_paren) t1 (pp_paren pp_var ~needs_paren) t2 | BitOr (t1, t2) -> - F.fprintf fmt "%a|%a" (pp_paren ~needs_paren) t1 (pp_paren ~needs_paren) t2 + F.fprintf fmt "%a|%a" (pp_paren pp_var ~needs_paren) t1 (pp_paren pp_var ~needs_paren) t2 | BitShiftLeft (t1, t2) -> - F.fprintf fmt "%a<<%a" (pp_paren ~needs_paren) t1 (pp_paren ~needs_paren) t2 + F.fprintf fmt "%a<<%a" (pp_paren pp_var ~needs_paren) t1 (pp_paren pp_var ~needs_paren) t2 | BitShiftRight (t1, t2) -> - F.fprintf fmt "%a>>%a" (pp_paren ~needs_paren) t1 (pp_paren ~needs_paren) t2 + F.fprintf fmt "%a>>%a" (pp_paren pp_var ~needs_paren) t1 (pp_paren pp_var ~needs_paren) t2 | BitXor (t1, t2) -> - F.fprintf fmt "%a xor %a" (pp_paren ~needs_paren) t1 (pp_paren ~needs_paren) t2 + F.fprintf fmt "%a xor %a" (pp_paren pp_var ~needs_paren) t1 (pp_paren pp_var ~needs_paren) + t2 | And (t1, t2) -> - F.fprintf fmt "%a∧%a" (pp_paren ~needs_paren) t1 (pp_paren ~needs_paren) t2 + F.fprintf fmt "%a∧%a" (pp_paren pp_var ~needs_paren) t1 (pp_paren pp_var ~needs_paren) t2 | Or (t1, t2) -> - F.fprintf fmt "%a∨%a" (pp_paren ~needs_paren) t1 (pp_paren ~needs_paren) t2 + F.fprintf fmt "%a∨%a" (pp_paren pp_var ~needs_paren) t1 (pp_paren pp_var ~needs_paren) t2 | LessThan (t1, t2) -> - F.fprintf fmt "%a<%a" (pp_paren ~needs_paren) t1 (pp_paren ~needs_paren) t2 + F.fprintf fmt "%a<%a" (pp_paren pp_var ~needs_paren) t1 (pp_paren pp_var ~needs_paren) t2 | LessEqual (t1, t2) -> - F.fprintf fmt "%a≤%a" (pp_paren ~needs_paren) t1 (pp_paren ~needs_paren) t2 + F.fprintf fmt "%a≤%a" (pp_paren pp_var ~needs_paren) t1 (pp_paren pp_var ~needs_paren) t2 | Equal (t1, t2) -> - F.fprintf fmt "%a=%a" (pp_paren ~needs_paren) t1 (pp_paren ~needs_paren) t2 + F.fprintf fmt "%a=%a" (pp_paren pp_var ~needs_paren) t1 (pp_paren pp_var ~needs_paren) t2 | NotEqual (t1, t2) -> - F.fprintf fmt "%a≠%a" (pp_paren ~needs_paren) t1 (pp_paren ~needs_paren) t2 + F.fprintf fmt "%a≠%a" (pp_paren pp_var ~needs_paren) t1 (pp_paren pp_var ~needs_paren) t2 - let pp fmt t = pp_no_paren fmt t + let pp_with_pp_var pp_var fmt t = pp_no_paren pp_var fmt t + + let pp fmt t = pp_with_pp_var AbstractValue.pp fmt t let of_absval v = Var v @@ -292,21 +296,24 @@ module Atom = struct type atom = t - let pp fmt atom = + let pp_with_pp_var pp_var fmt atom = (* add parens around terms that look like atoms to disambiguate *) let needs_paren (t : Term.t) = match t with LessThan _ | LessEqual _ | Equal _ | NotEqual _ -> true | _ -> false in + let pp_term = Term.pp_paren pp_var ~needs_paren in match atom with | LessEqual (t1, t2) -> - F.fprintf fmt "%a ≤ %a" (Term.pp_paren ~needs_paren) t1 (Term.pp_paren ~needs_paren) t2 + F.fprintf fmt "%a ≤ %a" pp_term t1 pp_term t2 | LessThan (t1, t2) -> - F.fprintf fmt "%a < %a" (Term.pp_paren ~needs_paren) t1 (Term.pp_paren ~needs_paren) t2 + F.fprintf fmt "%a < %a" pp_term t1 pp_term t2 | Equal (t1, t2) -> - F.fprintf fmt "%a = %a" (Term.pp_paren ~needs_paren) t1 (Term.pp_paren ~needs_paren) t2 + F.fprintf fmt "%a = %a" pp_term t1 pp_term t2 | NotEqual (t1, t2) -> - F.fprintf fmt "%a ≠ %a" (Term.pp_paren ~needs_paren) t1 (Term.pp_paren ~needs_paren) t2 + F.fprintf fmt "%a ≠ %a" pp_term t1 pp_term t2 + + let pp = pp_with_pp_var AbstractValue.pp let nnot = function | LessEqual (t1, t2) -> @@ -549,13 +556,13 @@ let is_literal_false = function False -> true | _ -> false let ttrue = True -let rec pp fmt = function +let rec pp_with_pp_var pp_var fmt = function | True -> F.fprintf fmt "true" | False -> F.fprintf fmt "false" | Atom atom -> - Atom.pp fmt atom + Atom.pp_with_pp_var pp_var fmt atom | NormalForm {congruences; facts} -> let pp_collection ~fold ~sep ~pp_item fmt coll = let pp_coll_aux is_first item = @@ -564,7 +571,7 @@ let rec pp fmt = function in F.fprintf fmt "@[%t@]" (fun _fmt -> fold coll ~init:true ~f:pp_coll_aux |> ignore) in - let term_pp_paren = Term.pp_paren ~needs_paren:Term.needs_paren in + let term_pp_paren = Term.pp_paren pp_var ~needs_paren:Term.needs_paren in let pp_ts_or_repr repr fmt ts = if UnionFind.Set.is_empty ts then term_pp_paren fmt repr else @@ -578,20 +585,22 @@ let rec pp fmt = function ~pp_item:(fun fmt ((repr : UnionFind.repr), ts) -> is_empty := false ; F.fprintf fmt "%a=%a" term_pp_paren (repr :> Term.t) (pp_ts_or_repr (repr :> Term.t)) ts ) ; - if !is_empty then pp fmt True + if !is_empty then pp_with_pp_var pp_var fmt True in let pp_atoms fmt atoms = - if Atom.Set.is_empty atoms then pp fmt True + if Atom.Set.is_empty atoms then pp_with_pp_var pp_var fmt True else pp_collection ~sep:"∧" ~fold:(IContainer.fold_of_pervasives_set_fold Atom.Set.fold) - ~pp_item:(fun fmt atom -> F.fprintf fmt "{%a}" Atom.pp atom) + ~pp_item:(fun fmt atom -> F.fprintf fmt "{%a}" (Atom.pp_with_pp_var pp_var) atom) fmt atoms in F.fprintf fmt "[@[%a@ &&@ %a@]]" pp_congruences congruences pp_atoms facts | And (phi1, phi2) -> - F.fprintf fmt "{%a}∧{%a}" pp phi1 pp phi2 + F.fprintf fmt "{%a}∧{%a}" (pp_with_pp_var pp_var) phi1 (pp_with_pp_var pp_var) phi2 + +let pp = pp_with_pp_var AbstractValue.pp module NormalForm : sig val of_formula : t -> t diff --git a/infer/src/pulse/PulseFormula.mli b/infer/src/pulse/PulseFormula.mli index f817fd037..261bf33ca 100644 --- a/infer/src/pulse/PulseFormula.mli +++ b/infer/src/pulse/PulseFormula.mli @@ -34,6 +34,10 @@ type t val pp : F.formatter -> t -> unit +val pp_with_pp_var : (F.formatter -> AbstractValue.t -> unit) -> F.formatter -> t -> unit + [@@warning "-32"] +(** only used for unit tests *) + (** {3 Build formulas from non-formulas} *) val ttrue : t diff --git a/infer/src/pulse/unit/PulseFormulaTest.ml b/infer/src/pulse/unit/PulseFormulaTest.ml index ca69bf0b1..c8c7c1205 100644 --- a/infer/src/pulse/unit/PulseFormulaTest.ml +++ b/infer/src/pulse/unit/PulseFormulaTest.ml @@ -12,12 +12,6 @@ module Formula = PulseFormula let%test_module _ = ( module struct - let normalize phi = Formula.normalize phi |> F.printf "%a" Formula.pp - - let simplify ~keep phi = - Formula.simplify ~keep:(AbstractValue.Set.of_list keep) phi |> F.printf "%a" Formula.pp - - (** shorthand for defining formulas easily *) let i i = Formula.Term.of_intlit (IntLit.of_int i) @@ -32,31 +26,59 @@ let%test_module _ = let ( && ) phi1 phi2 = Formula.aand phi1 phi2 - let x_var = AbstractValue.mk_fresh () + let var_names = Caml.Hashtbl.create 4 + + let mk_var name = + let v = AbstractValue.mk_fresh () in + Caml.Hashtbl.add var_names v name ; + v + + + let x_var = mk_var "x" let x = Formula.Term.of_absval x_var - let y_var = AbstractValue.mk_fresh () + let y_var = mk_var "y" let y = Formula.Term.of_absval y_var - let z_var = AbstractValue.mk_fresh () + let z_var = mk_var "z" let z = Formula.Term.of_absval z_var - let w = Formula.Term.of_absval (AbstractValue.mk_fresh ()) + let w = Formula.Term.of_absval (mk_var "w") + + let v = Formula.Term.of_absval (mk_var "v") + + (** utilities for writing tests *) + + let pp_var fmt v = + match Caml.Hashtbl.find_opt var_names v with + | Some name -> + F.pp_print_string fmt name + | None -> + AbstractValue.pp fmt v + + + let formula_pp = Formula.pp_with_pp_var pp_var + + let normalize phi = Formula.normalize phi |> F.printf "%a" formula_pp + + let simplify ~keep phi = + Formula.simplify ~keep:(AbstractValue.Set.of_list keep) phi |> F.printf "%a" formula_pp + - let v = Formula.Term.of_absval (AbstractValue.mk_fresh ()) + (** the actual tests *) let%expect_test _ = normalize (x + i 1 - i 1 < x) ; [%expect {| - [true && {(v1+1)+(-1) < v1}]|}] + [true && {(x+1)+(-1) < x}]|}] let%expect_test _ = normalize (x + (y - x) < y) ; [%expect {| - [true && {v1+(v2-v1) < v2}]|}] + [true && {x+(y-x) < y}]|}] let%expect_test _ = normalize (x = y && y = z && z = i 0 && x = i 1) ; @@ -67,36 +89,36 @@ let%test_module _ = let%expect_test _ = normalize (x = w + y + i 1 && y + i 1 = z && x = i 1 && w + z = i 0) ; [%expect {| -[0=(v4+v3) ∧ 1=v1=((v4+v2)+1) ∧ v3=(v2+1) && true]|}] +[0=(w+z) ∧ 1=x=((w+y)+1) ∧ z=(y+1) && true]|}] let%expect_test _ = - normalize (x = i 0 && Formula.Term.of_binop Ne x y = i 0 && y = i 1) ; + normalize (Formula.Term.of_binop Ne x y = i 0 && x = i 0 && y = i 1) ; [%expect {| - [0=v1=(0≠v2) ∧ 1=v2 && true]|}] + [0=x=(x≠y) ∧ 1=y && true]|}] let%expect_test _ = - normalize (x = i 0 && Formula.Term.of_binop Eq x y = i 0 && y = i 1) ; + normalize (Formula.Term.of_binop Eq x y = i 0 && x = i 0 && y = i 1) ; [%expect {| - [0=v1=(0=v2) ∧ 1=v2 && true]|}] + [0=x=(x=y) ∧ 1=y && true]|}] let%expect_test _ = simplify ~keep:[x_var] (x = i 0 && y = i 1 && z = i 2 && w = i 3) ; [%expect {| -[0=v1 ∧ 1=v2 ∧ 2=v3 ∧ 3=v4 && true]|}] +[0=x ∧ 1=y ∧ 2=z ∧ 3=w && true]|}] let%expect_test _ = simplify ~keep:[x_var] (x = y + i 1 && x = i 0) ; [%expect {| -[0=v1=(v2+1) && true]|}] +[0=x=(y+1) && true]|}] let%expect_test _ = simplify ~keep:[y_var] (x = y + i 1 && x = i 0) ; [%expect {| -[0=v1=(v2+1) && true]|}] +[0=x=(y+1) && true]|}] (* should keep most of this or realize that [w = z] hence this boils down to [z+1 = 0] *) let%expect_test _ = simplify ~keep:[y_var; z_var] (x = y + z && w = x - y && v = w + i 1 && v = i 0) ; [%expect {| -[0=v5=(v4+1) ∧ v1=(v2+v3) ∧ v4=(v1-v2) && true]|}] +[0=v=(w+1) ∧ x=(y+z) ∧ w=(x-y) && true]|}] end )