diff --git a/lib/Checker.ml b/lib/Checker.ml index e9f76c2d..7fc98cbc 100644 --- a/lib/Checker.ml +++ b/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 _ -> diff --git a/lib/Constant.ml b/lib/Constant.ml index 09903db3..b1d30629 100644 --- a/lib/Constant.ml +++ b/lib/Constant.ml @@ -69,6 +69,12 @@ 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 @@ -76,6 +82,40 @@ let is_signed = function 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 diff --git a/lib/Simplify.ml b/lib/Simplify.ml index c8713dd7..3feeb62c 100644 --- a/lib/Simplify.ml +++ b/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) diff --git a/test/pulse/IntCmpFold.expected.c b/test/pulse/IntCmpFold.expected.c new file mode 100644 index 00000000..2b0563fa --- /dev/null +++ b/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); +} + diff --git a/test/pulse/IntCmpFold.fst b/test/pulse/IntCmpFold.fst new file mode 100644 index 00000000..6d4832a9 --- /dev/null +++ b/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)