From 30c23f8cd6d6fd9724783609709d83a534ea1ed0 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Thu, 16 Apr 2020 03:37:28 -0700 Subject: [PATCH] [sledge] Fix term ordering bug between monomials and vars MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Summary: Fix the crash in ``` (And_eq () (Var (id 10) (name v)) (Mul (((Var (id 8) (name v)) 1) ((Var (id 9) (name v)) 1))) ((xs ()) (sat true) (rep ()))) ``` The solver for interpreted functions relies on the solution substitutions containing mappings from variables to interpreted applications, and never in the reverse. When solving equations involving polynomials, this constraint is specifically established. But for equalities involving only monomials, it could happen that e.g. `x` was chosen as the representative of `a × b`, which violates this constraint. Reviewed By: jvillard Differential Revision: D20596422 fbshipit-source-id: 69b026f03 --- sledge/lib/equality_test.ml | 23 ++++++++++++----------- sledge/lib/sh_test.ml | 14 +++++++------- sledge/lib/solver_test.ml | 6 ++---- sledge/lib/term.ml | 8 ++++---- sledge/lib/term.mli | 4 ++-- sledge/lib/term_test.ml | 28 ++++++++++++++-------------- 6 files changed, 41 insertions(+), 42 deletions(-) diff --git a/sledge/lib/equality_test.ml b/sledge/lib/equality_test.ml index a0f468d9f..0c6d25599 100644 --- a/sledge/lib/equality_test.ml +++ b/sledge/lib/equality_test.ml @@ -15,7 +15,7 @@ let%test_module _ = * Trace.init ~margin:160 * ~config:(Result.ok_exn (Trace.parse "+Equality")) * () - * + * * [@@@warning "-32"] *) let printf pp = Format.printf "@\n%a@." pp @@ -365,10 +365,10 @@ let%test_module _ = [%expect {| {sat= false; - rep= [[%x_5 ↦ (((u8) %y_6) + 3)]; - [%y_6 ↦ (((u8) %y_6) + 2)]; - [((u8) (%x_5 + -1)) ↦ (((u8) %y_6) + 5)]; - [((u8) %y_6) ↦ ]]} |}] + rep= [[%x_5 ↦ (((u8) (%x_5 + -1)) + -2)]; + [%y_6 ↦ (((u8) (%x_5 + -1)) + -3)]; + [((u8) %y_6) ↦ (((u8) (%x_5 + -1)) + -5)]; + [((u8) (%x_5 + -1)) ↦ ]]} |}] let%test _ = is_false r16 @@ -398,9 +398,9 @@ let%test_module _ = [((u8) %x_5) ↦ %x_5]; [((u8) %y_6) ↦ ]]} - (((u8) %y_6) + 1) = %y_6 - ∧ %x_5 = ((u8) %x_5) - ∧ ((u8) %y_6) = ((u8) (((u8) %y_6) + 1)) |}] + %x_5 = ((u8) %x_5) + ∧ ((u8) %y_6) = ((u8) (((u8) %y_6) + 1)) + ∧ (((u8) %y_6) + 1) = %y_6 |}] let r19 = of_eqs [(x, y + z); (x, !0); (y, !0)] @@ -413,7 +413,8 @@ let%test_module _ = let%expect_test _ = Equality.replay - {|(Solve_for_vars (() () ((Var (id 8) (name m)) (Var (id 9) (name n)))) - ((xs ()) (sat true) (rep (((Var (id 9) (name n)) (Var (id 8) (name m)))))))|} ; - [%expect {||}] + {|(And_eq () (Var (id 10) (name v)) + (Mul (((Var (id 8) (name v)) 1) ((Var (id 9) (name v)) 1))) + ((xs ()) (sat true) (rep ())))|} ; + [%expect {| |}] end ) diff --git a/sledge/lib/sh_test.ml b/sledge/lib/sh_test.ml index fbfc00f5b..fe68382d3 100644 --- a/sledge/lib/sh_test.ml +++ b/sledge/lib/sh_test.ml @@ -137,18 +137,18 @@ let%test_module _ = [%expect {| ∃ %x_6 . - (((u8) %y_7) + 1) = %y_7 - ∧ %x_6 = ((u8) %x_6) + %x_6 = ((u8) %x_6) ∧ ((u8) %y_7) = ((u8) (((u8) %y_7) + 1)) + ∧ (((u8) %y_7) + 1) = %y_7 ∧ emp - (((u8) %y_7) + 1) = %y_7 - ∧ ((u8) %y_7) = ((u8) (((u8) %y_7) + 1)) - ∧ ((%y_7 + -1) = ((u8) %y_7)) + ((u8) %y_7) = ((u8) (((u8) %y_7) + 1)) + ∧ (((u8) %y_7) + 1) = %y_7 + ∧ (((u8) %y_7) = (%y_7 + -1)) ∧ emp - (((u8) %y_7) + 1) = %y_7 - ∧ ((u8) %y_7) = ((u8) (((u8) %y_7) + 1)) + ((u8) %y_7) = ((u8) (((u8) %y_7) + 1)) + ∧ (((u8) %y_7) + 1) = %y_7 ∧ emp |}] let%expect_test _ = diff --git a/sledge/lib/solver_test.ml b/sledge/lib/solver_test.ml index 8828f715f..aa4c72902 100644 --- a/sledge/lib/solver_test.ml +++ b/sledge/lib/solver_test.ml @@ -238,8 +238,7 @@ let%test_module _ = [%expect {| ( infer_frame: - (%l_6 + 8 × %n_9) -[ %l_6, 16 )-> ⟨(-8 × %n_9 + 16),%a_3⟩ - * %l_6 -[ %l_6, 16 )-> ⟨(8 × %n_9),%a_2⟩ + %l_6 -[ %l_6, 16 )-> ⟨(8 × %n_9),%a_2⟩^⟨(-8 × %n_9 + 16),%a_3⟩ * ( ( 2 = %n_9 ∧ emp) ∨ ( 0 = %n_9 ∧ emp) ∨ ( 1 = %n_9 ∧ emp) @@ -273,8 +272,7 @@ let%test_module _ = {| ( infer_frame: (%n_9 ≤ 2) - ∧ (%l_6 + 8 × %n_9) -[ %l_6, 16 )-> ⟨(-8 × %n_9 + 16),%a_3⟩ - * %l_6 -[ %l_6, 16 )-> ⟨(8 × %n_9),%a_2⟩ + ∧ %l_6 -[ %l_6, 16 )-> ⟨(8 × %n_9),%a_2⟩^⟨(-8 × %n_9 + 16),%a_3⟩ \- ∃ %a_1, %m_8 . %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_1⟩ ) infer_frame: |}] diff --git a/sledge/lib/term.ml b/sledge/lib/term.ml index 5c5758b7b..0f31eee2e 100644 --- a/sledge/lib/term.ml +++ b/sledge/lib/term.ml @@ -58,14 +58,14 @@ and T : sig type qset = Qset.t [@@deriving compare, equal, hash, sexp] type t = - | Add of qset - | Mul of qset | Var of {id: int; name: string} | Ap1 of op1 * t | Ap2 of op2 * t * t | Ap3 of op3 * t * t * t | ApN of opN * t iarray | RecN of recN * t iarray (** NOTE: cyclic *) + | Add of qset + | Mul of qset | Label of {parent: string; name: string} | Nondet of {msg: string} | Float of {data: string} @@ -75,14 +75,14 @@ end = struct type qset = Qset.t [@@deriving compare, equal, hash, sexp] type t = - | Add of qset - | Mul of qset | Var of {id: int; name: string} | Ap1 of op1 * t | Ap2 of op2 * t * t | Ap3 of op3 * t * t * t | ApN of opN * t iarray | RecN of recN * t iarray (** NOTE: cyclic *) + | Add of qset + | Mul of qset | Label of {parent: string; name: string} | Nondet of {msg: string} | Float of {data: string} diff --git a/sledge/lib/term.mli b/sledge/lib/term.mli index ba24c85ae..5adb1c9c9 100644 --- a/sledge/lib/term.mli +++ b/sledge/lib/term.mli @@ -73,8 +73,6 @@ and T : sig type qset = Qset.t [@@deriving compare, equal, hash, sexp] and t = private - | Add of qset (** Sum of terms with rational coefficients *) - | Mul of qset (** Product of terms with rational exponents *) | Var of {id: int; name: string} (** Local variable / virtual register *) | Ap1 of op1 * t (** Unary application *) @@ -85,6 +83,8 @@ and T : sig (** Recursive n-ary application, may recursively refer to itself (transitively) from its args. NOTE: represented by cyclic values. *) + | Add of qset (** Sum of terms with rational coefficients *) + | Mul of qset (** Product of terms with rational exponents *) | Label of {parent: string; name: string} (** Address of named code block within parent function *) | Nondet of {msg: string} diff --git a/sledge/lib/term_test.ml b/sledge/lib/term_test.ml index 16918b33e..7be43cc99 100644 --- a/sledge/lib/term_test.ml +++ b/sledge/lib/term_test.ml @@ -75,7 +75,7 @@ let%test_module _ = let%expect_test _ = pp ((!2 * z * z) + (!3 * z) + !4) ; - [%expect {| (2 × (%z_2^2) + 3 × %z_2 + 4) |}] + [%expect {| (3 × %z_2 + 2 × (%z_2^2) + 4) |}] let%expect_test _ = pp @@ -88,9 +88,9 @@ let%test_module _ = + (!9 * z * z * z) ) ; [%expect {| - (6 × (%y_1 × %z_2) + 8 × (%y_1 × %z_2^2) + 5 × (%y_1^2) - + 7 × (%y_1^2 × %z_2) + 4 × (%z_2^2) + 9 × (%z_2^3) + 3 × %y_1 - + 2 × %z_2 + 1) |}] + (3 × %y_1 + 2 × %z_2 + 6 × (%y_1 × %z_2) + 8 × (%y_1 × %z_2^2) + + 5 × (%y_1^2) + 7 × (%y_1^2 × %z_2) + 4 × (%z_2^2) + 9 × (%z_2^3) + + 1) |}] let%expect_test _ = pp (!0 * z * y) ; @@ -142,7 +142,7 @@ let%test_module _ = let%expect_test _ = pp (((!3 * y) + !2) * (!4 + (!5 * z))) ; - [%expect {| (15 × (%y_1 × %z_2) + 12 × %y_1 + 10 × %z_2 + 8) |}] + [%expect {| (12 × %y_1 + 10 × %z_2 + 15 × (%y_1 × %z_2) + 8) |}] let%expect_test _ = pp (((!2 * z) - !3 + ((!(-2) * z) + !3)) * (!4 + (!5 * z))) ; @@ -170,19 +170,19 @@ let%test_module _ = let%expect_test _ = pp (!3 * y = z = true_) ; - [%expect {| ((3 × %y_1) = %z_2) |}] + [%expect {| (%z_2 = (3 × %y_1)) |}] let%expect_test _ = pp (true_ = (!3 * y = z)) ; - [%expect {| ((3 × %y_1) = %z_2) |}] + [%expect {| (%z_2 = (3 × %y_1)) |}] let%expect_test _ = pp (!3 * y = z = false_) ; - [%expect {| ((3 × %y_1) ≠ %z_2) |}] + [%expect {| (%z_2 ≠ (3 × %y_1)) |}] let%expect_test _ = pp (false_ = (!3 * y = z)) ; - [%expect {| ((3 × %y_1) ≠ %z_2) |}] + [%expect {| (%z_2 ≠ (3 × %y_1)) |}] let%expect_test _ = pp (y - (!(-3) * y) + !4) ; @@ -194,11 +194,11 @@ let%test_module _ = let%expect_test _ = pp (y = (!(-3) * y) + !4) ; - [%expect {| ((-3 × %y_1 + 4) = %y_1) |}] + [%expect {| (%y_1 = (-3 × %y_1 + 4)) |}] let%expect_test _ = pp ((!(-3) * y) + !4 = y) ; - [%expect {| ((-3 × %y_1 + 4) = %y_1) |}] + [%expect {| (%y_1 = (-3 × %y_1 + 4)) |}] let%expect_test _ = pp (sub true_ (z = !4)) ; @@ -206,7 +206,7 @@ let%test_module _ = let%expect_test _ = pp (add true_ (z = !4) = (z = !4)) ; - [%expect {| (((%z_2 = 4) + -1) = (%z_2 = 4)) |}] + [%expect {| ((%z_2 = 4) = ((%z_2 = 4) + -1)) |}] let%expect_test _ = pp ((!13 * z) + !42 = (!3 * y) + (!13 * z)) ; @@ -255,7 +255,7 @@ let%test_module _ = pp (z1_2 * z1_2) ; [%expect {| - ((%z_2^2) + 2 × %z_2 + 1) + (2 × %z_2 + (%z_2^2) + 1) - (6 × (%z_2^2) + 4 × (%z_2^3) + (%z_2^4) + 4 × %z_2 + 1) |}] + (4 × %z_2 + 6 × (%z_2^2) + 4 × (%z_2^3) + (%z_2^4) + 1) |}] end )