From 752b8ab56a31b1acb0de78b763d170d2d8e7ea90 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Fri, 1 Nov 2019 09:56:07 -0700
Subject: [PATCH] [sledge] Fix normalization of Convert terms

Summary:
In some cases the result of an integer conversion needs to be
truncated by a bit.

Differential Revision: D18271179

fbshipit-source-id: e80740045
---
 sledge/src/llair/term.ml             | 16 ++++++++++++----
 sledge/src/llair/term_test.ml        | 28 ++++++++++++++++++++++++++++
 sledge/src/symbheap/equality_test.ml |  5 ++---
 3 files changed, 42 insertions(+), 7 deletions(-)

diff --git a/sledge/src/llair/term.ml b/sledge/src/llair/term.ml
index 9dcbad980..92937b699 100644
--- a/sledge/src/llair/term.ml
+++ b/sledge/src/llair/term.ml
@@ -506,10 +506,18 @@ let simp_extract ~unsigned bits arg =
   | _ -> Ap1 (Extract {unsigned; bits}, arg)
 
 let simp_convert ~unsigned dst src arg =
-  match (dst, src, arg) with
-  | Typ.Integer {bits= m; _}, Typ.Integer {bits= n; _}, Integer {data} ->
-      if (not unsigned) && m >= n then arg
-      else integer (Z.extract ~unsigned (min m n) data)
+  match (dst, src) with
+  | Typ.Integer {bits= m; _}, Typ.Integer {bits= n; _} -> (
+      if m < n then
+        match arg with
+        | Integer {data} -> integer (Z.extract m data)
+        | _ -> Ap1 (Convert {unsigned= false; dst; src}, arg)
+      else
+        match arg with
+        | Integer {data} -> integer (Z.extract ~unsigned n data)
+        | _ ->
+            if unsigned then Ap1 (Convert {unsigned; dst; src}, arg)
+            else arg )
   | _ ->
       if Typ.equivalent dst src then arg
       else Ap1 (Convert {unsigned; dst; src}, arg)
diff --git a/sledge/src/llair/term_test.ml b/sledge/src/llair/term_test.ml
index d79356dad..bb7eef0f4 100644
--- a/sledge/src/llair/term_test.ml
+++ b/sledge/src/llair/term_test.ml
@@ -41,6 +41,34 @@ let%test_module _ =
               (Exp.integer Typ.siz Z.one)))
           .term
 
+    let%expect_test _ =
+      pp
+        (Exp.convert ~dst:Typ.byt ~unsigned:true ~src:Typ.int
+           (Exp.integer Typ.int (Z.of_int 255)))
+          .term ;
+      [%expect {| -1 |}]
+
+    let%expect_test _ =
+      pp
+        (Exp.convert ~dst:Typ.byt ~unsigned:false ~src:Typ.int
+           (Exp.integer Typ.int (Z.of_int 255)))
+          .term ;
+      [%expect {| -1 |}]
+
+    let%expect_test _ =
+      pp
+        (Exp.convert ~dst:Typ.int ~unsigned:true ~src:Typ.byt
+           (Exp.integer Typ.byt (Z.of_int (-1))))
+          .term ;
+      [%expect {| 255 |}]
+
+    let%expect_test _ =
+      pp
+        (Exp.convert ~dst:Typ.int ~unsigned:false ~src:Typ.byt
+           (Exp.integer Typ.byt (Z.of_int (-1))))
+          .term ;
+      [%expect {| -1 |}]
+
     let%test "unsigned boolean overflow" =
       Term.is_true
         (Exp.uge
diff --git a/sledge/src/symbheap/equality_test.ml b/sledge/src/symbheap/equality_test.ml
index 8137f8a53..1a9e9480d 100644
--- a/sledge/src/symbheap/equality_test.ml
+++ b/sledge/src/symbheap/equality_test.ml
@@ -99,10 +99,9 @@ let%test_module _ =
       pp r2 ;
       [%expect
         {|
-          %x_5 = %y_6 = %z_7 = ((i64)(i32) %x_5)
+          %x_5 = %y_6 = %z_7
 
-          {sat= true;
-           rep= [[%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]; [((i64)(i32) %x_5) ↦ %x_5]]} |}]
+          {sat= true; rep= [[%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]]} |}]
 
     let%test _ = entails_eq r2 x z
     let%test _ = entails_eq (or_ r1 r2) x y