Seahorn verifies assert!(false)

[fshaked]

The following minimal example is verified by Seahorn, even though it should obviously fail:

#[test]
fn t00() {
    for _ in 0..1 {
        verifier::VerifierNonDet::verifier_nondet(i32::default());
    }
    if prop_is_replay() { // prop_is_replay is always false for Seahorn
        verifier::VerifierNonDet::verifier_nondet(0);
    }
    verifier::assert!(false);
}

[fshaked]

Seams like the iterator of the range 0..1 confuses SH. If I change the loop to let mut c = 0; while c < 1 { ...; c += 1; } SH behaves as expected.

[alastairreid]

Iterators are surprisingly complex - lots of method calls.
See the expansion at the bottom of this page
With Rust optimization enabled, this goes away - but at low optimization levels or only using LLVM-level optimization, it is going to be quite horrible.

btw why is there a call to verifier_nondet inside the if statement?
I wasn't expecting the macros to expand to that.
(It shouldn't make a difference though - since a little LLVM inlining ought to replace it with false)

[fshaked]

Iterators are surprisingly complex - lots of method calls.
See the expansion at the bottom of this page
With Rust optimization enabled, this goes away - but at low optimization levels or only using LLVM-level optimization, it is going to be quite horrible.

Yes, but it's not that bad, I thought SH should handle it.
I also have an example where I use a simple loop and no iterators, instead I implemented the iterator calls explicitly. So I can see how "bad" it is.

btw why is there a call to verifier_nondet inside the if statement?
I wasn't expecting the macros to expand to that.

In the real code there's a print instruction there, and I replaced it with that nondet (rvt-patch-llvm does a similar thing for SH).

[fshaked]

Here is the example with everything unfolded (I looked at mem::replace and it could be challenging for verifiers):

struct MyRange {
    start: i32,
    end: i32,
}

impl MyRange {
    pub fn new(s: i32, e: i32) -> MyRange {
        MyRange { start: s, end: e }
    }

    pub fn next(&mut self) -> Option<i32> {
        if self.start < self.end {
            let n = self.start + 1;
            Some(std::mem::replace(&mut self.start, n))
        } else {
            None
        }
    }
}

#[test]
fn tsimpl_exp() {
    let mut r = MyRange::new(0,1);
    loop {
        match r.next() {
            Some(_) => {
                n(0);
                verifier::VerifierNonDet::verifier_nondet(0);
            },
            None => break,
        }
    }

    if is_one(0) {
        verifier::VerifierNonDet::verifier_nondet(0);
    }

    verifier::abort();
}

[alastairreid]

@fshaked IIRC, this was due to exceeding the bound during bounded verification combined with a confusing or unclear error message.
If this is correct, can you update this issue and maybe close it?