From 6f5b125aa069cd655338ce631de79336d6930cfb Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 13 Aug 2020 03:12:06 -0700 Subject: [PATCH] [pulse][formula] improve printing Summary: Do not always add parens around sub-terms, and add more parens around terms in atoms and normal forms when they can be confused with the atom or normal form structure. Reviewed By: skcho Differential Revision: D22925549 fbshipit-source-id: 8646e96a5 --- infer/src/pulse/PulseFormula.ml | 115 ++++++++++++++++------- infer/src/pulse/unit/PulseFormulaTest.ml | 33 ++++--- 2 files changed, 103 insertions(+), 45 deletions(-) diff --git a/infer/src/pulse/PulseFormula.ml b/infer/src/pulse/PulseFormula.ml index 5163f87fe..87745593c 100644 --- a/infer/src/pulse/PulseFormula.ml +++ b/infer/src/pulse/PulseFormula.ml @@ -36,49 +36,87 @@ module Term = struct let equal_syntax = [%compare.equal: t] - let rec pp fmt = function + let needs_paren = function + | Const (Cint i) when IntLit.isnegative i -> + true + | Const (Cfloat _) -> + true + | Const (Cint _ | Cfun _ | Cstr _ | Cclass _) -> + false + | Var _ -> + false + | Minus _ + | BitNot _ + | Not _ + | Add _ + | Mult _ + | Div _ + | Mod _ + | BitAnd _ + | BitOr _ + | BitShiftLeft _ + | BitShiftRight _ + | BitXor _ + | And _ + | Or _ + | LessThan _ + | LessEqual _ + | Equal _ + | NotEqual _ -> + 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 + + + and pp_no_paren fmt = function | Var v -> AbstractValue.pp fmt v | Const c -> Const.pp Pp.text fmt c | Minus t -> - F.fprintf fmt "-(%a)" pp t + F.fprintf fmt "-%a" (pp_paren ~needs_paren) t | BitNot t -> - F.fprintf fmt "BitNot(%a)" pp t + F.fprintf fmt "BitNot%a" (pp_paren ~needs_paren) t | Not t -> - F.fprintf fmt "¬(%a)" pp t + F.fprintf fmt "¬%a" (pp_paren ~needs_paren) t + | Add (t1, Minus t2) -> + F.fprintf fmt "%a-%a" (pp_paren ~needs_paren) t1 (pp_paren ~needs_paren) t2 | Add (t1, t2) -> - F.fprintf fmt "(%a)+(%a)" pp t1 pp t2 + F.fprintf fmt "%a+%a" (pp_paren ~needs_paren) t1 (pp_paren ~needs_paren) t2 | Mult (t1, t2) -> - F.fprintf fmt "(%a)×(%a)" pp t1 pp t2 + F.fprintf fmt "%a×%a" (pp_paren ~needs_paren) t1 (pp_paren ~needs_paren) t2 | Div (t1, t2) -> - F.fprintf fmt "(%a)÷(%a)" pp t1 pp t2 + F.fprintf fmt "%a÷%a" (pp_paren ~needs_paren) t1 (pp_paren ~needs_paren) t2 | Mod (t1, t2) -> - F.fprintf fmt "(%a) mod (%a)" pp t1 pp t2 + F.fprintf fmt "%a mod %a" (pp_paren ~needs_paren) t1 (pp_paren ~needs_paren) t2 | BitAnd (t1, t2) -> - F.fprintf fmt "(%a)&(%a)" pp t1 pp t2 + F.fprintf fmt "%a&%a" (pp_paren ~needs_paren) t1 (pp_paren ~needs_paren) t2 | BitOr (t1, t2) -> - F.fprintf fmt "(%a)|(%a)" pp t1 pp t2 + F.fprintf fmt "%a|%a" (pp_paren ~needs_paren) t1 (pp_paren ~needs_paren) t2 | BitShiftLeft (t1, t2) -> - F.fprintf fmt "(%a)<<(%a)" pp t1 pp t2 + F.fprintf fmt "%a<<%a" (pp_paren ~needs_paren) t1 (pp_paren ~needs_paren) t2 | BitShiftRight (t1, t2) -> - F.fprintf fmt "(%a)>>(%a)" pp t1 pp t2 + F.fprintf fmt "%a>>%a" (pp_paren ~needs_paren) t1 (pp_paren ~needs_paren) t2 | BitXor (t1, t2) -> - F.fprintf fmt "(%a) xor (%a)" pp t1 pp t2 + F.fprintf fmt "%a xor %a" (pp_paren ~needs_paren) t1 (pp_paren ~needs_paren) t2 | And (t1, t2) -> - F.fprintf fmt "(%a)∧(%a)" pp t1 pp t2 + F.fprintf fmt "%a∧%a" (pp_paren ~needs_paren) t1 (pp_paren ~needs_paren) t2 | Or (t1, t2) -> - F.fprintf fmt "(%a)∨(%a)" pp t1 pp t2 + F.fprintf fmt "%a∨%a" (pp_paren ~needs_paren) t1 (pp_paren ~needs_paren) t2 | LessThan (t1, t2) -> - F.fprintf fmt "(%a)<(%a)" pp t1 pp t2 + F.fprintf fmt "%a<%a" (pp_paren ~needs_paren) t1 (pp_paren ~needs_paren) t2 | LessEqual (t1, t2) -> - F.fprintf fmt "(%a)≤(%a)" pp t1 pp t2 + F.fprintf fmt "%a≤%a" (pp_paren ~needs_paren) t1 (pp_paren ~needs_paren) t2 | Equal (t1, t2) -> - F.fprintf fmt "(%a)=(%a)" pp t1 pp t2 + F.fprintf fmt "%a=%a" (pp_paren ~needs_paren) t1 (pp_paren ~needs_paren) t2 | NotEqual (t1, t2) -> - F.fprintf fmt "(%a)≠(%a)" pp t1 pp t2 + F.fprintf fmt "%a≠%a" (pp_paren ~needs_paren) t1 (pp_paren ~needs_paren) t2 + let pp fmt t = pp_no_paren fmt t + let of_absval v = Var v let of_intlit i = Const (Cint i) @@ -254,15 +292,20 @@ module Atom = struct type atom = t - let pp fmt = function + let pp 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 + match atom with | LessEqual (t1, t2) -> - F.fprintf fmt "%a ≤ %a" Term.pp t1 Term.pp t2 + F.fprintf fmt "%a ≤ %a" (Term.pp_paren ~needs_paren) t1 (Term.pp_paren ~needs_paren) t2 | LessThan (t1, t2) -> - F.fprintf fmt "%a < %a" Term.pp t1 Term.pp t2 + F.fprintf fmt "%a < %a" (Term.pp_paren ~needs_paren) t1 (Term.pp_paren ~needs_paren) t2 | Equal (t1, t2) -> - F.fprintf fmt "%a = %a" Term.pp t1 Term.pp t2 + F.fprintf fmt "%a = %a" (Term.pp_paren ~needs_paren) t1 (Term.pp_paren ~needs_paren) t2 | NotEqual (t1, t2) -> - F.fprintf fmt "%a ≠ %a" Term.pp t1 Term.pp t2 + F.fprintf fmt "%a ≠ %a" (Term.pp_paren ~needs_paren) t1 (Term.pp_paren ~needs_paren) t2 let nnot = function @@ -521,25 +564,31 @@ 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 pp_ts_or_repr repr fmt ts = - if UnionFind.Set.is_empty ts then Term.pp fmt repr + if UnionFind.Set.is_empty ts then term_pp_paren fmt repr else pp_collection ~sep:"=" ~fold:(IContainer.fold_of_pervasives_set_fold UnionFind.Set.fold) - ~pp_item:Term.pp fmt ts + ~pp_item:term_pp_paren fmt ts in let pp_congruences fmt congruences = - pp_collection ~sep:"∧" ~fold:UnionFind.fold_congruences fmt congruences + let is_empty = ref true in + pp_collection ~sep:" ∧ " ~fold:UnionFind.fold_congruences fmt congruences ~pp_item:(fun fmt ((repr : UnionFind.repr), ts) -> - F.fprintf fmt "%a=%a" Term.pp (repr :> Term.t) (pp_ts_or_repr (repr :> Term.t)) 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 in let pp_atoms fmt atoms = - 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) - fmt atoms + if Atom.Set.is_empty atoms then pp 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) + fmt atoms in - F.fprintf fmt "[%a@;&&@ %a]" pp_congruences congruences pp_atoms facts + F.fprintf fmt "[@[%a@ &&@ %a@]]" pp_congruences congruences pp_atoms facts | And (phi1, phi2) -> F.fprintf fmt "{%a}∧{%a}" pp phi1 pp phi2 diff --git a/infer/src/pulse/unit/PulseFormulaTest.ml b/infer/src/pulse/unit/PulseFormulaTest.ml index 0dfd9a3f1..ca69bf0b1 100644 --- a/infer/src/pulse/unit/PulseFormulaTest.ml +++ b/infer/src/pulse/unit/PulseFormulaTest.ml @@ -51,14 +51,12 @@ let%test_module _ = let%expect_test _ = normalize (x + i 1 - i 1 < x) ; [%expect {| - [ && - {((v1)+(1))+(-1) < v1}]|}] + [true && {(v1+1)+(-1) < v1}]|}] let%expect_test _ = normalize (x + (y - x) < y) ; [%expect {| - [ && - {(v1)+((v2)+(-(v1))) < v2}]|}] + [true && {v1+(v2-v1) < v2}]|}] let%expect_test _ = normalize (x = y && y = z && z = i 0 && x = i 1) ; @@ -69,25 +67,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) && -]|}] +[0=(v4+v3) ∧ 1=v1=((v4+v2)+1) ∧ v3=(v2+1) && true]|}] + + let%expect_test _ = + normalize (x = i 0 && Formula.Term.of_binop Ne x y = i 0 && y = i 1) ; + [%expect {| + [0=v1=(0≠v2) ∧ 1=v2 && true]|}] + + let%expect_test _ = + normalize (x = i 0 && Formula.Term.of_binop Eq x y = i 0 && y = i 1) ; + [%expect {| + [0=v1=(0=v2) ∧ 1=v2 && 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 && -]|}] +[0=v1 ∧ 1=v2 ∧ 2=v3 ∧ 3=v4 && true]|}] + + let%expect_test _ = + simplify ~keep:[x_var] (x = y + i 1 && x = i 0) ; + [%expect {| +[0=v1=(v2+1) && true]|}] let%expect_test _ = simplify ~keep:[y_var] (x = y + i 1 && x = i 0) ; [%expect {| -[0=v1=(v2)+(1) && -]|}] +[0=v1=(v2+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)) && -]|}] +[0=v5=(v4+1) ∧ v1=(v2+v3) ∧ v4=(v1-v2) && true]|}] end )