From c7f4ed65ce9090df2e1d625ae876d9f1b33c9ed7 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Wed, 31 Oct 2018 11:16:19 -0700
Subject: [PATCH] [sledge] Remove Exp.Sub, express x - y as x + -1y

Reviewed By: mbouaziz

Differential Revision: D12854507

fbshipit-source-id: f87b95df4
---
 sledge/TODO.org          |  1 -
 sledge/src/llair/exp.ml  | 36 +++++++++++++++---------------------
 sledge/src/llair/exp.mli |  1 -
 3 files changed, 15 insertions(+), 23 deletions(-)

diff --git a/sledge/TODO.org b/sledge/TODO.org
index 4b77e1c78..a148bd6de 100644
--- a/sledge/TODO.org
+++ b/sledge/TODO.org
@@ -18,7 +18,6 @@ rather than nearest enclosing
 * llair
 ** NEXT normalize arithmetic exps to polynomials
 and sort terms
-** when Sub exps have types, simplify e - e to 0
 ** when Xor exps have types, simplify e xor e to 0
 ** ? remove src typ from Convert
 ** ? distribute addition over multiplication
diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml
index 9a153625b..4393193ab 100644
--- a/sledge/src/llair/exp.ml
+++ b/sledge/src/llair/exp.ml
@@ -15,6 +15,7 @@ module Z = struct
   let pp = Z.pp_print
   let zero = Z.zero
   let one = Z.one
+  let minus_one = Z.minus_one
   let to_int = Z.to_int
   let numbits = Z.numbits
   let fits_int = Z.fits_int
@@ -33,8 +34,6 @@ module Z = struct
   let clamp_cmp ~signed bits op x y =
     op (clamp ~signed bits x) (clamp ~signed bits y)
 
-  let neg ~bits z = Z.neg (clamp bits ~signed:true z)
-
   let clamp_bop ~signed bits op x y =
     clamp ~signed bits (op (clamp ~signed bits x) (clamp ~signed bits y))
 
@@ -92,7 +91,6 @@ module T0 = struct
     | Uno
     (* binary: arithmetic, numeric and pointer *)
     | Add
-    | Sub
     | Mul
     | Div
     | Udiv
@@ -181,7 +179,6 @@ module T = struct
       | Ord -> pf "ord"
       | Uno -> pf "uno"
       | Add -> pf "+"
-      | Sub -> pf "-"
       | Mul -> pf "*"
       | Div -> pf "/"
       | Udiv -> pf "udiv"
@@ -267,8 +264,8 @@ let invariant ?(partial = false) e =
       | [Integer {typ}] -> assert (Typ.equal src typ)
       | _ -> assert_arity 1 ) ;
       assert (Typ.convertible src dst)
-  | Eq | Dq | Gt | Ge | Lt | Le | Ugt | Uge | Ult | Ule | Add | Sub | Mul
-   |Div | Udiv | Rem | Urem | And | Or | Xor | Shl | Lshr | Ashr -> (
+  | Eq | Dq | Gt | Ge | Lt | Le | Ugt | Uge | Ult | Ule | Add | Mul | Div
+   |Udiv | Rem | Urem | And | Or | Xor | Shl | Lshr | Ashr -> (
     match args with
     | [Integer {typ= Integer {bits= m}}; Integer {typ= Integer {bits= n}}]
       ->
@@ -708,25 +705,15 @@ let rec simp_add x y =
         ; arg= Integer {data= i; typ= Integer {bits} as typ} }
     , Integer {data= j} ) ->
       simp_add arg (integer (Z.add ~bits i j) typ)
-  (* (i-e) + j ==> (i+j)-e *)
+  (* (i+e) + j ==> (i+j)+e *)
   | ( App
         { op=
-            App {op= Sub; arg= Integer {data= i; typ= Integer {bits} as typ}}
+            App {op= Add; arg= Integer {data= i; typ= Integer {bits} as typ}}
         ; arg }
     , Integer {data= j} ) ->
-      simp_sub (integer (Z.add ~bits i j) typ) arg
+      simp_add (integer (Z.add ~bits i j) typ) arg
   | _ -> App {op= App {op= Add; arg= x}; arg= y}
 
-and simp_sub x y =
-  match (x, y) with
-  (* i - j *)
-  | Integer {data= i; typ}, Integer {data= j; typ= Integer {bits}} ->
-      integer (Z.sub ~bits i j) typ
-  (* e - i ==> e + (-i) *)
-  | _, Integer {data; typ= Integer {bits} as typ} ->
-      simp_add x (integer (Z.neg ~bits data) typ)
-  | _ -> App {op= App {op= Sub; arg= x}; arg= y}
-
 let simp_mul x y =
   match (x, y) with
   (* i * j *)
@@ -737,6 +724,14 @@ let simp_mul x y =
   | e, Integer {data} when Z.equal Z.one data -> e
   | _ -> App {op= App {op= Mul; arg= x}; arg= y}
 
+let simp_sub typ x y =
+  match (x, y) with
+  (* i - j *)
+  | Integer {data= i; typ}, Integer {data= j; typ= Integer {bits}} ->
+      integer (Z.sub ~bits i j) typ
+  (* x - y ==> x + (-1 * y) *)
+  | _ -> simp_add x (simp_mul (integer Z.minus_one typ) y)
+
 let simp_div x y =
   match (x, y) with
   (* i / j *)
@@ -788,7 +783,6 @@ let app1 ?(partial = false) op arg =
   | App {op= Ord; arg= x}, y -> simp_ord x y
   | App {op= Uno; arg= x}, y -> simp_uno x y
   | App {op= Add; arg= x}, y -> simp_add x y
-  | App {op= Sub; arg= x}, y -> simp_sub x y
   | App {op= Mul; arg= x}, y -> simp_mul x y
   | App {op= Div; arg= x}, y -> simp_div x y
   | App {op= Udiv; arg= x}, y -> simp_udiv x y
@@ -824,8 +818,8 @@ let ule = app2 Ule
 let ord = app2 Ord
 let uno = app2 Uno
 let add typ = app2 Add
-let sub typ = app2 Sub
 let mul typ = app2 Mul
+let sub = simp_sub
 let div = app2 Div
 let udiv = app2 Udiv
 let rem = app2 Rem
diff --git a/sledge/src/llair/exp.mli b/sledge/src/llair/exp.mli
index 59c015046..2b971f6fe 100644
--- a/sledge/src/llair/exp.mli
+++ b/sledge/src/llair/exp.mli
@@ -50,7 +50,6 @@ type t = private
   | Ord  (** Ordered test (neither arg is nan) *)
   | Uno  (** Unordered test (some arg is nan) *)
   | Add  (** Addition *)
-  | Sub  (** Subtraction *)
   | Mul  (** Multiplication *)
   | Div  (** Division *)
   | Udiv  (** Unsigned division *)