A crash bug identified during the verification

[stoneman258]

While verifying a Rust project with Prusti (version 0.2.2), it reports an internal error: "Consistency error: No matching local variable". The command used was cargo prusti. Below is a minimized code example reproducing the issue:

use prusti_contracts::*;
#[pure]
fn negate_i32(x: i32) -> i32 { [0-x, x][0] }
fn main() { negate_i32(i32::MIN); }

Crash Stack Trace

error: [Prusti: internal error] Prusti encountered an unexpected internal error
  |
  = note: This is likely to be a bug in Prusti. We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new
  = note: Details: consistency error in testcase::main: Consistency error: No matching local variable _1 found with type Ref, instead found Int. (@8.0)
error: [Prusti: internal error] Prusti encountered an unexpected internal error
  |
  = note: This is likely to be a bug in Prusti. We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new
  = note: Details: consistency error in testcase::main: Consistency error: All elements of sequence must have same type. (@11.0)

[stoneman258]

I find two additional crash bugs triggered by the contracts with distinct root causes.

Code Example 1

use prusti_contracts::*;
#[pure]
fn fib(n: isize) -> isize {
    if n <= 1 {
        1
    } else {
        fib_race(n)
    }
}
#[pure]
fn fib_race(n: isize) -> isize {
    fib(n - 1) + fib(n - 2)
}
fn main() {
    fib(5);
}

Crash Log

error: [Prusti: internal error] Prusti encountered an unexpected internal error
 --> src/main.rs:3:1
  |
3 | fn fib(n: isize) -> isize {
  | ^^^^^^^^^^^^^^^^^^^^^^^^^
  |
  = help: This could be caused by too small assertion timeout. Try increasing it by setting the configuration parameter ASSERT_TIMEOUT to a larger value.
  = note: This is likely to be a bug in Prusti. We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new
  = note: Details: unhandled verification error: Postcondition of f_fib__$TY$__$int$$$int$ might not hold. Assertion -9223372036854775808 <= result might not hold. (@6.0)
           [postcondition.violated:assertion.false] PureFunctionPostconditionValueRangeOfResult

Code Example 2

use prusti_contracts::*;
#[pure]
fn double(x: i64) -> i64 {
    let m = i64::MAX;
    x + m - x
}
fn main() {
    double(i64::MAX);
}

Crash Log

thread 'rustc' panicked at prusti-viper/src/encoder/mir/pure/pure_functions/interface.rs:255:36:
unevaluated const should have a promoted ID
stack backtrace:
  22:     0x559294bf9ba5 - <prusti_viper::encoder::encoder::Encoder as prusti_viper::encoder::mir::pure::pure_functions::interface::PureFunctionEncoderInterface>::encode_uneval_const::h269a2171b06f6b0e
  23:     0x55929501621f - prusti_viper::encoder::mir::pure::interpreter::interpreter_poly::PureFunctionBackwardInterpreter::encode_operand::hba5defa4097979c8
  24:     0x55929506e089 - <prusti_viper::encoder::mir::pure::interpreter::interpreter_poly::PureFunctionBackwardInterpreter as prusti_viper::encoder::mir::pure::interpreter::backward_interpreter::BackwardMirInterpreter>::apply_statement::h6f3176b9115c5b4b
  25:     0x559295049b58 - prusti_viper::encoder::mir::pure::interpreter::backward_interpreter::run_backward_interpretation::hb36f160e00687483
  26:     0x5592948756ce - prusti_viper::encoder::mir::pure::pure_functions::encoder_poly::PureFunctionEncoder::encode_function::h5ca0d9f4afcc857b
  ......