Contracts: Can't include non-Copy types in contract #3027
Description
When trying out the contracts feature (from Kani 0.46.0) in one of my projects, I got the following errors:
error[E0507]: cannot move out of `*e_renamed` which is behind a shared reference
--> src/lib.rs:79:5
|
79 | #[kani::ensures(match result { Ok(t) => Self::typecheck_2(*e, t), Err(_) => true})]
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ move occurs because `*e_renamed` has type `Expr`, which does not implement the `Copy` trait
|
= note: this error originates in the attribute macro `kani::ensures` (in Nightly builds, run with -Z macro-backtrace for more info)
error[E0507]: cannot move out of `*e_renamed` which is behind a shared reference
--> src/lib.rs:79:5
|
79 | #[kani::ensures(match result { Ok(t) => Self::typecheck_2(*e, t), Err(_) => true})]
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ move occurs because `*e_renamed` has type `Expr`, which does not implement the `Copy` trait
|
= note: this error originates in the attribute macro `kani::ensures` (in Nightly builds, run with -Z macro-backtrace for more info)
error: aborting due to 2 previous errors
For more information about this error, try `rustc --explain E0507`.
error: could not compile `interpreter` (lib) due to 3 previous errors
error: Failed to execute cargo (exit status: 101). Found 3 compilation errors.
I've opened #3026 for improving the error message, but anyway it's clear to me that it's asking for Expr to implement Copy. In my case, Expr is an enum defined as follows:
pub enum Expr {
Int(i32),
Bool(bool),
If {
test_expr: Box<Expr>,
then_expr: Box<Expr>,
else_expr: Box<Expr>,
},
BinaryApp {
op: BinaryOp,
arg1: Box<Expr>,
arg2: Box<Expr>,
},
}Here, the usage of Box<...> prevents me from directly deriving the Copy trait. As far as I know, the Copy trait cannot be implemented for Box<...> because we'd end up with multiple boxes referencing the same value.
Can you recommend a good workaround for this? I think it should be possible to have a custom impl for Copy that behaves like Clone, but then I'm not sure it'd work with the contracts implementation (and I'd expect performance issues even if it did).
If you'd like to reproduce the error or anything else, the complete program can be found in the kani-contracts branch of my project. Once it's cloned, simply run cargo kani.