From 49c9b3aec46dc89bb66dda8bd7e5917e548a8cfc Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Mon, 25 Feb 2019 07:07:39 -0800 Subject: [PATCH] [sledge] Strengthen Exp.invariant Summary: Arguments of `Eq | Dq | And | Or | Xor` exps are sorted. Reviewed By: mbouaziz Differential Revision: D14075514 fbshipit-source-id: 5e331758c --- sledge/src/llair/exp.ml | 37 ++++++++++++++++++++---------------- sledge/src/llair/exp.mli | 2 ++ sledge/src/llair/exp_test.ml | 32 +++++++++++++++---------------- 3 files changed, 39 insertions(+), 32 deletions(-) diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml index 80b16845c..8fa7ed22f 100644 --- a/sledge/src/llair/exp.ml +++ b/sledge/src/llair/exp.ml @@ -116,6 +116,8 @@ module T0 = struct [@@deriving compare, hash, sexp] let equal = [%compare.equal: t] + let sorted e f = compare e f <= 0 + let sort e f = if sorted e f then (e, f) else (f, e) end module T = struct @@ -406,9 +408,12 @@ let invariant ?(partial = false) e = |Urem | And | Or | Xor | Shl | Lshr | Ashr -> ( match args with | [x; y] -> ( - match (typ_of x, typ_of y) with - | Some typ, Some typ' -> assert (Typ.castable typ typ') - | _ -> assert true ) + ( match op with + | Eq | Dq | And | Or | Xor -> assert (sorted x y) + | _ -> () ) ; + match (typ_of x, typ_of y) with + | Some typ, Some typ' -> assert (Typ.castable typ typ') + | _ -> assert true ) | _ -> assert_arity 2 ) | Splat | Memory | Concat | Ord | Uno | Select -> assert_arity 2 | Conditional | Update -> assert_arity 3 @@ -682,7 +687,7 @@ let rec simp_mul typ axs bys = | ax0I, Integer {data= i}, by0M, Integer {data= j} -> mul_mf (mul_mm ax0I by0M) (integer (Z.mul ~bits i j) typ) | ax0I, axJ, by0M, byN -> - if compare axJ byN < 0 then mul_mf (mul_mm ax0J by0M) byN + if compare axJ byN <= 0 then mul_mf (mul_mm ax0J by0M) byN else mul_mf (mul_mm ax0I by0N) axJ ) in let rec mul_pm ax0J by = @@ -783,10 +788,10 @@ let simp_and x y = when Z.is_false data -> f | _ -> - let c = compare x y in + let ord = compare x y in (* e && e ==> e *) - if c = 0 then x - else if c < 0 then App {op= App {op= And; arg= x}; arg= y} + if ord = 0 then x + else if ord < 0 then App {op= App {op= And; arg= x}; arg= y} else App {op= App {op= And; arg= y}; arg= x} let simp_or x y = @@ -805,10 +810,10 @@ let simp_or x y = when Z.is_false data -> e | _ -> - let c = compare x y in + let ord = compare x y in (* e || e ==> e *) - if c = 0 then x - else if c < 0 then App {op= App {op= Or; arg= x}; arg= y} + if ord = 0 then x + else if ord < 0 then App {op= App {op= Or; arg= x}; arg= y} else App {op= App {op= Or; arg= y}; arg= x} let rec simp_not (typ : Typ.t) exp = @@ -888,11 +893,11 @@ and simp_eq x y = else (* b = true ==> b *) b | x, y -> - let c = compare x y in + let ord = compare x y in (* e = e ==> true *) - if c = 0 then bool true - else if c < 0 then App {op= App {op= Eq; arg= y}; arg= x} - else App {op= App {op= Eq; arg= x}; arg= y} + if ord = 0 then bool true + else if ord < 0 then App {op= App {op= Eq; arg= x}; arg= y} + else App {op= App {op= Eq; arg= y}; arg= x} and simp_dq x y = match simp_eq x y with @@ -911,8 +916,8 @@ let simp_xor x y = when Z.is_true data -> simp_not Typ.bool b | _ -> - let c = compare x y in - if c <= 0 then App {op= App {op= Xor; arg= x}; arg= y} + let ord = compare x y in + if ord <= 0 then App {op= App {op= Xor; arg= x}; arg= y} else App {op= App {op= Xor; arg= y}; arg= x} let simp_shl x y = diff --git a/sledge/src/llair/exp.mli b/sledge/src/llair/exp.mli index 406e2f5b1..91757ef1f 100644 --- a/sledge/src/llair/exp.mli +++ b/sledge/src/llair/exp.mli @@ -77,6 +77,8 @@ type exp = t include Comparator.S with type t := t val equal : t -> t -> bool +val sort : t -> t -> t * t +val sorted : t -> t -> bool val pp : t pp val invariant : ?partial:bool -> t -> unit diff --git a/sledge/src/llair/exp_test.ml b/sledge/src/llair/exp_test.ml index 7d1060ad4..e84c32fce 100644 --- a/sledge/src/llair/exp_test.ml +++ b/sledge/src/llair/exp_test.ml @@ -171,7 +171,7 @@ let%test_module _ = let%expect_test _ = pp (z = y) ; - [%expect {| (%z_2 = %y_1) |}] + [%expect {| (%y_1 = %z_2) |}] let%expect_test _ = pp (z = z) ; @@ -187,19 +187,19 @@ let%test_module _ = let%expect_test _ = pp (!3 * y = z = Exp.bool true) ; - [%expect {| (%z_2 = (3 × %y_1)) |}] + [%expect {| ((3 × %y_1) = %z_2) |}] let%expect_test _ = pp (Exp.bool true = (!3 * y = z)) ; - [%expect {| (%z_2 = (3 × %y_1)) |}] + [%expect {| ((3 × %y_1) = %z_2) |}] let%expect_test _ = pp (!3 * y = z = Exp.bool false) ; - [%expect {| (%z_2 ≠ (3 × %y_1)) |}] + [%expect {| ((3 × %y_1) ≠ %z_2) |}] let%expect_test _ = pp (Exp.bool false = (!3 * y = z)) ; - [%expect {| (%z_2 ≠ (3 × %y_1)) |}] + [%expect {| ((3 × %y_1) ≠ %z_2) |}] let%expect_test _ = pp (y - (!(-3) * y) + !4) ; @@ -211,15 +211,15 @@ let%test_module _ = let%expect_test _ = pp (y = (!(-3) * y) + !4) ; - [%expect {| (4 = (4 × %y_1)) |}] + [%expect {| ((4 × %y_1) = 4) |}] let%expect_test _ = pp ((!(-3) * y) + !4 = y) ; - [%expect {| (4 = (4 × %y_1)) |}] + [%expect {| ((4 × %y_1) = 4) |}] let%expect_test _ = pp (Exp.sub Typ.bool (Exp.bool true) (z = !4)) ; - [%expect {| ((4 = %z_2) + -1) |}] + [%expect {| ((%z_2 = 4) + -1) |}] let%expect_test _ = pp (Exp.add Typ.bool (Exp.bool true) (z = !4) = (z = !4)) ; @@ -227,23 +227,23 @@ let%test_module _ = let%expect_test _ = pp ((!13 * z) + !42 = (!3 * y) + (!13 * z)) ; - [%expect {| (42 = (3 × %y_1)) |}] + [%expect {| ((3 × %y_1) = 42) |}] let%expect_test _ = pp ((!13 * z) + !(-42) = (!3 * y) + (!13 * z)) ; - [%expect {| (42 = (-3 × %y_1)) |}] + [%expect {| ((-3 × %y_1) = 42) |}] let%expect_test _ = pp ((!13 * z) + !42 = (!(-3) * y) + (!13 * z)) ; - [%expect {| (42 = (-3 × %y_1)) |}] + [%expect {| ((-3 × %y_1) = 42) |}] let%expect_test _ = pp ((!10 * z) + !42 = (!(-3) * y) + (!13 * z)) ; - [%expect {| (42 = ((-3 × %y_1) + (3 × %z_2))) |}] + [%expect {| (((-3 × %y_1) + (3 × %z_2)) = 42) |}] let%expect_test _ = pp ~~((!13 * z) + !(-42) != (!3 * y) + (!13 * z)) ; - [%expect {| (42 = (-3 × %y_1)) |}] + [%expect {| ((-3 × %y_1) = 42) |}] let%expect_test _ = pp ~~(y > !2 && z <= !3) ; @@ -259,9 +259,9 @@ let%test_module _ = pp Exp.(dq (eq null z) (bool false)) ; [%expect {| - (null = %z_2) + (%z_2 = null) - (null = %z_2) + (%z_2 = null) - (null = %z_2) |}] + (%z_2 = null) |}] end )