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 :thinking:

[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?