Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

ICE: control character found while parsing a string #2261

Closed
matthiaskrgr opened this issue Mar 2, 2023 · 5 comments
Closed

ICE: control character found while parsing a string #2261

matthiaskrgr opened this issue Mar 2, 2023 · 5 comments
Assignees
@adpaco-aws
Labels
[C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed

Comments

@matthiaskrgr
Copy link
Contributor

matthiaskrgr commented Mar 2, 2023 •
edited
Loading

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
@matthiaskrgr matthiaskrgr added the [C] Bug This is a bug. Something isn't working. label Mar 2, 2023
@zhassan-aws zhassan-aws added the [F] Crash Kani crashed label Mar 2, 2023
@zhassan-aws
Copy link
Contributor

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

@zhassan-aws
Copy link
Contributor

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
Copy link
Contributor

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
Copy link
Contributor Author

this seems fixed with kani 0.40 \o/

@adpaco-aws
Copy link
Contributor

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@adpaco-aws adpaco-aws

Labels
[C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@matthiaskrgr @adpaco-aws @zhassan-aws