Skip to content

Commit

Permalink
kani-compiler is list-agnostic
Browse files Browse the repository at this point in the history
  • Loading branch information
@carolynzech
carolynzech committed Sep 20, 2024
1 parent 0e14cd1 commit e41c2b6
Show file tree
Hide file tree
Showing 14 changed files with 145 additions and 122 deletions.
73 changes: 64 additions & 9 deletions Cargo.lock
View file
Original file line number Diff line number Diff line change
Expand Up @@ -176,7 +176,7 @@ dependencies = [
"heck",
"proc-macro2",
"quote",
"syn",
"syn 2.0.77",
]

[[package]]
Expand All @@ -185,12 +185,44 @@ version = "0.7.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "1462739cb27611015575c0c11df5df7601141071f07518d56fcc1be504cbec97"

[[package]]
name = "cli-table"
version = "0.4.9"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "b53f9241f288a7b12c56565f04aaeaeeab6b8923d42d99255d4ca428b4d97f89"
dependencies = [
"cli-table-derive",
"csv",
"termcolor",
"unicode-width",
]

[[package]]
name = "cli-table-derive"
version = "0.4.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "3e83a93253aaae7c74eb7428ce4faa6e219ba94886908048888701819f82fb94"
dependencies = [
"proc-macro2",
"quote",
"syn 1.0.109",
]

[[package]]
name = "colorchoice"
version = "1.0.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "d3fd119d74b830634cea2a0f58bbd0d54540518a14397557951e79340abc28c0"

[[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 @@ -483,7 +515,7 @@ dependencies = [
"shell-words",
"strum",
"strum_macros",
"syn",
"syn 2.0.77",
"tracing",
"tracing-subscriber",
"tracing-tree",
Expand All @@ -496,6 +528,8 @@ dependencies = [
"anyhow",
"cargo_metadata",
"clap",
"cli-table",
"colour",
"comfy-table",
"console",
"glob",
Expand Down Expand Up @@ -541,7 +575,7 @@ dependencies = [
"proc-macro-error2",
"proc-macro2",
"quote",
"syn",
"syn 2.0.77",
]

[[package]]
Expand Down Expand Up @@ -819,7 +853,7 @@ dependencies = [
"proc-macro-error-attr2",
"proc-macro2",
"quote",
"syn",
"syn 2.0.77",
]

[[package]]
Expand Down Expand Up @@ -1027,7 +1061,7 @@ checksum = "243902eda00fad750862fc144cea25caca5e20d615af0a81bee94ca738f1df1f"
dependencies = [
"proc-macro2",
"quote",
"syn",
"syn 2.0.77",
]

[[package]]
Expand All @@ -1036,6 +1070,7 @@ version = "1.0.128"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "6ff5456707a1de34e7e37f2a6fd3d3f808c318259cbd01ab6377795054b483d8"
dependencies = [
"indexmap",
"itoa",
"memchr",
"ryu",
Expand Down Expand Up @@ -1134,7 +1169,18 @@ dependencies = [
"proc-macro2",
"quote",
"rustversion",
"syn",
"syn 2.0.77",
]

[[package]]
name = "syn"
version = "1.0.109"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237"
dependencies = [
"proc-macro2",
"quote",
"unicode-ident",
]

[[package]]
Expand All @@ -1161,6 +1207,15 @@ dependencies = [
"windows-sys 0.59.0",
]

[[package]]
name = "termcolor"
version = "1.4.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "06794f8f6c5c898b3275aebefa6b8a1cb24cd2c6c79397ab15774837a0bc5755"
dependencies = [
"winapi-util",
]

[[package]]
name = "thiserror"
version = "1.0.63"
Expand All @@ -1178,7 +1233,7 @@ checksum = "a4558b58466b9ad7ca0f102865eccc95938dca1a74a856f2b57b6629050da261"
dependencies = [
"proc-macro2",
"quote",
"syn",
"syn 2.0.77",
]

[[package]]
Expand Down Expand Up @@ -1275,7 +1330,7 @@ checksum = "34704c8d6ebcbc939824180af020566b01a7c01f80641264eba0999f6c2b6be7"
dependencies = [
"proc-macro2",
"quote",
"syn",
"syn 2.0.77",
]

[[package]]
Expand Down Expand Up @@ -1562,5 +1617,5 @@ checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e"
dependencies = [
"proc-macro2",
"quote",
"syn",
"syn 2.0.77",
]
3 changes: 0 additions & 3 deletions kani-compiler/src/args.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,9 +47,6 @@ pub struct Arguments {
pub reachability_analysis: ReachabilityType,
#[clap(long = "enable-stubbing")]
pub stubbing_enabled: bool,
/// Option name used to tell the compiler to execute the list subcommand
#[clap(long = "list")]
pub list_enabled: bool,
/// Option name used to define unstable features.
#[clap(short = 'Z', long = "unstable")]
pub unstable_features: Vec<String>,
Expand Down
17 changes: 5 additions & 12 deletions kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -343,12 +343,8 @@ impl CodegenBackend for GotocCodegenBackend {
}
}
ReachabilityType::None => {
// If the list subcommand is enabled, record the necessary KaniMetadata.
if queries.args().list_enabled {
let mut units: CodegenUnits = CodegenUnits::new(&queries, tcx);
collect_contracted_fns(tcx, &mut units);
units.write_metadata(&queries, tcx);
}
let units = CodegenUnits::new(&queries, tcx);
units.write_metadata(&queries, tcx);
}
ReachabilityType::PubFns => {
let unit = CodegenUnit::default();
Expand Down Expand Up @@ -388,7 +384,7 @@ impl CodegenBackend for GotocCodegenBackend {
write_file(
&base_filename,
ArtifactType::Metadata,
&results.generate_metadata(),
&results.generate_metadata(tcx),
queries.args().output_pretty_json,
);
}
Expand Down Expand Up @@ -627,7 +623,7 @@ impl GotoCodegenResults {
}
}
/// Method that generates `KaniMetadata` from the given compilation results.
pub fn generate_metadata(&self) -> KaniMetadata {
pub fn generate_metadata(&self, tcx: TyCtxt) -> KaniMetadata {
// Maps the goto-context "unsupported features" data into the KaniMetadata "unsupported features" format.
// TODO: Do we really need different formats??
let unsupported_features = self
Expand Down Expand Up @@ -659,10 +655,7 @@ impl GotoCodegenResults {
proof_harnesses: proofs,
unsupported_features,
test_harnesses: tests,
// Just leave contracted_functions empty, since we don't use this field unless we're running the
// list subcommand and that uses CodegenUnits::generate_metadata instead.
// TODO: should we consolidate these generate_metadata functions?
contracted_functions: vec![],
contracted_functions: collect_contracted_fns(tcx),
}
}

Expand Down
13 changes: 3 additions & 10 deletions kani-compiler/src/kani_middle/attributes.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -477,7 +477,7 @@ impl<'tcx> KaniAttributes<'tcx> {
///
/// We only extract attributes for harnesses that are local to the current crate.
/// Note that all attributes should be valid by now.
pub fn harness_attributes(&self, is_list_enabled: bool) -> HarnessAttributes {
pub fn harness_attributes(&self) -> HarnessAttributes {
// Abort if not local.
if !self.item.is_local() {
panic!("Expected a local item, but got: {:?}", self.item);
Expand Down Expand Up @@ -505,7 +505,7 @@ impl<'tcx> KaniAttributes<'tcx> {
harness.unwind_value = parse_unwind(self.tcx, attributes[0])
}
KaniAttributeKind::Proof => { /* no-op */ }
KaniAttributeKind::ProofForContract => self.handle_proof_for_contract(&mut harness, is_list_enabled),
KaniAttributeKind::ProofForContract => self.handle_proof_for_contract(&mut harness),
KaniAttributeKind::StubVerified => self.handle_stub_verified(&mut harness),
KaniAttributeKind::Unstable => {
// Internal attribute which shouldn't exist here.
Expand All @@ -531,7 +531,7 @@ impl<'tcx> KaniAttributes<'tcx> {
})
}

fn handle_proof_for_contract(&self, harness: &mut HarnessAttributes, is_list_enabled: bool) {
fn handle_proof_for_contract(&self, harness: &mut HarnessAttributes) {
let dcx = self.tcx.dcx();
let (name, id, span) = match self.interpret_for_contract_attribute() {
None => return, // This error was already emitted
Expand All @@ -540,13 +540,6 @@ impl<'tcx> KaniAttributes<'tcx> {
assert!(matches!(
&harness.kind, HarnessKind::ProofForContract { target_fn }
if *target_fn == name.to_string()));

// Only emit an error if we are trying to actually verify the contract.
// (If we are running the list subcommand, we just report later that there are no contracts for this harness).
if is_list_enabled {
return;
}

if KaniAttributes::for_item(self.tcx, id).contract_attributes().is_none() {
dcx.struct_span_err(
span,
Expand Down
48 changes: 15 additions & 33 deletions kani-compiler/src/kani_middle/codegen_units.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,14 +9,13 @@

use crate::args::ReachabilityType;
use crate::kani_middle::attributes::is_proof_harness;
use crate::kani_middle::list::collect_contracted_fns;
use crate::kani_middle::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};
use crate::kani_queries::QueryDb;
use kani_metadata::{
ArtifactType, AssignsContract, ContractedFunction, HarnessKind, HarnessMetadata, KaniMetadata,
};
use kani_metadata::{ArtifactType, AssignsContract, HarnessKind, HarnessMetadata, KaniMetadata};
use rustc_hir::def_id::DefId;
use rustc_middle::ty::TyCtxt;
use rustc_session::config::OutputType;
Expand Down Expand Up @@ -48,7 +47,6 @@ pub struct CodegenUnits {
units: Vec<CodegenUnit>,
harness_info: HashMap<Harness, HarnessMetadata>,
crate_info: CrateInfo,
pub contracted_functions: Vec<ContractedFunction>,
}

#[derive(Clone, Default, Debug)]
Expand All @@ -60,46 +58,29 @@ pub struct CodegenUnit {
impl CodegenUnits {
pub fn new(queries: &QueryDb, tcx: TyCtxt) -> Self {
let crate_info = CrateInfo { name: stable_mir::local_crate().name.as_str().into() };

if queries.args().reachability_analysis != ReachabilityType::Harnesses
&& !queries.args().list_enabled
{
// Leave other reachability type handling as is for now.
return CodegenUnits {
units: vec![],
harness_info: HashMap::default(),
crate_info,
contracted_functions: vec![],
};
}

let base_filepath = tcx.output_filenames(()).path(OutputType::Object);
let base_filename = base_filepath.as_path();
let harnesses = filter_crate_items(tcx, |_, instance| is_proof_harness(tcx, instance));
let all_harnesses = harnesses
.into_iter()
.map(|harness| {
let metadata =
gen_proof_metadata(tcx, harness, &base_filename, queries.args().list_enabled);
let metadata = gen_proof_metadata(tcx, harness, &base_filename);
(harness, metadata)
})
.collect::<HashMap<_, _>>();
let mut units = vec![];

if queries.args().reachability_analysis == ReachabilityType::Harnesses {
// Even if no_stubs is empty we still need to store rustc metadata.
units = group_by_stubs(tcx, &all_harnesses);
let units = group_by_stubs(tcx, &all_harnesses);
validate_units(tcx, &units);
debug!(?units, "CodegenUnits::new");
}

tcx.dcx().abort_if_errors();

CodegenUnits {
units,
harness_info: all_harnesses,
crate_info,
contracted_functions: vec![],
CodegenUnits { units, harness_info: all_harnesses, crate_info }
} else {
// Only ReachabilityType::Harnesses uses harness_info directly,
// but we collect it for the other ReachabilityTypes so that we can write the metadata to a file.
// Then, if the user invokes the list subcommand after verification, the metadata will already be cached
// and we do not need to recompile.
CodegenUnits { units: vec![], harness_info: all_harnesses, crate_info }
}
}

Expand All @@ -116,7 +97,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 @@ -126,15 +107,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: self.contracted_functions.clone(),
contracted_functions: collect_contracted_fns(tcx),
}
}
}
Expand Down Expand Up @@ -237,6 +218,7 @@ fn validate_units(tcx: TyCtxt, units: &[CodegenUnit]) {
tcx.dcx().span_err(rustc_internal::internal(tcx, span), msg);
}
}
tcx.dcx().abort_if_errors();
}

/// Apply stub transitivity operations.
Expand Down
Loading

0 comments on commit e41c2b6

Please sign in to comment.