diff --git a/src/pass/emit.rs b/src/pass/emit.rs index 2ffa211e..72f04807 100644 --- a/src/pass/emit.rs +++ b/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 }) => { diff --git a/test/integer_literal_casts/Makefile b/test/integer_literal_casts/Makefile new file mode 120000 index 00000000..3febeb16 --- /dev/null +++ b/test/integer_literal_casts/Makefile @@ -0,0 +1 @@ +../_templates/Makefile \ No newline at end of file diff --git a/test/integer_literal_casts/fstar.fst.config.json b/test/integer_literal_casts/fstar.fst.config.json new file mode 120000 index 00000000..4100b019 --- /dev/null +++ b/test/integer_literal_casts/fstar.fst.config.json @@ -0,0 +1 @@ +../_templates/fstar.fst.config.json \ No newline at end of file diff --git a/test/integer_literal_casts/integer_literal_casts.c b/test/integer_literal_casts/integer_literal_casts.c new file mode 100644 index 00000000..344c464a --- /dev/null +++ b/test/integer_literal_casts/integer_literal_casts.c @@ -0,0 +1,82 @@ +#include "pal.h" +#include + +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; +} diff --git a/test/integer_literal_casts/pal.config.json b/test/integer_literal_casts/pal.config.json new file mode 120000 index 00000000..d59f1cfa --- /dev/null +++ b/test/integer_literal_casts/pal.config.json @@ -0,0 +1 @@ +../_templates/pal.config.json \ No newline at end of file diff --git a/test/integer_literal_casts/pal.h b/test/integer_literal_casts/pal.h new file mode 120000 index 00000000..05ef83f9 --- /dev/null +++ b/test/integer_literal_casts/pal.h @@ -0,0 +1 @@ +../pal.h \ No newline at end of file