ICE: control character found while parsing a string

[matthiaskrgr]

I tried this code:

#[kani::proof]
pub fn main() {
    assert_eq!(r"newline:'
', tab:'    ', unicode:'●', null:''",
        "newline:'\n', tab:'\t', unicode:'\u{25cf}', null:'\0'");
}

using the following command line invocation:

kani 2.rs

with Kani version: 0.22.0

I expected to see this happen: explanation

Instead, this happened: explanation

Checking harness main...
CBMC 5.77.0 (cbmc-5.77.0)
CBMC version 5.77.0 (cbmc-5.77.0) 64-bit x86_64 linux
Reading GOTO program from file /home/matthias/vcs/github/icemaker/kani/2.for-main.out
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 16 object bits, 48 offset bits (user-specified)
Starting Bounded Model Checking
Unwinding loop memcmp.0 iteration 1 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 2 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 3 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 4 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 5 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 6 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 7 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 8 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 9 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 10 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 11 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 12 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 13 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 14 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 15 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 16 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 17 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 18 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 19 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 20 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 21 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 22 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 23 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 24 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 25 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 26 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 27 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 28 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 29 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 30 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 31 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 32 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 33 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 34 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 35 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 36 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 37 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 38 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 39 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 40 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 41 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 42 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 43 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 44 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 45 file <builtin-library-memcmp> line 25 function memcmp thread 0
Runtime Symex: 0.132867s
size of program expression: 1102 steps
slicing removed 770 assignments
Generated 568 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 0.000925857s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.00514879s
Running propositional reduction
Post-processing
Runtime Post-process: 3.8863e-05s
Solving with MiniSAT 2.2.1 with simplifier
1809 variables, 1809 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.00223997s
Runtime decision procedure: 0.00769175s
thread '<unnamed>' panicked at 'called `Result::unwrap()` on an `Err` value: Error("control character (\\u0000-\\u001F) found while parsing a string", line: 2073, column: 123)', kani-driver/src/cbmc_output_parser.rs:453:25
stack backtrace:
   0:     0x5567efb28b0a - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::h9271b09f3576b7e0
   1:     0x5567efb4fa1e - core::fmt::write::h27d0bbb767cff1d5
   2:     0x5567efb25205 - std::io::Write::write_fmt::hc409ea2bb818fbea
   3:     0x5567efb288d5 - std::sys_common::backtrace::print::he69ac0980f15620d
   4:     0x5567efb2a29f - std::panicking::default_hook::{{closure}}::h014cf704a69dce2b
   5:     0x5567efb29fdb - std::panicking::default_hook::h380e71f8d8d49df7
   6:     0x5567efb2a9ac - std::panicking::rust_panic_with_hook::h483f1ef90c766581
   7:     0x5567efb2a749 - std::panicking::begin_panic_handler::{{closure}}::hd4c7d9116c0ef489
   8:     0x5567efb28fbc - std::sys_common::backtrace::__rust_end_short_backtrace::had27a083c7d7188b
   9:     0x5567efb2a452 - rust_begin_unwind
  10:     0x5567ef866d33 - core::panicking::panic_fmt::hbacb72817da3b060
  11:     0x5567ef8671c3 - core::result::unwrap_failed::h75b01130eef49956
  12:     0x5567ef96175d - <kani_driver::cbmc_output_parser::Parser as core::iter::traits::iterator::Iterator>::next::hc23ea82bfbe873f4
  13:     0x5567ef90c3fb - <alloc::vec::Vec<T> as alloc::vec::spec_from_iter::SpecFromIter<T,I>>::from_iter::hc8a65883a163ddfa
  14:     0x5567ef9618dc - kani_driver::cbmc_output_parser::process_cbmc_output::hbb9dbe74ed55fee7
  15:     0x5567ef8c0e5e - kani_driver::harness_runner::<impl kani_driver::session::KaniSession>::check_harness::h04018ff03c56a0a9
  16:     0x5567ef8f1f6c - core::ops::function::impls::<impl core::ops::function::FnOnce<A> for &mut F>::call_once::hc0ff2473d26eac09
  17:     0x5567ef90684b - <alloc::vec::Vec<T,A> as alloc::vec::spec_extend::SpecExtend<T,I>>::spec_extend::h491b6cab1ef21da5
  18:     0x5567ef8b0821 - rayon::iter::plumbing::bridge_producer_consumer::helper::h60f2e69f51ca9637
  19:     0x5567ef8b06ef - rayon::iter::from_par_iter::collect_extended::h14dacc43c7a5fbce
  20:     0x5567ef8b0b7e - rayon::result::<impl rayon::iter::FromParallelIterator<core::result::Result<T,E>> for core::result::Result<C,E>>::from_par_iter::h861e35891938d021
  21:     0x5567ef898585 - <rayon_core::job::StackJob<L,F,R> as rayon_core::job::Job>::execute::hd5b4d3608b171307
  22:     0x5567ef85c324 - rayon_core::registry::WorkerThread::wait_until_cold::h0004c202f9e15e34
  23:     0x5567ef9a448c - rayon_core::registry::ThreadBuilder::run::h894cc7b54de41b26
  24:     0x5567ef9a2a8a - std::sys_common::backtrace::__rust_begin_short_backtrace::ha3a3bb138e8f9bec
  25:     0x5567ef9a6931 - core::ops::function::FnOnce::call_once{{vtable.shim}}::h86eb07bd2da94a69
  26:     0x5567efb2fdf3 - std::sys::unix::thread::Thread::new::thread_start::h5af9cdd9a5a58d64
  27:     0x7f9777856bb5 - <unknown>
  28:     0x7f97778d8d90 - <unknown>
  29:                0x0 - <unknown>

2.rs.tar.gz

[zhassan-aws]

@adpaco-aws this is an issue with the CBMC output parser. Can you take a look?

[zhassan-aws]

Note that you need to use the attached tarball (I couldn't reproduce it by copying and pasting the code).

This is the raw output from CBMC:

kani 2.rs --output-format old
...
/home/ubuntu/examples/iss2261/2.rs function main
[main.assertion.1] line 3 [KANI_CHECK_ID_2.a89191b9::2_0] assertion failed: r"newline:'
', tab:'        ', unicode:'●', null:''" ==
"newline:'\n', tab:'\t', unicode:'\u{25cf}', null:'\0'": SUCCESS

[adpaco-aws]

The failure corresponds to these lines (455-457) in parse_item:

        let complete_string = &self.input_so_far[0..self.input_so_far.len()];
        let result_item: Result<ParserItem, _> = serde_json::from_str(complete_string);
        result_item.unwrap()

serde_json returns an error because it finds control characters in the JSON output, which aren't considered valid. There may be a way to disable this validation, but I'm not sure we want to do that 😅

I see this more as a limitation that the JSON format introduces because of our current approach to post-processing. I don't have a good solution for that at the moment.

[matthiaskrgr]

this seems fixed with kani 0.40 \o/

[adpaco-aws]

This doesn't crash anymore as @matthiaskrgr pointed out. The assertion fails but that's also what happens in the Rust playground.

SUMMARY:
 ** 1 of 39 failed
Failed Checks: assertion failed: r"newline:'
', tab:'        ', unicode:'●', null:''" ==
"newline:'\n', tab:'\t', unicode:'\u{25cf}', null:'\0'"
 File: "src/main.rs", line 3, in main

VERIFICATION:- FAILED
Verification Time: 0.10546225s