Standard contracts not fully rebuilt when a contract is removed
darioncassel opened this issue · 2 comments
Issue
If a contract is fully removed from the standard contracts foreign_contracts
file, after rebuilding standard contracts, the results of MIRAI's analysis seem to indicate that the contract is still there.
Steps to Reproduce
This example is done on the move-binary-format
crate (https://github.com/darioncassel/libra/tree/main/language/move-binary-format). Before any of the steps below are followed, the function verify_impl
does not have unsatisfied preconditions, but analysis of it may time out.
- Add contract with a known-false precondition.
--- a/standard_contracts/src/foreign_contracts.rs
+++ b/standard_contracts/src/foreign_contracts.rs
@@ -3735,6 +3735,21 @@ pub mod move_binary_format {
}
}
}
+
+ pub mod check_bounds {
+ pub mod implement {
+ pub struct PartialVMResult<T> {
+ _result: T,
+ }
+
+ pub struct BoundsChecker {}
+
+ pub fn verify_impl(_self: &mut BoundsChecker) -> PartialVMResult<()> {
+ precondition!(false);
+ result!()
+ }
+ }
+ }
}
- Rebuild standard contracts and install MIRAI.
./rebuild_std.sh
./install_mirai.sh
- Run analysis on
language/move-binary-format/
from fully clean state.
cargo clean
RUSTFLAGS="-Z always_encode_mir" cargo build
touch src/lib.rs && RUSTFLAGS="-Z always_encode_mir" RUSTC_WRAPPER=mirai MIRAI_FLAGS="--diag=verify" cargo build
Result: The contract is reached and found to be unsatisfied as expected.
warning: unsatisfied precondition, defined in standard_contracts/src/foreign_contracts.rs:3748:17: 3748:38
--> language/move-binary-format/src/check_bounds.rs:86:9
|
86 | bounds_check.verify_impl()
| ^^^^^^^^^^^^^^^^^^
- Remove that contract, rebuild standard contracts, and install MIRAI.
./rebuild_std.sh
./install_mirai.sh
- Run the analysis.
cargo clean
RUSTFLAGS="-Z always_encode_mir" cargo build
touch src/lib.rs && RUSTFLAGS="-Z always_encode_mir" RUSTC_WRAPPER=mirai MIRAI_FLAGS="--diag=verify" cargo build
Result:
warning: unsatisfied precondition, defined in standard_contracts/src/foreign_contracts.rs:3748:17: 3748:38
--> language/move-binary-format/src/check_bounds.rs:55:9
|
55 | bounds_check.verify_impl()?;
| ^^^^^^^^^^^^^^^^^^^^^^^^^^
Expected Behavior
There should not be an unsatisfied precondition for verify_impl
at step 4 because the contract was removed in step 3.
Actual Results
The unsatisfied precondition (precondition!(false)
) results in a warning that still references foreign_contracts.rs
even though the contract was removed.
Environment
Rust version (rustc --version): rustc 1.55.0-nightly (7c3872e6b 2021-06-24)
I find myself wondering if the second call to ./install_mirai.sh does a rebuild of MIRAI. I.e. perhaps cargo install does not figure out that updating binaries/summary_store.tar invalidates the current binary for MIRAI and so the second call to cargo install just uses the same bits as the first call.
Perhaps, but I think that is less likely because if I use git to manually revert just the summary_store.tar
file and then follow that same rebuild process (including install_mirai.sh
) the contract no longer shows up in the analysis.