Validate integer constants on input and when folding

Paranoid check.

Author: mtzguido

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