diff --git a/cprover_bindings/src/goto_program/stmt.rs b/cprover_bindings/src/goto_program/stmt.rs index 2afbdafc95a3..79afb9a7b70e 100644 --- a/cprover_bindings/src/goto_program/stmt.rs +++ b/cprover_bindings/src/goto_program/stmt.rs @@ -82,7 +82,12 @@ pub enum StmtBody { arguments: Vec, }, /// `goto dest;` - Goto(InternedString), + Goto { + dest: InternedString, + // The loop invariants annotated to the goto, which can be + // applied as loop contracts in CBMC if it is a backward goto. + loop_invariants: Option, + }, /// `if (i) { t } else { e }` Ifthenelse { i: Expr, @@ -179,7 +184,7 @@ impl Stmt { stmt!(Assign { lhs, rhs }, loc) } - /// `assert(cond, property_class, commment);` + /// `assert(cond, property_class, comment);` pub fn assert(cond: Expr, property_name: &str, message: &str, loc: Location) -> Self { assert!(cond.typ().is_bool()); assert!(!property_name.is_empty() && !message.is_empty()); @@ -188,7 +193,7 @@ impl Stmt { let loc_with_property = Location::create_location_with_property(message, property_name, loc); - // Chose InternedString to seperate out codegen from the cprover_bindings logic + // Chose InternedString to separate out codegen from the cprover_bindings logic let property_class = property_name.intern(); let msg = message.into(); @@ -283,7 +288,7 @@ impl Stmt { pub fn goto>(dest: T, loc: Location) -> Self { let dest = dest.into(); assert!(!dest.is_empty()); - stmt!(Goto(dest), loc) + stmt!(Goto { dest, loop_invariants: None }, loc) } /// `if (i) { t } else { e }` or `if (i) { t }` @@ -325,6 +330,16 @@ impl Stmt { assert!(!label.is_empty()); stmt!(Label { label, body: self }, *self.location()) } + + /// `goto dest;` with loop invariant + pub fn with_loop_contracts(self, inv: Expr) -> Self { + if let Goto { dest, loop_invariants } = self.body() { + assert!(loop_invariants.is_none()); + stmt!(Goto { dest: *dest, loop_invariants: Some(inv) }, *self.location()) + } else { + unreachable!("Loop contracts should be annotated only to goto stmt") + } + } } /// Predicates diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs index 788c9f1e79d4..e007652a04a9 100644 --- a/cprover_bindings/src/irep/to_irep.rs +++ b/cprover_bindings/src/irep/to_irep.rs @@ -520,8 +520,18 @@ impl ToIrep for StmtBody { arguments_irep(arguments.iter(), mm), ]) } - StmtBody::Goto(dest) => code_irep(IrepId::Goto, vec![]) - .with_named_sub(IrepId::Destination, Irep::just_string_id(dest.to_string())), + StmtBody::Goto { dest, loop_invariants } => { + let stmt_goto = code_irep(IrepId::Goto, vec![]) + .with_named_sub(IrepId::Destination, Irep::just_string_id(dest.to_string())); + if let Some(inv) = loop_invariants { + stmt_goto.with_named_sub( + IrepId::CSpecLoopInvariant, + inv.clone().and(Expr::bool_true()).to_irep(mm), + ) + } else { + stmt_goto + } + } StmtBody::Ifthenelse { i, t, e } => code_irep(IrepId::Ifthenelse, vec![ i.to_irep(mm), t.to_irep(mm), diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index da3cef9e3564..8675d3fad3f3 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -10,11 +10,14 @@ use crate::codegen_cprover_gotoc::GotocCtx; use crate::codegen_cprover_gotoc::codegen::{PropertyClass, bb_label}; +use crate::kani_middle::attributes::KaniAttributes; use crate::kani_middle::attributes::matches_diagnostic as matches_function; use crate::unwrap_or_return_codegen_unimplemented_stmt; +use cbmc::goto_program::CIntType; use cbmc::goto_program::{BuiltinFn, Expr, Stmt, Type}; use rustc_middle::ty::TyCtxt; use rustc_smir::rustc_internal; +use rustc_span::Symbol; use stable_mir::mir::mono::Instance; use stable_mir::mir::{BasicBlockIdx, Place}; use stable_mir::{CrateDef, ty::Span}; @@ -539,6 +542,43 @@ impl GotocHook for InitContracts { } } +/// A loop contract register function call is assumed to be +/// 1. of form `kani_register_loop_contract(inv)` where `inv` +/// is the closure wrapping loop invariants +/// 2. is the last statement in some loop, so that its `target`` is +/// the head of the loop +/// +/// Such call will be translate to +/// ```c +/// goto target +/// ``` +/// with loop invariants (call to the register function) annotated as +/// a named sub of the `goto`. +pub struct LoopInvariantRegister; + +impl GotocHook for LoopInvariantRegister { + fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool { + KaniAttributes::for_instance(tcx, instance).fn_marker() + == Some(Symbol::intern("kani_register_loop_contract")) + } + + fn handle( + &self, + gcx: &mut GotocCtx, + instance: Instance, + fargs: Vec, + _assign_to: &Place, + target: Option, + span: Span, + ) -> Stmt { + let loc = gcx.codegen_span_stable(span); + let func_exp = gcx.codegen_func_expr(instance, loc); + + Stmt::goto(bb_label(target.unwrap()), loc) + .with_loop_contracts(func_exp.call(fargs).cast_to(Type::CInteger(CIntType::Bool))) + } +} + pub fn fn_hooks() -> GotocHooks { GotocHooks { hooks: vec![ @@ -555,6 +595,7 @@ pub fn fn_hooks() -> GotocHooks { Rc::new(MemCmp), Rc::new(UntrackedDeref), Rc::new(InitContracts), + Rc::new(LoopInvariantRegister), ], } } diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index 24fe5d8b2b2e..6cb104c7470a 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -59,6 +59,11 @@ impl MutableBody { self.arg_count } + #[allow(dead_code)] + pub fn var_debug_info(&self) -> &Vec { + &self.var_debug_info + } + /// Create a mutable body from the original MIR body. pub fn from(body: Body) -> Self { MutableBody { @@ -428,6 +433,15 @@ impl MutableBody { self.blocks.push(BasicBlock { statements: Vec::default(), terminator }) } + /// Replace statements from the given basic block + pub fn replace_statements( + &mut self, + source_instruction: &SourceInstruction, + new_stmts: Vec, + ) { + self.blocks.get_mut(source_instruction.bb()).unwrap().statements = new_stmts; + } + /// Replace a terminator from the given basic block pub fn replace_terminator( &mut self, @@ -559,7 +573,7 @@ pub trait MutMirVisitor { StatementKind::Assign(_, rvalue) => { self.visit_rvalue(rvalue); } - StatementKind::Intrinsic(intrisic) => match intrisic { + StatementKind::Intrinsic(intrinsic) => match intrinsic { NonDivergingIntrinsic::Assume(operand) => { self.visit_operand(operand); } diff --git a/kani-compiler/src/kani_middle/transform/loop_contracts.rs b/kani-compiler/src/kani_middle/transform/loop_contracts.rs new file mode 100644 index 000000000000..8038ef784970 --- /dev/null +++ b/kani-compiler/src/kani_middle/transform/loop_contracts.rs @@ -0,0 +1,401 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This module contains code related to the MIR-to-MIR pass to enable loop contracts. +//! + +use crate::kani_middle::KaniAttributes; +use crate::kani_middle::codegen_units::CodegenUnit; +use crate::kani_middle::find_fn_def; +use crate::kani_middle::transform::TransformationType; +use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceInstruction}; +use crate::kani_queries::QueryDb; +use crate::stable_mir::CrateDef; +use rustc_middle::ty::TyCtxt; +use rustc_span::Symbol; +use stable_mir::mir::mono::Instance; +use stable_mir::mir::{ + AggregateKind, BasicBlock, BasicBlockIdx, Body, ConstOperand, Operand, Place, Rvalue, + Statement, StatementKind, Terminator, TerminatorKind, VarDebugInfoContents, +}; +use stable_mir::ty::{FnDef, MirConst, RigidTy, UintTy}; +use std::collections::{HashMap, HashSet, VecDeque}; +use std::fmt::Debug; + +use super::TransformPass; + +#[derive(Debug, Default)] +pub struct LoopContractPass { + /// Cache KaniRunContract function used to implement contracts. + run_contract_fn: Option, + /// The map from original loop head to the new loop latch. + /// We use this map to redirect all original loop latches to a new single loop latch. + new_loop_latches: HashMap, +} + +impl TransformPass for LoopContractPass { + /// The type of transformation that this pass implements. + fn transformation_type() -> TransformationType + where + Self: Sized, + { + TransformationType::Stubbing + } + + fn is_enabled(&self, query_db: &QueryDb) -> bool + where + Self: Sized, + { + query_db.args().unstable_features.contains(&"loop-contracts".to_string()) + } + + /// Run a transformation pass on the whole codegen unit. + /// + /// This pass will perform the following operations: + /// 1. Replace the body of `kani_register_loop_contract` by `kani::internal::run_contract_fn` + /// to invoke the closure. + /// + /// 2. Transform loops with contracts from + /// ```ignore + /// bb_idx: { + /// loop_head_stmts + /// _v = kani_register_loop_contract(move args) -> [return: terminator_target]; + /// } + /// + /// ... + /// loop_body_blocks + /// ... + /// + /// loop_latch_block: { + /// loop_latch_stmts + /// goto -> bb_idx; + /// } + /// ``` + /// to blocks + /// ```ignore + /// bb_idx: { + /// loop_head_stmts + /// _v = true + /// goto -> terminator_target + /// } + /// + /// ... + /// loop_body_blocks + /// ... + /// + /// loop_latch_block: { + /// loop_latch_stmts + /// goto -> bb_new_loop_latch; + /// } + /// + /// bb_new_loop_latch: { + /// loop_head_body + /// _v = kani_register_loop_contract(move args) -> [return: terminator_target]; + /// } + /// ``` + fn transform(&mut self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) { + self.new_loop_latches = HashMap::new(); + match instance.ty().kind().rigid().unwrap() { + RigidTy::FnDef(_func, args) => { + if KaniAttributes::for_instance(tcx, instance).fn_marker() + == Some(Symbol::intern("kani_register_loop_contract")) + { + // Replace the body of the register function with `run_contract_fn`'s. + let run = Instance::resolve(self.run_contract_fn.unwrap(), args).unwrap(); + (true, run.body().unwrap()) + } else { + let mut new_body = MutableBody::from(body); + let mut contain_loop_contracts: bool = false; + + // Visit basic blocks in control flow order (BFS). + let mut visited: HashSet = HashSet::new(); + let mut queue: VecDeque = VecDeque::new(); + // Visit blocks in loops only when there is no blocks in queue. + let mut loop_queue: VecDeque = VecDeque::new(); + queue.push_back(0); + + while let Some(bb_idx) = queue.pop_front().or(loop_queue.pop_front()) { + visited.insert(bb_idx); + + let terminator = new_body.blocks()[bb_idx].terminator.clone(); + + let is_loop_head = self.transform_bb(tcx, &mut new_body, bb_idx); + contain_loop_contracts |= is_loop_head; + + // Add successors of the current basic blocks to + // the visiting queue. + for to_visit in terminator.successors() { + if !visited.contains(&to_visit) { + let target_queue = + if is_loop_head { &mut loop_queue } else { &mut queue }; + target_queue.push_back(to_visit); + } + } + } + (contain_loop_contracts, new_body.into()) + } + } + _ => { + /* static variables case */ + (false, body) + } + } + } +} + +impl LoopContractPass { + pub fn new(tcx: TyCtxt, unit: &CodegenUnit) -> LoopContractPass { + if !unit.harnesses.is_empty() { + let run_contract_fn = find_fn_def(tcx, "KaniRunLoopContract"); + assert!(run_contract_fn.is_some(), "Failed to find Kani run contract function"); + LoopContractPass { run_contract_fn, new_loop_latches: HashMap::new() } + } else { + // If reachability mode is PubFns or Tests, we just remove any contract logic. + // Note that in this path there is no proof harness. + LoopContractPass::default() + } + } + + /// Generate the body of loop head block by dropping all statements + /// except for `StorageLive` and `StorageDead`. + fn get_loop_head_block(&self, block: &BasicBlock) -> BasicBlock { + let new_stmts: Vec = block + .statements + .iter() + .filter(|stmt| { + matches!(stmt.kind, StatementKind::StorageLive(_) | StatementKind::StorageDead(_)) + }) + .cloned() + .collect(); + BasicBlock { statements: new_stmts, terminator: block.terminator.clone() } + } + + /// Remove `StorageDead closure_var` to avoid invariant closure becoming dead. + fn make_invariant_closure_alive(&self, body: &mut MutableBody, bb_idx: usize) { + let mut stmts = body.blocks()[bb_idx].statements.clone(); + if stmts.is_empty() || !matches!(stmts[0].kind, StatementKind::StorageDead(_)) { + unreachable!( + "The assumptions for loop-contracts transformation are violated by some other transformation. \ + Please report github.com/model-checking/kani/issues/new?template=bug_report.md" + ); + } + stmts.remove(0); + body.replace_statements(&SourceInstruction::Terminator { bb: bb_idx }, stmts); + } + + /// We only support closure arguments that are either `copy`` or `move`` of reference of user variables. + fn is_supported_argument_of_closure(&self, rv: &Rvalue, body: &MutableBody) -> bool { + let var_debug_info = &body.var_debug_info(); + matches!(rv, Rvalue::Ref(_, _, place) if + var_debug_info.iter().any(|info| + matches!(&info.value, VarDebugInfoContents::Place(debug_place) if *place == *debug_place) + )) + } + + /// Transform loops with contracts from + /// ```ignore + /// bb_idx: { + /// loop_head_stmts + /// _v = kani_register_loop_contract(move args) -> [return: terminator_target]; + /// } + /// + /// ... + /// loop_body_blocks + /// ... + /// + /// loop_latch_block: { + /// loop_latch_stmts + /// goto -> bb_idx; + /// } + /// ``` + /// to blocks + /// ```ignore + /// bb_idx: { + /// loop_head_stmts + /// _v = true + /// goto -> terminator_target + /// } + /// + /// ... + /// loop_body_blocks + /// ... + /// + /// loop_latch_block: { + /// loop_latch_stmts + /// goto -> bb_new_loop_latch; + /// } + /// + /// bb_new_loop_latch: { + /// loop_head_body + /// _v = kani_register_loop_contract(move args) -> [return: terminator_target]; + /// } + /// ``` + fn transform_bb(&mut self, tcx: TyCtxt, new_body: &mut MutableBody, bb_idx: usize) -> bool { + let terminator = new_body.blocks()[bb_idx].terminator.clone(); + let mut contain_loop_contracts = false; + + // Redirect loop latches to the new latches. + if let TerminatorKind::Goto { target: terminator_target } = &terminator.kind { + if self.new_loop_latches.contains_key(terminator_target) { + new_body.replace_terminator( + &SourceInstruction::Terminator { bb: bb_idx }, + Terminator { + kind: TerminatorKind::Goto { + target: self.new_loop_latches[terminator_target], + }, + span: terminator.span, + }, + ); + } + } + + // Transform loop heads with loop contracts. + if let TerminatorKind::Call { + func: terminator_func, + args: terminator_args, + destination: terminator_destination, + target: terminator_target, + unwind: terminator_unwind, + } = &terminator.kind + { + // Get the function signature of the terminator call. + let Some(RigidTy::FnDef(fn_def, ..)) = terminator_func + .ty(new_body.locals()) + .ok() + .map(|fn_ty| fn_ty.kind().rigid().unwrap().clone()) + else { + return false; + }; + + // The basic blocks end with register functions are loop head blocks. + if KaniAttributes::for_def_id(tcx, fn_def.def_id()).fn_marker() + == Some(Symbol::intern("kani_register_loop_contract")) + && matches!(&terminator_args[1], Operand::Constant(op) if op.const_.eval_target_usize().unwrap() == 0) + { + // Check if the MIR satisfy the assumptions of this transformation. + if !new_body.blocks()[terminator_target.unwrap()].statements.is_empty() + || !matches!( + new_body.blocks()[terminator_target.unwrap()].terminator.kind, + TerminatorKind::SwitchInt { .. } + ) + { + unreachable!( + "The assumptions for loop-contracts transformation are violated by some other transformation. \ + Please report github.com/model-checking/kani/issues/new?template=bug_report.md" + ); + } + + let ori_condition_bb_idx = + new_body.blocks()[terminator_target.unwrap()].terminator.successors()[1]; + self.make_invariant_closure_alive(new_body, ori_condition_bb_idx); + + contain_loop_contracts = true; + + // Collect supported vars assigned in the block. + // And check if all arguments of the closure is supported. + let mut supported_vars: Vec = Vec::new(); + // All user variables are support + supported_vars.extend(new_body.var_debug_info().iter().filter_map(|info| { + match &info.value { + VarDebugInfoContents::Place(debug_place) => Some(debug_place.clone()), + _ => None, + } + })); + + // For each assignment in the loop head block, + // if it assigns to the closure place, we check if all arguments are supported; + // if it assigns to other places, we cache if the assigned places are supported. + for stmt in &new_body.blocks()[bb_idx].statements { + if let StatementKind::Assign(place, rvalue) = &stmt.kind { + match rvalue { + Rvalue::Aggregate(AggregateKind::Closure(..), closure_args) => { + if closure_args.iter().any(|arg| !matches!(arg, Operand::Copy(arg_place) | Operand::Move(arg_place) if supported_vars.contains(arg_place))) { + unreachable!( + "The loop invariant support only reference of user variables. The provided invariants contain unsupported dereference. \ + Please report github.com/model-checking/kani/issues/new?template=bug_report.md" + ); + } + } + _ => { + if self.is_supported_argument_of_closure(rvalue, new_body) { + supported_vars.push(place.clone()); + } + } + } + } + } + + // Replace the original loop head block + // ```ignore + // bb_idx: { + // loop_head_stmts + // _v = kani_register_loop_contract(move args) -> [return: terminator_target]; + // } + // ``` + // with + // ```ignore + // bb_idx: { + // loop_head_stmts + // _v = true; + // goto -> terminator_target + // } + // ``` + new_body.assign_to( + terminator_destination.clone(), + Rvalue::Use(Operand::Constant(ConstOperand { + span: terminator.span, + user_ty: None, + const_: MirConst::from_bool(true), + })), + &mut SourceInstruction::Terminator { bb: bb_idx }, + InsertPosition::Before, + ); + let new_latch_block = self.get_loop_head_block(&new_body.blocks()[bb_idx]); + + // Insert a new basic block as the loop latch block, and later redirect + // all latches to the new loop latch block. + // ----- + // bb_new_loop_latch: { + // _v = kani_register_loop_contract(move args) -> [return: terminator_target]; + // } + new_body.insert_bb( + new_latch_block, + &mut SourceInstruction::Terminator { bb: bb_idx }, + InsertPosition::After, + ); + // Update the argument `transformed` to 1 to avoid double transformation. + let new_args = vec![ + terminator_args[0].clone(), + Operand::Constant(ConstOperand { + span: terminator.span, + user_ty: None, + const_: MirConst::try_from_uint(1, UintTy::Usize).unwrap(), + }), + ]; + new_body.replace_terminator( + &SourceInstruction::Terminator { bb: new_body.blocks().len() - 1 }, + Terminator { + kind: TerminatorKind::Call { + func: terminator_func.clone(), + args: new_args, + destination: terminator_destination.clone(), + target: *terminator_target, + unwind: *terminator_unwind, + }, + span: terminator.span, + }, + ); + new_body.replace_terminator( + &SourceInstruction::Terminator { bb: bb_idx }, + Terminator { + kind: TerminatorKind::Goto { target: terminator_target.unwrap() }, + span: terminator.span, + }, + ); + // Cache the new loop latch. + self.new_loop_latches.insert(bb_idx, new_body.blocks().len() - 1); + } + } + contain_loop_contracts + } +} diff --git a/kani-compiler/src/kani_middle/transform/mod.rs b/kani-compiler/src/kani_middle/transform/mod.rs index 7d97a49f287a..3f324d72c39e 100644 --- a/kani-compiler/src/kani_middle/transform/mod.rs +++ b/kani-compiler/src/kani_middle/transform/mod.rs @@ -23,6 +23,7 @@ use crate::kani_middle::transform::check_uninit::{DelayedUbPass, UninitPass}; use crate::kani_middle::transform::check_values::ValidValuePass; use crate::kani_middle::transform::contracts::{AnyModifiesPass, FunctionWithContractPass}; use crate::kani_middle::transform::kani_intrinsics::IntrinsicGeneratorPass; +use crate::kani_middle::transform::loop_contracts::LoopContractPass; use crate::kani_middle::transform::stubs::{ExternFnStubPass, FnStubPass}; use crate::kani_queries::QueryDb; use dump_mir_pass::DumpMirPass; @@ -41,6 +42,7 @@ mod contracts; mod dump_mir_pass; mod internal_mir; mod kani_intrinsics; +mod loop_contracts; mod stubs; /// Object used to retrieve a transformed instance body. @@ -89,6 +91,7 @@ impl BodyTransformation { mem_init_fn_cache: HashMap::new(), arguments: queries.args().clone(), }); + transformer.add_pass(queries, LoopContractPass::new(tcx, &unit)); transformer } diff --git a/kani-driver/src/call_goto_instrument.rs b/kani-driver/src/call_goto_instrument.rs index d31d4dae90f6..a77e3c675aec 100644 --- a/kani-driver/src/call_goto_instrument.rs +++ b/kani-driver/src/call_goto_instrument.rs @@ -39,6 +39,15 @@ impl KaniSession { self.instrument_contracts(harness, output)?; + if self + .args + .common_args + .unstable_features + .contains(kani_metadata::UnstableFeature::LoopContracts) + { + self.instrument_loop_contracts(harness, output)?; + } + if self.args.checks.undefined_function_on() { self.add_library(output)?; self.undefined_functions(output)?; @@ -183,6 +192,25 @@ impl KaniSession { self.call_goto_instrument(&args) } + /// Apply annotated loop contracts. + pub fn instrument_loop_contracts(&self, harness: &HarnessMetadata, file: &Path) -> Result<()> { + let args: Vec = vec![ + "--dfcc".into(), + (&harness.mangled_name).into(), + "--apply-loop-contracts".into(), + "--loop-contracts-no-unwind".into(), + "--no-malloc-may-fail".into(), + // Because loop contracts now are wrapped in a closure which will be a side-effect expression in CBMC even they + // may not contain side-effect. So we disable the side-effect check for now and will implement a better check + // instead of simply rejecting function calls and statement expressions. + // See issue: diffblue/cbmc#8393 + "--disable-loop-contracts-side-effect-check".into(), + file.into(), + file.into(), + ]; + self.call_goto_instrument(&args) + } + /// 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/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs index 145e0c9c63aa..99991798beb8 100644 --- a/kani-driver/src/cbmc_property_renderer.rs +++ b/kani-driver/src/cbmc_property_renderer.rs @@ -735,7 +735,7 @@ fn annotate_properties_with_reach_results( mut properties: Vec, reach_checks: Vec, ) -> Vec { - let mut reach_map: HashMap = HashMap::new(); + let mut reach_map: HashMap> = HashMap::new(); let reach_desc_pat = Regex::new("KANI_CHECK_ID_.*_([0-9])*").unwrap(); // Collect data (ID, status) from reachability checks for reach_check in reach_checks { @@ -746,8 +746,7 @@ fn annotate_properties_with_reach_results( let check_id_str = format!("[{check_id}]"); // Get the status and insert into `reach_map` let status = reach_check.status; - let res_ins = reach_map.insert(check_id_str, status); - assert!(res_ins.is_none()); + reach_map.entry(check_id_str).or_default().push(status); } for prop in properties.iter_mut() { @@ -761,7 +760,15 @@ fn annotate_properties_with_reach_results( let reach_status_opt = reach_map.get(prop_match_id); // Update the reachability status of the property if let Some(reach_status) = reach_status_opt { - prop.reach = Some(*reach_status); + for status in reach_status { + // Report if any copy of `prop` is not success. + if prop.reach.is_none() + || prop.reach.unwrap() == CheckStatus::Satisfied + || prop.reach.unwrap() == CheckStatus::Success + { + prop.reach = Some(*status); + } + } } } } diff --git a/kani_metadata/src/unstable.rs b/kani_metadata/src/unstable.rs index a602c33e0326..705732b6700e 100644 --- a/kani_metadata/src/unstable.rs +++ b/kani_metadata/src/unstable.rs @@ -83,6 +83,8 @@ pub enum UnstableFeature { SourceCoverage, /// Enable function contracts [RFC 9](https://model-checking.github.io/kani/rfc/rfcs/0009-function-contracts.html) FunctionContracts, + /// Enable loop contracts [RFC 12](https://model-checking.github.io/kani/rfc/rfcs/0012-loop-contracts.html) + LoopContracts, /// Memory predicate APIs. MemPredicates, /// Automatically check that no invalid value is produced which is considered UB in Rust. diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index 839313f084c2..ee0092554e56 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -435,6 +435,18 @@ macro_rules! kani_intrinsics { func() } + /// Function that calls a closure used to implement loop contracts. + /// + /// In contracts, we cannot invoke the generated closures directly, instead, we call register + /// contract. This function is a no-op. However, in the reality, we do want to call the closure, + /// so we swap the register body by this function body. + #[doc(hidden)] + #[allow(dead_code)] + #[rustc_diagnostic_item = "KaniRunLoopContract"] + fn run_loop_contract_fn bool>(func: &F, _transformed: usize) -> bool { + func() + } + /// This is used by contracts to select which version of the contract to use during codegen. #[doc(hidden)] pub type Mode = u8; diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 3e6c9d018422..f571e4592c4c 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -8,6 +8,7 @@ // So we have to enable this on the commandline (see kani-rustc) with: // RUSTFLAGS="-Zcrate-attr=feature(register_tool) -Zcrate-attr=register_tool(kanitool)" #![feature(proc_macro_diagnostic)] +#![feature(proc_macro_span)] mod derive; // proc_macro::quote is nightly-only, so we'll cobble things together instead @@ -394,6 +395,18 @@ pub fn modifies(attr: TokenStream, item: TokenStream) -> TokenStream { attr_impl::modifies(attr, item) } +/// Add a loop invariant to this loop. +/// +/// The contents of the attribute is a condition that should be satisfied at the +/// beginning of every iteration of the loop. +/// 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 loop_invariant(attr: TokenStream, item: TokenStream) -> TokenStream { + attr_impl::loop_invariant(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)] @@ -401,8 +414,10 @@ mod sysroot { use proc_macro_error2::{abort, abort_call_site}; mod contracts; + mod loop_contracts; pub use contracts::{ensures, modifies, proof_for_contract, requires, stub_verified}; + pub use loop_contracts::loop_invariant; use super::*; @@ -580,4 +595,5 @@ mod regular { no_op!(modifies); no_op!(proof_for_contract); no_op!(stub_verified); + no_op!(loop_invariant); } diff --git a/library/kani_macros/src/sysroot/loop_contracts/mod.rs b/library/kani_macros/src/sysroot/loop_contracts/mod.rs new file mode 100644 index 000000000000..01166af3d988 --- /dev/null +++ b/library/kani_macros/src/sysroot/loop_contracts/mod.rs @@ -0,0 +1,101 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Implementation of the loop contracts code generation. +//! + +use proc_macro::TokenStream; +use proc_macro_error2::abort_call_site; +use quote::{format_ident, quote}; +use syn::spanned::Spanned; +use syn::token::AndAnd; +use syn::{BinOp, Expr, ExprBinary, Stmt}; + +/// Expand loop contracts macros. +/// +/// A while loop of the form +/// ``` rust +/// while guard { +/// body +/// } +/// ``` +/// will be annotated as +/// ``` rust +/// #[inline(never)] +/// #[kanitool::fn_marker = "kani_register_loop_contract"] +/// const fn kani_register_loop_contract_id T>(f: F) -> T { +/// unreachable!() +/// } +/// while kani_register_loop_contract_id(|| -> bool {inv};) && guard { +/// body +/// } +/// ``` +pub fn loop_invariant(attr: TokenStream, item: TokenStream) -> TokenStream { + // parse the stmt of the loop + let mut loop_stmt: Stmt = syn::parse(item.clone()).unwrap(); + + // name of the loop invariant as closure of the form + // __kani_loop_invariant_#startline_#startcol_#endline_#endcol + let mut inv_name: String = "__kani_loop_invariant".to_owned(); + let loop_id = generate_unique_id_from_span(&loop_stmt); + inv_name.push_str(&loop_id); + + // expr of the loop invariant + let inv_expr: Expr = syn::parse(attr).unwrap(); + + // ident of the register function + let mut register_name: String = "kani_register_loop_contract".to_owned(); + register_name.push_str(&loop_id); + let register_ident = format_ident!("{}", register_name); + + match loop_stmt { + Stmt::Expr(ref mut e, _) => match e { + Expr::While(ref mut ew) => { + let new_cond: Expr = syn::parse( + quote!( + #register_ident(&||->bool{#inv_expr}, 0)) + .into(), + ) + .unwrap(); + *(ew.cond) = Expr::Binary(ExprBinary { + attrs: Vec::new(), + left: Box::new(new_cond), + op: BinOp::And(AndAnd::default()), + right: ew.cond.clone(), + }); + } + _ => { + abort_call_site!("`#[kani::loop_invariant]` is now only supported for while-loops."; + note = "for now, loop contracts is only supported for while-loops."; + ) + } + }, + _ => abort_call_site!("`#[kani::loop_invariant]` is now only supported for while-loops."; + note = "for now, loop contracts is only supported for while-loops."; + ), + } + quote!( + { + // Dummy function used to force the compiler to capture the environment. + // We cannot call closures inside constant functions. + // This function gets replaced by `kani::internal::call_closure`. + #[inline(never)] + #[kanitool::fn_marker = "kani_register_loop_contract"] + const fn #register_ident bool>(_f: &F, _transformed: usize) -> bool { + true + } + #loop_stmt}) + .into() +} + +fn generate_unique_id_from_span(stmt: &Stmt) -> String { + // Extract the span of the expression + let span = stmt.span().unwrap(); + + // Get the start and end line and column numbers + let start = span.start(); + let end = span.end(); + + // Create a tuple of location information (file path, start line, start column, end line, end column) + format!("_{:?}_{:?}_{:?}_{:?}", start.line(), start.column(), end.line(), end.column()) +} diff --git a/tests/expected/loop-contract/count_zero.expected b/tests/expected/loop-contract/count_zero.expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/expected/loop-contract/count_zero.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/loop-contract/count_zero.rs b/tests/expected/loop-contract/count_zero.rs new file mode 100644 index 000000000000..1b6cee925c97 --- /dev/null +++ b/tests/expected/loop-contract/count_zero.rs @@ -0,0 +1,35 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// kani-flags: -Z loop-contracts + +//! Check if loop contracts is correctly applied. + +#![feature(stmt_expr_attributes)] +#![feature(proc_macro_hygiene)] + +pub const BASE: usize = count_zero(&[]); + +const fn count_zero(slice: &[u8]) -> usize { + let mut counter: usize = 0; + let mut index: usize = 0; + + #[kani::loop_invariant(index <= slice.len() && counter <= slice.len() && counter == 0 )] + while index < slice.len() { + if slice[index] == 0 { + counter += 1; + } + index += 1; + } + + counter +} + +#[kani::proof] +pub fn check_counter() { + // Needed to avoid having `free` be removed as unused function. This is + // because DFCC contract enforcement assumes that a definition for `free` + // exists. + let _ = Box::new(10); + assert_eq!(count_zero(&[1, 2, 3]), 0) +} diff --git a/tests/expected/loop-contract/count_zero_loop_contracts_disable.expected b/tests/expected/loop-contract/count_zero_loop_contracts_disable.expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/expected/loop-contract/count_zero_loop_contracts_disable.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/loop-contract/count_zero_loop_contracts_disable.rs b/tests/expected/loop-contract/count_zero_loop_contracts_disable.rs new file mode 100644 index 000000000000..b64fbadeb4a4 --- /dev/null +++ b/tests/expected/loop-contract/count_zero_loop_contracts_disable.rs @@ -0,0 +1,30 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check if harness work loop contracts macro can be proved correctly +//! without loop contracts enable. + +#![feature(stmt_expr_attributes)] +#![feature(proc_macro_hygiene)] + +pub const BASE: usize = count_zero(&[]); + +#[kani::proof] +pub fn check_counter() { + assert_eq!(count_zero(&[1, 2, 3]), 0) +} + +const fn count_zero(slice: &[u8]) -> usize { + let mut counter: usize = 0; + let mut index: usize = 0; + + #[kani::loop_invariant(index <= slice.len() && counter <= slice.len() && counter == 0 )] + while index < slice.len() { + if slice[index] == 0 { + counter += 1; + } + index += 1; + } + + counter +} diff --git a/tests/expected/loop-contract/fixme_box.expected b/tests/expected/loop-contract/fixme_box.expected new file mode 100644 index 000000000000..59982b8b57a6 --- /dev/null +++ b/tests/expected/loop-contract/fixme_box.expected @@ -0,0 +1 @@ +internal error: entered unreachable code: The loop invariant support only reference of user variables. The provided invariants contain unsupported dereference.\ \ No newline at end of file diff --git a/tests/expected/loop-contract/fixme_box.rs b/tests/expected/loop-contract/fixme_box.rs new file mode 100644 index 000000000000..35dc0210d971 --- /dev/null +++ b/tests/expected/loop-contract/fixme_box.rs @@ -0,0 +1,25 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// kani-flags: -Z loop-contracts + +//! Loop contracts in CBMC backend doesn't support malloc or free in loop bodies. +//! Tracked in: https://github.com/model-checking/kani/issues/3587 + +#![feature(stmt_expr_attributes)] +#![feature(proc_macro_hygiene)] + +type Data = u8; + +#[kani::proof] +fn box_harness() { + let mut i: u8 = 0; + + let mut data: Box = Box::new(0); + + #[kani::loop_invariant(*data == i)] + while i < 10 { + i += 1; + data = Box::new(i); + } +} diff --git a/tests/expected/loop-contract/memchar_naive.expected b/tests/expected/loop-contract/memchar_naive.expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/expected/loop-contract/memchar_naive.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/loop-contract/memchar_naive.rs b/tests/expected/loop-contract/memchar_naive.rs new file mode 100644 index 000000000000..140d9f6342ed --- /dev/null +++ b/tests/expected/loop-contract/memchar_naive.rs @@ -0,0 +1,36 @@ +// Copyright rustc Contributors +// Adapted from rust std: https://github.com/rust-lang/rust/blob/master/library/core/src/slice/memchr.rs#L38 +// +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Modifications Copyright Kani Contributors +// See GitHub history for details. + +// kani-flags: -Z loop-contracts + +#![feature(stmt_expr_attributes)] +#![feature(proc_macro_hygiene)] + +#[kani::proof] +fn memchar_naive_harness() { + // Needed to avoid having `free` be removed as unused function. This is + // because DFCC contract enforcement assumes that a definition for `free` + // exists. + let _ = Box::new(10); + let text = [1, 2, 3, 4, 5]; + let x = 5; + let mut i = 0; + let mut r: Option = None; + + #[kani::loop_invariant(i <= text.len() && ((i == 0) || text[i-1]!= x))] + while i < text.len() { + if text[i] == x { + r = Some(i); + break; + } + + i += 1; + } + + assert_eq!(r, Some(4)); +} diff --git a/tests/expected/loop-contract/multiple_loops.expected b/tests/expected/loop-contract/multiple_loops.expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/expected/loop-contract/multiple_loops.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/loop-contract/multiple_loops.rs b/tests/expected/loop-contract/multiple_loops.rs new file mode 100644 index 000000000000..5fa2d6b9889a --- /dev/null +++ b/tests/expected/loop-contract/multiple_loops.rs @@ -0,0 +1,53 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// kani-flags: -Z loop-contracts --enable-unstable --cbmc-args --object-bits 8 + +//! Check if loop contracts is correctly applied. + +#![feature(stmt_expr_attributes)] +#![feature(proc_macro_hygiene)] + +fn multiple_loops() { + let mut x: u8 = kani::any_where(|i| *i >= 10); + + #[kani::loop_invariant(x >= 5)] + while x > 5 { + x = x - 1; + } + + assert!(x == 5); + + #[kani::loop_invariant(x >= 2)] + while x > 2 { + x = x - 1; + } + + assert!(x == 2); +} + +fn simple_while_loops() { + let mut x: u8 = kani::any_where(|i| *i >= 10); + let mut y: u8 = kani::any_where(|i| *i >= 10); + + #[kani::loop_invariant(x >= 2)] + while x > 2 { + x = x - 1; + #[kani::loop_invariant(y >= 2)] + while y > 2 { + y = y - 1; + } + } + + assert!(x == 2); +} + +#[kani::proof] +fn multiple_loops_harness() { + // Needed to avoid having `free` be removed as unused function. This is + // because DFCC contract enforcement assumes that a definition for `free` + // exists. + let _ = Box::new(10); + multiple_loops(); + simple_while_loops(); +} diff --git a/tests/expected/loop-contract/simple_while_loop.expected b/tests/expected/loop-contract/simple_while_loop.expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/expected/loop-contract/simple_while_loop.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/loop-contract/simple_while_loop.rs b/tests/expected/loop-contract/simple_while_loop.rs new file mode 100644 index 000000000000..6880d86d673a --- /dev/null +++ b/tests/expected/loop-contract/simple_while_loop.rs @@ -0,0 +1,26 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// kani-flags: -Z loop-contracts + +//! Check if loop contracts is correctly applied. + +#![feature(stmt_expr_attributes)] +#![feature(proc_macro_hygiene)] + +#[kani::proof] +#[kani::solver(kissat)] +fn simple_while_loop_harness() { + // Needed to avoid having `free` be removed as unused function. This is + // because DFCC contract enforcement assumes that a definition for `free` + // exists. + let _ = Box::new(10); + let mut x: u8 = kani::any_where(|i| *i >= 2); + + #[kani::loop_invariant(x >= 2)] + while x > 2 { + x = x - 1; + } + + assert!(x == 2); +} diff --git a/tests/expected/loop-contract/small_slice_eq.expected b/tests/expected/loop-contract/small_slice_eq.expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/expected/loop-contract/small_slice_eq.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/loop-contract/small_slice_eq.rs b/tests/expected/loop-contract/small_slice_eq.rs new file mode 100644 index 000000000000..a59436122da5 --- /dev/null +++ b/tests/expected/loop-contract/small_slice_eq.rs @@ -0,0 +1,51 @@ +// Copyright rustc Contributors +// Adapted from rust std: https://github.com/rust-lang/rust/blob/master/library/core/src/str/pattern.rs#L1885 +// +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Modifications Copyright Kani Contributors +// See GitHub history for details. + +// kani-flags: -Z loop-contracts --enable-unstable --cbmc-args --arrays-uf-always --no-standard-checks --object-bits 8 + +//! Check if loop contracts are correctly applied. The flag --no-standard-checks should be +//! removed once same_object predicate is supported in loop contracts. + +#![feature(stmt_expr_attributes)] +#![feature(proc_macro_hygiene)] +#![feature(ptr_sub_ptr)] +unsafe fn small_slice_eq(x: &[u8], y: &[u8]) -> bool { + debug_assert_eq!(x.len(), y.len()); + unsafe { + let (mut px, mut py) = (x.as_ptr(), y.as_ptr()); + let (pxend, pyend) = (px.add(x.len() - 4), py.add(y.len() - 4)); + #[kani::loop_invariant( px as isize >= x.as_ptr() as isize + && py as isize >= y.as_ptr() as isize + && px as isize - x.as_ptr() as isize == (py as isize - y.as_ptr() as isize))] + while px < pxend { + let vx = (px as *const u32).read_unaligned(); + let vy = (py as *const u32).read_unaligned(); + if vx != vy { + return false; + } + px = px.add(4); + py = py.add(4); + } + let vx = (pxend as *const u32).read_unaligned(); + let vy = (pyend as *const u32).read_unaligned(); + vx == vy + } +} + +#[kani::proof] +fn small_slice_eq_harness() { + // Needed to avoid having `free` be removed as unused function. This is + // because DFCC contract enforcement assumes that a definition for `free` + // exists. + let _ = Box::new(10); + let mut a = [1; 2000]; + let mut b = [1; 2000]; + unsafe { + small_slice_eq(&mut a, &mut b); + } +}