Crash in CBMC output parser with aws-lc-sys crate

[zhassan-aws]

Steps to reproduce:

1. cargo new foo
2. cd foo
3. cargo add aws-lc-sys
4. Put the following in src/main.rs:

use aws_lc_sys::RAND_bytes;

#[kani::proof]
fn foo() {
    let mut buf = [0u8; 1];
    let _ = unsafe { RAND_bytes(&mut buf as *mut u8, 1) };
}

fn main() {}

5. Run cargo kani

with Kani version: 3ea62b5

I expected to see this happen: Verification failed due to call to foreign C function.

Instead, this happened:

$ cargo kani
Kani Rust Verifier 0.56.0 (cargo plugin)
   Compiling libc v0.2.161
   Compiling shlex v1.3.0
   Compiling paste v1.0.15
   Compiling dunce v1.0.5
   Compiling fs_extra v1.3.0
   Compiling jobserver v0.1.32
   Compiling cc v1.1.34
   Compiling cmake v0.1.51
   Compiling aws-lc-sys v0.22.0
   Compiling foo v0.1.0 (/home/ubuntu/examples/tmp/foo)
warning: Found the following unsupported constructs:
             - foreign function (1)
         
         Verification will fail if one or more of these constructs is reachable.
         See https://model-checking.github.io/kani/rust-feature-support.html for more details.

    Finished `dev` profile [unoptimized + debuginfo] target(s) in 7.54s
Checking harness foo...
CBMC 6.3.1 (cbmc-6.3.1)
CBMC version 6.3.1 (cbmc-6.3.1) 64-bit x86_64 linux
Reading GOTO program from file /home/ubuntu/examples/tmp/foo/target/kani/x86_64-unknown-linux-gnu/debug/deps/foo-bd670bc017fbc03f__RNvCs1mm3qvRecAw_3foo3foo.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
aborting path on assume(false) at file /home/ubuntu/.cargo/registry/src/index.crates.io-6f17d22bba15001f/aws-lc-sys-0.22.0/src/x86_64_unknown_linux_gnu_crypto.rs line 26929 column 5 function foo thread 0
Runtime Symex: 0.00084355s
size of program expression: 37 steps
slicing removed 23 assignments
Generated 1 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 1.8081e-05s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.000134294s
Running propositional reduction
Post-processing
Runtime Post-process: 6.23e-06s
Solving with CaDiCaL 2.0.0
66 variables, 66 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 5.6502e-05s
Runtime decision procedure: 0.000236986s
thread '<unnamed>' panicked at kani-driver/src/cbmc_output_parser.rs:462:25:
called `Result::unwrap()` on an `Err` value: Error("control character (\\u0000-\\u001F) found while parsing a string", line: 4, column: 57)
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

[zhassan-aws]

Running with --output-format=old reveals that one of the functions has a unicode character in its name:

[foo.unsupported_construct.1] line 26929 call to foreign "C" function `�aws_lc_0_22_0_RAND_bytes` is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/2423: FAILURE

which the output parser is not expecting.

[zhassan-aws]

This is the source code of the function: https://docs.rs/aws-lc-sys/0.22.0/src/aws_lc_sys/x86_64_unknown_linux_gnu_crypto.rs.html#26929

It has a link_name attribute with a unicode character.

[zhassan-aws]

Here's a standalone reproducer without any dependencies:

extern "C" {
    #[link_name = "\u{1}f"]
    fn f() -> u32;
}

#[kani::proof]
fn main() {
    assert!(unsafe { f() == 1000 });
}

[justsmth]

For context, this is due to how rust-bindgen generates bindings for aws-lc-sys. There is an open issue related to it here: rust-lang/rust-bindgen#2935

[zhassan-aws]

Ah, thanks for providing the background!