Simplify: fold comparisons between integers

This deserves a look to make sure we're not messing up wrt overflow,
promotion, etc. I think this is correct since 1) we keep the invariant
that integer constants are in bounds (see the asserts) and 2) we are only
folding comparisons where the width of the operator and the width of
both constants exactly match.

Author: mtzguido

lib/Simplify.ml

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