diff --git a/Cargo.toml b/Cargo.toml index 54fb5c04abaa..c36151fc2f8d 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -65,4 +65,5 @@ exclude = [ "tests/perf", "tests/cargo-ui", "tests/slow", + "tests/assess-scan-test-scaffold", ] diff --git a/docs/src/SUMMARY.md b/docs/src/SUMMARY.md index 854b7d628d02..60df0b0faa31 100644 --- a/docs/src/SUMMARY.md +++ b/docs/src/SUMMARY.md @@ -23,6 +23,7 @@ - [Working with CBMC](./cbmc-hacks.md) - [Working with `rustc`](./rustc-hacks.md) - [Command cheat sheets](./cheat-sheets.md) + - [cargo kani assess](./dev-assess.md) - [Testing](./testing.md) - [Regression testing](./regression-testing.md) - [Book runner](./bookrunner.md) diff --git a/docs/src/dev-assess.md b/docs/src/dev-assess.md new file mode 100644 index 000000000000..8f79351d3a9c --- /dev/null +++ b/docs/src/dev-assess.md @@ -0,0 +1,185 @@ +# `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/kani-driver/src/args.rs b/kani-driver/src/args.rs index 65b4945b86cc..0292898eb5f8 100644 --- a/kani-driver/src/args.rs +++ b/kani-driver/src/args.rs @@ -45,7 +45,7 @@ pub struct CargoKaniArgs { #[derive(Debug, Parser)] pub enum CargoKaniSubcommand { #[command(hide = true)] - Assess, + Assess(crate::assess::AssessArgs), } // Common arguments for invoking Kani. This gets put into KaniContext, whereas @@ -396,7 +396,7 @@ impl CargoKaniArgs { pub fn validate(&self) { self.common_opts.validate::(); // --assess requires --enable-unstable, but the subcommand needs manual checking - if (matches!(self.command, Some(CargoKaniSubcommand::Assess)) || self.common_opts.assess) + if (matches!(self.command, Some(CargoKaniSubcommand::Assess(_))) || self.common_opts.assess) && !self.common_opts.enable_unstable { Self::command() @@ -519,6 +519,22 @@ mod tests { StandaloneArgs::parse_from(vec!["kani", "file.rs", "--enable-unstable", "--cbmc-args"]); // no assertion: the above might fail if it fails to allow 0 args to cbmc-args } + #[test] + fn check_multiple_packages() { + // accepts repeated: + let a = CargoKaniArgs::parse_from(vec!["cargo-kani", "-p", "a", "-p", "b"]); + assert_eq!(a.common_opts.package, vec!["a".to_owned(), "b".to_owned()]); + let b = CargoKaniArgs::try_parse_from(vec![ + "cargo-kani", + "-p", + "a", // no -p + "b", + ]); + // BUG: should not accept sequential: + // Related: https://github.com/model-checking/kani/issues/2025 + // Currently asserting this backwards from how it should be! + assert!(!b.is_err()); + } fn check(args: &str, require_unstable: bool, pred: fn(StandaloneArgs) -> bool) { let mut res = parse_unstable_disabled(&args); diff --git a/kani-driver/src/assess/args.rs b/kani-driver/src/assess/args.rs new file mode 100644 index 000000000000..38143c992a08 --- /dev/null +++ b/kani-driver/src/assess/args.rs @@ -0,0 +1,42 @@ +// 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 { + /// 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/assess/metadata.rs b/kani-driver/src/assess/metadata.rs new file mode 100644 index 000000000000..ab43e6d1fd47 --- /dev/null +++ b/kani-driver/src/assess/metadata.rs @@ -0,0 +1,92 @@ +// 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::table_builder::TableBuilder; +use super::table_failure_reasons::FailureReasonsTableRow; +use super::table_promising_tests::PromisingTestsTableRow; +use super::table_unsupported_features::UnsupportedFeaturesTableRow; +use super::AssessArgs; + +/// 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 { + /// 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, +} + +/// If given the argument to so do, write the assess metadata to the target file. +pub(crate) fn write_metadata(args: &AssessArgs, build: 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, &build)?; + } + Ok(()) +} + +/// Write metadata with unsupported features only, supporting the `--only-codegen` option. +pub(crate) fn write_partial_metadata( + args: &AssessArgs, + unsupported_features: TableBuilder, +) -> Result<()> { + write_metadata( + args, + AssessMetadata { + unsupported_features, + failure_reasons: TableBuilder::new(), + promising_tests: TableBuilder::new(), + }, + ) +} + +/// 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 { + unsupported_features: TableBuilder::new(), + failure_reasons: TableBuilder::new(), + promising_tests: TableBuilder::new(), + }; + 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 index d135a998b7a9..1674fc8cdb27 100644 --- a/kani-driver/src/assess/mod.rs +++ b/kani-driver/src/assess/mod.rs @@ -8,13 +8,28 @@ use crate::metadata::merge_kani_metadata; use crate::project; use crate::session::KaniSession; +pub use self::args::AssessArgs; + +mod args; +mod metadata; +mod scan; mod table_builder; mod table_failure_reasons; mod table_promising_tests; mod table_unsupported_features; -pub(crate) fn cargokani_assess_main(mut session: KaniSession) -> Result<()> { - // fix some settings +/// `cargo kani assess` main entry point. +/// +/// See +pub(crate) fn cargokani_assess_main(mut session: KaniSession, args: AssessArgs) -> Result<()> { + if let Some(args::AssessSubcommand::Scan(args)) = &args.command { + return scan::assess_scan_main(session, args); + } + + // 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(1); session.args.tests = true; session.args.output_format = crate::args::OutputFormat::Terse; @@ -34,7 +49,7 @@ pub(crate) fn cargokani_assess_main(mut session: KaniSession) -> Result<()> { // we will at least continue to see everything. project.metadata.clone() } else { - reconstruct_metadata_structure(cargo_metadata, &project.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, @@ -46,13 +61,15 @@ pub(crate) fn cargokani_assess_main(mut session: KaniSession) -> Result<()> { println!("Found {} packages", packages_metadata.len()); let metadata = merge_kani_metadata(packages_metadata.clone()); + let unsupported_features = table_unsupported_features::build(&packages_metadata); if !metadata.unsupported_features.is_empty() { - println!("{}", table_unsupported_features::build(&packages_metadata)); + println!("{}", unsupported_features.render()); } else { println!("No crates contained Rust features unsupported by Kani"); } if session.args.only_codegen { + metadata::write_partial_metadata(&args, unsupported_features)?; return Ok(()); } @@ -66,7 +83,8 @@ pub(crate) fn cargokani_assess_main(mut session: KaniSession) -> Result<()> { // 1. "Reason for failure" will count reasons why harnesses did not succeed // e.g. successs 6 // unwind 234 - println!("{}", table_failure_reasons::build(&results)); + 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. @@ -74,45 +92,70 @@ pub(crate) fn cargokani_assess_main(mut session: KaniSession) -> Result<()> { // 2. "Test cases that might be good proof harness starting points" // e.g. All Successes and maybe Assertions? - println!("{}", table_promising_tests::build(&results)); + let promising_tests = table_promising_tests::build(&results); + println!("{}", promising_tests.render()); + + metadata::write_metadata( + &args, + metadata::AssessMetadata { unsupported_features, failure_reasons, promising_tests }, + )?; Ok(()) } /// 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 search = kani_metadata.to_owned(); - let mut results = vec![]; - for package in &cargo_metadata.packages { - let mut artifacts = vec![]; + let mut remaining_metas = kani_metadata.to_owned(); + let mut package_metas = vec![]; + for package in cargo_metadata.workspace_packages() { + if !session.args.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.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 + // 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) = search.iter().position(|x| x.crate_name == target_name) { - let md = search.swap_remove(i); - artifacts.push(md); + 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 {} in package {}", - target.name, package.name + "Didn't find metadata for target {} (kind {:?}) in package {}", + target.name, target.kind, package.name ) } } - let mut merged = crate::metadata::merge_kani_metadata(artifacts); + let mut merged = crate::metadata::merge_kani_metadata(package_artifacts); merged.crate_name = package.name.clone(); - results.push(merged); + package_metas.push(merged); } - if !search.is_empty() { - let search_names: Vec<_> = search.into_iter().map(|x| x.crate_name).collect(); - println!("Found remaining (unused) metadata after reconstruction: {search_names:?}"); + 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(results) + Ok(package_metas) } diff --git a/kani-driver/src/assess/scan.rs b/kani-driver/src/assess/scan.rs new file mode 100644 index 000000000000..cf13246ecf5d --- /dev/null +++ b/kani-driver/src/assess/scan.rs @@ -0,0 +1,203 @@ +// 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::process::Command; +use std::time::Instant; + +use anyhow::Result; + +use crate::session::KaniSession; + +use super::args::ScanArgs; +use super::metadata::{aggregate_metadata, read_metadata}; + +/// `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 { + if !filter.contains(&package.name) { + 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) + }; + + if result.is_err() { + println!("Failed: {name}"); + failed_packages.push(package); + } else { + let meta = read_metadata(&outfile); + if let Ok(meta) = meta { + success_metas.push(meta); + } else { + println!("Failed: {name}"); + failed_packages.push(package); + } + } + //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); + println!("{}", results.unsupported_features.render()); + 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 = Command::new("cargo"); + 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); + cmd.arg("--enable-unstable"); // This has to be after `-p` due to an argument parsing bug in kani-driver + 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) + } + } +} diff --git a/kani-driver/src/assess/table_builder.rs b/kani-driver/src/assess/table_builder.rs index 27e93946050f..58f426b6a742 100644 --- a/kani-driver/src/assess/table_builder.rs +++ b/kani-driver/src/assess/table_builder.rs @@ -22,13 +22,14 @@ //! 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. +//! 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`]. @@ -149,6 +150,39 @@ impl TableBuilder { } } +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::*; diff --git a/kani-driver/src/assess/table_failure_reasons.rs b/kani-driver/src/assess/table_failure_reasons.rs index 73ce1c6cb98a..d4bedca118d9 100644 --- a/kani-driver/src/assess/table_failure_reasons.rs +++ b/kani-driver/src/assess/table_failure_reasons.rs @@ -2,8 +2,9 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use std::cmp::Ordering; +use std::collections::HashSet; -use comfy_table::Table; +use serde::{Deserialize, Serialize}; use crate::harness_runner::HarnessResult; @@ -30,7 +31,7 @@ use super::table_builder::{ColumnType, RenderableTableRow, TableBuilder, TableRo /// assertion + overflow | 2 /// ================================================ /// ``` -pub(crate) fn build(results: &[HarnessResult]) -> Table { +pub(crate) fn build(results: &[HarnessResult]) -> TableBuilder { let mut builder = TableBuilder::new(); for r in results { @@ -44,16 +45,28 @@ pub(crate) fn build(results: &[HarnessResult]) -> Table { classes.join(" + ") }; - builder.add(FailureReasonsTableRow { reason: classification, count: 1 }); + 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.render() + builder } -#[derive(Default)] +/// 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, - pub count: usize, + /// Tests are identified by "pretty_name @ /full/path/file.rs:line" + pub tests: HashSet, } impl TableRow for FailureReasonsTableRow { @@ -64,11 +77,15 @@ impl TableRow for FailureReasonsTableRow { } fn merge(&mut self, new: Self) { - self.count += new.count; + self.tests.extend(new.tests); } fn compare(&self, right: &Self) -> Ordering { - self.count.cmp(&right.count).reverse().then_with(|| self.reason.cmp(&right.reason)) + self.tests + .len() + .cmp(&right.tests.len()) + .reverse() + .then_with(|| self.reason.cmp(&right.reason)) } } @@ -82,7 +99,7 @@ impl RenderableTableRow for FailureReasonsTableRow { } fn row(&self) -> Vec { - vec![self.reason.clone(), self.count.to_string()] + vec![self.reason.clone(), self.tests.len().to_string()] } } diff --git a/kani-driver/src/assess/table_promising_tests.rs b/kani-driver/src/assess/table_promising_tests.rs index 9e1995fde618..7fd46fc9e7c8 100644 --- a/kani-driver/src/assess/table_promising_tests.rs +++ b/kani-driver/src/assess/table_promising_tests.rs @@ -3,7 +3,7 @@ use std::cmp::Ordering; -use comfy_table::Table; +use serde::{Deserialize, Serialize}; use crate::harness_runner::HarnessResult; @@ -26,7 +26,7 @@ use super::table_builder::{ColumnType, RenderableTableRow, TableBuilder, TableRo /// other::tests::test_misc | src/other.rs:284 /// ============================================================================= /// ``` -pub(crate) fn build(results: &[HarnessResult]) -> Table { +pub(crate) fn build(results: &[HarnessResult]) -> TableBuilder { let mut builder = TableBuilder::new(); for r in results { @@ -44,12 +44,17 @@ pub(crate) fn build(results: &[HarnessResult]) -> Table { } } - builder.render() + builder } -#[derive(Default)] +/// 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, } diff --git a/kani-driver/src/assess/table_unsupported_features.rs b/kani-driver/src/assess/table_unsupported_features.rs index e1640e553ec9..6466ca434bed 100644 --- a/kani-driver/src/assess/table_unsupported_features.rs +++ b/kani-driver/src/assess/table_unsupported_features.rs @@ -3,8 +3,8 @@ use std::{cmp::Ordering, collections::HashSet}; -use comfy_table::Table; use kani_metadata::KaniMetadata; +use serde::{Deserialize, Serialize}; use super::table_builder::{ColumnType, RenderableTableRow, TableBuilder, TableRow}; @@ -24,7 +24,7 @@ use super::table_builder::{ColumnType, RenderableTableRow, TableBuilder, TableRo /// drop_in_place | 2 | 2 /// =================================================== /// ``` -pub(crate) fn build(metadata: &[KaniMetadata]) -> Table { +pub(crate) fn build(metadata: &[KaniMetadata]) -> TableBuilder { let mut builder = TableBuilder::new(); for package_metadata in metadata { @@ -46,13 +46,19 @@ pub(crate) fn build(metadata: &[KaniMetadata]) -> Table { } } - builder.render() + builder } -#[derive(Default)] +/// 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, } diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index 47d7c777f1b1..acd7c795196b 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -53,9 +53,10 @@ fn cargokani_main(input_args: Vec) -> Result<()> { args.validate(); let session = session::KaniSession::new(args.common_opts)?; - if matches!(args.command, Some(CargoKaniSubcommand::Assess)) || session.args.assess { - // Run cargo assess. - return assess::cargokani_assess_main(session); + if let Some(CargoKaniSubcommand::Assess(args)) = args.command { + return assess::cargokani_assess_main(session, args); + } else if session.args.assess { + return assess::cargokani_assess_main(session, assess::AssessArgs::default()); } let project = project::cargo_project(&session)?; diff --git a/scripts/assess-scan-regression.sh b/scripts/assess-scan-regression.sh new file mode 100755 index 000000000000..14bf57d34c56 --- /dev/null +++ b/scripts/assess-scan-regression.sh @@ -0,0 +1,34 @@ +#!/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 --enable-unstable assess scan + +# Clean up +(cd foo && cargo clean) +(cd bar && cargo clean) + +# Check for expected files (and clean up) +EXPECTED_FILES=( + bar/bar.kani-assess-metadata.json + foo/foo.kani-assess-metadata.json + bar/bar.kani-assess.log + foo/foo.kani-assess.log +) +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 + echo "Failed to find $file" && exit 1 + fi +done + +echo "Done with assess scan test" diff --git a/scripts/exps/assess-scan-on-repos.sh b/scripts/exps/assess-scan-on-repos.sh new file mode 100755 index 000000000000..b80673ff3d1f --- /dev/null +++ b/scripts/exps/assess-scan-on-repos.sh @@ -0,0 +1,62 @@ +#!/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 + +echo "Starting assess scan..." + +cargo kani --only-codegen --enable-unstable 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 5253d54501ea..d948e47ca19e 100755 --- a/scripts/kani-regression.sh +++ b/scripts/kani-regression.sh @@ -94,7 +94,11 @@ fi # Check codegen of firecracker time "$SCRIPT_DIR"/codegen-firecracker.sh +# Test run 'cargo kani assess scan' +"$SCRIPT_DIR"/assess-scan-regression.sh + # Check that documentation compiles. +echo "Starting doc tests:" cargo doc --workspace --no-deps --exclude std echo diff --git a/tests/assess-scan-test-scaffold/README.md b/tests/assess-scan-test-scaffold/README.md new file mode 100644 index 000000000000..42c087647cb5 --- /dev/null +++ b/tests/assess-scan-test-scaffold/README.md @@ -0,0 +1,9 @@ +# 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 new file mode 100644 index 000000000000..fa4e4da798b0 --- /dev/null +++ b/tests/assess-scan-test-scaffold/bar/Cargo.toml @@ -0,0 +1,7 @@ +# 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 new file mode 100644 index 000000000000..6581fe81c0c2 --- /dev/null +++ b/tests/assess-scan-test-scaffold/bar/src/lib.rs @@ -0,0 +1,13 @@ +// 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/foo/Cargo.toml b/tests/assess-scan-test-scaffold/foo/Cargo.toml new file mode 100644 index 000000000000..bbf5539c5dd5 --- /dev/null +++ b/tests/assess-scan-test-scaffold/foo/Cargo.toml @@ -0,0 +1,7 @@ +# 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 new file mode 100644 index 000000000000..dbbfe74a4001 --- /dev/null +++ b/tests/assess-scan-test-scaffold/foo/src/lib.rs @@ -0,0 +1,13 @@ +// 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/remote-target-lists/top-100-crate-names-2022-12-26.txt b/tests/remote-target-lists/top-100-crate-names-2022-12-26.txt new file mode 100644 index 000000000000..4554e97d9ace --- /dev/null +++ b/tests/remote-target-lists/top-100-crate-names-2022-12-26.txt @@ -0,0 +1,100 @@ +aho-corasick +ansi_term +anyhow +arrayvec +atty +autocfg +base64 +bitflags +block-buffer +byteorder +bytes +cc +cfg-if +chrono +clap +crossbeam-channel +crossbeam-epoch +crossbeam-utils +digest +either +env_logger +fnv +futures +futures-channel +futures-core +futures-io +futures-sink +futures-task +futures-util +generic-array +getrandom +hashbrown +heck +http +httparse +hyper +idna +indexmap +itertools +itoa +lazy_static +libc +lock_api +log +matches +memchr +memoffset +miniz_oxide +mio +nom +num-integer +num-traits +num_cpus +once_cell +opaque-debug +parking_lot +parking_lot_core +percent-encoding +pin-project-lite +pkg-config +ppv-lite86 +proc-macro2 +quote +rand +rand_chacha +rand_core +regex +regex-syntax +rustc_version +ryu +scopeguard +semver +serde +serde_derive +serde_json +sha2 +slab +smallvec +socket2 +strsim +syn +termcolor +textwrap +thiserror +thiserror-impl +thread_local +time +tokio +tokio-util +toml +tracing +tracing-core +typenum +unicode-bidi +unicode-normalization +unicode-width +unicode-xid +url +version_check +winapi diff --git a/tests/remote-target-lists/top-100-crates-2022-12-26.txt b/tests/remote-target-lists/top-100-crates-2022-12-26.txt new file mode 100644 index 000000000000..bbfe086f3d77 --- /dev/null +++ b/tests/remote-target-lists/top-100-crates-2022-12-26.txt @@ -0,0 +1,80 @@ +https://github.com/Amanieu/parking_lot +https://github.com/Amanieu/thread_local-rs +https://github.com/BurntSushi/aho-corasick +https://github.com/BurntSushi/byteorder +https://github.com/BurntSushi/memchr +https://github.com/BurntSushi/termcolor +https://github.com/Frommi/miniz_oxide +https://github.com/Geal/nom +https://github.com/Gilnaa/memoffset +https://github.com/Kimundi/rustc-version-rs +https://github.com/RustCrypto/hashes +https://github.com/RustCrypto/traits +https://github.com/RustCrypto/utils +https://github.com/SergioBenitez/version_check +https://github.com/SimonSapin/rust-std-candidates +https://github.com/alexcrichton/cfg-if +https://github.com/bitflags/bitflags +https://github.com/bluss/arrayvec +https://github.com/bluss/either +https://github.com/bluss/indexmap +https://github.com/bluss/scopeguard +https://github.com/chronotope/chrono +https://github.com/clap-rs/clap +https://github.com/crossbeam-rs/crossbeam +https://github.com/cryptocorrosion/cryptocorrosion +https://github.com/cuviper/autocfg +https://github.com/dguo/strsim-rs +https://github.com/dtolnay/anyhow +https://github.com/dtolnay/itoa +https://github.com/dtolnay/proc-macro2 +https://github.com/dtolnay/quote +https://github.com/dtolnay/ryu +https://github.com/dtolnay/semver +https://github.com/dtolnay/syn +https://github.com/dtolnay/thiserror +https://github.com/fizyk20/generic-array.git +https://github.com/hyperium/http +https://github.com/hyperium/hyper +https://github.com/marshallpierce/rust-base64 +https://github.com/matklad/once_cell +https://github.com/mgeisler/textwrap +https://github.com/ogham/rust-ansi-term +https://github.com/paholg/typenum +https://github.com/retep998/winapi-rs +https://github.com/rust-cli/env_logger +https://github.com/rust-itertools/itertools +https://github.com/rust-lang-nursery/lazy-static.rs +https://github.com/rust-lang/cc-rs +https://github.com/rust-lang/futures-rs +https://github.com/rust-lang/hashbrown +https://github.com/rust-lang/libc +https://github.com/rust-lang/log +https://github.com/rust-lang/pkg-config-rs +https://github.com/rust-lang/regex +https://github.com/rust-lang/socket2 +https://github.com/rust-num/num-integer +https://github.com/rust-num/num-traits +https://github.com/rust-random/getrandom +https://github.com/rust-random/rand +https://github.com/seanmonstar/httparse +https://github.com/seanmonstar/num_cpus +https://github.com/serde-rs/json +https://github.com/serde-rs/serde +https://github.com/servo/rust-fnv +https://github.com/servo/rust-smallvec +https://github.com/servo/rust-url +https://github.com/servo/unicode-bidi +https://github.com/softprops/atty +https://github.com/taiki-e/pin-project-lite +https://github.com/time-rs/time +https://github.com/tokio-rs/bytes +https://github.com/tokio-rs/mio +https://github.com/tokio-rs/slab +https://github.com/tokio-rs/tokio +https://github.com/tokio-rs/tracing +https://github.com/toml-rs/toml +https://github.com/unicode-rs/unicode-normalization +https://github.com/unicode-rs/unicode-width +https://github.com/unicode-rs/unicode-xid +https://github.com/withoutboats/heck