Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

List Subcommand (Implementation) #3523

Merged
merged 40 commits into from
Oct 9, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
40 commits
Select commit Hold shift + click to select a range
f54c0f3
standalone list command
carolynzech Sep 12, 2024
67ed073
more concise pretty output
carolynzech Sep 12, 2024
4ace776
json output
carolynzech Sep 12, 2024
b903473
use standalone project instead
carolynzech Sep 12, 2024
b412d06
clippy
carolynzech Sep 12, 2024
bc802a1
refactor
carolynzech Sep 12, 2024
bfd2684
cargo list
carolynzech Sep 12, 2024
8e4efc0
use CrateItems instead; refactor into kani-middle
carolynzech Sep 16, 2024
2e79fbc
add std flag
carolynzech Sep 16, 2024
b1c5a9e
output updates
carolynzech Sep 16, 2024
ced1dab
update RFC with implementation
carolynzech Sep 16, 2024
c98b0b0
nits
carolynzech Sep 17, 2024
b57e47d
add tests
carolynzech Sep 17, 2024
6a659d0
add modifies rationale to rfc
carolynzech Sep 17, 2024
d88a4aa
Merge branch 'main' into list-subcommand
carolynzech Sep 17, 2024
87328bc
copyrights
carolynzech Sep 17, 2024
0e14cd1
Merge branch 'list-subcommand' of github.com:carolynzech/kani into li…
carolynzech Sep 17, 2024
e41c2b6
kani-compiler is list-agnostic
carolynzech Sep 20, 2024
5d0edb8
check explicitly that fn resolves
carolynzech Sep 20, 2024
e5de12c
change tests to json; sort output
carolynzech Sep 26, 2024
7a52503
clippy
carolynzech Sep 26, 2024
552f339
Merge branch 'main' into list-subcommand
carolynzech Sep 27, 2024
7383445
clippy
carolynzech Sep 27, 2024
55c9937
revert unnecessary changes
carolynzech Sep 27, 2024
a85ec2c
update rfc
carolynzech Sep 27, 2024
76365a3
Merge branch 'main' into list-subcommand
carolynzech Sep 27, 2024
b5f48a1
update RFC status
carolynzech Oct 1, 2024
a2a5082
Merge branch 'main' into list-subcommand
carolynzech Oct 1, 2024
0854cb3
update Cargo.lock
carolynzech Oct 1, 2024
7faeb2a
remove cli-table dependency; print manually
carolynzech Oct 1, 2024
15dd78a
add Markdown explanation to RFc
carolynzech Oct 2, 2024
3f583d3
remove contracts count; reduce rfc detail
carolynzech Oct 2, 2024
9daa8ba
use StableDefId
carolynzech Oct 3, 2024
cfc1db3
Doc comments formatting
carolynzech Oct 4, 2024
3380cb8
PR feedback
carolynzech Oct 4, 2024
e3455c0
Apply RFC suggestions from code review
carolynzech Oct 7, 2024
2ad1360
Apply suggestions from code review
carolynzech Oct 7, 2024
1cc50a0
remove contracts count mention from RFC
carolynzech Oct 7, 2024
c2474e3
rfc nit
carolynzech Oct 7, 2024
5d536c1
Merge branch 'main' into list-subcommand
carolynzech Oct 9, 2024
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 11 additions & 0 deletions Cargo.lock
Original file line number Diff line number Diff line change
Expand Up @@ -306,6 +306,15 @@ dependencies = [
"windows-sys 0.48.0",
]

[[package]]
name = "colour"
version = "2.1.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "b536eebcabe54980476d120a182f7da2268fe02d22575cca99cee5fdda178280"
dependencies = [
"winapi",
]

[[package]]
name = "comfy-table"
version = "7.1.1"
Expand Down Expand Up @@ -767,6 +776,7 @@ dependencies = [
"anyhow",
"cargo_metadata",
"clap",
"colour",
"comfy-table",
"console",
"glob",
Expand Down Expand Up @@ -1419,6 +1429,7 @@ version = "1.0.128"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "6ff5456707a1de34e7e37f2a6fd3d3f808c318259cbd01ab6377795054b483d8"
dependencies = [
"indexmap",
"itoa",
"memchr",
"ryu",
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -20,9 +20,8 @@ use cbmc::RoundingMode;
use cbmc::goto_program::Location;
use cbmc::irep::goto_binary_serde::write_goto_binary_file;
use cbmc::{InternedString, MachineModel};
use kani_metadata::UnsupportedFeature;
use kani_metadata::artifact::convert_type;
use kani_metadata::{ArtifactType, HarnessMetadata, KaniMetadata};
use kani_metadata::{ArtifactType, HarnessMetadata, KaniMetadata, UnsupportedFeature};
use kani_metadata::{AssignsContract, CompilerArtifactStub};
use rustc_codegen_ssa::back::archive::{
ArArchiveBuilder, ArchiveBuilder, ArchiveBuilderBuilder, DEFAULT_OBJECT_READER,
Expand Down Expand Up @@ -643,6 +642,10 @@ impl GotoCodegenResults {
proof_harnesses: proofs,
unsupported_features,
test_harnesses: tests,
// We don't collect the contracts metadata because the FunctionWithContractPass
// removes any contracts logic for ReachabilityType::Test or ReachabilityType::PubFns,
// which are the two ReachabilityTypes under which the compiler calls this function.
contracted_functions: vec![],
}
}

Expand Down
7 changes: 4 additions & 3 deletions kani-compiler/src/kani_middle/codegen_units.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@

use crate::args::ReachabilityType;
use crate::kani_middle::attributes::is_proof_harness;
use crate::kani_middle::metadata::gen_proof_metadata;
use crate::kani_middle::metadata::{gen_contracts_metadata, gen_proof_metadata};
use crate::kani_middle::reachability::filter_crate_items;
use crate::kani_middle::resolve::expect_resolve_fn;
use crate::kani_middle::stubbing::{check_compatibility, harness_stub_map};
Expand Down Expand Up @@ -93,7 +93,7 @@ impl CodegenUnits {

/// Write compilation metadata into a file.
pub fn write_metadata(&self, queries: &QueryDb, tcx: TyCtxt) {
let metadata = self.generate_metadata();
let metadata = self.generate_metadata(tcx);
let outpath = metadata_output_path(tcx);
store_metadata(queries, &metadata, &outpath);
}
Expand All @@ -103,14 +103,15 @@ impl CodegenUnits {
}

/// Generate [KaniMetadata] for the target crate.
fn generate_metadata(&self) -> KaniMetadata {
fn generate_metadata(&self, tcx: TyCtxt) -> KaniMetadata {
let (proof_harnesses, test_harnesses) =
self.harness_info.values().cloned().partition(|md| md.attributes.is_proof_harness());
KaniMetadata {
crate_name: self.crate_info.name.clone(),
proof_harnesses,
unsupported_features: vec![],
test_harnesses,
contracted_functions: gen_contracts_metadata(tcx),
}
}
}
Expand Down
51 changes: 47 additions & 4 deletions kani-compiler/src/kani_middle/metadata.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,15 +3,16 @@
//! This module handles Kani metadata generation. For example, generating HarnessMetadata for a
//! given function.

use std::collections::HashMap;
use std::path::Path;

use crate::kani_middle::attributes::test_harness_name;
use crate::kani_middle::attributes::{KaniAttributes, test_harness_name};
use crate::kani_middle::{SourceLocation, stable_fn_def};
use kani_metadata::ContractedFunction;
use kani_metadata::{ArtifactType, HarnessAttributes, HarnessKind, HarnessMetadata};
use rustc_middle::ty::TyCtxt;
use stable_mir::CrateDef;
use stable_mir::mir::mono::Instance;

use super::{SourceLocation, attributes::KaniAttributes};
use stable_mir::{CrateDef, CrateItems, DefId};

/// Create the harness metadata for a proof harness for a given function.
pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) -> HarnessMetadata {
Expand Down Expand Up @@ -40,6 +41,48 @@ pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) ->
}
}

/// Collects contract and contract harness metadata.
///
/// For each function with contracts (or that is a target of a contract harness),
/// construct a `ContractedFunction` object for it.
pub fn gen_contracts_metadata(tcx: TyCtxt) -> Vec<ContractedFunction> {
// We work with `stable_mir::CrateItem` instead of `stable_mir::Instance` to include generic items
let crate_items: CrateItems = stable_mir::all_local_items();

let mut fn_to_data: HashMap<DefId, ContractedFunction> = HashMap::new();

for item in crate_items {
carolynzech marked this conversation as resolved.
Show resolved Hide resolved
let function = item.name();
let file = SourceLocation::new(item.span()).filename;
let attributes = KaniAttributes::for_def_id(tcx, item.def_id());

if attributes.has_contract() {
fn_to_data.insert(item.def_id(), ContractedFunction {
function,
file,
harnesses: vec![],
});
} else if let Some((target_name, internal_def_id, _)) =
attributes.interpret_for_contract_attribute()
{
let target_def_id = stable_fn_def(tcx, internal_def_id)
.expect("The target of a proof for contract should be a function definition")
.def_id();
if let Some(cf) = fn_to_data.get_mut(&target_def_id) {
cf.harnesses.push(function);
} else {
fn_to_data.insert(target_def_id, ContractedFunction {
function: target_name.to_string(),
file,
harnesses: vec![function],
});
}
}
}

fn_to_data.into_values().collect()
}

/// Create the harness metadata for a test description.
#[allow(dead_code)]
pub fn gen_test_metadata(
Expand Down
3 changes: 2 additions & 1 deletion kani-driver/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -18,8 +18,9 @@ anyhow = "1"
console = "0.15.1"
once_cell = "1.19.0"
serde = { version = "1", features = ["derive"] }
serde_json = "1"
serde_json = { version = "1", features = ["preserve_order"] }
clap = { version = "4.4.11", features = ["derive"] }
colour = "2.1.0"
glob = "0.3"
toml = "0.8"
regex = "1.6"
Expand Down
127 changes: 127 additions & 0 deletions kani-driver/src/args/list_args.rs
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()
),
))
}
}
}
8 changes: 8 additions & 0 deletions kani-driver/src/args/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@
pub mod assess_args;
pub mod cargo;
pub mod common;
pub mod list_args;
pub mod playback_args;
pub mod std_args;

Expand Down Expand Up @@ -94,6 +95,8 @@ pub enum StandaloneSubcommand {
Playback(Box<playback_args::KaniPlaybackArgs>),
/// Verify the rust standard library.
VerifyStd(Box<std_args::VerifyStdArgs>),
/// Execute the list subcommand
List(Box<list_args::StandaloneListArgs>),
}

#[derive(Debug, clap::Parser)]
Expand All @@ -119,6 +122,9 @@ pub enum CargoKaniSubcommand {

/// Execute concrete playback testcases of a local package.
Playback(Box<playback_args::CargoPlaybackArgs>),

/// List metadata relevant to verification, e.g., harnesses.
List(Box<list_args::CargoListArgs>),
}

// Common arguments for invoking Kani for verification purpose. This gets put into KaniContext,
Expand Down Expand Up @@ -421,6 +427,7 @@ impl ValidateArgs for StandaloneArgs {

match &self.command {
Some(StandaloneSubcommand::VerifyStd(args)) => args.validate()?,
Some(StandaloneSubcommand::List(args)) => args.validate()?,
// TODO: Invoke PlaybackArgs::validate()
None | Some(StandaloneSubcommand::Playback(..)) => {}
};
Expand Down Expand Up @@ -467,6 +474,7 @@ impl ValidateArgs for CargoKaniSubcommand {
// Assess doesn't implement validation yet.
CargoKaniSubcommand::Assess(_) => Ok(()),
CargoKaniSubcommand::Playback(playback) => playback.validate(),
CargoKaniSubcommand::List(list) => list.validate(),
}
}
}
Expand Down
Loading
Loading