From e5de12cde4eba8f47755166d24e0f2c8067d8c67 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Thu, 26 Sep 2024 17:34:24 -0400 Subject: [PATCH] change tests to json; sort output --- .../compiler_interface.rs | 15 ++- .../src/kani_middle/codegen_units.rs | 5 +- kani-compiler/src/kani_middle/list.rs | 103 ------------------ kani-compiler/src/kani_middle/metadata.rs | 90 ++++++++++++++- kani-compiler/src/kani_middle/mod.rs | 1 - kani-driver/src/list/collect_metadata.rs | 19 ++-- kani-driver/src/list/output.rs | 17 ++- kani_metadata/src/lib.rs | 2 +- tests/script-based-pre/cargo_list/Cargo.toml | 2 +- tests/script-based-pre/cargo_list/config.yml | 2 +- .../cargo_list/list-pretty.expected | 36 ------ .../script-based-pre/cargo_list/list.expected | 57 ++++++++++ tests/script-based-pre/cargo_list/list.sh | 8 +- tests/script-based-pre/cargo_list/src/lib.rs | 32 ++---- tests/script-based-pre/kani_list/config.yml | 2 +- .../kani_list/list-pretty.expected | 36 ------ .../script-based-pre/kani_list/list.expected | 57 ++++++++++ tests/script-based-pre/kani_list/list.sh | 8 +- tests/script-based-pre/kani_list/src/lib.rs | 24 ++-- 19 files changed, 258 insertions(+), 258 deletions(-) delete mode 100644 kani-compiler/src/kani_middle/list.rs delete mode 100644 tests/script-based-pre/cargo_list/list-pretty.expected create mode 100644 tests/script-based-pre/cargo_list/list.expected delete mode 100644 tests/script-based-pre/kani_list/list-pretty.expected create mode 100644 tests/script-based-pre/kani_list/list.expected diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index e57baa35f860..bb82d6403627 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -9,7 +9,6 @@ use crate::kani_middle::analysis; use crate::kani_middle::attributes::{is_test_harness_description, KaniAttributes}; use crate::kani_middle::check_reachable_items; use crate::kani_middle::codegen_units::{CodegenUnit, CodegenUnits}; -use crate::kani_middle::list::collect_contracted_fns; use crate::kani_middle::metadata::gen_test_metadata; use crate::kani_middle::provide; use crate::kani_middle::reachability::{ @@ -342,10 +341,7 @@ impl CodegenBackend for GotocCodegenBackend { results.harnesses.push(metadata); } } - ReachabilityType::None => { - let units = CodegenUnits::new(&queries, tcx); - units.write_metadata(&queries, tcx); - } + ReachabilityType::None => {} ReachabilityType::PubFns => { let unit = CodegenUnit::default(); let transformer = BodyTransformation::new(&queries, tcx, &unit); @@ -384,7 +380,7 @@ impl CodegenBackend for GotocCodegenBackend { write_file( &base_filename, ArtifactType::Metadata, - &results.generate_metadata(tcx), + &results.generate_metadata(), queries.args().output_pretty_json, ); } @@ -623,7 +619,7 @@ impl GotoCodegenResults { } } /// Method that generates `KaniMetadata` from the given compilation results. - pub fn generate_metadata(&self, tcx: TyCtxt) -> KaniMetadata { + pub fn generate_metadata(&self) -> 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 @@ -655,7 +651,10 @@ impl GotoCodegenResults { proof_harnesses: proofs, unsupported_features, test_harnesses: tests, - contracted_functions: collect_contracted_fns(tcx), + // We don't collect the functions under contract because the logic assumes that, if contract attributes are present, + // they are well-formed, which Kani only checks if we run verification or the list subcommand (i.e., for ReachabilityType::Harnesses). + // In those cases, we use the CodegenUnits object to generate the metadata instead of this function. + contracted_functions: vec![], } } diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 36c3fbd28e3d..ce9fc7e0ed09 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -9,8 +9,7 @@ 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::metadata::{gen_proof_metadata, gen_contracts_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}; @@ -115,7 +114,7 @@ impl CodegenUnits { proof_harnesses, unsupported_features: vec![], test_harnesses, - contracted_functions: collect_contracted_fns(tcx), + contracted_functions: gen_contracts_metadata(tcx), } } } diff --git a/kani-compiler/src/kani_middle/list.rs b/kani-compiler/src/kani_middle/list.rs deleted file mode 100644 index 5d03bb86cb20..000000000000 --- a/kani-compiler/src/kani_middle/list.rs +++ /dev/null @@ -1,103 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -// Collects contract and contract harness metadata for the list subcommand. - -use std::collections::HashMap; - -use crate::kani_middle::attributes::{matches_diagnostic as matches_function, KaniAttributes}; -use crate::kani_middle::{find_closure_in_body, InternalDefId, SourceLocation}; -use kani_metadata::ContractedFunction; -use rustc_middle::ty::TyCtxt; -use rustc_smir::rustc_internal; -use stable_mir::mir::mono::Instance; -use stable_mir::mir::{Body, TerminatorKind}; -use stable_mir::ty::{RigidTy, TyKind}; -use stable_mir::{CrateDef, CrateItems}; - -/// Map each function to its contract harnesses -/// `fns` includes all functions with contracts and all functions that are targets of a contract harness. -fn fns_to_harnesses(tcx: TyCtxt) -> HashMap> { - // 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 fns_to_harnesses: HashMap> = HashMap::new(); - - for item in crate_items { - let def_id = rustc_internal::internal(tcx, item.def_id()); - let fn_name = tcx.def_path_str(def_id); - let attributes = KaniAttributes::for_item(tcx, def_id); - - if attributes.has_contract() { - fns_to_harnesses.insert(def_id, vec![]); - } else if let Some((_, target_def_id, _)) = attributes.interpret_for_contract_attribute() { - if let Some(harnesses) = fns_to_harnesses.get_mut(&target_def_id) { - harnesses.push(fn_name); - } else { - fns_to_harnesses.insert(target_def_id, vec![fn_name]); - } - } - } - - fns_to_harnesses -} - -/// Count the number of contracts in `check_body`, where `check_body` is the body of the -/// kanitool::checked_with closure (c.f. kani_macros::sysroot::contracts). -/// In this closure, preconditions are denoted by kani::assume() calls and postconditions by kani::assert() calls. -/// The number of contracts is the number of times these functions are called inside the closure -fn count_contracts(tcx: TyCtxt, check_body: &Body) -> usize { - let mut count = 0; - - for bb in &check_body.blocks { - if let TerminatorKind::Call { ref func, .. } = bb.terminator.kind { - let fn_ty = func.ty(check_body.locals()).unwrap(); - if let TyKind::RigidTy(RigidTy::FnDef(fn_def, args)) = fn_ty.kind() { - if let Ok(instance) = Instance::resolve(fn_def, &args) { - // For each precondition or postcondition, increment the count - if matches_function(tcx, instance.def, "KaniAssume") - || matches_function(tcx, instance.def, "KaniAssert") - { - count += 1; - } - } - } - } - } - count -} - -/// For each function with contracts (or that is a target of a contract harness), -/// construct a ContractedFunction object for it and store it in `units`. -pub fn collect_contracted_fns(tcx: TyCtxt) -> Vec { - let mut contracted_fns = vec![]; - for (fn_def_id, harnesses) in fns_to_harnesses(tcx) { - let attrs = KaniAttributes::for_item(tcx, fn_def_id); - - // It's possible that a function is a target of a proof for contract but does not actually have contracts. - // If the function does have contracts, count them. - let total_contracts = if attrs.has_contract() { - let contract_attrs = - KaniAttributes::for_item(tcx, fn_def_id).contract_attributes().unwrap(); - let body: Body = rustc_internal::stable(tcx.optimized_mir(fn_def_id)); - let check_body: Body = - find_closure_in_body(&body, contract_attrs.checked_with.as_str()) - .unwrap() - .body() - .unwrap(); - - count_contracts(tcx, &check_body) - } else { - 0 - }; - - contracted_fns.push(ContractedFunction { - function: tcx.def_path_str(fn_def_id), - file: SourceLocation::new(rustc_internal::stable(tcx.def_span(fn_def_id))).filename, - harnesses, - total_contracts, - }); - } - - contracted_fns -} diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs index 40686362cbca..30b9851ec1af 100644 --- a/kani-compiler/src/kani_middle/metadata.rs +++ b/kani-compiler/src/kani_middle/metadata.rs @@ -3,15 +3,22 @@ //! 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::{ + matches_diagnostic as matches_function, ContractAttributes, KaniAttributes, +}; +use crate::kani_middle::{find_closure_in_body, InternalDefId, SourceLocation}; +use kani_metadata::ContractedFunction; use kani_metadata::{ArtifactType, HarnessAttributes, HarnessKind, HarnessMetadata}; use rustc_middle::ty::TyCtxt; +use rustc_smir::rustc_internal; use stable_mir::mir::mono::Instance; -use stable_mir::CrateDef; - -use super::{attributes::KaniAttributes, SourceLocation}; +use stable_mir::mir::{Body, TerminatorKind}; +use stable_mir::ty::{RigidTy, TyKind}; +use stable_mir::{CrateDef, CrateItems}; pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) -> HarnessMetadata { let def = instance.def; @@ -39,6 +46,83 @@ pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) -> } } +/// Map each function under contract to its contract harnesses +fn fns_to_contract_harnesses(tcx: TyCtxt) -> HashMap> { + // 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 fns_to_harnesses: HashMap> = HashMap::new(); + + for item in crate_items { + let def_id = rustc_internal::internal(tcx, item.def_id()); + let fn_name = tcx.def_path_str(def_id); + let attributes = KaniAttributes::for_item(tcx, def_id); + + if attributes.has_contract() { + fns_to_harnesses.insert(def_id, vec![]); + } else if let Some((_, target_def_id, _)) = attributes.interpret_for_contract_attribute() { + if let Some(harnesses) = fns_to_harnesses.get_mut(&target_def_id) { + harnesses.push(fn_name); + } else { + fns_to_harnesses.insert(target_def_id, vec![fn_name]); + } + } + } + + fns_to_harnesses +} + +/// Count the number of contracts in `check_body`, where `check_body` is the body of the +/// kanitool::checked_with closure (c.f. kani_macros::sysroot::contracts). +/// In this closure, preconditions are denoted by kani::assume() calls and postconditions by kani::assert() calls. +/// The number of contracts is the number of times these functions are called inside the closure +fn count_contracts(tcx: TyCtxt, check_body: &Body) -> usize { + let mut count = 0; + + for bb in &check_body.blocks { + if let TerminatorKind::Call { ref func, .. } = bb.terminator.kind { + let fn_ty = func.ty(check_body.locals()).unwrap(); + if let TyKind::RigidTy(RigidTy::FnDef(fn_def, args)) = fn_ty.kind() { + if let Ok(instance) = Instance::resolve(fn_def, &args) { + // For each precondition or postcondition, increment the count + if matches_function(tcx, instance.def, "KaniAssume") + || matches_function(tcx, instance.def, "KaniAssert") + { + count += 1; + } + } + } + } + } + count +} + +/// 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 { + let mut contracted_fns = vec![]; + for (fn_def_id, harnesses) in fns_to_contract_harnesses(tcx) { + let attrs: ContractAttributes = + KaniAttributes::for_item(tcx, fn_def_id).contract_attributes().unwrap(); + let body: Body = rustc_internal::stable(tcx.optimized_mir(fn_def_id)); + let check_body: Body = + find_closure_in_body(&body, attrs.checked_with.as_str()).unwrap().body().unwrap(); + + let total_contracts = count_contracts(tcx, &check_body); + + contracted_fns.push(ContractedFunction { + function: tcx.def_path_str(fn_def_id), + file: SourceLocation::new(rustc_internal::stable(tcx.def_span(fn_def_id))).filename, + harnesses, + total_contracts, + }); + } + + contracted_fns +} + /// Create the harness metadata for a test description. #[allow(dead_code)] pub fn gen_test_metadata( diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 0d99ba08ce85..ec16b4cd9449 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -32,7 +32,6 @@ pub mod attributes; pub mod codegen_units; pub mod coercion; mod intrinsics; -pub mod list; pub mod metadata; pub mod points_to; pub mod provide; diff --git a/kani-driver/src/list/collect_metadata.rs b/kani-driver/src/list/collect_metadata.rs index 028adec68444..d74cf60d71e0 100644 --- a/kani-driver/src/list/collect_metadata.rs +++ b/kani-driver/src/list/collect_metadata.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // This module invokes the compiler to gather the metadata for the list subcommand, then post-processes the output. -use std::collections::BTreeMap; +use std::collections::{BTreeMap, BTreeSet}; use crate::{ args::list_args::{CargoListArgs, Format, StandaloneListArgs}, @@ -18,9 +18,9 @@ use kani_metadata::{ContractedFunction, HarnessKind, KaniMetadata}; fn process_metadata(metadata: Vec, format: Format) -> Result<()> { // Map each file to a vector of its harnesses - let mut standard_harnesses: BTreeMap> = BTreeMap::new(); - let mut contract_harnesses: BTreeMap> = BTreeMap::new(); - let mut contracted_functions: Vec = vec![]; + let mut standard_harnesses: BTreeMap> = BTreeMap::new(); + let mut contract_harnesses: BTreeMap> = BTreeMap::new(); + let mut contracted_functions: BTreeSet = BTreeSet::new(); let mut total_standard_harnesses = 0; let mut total_contract_harnesses = 0; @@ -33,20 +33,20 @@ fn process_metadata(metadata: Vec, format: Format) -> Result<()> { total_standard_harnesses += 1; if let Some(harnesses) = standard_harnesses.get_mut(&harness_meta.original_file) { - harnesses.push(harness_meta.pretty_name); + harnesses.insert(harness_meta.pretty_name); } else { standard_harnesses - .insert(harness_meta.original_file, vec![harness_meta.pretty_name]); + .insert(harness_meta.original_file, BTreeSet::from([harness_meta.pretty_name])); } } HarnessKind::ProofForContract { .. } => { total_contract_harnesses += 1; if let Some(harnesses) = contract_harnesses.get_mut(&harness_meta.original_file) { - harnesses.push(harness_meta.pretty_name); + harnesses.insert(harness_meta.pretty_name); } else { contract_harnesses - .insert(harness_meta.original_file, vec![harness_meta.pretty_name]); + .insert(harness_meta.original_file, BTreeSet::from([harness_meta.pretty_name])); } } HarnessKind::Test => {} @@ -60,9 +60,6 @@ fn process_metadata(metadata: Vec, format: Format) -> Result<()> { contracted_functions.extend(kani_meta.contracted_functions.into_iter()); } - // Print in alphabetical order - contracted_functions.sort_by_key(|cf| cf.function.clone()); - let totals = Totals { standard_harnesses: total_standard_harnesses, contract_harnesses: total_contract_harnesses, diff --git a/kani-driver/src/list/output.rs b/kani-driver/src/list/output.rs index 80f134ee5dbf..d71b69bf7422 100644 --- a/kani-driver/src/list/output.rs +++ b/kani-driver/src/list/output.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // This module handles outputting the result for the list subcommand -use std::{collections::BTreeMap, fs::File, io::BufWriter}; +use std::{collections::{BTreeMap, BTreeSet}, fs::File, io::BufWriter}; use crate::{list::Totals, version::KANI_VERSION}; use anyhow::Result; @@ -14,10 +14,11 @@ use serde_json::json; // Represents the version of our JSON file format. // Increment this version (according to semantic versioning rules) whenever the JSON output format changes. const FILE_VERSION: &str = "0.1"; +const JSON_FILENAME: &str = "kani-list.json"; pub fn pretty( - standard_harnesses: BTreeMap>, - contracted_functions: Vec, + standard_harnesses: BTreeMap>, + contracted_functions: BTreeSet, totals: Totals, ) -> Result<()> { fn format_contract_harnesses(harnesses: &mut [String]) -> String { @@ -80,14 +81,12 @@ pub fn pretty( } pub fn json( - standard_harnesses: BTreeMap>, - contract_harnesses: BTreeMap>, - contracted_functions: Vec, + standard_harnesses: BTreeMap>, + contract_harnesses: BTreeMap>, + contracted_functions: BTreeSet, totals: Totals, ) -> Result<()> { - let filename = "kani-list.json"; - - let out_file = File::create(filename).unwrap(); + let out_file = File::create(JSON_FILENAME).unwrap(); let writer = BufWriter::new(out_file); let json_obj = json!({ diff --git a/kani_metadata/src/lib.rs b/kani_metadata/src/lib.rs index 0a7229d18635..3906b41ff89e 100644 --- a/kani_metadata/src/lib.rs +++ b/kani_metadata/src/lib.rs @@ -35,7 +35,7 @@ pub struct KaniMetadata { pub contracted_functions: Vec, } -#[derive(Debug, Clone, Serialize, Deserialize)] +#[derive(Debug, Clone, Serialize, Deserialize, Eq, PartialEq, PartialOrd, Ord)] pub struct ContractedFunction { /// The fully qualified name the user gave to the function (i.e. includes the module path). pub function: String, diff --git a/tests/script-based-pre/cargo_list/Cargo.toml b/tests/script-based-pre/cargo_list/Cargo.toml index 00f6ef48965e..487d2356f381 100644 --- a/tests/script-based-pre/cargo_list/Cargo.toml +++ b/tests/script-based-pre/cargo_list/Cargo.toml @@ -2,7 +2,7 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [package] -name = "sample_crate" +name = "cargo_list" version = "0.1.0" edition = "2021" diff --git a/tests/script-based-pre/cargo_list/config.yml b/tests/script-based-pre/cargo_list/config.yml index 816e3413c65f..ce681685e7c2 100644 --- a/tests/script-based-pre/cargo_list/config.yml +++ b/tests/script-based-pre/cargo_list/config.yml @@ -1,4 +1,4 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT script: list.sh -expected: list-pretty.expected +expected: list.expected \ No newline at end of file diff --git a/tests/script-based-pre/cargo_list/list-pretty.expected b/tests/script-based-pre/cargo_list/list-pretty.expected deleted file mode 100644 index e86fd0d595b2..000000000000 --- a/tests/script-based-pre/cargo_list/list-pretty.expected +++ /dev/null @@ -1,36 +0,0 @@ -Contracts: -Each function in the table below either has contracts or is the target of a contract harness (#[kani::proof_for_contract]). - -Function -# of Contracts -Contract Harnesses - -example::implementation::bar -4 -example::verify::check_bar - -example::implementation::baz -0 -example::verify::check_baz - -example::implementation::foo -2 -example::verify::check_foo_u32 - -example::verify::check_foo_u64 -example::implementation::func -1 -example::verify::check_func - -example::prep::parse -1 -NONE - -Total -5 -8 -5 - -Standard Harnesses (#[kani::proof]): -1. standard_harnesses::example::verify::check_modify -2. standard_harnesses::example::verify::check_new \ No newline at end of file diff --git a/tests/script-based-pre/cargo_list/list.expected b/tests/script-based-pre/cargo_list/list.expected new file mode 100644 index 000000000000..3e57203438dc --- /dev/null +++ b/tests/script-based-pre/cargo_list/list.expected @@ -0,0 +1,57 @@ +{ + "kani-version": + "file-version": "0.1", + "standard-harnesses": { + "src/standard_harnesses.rs": [ + "standard_harnesses::example::verify::check_modify", + "standard_harnesses::example::verify::check_new" + ] + }, + "contract-harnesses": { + "src/lib.rs": [ + "example::verify::check_bar", + "example::verify::check_foo_u32", + "example::verify::check_foo_u64", + "example::verify::check_func" + ] + }, + "contracts": [ + { + "function": "example::implementation::bar", + "file": "src/lib.rs", + "total_contracts": 4, + "harnesses": [ + "example::verify::check_bar" + ] + }, + { + "function": "example::implementation::foo", + "file": "src/lib.rs", + "total_contracts": 2, + "harnesses": [ + "example::verify::check_foo_u32", + "example::verify::check_foo_u64" + ] + }, + { + "function": "example::implementation::func", + "file": "src/lib.rs", + "total_contracts": 1, + "harnesses": [ + "example::verify::check_func" + ] + }, + { + "function": "example::prep::parse", + "file": "src/lib.rs", + "total_contracts": 1, + "harnesses": [] + } + ], + "totals": { + "standard-harnesses": 2, + "contract-harnesses": 4, + "functions-under-contract": 4, + "contracts": 8 + } +} \ No newline at end of file diff --git a/tests/script-based-pre/cargo_list/list.sh b/tests/script-based-pre/cargo_list/list.sh index c394e8dff8de..6b1ab80b0f5f 100755 --- a/tests/script-based-pre/cargo_list/list.sh +++ b/tests/script-based-pre/cargo_list/list.sh @@ -2,7 +2,9 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT -# The table in the expected omits the table borders because the runtest script -# does not evaluate the table borders in the captured output as equal to the table borders in the expected file. +# Check that the JSON file produced by `cargo kani list` is correct. +# Note that the list.expected file omits the value for "kani-version" +# to avoid having to update the test every time we bump versions. -cargo kani list -Z list \ No newline at end of file +cargo kani list -Z list -Z function-contracts --format json +cat "kani-list.json" diff --git a/tests/script-based-pre/cargo_list/src/lib.rs b/tests/script-based-pre/cargo_list/src/lib.rs index 82044b6d7ea5..e7382a9124a3 100644 --- a/tests/script-based-pre/cargo_list/src/lib.rs +++ b/tests/script-based-pre/cargo_list/src/lib.rs @@ -8,6 +8,13 @@ mod standard_harnesses; #[cfg(kani)] mod example { + mod prep { + #[kani::requires(s.len() < 10)] + fn parse(s: &str) -> u32 { + s.parse().unwrap() + } + } + pub mod implementation { #[kani::requires(*x < 4)] #[kani::requires(*x > 2)] @@ -18,27 +25,16 @@ mod example { *x += 1; } - #[kani::requires(true)] - #[kani::ensures(|_| old(*x) == *x)] - pub fn foo(x: &mut T) -> T { - *x - } - #[kani::requires(*x < 100)] #[kani::modifies(x)] pub fn func(x: &mut i32) { *x *= 1; } - pub fn baz(x: &mut i32) { - *x /= 1; - } - } - - mod prep { - #[kani::requires(s.len() < 10)] - fn parse(s: &str) -> u32 { - s.parse().unwrap() + #[kani::requires(true)] + #[kani::ensures(|_| old(*x) == *x)] + pub fn foo(x: &mut T) -> T { + *x } } @@ -68,11 +64,5 @@ mod example { let mut x = 7; implementation::func(&mut x); } - - #[kani::proof_for_contract(implementation::baz)] - fn check_baz() { - let mut x = 7; - implementation::baz(&mut x); - } } } diff --git a/tests/script-based-pre/kani_list/config.yml b/tests/script-based-pre/kani_list/config.yml index 816e3413c65f..4eac6f79588c 100644 --- a/tests/script-based-pre/kani_list/config.yml +++ b/tests/script-based-pre/kani_list/config.yml @@ -1,4 +1,4 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT script: list.sh -expected: list-pretty.expected +expected: list.expected diff --git a/tests/script-based-pre/kani_list/list-pretty.expected b/tests/script-based-pre/kani_list/list-pretty.expected deleted file mode 100644 index 5d22cd0e7eb9..000000000000 --- a/tests/script-based-pre/kani_list/list-pretty.expected +++ /dev/null @@ -1,36 +0,0 @@ -Contracts: -Each function in the table below either has contracts or is the target of a contract harness (#[kani::proof_for_contract]). - -Function -# of Contracts -Contract Harnesses - -example::implementation::bar -4 -example::verify::check_bar - -example::implementation::baz -0 -example::verify::check_baz - -example::implementation::foo -2 -example::verify::check_foo_u32 - -example::verify::check_foo_u64 -example::implementation::func -1 -example::verify::check_func - -example::prep::parse -1 -NONE - -Total -5 -8 -5 - -Standard Harnesses (#[kani::proof]): -1. example::verify::check_modify -2. example::verify::check_new \ No newline at end of file diff --git a/tests/script-based-pre/kani_list/list.expected b/tests/script-based-pre/kani_list/list.expected new file mode 100644 index 000000000000..806a2d0e7550 --- /dev/null +++ b/tests/script-based-pre/kani_list/list.expected @@ -0,0 +1,57 @@ +{ + "kani-version": + "file-version": "0.1", + "standard-harnesses": { + "src/lib.rs": [ + "example::verify::check_modify", + "example::verify::check_new" + ] + }, + "contract-harnesses": { + "src/lib.rs": [ + "example::verify::check_bar", + "example::verify::check_foo_u32", + "example::verify::check_foo_u64", + "example::verify::check_func" + ] + }, + "contracts": [ + { + "function": "example::implementation::bar", + "file": "src/lib.rs", + "total_contracts": 4, + "harnesses": [ + "example::verify::check_bar" + ] + }, + { + "function": "example::implementation::foo", + "file": "src/lib.rs", + "total_contracts": 2, + "harnesses": [ + "example::verify::check_foo_u32", + "example::verify::check_foo_u64" + ] + }, + { + "function": "example::implementation::func", + "file": "src/lib.rs", + "total_contracts": 1, + "harnesses": [ + "example::verify::check_func" + ] + }, + { + "function": "example::prep::parse", + "file": "src/lib.rs", + "total_contracts": 1, + "harnesses": [] + } + ], + "totals": { + "standard-harnesses": 2, + "contract-harnesses": 4, + "functions-under-contract": 4, + "contracts": 8 + } +} \ No newline at end of file diff --git a/tests/script-based-pre/kani_list/list.sh b/tests/script-based-pre/kani_list/list.sh index bbd852a8b054..f969709e081d 100755 --- a/tests/script-based-pre/kani_list/list.sh +++ b/tests/script-based-pre/kani_list/list.sh @@ -2,7 +2,9 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT -# The table in the expected omits the table borders because the runtest script -# does not evaluate the table borders in the captured output as equal to the table borders in the expected file. +# Check that the JSON file produced by `kani list` is correct. +# Note that the list.expected file omits the value for "kani-version" +# to avoid having to update the test every time we bump versions. -kani list -Z list src/lib.rs \ No newline at end of file +kani list -Z list -Z function-contracts src/lib.rs --format json +cat "kani-list.json" \ No newline at end of file diff --git a/tests/script-based-pre/kani_list/src/lib.rs b/tests/script-based-pre/kani_list/src/lib.rs index 16bab7aaaebc..69dbba5a9e0f 100644 --- a/tests/script-based-pre/kani_list/src/lib.rs +++ b/tests/script-based-pre/kani_list/src/lib.rs @@ -5,6 +5,13 @@ //! It ensures that the list command across modules, and with modifies clauses, history expressions, and generic functions. mod example { + mod prep { + #[kani::requires(s.len() < 10)] + fn parse(s: &str) -> u32 { + s.parse().unwrap() + } + } + pub mod implementation { #[kani::requires(*x < 4)] #[kani::requires(*x > 2)] @@ -26,17 +33,6 @@ mod example { pub fn func(x: &mut i32) { *x *= 1; } - - pub fn baz(x: &mut i32) { - *x /= 1; - } - } - - mod prep { - #[kani::requires(s.len() < 10)] - fn parse(s: &str) -> u32 { - s.parse().unwrap() - } } mod verify { @@ -66,12 +62,6 @@ mod example { implementation::func(&mut x); } - #[kani::proof_for_contract(implementation::baz)] - fn check_baz() { - let mut x = 7; - implementation::baz(&mut x); - } - #[kani::proof] fn check_modify() {}