[Prusti internal error] Consistency error: No matching local variable _2 found with type Ref, instead found Int.

[Pointerbender]

The following Rust program, which is a slight variation on #815, triggers a consistency error in Prusti/Viper:

use prusti_contracts::*;

fn main() {
    let a = A::new(2, 3);
    A::test(a, 4);
}

#[derive(Clone, Copy)]
pub struct A {
    foo: isize,
    bar: usize,
}

impl A {
    #[pure]
    #[requires(num < isize::MAX as usize)]
    pub fn new(num: usize, bar: usize) -> Self {
        Self {
            foo: num as isize + isize::MIN,
            bar,
        }
    }

    #[pure]
    pub fn bar(&self) -> usize {
        self.bar
    }

    #[pure]
    #[requires(num < isize::MAX as usize)]
    pub fn test(a: A, num: usize) -> A {
        A::new(num, a.bar)
    }
}

The error message is:

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_example::A::test: Consistency error: No matching local variable _2 found with type Ref, instead found Int. (@36.13)

This happens for both Viper programs for fn main and fn test. In both cases, the relevant Viper code is:

function m_new__$TY$__(_1: Int, _2: Int): Snap$struct$m_A
  requires true
  requires _1 < builtin$cast$isize$usize__$TY$__(9223372036854775807)
  requires 0 <= _1
  requires _1 <= 18446744073709551615
  requires 0 <= _2
  requires _2 <= 18446744073709551615
  ensures true
  ensures [result == mirror_simple$m_new__$TY$__(_1, _2), true]
{
  (
    !(
      builtin$cast$usize$isize__$TY$__(_1) + -9223372036854775808 < -9223372036854775808
      || builtin$cast$usize$isize__$TY$__(_1) + -9223372036854775808 > 9223372036854775807
    )
      ? cons$0$__$TY$__Snap$struct$m_A$(
          builtin$cast$usize$isize__$TY$__(_1) + -9223372036854775808,
           _2.val_int // <-- the error comes from here
        )
      : builtin$unreach__$TY$__Snap$struct$m_A$()
  )
}

Something seems to be going wrong during the encoding step, where _2 is mistaken for a Ref instead of an Int as declared in the function signature.

[Pointerbender]

I did some debugging to see if I could find out more. In the snapshot patcher

prusti-dev/prusti-viper/src/encoder/snapshot/patcher.rs

Lines 134 to 154 in aaddd28

	receiver => {
	let receiver = self.fallible_fold_boxed(receiver)?;
	match receiver.get_type() {
	vir::Type::Int if field.name == "val_int" => Ok(*receiver),
	vir::Type::Bool if field.name == "val_bool" => Ok(*receiver),
	vir::Type::Snapshot(_) => match field.name.as_str() {
	"val_ref" => Ok(*receiver),
	_ => self.snapshot_encoder.snap_field(
	self.encoder,
	*receiver,
	field,
	self.tymap,
	),
	},
	_ => Ok(vir::Expr::Field(vir::FieldExpr {
	base: receiver,
	field,
	position,
	})),
	}
	}

indeed _2 is passed in as a vir::Type::TypedRef when inspecting receiver.get_type():

Local(
    Local {
        variable: _2: Ref(usize),
        position: Position {
            line: 36,
            column: 13,
            id: 50,
        },
    },
)

While at this point I believe it should already be passed as a:

Local(
    Local {
        variable: _2: Int,
        position: Position {
            line: 0,
            column: 0,
            id: 0,
        },
    },
)

Im not sure whether the snapshot patcher is the best place to fix this, I have a feeling that an earlier substitution already went off the rails and its best fixed there, but I haven't been able to pin-point that one yet.

[Aurel300]

Just wondering: does this occur under #899? I changed some var substitution stuff there.

[Pointerbender]

Indeed the same error happens on the branch for #899 (also on the master branch).

[Pointerbender]

I suspect that the cause of the problem can be found somewhere in the logic of the PureFunctionBackwardInterpreter.

The MIR for A::new is:

// MIR for `<impl at src/lib.rs:30:1: 50:2>::new` 0 renumber

fn <impl at src/lib.rs:30:1: 50:2>::new(_1: usize, _2: usize) -> A {
    debug num => _1;                     // in scope 0 at src/lib.rs:33:16: 33:19
    debug bar => _2;                     // in scope 0 at src/lib.rs:33:28: 33:31
    let mut _0: A;                       // return place in scope 0 at src/lib.rs:33:43: 33:47
    let mut _3: isize;                   // in scope 0 at src/lib.rs:35:18: 35:43
    let mut _4: isize;                   // in scope 0 at src/lib.rs:35:18: 35:30
    let mut _5: usize;                   // in scope 0 at src/lib.rs:35:18: 35:21
    let mut _6: (isize, bool);           // in scope 0 at src/lib.rs:35:18: 35:43
    let mut _7: usize;                   // in scope 0 at src/lib.rs:36:13: 36:16

    bb0: {
        StorageLive(_3);                 // scope 0 at src/lib.rs:35:18: 35:43
        StorageLive(_4);                 // scope 0 at src/lib.rs:35:18: 35:30
        StorageLive(_5);                 // scope 0 at src/lib.rs:35:18: 35:21
        _5 = _1;                         // scope 0 at src/lib.rs:35:18: 35:21
        _4 = move _5 as isize (Misc);    // scope 0 at src/lib.rs:35:18: 35:30
        StorageDead(_5);                 // scope 0 at src/lib.rs:35:29: 35:30
        _6 = CheckedAdd(_4, const core::num::<impl isize>::MIN); // scope 0 at src/lib.rs:35:18: 35:43
        assert(!move (_6.1: bool), "attempt to compute `{} + {}`, which would overflow", move _4, const core::num::<impl isize>::MIN) -> [success: bb1, unwind: bb2]; // scope 0 at src/lib.rs:35:18: 35:43
    }

    bb1: {
        _3 = move (_6.0: isize);         // scope 0 at src/lib.rs:35:18: 35:43
        StorageDead(_4);                 // scope 0 at src/lib.rs:35:42: 35:43
        StorageLive(_7);                 // scope 0 at src/lib.rs:36:13: 36:16
        _7 = _2;                         // scope 0 at src/lib.rs:36:13: 36:16
        _0 = A { foo: move _3, bar: move _7 }; // scope 0 at src/lib.rs:34:9: 37:10
        StorageDead(_7);                 // scope 0 at src/lib.rs:37:9: 37:10
        StorageDead(_3);                 // scope 0 at src/lib.rs:37:9: 37:10
        return;                          // scope 0 at src/lib.rs:38:6: 38:6
    }

    bb2 (cleanup): {
        resume;                          // scope 0 at src/lib.rs:33:5: 38:6
    }
}

[Pointerbender]

I found some code that hints at a similar fix as would be applied to the problem in this issue:

prusti-dev/prusti-viper/src/encoder/mir/pure/pure_functions/encoder.rs

Lines 142 to 167 in 6a9291b

	pub fn encode_function(&self) -> SpannedEncodingResult<vir::Function> {
	let function_name = self.encode_function_name();
	debug!("Encode pure function {}", function_name);
	let mut state = run_backward_interpretation(self.mir, &self.interpreter)?
	.unwrap_or_else(|| panic!("Procedure {:?} contains a loop", self.proc_def_id));
	// Fix arguments
	for arg in self.mir.args_iter() {
	let arg_ty = self.interpreter.mir_encoder().get_local_ty(arg);
	let span = self.get_local_span(arg);
	let target_place = self
	.encoder
	.encode_value_expr(
	vir::Expr::local(self.interpreter.mir_encoder().encode_local(arg)?),
	arg_ty,
	)
	.with_span(span)?;
	let mut new_place: vir::Expr = self.encode_local(arg)?.into();
	if let ty::TyKind::Ref(_, _, _) = arg_ty.kind() {
	// patch references with an explicit snap app
	// TODO: this probably needs to be adjusted when snapshots of
	// references are implemented
	new_place = vir::Expr::snap_app(new_place);
	}
	state.substitute_value(&target_place, new_place);
	}

It looks like it is checked already here, but maybe it's missing a corner case somewhere.

[Pointerbender]

I think I've fixed it locally, I'll open a PR once the test suite passes :)

[fpoli]

Fixed in #928. Thanks!