Normalize out-of-range integer literal casts

src/pass/emit.rs

@@ -29,6 +29,63 @@ fn normalize_unsigned(val: &BigInt, width: u32) -> BigInt {
     ((val % &modulus) + &modulus) % &modulus
 }
 
+/// Normalize an integer literal to PAL's two's-complement signed cast model.
+fn normalize_signed(val: &BigInt, width: u32) -> BigInt {
+    let modulus = BigInt::from(1u32) << width;
+    let sign_bit = BigInt::from(1u32) << (width - 1);
+    let unsigned = normalize_unsigned(val, width);
+    if unsigned >= sign_bit {
+        unsigned - modulus
+    } else {
+        unsigned
+    }
+}
+
+fn integer_fits(val: &BigInt, signed: bool, width: u32) -> bool {
+    if signed {
+        let upper_exclusive = BigInt::from(1u32) << (width - 1);
+        let lower_inclusive = -upper_exclusive.clone();
+        val >= &lower_inclusive && val < &upper_exclusive
+    } else {
+        val >= &BigInt::ZERO && val < &(BigInt::from(1u32) << width)
+    }
+}
+
+fn machine_int_suffix(signed: bool, width: u32) -> Option<&'static str> {
+    match (signed, width) {
+        (true, 8) => Some("y"),
+        (false, 8) => Some("uy"),
+        (true, 16) => Some("s"),
+        (false, 16) => Some("us"),
+        (true, 32) => Some("l"),
+        (false, 32) => Some("ul"),
+        (true, 64) => Some("L"),
+        (false, 64) => Some("UL"),
+        _ => None,
+    }
+}
+
+fn emit_machine_int_literal(val: &BigInt, signed: bool, width: u32) -> Doc {
+    let normalized = if signed {
+        normalize_signed(val, width)
+    } else {
+        normalize_unsigned(val, width)
+    };
+
+    let Some(suffix) = machine_int_suffix(signed, width) else {
+        let module = if signed { "Int" } else { "UInt" };
+        let conversion = if signed { "int_to_t" } else { "uint_to_t" };
+        return Doc::text(format!("({module}{width}.{conversion} {normalized})"));
+    };
+
+    let literal = format!("{normalized}{suffix}");
+    if signed && normalized < BigInt::ZERO {
+        parens(Doc::text(literal))
+    } else {
+        Doc::text(literal)
+    }
+}
+
 /// Determines the output module name for a given top-level declaration.
 pub fn module_name_for_decl(decl: &Decl) -> String {
     match &decl.val {
@@ -2060,33 +2117,9 @@ impl<'a> Emitter<'a> {
                 ExprT::IntLit(val, ty) => {
                     let resolved = env.vtype_whnf(ty.clone().into());
                     match resolved.val {
-                        TypeT::Int {
-                            signed: true,
-                            width: 32,
-                        } => Doc::text(format!("{}l", val)),
-                        TypeT::Int {
-                            signed: false,
-                            width: 32,
-                        } => {
-                            // clang hands us the signed interpretation of the
-                            // bit pattern (see toBigInt in cpp/impl.cpp), so a
-                            // u32 literal with the high bit set arrives as a
-                            // negative BigInt (e.g. 0xFFFFFFFF as -1). F*'s `ul`
-                            // literals must lie in [0, 2^32), so normalize first.
-                            Doc::text(format!("{}ul", normalize_unsigned(val, 32)))
+                        TypeT::Int { signed, width } => {
+                            emit_machine_int_literal(val, signed, width)
                         }
-                        TypeT::Int {
-                            signed: true,
-                            width,
-                        } => Doc::text(format!("(Int{}.int_to_t {})", width, val)),
-                        TypeT::Int {
-                            signed: false,
-                            width,
-                        } => Doc::text(format!(
-                            "(UInt{}.uint_to_t {})",
-                            width,
-                            normalize_unsigned(val, width)
-                        )),
                         TypeT::SizeT => Doc::text(format!("{}sz", val)),
                         TypeT::SpecInt | TypeT::SpecNat => Doc::text(format!("{}", val)),
                         TypeT::Pointer(_, PointerKind::Ref | PointerKind::Unknown)
@@ -2157,6 +2190,22 @@ impl<'a> Emitter<'a> {
                         // Same underlying type, no cast necessary.
                         return val_doc;
                     }
+
+                    if let (ExprT::IntLit(val, literal_ty), TypeT::Int { signed, width }) =
+                        (&val.val, &to_ty.val)
+                    {
+                        let literal_value = match env.vtype_whnf(literal_ty.clone().into()).val {
+                            TypeT::Int {
+                                signed: false,
+                                width,
+                            } => normalize_unsigned(val, width),
+                            _ => val.as_ref().clone(),
+                        };
+                        if !integer_fits(&literal_value, *signed, *width) {
+                            return emit_machine_int_literal(&literal_value, *signed, *width);
+                        }
+                    }
+
                     let default_msg = format!("unsupported cast from {} to {}", from_ty, to_ty);
                     match (&from_ty.val, &to_ty.val) {
                         (TypeT::Bool, TypeT::Int { signed, width }) => {

test/integer_literal_casts/Makefile

@@ -0,0 +1 @@
+../_templates/Makefile

test/integer_literal_casts/fstar.fst.config.json

@@ -0,0 +1 @@
+../_templates/fstar.fst.config.json

test/integer_literal_casts/integer_literal_casts.c

@@ -0,0 +1,82 @@
+#include "pal.h"
+#include <stdint.h>
+
+int8_t cast_literal_to_int8(void)
+    _ensures(return == -1)
+{
+    return (int8_t)255;
+}
+
+uint8_t cast_literal_to_uint8(void)
+    _ensures(return == UINT8_MAX)
+{
+    return (uint8_t)511;
+}
+
+int16_t cast_literal_to_int16(void)
+    _ensures(return == -1)
+{
+    return (int16_t)65535;
+}
+
+uint16_t cast_literal_to_uint16(void)
+    _ensures(return == UINT16_MAX)
+{
+    return (uint16_t)131071;
+}
+
+#define GENERATED_CODE_FIRST ((int32_t)0x80010001L)
+#define GENERATED_CODE_SECOND ((int32_t)0x80010002L)
+#define GENERATED_CODE_LIST \
+    X(GENERATED_CODE_FIRST) \
+    X(GENERATED_CODE_SECOND)
+
+uint8_t is_direct_code(int32_t code)
+{
+    switch (code)
+    {
+    case (int32_t)0x80010001L:
+    case (int32_t)0x80010002L:
+        return 1;
+    default:
+        return 0;
+    }
+}
+
+uint8_t is_generated_code(int32_t code)
+{
+    switch (code)
+    {
+#define X(CODE) \
+    case CODE:
+        GENERATED_CODE_LIST
+#undef X
+        return 1;
+    default:
+        return 0;
+    }
+}
+
+uint32_t cast_literal_to_uint32(void)
+    _ensures(return == 1)
+{
+    return (uint32_t)4294967297ULL;
+}
+
+int64_t cast_literal_to_int64(void)
+    _ensures(return == -1)
+{
+    return (int64_t)UINT64_MAX;
+}
+
+uint64_t uint64_max_literal(void)
+    _ensures(return == UINT64_MAX)
+{
+    return UINT64_MAX;
+}
+
+uint64_t preserve_representable_uint64_cast(void)
+    _ensures(return == INT64_MAX)
+{
+    return (uint64_t)INT64_MAX;
+}

test/integer_literal_casts/pal.config.json

@@ -0,0 +1 @@
+../_templates/pal.config.json

test/integer_literal_casts/pal.h

@@ -0,0 +1 @@
+../pal.h