diff --git a/Cargo.toml b/Cargo.toml index 11b3337cd77a..cfa94e5ce44e 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -67,7 +67,6 @@ exclude = [ "tests/cargo-ui", "tests/slow", "tests/std-checks", - "tests/assess-scan-test-scaffold", "tests/script-based-pre", "tests/script-based-pre/build-cache-bin/target/new_dep", "tests/script-based-pre/build-cache-dirty/target/new_dep", diff --git a/docs/src/SUMMARY.md b/docs/src/SUMMARY.md index 9d7553a668d7..7c37e0445314 100644 --- a/docs/src/SUMMARY.md +++ b/docs/src/SUMMARY.md @@ -36,10 +36,8 @@ - [Working with `rustc`](./rustc-hacks.md) - [Migrating to StableMIR](./stable-mir.md) - [Command cheat sheets](./cheat-sheets.md) - - [cargo kani assess](./dev-assess.md) - [Testing](./testing.md) - [Regression testing](./regression-testing.md) - - [(Experimental) Testing with a Large Number of Repositories](./repo-crawl.md) - [Performance comparisons](./performance-comparisons.md) - [`benchcomp` command line](./benchcomp-cli.md) - [`benchcomp` configuration file](./benchcomp-conf.md) diff --git a/docs/src/dev-assess.md b/docs/src/dev-assess.md deleted file mode 100644 index 8f79351d3a9c..000000000000 --- a/docs/src/dev-assess.md +++ /dev/null @@ -1,185 +0,0 @@ -# `cargo kani assess` - -Assess is an experimental new feature to gather data about Rust crates, to aid the start of proof writing. - -In the short-term, assess collects and dumps tables of data that may help _Kani developers_ understand what's needed to begin writing proofs for another project. -For instance, assess may help answer questions like: - -1. Does Kani successfully build all of the crates involved in this project? If not, why not? -2. Does Kani support all the Rust language features necessary to do verification with this project? If not, which are most important? - -In the long-term, assess will become a user-facing feature, and help _Kani users_ get started writing proofs. -We expect that users will have the same questions as above, but in the long term, hopefully the answers to those trend towards an uninteresting "yes." -So the new questions might be: - -3. Is this project ready for verification? Projects need to be reasonably well-tested first. -Our operating hypothesis is that code currently covered by unit tests is the code that could become covered by proofs. -4. How much of given project (consisting of multiple packages or workspaces) or which of the user's projects might be verifiable? -If a user wants to start trying Kani, but they have the choice of several different packages where they might try, we can help find the package with the lowest hanging fruit. -5. Given a package, where in that package's code should the user look, in order to write the first (or next) proof? - -These long-term goals are only "hinted at" with the present experimental version of assess. -Currently, we only get as far as finding out which tests successfully verify (concretely) with Kani. -This might indicate tests that could be generalized and converted into proofs, but we currently don't do anything to group, rank, or otherwise heuristically prioritize what might be most "interesting." -(For instance, we'd like to eventually compute coverage information and use that to help rank the results.) -As a consequence, the output of the tool is very hard to interpret, and likely not (yet!) helpful to new or potential Kani users. - -## Using Assess - -To assess a package, run: - -```text -cargo kani --enable-unstable assess -``` - -As a temporary hack (arguments shouldn't work like this), to assess a single cargo workspace, run: - -```text -cargo kani --enable-unstable --workspace assess -``` - -To scan a collection of workspaces or packages that are not part of a shared workspace, run: - -```text -cargo kani --enable-unstable assess scan -``` - -The only difference between 'scan' and 'regular' assess is how the packages built are located. -All versions of assess produce the same output and metrics. -Assess will normally build just like `cargo kani` or `cargo build`, whereas `scan` will find all cargo packages beneath the current directory, even in unrelated workspaces. -Thus, 'scan' may be helpful in the case where the user has a choice of packages and is looking for the easiest to get started with (in addition to the Kani developer use-case, of aggregating statistics across many packages). - -(Tip: Assess may need to run for awhile, so try using `screen`, `tmux` or `nohup` to avoid terminating the process if, for example, an ssh connection breaks. -Some tests can also consume huge amounts of ram when run through Kani, so you may wish to use `ulimit -v 6000000` to prevent any processes from using more than 6GB. -You can also limit the number of concurrent tests that will be run by providing e.g. `-j 4`, currently as a prepended argument, like `--enable-unstable` or `--workspace` in the examples above.) - -## What assess does - -Assess builds all the packages requested in "test mode" (i.e. `--tests`), and runs all the same tests that `cargo test` would, except through Kani. -This gives end-to-end assurance we're able to actually build and run code from these packages, skipping nothing of what the verification process would need, except that the harnesses don't have any nondeterminism (`kani::any()`) and consequently don't "prove" much. -The interesting signal comes from what tests cannot be analyzed by Kani due to unsupported features, performance problems, crash bugs, or other issues that get in the way. - -Currently, assess forces termination by using `unwind(1)` on all tests, so many tests will fail with unwinding assertions. - -## Current Assess Results - -Assess produces a few tables of output (both visually in the terminal, and in a more detailed json format) so far: - -### Unsupported features - -```text -====================================================== - Unsupported feature | Crates | Instances - | impacted | of use --------------------------------+----------+----------- - caller_location | 71 | 239 - simd_bitmask | 39 | 160 -... -``` - -The unsupported features table aggregates information about features that Kani does not yet support. -These correspond to uses of `codegen_unimplemented` in the `kani-compiler`, and appear as warnings during compilation. - -Unimplemented features are not necessarily actually hit by (dynamically) reachable code, so an immediate future improvement on this table would be to count the features *actually hit* by failing test cases, instead of just those features reported as existing in code by the compiler. -In other words, the current unsupported features table is **not** what we want to see, in order to _perfectly_ prioritize implementing these features, because we may be counting features that no proof would ever hit. -A perfect signal here isn't possible: there may be code that looks statically reachable, but is never dynamically reachable, and we can't tell. -But we can use test coverage as an approximation: well-tested code will hopefully cover most of the dynamically reachable code. -The operating hypothesis of assess is that code covered by tests is code that could be covered by proof, and so measuring unsupported features by those actually hit by a test should provide a better "signal" about priorities. -Implicitly deprioritizing unsupported features because they aren't covered by tests may not be a bug, but a feature: we may simply not want to prove anything about that code, if it hasn't been tested first, and so adding support for that feature may not be important. - -A few notes on terminology: - -1. "Crates impacted" here means "packages in the current workspace (or scan) where the building of that package (and all of its dependencies) ultimately resulted in this warning." -For example, if only assessing a single package (not a workspace) this could only be `1` in this column, regardless of the number of dependencies. -2. "Instances of use" likewise means "total instances found while compiling this package's tests and all the (reachable) code in its dependencies." -3. These counts are influenced by (static) reachability: if code is not potentially reachable from a test somehow, it will not be built and will not be counted. - -### Test failure reasons - -```text -================================================ - Reason for failure | Number of tests -------------------------------+----------------- - unwind | 61 - none (success) | 6 - assertion + overflow | 2 -... -``` - -The test failure reasons table indicates why, when assess ran a test through Kani, it failed to verify. -Notably: - -1. Because we force termination with `unwind(1)`, we expect `unwind` to rank highly. -2. We do report number of tests succeeding on this table, to aid understanding how well things went overall. -3. The reported reason is the "property class" of the CBMC property that failed. So `assertion` means an ordinary `assert!()` was hit (or something else with this property class). -4. When multiple properties fail, they are aggregated with `+`, such as `assertion + overflow`. -5. Currently this table does not properly account for `should_fail` tests, so `assertion` may actually be "success": the test should hit an assertion and did. - -### Promising test cases - -```text -============================================================================= - Candidate for proof harness | Location --------------------------------------------------------+--------------------- - float::tests::f64_edge_cases | src/float.rs:226 - float::tests::f32_edge_cases | src/float.rs:184 - integer::tests::test_integers | src/integer.rs:171 -``` - -This table is the most rudimentary so far, but is the core of what long-term assess will help accomplish. -Currently, this table just presents (with paths displayed in a clickable manner) the tests that successfully "verify" with Kani. -These might be good candidates for turning into proof harnesses. -This list is presently unordered; the next step for improving it would be to find even a rudimentary way of ranking these test cases (e.g. perhaps by code coverage). - -## How Assess Works - -`kani-compiler` emits `*.kani-metadata.json` for each target it builds. -This format can be found in the `kani_metadata` crate, shared by `kani-compiler` and `kani-driver`. -This is the starting point for assess. - -Assess obtains this metadata by essentially running a `cargo kani`: - -1. With `--all-features` turned on -2. With `unwind` always set to `1` -3. In test mode, i.e. `--tests` -4. With test-case reachability mode. Normally Kani looks for proof harnesses and builds only those. Here we switch to building only the test harnesses instead. - -Assess starts by getting all the information from these metadata files. -This is enough by itself to construct a rudimentary "unsupported features" table. -But assess also uses it to discover all the test cases, and (instead of running proof harnesses) it then runs all these test harnesses under Kani. - -Assess produces a second metadata format, called (unsurprisingly) "assess metadata". -(Found in `kani-driver` under [`src/assess/metadata.rs`](https://github.com/model-checking/kani/blob/main/kani-driver/src/assess/metadata.rs).) -This format records the results of what assess does. - -This metadata can be written to a json file by providing `--emit-metadata ` to `assess`. -Likewise, `scan` can be told to write out this data with the same option. - -Assess metadata is an aggregatable format. -It does not apply to just one package, as assess can work on a workspace of packages. -Likewise, `scan` uses and produces the exact same format, across multiple workspaces. - -So far all assess metadata comes in the form of "tables" which are built with `TableBuilder`. -This is documented further in [`src/assess/table_builder.rs`](https://github.com/model-checking/kani/blob/main/kani-driver/src/assess/table_builder.rs). - -## Using Assess on the top-100 crates - -There is a script in the Kani repo for this purpose. - -This will clone the top-100 crates to `/tmp/top-100-experiment` and run assess scan on them: - -```text -./scripts/exps/assess-scan-on-repos.sh -``` - -If you'd like to preseve the results, you can direct scan to use a different directory with an environment variable: - -```text -ASSESS_SCAN="~/top-100-experiment" ./scripts/exps/assess-scan-on-repos.sh -``` - -To re-run the experiment, it suffices to be in the experiment directory: - -```text -cd ~/top-100-experiment && ~/kani/scripts/exps/assess-scan-on-repos.sh -``` diff --git a/docs/src/repo-crawl.md b/docs/src/repo-crawl.md deleted file mode 100644 index e0407939f6dc..000000000000 --- a/docs/src/repo-crawl.md +++ /dev/null @@ -1,93 +0,0 @@ -# (Experimental) Testing with a Large Number of Repositories - -This section explains how to run Kani on a large number of crates -downloaded from git forges. You may want to do this if you are going -to test Kani's ability to handle Rust features found in projects out -in the wild. - -For the first half, we will explain how to use data from crates.io to -pick targets. Second half will explain how to use a script to run on a -list of selected repositories. - -## Picking Repositories - -In picking repositories, you may want to select by metrics like -popularity or by the presence of certain features. In this section, we -will explain how to select top ripostes by download count. - -We will use the `db-dump` method of getting data from crates.io as it -is zero cost to their website and gives us SQL access. To start, have -the following programs set up on your computer. -- docker -- docker-compose. - -1. Start PostgreSQL. Paste in the following yaml file as -`docker-compose.yaml`. `version: '3.3'` may need to change. -```yaml -version: '3.3' -services: - db: - image: postgres:latest - restart: always - environment: - - POSTGRES_USER=postgres - - POSTGRES_PASSWORD=postgres - volumes: - - crates-data:/var/lib/postgresql/data - logging: - driver: "json-file" - options: - max-size: "50m" -volumes: - crates-data: - driver: local -``` -Then, run the following to start the setup. -```bash -docker-compose up -d -``` - -Once set up, run `docker ls` to figure out the container's name. We -will refer to the name as `$CONTAINER_NAME` from now on. - -2. Download actual data from crates.io. First, run the following - command to get a shell in the container: `docker exec -it --user - postgres $CONTAINER_NAME bash`. Now, run the following to grab and - install the data into the repository. Please note that this may - take a while. - - ```bash - wget https://static.crates.io/db-dump.tar.gz - tar -xf db-dump.tar.gz - psql postgres -f */schema.sql - psql postgres -f */import.sql - ``` - -3. Extract the data. In the same docker shell, run the following to - extract the top 1k repositories. Other SQL queries may be used if - you want another criteria - - ```sql - \copy - (SELECT name, repository, downloads FROM crates - WHERE repository LIKE 'http%' ORDER BY DOWNLOADS DESC LIMIT 1000) - to 'top-1k.csv' csv header; - ``` - -4. Clean the data. The above query will capture duplicates paths that - are deeper than the repository. You can clean these out. - - URL from CSV: `cat top-1k.csv | awk -F ',' '{ print $2 }' | grep -v 'http.*'` - - Remove long paths: `sed 's/tree\/master.*$//g'` - - Once processed, you can dedup with `sort | uniq --unique` - -## Running the List of Repositories -In this step we will download the list of repositories using a script -[assess-scan-on-repos.sh](../../scripts/exps/assess-scan-on-repos.sh) - -Make sure to have Kani ready to run. For that, see the [build instructions](cheat-sheets.md#build). - -From the repository root, you can run the script with -`./scripts/exps/assess-scan-on-repos.sh $URL_LIST_FILE` where -`$URL_LIST_FILE` points to a line-delimited list of URLs you want to -run Kani on. Repositories that give warnings or errors can be grepping -for with "STDERR Warnings" and "Error exit in" respectively. diff --git a/docs/src/testing.md b/docs/src/testing.md index 85e1a46838bf..cefe243ea4ca 100644 --- a/docs/src/testing.md +++ b/docs/src/testing.md @@ -15,5 +15,4 @@ two very good reasons to do it: We recommend reading our section on [Regression Testing](./regression-testing.md) if you're interested in Kani -development. To run kani on a large number of remotely -hosted crates, please see [Repository Crawl](./repo-crawl.md). +development. diff --git a/kani-compiler/src/args.rs b/kani-compiler/src/args.rs index 34a913088037..287e478d7d3c 100644 --- a/kani-compiler/src/args.rs +++ b/kani-compiler/src/args.rs @@ -28,8 +28,6 @@ pub enum ReachabilityType { None, /// Start the cross-crate reachability analysis from all public functions in the local crate. PubFns, - /// Start the cross-crate reachability analysis from all *test* (i.e. `#[test]`) harnesses in the local crate. - Tests, /// Start the cross-crate reachability analysis from all functions in the local crate. /// Currently, this mode is only used for automatic harness generation. AllFns, diff --git a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs index f577d2886e6c..fb1666526cf1 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs @@ -253,7 +253,7 @@ impl CodegenBackend for LlbcCodegenBackend { units.store_modifies(&modifies_instances); units.write_metadata(&queries, tcx); } - ReachabilityType::Tests | ReachabilityType::AllFns => todo!(), + ReachabilityType::AllFns => todo!(), ReachabilityType::None => {} ReachabilityType::PubFns => { let unit = CodegenUnit::default(); diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index cf428c44dbb4..2561c51b2c68 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -6,14 +6,11 @@ use crate::args::ReachabilityType; use crate::codegen_cprover_gotoc::GotocCtx; use crate::kani_middle::analysis; -use crate::kani_middle::attributes::{KaniAttributes, is_test_harness_description}; +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::metadata::gen_test_metadata; use crate::kani_middle::provide; -use crate::kani_middle::reachability::{ - collect_reachable_items, filter_const_crate_items, filter_crate_items, -}; +use crate::kani_middle::reachability::{collect_reachable_items, filter_crate_items}; use crate::kani_middle::transform::{BodyTransformation, GlobalPasses}; use crate::kani_queries::QueryDb; use cbmc::RoundingMode; @@ -371,53 +368,6 @@ impl CodegenBackend for GotocCodegenBackend { units.store_loop_contracts(&loop_contracts_instances); units.write_metadata(&queries, tcx); } - ReachabilityType::Tests => { - // We're iterating over crate items here, so what we have to codegen is the "test description" containing the - // test closure that we want to execute - // TODO: Refactor this code so we can guarantee that the pair (test_fn, test_desc) actually match. - let unit = CodegenUnit::default(); - let mut transformer = BodyTransformation::new(&queries, tcx, &unit); - let mut descriptions = vec![]; - let harnesses = filter_const_crate_items(tcx, &mut transformer, |_, item| { - if is_test_harness_description(tcx, item.def) { - descriptions.push(item.def); - true - } else { - false - } - }); - // Codegen still takes a considerable amount, thus, we only generate one model for - // all harnesses and copy them for each harness. - // We will be able to remove this once we optimize all calls to CBMC utilities. - // https://github.com/model-checking/kani/issues/1971 - let model_path = base_filename.with_extension(ArtifactType::SymTabGoto); - let (gcx, items, contract_info) = self.codegen_items( - tcx, - &harnesses, - &model_path, - &results.machine_model, - Default::default(), - transformer, - ); - results.extend(gcx, items, None); - - assert!(contract_info.is_none()); - - for (test_fn, test_desc) in harnesses.iter().zip(descriptions.iter()) { - let instance = - if let MonoItem::Fn(instance) = test_fn { instance } else { continue }; - let metadata = gen_test_metadata(tcx, *test_desc, *instance, base_filename); - let test_model_path = &metadata.goto_file.as_ref().unwrap(); - std::fs::copy(&model_path, test_model_path).unwrap_or_else(|_| { - panic!( - "Failed to copy {} to {}", - model_path.display(), - test_model_path.display() - ) - }); - results.harnesses.push(metadata); - } - } ReachabilityType::None => {} ReachabilityType::PubFns => { let unit = CodegenUnit::default(); @@ -679,8 +629,8 @@ impl GotoCodegenResults { 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. + // removes any contracts logic for ReachabilityType::PubFns, + // which is the only ReachabilityType under which the compiler calls this function. contracted_functions: vec![], autoharness_md: None, } diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 4dfb8cd64bee..911e1682c143 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -6,7 +6,7 @@ use std::collections::{BTreeMap, HashSet}; use kani_metadata::{CbmcSolver, HarnessAttributes, HarnessKind, Stub}; use quote::ToTokens; -use rustc_ast::{LitKind, MetaItem, MetaItemKind, attr}; +use rustc_ast::{LitKind, MetaItem, MetaItemKind}; use rustc_errors::ErrorGuaranteed; use rustc_hir::{AttrArgs, Attribute, def::DefKind, def_id::DefId}; use rustc_middle::ty::{Instance, TyCtxt, TyKind}; @@ -708,21 +708,6 @@ pub fn is_proof_harness(tcx: TyCtxt, instance: InstanceStable) -> bool { }) } -/// Does this `def_id` have `#[rustc_test_marker]`? -pub fn is_test_harness_description(tcx: TyCtxt, item: impl CrateDef) -> bool { - let def_id = rustc_internal::internal(tcx, item.def_id()); - let attrs = tcx.get_attrs_unchecked(def_id); - attr::contains_name(attrs, rustc_span::symbol::sym::rustc_test_marker) -} - -/// Extract the test harness name from the `#[rustc_test_maker]` -pub fn test_harness_name(tcx: TyCtxt, def: &impl CrateDef) -> String { - let def_id = rustc_internal::internal(tcx, def.def_id()); - let attrs = tcx.get_attrs_unchecked(def_id); - let marker = attr::find_by_name(attrs, rustc_span::symbol::sym::rustc_test_marker).unwrap(); - parse_str_value(marker).unwrap() -} - /// Expect the contents of this attribute to be of the format #[attribute = /// "value"] and return the `"value"`. fn expect_key_string_value( @@ -1014,16 +999,6 @@ fn parse_key_values(attr: &Attribute) -> Result, String .collect() } -/// Extracts the string value argument from the attribute provided. -/// -/// For attributes with the following format, this will return a string that represents "VALUE". -/// - `#[attribute = "VALUE"]` -fn parse_str_value(attr: &Attribute) -> Option { - // Vector of meta items , that contain the arguments given the attribute - let value = attr.value_str(); - value.map(|sym| sym.to_string()) -} - /// If the attribute is named `kanitool::name`, this extracts `name` fn attr_kind(tcx: TyCtxt, attr: &Attribute) -> Option { if let Attribute::Unparsed(normal) = attr { diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs index 4a7a0aa07b94..f4f0a99517d4 100644 --- a/kani-compiler/src/kani_middle/metadata.rs +++ b/kani-compiler/src/kani_middle/metadata.rs @@ -6,7 +6,7 @@ use std::collections::HashMap; use std::path::Path; -use crate::kani_middle::attributes::{KaniAttributes, test_harness_name}; +use crate::kani_middle::attributes::KaniAttributes; use crate::kani_middle::codegen_units::Harness; use crate::kani_middle::{SourceLocation, stable_fn_def}; use kani_metadata::ContractedFunction; @@ -154,33 +154,3 @@ pub fn gen_automatic_proof_metadata( is_automatically_generated: true, } } - -/// Create the harness metadata for a test description. -#[allow(dead_code)] -pub fn gen_test_metadata( - tcx: TyCtxt, - test_desc: impl CrateDef, - test_fn: Instance, - base_name: &Path, -) -> HarnessMetadata { - let pretty_name = test_harness_name(tcx, &test_desc); - let mangled_name = test_fn.mangled_name(); - let loc = SourceLocation::new(test_desc.span()); - let file_stem = format!("{}_{mangled_name}", base_name.file_stem().unwrap().to_str().unwrap()); - let model_file = base_name.with_file_name(file_stem).with_extension(ArtifactType::SymTabGoto); - - HarnessMetadata { - pretty_name, - mangled_name, - crate_name: test_desc.krate().name, - original_file: loc.filename, - original_start_line: loc.start_line, - original_end_line: loc.end_line, - attributes: HarnessAttributes::new(HarnessKind::Test), - // TODO: This no longer needs to be an Option. - goto_file: Some(model_file), - contract: Default::default(), - has_loop_contracts: false, - is_automatically_generated: false, - } -} diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 5ccd611cbeab..f7d8768e0554 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -104,36 +104,6 @@ where .collect::>() } -/// Use a predicate to find `const` declarations, then extract all items reachable from them. -/// -/// Probably only specifically useful with a predicate to find `TestDescAndFn` const declarations from -/// tests and extract the closures from them. -pub fn filter_const_crate_items( - tcx: TyCtxt, - transformer: &mut BodyTransformation, - mut predicate: F, -) -> Vec -where - F: FnMut(TyCtxt, Instance) -> bool, -{ - let crate_items = stable_mir::all_local_items(); - let mut roots = Vec::new(); - // Filter regular items. - for item in crate_items { - // Only collect monomorphic items. - if let Ok(instance) = Instance::try_from(item) - && predicate(tcx, instance) - { - let body = transformer.body(tcx, instance); - let mut collector = - MonoItemsFnCollector { tcx, body: &body, collected: FxHashSet::default() }; - collector.visit_body(&body); - roots.extend(collector.collected.into_iter()); - } - } - roots.into_iter().map(|root| root.item).collect() -} - /// Reason for introducing an edge in the call graph. #[derive(Clone, Copy, Debug, Eq, PartialEq, Hash)] enum CollectionReason { diff --git a/kani-driver/src/args/assess_args.rs b/kani-driver/src/args/assess_args.rs deleted file mode 100644 index ccb69910229b..000000000000 --- a/kani-driver/src/args/assess_args.rs +++ /dev/null @@ -1,45 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -//! This module contains arguments specific to the `cargo kani assess` subcommand. - -use std::path::PathBuf; - -use clap::Parser; - -/// `cargo kani assess` subcommand arguments -#[derive(Default, Debug, Parser)] -pub struct AssessArgs { - #[command(subcommand)] - pub command: Option, - - /// Write Assess metadata (unstable file format) to the given file - #[arg(long, hide = true)] - pub emit_metadata: Option, -} - -/// `cargo kani assess` takes optional subcommands to request specialized behavior -#[derive(Debug, Parser)] -pub enum AssessSubcommand { - /// Run assess on a directory containing multiple cargo projects, and aggregate the results - Scan(ScanArgs), -} - -/// `cargo kani assess scan` subcommand arguments -#[derive(Debug, Parser)] -pub struct ScanArgs { - // TODO: When assess scan is invoked using `--existing-only`, it should check if the Kani version - // from the existing metadata files matches the current version. Otherwise, the results may no - // longer hold. - /// Don't run assess on found packages, just re-analyze the results from a previous run - #[arg(long, hide = true)] - pub existing_only: bool, - - /// Only consider the packages named in the given file - #[arg(long, hide = true)] - pub filter_packages_file: Option, - - /// Write Assess-Scan metadata (unstable file format) to the given file - #[arg(long, hide = true)] - pub emit_metadata: Option, -} diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 13a4175a6d99..ef413e228939 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -2,7 +2,6 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT //! Module that define Kani's command line interface. This includes all subcommands. -pub mod assess_args; pub mod autoharness_args; pub mod cargo; pub mod common; @@ -10,8 +9,6 @@ pub mod list_args; pub mod playback_args; pub mod std_args; -pub use assess_args::*; - use self::common::*; use crate::args::cargo::CargoTargetArgs; use crate::util::warning; @@ -198,9 +195,6 @@ pub struct CargoKaniArgs { /// cargo-kani takes optional subcommands to request specialized behavior #[derive(Debug, clap::Subcommand)] pub enum CargoKaniSubcommand { - #[command(hide = true)] - Assess(Box), - /// Create and run harnesses automatically for eligible functions. Implies -Z function-contracts and -Z loop-contracts. /// See https://model-checking.github.io/kani/reference/experimental/autoharness.html for documentation. Autoharness(Box), @@ -218,11 +212,6 @@ pub enum CargoKaniSubcommand { #[derive(Debug, clap::Args)] #[clap(next_help_heading = "Verification Options")] pub struct VerificationArgs { - /// Temporary option to trigger assess mode for out test suite - /// where we are able to add options but not subcommands - #[arg(long, hide = true)] - pub assess: bool, - /// Link external C files referenced by Rust code. /// This is an experimental feature and requires `-Z c-ffi` to be used #[arg(long, hide = true, num_args(1..))] @@ -624,8 +613,6 @@ where impl ValidateArgs for CargoKaniSubcommand { fn validate(&self) -> Result<(), Error> { match self { - // Assess doesn't implement validation yet. - CargoKaniSubcommand::Assess(_) => Ok(()), CargoKaniSubcommand::Autoharness(autoharness) => autoharness.validate(), CargoKaniSubcommand::Playback(playback) => playback.validate(), CargoKaniSubcommand::List(list) => list.validate(), @@ -637,14 +624,7 @@ impl ValidateArgs for CargoKaniArgs { fn validate(&self) -> Result<(), Error> { self.verify_opts.validate()?; self.command.validate()?; - - // --assess requires -Z unstable-options, but the subcommand needs manual checking - self.verify_opts.common_args.check_unstable( - (matches!(self.command, Some(CargoKaniSubcommand::Assess(_))) - || self.verify_opts.assess), - "assess", - UnstableFeature::UnstableOptions, - ) + Ok(()) } } diff --git a/kani-driver/src/assess/metadata.rs b/kani-driver/src/assess/metadata.rs deleted file mode 100644 index 14018541d0e5..000000000000 --- a/kani-driver/src/assess/metadata.rs +++ /dev/null @@ -1,123 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -//! Assess metadata. This format is shared between 'assess' and 'assess scan'. -//! Assess produces this for one workspace, scan for several. -//! It is not a stable file format: it is meant for assess to directly communicate -//! from assess subprocesses to a parent scan process. -//! We can build other tools that make use of it, but they need to be built for or distributed -//! with the specific version of Kani. - -use std::fs::File; -use std::io::BufWriter; -use std::path::Path; - -use anyhow::Result; -use serde::{Deserialize, Serialize}; - -use super::AssessArgs; -use super::table_builder::TableBuilder; -use super::table_failure_reasons::FailureReasonsTableRow; -use super::table_promising_tests::PromisingTestsTableRow; -use super::table_unsupported_features::UnsupportedFeaturesTableRow; - -/// The structure of `.kani-assess-metadata.json` files. This is a the structure for both -/// assess (standard) and scan. It it meant to hold results for one or more packages. -/// -/// This is not a stable interface. -#[derive(Serialize, Deserialize)] -pub struct AssessMetadata { - /// Kani version that was used to generate the metadata. - #[serde(rename = "kani_version")] - pub version: String, - /// Contains an error message in cases where it failed the execution. - pub error: Option, - /// Report on the presence of `codegen_unimplemented` in the analyzed packages - pub unsupported_features: TableBuilder, - /// Report of the reasons why tests could not be analyzed by Kani - pub failure_reasons: TableBuilder, - /// Report on the tests that Kani can successfully analyze - pub promising_tests: TableBuilder, -} - -impl AssessMetadata { - pub fn new( - unsupported_features: TableBuilder, - failure_reasons: TableBuilder, - promising_tests: TableBuilder, - ) -> AssessMetadata { - AssessMetadata { - version: env!("CARGO_PKG_VERSION").to_string(), - error: None, - unsupported_features, - failure_reasons, - promising_tests, - } - } - - pub fn from_error(err: &dyn std::error::Error) -> AssessMetadata { - let error = Some(SessionError { - root_cause: err.source().map(|e| format!("{e:#}")), - msg: err.to_string(), - }); - AssessMetadata { - version: env!("CARGO_PKG_VERSION").to_string(), - error, - unsupported_features: TableBuilder::new(), - failure_reasons: TableBuilder::new(), - promising_tests: TableBuilder::new(), - } - } - pub fn empty() -> AssessMetadata { - AssessMetadata { - version: env!("CARGO_PKG_VERSION").to_string(), - error: None, - unsupported_features: TableBuilder::new(), - failure_reasons: TableBuilder::new(), - promising_tests: TableBuilder::new(), - } - } -} - -#[derive(Serialize, Deserialize, Debug)] -pub struct SessionError { - pub root_cause: Option, - pub msg: String, -} - -/// If given the argument to so do, write the assess metadata to the target file. -pub(crate) fn write_metadata(args: &AssessArgs, metadata: AssessMetadata) -> Result<()> { - if let Some(path) = &args.emit_metadata { - let out_file = File::create(path)?; - let writer = BufWriter::new(out_file); - // use pretty for now to keep things readable and debuggable, but this should change eventually - serde_json::to_writer_pretty(writer, &metadata)?; - } - Ok(()) -} - -/// Read assess metadata from a file. -pub(crate) fn read_metadata(path: &Path) -> Result { - // this function already exists, but a proxy here helps find it :) - crate::metadata::from_json(path) -} - -/// Given assess metadata from several sources, aggregate them into a single strcture. -/// -/// This is not a complicated operation, because the assess metadata structure is meant -/// to accomodate multiple packages already, so we're just "putting it together". -pub(crate) fn aggregate_metadata(metas: Vec) -> AssessMetadata { - let mut result = AssessMetadata::empty(); - for meta in metas { - for item in meta.unsupported_features.build() { - result.unsupported_features.add(item.clone()); - } - for item in meta.failure_reasons.build() { - result.failure_reasons.add(item.clone()); - } - for item in meta.promising_tests.build() { - result.promising_tests.add(item.clone()); - } - } - result -} diff --git a/kani-driver/src/assess/mod.rs b/kani-driver/src/assess/mod.rs deleted file mode 100644 index 02b3da0974f8..000000000000 --- a/kani-driver/src/assess/mod.rs +++ /dev/null @@ -1,176 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -use self::metadata::{AssessMetadata, write_metadata}; -use anyhow::{Result, bail}; -use kani_metadata::KaniMetadata; - -use crate::assess::table_builder::TableBuilder; -use crate::metadata::merge_kani_metadata; -use crate::project; -use crate::session::KaniSession; - -pub use crate::args::{AssessArgs, AssessSubcommand}; - -mod metadata; -mod scan; -mod table_builder; -mod table_failure_reasons; -mod table_promising_tests; -mod table_unsupported_features; - -/// `cargo kani assess` main entry point. -/// -/// See -pub(crate) fn run_assess(session: KaniSession, args: AssessArgs) -> Result<()> { - if let Some(AssessSubcommand::Scan(args)) = &args.command { - return scan::assess_scan_main(session, args); - } - - let result = assess_project(session); - match result { - Ok(metadata) => write_metadata(&args, metadata), - Err(err) => { - let metadata = AssessMetadata::from_error(err.as_ref()); - write_metadata(&args, metadata)?; - Err(err.context("Failed to assess project")) - } - } -} - -fn assess_project(mut session: KaniSession) -> Result { - // Fix (as in "make unchanging/unchangable") some settings. - // This is a temporary hack to make things work, until we get around to refactoring how arguments - // work generally in kani-driver. These arguments, for instance, are all prepended to the subcommand, - // which is not a nice way of taking arguments. - session.args.unwind = Some(session.args.default_unwind.unwrap_or(1)); - session.args.tests = true; - session.args.output_format = crate::args::OutputFormat::Terse; - session.codegen_tests = true; - if session.args.jobs.is_none() { - // assess will default to fully parallel instead of single-threaded. - // can be overridden with e.g. `cargo kani -Z unstable-options -j 8 assess` - session.args.jobs = Some(None); // -j, num_cpu - } - - let project = project::cargo_project(&mut session, true)?; - let cargo_metadata = project.cargo_metadata.as_ref().expect("built with cargo"); - - let packages_metadata = - reconstruct_metadata_structure(&session, cargo_metadata, &project.metadata)?; - - // We don't really have a list of crates that went into building our various targets, - // so we can't easily count them. - - // It would also be interesting to classify them by whether they build without warnings or not. - // Tracking for the latter: https://github.com/model-checking/kani/issues/1758 - - let build_fail = project.failed_targets.as_ref().unwrap(); - match (build_fail.len(), packages_metadata.len()) { - (0, 0) => println!("No relevant data was found."), - (0, succeeded) => println!("Analyzed {succeeded} packages"), - (_failed, 0) => bail!("Failed to build all targets"), - (failed, succeeded) => { - println!("Analyzed {succeeded} packages. Failed to build {failed} targets",) - } - } - - let metadata = merge_kani_metadata(packages_metadata.clone()); - let unsupported_features = table_unsupported_features::build(&packages_metadata); - if !metadata.unsupported_features.is_empty() { - println!("{}", unsupported_features.render()); - } else { - println!("No crates contained Rust features unsupported by Kani"); - } - - if session.args.only_codegen { - return Ok(AssessMetadata::new( - unsupported_features, - TableBuilder::new(), - TableBuilder::new(), - )); - } - - // Done with the 'cargo-kani' part, now we're going to run *test* harnesses instead of proof: - let harnesses = Vec::from_iter(metadata.test_harnesses.iter()); - let runner = crate::harness_runner::HarnessRunner { sess: &session, project: &project }; - - let results = runner.check_all_harnesses(&harnesses)?; - - // two tables we want to print: - // 1. "Reason for failure" will count reasons why harnesses did not succeed - // e.g. successs 6 - // unwind 234 - let failure_reasons = table_failure_reasons::build(&results); - println!("{}", failure_reasons.render()); - - // TODO: Should add another interesting table: Count the actually hit constructs (e.g. 'try', 'InlineAsm', etc) - // The above table will just say "unsupported_construct 6" without telling us which constructs. - // Tracking issue: https://github.com/model-checking/kani/issues/1819 - - // 2. "Test cases that might be good proof harness starting points" - // e.g. All Successes and maybe Assertions? - let promising_tests = table_promising_tests::build(&results); - println!("{}", promising_tests.render()); - - Ok(AssessMetadata::new(unsupported_features, failure_reasons, promising_tests)) -} - -/// Merges a collection of Kani metadata by figuring out which package each belongs to, from cargo metadata. -/// -/// Initially, `kani_metadata` is a kani metadata structure for each _target_ of every package. -/// This function works by collecting each target and merging them into a package-wide metadata. -/// -/// This function, properly speaking, should not exist. We should have this information already from `Project`. -/// This should function should be removable when we fix how driver handles metadata: -/// -fn reconstruct_metadata_structure( - session: &KaniSession, - cargo_metadata: &cargo_metadata::Metadata, - kani_metadata: &[KaniMetadata], -) -> Result> { - let mut remaining_metas = kani_metadata.to_owned(); - let mut package_metas = vec![]; - for package in cargo_metadata.workspace_packages() { - if !session.args.cargo.package.is_empty() { - // If a specific package (set) is requested, skip all other packages. - // This is a necessary workaround because we're reconstructing which metas go to which packages - // based on the "crate name" given to the target, and the same workspace can have two - // packages with targets that have the same crate name. - // This is just an inherent problem with trying to reconstruct this information, and should - // be fixed by the issue linked in the function description. - // The best we can do for now is ignore packages we know we didn't build, to reduce the amount - // of confusion we might suffer here (which at least solves the problem for 'scan' which only - // builds 1 package at a time.) - if !session.args.cargo.package.contains(&package.name) { - continue; - } - } - let mut package_artifacts = vec![]; - for target in &package.targets { - // cargo_metadata doesn't provide name mangling help here? - // We need to know cargo's name changes when it's given to rustc, because kani-metadata - // records `crate_name` as rustc sees it, but `target` is name as cargo sees it - let target_name = target.name.replace('-', "_"); - if let Some(i) = remaining_metas.iter().position(|x| x.crate_name == target_name) { - let md = remaining_metas.swap_remove(i); - package_artifacts.push(md); - } else { - println!( - "Didn't find metadata for target {} (kind {:?}) in package {}", - target.name, target.kind, package.name - ) - } - } - if !package_artifacts.is_empty() { - let mut merged = crate::metadata::merge_kani_metadata(package_artifacts); - merged.crate_name.clone_from(&package.name); - package_metas.push(merged); - } - } - if !remaining_metas.is_empty() { - let remaining_names: Vec<_> = remaining_metas.into_iter().map(|x| x.crate_name).collect(); - println!("Found remaining (unused) metadata after reconstruction: {remaining_names:?}"); - } - Ok(package_metas) -} diff --git a/kani-driver/src/assess/scan.rs b/kani-driver/src/assess/scan.rs deleted file mode 100644 index b7c0aa7463cb..000000000000 --- a/kani-driver/src/assess/scan.rs +++ /dev/null @@ -1,240 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -use std::collections::HashSet; -use std::path::Path; -use std::path::PathBuf; -use std::time::Instant; - -use anyhow::Result; -use cargo_metadata::Package; - -use crate::session::KaniSession; -use crate::session::setup_cargo_command; - -use super::metadata::AssessMetadata; -use super::metadata::{aggregate_metadata, read_metadata}; -use crate::args::ScanArgs; - -/// `cargo kani assess scan` is not a normal invocation of `cargo kani`: we don't directly build anything. -/// Instead we perform a scan of the local directory for all cargo projects, and run assess on each of those. -/// Then we aggregate the results. -/// -/// This is actually similar to something cargo does when it's trying to find a package in a git repo -/// (e.g. from `cargo install --git`) so we draw inspiration from `cargo::ops::cargo_read_manifest::read_packages`. -/// -/// A simplified version of this algorithm looks like: -/// 1. Walk directory trees, don't descend into `target` and also stop when finding a `Cargo.toml` -/// 2. Examine each `Cargo.toml` (potentially a workspace of multiple packages) -/// 3. Aggregate all of those together. -pub(crate) fn assess_scan_main(session: KaniSession, args: &ScanArgs) -> Result<()> { - let cargo_toml_files = { - let mut files = Vec::new(); - scan_cargo_projects(PathBuf::from("."), &mut files); - files - }; - let build_target = env!("TARGET"); // see build.rs - let project_metadata = { - // Things kind blow up trying to handle errors here, so write it iteratively instead of using map - let mut metas = Vec::with_capacity(cargo_toml_files.len()); - for file in cargo_toml_files { - let meta = cargo_metadata::MetadataCommand::new() - .features(cargo_metadata::CargoOpt::AllFeatures) - .no_deps() - .manifest_path(file) - .other_options(vec![String::from("--filter-platform"), build_target.to_owned()]) - .exec()?; - metas.push(meta); - } - metas - }; - let projects: Vec<_> = project_metadata.iter().flat_map(|x| &x.packages).collect(); - let package_filter = { - if let Some(path) = &args.filter_packages_file { - let file = std::fs::File::open(path)?; - let reader = std::io::BufReader::new(file); - use std::io::BufRead; - let set: HashSet = reader.lines().map(|x| x.expect("text")).collect(); - Some(set) - } else { - None - } - }; - - for project in projects { - println!("Found {}: {}", project.name, project.manifest_path); - } - - let overall_start_time = Instant::now(); - - let mut failed_packages = Vec::new(); - let mut success_metas = Vec::new(); - for workspace in &project_metadata { - let workspace_root = workspace.workspace_root.as_std_path(); - for package in workspace.workspace_packages() { - if let Some(filter) = &package_filter - && !filter.contains(package.name.as_ref()) - { - println!("Skipping filtered-out package {}", package.name); - continue; - } - // This is a hack. Some repos contains workspaces with "examples" (not actually cargo examples, but - // full packages as workspace members) that are named after other crates. - // It's not fully clear what approach we should take to fix this. - // For the moment, we try to filter out "example" packages through this hack. - // Current known instances: `syn` contains a package named `lazy_static`. - // (syn/examples/lazy-static/lazy-static/Cargo.toml) - if package.manifest_path.components().any(|x| x.as_str() == "examples") { - println!( - "Warning: Skipping (by heuristic) {} in {}", - package.name, workspace.workspace_root - ); - continue; - } - let package_start_time = Instant::now(); - let name = &package.name; - let manifest = package.manifest_path.as_std_path(); - - // We could reasonably choose to write these under 'target/kani', but can't because that gets deleted when 'cargo kani' runs. - // We could reasonably choose to write these under 'target', but the present way I experiment with 'assess' - // deletes target directories to save disk space in large runs. (Builds are big!) - // So at present we choose to put them next to the workspace root Cargo.toml. - let outfile = workspace_root.join(format!("{name}.kani-assess-metadata.json")); - let logfile = workspace_root.join(format!("{name}.kani-assess.log")); - - let result = if args.existing_only { - Ok(()) - } else { - invoke_assess(&session, name, manifest, &outfile, &logfile) - }; - - let meta = read_metadata(&outfile); - if let Ok(meta) = meta { - if meta.error.is_some() { - println!("Failed: {name}"); - // Some execution error that we have collected. - failed_packages.push((package, Some(meta))) - } else { - success_metas.push(meta); - } - } else { - println!("Failed: {name}"); - failed_packages.push(( - package, - result.err().map(|err| AssessMetadata::from_error(err.as_ref())), - )); - } - //TODO: cargo clean? - println!( - "Package {} analysis time: {}", - name, - package_start_time.elapsed().as_secs_f32() - ); - } - } - - println!("Overall analysis time: {}s", overall_start_time.elapsed().as_secs_f32()); - println!( - "Assessed {} successfully, with {} failures.", - success_metas.len(), - failed_packages.len() - ); - let results = aggregate_metadata(success_metas); - print_failures(failed_packages); - println!("{}", results.unsupported_features.render()); - - if !session.args.only_codegen { - println!("{}", results.failure_reasons.render()); - println!("{}", results.promising_tests.render()); - } - - if let Some(path) = &args.emit_metadata { - let out_file = std::fs::File::create(path)?; - let writer = std::io::BufWriter::new(out_file); - // use pretty for now to keep things readable and debuggable, but this should change eventually - serde_json::to_writer_pretty(writer, &results)?; - } - - Ok(()) -} - -/// Calls `cargo kani assess` on a single package. -fn invoke_assess( - session: &KaniSession, - package: &str, - manifest: &Path, - outfile: &Path, - logfile: &Path, -) -> Result<()> { - let dir = manifest.parent().expect("file not in a directory?"); - let log = std::fs::File::create(logfile)?; - - let mut cmd = setup_cargo_command()?; - cmd.arg("kani"); - // Use of options before 'assess' subcommand is a hack, these should be factored out. - // TODO: --only-codegen should be outright an option to assess. (perhaps tests too?) - if session.args.only_codegen { - cmd.arg("--only-codegen"); - } - // TODO: -p likewise, probably fixed with a "CargoArgs" refactoring - // Additionally, this should be `--manifest-path` but `cargo kani` doesn't support that yet. - cmd.arg("-p").arg(package); - // This has to be after `-p` due to an argument parsing bug in kani-driver - cmd.arg("-Zunstable-options"); - cmd.args(["assess", "--emit-metadata"]) - .arg(outfile) - .current_dir(dir) - .stdout(log.try_clone()?) - .stderr(log) - .env("RUST_BACKTRACE", "1"); - println!("Running {}", crate::util::render_command(&cmd).to_string_lossy()); - anyhow::ensure!(cmd.status()?.success()); - Ok(()) -} - -/// A short-circuiting directory walk for finding Cargo.toml files. -/// Sadly, strangely difficult to do with high-level libraries, so implement it ourselves -fn scan_cargo_projects(path: PathBuf, accumulator: &mut Vec) { - debug_assert!(path.is_dir()); - let cargo_file = path.join("Cargo.toml"); - if cargo_file.exists() { - accumulator.push(cargo_file); - // short-circuit and stop descending - return; - } - // Errors are silently skipped entirely here - let Ok(entries) = std::fs::read_dir(path) else { - return; - }; - for entry in entries { - let Ok(entry) = entry else { - continue; - }; - let Ok(typ) = entry.file_type() else { - continue; - }; - // symlinks are not `is_dir()` - if typ.is_dir() { - scan_cargo_projects(entry.path(), accumulator) - } - } -} - -/// Print failures if any happened. -fn print_failures(mut failures: Vec<(&Package, Option)>) { - if !failures.is_empty() { - println!("Failed to assess packages:"); - let unknown = "Unknown".to_string(); - failures.sort_by_key(|(pkg, _)| &pkg.name); - for (pkg, meta) in failures { - println!( - " - `{}`: {}", - pkg.name, - meta.as_ref().map_or(&unknown, |md| { - md.error.as_ref().map_or(&unknown, |error| &error.msg) - }), - ); - } - println!(); - } -} diff --git a/kani-driver/src/assess/table_builder.rs b/kani-driver/src/assess/table_builder.rs deleted file mode 100644 index 58f426b6a742..000000000000 --- a/kani-driver/src/assess/table_builder.rs +++ /dev/null @@ -1,202 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -//! This module contains code that helps build tables more easily. -//! -//! Virtually all assess tables are built via the same method: -//! -//! 1. There is some input data with irregular structure -//! 2. There is an implied (we avoid writing it) type with regular structure -//! 3. There is the type of the table row -//! -//! As an abstract example, #1 is often something like `[(Node, [Node])]` which you can think of -//! as a graph. #2 is a normalized version like `[(Node, Node)]` which is an ordinary -//! adjacency list. #3 ends up being a structure like `(Node name, outgoing edge count)`. -//! -//! With this module, you construct a table by: -//! -//! 1. Create a type for a table row (#3 above). -//! 2. Write the code to traverse your irregular structure (#1) and produce table rows. -//! 3. Implement [`TableRow`] for your table row type, which implements -//! an [`TableRow::merge`] method. This avoids having to create a type for -//! the intermediate "regular" structure (#2 above), by instead thinking in -//! terms of merging rows by their [`TableRow::key`]. (Vaguely like map-reduce.) -//! 4. Use [`TableBuilder`] to construct the table. -//! 5. (Optional) Implement [`RenderableTableRow`] so you can print the table. - -use std::cmp::Ordering; -use std::collections::HashMap; -use std::hash::Hash; - -use comfy_table::Table; -use serde::{Deserialize, Serialize}; - -/// A [`TableRow`] is a type where multiple "rows" with the same `key` should be `merge`d into one. -/// This type is used in conjuction with [`TableBuilder`]. -/// -/// We further give an ordering (via `compare`) that defines how rows should appear in the final table. -pub trait TableRow { - type Key: Eq + Hash; - - /// Returns the key for this row entry, so that multiple entries with the same key can be aggregated - fn key(&self) -> Self::Key; - /// Merges two rows into one. `self` is always the existing (or first) entry, `new` is what should be merged in. - fn merge(&mut self, new: Self); - /// Define the order rows should appear in a table. Not needed for merging, but required for producing results. - fn compare(&self, right: &Self) -> Ordering; -} - -/// What kind of data appears in a table column, when visually rendered for the user. -pub enum ColumnType { - /// Text might be very wide and need limiting, and it should be left-justified. - Text, - /// Numbers should be right-justified. - Number, -} - -/// Describes how a table should be printed visually. -/// -/// This is an extension to [`TableRow`] (which is solely concerned with computing a table's contents.) -/// In this trait, we are solely concerned with how the table should look when printed. -pub trait RenderableTableRow { - /// Headers, e.g. " Reason for failure | Number of tests " - fn headers() -> Vec<&'static str>; - /// Column types, e.g. [Text, Number] - fn columns() -> Vec; - /// The row contents, e.g. ["unwind", "1"] - fn row(&self) -> Vec; -} - -/// Implements the basic algorithm for constructing tables by merging rows by their keys. -/// -/// ``` -/// let mut builder = TableBuilder::new(); -/// -/// for entry in some_data { -/// builder.add(MyTableRowType { ... }); -/// } -/// -/// builder.build() -/// // or -/// builder.render() -/// ``` -pub struct TableBuilder -where - R: TableRow, -{ - map: HashMap, -} - -impl TableBuilder { - /// Creates a new TableBuilder. `R` must implement `TableRow`. - pub fn new() -> Self { - TableBuilder { map: HashMap::new() } - } - - /// Incrementally add new row data to the table, by merging it with any entry that - /// shares its key. - pub fn add(&mut self, row: R) { - let entry = self.map.entry(row.key()); - // unfortunately ownership of row makes it somewhat difficult to use the entry methods, - // so actually branch here so it's clear we only use 'row' once really - use std::collections::hash_map::Entry::*; - match entry { - Occupied(o) => { - o.into_mut().merge(row); - } - Vacant(v) => { - v.insert(row); - } - } - } - - /// Construct a pure-data table. - pub fn build(&self) -> Vec<&R> { - let mut values: Vec<_> = self.map.values().collect(); - values.sort_by(|a, b| a.compare(b)); - values - } - - /// Returns a renderable `Table` for human consumption. - /// - /// This is the only part of `TableBuilder` that requires `RenderableTableRow`. - pub fn render(&self) -> Table - where - R: RenderableTableRow, - { - use comfy_table::*; - - let mut table = assess_table_new(); - table.set_header(R::headers()); - for (index, ty) in R::columns().iter().enumerate() { - let col = table.column_mut(index).unwrap(); - - match ty { - ColumnType::Text => { - col.set_cell_alignment(CellAlignment::Left); - col.set_constraint(ColumnConstraint::UpperBoundary(Width::Fixed(80))); - } - ColumnType::Number => { - col.set_cell_alignment(CellAlignment::Right); - } - } - } - - for v in self.build() { - table.add_row(v.row()); - } - - table - } -} - -impl Serialize for TableBuilder -where - R: Serialize + TableRow, -{ - /// To serialize a TableBuilder, we use [`TableBuilder::build`] to construct a vector - /// and simply serialize the result. - fn serialize(&self, serializer: S) -> Result - where - S: serde::Serializer, - { - let result = self.build(); - result.serialize(serializer) - } -} -impl<'de, R> Deserialize<'de> for TableBuilder -where - R: Deserialize<'de> + TableRow, -{ - /// To deserialize a TableBuilder, we deserialize a vector of [`TableRow`] and - /// add each one to the table. - fn deserialize(deserializer: D) -> Result - where - D: serde::Deserializer<'de>, - { - let rows: Vec = Deserialize::deserialize(deserializer)?; - let mut result = TableBuilder::new(); - for row in rows { - result.add(row); - } - Ok(result) - } -} - -/// Internal helper function for [`TableBuilder::render`] that sets our "comfy table" styling -fn assess_table_new() -> Table { - use comfy_table::*; - - let mut table = Table::new(); - table.set_content_arrangement(ContentArrangement::Dynamic); - table - .load_preset(comfy_table::presets::NOTHING) - .set_style(TableComponent::BottomBorder, '=') - .set_style(TableComponent::BottomBorderIntersections, '=') - .set_style(TableComponent::TopBorder, '=') - .set_style(TableComponent::TopBorderIntersections, '=') - .set_style(TableComponent::HeaderLines, '-') - .set_style(TableComponent::MiddleHeaderIntersections, '+') - .set_style(TableComponent::VerticalLines, '|'); - table -} diff --git a/kani-driver/src/assess/table_failure_reasons.rs b/kani-driver/src/assess/table_failure_reasons.rs deleted file mode 100644 index 0566532dd9df..000000000000 --- a/kani-driver/src/assess/table_failure_reasons.rs +++ /dev/null @@ -1,125 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -use std::cmp::Ordering; -use std::collections::HashSet; - -use serde::{Deserialize, Serialize}; - -use crate::{call_cbmc::ExitStatus, harness_runner::HarnessResult}; - -use super::table_builder::{ColumnType, RenderableTableRow, TableBuilder, TableRow}; - -/// Reports the most common "failure reasons" for tests run by assess. -/// -/// The reasons are presently just a combination of "property classes" -/// from failed CBMC properties. This is only really meaningful to us, -/// and could use significant improvement for customers. In fact, -/// this particular data set might *only* be interesting to us as -/// developers of 'assess', and not customers, once we get fewer failures -/// and the heuristics for "promising tests" are improved. -/// -/// Example: -/// -/// ```text -/// ================================================ -/// Reason for failure | Number of tests -/// ------------------------------+----------------- -/// unwind | 61 -/// none (success) | 6 -/// assertion | 4 -/// assertion + overflow | 2 -/// ================================================ -/// ``` -pub(crate) fn build(results: &[HarnessResult]) -> TableBuilder { - let mut builder = TableBuilder::new(); - - for r in results { - let classification = if let Err(exit_status) = r.result.results { - match exit_status { - ExitStatus::Timeout => String::from("CBMC timed out"), - ExitStatus::OutOfMemory => String::from("CBMC ran out of memory"), - ExitStatus::Other(exit_code) => format!("CBMC failed with status {exit_code}"), - } - } else { - let failures = r.result.failed_properties(); - if failures.is_empty() { - "none (success)".to_string() - } else { - let mut classes: Vec<_> = - failures.into_iter().map(|p| p.property_class()).collect(); - classes.sort(); - classes.dedup(); - classes.join(" + ") - } - }; - - let name = r.harness.pretty_name.trim_end_matches("::{closure#0}").to_string(); - let identity = - format!("{} @ {}:{}", name, r.harness.original_file, r.harness.original_start_line); - - builder.add(FailureReasonsTableRow { - reason: classification, - tests: HashSet::from([identity]), - }); - } - - builder -} - -/// Reports the reasons that tests failed to be analyzed by Kani -/// -/// See [`build`] -#[derive(Default, Debug, Clone, Serialize, Deserialize)] -pub struct FailureReasonsTableRow { - /// "Failure reasons" look like "unwind" or "assertion + overflow" - pub reason: String, - /// Tests are identified by "pretty_name @ /full/path/file.rs:line" - pub tests: HashSet, -} - -impl TableRow for FailureReasonsTableRow { - type Key = String; - - fn key(&self) -> Self::Key { - self.reason.clone() - } - - fn merge(&mut self, new: Self) { - self.tests.extend(new.tests); - } - - fn compare(&self, right: &Self) -> Ordering { - self.tests - .len() - .cmp(&right.tests.len()) - .reverse() - .then_with(|| self.reason.cmp(&right.reason)) - } -} - -impl RenderableTableRow for FailureReasonsTableRow { - fn headers() -> Vec<&'static str> { - vec!["Reason for failure", "Number of tests"] - } - - fn columns() -> Vec { - vec![ColumnType::Text, ColumnType::Number] - } - - fn row(&self) -> Vec { - vec![self.reason.clone(), self.tests.len().to_string()] - } -} - -#[cfg(test)] -mod tests { - use super::*; - - #[test] - fn check_row_lengths() { - use FailureReasonsTableRow as Row; - assert_eq!(Row::columns().len(), Row::headers().len()); - assert_eq!(Row::columns().len(), Row::row(&Default::default()).len()); - } -} diff --git a/kani-driver/src/assess/table_promising_tests.rs b/kani-driver/src/assess/table_promising_tests.rs deleted file mode 100644 index 8a84959a3b9b..000000000000 --- a/kani-driver/src/assess/table_promising_tests.rs +++ /dev/null @@ -1,103 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -use std::cmp::Ordering; - -use serde::{Deserialize, Serialize}; - -use crate::harness_runner::HarnessResult; - -use super::table_builder::{ColumnType, RenderableTableRow, TableBuilder, TableRow}; - -/// Reports the "test harnesses" most likely to be easily turned into proof harnesses. -/// -/// This presently is very naive and just reports successful harnesses, however -/// there is significant potential here to make use of improved heuristics, -/// and to find a way to *sort* these harnesses. -/// -/// Example: -/// ```text -/// ============================================================================= -/// Candidate for proof harness | Location -/// -------------------------------------------------------+--------------------- -/// float::tests::f64_edge_cases | src/float.rs:226 -/// float::tests::f32_edge_cases | src/float.rs:184 -/// integer::tests::test_integers | src/integer.rs:171 -/// other::tests::test_misc | src/other.rs:284 -/// ============================================================================= -/// ``` -pub(crate) fn build(results: &[HarnessResult]) -> TableBuilder { - let mut builder = TableBuilder::new(); - - for r in results.iter().filter(|res| res.result.results.is_ok()) { - // For now we're just reporting "successful" harnesses as candidates. - // In the future this heuristic should be expanded. More data is required to do this, however. - if r.result.failed_properties().is_empty() { - // The functions assess runs are actually the closures inside the test harness macro expansion. - // This means they have (pretty) names like `krate::module::a_test_name::{closure#0}` - // Strip that closure suffix, so we have better names for showing humans: - let name = r.harness.pretty_name.trim_end_matches("::{closure#0}").to_string(); - // Location in a format "clickable" in e.g. IDE terminals - let location = format!("{}:{}", r.harness.original_file, r.harness.original_start_line); - - builder.add(PromisingTestsTableRow { name, location }); - } - } - - builder -} - -/// Reports tests that Kani successfully analyzes, with a direct link to the test for easy viewing. -/// -/// See [`build`] -#[derive(Default, Debug, Clone, Serialize, Deserialize)] -pub struct PromisingTestsTableRow { - /// The "pretty name" of the test, like "module::test_name" - pub name: String, - /// The "clickable location" of the test, like "/full/path/to/file.rs:123" - pub location: String, -} - -impl TableRow for PromisingTestsTableRow { - type Key = String; - - fn key(&self) -> Self::Key { - self.name.clone() - } - - fn merge(&mut self, _new: Self) { - unreachable!("This table should never have duplicate keys") - } - - fn compare(&self, right: &Self) -> Ordering { - // In the future this should use heuristics, but for now we have no really desired order - self.name.cmp(&right.name) - } -} - -impl RenderableTableRow for PromisingTestsTableRow { - fn headers() -> Vec<&'static str> { - vec!["Candidate for proof harness", "Location"] - } - - fn columns() -> Vec { - use ColumnType::*; - vec![Text, Text] - } - - fn row(&self) -> Vec { - vec![self.name.to_owned(), self.location.to_owned()] - } -} - -#[cfg(test)] -mod tests { - use super::*; - - #[test] - fn check_row_lengths() { - use PromisingTestsTableRow as Row; - assert_eq!(Row::columns().len(), Row::headers().len()); - assert_eq!(Row::columns().len(), Row::row(&Default::default()).len()); - } -} diff --git a/kani-driver/src/assess/table_unsupported_features.rs b/kani-driver/src/assess/table_unsupported_features.rs deleted file mode 100644 index 6466ca434bed..000000000000 --- a/kani-driver/src/assess/table_unsupported_features.rs +++ /dev/null @@ -1,115 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -use std::{cmp::Ordering, collections::HashSet}; - -use kani_metadata::KaniMetadata; -use serde::{Deserialize, Serialize}; - -use super::table_builder::{ColumnType, RenderableTableRow, TableBuilder, TableRow}; - -/// Reports unsupported features, in descending order of number of crates impacted. -/// -/// The feature names come directly from the `operation_name` listed in `codegen_unimplemented` -/// -/// For example: -/// -/// ```text -/// =================================================== -/// Unsupported feature | Crates | Instances -/// | impacted | of use -/// ----------------------------+----------+----------- -/// 'simd_or' intrinsic | 4 | 5 -/// try | 2 | 17 -/// drop_in_place | 2 | 2 -/// =================================================== -/// ``` -pub(crate) fn build(metadata: &[KaniMetadata]) -> TableBuilder { - let mut builder = TableBuilder::new(); - - for package_metadata in metadata { - for item in &package_metadata.unsupported_features { - // key is unsupported feature name - let mut key = item.feature.clone(); - // There are several "feature for " unsupported features. - // We aggregate those here by reducing it to just "feature". - // We should replace this with an enum: https://github.com/model-checking/kani/issues/1765 - if let Some((prefix, _)) = key.split_once(" for ") { - key = prefix.to_string(); - } - - builder.add(UnsupportedFeaturesTableRow { - unsupported_feature: key, - crates_impacted: HashSet::from([package_metadata.crate_name.to_owned()]), - instances_of_use: item.locations.len(), - }) - } - } - - builder -} - -/// Reports features that Kani does not yet support and records the packages that triggered these warnings. -/// -/// See [`build`] -#[derive(Default, Debug, Clone, Serialize, Deserialize)] -pub struct UnsupportedFeaturesTableRow { - /// The unsupported feature name, generally given to `codegen_unimplemented` in `kani-compiler` - pub unsupported_feature: String, - /// The set of packages which had an instance of this feature somewhere in their build (even if from a reachable dependency) - pub crates_impacted: HashSet, - /// The total count of the uses of this feature (we don't record details about where from only because that seems uninteresting so far) - pub instances_of_use: usize, -} - -impl TableRow for UnsupportedFeaturesTableRow { - type Key = String; - - fn key(&self) -> Self::Key { - self.unsupported_feature.clone() - } - - fn merge(&mut self, new: Self) { - self.crates_impacted.extend(new.crates_impacted); - self.instances_of_use += new.instances_of_use; - } - - fn compare(&self, right: &Self) -> Ordering { - self.crates_impacted - .len() - .cmp(&right.crates_impacted.len()) - .reverse() - .then_with(|| self.instances_of_use.cmp(&right.instances_of_use).reverse()) - .then_with(|| self.unsupported_feature.cmp(&right.unsupported_feature)) - } -} -impl RenderableTableRow for UnsupportedFeaturesTableRow { - fn headers() -> Vec<&'static str> { - vec!["Unsupported feature", "Crates\nimpacted", "Instances\nof use"] - } - - fn columns() -> Vec { - use ColumnType::*; - vec![Text, Number, Number] - } - - fn row(&self) -> Vec { - vec![ - self.unsupported_feature.clone(), - self.crates_impacted.len().to_string(), - self.instances_of_use.to_string(), - ] - } -} - -#[cfg(test)] -mod tests { - use super::*; - - #[test] - fn check_row_lengths() { - use UnsupportedFeaturesTableRow as Row; - assert_eq!(Row::columns().len(), Row::headers().len()); - assert_eq!(Row::columns().len(), Row::row(&Default::default()).len()); - } -} diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index 717c7c65b297..b834dad3c657 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -34,8 +34,6 @@ pub struct CargoOutputs { pub metadata: Vec, /// Recording the cargo metadata from the build pub cargo_metadata: Metadata, - /// For build `keep_going` mode, we collect the targets that we failed to compile. - pub failed_targets: Option>, } impl KaniSession { @@ -238,12 +236,7 @@ crate-type = ["lib"] bail!("No supported targets were found."); } - Ok(CargoOutputs { - outdir, - metadata: artifacts, - cargo_metadata: metadata, - failed_targets: keep_going.then_some(failed_targets), - }) + Ok(CargoOutputs { outdir, metadata: artifacts, cargo_metadata: metadata }) } pub fn cargo_metadata(&self, build_target: &str) -> Result { diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 96351a4095ee..04ac73f79b51 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -424,16 +424,6 @@ impl VerificationResult { } } } - - /// Find the failed properties from this verification run - pub fn failed_properties(&self) -> Vec<&Property> { - if let Ok(properties) = &self.results { - properties.iter().filter(|prop| prop.status == CheckStatus::Failure).collect() - } else { - debug_assert!(false, "expected error to be handled before invoking this function"); - vec![] - } - } } /// We decide if verification succeeded based on properties, not (typically) on exit code diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index 5e32e458fa0a..972cbd5dfbd3 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -22,7 +22,6 @@ use tracing::debug; mod args; mod args_toml; -mod assess; mod autoharness; mod call_cargo; mod call_cbmc; @@ -70,25 +69,16 @@ fn cargokani_main(input_args: Vec) -> Result<()> { let args = args::CargoKaniArgs::parse_from(&input_args); check_is_valid(&args); - if let Some(CargoKaniSubcommand::List(list_args)) = args.command { - return list_cargo(*list_args, args.verify_opts); - } - - if let Some(CargoKaniSubcommand::Autoharness(autoharness_args)) = args.command { - return autoharness_cargo(*autoharness_args); - } - let mut session = match args.command { - Some(CargoKaniSubcommand::Assess(assess_args)) => { - let sess = session::KaniSession::new(args.verify_opts)?; - return assess::run_assess(sess, *assess_args); + Some(CargoKaniSubcommand::Autoharness(autoharness_args)) => { + return autoharness_cargo(*autoharness_args); + } + Some(CargoKaniSubcommand::List(list_args)) => { + return list_cargo(*list_args, args.verify_opts); } Some(CargoKaniSubcommand::Playback(args)) => { return playback_cargo(*args); } - Some(CargoKaniSubcommand::Autoharness(_)) | Some(CargoKaniSubcommand::List(_)) => { - unreachable!() - } None => session::KaniSession::new(args.verify_opts)?, }; @@ -96,10 +86,6 @@ fn cargokani_main(input_args: Vec) -> Result<()> { print_kani_version(InvocationType::CargoKani(input_args)); } - if session.args.assess { - return assess::run_assess(session, assess::AssessArgs::default()); - } - let project = project::cargo_project(&mut session, false)?; if session.args.only_codegen { Ok(()) } else { verify_project(project, session) } } diff --git a/kani-driver/src/metadata.rs b/kani-driver/src/metadata.rs index 5f83b298b9b8..367afbd5331f 100644 --- a/kani-driver/src/metadata.rs +++ b/kani-driver/src/metadata.rs @@ -5,9 +5,7 @@ use anyhow::{Result, bail}; use std::path::Path; use tracing::{debug, trace}; -use kani_metadata::{ - HarnessMetadata, InternedString, KaniMetadata, TraitDefinedMethod, VtableCtxResults, -}; +use kani_metadata::{HarnessMetadata, InternedString, TraitDefinedMethod, VtableCtxResults}; use std::collections::{BTreeSet, HashMap}; use std::fs::File; use std::io::{BufReader, BufWriter}; @@ -89,29 +87,6 @@ pub fn from_json Deserialize<'a>>(path: &Path) -> Result { Ok(obj) } -/// Consumes a vector of parsed metadata, and produces a combined structure -pub fn merge_kani_metadata(files: Vec) -> KaniMetadata { - let mut result = KaniMetadata { - crate_name: "cbmc-linked".to_string(), - proof_harnesses: vec![], - unsupported_features: vec![], - test_harnesses: vec![], - contracted_functions: vec![], - autoharness_md: None, - }; - 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. - result.proof_harnesses.extend(md.proof_harnesses); - // TODO: these should be merged via a map to aggregate them all - // 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); - // We do not handle autoharness metadata here, since this function is not reachable from the autoharness subcommand. - } - result -} - impl KaniSession { /// Determine which function to use as entry point, based on command-line arguments and kani-metadata. pub fn determine_targets<'a>( diff --git a/kani-driver/src/project.rs b/kani-driver/src/project.rs index 80a4b050adff..b17405032281 100644 --- a/kani-driver/src/project.rs +++ b/kani-driver/src/project.rs @@ -42,8 +42,6 @@ pub struct Project { artifacts: Vec, /// Records the cargo metadata from the build, if there was any pub cargo_metadata: Option, - /// For build `keep_going` mode, we collect the targets that we failed to compile. - pub failed_targets: Option>, } impl Project { @@ -90,7 +88,6 @@ impl Project { input: Option, metadata: Vec, cargo_metadata: Option, - failed_targets: Option>, ) -> Result { // For each harness (test or proof) from each metadata, read the path for the goto // SymTabGoto file. Use that path to find all the other artifacts. @@ -121,7 +118,7 @@ impl Project { } } - Ok(Project { outdir, input, metadata, artifacts, cargo_metadata, failed_targets }) + Ok(Project { outdir, input, metadata, artifacts, cargo_metadata }) } } @@ -188,14 +185,7 @@ pub fn cargo_project(session: &mut KaniSession, keep_going: bool) -> Result>>()?; - Project::try_new( - session, - outdir, - None, - metadata, - Some(outputs.cargo_metadata), - outputs.failed_targets, - ) + Project::try_new(session, outdir, None, metadata, Some(outputs.cargo_metadata)) } /// Generate a project directly using `kani-compiler` on a single crate. @@ -257,14 +247,8 @@ impl<'a> StandaloneProjectBuilder<'a> { let metadata = from_json(&self.metadata)?; // Create the project with the artifacts built by the compiler. - let result = Project::try_new( - self.session, - self.outdir, - Some(self.input), - vec![metadata], - None, - None, - ); + let result = + Project::try_new(self.session, self.outdir, Some(self.input), vec![metadata], None); if let Ok(project) = &result { self.session.record_temporary_files(&project.artifacts); } @@ -318,5 +302,5 @@ pub(crate) fn std_project(std_path: &Path, session: &KaniSession) -> Result>>()?; - Project::try_new(session, outdir, None, metadata, None, None) + Project::try_new(session, outdir, None, metadata, None) } diff --git a/kani-driver/src/session.rs b/kani-driver/src/session.rs index 900e7386ef47..01c475309972 100644 --- a/kani-driver/src/session.rs +++ b/kani-driver/src/session.rs @@ -35,11 +35,6 @@ pub struct KaniSession { /// Invariant: this field is_some() iff the autoharness subcommand is enabled. pub autoharness_compiler_flags: Option>, - /// Include all publicly-visible symbols in the generated goto binary, not just those reachable from - /// a proof harness. Useful when attempting to verify things that were not annotated with kani - /// proof attributes. - pub codegen_tests: bool, - /// The location we found the 'kani_rustc' command pub kani_compiler: PathBuf, /// The location we found 'kani_lib.c' @@ -70,7 +65,6 @@ impl KaniSession { Ok(KaniSession { args, autoharness_compiler_flags: None, - codegen_tests: false, kani_compiler: install.kani_compiler()?, kani_lib_c: install.kani_lib_c()?, temporaries: Mutex::new(vec![]), @@ -96,9 +90,7 @@ impl KaniSession { /// Determine which symbols Kani should codegen (i.e. by slicing away symbols /// that are considered unreachable.) pub fn reachability_mode(&self) -> ReachabilityMode { - if self.codegen_tests { - ReachabilityMode::Tests - } else if self.autoharness_compiler_flags.is_some() { + if self.autoharness_compiler_flags.is_some() { ReachabilityMode::AllFns } else { ReachabilityMode::ProofHarnesses @@ -112,7 +104,6 @@ pub enum ReachabilityMode { AllFns, #[strum(to_string = "harnesses")] ProofHarnesses, - Tests, } impl Drop for KaniSession { diff --git a/scripts/assess-scan-regression.sh b/scripts/assess-scan-regression.sh deleted file mode 100755 index 23800bb632f6..000000000000 --- a/scripts/assess-scan-regression.sh +++ /dev/null @@ -1,44 +0,0 @@ -#!/usr/bin/env bash -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -set -eu - -SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" -KANI_DIR=$SCRIPT_DIR/.. - -echo "Running assess scan test:" - -cd $KANI_DIR/tests/assess-scan-test-scaffold -cargo kani -Z unstable-options assess scan - -# Clean up -(cd foo && cargo clean) -(cd bar && cargo clean) -(cd compile_error && cargo clean) -(cd manifest_error && cargo clean) - -# Check for expected files (and clean up) -EXPECTED_FILES=( - bar/bar.kani-assess.log - bar/bar.kani-assess-metadata.json - compile_error/compile_error.kani-assess.log - compile_error/compile_error.kani-assess-metadata.json - manifest_error/manifest_error.kani-assess.log - manifest_error/manifest_error.kani-assess-metadata.json - foo/foo.kani-assess.log - foo/foo.kani-assess-metadata.json -) - -errors=0 -for file in ${EXPECTED_FILES[@]}; do - if [ -f $KANI_DIR/tests/assess-scan-test-scaffold/$file ]; then - rm $KANI_DIR/tests/assess-scan-test-scaffold/$file - else - errors=1 - echo "Failed to find $file" - fi -done - -echo "Done with assess scan test" -exit $errors diff --git a/scripts/exps/assess-scan-on-repos.sh b/scripts/exps/assess-scan-on-repos.sh deleted file mode 100755 index eaa6acb65f35..000000000000 --- a/scripts/exps/assess-scan-on-repos.sh +++ /dev/null @@ -1,68 +0,0 @@ -#!/bin/bash -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -# This script automates the process of checking out several git repos, then running -# 'cargo kani assess scan' on them (with '--only-codegen'). - -# Usage: -# ./scripts/exps/assess-scan-on-repos.sh -# Or (will clone in ~): -# ASSESS_SCAN="~/top-100-experiment" ./scripts/exps/assess-scan-on-repos.sh - -# To use a different set of packages, the script needs updating (below). - -set -eu - -THIS_SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" -# Remove 'scripts/exps/' -KANI_DIR=$THIS_SCRIPT_DIR/../.. - -# The target repos and crates to analyze -REPO_FILE="$KANI_DIR/tests/remote-target-lists/top-100-crates-2022-12-26.txt" -NAME_FILE="$KANI_DIR/tests/remote-target-lists/top-100-crate-names-2022-12-26.txt" - -# Where should we clone the repos? -# 1. If 'ASSESS_SCAN' environment variable is set, use that directory -if [ ${ASSESS_SCAN:-unset} != "unset" ]; then - mkdir -p $ASSESS_SCAN - cd $ASSESS_SCAN -# 2. If the current working directory happens to be named 'top-100-experiment' let's do it here -elif [ "${PWD##*/}" == "top-100-experiment" ]; then - true # nothing to do -# 3. Not finding any other direction, default to doing it in a directory in /tmp -else - mkdir -p /tmp/top-100-experiment - cd /tmp/top-100-experiment -fi - -echo "Cloning repos into ${PWD}" - -REPOS=$(cat $REPO_FILE) -for repo in $REPOS; do - # The directory that gets checked out is the final name in the url - dir=${repo##*/} - # Sometimes there's a '.git' after the end, strip that off - dir=${dir%.git} - if [ -d $dir ]; then - echo "Updating $dir..." - (cd $dir && git pull) - else - echo "Cloning $dir..." - git clone $repo - fi -done - -# Use release mode to speed up the run. -echo "Build kani on release mode..." -pushd ${KANI_DIR} -cargo build-dev --release -popd - -echo "Starting assess scan..." - -time cargo kani --only-codegen -Z unstable-options assess scan \ - --filter-packages-file $NAME_FILE \ - --emit-metadata ./scan-results.json - -echo "Complete." diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh index 6c3334a3e794..5c7767ded3ce 100755 --- a/scripts/kani-regression.sh +++ b/scripts/kani-regression.sh @@ -91,9 +91,6 @@ fi # Check codegen of firecracker time "$SCRIPT_DIR"/codegen-firecracker.sh -# Test run 'cargo kani assess scan' -"$SCRIPT_DIR"/assess-scan-regression.sh - # Test for --manifest-path which we cannot do through compiletest. # It should just successfully find the project and specified proof harness. (Then clean up.) FEATURES_MANIFEST_PATH="$KANI_DIR/tests/cargo-kani/cargo-features-flag/Cargo.toml" diff --git a/tests/assess-scan-test-scaffold/README.md b/tests/assess-scan-test-scaffold/README.md deleted file mode 100644 index 42c087647cb5..000000000000 --- a/tests/assess-scan-test-scaffold/README.md +++ /dev/null @@ -1,9 +0,0 @@ -# cargo kani assess scan test scaffold - -This directory contains two totally unrelated (i.e. no shared workspace) packages. -Its purpose is to test "assess scan" running in a directory containing such. - -This is used from `kani-regression.sh` to include a test for scan in CI. -The only thing we currently check is that the exit status was success and that files were emitted. -We presently don't have a way to run an arbitrary command with e.g. compiletest and expect. - diff --git a/tests/assess-scan-test-scaffold/bar/Cargo.toml b/tests/assess-scan-test-scaffold/bar/Cargo.toml deleted file mode 100644 index fa4e4da798b0..000000000000 --- a/tests/assess-scan-test-scaffold/bar/Cargo.toml +++ /dev/null @@ -1,7 +0,0 @@ -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -[package] -name = "bar" -version = "0.1.0" -edition = "2021" diff --git a/tests/assess-scan-test-scaffold/bar/src/lib.rs b/tests/assess-scan-test-scaffold/bar/src/lib.rs deleted file mode 100644 index 6581fe81c0c2..000000000000 --- a/tests/assess-scan-test-scaffold/bar/src/lib.rs +++ /dev/null @@ -1,13 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -#[test] -fn an_unsupported_test_from_bar() { - // unsupported feature: try instrinsic - assert!(std::panic::catch_unwind(|| panic!("test")).is_err()); -} - -#[test] -fn a_supported_test_from_bar() { - assert!(1 == 1); -} diff --git a/tests/assess-scan-test-scaffold/compile_error/Cargo.toml b/tests/assess-scan-test-scaffold/compile_error/Cargo.toml deleted file mode 100644 index 1189e08d0956..000000000000 --- a/tests/assess-scan-test-scaffold/compile_error/Cargo.toml +++ /dev/null @@ -1,11 +0,0 @@ -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -[package] -name = "compile_error" -version = "0.1.0" -edition = "2021" - -# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html - -[dependencies] diff --git a/tests/assess-scan-test-scaffold/compile_error/src/lib.rs b/tests/assess-scan-test-scaffold/compile_error/src/lib.rs deleted file mode 100644 index 2bad1be422f9..000000000000 --- a/tests/assess-scan-test-scaffold/compile_error/src/lib.rs +++ /dev/null @@ -1,7 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -/// Function with a compilation error -pub fn with_error(left: usize, right: u32) -> usize { - left + right -} diff --git a/tests/assess-scan-test-scaffold/foo/Cargo.toml b/tests/assess-scan-test-scaffold/foo/Cargo.toml deleted file mode 100644 index bbf5539c5dd5..000000000000 --- a/tests/assess-scan-test-scaffold/foo/Cargo.toml +++ /dev/null @@ -1,7 +0,0 @@ -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -[package] -name = "foo" -version = "0.1.0" -edition = "2021" diff --git a/tests/assess-scan-test-scaffold/foo/src/lib.rs b/tests/assess-scan-test-scaffold/foo/src/lib.rs deleted file mode 100644 index dbbfe74a4001..000000000000 --- a/tests/assess-scan-test-scaffold/foo/src/lib.rs +++ /dev/null @@ -1,13 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -#[test] -fn an_unsupported_test_from_foo() { - // unsupported feature: try instrinsic - assert!(std::panic::catch_unwind(|| panic!("test")).is_err()); -} - -#[test] -fn a_supported_test_from_foo() { - assert!(1 == 1); -} diff --git a/tests/assess-scan-test-scaffold/manifest_error/Cargo.toml b/tests/assess-scan-test-scaffold/manifest_error/Cargo.toml deleted file mode 100644 index 09b611dc645c..000000000000 --- a/tests/assess-scan-test-scaffold/manifest_error/Cargo.toml +++ /dev/null @@ -1,12 +0,0 @@ -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -[package] -name = "manifest_error" -version = "0.1.0" -edition = "2021" - -# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html - -[dependencies] -unknown = { path="./does/not/exist" } diff --git a/tests/assess-scan-test-scaffold/manifest_error/src/lib.rs b/tests/assess-scan-test-scaffold/manifest_error/src/lib.rs deleted file mode 100644 index 0058f8ca1b58..000000000000 --- a/tests/assess-scan-test-scaffold/manifest_error/src/lib.rs +++ /dev/null @@ -1,5 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -/// Nothing here -pub fn void() {} diff --git a/tests/cargo-kani/assess-artifacts/Cargo.toml b/tests/cargo-kani/assess-artifacts/Cargo.toml deleted file mode 100644 index 7b40e3443500..000000000000 --- a/tests/cargo-kani/assess-artifacts/Cargo.toml +++ /dev/null @@ -1,13 +0,0 @@ -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -[package] -name = "assess-artifacts" -version = "0.1.0" -edition = "2021" - -# See src/lib.rs for a comment on this tests's purpose - -[package.metadata.kani] -flags = { assess = true } -unstable = { unstable-options = true } diff --git a/tests/cargo-kani/assess-artifacts/expected b/tests/cargo-kani/assess-artifacts/expected deleted file mode 100644 index b8a25c834ab6..000000000000 --- a/tests/cargo-kani/assess-artifacts/expected +++ /dev/null @@ -1,19 +0,0 @@ -Analyzed 1 packages -============================================ - Unsupported feature | Crates | Instances - | impacted | of use ----------------------+----------+----------- - catch_unwind | 1 | 2 -============================================ -========================================= - Reason for failure | Number of tests ------------------------+----------------- - none (success) | 2 - unsupported_construct | 2 -========================================= -========================================== - Candidate for proof harness | Location --------------------------------+---------- - a_supported_test_from_tests | - a_supported_test_from_the_lib | -========================================== diff --git a/tests/cargo-kani/assess-artifacts/src/lib.rs b/tests/cargo-kani/assess-artifacts/src/lib.rs deleted file mode 100644 index 142287666db7..000000000000 --- a/tests/cargo-kani/assess-artifacts/src/lib.rs +++ /dev/null @@ -1,19 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -//! This test ensures: -//! 1. Assess is able to correctly build and report on a package -//! 2. Assess is able to correctly count the number of packages (1), -//! in the presence of an integration test (which might otherwise -//! look like two crates: 'assess-artifact' and 'integ') - -#[test] -fn an_unsupported_test_from_the_lib() { - // unsupported feature: try instrinsic - assert!(std::panic::catch_unwind(|| panic!("test")).is_err()); -} - -#[test] -fn a_supported_test_from_the_lib() { - assert!(1 == 1); -} diff --git a/tests/cargo-kani/assess-artifacts/tests/integ.rs b/tests/cargo-kani/assess-artifacts/tests/integ.rs deleted file mode 100644 index 368567eb20e4..000000000000 --- a/tests/cargo-kani/assess-artifacts/tests/integ.rs +++ /dev/null @@ -1,13 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -#[test] -fn an_unsupported_test_from_tests() { - // unsupported feature: try instrinsic - assert!(std::panic::catch_unwind(|| panic!("test")).is_err()); -} - -#[test] -fn a_supported_test_from_tests() { - assert!(1 == 1); -} diff --git a/tests/cargo-kani/assess-workspace-artifacts/Cargo.toml b/tests/cargo-kani/assess-workspace-artifacts/Cargo.toml deleted file mode 100644 index 1e041ae4734d..000000000000 --- a/tests/cargo-kani/assess-workspace-artifacts/Cargo.toml +++ /dev/null @@ -1,16 +0,0 @@ -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -[package] -name = "assess-artifacts" -version = "0.1.0" -edition = "2021" - -# See src/lib.rs for a comment on this tests's purpose - -[package.metadata.kani] -flags = { assess = true, workspace = true } -unstable = { unstable-options = true } - -[workspace] -members = ["subpackage"] diff --git a/tests/cargo-kani/assess-workspace-artifacts/expected b/tests/cargo-kani/assess-workspace-artifacts/expected deleted file mode 100644 index fba2cd94f212..000000000000 --- a/tests/cargo-kani/assess-workspace-artifacts/expected +++ /dev/null @@ -1,20 +0,0 @@ -Analyzed 2 packages -============================================ - Unsupported feature | Crates | Instances - | impacted | of use ----------------------+----------+----------- - catch_unwind | 2 | 3 -============================================ -========================================= - Reason for failure | Number of tests ------------------------+----------------- - unsupported_construct | 3 - none (success) | 3 -========================================= -================================================= - Candidate for proof harness | Location ---------------------------------------+---------- - a_supported_test_from_tests | - a_supported_test_from_the_lib | - a_supported_test_from_the_subpackage | -================================================== diff --git a/tests/cargo-kani/assess-workspace-artifacts/src/lib.rs b/tests/cargo-kani/assess-workspace-artifacts/src/lib.rs deleted file mode 100644 index de921fad22f5..000000000000 --- a/tests/cargo-kani/assess-workspace-artifacts/src/lib.rs +++ /dev/null @@ -1,20 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -//! This test ensures: -//! 1. Assess is able to correctly build and report on a _workspace_ -//! 2. Assess is able to correctly count the number of packages (2), -//! in the presence of an integration test (which might otherwise -//! look like three crates: -//! 'assess-artifact', 'subpackage', and 'integ') - -#[test] -fn an_unsupported_test_from_the_lib() { - // unsupported feature: try instrinsic - assert!(std::panic::catch_unwind(|| panic!("test")).is_err()); -} - -#[test] -fn a_supported_test_from_the_lib() { - assert!(1 == 1); -} diff --git a/tests/cargo-kani/assess-workspace-artifacts/subpackage/Cargo.toml b/tests/cargo-kani/assess-workspace-artifacts/subpackage/Cargo.toml deleted file mode 100644 index 06f3a7a21655..000000000000 --- a/tests/cargo-kani/assess-workspace-artifacts/subpackage/Cargo.toml +++ /dev/null @@ -1,9 +0,0 @@ -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -[package] -name = "subpackage" -version = "0.1.0" -edition = "2021" - -[dependencies] diff --git a/tests/cargo-kani/assess-workspace-artifacts/subpackage/src/lib.rs b/tests/cargo-kani/assess-workspace-artifacts/subpackage/src/lib.rs deleted file mode 100644 index dc91211887d9..000000000000 --- a/tests/cargo-kani/assess-workspace-artifacts/subpackage/src/lib.rs +++ /dev/null @@ -1,13 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -#[test] -fn an_unsupported_test_from_the_subpackage() { - // unsupported feature: try instrinsic - assert!(std::panic::catch_unwind(|| panic!("test")).is_err()); -} - -#[test] -fn a_supported_test_from_the_subpackage() { - assert!(1 == 1); -} diff --git a/tests/cargo-kani/assess-workspace-artifacts/tests/integ.rs b/tests/cargo-kani/assess-workspace-artifacts/tests/integ.rs deleted file mode 100644 index 368567eb20e4..000000000000 --- a/tests/cargo-kani/assess-workspace-artifacts/tests/integ.rs +++ /dev/null @@ -1,13 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -#[test] -fn an_unsupported_test_from_tests() { - // unsupported feature: try instrinsic - assert!(std::panic::catch_unwind(|| panic!("test")).is_err()); -} - -#[test] -fn a_supported_test_from_tests() { - assert!(1 == 1); -} diff --git a/tests/cargo-ui/assess-error/Cargo.toml b/tests/cargo-ui/assess-error/Cargo.toml deleted file mode 100644 index 9480d8519d57..000000000000 --- a/tests/cargo-ui/assess-error/Cargo.toml +++ /dev/null @@ -1,13 +0,0 @@ -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -[package] -name = "compilation-error" -version = "0.1.0" -edition = "2021" - -# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html - -[package.metadata.kani] -flags = { assess = true } -unstable = { unstable-options = true } diff --git a/tests/cargo-ui/assess-error/expected b/tests/cargo-ui/assess-error/expected deleted file mode 100644 index 213d811ae577..000000000000 --- a/tests/cargo-ui/assess-error/expected +++ /dev/null @@ -1,2 +0,0 @@ -error: Failed to compile lib `compilation_error` -error: Failed to assess project: Failed to build all targets diff --git a/tests/cargo-ui/assess-error/src/lib.rs b/tests/cargo-ui/assess-error/src/lib.rs deleted file mode 100644 index e37051854821..000000000000 --- a/tests/cargo-ui/assess-error/src/lib.rs +++ /dev/null @@ -1,19 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT -//! Check that the compilation error detection works as expected -use std::option; - -pub fn add(left: usize, right: u32) -> usize { - left + right -} - -#[cfg(test)] -mod tests { - use super::*; - - #[test] - fn it_works() { - let result = add(2, 2); - assert_eq!(result, 4); - } -}