Confused why this hangs ?

[DavePearce]

Hey,

So, basically, I'm just refactoring some tests and I had something like this:

    let xs : [u32; 3] = __nondet();
    // Ensure element not in array
    for x in xs {
	__VERIFIER_assume(x != 0);
    }        
    //
    assert!(indexof(&xs,0) == usize::MAX);

This seems to work fine, and I was writing more tests like this so refactored like so:

#[cfg(rmc)]
#[no_mangle]
fn disjoint(items : &[u32], item: u32) {
    for ith in items {
	__VERIFIER_assume(*ith != item);
    }        
}

...

    // Create arbitrary array of size 3
    let xs : [u32; 3] = __nondet();
    // Ensure element not in array
    disjoint(&xs,0);
    //
    assert!(indexof(&xs,0) == usize::MAX);

But, the second version hangs for reasons unknown. They seem equivalent to me! (full listing below)

Thoughts appreciated!!

fn indexof(items: &[u32], item: u32) -> usize {
    for i in 0..items.len() {
	if items[i] == item {
            return i;
	}
    }
    //
    return usize::MAX;
}

fn __nondet<T>() -> T {
    unimplemented!()
}
fn __VERIFIER_assume(cond: bool) {
    unimplemented!()
}

/**
 * Ensure that a given item is not in the give array.
 */
#[cfg(rmc)]
#[no_mangle]
fn disjoint(items : &[u32], item: u32) {
    for ith in items {
	__VERIFIER_assume(*ith != item);
    }        
}

#[cfg(rmc)]
#[no_mangle]
pub fn test_01() {
    // Create arbitrary array of size 3
    let xs : [u32; 3] = __nondet();
    // Ensure element not in array
    for x in xs {
	__VERIFIER_assume(x != 0);
    }        
    //
    assert!(indexof(&xs,0) == usize::MAX);
} 

#[cfg(rmc)]
#[no_mangle]
pub fn test_02() {
    // Create arbitrary array of size 3
    let xs : [u32; 3] = __nondet();
    // Ensure element not in array
    disjoint(&xs,0);
    //
    assert!(indexof(&xs,0) == usize::MAX);
} 

#[cfg(rmc)]
#[no_mangle]
pub fn main() {
    test_01();
    test_02();    
}

[DavePearce]

And, likewise I'm struggling to get quantified statements through:

#[cfg(rmc)]
#[no_mangle]
pub fn test_02() {
    // Create arbitrary array of size 3
    let xs : [u32; 2] = __nondet();
    // Create arbitrary index within array
    let i : usize = __nondet();
    __VERIFIER_assume(i < xs.len());
    // Ensure known value at that point
    __VERIFIER_assume(xs[i] == 0);    
    // Ensure nothing in array below i matches
    for j in 0..2 {
	if j != i {
	    __VERIFIER_assume(xs[j] != 0);
	}
    }
    //
    assert!(indexof(&xs,0) == i);
} 

If I manually unroll the loop then its fine.

[zhassan-aws]

The non-termination in test_02 is caused by CBMC unwinding forever (because the first parameter in disjoint has an unspecified length). An unwinding depth can be specified by passing --cbmc-args --unwind <value> to RMC. For this example, an unwinding depth of 4 (--cbmc-args --unwind 4) is sufficient. Please refer to the Loops, unwinding, and bounds section of the RMC tutorial for more details.

There is an ongoing discussion to change the default unwinding depth to 0 to avoid this confusion.

[DavePearce]

Hey @zhassan-aws,

Ah, thanks --- I should have looked at that. For some reason I was expecting, since the number of iterations is fixed it would effectively just unroll it.

[DavePearce]

Hmmm, have made progress but I don't really understand from the tutorial what exactly the "unwinding assertion" is telling me when its failing. Its somehow telling me that I need to unwind more? How does RMC / CBMC decide this?

[zhassan-aws]

Yes, a failing unwinding assertion indicates that a larger unwinding is needed. The unwinding assertions option adds a check that the unwind + 1 iteration of the loop is unreachable. If the check is proven, then the unwinding depth was sufficient.

[DavePearce]

Thanks! I'm making progress on this. Here's what I have now:

const LIMIT : usize = 6;

#[cfg(rmc)]
#[no_mangle]
pub fn test_01() {
    // Create arbitrary array
    let xs : [u32; LIMIT] = __nondet();
    // Create arbitrary element
    let x : u32 = __nondet();
    // Create arbitrary (valid) length
    let len : usize = __nondet();
    __VERIFIER_assume(len <= LIMIT);
    // Ensure element not in array below len
    for i in 0..len {
	__VERIFIER_assume(xs[i] != x);
    }  
    // Check
    assert!(indexof(&xs[..len],x) == usize::MAX);
} 

#[cfg(rmc)]
#[no_mangle]
pub fn test_02() {
    // Create arbitrary array
    let xs : [u32; LIMIT] = __nondet();
    // Create arbitrary element
    let x : u32 = __nondet();
    // Create arbitrary (valid) length
    let len : usize = __nondet();
    __VERIFIER_assume(len <= LIMIT);
    // Create arbitrary index within array
    let i : usize = __nondet();
    __VERIFIER_assume(i < len);
    // Ensure known value at index i
    __VERIFIER_assume(xs[i] == x);    
    // Ensure nothing in array below i matches
    for j in 0..i {
	__VERIFIER_assume(xs[j] != x);
    }
    // Check find correct one
    assert!(indexof(&xs[..len],x) == i);
} 

How does this look in terms of how you would write it?

The performance is interesting as with LIMIT==6 and --unwind 7 it seems to take a very long time, whilst with LIMIT==5 and --unwind 6 it completes pretty quickly.

[zhassan-aws]

Looks good to me. By default, CBMC uses MiniSat. You might want to try with a more modern SAT solver, e.g. Kissat. To specify a different SAT solver, use --cbmc-args --external-sat-solver <path-to-sat-solver-executable>, e.g.

rmc test.rs --cbmc-args --external-sat-solver kissat --unwind 5

[DavePearce]

Ok, will do --- thanks!!