Merge branch 'main' into fix-iss2857

.github/workflows/cbmc-latest.yml

@@ -38,14 +38,24 @@ jobs:
  repository: diffblue/cbmc
  path: cbmc
 
- - name: Build CBMC
+ - name: Build CBMC (Linux)
+ if: ${{ startsWith(matrix.os, 'ubuntu') }}
  working-directory: ./cbmc
  run: |
  cmake -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical"
  cmake --build build -- -j 4
  # Prepend the bin directory to $PATH
  echo "${GITHUB_WORKSPACE}/cbmc/build/bin" >> $GITHUB_PATH
 
+ - name: Build CBMC (macOS)
+ if: ${{ startsWith(matrix.os, 'macos') }}
+ working-directory: ./cbmc
+ run: |
+ cmake -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical" -DCMAKE_CXX_COMPILER=$(which clang++)
+ cmake --build build -- -j 4
+ # Prepend the bin directory to $PATH
+ echo "${GITHUB_WORKSPACE}/cbmc/build/bin" >> $GITHUB_PATH
+
  - name: Execute Kani regressions
  working-directory: ./kani
  run: ./scripts/kani-regression.sh

Cargo.lock

@@ -288,6 +288,27 @@ dependencies = [
  "winapi",
 ]
 
+[[package]]
+name = "csv"
+version = "1.3.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ac574ff4d437a7b5ad237ef331c17ccca63c46479e5b5453eb8e10bb99a759fe"
+dependencies = [
+ "csv-core",
+ "itoa",
+ "ryu",
+ "serde",
+]
+
+[[package]]
+name = "csv-core"
+version = "0.1.11"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5efa2b3d7902f4b634a20cae3c9c4e6209dc4779feb6863329607560143efa70"
+dependencies = [
+ "memchr",
+]
+
 [[package]]
 name = "either"
 version = "1.13.0"
@@ -892,6 +913,16 @@ dependencies = [
  "winapi-util",
 ]
 
+[[package]]
+name = "scanner"
+version = "0.0.0"
+dependencies = [
+ "csv",
+ "serde",
+ "strum",
+ "strum_macros",
+]
+
 [[package]]
 name = "scopeguard"
 version = "1.2.0"

Cargo.toml

@@ -40,6 +40,7 @@ members = [
  "library/std",
  "tools/compiletest",
  "tools/build-kani",
+ "tools/scanner",
  "kani-driver",
  "kani-compiler",
  "kani_metadata",

cprover_bindings/src/env.rs

@@ -8,7 +8,7 @@
 //! c.f. CBMC code [src/ansi-c/ansi_c_internal_additions.cpp].
 //! One possible invocation of this insertion in CBMC can be found in \[ansi_c_languaget::parse\].
 
-use super::goto_program::{Expr, Location, Symbol, Type};
+use super::goto_program::{Expr, Location, Symbol, SymbolTable, Type};
 use super::MachineModel;
 use num::bigint::BigInt;
 fn int_constant<T>(name: &str, value: T) -> Symbol
@@ -71,6 +71,8 @@ pub fn machine_model_symbols(mm: &MachineModel) -> Vec<Symbol> {
  ]
 }
 
+const DEAD_OBJECT_IDENTIFIER: &str = "__CPROVER_dead_object";
+
 pub fn additional_env_symbols() -> Vec<Symbol> {
  vec![
  Symbol::builtin_function("__CPROVER_initialize", vec![], Type::empty()),
@@ -82,5 +84,16 @@ pub fn additional_env_symbols() -> Vec<Symbol> {
  Location::none(),
  )
  .with_is_extern(true),
+ Symbol::static_variable(
+ DEAD_OBJECT_IDENTIFIER,
+ DEAD_OBJECT_IDENTIFIER,
+ Type::void_pointer(),
+ Location::none(),
+ )
+ .with_is_extern(true),
  ]
 }
+
+pub fn global_dead_object(symbol_table: &SymbolTable) -> Expr {
+ symbol_table.lookup(DEAD_OBJECT_IDENTIFIER).unwrap().to_expr()
+}

cprover_bindings/src/irep/goto_binary_serde.rs

@@ -11,7 +11,7 @@ use std::io::{self, BufReader};
 use std::io::{BufWriter, Bytes, Error, ErrorKind, Read, Write};
 use std::path::Path;
 
-/// Writes a symbol table to a file in goto binary format in version 5.
+/// Writes a symbol table to a file in goto binary format in version 6.
 ///
 /// In CBMC, the serialization rules are defined in :
 /// - src/goto-programs/write_goto_binary.h
@@ -26,7 +26,7 @@ pub fn write_goto_binary_file(filename: &Path, source: &crate::goto_program::Sym
  serializer.write_file(irep_symbol_table);
 }
 
-/// Reads a symbol table from a file expected to be in goto binary format in version 5.
+/// Reads a symbol table from a file expected to be in goto binary format in version 6.
 //
 /// In CBMC, the deserialization rules are defined in :
 /// - src/goto-programs/read_goto_binary.h
@@ -540,7 +540,7 @@ where
  assert!(written == 4);
 
  // Write goto binary version
- self.write_usize_varenc(5);
+ self.write_usize_varenc(6);
  }
 
  /// Writes the symbol table using the GOTO binary file format to the byte stream.
@@ -921,12 +921,12 @@ where
 
  // Read goto binary version
  let goto_binary_version = self.read_usize_varenc()?;
- if goto_binary_version != 5 {
+ if goto_binary_version != 6 {
  return Err(Error::new(
  ErrorKind::Other,
  format!(
  "Unsupported GOTO binary version: {}. Supported version: {}",
- goto_binary_version, 5
+ goto_binary_version, 6
  ),
  ));
  }

cprover_bindings/src/irep/irep_id.rs

@@ -366,7 +366,7 @@ pub enum IrepId {
  Div,
  Power,
  FactorialPower,
- PrettyName,
+ CPrettyName,
  CClass,
  CField,
  CInterface,
@@ -1242,7 +1242,7 @@ impl Display for IrepId {
  IrepId::Div => "/",
  IrepId::Power => "**",
  IrepId::FactorialPower => "factorial_power",
- IrepId::PrettyName => "pretty_name",
+ IrepId::CPrettyName => "#pretty_name",
  IrepId::CClass => "#class",
  IrepId::CField => "#field",
  IrepId::CInterface => "#interface",

cprover_bindings/src/irep/to_irep.rs

@@ -132,7 +132,7 @@ impl ToIrep for DatatypeComponent {
  match self {
  DatatypeComponent::Field { name, typ } => Irep::just_named_sub(linear_map![
  (IrepId::Name, Irep::just_string_id(name.to_string())),
- (IrepId::PrettyName, Irep::just_string_id(name.to_string())),
+ (IrepId::CPrettyName, Irep::just_string_id(name.to_string())),
  (IrepId::Type, typ.to_irep(mm)),
  ]),
  DatatypeComponent::Padding { name, bits } => Irep::just_named_sub(linear_map![

cprover_bindings/src/lib.rs

@@ -33,6 +33,7 @@
 #![feature(f16)]
 
 mod env;
+pub use env::global_dead_object;
 pub mod goto_program;
 pub mod irep;
 mod machine_model;

docs/src/SUMMARY.md

@@ -12,12 +12,13 @@
  - [Failures that Kani can spot](./tutorial-kinds-of-failure.md)
  - [Loop unwinding](./tutorial-loop-unwinding.md)
  - [Nondeterministic variables](./tutorial-nondeterministic-variables.md)
- - [Debugging verification failures](./debugging-verification-failures.md)
 
 - [Reference](./reference.md)
  - [Attributes](./reference/attributes.md)
- - [Stubbing](./reference/stubbing.md)
-
+ - [Experimental features](./reference/experimental/experimental-features.md)
+ - [Coverage](./reference/experimental/coverage.md)
+ - [Stubbing](./reference/experimental/stubbing.md)
+ - [Concrete Playback](./reference/experimental/concrete-playback.md)
 - [Application](./application.md)
  - [Comparison with other tools](./tool-comparison.md)
  - [Where to start on real code](./tutorial-real-code.md)

docs/src/reference/attributes.md

@@ -60,7 +60,7 @@ For example, the class in `Check 1: my_harness.assertion.1` is `assertion`, so t
 
 > **NOTE**: The `#[kani::should_panic]` is only recommended for writing
 > harnesses which complement existing harnesses that don't use the same
-> attribute. In order words, it's only recommended to write *negative harnesses*
+> attribute. In other words, it's only recommended to write *negative harnesses*
 > after having written *positive* harnesses that successfully verify interesting
 > properties about the function under verification.
 

docs/src/debugging-verification-failures.md → docs/src/reference/experimental/concrete-playback.md

@@ -1,20 +1,13 @@
-# Debugging verification failures
+# Concrete Playback
 
-When the result of a certain check comes back as a `FAILURE`,
-Kani offers different options to help debug:
-* `--concrete-playback`. This _experimental_ feature generates a Rust unit test case that plays back a failing
-proof harness using a concrete counterexample.
-* `--visualize`. This feature generates an HTML text-based trace that
-enumerates the execution steps leading to the check failure.
-
-## Concrete playback
+When the result of a certain check comes back as a `FAILURE`, Kani offers the `concrete-playback` option to help debug. This feature generates a Rust unit test case that plays back a failing proof harness using a concrete counterexample.
 
 When concrete playback is enabled, Kani will generate unit tests for assertions that failed during verification,
 as well as cover statements that are reachable.
 
 These tests can then be executed using Kani's playback subcommand.
 
-### Usage
+## Usage
 
 In order to enable this feature, run Kani with the `-Z concrete-playback --concrete-playback=[print|inplace]` flag.
 After getting a verification failure, Kani will generate a Rust unit test case that plays back a failing
@@ -46,7 +39,7 @@ The output will have a line in the beginning like
 
 You can further debug the binary with tools like `rust-gdb` or `lldb`.
 
-### Example
+## Example
 
 Running `kani -Z concrete-playback --concrete-playback=print` on the following source file:
 ```rust
@@ -75,15 +68,15 @@ Here, `133` and `35207` are the concrete values that, when substituted for `a` a
 cause an assertion failure.
 `vec![135, 137]` is the byte array representation of `35207`.
 
-### Request for comments
+## Request for comments
 
 This feature is experimental and is therefore subject to change.
 If you have ideas for improving the user experience of this feature,
 please add them to [this GitHub issue](https://github.com/model-checking/kani/issues/1536).
 We are tracking the existing feature requests in
 [this GitHub milestone](https://github.com/model-checking/kani/milestone/10).
 
-### Limitations 
+## Limitations 
 
 * This feature does not generate unit tests for failing non-panic checks (e.g., UB checks).
 This is because checks would not trigger runtime errors during concrete playback.

docs/src/reference/experimental/coverage.md

@@ -0,0 +1,32 @@
+## Coverage
+
+Recall our `estimate_size` example from [First steps](../../tutorial-first-steps.md),
+where we wrote a proof harness constraining the range of inputs to integers less than 4096:
+
+```rust
+{{#include ../../tutorial/first-steps-v2/src/lib.rs:kani}}
+```
+
+We must wonder if we've really fully tested our function.
+What if we revise the function, but forget to update the assumption in our proof harness to cover the new range of inputs?
+
+Fortunately, Kani is able to report a coverage metric for each proof harness.
+In the `first-steps-v2` directory, try running:
+
+```
+cargo kani --coverage -Z line-coverage --harness verify_success
+```
+
+which verifies the harness, then prints coverage information for each line.
+In this case, we see that each line of `estimate_size` is followed by `FULL`, indicating that our proof harness provides full coverage.
+
+Try changing the assumption in the proof harness to `x < 2048`.
+Now the harness won't be testing all possible cases.
+Rerun the command.
+You'll see this line:
+
+```
+src/lib.rs, 24, NONE
+```
+
+which indicates that the proof no longer covers line 24, which addresses the case where `x >= 2048`.

docs/src/reference/experimental/experimental-features.md

@@ -0,0 +1,5 @@
+# Experimental Features
+
+We elaborate on some of the more commonly used experimental features in Kani.
+This is not an exhaustive list; to see all of Kani's experimental features, run `cargo kani --help`.
+To use an experimental feature, invoke Kani with the `--unstable` or `-Z` flag followed by the name of the feature.

docs/src/reference/stubbing.md → docs/src/reference/experimental/stubbing.md

@@ -113,7 +113,7 @@ In the following, we describe all the limitations of the stubbing feature.
 The usage of stubbing is limited to the verification of a single harness.
 Therefore, users are **required to pass the `--harness` option** when using the stubbing feature.
 
-In addition, this feature **isn't compatible with [concrete playback](../debugging-verification-failures.md#concrete-playback)**.
+In addition, this feature **isn't compatible with [concrete playback](./concrete-playback.md)**.
 
 ### Support
 

docs/src/tutorial-first-steps.md

@@ -53,40 +53,11 @@ Kani has immediately found a failure.
 Notably, we haven't had to write explicit assertions in our proof harness: by default, Kani will find a host of erroneous conditions which include a reachable call to `panic` or a failing `assert`.
 If Kani had run successfully on this harness, this amounts to a mathematical proof that there is no input that could cause a panic in `estimate_size`.
 
-### Getting a trace
+> By default, Kani only reports failures, not how the failure happened.
+> In this example, it would be nice to get a concrete example of a value of `x` that triggers the failure.
+> Kani offers an (experimental) [concrete playback](reference/experimental/concrete-playback.md) feature that serves this purpose.
+> As an exercise, try applying concrete playback to this example and see what Kani outputs.
 
-By default, Kani only reports failures, not how the failure happened.
-In this running example, it seems obvious what we're interested in (the value of `x` that caused the failure) because we just have one unknown input at the start (similar to the property test), but that's kind of a special case.
-In general, understanding how a failure happened requires exploring a full (potentially large) _execution trace_.
-
-An execution trace is a record of exactly how a failure can occur.
-Nondeterminism (like a call to `kani::any()`, which could return any value) can appear in the middle of its execution.
-A trace is a record of exactly how execution proceeded, including concrete choices (like `1023`) for all of these nondeterministic values.
-
-To get a trace for a failing check in Kani, run:
-
-```
-cargo kani --visualize --enable-unstable
-```
-
-This command runs Kani and generates an HTML report that includes a trace.
-Open the report with your preferred browser.
-Under the "Errors" heading, click on the "trace" link to find the trace for this failure.
-
-From this trace report, we can filter through it to find relevant lines.
-A good rule of thumb is to search for either `kani::any()` or assignments to variables you're interested in.
-At present time, an unfortunate amount of generated code is present in the trace.
-This code isn't a part of the Rust code you wrote, but is an internal implementation detail of how Kani runs proof harnesses.
-Still, searching for `kani::any()` quickly finds us these lines:
-
-```
-let x: u32 = kani::any();
-x = 1023u
-```
-
-Here we're seeing the line of code and the value assigned in this particular trace.
-Like property testing, this is just one **example** of a failure.
-To proceed, we recommend fixing the code to avoid this particular issue and then re-running Kani to see if you find more issues.
 
 ### Exercise: Try other failures
 
@@ -193,32 +164,11 @@ Here's a revised example of the proof harness, one that now succeeds:
 {{#include tutorial/first-steps-v2/src/lib.rs:kani}}
 ```
 
-But now we must wonder if we've really fully tested our function.
-What if we revise the function, but forget to update the assumption in our proof harness to cover the new range of inputs?
-
-Fortunately, Kani is able to report a coverage metric for each proof harness.
-Try running:
-
-```
-cargo kani --visualize --harness verify_success
-```
-
-The beginning of the report includes coverage information.
-Clicking through to the file will show fully-covered lines in green.
-Lines not covered by our proof harness will show in red.
-
-Try changing the assumption in the proof harness to `x < 2048`.
-Now the harness won't be testing all possible cases.
-Rerun `cargo kani --visualize`.
-Look at the report: you'll see we no longer have 100% coverage of the function.
-
 ## Summary
 
 In this section:
 
 1. We saw Kani find panics, assertion failures, and even some other failures like unsafe dereferencing of null pointers.
 2. We saw Kani find failures that testing could not easily find.
 3. We saw how to write a proof harness and use `kani::any()`.
-4. We saw how to get a failing **trace** using `kani --visualize`
-5. We saw how proof harnesses are used to set up preconditions with `kani::assume()`.
-6. We saw how to obtain **coverage** metrics and use them to ensure our proofs are covering as much as they should be.
+4. We saw how proof harnesses are used to set up preconditions with `kani::assume()`.