Repository navigation
Memory blows up on a small program involving String split #2302
Description
I tried this code:
#[kani::proof]
#[kani::unwind(4)]
#[kani::solver(cadical)]
fn main() {
let mut s = String::with_capacity(3);
//let c1 = 'a';
let c1: char = kani::any();
kani::assume(c1 == 'a');
s.push(c1);
s.push('.');
let c2 = 'b';
s.push(c2);
let v: Vec<&str> = s.split('.').collect();
assert_eq!(v.len(), 2);
assert_eq!(v[0], "a");
assert_eq!(v[1], "b");
}using the following command line invocation:
kani test.rs
with Kani version: 048b598
The version that uses let c1 = 'a'; verifies in ~1 second, but for the version the uses:
let c1: char = kani::any();
kani::assume(c1 == 'a');memory consumption reaches 30 GB.
Activity
zhassan-aws commentedon Mar 21, 2023
The original program I was trying to prove is as follows:
hence the need for the assumption.
tautschnig commentedon Apr 20, 2023
The challenge in this example is that
std::char::methods::len_utf8could return any of {1,2,3,4} for a non-constantchar. Consequently, CBMC cannot use a fixed size for the (re-)allocation. This, in turn, means that we need to use the array theory to reason about such programs. CBMC's encoding thereof in the propositional back-end needs improvement. In the meantime, I tried to use the SMT back-end on this example. Running Z3 and CVC5 demonstrates a much lower memory footprint (at most 2 GB), but they are still running for a very long time (more than 15 minutes and still going).