Too many addressed objects in RAII example

[adpaco-aws]

Currently, the Rust by Example/Scoping rules/RAII/11.rs fails to verify with default CBMC values. See the example below:

#![allow(unused)]
// raii.rs
fn create_box() {
    // Allocate an integer on the heap
    let _box1 = Box::new(3i32);

    // `_box1` is destroyed here, and memory gets freed
}

pub fn main() {
    // Allocate an integer on the heap
    let _box2 = Box::new(5i32);

    // A nested scope:
    {
        // Allocate an integer on the heap
        let _box3 = Box::new(4i32);

        // `_box3` is destroyed here, and memory gets freed
    }

    // Creating lots of boxes just for fun
    // There's no need to manually free memory!
    for _ in 0u32..1_000 {
        create_box();
    }

    // `_box2` is destroyed here, and memory gets freed
}

The create_box creates a box, then frees its memory since it goes out of scope.

One needs to use --cbmc-args --object-bits 13 in order to successfully verify this example, but even then it takes 5 minutes to do so.

As far as I can tell, this is a good candidate for verification optimizations.

[zhassan-aws]

Still takes ~5 minutes with af11d38d93a.

[tautschnig]

What would be deemed "acceptable" for this harness? With #2301 this takes 150 seconds (2.5 minutes).

[adpaco-aws]

It depends on where the time is being spent. What I'd expect to see for this example is near-zero time spent on solving (we create objects that are independent), and I'd consider the time you posted acceptable if >2mins are spent on unwinding.

Then there's also the problem of requiring --cbmc-args --object-bits 13: the program doesn't allocate more than 2 objects in the heap at any point in time, but CBMC appears to not be reusing free'd memory addresses. Is that a limitation of its memory model?

[zhassan-aws]

This is not real code, so I wouldn't worry about it too much. I think what was surprising is that even though the test does nothing but allocate and deallocate memory a number of times, it takes long to analyze.