From 201302f3eba2deddeeec88f2f70bf28965acc538 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 22 Jun 2023 12:36:05 -0700 Subject: [PATCH 01/22] Basic implementation for function contracts Adds pre- and postconditions --- cprover_bindings/src/goto_program/expr.rs | 6 + cprover_bindings/src/goto_program/mod.rs | 5 +- cprover_bindings/src/goto_program/symbol.rs | 28 ++++- .../src/goto_program/symbol_table.rs | 7 +- cprover_bindings/src/irep/irep.rs | 9 ++ cprover_bindings/src/irep/irep_id.rs | 2 + cprover_bindings/src/irep/to_irep.rs | 58 +++++++-- .../codegen_cprover_gotoc/codegen/function.rs | 65 +++++++++- .../codegen_cprover_gotoc/codegen/operand.rs | 4 +- .../compiler_interface.rs | 52 ++++++-- .../src/codegen_cprover_gotoc/mod.rs | 2 + .../src/codegen_cprover_gotoc/utils/mod.rs | 1 + .../src/codegen_cprover_gotoc/utils/names.rs | 40 ++++--- kani-compiler/src/kani_compiler.rs | 23 +++- kani-compiler/src/kani_middle/attributes.rs | 74 +++++++++++- kani-compiler/src/kani_middle/contracts.rs | 36 ++++++ kani-compiler/src/kani_middle/metadata.rs | 9 +- kani-compiler/src/kani_middle/mod.rs | 1 + kani-compiler/src/kani_middle/reachability.rs | 49 ++++++-- kani-driver/src/call_goto_instrument.rs | 14 +++ kani-driver/src/metadata.rs | 1 + kani_metadata/src/harness.rs | 2 + library/kani/src/lib.rs | 4 + library/kani_macros/src/lib.rs | 113 ++++++++++++++++++ .../arbitrary_ensures_fail.rs | 17 +++ .../arbitrary_ensures_pass.rs | 16 +++ .../FunctionContract/simple_ensures_fail.rs | 17 +++ .../FunctionContract/simple_ensures_pass.rs | 16 +++ 28 files changed, 615 insertions(+), 56 deletions(-) create mode 100644 kani-compiler/src/kani_middle/contracts.rs create mode 100644 tests/kani/FunctionContract/arbitrary_ensures_fail.rs create mode 100644 tests/kani/FunctionContract/arbitrary_ensures_pass.rs create mode 100644 tests/kani/FunctionContract/simple_ensures_fail.rs create mode 100644 tests/kani/FunctionContract/simple_ensures_pass.rs diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs index 3a6da89239b5..c52697b06fd2 100644 --- a/cprover_bindings/src/goto_program/expr.rs +++ b/cprover_bindings/src/goto_program/expr.rs @@ -170,6 +170,12 @@ pub enum ExprValue { }, } +#[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..33d9c8205391 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::{Contract, 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..54bef00ec73c 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,7 @@ pub struct Symbol { pub location: Location, pub typ: Type, pub value: SymbolValues, + pub contract: Option>, /// Optional debugging information @@ -44,6 +45,19 @@ pub struct Symbol { pub is_weak: bool, } +#[derive(Clone, Debug)] +pub struct Contract { + pub(crate) requires: Vec, + pub(crate) ensures: Vec, + pub(crate) assigns: Vec, +} + +impl Contract { + 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 +98,7 @@ impl Symbol { base_name, pretty_name, + contract: None, module: None, mode: SymbolModes::C, // global properties @@ -107,6 +122,17 @@ impl Symbol { } } + pub fn attach_contract(&mut self, contract: Contract) { + 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..9319afdbb667 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, Contract, 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,11 @@ 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: Contract) { + 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/irep_id.rs b/cprover_bindings/src/irep/irep_id.rs index 3ad8f71a7e86..cad6eb563bf4 100644 --- a/cprover_bindings/src/irep/irep_id.rs +++ b/cprover_bindings/src/irep/irep_id.rs @@ -593,6 +593,7 @@ pub enum IrepId { CSpecLoopInvariant, CSpecRequires, CSpecEnsures, + CSpecAssigns, VirtualFunction, ElementType, WorkingDirectory, @@ -1462,6 +1463,7 @@ impl ToString for IrepId { IrepId::CSpecLoopInvariant => "#spec_loop_invariant", IrepId::CSpecRequires => "#spec_requires", IrepId::CSpecEnsures => "#spec_ensures", + IrepId::CSpecAssigns => "#spec_assigns", IrepId::VirtualFunction => "virtual_function", IrepId::ElementType => "element_type", IrepId::WorkingDirectory => "working_directory", diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs index 70810e403c54..ced43700cbf6 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,45 @@ 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::just_sub(vec![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 { + for requires in &contract.requires { + typ = typ.with_named_sub(IrepId::CSpecRequires, requires.to_irep(mm)); + } + for ensures in &contract.ensures { + typ = typ.with_named_sub(IrepId::CSpecEnsures, ensures.to_irep(mm)); + } + for assigns in &contract.assigns { + typ = typ.with_named_sub(IrepId::CSpecAssigns, assigns.to_irep(mm)); + } + } 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..af94deda06df 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::{Contract, Expr, Lambda, Stmt, Symbol, Type}; use cbmc::InternString; use rustc_middle::mir::traversal::reverse_postorder; use rustc_middle::mir::{Body, HasLocalDecls, Local}; @@ -222,6 +223,68 @@ impl<'tcx> GotocCtx<'tcx> { ); } + /// 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>) -> Contract { + use rustc_middle::mir; + let mut handle_contract_expr = |instance| { + let mir = self.current_fn().mir(); + assert!(!mir.spread_arg.is_some()); + 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(); + Contract::new(requires, ensures, vec![]) + } + + 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..05db0cd96d52 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::{ @@ -81,11 +82,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 +121,18 @@ impl GotocCodegenBackend { } } + // 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 +193,7 @@ impl GotocCodegenBackend { } } - (gcx, items) + (gcx, items_with_contracts) } } @@ -238,8 +252,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 +276,30 @@ 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 functions_with_contracts = vec![]; + let items = items_with_contracts + .into_iter() + .map(|(i, contract)| { + if let Some(_) = contract { + let instance = match i { + MonoItem::Fn(f) => f, + _ => unreachable!(), + }; + functions_with_contracts.push(gcx.symbol_name(instance)) + } + 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.contracts = functions_with_contracts.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 +317,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..af0a04c04479 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,27 @@ impl<'tcx> GotocCtx<'tcx> { } } +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 } +} + +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..83de3f1adea4 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,8 @@ 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 contracts = contracts_for_harness(tcx, harness); + let metadata = gen_proof_metadata(tcx, def_id, &base_filename, contracts); let stub_map = harness_stub_map(tcx, def_id, &metadata); (def_path, HarnessInfo { metadata, stub_map }) }) @@ -320,6 +322,20 @@ impl KaniCompiler { } } +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 +426,7 @@ mod tests { original_end_line: 20, goto_file: None, attributes: HarnessAttributes::default(), + contracts: vec![], } } diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 6ee5136e12e5..4c71c04b5da2 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,68 @@ pub fn extract_harness_attributes(tcx: TyCtxt, def_id: DefId) -> HarnessAttribut // Internal attribute which shouldn't exist here. unreachable!() } + KaniAttributeKind::Ensures | KaniAttributeKind::Requires => { + todo!("Contract attributes are not supported on proofs (yet)") + } }; harness }) } +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() + }; + + //println!("Searching in {:?}", hir_map.module_items(enclosing_mod).map(|it| hir_map.item(it).ident.name).collect::>()); + + 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, vec![]) +} + /// 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..0bc9228b0d4c --- /dev/null +++ b/kani-compiler/src/kani_middle/contracts.rs @@ -0,0 +1,36 @@ +use rustc_hir::def_id::DefId; + +#[derive(Default)] +pub struct GFnContract { + requires: Vec, + ensures: Vec, + assigns: Vec, +} + +pub type FnContract = GFnContract; + +impl GFnContract { + pub fn requires(&self) -> &[C] { + &self.requires + } + + pub fn ensures(&self) -> &[C] { + &self.ensures + } + + pub fn new(requires: Vec, ensures: Vec, assigns: Vec) -> Self { + Self { requires, ensures, assigns } + } + + 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(), + assigns: self.assigns.iter().map(&mut f).collect(), + } + } + + 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..4ffbfd76e8f7 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, + contracts: Vec, +) -> 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), + contracts, } } @@ -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), + contracts: vec![], } } 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..580b145a9da1 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -16,7 +16,7 @@ use tracing::{debug, debug_span, trace, warn}; 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 +37,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 +64,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 +147,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 +158,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(), @@ -172,8 +175,32 @@ impl<'tcx> MonoItemsCollector<'tcx> { /// 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.collected.contains_key(&to_visit) { + let opt_contract = to_visit.def_id().as_local().and_then(|local_def_id| { + let substs = match to_visit { + 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 visit_obligations_from_contract = if let Some(contract) = opt_contract.as_ref() + { + [contract.requires(), contract.ensures()] + .into_iter() + .flat_map(IntoIterator::into_iter) + .copied() + .map(MonoItem::Fn) + .collect() + } else { + vec![] + }; + self.collected.insert(to_visit, opt_contract); let next_items = match to_visit { MonoItem::Fn(instance) => self.visit_fn(instance), MonoItem::Static(def_id) => self.visit_static(def_id), @@ -185,8 +212,12 @@ 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.queue.extend( + next_items + .into_iter() + .chain(visit_obligations_from_contract) + .filter(|item| !self.collected.contains_key(item)), + ); } } } diff --git a/kani-driver/src/call_goto_instrument.rs b/kani-driver/src/call_goto_instrument.rs index 8a97d9e15747..3a74eba0ea4e 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)?; } + for function in &harness.contracts { + self.enforce_contract(output, &function)?; + } + if self.args.checks.undefined_function_on() { self.add_library(output)?; self.undefined_functions(output)?; @@ -160,6 +164,16 @@ impl KaniSession { self.call_goto_instrument(args) } + pub fn enforce_contract(&self, file: &Path, function: &str) -> Result<()> { + println!("enforcing {function} 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..c10258c8aaa1 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, + contracts: vec![], } } diff --git a/kani_metadata/src/harness.rs b/kani_metadata/src/harness.rs index 2aadc70e9468..1f8812aa46ad 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, + + pub contracts: Vec, } /// 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..a3250626d542 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -65,6 +65,10 @@ pub fn assume(cond: bool) { assert!(cond, "`kani::assume` should always hold"); } +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..28e36d4478ee 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -89,10 +89,20 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream { derive::expand_derive_arbitrary(item) } +#[proc_macro_attribute] +pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream { + attr_impl::requires(attr, item) +} + +#[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 +110,27 @@ mod sysroot { syn::{parse_macro_input, ItemFn}, }; + use proc_macro2::Ident; + + 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 +215,86 @@ mod sysroot { } } + macro_rules! requires_ensures { + ($name: ident) => { + pub fn $name(attr: TokenStream, item: TokenStream) -> TokenStream { + use syn::{FnArg, PatType, PatIdent, Pat, Signature, Token, ReturnType, TypeTuple, punctuated::Punctuated, Type}; + use proc_macro2::Span; + 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, stringify!($name), a_short_hash); + let attribute = format_ident!("{}", stringify!($name)); + let kani_attributes = quote!( + #[allow(dead_code)] + #[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(), "Varaidic 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() + } + } + } + + 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 + } + + 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()) + } + + requires_ensures!(requires); + requires_ensures!(ensures); + kani_attribute!(should_panic, no_args); kani_attribute!(solver); kani_attribute!(stub); @@ -221,4 +332,6 @@ mod regular { no_op!(stub); no_op!(unstable); no_op!(unwind); + no_op!(requires); + no_op!(ensures); } diff --git a/tests/kani/FunctionContract/arbitrary_ensures_fail.rs b/tests/kani/FunctionContract/arbitrary_ensures_fail.rs new file mode 100644 index 000000000000..f03a497aa4e7 --- /dev/null +++ b/tests/kani/FunctionContract/arbitrary_ensures_fail.rs @@ -0,0 +1,17 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-verify-fail + +#[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()); +} \ No newline at end of file diff --git a/tests/kani/FunctionContract/arbitrary_ensures_pass.rs b/tests/kani/FunctionContract/arbitrary_ensures_pass.rs new file mode 100644 index 000000000000..8f00622316c4 --- /dev/null +++ b/tests/kani/FunctionContract/arbitrary_ensures_pass.rs @@ -0,0 +1,16 @@ +// 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()); +} \ No newline at end of file diff --git a/tests/kani/FunctionContract/simple_ensures_fail.rs b/tests/kani/FunctionContract/simple_ensures_fail.rs new file mode 100644 index 000000000000..e1bfa8f57342 --- /dev/null +++ b/tests/kani/FunctionContract/simple_ensures_fail.rs @@ -0,0 +1,17 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-verify-fail + +#[kani::ensures(result == x)] +fn max(x: u32, y: u32) -> u32 { + if x > y { + x + } else { + y + } +} + +#[kani::proof] +fn main() { + max(7, 9); +} \ No newline at end of file diff --git a/tests/kani/FunctionContract/simple_ensures_pass.rs b/tests/kani/FunctionContract/simple_ensures_pass.rs new file mode 100644 index 000000000000..5cb4c8ac7b9d --- /dev/null +++ b/tests/kani/FunctionContract/simple_ensures_pass.rs @@ -0,0 +1,16 @@ +// 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); +} \ No newline at end of file From b400f1c55df7b305648cdf69ea60d4d32af308cc Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 22 Jun 2023 13:20:48 -0700 Subject: [PATCH 02/22] Documentation --- cprover_bindings/src/goto_program/expr.rs | 3 ++ cprover_bindings/src/goto_program/symbol.rs | 7 +++ .../codegen_cprover_gotoc/codegen/function.rs | 22 ++++++++++ .../src/codegen_cprover_gotoc/utils/names.rs | 2 + kani-compiler/src/kani_compiler.rs | 1 + kani-compiler/src/kani_middle/attributes.rs | 7 +++ kani-compiler/src/kani_middle/contracts.rs | 8 ++++ kani-driver/src/call_goto_instrument.rs | 1 + library/kani/src/lib.rs | 1 + library/kani_macros/src/lib.rs | 43 +++++++++++++++++++ 10 files changed, 95 insertions(+) diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs index c52697b06fd2..909875258ccc 100644 --- a/cprover_bindings/src/goto_program/expr.rs +++ b/cprover_bindings/src/goto_program/expr.rs @@ -170,6 +170,9 @@ pub enum ExprValue { }, } +/// The equivalent of a "mathematical function" in CBMC but spiritually it is more like a function object. +/// +/// This is only used to implement function contracts and values of this sort are otherwise not constructible. #[derive(Debug, Clone)] pub struct Lambda { pub arguments: Vec<(InternedString, Type)>, diff --git a/cprover_bindings/src/goto_program/symbol.rs b/cprover_bindings/src/goto_program/symbol.rs index 54bef00ec73c..a4b792ecd5f6 100644 --- a/cprover_bindings/src/goto_program/symbol.rs +++ b/cprover_bindings/src/goto_program/symbol.rs @@ -13,6 +13,7 @@ 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 @@ -45,6 +46,9 @@ 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 Contract { pub(crate) requires: Vec, @@ -122,7 +126,10 @@ 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: Contract) { + assert!(self.typ.is_code()); match self.contract { Some(ref mut prior) => { prior.assigns.extend(contract.assigns); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index af94deda06df..5ca768d5e033 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -223,6 +223,24 @@ 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 @@ -271,6 +289,10 @@ impl<'tcx> GotocCtx<'tcx> { Contract::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>, diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs index af0a04c04479..baba473db397 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs @@ -87,6 +87,7 @@ 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!( @@ -104,6 +105,7 @@ pub fn symbol_name_for_instance<'tcx>(tcx: TyCtxt<'tcx>, instance: Instance<'tcx 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)) } diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index 83de3f1adea4..0cf17751ca0b 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/kani-compiler/src/kani_compiler.rs @@ -322,6 +322,7 @@ 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() diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 4c71c04b5da2..6235dcea38ba 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -156,6 +156,13 @@ pub fn extract_harness_attributes(tcx: TyCtxt, def_id: DefId) -> HarnessAttribut }) } +/// 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}; diff --git a/kani-compiler/src/kani_middle/contracts.rs b/kani-compiler/src/kani_middle/contracts.rs index 0bc9228b0d4c..95dfd2bba8bf 100644 --- a/kani-compiler/src/kani_middle/contracts.rs +++ b/kani-compiler/src/kani_middle/contracts.rs @@ -1,5 +1,8 @@ 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, @@ -10,10 +13,12 @@ pub struct GFnContract { 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 } @@ -22,6 +27,8 @@ impl GFnContract { Self { requires, ensures, assigns } } + /// 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(), @@ -30,6 +37,7 @@ impl GFnContract { } } + /// 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-driver/src/call_goto_instrument.rs b/kani-driver/src/call_goto_instrument.rs index 3a74eba0ea4e..7be64a4df719 100644 --- a/kani-driver/src/call_goto_instrument.rs +++ b/kani-driver/src/call_goto_instrument.rs @@ -164,6 +164,7 @@ impl KaniSession { self.call_goto_instrument(args) } + /// Make CBMC enforce a function contract. pub fn enforce_contract(&self, file: &Path, function: &str) -> Result<()> { println!("enforcing {function} contract"); self.call_goto_instrument(vec![ diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index a3250626d542..71a0d58d03ef 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -65,6 +65,7 @@ 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 } diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 28e36d4478ee..70e4af321b32 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -89,11 +89,28 @@ 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 condtition 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 condtition 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) @@ -112,6 +129,8 @@ mod sysroot { 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, @@ -215,6 +234,30 @@ mod sysroot { } } + /// Rewrites function contract annotations (`requires`, `ensures`) by lifing + /// the condition into a separate function. As an example: (using `ensures`) + /// + /// ```rs + /// #[kani::ensures(x < result)] + /// fn foo(x: u32) -> u32 { .. } + /// ``` + /// + /// Is rewritten to + /// + /// ```rs + /// fn foo_enusres_(x: u32, result: u32) { + /// x < result + /// } + /// + /// #[kanitook::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)` macro_rules! requires_ensures { ($name: ident) => { pub fn $name(attr: TokenStream, item: TokenStream) -> TokenStream { From c69bf06ca362c2abdc25f4754e294ebb58b86c49 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 22 Jun 2023 14:30:33 -0700 Subject: [PATCH 03/22] Formatting for tests --- tests/kani/FunctionContract/arbitrary_ensures_fail.rs | 8 ++------ tests/kani/FunctionContract/arbitrary_ensures_pass.rs | 8 ++------ tests/kani/FunctionContract/simple_ensures_fail.rs | 8 ++------ tests/kani/FunctionContract/simple_ensures_pass.rs | 8 ++------ 4 files changed, 8 insertions(+), 24 deletions(-) diff --git a/tests/kani/FunctionContract/arbitrary_ensures_fail.rs b/tests/kani/FunctionContract/arbitrary_ensures_fail.rs index f03a497aa4e7..1788538b9254 100644 --- a/tests/kani/FunctionContract/arbitrary_ensures_fail.rs +++ b/tests/kani/FunctionContract/arbitrary_ensures_fail.rs @@ -4,14 +4,10 @@ #[kani::ensures(result == x)] fn max(x: u32, y: u32) -> u32 { - if x > y { - x - } else { - y - } + if x > y { x } else { y } } #[kani::proof] fn main() { max(kani::any(), kani::any()); -} \ No newline at end of file +} diff --git a/tests/kani/FunctionContract/arbitrary_ensures_pass.rs b/tests/kani/FunctionContract/arbitrary_ensures_pass.rs index 8f00622316c4..63f975a62e4d 100644 --- a/tests/kani/FunctionContract/arbitrary_ensures_pass.rs +++ b/tests/kani/FunctionContract/arbitrary_ensures_pass.rs @@ -3,14 +3,10 @@ #[kani::ensures(result == x || result == y)] fn max(x: u32, y: u32) -> u32 { - if x > y { - x - } else { - y - } + if x > y { x } else { y } } #[kani::proof] fn main() { max(kani::any(), kani::any()); -} \ No newline at end of file +} diff --git a/tests/kani/FunctionContract/simple_ensures_fail.rs b/tests/kani/FunctionContract/simple_ensures_fail.rs index e1bfa8f57342..0ee61c78bc7a 100644 --- a/tests/kani/FunctionContract/simple_ensures_fail.rs +++ b/tests/kani/FunctionContract/simple_ensures_fail.rs @@ -4,14 +4,10 @@ #[kani::ensures(result == x)] fn max(x: u32, y: u32) -> u32 { - if x > y { - x - } else { - y - } + if x > y { x } else { y } } #[kani::proof] fn main() { max(7, 9); -} \ No newline at end of file +} diff --git a/tests/kani/FunctionContract/simple_ensures_pass.rs b/tests/kani/FunctionContract/simple_ensures_pass.rs index 5cb4c8ac7b9d..2a93964e1e83 100644 --- a/tests/kani/FunctionContract/simple_ensures_pass.rs +++ b/tests/kani/FunctionContract/simple_ensures_pass.rs @@ -3,14 +3,10 @@ #[kani::ensures(result == x)] fn max(x: u32, y: u32) -> u32 { - if x > y { - x - } else { - y - } + if x > y { x } else { y } } #[kani::proof] fn main() { max(7, 6); -} \ No newline at end of file +} From 46069ef8d459770d1159f65a74916fdbc54c72c5 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 22 Jun 2023 16:10:54 -0700 Subject: [PATCH 04/22] Hopefully fixing clippy suggestions --- kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs | 2 +- .../src/codegen_cprover_gotoc/compiler_interface.rs | 6 ++++-- kani-compiler/src/kani_middle/attributes.rs | 2 +- kani-compiler/src/kani_middle/contracts.rs | 3 +++ kani-compiler/src/kani_middle/reachability.rs | 6 ++++-- 5 files changed, 13 insertions(+), 6 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index 5ca768d5e033..e599e17dd246 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -251,7 +251,7 @@ impl<'tcx> GotocCtx<'tcx> { use rustc_middle::mir; let mut handle_contract_expr = |instance| { let mir = self.current_fn().mir(); - assert!(!mir.spread_arg.is_some()); + 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)) diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 05db0cd96d52..279c1bcf69f0 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -70,6 +70,8 @@ pub struct GotocCodegenBackend { queries: Arc>, } +type MonoContract<'tcx> = GFnContract>; + impl GotocCodegenBackend { pub fn new(queries: Arc>) -> Self { GotocCodegenBackend { queries } @@ -82,7 +84,7 @@ impl GotocCodegenBackend { starting_items: &[MonoItem<'tcx>], symtab_goto: &Path, machine_model: &MachineModel, - ) -> (GotocCtx<'tcx>, Vec<(MonoItem<'tcx>, Option>>)>) { + ) -> (GotocCtx<'tcx>, Vec<(MonoItem<'tcx>, Option>)>) { let items_with_contracts = with_timer( || collect_reachable_items(tcx, starting_items), "codegen reachability analysis", @@ -282,7 +284,7 @@ impl CodegenBackend for GotocCodegenBackend { let items = items_with_contracts .into_iter() .map(|(i, contract)| { - if let Some(_) = contract { + if contract.is_some() { let instance = match i { MonoItem::Fn(f) => f, _ => unreachable!(), diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 6235dcea38ba..2f3f5d07138a 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -175,7 +175,7 @@ pub fn extract_contract(tcx: TyCtxt, local_def_id: LocalDefId) -> super::contrac match hir_map.get_parent(hir_id) { Node::Item(Item { kind, .. }) => match kind { - ItemKind::Mod(m) => find_in_mod(*m), + ItemKind::Mod(m) => find_in_mod(m), ItemKind::Impl(imp) => { imp.items.iter().find(|it| it.ident.name == name).unwrap().id.hir_id() } diff --git a/kani-compiler/src/kani_middle/contracts.rs b/kani-compiler/src/kani_middle/contracts.rs index 95dfd2bba8bf..4ae642b2d90c 100644 --- a/kani-compiler/src/kani_middle/contracts.rs +++ b/kani-compiler/src/kani_middle/contracts.rs @@ -1,3 +1,6 @@ +// 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 diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 580b145a9da1..95712d078b68 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -15,6 +15,8 @@ //! 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::{FxHashMap, FxHashSet}; use rustc_data_structures::stable_hasher::{HashStable, StableHasher}; @@ -175,7 +177,7 @@ impl<'tcx> MonoItemsCollector<'tcx> { /// 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_key(&to_visit) { + if let Entry::Vacant(e) = self.collected.entry(to_visit) { let opt_contract = to_visit.def_id().as_local().and_then(|local_def_id| { let substs = match to_visit { MonoItem::Fn(inst) => inst.substs, @@ -200,7 +202,7 @@ impl<'tcx> MonoItemsCollector<'tcx> { } else { vec![] }; - self.collected.insert(to_visit, opt_contract); + e.insert(opt_contract); let next_items = match to_visit { MonoItem::Fn(instance) => self.visit_fn(instance), MonoItem::Static(def_id) => self.visit_static(def_id), From 95fe43cfcd817642bca58bb1996747375e851117 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Wed, 28 Jun 2023 11:38:22 -0700 Subject: [PATCH 05/22] Update library/kani_macros/src/lib.rs Co-authored-by: Celina G. Val --- library/kani_macros/src/lib.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 70e4af321b32..ab8035e04b19 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -106,7 +106,7 @@ pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream { /// /// This is part of the function contract API, together with [`requires`]. /// -/// The contents of the attribute is a condtition over the input values to the +/// 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 From 7ef5a587b930de8b9fb8e8bc5582d8379adcffb9 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Wed, 28 Jun 2023 12:10:30 -0700 Subject: [PATCH 06/22] Apply suggestions from code review Co-authored-by: Celina G. Val --- library/kani_macros/src/lib.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index ab8035e04b19..aab58a698ff4 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -93,7 +93,7 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream { /// /// This is part of the function contract API, together with [`ensures`]. /// -/// The contents of the attribute is a condtition over the input values to the +/// 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. @@ -245,11 +245,11 @@ mod sysroot { /// Is rewritten to /// /// ```rs - /// fn foo_enusres_(x: u32, result: u32) { + /// fn foo_ensures_(x: u32, result: u32) { /// x < result /// } /// - /// #[kanitook::ensures = "foo_ensures_"] + /// #[kanitool::ensures = "foo_ensures_"] /// fn foo(x: u32) -> u32 { .. } /// ``` /// From c02f1713db4b6e4e7a4418706fc4609d67fbc2f2 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Wed, 28 Jun 2023 12:10:35 -0700 Subject: [PATCH 07/22] Addressing comments Added `requires` test case Made tests `expected` tests Changes `requires_ensures` macro to function --- cprover_bindings/src/goto_program/expr.rs | 11 +- cprover_bindings/src/goto_program/mod.rs | 2 +- cprover_bindings/src/goto_program/symbol.rs | 8 +- .../src/goto_program/symbol_table.rs | 8 +- .../codegen_cprover_gotoc/codegen/function.rs | 6 +- .../compiler_interface.rs | 5 +- library/kani_macros/src/lib.rs | 124 ++++++++++-------- .../arbitrary_ensures_fail.expected | 5 + .../arbitrary_ensures_fail.rs | 0 .../arbitrary_ensures_pass.expected | 5 + .../arbitrary_ensures_pass.rs | 0 .../arbitrary_requires_fail.expected | 10 ++ .../arbitrary_requires_fail.rs | 12 ++ .../arbitrary_requires_pass.expected | 10 ++ .../arbitrary_requires_pass.rs | 12 ++ .../simple_ensures_fail.expected | 5 + .../function-contract}/simple_ensures_fail.rs | 0 .../simple_ensures_pass.expected | 5 + .../function-contract}/simple_ensures_pass.rs | 0 19 files changed, 157 insertions(+), 71 deletions(-) create mode 100644 tests/expected/function-contract/arbitrary_ensures_fail.expected rename tests/{kani/FunctionContract => expected/function-contract}/arbitrary_ensures_fail.rs (100%) create mode 100644 tests/expected/function-contract/arbitrary_ensures_pass.expected rename tests/{kani/FunctionContract => expected/function-contract}/arbitrary_ensures_pass.rs (100%) create mode 100644 tests/expected/function-contract/arbitrary_requires_fail.expected create mode 100644 tests/expected/function-contract/arbitrary_requires_fail.rs create mode 100644 tests/expected/function-contract/arbitrary_requires_pass.expected create mode 100644 tests/expected/function-contract/arbitrary_requires_pass.rs create mode 100644 tests/expected/function-contract/simple_ensures_fail.expected rename tests/{kani/FunctionContract => expected/function-contract}/simple_ensures_fail.rs (100%) create mode 100644 tests/expected/function-contract/simple_ensures_pass.expected rename tests/{kani/FunctionContract => expected/function-contract}/simple_ensures_pass.rs (100%) diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs index 909875258ccc..2f92a3b83b17 100644 --- a/cprover_bindings/src/goto_program/expr.rs +++ b/cprover_bindings/src/goto_program/expr.rs @@ -170,9 +170,16 @@ pub enum ExprValue { }, } -/// The equivalent of a "mathematical function" in CBMC but spiritually it is more like a function object. +/// 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 used to implement function contracts and values of this sort are otherwise not constructible. +/// 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)>, diff --git a/cprover_bindings/src/goto_program/mod.rs b/cprover_bindings/src/goto_program/mod.rs index 33d9c8205391..d8987b6df738 100644 --- a/cprover_bindings/src/goto_program/mod.rs +++ b/cprover_bindings/src/goto_program/mod.rs @@ -23,6 +23,6 @@ pub use expr::{ }; pub use location::Location; pub use stmt::{Stmt, StmtBody, SwitchCase}; -pub use symbol::{Contract, 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 a4b792ecd5f6..fd1d76328ac5 100644 --- a/cprover_bindings/src/goto_program/symbol.rs +++ b/cprover_bindings/src/goto_program/symbol.rs @@ -14,7 +14,7 @@ pub struct Symbol { pub typ: Type, pub value: SymbolValues, /// Contracts to be enforced (only supported for functions) - pub contract: Option>, + pub contract: Option>, /// Optional debugging information @@ -50,13 +50,13 @@ pub struct Symbol { /// See https://diffblue.github.io/cbmc/contracts-user.html for the meaning of /// each type of clause. #[derive(Clone, Debug)] -pub struct Contract { +pub struct FunctionContract { pub(crate) requires: Vec, pub(crate) ensures: Vec, pub(crate) assigns: Vec, } -impl Contract { +impl FunctionContract { pub fn new(requires: Vec, ensures: Vec, assigns: Vec) -> Self { Self { requires, ensures, assigns } } @@ -128,7 +128,7 @@ 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: Contract) { + pub fn attach_contract(&mut self, contract: FunctionContract) { assert!(self.typ.is_code()); match self.contract { Some(ref mut prior) => { diff --git a/cprover_bindings/src/goto_program/symbol_table.rs b/cprover_bindings/src/goto_program/symbol_table.rs index 9319afdbb667..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, Contract, 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: @@ -80,7 +80,11 @@ impl SymbolTable { self.symbol_table.get_mut(&name).unwrap().update_fn_declaration_with_definition(body); } - pub fn attach_contract>(&mut self, name: T, contract: Contract) { + pub fn attach_contract>( + &mut self, + name: T, + contract: FunctionContract, + ) { let sym = self.symbol_table.get_mut(&name.into()).unwrap(); sym.attach_contract(contract); } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index e599e17dd246..fcb5b2ed920d 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -5,7 +5,7 @@ use crate::codegen_cprover_gotoc::GotocCtx; use crate::kani_middle::contracts::GFnContract; -use cbmc::goto_program::{Contract, Expr, Lambda, Stmt, Symbol, Type}; +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}; @@ -247,7 +247,7 @@ impl<'tcx> GotocCtx<'tcx> { /// 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>) -> Contract { + 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(); @@ -286,7 +286,7 @@ impl<'tcx> GotocCtx<'tcx> { fn_contract.requires().iter().copied().map(&mut handle_contract_expr).collect(); let ensures = fn_contract.ensures().iter().copied().map(&mut handle_contract_expr).collect(); - Contract::new(requires, ensures, vec![]) + FunctionContract::new(requires, ensures, vec![]) } /// Convert the contract to a CBMC contract, then attach it to `instance`. diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 279c1bcf69f0..099c0ac819b8 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -123,8 +123,9 @@ impl GotocCodegenBackend { } } - // Gets its own loop, because the functions used in the contract - // expressions must have been declared before + // 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 { diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index aab58a698ff4..fd4094efe208 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -237,14 +237,14 @@ mod sysroot { /// Rewrites function contract annotations (`requires`, `ensures`) by lifing /// the condition into a separate function. As an example: (using `ensures`) /// - /// ```rs + /// ```ignore /// #[kani::ensures(x < result)] /// fn foo(x: u32) -> u32 { .. } /// ``` /// /// Is rewritten to /// - /// ```rs + /// ```ignore /// fn foo_ensures_(x: u32, result: u32) { /// x < result /// } @@ -258,66 +258,68 @@ mod sysroot { /// /// This macro is supposed to be called with the name of the procedural /// macro it should generate, e.g. `requires_ensures(requires)` - macro_rules! requires_ensures { - ($name: ident) => { - pub fn $name(attr: TokenStream, item: TokenStream) -> TokenStream { - use syn::{FnArg, PatType, PatIdent, Pat, Signature, Token, ReturnType, TypeTuple, punctuated::Punctuated, Type}; - use proc_macro2::Span; - let attr = proc_macro2::TokenStream::from(attr); + 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 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 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, stringify!($name), a_short_hash); - let attribute = format_ident!("{}", stringify!($name)); - let kani_attributes = quote!( - #[allow(dead_code)] - #[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(), "Varaidic 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; + 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)] + #[kanitool::#attribute = stringify!(#gen_fn_name)] + ); - quote!( - #gen_sig { - #attr - } - - #kani_attributes - #item_fn - ) - .into() + 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(); @@ -326,6 +328,9 @@ mod sysroot { 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, @@ -335,8 +340,13 @@ mod sysroot { Ident::new(&identifier, proc_macro2::Span::mixed_site()) } - requires_ensures!(requires); - requires_ensures!(ensures); + 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); 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..22af34a550eb --- /dev/null +++ b/tests/expected/function-contract/arbitrary_ensures_fail.expected @@ -0,0 +1,5 @@ +RESULTS: +Check 1: arbitrary_ensures_fail::max.missing_definition.1 + - Status: FAILURE + - Description: "Function `arbitrary_ensures_fail::max` with missing definition is unreachable" + - Location: Unknown file in function arbitrary_ensures_fail::max diff --git a/tests/kani/FunctionContract/arbitrary_ensures_fail.rs b/tests/expected/function-contract/arbitrary_ensures_fail.rs similarity index 100% rename from tests/kani/FunctionContract/arbitrary_ensures_fail.rs rename to tests/expected/function-contract/arbitrary_ensures_fail.rs 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..04c42f9cc2e6 --- /dev/null +++ b/tests/expected/function-contract/arbitrary_ensures_pass.expected @@ -0,0 +1,5 @@ +RESULTS: +Check 1: arbitrary_ensures_pass::max.missing_definition.1 + - Status: SUCCESS + - Description: "Function `arbitrary_ensures_pass::max` with missing definition is unreachable" + - Location: Unknown file in function arbitrary_ensures_pass::max diff --git a/tests/kani/FunctionContract/arbitrary_ensures_pass.rs b/tests/expected/function-contract/arbitrary_ensures_pass.rs similarity index 100% rename from tests/kani/FunctionContract/arbitrary_ensures_pass.rs rename to tests/expected/function-contract/arbitrary_ensures_pass.rs 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..6b9a8e3d4bfb --- /dev/null +++ b/tests/expected/function-contract/arbitrary_requires_fail.expected @@ -0,0 +1,10 @@ +RESULTS: +Check 1: div.assertion.1 + - Status: FAILURE + - Description: "attempt to divide by zero" + - Location: arbitrary_requires_fail.rs:6:5 in function div + +Check 2: div.division-by-zero.1 + - Status: SUCCESS + - Description: "division by zero" + - Location: arbitrary_requires_fail.rs:6:5 in function div 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..9491788fc564 --- /dev/null +++ b/tests/expected/function-contract/arbitrary_requires_fail.rs @@ -0,0 +1,12 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-verify-fail + +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..e4033b162c0a --- /dev/null +++ b/tests/expected/function-contract/arbitrary_requires_pass.expected @@ -0,0 +1,10 @@ +RESULTS: +Check 1: div.assertion.1 + - Status: SUCCESS + - Description: "attempt to divide by zero" + - Location: arbitrary_requires_pass.rs:6:5 in function div + +Check 2: div.division-by-zero.1 + - Status: SUCCESS + - Description: "division by zero" + - Location: arbitrary_requires_pass.rs:6:5 in function div 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/simple_ensures_fail.expected b/tests/expected/function-contract/simple_ensures_fail.expected new file mode 100644 index 000000000000..41b151c49ac4 --- /dev/null +++ b/tests/expected/function-contract/simple_ensures_fail.expected @@ -0,0 +1,5 @@ +RESULTS: +Check 1: simple_ensures_fail::max.missing_definition.1 + - Status: FAILURE + - Description: "Function `simple_ensures_fail::max` with missing definition is unreachable" + - Location: Unknown file in function simple_ensures_fail::max diff --git a/tests/kani/FunctionContract/simple_ensures_fail.rs b/tests/expected/function-contract/simple_ensures_fail.rs similarity index 100% rename from tests/kani/FunctionContract/simple_ensures_fail.rs rename to tests/expected/function-contract/simple_ensures_fail.rs 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..3b26315ec354 --- /dev/null +++ b/tests/expected/function-contract/simple_ensures_pass.expected @@ -0,0 +1,5 @@ +RESULTS: +Check 1: simple_ensures_pass::max.missing_definition.1 + - Status: SUCCESS + - Description: "Function `simple_ensures_pass::max` with missing definition is unreachable" + - Location: Unknown file in function simple_ensures_pass::max diff --git a/tests/kani/FunctionContract/simple_ensures_pass.rs b/tests/expected/function-contract/simple_ensures_pass.rs similarity index 100% rename from tests/kani/FunctionContract/simple_ensures_pass.rs rename to tests/expected/function-contract/simple_ensures_pass.rs From bed5def0cd2e155bbfe27d739c138f389dcd0743 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Wed, 28 Jun 2023 15:08:34 -0700 Subject: [PATCH 08/22] Fixing regression test setup --- tests/expected/function-contract/arbitrary_ensures_fail.rs | 1 - tests/expected/function-contract/arbitrary_requires_fail.rs | 1 - tests/expected/function-contract/simple_ensures_fail.rs | 1 - 3 files changed, 3 deletions(-) diff --git a/tests/expected/function-contract/arbitrary_ensures_fail.rs b/tests/expected/function-contract/arbitrary_ensures_fail.rs index 1788538b9254..4ebbe16b5c02 100644 --- a/tests/expected/function-contract/arbitrary_ensures_fail.rs +++ b/tests/expected/function-contract/arbitrary_ensures_fail.rs @@ -1,6 +1,5 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-verify-fail #[kani::ensures(result == x)] fn max(x: u32, y: u32) -> u32 { diff --git a/tests/expected/function-contract/arbitrary_requires_fail.rs b/tests/expected/function-contract/arbitrary_requires_fail.rs index 9491788fc564..526753673f57 100644 --- a/tests/expected/function-contract/arbitrary_requires_fail.rs +++ b/tests/expected/function-contract/arbitrary_requires_fail.rs @@ -1,6 +1,5 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-verify-fail fn div(dividend: u32, divisor: u32) -> u32 { dividend / divisor diff --git a/tests/expected/function-contract/simple_ensures_fail.rs b/tests/expected/function-contract/simple_ensures_fail.rs index 0ee61c78bc7a..b1e2132b6cbc 100644 --- a/tests/expected/function-contract/simple_ensures_fail.rs +++ b/tests/expected/function-contract/simple_ensures_fail.rs @@ -1,6 +1,5 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-verify-fail #[kani::ensures(result == x)] fn max(x: u32, y: u32) -> u32 { From 38ca8cf9d041e9651b250a2488ef9aea9c0ab56f Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Wed, 28 Jun 2023 16:40:43 -0700 Subject: [PATCH 09/22] Fixing test cases and allowing multiple `.expected` files --- .../function-contract/arbitrary_requires_fail.expected | 2 -- .../function-contract/arbitrary_requires_pass.expected | 2 -- tools/compiletest/src/runtest.rs | 7 ++++++- 3 files changed, 6 insertions(+), 5 deletions(-) diff --git a/tests/expected/function-contract/arbitrary_requires_fail.expected b/tests/expected/function-contract/arbitrary_requires_fail.expected index 6b9a8e3d4bfb..132a7455f12d 100644 --- a/tests/expected/function-contract/arbitrary_requires_fail.expected +++ b/tests/expected/function-contract/arbitrary_requires_fail.expected @@ -2,9 +2,7 @@ RESULTS: Check 1: div.assertion.1 - Status: FAILURE - Description: "attempt to divide by zero" - - Location: arbitrary_requires_fail.rs:6:5 in function div Check 2: div.division-by-zero.1 - Status: SUCCESS - Description: "division by zero" - - Location: arbitrary_requires_fail.rs:6:5 in function div diff --git a/tests/expected/function-contract/arbitrary_requires_pass.expected b/tests/expected/function-contract/arbitrary_requires_pass.expected index e4033b162c0a..2a5317f904a4 100644 --- a/tests/expected/function-contract/arbitrary_requires_pass.expected +++ b/tests/expected/function-contract/arbitrary_requires_pass.expected @@ -2,9 +2,7 @@ RESULTS: Check 1: div.assertion.1 - Status: SUCCESS - Description: "attempt to divide by zero" - - Location: arbitrary_requires_pass.rs:6:5 in function div Check 2: div.division-by-zero.1 - Status: SUCCESS - Description: "division by zero" - - Location: arbitrary_requires_pass.rs:6:5 in function div diff --git a/tools/compiletest/src/runtest.rs b/tools/compiletest/src/runtest.rs index 59b79a24d8d9..946e8cd94712 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); } From 787e54403d1930230f91648b63dd17fdcdf399cf Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Mon, 10 Jul 2023 12:27:30 -0700 Subject: [PATCH 10/22] Update kani-driver/src/call_goto_instrument.rs Co-authored-by: Celina G. Val --- kani-driver/src/call_goto_instrument.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-driver/src/call_goto_instrument.rs b/kani-driver/src/call_goto_instrument.rs index 7be64a4df719..7f32b136ae28 100644 --- a/kani-driver/src/call_goto_instrument.rs +++ b/kani-driver/src/call_goto_instrument.rs @@ -166,7 +166,7 @@ impl KaniSession { /// Make CBMC enforce a function contract. pub fn enforce_contract(&self, file: &Path, function: &str) -> Result<()> { - println!("enforcing {function} contract"); + tracing::debug!(?function, "enforce_contract"); self.call_goto_instrument(vec![ "--enforce-contract".into(), function.into(), From e0f3e58007ca94bf5769dc6d1f92dae76c876a90 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Mon, 10 Jul 2023 12:12:08 -0700 Subject: [PATCH 11/22] Alloow only one contract at a time --- .../src/codegen_cprover_gotoc/compiler_interface.rs | 9 ++++++--- kani-compiler/src/kani_compiler.rs | 11 ++++++++--- kani-compiler/src/kani_middle/metadata.rs | 6 +++--- kani-driver/src/call_goto_instrument.rs | 2 +- kani-driver/src/metadata.rs | 2 +- kani_metadata/src/harness.rs | 4 ++-- 6 files changed, 21 insertions(+), 13 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 099c0ac819b8..d2d587fd3a81 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -281,7 +281,7 @@ impl CodegenBackend for GotocCodegenBackend { let model_path = base_filename.with_extension(ArtifactType::SymTabGoto); let (gcx, items_with_contracts) = self.codegen_items(tcx, &harnesses, &model_path, &results.machine_model); - let mut functions_with_contracts = vec![]; + let mut contract_function = None; let items = items_with_contracts .into_iter() .map(|(i, contract)| { @@ -290,7 +290,10 @@ impl CodegenBackend for GotocCodegenBackend { MonoItem::Fn(f) => f, _ => unreachable!(), }; - functions_with_contracts.push(gcx.symbol_name(instance)) + assert!( + contract_function.replace(gcx.symbol_name(instance)).is_none(), + "Only one function contract can be enforced at a time" + ); } i }) @@ -302,7 +305,7 @@ impl CodegenBackend for GotocCodegenBackend { if let MonoItem::Fn(instance) = test_fn { instance } else { continue }; let mut metadata = gen_test_metadata(tcx, *test_desc, *instance, &base_filename); - metadata.contracts = functions_with_contracts.clone(); + metadata.contract = 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 {}", diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index 0cf17751ca0b..353d38393c26 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/kani-compiler/src/kani_compiler.rs @@ -233,8 +233,13 @@ impl KaniCompiler { .map(|harness| { let def_id = harness.def_id(); let def_path = tcx.def_path_hash(def_id); - let contracts = contracts_for_harness(tcx, harness); - let metadata = gen_proof_metadata(tcx, def_id, &base_filename, contracts); + 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 }) }) @@ -427,7 +432,7 @@ mod tests { original_end_line: 20, goto_file: None, attributes: HarnessAttributes::default(), - contracts: vec![], + contract: None, } } diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs index 4ffbfd76e8f7..af6da19a5ae3 100644 --- a/kani-compiler/src/kani_middle/metadata.rs +++ b/kani-compiler/src/kani_middle/metadata.rs @@ -17,7 +17,7 @@ pub fn gen_proof_metadata( tcx: TyCtxt, def_id: DefId, base_name: &Path, - contracts: Vec, + contract: Option, ) -> HarnessMetadata { let attributes = extract_harness_attributes(tcx, def_id); let pretty_name = tcx.def_path_str(def_id); @@ -44,7 +44,7 @@ pub fn gen_proof_metadata( attributes, // TODO: This no longer needs to be an Option. goto_file: Some(model_file), - contracts, + contract, } } @@ -73,6 +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), - contracts: vec![], + contract: None, } } diff --git a/kani-driver/src/call_goto_instrument.rs b/kani-driver/src/call_goto_instrument.rs index 7f32b136ae28..66cd38cd78f8 100644 --- a/kani-driver/src/call_goto_instrument.rs +++ b/kani-driver/src/call_goto_instrument.rs @@ -37,7 +37,7 @@ impl KaniSession { self.goto_sanity_check(output)?; } - for function in &harness.contracts { + if let Some(function) = &harness.contract { self.enforce_contract(output, &function)?; } diff --git a/kani-driver/src/metadata.rs b/kani-driver/src/metadata.rs index c10258c8aaa1..d2fe1b0987a1 100644 --- a/kani-driver/src/metadata.rs +++ b/kani-driver/src/metadata.rs @@ -184,7 +184,7 @@ pub fn mock_proof_harness( original_end_line: 0, attributes: HarnessAttributes { unwind_value, proof: true, ..Default::default() }, goto_file: model_file, - contracts: vec![], + contract: None, } } diff --git a/kani_metadata/src/harness.rs b/kani_metadata/src/harness.rs index 1f8812aa46ad..bdb70fbcd957 100644 --- a/kani_metadata/src/harness.rs +++ b/kani_metadata/src/harness.rs @@ -24,8 +24,8 @@ pub struct HarnessMetadata { pub goto_file: Option, /// The `#[kani::<>]` attributes added to a harness. pub attributes: HarnessAttributes, - - pub contracts: Vec, + /// The names of functions for which contracts should be enforced + pub contract: Option, } /// The attributes added by the user to control how a harness is executed. From 8bc7532f8b77ef4e39d4151f658292bd874b0717 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Mon, 10 Jul 2023 12:28:36 -0700 Subject: [PATCH 12/22] Addressing leftover comments --- cprover_bindings/src/irep/irep_id.rs | 2 -- .../src/codegen_cprover_gotoc/compiler_interface.rs | 2 +- kani-compiler/src/kani_compiler.rs | 2 +- kani-compiler/src/kani_middle/attributes.rs | 10 +++++----- kani-compiler/src/kani_middle/metadata.rs | 4 ++-- kani-driver/src/call_goto_instrument.rs | 2 +- kani-driver/src/metadata.rs | 2 +- kani_metadata/src/harness.rs | 2 +- 8 files changed, 12 insertions(+), 14 deletions(-) diff --git a/cprover_bindings/src/irep/irep_id.rs b/cprover_bindings/src/irep/irep_id.rs index cad6eb563bf4..3ad8f71a7e86 100644 --- a/cprover_bindings/src/irep/irep_id.rs +++ b/cprover_bindings/src/irep/irep_id.rs @@ -593,7 +593,6 @@ pub enum IrepId { CSpecLoopInvariant, CSpecRequires, CSpecEnsures, - CSpecAssigns, VirtualFunction, ElementType, WorkingDirectory, @@ -1463,7 +1462,6 @@ impl ToString for IrepId { IrepId::CSpecLoopInvariant => "#spec_loop_invariant", IrepId::CSpecRequires => "#spec_requires", IrepId::CSpecEnsures => "#spec_ensures", - IrepId::CSpecAssigns => "#spec_assigns", IrepId::VirtualFunction => "virtual_function", IrepId::ElementType => "element_type", IrepId::WorkingDirectory => "working_directory", diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index d2d587fd3a81..4cbdbef71749 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -305,7 +305,7 @@ impl CodegenBackend for GotocCodegenBackend { if let MonoItem::Fn(instance) = test_fn { instance } else { continue }; let mut metadata = gen_test_metadata(tcx, *test_desc, *instance, &base_filename); - metadata.contract = contract_function.clone(); + 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 {}", diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index 353d38393c26..b2be4d796468 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/kani-compiler/src/kani_compiler.rs @@ -432,7 +432,7 @@ mod tests { original_end_line: 20, goto_file: None, attributes: HarnessAttributes::default(), - contract: None, + contract_to_enforce: None, } } diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 2f3f5d07138a..d6be165a4185 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -148,9 +148,11 @@ pub fn extract_harness_attributes(tcx: TyCtxt, def_id: DefId) -> HarnessAttribut // Internal attribute which shouldn't exist here. unreachable!() } - KaniAttributeKind::Ensures | KaniAttributeKind::Requires => { - todo!("Contract attributes are not supported on proofs (yet)") - } + KaniAttributeKind::Ensures | KaniAttributeKind::Requires => tcx.sess.fatal(format!( + "Contracts on harnesses are not supported (found {} on {})", + kind, + tcx.def_path_debug_str(def_id) + )), }; harness }) @@ -189,8 +191,6 @@ pub fn extract_contract(tcx: TyCtxt, local_def_id: LocalDefId) -> super::contrac .to_def_id() }; - //println!("Searching in {:?}", hir_map.module_items(enclosing_mod).map(|it| hir_map.item(it).ident.name).collect::>()); - let parse_and_resolve = |attr: &Vec<&Attribute>| { attr.iter() .map(|clause| match &clause.get_normal_item().args { diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs index af6da19a5ae3..a77a2471a5da 100644 --- a/kani-compiler/src/kani_middle/metadata.rs +++ b/kani-compiler/src/kani_middle/metadata.rs @@ -44,7 +44,7 @@ pub fn gen_proof_metadata( attributes, // TODO: This no longer needs to be an Option. goto_file: Some(model_file), - contract, + contract_to_enforce: contract, } } @@ -73,6 +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: None, + contract_to_enforce: None, } } diff --git a/kani-driver/src/call_goto_instrument.rs b/kani-driver/src/call_goto_instrument.rs index 66cd38cd78f8..d7cb12a9590e 100644 --- a/kani-driver/src/call_goto_instrument.rs +++ b/kani-driver/src/call_goto_instrument.rs @@ -37,7 +37,7 @@ impl KaniSession { self.goto_sanity_check(output)?; } - if let Some(function) = &harness.contract { + if let Some(function) = &harness.contract_to_enforce { self.enforce_contract(output, &function)?; } diff --git a/kani-driver/src/metadata.rs b/kani-driver/src/metadata.rs index d2fe1b0987a1..a1751b7d11ee 100644 --- a/kani-driver/src/metadata.rs +++ b/kani-driver/src/metadata.rs @@ -184,7 +184,7 @@ pub fn mock_proof_harness( original_end_line: 0, attributes: HarnessAttributes { unwind_value, proof: true, ..Default::default() }, goto_file: model_file, - contract: None, + contract_to_enforce: None, } } diff --git a/kani_metadata/src/harness.rs b/kani_metadata/src/harness.rs index bdb70fbcd957..be98f64a2a63 100644 --- a/kani_metadata/src/harness.rs +++ b/kani_metadata/src/harness.rs @@ -25,7 +25,7 @@ pub struct HarnessMetadata { /// The `#[kani::<>]` attributes added to a harness. pub attributes: HarnessAttributes, /// The names of functions for which contracts should be enforced - pub contract: Option, + pub contract_to_enforce: Option, } /// The attributes added by the user to control how a harness is executed. From 11d01fa41d9f9dd5161d4002003eb8c6627c1b0e Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Mon, 10 Jul 2023 12:31:05 -0700 Subject: [PATCH 13/22] Removing last vestiges of `assigns` --- cprover_bindings/src/irep/to_irep.rs | 3 --- kani-compiler/src/kani_middle/attributes.rs | 4 ++-- kani-compiler/src/kani_middle/contracts.rs | 6 ++---- 3 files changed, 4 insertions(+), 9 deletions(-) diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs index ced43700cbf6..cc3309d1c2b0 100644 --- a/cprover_bindings/src/irep/to_irep.rs +++ b/cprover_bindings/src/irep/to_irep.rs @@ -537,9 +537,6 @@ impl goto_program::Symbol { for ensures in &contract.ensures { typ = typ.with_named_sub(IrepId::CSpecEnsures, ensures.to_irep(mm)); } - for assigns in &contract.assigns { - typ = typ.with_named_sub(IrepId::CSpecAssigns, assigns.to_irep(mm)); - } } super::Symbol { typ, diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index d6be165a4185..657a44164007 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -150,7 +150,7 @@ pub fn extract_harness_attributes(tcx: TyCtxt, def_id: DefId) -> HarnessAttribut } KaniAttributeKind::Ensures | KaniAttributeKind::Requires => tcx.sess.fatal(format!( "Contracts on harnesses are not supported (found {} on {})", - kind, + kind.as_ref(), tcx.def_path_debug_str(def_id) )), }; @@ -214,7 +214,7 @@ pub fn extract_contract(tcx: TyCtxt, local_def_id: LocalDefId) -> super::contrac 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, vec![]) + super::contracts::FnContract::new(requires, ensures) } /// Check that any unstable API has been enabled. Otherwise, emit an error. diff --git a/kani-compiler/src/kani_middle/contracts.rs b/kani-compiler/src/kani_middle/contracts.rs index 4ae642b2d90c..a91f3d9c0577 100644 --- a/kani-compiler/src/kani_middle/contracts.rs +++ b/kani-compiler/src/kani_middle/contracts.rs @@ -10,7 +10,6 @@ use rustc_hir::def_id::DefId; pub struct GFnContract { requires: Vec, ensures: Vec, - assigns: Vec, } pub type FnContract = GFnContract; @@ -26,8 +25,8 @@ impl GFnContract { &self.ensures } - pub fn new(requires: Vec, ensures: Vec, assigns: Vec) -> Self { - Self { requires, ensures, assigns } + pub fn new(requires: Vec, ensures: Vec) -> Self { + Self { requires, ensures } } /// Perform a transformation on each implementation item. Usually these are @@ -36,7 +35,6 @@ impl GFnContract { GFnContract { requires: self.requires.iter().map(&mut f).collect(), ensures: self.ensures.iter().map(&mut f).collect(), - assigns: self.assigns.iter().map(&mut f).collect(), } } From 26b1b975a4ade71a01e7de43f65be09fd3d732d3 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Mon, 10 Jul 2023 13:00:40 -0700 Subject: [PATCH 14/22] Refactoring reachabiity --- kani-compiler/src/kani_middle/reachability.rs | 74 +++++++++++-------- 1 file changed, 42 insertions(+), 32 deletions(-) diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 95712d078b68..c529b024359c 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -173,36 +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 let Entry::Vacant(e) = self.collected.entry(to_visit) { - let opt_contract = to_visit.def_id().as_local().and_then(|local_def_id| { - let substs = match to_visit { - 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 visit_obligations_from_contract = if let Some(contract) = opt_contract.as_ref() - { - [contract.requires(), contract.ensures()] - .into_iter() - .flat_map(IntoIterator::into_iter) - .copied() - .map(MonoItem::Fn) - .collect() - } else { - vec![] - }; - e.insert(opt_contract); + 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), @@ -214,12 +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() - .chain(visit_obligations_from_contract) - .filter(|item| !self.collected.contains_key(item)), - ); + self.add_to_queue(next_items); } } } From 8bfaae211497557dc63be6dde574c567777b2e1b Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Fri, 14 Jul 2023 14:56:35 -0700 Subject: [PATCH 15/22] Fixed small import issue --- kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 4cbdbef71749..fa0735a242e3 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -38,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; From 8b16da6c0776d4268ebea00200bc898384bb1241 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Fri, 14 Jul 2023 15:35:25 -0700 Subject: [PATCH 16/22] Fixing multi-contract and adding a test case --- cprover_bindings/src/irep/to_irep.rs | 18 +++++++------ .../double_required.expected | 9 +++++++ .../function-contract/double_requires.rs | 26 +++++++++++++++++++ 3 files changed, 45 insertions(+), 8 deletions(-) create mode 100644 tests/expected/function-contract/double_required.expected create mode 100644 tests/expected/function-contract/double_requires.rs diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs index cc3309d1c2b0..8991ebb9a210 100644 --- a/cprover_bindings/src/irep/to_irep.rs +++ b/cprover_bindings/src/irep/to_irep.rs @@ -519,11 +519,11 @@ impl ToIrep for Lambda { sub: vec![Irep::just_sub(types), self.body.typ().to_irep(mm)], named_sub: Default::default(), }; - Irep::just_sub(vec![Irep { + Irep { id: IrepId::Lambda, sub: vec![Irep::tuple(ops_ireps), self.body.to_irep(mm)], named_sub: linear_map!((IrepId::Type, typ)), - }]) + } } } @@ -531,12 +531,14 @@ 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 { - for requires in &contract.requires { - typ = typ.with_named_sub(IrepId::CSpecRequires, requires.to_irep(mm)); - } - for ensures in &contract.ensures { - typ = typ.with_named_sub(IrepId::CSpecEnsures, ensures.to_irep(mm)); - } + 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, diff --git a/tests/expected/function-contract/double_required.expected b/tests/expected/function-contract/double_required.expected new file mode 100644 index 000000000000..d8cc6dfa0d18 --- /dev/null +++ b/tests/expected/function-contract/double_required.expected @@ -0,0 +1,9 @@ +Check 3: double_requires::reduce1.missing_definition.2 + - Status: FAILURE + - Description: "Function `double_requires::reduce1` with missing definition is unreachable" + +VERIFICATION:- FAILED + +Check 1: double_requires::reduce2.missing_definition.1 + - 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()); +} From 954ab56946661c49dcbbf19ca5ad0105af46daa1 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Fri, 14 Jul 2023 15:57:11 -0700 Subject: [PATCH 17/22] Must allow unused variables I guess --- library/kani_macros/src/lib.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index fd4094efe208..2f090d6c2db2 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -275,6 +275,7 @@ mod sysroot { let attribute = format_ident!("{name}"); let kani_attributes = quote!( #[allow(dead_code)] + #[allow(unused_variables)] #[kanitool::#attribute = stringify!(#gen_fn_name)] ); From 3116074dcd3a791d328d751ed2228b7689cc0733 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Fri, 14 Jul 2023 20:27:07 -0700 Subject: [PATCH 18/22] Apparently some of the test messages had changed --- .../expected/function-contract/arbitrary_requires_fail.expected | 2 +- .../expected/function-contract/arbitrary_requires_pass.expected | 2 +- .../{double_required.expected => double_requires.expected} | 0 3 files changed, 2 insertions(+), 2 deletions(-) rename tests/expected/function-contract/{double_required.expected => double_requires.expected} (100%) diff --git a/tests/expected/function-contract/arbitrary_requires_fail.expected b/tests/expected/function-contract/arbitrary_requires_fail.expected index 132a7455f12d..e4fa03879db6 100644 --- a/tests/expected/function-contract/arbitrary_requires_fail.expected +++ b/tests/expected/function-contract/arbitrary_requires_fail.expected @@ -3,6 +3,6 @@ Check 1: div.assertion.1 - Status: FAILURE - Description: "attempt to divide by zero" -Check 2: div.division-by-zero.1 +Check 3: div.division-by-zero.1 - Status: SUCCESS - Description: "division by zero" diff --git a/tests/expected/function-contract/arbitrary_requires_pass.expected b/tests/expected/function-contract/arbitrary_requires_pass.expected index 2a5317f904a4..a5013aa476ae 100644 --- a/tests/expected/function-contract/arbitrary_requires_pass.expected +++ b/tests/expected/function-contract/arbitrary_requires_pass.expected @@ -3,6 +3,6 @@ Check 1: div.assertion.1 - Status: SUCCESS - Description: "attempt to divide by zero" -Check 2: div.division-by-zero.1 +Check 3: div.division-by-zero.1 - Status: SUCCESS - Description: "division by zero" diff --git a/tests/expected/function-contract/double_required.expected b/tests/expected/function-contract/double_requires.expected similarity index 100% rename from tests/expected/function-contract/double_required.expected rename to tests/expected/function-contract/double_requires.expected From 9b796fa3646e8fb842511ad14970e8d09c749d03 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Fri, 21 Jul 2023 13:40:06 -0700 Subject: [PATCH 19/22] Corrected expected files Changed tesdt runner to not leave trailing checks and to ignore whitespace around expected lines --- .../arbitrary_ensures_fail.expected | 8 ++-- .../arbitrary_ensures_pass.expected | 8 ++-- .../arbitrary_requires_fail.expected | 11 ++---- .../arbitrary_requires_pass.expected | 10 ++--- .../double_requires.expected | 8 ++-- .../simple_ensures_fail.expected | 8 ++-- .../simple_ensures_pass.expected | 6 +-- tools/compiletest/src/runtest.rs | 39 +++++++------------ 8 files changed, 36 insertions(+), 62 deletions(-) diff --git a/tests/expected/function-contract/arbitrary_ensures_fail.expected b/tests/expected/function-contract/arbitrary_ensures_fail.expected index 22af34a550eb..d9244895bed8 100644 --- a/tests/expected/function-contract/arbitrary_ensures_fail.expected +++ b/tests/expected/function-contract/arbitrary_ensures_fail.expected @@ -1,5 +1,3 @@ -RESULTS: -Check 1: arbitrary_ensures_fail::max.missing_definition.1 - - Status: FAILURE - - Description: "Function `arbitrary_ensures_fail::max` with missing definition is unreachable" - - Location: Unknown file in function arbitrary_ensures_fail::max +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_pass.expected b/tests/expected/function-contract/arbitrary_ensures_pass.expected index 04c42f9cc2e6..bad92983bd8d 100644 --- a/tests/expected/function-contract/arbitrary_ensures_pass.expected +++ b/tests/expected/function-contract/arbitrary_ensures_pass.expected @@ -1,5 +1,3 @@ -RESULTS: -Check 1: arbitrary_ensures_pass::max.missing_definition.1 - - Status: SUCCESS - - Description: "Function `arbitrary_ensures_pass::max` with missing definition is unreachable" - - Location: Unknown file in function arbitrary_ensures_pass::max +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_requires_fail.expected b/tests/expected/function-contract/arbitrary_requires_fail.expected index e4fa03879db6..644bfc97aeb8 100644 --- a/tests/expected/function-contract/arbitrary_requires_fail.expected +++ b/tests/expected/function-contract/arbitrary_requires_fail.expected @@ -1,8 +1,3 @@ -RESULTS: -Check 1: div.assertion.1 - - Status: FAILURE - - Description: "attempt to divide by zero" - -Check 3: div.division-by-zero.1 - - Status: SUCCESS - - Description: "division by zero" +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_pass.expected b/tests/expected/function-contract/arbitrary_requires_pass.expected index a5013aa476ae..6a5faa7e2b6c 100644 --- a/tests/expected/function-contract/arbitrary_requires_pass.expected +++ b/tests/expected/function-contract/arbitrary_requires_pass.expected @@ -1,8 +1,4 @@ -RESULTS: -Check 1: div.assertion.1 - - Status: SUCCESS - - Description: "attempt to divide by zero" +div.assertion \ + - Status: SUCCESS \ + - Description: "attempt to divide by zero" -Check 3: div.division-by-zero.1 - - Status: SUCCESS - - Description: "division by zero" diff --git a/tests/expected/function-contract/double_requires.expected b/tests/expected/function-contract/double_requires.expected index d8cc6dfa0d18..d1894fad59d9 100644 --- a/tests/expected/function-contract/double_requires.expected +++ b/tests/expected/function-contract/double_requires.expected @@ -1,9 +1,9 @@ -Check 3: double_requires::reduce1.missing_definition.2 - - Status: FAILURE +double_requires::reduce1.missing_definition \ + - Status: FAILURE \ - Description: "Function `double_requires::reduce1` with missing definition is unreachable" VERIFICATION:- FAILED -Check 1: double_requires::reduce2.missing_definition.1 - - Status: FAILURE +double_requires::reduce2.missing_definition \ + - Status: FAILURE \ - Description: "Function `double_requires::reduce2` with missing definition is unreachable" diff --git a/tests/expected/function-contract/simple_ensures_fail.expected b/tests/expected/function-contract/simple_ensures_fail.expected index 41b151c49ac4..bd6e84b407ef 100644 --- a/tests/expected/function-contract/simple_ensures_fail.expected +++ b/tests/expected/function-contract/simple_ensures_fail.expected @@ -1,5 +1,3 @@ -RESULTS: -Check 1: simple_ensures_fail::max.missing_definition.1 - - Status: FAILURE - - Description: "Function `simple_ensures_fail::max` with missing definition is unreachable" - - Location: Unknown file in function simple_ensures_fail::max +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_pass.expected b/tests/expected/function-contract/simple_ensures_pass.expected index 3b26315ec354..371c7539df24 100644 --- a/tests/expected/function-contract/simple_ensures_pass.expected +++ b/tests/expected/function-contract/simple_ensures_pass.expected @@ -1,5 +1,3 @@ -RESULTS: -Check 1: simple_ensures_pass::max.missing_definition.1 - - Status: SUCCESS +simple_ensures_pass::max.missing_definition \ + - Status: SUCCESS \ - Description: "Function `simple_ensures_pass::max` with missing definition is unreachable" - - Location: Unknown file in function simple_ensures_pass::max diff --git a/tools/compiletest/src/runtest.rs b/tools/compiletest/src/runtest.rs index 946e8cd94712..4645d1409dd9 100644 --- a/tools/compiletest/src/runtest.rs +++ b/tools/compiletest/src/runtest.rs @@ -453,35 +453,26 @@ 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 + let slice_len = lines.len(); + // Does *any* subslice of length `lines.len()` satisfy the containment of + // *all* `lines` + // `trim()` added to ignore trailing and preceding whitespace + (0..(str.len() - slice_len)).any(|i| { + str[i..i + slice_len] + .into_iter() + .zip(lines) + .all(|(output, expected)| output.contains(expected.trim())) + }) } fn create_stamp(&self) { From 21bd441139830374fd03d4143a3091fda904c319 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Fri, 21 Jul 2023 13:45:42 -0700 Subject: [PATCH 20/22] Actually there is a `windows` method --- tools/compiletest/src/runtest.rs | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/tools/compiletest/src/runtest.rs b/tools/compiletest/src/runtest.rs index 4645d1409dd9..905d11eea9d9 100644 --- a/tools/compiletest/src/runtest.rs +++ b/tools/compiletest/src/runtest.rs @@ -463,12 +463,11 @@ impl<'test> TestCx<'test> { /// 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 slice_len = lines.len(); // Does *any* subslice of length `lines.len()` satisfy the containment of // *all* `lines` // `trim()` added to ignore trailing and preceding whitespace - (0..(str.len() - slice_len)).any(|i| { - str[i..i + slice_len] + str.windows(lines.len()).any(|subslice| { + subslice .into_iter() .zip(lines) .all(|(output, expected)| output.contains(expected.trim())) From 48f617bd8856210d745c4866acecc56d0f739f9d Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Fri, 21 Jul 2023 13:51:32 -0700 Subject: [PATCH 21/22] Clippy doesn't like me --- tools/compiletest/src/runtest.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/compiletest/src/runtest.rs b/tools/compiletest/src/runtest.rs index 905d11eea9d9..2d59e9267481 100644 --- a/tools/compiletest/src/runtest.rs +++ b/tools/compiletest/src/runtest.rs @@ -468,7 +468,7 @@ impl<'test> TestCx<'test> { // `trim()` added to ignore trailing and preceding whitespace str.windows(lines.len()).any(|subslice| { subslice - .into_iter() + .iter() .zip(lines) .all(|(output, expected)| output.contains(expected.trim())) }) From 7122fd3f5fdcb505818027a5dfb0bda69dccefb8 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Sat, 22 Jul 2023 17:49:13 -0700 Subject: [PATCH 22/22] fmt --- tools/compiletest/src/runtest.rs | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/tools/compiletest/src/runtest.rs b/tools/compiletest/src/runtest.rs index 2d59e9267481..71d723dceb59 100644 --- a/tools/compiletest/src/runtest.rs +++ b/tools/compiletest/src/runtest.rs @@ -467,10 +467,7 @@ impl<'test> TestCx<'test> { // *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())) + subslice.iter().zip(lines).all(|(output, expected)| output.contains(expected.trim())) }) }