[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

@@ -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)

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

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