[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

@@ -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} -> (

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