Fix handling of shifts

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
         }

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
 

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;

charon/tests/ui/unsupported/foreign-constant-aux.rs

@@ -0,0 +1,2 @@
+//@ skip
+pub const CONSTANT: u8 = 16;

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

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;