Open cliu369 opened 2 weeks ago
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.
prusti_assert!(false) passes in this example:
The issue is similar to #1189.
I am using Prusti version: 0.2.2, commit 0d4a8d497ac 2024-03-26 13:08:03 UTC, built on 2024-05-25 14:23:53 UTC.