From 3e7bf4343bbd66c1fab4f2fb069211a45d806b7c Mon Sep 17 00:00:00 2001
From: Jules Villard <jul@fb.com>
Date: Wed, 19 Aug 2020 04:29:37 -0700
Subject: [PATCH] [pulse] make unit tests more robust to adding more tests

Summary:
Reset the state before each test so that adding tests doesn't affect
other tests by shifting the ids of their anonymous variables.

Reviewed By: skcho

Differential Revision: D23194171

fbshipit-source-id: 7b717f160
---
 infer/src/pulse/PulseFormula.ml          |  2 +-
 infer/src/pulse/unit/PulseFormulaTest.ml | 62 +++++++++++-------------
 2 files changed, 29 insertions(+), 35 deletions(-)

diff --git a/infer/src/pulse/PulseFormula.ml b/infer/src/pulse/PulseFormula.ml
index 09ba30d0a..1cf14ca43 100644
--- a/infer/src/pulse/PulseFormula.ml
+++ b/infer/src/pulse/PulseFormula.ml
@@ -730,7 +730,7 @@ let pp_with_pp_var pp_var fmt phi =
         ~pp_item:(fun fmt atom -> F.fprintf fmt "{%a}" (Atom.pp_with_pp_var pp_var) atom)
         fmt atoms
   in
-  F.fprintf fmt "[@[<hv>%a@ &&@ %a@ &&@ %a@]]"
+  F.fprintf fmt "@[<hv>%a@ &&@ %a@ &&@ %a@]"
     (VarUF.pp ~pp_empty:(fun fmt -> F.pp_print_string fmt "true (no var=var)") pp_var)
     phi.var_eqs pp_linear_eqs phi.linear_eqs pp_atoms phi.atoms
 
diff --git a/infer/src/pulse/unit/PulseFormulaTest.ml b/infer/src/pulse/unit/PulseFormulaTest.ml
index 1513b1297..a33cee5fd 100644
--- a/infer/src/pulse/unit/PulseFormulaTest.ml
+++ b/infer/src/pulse/unit/PulseFormulaTest.ml
@@ -90,6 +90,10 @@ let%test_module _ =
 
     let v = op_of_var (mk_var "v")
 
+    (** reset to this state before each test so that variable id's remain stable when tests are
+        added in the future *)
+    let init_vars_state = AbstractValue.State.get ()
+
     let pp_var fmt v =
       match Caml.Hashtbl.find_opt var_names v with
       | Some name ->
@@ -105,28 +109,28 @@ let%test_module _ =
           pp_with_pp_var pp_var fmt phi
 
 
-    let normalize f = f ttrue >>= normalize |> F.printf "%a" normalized_pp
+    let test ~f phi =
+      AbstractValue.State.set init_vars_state ;
+      phi ttrue >>= f |> F.printf "%a" normalized_pp
+
 
-    let simplify ~keep f =
-      f ttrue >>= simplify ~keep:(AbstractValue.Set.of_list keep) |> F.printf "%a" normalized_pp
+    let normalize phi = test ~f:normalize phi
 
+    let simplify ~keep phi = test ~f:(simplify ~keep:(AbstractValue.Set.of_list keep)) phi
 
     (** the actual tests *)
 
     let%expect_test _ =
       normalize (x < y) ;
-      [%expect {|
-        [true (no var=var) && true (no linear) && {x < y}]|}]
+      [%expect {|true (no var=var) && true (no linear) && {x < y}|}]
 
     let%expect_test _ =
       normalize (x + i 1 - i 1 < x) ;
-      [%expect {|
-        unsat|}]
+      [%expect {|unsat|}]
 
     let%expect_test _ =
       normalize (x + (y - x) < y) ;
-      [%expect {|
-        unsat|}]
+      [%expect {|unsat|}]
 
     let%expect_test _ =
       normalize (x = y && y = z && z = i 0 && x = i 1) ;
@@ -135,63 +139,53 @@ let%test_module _ =
     (* should be false (x = w + (y+1) -> 1 = w + z -> 1 = 0)  *)
     let%expect_test _ =
       normalize (x = w + y + i 1 && y + i 1 = z && x = i 1 && w + z = i 0) ;
-      [%expect {|
-unsat|}]
+      [%expect {|unsat|}]
 
     (* same as above but atoms are given in the opposite order *)
     let%expect_test _ =
       normalize (w + z = i 0 && x = i 1 && y + i 1 = z && x = w + y + i 1) ;
-      [%expect {|
-unsat|}]
+      [%expect {|unsat|}]
 
     let%expect_test _ =
       normalize (of_binop Ne x y = i 0 && x = i 0 && y = i 1) ;
-      [%expect {|
-        unsat|}]
+      [%expect {|unsat|}]
 
     let%expect_test _ =
       normalize (of_binop Eq x y = i 0 && x = i 0 && y = i 1) ;
-      [%expect {|
-        [true (no var=var) && x = 0 ∧ y = 1 ∧ v19 = 0 && true (no atoms)]|}]
+      [%expect {|true (no var=var) && x = 0 ∧ y = 1 ∧ v6 = 0 && true (no atoms)|}]
 
     let%expect_test _ =
       normalize (x = i 0 && x < i 0) ;
-      [%expect {|
-        unsat|}]
+      [%expect {|unsat|}]
 
     let%expect_test _ =
       simplify ~keep:[x_var] (x = i 0 && y = i 1 && z = i 2 && w = i 3) ;
-      [%expect {|
-[true (no var=var) && x = 0 && true (no atoms)]|}]
+      [%expect {|true (no var=var) && x = 0 && true (no atoms)|}]
 
     let%expect_test _ =
       simplify ~keep:[x_var] (x = y + i 1 && x = i 0) ;
-      [%expect {|
-[x=v20 && x = 0 && true (no atoms)]|}]
+      [%expect {|x=v6 && x = 0 && true (no atoms)|}]
 
     let%expect_test _ =
       simplify ~keep:[y_var] (x = y + i 1 && x = i 0) ;
-      [%expect {|
-[true (no var=var) && y = -1 && true (no atoms)]|}]
+      [%expect {|true (no var=var) && y = -1 && true (no atoms)|}]
 
     (* 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 {|
-[x=v22 ∧ z=w=v23 && x = y -1 ∧ z = -1 && true (no atoms)]|}]
+      [%expect {|x=v6 ∧ z=w=v7 && x = y -1 ∧ z = -1 && true (no atoms)|}]
 
     let%expect_test _ =
       simplify ~keep:[x_var; y_var] (x = y + z && w + x + y = i 0 && v = w + i 1) ;
       [%expect
         {|
-[x=v25 ∧ v=v28
- &&
- x = 1/2·z + -1/2·w ∧ y = -1/2·z + -1/2·w ∧ v = w +1 ∧ v26 = 1/2·z + 1/2·w
- &&
- true (no atoms)]|}]
+        x=v6 ∧ v=v9
+        &&
+        x = 1/2·z + -1/2·w ∧ y = -1/2·z + -1/2·w ∧ v = w +1 ∧ v7 = 1/2·z + 1/2·w
+        &&
+        true (no atoms)|}]
 
     let%expect_test _ =
       simplify ~keep:[x_var; y_var] (x = y + i 4 && x = w && y = z) ;
-      [%expect {|
-[x=w=v29 ∧ y=z && x = y +4 && true (no atoms)]|}]
+      [%expect {|x=w=v6 ∧ y=z && x = y +4 && true (no atoms)|}]
   end )