From 21f4af94201eaf412ed7802892721ebcbd539558 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 7 Oct 2024 17:46:25 -0400 Subject: [PATCH 1/6] Fix issue when linking rlib + another library type (#3576) Invoking the native linker was overriding the `json` we create in Kani's compiler. Thus, invoke the native linker first, then create the `json` files. Resolves #3569 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- .../compiler_interface.rs | 21 +++++++++---------- .../cdylib-rlib/Cargo.toml | 13 ++++++++++++ .../supported-lib-types/cdylib-rlib/expected | 2 ++ 3 files changed, 25 insertions(+), 11 deletions(-) create mode 100644 tests/cargo-ui/supported-lib-types/cdylib-rlib/Cargo.toml create mode 100644 tests/cargo-ui/supported-lib-types/cdylib-rlib/expected diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 85117b6a2974..da211c58946c 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -403,13 +403,7 @@ impl CodegenBackend for GotocCodegenBackend { /// We need to emit `rlib` files normally if requested. Cargo expects these in some /// circumstances and sends them to subsequent builds with `-L`. /// - /// We CAN NOT invoke the native linker, because that will fail. We don't have real objects. - /// What determines whether the native linker is invoked or not is the set of `crate_types`. - /// Types such as `bin`, `cdylib`, `dylib` will trigger the native linker. - /// - /// Thus, we manually build the rlib file including only the `rmeta` file. - /// - /// For cases where no metadata file was requested, we stub the file requested by writing the + /// For other crate types, we stub the file requested by writing the /// path of the `kani-metadata.json` file so `kani-driver` can safely find the latest metadata. /// See for more details. fn link( @@ -419,6 +413,14 @@ impl CodegenBackend for GotocCodegenBackend { outputs: &OutputFilenames, ) -> Result<(), ErrorGuaranteed> { let requested_crate_types = &codegen_results.crate_info.crate_types; + // Create the rlib if one was requested. + if requested_crate_types.iter().any(|crate_type| *crate_type == CrateType::Rlib) { + link_binary(sess, &ArArchiveBuilderBuilder, &codegen_results, outputs)?; + } + + // But override all the other outputs. + // Note: Do this after `link_binary` call, since it may write to the object files + // and override the json we are creating. for crate_type in requested_crate_types { let out_fname = out_filename( sess, @@ -428,10 +430,7 @@ impl CodegenBackend for GotocCodegenBackend { ); let out_path = out_fname.as_path(); debug!(?crate_type, ?out_path, "link"); - if *crate_type == CrateType::Rlib { - // Emit the `rlib` that contains just one file: `.rmeta` - link_binary(sess, &ArArchiveBuilderBuilder, &codegen_results, outputs)? - } else { + if *crate_type != CrateType::Rlib { // Write the location of the kani metadata file in the requested compiler output file. let base_filepath = outputs.path(OutputType::Object); let base_filename = base_filepath.as_path(); diff --git a/tests/cargo-ui/supported-lib-types/cdylib-rlib/Cargo.toml b/tests/cargo-ui/supported-lib-types/cdylib-rlib/Cargo.toml new file mode 100644 index 000000000000..fcf91e061e57 --- /dev/null +++ b/tests/cargo-ui/supported-lib-types/cdylib-rlib/Cargo.toml @@ -0,0 +1,13 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +[package] +name = "supported-lib" +version = "0.1.0" +edition = "2021" +description = "Test that Kani correctly handle supported crate types" + +[lib] +name = "lib" +crate-type = ["cdylib", "rlib"] +path = "../src/lib.rs" + diff --git a/tests/cargo-ui/supported-lib-types/cdylib-rlib/expected b/tests/cargo-ui/supported-lib-types/cdylib-rlib/expected new file mode 100644 index 000000000000..426470e8702c --- /dev/null +++ b/tests/cargo-ui/supported-lib-types/cdylib-rlib/expected @@ -0,0 +1,2 @@ +Checking harness check_ok... +VERIFICATION:- SUCCESSFUL From 91044db940d11193a75bef8414f65f1fd5832503 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 8 Oct 2024 07:16:12 -0700 Subject: [PATCH 2/6] Running `verify-std` no longer changes Cargo files (#3577) In order to create a dummy crate we were using `cargo init` command. However, this command will interact with any existing workspace. Instead, explicitly create a dummy `Cargo.toml` and `src/lib.rs`. Resolves #3574 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- kani-driver/src/call_cargo.rs | 35 +++++++++++++++-- .../verify_std_cmd/verify_std.expected | 4 ++ .../verify_std_cmd/verify_std.sh | 39 ++++++++++++++++--- 3 files changed, 69 insertions(+), 9 deletions(-) diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index 191b104a8c1c..bc0e9d8361d7 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -46,10 +46,39 @@ pub struct CargoOutputs { impl KaniSession { /// Create a new cargo library in the given path. + /// + /// Since we cannot create a new workspace with `cargo init --lib`, we create the dummy + /// crate manually. =( See . + /// + /// Without setting up a new workspace, cargo init will modify the workspace where this is + /// running. See for details. pub fn cargo_init_lib(&self, path: &Path) -> Result<()> { - let mut cmd = setup_cargo_command()?; - cmd.args(["init", "--lib", path.to_string_lossy().as_ref()]); - self.run_terminal(cmd) + let toml_path = path.join("Cargo.toml"); + if toml_path.exists() { + bail!("Cargo.toml already exists in {}", path.display()); + } + + // Create folder for library + fs::create_dir_all(path.join("src"))?; + + // Create dummy crate and write dummy body + let lib_path = path.join("src/lib.rs"); + fs::write(&lib_path, "pub fn dummy() {}")?; + + // Create Cargo.toml + fs::write( + &toml_path, + r#"[package] +name = "dummy" +version = "0.1.0" + +[lib] +crate-type = ["lib"] + +[workspace] +"#, + )?; + Ok(()) } pub fn cargo_build_std(&self, std_path: &Path, krate_path: &Path) -> Result> { diff --git a/tests/script-based-pre/verify_std_cmd/verify_std.expected b/tests/script-based-pre/verify_std_cmd/verify_std.expected index 157adb94ba16..3c1f474af0e7 100644 --- a/tests/script-based-pre/verify_std_cmd/verify_std.expected +++ b/tests/script-based-pre/verify_std_cmd/verify_std.expected @@ -1,3 +1,7 @@ +[TEST] Only codegen inside library folder +No kani crate inside Cargo.toml as expected + + [TEST] Run kani verify-std Checking harness verify::dummy_proof... diff --git a/tests/script-based-pre/verify_std_cmd/verify_std.sh b/tests/script-based-pre/verify_std_cmd/verify_std.sh index 022e7b79de4a..e7276867a2a5 100755 --- a/tests/script-based-pre/verify_std_cmd/verify_std.sh +++ b/tests/script-based-pre/verify_std_cmd/verify_std.sh @@ -50,17 +50,44 @@ cp ${TMP_DIR}/library/std/src/lib.rs ${TMP_DIR}/std_lib.rs echo '#![cfg_attr(kani, feature(kani))]' > ${TMP_DIR}/library/std/src/lib.rs cat ${TMP_DIR}/std_lib.rs >> ${TMP_DIR}/library/std/src/lib.rs +# Test that the command works inside the library folder and does not change +# the existing workspace +# See https://github.com/model-checking/kani/issues/3574 +echo "[TEST] Only codegen inside library folder" +pushd "${TMP_DIR}/library" >& /dev/null +RUSTFLAGS="--cfg=uninit_checks" kani verify-std \ + -Z unstable-options \ + . \ + -Z function-contracts \ + -Z stubbing \ + -Z mem-predicates \ + --only-codegen +popd +# Grep should not find anything and exit status is 1. +grep -c kani ${TMP_DIR}/library/Cargo.toml \ + && echo "Unexpected kani crate inside Cargo.toml" \ + || echo "No kani crate inside Cargo.toml as expected" + echo "[TEST] Run kani verify-std" export RUST_BACKTRACE=1 -kani verify-std -Z unstable-options "${TMP_DIR}/library" \ - --target-dir "${TMP_DIR}/target" -Z function-contracts -Z stubbing \ +kani verify-std \ + -Z unstable-options \ + "${TMP_DIR}/library" \ + --target-dir "${TMP_DIR}/target" \ + -Z function-contracts \ + -Z stubbing \ -Z mem-predicates +# Test that uninit-checks basic setup works on a no-core library echo "[TEST] Run kani verify-std -Z uninit-checks" -export RUSTFLAGS="--cfg=uninit_checks" -kani verify-std -Z unstable-options "${TMP_DIR}/library" \ - --target-dir "${TMP_DIR}/target" -Z function-contracts -Z stubbing \ - -Z mem-predicates -Z uninit-checks +RUSTFLAGS="--cfg=uninit_checks" kani verify-std \ + -Z unstable-options \ + "${TMP_DIR}/library" \ + --target-dir "${TMP_DIR}/target" \ + -Z function-contracts \ + -Z stubbing \ + -Z mem-predicates \ + -Z uninit-checks # Cleanup rm -r ${TMP_DIR} From e7ab0903fb6c8da27b96d7148226d6808c1c2a86 Mon Sep 17 00:00:00 2001 From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Date: Tue, 8 Oct 2024 10:54:42 -0700 Subject: [PATCH 3/6] Add an LLBC backend (#3514) This PR adds a new codegen backend that generates low-level borrow calculus (LLBC), which is the format defined by [Charon](https://github.com/AeneasVerif/charon) and [Aeneas](https://github.com/AeneasVerif/aeneas). The backend can be invoked using `-Zaeneas`, and will generate a `.llbc` file. This file can then be passed to Aeneas to generate Lean for example. Currently, Aeneas needs to be manually run on the generated LLBC. The PR translates stable MIR to unstructured LLBC (ULLBC) and then uses the Charon library to apply transformations that reconstruct the control flow to regain some of the high-level structure (loops, if statements, etc.). In this PR, very few MIR constructs are handled, but the PR is already pretty big. More support to come in subsequent PRs. Call-outs: - Charon is currently not released on crates.io, so the library is added as a dependency through GitHub with a particular commit. - The Kani driver is currenty heavily tailored towards CBMC, so currently it's expecting a goto file, and thus errors out when the Aeneas backend is invoked. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- .github/workflows/deny.yml | 2 + .github/workflows/format-check.yml | 2 +- .github/workflows/kani.yml | 2 + .gitignore | 3 + .gitmodules | 3 + Cargo.lock | 1060 ++++++++++++++++- charon | 1 + deny.toml | 10 +- kani-compiler/Cargo.toml | 4 +- kani-compiler/src/args.rs | 26 +- .../codegen_aeneas_llbc/compiler_interface.rs | 411 +++++++ .../codegen_aeneas_llbc/mir_to_ullbc/mod.rs | 802 +++++++++++++ kani-compiler/src/codegen_aeneas_llbc/mod.rs | 10 + kani-compiler/src/kani_compiler.rs | 35 +- kani-compiler/src/main.rs | 2 + kani-driver/src/args/mod.rs | 29 + kani-driver/src/call_cargo.rs | 3 + kani-driver/src/call_single_file.rs | 19 +- kani_metadata/src/unstable.rs | 2 + rustfmt.toml | 1 + scripts/codegen-firecracker.sh | 2 +- scripts/std-lib-regression.sh | 2 +- tests/expected/llbc/basic0/expected | 8 + tests/expected/llbc/basic0/test.rs | 15 + tests/expected/llbc/basic1/expected | 15 + tests/expected/llbc/basic1/test.rs | 15 + 26 files changed, 2416 insertions(+), 68 deletions(-) create mode 160000 charon create mode 100644 kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs create mode 100644 kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs create mode 100644 kani-compiler/src/codegen_aeneas_llbc/mod.rs create mode 100644 tests/expected/llbc/basic0/expected create mode 100644 tests/expected/llbc/basic0/test.rs create mode 100644 tests/expected/llbc/basic1/expected create mode 100644 tests/expected/llbc/basic1/test.rs diff --git a/.github/workflows/deny.yml b/.github/workflows/deny.yml index 7ce00cabd2f9..a5db349f8abc 100644 --- a/.github/workflows/deny.yml +++ b/.github/workflows/deny.yml @@ -18,6 +18,8 @@ jobs: runs-on: ubuntu-latest steps: - uses: actions/checkout@v4 + with: + submodules: recursive - uses: EmbarkStudios/cargo-deny-action@v2 with: arguments: --all-features --workspace diff --git a/.github/workflows/format-check.yml b/.github/workflows/format-check.yml index cc13306a4eaf..81253f1a9790 100644 --- a/.github/workflows/format-check.yml +++ b/.github/workflows/format-check.yml @@ -47,7 +47,7 @@ jobs: - name: 'Run Clippy' run: | - cargo clippy --all -- -D warnings + cargo clippy --workspace --exclude charon --exclude macros --no-deps -- -D warnings - name: 'Print Clippy Statistics' run: | diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index a565c9cd4cbe..d8cb0fc2bb2d 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -98,6 +98,8 @@ jobs: steps: - name: Checkout Kani uses: actions/checkout@v4 + with: + submodules: recursive - name: Install book dependencies run: ./scripts/setup/ubuntu/install_doc_deps.sh diff --git a/.gitignore b/.gitignore index a2defc0df119..db10863e2b0f 100644 --- a/.gitignore +++ b/.gitignore @@ -77,6 +77,9 @@ package-lock.json ## Rustdoc GUI tests tests/rustdoc-gui/src/**.lock +## Charon/Aeneas LLBC files +*.llbc + # Before adding new lines, see the comment at the top. /.ninja_deps /.ninja_log diff --git a/.gitmodules b/.gitmodules index b02c263a898e..c7e25f120c95 100644 --- a/.gitmodules +++ b/.gitmodules @@ -5,3 +5,6 @@ path = tests/perf/s2n-quic url = https://github.com/aws/s2n-quic branch = main +[submodule "charon"] + path = charon + url = https://github.com/AeneasVerif/charon diff --git a/Cargo.lock b/Cargo.lock index 0cd3c1af05f4..41fb02073f6a 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2,6 +2,21 @@ # It is not intended for manual editing. version = 4 +[[package]] +name = "addr2line" +version = "0.24.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "dfbe277e56a376000877090da837660b4427aad530e3028d44e0bffe4f89a1c1" +dependencies = [ + "gimli", +] + +[[package]] +name = "adler2" +version = "2.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "512761e0bb2578dd7380c6baaa0f4ce03e84f95e960231d1dec8bf4d7d6e2627" + [[package]] name = "ahash" version = "0.8.11" @@ -24,6 +39,15 @@ dependencies = [ "memchr", ] +[[package]] +name = "ansi_term" +version = "0.12.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d52a9bb7ec0cf484c551830a7ce27bd20d67eac647e1befb56b0be4ee39a55d2" +dependencies = [ + "winapi", +] + [[package]] name = "anstream" version = "0.6.15" @@ -79,18 +103,122 @@ version = "1.0.89" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "86fdf8605db99b54d3cd748a44c6d04df638eb5dafb219b135d0149bd0db01f6" +[[package]] +name = "arrayvec" +version = "0.5.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "23b62fc65de8e4e7f52534fb52b0f3ed04746ae267519eef2a83941e8085068b" + +[[package]] +name = "arrayvec" +version = "0.7.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7c02d123df017efcdfbd739ef81735b36c5ba83ec3c59c80a9d7ecc718f92e50" + +[[package]] +name = "assert_cmd" +version = "2.0.16" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "dc1835b7f27878de8525dc71410b5a31cdcc5f230aed5ba5df968e09c201b23d" +dependencies = [ + "anstyle", + "bstr", + "doc-comment", + "libc", + "predicates", + "predicates-core", + "predicates-tree", + "wait-timeout", +] + +[[package]] +name = "assert_tokens_eq" +version = "0.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6b21f4c5ba5c8b55031306325f196df925939bcc2bd7188ce68fabd93fb4f149" +dependencies = [ + "ansi_term", + "ctor", + "difference", + "output_vt100", + "snafu", +] + [[package]] name = "autocfg" version = "1.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ace50bade8e6234aa140d9a2f552bbee1db4d353f69b8217bc503490fc1a9f26" +[[package]] +name = "backtrace" +version = "0.3.74" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8d82cb332cdfaed17ae235a638438ac4d4839913cc2af585c3c6746e8f8bee1a" +dependencies = [ + "addr2line", + "cfg-if", + "libc", + "miniz_oxide", + "object", + "rustc-demangle", + "windows-targets 0.52.6", +] + +[[package]] +name = "bincode" +version = "2.0.0-rc.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f11ea1a0346b94ef188834a65c068a03aec181c94896d481d7a0a40d85b0ce95" +dependencies = [ + "bincode_derive", + "serde", +] + +[[package]] +name = "bincode_derive" +version = "2.0.0-rc.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7e30759b3b99a1b802a7a3aa21c85c3ded5c28e1c83170d82d70f08bbf7f3e4c" +dependencies = [ + "virtue", +] + [[package]] name = "bitflags" version = "2.6.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b048fb63fd8b5923fc5aa7b340d8e156aec7ec02f0c78fa8a6ddc2613f6f71de" +[[package]] +name = "bitmaps" +version = "2.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "031043d04099746d8db04daf1fa424b2bc8bd69d92b25962dcde24da39ab64a2" +dependencies = [ + "typenum", +] + +[[package]] +name = "brownstone" +version = "3.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c5839ee4f953e811bfdcf223f509cb2c6a3e1447959b0bff459405575bc17f22" +dependencies = [ + "arrayvec 0.7.6", +] + +[[package]] +name = "bstr" +version = "1.10.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "40723b8fb387abc38f4f4a37c09073622e41dd12327033091ef8950659e6dc0c" +dependencies = [ + "memchr", + "regex-automata 0.4.8", + "serde", +] + [[package]] name = "build-kani" version = "0.55.0" @@ -139,12 +267,66 @@ dependencies = [ "thiserror", ] +[[package]] +name = "cc" +version = "1.1.28" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2e80e3b6a3ab07840e1cae9b0666a63970dc28e8ed5ffbcdacbfc760c281bfc1" +dependencies = [ + "shlex", +] + [[package]] name = "cfg-if" version = "1.0.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" +[[package]] +name = "charon" +version = "0.1.36" +dependencies = [ + "anyhow", + "assert_cmd", + "clap", + "colored", + "convert_case 0.6.0", + "derivative", + "derive-visitor", + "env_logger", + "hashlink", + "hax-frontend-exporter", + "ignore", + "im", + "index_vec", + "indoc", + "itertools 0.13.0", + "lazy_static", + "libtest-mimic", + "log", + "macros", + "nom", + "nom-supreme", + "petgraph", + "pretty", + "regex", + "rustc_version", + "serde", + "serde-map-to-array", + "serde_json", + "serde_stacker", + "snapbox", + "stacker", + "take_mut", + "tempfile", + "toml", + "tracing", + "tracing-subscriber", + "tracing-tree 0.3.1", + "walkdir", + "which", +] + [[package]] name = "clap" version = "4.5.19" @@ -174,9 +356,9 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "4ac6a0c7b1a9e9a5186361f67dfa1b88213572f427fb9ab038efb2bd8c582dab" dependencies = [ "heck", - "proc-macro2", - "quote", - "syn", + "proc-macro2 1.0.86", + "quote 1.0.37", + "syn 2.0.79", ] [[package]] @@ -191,6 +373,16 @@ version = "1.0.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d3fd119d74b830634cea2a0f58bbd0d54540518a14397557951e79340abc28c0" +[[package]] +name = "colored" +version = "2.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cbf2150cce219b664a8a70df7a1f933836724b503f8a413af9365b4dcc4d90b8" +dependencies = [ + "lazy_static", + "windows-sys 0.48.0", +] + [[package]] name = "comfy-table" version = "7.1.1" @@ -233,6 +425,21 @@ dependencies = [ "windows-sys 0.52.0", ] +[[package]] +name = "convert_case" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6245d59a3e82a7fc217c5828a6692dbc6dfb63a0c8c90495621f7b9d79704a0e" + +[[package]] +name = "convert_case" +version = "0.6.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ec182b0ca2f35d8fc196cf3404988fd8b8c739a4d270ff118a398feb0cbec1ca" +dependencies = [ + "unicode-segmentation", +] + [[package]] name = "cprover_bindings" version = "0.55.0" @@ -316,6 +523,16 @@ dependencies = [ "memchr", ] +[[package]] +name = "ctor" +version = "0.1.26" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6d2301688392eb071b0bf1a37be05c469d3cc4dbbd95df672fe28ab021e6a096" +dependencies = [ + "quote 1.0.37", + "syn 1.0.109", +] + [[package]] name = "deranged" version = "0.3.11" @@ -325,6 +542,63 @@ dependencies = [ "powerfmt", ] +[[package]] +name = "derivative" +version = "2.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "fcc3dd5e9e9c0b295d6e1e4d811fb6f157d5ffd784b8d202fc62eac8035a770b" +dependencies = [ + "proc-macro2 1.0.86", + "quote 1.0.37", + "syn 1.0.109", +] + +[[package]] +name = "derive-visitor" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d47165df83b9707cbada3216607a5d66125b6a66906de0bc1216c0669767ca9e" +dependencies = [ + "derive-visitor-macros", +] + +[[package]] +name = "derive-visitor-macros" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "427b39a85fecafea16b1a5f3f50437151022e35eb4fe038107f08adbf7f8def6" +dependencies = [ + "convert_case 0.4.0", + "itertools 0.10.5", + "proc-macro2 1.0.86", + "quote 1.0.37", + "syn 1.0.109", +] + +[[package]] +name = "difference" +version = "2.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "524cbf6897b527295dff137cec09ecf3a05f4fddffd7dfcd1585403449e74198" + +[[package]] +name = "difflib" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6184e33543162437515c2e2b48714794e37845ec9851711914eec9d308f6ebe8" + +[[package]] +name = "doc-comment" +version = "0.3.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "fea41bba32d969b513997752735605054bc0dfa92b4c56bf1189f2e174be7a10" + +[[package]] +name = "dyn-clone" +version = "1.0.17" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0d6ef0072f8a535281e4876be788938b528e9a1d43900b82c2569af7da799125" + [[package]] name = "either" version = "1.13.0" @@ -337,6 +611,29 @@ version = "0.3.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "a357d28ed41a50f9c765dbfe56cbc04a64e53e5fc58ba79fbc34c10ef3df831f" +[[package]] +name = "env_filter" +version = "0.1.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4f2c92ceda6ceec50f43169f9ee8424fe2db276791afde7b2cd8bc084cb376ab" +dependencies = [ + "log", + "regex", +] + +[[package]] +name = "env_logger" +version = "0.11.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e13fa619b91fb2381732789fc5de83b45675e882f66623b7d8cb4f643017018d" +dependencies = [ + "anstream", + "anstyle", + "env_filter", + "humantime", + "log", +] + [[package]] name = "equivalent" version = "1.0.1" @@ -353,6 +650,41 @@ dependencies = [ "windows-sys 0.52.0", ] +[[package]] +name = "escape8259" +version = "0.5.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5692dd7b5a1978a5aeb0ce83b7655c58ca8efdcb79d21036ea249da95afec2c6" + +[[package]] +name = "ext-trait" +version = "1.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d772df1c1a777963712fb68e014235e80863d6a91a85c4e06ba2d16243a310e5" +dependencies = [ + "ext-trait-proc_macros", +] + +[[package]] +name = "ext-trait-proc_macros" +version = "1.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1ab7934152eaf26aa5aa9f7371408ad5af4c31357073c9e84c3b9d7f11ad639a" +dependencies = [ + "proc-macro2 1.0.86", + "quote 1.0.37", + "syn 1.0.109", +] + +[[package]] +name = "extension-traits" +version = "1.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a296e5a895621edf9fa8329c83aa1cb69a964643e36cf54d8d7a69b789089537" +dependencies = [ + "ext-trait", +] + [[package]] name = "fastrand" version = "2.1.1" @@ -385,12 +717,31 @@ dependencies = [ "wasi", ] +[[package]] +name = "gimli" +version = "0.31.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "07e28edb80900c19c28f1072f2e8aeca7fa06b23cd4169cefe1af5aa3260783f" + [[package]] name = "glob" version = "0.3.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d2fabcfbdc87f4758337ca535fb41a6d701b65693ce38287d856d1674551ec9b" +[[package]] +name = "globset" +version = "0.4.15" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "15f1ce686646e7f1e19bf7d5533fe443a45dbfb990e00629110797578b42fb19" +dependencies = [ + "aho-corasick", + "bstr", + "log", + "regex-automata 0.4.8", + "regex-syntax 0.8.5", +] + [[package]] name = "graph-cycles" version = "0.1.0" @@ -417,12 +768,69 @@ version = "0.15.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "1e087f84d4f86bf4b218b927129862374b72199ae7d8657835f1e89000eea4fb" +[[package]] +name = "hashlink" +version = "0.9.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6ba4ff7128dee98c7dc9794b6a411377e1404dba1c97deb8d1a55297bd25d8af" +dependencies = [ + "hashbrown 0.14.5", + "serde", +] + +[[package]] +name = "hax-adt-into" +version = "0.1.0-alpha.1" +source = "git+https://github.com/hacspec/hax?branch=main#496e381186de242f46ee2fd2b4b8971c70aa07a4" +dependencies = [ + "itertools 0.11.0", + "proc-macro2 1.0.86", + "quote 1.0.37", + "syn 1.0.109", +] + +[[package]] +name = "hax-frontend-exporter" +version = "0.1.0-alpha.1" +source = "git+https://github.com/hacspec/hax?branch=main#496e381186de242f46ee2fd2b4b8971c70aa07a4" +dependencies = [ + "bincode", + "extension-traits", + "hax-adt-into", + "hax-frontend-exporter-options", + "itertools 0.11.0", + "lazy_static", + "paste", + "schemars", + "serde", + "serde_json", + "tracing", +] + +[[package]] +name = "hax-frontend-exporter-options" +version = "0.1.0-alpha.1" +source = "git+https://github.com/hacspec/hax?branch=main#496e381186de242f46ee2fd2b4b8971c70aa07a4" +dependencies = [ + "bincode", + "hax-adt-into", + "schemars", + "serde", + "serde_json", +] + [[package]] name = "heck" version = "0.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "2304e00983f87ffb38b55b444b5e3b60a884b5d30c0fca7d82fe33449bbe55ea" +[[package]] +name = "hermit-abi" +version = "0.3.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d231dfb89cfffdbc30e7fc41579ed6066ad03abda9e567ccafae602b97ec5024" + [[package]] name = "home" version = "0.5.9" @@ -432,6 +840,57 @@ dependencies = [ "windows-sys 0.52.0", ] +[[package]] +name = "humantime" +version = "2.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9a3a5bfb195931eeb336b2a7b4d761daec841b97f947d34394601737a7bba5e4" + +[[package]] +name = "ignore" +version = "0.4.23" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6d89fd380afde86567dfba715db065673989d6253f42b88179abd3eae47bda4b" +dependencies = [ + "crossbeam-deque", + "globset", + "log", + "memchr", + "regex-automata 0.4.8", + "same-file", + "walkdir", + "winapi-util", +] + +[[package]] +name = "im" +version = "15.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d0acd33ff0285af998aaf9b57342af478078f53492322fafc47450e09397e0e9" +dependencies = [ + "bitmaps", + "rand_core", + "rand_xoshiro", + "sized-chunks", + "typenum", + "version_check", +] + +[[package]] +name = "indent_write" +version = "2.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0cfe9645a18782869361d9c8732246be7b410ad4e919d3609ebabdac00ba12c3" + +[[package]] +name = "index_vec" +version = "0.1.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "44faf5bb8861a9c72e20d3fb0fdbd59233e43056e2b80475ab0aacdc2e781355" +dependencies = [ + "serde", +] + [[package]] name = "indexmap" version = "2.6.0" @@ -442,12 +901,36 @@ dependencies = [ "hashbrown 0.15.0", ] +[[package]] +name = "indoc" +version = "2.0.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b248f5224d1d606005e02c97f5aa4e88eeb230488bcc03bc9ca4d7991399f2b5" + [[package]] name = "is_terminal_polyfill" version = "1.70.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "7943c866cc5cd64cbc25b2e01621d07fa8eb2a1a23160ee81ce38704e97b8ecf" +[[package]] +name = "itertools" +version = "0.10.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b0fd2260e829bddf4cb6ea802289de2f86d6a7a690192fbe91b3f46e0f2c8473" +dependencies = [ + "either", +] + +[[package]] +name = "itertools" +version = "0.11.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b1c173a5686ce8bfa551b3563d0c2170bf24ca44da99c7ca4bfdab5418c3fe57" +dependencies = [ + "either", +] + [[package]] name = "itertools" version = "0.13.0" @@ -463,6 +946,12 @@ version = "1.0.11" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "49f1f14873335454500d59611f1cf4a4b0f786f9ac11f4312a78e4cf2566695b" +[[package]] +name = "joinery" +version = "2.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "72167d68f5fce3b8655487b8038691a3c9984ee769590f93f2a631f4ad64e4f5" + [[package]] name = "kani" version = "0.55.0" @@ -475,24 +964,25 @@ dependencies = [ name = "kani-compiler" version = "0.55.0" dependencies = [ + "charon", "clap", "cprover_bindings", "home", - "itertools", + "itertools 0.13.0", "kani_metadata", "lazy_static", "num", - "quote", + "quote 1.0.37", "regex", "serde", "serde_json", "shell-words", "strum", "strum_macros", - "syn", + "syn 2.0.79", "tracing", "tracing-subscriber", - "tracing-tree", + "tracing-tree 0.4.0", ] [[package]] @@ -545,9 +1035,9 @@ name = "kani_macros" version = "0.55.0" dependencies = [ "proc-macro-error2", - "proc-macro2", - "quote", - "syn", + "proc-macro2 1.0.86", + "quote 1.0.37", + "syn 2.0.79", ] [[package]] @@ -573,6 +1063,18 @@ version = "0.2.159" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "561d97a539a36e26a9a5fad1ea11a3039a67714694aaa379433e580854bc3dc5" +[[package]] +name = "libtest-mimic" +version = "0.7.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cc0bda45ed5b3a2904262c1bb91e526127aa70e7ef3758aba2ef93cf896b9b58" +dependencies = [ + "clap", + "escape8259", + "termcolor", + "threadpool", +] + [[package]] name = "linear-map" version = "1.2.0" @@ -605,6 +1107,16 @@ version = "0.4.22" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "a7a70ba024b9dc04c27ea2f0c0548feb474ec5c54bba33a7f72f873a39d07b24" +[[package]] +name = "macros" +version = "0.1.0" +dependencies = [ + "assert_tokens_eq", + "proc-macro2 1.0.86", + "quote 1.0.37", + "syn 2.0.79", +] + [[package]] name = "matchers" version = "0.1.0" @@ -618,13 +1130,57 @@ dependencies = [ name = "memchr" version = "2.7.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "78ca9ab1a0babb1e7d5695e3530886289c18cf2f87ec19a575a0abdce112e3a3" +checksum = "78ca9ab1a0babb1e7d5695e3530886289c18cf2f87ec19a575a0abdce112e3a3" + +[[package]] +name = "memuse" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2145869435ace5ea6ea3d35f59be559317ec9a0d04e1812d5f185a87b6d36f1a" + +[[package]] +name = "minimal-lexical" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "68354c5c6bd36d73ff3feceb05efa59b6acb7626617f4962be322a825e61f79a" + +[[package]] +name = "miniz_oxide" +version = "0.8.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e2d80299ef12ff69b16a84bb182e3b9df68b5a91574d3d4fa6e41b65deec4df1" +dependencies = [ + "adler2", +] + +[[package]] +name = "nom" +version = "7.1.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d273983c5a657a70a3e8f2a01329822f3b8c8172b73826411a55751e404a0a4a" +dependencies = [ + "memchr", + "minimal-lexical", +] + +[[package]] +name = "nom-supreme" +version = "0.8.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2bd3ae6c901f1959588759ff51c95d24b491ecb9ff91aa9c2ef4acc5b1dcab27" +dependencies = [ + "brownstone", + "indent_write", + "joinery", + "memchr", + "nom", +] [[package]] -name = "memuse" -version = "0.2.1" +name = "normalize-line-endings" +version = "0.3.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2145869435ace5ea6ea3d35f59be559317ec9a0d04e1812d5f185a87b6d36f1a" +checksum = "61807f77802ff30975e01f4f071c8ba10c022052f98b3294119f3e615d13e5be" [[package]] name = "nu-ansi-term" @@ -724,6 +1280,25 @@ dependencies = [ "autocfg", ] +[[package]] +name = "num_cpus" +version = "1.16.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4161fcb6d602d4d2081af7c3a45852d875a03dd337a6bfdd6e06407b61342a43" +dependencies = [ + "hermit-abi", + "libc", +] + +[[package]] +name = "object" +version = "0.36.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "aedf0a2d09c573ed1d8d85b30c119153926a2b36dce0ab28322c09a117a4683e" +dependencies = [ + "memchr", +] + [[package]] name = "once_cell" version = "1.20.2" @@ -740,6 +1315,15 @@ dependencies = [ "windows-sys 0.52.0", ] +[[package]] +name = "output_vt100" +version = "0.1.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "628223faebab4e3e40667ee0b2336d34a5b960ff60ea743ddfdbcf7770bcfb66" +dependencies = [ + "winapi", +] + [[package]] name = "overload" version = "0.1.1" @@ -766,9 +1350,15 @@ dependencies = [ "libc", "redox_syscall", "smallvec", - "windows-targets", + "windows-targets 0.52.6", ] +[[package]] +name = "paste" +version = "1.0.15" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "57c0d7b74b563b49d38dae00a0c37d4d6de9b432382b2892f0574ddcae73fd0a" + [[package]] name = "pathdiff" version = "0.2.1" @@ -806,14 +1396,52 @@ dependencies = [ "zerocopy", ] +[[package]] +name = "predicates" +version = "3.1.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7e9086cc7640c29a356d1a29fd134380bee9d8f79a17410aa76e7ad295f42c97" +dependencies = [ + "anstyle", + "difflib", + "predicates-core", +] + +[[package]] +name = "predicates-core" +version = "1.0.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ae8177bee8e75d6846599c6b9ff679ed51e882816914eec639944d7c9aa11931" + +[[package]] +name = "predicates-tree" +version = "1.0.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "41b740d195ed3166cd147c8047ec98db0e22ec019eb8eeb76d343b795304fb13" +dependencies = [ + "predicates-core", + "termtree", +] + +[[package]] +name = "pretty" +version = "0.12.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b55c4d17d994b637e2f4daf6e5dc5d660d209d5642377d675d7a1c3ab69fa579" +dependencies = [ + "arrayvec 0.5.2", + "typed-arena", + "unicode-width", +] + [[package]] name = "proc-macro-error-attr2" version = "2.0.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "96de42df36bb9bba5542fe9f1a054b8cc87e172759a1868aa05c1f3acc89dfc5" dependencies = [ - "proc-macro2", - "quote", + "proc-macro2 1.0.86", + "quote 1.0.37", ] [[package]] @@ -823,9 +1451,18 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "11ec05c52be0a07b08061f7dd003e7d7092e0472bc731b4af7bb1ef876109802" dependencies = [ "proc-macro-error-attr2", - "proc-macro2", - "quote", - "syn", + "proc-macro2 1.0.86", + "quote 1.0.37", + "syn 2.0.79", +] + +[[package]] +name = "proc-macro2" +version = "0.4.30" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cf3d2011ab5c909338f7887f4fc896d35932e29146c12c8d01da6b22a80ba759" +dependencies = [ + "unicode-xid", ] [[package]] @@ -837,13 +1474,31 @@ dependencies = [ "unicode-ident", ] +[[package]] +name = "psm" +version = "0.1.23" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "aa37f80ca58604976033fae9515a8a2989fc13797d953f7c04fb8fa36a11f205" +dependencies = [ + "cc", +] + +[[package]] +name = "quote" +version = "0.6.13" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6ce23b6b870e8f94f81fb0a363d65d86675884b34a09043c81e5562f11c1f8e1" +dependencies = [ + "proc-macro2 0.4.30", +] + [[package]] name = "quote" version = "1.0.37" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b5b9d34b8991d19d98081b46eacdd8eb58c6f2b201139f7c5f643cc155a633af" dependencies = [ - "proc-macro2", + "proc-macro2 1.0.86", ] [[package]] @@ -876,6 +1531,15 @@ dependencies = [ "getrandom", ] +[[package]] +name = "rand_xoshiro" +version = "0.6.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6f97cdb2a36ed4183de61b2f824cc45c9f1037f28afe0a322e9fff4c108b5aaa" +dependencies = [ + "rand_core", +] + [[package]] name = "rayon" version = "1.10.0" @@ -955,6 +1619,15 @@ version = "0.1.24" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "719b953e2095829ee67db738b3bfa9fa368c94900df327b3f07fe6e794d2fe1f" +[[package]] +name = "rustc_version" +version = "0.4.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cfcb3a22ef46e85b45de6ee7e79d063319ebb6594faafcf1c225ea92ab6e9b92" +dependencies = [ + "semver", +] + [[package]] name = "rustix" version = "0.38.37" @@ -1001,6 +1674,30 @@ dependencies = [ "strum_macros", ] +[[package]] +name = "schemars" +version = "0.8.21" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "09c024468a378b7e36765cd36702b7a90cc3cba11654f6685c8f233408e89e92" +dependencies = [ + "dyn-clone", + "schemars_derive", + "serde", + "serde_json", +] + +[[package]] +name = "schemars_derive" +version = "0.8.21" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b1eee588578aff73f856ab961cd2f79e36bc45d7ded33a7562adba4667aecc0e" +dependencies = [ + "proc-macro2 1.0.86", + "quote 1.0.37", + "serde_derive_internals", + "syn 2.0.79", +] + [[package]] name = "scopeguard" version = "1.2.0" @@ -1025,15 +1722,35 @@ dependencies = [ "serde_derive", ] +[[package]] +name = "serde-map-to-array" +version = "1.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c14b52efc56c711e0dbae3f26e0cc233f5dac336c1bf0b07e1b7dc2dca3b2cc7" +dependencies = [ + "serde", +] + [[package]] name = "serde_derive" version = "1.0.210" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "243902eda00fad750862fc144cea25caca5e20d615af0a81bee94ca738f1df1f" dependencies = [ - "proc-macro2", - "quote", - "syn", + "proc-macro2 1.0.86", + "quote 1.0.37", + "syn 2.0.79", +] + +[[package]] +name = "serde_derive_internals" +version = "0.29.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "18d26a20a969b9e3fdf2fc2d9f21eda6c40e2de84c9408bb5d3b05d499aae711" +dependencies = [ + "proc-macro2 1.0.86", + "quote 1.0.37", + "syn 2.0.79", ] [[package]] @@ -1057,6 +1774,16 @@ dependencies = [ "serde", ] +[[package]] +name = "serde_stacker" +version = "0.1.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "babfccff5773ff80657f0ecf553c7c516bdc2eb16389c0918b36b73e7015276e" +dependencies = [ + "serde", + "stacker", +] + [[package]] name = "serde_test" version = "1.0.177" @@ -1094,12 +1821,91 @@ version = "1.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "24188a676b6ae68c3b2cb3a01be17fbf7240ce009799bb56d5b1409051e78fde" +[[package]] +name = "shlex" +version = "1.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64" + +[[package]] +name = "similar" +version = "2.6.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1de1d4f81173b03af4c0cbed3c898f6bff5b870e4a7f5d6f4057d62a7a4b686e" + +[[package]] +name = "sized-chunks" +version = "0.6.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "16d69225bde7a69b235da73377861095455d298f2b970996eec25ddbb42b3d1e" +dependencies = [ + "bitmaps", + "typenum", +] + [[package]] name = "smallvec" version = "1.13.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "3c5e1a9a646d36c3599cd173a41282daf47c44583ad367b8e6837255952e5c67" +[[package]] +name = "snafu" +version = "0.4.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b028158eb06caa8345bee10cccfb25fa632beccf0ef5308832b4fd4b78a7db48" +dependencies = [ + "backtrace", + "doc-comment", + "snafu-derive", +] + +[[package]] +name = "snafu-derive" +version = "0.4.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bf50aaef500c248a590e2696e8bf8c7620ca2235b9bb90a70363d82dd1abec6a" +dependencies = [ + "proc-macro2 0.4.30", + "quote 0.6.13", + "syn 0.15.44", +] + +[[package]] +name = "snapbox" +version = "0.6.18" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7ba434818a8a9b1b106404288d6bd75a94348aae8fc9a518b211b609a36a54bc" +dependencies = [ + "anstream", + "anstyle", + "normalize-line-endings", + "similar", + "snapbox-macros", +] + +[[package]] +name = "snapbox-macros" +version = "0.3.10" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "16569f53ca23a41bb6f62e0a5084aa1661f4814a67fa33696a79073e03a664af" +dependencies = [ + "anstream", +] + +[[package]] +name = "stacker" +version = "0.1.17" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "799c883d55abdb5e98af1a7b3f23b9b6de8ecada0ecac058672d7635eb48ca7b" +dependencies = [ + "cc", + "cfg-if", + "libc", + "psm", + "windows-sys 0.59.0", +] + [[package]] name = "std" version = "0.55.0" @@ -1137,10 +1943,32 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "4c6bee85a5a24955dc440386795aa378cd9cf82acd5f764469152d2270e581be" dependencies = [ "heck", - "proc-macro2", - "quote", + "proc-macro2 1.0.86", + "quote 1.0.37", "rustversion", - "syn", + "syn 2.0.79", +] + +[[package]] +name = "syn" +version = "0.15.44" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9ca4b3b69a77cbe1ffc9e198781b7acb0c7365a883670e8f1c1bc66fba79a5c5" +dependencies = [ + "proc-macro2 0.4.30", + "quote 0.6.13", + "unicode-xid", +] + +[[package]] +name = "syn" +version = "1.0.109" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237" +dependencies = [ + "proc-macro2 1.0.86", + "quote 1.0.37", + "unicode-ident", ] [[package]] @@ -1149,11 +1977,17 @@ version = "2.0.79" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "89132cd0bf050864e1d38dc3bbc07a0eb8e7530af26344d3d2bbbef83499f590" dependencies = [ - "proc-macro2", - "quote", + "proc-macro2 1.0.86", + "quote 1.0.37", "unicode-ident", ] +[[package]] +name = "take_mut" +version = "0.2.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f764005d11ee5f36500a149ace24e00e3da98b0158b3e2d53a7495660d3f4d60" + [[package]] name = "tempfile" version = "3.13.0" @@ -1167,6 +2001,21 @@ dependencies = [ "windows-sys 0.59.0", ] +[[package]] +name = "termcolor" +version = "1.4.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "06794f8f6c5c898b3275aebefa6b8a1cb24cd2c6c79397ab15774837a0bc5755" +dependencies = [ + "winapi-util", +] + +[[package]] +name = "termtree" +version = "0.4.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3369f5ac52d5eb6ab48c6b4ffdc8efbcad6b89c765749064ba298f2c68a16a76" + [[package]] name = "thiserror" version = "1.0.64" @@ -1182,9 +2031,9 @@ version = "1.0.64" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "08904e7672f5eb876eaaf87e0ce17857500934f4981c4a0ab2b4aa98baac7fc3" dependencies = [ - "proc-macro2", - "quote", - "syn", + "proc-macro2 1.0.86", + "quote 1.0.37", + "syn 2.0.79", ] [[package]] @@ -1197,6 +2046,15 @@ dependencies = [ "once_cell", ] +[[package]] +name = "threadpool" +version = "1.8.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d050e60b33d41c19108b32cea32164033a9013fe3b46cbd4457559bfbf77afaa" +dependencies = [ + "num_cpus", +] + [[package]] name = "time" version = "0.3.36" @@ -1279,9 +2137,9 @@ version = "0.1.27" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "34704c8d6ebcbc939824180af020566b01a7c01f80641264eba0999f6c2b6be7" dependencies = [ - "proc-macro2", - "quote", - "syn", + "proc-macro2 1.0.86", + "quote 1.0.37", + "syn 2.0.79", ] [[package]] @@ -1337,6 +2195,18 @@ dependencies = [ "tracing-serde", ] +[[package]] +name = "tracing-tree" +version = "0.3.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b56c62d2c80033cb36fae448730a2f2ef99410fe3ecbffc916681a32f6807dbe" +dependencies = [ + "nu-ansi-term 0.50.1", + "tracing-core", + "tracing-log", + "tracing-subscriber", +] + [[package]] name = "tracing-tree" version = "0.4.0" @@ -1349,18 +2219,42 @@ dependencies = [ "tracing-subscriber", ] +[[package]] +name = "typed-arena" +version = "2.0.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6af6ae20167a9ece4bcb41af5b80f8a1f1df981f6391189ce00fd257af04126a" + +[[package]] +name = "typenum" +version = "1.17.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "42ff0bf0c66b8238c6f3b578df37d0b7848e55df8577b3f74f92a69acceeb825" + [[package]] name = "unicode-ident" version = "1.0.13" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "e91b56cd4cadaeb79bbf1a5645f6b4f8dc5bde8834ad5894a8db35fda9efa1fe" +[[package]] +name = "unicode-segmentation" +version = "1.12.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f6ccf251212114b54433ec949fd6a7841275f9ada20dddd2f29e9ceea4501493" + [[package]] name = "unicode-width" version = "0.1.14" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "7dd6e30e90baa6f72411720665d41d89b9a3d039dc45b8faea1ddd07f617f6af" +[[package]] +name = "unicode-xid" +version = "0.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "fc72304796d0818e357ead4e000d19c9c174ab23dc11093ac919054d20a6a7fc" + [[package]] name = "unsafe-libyaml" version = "0.2.11" @@ -1385,6 +2279,12 @@ version = "0.9.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a" +[[package]] +name = "virtue" +version = "0.0.13" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9dcc60c0624df774c82a0ef104151231d37da4962957d691c011c852b2473314" + [[package]] name = "wait-timeout" version = "0.2.0" @@ -1453,13 +2353,22 @@ version = "0.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f" +[[package]] +name = "windows-sys" +version = "0.48.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "677d2418bec65e3338edb076e806bc1ec15693c5d0104683f2efe857f61056a9" +dependencies = [ + "windows-targets 0.48.5", +] + [[package]] name = "windows-sys" version = "0.52.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "282be5f36a8ce781fad8c8ae18fa3f9beff57ec1b52cb3de0789201425d9a33d" dependencies = [ - "windows-targets", + "windows-targets 0.52.6", ] [[package]] @@ -1468,7 +2377,22 @@ version = "0.59.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "1e38bc4d79ed67fd075bcc251a1c39b32a1776bbe92e5bef1f0bf1f8c531853b" dependencies = [ - "windows-targets", + "windows-targets 0.52.6", +] + +[[package]] +name = "windows-targets" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9a2fa6e2155d7247be68c096456083145c183cbbbc2764150dda45a87197940c" +dependencies = [ + "windows_aarch64_gnullvm 0.48.5", + "windows_aarch64_msvc 0.48.5", + "windows_i686_gnu 0.48.5", + "windows_i686_msvc 0.48.5", + "windows_x86_64_gnu 0.48.5", + "windows_x86_64_gnullvm 0.48.5", + "windows_x86_64_msvc 0.48.5", ] [[package]] @@ -1477,28 +2401,46 @@ version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9b724f72796e036ab90c1021d4780d4d3d648aca59e491e6b98e725b84e99973" dependencies = [ - "windows_aarch64_gnullvm", - "windows_aarch64_msvc", - "windows_i686_gnu", + "windows_aarch64_gnullvm 0.52.6", + "windows_aarch64_msvc 0.52.6", + "windows_i686_gnu 0.52.6", "windows_i686_gnullvm", - "windows_i686_msvc", - "windows_x86_64_gnu", - "windows_x86_64_gnullvm", - "windows_x86_64_msvc", + "windows_i686_msvc 0.52.6", + "windows_x86_64_gnu 0.52.6", + "windows_x86_64_gnullvm 0.52.6", + "windows_x86_64_msvc 0.52.6", ] +[[package]] +name = "windows_aarch64_gnullvm" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2b38e32f0abccf9987a4e3079dfb67dcd799fb61361e53e2882c3cbaf0d905d8" + [[package]] name = "windows_aarch64_gnullvm" version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "32a4622180e7a0ec044bb555404c800bc9fd9ec262ec147edd5989ccd0c02cd3" +[[package]] +name = "windows_aarch64_msvc" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "dc35310971f3b2dbbf3f0690a219f40e2d9afcf64f9ab7cc1be722937c26b4bc" + [[package]] name = "windows_aarch64_msvc" version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "09ec2a7bb152e2252b53fa7803150007879548bc709c039df7627cabbd05d469" +[[package]] +name = "windows_i686_gnu" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a75915e7def60c94dcef72200b9a8e58e5091744960da64ec734a6c6e9b3743e" + [[package]] name = "windows_i686_gnu" version = "0.52.6" @@ -1511,24 +2453,48 @@ version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0eee52d38c090b3caa76c563b86c3a4bd71ef1a819287c19d586d7334ae8ed66" +[[package]] +name = "windows_i686_msvc" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8f55c233f70c4b27f66c523580f78f1004e8b5a8b659e05a4eb49d4166cca406" + [[package]] name = "windows_i686_msvc" version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "240948bc05c5e7c6dabba28bf89d89ffce3e303022809e73deaefe4f6ec56c66" +[[package]] +name = "windows_x86_64_gnu" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "53d40abd2583d23e4718fddf1ebec84dbff8381c07cae67ff7768bbf19c6718e" + [[package]] name = "windows_x86_64_gnu" version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "147a5c80aabfbf0c7d901cb5895d1de30ef2907eb21fbbab29ca94c5b08b1a78" +[[package]] +name = "windows_x86_64_gnullvm" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0b7b52767868a23d5bab768e390dc5f5c55825b6d30b86c844ff2dc7414044cc" + [[package]] name = "windows_x86_64_gnullvm" version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "24d5b23dc417412679681396f2b49f3de8c1473deb516bd34410872eff51ed0d" +[[package]] +name = "windows_x86_64_msvc" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ed94fce61571a4006852b7389a063ab983c02eb1bb37b47f8272ce92d06d9538" + [[package]] name = "windows_x86_64_msvc" version = "0.52.6" @@ -1566,7 +2532,7 @@ version = "0.7.35" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e" dependencies = [ - "proc-macro2", - "quote", - "syn", + "proc-macro2 1.0.86", + "quote 1.0.37", + "syn 2.0.79", ] diff --git a/charon b/charon new file mode 160000 index 000000000000..cdc1dcde447a --- /dev/null +++ b/charon @@ -0,0 +1 @@ +Subproject commit cdc1dcde447a50cbc20336c79b21b42ac977b7fd diff --git a/deny.toml b/deny.toml index 733f91e12f36..e44b234f4ca8 100644 --- a/deny.toml +++ b/deny.toml @@ -11,7 +11,10 @@ yanked = "deny" # A list of advisory IDs to ignore. Note that ignored advisories will still # output a note when they are encountered. ignore = [ - #"RUSTSEC-0000-0000", + # This is for a crate that is used by Charon + "RUSTSEC-2021-0139", + # This is for a crate that is used by Charon + "RUSTSEC-2020-0095", ] # This section is considered when running `cargo deny check licenses` @@ -21,6 +24,7 @@ ignore = [ allow = [ "MIT", "Apache-2.0", + "MPL-2.0", ] confidence-threshold = 0.8 @@ -46,4 +50,6 @@ wildcards = "allow" unknown-registry = "deny" unknown-git = "deny" allow-registry = ["https://github.com/rust-lang/crates.io-index"] -allow-git = [] +allow-git = [ + "https://github.com/hacspec/hax", +] diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index 9ca8d10f5275..0360763f9068 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -10,6 +10,7 @@ publish = false [dependencies] cbmc = { path = "../cprover_bindings", package = "cprover_bindings", optional = true } +charon = { path = "../charon/charon", optional = true, default-features = false } clap = { version = "4.4.11", features = ["derive", "cargo"] } home = "0.5" itertools = "0.13" @@ -30,7 +31,8 @@ tracing-tree = "0.4.0" # Future proofing: enable backend dependencies using feature. [features] -default = ['cprover'] +default = ['aeneas', 'cprover'] +aeneas = ['charon'] cprover = ['cbmc', 'num', 'serde'] write_json_symtab = [] diff --git a/kani-compiler/src/args.rs b/kani-compiler/src/args.rs index 3fa74b0e5aba..b5b799321cf3 100644 --- a/kani-compiler/src/args.rs +++ b/kani-compiler/src/args.rs @@ -1,9 +1,23 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -use strum_macros::{AsRefStr, EnumString, VariantNames}; +use strum_macros::{AsRefStr, Display, EnumString, VariantNames}; use tracing_subscriber::filter::Directive; +#[derive(Debug, Default, Display, Clone, Copy, AsRefStr, EnumString, VariantNames, PartialEq, Eq)] +#[strum(serialize_all = "snake_case")] +pub enum BackendOption { + /// Aeneas (LLBC) backend + #[cfg(feature = "aeneas")] + Aeneas, + + /// CProver (Goto) backend + #[cfg(feature = "cprover")] + #[strum(serialize = "cprover")] + #[default] + CProver, +} + #[derive(Debug, Default, Clone, Copy, AsRefStr, EnumString, VariantNames, PartialEq, Eq)] #[strum(serialize_all = "snake_case")] pub enum ReachabilityType { @@ -69,11 +83,13 @@ pub struct Arguments { /// Pass the kani version to the compiler to ensure cache coherence. check_version: Option, #[clap(long)] - /// A legacy flag that is now ignored. - goto_c: bool, - /// Enable specific checks. - #[clap(long)] pub ub_check: Vec, + /// Option name used to select which backend to use. + #[clap(long = "backend", default_value_t = BackendOption::CProver)] + pub backend: BackendOption, + /// Print the final LLBC file to stdout. This requires `-Zaeneas`. + #[clap(long)] + pub print_llbc: bool, } #[derive(Debug, Clone, Copy, AsRefStr, EnumString, VariantNames, PartialEq, Eq)] diff --git a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs new file mode 100644 index 000000000000..f9922f237bd5 --- /dev/null +++ b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs @@ -0,0 +1,411 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This file contains the code necessary to interface with the compiler backend + +use crate::args::ReachabilityType; +use crate::codegen_aeneas_llbc::mir_to_ullbc::Context; +use crate::kani_middle::attributes::KaniAttributes; +use crate::kani_middle::check_reachable_items; +use crate::kani_middle::codegen_units::{CodegenUnit, CodegenUnits}; +use crate::kani_middle::provide; +use crate::kani_middle::reachability::{collect_reachable_items, filter_crate_items}; +use crate::kani_middle::transform::{BodyTransformation, GlobalPasses}; +use crate::kani_queries::QueryDb; +use charon_lib::ast::TranslatedCrate; +use charon_lib::errors::ErrorCtx; +use charon_lib::transform::TransformCtx; +use charon_lib::transform::ctx::TransformOptions; +use kani_metadata::ArtifactType; +use kani_metadata::{AssignsContract, CompilerArtifactStub}; +use rustc_codegen_ssa::back::archive::{ + ArArchiveBuilder, ArchiveBuilder, ArchiveBuilderBuilder, DEFAULT_OBJECT_READER, +}; +use rustc_codegen_ssa::back::link::link_binary; +use rustc_codegen_ssa::traits::CodegenBackend; +use rustc_codegen_ssa::{CodegenResults, CrateInfo}; +use rustc_data_structures::fx::FxIndexMap; +use rustc_errors::{DEFAULT_LOCALE_RESOURCE, ErrorGuaranteed}; +use rustc_hir::def_id::{DefId as InternalDefId, LOCAL_CRATE}; +use rustc_metadata::EncodedMetadata; +use rustc_middle::dep_graph::{WorkProduct, WorkProductId}; +use rustc_middle::ty::TyCtxt; +use rustc_middle::util::Providers; +use rustc_session::Session; +use rustc_session::config::{CrateType, OutputFilenames, OutputType}; +use rustc_session::output::out_filename; +use rustc_smir::rustc_internal; +use stable_mir::mir::mono::{Instance, MonoItem}; +use stable_mir::{CrateDef, DefId}; +use std::any::Any; +use std::collections::{HashMap, HashSet}; +use std::fs::File; +use std::path::Path; +use std::sync::{Arc, Mutex}; +use std::time::Instant; +use tracing::{debug, info, trace}; + +#[derive(Clone)] +pub struct LlbcCodegenBackend { + /// The query is shared with `KaniCompiler` and it is initialized as part of `rustc` + /// initialization, which may happen after this object is created. + /// Since we don't have any guarantees on when the compiler creates the Backend object, neither + /// in which thread it will be used, we prefer to explicitly synchronize any query access. + queries: Arc>, +} + +impl LlbcCodegenBackend { + pub fn new(queries: Arc>) -> Self { + LlbcCodegenBackend { queries } + } + + /// Generate code that is reachable from the given starting points. + /// + /// Invariant: iff `check_contract.is_some()` then `return.2.is_some()` + fn codegen_items( + &self, + tcx: TyCtxt, + starting_items: &[MonoItem], + llbc_file: &Path, + _check_contract: Option, + mut transformer: BodyTransformation, + ) -> (Vec, Option) { + let (items, call_graph) = with_timer( + || collect_reachable_items(tcx, &mut transformer, starting_items), + "codegen reachability analysis", + ); + + // Retrieve all instances from the currently codegened items. + let instances = items + .iter() + .filter_map(|item| match item { + MonoItem::Fn(instance) => Some(*instance), + MonoItem::Static(static_def) => { + let instance: Instance = (*static_def).into(); + instance.has_body().then_some(instance) + } + MonoItem::GlobalAsm(_) => None, + }) + .collect(); + + // Apply all transformation passes, including global passes. + let mut global_passes = GlobalPasses::new(&self.queries.lock().unwrap(), tcx); + global_passes.run_global_passes( + &mut transformer, + tcx, + starting_items, + instances, + call_graph, + ); + + let queries = self.queries.lock().unwrap().clone(); + check_reachable_items(tcx, &queries, &items); + + // Follow rustc naming convention (cx is abbrev for context). + // https://rustc-dev-guide.rust-lang.org/conventions.html#naming-conventions + + // Create a Charon transformation context that will be populated with translation results + let mut ccx = create_charon_transformation_context(tcx); + + // Translate all the items + for item in &items { + match item { + MonoItem::Fn(instance) => { + let mut fcx = + Context::new(tcx, *instance, &mut ccx.translated, &mut ccx.errors); + let _ = fcx.translate(); + } + MonoItem::Static(_def) => todo!(), + MonoItem::GlobalAsm(_) => {} // We have already warned above + } + } + + trace!("# ULLBC after translation from MIR:\n\n{}\n", ccx); + + // # Reorder the graph of dependencies and compute the strictly + // connex components to: + // - compute the order in which to extract the definitions + // - find the recursive definitions + // - group the mutually recursive definitions + let reordered_decls = charon_lib::reorder_decls::compute_reordered_decls(&ccx); + ccx.translated.ordered_decls = Some(reordered_decls); + + // + // ================= + // **Micro-passes**: + // ================= + // At this point, the bulk of the translation is done. From now onwards, + // we simply apply some micro-passes to make the code cleaner, before + // serializing the result. + + // Run the micro-passes that clean up bodies. + for pass in charon_lib::transform::ULLBC_PASSES.iter() { + pass.transform_ctx(&mut ccx) + } + + // # Go from ULLBC to LLBC (Low-Level Borrow Calculus) by reconstructing + // the control flow. + charon_lib::ullbc_to_llbc::translate_functions(&mut ccx); + + trace!("# LLBC resulting from control-flow reconstruction:\n\n{}\n", ccx); + + // Run the micro-passes that clean up bodies. + for pass in charon_lib::transform::LLBC_PASSES.iter() { + pass.transform_ctx(&mut ccx) + } + + // Print the LLBC if requested. This is useful for expected tests. + if queries.args().print_llbc { + println!("# Final LLBC before serialization:\n\n{}\n", ccx); + } else { + debug!("# Final LLBC before serialization:\n\n{}\n", ccx); + } + + // Display an error report about the external dependencies, if necessary + ccx.errors.report_external_deps_errors(); + + let crate_data: charon_lib::export::CrateData = charon_lib::export::CrateData::new(&ccx); + + // No output should be generated if user selected no_codegen. + if !tcx.sess.opts.unstable_opts.no_codegen && tcx.sess.opts.output_types.should_codegen() { + // # Final step: generate the files. + // `crate_data` is set by our callbacks when there is no fatal error. + let mut pb = llbc_file.to_path_buf(); + pb.set_extension("llbc"); + println!("Writing LLBC file to {}", pb.display()); + if let Err(()) = crate_data.serialize_to_file(&pb) { + tcx.sess.dcx().err("Failed to write LLBC file"); + } + } + + (items, None) + } +} + +impl CodegenBackend for LlbcCodegenBackend { + fn provide(&self, providers: &mut Providers) { + provide::provide(providers, &self.queries.lock().unwrap()); + } + + fn print_version(&self) { + println!("Kani-llbc version: {}", env!("CARGO_PKG_VERSION")); + } + + fn locale_resource(&self) -> &'static str { + // We don't currently support multiple languages. + DEFAULT_LOCALE_RESOURCE + } + + fn codegen_crate( + &self, + tcx: TyCtxt, + rustc_metadata: EncodedMetadata, + _need_metadata_module: bool, + ) -> Box { + let ret_val = rustc_internal::run(tcx, || { + // Queries shouldn't change today once codegen starts. + let queries = self.queries.lock().unwrap().clone(); + + // Codegen all items that need to be processed according to the selected reachability mode: + // + // - Harnesses: Generate one model per local harnesses (marked with `kani::proof` attribute). + // - Tests: Generate one model per test harnesses. + // - PubFns: Generate code for all reachable logic starting from the local public functions. + // - None: Don't generate code. This is used to compile dependencies. + let base_filepath = tcx.output_filenames(()).path(OutputType::Object); + let base_filename = base_filepath.as_path(); + let reachability = queries.args().reachability_analysis; + match reachability { + ReachabilityType::Harnesses => { + let mut units = CodegenUnits::new(&queries, tcx); + let modifies_instances = vec![]; + // Cross-crate collecting of all items that are reachable from the crate harnesses. + for unit in units.iter() { + // We reset the body cache for now because each codegen unit has different + // configurations that affect how we transform the instance body. + let mut transformer = BodyTransformation::new(&queries, tcx, &unit); + for harness in &unit.harnesses { + let model_path = units.harness_model_path(*harness).unwrap(); + let contract_metadata = + contract_metadata_for_harness(tcx, harness.def.def_id()).unwrap(); + let (_items, contract_info) = self.codegen_items( + tcx, + &[MonoItem::Fn(*harness)], + model_path, + contract_metadata, + transformer, + ); + transformer = BodyTransformation::new(&queries, tcx, &unit); + if let Some(_assigns_contract) = contract_info { + //self.queries.lock().unwrap().register_assigns_contract( + // canonical_mangled_name(harness).intern(), + // assigns_contract, + //); + } + } + } + units.store_modifies(&modifies_instances); + units.write_metadata(&queries, tcx); + } + ReachabilityType::Tests => todo!(), + ReachabilityType::None => {} + ReachabilityType::PubFns => { + let unit = CodegenUnit::default(); + let transformer = BodyTransformation::new(&queries, tcx, &unit); + let main_instance = + stable_mir::entry_fn().map(|main_fn| Instance::try_from(main_fn).unwrap()); + let local_reachable = filter_crate_items(tcx, |_, instance| { + let def_id = rustc_internal::internal(tcx, instance.def.def_id()); + Some(instance) == main_instance || tcx.is_reachable_non_generic(def_id) + }) + .into_iter() + .map(MonoItem::Fn) + .collect::>(); + let model_path = base_filename.with_extension(ArtifactType::SymTabGoto); + let (_items, contract_info) = self.codegen_items( + tcx, + &local_reachable, + &model_path, + Default::default(), + transformer, + ); + assert!(contract_info.is_none()); + } + } + + if reachability != ReachabilityType::None && reachability != ReachabilityType::Harnesses + { + // In a workspace, cargo seems to be using the same file prefix to build a crate that is + // a package lib and also a dependency of another package. + // To avoid overriding the metadata for its verification, we skip this step when + // reachability is None, even because there is nothing to record. + } + codegen_results(tcx, rustc_metadata) + }); + ret_val.unwrap() + } + + fn join_codegen( + &self, + ongoing_codegen: Box, + _sess: &Session, + _filenames: &OutputFilenames, + ) -> (CodegenResults, FxIndexMap) { + match ongoing_codegen.downcast::<(CodegenResults, FxIndexMap)>() + { + Ok(val) => *val, + Err(val) => panic!("unexpected error: {:?}", (*val).type_id()), + } + } + + /// Emit output files during the link stage if it was requested. + /// + /// We need to emit `rlib` files normally if requested. Cargo expects these in some + /// circumstances and sends them to subsequent builds with `-L`. + /// + /// We CAN NOT invoke the native linker, because that will fail. We don't have real objects. + /// What determines whether the native linker is invoked or not is the set of `crate_types`. + /// Types such as `bin`, `cdylib`, `dylib` will trigger the native linker. + /// + /// Thus, we manually build the rlib file including only the `rmeta` file. + /// + /// For cases where no metadata file was requested, we stub the file requested by writing the + /// path of the `kani-metadata.json` file so `kani-driver` can safely find the latest metadata. + /// See for more details. + fn link( + &self, + sess: &Session, + codegen_results: CodegenResults, + outputs: &OutputFilenames, + ) -> Result<(), ErrorGuaranteed> { + let requested_crate_types = &codegen_results.crate_info.crate_types; + for crate_type in requested_crate_types { + let out_fname = out_filename( + sess, + *crate_type, + outputs, + codegen_results.crate_info.local_crate_name, + ); + let out_path = out_fname.as_path(); + debug!(?crate_type, ?out_path, "link"); + if *crate_type == CrateType::Rlib { + // Emit the `rlib` that contains just one file: `.rmeta` + link_binary(sess, &ArArchiveBuilderBuilder, &codegen_results, outputs)? + } else { + // Write the location of the kani metadata file in the requested compiler output file. + let base_filepath = outputs.path(OutputType::Object); + let base_filename = base_filepath.as_path(); + let content_stub = CompilerArtifactStub { + metadata_path: base_filename.with_extension(ArtifactType::Metadata), + }; + let out_file = File::create(out_path).unwrap(); + serde_json::to_writer(out_file, &content_stub).unwrap(); + } + } + Ok(()) + } +} + +struct ArArchiveBuilderBuilder; +impl ArchiveBuilderBuilder for ArArchiveBuilderBuilder { + fn new_archive_builder<'a>(&self, sess: &'a Session) -> Box { + Box::new(ArArchiveBuilder::new(sess, &DEFAULT_OBJECT_READER)) + } +} + +fn contract_metadata_for_harness( + tcx: TyCtxt, + def_id: DefId, +) -> Result, ErrorGuaranteed> { + let attrs = KaniAttributes::for_def_id(tcx, def_id); + Ok(attrs.interpret_for_contract_attribute().map(|(_, id, _)| id)) +} + +/// Return a struct that contains information about the codegen results as expected by `rustc`. +fn codegen_results(tcx: TyCtxt, rustc_metadata: EncodedMetadata) -> Box { + let work_products = FxIndexMap::::default(); + Box::new(( + CodegenResults { + modules: vec![], + allocator_module: None, + metadata_module: None, + metadata: rustc_metadata, + crate_info: CrateInfo::new(tcx, tcx.sess.target.arch.clone().to_string()), + }, + work_products, + )) +} + +/// Execute the provided function and measure the clock time it took for its execution. +/// Log the time with the given description. +pub fn with_timer(func: F, description: &str) -> T +where + F: FnOnce() -> T, +{ + let start = Instant::now(); + let ret = func(); + let elapsed = start.elapsed(); + info!("Finished {description} in {}s", elapsed.as_secs_f32()); + ret +} + +fn create_charon_transformation_context(tcx: TyCtxt) -> TransformCtx { + let options = TransformOptions { + no_code_duplication: false, + hide_marker_traits: false, + item_opacities: Vec::new(), + }; + let crate_name = tcx.crate_name(LOCAL_CRATE).as_str().into(); + let translated = TranslatedCrate { crate_name, ..TranslatedCrate::default() }; + let errors = ErrorCtx { + continue_on_failure: true, + errors_as_warnings: false, + dcx: tcx.dcx(), + decls_with_errors: HashSet::new(), + ignored_failed_decls: HashSet::new(), + dep_sources: HashMap::new(), + def_id: None, + error_count: 0, + }; + TransformCtx { options, translated, errors } +} diff --git a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs new file mode 100644 index 000000000000..62462915480e --- /dev/null +++ b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs @@ -0,0 +1,802 @@ +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Modifications Copyright Kani Contributors +// See GitHub history for details. + +//! This module contains a context for translating stable MIR into Charon's +//! unstructured low-level borrow calculus (ULLBC) + +use core::panic; +use std::path::PathBuf; + +use charon_lib::ast::CastKind as CharonCastKind; +use charon_lib::ast::Place as CharonPlace; +use charon_lib::ast::ProjectionElem as CharonProjectionElem; +use charon_lib::ast::Rvalue as CharonRvalue; +use charon_lib::ast::Span as CharonSpan; +use charon_lib::ast::meta::{AttrInfo, Loc, RawSpan}; +use charon_lib::ast::types::Ty as CharonTy; +use charon_lib::ast::{AbortKind, Body as CharonBody, Var, VarId, make_locals_generator}; +use charon_lib::ast::{ + AnyTransId, Assert, BodyId, BuiltinTy, Disambiguator, FileName, FunDecl, FunSig, GenericArgs, + GenericParams, IntegerTy, ItemKind, ItemMeta, ItemOpacity, Literal, LiteralTy, Name, Opaque, + PathElem, RawConstantExpr, RefKind, Region as CharonRegion, ScalarValue, TranslatedCrate, + TypeId, +}; +use charon_lib::ast::{ + BinOp as CharonBinOp, Call, FnOperand, FnPtr, FunDeclId, FunId, FunIdOrTraitMethodRef, + VariantId, +}; +use charon_lib::ast::{ + BorrowKind as CharonBorrowKind, ConstantExpr, Operand as CharonOperand, UnOp, +}; +use charon_lib::common::Error; +use charon_lib::errors::ErrorCtx; +use charon_lib::ids::Vector; +use charon_lib::ullbc_ast::{ + BlockData, BlockId, BodyContents, ExprBody, RawStatement, RawTerminator, + Statement as CharonStatement, SwitchTargets as CharonSwitchTargets, + Terminator as CharonTerminator, +}; +use charon_lib::{error_assert, error_or_panic}; +use rustc_errors::MultiSpan; +use rustc_middle::ty::TyCtxt; +use rustc_smir::rustc_internal; +use rustc_span::def_id::DefId as InternalDefId; +use stable_mir::abi::PassMode; +use stable_mir::mir::mono::Instance; +use stable_mir::mir::{ + BasicBlock, BinOp, Body, BorrowKind, CastKind, ConstOperand, Mutability, Operand, Place, + ProjectionElem, Rvalue, Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind, +}; +use stable_mir::ty::{ + Allocation, ConstantKind, IndexedVal, IntTy, MirConst, Region, RegionKind, RigidTy, Span, Ty, + TyKind, UintTy, +}; + +use stable_mir::{CrateDef, DefId}; +use tracing::{debug, trace}; + +/// A context for translating a single MIR function to ULLBC. +/// The results of the translation are stored in the `translated` field. +pub struct Context<'a, 'tcx> { + tcx: TyCtxt<'tcx>, + instance: Instance, + translated: &'a mut TranslatedCrate, + errors: &'a mut ErrorCtx<'tcx>, +} + +impl<'a, 'tcx> Context<'a, 'tcx> { + /// Create a new context for translating the function `instance`, populating + /// the results of the translation in `translated` + pub fn new( + tcx: TyCtxt<'tcx>, + instance: Instance, + translated: &'a mut TranslatedCrate, + errors: &'a mut ErrorCtx<'tcx>, + ) -> Self { + Self { tcx, instance, translated, errors } + } + + fn tcx(&self) -> TyCtxt<'tcx> { + self.tcx + } + + fn span_err>(&mut self, span: S, msg: &str) { + self.errors.span_err(span, msg); + } + + fn continue_on_failure(&self) -> bool { + self.errors.continue_on_failure() + } + + /// Perform the translation + pub fn translate(&mut self) -> Result<(), ()> { + // Charon's `id_map` is in terms of internal `DefId` + let def_id = rustc_internal::internal(self.tcx(), self.instance.def.def_id()); + + // TODO: might want to populate `errors.dep_sources` to help with + // debugging + + let fid = self.register_fun_decl_id(def_id); + + let item_meta = match self.translate_item_meta_from_rid(self.instance) { + Ok(item_meta) => item_meta, + Err(_) => { + return Err(()); + } + }; + + let signature = self.translate_function_signature(); + let body = match self.translate_function_body() { + Ok(body) => body, + Err(_) => { + return Err(()); + } + }; + + let fun_decl = FunDecl { + def_id: fid, + rust_id: def_id, + item_meta, + signature, + kind: ItemKind::Regular, + body: Ok(body), + }; + + self.translated.fun_decls.set_slot(fid, fun_decl); + + Ok(()) + } + + /// Get or create a `FunDeclId` for the given function + fn register_fun_decl_id(&mut self, def_id: InternalDefId) -> FunDeclId { + let tid = match self.translated.id_map.get(&def_id) { + Some(tid) => *tid, + None => { + let tid = AnyTransId::Fun(self.translated.fun_decls.reserve_slot()); + self.translated.id_map.insert(def_id, tid); + self.translated.reverse_id_map.insert(tid, def_id); + self.translated.all_ids.insert(tid); + tid + } + }; + *tid.as_fun() + } + + /// Compute the meta information for a Rust item identified by its id. + fn translate_item_meta_from_rid(&mut self, instance: Instance) -> Result { + let span = self.translate_instance_span(instance); + let name = self.def_id_to_name(instance.def.def_id())?; + // TODO: populate the source text + let source_text = None; + // TODO: populate the attribute info + let attr_info = + AttrInfo { attributes: Vec::new(), inline: None, rename: None, public: true }; + + // Aeneas only translates items that are local to the top-level crate + // Since we want all reachable items (including those in external + // crates) to be translated, always set `is_local` to true + let is_local = true; + + // For now, assume all items are transparent + let opacity = ItemOpacity::Transparent; + + Ok(ItemMeta { span, source_text, attr_info, name, is_local, opacity }) + } + + /// Retrieve an item name from a [DefId]. + /// This function is adapted from Charon: + /// https://github.com/AeneasVerif/charon/blob/53530427db2941ce784201e64086766504bc5642/charon/src/bin/charon-driver/translate/translate_ctx.rs#L344 + fn def_id_to_name(&mut self, def_id: DefId) -> Result { + trace!("{:?}", def_id); + let def_id = rustc_internal::internal(self.tcx(), def_id); + let tcx = self.tcx(); + let span = tcx.def_span(def_id); + + // We have to be a bit careful when retrieving names from def ids. For instance, + // due to reexports, [`TyCtxt::def_path_str`](TyCtxt::def_path_str) might give + // different names depending on the def id on which it is called, even though + // those def ids might actually identify the same definition. + // For instance: `std::boxed::Box` and `alloc::boxed::Box` are actually + // the same (the first one is a reexport). + // This is why we implement a custom function to retrieve the original name + // (though this makes us lose aliases - we may want to investigate this + // issue in the future). + + // We lookup the path associated to an id, and convert it to a name. + // Paths very precisely identify where an item is. There are important + // subcases, like the items in an `Impl` block: + // ``` + // impl List { + // fn new() ... + // } + // ``` + // + // One issue here is that "List" *doesn't appear* in the path, which would + // look like the following: + // + // `TypeNS("Crate") :: Impl :: ValueNs("new")` + // ^^^ + // This is where "List" should be + // + // For this reason, whenever we find an `Impl` path element, we actually + // lookup the type of the sub-path, from which we can derive a name. + // + // Besides, as there may be several "impl" blocks for one type, each impl + // block is identified by a unique number (rustc calls this a + // "disambiguator"), which we grab. + // + // Example: + // ======== + // For instance, if we write the following code in crate `test` and module + // `bla`: + // ``` + // impl Foo { + // fn foo() { ... } + // } + // + // impl Foo { + // fn bar() { ... } + // } + // ``` + // + // The names we will generate for `foo` and `bar` are: + // `[Ident("test"), Ident("bla"), Ident("Foo"), Disambiguator(0), Ident("foo")]` + // `[Ident("test"), Ident("bla"), Ident("Foo"), Disambiguator(1), Ident("bar")]` + let mut found_crate_name = false; + let mut name: Vec = Vec::new(); + + let def_path = tcx.def_path(def_id); + let crate_name = tcx.crate_name(def_path.krate).to_string(); + + let parents: Vec<_> = { + let mut parents = vec![def_id]; + let mut cur_id = def_id; + while let Some(parent) = tcx.opt_parent(cur_id) { + parents.push(parent); + cur_id = parent; + } + parents.into_iter().rev().collect() + }; + + // Rk.: below we try to be as tight as possible with regards to sanity + // checks, to make sure we understand what happens with def paths, and + // fail whenever we get something which is even slightly outside what + // we expect. + for cur_id in parents { + let data = tcx.def_key(cur_id).disambiguated_data; + // Match over the key data + let disambiguator = Disambiguator::new(data.disambiguator as usize); + use rustc_hir::definitions::DefPathData; + match &data.data { + DefPathData::TypeNs(symbol) => { + error_assert!(self, span, data.disambiguator == 0); // Sanity check + name.push(PathElem::Ident(symbol.to_string(), disambiguator)); + } + DefPathData::ValueNs(symbol) => { + // I think `disambiguator != 0` only with names introduced by macros (though + // not sure). + name.push(PathElem::Ident(symbol.to_string(), disambiguator)); + } + DefPathData::CrateRoot => { + // Sanity check + error_assert!(self, span, data.disambiguator == 0); + + // This should be the beginning of the path + error_assert!(self, span, name.is_empty()); + found_crate_name = true; + name.push(PathElem::Ident(crate_name.clone(), disambiguator)); + } + DefPathData::Impl => todo!(), + DefPathData::OpaqueTy => { + // TODO: do nothing for now + } + DefPathData::MacroNs(symbol) => { + error_assert!(self, span, data.disambiguator == 0); // Sanity check + + // There may be namespace collisions between, say, function + // names and macros (not sure). However, this isn't much + // of an issue here, because for now we don't expose macros + // in the AST, and only use macro names in [register], for + // instance to filter opaque modules. + name.push(PathElem::Ident(symbol.to_string(), disambiguator)); + } + DefPathData::Closure => { + // TODO: this is not very satisfactory, but on the other hand + // we should be able to extract closures in local let-bindings + // (i.e., we shouldn't have to introduce top-level let-bindings). + name.push(PathElem::Ident("closure".to_string(), disambiguator)) + } + DefPathData::ForeignMod => { + // Do nothing, functions in `extern` blocks are in the same namespace as the + // block. + } + _ => { + error_or_panic!(self, span, format!("Unexpected DefPathData: {:?}", data)); + } + } + } + + // We always add the crate name + if !found_crate_name { + name.push(PathElem::Ident(crate_name, Disambiguator::new(0))); + } + + trace!("{:?}", name); + Ok(Name { name }) + } + + /// Compute the span information for the given instance + fn translate_instance_span(&mut self, instance: Instance) -> CharonSpan { + self.translate_span(instance.def.span()) + } + + /// Compute the span information for MIR span + fn translate_span(&mut self, span: Span) -> CharonSpan { + let filename = FileName::Local(PathBuf::from(span.get_filename())); + let file_id = match self.translated.file_to_id.get(&filename) { + Some(file_id) => *file_id, + None => { + let file_id = self.translated.id_to_file.push(filename.clone()); + self.translated.file_to_id.insert(filename, file_id); + file_id + } + }; + let lineinfo = span.get_lines(); + let rspan = RawSpan { + file_id, + beg: Loc { line: lineinfo.start_line, col: lineinfo.start_col }, + end: Loc { line: lineinfo.end_line, col: lineinfo.end_col }, + rust_span_data: rustc_internal::internal(self.tcx(), span).data(), + }; + + // TODO: populate `generated_from_span` info + CharonSpan { span: rspan, generated_from_span: None } + } + + fn translate_function_signature(&mut self) -> FunSig { + let instance = self.instance; + let fn_abi = instance.fn_abi().unwrap(); + let requires_caller_location = self.requires_caller_location(instance); + let num_args = fn_abi.args.len(); + let args = fn_abi + .args + .iter() + .enumerate() + .filter_map(|(idx, arg_abi)| { + // We ignore zero-sized parameters. + // See https://github.com/model-checking/kani/issues/274 for more details. + // We also ingore the last parameter if the function requires + // caller location. + if arg_abi.mode == PassMode::Ignore + || (requires_caller_location && idx + 1 == num_args) + { + None + } else { + let ty = arg_abi.ty; + debug!(?idx, ?arg_abi, "fn_typ"); + Some(self.translate_ty(ty)) + } + }) + .collect(); + + debug!(?args, ?fn_abi, "function_type"); + let ret_type = self.translate_ty(fn_abi.ret.ty); + + // TODO: populate the rest of the information (`is_unsafe`, `is_closure`, etc.) + FunSig { + is_unsafe: false, + is_closure: false, + closure_info: None, + generics: GenericParams::default(), + parent_params_info: None, + inputs: args, + output: ret_type, + } + } + + fn translate_function_body(&mut self) -> Result { + let instance = self.instance; + let mir_body = instance.body().unwrap(); + let body_id = self.translated.bodies.reserve_slot(); + let body = self.translate_body(mir_body); + self.translated.bodies.set_slot(body_id, body); + Ok(body_id) + } + + fn translate_body(&mut self, mir_body: Body) -> CharonBody { + let span = self.translate_span(mir_body.span); + let arg_count = self.instance.fn_abi().unwrap().args.len(); + let locals = self.translate_body_locals(&mir_body); + let body: BodyContents = + mir_body.blocks.iter().map(|bb| self.translate_block(bb)).collect(); + + let body_expr = ExprBody { span, arg_count, locals, body }; + CharonBody::Unstructured(body_expr) + } + + fn requires_caller_location(&self, instance: Instance) -> bool { + let instance_internal = rustc_internal::internal(self.tcx(), instance); + instance_internal.def.requires_caller_location(self.tcx()) + } + + fn translate_ty(&self, ty: Ty) -> CharonTy { + match ty.kind() { + TyKind::RigidTy(rigid_ty) => self.translate_rigid_ty(rigid_ty), + _ => todo!(), + } + } + + fn translate_rigid_ty(&self, rigid_ty: RigidTy) -> CharonTy { + debug!("translate_rigid_ty: {rigid_ty:?}"); + match rigid_ty { + RigidTy::Bool => CharonTy::Literal(LiteralTy::Bool), + RigidTy::Char => CharonTy::Literal(LiteralTy::Char), + RigidTy::Int(it) => CharonTy::Literal(LiteralTy::Integer(translate_int_ty(it))), + RigidTy::Uint(uit) => CharonTy::Literal(LiteralTy::Integer(translate_uint_ty(uit))), + RigidTy::Never => CharonTy::Never, + RigidTy::Str => CharonTy::Adt( + TypeId::Builtin(BuiltinTy::Str), + // TODO: find out whether any of the information below should be + // populated for strings + GenericArgs { + regions: Vector::new(), + types: Vector::new(), + const_generics: Vector::new(), + trait_refs: Vector::new(), + }, + ), + RigidTy::Ref(region, ty, mutability) => CharonTy::Ref( + self.translate_region(region), + Box::new(self.translate_ty(ty)), + match mutability { + Mutability::Mut => RefKind::Mut, + Mutability::Not => RefKind::Shared, + }, + ), + RigidTy::Tuple(ty) => { + let types = ty.iter().map(|ty| self.translate_ty(*ty)).collect(); + // TODO: find out if any of the information below is needed + let generic_args = GenericArgs { + regions: Vector::new(), + types, + const_generics: Vector::new(), + trait_refs: Vector::new(), + }; + CharonTy::Adt(TypeId::Tuple, generic_args) + } + RigidTy::FnDef(def_id, args) => { + if !args.0.is_empty() { + unimplemented!("generic args are not yet handled"); + } + let sig = def_id.fn_sig().value; + let inputs = sig.inputs().iter().map(|ty| self.translate_ty(*ty)).collect(); + let output = self.translate_ty(sig.output()); + // TODO: populate regions? + CharonTy::Arrow(Vector::new(), inputs, Box::new(output)) + } + _ => todo!(), + } + } + + fn translate_body_locals(&mut self, mir_body: &Body) -> Vector { + // Charon expects the locals in the following order: + // - the local used for the return value (index 0) + // - the input arguments + // - the remaining locals, used for the intermediate computations + let mut locals = Vector::new(); + { + let mut add_variable = make_locals_generator(&mut locals); + mir_body.local_decls().for_each(|(_, local)| { + add_variable(self.translate_ty(local.ty)); + }); + } + locals + } + + fn translate_block(&mut self, bb: &BasicBlock) -> BlockData { + let statements = + bb.statements.iter().filter_map(|stmt| self.translate_statement(stmt)).collect(); + let terminator = self.translate_terminator(&bb.terminator); + BlockData { statements, terminator } + } + + fn translate_statement(&mut self, stmt: &Statement) -> Option { + let content = match &stmt.kind { + StatementKind::Assign(place, rhs) => Some(RawStatement::Assign( + self.translate_place(&place), + self.translate_rvalue(&rhs), + )), + StatementKind::SetDiscriminant { place, variant_index } => { + Some(RawStatement::SetDiscriminant( + self.translate_place(&place), + VariantId::from_usize(variant_index.to_index()), + )) + } + StatementKind::StorageLive(_) => None, + StatementKind::StorageDead(local) => { + Some(RawStatement::StorageDead(VarId::from_usize(*local))) + } + StatementKind::Nop => None, + _ => todo!(), + }; + if let Some(content) = content { + let span = self.translate_span(stmt.span); + return Some(CharonStatement { span, content }); + }; + None + } + + fn translate_terminator(&mut self, terminator: &Terminator) -> CharonTerminator { + let span = self.translate_span(terminator.span); + let content = match &terminator.kind { + TerminatorKind::Return => RawTerminator::Return, + TerminatorKind::Goto { target } => { + RawTerminator::Goto { target: BlockId::from_usize(*target) } + } + TerminatorKind::Unreachable => RawTerminator::Abort(AbortKind::UndefinedBehavior), + TerminatorKind::Drop { place, target, .. } => RawTerminator::Drop { + place: self.translate_place(&place), + target: BlockId::from_usize(*target), + }, + TerminatorKind::SwitchInt { discr, targets } => { + let (discr, targets) = self.translate_switch_targets(discr, targets); + RawTerminator::Switch { discr, targets } + } + TerminatorKind::Call { func, args, destination, target, .. } => { + debug!("translate_call: {func:?} {args:?} {destination:?} {target:?}"); + let fn_ty = func.ty(self.instance.body().unwrap().locals()).unwrap(); + let fn_ptr = match fn_ty.kind() { + TyKind::RigidTy(RigidTy::FnDef(def, args)) => { + let instance = Instance::resolve(def, &args).unwrap(); + let def_id = rustc_internal::internal(self.tcx(), instance.def.def_id()); + let fid = self.register_fun_decl_id(def_id); + FnPtr { + func: FunIdOrTraitMethodRef::Fun(FunId::Regular(fid)), + // TODO: populate generics? + generics: GenericArgs { + regions: Vector::new(), + types: Vector::new(), + const_generics: Vector::new(), + trait_refs: Vector::new(), + }, + } + } + TyKind::RigidTy(RigidTy::FnPtr(..)) => todo!(), + x => unreachable!( + "Function call where the function was of unexpected type: {:?}", + x + ), + }; + let func = FnOperand::Regular(fn_ptr); + let call = Call { + func, + args: args.iter().map(|arg| self.translate_operand(arg)).collect(), + dest: self.translate_place(destination), + }; + RawTerminator::Call { call, target: target.map(BlockId::from_usize) } + } + TerminatorKind::Assert { cond, expected, msg: _, target, .. } => { + RawTerminator::Assert { + assert: Assert { cond: self.translate_operand(cond), expected: *expected }, + target: BlockId::from_usize(*target), + } + } + _ => todo!(), + }; + CharonTerminator { span, content } + } + + fn translate_place(&self, place: &Place) -> CharonPlace { + let projection = self.translate_projection(&place.projection); + let local = place.local; + let var_id = VarId::from_usize(local); + CharonPlace { var_id, projection } + } + + fn translate_rvalue(&self, rvalue: &Rvalue) -> CharonRvalue { + trace!("translate_rvalue: {rvalue:?}"); + match rvalue { + Rvalue::Use(operand) => CharonRvalue::Use(self.translate_operand(operand)), + Rvalue::Repeat(_operand, _) => todo!(), + Rvalue::Ref(_region, kind, place) => { + CharonRvalue::Ref(self.translate_place(&place), translate_borrow_kind(kind)) + } + Rvalue::AddressOf(_, _) => todo!(), + Rvalue::Len(place) => CharonRvalue::Len( + self.translate_place(&place), + self.translate_ty(rvalue.ty(self.instance.body().unwrap().locals()).unwrap()), + None, + ), + Rvalue::Cast(kind, operand, ty) => CharonRvalue::UnaryOp( + UnOp::Cast(self.translate_cast(*kind, operand, *ty)), + self.translate_operand(operand), + ), + Rvalue::BinaryOp(bin_op, lhs, rhs) => CharonRvalue::BinaryOp( + translate_bin_op(*bin_op), + self.translate_operand(lhs), + self.translate_operand(rhs), + ), + Rvalue::CheckedBinaryOp(_, _, _) => todo!(), + Rvalue::UnaryOp(_, _) => todo!(), + Rvalue::Discriminant(_) => todo!(), + Rvalue::Aggregate(_, _) => todo!(), + Rvalue::ShallowInitBox(_, _) => todo!(), + Rvalue::CopyForDeref(_) => todo!(), + Rvalue::ThreadLocalRef(_) => todo!(), + _ => todo!(), + } + } + + fn translate_operand(&self, operand: &Operand) -> CharonOperand { + trace!("translate_operand: {operand:?}"); + match operand { + Operand::Constant(constant) => CharonOperand::Const(self.translate_constant(constant)), + Operand::Copy(place) => CharonOperand::Copy(self.translate_place(&place)), + Operand::Move(place) => CharonOperand::Move(self.translate_place(&place)), + } + } + + fn translate_constant(&self, constant: &ConstOperand) -> ConstantExpr { + trace!("translate_constant: {constant:?}"); + let value = self.translate_constant_value(&constant.const_); + ConstantExpr { value, ty: self.translate_ty(constant.ty()) } + } + + fn translate_constant_value(&self, constant: &MirConst) -> RawConstantExpr { + trace!("translate_constant_value: {constant:?}"); + match constant.kind() { + ConstantKind::Allocated(alloc) => self.translate_allocation(alloc, constant.ty()), + ConstantKind::Ty(_) => todo!(), + ConstantKind::ZeroSized => todo!(), + ConstantKind::Unevaluated(_) => todo!(), + ConstantKind::Param(_) => todo!(), + } + } + + fn translate_allocation(&self, alloc: &Allocation, ty: Ty) -> RawConstantExpr { + match ty.kind() { + TyKind::RigidTy(RigidTy::Int(it)) => { + let value = alloc.read_int().unwrap(); + let scalar_value = match it { + IntTy::I8 => ScalarValue::I8(value as i8), + IntTy::I16 => ScalarValue::I16(value as i16), + IntTy::I32 => ScalarValue::I32(value as i32), + IntTy::I64 => ScalarValue::I64(value as i64), + IntTy::I128 => ScalarValue::I128(value), + IntTy::Isize => ScalarValue::Isize(value as i64), + }; + RawConstantExpr::Literal(Literal::Scalar(scalar_value)) + } + TyKind::RigidTy(RigidTy::Uint(uit)) => { + let value = alloc.read_uint().unwrap(); + let scalar_value = match uit { + UintTy::U8 => ScalarValue::U8(value as u8), + UintTy::U16 => ScalarValue::U16(value as u16), + UintTy::U32 => ScalarValue::U32(value as u32), + UintTy::U64 => ScalarValue::U64(value as u64), + UintTy::U128 => ScalarValue::U128(value), + UintTy::Usize => ScalarValue::Usize(value as u64), + }; + RawConstantExpr::Literal(Literal::Scalar(scalar_value)) + } + TyKind::RigidTy(RigidTy::Bool) => { + let value = alloc.read_bool().unwrap(); + RawConstantExpr::Literal(Literal::Bool(value)) + } + TyKind::RigidTy(RigidTy::Char) => { + let value = char::from_u32(alloc.read_uint().unwrap() as u32); + RawConstantExpr::Literal(Literal::Char(value.unwrap())) + } + _ => todo!(), + } + } + + fn translate_cast(&self, _kind: CastKind, _operand: &Operand, _ty: Ty) -> CharonCastKind { + todo!() + } + + fn translate_switch_targets( + &self, + discr: &Operand, + targets: &SwitchTargets, + ) -> (CharonOperand, CharonSwitchTargets) { + trace!("translate_switch_targets: {discr:?} {targets:?}"); + let ty = discr.ty(self.instance.body().unwrap().locals()).unwrap(); + let discr = self.translate_operand(discr); + let charon_ty = self.translate_ty(ty); + let switch_targets = if ty.kind().is_bool() { + // Charon/Aeneas expects types with a bool discriminant to be translated to an `If` + // `len` includes the `otherwise` branch + assert_eq!(targets.len(), 2); + let (value, bb) = targets.branches().last().unwrap(); + let (then_bb, else_bb) = + if value == 0 { (targets.otherwise(), bb) } else { (bb, targets.otherwise()) }; + CharonSwitchTargets::If(BlockId::from_usize(then_bb), BlockId::from_usize(else_bb)) + } else { + let CharonTy::Literal(LiteralTy::Integer(int_ty)) = charon_ty else { + panic!("Expected integer type for switch discriminant"); + }; + let branches = targets + .branches() + .map(|(value, bb)| { + let scalar_val = match int_ty { + IntegerTy::I8 => ScalarValue::I8(value as i8), + IntegerTy::I16 => ScalarValue::I16(value as i16), + IntegerTy::I32 => ScalarValue::I32(value as i32), + IntegerTy::I64 => ScalarValue::I64(value as i64), + IntegerTy::I128 => ScalarValue::I128(value as i128), + IntegerTy::Isize => ScalarValue::Isize(value as i64), + IntegerTy::U8 => ScalarValue::U8(value as u8), + IntegerTy::U16 => ScalarValue::U16(value as u16), + IntegerTy::U32 => ScalarValue::U32(value as u32), + IntegerTy::U64 => ScalarValue::U64(value as u64), + IntegerTy::U128 => ScalarValue::U128(value), + IntegerTy::Usize => ScalarValue::Usize(value as u64), + }; + (scalar_val, BlockId::from_usize(bb)) + }) + .collect(); + let otherwise = BlockId::from_usize(targets.otherwise()); + CharonSwitchTargets::SwitchInt(int_ty, branches, otherwise) + }; + (discr, switch_targets) + } + + fn translate_projection(&self, projection: &[ProjectionElem]) -> Vec { + projection.iter().map(|elem| self.translate_projection_elem(elem)).collect() + } + + fn translate_projection_elem(&self, projection_elem: &ProjectionElem) -> CharonProjectionElem { + match projection_elem { + ProjectionElem::Deref => CharonProjectionElem::Deref, + _ => todo!(), + } + } + + fn translate_region(&self, region: Region) -> CharonRegion { + match region.kind { + RegionKind::ReStatic => CharonRegion::Static, + RegionKind::ReErased => CharonRegion::Erased, + RegionKind::ReEarlyParam(_) + | RegionKind::ReBound(_, _) + | RegionKind::RePlaceholder(_) => todo!(), + } + } +} + +fn translate_int_ty(int_ty: IntTy) -> IntegerTy { + match int_ty { + IntTy::I8 => IntegerTy::I8, + IntTy::I16 => IntegerTy::I16, + IntTy::I32 => IntegerTy::I32, + IntTy::I64 => IntegerTy::I64, + IntTy::I128 => IntegerTy::I128, + // TODO: assumes 64-bit platform + IntTy::Isize => IntegerTy::I64, + } +} + +fn translate_uint_ty(uint_ty: UintTy) -> IntegerTy { + match uint_ty { + UintTy::U8 => IntegerTy::U8, + UintTy::U16 => IntegerTy::U16, + UintTy::U32 => IntegerTy::U32, + UintTy::U64 => IntegerTy::U64, + UintTy::U128 => IntegerTy::U128, + // TODO: assumes 64-bit platform + UintTy::Usize => IntegerTy::U64, + } +} + +fn translate_bin_op(bin_op: BinOp) -> CharonBinOp { + match bin_op { + BinOp::Add | BinOp::AddUnchecked => CharonBinOp::Add, + BinOp::Sub | BinOp::SubUnchecked => CharonBinOp::Sub, + BinOp::Mul | BinOp::MulUnchecked => CharonBinOp::Mul, + BinOp::Div => CharonBinOp::Div, + BinOp::Rem => CharonBinOp::Rem, + BinOp::BitXor => CharonBinOp::BitXor, + BinOp::BitAnd => CharonBinOp::BitAnd, + BinOp::BitOr => CharonBinOp::BitOr, + BinOp::Shl | BinOp::ShlUnchecked => CharonBinOp::Shl, + BinOp::Shr | BinOp::ShrUnchecked => CharonBinOp::Shr, + BinOp::Eq => CharonBinOp::Eq, + BinOp::Lt => CharonBinOp::Lt, + BinOp::Le => CharonBinOp::Le, + BinOp::Ne => CharonBinOp::Ne, + BinOp::Ge => CharonBinOp::Ge, + BinOp::Gt => CharonBinOp::Gt, + BinOp::Cmp => todo!(), + BinOp::Offset => todo!(), + } +} + +fn translate_borrow_kind(kind: &BorrowKind) -> CharonBorrowKind { + match kind { + BorrowKind::Shared => CharonBorrowKind::Shared, + BorrowKind::Mut { .. } => CharonBorrowKind::Mut, + BorrowKind::Fake(_kind) => todo!(), + } +} diff --git a/kani-compiler/src/codegen_aeneas_llbc/mod.rs b/kani-compiler/src/codegen_aeneas_llbc/mod.rs new file mode 100644 index 000000000000..085c42ea4119 --- /dev/null +++ b/kani-compiler/src/codegen_aeneas_llbc/mod.rs @@ -0,0 +1,10 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This module hosts a codegen backend that produces low-level borrow calculus +//! (LLBC), which is the format defined by Charon/Aeneas + +mod compiler_interface; +mod mir_to_ullbc; + +pub use compiler_interface::LlbcCodegenBackend; diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index 58c22f940352..a6b6cf3a03af 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/kani-compiler/src/kani_compiler.rs @@ -15,7 +15,9 @@ //! in order to apply the stubs. For the subsequent runs, we add the stub configuration to //! `-C llvm-args`. -use crate::args::Arguments; +use crate::args::{Arguments, BackendOption}; +#[cfg(feature = "aeneas")] +use crate::codegen_aeneas_llbc::LlbcCodegenBackend; #[cfg(feature = "cprover")] use crate::codegen_cprover_gotoc::GotocCodegenBackend; use crate::kani_middle::check_crate_items; @@ -42,16 +44,37 @@ pub fn run(args: Vec) -> ExitCode { } } -/// Configure the cprover backend that generate goto-programs. -#[cfg(feature = "cprover")] +/// Configure the Aeneas backend that generates LLBC. +fn aeneas_backend(_queries: Arc>) -> Box { + #[cfg(feature = "aeneas")] + return Box::new(LlbcCodegenBackend::new(_queries)); + #[cfg(not(feature = "aeneas"))] + unreachable!() +} + +/// Configure the cprover backend that generates goto-programs. +fn cprover_backend(_queries: Arc>) -> Box { + #[cfg(feature = "cprover")] + return Box::new(GotocCodegenBackend::new(_queries)); + #[cfg(not(feature = "cprover"))] + unreachable!() +} + +#[cfg(any(feature = "aeneas", feature = "cprover"))] fn backend(queries: Arc>) -> Box { - Box::new(GotocCodegenBackend::new(queries)) + let backend = queries.lock().unwrap().args().backend; + match backend { + #[cfg(feature = "aeneas")] + BackendOption::Aeneas => aeneas_backend(queries), + #[cfg(feature = "cprover")] + BackendOption::CProver => cprover_backend(queries), + } } /// Fallback backend. It will trigger an error if no backend has been enabled. -#[cfg(not(feature = "cprover"))] +#[cfg(not(any(feature = "aeneas", feature = "cprover")))] fn backend(queries: Arc>) -> Box { - compile_error!("No backend is available. Only supported value today is `cprover`"); + compile_error!("No backend is available. Use `aeneas` or `cprover`."); } /// This object controls the compiler behavior. diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs index 3a7816c1b084..1ba05d990955 100644 --- a/kani-compiler/src/main.rs +++ b/kani-compiler/src/main.rs @@ -38,6 +38,8 @@ extern crate stable_mir; extern crate tempfile; mod args; +#[cfg(feature = "aeneas")] +mod codegen_aeneas_llbc; #[cfg(feature = "cprover")] mod codegen_cprover_gotoc; mod intrinsics; diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 573ad21ab31a..30c6bd7073a6 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -271,6 +271,10 @@ pub struct VerificationArgs { #[arg(long, hide_short_help = true)] pub coverage: bool, + /// Print final LLBC for Aeneas backend. This requires the `-Z aeneas` option. + #[arg(long, hide = true)] + pub print_llbc: bool, + /// Arguments to pass down to Cargo #[command(flatten)] pub cargo: CargoCommonArgs, @@ -609,6 +613,23 @@ impl ValidateArgs for VerificationArgs { )); } + if self.print_llbc && !self.common_args.unstable_features.contains(UnstableFeature::Aeneas) + { + return Err(Error::raw( + ErrorKind::MissingRequiredArgument, + "The `--print-llbc` argument is unstable and requires `-Z aeneas` to be used.", + )); + } + + // TODO: error out for other CBMC-backend-specific arguments + if self.common_args.unstable_features.contains(UnstableFeature::Aeneas) + && !self.cbmc_args.is_empty() + { + return Err(Error::raw( + ErrorKind::ArgumentConflict, + "The `--cbmc-args` argument cannot be used with -Z aeneas.", + )); + } Ok(()) } } @@ -899,4 +920,12 @@ mod tests { check_invalid_args("kani input.rs --package foo".split_whitespace()); check_invalid_args("kani input.rs --exclude bar --workspace".split_whitespace()); } + + #[test] + fn check_cbmc_args_aeneas_backend() { + let args = "kani input.rs -Z aeneas --enable-unstable --cbmc-args --object-bits 10" + .split_whitespace(); + let err = StandaloneArgs::try_parse_from(args).unwrap().validate().unwrap_err(); + assert_eq!(err.kind(), ErrorKind::ArgumentConflict); + } } diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index bc0e9d8361d7..b566f0ff79c7 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -193,6 +193,9 @@ crate-type = ["lib"] // Arguments that will only be passed to the target package. let mut pkg_args: Vec = vec![]; pkg_args.extend(["--".to_string(), self.reachability_arg()]); + if let Some(backend_arg) = self.backend_arg() { + pkg_args.push(backend_arg); + } let mut found_target = false; let packages = packages_to_verify(&self.args, &metadata)?; diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index 63ca71d5b8d1..e33fbe874946 100644 --- a/kani-driver/src/call_single_file.rs +++ b/kani-driver/src/call_single_file.rs @@ -53,6 +53,9 @@ impl KaniSession { ) -> Result<()> { let mut kani_args = self.kani_compiler_flags(); kani_args.push(format!("--reachability={}", self.reachability_mode())); + if self.args.common_args.unstable_features.contains(UnstableFeature::Aeneas) { + kani_args.push("--backend=aeneas".into()); + } let lib_path = lib_folder().unwrap(); let mut rustc_args = self.kani_rustc_flags(LibConfig::new(lib_path)); @@ -95,6 +98,14 @@ impl KaniSession { to_rustc_arg(vec![format!("--reachability={}", self.reachability_mode())]) } + pub fn backend_arg(&self) -> Option { + if self.args.common_args.unstable_features.contains(UnstableFeature::Aeneas) { + Some(to_rustc_arg(vec!["--backend=aeneas".into()])) + } else { + None + } + } + /// These arguments are arguments passed to kani-compiler that are `kani` compiler specific. pub fn kani_compiler_flags(&self) -> Vec { let mut flags = vec![check_version()]; @@ -142,11 +153,11 @@ impl KaniSession { flags.push("--ub-check=uninit".into()); } - flags.extend(self.args.common_args.unstable_features.as_arguments().map(str::to_string)); + if self.args.print_llbc { + flags.push("--print-llbc".into()); + } - // This argument will select the Kani flavour of the compiler. It will be removed before - // rustc driver is invoked. - flags.push("--goto-c".into()); + flags.extend(self.args.common_args.unstable_features.as_arguments().map(str::to_string)); flags } diff --git a/kani_metadata/src/unstable.rs b/kani_metadata/src/unstable.rs index 11df998c820f..abab48304914 100644 --- a/kani_metadata/src/unstable.rs +++ b/kani_metadata/src/unstable.rs @@ -88,6 +88,8 @@ pub enum UnstableFeature { /// Automatically check that no invalid value is produced which is considered UB in Rust. /// Note that this does not include checking uninitialized value. ValidValueChecks, + /// Aeneas/LLBC + Aeneas, /// Ghost state and shadow memory APIs. GhostState, /// Automatically check that uninitialized memory is not used. diff --git a/rustfmt.toml b/rustfmt.toml index 44cbfe4a3dc9..f895fafbbdef 100644 --- a/rustfmt.toml +++ b/rustfmt.toml @@ -15,4 +15,5 @@ ignore = [ # For some reason, this is not working without the directory wildcard. "**/firecracker", "**/tests/perf/s2n-quic/", + "**/charon/charon/", ] diff --git a/scripts/codegen-firecracker.sh b/scripts/codegen-firecracker.sh index 3ac7dfa6585d..bffb27023412 100755 --- a/scripts/codegen-firecracker.sh +++ b/scripts/codegen-firecracker.sh @@ -42,7 +42,7 @@ RUST_FLAGS=( "--kani-compiler" "-Cpanic=abort" "-Zalways-encode-mir" - "-Cllvm-args=--goto-c" + "-Cllvm-args=--backend=cprover" "-Cllvm-args=--ignore-global-asm" "-Cllvm-args=--reachability=pub_fns" "--sysroot=${KANI_DIR}/target/kani" diff --git a/scripts/std-lib-regression.sh b/scripts/std-lib-regression.sh index a7881f1dc19a..b010da4581f6 100755 --- a/scripts/std-lib-regression.sh +++ b/scripts/std-lib-regression.sh @@ -71,7 +71,7 @@ RUST_FLAGS=( "--kani-compiler" "-Cpanic=abort" "-Zalways-encode-mir" - "-Cllvm-args=--goto-c" + "-Cllvm-args=--backend=cprover" "-Cllvm-args=--ignore-global-asm" "-Cllvm-args=--reachability=pub_fns" "-Cllvm-args=--build-std" diff --git a/tests/expected/llbc/basic0/expected b/tests/expected/llbc/basic0/expected new file mode 100644 index 000000000000..112a67a21548 --- /dev/null +++ b/tests/expected/llbc/basic0/expected @@ -0,0 +1,8 @@ +fn test::is_zero(@1: i32) -> bool\ +{\ + let @0: bool; // return\ + let @1: i32; // arg #1\ + + @0 := copy (@1) == const (0 : i32)\ + return\ +} diff --git a/tests/expected/llbc/basic0/test.rs b/tests/expected/llbc/basic0/test.rs new file mode 100644 index 000000000000..5025994ab31c --- /dev/null +++ b/tests/expected/llbc/basic0/test.rs @@ -0,0 +1,15 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zaeneas --print-llbc + +//! This test checks that Kani's LLBC backend handles basic expressions, in this +//! case an equality between a variable and a constant + +fn is_zero(i: i32) -> bool { + i == 0 +} + +#[kani::proof] +fn main() { + let _ = is_zero(0); +} diff --git a/tests/expected/llbc/basic1/expected b/tests/expected/llbc/basic1/expected new file mode 100644 index 000000000000..9cb0bef6f7c6 --- /dev/null +++ b/tests/expected/llbc/basic1/expected @@ -0,0 +1,15 @@ +fn test::select(@1: bool, @2: i32, @3: i32) -> i32 +{ + let @0: i32; // return + let @1: bool; // arg #1 + let @2: i32; // arg #2 + let @3: i32; // arg #3 + + if copy (@1) { + @0 := copy (@2) + } + else { + @0 := copy (@3) + } + return +} diff --git a/tests/expected/llbc/basic1/test.rs b/tests/expected/llbc/basic1/test.rs new file mode 100644 index 000000000000..92818fb93bfb --- /dev/null +++ b/tests/expected/llbc/basic1/test.rs @@ -0,0 +1,15 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zaeneas --print-llbc + +//! This test checks that Kani's LLBC backend handles basic expressions, in this +//! case an if condition + +fn select(s: bool, x: i32, y: i32) -> i32 { + if s { x } else { y } +} + +#[kani::proof] +fn main() { + let _ = select(true, 3, 7); +} From f17cc4d31e0f61055b4997c41cb84c5ece71aed8 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 8 Oct 2024 18:08:56 -0700 Subject: [PATCH 4/6] Bump Kani version to 0.56.0 (#3581) Bump our crates version and exclude `charon` from our workspace (otherwise building the workspace wouldn't work). See my comment for the original notes. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- CHANGELOG.md | 21 ++ Cargo.lock | 511 +++------------------------------ Cargo.toml | 3 +- cprover_bindings/Cargo.toml | 2 +- kani-compiler/Cargo.toml | 2 +- kani-driver/Cargo.toml | 2 +- kani_metadata/Cargo.toml | 2 +- library/kani/Cargo.toml | 2 +- library/kani_core/Cargo.toml | 2 +- library/kani_macros/Cargo.toml | 2 +- library/std/Cargo.toml | 2 +- tools/build-kani/Cargo.toml | 2 +- 12 files changed, 72 insertions(+), 481 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index e35af4c8fa24..23d740f534a9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,6 +4,27 @@ This file contains notable changes (e.g. breaking changes, major changes, etc.) This file was introduced starting Kani 0.23.0, so it only contains changes from version 0.23.0 onwards. +## [0.56.0] + +### Breaking Changes + +* Remove obsolete linker options (`--mir-linker` and `--legacy-linker`) by @zhassan-aws in https://github.com/model-checking/kani/pull/3559 +* Deprecate `kani::check` by @celinval in https://github.com/model-checking/kani/pull/3557 + +### What's Changed + +* Enable stubbing and function contracts for primitive types by @celinval in https://github.com/model-checking/kani/pull/3496 +* Instrument validity checks for pointer to reference casts for slices and str's by @zhassan-aws in https://github.com/model-checking/kani/pull/3513 +* Fail compilation if `proof_for_contract` is added to generic function by @carolynzech in https://github.com/model-checking/kani/pull/3522 +* Fix storing coverage data in cargo projects by @adpaco-aws in https://github.com/model-checking/kani/pull/3527 +* Add experimental API to generate arbitrary pointers by @celinval in https://github.com/model-checking/kani/pull/3538 +* Running `verify-std` no longer changes Cargo files by @celinval in https://github.com/model-checking/kani/pull/3577 +* Add an LLBC backend by @zhassan-aws in https://github.com/model-checking/kani/pull/3514 +* Rust toolchain upgraded to nightly-2024-10-03 by @qinheping @tautschnig @celinval +* CBMC upgraded to 6.3.1 by @tautschnig in https://github.com/model-checking/kani/pull/3537 + +**Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.55.0...kani-0.56.0 + ## [0.55.0] ### Major/Breaking Changes diff --git a/Cargo.lock b/Cargo.lock index 41fb02073f6a..21997d7bc332 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2,21 +2,6 @@ # It is not intended for manual editing. version = 4 -[[package]] -name = "addr2line" -version = "0.24.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "dfbe277e56a376000877090da837660b4427aad530e3028d44e0bffe4f89a1c1" -dependencies = [ - "gimli", -] - -[[package]] -name = "adler2" -version = "2.0.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "512761e0bb2578dd7380c6baaa0f4ce03e84f95e960231d1dec8bf4d7d6e2627" - [[package]] name = "ahash" version = "0.8.11" @@ -39,15 +24,6 @@ dependencies = [ "memchr", ] -[[package]] -name = "ansi_term" -version = "0.12.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d52a9bb7ec0cf484c551830a7ce27bd20d67eac647e1befb56b0be4ee39a55d2" -dependencies = [ - "winapi", -] - [[package]] name = "anstream" version = "0.6.15" @@ -131,59 +107,12 @@ dependencies = [ "wait-timeout", ] -[[package]] -name = "assert_tokens_eq" -version = "0.1.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6b21f4c5ba5c8b55031306325f196df925939bcc2bd7188ce68fabd93fb4f149" -dependencies = [ - "ansi_term", - "ctor", - "difference", - "output_vt100", - "snafu", -] - [[package]] name = "autocfg" version = "1.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ace50bade8e6234aa140d9a2f552bbee1db4d353f69b8217bc503490fc1a9f26" -[[package]] -name = "backtrace" -version = "0.3.74" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8d82cb332cdfaed17ae235a638438ac4d4839913cc2af585c3c6746e8f8bee1a" -dependencies = [ - "addr2line", - "cfg-if", - "libc", - "miniz_oxide", - "object", - "rustc-demangle", - "windows-targets 0.52.6", -] - -[[package]] -name = "bincode" -version = "2.0.0-rc.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f11ea1a0346b94ef188834a65c068a03aec181c94896d481d7a0a40d85b0ce95" -dependencies = [ - "bincode_derive", - "serde", -] - -[[package]] -name = "bincode_derive" -version = "2.0.0-rc.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7e30759b3b99a1b802a7a3aa21c85c3ded5c28e1c83170d82d70f08bbf7f3e4c" -dependencies = [ - "virtue", -] - [[package]] name = "bitflags" version = "2.6.0" @@ -221,7 +150,7 @@ dependencies = [ [[package]] name = "build-kani" -version = "0.55.0" +version = "0.56.0" dependencies = [ "anyhow", "cargo_metadata", @@ -295,14 +224,11 @@ dependencies = [ "derive-visitor", "env_logger", "hashlink", - "hax-frontend-exporter", - "ignore", "im", "index_vec", "indoc", "itertools 0.13.0", "lazy_static", - "libtest-mimic", "log", "macros", "nom", @@ -315,15 +241,12 @@ dependencies = [ "serde-map-to-array", "serde_json", "serde_stacker", - "snapbox", "stacker", "take_mut", - "tempfile", "toml", "tracing", "tracing-subscriber", "tracing-tree 0.3.1", - "walkdir", "which", ] @@ -356,8 +279,8 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "4ac6a0c7b1a9e9a5186361f67dfa1b88213572f427fb9ab038efb2bd8c582dab" dependencies = [ "heck", - "proc-macro2 1.0.86", - "quote 1.0.37", + "proc-macro2", + "quote", "syn 2.0.79", ] @@ -442,7 +365,7 @@ dependencies = [ [[package]] name = "cprover_bindings" -version = "0.55.0" +version = "0.56.0" dependencies = [ "lazy_static", "linear-map", @@ -523,16 +446,6 @@ dependencies = [ "memchr", ] -[[package]] -name = "ctor" -version = "0.1.26" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6d2301688392eb071b0bf1a37be05c469d3cc4dbbd95df672fe28ab021e6a096" -dependencies = [ - "quote 1.0.37", - "syn 1.0.109", -] - [[package]] name = "deranged" version = "0.3.11" @@ -548,8 +461,8 @@ version = "2.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "fcc3dd5e9e9c0b295d6e1e4d811fb6f157d5ffd784b8d202fc62eac8035a770b" dependencies = [ - "proc-macro2 1.0.86", - "quote 1.0.37", + "proc-macro2", + "quote", "syn 1.0.109", ] @@ -570,17 +483,11 @@ checksum = "427b39a85fecafea16b1a5f3f50437151022e35eb4fe038107f08adbf7f8def6" dependencies = [ "convert_case 0.4.0", "itertools 0.10.5", - "proc-macro2 1.0.86", - "quote 1.0.37", + "proc-macro2", + "quote", "syn 1.0.109", ] -[[package]] -name = "difference" -version = "2.0.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "524cbf6897b527295dff137cec09ecf3a05f4fddffd7dfcd1585403449e74198" - [[package]] name = "difflib" version = "0.4.0" @@ -593,12 +500,6 @@ version = "0.3.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "fea41bba32d969b513997752735605054bc0dfa92b4c56bf1189f2e174be7a10" -[[package]] -name = "dyn-clone" -version = "1.0.17" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0d6ef0072f8a535281e4876be788938b528e9a1d43900b82c2569af7da799125" - [[package]] name = "either" version = "1.13.0" @@ -650,41 +551,6 @@ dependencies = [ "windows-sys 0.52.0", ] -[[package]] -name = "escape8259" -version = "0.5.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5692dd7b5a1978a5aeb0ce83b7655c58ca8efdcb79d21036ea249da95afec2c6" - -[[package]] -name = "ext-trait" -version = "1.0.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d772df1c1a777963712fb68e014235e80863d6a91a85c4e06ba2d16243a310e5" -dependencies = [ - "ext-trait-proc_macros", -] - -[[package]] -name = "ext-trait-proc_macros" -version = "1.0.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1ab7934152eaf26aa5aa9f7371408ad5af4c31357073c9e84c3b9d7f11ad639a" -dependencies = [ - "proc-macro2 1.0.86", - "quote 1.0.37", - "syn 1.0.109", -] - -[[package]] -name = "extension-traits" -version = "1.0.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a296e5a895621edf9fa8329c83aa1cb69a964643e36cf54d8d7a69b789089537" -dependencies = [ - "ext-trait", -] - [[package]] name = "fastrand" version = "2.1.1" @@ -717,31 +583,12 @@ dependencies = [ "wasi", ] -[[package]] -name = "gimli" -version = "0.31.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "07e28edb80900c19c28f1072f2e8aeca7fa06b23cd4169cefe1af5aa3260783f" - [[package]] name = "glob" version = "0.3.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d2fabcfbdc87f4758337ca535fb41a6d701b65693ce38287d856d1674551ec9b" -[[package]] -name = "globset" -version = "0.4.15" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "15f1ce686646e7f1e19bf7d5533fe443a45dbfb990e00629110797578b42fb19" -dependencies = [ - "aho-corasick", - "bstr", - "log", - "regex-automata 0.4.8", - "regex-syntax 0.8.5", -] - [[package]] name = "graph-cycles" version = "0.1.0" @@ -778,59 +625,12 @@ dependencies = [ "serde", ] -[[package]] -name = "hax-adt-into" -version = "0.1.0-alpha.1" -source = "git+https://github.com/hacspec/hax?branch=main#496e381186de242f46ee2fd2b4b8971c70aa07a4" -dependencies = [ - "itertools 0.11.0", - "proc-macro2 1.0.86", - "quote 1.0.37", - "syn 1.0.109", -] - -[[package]] -name = "hax-frontend-exporter" -version = "0.1.0-alpha.1" -source = "git+https://github.com/hacspec/hax?branch=main#496e381186de242f46ee2fd2b4b8971c70aa07a4" -dependencies = [ - "bincode", - "extension-traits", - "hax-adt-into", - "hax-frontend-exporter-options", - "itertools 0.11.0", - "lazy_static", - "paste", - "schemars", - "serde", - "serde_json", - "tracing", -] - -[[package]] -name = "hax-frontend-exporter-options" -version = "0.1.0-alpha.1" -source = "git+https://github.com/hacspec/hax?branch=main#496e381186de242f46ee2fd2b4b8971c70aa07a4" -dependencies = [ - "bincode", - "hax-adt-into", - "schemars", - "serde", - "serde_json", -] - [[package]] name = "heck" version = "0.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "2304e00983f87ffb38b55b444b5e3b60a884b5d30c0fca7d82fe33449bbe55ea" -[[package]] -name = "hermit-abi" -version = "0.3.9" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d231dfb89cfffdbc30e7fc41579ed6066ad03abda9e567ccafae602b97ec5024" - [[package]] name = "home" version = "0.5.9" @@ -846,22 +646,6 @@ version = "2.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9a3a5bfb195931eeb336b2a7b4d761daec841b97f947d34394601737a7bba5e4" -[[package]] -name = "ignore" -version = "0.4.23" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6d89fd380afde86567dfba715db065673989d6253f42b88179abd3eae47bda4b" -dependencies = [ - "crossbeam-deque", - "globset", - "log", - "memchr", - "regex-automata 0.4.8", - "same-file", - "walkdir", - "winapi-util", -] - [[package]] name = "im" version = "15.1.0" @@ -922,15 +706,6 @@ dependencies = [ "either", ] -[[package]] -name = "itertools" -version = "0.11.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b1c173a5686ce8bfa551b3563d0c2170bf24ca44da99c7ca4bfdab5418c3fe57" -dependencies = [ - "either", -] - [[package]] name = "itertools" version = "0.13.0" @@ -954,7 +729,7 @@ checksum = "72167d68f5fce3b8655487b8038691a3c9984ee769590f93f2a631f4ad64e4f5" [[package]] name = "kani" -version = "0.55.0" +version = "0.56.0" dependencies = [ "kani_core", "kani_macros", @@ -962,7 +737,7 @@ dependencies = [ [[package]] name = "kani-compiler" -version = "0.55.0" +version = "0.56.0" dependencies = [ "charon", "clap", @@ -972,7 +747,7 @@ dependencies = [ "kani_metadata", "lazy_static", "num", - "quote 1.0.37", + "quote", "regex", "serde", "serde_json", @@ -987,7 +762,7 @@ dependencies = [ [[package]] name = "kani-driver" -version = "0.55.0" +version = "0.56.0" dependencies = [ "anyhow", "cargo_metadata", @@ -1016,7 +791,7 @@ dependencies = [ [[package]] name = "kani-verifier" -version = "0.55.0" +version = "0.56.0" dependencies = [ "anyhow", "home", @@ -1025,24 +800,24 @@ dependencies = [ [[package]] name = "kani_core" -version = "0.55.0" +version = "0.56.0" dependencies = [ "kani_macros", ] [[package]] name = "kani_macros" -version = "0.55.0" +version = "0.56.0" dependencies = [ "proc-macro-error2", - "proc-macro2 1.0.86", - "quote 1.0.37", + "proc-macro2", + "quote", "syn 2.0.79", ] [[package]] name = "kani_metadata" -version = "0.55.0" +version = "0.56.0" dependencies = [ "clap", "cprover_bindings", @@ -1063,18 +838,6 @@ version = "0.2.159" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "561d97a539a36e26a9a5fad1ea11a3039a67714694aaa379433e580854bc3dc5" -[[package]] -name = "libtest-mimic" -version = "0.7.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cc0bda45ed5b3a2904262c1bb91e526127aa70e7ef3758aba2ef93cf896b9b58" -dependencies = [ - "clap", - "escape8259", - "termcolor", - "threadpool", -] - [[package]] name = "linear-map" version = "1.2.0" @@ -1111,9 +874,8 @@ checksum = "a7a70ba024b9dc04c27ea2f0c0548feb474ec5c54bba33a7f72f873a39d07b24" name = "macros" version = "0.1.0" dependencies = [ - "assert_tokens_eq", - "proc-macro2 1.0.86", - "quote 1.0.37", + "proc-macro2", + "quote", "syn 2.0.79", ] @@ -1144,15 +906,6 @@ version = "0.2.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "68354c5c6bd36d73ff3feceb05efa59b6acb7626617f4962be322a825e61f79a" -[[package]] -name = "miniz_oxide" -version = "0.8.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e2d80299ef12ff69b16a84bb182e3b9df68b5a91574d3d4fa6e41b65deec4df1" -dependencies = [ - "adler2", -] - [[package]] name = "nom" version = "7.1.3" @@ -1176,12 +929,6 @@ dependencies = [ "nom", ] -[[package]] -name = "normalize-line-endings" -version = "0.3.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "61807f77802ff30975e01f4f071c8ba10c022052f98b3294119f3e615d13e5be" - [[package]] name = "nu-ansi-term" version = "0.46.0" @@ -1280,25 +1027,6 @@ dependencies = [ "autocfg", ] -[[package]] -name = "num_cpus" -version = "1.16.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4161fcb6d602d4d2081af7c3a45852d875a03dd337a6bfdd6e06407b61342a43" -dependencies = [ - "hermit-abi", - "libc", -] - -[[package]] -name = "object" -version = "0.36.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "aedf0a2d09c573ed1d8d85b30c119153926a2b36dce0ab28322c09a117a4683e" -dependencies = [ - "memchr", -] - [[package]] name = "once_cell" version = "1.20.2" @@ -1315,15 +1043,6 @@ dependencies = [ "windows-sys 0.52.0", ] -[[package]] -name = "output_vt100" -version = "0.1.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "628223faebab4e3e40667ee0b2336d34a5b960ff60ea743ddfdbcf7770bcfb66" -dependencies = [ - "winapi", -] - [[package]] name = "overload" version = "0.1.1" @@ -1353,12 +1072,6 @@ dependencies = [ "windows-targets 0.52.6", ] -[[package]] -name = "paste" -version = "1.0.15" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "57c0d7b74b563b49d38dae00a0c37d4d6de9b432382b2892f0574ddcae73fd0a" - [[package]] name = "pathdiff" version = "0.2.1" @@ -1440,8 +1153,8 @@ version = "2.0.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "96de42df36bb9bba5542fe9f1a054b8cc87e172759a1868aa05c1f3acc89dfc5" dependencies = [ - "proc-macro2 1.0.86", - "quote 1.0.37", + "proc-macro2", + "quote", ] [[package]] @@ -1451,20 +1164,11 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "11ec05c52be0a07b08061f7dd003e7d7092e0472bc731b4af7bb1ef876109802" dependencies = [ "proc-macro-error-attr2", - "proc-macro2 1.0.86", - "quote 1.0.37", + "proc-macro2", + "quote", "syn 2.0.79", ] -[[package]] -name = "proc-macro2" -version = "0.4.30" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cf3d2011ab5c909338f7887f4fc896d35932e29146c12c8d01da6b22a80ba759" -dependencies = [ - "unicode-xid", -] - [[package]] name = "proc-macro2" version = "1.0.86" @@ -1483,22 +1187,13 @@ dependencies = [ "cc", ] -[[package]] -name = "quote" -version = "0.6.13" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6ce23b6b870e8f94f81fb0a363d65d86675884b34a09043c81e5562f11c1f8e1" -dependencies = [ - "proc-macro2 0.4.30", -] - [[package]] name = "quote" version = "1.0.37" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b5b9d34b8991d19d98081b46eacdd8eb58c6f2b201139f7c5f643cc155a633af" dependencies = [ - "proc-macro2 1.0.86", + "proc-macro2", ] [[package]] @@ -1674,30 +1369,6 @@ dependencies = [ "strum_macros", ] -[[package]] -name = "schemars" -version = "0.8.21" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "09c024468a378b7e36765cd36702b7a90cc3cba11654f6685c8f233408e89e92" -dependencies = [ - "dyn-clone", - "schemars_derive", - "serde", - "serde_json", -] - -[[package]] -name = "schemars_derive" -version = "0.8.21" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b1eee588578aff73f856ab961cd2f79e36bc45d7ded33a7562adba4667aecc0e" -dependencies = [ - "proc-macro2 1.0.86", - "quote 1.0.37", - "serde_derive_internals", - "syn 2.0.79", -] - [[package]] name = "scopeguard" version = "1.2.0" @@ -1737,19 +1408,8 @@ version = "1.0.210" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "243902eda00fad750862fc144cea25caca5e20d615af0a81bee94ca738f1df1f" dependencies = [ - "proc-macro2 1.0.86", - "quote 1.0.37", - "syn 2.0.79", -] - -[[package]] -name = "serde_derive_internals" -version = "0.29.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "18d26a20a969b9e3fdf2fc2d9f21eda6c40e2de84c9408bb5d3b05d499aae711" -dependencies = [ - "proc-macro2 1.0.86", - "quote 1.0.37", + "proc-macro2", + "quote", "syn 2.0.79", ] @@ -1827,12 +1487,6 @@ version = "1.3.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64" -[[package]] -name = "similar" -version = "2.6.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1de1d4f81173b03af4c0cbed3c898f6bff5b870e4a7f5d6f4057d62a7a4b686e" - [[package]] name = "sized-chunks" version = "0.6.5" @@ -1849,50 +1503,6 @@ version = "1.13.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "3c5e1a9a646d36c3599cd173a41282daf47c44583ad367b8e6837255952e5c67" -[[package]] -name = "snafu" -version = "0.4.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b028158eb06caa8345bee10cccfb25fa632beccf0ef5308832b4fd4b78a7db48" -dependencies = [ - "backtrace", - "doc-comment", - "snafu-derive", -] - -[[package]] -name = "snafu-derive" -version = "0.4.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bf50aaef500c248a590e2696e8bf8c7620ca2235b9bb90a70363d82dd1abec6a" -dependencies = [ - "proc-macro2 0.4.30", - "quote 0.6.13", - "syn 0.15.44", -] - -[[package]] -name = "snapbox" -version = "0.6.18" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7ba434818a8a9b1b106404288d6bd75a94348aae8fc9a518b211b609a36a54bc" -dependencies = [ - "anstream", - "anstyle", - "normalize-line-endings", - "similar", - "snapbox-macros", -] - -[[package]] -name = "snapbox-macros" -version = "0.3.10" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "16569f53ca23a41bb6f62e0a5084aa1661f4814a67fa33696a79073e03a664af" -dependencies = [ - "anstream", -] - [[package]] name = "stacker" version = "0.1.17" @@ -1908,7 +1518,7 @@ dependencies = [ [[package]] name = "std" -version = "0.55.0" +version = "0.56.0" dependencies = [ "kani", ] @@ -1943,31 +1553,20 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "4c6bee85a5a24955dc440386795aa378cd9cf82acd5f764469152d2270e581be" dependencies = [ "heck", - "proc-macro2 1.0.86", - "quote 1.0.37", + "proc-macro2", + "quote", "rustversion", "syn 2.0.79", ] -[[package]] -name = "syn" -version = "0.15.44" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9ca4b3b69a77cbe1ffc9e198781b7acb0c7365a883670e8f1c1bc66fba79a5c5" -dependencies = [ - "proc-macro2 0.4.30", - "quote 0.6.13", - "unicode-xid", -] - [[package]] name = "syn" version = "1.0.109" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237" dependencies = [ - "proc-macro2 1.0.86", - "quote 1.0.37", + "proc-macro2", + "quote", "unicode-ident", ] @@ -1977,8 +1576,8 @@ version = "2.0.79" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "89132cd0bf050864e1d38dc3bbc07a0eb8e7530af26344d3d2bbbef83499f590" dependencies = [ - "proc-macro2 1.0.86", - "quote 1.0.37", + "proc-macro2", + "quote", "unicode-ident", ] @@ -2001,15 +1600,6 @@ dependencies = [ "windows-sys 0.59.0", ] -[[package]] -name = "termcolor" -version = "1.4.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "06794f8f6c5c898b3275aebefa6b8a1cb24cd2c6c79397ab15774837a0bc5755" -dependencies = [ - "winapi-util", -] - [[package]] name = "termtree" version = "0.4.1" @@ -2031,8 +1621,8 @@ version = "1.0.64" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "08904e7672f5eb876eaaf87e0ce17857500934f4981c4a0ab2b4aa98baac7fc3" dependencies = [ - "proc-macro2 1.0.86", - "quote 1.0.37", + "proc-macro2", + "quote", "syn 2.0.79", ] @@ -2046,15 +1636,6 @@ dependencies = [ "once_cell", ] -[[package]] -name = "threadpool" -version = "1.8.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d050e60b33d41c19108b32cea32164033a9013fe3b46cbd4457559bfbf77afaa" -dependencies = [ - "num_cpus", -] - [[package]] name = "time" version = "0.3.36" @@ -2137,8 +1718,8 @@ version = "0.1.27" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "34704c8d6ebcbc939824180af020566b01a7c01f80641264eba0999f6c2b6be7" dependencies = [ - "proc-macro2 1.0.86", - "quote 1.0.37", + "proc-macro2", + "quote", "syn 2.0.79", ] @@ -2249,12 +1830,6 @@ version = "0.1.14" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "7dd6e30e90baa6f72411720665d41d89b9a3d039dc45b8faea1ddd07f617f6af" -[[package]] -name = "unicode-xid" -version = "0.1.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fc72304796d0818e357ead4e000d19c9c174ab23dc11093ac919054d20a6a7fc" - [[package]] name = "unsafe-libyaml" version = "0.2.11" @@ -2279,12 +1854,6 @@ version = "0.9.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a" -[[package]] -name = "virtue" -version = "0.0.13" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9dcc60c0624df774c82a0ef104151231d37da4962957d691c011c852b2473314" - [[package]] name = "wait-timeout" version = "0.2.0" @@ -2532,7 +2101,7 @@ version = "0.7.35" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e" dependencies = [ - "proc-macro2 1.0.86", - "quote 1.0.37", + "proc-macro2", + "quote", "syn 2.0.79", ] diff --git a/Cargo.toml b/Cargo.toml index ee9848b578dc..42c6f2c722b6 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-verifier" -version = "0.55.0" +version = "0.56.0" edition = "2021" description = "A bit-precise model checker for Rust." readme = "README.md" @@ -56,6 +56,7 @@ default-members = [ exclude = [ "build", + "charon", "target", # dependency tests have their own workspace "tests/kani-dependency-test/dependency3", diff --git a/cprover_bindings/Cargo.toml b/cprover_bindings/Cargo.toml index 008c81aef2ad..e26f23d5c081 100644 --- a/cprover_bindings/Cargo.toml +++ b/cprover_bindings/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "cprover_bindings" -version = "0.55.0" +version = "0.56.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index 0360763f9068..7b17e6073bb3 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-compiler" -version = "0.55.0" +version = "0.56.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index 7485d2279ad6..555534959474 100644 --- a/kani-driver/Cargo.toml +++ b/kani-driver/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-driver" -version = "0.55.0" +version = "0.56.0" edition = "2021" description = "Build a project with Kani and run all proof harnesses" license = "MIT OR Apache-2.0" diff --git a/kani_metadata/Cargo.toml b/kani_metadata/Cargo.toml index 18eadc4095ed..2a0a03401c40 100644 --- a/kani_metadata/Cargo.toml +++ b/kani_metadata/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_metadata" -version = "0.55.0" +version = "0.56.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani/Cargo.toml b/library/kani/Cargo.toml index fa50783516f4..3ad1b286ebe6 100644 --- a/library/kani/Cargo.toml +++ b/library/kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani" -version = "0.55.0" +version = "0.56.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani_core/Cargo.toml b/library/kani_core/Cargo.toml index 447cd0b3f298..df55e6278282 100644 --- a/library/kani_core/Cargo.toml +++ b/library/kani_core/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_core" -version = "0.55.0" +version = "0.56.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani_macros/Cargo.toml b/library/kani_macros/Cargo.toml index 6930366b84fc..a7876176adb2 100644 --- a/library/kani_macros/Cargo.toml +++ b/library/kani_macros/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_macros" -version = "0.55.0" +version = "0.56.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/std/Cargo.toml b/library/std/Cargo.toml index 12c923e9b655..e1e353704723 100644 --- a/library/std/Cargo.toml +++ b/library/std/Cargo.toml @@ -5,7 +5,7 @@ # Note: this package is intentionally named std to make sure the names of # standard library symbols are preserved name = "std" -version = "0.55.0" +version = "0.56.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/tools/build-kani/Cargo.toml b/tools/build-kani/Cargo.toml index 41095f1d7c3c..25e022e70d3f 100644 --- a/tools/build-kani/Cargo.toml +++ b/tools/build-kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "build-kani" -version = "0.55.0" +version = "0.56.0" edition = "2021" description = "Builds Kani, Sysroot and release bundle." license = "MIT OR Apache-2.0" From c64575219fc672f3884a2e965f5f1438c7d2033c Mon Sep 17 00:00:00 2001 From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Date: Wed, 9 Oct 2024 08:55:32 -0700 Subject: [PATCH 5/6] Fix the computation of the number of bytes of a pointer offset (#3584) This PR fixes the logic that computes the number of bytes of a pointer offset. The logic was incorrectly using the size of the pointer as opposed to the size of the pointee. This fixes the soundness issue in #3582 (but not the spurious failures). By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- .../codegen_cprover_gotoc/codegen/rvalue.rs | 2 +- .../offset-from-bytes-overflow/expected | 2 +- tests/expected/offset-overflow/expected | 2 +- tests/expected/offset-overflow/main.rs | 9 ++++--- tests/expected/ptr-offset-overflow/expected | 5 ++++ tests/expected/ptr-offset-overflow/main.rs | 27 +++++++++++++++++++ 6 files changed, 41 insertions(+), 6 deletions(-) create mode 100644 tests/expected/ptr-offset-overflow/expected create mode 100644 tests/expected/ptr-offset-overflow/main.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 7a4594a181e3..14e012aac76b 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -410,7 +410,7 @@ impl<'tcx> GotocCtx<'tcx> { // Check that computing `offset` in bytes would not overflow let (offset_bytes, bytes_overflow_check) = self.count_in_bytes( ce2.clone().cast_to(Type::ssize_t()), - ty, + pointee_type_stable(ty).unwrap(), Type::ssize_t(), "offset", loc, diff --git a/tests/expected/offset-from-bytes-overflow/expected b/tests/expected/offset-from-bytes-overflow/expected index 9613638bf8f9..bcf0242f9e9d 100644 --- a/tests/expected/offset-from-bytes-overflow/expected +++ b/tests/expected/offset-from-bytes-overflow/expected @@ -1,2 +1,2 @@ FAILURE\ -attempt to compute offset which would overflow +attempt to compute number in bytes which would overflow diff --git a/tests/expected/offset-overflow/expected b/tests/expected/offset-overflow/expected index 72ded2ac24c1..bcf0242f9e9d 100644 --- a/tests/expected/offset-overflow/expected +++ b/tests/expected/offset-overflow/expected @@ -1,2 +1,2 @@ FAILURE\ -attempt to compute offset which would overflow \ No newline at end of file +attempt to compute number in bytes which would overflow diff --git a/tests/expected/offset-overflow/main.rs b/tests/expected/offset-overflow/main.rs index 55b79df854cc..43f294848012 100644 --- a/tests/expected/offset-overflow/main.rs +++ b/tests/expected/offset-overflow/main.rs @@ -8,10 +8,13 @@ use std::intrinsics::offset; #[kani::proof] fn test_offset_overflow() { - let s: &str = "123"; - let ptr: *const u8 = s.as_ptr(); + let a: [i32; 3] = [1, 2, 3]; + let ptr: *const i32 = a.as_ptr(); + // a value that when multiplied by the size of i32 (i.e. 4 bytes) + // would overflow `isize` + let count: isize = isize::MAX / 4 + 1; unsafe { - let _d = offset(ptr, isize::MAX / 8); + let _d = offset(ptr, count); } } diff --git a/tests/expected/ptr-offset-overflow/expected b/tests/expected/ptr-offset-overflow/expected new file mode 100644 index 000000000000..ad33ce91dabb --- /dev/null +++ b/tests/expected/ptr-offset-overflow/expected @@ -0,0 +1,5 @@ +std::ptr::const_ptr::::offset.arithmetic_overflow\ +Status: FAILURE\ +Description: "offset: attempt to compute number in bytes which would overflow" + +VERIFICATION:- FAILED diff --git a/tests/expected/ptr-offset-overflow/main.rs b/tests/expected/ptr-offset-overflow/main.rs new file mode 100644 index 000000000000..d2877addb923 --- /dev/null +++ b/tests/expected/ptr-offset-overflow/main.rs @@ -0,0 +1,27 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This test checks that Kani detects the overflow in pointer offset + +use std::convert::TryFrom; + +struct Foo { + arr: [i32; 4096], +} + +#[cfg_attr(kani, kani::proof)] +fn main() { + let f = Foo { arr: [0; 4096] }; + assert_eq!(std::mem::size_of::(), 16384); + // a large enough count that causes `count * size_of::()` to overflow + // `isize` without overflowing `usize` + let count: usize = 562949953421320; + // the `unwrap` ensures that it indeed doesn't overflow `usize` + let bytes = count.checked_mul(std::mem::size_of::()).unwrap(); + // ensure that it overflows `isize`: + assert!(isize::try_from(bytes).is_err()); + + let ptr: *const Foo = &f as *const Foo; + // this should fail because `count * size_of::` overflows `isize` + let _p = unsafe { ptr.offset(count as isize) }; +} From 04000248aaa2d44d2c990c059542c9245c78eab0 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Wed, 9 Oct 2024 12:27:13 -0400 Subject: [PATCH 6/6] List Subcommand (Implementation) (#3523) Implementation of the list subcommand (and updates to the RFC). As a larger test, I ran on the standard library (`kani list -Z list -Z function-contracts -Z mem-predicates ./library --std`) and manually verified that the results were correct. I pasted the output below. Contracts: | | Function | Contract Harnesses (#[kani::proof_for_contract]) | | ----- | ------------------------------------------------ | ------------------------------------------------------ | | | alloc::layout::Layout::from_size_align_unchecked | alloc::layout::verify::check_from_size_align_unchecked | | | ascii::ascii_char::AsciiChar::from_u8 | ascii::ascii_char::verify::check_from_u8 | | | ascii::ascii_char::AsciiChar::from_u8_unchecked | ascii::ascii_char::verify::check_from_u8_unchecked | | | char::convert::from_u32_unchecked | char::convert::verify::check_from_u32_unchecked | | | char::methods::verify::as_ascii_clone | char::methods::verify::check_as_ascii_ascii_char | | | | char::methods::verify::check_as_ascii_non_ascii_char | | | intrinsics::typed_swap | intrinsics::verify::check_typed_swap_u8 | | | | intrinsics::verify::check_typed_swap_char | | | | intrinsics::verify::check_typed_swap_non_zero | | | mem::swap | mem::verify::check_swap_primitive | | | | mem::verify::check_swap_adt_no_drop | | | ptr::align_offset | ptr::verify::check_align_offset_zst | | | | ptr::verify::check_align_offset_u8 | | | | ptr::verify::check_align_offset_u16 | | | | ptr::verify::check_align_offset_u32 | | | | ptr::verify::check_align_offset_u64 | | | | ptr::verify::check_align_offset_u128 | | | | ptr::verify::check_align_offset_4096 | | | | ptr::verify::check_align_offset_5 | | | ptr::alignment::Alignment::as_nonzero | ptr::alignment::verify::check_as_nonzero | | | ptr::alignment::Alignment::as_usize | ptr::alignment::verify::check_as_usize | | | ptr::alignment::Alignment::log2 | ptr::alignment::verify::check_log2 | | | ptr::alignment::Alignment::mask | ptr::alignment::verify::check_mask | | | ptr::alignment::Alignment::new | ptr::alignment::verify::check_new | | | ptr::alignment::Alignment::new_unchecked | ptr::alignment::verify::check_new_unchecked | | | ptr::alignment::Alignment::of | ptr::alignment::verify::check_of_i32 | | | ptr::non_null::NonNull::::new | ptr::non_null::verify::non_null_check_new | | | ptr::non_null::NonNull::::new_unchecked | ptr::non_null::verify::non_null_check_new_unchecked | | | ptr::read_volatile | ptr::verify::check_read_u128 | | | ptr::unique::Unique::::as_non_null_ptr | ptr::unique::verify::check_as_non_null_ptr | | | ptr::unique::Unique::::as_ptr | ptr::unique::verify::check_as_ptr | | | ptr::unique::Unique::::new | ptr::unique::verify::check_new | | | ptr::unique::Unique::::new_unchecked | ptr::unique::verify::check_new_unchecked | | | ptr::verify::mod_inv_copy | ptr::verify::check_mod_inv | | | ptr::write_volatile | NONE | | Total | 24 | 34 | Standard Harnesses (#[kani::proof]): 1. ptr::unique::verify::check_as_mut 2. ptr::unique::verify::check_as_ref 3. ptr::unique::verify::check_cast Terminal view (`--pretty` format): list By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Felipe R. Monteiro Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- Cargo.lock | 11 ++ .../compiler_interface.rs | 7 +- .../src/kani_middle/codegen_units.rs | 7 +- kani-compiler/src/kani_middle/metadata.rs | 51 ++++- kani-driver/Cargo.toml | 3 +- kani-driver/src/args/list_args.rs | 127 ++++++++++++ kani-driver/src/args/mod.rs | 8 + kani-driver/src/list/collect_metadata.rs | 101 ++++++++++ kani-driver/src/list/mod.rs | 14 ++ kani-driver/src/list/output.rs | 180 ++++++++++++++++++ kani-driver/src/main.rs | 8 + kani-driver/src/metadata.rs | 2 + kani-driver/src/version.rs | 2 +- kani_metadata/src/lib.rs | 15 +- kani_metadata/src/unstable.rs | 2 + rfc/src/rfcs/0013-list.md | 112 ++++++----- tests/script-based-pre/cargo_list/Cargo.toml | 10 + tests/script-based-pre/cargo_list/config.yml | 4 + .../script-based-pre/cargo_list/list.expected | 52 +++++ tests/script-based-pre/cargo_list/list.sh | 10 + tests/script-based-pre/cargo_list/src/lib.rs | 68 +++++++ .../cargo_list/src/standard_harnesses.rs | 15 ++ tests/script-based-pre/kani_list/config.yml | 4 + .../script-based-pre/kani_list/list.expected | 52 +++++ tests/script-based-pre/kani_list/list.sh | 10 + tests/script-based-pre/kani_list/src/lib.rs | 71 +++++++ 26 files changed, 883 insertions(+), 63 deletions(-) create mode 100644 kani-driver/src/args/list_args.rs create mode 100644 kani-driver/src/list/collect_metadata.rs create mode 100644 kani-driver/src/list/mod.rs create mode 100644 kani-driver/src/list/output.rs create mode 100644 tests/script-based-pre/cargo_list/Cargo.toml create mode 100644 tests/script-based-pre/cargo_list/config.yml create mode 100644 tests/script-based-pre/cargo_list/list.expected create mode 100755 tests/script-based-pre/cargo_list/list.sh create mode 100644 tests/script-based-pre/cargo_list/src/lib.rs create mode 100644 tests/script-based-pre/cargo_list/src/standard_harnesses.rs create mode 100644 tests/script-based-pre/kani_list/config.yml create mode 100644 tests/script-based-pre/kani_list/list.expected create mode 100755 tests/script-based-pre/kani_list/list.sh create mode 100644 tests/script-based-pre/kani_list/src/lib.rs diff --git a/Cargo.lock b/Cargo.lock index 21997d7bc332..580cdf70946a 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -306,6 +306,15 @@ dependencies = [ "windows-sys 0.48.0", ] +[[package]] +name = "colour" +version = "2.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b536eebcabe54980476d120a182f7da2268fe02d22575cca99cee5fdda178280" +dependencies = [ + "winapi", +] + [[package]] name = "comfy-table" version = "7.1.1" @@ -767,6 +776,7 @@ dependencies = [ "anyhow", "cargo_metadata", "clap", + "colour", "comfy-table", "console", "glob", @@ -1419,6 +1429,7 @@ version = "1.0.128" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "6ff5456707a1de34e7e37f2a6fd3d3f808c318259cbd01ab6377795054b483d8" dependencies = [ + "indexmap", "itoa", "memchr", "ryu", diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index da211c58946c..25bc0cbe8ad1 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -20,9 +20,8 @@ use cbmc::RoundingMode; use cbmc::goto_program::Location; use cbmc::irep::goto_binary_serde::write_goto_binary_file; use cbmc::{InternedString, MachineModel}; -use kani_metadata::UnsupportedFeature; use kani_metadata::artifact::convert_type; -use kani_metadata::{ArtifactType, HarnessMetadata, KaniMetadata}; +use kani_metadata::{ArtifactType, HarnessMetadata, KaniMetadata, UnsupportedFeature}; use kani_metadata::{AssignsContract, CompilerArtifactStub}; use rustc_codegen_ssa::back::archive::{ ArArchiveBuilder, ArchiveBuilder, ArchiveBuilderBuilder, DEFAULT_OBJECT_READER, @@ -643,6 +642,10 @@ impl GotoCodegenResults { proof_harnesses: proofs, unsupported_features, test_harnesses: tests, + // We don't collect the contracts metadata because the FunctionWithContractPass + // removes any contracts logic for ReachabilityType::Test or ReachabilityType::PubFns, + // which are the two ReachabilityTypes under which the compiler calls this function. + contracted_functions: vec![], } } diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 071e880ffd9f..ebb12f7656b6 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -9,7 +9,7 @@ use crate::args::ReachabilityType; use crate::kani_middle::attributes::is_proof_harness; -use crate::kani_middle::metadata::gen_proof_metadata; +use crate::kani_middle::metadata::{gen_contracts_metadata, gen_proof_metadata}; use crate::kani_middle::reachability::filter_crate_items; use crate::kani_middle::resolve::expect_resolve_fn; use crate::kani_middle::stubbing::{check_compatibility, harness_stub_map}; @@ -93,7 +93,7 @@ impl CodegenUnits { /// Write compilation metadata into a file. pub fn write_metadata(&self, queries: &QueryDb, tcx: TyCtxt) { - let metadata = self.generate_metadata(); + let metadata = self.generate_metadata(tcx); let outpath = metadata_output_path(tcx); store_metadata(queries, &metadata, &outpath); } @@ -103,7 +103,7 @@ impl CodegenUnits { } /// Generate [KaniMetadata] for the target crate. - fn generate_metadata(&self) -> KaniMetadata { + fn generate_metadata(&self, tcx: TyCtxt) -> KaniMetadata { let (proof_harnesses, test_harnesses) = self.harness_info.values().cloned().partition(|md| md.attributes.is_proof_harness()); KaniMetadata { @@ -111,6 +111,7 @@ impl CodegenUnits { proof_harnesses, unsupported_features: vec![], test_harnesses, + contracted_functions: gen_contracts_metadata(tcx), } } } diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs index db6b6b06149a..c92b20cf49d6 100644 --- a/kani-compiler/src/kani_middle/metadata.rs +++ b/kani-compiler/src/kani_middle/metadata.rs @@ -3,15 +3,16 @@ //! This module handles Kani metadata generation. For example, generating HarnessMetadata for a //! given function. +use std::collections::HashMap; use std::path::Path; -use crate::kani_middle::attributes::test_harness_name; +use crate::kani_middle::attributes::{KaniAttributes, test_harness_name}; +use crate::kani_middle::{SourceLocation, stable_fn_def}; +use kani_metadata::ContractedFunction; use kani_metadata::{ArtifactType, HarnessAttributes, HarnessKind, HarnessMetadata}; use rustc_middle::ty::TyCtxt; -use stable_mir::CrateDef; use stable_mir::mir::mono::Instance; - -use super::{SourceLocation, attributes::KaniAttributes}; +use stable_mir::{CrateDef, CrateItems, DefId}; /// Create the harness metadata for a proof harness for a given function. pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) -> HarnessMetadata { @@ -40,6 +41,48 @@ pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) -> } } +/// Collects contract and contract harness metadata. +/// +/// For each function with contracts (or that is a target of a contract harness), +/// construct a `ContractedFunction` object for it. +pub fn gen_contracts_metadata(tcx: TyCtxt) -> Vec { + // We work with `stable_mir::CrateItem` instead of `stable_mir::Instance` to include generic items + let crate_items: CrateItems = stable_mir::all_local_items(); + + let mut fn_to_data: HashMap = HashMap::new(); + + for item in crate_items { + let function = item.name(); + let file = SourceLocation::new(item.span()).filename; + let attributes = KaniAttributes::for_def_id(tcx, item.def_id()); + + if attributes.has_contract() { + fn_to_data.insert(item.def_id(), ContractedFunction { + function, + file, + harnesses: vec![], + }); + } else if let Some((target_name, internal_def_id, _)) = + attributes.interpret_for_contract_attribute() + { + let target_def_id = stable_fn_def(tcx, internal_def_id) + .expect("The target of a proof for contract should be a function definition") + .def_id(); + if let Some(cf) = fn_to_data.get_mut(&target_def_id) { + cf.harnesses.push(function); + } else { + fn_to_data.insert(target_def_id, ContractedFunction { + function: target_name.to_string(), + file, + harnesses: vec![function], + }); + } + } + } + + fn_to_data.into_values().collect() +} + /// Create the harness metadata for a test description. #[allow(dead_code)] pub fn gen_test_metadata( diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index 555534959474..67214738fa7c 100644 --- a/kani-driver/Cargo.toml +++ b/kani-driver/Cargo.toml @@ -18,8 +18,9 @@ anyhow = "1" console = "0.15.1" once_cell = "1.19.0" serde = { version = "1", features = ["derive"] } -serde_json = "1" +serde_json = { version = "1", features = ["preserve_order"] } clap = { version = "4.4.11", features = ["derive"] } +colour = "2.1.0" glob = "0.3" toml = "0.8" regex = "1.6" diff --git a/kani-driver/src/args/list_args.rs b/kani-driver/src/args/list_args.rs new file mode 100644 index 000000000000..7129bd0a85c4 --- /dev/null +++ b/kani-driver/src/args/list_args.rs @@ -0,0 +1,127 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Implements the subcommand handling of the list subcommand + +use std::path::PathBuf; + +use crate::args::ValidateArgs; +use clap::{Error, Parser, ValueEnum, error::ErrorKind}; +use kani_metadata::UnstableFeature; + +use super::VerificationArgs; + +/// List information relevant to verification +#[derive(Debug, Parser)] +pub struct CargoListArgs { + #[command(flatten)] + pub verify_opts: VerificationArgs, + + /// Output format + #[clap(long, default_value = "pretty")] + pub format: Format, +} + +/// List information relevant to verification +#[derive(Debug, Parser)] +pub struct StandaloneListArgs { + /// Rust file to verify + #[arg(required = true)] + pub input: PathBuf, + + #[arg(long, hide = true)] + pub crate_name: Option, + + #[command(flatten)] + pub verify_opts: VerificationArgs, + + /// Output format + #[clap(long, default_value = "pretty")] + pub format: Format, + + /// Pass this flag to run the `list` command on the standard library. + /// Ensure that the provided `path` is the `library` folder. + #[arg(long)] + pub std: bool, +} + +/// Message formats available for the subcommand. +#[derive(Copy, Clone, Debug, PartialEq, Eq, ValueEnum, strum_macros::Display)] +#[strum(serialize_all = "kebab-case")] +pub enum Format { + /// Print diagnostic messages in a user friendly format. + Pretty, + /// Print diagnostic messages in JSON format. + Json, +} + +impl ValidateArgs for CargoListArgs { + fn validate(&self) -> Result<(), Error> { + self.verify_opts.validate()?; + if !self.verify_opts.common_args.unstable_features.contains(UnstableFeature::List) { + return Err(Error::raw( + ErrorKind::MissingRequiredArgument, + "The `list` subcommand is unstable and requires -Z list", + )); + } + + Ok(()) + } +} + +impl ValidateArgs for StandaloneListArgs { + fn validate(&self) -> Result<(), Error> { + self.verify_opts.validate()?; + if !self.verify_opts.common_args.unstable_features.contains(UnstableFeature::List) { + return Err(Error::raw( + ErrorKind::MissingRequiredArgument, + "The `list` subcommand is unstable and requires -Z list", + )); + } + + if self.std { + if !self.input.exists() { + Err(Error::raw( + ErrorKind::InvalidValue, + format!( + "Invalid argument: `` argument `{}` does not exist", + self.input.display() + ), + )) + } else if !self.input.is_dir() { + Err(Error::raw( + ErrorKind::InvalidValue, + format!( + "Invalid argument: `` argument `{}` is not a directory", + self.input.display() + ), + )) + } else { + let full_path = self.input.canonicalize()?; + let dir = full_path.file_stem().unwrap(); + if dir != "library" { + Err(Error::raw( + ErrorKind::InvalidValue, + format!( + "Invalid argument: Expected `` to point to the `library` folder \ + containing the standard library crates.\n\ + Found `{}` folder instead", + dir.to_string_lossy() + ), + )) + } else { + Ok(()) + } + } + } else if self.input.is_file() { + Ok(()) + } else { + Err(Error::raw( + ErrorKind::InvalidValue, + format!( + "Invalid argument: Input invalid. `{}` is not a regular file.", + self.input.display() + ), + )) + } + } +} diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 30c6bd7073a6..8aa758219524 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -5,6 +5,7 @@ pub mod assess_args; pub mod cargo; pub mod common; +pub mod list_args; pub mod playback_args; pub mod std_args; @@ -94,6 +95,8 @@ pub enum StandaloneSubcommand { Playback(Box), /// Verify the rust standard library. VerifyStd(Box), + /// Execute the list subcommand + List(Box), } #[derive(Debug, clap::Parser)] @@ -119,6 +122,9 @@ pub enum CargoKaniSubcommand { /// Execute concrete playback testcases of a local package. Playback(Box), + + /// List metadata relevant to verification, e.g., harnesses. + List(Box), } // Common arguments for invoking Kani for verification purpose. This gets put into KaniContext, @@ -421,6 +427,7 @@ impl ValidateArgs for StandaloneArgs { match &self.command { Some(StandaloneSubcommand::VerifyStd(args)) => args.validate()?, + Some(StandaloneSubcommand::List(args)) => args.validate()?, // TODO: Invoke PlaybackArgs::validate() None | Some(StandaloneSubcommand::Playback(..)) => {} }; @@ -467,6 +474,7 @@ impl ValidateArgs for CargoKaniSubcommand { // Assess doesn't implement validation yet. CargoKaniSubcommand::Assess(_) => Ok(()), CargoKaniSubcommand::Playback(playback) => playback.validate(), + CargoKaniSubcommand::List(list) => list.validate(), } } } diff --git a/kani-driver/src/list/collect_metadata.rs b/kani-driver/src/list/collect_metadata.rs new file mode 100644 index 000000000000..99da0477314d --- /dev/null +++ b/kani-driver/src/list/collect_metadata.rs @@ -0,0 +1,101 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// This module invokes the compiler to gather the metadata for the list subcommand, then post-processes the output. + +use std::collections::{BTreeMap, BTreeSet}; + +use crate::{ + InvocationType, + args::list_args::{CargoListArgs, Format, StandaloneListArgs}, + list::Totals, + list::output::{json, pretty}, + project::{Project, cargo_project, standalone_project, std_project}, + session::KaniSession, + version::print_kani_version, +}; +use anyhow::Result; +use kani_metadata::{ContractedFunction, HarnessKind, KaniMetadata}; + +/// Process the KaniMetadata output from kani-compiler and output the list subcommand results +fn process_metadata(metadata: Vec, format: Format) -> Result<()> { + // We use ordered maps and sets so that the output is in lexicographic order (and consistent across invocations). + + // Map each file to a vector of its harnesses. + let mut standard_harnesses: BTreeMap> = BTreeMap::new(); + let mut contract_harnesses: BTreeMap> = BTreeMap::new(); + + let mut contracted_functions: BTreeSet = BTreeSet::new(); + + let mut total_standard_harnesses = 0; + let mut total_contract_harnesses = 0; + + for kani_meta in metadata { + for harness_meta in kani_meta.proof_harnesses { + match harness_meta.attributes.kind { + HarnessKind::Proof => { + total_standard_harnesses += 1; + if let Some(harnesses) = standard_harnesses.get_mut(&harness_meta.original_file) + { + harnesses.insert(harness_meta.pretty_name); + } else { + standard_harnesses.insert( + harness_meta.original_file, + BTreeSet::from([harness_meta.pretty_name]), + ); + } + } + HarnessKind::ProofForContract { .. } => { + total_contract_harnesses += 1; + if let Some(harnesses) = contract_harnesses.get_mut(&harness_meta.original_file) + { + harnesses.insert(harness_meta.pretty_name); + } else { + contract_harnesses.insert( + harness_meta.original_file, + BTreeSet::from([harness_meta.pretty_name]), + ); + } + } + HarnessKind::Test => {} + } + } + + contracted_functions.extend(kani_meta.contracted_functions.into_iter()); + } + + let totals = Totals { + standard_harnesses: total_standard_harnesses, + contract_harnesses: total_contract_harnesses, + contracted_functions: contracted_functions.len(), + }; + + match format { + Format::Pretty => pretty(standard_harnesses, contracted_functions, totals), + Format::Json => json(standard_harnesses, contract_harnesses, contracted_functions, totals), + } +} + +pub fn list_cargo(args: CargoListArgs) -> Result<()> { + let session = KaniSession::new(args.verify_opts)?; + if !session.args.common_args.quiet { + print_kani_version(InvocationType::CargoKani(vec![])); + } + + let project = cargo_project(&session, false)?; + process_metadata(project.metadata, args.format) +} + +pub fn list_standalone(args: StandaloneListArgs) -> Result<()> { + let session = KaniSession::new(args.verify_opts)?; + if !session.args.common_args.quiet { + print_kani_version(InvocationType::Standalone); + } + + let project: Project = if args.std { + std_project(&args.input, &session)? + } else { + standalone_project(&args.input, args.crate_name, &session)? + }; + + process_metadata(project.metadata, args.format) +} diff --git a/kani-driver/src/list/mod.rs b/kani-driver/src/list/mod.rs new file mode 100644 index 000000000000..0987a0e9c927 --- /dev/null +++ b/kani-driver/src/list/mod.rs @@ -0,0 +1,14 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// Implements the list subcommand logic + +pub mod collect_metadata; +mod output; + +/// Stores the total count of standard harnesses, contract harnesses, +/// and functions under contract across all `KaniMetadata` objects. +struct Totals { + standard_harnesses: usize, + contract_harnesses: usize, + contracted_functions: usize, +} diff --git a/kani-driver/src/list/output.rs b/kani-driver/src/list/output.rs new file mode 100644 index 000000000000..79a5fcf6fe5e --- /dev/null +++ b/kani-driver/src/list/output.rs @@ -0,0 +1,180 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! This module handles outputting the result for the list subcommand + +use std::{ + cmp::max, + collections::{BTreeMap, BTreeSet}, + fs::File, + io::BufWriter, +}; + +use crate::{list::Totals, version::KANI_VERSION}; +use anyhow::Result; +use colour::print_ln_bold; +use kani_metadata::ContractedFunction; +use serde_json::json; + +// Represents the version of our JSON file format. +// Increment this version (according to semantic versioning rules) whenever the JSON output format changes. +const FILE_VERSION: &str = "0.1"; +const JSON_FILENAME: &str = "kani-list.json"; + +/// Construct the table of contracts information. +fn construct_contracts_table( + contracted_functions: BTreeSet, + totals: Totals, +) -> Vec { + const NO_HARNESSES_MSG: &str = "NONE"; + + // Since the harnesses will be separated by newlines, the column length is equal to the length of the longest harness + fn column_len(harnesses: &[String]) -> usize { + harnesses.iter().map(|s| s.len()).max().unwrap_or(NO_HARNESSES_MSG.len()) + } + + // Contracts table headers + const FUNCTION_HEADER: &str = "Function"; + const CONTRACT_HARNESSES_HEADER: &str = "Contract Harnesses (#[kani::proof_for_contract])"; + + // Contracts table totals row + const TOTALS_HEADER: &str = "Total"; + let functions_total = totals.contracted_functions.to_string(); + let harnesses_total = totals.contract_harnesses.to_string(); + + let mut table_rows: Vec = vec![]; + let mut max_function_fmt_width = max(FUNCTION_HEADER.len(), functions_total.len()); + let mut max_contract_harnesses_fmt_width = + max(CONTRACT_HARNESSES_HEADER.len(), harnesses_total.len()); + + let mut data_rows: Vec<(String, Vec)> = vec![]; + + for cf in contracted_functions { + max_function_fmt_width = max(max_function_fmt_width, cf.function.len()); + max_contract_harnesses_fmt_width = + max(max_contract_harnesses_fmt_width, column_len(&cf.harnesses)); + + data_rows.push((cf.function, cf.harnesses)); + } + + let function_sep = "-".repeat(max_function_fmt_width); + let contract_harnesses_sep = "-".repeat(max_contract_harnesses_fmt_width); + let totals_sep = "-".repeat(TOTALS_HEADER.len()); + + let sep_row = format!("| {totals_sep} | {function_sep} | {contract_harnesses_sep} |"); + table_rows.push(sep_row.clone()); + + let function_space = " ".repeat(max_function_fmt_width - FUNCTION_HEADER.len()); + let contract_harnesses_space = + " ".repeat(max_contract_harnesses_fmt_width - CONTRACT_HARNESSES_HEADER.len()); + let totals_space = " ".repeat(TOTALS_HEADER.len()); + + let header_row = format!( + "| {totals_space} | {FUNCTION_HEADER}{function_space} | {CONTRACT_HARNESSES_HEADER}{contract_harnesses_space} |" + ); + table_rows.push(header_row); + table_rows.push(sep_row.clone()); + + for (function, harnesses) in data_rows { + let function_space = " ".repeat(max_function_fmt_width - function.len()); + let first_harness = harnesses.first().map_or(NO_HARNESSES_MSG, |v| v); + let contract_harnesses_space = + " ".repeat(max_contract_harnesses_fmt_width - first_harness.len()); + + let first_row = format!( + "| {totals_space} | {function}{function_space} | {first_harness}{contract_harnesses_space} |" + ); + table_rows.push(first_row); + + for subsequent_harness in harnesses.iter().skip(1) { + let function_space = " ".repeat(max_function_fmt_width); + let contract_harnesses_space = + " ".repeat(max_contract_harnesses_fmt_width - subsequent_harness.len()); + let row = format!( + "| {totals_space} | {function_space} | {subsequent_harness}{contract_harnesses_space} |" + ); + table_rows.push(row); + } + + table_rows.push(sep_row.clone()) + } + + let total_function_space = " ".repeat(max_function_fmt_width - functions_total.len()); + let total_harnesses_space = + " ".repeat(max_contract_harnesses_fmt_width - harnesses_total.len()); + + let totals_row = format!( + "| {TOTALS_HEADER} | {functions_total}{total_function_space} | {harnesses_total}{total_harnesses_space} |" + ); + + table_rows.push(totals_row); + table_rows.push(sep_row.clone()); + + table_rows +} + +/// Output results as a table printed to the terminal. +pub fn pretty( + standard_harnesses: BTreeMap>, + contracted_functions: BTreeSet, + totals: Totals, +) -> Result<()> { + const CONTRACTS_SECTION: &str = "Contracts:"; + const HARNESSES_SECTION: &str = "Standard Harnesses (#[kani::proof]):"; + const NO_CONTRACTS_MSG: &str = "No contracts or contract harnesses found."; + const NO_HARNESSES_MSG: &str = "No standard harnesses found."; + + print_ln_bold!("\n{CONTRACTS_SECTION}"); + + if contracted_functions.is_empty() { + println!("{NO_CONTRACTS_MSG}"); + } else { + let table_rows = construct_contracts_table(contracted_functions, totals); + println!("{}", table_rows.join("\n")); + }; + + print_ln_bold!("\n{HARNESSES_SECTION}"); + if standard_harnesses.is_empty() { + println!("{NO_HARNESSES_MSG}"); + } + + let mut std_harness_index = 0; + + for (_, harnesses) in standard_harnesses { + for harness in harnesses { + println!("{}. {harness}", std_harness_index + 1); + std_harness_index += 1; + } + } + + println!(); + + Ok(()) +} + +/// Output results as a JSON file. +pub fn json( + standard_harnesses: BTreeMap>, + contract_harnesses: BTreeMap>, + contracted_functions: BTreeSet, + totals: Totals, +) -> Result<()> { + let out_file = File::create(JSON_FILENAME).unwrap(); + let writer = BufWriter::new(out_file); + + let json_obj = json!({ + "kani-version": KANI_VERSION, + "file-version": FILE_VERSION, + "standard-harnesses": &standard_harnesses, + "contract-harnesses": &contract_harnesses, + "contracts": &contracted_functions, + "totals": { + "standard-harnesses": totals.standard_harnesses, + "contract-harnesses": totals.contract_harnesses, + "functions-under-contract": totals.contracted_functions, + } + }); + + serde_json::to_writer_pretty(writer, &json_obj)?; + + Ok(()) +} diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index e8ede555f180..88f92b3a70f6 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -12,6 +12,7 @@ use args_toml::join_args; use crate::args::StandaloneSubcommand; use crate::concrete_playback::playback::{playback_cargo, playback_standalone}; +use crate::list::collect_metadata::{list_cargo, list_standalone}; use crate::project::Project; use crate::session::KaniSession; use crate::version::print_kani_version; @@ -33,6 +34,7 @@ mod cbmc_property_renderer; mod concrete_playback; mod coverage; mod harness_runner; +mod list; mod metadata; mod project; mod session; @@ -67,6 +69,10 @@ fn cargokani_main(input_args: Vec) -> Result<()> { let args = args::CargoKaniArgs::parse_from(&input_args); check_is_valid(&args); + if let Some(CargoKaniSubcommand::List(args)) = args.command { + return list_cargo(*args); + } + let session = session::KaniSession::new(args.verify_opts)?; if !session.args.common_args.quiet { @@ -80,6 +86,7 @@ fn cargokani_main(input_args: Vec) -> Result<()> { Some(CargoKaniSubcommand::Playback(args)) => { return playback_cargo(*args); } + Some(CargoKaniSubcommand::List(_)) => unreachable!(), None => {} } @@ -98,6 +105,7 @@ fn standalone_main() -> Result<()> { let (session, project) = match args.command { Some(StandaloneSubcommand::Playback(args)) => return playback_standalone(*args), + Some(StandaloneSubcommand::List(args)) => return list_standalone(*args), Some(StandaloneSubcommand::VerifyStd(args)) => { let session = KaniSession::new(args.verify_opts)?; if !session.args.common_args.quiet { diff --git a/kani-driver/src/metadata.rs b/kani-driver/src/metadata.rs index 625d8b4bbcaa..174ce55187a6 100644 --- a/kani-driver/src/metadata.rs +++ b/kani-driver/src/metadata.rs @@ -96,6 +96,7 @@ pub fn merge_kani_metadata(files: Vec) -> KaniMetadata { proof_harnesses: vec![], unsupported_features: vec![], test_harnesses: vec![], + contracted_functions: vec![], }; for md in files { // Note that we're taking ownership of the original vec, and so we can move the data into the new data structure. @@ -104,6 +105,7 @@ pub fn merge_kani_metadata(files: Vec) -> KaniMetadata { // https://github.com/model-checking/kani/issues/1758 result.unsupported_features.extend(md.unsupported_features); result.test_harnesses.extend(md.test_harnesses); + result.contracted_functions.extend(md.contracted_functions); } result } diff --git a/kani-driver/src/version.rs b/kani-driver/src/version.rs index 95d98b0d6d3e..e1b995c3cd53 100644 --- a/kani-driver/src/version.rs +++ b/kani-driver/src/version.rs @@ -7,7 +7,7 @@ const KANI_RUST_VERIFIER: &str = "Kani Rust Verifier"; /// We assume this is the same as the `kani-verifier` version, but we should /// make sure it's enforced through CI: /// -const KANI_VERSION: &str = env!("CARGO_PKG_VERSION"); +pub(crate) const KANI_VERSION: &str = env!("CARGO_PKG_VERSION"); /// Print Kani version. At present, this is only release version information. pub(crate) fn print_kani_version(invocation_type: InvocationType) { diff --git a/kani_metadata/src/lib.rs b/kani_metadata/src/lib.rs index fa5a8828b6be..96caf92133e9 100644 --- a/kani_metadata/src/lib.rs +++ b/kani_metadata/src/lib.rs @@ -3,9 +3,8 @@ extern crate clap; -use std::{collections::HashSet, path::PathBuf}; - use serde::{Deserialize, Serialize}; +use std::{collections::HashSet, path::PathBuf}; pub use artifact::ArtifactType; pub use cbmc_solver::CbmcSolver; @@ -32,6 +31,18 @@ pub struct KaniMetadata { pub unsupported_features: Vec, /// If crates are built in test-mode, then test harnesses will be recorded here. pub test_harnesses: Vec, + /// The functions with contracts in this crate + pub contracted_functions: Vec, +} + +#[derive(Debug, Clone, Serialize, Deserialize, Eq, PartialEq, PartialOrd, Ord)] +pub struct ContractedFunction { + /// The fully qualified name the user gave to the function (i.e. includes the module path). + pub function: String, + /// The (currently full-) path to the file this function was declared within. + pub file: String, + /// The pretty names of the proof harnesses (`#[kani::proof_for_contract]`) for this function + pub harnesses: Vec, } #[derive(Debug, Clone, Serialize, Deserialize)] diff --git a/kani_metadata/src/unstable.rs b/kani_metadata/src/unstable.rs index abab48304914..a602c33e0326 100644 --- a/kani_metadata/src/unstable.rs +++ b/kani_metadata/src/unstable.rs @@ -96,6 +96,8 @@ pub enum UnstableFeature { UninitChecks, /// Enable an unstable option or subcommand. UnstableOptions, + /// The list subcommand [RFC 13](https://model-checking.github.io/kani/rfc/rfcs/0013-list.html) + List, } impl UnstableFeature { diff --git a/rfc/src/rfcs/0013-list.md b/rfc/src/rfcs/0013-list.md index bdbf4681f430..0d2baee2b594 100644 --- a/rfc/src/rfcs/0013-list.md +++ b/rfc/src/rfcs/0013-list.md @@ -1,8 +1,8 @@ - **Feature Name:** List Subcommand - **Feature Request Issue:** [#2573](https://github.com/model-checking/kani/issues/2573), [#1612](https://github.com/model-checking/kani/issues/1612) - **RFC PR:** #3463 -- **Status:** Under Review -- **Version:** 1 +- **Status:** Unstable +- **Version:** 2 ------------------- @@ -20,53 +20,50 @@ This feature will not cause any regressions for exisiting users. ## User Experience -Users run a `list` subcommand, which prints metadata about the harnesses and contracts in each crate under verification. The subcommand will take the option `--message-format=[pretty|json]`, which changes the output format. The default is `pretty`, which prints to the terminal. The `json` option creates and writes to a JSON file instead. +Users run a `list` subcommand, which prints metadata about the harnesses and contracts in each crate under verification. The subcommand takes two options: +- `--message-format=[pretty|json]`: choose the output format. The default is `pretty`, which prints to the terminal. The `json` option creates and writes to a JSON file instead. +- `--std`: this option should be specified when listing the harnesses and contracts in the standard library. This option is only available for `kani list` (not `cargo kani list`), which mirrors the verification workflow for the standard library. -This subcommand will not fail. In the case that it does not find any harnesses or contracts, it will print a message informing the user of that fact. +This subcommand does not fail. In the case that it does not find any harnesses or contracts, it prints a message informing the user of that fact. ### Pretty Format -The default format, `pretty`, will print the harnesses and contracts in a project, along with the total counts of each. +The default format, `pretty`, prints a "Contracts" table and a "Standard Harnesses" list. +Each row of the "Contracts" table consists of a function under contract and its contract harnesses. +The results are printed in lexicographic order. For example: ``` Kani Rust Verifier 0.54.0 (standalone) -Standard Harnesses: -- example::verify::check_new -- example::verify::check_modify - -Contract Harnesses: -- example::verify::check_foo_u32 -- example::verify::check_foo_u64 -- example::verify::check_func -- example::verify::check_bar - Contracts: -|--------------------------|-----------------------------------------------| -| Function | Contract Harnesses | -|--------------------------|-----------------------------------------------| -| example::impl::func | example::verify::check_func | -|--------------------------|-----------------------------------------------| -| example::impl::bar | example::verify::check_bar | -|--------------------------|-----------------------------------------------| -| example::impl::foo | example::verify::check_foo_u32, | -| | example::verify::check_foo_u64 | -|--------------------------|-----------------------------------------------| -| example::prep::parse | NONE | -|--------------------------|-----------------------------------------------| - -Totals: -- Standard Harnesses: 2 -- Contract Harnesses: 4 -- Functions with Contracts: 4 -- Contracts: 10 +|-------|-------------------------|--------------------------------------------------| +| | Function | Contract Harnesses (#[kani::proof_for_contract]) | +|-------|-------------------------|--------------------------------------------------| +| | example::impl::bar | example::verify::check_bar | +|-------|-------------------------|--------------------------------------------------| +| | example::impl::baz | example::verify::check_baz | +|-------|-------------------------|--------------------------------------------------| +| | example::impl::foo | example::verify::check_foo_u32 | +| | | example::verify::check_foo_u64 | +|-------|-------------------------|--------------------------------------------------| +| | example::impl::func | example::verify::check_func | +|-------|-------------------------|--------------------------------------------------| +| | example::prep::parse | NONE | +|-------|-------------------------|--------------------------------------------------| +| Total | 5 | 5 | +|-------|-------------------------|--------------------------------------------------| + +Standard Harnesses (#[kani::proof]): +1. example::verify::check_modify +2. example::verify::check_new ``` -A "Standard Harness" is a `#[proof]` harness, while a "Contract Harness" is a `#[proof_for_contract]` harness. - -All sections will be present in the output, regardless of the result. If a list is empty, Kani will output a `NONE` string. +All sections will be present in the output, regardless of the result. +If there are no harnesses for a function under contract, Kani inserts `NONE` in the "Contract Harnesses" column. +If the "Contracts" section is empty, Kani prints a message that "No contracts or contract harnesses were found." +If the "Standard Harnesses" section is empty, Kani prints a message that "No standard harnesses were found." ### JSON Format @@ -96,6 +93,7 @@ For example: file: /Users/johnsmith/example/kani_contract_proofs.rs harnesses: [ example::verify::check_bar, + example::verify::check_baz, example::verify::check_foo_u32, example::verify::check_foo_u64, example::verify::check_func @@ -104,14 +102,14 @@ For example: ], contracts: [ { - function: example::impl::func + function: example::impl::bar file: /Users/johnsmith/example/impl.rs - harnesses: [example::verify::check_func] + harnesses: [example::verify::check_bar] }, { - function: example::impl::bar + function: example::impl::baz file: /Users/johnsmith/example/impl.rs - harnesses: [example::verify::check_bar] + harnesses: [example::verify::check_baz] }, { function: example::impl::foo @@ -121,6 +119,11 @@ For example: example::verify::check_foo_u64 ] }, + { + function: example::impl::func + file: /Users/johnsmith/example/impl.rs + harnesses: [example::verify::check_func] + }, { function: example::prep::parse file: /Users/johnsmith/example/prep.rs @@ -129,9 +132,8 @@ For example: ], totals: { standard-harnesses: 2, - contract-harnesses: 4, - functions-with-contracts: 4, - contracts: 10, + contract-harnesses: 5, + functions-with-contracts: 5, } } ``` @@ -141,9 +143,16 @@ If there is no result for a given field (e.g., there are no contracts), Kani wil ## Software Design -We will add a new subcommand to `kani-driver`. +### Driver/Metdata Changes -*We will update this section once the UX is finalized*. +We add a new `list` subcommand to `kani-driver`, which invokes the compiler to collect metadata, then post-processes that metadata and outputs the result. +We extend `KaniMetadata` to include a new field containing each function under contract and its contract harnesses. + +### Compiler Changes + +In `codegen_crate`, we update the generation of `KaniMetadata` to include the new contracts information. +We iterate through each local item in the crate. +Each time we find a function under contract or a contract harness, we include it in the metadata. ## Rationale and alternatives @@ -152,19 +161,22 @@ Users of Kani may have many questions about their project--not only where their 1. Where are the harnesses? 2. Where are the contracts? 3. Which contracts are verified, and by which harnesses? -4. How many harnesses and contracts are there? +4. How many harnesses and functions under contract are there? We believe these questions are the most important for our use cases of tracking verification progress for customers and the standard library. The UX is designed to answer these questions clearly and concisely. We could have a more verbose or granular output, e.g., printing the metadata on a per-crate or per-module level, or including stubs or other attributes. Such a design would have the benefit of providing more information, with the disadvantage of being more complex to implement and more information for the user to process. - If we do not implement this feature, users will have to obtain this metadata through manual searching, or by writing a script to do it themselves. This feature will improve our internal productivity by automating the process. +The Contracts table is close to Markdown, but not quite Markdown--it includes line separators between each row, when Markdown would only have a separator for the header. +We include the separator because without it, it can be difficult to tell from reading the terminal output which entries are in the same row. +The user can transform the table to Markdown by deleting these separators, and we can trivially add a Markdown option in the future if there is demand for it. + ## Open questions -1. Do we want to include more contracts information? We could print more granular information about contracts, e.g., the text of the contracts, the number of `requires`, `ensures`, or `modifies` contracts, or the locations of the contracts. +1. Do we want to include more contracts information? We could print more granular information about contracts, e.g., the text of the contracts or the number of contracts. 2. More generally, we could introduce additional options that collect information about other Kani attributes (e.g., stubs). The default would be to leave them out, but this way a user could get more verbose output if they so choose. -3. Do we want to add a filtering option? For instance, `--harnesses ` and `--contracts `, where `pattern` corresponds to a Rust-style path. For example, `kani list --harnesses "my_crate::my_module::*"` would include all harnesses with that path prefix, while `kani list --contracts "my_crate::my_module::*"` would include all functions under contract with that path prefix. +3. Do we want to add a filtering option? For instance, `--harnesses ` and `--contracts `, where `pattern` corresponds to a Rust-style path. For example, `kani list --harnesses "my_crate::my_module::*"` would include all harnesses with that path prefix, while `kani list --contracts "my_crate::my_module::*"` would include all functions under contract with that path prefix. (If we do this work, we could use it to improve our `--harness` [pattern handling for verification](https://github.com/model-checking/kani/blob/main/kani-driver/src/metadata.rs#L187-L189)). ## Out of scope / Future Improvements @@ -179,4 +191,4 @@ fn check() { See [this blog post](https://model-checking.github.io/kani-verifier-blog/2022/10/27/using-kani-with-the-bolero-property-testing-framework.html) for more information. -There's no easy way for us to know whether a harness comes from Bolero, since Bolero takes care of rewriting the test to use Kani syntax and invoking the Kani engine. By the time the harness gets to Kani, there's no way for us to tell it apart from a regular harness. Fixing this would require some changes to our Bolero integration. \ No newline at end of file +There's no easy way for us to know whether a harness comes from Bolero, since Bolero takes care of rewriting the test to use Kani syntax and invoking the Kani engine. By the time the harness gets to Kani, there's no way for us to tell it apart from a regular harness. Fixing this would require some changes to our Bolero integration. diff --git a/tests/script-based-pre/cargo_list/Cargo.toml b/tests/script-based-pre/cargo_list/Cargo.toml new file mode 100644 index 000000000000..2f213d2fccd7 --- /dev/null +++ b/tests/script-based-pre/cargo_list/Cargo.toml @@ -0,0 +1,10 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "cargo_list" +version = "0.1.0" +edition = "2021" + +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } diff --git a/tests/script-based-pre/cargo_list/config.yml b/tests/script-based-pre/cargo_list/config.yml new file mode 100644 index 000000000000..4eac6f79588c --- /dev/null +++ b/tests/script-based-pre/cargo_list/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: list.sh +expected: list.expected diff --git a/tests/script-based-pre/cargo_list/list.expected b/tests/script-based-pre/cargo_list/list.expected new file mode 100644 index 000000000000..fb168c5a3bd2 --- /dev/null +++ b/tests/script-based-pre/cargo_list/list.expected @@ -0,0 +1,52 @@ +{ + "kani-version": + "file-version": "0.1", + "standard-harnesses": { + "src/standard_harnesses.rs": [ + "standard_harnesses::example::verify::check_modify", + "standard_harnesses::example::verify::check_new" + ] + }, + "contract-harnesses": { + "src/lib.rs": [ + "example::verify::check_bar", + "example::verify::check_foo_u32", + "example::verify::check_foo_u64", + "example::verify::check_func" + ] + }, + "contracts": [ + { + "function": "example::implementation::bar", + "file": "src/lib.rs", + "harnesses": [ + "example::verify::check_bar" + ] + }, + { + "function": "example::implementation::foo", + "file": "src/lib.rs", + "harnesses": [ + "example::verify::check_foo_u32", + "example::verify::check_foo_u64" + ] + }, + { + "function": "example::implementation::func", + "file": "src/lib.rs", + "harnesses": [ + "example::verify::check_func" + ] + }, + { + "function": "example::prep::parse", + "file": "src/lib.rs", + "harnesses": [] + } + ], + "totals": { + "standard-harnesses": 2, + "contract-harnesses": 4, + "functions-under-contract": 4 + } +} diff --git a/tests/script-based-pre/cargo_list/list.sh b/tests/script-based-pre/cargo_list/list.sh new file mode 100755 index 000000000000..6b1ab80b0f5f --- /dev/null +++ b/tests/script-based-pre/cargo_list/list.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +# Check that the JSON file produced by `cargo kani list` is correct. +# Note that the list.expected file omits the value for "kani-version" +# to avoid having to update the test every time we bump versions. + +cargo kani list -Z list -Z function-contracts --format json +cat "kani-list.json" diff --git a/tests/script-based-pre/cargo_list/src/lib.rs b/tests/script-based-pre/cargo_list/src/lib.rs new file mode 100644 index 000000000000..e7382a9124a3 --- /dev/null +++ b/tests/script-based-pre/cargo_list/src/lib.rs @@ -0,0 +1,68 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +//! This test replicates the module structure from the running example in the list RFC. +//! It ensures that the list command works across modules, and with modifies clauses, history expressions, and generic functions. + +mod standard_harnesses; + +#[cfg(kani)] +mod example { + mod prep { + #[kani::requires(s.len() < 10)] + fn parse(s: &str) -> u32 { + s.parse().unwrap() + } + } + + pub mod implementation { + #[kani::requires(*x < 4)] + #[kani::requires(*x > 2)] + #[kani::ensures(|_| old(*x - 1) == *x)] + #[kani::ensures(|_| *x == 4)] + #[kani::modifies(x)] + pub fn bar(x: &mut u32) { + *x += 1; + } + + #[kani::requires(*x < 100)] + #[kani::modifies(x)] + pub fn func(x: &mut i32) { + *x *= 1; + } + + #[kani::requires(true)] + #[kani::ensures(|_| old(*x) == *x)] + pub fn foo(x: &mut T) -> T { + *x + } + } + + mod verify { + use crate::example::implementation; + + #[kani::proof_for_contract(implementation::bar)] + fn check_bar() { + let mut x = 7; + implementation::bar(&mut x); + } + + #[kani::proof_for_contract(implementation::foo)] + fn check_foo_u32() { + let mut x: u32 = 7; + implementation::foo(&mut x); + } + + #[kani::proof_for_contract(implementation::foo)] + fn check_foo_u64() { + let mut x: u64 = 7; + implementation::foo(&mut x); + } + + #[kani::proof_for_contract(implementation::func)] + fn check_func() { + let mut x = 7; + implementation::func(&mut x); + } + } +} diff --git a/tests/script-based-pre/cargo_list/src/standard_harnesses.rs b/tests/script-based-pre/cargo_list/src/standard_harnesses.rs new file mode 100644 index 000000000000..5df490461d0c --- /dev/null +++ b/tests/script-based-pre/cargo_list/src/standard_harnesses.rs @@ -0,0 +1,15 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +//! Test that the cargo list command can find Kani attributes across multiple files. + +#[cfg(kani)] +mod example { + mod verify { + #[kani::proof] + fn check_modify() {} + + #[kani::proof] + fn check_new() {} + } +} diff --git a/tests/script-based-pre/kani_list/config.yml b/tests/script-based-pre/kani_list/config.yml new file mode 100644 index 000000000000..4eac6f79588c --- /dev/null +++ b/tests/script-based-pre/kani_list/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: list.sh +expected: list.expected diff --git a/tests/script-based-pre/kani_list/list.expected b/tests/script-based-pre/kani_list/list.expected new file mode 100644 index 000000000000..e2ed4506eb4e --- /dev/null +++ b/tests/script-based-pre/kani_list/list.expected @@ -0,0 +1,52 @@ +{ + "kani-version": + "file-version": "0.1", + "standard-harnesses": { + "src/lib.rs": [ + "example::verify::check_modify", + "example::verify::check_new" + ] + }, + "contract-harnesses": { + "src/lib.rs": [ + "example::verify::check_bar", + "example::verify::check_foo_u32", + "example::verify::check_foo_u64", + "example::verify::check_func" + ] + }, + "contracts": [ + { + "function": "example::implementation::bar", + "file": "src/lib.rs", + "harnesses": [ + "example::verify::check_bar" + ] + }, + { + "function": "example::implementation::foo", + "file": "src/lib.rs", + "harnesses": [ + "example::verify::check_foo_u32", + "example::verify::check_foo_u64" + ] + }, + { + "function": "example::implementation::func", + "file": "src/lib.rs", + "harnesses": [ + "example::verify::check_func" + ] + }, + { + "function": "example::prep::parse", + "file": "src/lib.rs", + "harnesses": [] + } + ], + "totals": { + "standard-harnesses": 2, + "contract-harnesses": 4, + "functions-under-contract": 4 + } +} diff --git a/tests/script-based-pre/kani_list/list.sh b/tests/script-based-pre/kani_list/list.sh new file mode 100755 index 000000000000..e7bb6f081044 --- /dev/null +++ b/tests/script-based-pre/kani_list/list.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +# Check that the JSON file produced by `kani list` is correct. +# Note that the list.expected file omits the value for "kani-version" +# to avoid having to update the test every time we bump versions. + +kani list -Z list -Z function-contracts src/lib.rs --format json +cat "kani-list.json" diff --git a/tests/script-based-pre/kani_list/src/lib.rs b/tests/script-based-pre/kani_list/src/lib.rs new file mode 100644 index 000000000000..69dbba5a9e0f --- /dev/null +++ b/tests/script-based-pre/kani_list/src/lib.rs @@ -0,0 +1,71 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +//! This test replicates the module structure from the running example in the list RFC. +//! It ensures that the list command across modules, and with modifies clauses, history expressions, and generic functions. + +mod example { + mod prep { + #[kani::requires(s.len() < 10)] + fn parse(s: &str) -> u32 { + s.parse().unwrap() + } + } + + pub mod implementation { + #[kani::requires(*x < 4)] + #[kani::requires(*x > 2)] + #[kani::ensures(|_| old(*x - 1) == *x)] + #[kani::ensures(|_| *x == 4)] + #[kani::modifies(x)] + pub fn bar(x: &mut u32) { + *x += 1; + } + + #[kani::requires(true)] + #[kani::ensures(|_| old(*x) == *x)] + pub fn foo(x: &mut T) -> T { + *x + } + + #[kani::requires(*x < 100)] + #[kani::modifies(x)] + pub fn func(x: &mut i32) { + *x *= 1; + } + } + + mod verify { + use crate::example::implementation; + + #[kani::proof_for_contract(implementation::bar)] + fn check_bar() { + let mut x = 7; + implementation::bar(&mut x); + } + + #[kani::proof_for_contract(implementation::foo)] + fn check_foo_u32() { + let mut x: u32 = 7; + implementation::foo(&mut x); + } + + #[kani::proof_for_contract(implementation::foo)] + fn check_foo_u64() { + let mut x: u64 = 7; + implementation::foo(&mut x); + } + + #[kani::proof_for_contract(implementation::func)] + fn check_func() { + let mut x = 7; + implementation::func(&mut x); + } + + #[kani::proof] + fn check_modify() {} + + #[kani::proof] + fn check_new() {} + } +}