-
Notifications
You must be signed in to change notification settings - Fork 89
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
List Subcommand (Implementation) (#3523)
Implementation of the list subcommand (and updates to the RFC). As a larger test, I ran on the standard library (`kani list -Z list -Z function-contracts -Z mem-predicates ./library --std`) and manually verified that the results were correct. I pasted the output below. Contracts: | | Function | Contract Harnesses (#[kani::proof_for_contract]) | | ----- | ------------------------------------------------ | ------------------------------------------------------ | | | alloc::layout::Layout::from_size_align_unchecked | alloc::layout::verify::check_from_size_align_unchecked | | | ascii::ascii_char::AsciiChar::from_u8 | ascii::ascii_char::verify::check_from_u8 | | | ascii::ascii_char::AsciiChar::from_u8_unchecked | ascii::ascii_char::verify::check_from_u8_unchecked | | | char::convert::from_u32_unchecked | char::convert::verify::check_from_u32_unchecked | | | char::methods::verify::as_ascii_clone | char::methods::verify::check_as_ascii_ascii_char | | | | char::methods::verify::check_as_ascii_non_ascii_char | | | intrinsics::typed_swap | intrinsics::verify::check_typed_swap_u8 | | | | intrinsics::verify::check_typed_swap_char | | | | intrinsics::verify::check_typed_swap_non_zero | | | mem::swap | mem::verify::check_swap_primitive | | | | mem::verify::check_swap_adt_no_drop | | | ptr::align_offset | ptr::verify::check_align_offset_zst | | | | ptr::verify::check_align_offset_u8 | | | | ptr::verify::check_align_offset_u16 | | | | ptr::verify::check_align_offset_u32 | | | | ptr::verify::check_align_offset_u64 | | | | ptr::verify::check_align_offset_u128 | | | | ptr::verify::check_align_offset_4096 | | | | ptr::verify::check_align_offset_5 | | | ptr::alignment::Alignment::as_nonzero | ptr::alignment::verify::check_as_nonzero | | | ptr::alignment::Alignment::as_usize | ptr::alignment::verify::check_as_usize | | | ptr::alignment::Alignment::log2 | ptr::alignment::verify::check_log2 | | | ptr::alignment::Alignment::mask | ptr::alignment::verify::check_mask | | | ptr::alignment::Alignment::new | ptr::alignment::verify::check_new | | | ptr::alignment::Alignment::new_unchecked | ptr::alignment::verify::check_new_unchecked | | | ptr::alignment::Alignment::of | ptr::alignment::verify::check_of_i32 | | | ptr::non_null::NonNull::<T>::new | ptr::non_null::verify::non_null_check_new | | | ptr::non_null::NonNull::<T>::new_unchecked | ptr::non_null::verify::non_null_check_new_unchecked | | | ptr::read_volatile | ptr::verify::check_read_u128 | | | ptr::unique::Unique::<T>::as_non_null_ptr | ptr::unique::verify::check_as_non_null_ptr | | | ptr::unique::Unique::<T>::as_ptr | ptr::unique::verify::check_as_ptr | | | ptr::unique::Unique::<T>::new | ptr::unique::verify::check_new | | | ptr::unique::Unique::<T>::new_unchecked | ptr::unique::verify::check_new_unchecked | | | ptr::verify::mod_inv_copy | ptr::verify::check_mod_inv | | | ptr::write_volatile | NONE | | Total | 24 | 34 | Standard Harnesses (#[kani::proof]): 1. ptr::unique::verify::check_as_mut 2. ptr::unique::verify::check_as_ref 3. ptr::unique::verify::check_cast Terminal view (`--pretty` format): <img alt="list" src="https://github.com/user-attachments/assets/ebaf22a0-853a-4c60-8308-b2eeebde5239"> By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Felipe R. Monteiro <[email protected]> Co-authored-by: Zyad Hassan <[email protected]>
- Loading branch information
3 people
authored
Oct 9, 2024
1 parent
c645752
commit 0400024
Showing
26 changed files
with
883 additions
and
63 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,127 @@ | ||
| // Copyright Kani Contributors | ||
| // SPDX-License-Identifier: Apache-2.0 OR MIT | ||
| //! Implements the subcommand handling of the list subcommand | ||
|
|
||
| use std::path::PathBuf; | ||
|
|
||
| use crate::args::ValidateArgs; | ||
| use clap::{Error, Parser, ValueEnum, error::ErrorKind}; | ||
| use kani_metadata::UnstableFeature; | ||
|
|
||
| use super::VerificationArgs; | ||
|
|
||
| /// List information relevant to verification | ||
| #[derive(Debug, Parser)] | ||
| pub struct CargoListArgs { | ||
| #[command(flatten)] | ||
| pub verify_opts: VerificationArgs, | ||
|
|
||
| /// Output format | ||
| #[clap(long, default_value = "pretty")] | ||
| pub format: Format, | ||
| } | ||
|
|
||
| /// List information relevant to verification | ||
| #[derive(Debug, Parser)] | ||
| pub struct StandaloneListArgs { | ||
| /// Rust file to verify | ||
| #[arg(required = true)] | ||
| pub input: PathBuf, | ||
|
|
||
| #[arg(long, hide = true)] | ||
| pub crate_name: Option<String>, | ||
|
|
||
| #[command(flatten)] | ||
| pub verify_opts: VerificationArgs, | ||
|
|
||
| /// Output format | ||
| #[clap(long, default_value = "pretty")] | ||
| pub format: Format, | ||
|
|
||
| /// Pass this flag to run the `list` command on the standard library. | ||
| /// Ensure that the provided `path` is the `library` folder. | ||
| #[arg(long)] | ||
| pub std: bool, | ||
| } | ||
|
|
||
| /// Message formats available for the subcommand. | ||
| #[derive(Copy, Clone, Debug, PartialEq, Eq, ValueEnum, strum_macros::Display)] | ||
| #[strum(serialize_all = "kebab-case")] | ||
| pub enum Format { | ||
| /// Print diagnostic messages in a user friendly format. | ||
| Pretty, | ||
| /// Print diagnostic messages in JSON format. | ||
| Json, | ||
| } | ||
|
|
||
| impl ValidateArgs for CargoListArgs { | ||
| fn validate(&self) -> Result<(), Error> { | ||
| self.verify_opts.validate()?; | ||
| if !self.verify_opts.common_args.unstable_features.contains(UnstableFeature::List) { | ||
| return Err(Error::raw( | ||
| ErrorKind::MissingRequiredArgument, | ||
| "The `list` subcommand is unstable and requires -Z list", | ||
| )); | ||
| } | ||
|
|
||
| Ok(()) | ||
| } | ||
| } | ||
|
|
||
| impl ValidateArgs for StandaloneListArgs { | ||
| fn validate(&self) -> Result<(), Error> { | ||
| self.verify_opts.validate()?; | ||
| if !self.verify_opts.common_args.unstable_features.contains(UnstableFeature::List) { | ||
| return Err(Error::raw( | ||
| ErrorKind::MissingRequiredArgument, | ||
| "The `list` subcommand is unstable and requires -Z list", | ||
| )); | ||
| } | ||
|
|
||
| if self.std { | ||
| if !self.input.exists() { | ||
| Err(Error::raw( | ||
| ErrorKind::InvalidValue, | ||
| format!( | ||
| "Invalid argument: `<input>` argument `{}` does not exist", | ||
| self.input.display() | ||
| ), | ||
| )) | ||
| } else if !self.input.is_dir() { | ||
| Err(Error::raw( | ||
| ErrorKind::InvalidValue, | ||
| format!( | ||
| "Invalid argument: `<input>` argument `{}` is not a directory", | ||
| self.input.display() | ||
| ), | ||
| )) | ||
| } else { | ||
| let full_path = self.input.canonicalize()?; | ||
| let dir = full_path.file_stem().unwrap(); | ||
| if dir != "library" { | ||
| Err(Error::raw( | ||
| ErrorKind::InvalidValue, | ||
| format!( | ||
| "Invalid argument: Expected `<input>` to point to the `library` folder \ | ||
| containing the standard library crates.\n\ | ||
| Found `{}` folder instead", | ||
| dir.to_string_lossy() | ||
| ), | ||
| )) | ||
| } else { | ||
| Ok(()) | ||
| } | ||
| } | ||
| } else if self.input.is_file() { | ||
| Ok(()) | ||
| } else { | ||
| Err(Error::raw( | ||
| ErrorKind::InvalidValue, | ||
| format!( | ||
| "Invalid argument: Input invalid. `{}` is not a regular file.", | ||
| self.input.display() | ||
| ), | ||
| )) | ||
| } | ||
| } | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.