From 471d29626622e1f89e657bba806bff6ee9197d88 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Wed, 9 Oct 2019 02:56:23 -0700
Subject: [PATCH] [sledge] Fix check for range of representable integers

Summary:
Z.numbits ignores the sign, which allows 2^(N - 1) as representable
within N bits, while it is not. So check explicitly.

Reviewed By: bennostein

Differential Revision: D17665231

fbshipit-source-id: 0d3940517
---
 sledge/src/llair/exp.ml          | 5 ++++-
 sledge/src/symbheap/term_test.ml | 6 ++++--
 2 files changed, 8 insertions(+), 3 deletions(-)

diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml
index 36038c306..68ddd9eed 100644
--- a/sledge/src/llair/exp.ml
+++ b/sledge/src/llair/exp.ml
@@ -191,7 +191,10 @@ let rec invariant exp =
   | Reg {typ} | Nondet {typ} -> assert (Typ.is_sized typ)
   | Integer {data; typ} -> (
     match typ with
-    | Integer {bits} -> assert (Z.numbits data <= bits)
+    | Integer {bits} ->
+        (* data in −(2^(bits − 1)) to 2^(bits − 1) − 1 *)
+        let n = Z.shift_left Z.one (bits - 1) in
+        assert (Z.(Compare.(neg n <= data && data < n)))
     | Pointer _ -> assert (Z.equal Z.zero data)
     | _ -> assert false )
   | Float {typ} -> (
diff --git a/sledge/src/symbheap/term_test.ml b/sledge/src/symbheap/term_test.ml
index c1616931b..893864cd3 100644
--- a/sledge/src/symbheap/term_test.ml
+++ b/sledge/src/symbheap/term_test.ml
@@ -47,14 +47,16 @@ let%test_module _ =
         (Term.of_exp
            (Exp.eq Typ.bool
               (Exp.integer Typ.bool Z.minus_one)
-              (Exp.integer Typ.bool Z.one)))
+              (Exp.convert ~dst:Typ.bool ~src:Typ.siz
+                 (Exp.integer Typ.siz Z.one))))
 
     let%test "unsigned boolean overflow" =
       Term.is_true
         (Term.of_exp
            (Exp.uge Typ.bool
               (Exp.integer Typ.bool Z.minus_one)
-              (Exp.integer Typ.bool Z.one)))
+              (Exp.convert ~dst:Typ.bool ~src:Typ.siz
+                 (Exp.integer Typ.siz Z.one))))
 
     let%expect_test _ =
       pp (!42 + !13) ;