[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

@@ -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,6 +408,9 @@ let invariant ?(partial = false) e =
    |Urem | And | Or | Xor | Shl | Lshr | Ashr -> (
     match args with
     | [x; y] -> (
+        ( 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 )
@@ -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 =

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
 

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 )