hangs on string.repeat() ?

[matthiaskrgr]

I tried this code:

#[kani::proof]  fn main() {
	
	let x = String::new().repeat(1);
	let z = x.chars().nth(1).unwrap();
}

using the following command line invocation:

RUSTC_WRAPPER="" cargo kani --harness  main --tests

with Kani version: 0.22.0

I expected to see this happen: explanation
It looks like there was some kind of hang..? kani/cmbc was crunching on that for more than 5 minutes until I cancelled it.
If I remove the repeat(1) , it finishes within a second 🤔

[zhassan-aws]

Hi @matthiaskrgr. Kani currently performs poorly on programs involving strings (e.g. see #2001 and #2015). The issue here seems to be a combination of using repeat and chars because this program that involves repeat verifies quickly:

#[kani::proof]
fn main() {
    let x = String::new().repeat(1);
    assert!(x.is_empty());
}

SUMMARY:
 ** 0 of 322 failed (9 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 0.68734515s

The chars method in particular deals with the UTF-8 encoding, which seems difficult to reason about. If it's possible to express properties in term of bytes, Kani may perform better. For instance, this program is verified in ~1 second:

#[kani::proof]
fn main() {
    let x = String::from("abc").repeat(5);
    let bytes = x.as_bytes();
    assert_eq!(bytes.len(), 15);
}

SUMMARY:
 ** 0 of 322 failed (3 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 1.2358496s

[zhassan-aws]

CC @tautschnig. This doesn't seem to get to the SAT solver stage after running for 20 minutes.

[zhassan-aws]

This is the CBMC call stack after running for an hour:

#270 0x0000556fa14997f3 in irept::compare(irept const&) const ()
#271 0x0000556fa14997f3 in irept::compare(irept const&) const ()
#272 0x0000556fa14997f3 in irept::compare(irept const&) const ()
#273 0x0000556fa14997f3 in irept::compare(irept const&) const ()
#274 0x0000556fa14997f3 in irept::compare(irept const&) const ()
#275 0x0000556fa14997f3 in irept::compare(irept const&) const ()
#276 0x0000556fa149a08d in irept::operator<(irept const&) const ()
#277 0x0000556fa0bad77e in std::_Rb_tree<exprt, exprt, std::_Identity<exprt>, std::less<exprt>, std::allocator<exprt> >::_M_get_insert_unique_pos(exprt const&) ()
#278 0x0000556fa1172a9a in arrayst::update_index_map(unsigned long) ()
#279 0x0000556fa1172c6c in arrayst::update_index_map(bool) ()
#280 0x0000556fa117512f in arrayst::add_array_constraints() ()
#281 0x0000556fa11c7b0f in bv_pointerst::finish_eager_conversion() ()
#282 0x0000556fa11e84dd in prop_conv_solvert::dec_solve() ()
#283 0x0000556fa0cb707c in run_property_decider(incremental_goto_checkert::resultt&, std::map<dstringt, property_infot, std::less<dstringt>, std::allocator<std::pair<dstringt const, property_infot> > >&, goto_symex_property_decidert&, ui_message_handlert&, std::chrono::duration<double, std::ratio<1l, 1l> >, bool) ()
#284 0x0000556fa0cc84f9 in multi_path_symex_checkert::operator()(std::map<dstringt, property_infot, std::less<dstringt>, std::allocator<std::pair<dstringt const, property_infot> > >&) ()
#285 0x0000556fa0b6f299 in all_properties_verifier_with_trace_storaget<multi_path_symex_checkert>::operator()() ()
#286 0x0000556fa0b6b71e in cbmc_parse_optionst::doit() ()
#287 0x0000556fa0b62f9f in parse_options_baset::main() ()
#288 0x0000556fa0b4ebe9 in main ()

[tautschnig]

See #2302: this is stuck in applying the array theory. Work-in-progress on the CBMC side.

[zhassan-aws]

@tautschnig are the arrays that the array theory is applied to within the String library? Just trying to understand the problem a bit more.

[rahulku]

@tautschnig - what are the array theory issues?

[remi-delmas-3000]

@tautschnig are the arrays that the array theory is applied to within the String library? Just trying to understand the problem a bit more.
@tautschnig - what are the array theory issues?

The problem with CBMC's array theory is that it does an eager encoding of read-over-write lemmas for all pairs of read/writes that are over the same base array, so it has a quadratic blowup in the worst case where all read/write pairs are over the same base array. CBMC's algorithm builds a weak equivalence graph (cf. https://arxiv.org/pdf/1405.6939) for all arrays used in the program and uses the graph to drive lemma instantiation.

Possible optimizations would be:

• extend symex with interval propagation and prune (read, write) pairs where the range of read indices is disjoint from the range of written indices;
• make the lemma instantiation incremental, i.e. don't generate all lemmas ahead of time but only when needed to block a spurious counter example (which @tautschnig has been experimenting with);
• use cargo kani --enable-unstable --cbmc-args --bitwuzla for cases like this one

[zhassan-aws]

Thanks @remi-delmas-3000. It's still unclear to me which array is causing a quadratic blowup. The strings in the examples above are either empty or consist of 3-4 bytes. Also, there is no non-determinism involved. My interpretation of a blowup is that as we increase the size of the string, the expression size is going to grow quadratically. But here, there is no size that we're trying to increase in this example. Is my interpretation incorrect?