Unhandled variant in ParserItem JSON

[camshaft]

I'm working on a lock-free, async spsc channel in s2n-quic and wanted to write a kani proof for it. I have a harness written that simply allocates the channel. After running Kani, I get a panic inside the kani-driver crate:

...snip...
Runtime Symex: 1.36531s
size of program expression: 83108 steps
slicing removed 47540 assignments
Generated 4442 VCC(s), 2676 remaining after simplification
Runtime Postprocess Equation: 0.0723243s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.339988s
Running propositional reduction
Post-processing
Runtime Post-process: 1.14201s
Solving with MiniSAT 2.2.1 with simplifier
672691 variables, 3828307 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 70.2977s
Runtime decision procedure: 70.6452s
Running propositional reduction
Solving with MiniSAT 2.2.1 with simplifier
672691 variables, 1113105 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.0784595s
Runtime decision procedure: 0.0795185s
Running propositional reduction
Solving with MiniSAT 2.2.1 with simplifier
672691 variables, 1111673 clauses
SAT checker: instance is UNSATISFIABLE
Runtime Solver: 5.03282s
Runtime decision procedure: 5.04014s
thread '<unnamed>' panicked at 'called `Result::unwrap()` on an `Err` value: Error("data did not match any variant of untagged enum ParserItem", line: 0, column: 0)', kani-driver/src/cbmc_output_parser.rs:425:21
stack backtrace:
   0: rust_begin_unwind
   1: core::panicking::panic_fmt
   2: core::result::unwrap_failed
   3: <kani_driver::cbmc_output_parser::Parser as core::iter::traits::iterator::Iterator>::next
   4: <alloc::vec::Vec<T> as alloc::vec::spec_from_iter::SpecFromIter<T,I>>::from_iter
   5: kani_driver::cbmc_output_parser::process_cbmc_output
   6: kani_driver::harness_runner::<impl kani_driver::session::KaniSession>::check_harness
   7: core::ops::function::impls::<impl core::ops::function::FnOnce<A> for &mut F>::call_once
   8: <alloc::vec::Vec<T,A> as alloc::vec::spec_extend::SpecExtend<T,I>>::spec_extend
   9: rayon::iter::plumbing::bridge_producer_consumer::helper
  10: <rayon::iter::plumbing::bridge::Callback<C> as rayon::iter::plumbing::ProducerCallback<I>>::callback
  11: rayon::iter::from_par_iter::collect_extended
  12: rayon::iter::ParallelIterator::collect
  13: std::panic::catch_unwind
  14: <rayon_core::job::StackJob<L,F,R> as rayon_core::job::Job>::execute
  15: rayon_core::registry::WorkerThread::wait_until_cold
  16: rayon_core::registry::ThreadBuilder::run

To reproduce, you can run the following command:

$ git clone --branch camshaft/spsc https://github.com/aws/s2n-quic.git
$ cd s2n-quic/quic/s2n-quic-core
$ RUST_BACKTRACE=1 RUSTFLAGS="--cfg kani_slow" cargo kani --harness alloc_test --tests

with Kani version: 0.20

[adpaco-aws]

The CBMC postprocessor cannot parse one item for some (still unknown) reason. Unfortunately, the item it cannot parse is "result", which contains all the properties checked in the program, including traces if their status is "FAILURE" (this is the largest part of CBMC's output).

I've extracted the item but cannot upload it here due to the size limit (25MB, the item is 33MB). Since we're doing parsing on untagged items, I'm not getting useful information about what went wrong during parsing. In total, there are 1086 properties (1064 successful, 22 failed).

[adpaco-aws]

I'm using jq to determine if there is a missing field in a programmatic way, but it appears they're all there. I'll continue debugging tomorrow with another approach.

[adpaco-aws]

To be clear, the error message we get when doing on untagged items is "data did not match any variant of untagged enum ParserItem".

What I've tried now is to specialize parsing for the "result" item, by deserializing into a struct rather than a variant of ParserItem (both are still equivalent). This has achieved a more informative error:

Error("invalid value: integer `960`, expected u8", line: 23367, column: 26)

The line in question is marked below ("width" field):

            "stepType": "assignment",
            "thread": 0,
            "value": {
              "binary": "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
              "data": "0",
              "name": "integer",
              "type": "unsigned __CPROVER_bitvector[960]",
              "width": 960 # <--- this line
            }

It wasn't clear to me why serde_json was expecting a u8 value there, but I recall concrete playback defined width to be u8. Going to check that code now.

[adpaco-aws]

It's an easy fix. That said, I'm adding some code to get more informative errors in the future.