Assert(false) passing with Shared References

[cliu369]

prusti_assert!(false) passes in this example:

fn foo(a: &u8, b: &u8) {}

fn bar() {
    let x: u8 = 5;
    foo(&x, &x);
    prusti_assert!(false);
}

The issue is similar to #1189.

I am using Prusti version: 0.2.2, commit 0d4a8d4 2024-03-26 13:08:03 UTC, built on 2024-05-25 14:23:53 UTC.

[nishanthkarthik]

I reduced the generated viper encoding down to the following (perm of val_int in comments)

field val_int: Int

field val_ref: Ref

function read$(): Perm
  ensures none < result
  ensures result < write

method m_main() returns (_0: Ref)
{
  var read: Perm := read$()

  var a: Ref := builtin$havoc_ref()
  inhale acc(a.val_int, write) // write
  a.val_int := 1

  // borrow 1
  var b: Ref := builtin$havoc_ref()
  inhale acc(b.val_ref, write)
  b.val_ref := a
  exhale acc(a.val_int, write - read) // read
  inhale acc(b.val_ref.val_int, read) // 2 * read

  // reborrow 1
  var c: Ref := builtin$havoc_ref()
  inhale acc(c.val_ref, write)
  c.val_ref := b.val_ref
  inhale acc(c.val_ref.val_int, read) // 3 * read

  label post1rb

  // borrow 2
  var d: Ref := builtin$havoc_ref()
  inhale acc(d.val_ref, write)
  d.val_ref := a
  inhale acc(d.val_ref.val_int, read) // 4 * read

  // reborrow 2
  var e: Ref := builtin$havoc_ref()
  inhale acc(e.val_ref, write)
  e.val_ref := d.val_ref
  inhale acc(e.val_ref.val_int, read) // 5 * read

  label post2rb

  exhale acc(c.val_ref, write) && acc(e.val_ref, write)

  // drop reborrows
  exhale acc(old[post1rb](c.val_ref).val_int, read) // 4 * read
  exhale acc(old[post2rb](e.val_ref).val_int, read) // 3 * read

  // drop borrow 2
  exhale acc(d.val_ref.val_int, read) // 2 * read
  inhale acc(a.val_int, write - read) // read + write

  // unsound from here onwards
  assert false

  // drop borrow 1
  exhale acc(b.val_ref.val_int, read) // read
  inhale acc(a.val_int, write - read) // write

  assert perm(a.val_int) == write
}

method builtin$havoc_ref() returns (ret: Ref)

Looking at the structure of the viper program generated, here's an even more minimal example

fn main() {
    let x: u8 = 5;
    let r = &x;
    let rb = &*r;
    let s = &x;
    let rs = &*s;
    prusti_assert!(rb == rs); // necessary to keep rb and rs
    prusti_assert!(false); // passes
}

Creating two shared reborrows and prolonging them leads to this unsoundness. Note - after dropping all borrows, the perm of val_int is write. I guess the bug here is in the order of inhales.