From 591d60e20a5feaa3bdcf1ad719cf41b4e5dfe37a Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Fri, 8 Mar 2019 07:07:10 -0800
Subject: [PATCH] [sledge] Prefer simple exps over applications as class reps

Reviewed By: jvillard

Differential Revision: D14344293

fbshipit-source-id: 2097959b5
---
 sledge/src/llair/exp.ml              |  7 +++---
 sledge/src/llair/exp.mli             |  4 ++--
 sledge/src/symbheap/equality_test.ml | 32 ++++++++++++++--------------
 3 files changed, 22 insertions(+), 21 deletions(-)

diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml
index fb49a8810..9b54747d3 100644
--- a/sledge/src/llair/exp.ml
+++ b/sledge/src/llair/exp.ml
@@ -57,7 +57,6 @@ module rec T : sig
   type qset = Qset.M(T).t [@@deriving compare, equal, hash, sexp]
 
   type t =
-    | App of {op: t; arg: t}
     (* nary: arithmetic, numeric and pointer *)
     | Add of {args: qset; typ: Typ.t}
     | Mul of {args: qset; typ: Typ.t}
@@ -69,6 +68,8 @@ module rec T : sig
     | Var of {id: int; name: string}
     | Nondet of {msg: string}
     | Label of {parent: string; name: string}
+    (* curried application *)
+    | App of {op: t; arg: t}
     (* numeric constants *)
     | Integer of {data: Z.t; typ: Typ.t}
     | Float of {data: string}
@@ -121,7 +122,6 @@ and T0 : sig
   type qset = Qset.M(T).t [@@deriving compare, equal, hash, sexp]
 
   type t =
-    | App of {op: t; arg: t}
     | Add of {args: qset; typ: Typ.t}
     | Mul of {args: qset; typ: Typ.t}
     | Splat of {byt: t; siz: t}
@@ -130,6 +130,7 @@ and T0 : sig
     | Var of {id: int; name: string}
     | Nondet of {msg: string}
     | Label of {parent: string; name: string}
+    | App of {op: t; arg: t}
     | Integer of {data: Z.t; typ: Typ.t}
     | Float of {data: string}
     | Eq
@@ -165,7 +166,6 @@ end = struct
   type qset = Qset.M(T).t [@@deriving compare, equal, hash, sexp]
 
   type t =
-    | App of {op: t; arg: t}
     | Add of {args: qset; typ: Typ.t}
     | Mul of {args: qset; typ: Typ.t}
     | Splat of {byt: t; siz: t}
@@ -174,6 +174,7 @@ end = struct
     | Var of {id: int; name: string}
     | Nondet of {msg: string}
     | Label of {parent: string; name: string}
+    | App of {op: t; arg: t}
     | Integer of {data: Z.t; typ: Typ.t}
     | Float of {data: string}
     | Eq
diff --git a/sledge/src/llair/exp.mli b/sledge/src/llair/exp.mli
index 2345f8c6f..6834ddeda 100644
--- a/sledge/src/llair/exp.mli
+++ b/sledge/src/llair/exp.mli
@@ -26,8 +26,6 @@ type comparator_witness
 type qset = (t, comparator_witness) Qset.t
 
 and t = private
-  | App of {op: t; arg: t}
-      (** Application of function symbol to argument, curried *)
   | Add of {args: qset; typ: Typ.t}  (** Addition *)
   | Mul of {args: qset; typ: Typ.t}  (** Multiplication *)
   | Splat of {byt: t; siz: t}
@@ -40,6 +38,8 @@ and t = private
           non-deterministic approximation of value described by [msg] *)
   | Label of {parent: string; name: string}
       (** Address of named code block within parent function *)
+  | App of {op: t; arg: t}
+      (** Application of function symbol to argument, curried *)
   | Integer of {data: Z.t; typ: Typ.t}
       (** Integer constant, or if [typ] is a [Pointer], null pointer value
           that never refers to an object *)
diff --git a/sledge/src/symbheap/equality_test.ml b/sledge/src/symbheap/equality_test.ml
index 0bfd4e19c..9ce11e30c 100644
--- a/sledge/src/symbheap/equality_test.ml
+++ b/sledge/src/symbheap/equality_test.ml
@@ -108,13 +108,13 @@ let%test_module _ =
       pp r2 ;
       [%expect
         {|
-          ((i64)(i8) %x_5) = %x_5 = %y_6 = %z_7
+          %x_5 = %y_6 = %z_7 = ((i64)(i8) %x_5)
 
           {sat= true;
-           rep= [[((i64)(i8) %x_5) ↦ ];
-                 [%x_5 ↦ ((i64)(i8) %x_5)];
-                 [%y_6 ↦ ((i64)(i8) %x_5)];
-                 [%z_7 ↦ ((i64)(i8) %x_5)];
+           rep= [[%x_5 ↦ ];
+                 [%y_6 ↦ %x_5];
+                 [%z_7 ↦ %x_5];
+                 [((i64)(i8) %x_5) ↦ %x_5];
                  [(i64)(i8) ↦ ]]} |}]
 
     let%test _ = entails_eq r2 x z
@@ -152,20 +152,20 @@ let%test_module _ =
       pp r3 ;
       [%expect
         {|
-      (%y_6 rem (%y_6 rem %z_7)) = (%y_6 rem %z_7) = %t_1 = %u_2 = %v_3
-      = %w_4 = %x_5 = %z_7
+      %t_1 = %u_2 = %v_3 = %w_4 = %x_5 = %z_7 = (%y_6 rem %v_3)
+      = (%y_6 rem %z_7)
 
       {sat= true;
-       rep= [[(%y_6 rem (%y_6 rem %z_7)) ↦ ];
-             [(%y_6 rem %z_7) ↦ (%y_6 rem (%y_6 rem %z_7))];
-             [(rem %y_6) ↦ ];
-             [%t_1 ↦ (%y_6 rem (%y_6 rem %z_7))];
-             [%u_2 ↦ (%y_6 rem (%y_6 rem %z_7))];
-             [%v_3 ↦ (%y_6 rem (%y_6 rem %z_7))];
-             [%w_4 ↦ (%y_6 rem (%y_6 rem %z_7))];
-             [%x_5 ↦ (%y_6 rem (%y_6 rem %z_7))];
+       rep= [[%t_1 ↦ ];
+             [%u_2 ↦ %t_1];
+             [%v_3 ↦ %t_1];
+             [%w_4 ↦ %t_1];
+             [%x_5 ↦ %t_1];
              [%y_6 ↦ ];
-             [%z_7 ↦ (%y_6 rem (%y_6 rem %z_7))];
+             [%z_7 ↦ %t_1];
+             [(%y_6 rem %v_3) ↦ %t_1];
+             [(%y_6 rem %z_7) ↦ %t_1];
+             [(rem %y_6) ↦ ];
              [rem ↦ ]]} |}]
 
     let%test _ = entails_eq r3 t z