viperproject
Consistency error when running `cargo-prusti --release`
The cargo-prusti binary (tested with Nightly Release v-2023-03-29-1508 for Ubuntu-22.04) can be used with the parameter cargo-prusti --release, which caused a consistency error:
error: [Prusti internal error] Prusti encountered an unexpected internal error
|
= note: We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new
= note: Details: consistency error in prusti_tests::test: Consistency error: Local variable _2 not found. (@26.5)
error: could not compile `prusti_tests` due to previous error
Not all crates cause this error, one way to trigger it is this:
use prusti_contracts::*;
fn test(a: i32) -> i32 {
let (b, c) = tuple(a);
a / 2
}
#[pure]
fn tuple(x: i32) -> (i32, i32) {
(x + x, x)
}
My guess is that (b, c) is optimized away in release mode, but Prusti expects it to still exist. The error is not triggered when using a function returning just an i32 instead of a tuple or if the tuple function is not marked with #[pure].
Running with --release might not be intended to be used with cargo-prusti anyways.
Using prusti-rustc with the -O flag causes the same error. It seems to be a bug in the pure encoder, when overflow checks are disabled. -O or --release should make no difference for Prusti because we set -Coverflow-checks=on when the overflow checks are enabled.
The relevant part of the generated Viper program before and after adding the optimization flag:
function builtin$unreach__$TY$__Snap$tuple2$i32$i32$Snap$tuple2$i32$i32(): Snap$tuple2$i32$i32
requires false
function m_tuple__$TY$__$int$$Snap$tuple2$i32$i32(_1: Int): Snap$tuple2$i32$i32
requires true
requires true
ensures true
ensures [result ==
mirror_simple$m_tuple__$TY$__$int$$Snap$tuple2$i32$i32(_1),
true]
{
cons$0$__$TY$__Snap$tuple2$i32$i32$$int$$$int$$Snap$tuple2$i32$i32(_1 +
_1, _1)
}
:arrow_down:
function m_tuple__$TY$__$int$$Snap$tuple2$i32$i32(_1: Int): Snap$tuple2$i32$i32
requires true
requires true
ensures true
ensures [result ==
mirror_simple$m_tuple__$TY$__$int$$Snap$tuple2$i32$i32(_1),
true]
{
cons$0$__$TY$__Snap$tuple2$i32$i32$$int$$$int$$Snap$tuple2$i32$i32(_2.val_int,
_1)
}
The source MIR of the second generated program is perfectly standard:
fn tuple(_1: i32) -> (i32, i32) {
debug x => _1; // in scope 0 at /home/fpoli/src/snippets/prusti/20230331_120304.rs:9:10: 9:11
let mut _0: (i32, i32); // return place in scope 0 at /home/fpoli/src/snippets/prusti/20230331_120304.rs:9:21: 9:31
let mut _2: i32; // in scope 0 at /home/fpoli/src/snippets/prusti/20230331_120304.rs:10:6: 10:11
let mut _3: i32; // in scope 0 at /home/fpoli/src/snippets/prusti/20230331_120304.rs:10:6: 10:7
let mut _4: i32; // in scope 0 at /home/fpoli/src/snippets/prusti/20230331_120304.rs:10:10: 10:11
let mut _5: i32; // in scope 0 at /home/fpoli/src/snippets/prusti/20230331_120304.rs:10:13: 10:14
bb0: {
StorageLive(_2); // scope 0 at /home/fpoli/src/snippets/prusti/20230331_120304.rs:10:6: 10:11
StorageLive(_3); // scope 0 at /home/fpoli/src/snippets/prusti/20230331_120304.rs:10:6: 10:7
_3 = _1; // scope 0 at /home/fpoli/src/snippets/prusti/20230331_120304.rs:10:6: 10:7
StorageLive(_4); // scope 0 at /home/fpoli/src/snippets/prusti/20230331_120304.rs:10:10: 10:11
_4 = _1; // scope 0 at /home/fpoli/src/snippets/prusti/20230331_120304.rs:10:10: 10:11
_2 = Add(move _3, move _4); // scope 0 at /home/fpoli/src/snippets/prusti/20230331_120304.rs:10:6: 10:11
StorageDead(_4); // scope 0 at /home/fpoli/src/snippets/prusti/20230331_120304.rs:10:10: 10:11
StorageDead(_3); // scope 0 at /home/fpoli/src/snippets/prusti/20230331_120304.rs:10:10: 10:11
StorageLive(_5); // scope 0 at /home/fpoli/src/snippets/prusti/20230331_120304.rs:10:13: 10:14
_5 = _1; // scope 0 at /home/fpoli/src/snippets/prusti/20230331_120304.rs:10:13: 10:14
_0 = (move _2, move _5); // scope 0 at /home/fpoli/src/snippets/prusti/20230331_120304.rs:10:5: 10:15
StorageDead(_5); // scope 0 at /home/fpoli/src/snippets/prusti/20230331_120304.rs:10:14: 10:15
StorageDead(_2); // scope 0 at /home/fpoli/src/snippets/prusti/20230331_120304.rs:10:14: 10:15
return; // scope 0 at /home/fpoli/src/snippets/prusti/20230331_120304.rs:11:2: 11:2
}
}
It's like if this line has no effect: https://github.com/viperproject/prusti-dev/blob/a3fd92b08332bd4685cdac62ecbf8ad4695944cb/prusti-viper/src/encoder/mir/pure/interpreter/interpreter_poly.rs#L1062