Kani not propagating goto-cc error code.

[YoshikiTakashima]

I tried this code: https://github.com/tokio-rs/prost.git
(commit 25d50ad325682cbc090fdc82686a03e52d4d4277)

using the following command line invocation:

cargo kani --workspace --all-features

with Kani version: 0.8 commit 90330b2

I expected to see this happen: If gotocc failed, then Kani should give nonzero error code

Instead, this happened: Message shows goto-cc failure, but kani-driver
is giving exit code 0.

This goes against UNIX standards, and will provide negative
experiences for customers who are using Kani via a script.

Suggested method of correction: propagate goto-cc's exit code as
cargo-kani's exit code when it is nonzero.

[YoshikiTakashima]

@adpaco-aws This issue has the risk of making stats over-optimistic wrt to milestone "Code generation succeeds on at least 80% of top 100 crates"

Until it is fixed, have the script look at the STDOUT/ERR. Exit code cannot be trusted.

[adpaco-aws]

Thanks @YoshikiTakashima , I wasn't aware of this issue but that explains why stats are not affected in #1585. Are you looking into this or should I take it?

[YoshikiTakashima]

@adpaco-aws I am not looking into it right now. All of my time is taken up with #1312 and #1587

[adpaco-aws]

I haven't been able to reproduce this issue in my environment (Kani commit 42bfc94, Ubuntu 20.04). Running the same command on the same commit you posted gets me the following error:

[BUNCH OF WARNINGS]
   Compiling tests v0.0.0 (/home/ubuntu/prost/tests)
   Compiling tests-2015 v0.0.0 (/home/ubuntu/prost/tests-2015)
   Compiling tests-no-std v0.0.0 (/home/ubuntu/prost/tests-no-std)
error: failed to run custom build command for `tests-no-std v0.0.0 (/home/ubuntu/prost/tests-no-std)`

Caused by:
  process didn't exit successfully: `/home/ubuntu/prost/target/debug/build/tests-no-std-ac8c37a7962eca64/build-script-build` (exit status: 101)
  --- stdout
  Running: "/usr/bin/protoc" "--include_imports" "--include_source_info" "-o" "/home/ubuntu/prost/target/x86_64-unknown-linux-gnu/debug/build/tests-no-std-de493d75f783c634/out/file_descriptor_set.bin" "-I" "../tests/src" "../tests/src/ident_conversion.proto"
  Running: "/usr/bin/protoc" "--include_imports" "--include_source_info" "-o" "/home/ubuntu/prost/target/x86_64-unknown-linux-gnu/debug/build/tests-no-std-de493d75f783c634/out/file_descriptor_set.bin" "-I" "../tests/src" "../tests/src/nesting.proto"
  Running: "/usr/bin/protoc" "--include_imports" "--include_source_info" "-o" "/home/ubuntu/prost/target/x86_64-unknown-linux-gnu/debug/build/tests-no-std-de493d75f783c634/out/file_descriptor_set.bin" "-I" "../tests/src" "../tests/src/recursive_oneof.proto"
  Running: "/usr/bin/protoc" "--include_imports" "--include_source_info" "-o" "/home/ubuntu/prost/target/x86_64-unknown-linux-gnu/debug/build/tests-no-std-de493d75f783c634/out/file_descriptor_set.bin" "-I" "../tests/src" "../tests/src/custom_attributes.proto"
  Running: "/usr/bin/protoc" "--include_imports" "--include_source_info" "-o" "/home/ubuntu/prost/target/x86_64-unknown-linux-gnu/debug/build/tests-no-std-de493d75f783c634/out/file_descriptor_set.bin" "-I" "../tests/src" "../tests/src/oneof_attributes.proto"
  Running: "/usr/bin/protoc" "--include_imports" "--include_source_info" "-o" "/home/ubuntu/prost/target/x86_64-unknown-linux-gnu/debug/build/tests-no-std-de493d75f783c634/out/file_descriptor_set.bin" "-I" "../tests/src" "../tests/src/no_unused_results.proto"
  Running: "/usr/bin/protoc" "--include_imports" "--include_source_info" "-o" "/home/ubuntu/prost/target/x86_64-unknown-linux-gnu/debug/build/tests-no-std-de493d75f783c634/out/file_descriptor_set.bin" "-I" "../tests/src" "../tests/src/default_enum_value.proto"
  Running: "/usr/bin/protoc" "--include_imports" "--include_source_info" "-o" "/home/ubuntu/prost/target/x86_64-unknown-linux-gnu/debug/build/tests-no-std-de493d75f783c634/out/file_descriptor_set.bin" "-I" "../tests/src" "../tests/src/groups.proto"
  Running: "/usr/bin/protoc" "--include_imports" "--include_source_info" "-o" "/home/ubuntu/prost/target/x86_64-unknown-linux-gnu/debug/build/tests-no-std-de493d75f783c634/out/file_descriptor_set.bin" "-I" "../tests/src" "../tests/src/deprecated_field.proto"
  Running: "/usr/bin/protoc" "--include_imports" "--include_source_info" "-o" "/home/ubuntu/prost/target/x86_64-unknown-linux-gnu/debug/build/tests-no-std-de493d75f783c634/out/file_descriptor_set.bin" "-I" "../tests/src" "../tests/src/default_string_escape.proto"
  Running: "/usr/bin/protoc" "--include_imports" "--include_source_info" "-o" "/tmp/prost-buildXwkx3w/prost-descriptor-set" "-I" "../tests/src" "--experimental_allow_proto3_optional" "../tests/src/proto3_presence.proto"

  --- stderr
  thread 'main' panicked at 'called `Result::unwrap()` on an `Err` value: Custom { kind: Other, error: "protoc failed: Unknown flag: --experimental_allow_proto3_optional\n" }', tests-no-std/../tests/src/build.rs:96:10
  note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
warning: build failed, waiting for other jobs to finish...
error: failed to run custom build command for `tests v0.0.0 (/home/ubuntu/prost/tests)`
[MORE ERRORS LIKE THIS, ALL PROPAGATE EXIT CODE 101]

In addition, I examined the stdout & stderr of the top100 crates experiment and couldn't find any error related to goto-cc. Are you running this on macOS? Can you post the error message you got from goto-cc if you have it?

[YoshikiTakashima]

@adpaco-aws I've confirmed that kani's issues WRT prost is fixed.

Let us replicate a different way, we will force it to fail using a fake goto-cc that will always fail.

ytakashl@3c063046a79c kani-driver % grep -rn '"goto-cc"'
./src/call_goto_cc.rs:37:        let mut cmd = Command::new("goto-cc");
./src/call_goto_cc.rs:52:        let mut cmd = Command::new("goto-cc");

Change to

./src/call_goto_cc.rs:37:        let mut cmd = Command::new("false");
./src/call_goto_cc.rs:52:        let mut cmd = Command::new("false");

Replicated using:

ytakashl@3c063046a79c ~ % cargo build --workspace
ytakashl@3c063046a79c ~ % cd tests/cargo-kani/ws-flag
ytakashl@3c063046a79c ws-flag % cargo kani --only-codegen
   Compiling ws-flag v0.1.0 (/Users/ytakashl/Desktop/kani/tests/cargo-kani/ws-flag)
   Compiling libcrate v0.1.0 (/Users/ytakashl/Desktop/kani/tests/cargo-kani/ws-flag/libcrate)
    Finished dev [unoptimized + debuginfo] target(s) in 0.30s
ytakashl@3c063046a79c ws-flag % echo $?
0

[tedinski]

--only-codegen doesn't call goto-cc

[adpaco-aws]

--only-codegen doesn't call goto-cc

Right, --only-codegen stops after running symtab2gb on the project files since #1585.

Closing this because issues with prost are fixed now.