prusti-dev icon indicating copy to clipboard operation
prusti-dev copied to clipboard

Consistency error with chained pure fns and tuples

Open JonasAlaif opened this issue 3 years ago • 1 comments

The following runs into a Consistency error: Local variable _1 not found. when verifying the main function:

use prusti_contracts::*;

#[pure]
pub fn zero() -> usize { 0 }
#[pure]
pub fn tpl() -> (usize, usize) {
    (zero(), zero())
}
fn main() {
    let (a, b) = tpl();
}

In the above, tpl (as used in main) is encoded as:

function m_tpl__$TY$__(): Snap$tuple2$usize$usize
  requires true
  requires true
  ensures true
  ensures [result == mirror_simple$m_tpl__$TY$__(), true]
{
  cons$0$__$TY$__Snap$tuple2$usize$usize$(_1.val_int, _2.val_int)
}

Ignoring the superfluous lines of true, somehow the call to zero() fails to be included and _1/_2 are never set.

JonasAlaif avatar Feb 21 '22 13:02 JonasAlaif

Is this check causing the interpreter to skip the assignment?

https://github.com/viperproject/prusti-dev/blob/7977d30a028edfe0e300bb2931992d4029385b41/prusti-viper/src/encoder/mir/pure/pure_functions/interpreter.rs#L851

Aurel300 avatar Feb 21 '22 14:02 Aurel300