From 036d0d37ce3aac2a5d0554d7f978a236751c48dd Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 3 May 2024 16:06:33 +0200 Subject: [PATCH] Fix handling of shifts --- charon/src/transform/remove_dynamic_checks.rs | 21 ++- charon/tests/ui/remove-dynamic-checks.out | 140 +++++++++++++++++- charon/tests/ui/remove-dynamic-checks.rs | 28 +++- .../ui/unsupported/foreign-constant-aux.rs | 2 + .../tests/ui/unsupported/foreign-constant.out | 11 ++ .../tests/ui/unsupported/foreign-constant.rs | 4 + 6 files changed, 187 insertions(+), 19 deletions(-) create mode 100644 charon/tests/ui/unsupported/foreign-constant-aux.rs create mode 100644 charon/tests/ui/unsupported/foreign-constant.out create mode 100644 charon/tests/ui/unsupported/foreign-constant.rs diff --git a/charon/src/transform/remove_dynamic_checks.rs b/charon/src/transform/remove_dynamic_checks.rs index 35a4086b3..79e1289b6 100644 --- a/charon/src/transform/remove_dynamic_checks.rs +++ b/charon/src/transform/remove_dynamic_checks.rs @@ -70,9 +70,9 @@ fn remove_dynamic_checks(ctx: &mut TransCtx, block: &mut BlockData) { rest } - // Overflow checks for left shift. They look like: + // Overflow checks for right/left shift. They can look like: // x := ...; - // b := copy x < const 32; // or another constant + // b := move x < const 32; // or another constant // assert(move b == true); [rest @ .., Statement { content: RawStatement::Assign(x, _), @@ -81,10 +81,21 @@ fn remove_dynamic_checks(ctx: &mut TransCtx, block: &mut BlockData) { content: RawStatement::Assign( has_overflow, - Rvalue::BinaryOp(BinOp::Lt, Operand::Copy(lt_op2), Operand::Const(..)), + Rvalue::BinaryOp(BinOp::Lt, Operand::Move(lt_op2), Operand::Const(..)), ), .. }] if lt_op2 == x && cond == has_overflow && *expected == true => rest, + // They can also look like: + // b := const c < const 32; // or another constant + // assert(move b == true); + [rest @ .., Statement { + content: + RawStatement::Assign( + has_overflow, + Rvalue::BinaryOp(BinOp::Lt, Operand::Const(..), Operand::Const(..)), + ), + .. + }] if cond == has_overflow && *expected == true => rest, // Overflow checks for addition/subtraction/multiplication. They look like: // r := x checked.+ y; @@ -109,10 +120,12 @@ fn remove_dynamic_checks(ctx: &mut TransCtx, block: &mut BlockData) { // This can happen for the dynamic checks we don't handle, corresponding to the // `rustc_middle::mir::AssertKind` variants `ResumedAfterReturn`, `ResumedAfterPanic` // and `MisalignedPointerDereference`. + let fmt_ctx = ctx.into_fmt(); + let msg = format!("Found an `assert` we don't recognize:\n{}", block.fmt_with_ctx("", &fmt_ctx)); register_error_or_panic!( ctx, block.terminator.meta.span, - format!("Found an `assert` we don't recognize: {block:?}") + msg ); return } diff --git a/charon/tests/ui/remove-dynamic-checks.out b/charon/tests/ui/remove-dynamic-checks.out index 8859c2aab..babd9b942 100644 --- a/charon/tests/ui/remove-dynamic-checks.out +++ b/charon/tests/ui/remove-dynamic-checks.out @@ -371,26 +371,150 @@ fn test_crate::shr(@1: u32, @2: u32) -> u32 return } -global test_crate::CONST0 { - let @0: usize; // return - let @1: (usize, bool); // anonymous local +global test_crate::_ { + let @0: isize; // return + let @1: (isize, bool); // anonymous local - @1 := const (1 : usize) checked.+ const (1 : usize) + @1 := const (1 : isize) checked.+ const (1 : isize) assert(move ((@1).1) == false) @0 := move ((@1).0) return } -global test_crate::CONST1 { - let @0: usize; // return - let @1: (usize, bool); // anonymous local +global test_crate::_#1 { + let @0: isize; // return + let @1: (isize, bool); // anonymous local - @1 := const (2 : usize) checked.* const (2 : usize) + @1 := const (1 : isize) checked.- const (1 : isize) assert(move ((@1).1) == false) @0 := move ((@1).0) return } +global test_crate::_#2 { + let @0: isize; // return + + @0 := const (-1 : isize) + return +} + +global test_crate::_#3 { + let @0: isize; // return + let @1: (isize, bool); // anonymous local + + @1 := const (2 : isize) checked.* const (2 : isize) + assert(move ((@1).1) == false) + @0 := move ((@1).0) + return +} + +global test_crate::_#4 { + let @0: isize; // return + + @0 := const (2 : isize) >> const (2 : i32) + return +} + +global test_crate::_#5 { + let @0: isize; // return + + @0 := const (2 : isize) << const (2 : i32) + return +} + +global test_crate::_#6 { + let @0: isize; // return + + @0 := const (2 : isize) % const (2 : isize) + return +} + +global test_crate::_#7 { + let @0: isize; // return + + @0 := const (2 : isize) / const (2 : isize) + return +} + +global test_crate::FOO { + let @0: u32; // return + + @0 := const (10 : u32) + return +} + +global test_crate::_#8 { + let @0: u32; // return + let @1: (u32, bool); // anonymous local + let @2: u32; // anonymous local + + @2 := test_crate::FOO + @1 := const (1 : u32) checked.+ move (@2) + assert(move ((@1).1) == false) + @0 := move ((@1).0) + return +} + +global test_crate::_#9 { + let @0: u32; // return + let @1: (u32, bool); // anonymous local + let @2: u32; // anonymous local + + @2 := test_crate::FOO + @1 := const (1 : u32) checked.- move (@2) + assert(move ((@1).1) == false) + @0 := move ((@1).0) + return +} + +global test_crate::_#10 { + let @0: u32; // return + let @1: (u32, bool); // anonymous local + let @2: u32; // anonymous local + + @2 := test_crate::FOO + @1 := const (2 : u32) checked.* move (@2) + assert(move ((@1).1) == false) + @0 := move ((@1).0) + return +} + +global test_crate::_#11 { + let @0: u32; // return + let @1: u32; // anonymous local + + @1 := test_crate::FOO + @0 := const (2 : u32) >> move (@1) + return +} + +global test_crate::_#12 { + let @0: u32; // return + let @1: u32; // anonymous local + + @1 := test_crate::FOO + @0 := const (2 : u32) << move (@1) + return +} + +global test_crate::_#13 { + let @0: u32; // return + let @1: u32; // anonymous local + + @1 := test_crate::FOO + @0 := const (2 : u32) % move (@1) + return +} + +global test_crate::_#14 { + let @0: u32; // return + let @1: u32; // anonymous local + + @1 := test_crate::FOO + @0 := const (2 : u32) / move (@1) + return +} + global test_crate::div_signed_with_constant::FOO { let @0: i32; // return diff --git a/charon/tests/ui/remove-dynamic-checks.rs b/charon/tests/ui/remove-dynamic-checks.rs index 431cb0393..5ae953cfb 100644 --- a/charon/tests/ui/remove-dynamic-checks.rs +++ b/charon/tests/ui/remove-dynamic-checks.rs @@ -86,13 +86,27 @@ fn shr(x: u32, y: u32) -> u32 { x >> y } -/* Checking the simplification of binop operations *inside* global constants. - - In release mode, the Rust compiler inserts additional checks inside constant - bodies. -*/ -pub const CONST0: usize = 1 + 1; -pub const CONST1: usize = 2 * 2; +// Checking the simplification of binop operations *inside* global constants. +// Even in release mode, rustc inserts additional checks inside constant bodies. +pub const _: isize = 1 + 1; +pub const _: isize = 1 - 1; +pub const _: isize = -1; +pub const _: isize = 2 * 2; +pub const _: isize = 2 >> 2; +pub const _: isize = 2 << 2; +pub const _: isize = 2 % 2; +pub const _: isize = 2 / 2; + +// When the operand is a bare const it sometimes gets inlined, which trips up our simplification +// pass. I used `u32` here because other types use a `cast` and thus aren't inlined. +pub const FOO: u32 = 10; +pub const _: u32 = 1 + FOO; +pub const _: u32 = 1 - FOO; +pub const _: u32 = 2 * FOO; +pub const _: u32 = 2 >> FOO; +pub const _: u32 = 2 << FOO; +pub const _: u32 = 2 % FOO; +pub const _: u32 = 2 / FOO; fn div_signed_with_constant() -> i32 { const FOO: i32 = 42; diff --git a/charon/tests/ui/unsupported/foreign-constant-aux.rs b/charon/tests/ui/unsupported/foreign-constant-aux.rs new file mode 100644 index 000000000..cc81d65ec --- /dev/null +++ b/charon/tests/ui/unsupported/foreign-constant-aux.rs @@ -0,0 +1,2 @@ +//@ skip +pub const CONSTANT: u8 = 16; diff --git a/charon/tests/ui/unsupported/foreign-constant.out b/charon/tests/ui/unsupported/foreign-constant.out new file mode 100644 index 000000000..a8db4b184 --- /dev/null +++ b/charon/tests/ui/unsupported/foreign-constant.out @@ -0,0 +1,11 @@ +thread 'rustc' panicked at 'foreign_constant_aux does not have a "explicit_predicates_of"', compiler/rustc_metadata/src/rmeta/decoder/cstore_impl.rs:205:1 +note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace +error: Thread panicked when extracting body. + --> tests/ui/unsupported/foreign-constant.rs:4:1 + | +4 | const _: i32 = 1 << CONSTANT; + | ^^^^^^^^^^^^ + +error: aborting due to previous error + +[ ERROR charon_driver:200] The extraction encountered 1 errors diff --git a/charon/tests/ui/unsupported/foreign-constant.rs b/charon/tests/ui/unsupported/foreign-constant.rs new file mode 100644 index 000000000..6b2543517 --- /dev/null +++ b/charon/tests/ui/unsupported/foreign-constant.rs @@ -0,0 +1,4 @@ +//@ known-failure +//@ aux-crate=foreign-constant-aux.rs +use foreign_constant_aux::CONSTANT; +const _: i32 = 1 << CONSTANT;