Simplify: fold comparisons between integers

lib/Checker.ml

@@ -646,7 +646,11 @@ and infer' env e =
   | EQualified lid ->
       lookup_global env lid
 
-  | EConstant (w, _) ->
+  | EConstant ((w, s) as k) ->
+      (* Validate integers to make sure we are not accepting constants
+         like "-1" as unsigned. *)
+      if not (is_float w) && not (is_valid_int k) then
+        checker_error env "constant %s is not a valid %a" s ptyp (TInt w);
       TInt w
 
   | EStandaloneComment _ ->

lib/Constant.ml

@@ -69,13 +69,53 @@ let unsigned_of_signed = function
   | CInt | UInt8 | UInt16 | UInt32 | UInt64 | SizeT
   | Float32 | Float64 -> raise (Invalid_argument "unsigned_of_signed")
 
+let is_int = function
+  | UInt8 | UInt16 | UInt32 | UInt64
+  | Int8 | Int16 | Int32 | Int64
+  | SizeT -> true
+  | _ -> false
+
 let is_signed = function
   | Int8 | Int16 | Int32 | Int64 | CInt | PtrdiffT -> true
   | UInt8 | UInt16 | UInt32 | UInt64 | SizeT -> false
   | Float32 | Float64 -> raise (Invalid_argument "is_signed: float")
 
 let is_unsigned w = not (is_signed w)
 
+(* The range of the values representable at a given width, when known. *)
+let bounds_of_width (w: width) : (Z.t * Z.t) option =
+  let two = Z.of_int 2 in
+  let unsigned bits = Some (Z.zero, Z.pred (Z.pow two bits)) in
+  let signed bits =
+    Some (Z.neg (Z.pow two (bits - 1)), Z.pred (Z.pow two (bits - 1)))
+  in
+  match w with
+  | UInt8  -> unsigned 8
+  | UInt16 -> unsigned 16
+  | UInt32 -> unsigned 32
+  | UInt64 -> unsigned 64
+  (* size_t is platform-dependent (at least 16 bits, at most 64 in practice),
+     we use the loosest bound *)
+  | SizeT -> unsigned 64
+  | Int8  -> signed 8
+  | Int16 -> signed 16
+  | Int32 -> signed 32
+  | Int64 -> signed 64
+  | CInt | PtrdiffT -> None
+  | Float32 | Float64 -> None
+
+(* Whether this is a well-formed integer constant. *)
+let is_valid_int ((w, s): t) : bool =
+  if is_float w then
+    false
+  else
+    match Z.of_string s with
+    | exception Invalid_argument _ -> false
+    | z ->
+        match bounds_of_width w with
+        | None -> true
+        | Some (lo, hi) -> Z.leq lo z && Z.leq z hi
+
 let without_wrap = function
   | AddW -> Add
   | SubW -> Sub

lib/Simplify.ml

@@ -466,14 +466,10 @@ let constant_fold = object (self)
     | EOp (K.Add, TInt w), [ e1; e2 ] -> (
         let e1 = self#visit_expr env e1 in
         let e2 = self#visit_expr env e2 in
-        let is_int w =
-          match w with
-          | K.UInt8 | K.UInt16 | K.UInt32 | K.UInt64 | K.Int8 | K.Int16 | K.Int32 | K.Int64 | K.SizeT -> true
-          | _ -> false
-        in
         match e1.node, e2.node with
         (* Sum literals *)
-        | EConstant (w1, s1), EConstant (w2, s2) when is_int w && w = w1 && w1 = w2 ->
+        | EConstant (w1, s1), EConstant (w2, s2) when K.is_int w && w = w1 && w1 = w2 ->
+          assert (K.is_valid_int (w1, s1) && K.is_valid_int (w2, s2));
           EConstant (w1, op_on_strings Z.add w s1 s2)
         (* 0+x, x+0 ~> x *)
         | EConstant (w1, "0"), e2 when w = w1 -> e2
@@ -487,6 +483,7 @@ let constant_fold = object (self)
         match e1.node, e2.node with
         (* Multiply literals *)
         | EConstant (w1, s1), EConstant (w2, s2) when w = w1 && w1 = w2 ->
+          assert (K.is_valid_int (w1, s1) && K.is_valid_int (w2, s2));
           EConstant (w1, op_on_strings Z.mul w s1 s2)
         (* 0*x, x*0 ~> 0 *)
         | EConstant (w1, "0"), _ when w = w1 && is_readonly_c_expression e2 -> EConstant(w1, "0");
@@ -503,6 +500,7 @@ let constant_fold = object (self)
         match e1.node, e2.node with
         (* Division of literals. Note, ZArith div/rem coincides with C semantics. *)
         | EConstant (w1, s1), EConstant (w2, s2) when w = w1 && w1 = w2 ->
+          assert (K.is_valid_int (w1, s1) && K.is_valid_int (w2, s2));
           EConstant (w1, op_on_strings Z.div w s1 s2)
         (* 0/x ~> 0 *)
         | EConstant (w2, "0"), _ when w = w2 && is_readonly_c_expression e2 -> EConstant(w2, "0")
@@ -517,6 +515,7 @@ let constant_fold = object (self)
         match e1.node, e2.node with
         (* Mod of literals. Note, ZArith div/rem coincides with C semantics. *)
         | EConstant (w1, s1), EConstant (w2, s2) when w = w1 && w1 = w2 ->
+          assert (K.is_valid_int (w1, s1) && K.is_valid_int (w2, s2));
           EConstant (w1, op_on_strings Z.rem w s1 s2)
         (* 0 % x ~> 0 *)
         | EConstant (w2, "0"), _ when w = w2 && is_readonly_c_expression e2 -> EConstant(w2, "0")
@@ -554,6 +553,24 @@ let constant_fold = object (self)
         | _ -> EApp (e, [e1])
     )
 
+    | EOp ((K.Eq | K.Neq | K.Lt | K.Lte | K.Gt | K.Gte) as cmp, TInt w), [ e1; e2 ] -> (
+        let e1 = self#visit_expr env e1 in
+        let e2 = self#visit_expr env e2 in
+        match e1.node, e2.node with
+        | EConstant (w1, s1), EConstant (w2, s2) when K.is_int w && w = w1 && w1 = w2 ->
+          assert (K.is_valid_int (w1, s1) && K.is_valid_int (w2, s2));
+          let c = Z.compare (Z.of_string s1) (Z.of_string s2) in
+          EBool (match cmp with
+            | K.Eq -> c = 0
+            | K.Neq -> c <> 0
+            | K.Lt -> c < 0
+            | K.Lte -> c <= 0
+            | K.Gt -> c > 0
+            | K.Gte -> c >= 0
+            | _ -> assert false)
+        | _ -> EApp (e, [ e1; e2 ])
+    )
+
     | _ ->
         EApp (self#visit_expr env e, List.map (self#visit_expr env) es)
 

test/pulse/IntCmpFold.expected.c

@@ -0,0 +1,96 @@
+/* krml header omitted for test repeatability */
+
+
+#include "IntCmpFold.h"
+
+void IntCmpFold_main(void)
+{
+  IntCmpFold_f(false);
+  IntCmpFold_f(true);
+  IntCmpFold_f(true);
+  IntCmpFold_f(false);
+  IntCmpFold_f(false);
+  IntCmpFold_f(true);
+  IntCmpFold_f(true);
+  IntCmpFold_f(false);
+  IntCmpFold_f(true);
+}
+
+void IntCmpFold_main_signed(void)
+{
+  IntCmpFold_f(false);
+  IntCmpFold_f(true);
+  IntCmpFold_f(true);
+  IntCmpFold_f(false);
+  IntCmpFold_f(false);
+  IntCmpFold_f(true);
+  IntCmpFold_f(true);
+  IntCmpFold_f(false);
+  IntCmpFold_f(true);
+}
+
+void IntCmpFold_main_uint8(void)
+{
+  IntCmpFold_f(true);
+  IntCmpFold_f(false);
+}
+
+void IntCmpFold_main_int8(void)
+{
+  IntCmpFold_f(true);
+  IntCmpFold_f(false);
+}
+
+void IntCmpFold_main_uint16(void)
+{
+  IntCmpFold_f(true);
+  IntCmpFold_f(false);
+}
+
+void IntCmpFold_main_int16(void)
+{
+  IntCmpFold_f(true);
+  IntCmpFold_f(false);
+}
+
+void IntCmpFold_main_uint64(void)
+{
+  IntCmpFold_f(true);
+  IntCmpFold_f(false);
+}
+
+void IntCmpFold_main_int64(void)
+{
+  IntCmpFold_f(true);
+  IntCmpFold_f(false);
+}
+
+void IntCmpFold_main_sizet(void)
+{
+  IntCmpFold_f(true);
+  IntCmpFold_f(false);
+}
+
+void IntCmpFold_main_var(uint32_t z)
+{
+  IntCmpFold_f(1U == z);
+  IntCmpFold_f(z < 1U);
+}
+
+void IntCmpFold_main_var_signed(int32_t z)
+{
+  IntCmpFold_f(-1 == z);
+  IntCmpFold_f(z < -1);
+}
+
+void IntCmpFold_main_var_narrow(uint8_t z)
+{
+  IntCmpFold_f(255U == z);
+  IntCmpFold_f(z < 255U);
+}
+
+void IntCmpFold_cast_prevents_fold(void)
+{
+  IntCmpFold_f((uint16_t)1U < 2U);
+}
+

test/pulse/IntCmpFold.fst

@@ -0,0 +1,123 @@
+module IntCmpFold
+
+assume
+val f : bool -> Dv unit
+
+let main () =
+  let open FStar.UInt32 in
+  [@@CInline] let x = 1ul in
+  [@@CInline] let y = 2ul in
+  f (x = y);
+  f (x < y);
+  f (x <= y);
+  f (x > y);
+  f (x >= y);
+  f (x <> y);
+  f (x = x);
+  f (x < x);
+  f (x <= x);
+  ()
+
+(* Same, but signed, and with a negative constant: the comparisons must be
+   folded according to the *signed* order. *)
+let main_signed () =
+  let open FStar.Int32 in
+  [@@CInline] let x = (-1l) in
+  [@@CInline] let y = 1l in
+  f (x = y);
+  f (x < y);
+  f (x <= y);
+  f (x > y);
+  f (x >= y);
+  f (x <> y);
+  f (x = x);
+  f (x < x);
+  f (x <= x);
+  ()
+
+(* The extremal values of every width. The [@@CInline] lets are what keeps F*
+   from doing the folding itself, before krml even sees the comparison. *)
+let main_uint8 () =
+  let open FStar.UInt8 in
+  [@@CInline] let x = 0uy in
+  [@@CInline] let y = 255uy in
+  f (x < y);
+  f (y < x);
+  ()
+
+let main_int8 () =
+  let open FStar.Int8 in
+  [@@CInline] let x = (-128y) in
+  [@@CInline] let y = 127y in
+  f (x < y);
+  f (y < x);
+  ()
+
+let main_uint16 () =
+  let open FStar.UInt16 in
+  [@@CInline] let x = 0us in
+  [@@CInline] let y = 65535us in
+  f (x < y);
+  f (y < x);
+  ()
+
+let main_int16 () =
+  let open FStar.Int16 in
+  [@@CInline] let x = (-32768s) in
+  [@@CInline] let y = 32767s in
+  f (x < y);
+  f (y < x);
+  ()
+
+let main_uint64 () =
+  let open FStar.UInt64 in
+  [@@CInline] let x = 0uL in
+  [@@CInline] let y = 18446744073709551615uL in
+  f (x < y);
+  f (y < x);
+  ()
+
+(* Note: reading these two as unsigned would flip both answers. *)
+let main_int64 () =
+  let open FStar.Int64 in
+  [@@CInline] let x = (-9223372036854775808L) in
+  [@@CInline] let y = 9223372036854775807L in
+  f (x < y);
+  f (y < x);
+  ()
+
+let main_sizet () =
+  let open FStar.SizeT in
+  [@@CInline] let x = 1sz in
+  f (x = x);
+  f (x < x);
+  ()
+
+(* Nothing to fold here: only one side is a constant. *)
+let main_var (z : UInt32.t) =
+  let open FStar.UInt32 in
+  [@@CInline] let x = 1ul in
+  f (x = z);
+  f (z < x);
+  ()
+
+(* Idem, at a signed type and with a negative constant. *)
+let main_var_signed (z : Int32.t) =
+  let open FStar.Int32 in
+  [@@CInline] let x = (-1l) in
+  f (x = z);
+  f (z < x);
+  ()
+
+(* Idem, at a narrow width, where C would promote both operands to int. *)
+let main_var_narrow (z : UInt8.t) =
+  let open FStar.UInt8 in
+  [@@CInline] let x = 255uy in
+  f (x = z);
+  f (z < x);
+  ()
+
+let cast_prevents_fold () =
+  [@@CInline] let x = 1uy in
+  [@@CInline] let y = 2us in
+  f (FStar.Int.Cast.uint8_to_uint16 x `FStar.UInt16.lt` y)