diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs index 3a6da89239b5..2f92a3b83b17 100644 --- a/cprover_bindings/src/goto_program/expr.rs +++ b/cprover_bindings/src/goto_program/expr.rs @@ -170,6 +170,22 @@ pub enum ExprValue { }, } +/// The equivalent of a "mathematical function" in CBMC. Semantically this is an +/// anonymous function object, similar to a closure, but without closing over an +/// environment. +/// +/// This is only valid for use as a function contract. It may not perform side +/// effects, a property that is enforced on the CBMC side. +/// +/// The precise nomenclature is that in CBMC a contract value has *type* +/// `mathematical_function` and values of that type are `lambda`s. Since this +/// struct represents such values it is named `Lambda`. +#[derive(Debug, Clone)] +pub struct Lambda { + pub arguments: Vec<(InternedString, Type)>, + pub body: Expr, +} + /// Binary operators. The names are the same as in the Irep representation. #[derive(Debug, Clone, Copy)] pub enum BinaryOperator { diff --git a/cprover_bindings/src/goto_program/mod.rs b/cprover_bindings/src/goto_program/mod.rs index 15c0282f9a40..d8987b6df738 100644 --- a/cprover_bindings/src/goto_program/mod.rs +++ b/cprover_bindings/src/goto_program/mod.rs @@ -18,10 +18,11 @@ mod typ; pub use builtin::BuiltinFn; pub use expr::{ arithmetic_overflow_result_type, ArithmeticOverflowResult, BinaryOperator, Expr, ExprValue, - SelfOperator, UnaryOperator, ARITH_OVERFLOW_OVERFLOWED_FIELD, ARITH_OVERFLOW_RESULT_FIELD, + Lambda, SelfOperator, UnaryOperator, ARITH_OVERFLOW_OVERFLOWED_FIELD, + ARITH_OVERFLOW_RESULT_FIELD, }; pub use location::Location; pub use stmt::{Stmt, StmtBody, SwitchCase}; -pub use symbol::{Symbol, SymbolValues}; +pub use symbol::{FunctionContract, Symbol, SymbolValues}; pub use symbol_table::SymbolTable; pub use typ::{CIntType, DatatypeComponent, Parameter, Type}; diff --git a/cprover_bindings/src/goto_program/symbol.rs b/cprover_bindings/src/goto_program/symbol.rs index 7f74abaa9816..fd1d76328ac5 100644 --- a/cprover_bindings/src/goto_program/symbol.rs +++ b/cprover_bindings/src/goto_program/symbol.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT use super::super::utils::aggr_tag; -use super::{DatatypeComponent, Expr, Location, Parameter, Stmt, Type}; +use super::{DatatypeComponent, Expr, Lambda, Location, Parameter, Stmt, Type}; use crate::{InternStringOption, InternedString}; /// Based off the CBMC symbol implementation here: @@ -13,6 +13,8 @@ pub struct Symbol { pub location: Location, pub typ: Type, pub value: SymbolValues, + /// Contracts to be enforced (only supported for functions) + pub contract: Option>, /// Optional debugging information @@ -44,6 +46,22 @@ pub struct Symbol { pub is_weak: bool, } +/// The CBMC representation of a function contract with three types of clauses. +/// See https://diffblue.github.io/cbmc/contracts-user.html for the meaning of +/// each type of clause. +#[derive(Clone, Debug)] +pub struct FunctionContract { + pub(crate) requires: Vec, + pub(crate) ensures: Vec, + pub(crate) assigns: Vec, +} + +impl FunctionContract { + pub fn new(requires: Vec, ensures: Vec, assigns: Vec) -> Self { + Self { requires, ensures, assigns } + } +} + /// Currently, only C is understood by CBMC. // TODO: #[derive(Clone, Debug)] @@ -84,6 +102,7 @@ impl Symbol { base_name, pretty_name, + contract: None, module: None, mode: SymbolModes::C, // global properties @@ -107,6 +126,20 @@ impl Symbol { } } + /// Add this contract to the symbol (symbol must be a function) or fold the + /// conditions into an existing contract. + pub fn attach_contract(&mut self, contract: FunctionContract) { + assert!(self.typ.is_code()); + match self.contract { + Some(ref mut prior) => { + prior.assigns.extend(contract.assigns); + prior.requires.extend(contract.requires); + prior.ensures.extend(contract.ensures); + } + None => self.contract = Some(Box::new(contract)), + } + } + /// The symbol that defines the type of the struct or union. /// For a struct foo this is the symbol "tag-foo" that maps to the type struct foo. pub fn aggr_ty>(t: Type, pretty_name: T) -> Symbol { diff --git a/cprover_bindings/src/goto_program/symbol_table.rs b/cprover_bindings/src/goto_program/symbol_table.rs index 1e635ec925da..9bcd14cb624e 100644 --- a/cprover_bindings/src/goto_program/symbol_table.rs +++ b/cprover_bindings/src/goto_program/symbol_table.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT use super::super::{env, MachineModel}; -use super::{BuiltinFn, Stmt, Symbol}; +use super::{BuiltinFn, FunctionContract, Stmt, Symbol}; use crate::InternedString; use std::collections::BTreeMap; /// This is a typesafe implementation of the CBMC symbol table, based on the CBMC code at: @@ -79,6 +79,15 @@ impl SymbolTable { let name = name.into(); self.symbol_table.get_mut(&name).unwrap().update_fn_declaration_with_definition(body); } + + pub fn attach_contract>( + &mut self, + name: T, + contract: FunctionContract, + ) { + let sym = self.symbol_table.get_mut(&name.into()).unwrap(); + sym.attach_contract(contract); + } } /// Getters diff --git a/cprover_bindings/src/irep/irep.rs b/cprover_bindings/src/irep/irep.rs index 68e094000884..0d0c6dc4ace7 100644 --- a/cprover_bindings/src/irep/irep.rs +++ b/cprover_bindings/src/irep/irep.rs @@ -6,6 +6,7 @@ use super::super::goto_program::{Location, Type}; use super::super::MachineModel; use super::{IrepId, ToIrep}; use crate::cbmc_string::InternedString; +use crate::linear_map; use linear_map::LinearMap; use num::BigInt; use std::fmt::Debug; @@ -141,4 +142,12 @@ impl Irep { pub fn zero() -> Irep { Irep::just_id(IrepId::Id0) } + + pub fn tuple(sub: Vec) -> Self { + Irep { + id: IrepId::Tuple, + sub, + named_sub: linear_map![(IrepId::Type, Irep::just_id(IrepId::Tuple))], + } + } } diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs index 70810e403c54..8991ebb9a210 100644 --- a/cprover_bindings/src/irep/to_irep.rs +++ b/cprover_bindings/src/irep/to_irep.rs @@ -5,7 +5,9 @@ use super::super::goto_program; use super::super::MachineModel; use super::{Irep, IrepId}; +use crate::goto_program::Lambda; use crate::linear_map; +use crate::InternedString; use goto_program::{ BinaryOperator, CIntType, DatatypeComponent, Expr, ExprValue, Location, Parameter, SelfOperator, Stmt, StmtBody, SwitchCase, SymbolValues, Type, UnaryOperator, @@ -169,6 +171,16 @@ impl ToIrep for Expr { } } +impl Irep { + pub fn symbol(identifier: InternedString) -> Self { + Irep { + id: IrepId::Symbol, + sub: vec![], + named_sub: linear_map![(IrepId::Identifier, Irep::just_string_id(identifier))], + } + } +} + impl ToIrep for ExprValue { fn to_irep(&self, mm: &MachineModel) -> Irep { match self { @@ -297,14 +309,7 @@ impl ToIrep for ExprValue { sub: values.iter().map(|x| x.to_irep(mm)).collect(), named_sub: linear_map![], }, - ExprValue::Symbol { identifier } => Irep { - id: IrepId::Symbol, - sub: vec![], - named_sub: linear_map![( - IrepId::Identifier, - Irep::just_string_id(identifier.to_string()), - )], - }, + ExprValue::Symbol { identifier } => Irep::symbol(*identifier), ExprValue::Typecast(e) => { Irep { id: IrepId::Typecast, sub: vec![e.to_irep(mm)], named_sub: linear_map![] } } @@ -499,10 +504,44 @@ impl ToIrep for SwitchCase { } } +impl ToIrep for Lambda { + fn to_irep(&self, mm: &MachineModel) -> Irep { + let (ops_ireps, types) = self + .arguments + .iter() + .map(|(i, ty)| { + let ty_rep = ty.to_irep(mm); + (Irep::symbol(*i).with_named_sub(IrepId::Type, ty_rep.clone()), ty_rep) + }) + .unzip(); + let typ = Irep { + id: IrepId::MathematicalFunction, + sub: vec![Irep::just_sub(types), self.body.typ().to_irep(mm)], + named_sub: Default::default(), + }; + Irep { + id: IrepId::Lambda, + sub: vec![Irep::tuple(ops_ireps), self.body.to_irep(mm)], + named_sub: linear_map!((IrepId::Type, typ)), + } + } +} + impl goto_program::Symbol { pub fn to_irep(&self, mm: &MachineModel) -> super::Symbol { + let mut typ = self.typ.to_irep(mm); + if let Some(contract) = &self.contract { + typ = typ.with_named_sub( + IrepId::CSpecRequires, + Irep::just_sub(contract.requires.iter().map(|c| c.to_irep(mm)).collect()), + ); + typ = typ.with_named_sub( + IrepId::CSpecEnsures, + Irep::just_sub(contract.ensures.iter().map(|c| c.to_irep(mm)).collect()), + ); + } super::Symbol { - typ: self.typ.to_irep(mm), + typ, value: match &self.value { SymbolValues::Expr(e) => e.to_irep(mm), SymbolValues::Stmt(s) => s.to_irep(mm), diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index 800ec8219e40..fcb5b2ed920d 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -4,7 +4,8 @@ //! This file contains functions related to codegenning MIR functions into gotoc use crate::codegen_cprover_gotoc::GotocCtx; -use cbmc::goto_program::{Expr, Stmt, Symbol}; +use crate::kani_middle::contracts::GFnContract; +use cbmc::goto_program::{Expr, FunctionContract, Lambda, Stmt, Symbol, Type}; use cbmc::InternString; use rustc_middle::mir::traversal::reverse_postorder; use rustc_middle::mir::{Body, HasLocalDecls, Local}; @@ -222,6 +223,90 @@ impl<'tcx> GotocCtx<'tcx> { ); } + /// Convert the Kani level contract into a CBMC level contract by creating a + /// lambda that calls the contract implementation function. + /// + /// For instance say we are processing a contract on `f` + /// + /// ```rs + /// as_goto_contract(..., GFnContract { requires: , .. }) + /// = Contract { + /// requires: [ + /// Lambda { + /// arguments: , + /// body: Call(codegen_fn_expr(contract_impl_fn), [args of f..., return arg]) + /// } + /// ], + /// ... + /// } + /// ``` + /// + /// A spec lambda in GOTO receives as its first argument the return value of + /// the annotated function. However at the top level we must receive `self` + /// as first argument, because rust requires it. As a result the generated + /// lambda takes the return value as first argument and then immediately + /// calls the generated spec function, but passing the return value as the + /// last argument. + fn as_goto_contract(&mut self, fn_contract: &GFnContract>) -> FunctionContract { + use rustc_middle::mir; + let mut handle_contract_expr = |instance| { + let mir = self.current_fn().mir(); + assert!(mir.spread_arg.is_none()); + let func_expr = self.codegen_func_expr(instance, None); + let mut mir_arguments: Vec<_> = + std::iter::successors(Some(mir::RETURN_PLACE + 1), |i| Some(*i + 1)) + .take(mir.arg_count + 1) // one extra for return value + .collect(); + let return_arg = mir_arguments.pop().unwrap(); + let mir_operands: Vec<_> = + mir_arguments.iter().map(|l| mir::Operand::Copy((*l).into())).collect(); + let mut arguments = self.codegen_funcall_args(&mir_operands, true); + let goto_argument_types: Vec<_> = [mir::RETURN_PLACE] + .into_iter() + .chain(mir_arguments.iter().copied()) + .map(|a| self.codegen_ty(self.monomorphize(mir.local_decls()[a].ty))) + .collect(); + + mir_arguments.insert(0, return_arg); + arguments.push(Expr::symbol_expression( + self.codegen_var_name(&return_arg), + goto_argument_types.first().unwrap().clone(), + )); + Lambda { + arguments: mir_arguments + .into_iter() + .map(|l| self.codegen_var_name(&l).into()) + .zip(goto_argument_types) + .collect(), + body: func_expr.call(arguments).cast_to(Type::Bool), + } + }; + + let requires = + fn_contract.requires().iter().copied().map(&mut handle_contract_expr).collect(); + let ensures = + fn_contract.ensures().iter().copied().map(&mut handle_contract_expr).collect(); + FunctionContract::new(requires, ensures, vec![]) + } + + /// Convert the contract to a CBMC contract, then attach it to `instance`. + /// `instance` must have previously been declared. + /// + /// This does not overwrite prior contracts but merges with them. + pub fn attach_contract( + &mut self, + instance: Instance<'tcx>, + contract: &GFnContract>, + ) { + // This should be safe, since the contract is pretty much evaluated as + // though it was the first (or last) assertion in the function. + self.set_current_fn(instance); + let goto_contract = self.as_goto_contract(contract); + let name = self.current_fn().name(); + self.symbol_table.attach_contract(name, goto_contract); + self.reset_current_fn() + } + pub fn declare_function(&mut self, instance: Instance<'tcx>) { debug!("declaring {}; {:?}", instance, instance); self.set_current_fn(instance); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 23211f022b23..b0e02788a0ac 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -723,8 +723,8 @@ impl<'tcx> GotocCtx<'tcx> { trace!(func=?instance, "codegen_func_symbol"); let func = self.symbol_name(instance); self.symbol_table - .lookup(func) - .expect("Function `{func}` should've been declared before usage") + .lookup(&func) + .unwrap_or_else(|| panic!("Function `{func}` should've been declared before usage")) }; (sym, funct) } diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index a89e5035f2a2..fa0735a242e3 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -6,6 +6,7 @@ use crate::codegen_cprover_gotoc::GotocCtx; use crate::kani_middle::analysis; use crate::kani_middle::attributes::is_test_harness_description; +use crate::kani_middle::contracts::GFnContract; use crate::kani_middle::metadata::gen_test_metadata; use crate::kani_middle::provide; use crate::kani_middle::reachability::{ @@ -37,7 +38,7 @@ use rustc_metadata::EncodedMetadata; use rustc_middle::dep_graph::{WorkProduct, WorkProductId}; use rustc_middle::mir::mono::MonoItem; use rustc_middle::query::{ExternProviders, Providers}; -use rustc_middle::ty::TyCtxt; +use rustc_middle::ty::{self, TyCtxt}; use rustc_session::config::{CrateType, OutputFilenames, OutputType}; use rustc_session::cstore::MetadataLoaderDyn; use rustc_session::output::out_filename; @@ -69,6 +70,8 @@ pub struct GotocCodegenBackend { queries: Arc>, } +type MonoContract<'tcx> = GFnContract>; + impl GotocCodegenBackend { pub fn new(queries: Arc>) -> Self { GotocCodegenBackend { queries } @@ -81,11 +84,12 @@ impl GotocCodegenBackend { starting_items: &[MonoItem<'tcx>], symtab_goto: &Path, machine_model: &MachineModel, - ) -> (GotocCtx<'tcx>, Vec>) { - let items = with_timer( + ) -> (GotocCtx<'tcx>, Vec<(MonoItem<'tcx>, Option>)>) { + let items_with_contracts = with_timer( || collect_reachable_items(tcx, starting_items), "codegen reachability analysis", ); + let items: Vec<_> = items_with_contracts.iter().map(|i| i.0).collect(); dump_mir_items(tcx, &items, &symtab_goto.with_extension("kani.mir")); // Follow rustc naming convention (cx is abbrev for context). @@ -119,6 +123,19 @@ impl GotocCodegenBackend { } } + // Attaching the contrcts gets its own loop, because the + // functions used in the contract expressions must have been + // declared before + for (item, contract) in &items_with_contracts { + if let Some(contract) = contract { + let instance = match item { + MonoItem::Fn(instance) => *instance, + _ => unreachable!(), + }; + gcx.attach_contract(instance, contract); + } + } + // then we move on to codegen for item in &items { match *item { @@ -179,7 +196,7 @@ impl GotocCodegenBackend { } } - (gcx, items) + (gcx, items_with_contracts) } } @@ -238,8 +255,9 @@ impl CodegenBackend for GotocCodegenBackend { for harness in harnesses { let model_path = queries.harness_model_path(&tcx.def_path_hash(harness.def_id())).unwrap(); - let (gcx, items) = + let (gcx, items_with_contracts) = self.codegen_items(tcx, &[harness], model_path, &results.machine_model); + let items = items_with_contracts.into_iter().map(|(i, _contract)| i).collect(); results.extend(gcx, items, None); } } @@ -261,14 +279,33 @@ impl CodegenBackend for GotocCodegenBackend { // We will be able to remove this once we optimize all calls to CBMC utilities. // https://github.com/model-checking/kani/issues/1971 let model_path = base_filename.with_extension(ArtifactType::SymTabGoto); - let (gcx, items) = + let (gcx, items_with_contracts) = self.codegen_items(tcx, &harnesses, &model_path, &results.machine_model); + let mut contract_function = None; + let items = items_with_contracts + .into_iter() + .map(|(i, contract)| { + if contract.is_some() { + let instance = match i { + MonoItem::Fn(f) => f, + _ => unreachable!(), + }; + assert!( + contract_function.replace(gcx.symbol_name(instance)).is_none(), + "Only one function contract can be enforced at a time" + ); + } + i + }) + .collect(); results.extend(gcx, items, None); for (test_fn, test_desc) in harnesses.iter().zip(descriptions.iter()) { let instance = if let MonoItem::Fn(instance) = test_fn { instance } else { continue }; - let metadata = gen_test_metadata(tcx, *test_desc, *instance, &base_filename); + let mut metadata = + gen_test_metadata(tcx, *test_desc, *instance, &base_filename); + metadata.contract_to_enforce = contract_function.clone(); let test_model_path = &metadata.goto_file.as_ref().unwrap(); std::fs::copy(&model_path, &test_model_path).expect(&format!( "Failed to copy {} to {}", @@ -286,8 +323,15 @@ impl CodegenBackend for GotocCodegenBackend { || entry_fn == Some(def_id) }); let model_path = base_filename.with_extension(ArtifactType::SymTabGoto); - let (gcx, items) = + let (gcx, items_with_contracts) = self.codegen_items(tcx, &local_reachable, &model_path, &results.machine_model); + let items = items_with_contracts + .into_iter() + .map(|(i, contract)| { + assert!(contract.is_none()); + i + }) + .collect(); results.extend(gcx, items, None); } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/mod.rs b/kani-compiler/src/codegen_cprover_gotoc/mod.rs index 7454d748d660..00f89cb434f2 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/mod.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/mod.rs @@ -9,3 +9,5 @@ mod utils; pub use compiler_interface::{GotocCodegenBackend, UnsupportedConstructs}; pub use context::GotocCtx; pub use context::VtableCtx; + +pub use utils::symbol_name_for_instance; diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/mod.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/mod.rs index 9d832146e3e8..69176bddfb2e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/utils/mod.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/utils/mod.rs @@ -14,3 +14,4 @@ pub use names::*; pub use utils::*; pub use debug::init; +pub use names::{readable_name_of_instance, symbol_name_for_instance}; diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs index a2c3ea3518e9..baba473db397 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs @@ -54,27 +54,12 @@ impl<'tcx> GotocCtx<'tcx> { /// A human readable name in Rust for reference, should not be used as a key. pub fn readable_instance_name(&self, instance: Instance<'tcx>) -> String { - with_no_trimmed_paths!( - self.tcx.def_path_str_with_substs(instance.def_id(), instance.substs) - ) + readable_name_of_instance(self.tcx, instance) } /// The actual function name used in the symbol table pub fn symbol_name(&self, instance: Instance<'tcx>) -> String { - let llvm_mangled = self.tcx.symbol_name(instance).name.to_string(); - debug!( - "finding function name for instance: {}, debug: {:?}, name: {}, symbol: {}", - instance, - instance, - self.readable_instance_name(instance), - llvm_mangled, - ); - - let pretty = self.readable_instance_name(instance); - - // Make main function a special case in order to support `--function main` - // TODO: Get rid of this: https://github.com/model-checking/kani/issues/2129 - if pretty == "main" { pretty } else { llvm_mangled } + symbol_name_for_instance(self.tcx, instance) } /// The name for a tuple field @@ -102,6 +87,29 @@ impl<'tcx> GotocCtx<'tcx> { } } +/// The actual function name used in the symbol table +pub fn symbol_name_for_instance<'tcx>(tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> String { + let llvm_mangled = tcx.symbol_name(instance).name.to_string(); + debug!( + "finding function name for instance: {}, debug: {:?}, name: {}, symbol: {}", + instance, + instance, + readable_name_of_instance(tcx, instance), + llvm_mangled, + ); + + let pretty = readable_name_of_instance(tcx, instance); + + // Make main function a special case in order to support `--function main` + // TODO: Get rid of this: https://github.com/model-checking/kani/issues/2129 + if pretty == "main" { pretty } else { llvm_mangled } +} + +/// A human readable name in Rust for reference, should not be used as a key. +pub fn readable_name_of_instance<'tcx>(tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> String { + with_no_trimmed_paths!(tcx.def_path_str_with_substs(instance.def_id(), instance.substs)) +} + /// The full crate name should use the Codegen Unit builder to include full name resolution, /// for example, the versioning information if a build requires two different versions /// of the same crate. diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index cdb17b8cd0ac..b2be4d796468 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/kani-compiler/src/kani_compiler.rs @@ -16,11 +16,11 @@ //! `-C llvm-args`. #[cfg(feature = "cprover")] -use crate::codegen_cprover_gotoc::GotocCodegenBackend; +use crate::codegen_cprover_gotoc::{symbol_name_for_instance, GotocCodegenBackend}; use crate::kani_middle::attributes::is_proof_harness; use crate::kani_middle::check_crate_items; use crate::kani_middle::metadata::gen_proof_metadata; -use crate::kani_middle::reachability::filter_crate_items; +use crate::kani_middle::reachability::{collect_reachable_items, filter_crate_items}; use crate::kani_middle::stubbing::{self, harness_stub_map}; use crate::kani_queries::{QueryDb, ReachabilityType}; use crate::parser::{self, KaniCompilerParser}; @@ -31,6 +31,7 @@ use rustc_driver::{Callbacks, Compilation, RunCompiler}; use rustc_hir::def_id::LOCAL_CRATE; use rustc_hir::definitions::DefPathHash; use rustc_interface::Config; +use rustc_middle::mir::mono::MonoItem; use rustc_middle::ty::TyCtxt; use rustc_session::config::{ErrorOutputType, OutputType}; use rustc_span::ErrorGuaranteed; @@ -232,7 +233,13 @@ impl KaniCompiler { .map(|harness| { let def_id = harness.def_id(); let def_path = tcx.def_path_hash(def_id); - let metadata = gen_proof_metadata(tcx, def_id, &base_filename); + let mut contracts = contracts_for_harness(tcx, harness); + let contract = contracts.pop(); + assert!( + contracts.is_empty(), + "Only one function contract may be enforced at a time." + ); + let metadata = gen_proof_metadata(tcx, def_id, &base_filename, contract); let stub_map = harness_stub_map(tcx, def_id, &metadata); (def_path, HarnessInfo { metadata, stub_map }) }) @@ -320,6 +327,21 @@ impl KaniCompiler { } } +/// Find all functions reachable from this harness that have a contract attached to them. +fn contracts_for_harness<'tcx>(tcx: TyCtxt<'tcx>, harness: MonoItem<'tcx>) -> Vec { + collect_reachable_items(tcx, &[harness]) + .into_iter() + .filter_map(|(i, contract)| { + let _ = contract?; + let instance = match i { + MonoItem::Fn(f) => f, + _ => unreachable!("Cannot add contracts to non-functions"), + }; + Some(symbol_name_for_instance(tcx, instance)) + }) + .collect() +} + /// Group the harnesses by their stubs. fn group_by_stubs( harnesses: Vec, @@ -410,6 +432,7 @@ mod tests { original_end_line: 20, goto_file: None, attributes: HarnessAttributes::default(), + contract_to_enforce: None, } } diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 6ee5136e12e5..657a44164007 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -5,9 +5,15 @@ use std::collections::BTreeMap; use kani_metadata::{CbmcSolver, HarnessAttributes, Stub}; -use rustc_ast::{attr, AttrKind, Attribute, LitKind, MetaItem, MetaItemKind, NestedMetaItem}; +use rustc_ast::{ + attr, AttrArgs, AttrArgsEq, AttrKind, Attribute, LitKind, MetaItem, MetaItemKind, + NestedMetaItem, +}; use rustc_errors::ErrorGuaranteed; -use rustc_hir::{def::DefKind, def_id::DefId}; +use rustc_hir::{ + def::DefKind, + def_id::{DefId, LocalDefId}, +}; use rustc_middle::ty::{Instance, TyCtxt, TyKind}; use rustc_span::Span; use std::str::FromStr; @@ -27,6 +33,8 @@ enum KaniAttributeKind { /// Attribute used to mark unstable APIs. Unstable, Unwind, + Requires, + Ensures, } impl KaniAttributeKind { @@ -38,7 +46,9 @@ impl KaniAttributeKind { | KaniAttributeKind::Solver | KaniAttributeKind::Stub | KaniAttributeKind::Unwind => true, - KaniAttributeKind::Unstable => false, + KaniAttributeKind::Unstable + | KaniAttributeKind::Ensures + | KaniAttributeKind::Requires => false, } } } @@ -90,6 +100,7 @@ pub(super) fn check_attributes(tcx: TyCtxt, def_id: DefId) { KaniAttributeKind::Unstable => attrs.iter().for_each(|attr| { let _ = UnstableAttribute::try_from(*attr).map_err(|err| err.report(tcx)); }), + KaniAttributeKind::Ensures | KaniAttributeKind::Requires => (), }; } } @@ -137,11 +148,75 @@ pub fn extract_harness_attributes(tcx: TyCtxt, def_id: DefId) -> HarnessAttribut // Internal attribute which shouldn't exist here. unreachable!() } + KaniAttributeKind::Ensures | KaniAttributeKind::Requires => tcx.sess.fatal(format!( + "Contracts on harnesses are not supported (found {} on {})", + kind.as_ref(), + tcx.def_path_debug_str(def_id) + )), }; harness }) } +/// Extract function contracts on this item. +/// +/// This parses the annotation and resolves the mentioned implementation +/// functions for the contract. +/// +/// If no contract annotations are found the return value of this function will +/// simply not be [`enforceable()`](super::contracts::GFnContract::enforceable) and can be ignored. +pub fn extract_contract(tcx: TyCtxt, local_def_id: LocalDefId) -> super::contracts::FnContract { + use rustc_ast::ExprKind; + use rustc_hir::{Item, ItemKind, Mod, Node}; + let hir_map = tcx.hir(); + let hir_id = hir_map.local_def_id_to_hir_id(local_def_id); + let find_sibling_by_name = |name| { + let find_in_mod = |md: &Mod<'_>| { + md.item_ids.iter().find(|it| hir_map.item(**it).ident.name == name).unwrap().hir_id() + }; + + match hir_map.get_parent(hir_id) { + Node::Item(Item { kind, .. }) => match kind { + ItemKind::Mod(m) => find_in_mod(m), + ItemKind::Impl(imp) => { + imp.items.iter().find(|it| it.ident.name == name).unwrap().id.hir_id() + } + other => panic!("Odd parent item kind {other:?}"), + }, + Node::Crate(m) => find_in_mod(m), + other => panic!("Odd prant node type {other:?}"), + } + .expect_owner() + .def_id + .to_def_id() + }; + + let parse_and_resolve = |attr: &Vec<&Attribute>| { + attr.iter() + .map(|clause| match &clause.get_normal_item().args { + AttrArgs::Eq(_, it) => { + let sym = match it { + AttrArgsEq::Ast(expr) => match expr.kind { + ExprKind::Lit(tok) => LitKind::from_token_lit(tok).unwrap().str(), + _ => unreachable!(), + }, + AttrArgsEq::Hir(lit) => lit.kind.str(), + } + .unwrap(); + find_sibling_by_name(sym) + } + _ => unreachable!(), + }) + .collect() + }; + let attributes = extract_kani_attributes(tcx, local_def_id.to_def_id()); + let requires = + attributes.get(&KaniAttributeKind::Requires).map_or_else(Vec::new, parse_and_resolve); + let ensures = + attributes.get(&KaniAttributeKind::Ensures).map_or_else(Vec::new, parse_and_resolve); + super::contracts::FnContract::new(requires, ensures) +} + /// Check that any unstable API has been enabled. Otherwise, emit an error. /// /// TODO: Improve error message by printing the span of the harness instead of the definition. diff --git a/kani-compiler/src/kani_middle/contracts.rs b/kani-compiler/src/kani_middle/contracts.rs new file mode 100644 index 000000000000..a91f3d9c0577 --- /dev/null +++ b/kani-compiler/src/kani_middle/contracts.rs @@ -0,0 +1,45 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Basic type definitions for function contracts. +use rustc_hir::def_id::DefId; + +/// Generic representation for a function contract. This is so that we can reuse +/// this type for different resolution stages if the implementation functions +/// (`C`). +#[derive(Default)] +pub struct GFnContract { + requires: Vec, + ensures: Vec, +} + +pub type FnContract = GFnContract; + +impl GFnContract { + /// Read access to all preondition clauses. + pub fn requires(&self) -> &[C] { + &self.requires + } + + /// Read access to all postcondition clauses. + pub fn ensures(&self) -> &[C] { + &self.ensures + } + + pub fn new(requires: Vec, ensures: Vec) -> Self { + Self { requires, ensures } + } + + /// Perform a transformation on each implementation item. Usually these are + /// resolution steps. + pub fn map C0>(&self, mut f: F) -> GFnContract { + GFnContract { + requires: self.requires.iter().map(&mut f).collect(), + ensures: self.ensures.iter().map(&mut f).collect(), + } + } + + /// If this is false, then this contract has no clauses and can safely be ignored. + pub fn enforceable(&self) -> bool { + !self.requires().is_empty() || !self.ensures().is_empty() + } +} diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs index 506779001689..a77a2471a5da 100644 --- a/kani-compiler/src/kani_middle/metadata.rs +++ b/kani-compiler/src/kani_middle/metadata.rs @@ -13,7 +13,12 @@ use rustc_middle::ty::{Instance, InstanceDef, TyCtxt}; use super::{attributes::extract_harness_attributes, SourceLocation}; /// Create the harness metadata for a proof harness for a given function. -pub fn gen_proof_metadata(tcx: TyCtxt, def_id: DefId, base_name: &Path) -> HarnessMetadata { +pub fn gen_proof_metadata( + tcx: TyCtxt, + def_id: DefId, + base_name: &Path, + contract: Option, +) -> HarnessMetadata { let attributes = extract_harness_attributes(tcx, def_id); let pretty_name = tcx.def_path_str(def_id); // Main function a special case in order to support `--function main` @@ -39,6 +44,7 @@ pub fn gen_proof_metadata(tcx: TyCtxt, def_id: DefId, base_name: &Path) -> Harne attributes, // TODO: This no longer needs to be an Option. goto_file: Some(model_file), + contract_to_enforce: contract, } } @@ -67,5 +73,6 @@ pub fn gen_test_metadata<'tcx>( attributes: HarnessAttributes::default(), // TODO: This no longer needs to be an Option. goto_file: Some(model_file), + contract_to_enforce: None, } } diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index ba235db26805..8fd8b8733311 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -30,6 +30,7 @@ use self::attributes::{check_attributes, check_unstable_features}; pub mod analysis; pub mod attributes; pub mod coercion; +pub mod contracts; pub mod metadata; pub mod provide; pub mod reachability; diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index a3110426dc57..c529b024359c 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -15,8 +15,10 @@ //! We have kept this module agnostic of any Kani code in case we can contribute this back to rustc. use tracing::{debug, debug_span, trace, warn}; +use std::collections::hash_map::Entry; + use rustc_data_structures::fingerprint::Fingerprint; -use rustc_data_structures::fx::FxHashSet; +use rustc_data_structures::fx::{FxHashMap, FxHashSet}; use rustc_data_structures::stable_hasher::{HashStable, StableHasher}; use rustc_hir::def::DefKind; use rustc_hir::def_id::DefId; @@ -37,11 +39,14 @@ use rustc_middle::ty::{ use crate::kani_middle::coercion; use crate::kani_middle::stubbing::get_stub; +use super::attributes; +use super::contracts::GFnContract; + /// Collect all reachable items starting from the given starting points. pub fn collect_reachable_items<'tcx>( tcx: TyCtxt<'tcx>, starting_points: &[MonoItem<'tcx>], -) -> Vec> { +) -> Vec<(MonoItem<'tcx>, Option>>)> { // For each harness, collect items using the same collector. // I.e.: This will return any item that is reachable from one or more of the starting points. let mut collector = MonoItemsCollector::new(tcx); @@ -61,7 +66,7 @@ pub fn collect_reachable_items<'tcx>( // This helps us to debug the code, but it also provides the user a good experience since the // order of the errors and warnings is stable. let mut sorted_items: Vec<_> = collector.collected.into_iter().collect(); - sorted_items.sort_by_cached_key(|item| to_fingerprint(tcx, item)); + sorted_items.sort_by_cached_key(|item| to_fingerprint(tcx, &item.0)); sorted_items } @@ -144,7 +149,7 @@ struct MonoItemsCollector<'tcx> { /// The compiler context. tcx: TyCtxt<'tcx>, /// Set of collected items used to avoid entering recursion loops. - collected: FxHashSet>, + collected: FxHashMap, Option>>>, /// Items enqueued for visiting. queue: Vec>, #[cfg(debug_assertions)] @@ -155,7 +160,7 @@ impl<'tcx> MonoItemsCollector<'tcx> { pub fn new(tcx: TyCtxt<'tcx>) -> Self { MonoItemsCollector { tcx, - collected: FxHashSet::default(), + collected: FxHashMap::default(), queue: vec![], #[cfg(debug_assertions)] call_graph: debug::CallGraph::default(), @@ -168,12 +173,51 @@ impl<'tcx> MonoItemsCollector<'tcx> { self.reachable_items(); } + pub fn add_to_queue>>(&mut self, i: I) { + self.queue.extend(i.into_iter().filter(|it| !self.collected.contains_key(it))) + } + + /// Check if there are contracts attached to this visitable item and insert + /// them in the map if so. Returns whether the item was not yet present in + /// the map before (e.g. whether the reachability analysis should continue). + fn handle_contract(&mut self, to_visit: MonoItem<'tcx>) -> bool { + let (is_hit, visit_obligations) = if let Entry::Vacant(entry) = + self.collected.entry(to_visit) + { + let opt_contract = entry.key().def_id().as_local().and_then(|local_def_id| { + let substs = match entry.key() { + MonoItem::Fn(inst) => inst.substs, + _ => rustc_middle::ty::List::empty(), + }; + let contract = attributes::extract_contract(self.tcx, local_def_id).map(|def_id| { + Instance::resolve(self.tcx, ParamEnv::reveal_all(), *def_id, substs) + .unwrap() + .expect("No specific instance found") + }); + contract.enforceable().then_some(contract) + }); + let obligations = opt_contract.as_ref().map_or_else(Vec::new, |contract| { + [contract.requires(), contract.ensures()] + .into_iter() + .flat_map(IntoIterator::into_iter) + .copied() + .map(MonoItem::Fn) + .collect() + }); + entry.insert(opt_contract); + (true, obligations) + } else { + (false, vec![]) + }; + self.add_to_queue(visit_obligations); + is_hit + } + /// Traverses the call graph starting from the given root. For every function, we visit all /// instruction looking for the items that should be included in the compilation. fn reachable_items(&mut self) { while let Some(to_visit) = self.queue.pop() { - if !self.collected.contains(&to_visit) { - self.collected.insert(to_visit); + if self.handle_contract(to_visit) { let next_items = match to_visit { MonoItem::Fn(instance) => self.visit_fn(instance), MonoItem::Static(def_id) => self.visit_static(def_id), @@ -185,8 +229,7 @@ impl<'tcx> MonoItemsCollector<'tcx> { #[cfg(debug_assertions)] self.call_graph.add_edges(to_visit, &next_items); - self.queue - .extend(next_items.into_iter().filter(|item| !self.collected.contains(item))); + self.add_to_queue(next_items); } } } diff --git a/kani-driver/src/call_goto_instrument.rs b/kani-driver/src/call_goto_instrument.rs index 8a97d9e15747..d7cb12a9590e 100644 --- a/kani-driver/src/call_goto_instrument.rs +++ b/kani-driver/src/call_goto_instrument.rs @@ -37,6 +37,10 @@ impl KaniSession { self.goto_sanity_check(output)?; } + if let Some(function) = &harness.contract_to_enforce { + self.enforce_contract(output, &function)?; + } + if self.args.checks.undefined_function_on() { self.add_library(output)?; self.undefined_functions(output)?; @@ -160,6 +164,17 @@ impl KaniSession { self.call_goto_instrument(args) } + /// Make CBMC enforce a function contract. + pub fn enforce_contract(&self, file: &Path, function: &str) -> Result<()> { + tracing::debug!(?function, "enforce_contract"); + self.call_goto_instrument(vec![ + "--enforce-contract".into(), + function.into(), + file.into(), + file.into(), + ]) + } + /// Generate a .demangled.c file from the .c file using the `prettyName`s from the symbol table /// /// Currently, only top-level function names and (most) type names are demangled. diff --git a/kani-driver/src/metadata.rs b/kani-driver/src/metadata.rs index 871be621c6b0..a1751b7d11ee 100644 --- a/kani-driver/src/metadata.rs +++ b/kani-driver/src/metadata.rs @@ -184,6 +184,7 @@ pub fn mock_proof_harness( original_end_line: 0, attributes: HarnessAttributes { unwind_value, proof: true, ..Default::default() }, goto_file: model_file, + contract_to_enforce: None, } } diff --git a/kani_metadata/src/harness.rs b/kani_metadata/src/harness.rs index 2aadc70e9468..be98f64a2a63 100644 --- a/kani_metadata/src/harness.rs +++ b/kani_metadata/src/harness.rs @@ -24,6 +24,8 @@ pub struct HarnessMetadata { pub goto_file: Option, /// The `#[kani::<>]` attributes added to a harness. pub attributes: HarnessAttributes, + /// The names of functions for which contracts should be enforced + pub contract_to_enforce: Option, } /// The attributes added by the user to control how a harness is executed. diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index 5ab09d69f9bb..71a0d58d03ef 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -65,6 +65,11 @@ pub fn assume(cond: bool) { assert!(cond, "`kani::assume` should always hold"); } +/// If the `premise` is true, so must be the `conclusion` +pub fn implies(premise: bool, conclusion: bool) -> bool { + !premise || conclusion +} + /// Creates an assertion of the specified condition and message. /// /// # Example: diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 6cded7052369..2f090d6c2db2 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -89,10 +89,37 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream { derive::expand_derive_arbitrary(item) } +/// Add a precondition to this function. +/// +/// This is part of the function contract API, together with [`ensures`]. +/// +/// The contents of the attribute is a condition over the input values to the +/// annotated function. All Rust syntax is supported, even calling other +/// functions, but the computations must be side effect free, e.g. it cannot +/// perform I/O or use mutable memory. +#[proc_macro_attribute] +pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream { + attr_impl::requires(attr, item) +} + +/// Add a postcondition to this function. +/// +/// This is part of the function contract API, together with [`requires`]. +/// +/// The contents of the attribute is a condition over the input values to the +/// annotated function *and* its return value, accessible as a variable called +/// `result`. All Rust syntax is supported, even calling other functions, but +/// the computations must be side effect free, e.g. it cannot perform I/O or use +/// mutable memory. +#[proc_macro_attribute] +pub fn ensures(attr: TokenStream, item: TokenStream) -> TokenStream { + attr_impl::ensures(attr, item) +} /// This module implements Kani attributes in a way that only Kani's compiler can understand. /// This code should only be activated when pre-building Kani's sysroot. #[cfg(kani_sysroot)] mod sysroot { + use super::*; use { @@ -100,6 +127,29 @@ mod sysroot { syn::{parse_macro_input, ItemFn}, }; + use proc_macro2::Ident; + + /// Create a unique hash for a token stream (basically a [`std::hash::Hash`] + /// impl for `proc_macro2::TokenStream`). + fn hash_of_token_stream( + hasher: &mut H, + stream: proc_macro2::TokenStream, + ) { + use proc_macro2::TokenTree; + use std::hash::Hash; + for token in stream { + match token { + TokenTree::Ident(i) => i.hash(hasher), + TokenTree::Punct(p) => p.as_char().hash(hasher), + TokenTree::Group(g) => { + std::mem::discriminant(&g.delimiter()).hash(hasher); + hash_of_token_stream(hasher, g.stream()); + } + TokenTree::Literal(lit) => lit.to_string().hash(hasher), + } + } + } + /// Annotate the harness with a #[kanitool::] with optional arguments. macro_rules! kani_attribute { ($name:ident) => { @@ -184,6 +234,121 @@ mod sysroot { } } + /// Rewrites function contract annotations (`requires`, `ensures`) by lifing + /// the condition into a separate function. As an example: (using `ensures`) + /// + /// ```ignore + /// #[kani::ensures(x < result)] + /// fn foo(x: u32) -> u32 { .. } + /// ``` + /// + /// Is rewritten to + /// + /// ```ignore + /// fn foo_ensures_(x: u32, result: u32) { + /// x < result + /// } + /// + /// #[kanitool::ensures = "foo_ensures_"] + /// fn foo(x: u32) -> u32 { .. } + /// ``` + /// + /// Note that CBMC's contracts always pass the return value (even for + /// `requires`) and so we also append it here. + /// + /// This macro is supposed to be called with the name of the procedural + /// macro it should generate, e.g. `requires_ensures(requires)` + fn handle_requires_ensures(name: &str, attr: TokenStream, item: TokenStream) -> TokenStream { + use proc_macro2::Span; + use syn::{ + punctuated::Punctuated, FnArg, Pat, PatIdent, PatType, ReturnType, Signature, Token, + Type, TypeTuple, + }; + let attr = proc_macro2::TokenStream::from(attr); + + let a_short_hash = short_hash_of_token_stream(&item); + + let item_fn @ ItemFn { sig, .. } = &parse_macro_input!(item as ItemFn); + let Signature { inputs, output, .. } = sig; + + let gen_fn_name = identifier_for_generated_function(item_fn, name, a_short_hash); + let attribute = format_ident!("{name}"); + let kani_attributes = quote!( + #[allow(dead_code)] + #[allow(unused_variables)] + #[kanitool::#attribute = stringify!(#gen_fn_name)] + ); + + let typ = match output { + ReturnType::Type(_, t) => t.clone(), + _ => Box::new( + TypeTuple { paren_token: Default::default(), elems: Punctuated::new() }.into(), + ), + }; + + let mut gen_fn_inputs = inputs.clone(); + gen_fn_inputs.push(FnArg::Typed(PatType { + attrs: vec![], + pat: Box::new(Pat::Ident(PatIdent { + attrs: vec![], + by_ref: None, + mutability: None, + ident: Ident::new("result", Span::call_site()), + subpat: None, + })), + colon_token: Token![:](Span::call_site()), + ty: typ, + })); + + assert!(sig.variadic.is_none(), "Variadic signatures are not supported"); + + let mut gen_sig = sig.clone(); + gen_sig.inputs = gen_fn_inputs; + gen_sig.output = + ReturnType::Type(Default::default(), Box::new(Type::Verbatim(quote!(bool)))); + gen_sig.ident = gen_fn_name; + + quote!( + #gen_sig { + #attr + } + + #kani_attributes + #item_fn + ) + .into() + } + + /// Hash this `TokenStream` and return an integer that is at most digits + /// long when hex formatted. + fn short_hash_of_token_stream(stream: &proc_macro::TokenStream) -> u64 { + use std::hash::Hasher; + let mut hasher = std::collections::hash_map::DefaultHasher::default(); + hash_of_token_stream(&mut hasher, proc_macro2::TokenStream::from(stream.clone())); + let long_hash = hasher.finish(); + long_hash % 0x1_000_000 // six hex digits + } + + /// Makes consistent names for a generated function which was created for + /// `purpose`, from an attribute that decorates `related_function` with the + /// hash `hash`. + fn identifier_for_generated_function( + related_function: &ItemFn, + purpose: &str, + hash: u64, + ) -> Ident { + let identifier = format!("{}_{purpose}_{hash:x}", related_function.sig.ident); + Ident::new(&identifier, proc_macro2::Span::mixed_site()) + } + + pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream { + handle_requires_ensures("requires", attr, item) + } + + pub fn ensures(attr: TokenStream, item: TokenStream) -> TokenStream { + handle_requires_ensures("ensures", attr, item) + } + kani_attribute!(should_panic, no_args); kani_attribute!(solver); kani_attribute!(stub); @@ -221,4 +386,6 @@ mod regular { no_op!(stub); no_op!(unstable); no_op!(unwind); + no_op!(requires); + no_op!(ensures); } diff --git a/tests/expected/function-contract/arbitrary_ensures_fail.expected b/tests/expected/function-contract/arbitrary_ensures_fail.expected new file mode 100644 index 000000000000..d9244895bed8 --- /dev/null +++ b/tests/expected/function-contract/arbitrary_ensures_fail.expected @@ -0,0 +1,3 @@ +arbitrary_ensures_fail::max.missing_definition \ + - Status: FAILURE \ + - Description: "Function `arbitrary_ensures_fail::max` with missing definition is unreachable" \ diff --git a/tests/expected/function-contract/arbitrary_ensures_fail.rs b/tests/expected/function-contract/arbitrary_ensures_fail.rs new file mode 100644 index 000000000000..4ebbe16b5c02 --- /dev/null +++ b/tests/expected/function-contract/arbitrary_ensures_fail.rs @@ -0,0 +1,12 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::ensures(result == x)] +fn max(x: u32, y: u32) -> u32 { + if x > y { x } else { y } +} + +#[kani::proof] +fn main() { + max(kani::any(), kani::any()); +} diff --git a/tests/expected/function-contract/arbitrary_ensures_pass.expected b/tests/expected/function-contract/arbitrary_ensures_pass.expected new file mode 100644 index 000000000000..bad92983bd8d --- /dev/null +++ b/tests/expected/function-contract/arbitrary_ensures_pass.expected @@ -0,0 +1,3 @@ +arbitrary_ensures_pass::max.missing_definition\ + - Status: SUCCESS\ + - Description: "Function `arbitrary_ensures_pass::max` with missing definition is unreachable" \ No newline at end of file diff --git a/tests/expected/function-contract/arbitrary_ensures_pass.rs b/tests/expected/function-contract/arbitrary_ensures_pass.rs new file mode 100644 index 000000000000..63f975a62e4d --- /dev/null +++ b/tests/expected/function-contract/arbitrary_ensures_pass.rs @@ -0,0 +1,12 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::ensures(result == x || result == y)] +fn max(x: u32, y: u32) -> u32 { + if x > y { x } else { y } +} + +#[kani::proof] +fn main() { + max(kani::any(), kani::any()); +} diff --git a/tests/expected/function-contract/arbitrary_requires_fail.expected b/tests/expected/function-contract/arbitrary_requires_fail.expected new file mode 100644 index 000000000000..644bfc97aeb8 --- /dev/null +++ b/tests/expected/function-contract/arbitrary_requires_fail.expected @@ -0,0 +1,3 @@ +div.assertion \ + - Status: FAILURE \ + - Description: "attempt to divide by zero" \ No newline at end of file diff --git a/tests/expected/function-contract/arbitrary_requires_fail.rs b/tests/expected/function-contract/arbitrary_requires_fail.rs new file mode 100644 index 000000000000..526753673f57 --- /dev/null +++ b/tests/expected/function-contract/arbitrary_requires_fail.rs @@ -0,0 +1,11 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +fn div(dividend: u32, divisor: u32) -> u32 { + dividend / divisor +} + +#[kani::proof] +fn main() { + div(kani::any(), kani::any()); +} diff --git a/tests/expected/function-contract/arbitrary_requires_pass.expected b/tests/expected/function-contract/arbitrary_requires_pass.expected new file mode 100644 index 000000000000..6a5faa7e2b6c --- /dev/null +++ b/tests/expected/function-contract/arbitrary_requires_pass.expected @@ -0,0 +1,4 @@ +div.assertion \ + - Status: SUCCESS \ + - Description: "attempt to divide by zero" + diff --git a/tests/expected/function-contract/arbitrary_requires_pass.rs b/tests/expected/function-contract/arbitrary_requires_pass.rs new file mode 100644 index 000000000000..708968f261e8 --- /dev/null +++ b/tests/expected/function-contract/arbitrary_requires_pass.rs @@ -0,0 +1,12 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::requires(divisor != 0)] +fn div(dividend: u32, divisor: u32) -> u32 { + dividend / divisor +} + +#[kani::proof] +fn main() { + div(kani::any(), kani::any()); +} diff --git a/tests/expected/function-contract/double_requires.expected b/tests/expected/function-contract/double_requires.expected new file mode 100644 index 000000000000..d1894fad59d9 --- /dev/null +++ b/tests/expected/function-contract/double_requires.expected @@ -0,0 +1,9 @@ +double_requires::reduce1.missing_definition \ + - Status: FAILURE \ + - Description: "Function `double_requires::reduce1` with missing definition is unreachable" + +VERIFICATION:- FAILED + +double_requires::reduce2.missing_definition \ + - Status: FAILURE \ + - Description: "Function `double_requires::reduce2` with missing definition is unreachable" diff --git a/tests/expected/function-contract/double_requires.rs b/tests/expected/function-contract/double_requires.rs new file mode 100644 index 000000000000..e2f76d328f10 --- /dev/null +++ b/tests/expected/function-contract/double_requires.rs @@ -0,0 +1,26 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::ensures(result <= x || result == 1)] +#[kani::ensures(result != 0)] +#[kani::requires(x < u32::MAX)] +fn reduce1(x: u32, y: u32) -> u32 { + x + 1 +} + +#[kani::ensures(result <= x || result == 1)] +#[kani::ensures(result != 0)] +#[kani::requires(x < u32::MAX)] +fn reduce2(x: u32, y: u32) -> u32 { + x +} + +#[kani::proof] +fn main2() { + reduce2(kani::any(), kani::any()); +} + +#[kani::proof] +fn main() { + reduce1(kani::any(), kani::any()); +} diff --git a/tests/expected/function-contract/simple_ensures_fail.expected b/tests/expected/function-contract/simple_ensures_fail.expected new file mode 100644 index 000000000000..bd6e84b407ef --- /dev/null +++ b/tests/expected/function-contract/simple_ensures_fail.expected @@ -0,0 +1,3 @@ +simple_ensures_fail::max.missing_definition \ + - Status: FAILURE \ + - Description: "Function `simple_ensures_fail::max` with missing definition is unreachable" diff --git a/tests/expected/function-contract/simple_ensures_fail.rs b/tests/expected/function-contract/simple_ensures_fail.rs new file mode 100644 index 000000000000..b1e2132b6cbc --- /dev/null +++ b/tests/expected/function-contract/simple_ensures_fail.rs @@ -0,0 +1,12 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::ensures(result == x)] +fn max(x: u32, y: u32) -> u32 { + if x > y { x } else { y } +} + +#[kani::proof] +fn main() { + max(7, 9); +} diff --git a/tests/expected/function-contract/simple_ensures_pass.expected b/tests/expected/function-contract/simple_ensures_pass.expected new file mode 100644 index 000000000000..371c7539df24 --- /dev/null +++ b/tests/expected/function-contract/simple_ensures_pass.expected @@ -0,0 +1,3 @@ +simple_ensures_pass::max.missing_definition \ + - Status: SUCCESS \ + - Description: "Function `simple_ensures_pass::max` with missing definition is unreachable" diff --git a/tests/expected/function-contract/simple_ensures_pass.rs b/tests/expected/function-contract/simple_ensures_pass.rs new file mode 100644 index 000000000000..2a93964e1e83 --- /dev/null +++ b/tests/expected/function-contract/simple_ensures_pass.rs @@ -0,0 +1,12 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::ensures(result == x)] +fn max(x: u32, y: u32) -> u32 { + if x > y { x } else { y } +} + +#[kani::proof] +fn main() { + max(7, 6); +} diff --git a/tools/compiletest/src/runtest.rs b/tools/compiletest/src/runtest.rs index 59b79a24d8d9..71d723dceb59 100644 --- a/tools/compiletest/src/runtest.rs +++ b/tools/compiletest/src/runtest.rs @@ -375,7 +375,12 @@ impl<'test> TestCx<'test> { /// the expected output in `expected` file. fn run_expected_test(&self) { let proc_res = self.run_kani(); - let expected_path = self.testpaths.file.parent().unwrap().join("expected"); + let dot_expected_path = self.testpaths.file.with_extension("expected"); + let expected_path = if dot_expected_path.exists() { + dot_expected_path + } else { + self.testpaths.file.parent().unwrap().join("expected") + }; self.verify_output(&proc_res, &expected_path); } @@ -448,35 +453,22 @@ impl<'test> TestCx<'test> { consecutive_lines.clear(); } } - None + // Someone may add a `\` to the last line (probably by accident) but + // that would mean this test would succeed without actually testing so + // we add a check here again. + (!consecutive_lines.is_empty() && !TestCx::contains(str, &consecutive_lines)) + .then_some(consecutive_lines) } /// Check if there is a set of consecutive lines in `str` where each line /// contains a line from `lines` fn contains(str: &[&str], lines: &[&str]) -> bool { - let mut i = str.iter(); - while let Some(output_line) = i.next() { - if output_line.contains(&lines[0]) { - // Check if the rest of the lines in `lines` are contained in - // the subsequent lines in `str` - let mut matches = true; - // Clone the iterator so that we keep i unchanged - let mut j = i.clone(); - for line in lines.iter().skip(1) { - if let Some(output_line) = j.next() { - if output_line.contains(line) { - continue; - } - } - matches = false; - break; - } - if matches { - return true; - } - } - } - false + // Does *any* subslice of length `lines.len()` satisfy the containment of + // *all* `lines` + // `trim()` added to ignore trailing and preceding whitespace + str.windows(lines.len()).any(|subslice| { + subslice.iter().zip(lines).all(|(output, expected)| output.contains(expected.trim())) + }) } fn create_stamp(&self) {