diff --git a/cprover_bindings/src/goto_program/symbol.rs b/cprover_bindings/src/goto_program/symbol.rs index ad71b0f84346..457be1163a3a 100644 --- a/cprover_bindings/src/goto_program/symbol.rs +++ b/cprover_bindings/src/goto_program/symbol.rs @@ -8,6 +8,8 @@ use std::fmt::Display; /// Based off the CBMC symbol implementation here: /// +/// +/// TODO: We should consider using BitFlags for all the boolean flags. #[derive(Clone, Debug)] pub struct Symbol { /// Unique identifier. Mangled name from compiler `foo12_bar17_x@1` @@ -46,6 +48,14 @@ pub struct Symbol { pub is_thread_local: bool, pub is_volatile: bool, pub is_weak: bool, + + /// This flag marks a variable as constant (IrepId: `ID_C_constant`). + /// + /// In CBMC, this is a property of the type or expression. However, we keep it here to avoid + /// having to propagate the attribute to all variants of `Type` and `Expr`. + /// + /// During contract verification, CBMC will not havoc static variables marked as constant. + pub is_static_const: bool, } /// The equivalent of a "mathematical function" in CBMC. Semantically this is an @@ -157,6 +167,7 @@ impl Symbol { is_lvalue: false, is_parameter: false, is_static_lifetime: false, + is_static_const: false, is_thread_local: false, is_volatile: false, is_weak: false, @@ -363,6 +374,11 @@ impl Symbol { self } + pub fn set_is_static_const(&mut self, v: bool) -> &mut Symbol { + self.is_static_const = v; + self + } + pub fn with_is_state_var(mut self, v: bool) -> Symbol { self.is_state_var = v; self @@ -383,11 +399,21 @@ impl Symbol { self } + pub fn set_pretty_name>(&mut self, pretty_name: T) -> &mut Symbol { + self.pretty_name = Some(pretty_name.into()); + self + } + pub fn with_is_hidden(mut self, hidden: bool) -> Symbol { self.is_auxiliary = hidden; self } + pub fn set_is_hidden(&mut self, hidden: bool) -> &mut Symbol { + self.is_auxiliary = hidden; + self + } + /// Set `is_property`. pub fn with_is_property(mut self, v: bool) -> Self { self.is_property = v; diff --git a/cprover_bindings/src/goto_program/symbol_table.rs b/cprover_bindings/src/goto_program/symbol_table.rs index 8125c8df3cd9..cd5bd8a6d967 100644 --- a/cprover_bindings/src/goto_program/symbol_table.rs +++ b/cprover_bindings/src/goto_program/symbol_table.rs @@ -107,6 +107,11 @@ impl SymbolTable { self.symbol_table.get(&name) } + pub fn lookup_mut>(&mut self, name: T) -> Option<&mut Symbol> { + let name = name.into(); + self.symbol_table.get_mut(&name) + } + pub fn machine_model(&self) -> &MachineModel { &self.machine_model } diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs index d1e84669121d..05774fdf8b43 100644 --- a/cprover_bindings/src/irep/to_irep.rs +++ b/cprover_bindings/src/irep/to_irep.rs @@ -598,6 +598,10 @@ impl goto_program::Symbol { Irep::just_sub(contract.assigns.iter().map(|req| req.to_irep(mm)).collect()), ); } + if self.is_static_const { + // Add a `const` to the type. + typ = typ.with_named_sub(IrepId::CConstant, Irep::just_id(IrepId::from_int(1))) + } super::Symbol { typ, value: match &self.value { diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 5549edcced25..85bb8292ec67 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -3,13 +3,13 @@ use crate::codegen_cprover_gotoc::utils::slice_fat_ptr; use crate::codegen_cprover_gotoc::GotocCtx; use crate::unwrap_or_return_codegen_unimplemented; -use cbmc::goto_program::{DatatypeComponent, Expr, ExprValue, Location, Stmt, Symbol, Type}; +use cbmc::goto_program::{DatatypeComponent, Expr, ExprValue, Location, Symbol, Type}; use rustc_middle::ty::Const as ConstInternal; use rustc_smir::rustc_internal; use rustc_span::Span as SpanInternal; use stable_mir::mir::alloc::{AllocId, GlobalAlloc}; use stable_mir::mir::mono::{Instance, StaticDef}; -use stable_mir::mir::Operand; +use stable_mir::mir::{Mutability, Operand}; use stable_mir::ty::{ Allocation, ConstantKind, FloatTy, FnDef, GenericArgs, IntTy, MirConst, RigidTy, Size, Ty, TyConst, TyConstKind, TyKind, UintTy, @@ -470,11 +470,17 @@ impl<'tcx> GotocCtx<'tcx> { name: Option, loc: Location, ) -> Expr { - debug!(?name, "codegen_const_allocation"); + debug!(?name, ?alloc, "codegen_const_allocation"); let alloc_name = match self.alloc_map.get(alloc) { None => { let alloc_name = if let Some(name) = name { name } else { self.next_global_name() }; - self.codegen_alloc_in_memory(alloc.clone(), alloc_name.clone(), loc); + let has_interior_mutabity = false; // Constants cannot be mutated. + self.codegen_alloc_in_memory( + alloc.clone(), + alloc_name.clone(), + loc, + has_interior_mutabity, + ); alloc_name } Some(name) => name.clone(), @@ -484,13 +490,18 @@ impl<'tcx> GotocCtx<'tcx> { mem_place.address_of() } - /// Insert an allocation into the goto symbol table, and generate a goto function that will - /// initialize it. + /// Insert an allocation into the goto symbol table, and generate an init value. /// - /// This function is ultimately responsible for creating new statically initialized global variables - /// in our goto binaries. - pub fn codegen_alloc_in_memory(&mut self, alloc: Allocation, name: String, loc: Location) { - debug!(?alloc, ?name, "codegen_alloc_in_memory"); + /// This function is ultimately responsible for creating new statically initialized global + /// variables. + pub fn codegen_alloc_in_memory( + &mut self, + alloc: Allocation, + name: String, + loc: Location, + has_interior_mutabity: bool, + ) { + debug!(?name, ?alloc, "codegen_alloc_in_memory"); let struct_name = &format!("{name}::struct"); // The declaration of a static variable may have one type and the constant initializer for @@ -513,50 +524,40 @@ impl<'tcx> GotocCtx<'tcx> { .collect() }); + // Create the allocation from a byte array. + let init_fn = |gcx: &mut GotocCtx, var: Symbol| { + let val = Expr::struct_expr_from_values( + alloc_typ_ref.clone(), + alloc_data + .iter() + .map(|d| match d { + AllocData::Bytes(bytes) => Expr::array_expr( + Type::unsigned_int(8).array_of(bytes.len()), + bytes + .iter() + // We should consider adding a poison / undet where we have none + // This mimics the behaviour before StableMIR though. + .map(|b| Expr::int_constant(b.unwrap_or(0), Type::unsigned_int(8))) + .collect(), + ), + AllocData::Expr(e) => e.clone(), + }) + .collect(), + &gcx.symbol_table, + ); + if val.typ() == &var.typ { val } else { val.transmute_to(var.typ, &gcx.symbol_table) } + }; + // The global static variable may not be in the symbol table if we are dealing - // with a literal that can be statically allocated. - // We need to make a constructor whether it was in the table or not, so we can't use the - // closure argument to ensure_global_var to do that here. - let var = self.ensure_global_var( + // with a promoted constant. + let _var = self.ensure_global_var_init( &name, false, //TODO is this correct? + alloc.mutability == Mutability::Not && !has_interior_mutabity, alloc_typ_ref.clone(), loc, - |_, _| None, - ); - let var_typ = var.typ().clone(); - - // Assign the initial value `val` to `var` via an intermediate `temp_var` to allow for - // transmuting the allocation type to the global static variable type. - let val = Expr::struct_expr_from_values( - alloc_typ_ref.clone(), - alloc_data - .iter() - .map(|d| match d { - AllocData::Bytes(bytes) => Expr::array_expr( - Type::unsigned_int(8).array_of(bytes.len()), - bytes - .iter() - // We should consider adding a poison / undet where we have none - // This mimics the behaviour before StableMIR though. - .map(|b| Expr::int_constant(b.unwrap_or(0), Type::unsigned_int(8))) - .collect(), - ), - AllocData::Expr(e) => e.clone(), - }) - .collect(), - &self.symbol_table, - ); - let fn_name = Self::initializer_fn_name(&name); - let temp_var = self.gen_function_local_variable(0, &fn_name, alloc_typ_ref, loc).to_expr(); - let body = Stmt::block( - vec![ - Stmt::decl(temp_var.clone(), Some(val), loc), - var.assign(temp_var.transmute_to(var_typ, &self.symbol_table), loc), - ], - loc, + init_fn, ); - self.register_initializer(&name, body); self.alloc_map.insert(alloc, name); } @@ -663,12 +664,6 @@ impl<'tcx> GotocCtx<'tcx> { let fn_item_struct_ty = self.codegen_fndef_type_stable(instance); // This zero-sized object that a function name refers to in Rust is globally unique, so we create such a global object. let fn_singleton_name = format!("{mangled_name}::FnDefSingleton"); - self.ensure_global_var( - &fn_singleton_name, - false, - fn_item_struct_ty, - loc, - |_, _| None, // zero-sized, so no initialization necessary - ) + self.ensure_global_var(&fn_singleton_name, false, fn_item_struct_ty, loc).to_expr() } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index f84708b9bdd5..4883c608f482 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -1444,9 +1444,10 @@ impl<'tcx> GotocCtx<'tcx> { let vtable_name = self.vtable_name_stable(trait_type).intern(); let vtable_impl_name = format!("{vtable_name}_impl_for_{src_name}"); - self.ensure_global_var( + self.ensure_global_var_init( vtable_impl_name, true, + true, Type::struct_tag(vtable_name), loc, |ctx, var| { @@ -1487,11 +1488,10 @@ impl<'tcx> GotocCtx<'tcx> { vtable_fields, &ctx.symbol_table, ); - let body = var.assign(vtable, loc); - let block = Stmt::block(vec![size_assert, body], loc); - Some(block) + Expr::statement_expression(vec![size_assert, vtable.as_stmt(loc)], var.typ, loc) }, ) + .to_expr() } /// Cast a pointer to a fat pointer. diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index c606ae13d095..697cacd3b191 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -317,9 +317,8 @@ impl<'tcx> GotocCtx<'tcx> { fn codegen_ret_unit(&mut self, loc: Location) -> Stmt { let is_file_local = false; let ty = self.codegen_ty_unit(); - let var = - self.ensure_global_var(FN_RETURN_VOID_VAR_NAME, is_file_local, ty, loc, |_, _| None); - Stmt::ret(Some(var), loc) + let var = self.ensure_global_var(FN_RETURN_VOID_VAR_NAME, is_file_local, ty, loc); + Stmt::ret(Some(var.to_expr()), loc) } /// Generates Goto-C for MIR [TerminatorKind::Drop] calls. We only handle code _after_ Rust's "drop elaboration" diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs index e05da3f7f622..537fbcb63fbb 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs @@ -4,7 +4,7 @@ //! This file contains functions related to codegenning MIR static variables into gotoc use crate::codegen_cprover_gotoc::GotocCtx; -use cbmc::goto_program::Symbol; +use crate::kani_middle::is_interior_mut; use stable_mir::mir::mono::{Instance, StaticDef}; use stable_mir::CrateDef; use tracing::debug; @@ -19,7 +19,12 @@ impl<'tcx> GotocCtx<'tcx> { debug!("codegen_static"); let alloc = def.eval_initializer().unwrap(); let symbol_name = Instance::from(def).mangled_name(); - self.codegen_alloc_in_memory(alloc, symbol_name, self.codegen_span_stable(def.span())); + self.codegen_alloc_in_memory( + alloc, + symbol_name, + self.codegen_span_stable(def.span()), + is_interior_mut(self.tcx, def.ty()), + ); } /// Mutates the Goto-C symbol table to add a forward-declaration of the static variable. @@ -37,9 +42,8 @@ impl<'tcx> GotocCtx<'tcx> { // havoc static variables. Kani uses the location and pretty name to identify // the correct variables. If the wrong name is used, CBMC may fail silently. // More details at https://github.com/diffblue/cbmc/issues/8225. - let symbol = Symbol::static_variable(symbol_name.clone(), symbol_name, typ, location) - .with_is_hidden(false) // Static items are always user defined. - .with_pretty_name(pretty_name); - self.symbol_table.insert(symbol); + self.ensure_global_var(symbol_name, false, typ, location) + .set_is_hidden(false) // Static items are always user defined. + .set_pretty_name(pretty_name); } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs index 7d51cff037c6..e360cd491edd 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -21,7 +21,9 @@ use crate::codegen_cprover_gotoc::utils::full_crate_name; use crate::codegen_cprover_gotoc::UnsupportedConstructs; use crate::kani_middle::transform::BodyTransformation; use crate::kani_queries::QueryDb; -use cbmc::goto_program::{DatatypeComponent, Expr, Location, Stmt, Symbol, SymbolTable, Type}; +use cbmc::goto_program::{ + DatatypeComponent, Expr, Location, Stmt, Symbol, SymbolTable, SymbolValues, Type, +}; use cbmc::utils::aggr_tag; use cbmc::{InternedString, MachineModel}; use rustc_data_structures::fx::FxHashMap; @@ -38,6 +40,7 @@ use rustc_target::abi::{HasDataLayout, TargetDataLayout}; use stable_mir::mir::mono::Instance; use stable_mir::mir::Body; use stable_mir::ty::Allocation; +use std::fmt::Debug; pub struct GotocCtx<'tcx> { /// the typing context @@ -200,34 +203,58 @@ impl<'tcx> GotocCtx<'tcx> { self.symbol_table.lookup(name).unwrap() } + /// Ensures that a global variable `name` appears in the Symbol table and is initialized. + /// + /// This will add the symbol to the Symbol Table if not inserted yet. + /// This will register the initialization function if not initialized yet. + /// - This case can happen for static variables, since they are declared first. + pub fn ensure_global_var_init( + &mut self, + name: T, + is_file_local: bool, + is_const: bool, + t: Type, + loc: Location, + init: F, + ) -> &mut Symbol + where + T: Into + Clone + Debug, + F: Fn(&mut GotocCtx, Symbol) -> Expr, + { + let sym = self.ensure_global_var(name.clone(), is_file_local, t, loc); + sym.set_is_static_const(is_const); + if matches!(sym.value, SymbolValues::None) { + // Clone sym so we can use `&mut self`. + let sym = sym.clone(); + let init_expr = SymbolValues::Expr(init(self, sym)); + // Need to lookup again since symbol table might've changed. + let sym = self.symbol_table.lookup_mut(name).unwrap(); + sym.value = init_expr; + sym + } else { + self.symbol_table.lookup_mut(name).unwrap() + } + } + /// Ensures that a global variable `name` appears in the Symbol table. - /// If it doesn't, inserts it. - /// If `init_fn` returns `Some(body)`, creates an initializer for the variable using `body`. - /// Otherwise, leaves the variable uninitialized . - pub fn ensure_global_var< - F: FnOnce(&mut GotocCtx<'tcx>, Expr) -> Option, - T: Into, - >( + /// + /// This will add the symbol to the Symbol Table if not inserted yet. + pub fn ensure_global_var + Clone>( &mut self, name: T, is_file_local: bool, t: Type, loc: Location, - init_fn: F, - ) -> Expr { - let name = name.into(); - if !self.symbol_table.contains(name) { - tracing::debug!(?name, "Ensure global variable"); - let sym = Symbol::static_variable(name, name, t, loc) + ) -> &mut Symbol { + let sym_name = name.clone().into(); + if !self.symbol_table.contains(sym_name) { + tracing::debug!(?sym_name, "ensure_global_var insert"); + let sym = Symbol::static_variable(sym_name, sym_name, t, loc) .with_is_file_local(is_file_local) .with_is_hidden(false); - let var = sym.to_expr(); - self.symbol_table.insert(sym); - if let Some(body) = init_fn(self, var) { - self.register_initializer(&name.to_string(), body); - } + self.symbol_table.insert(sym.clone()); } - self.symbol_table.lookup(name).unwrap().to_expr() + self.symbol_table.lookup_mut(sym_name).unwrap() } /// Ensures that a struct with name `struct_name` appears in the symbol table. @@ -284,23 +311,6 @@ impl<'tcx> GotocCtx<'tcx> { } Type::union_tag(union_name) } - - /// Makes a `__attribute__((constructor)) fnname() {body}` initalizer function - pub fn register_initializer(&mut self, var_name: &str, body: Stmt) -> &Symbol { - let fn_name = Self::initializer_fn_name(var_name); - let pretty_name = format!("{var_name}::init"); - let loc = *body.location(); - self.ensure(&fn_name, |_tcx, _| { - Symbol::function( - &fn_name, - Type::code(vec![], Type::constructor()), - Some(Stmt::block(vec![body], loc)), //TODO is this block needed? - &pretty_name, - loc, - ) - .with_is_file_local(true) - }) - } } /// Mutators diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 3c300e9da52c..a7a512c86de3 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -19,8 +19,10 @@ use rustc_span::Span; use rustc_target::abi::call::FnAbi; use rustc_target::abi::{HasDataLayout, TargetDataLayout}; use stable_mir::mir::mono::MonoItem; -use stable_mir::ty::{FnDef, RigidTy, Span as SpanStable, TyKind}; +use stable_mir::ty::{FnDef, RigidTy, Span as SpanStable, Ty, TyKind}; +use stable_mir::visitor::{Visitable, Visitor as TyVisitor}; use stable_mir::CrateDef; +use std::ops::ControlFlow; use self::attributes::KaniAttributes; @@ -62,6 +64,36 @@ pub fn check_crate_items(tcx: TyCtxt, ignore_asm: bool) { tcx.dcx().abort_if_errors(); } +/// Traverse the type definition to see if the type contains interior mutability. +/// +/// See for more details. +pub fn is_interior_mut(tcx: TyCtxt, ty: Ty) -> bool { + let mut visitor = FindUnsafeCell { tcx }; + visitor.visit_ty(&ty) == ControlFlow::Break(()) +} + +struct FindUnsafeCell<'tcx> { + tcx: TyCtxt<'tcx>, +} + +impl<'tcx> TyVisitor for FindUnsafeCell<'tcx> { + type Break = (); + fn visit_ty(&mut self, ty: &Ty) -> ControlFlow { + match ty.kind() { + TyKind::RigidTy(RigidTy::Adt(def, _)) + if rustc_internal::internal(self.tcx, def).is_unsafe_cell() => + { + ControlFlow::Break(()) + } + TyKind::RigidTy(RigidTy::Ref(..) | RigidTy::RawPtr(..)) => { + // We only care about the current memory space. + ControlFlow::Continue(()) + } + _ => ty.super_visit(self), + } + } +} + /// Check that all given items are supported and there's no misconfiguration. /// This method will exhaustively print any error / warning and it will abort at the end if any /// error was found. diff --git a/tests/expected/uninit/access-static-padding.expected b/tests/expected/uninit/access-static-padding.expected new file mode 100644 index 000000000000..5577aa3684c5 --- /dev/null +++ b/tests/expected/uninit/access-static-padding.expected @@ -0,0 +1,12 @@ +Checking harness check_read_assoc_const_padding_fails... +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const [u8; 32]` + +Checking harness check_read_static_padding_fails... +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const [u8; 8]` + +Checking harness check_read_const_padding_fails... +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const [u8; 4]` + +Verification failed for - check_read_assoc_const_padding_fails +Verification failed for - check_read_static_padding_fails +Verification failed for - check_read_const_padding_fails diff --git a/tests/expected/uninit/access-static-padding.rs b/tests/expected/uninit/access-static-padding.rs new file mode 100644 index 000000000000..5e9edb5ff9fc --- /dev/null +++ b/tests/expected/uninit/access-static-padding.rs @@ -0,0 +1,34 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z uninit-checks +//! Add a check to ensure that we correctly detect reading the padding values of a static and +//! also of a constant. + +#![feature(generic_const_exprs)] + +/// Check if all the values in the buffer is equals to zero. +unsafe fn is_zeroed(orig: *const T) -> bool +where + [(); size_of::()]:, +{ + let buf = orig as *const [u8; size_of::()]; + unsafe { &*buf }.iter().all(|val| *val == 0) +} + +const CONST_PADDING: (u8, u16) = (0, 0); +static STATIC_PADDING: (u8, char) = (0, '\0'); + +#[kani::proof] +fn check_read_const_padding_fails() { + assert!(unsafe { is_zeroed(&CONST_PADDING) }); +} + +#[kani::proof] +fn check_read_static_padding_fails() { + assert!(unsafe { is_zeroed(&STATIC_PADDING) }); +} + +#[kani::proof] +fn check_read_assoc_const_padding_fails() { + assert!(unsafe { is_zeroed(&(0u128, 0u16)) }); +} diff --git a/tests/kani/CodegenStatic/main.rs b/tests/kani/CodegenStatic/main.rs index 9731ca4fe080..7d2791268c7d 100644 --- a/tests/kani/CodegenStatic/main.rs +++ b/tests/kani/CodegenStatic/main.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT static STATIC: [&str; 1] = ["FOO"]; #[kani::proof] -fn main() { +fn check_static() { let x = STATIC[0]; let bytes = x.as_bytes(); assert!(bytes.len() == 3); diff --git a/tests/kani/CodegenStatic/struct.rs b/tests/kani/CodegenStatic/struct.rs index 441e118175b1..1801de3c7613 100644 --- a/tests/kani/CodegenStatic/struct.rs +++ b/tests/kani/CodegenStatic/struct.rs @@ -8,6 +8,24 @@ pub struct Foo { const x: Foo<3> = Foo { bytes: [1, 2, 3] }; #[kani::proof] -fn main() { +fn simple_struct() { assert!(x.bytes[0] == 1); } + +pub struct Outer { + data: char, + inner: Inner, +} + +pub struct Inner { + a: char, + b: char, + c: char, +} + +static OUTER: Outer = Outer { data: 'a', inner: Inner { a: 'a', b: 'b', c: 'c' } }; + +#[kani::proof] +fn nested_struct() { + assert!(OUTER.inner.c == 'c'); +} diff --git a/tests/kani/FunctionContracts/fixme_static_interior_mut.rs b/tests/kani/FunctionContracts/fixme_static_interior_mut.rs new file mode 100644 index 000000000000..1b18472b5590 --- /dev/null +++ b/tests/kani/FunctionContracts/fixme_static_interior_mut.rs @@ -0,0 +1,35 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts +//! This file is a duplicate of `static_interior_mut.rs` that captures the current over-approx +//! we perform for static variables with `UnsafeCell`. +//! When you fix this, please delete this file and enable the `regular_field` harness in the +//! original file. + +extern crate kani; + +use std::cell::UnsafeCell; + +pub struct WithMut { + regular_field: u8, + mut_field: UnsafeCell, +} + +/// Just for test purpose. +unsafe impl Sync for WithMut {} + +/// A static definition of `WithMut` +static ZERO_VAL: WithMut = WithMut { regular_field: 0, mut_field: UnsafeCell::new(0) }; + +/// The regular field should be 0. +#[kani::ensures(|result| *result == 0)] +pub fn regular_field() -> u8 { + ZERO_VAL.regular_field +} + +/// This harness is a copy from `static_interior_mut.rs`. +/// Once this gets fixed, please delete this file and enable the original one. +#[kani::proof_for_contract(regular_field)] +fn check_regular_field_is_const() { + assert_eq!(regular_field(), 0); // ** This should succeed since this field is constant. +} diff --git a/tests/kani/FunctionContracts/fixme_static_mut.rs b/tests/kani/FunctionContracts/fixme_static_mut.rs new file mode 100644 index 000000000000..0ee88a3e5ad5 --- /dev/null +++ b/tests/kani/FunctionContracts/fixme_static_mut.rs @@ -0,0 +1,46 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts +//! This test checks that contracts correctly handles mutable static. + +static mut WRAP_COUNTER: Option = None; + +/// This function is safe and should never crash. Counter starts at 0. +#[kani::modifies(std::ptr::addr_of!(WRAP_COUNTER))] +#[kani::ensures(|_| true)] +pub fn next() -> u32 { + // Safe in single-threaded. + unsafe { + match &WRAP_COUNTER { + Some(val) => { + WRAP_COUNTER = Some(val.wrapping_add(1)); + *val + } + None => { + WRAP_COUNTER = Some(0); + 0 + } + } + } +} + +/// This harness should succeed. +/// +/// Today, CBMC havocs WRAP_COUNTER, which includes invalid discriminants triggering UB. +#[kani::proof_for_contract(next)] +fn check_next() { + let _ret = next(); +} + +/// Without contracts, we can safely verify `next`. +#[kani::proof] +fn check_next_directly() { + // First check that initial iteration returns 0 (base case). + let first = next(); + assert_eq!(first, 0); + + // Havoc WRAP_COUNTER and invoke next. + unsafe { WRAP_COUNTER = kani::any() }; + let ret = next(); + kani::cover!(ret == 0); +} diff --git a/tests/kani/FunctionContracts/promoted_constants.rs b/tests/kani/FunctionContracts/promoted_constants.rs new file mode 100644 index 000000000000..75202f1bfedd --- /dev/null +++ b/tests/kani/FunctionContracts/promoted_constants.rs @@ -0,0 +1,54 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts +//! This test checks that contracts does not havoc +//! [promoted constants](https://github.com/rust-lang/const-eval/blob/master/promotion.md). +//! Related issue: + +extern crate kani; + +#[derive(PartialEq, Eq, kani::Arbitrary)] +pub struct Foo(u8); + +/// A named constant static should work the same way as a promoted constant. +static FOO: Foo = Foo(1); + +/// A mutable static that should be havocked before contract validation. +static mut FOO_MUT: Foo = Foo(1); + +/// Add a contract using a temporary variable that is lifted to a const static. +#[kani::requires(foo == Foo(1))] +pub fn foo_promoted(foo: Foo) -> Foo { + assert!(foo.0 == 1); + foo +} + +/// Add a contract using a const static. +#[kani::requires(foo == FOO)] +pub fn foo_static(foo: Foo) -> Foo { + assert!(foo.0 == 1); + foo +} + +/// Add a contract using a mutable static. +#[kani::requires(&foo == unsafe { &FOO_MUT })] +pub fn foo_mut_static(foo: Foo) -> Foo { + assert!(foo.0 == 1); + foo +} + +#[kani::proof_for_contract(foo_promoted)] +fn check_promoted() { + foo_promoted(kani::any()); +} + +#[kani::proof_for_contract(foo_static)] +fn check_static() { + foo_static(kani::any()); +} + +#[kani::proof_for_contract(foo_mut_static)] +#[kani::should_panic] +fn check_mut_static() { + foo_mut_static(kani::any()); +} diff --git a/tests/kani/FunctionContracts/promoted_constants_enum.rs b/tests/kani/FunctionContracts/promoted_constants_enum.rs new file mode 100644 index 000000000000..12878eee8044 --- /dev/null +++ b/tests/kani/FunctionContracts/promoted_constants_enum.rs @@ -0,0 +1,32 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts +//! This test checks that contracts does not havoc +//! [promoted constants](https://github.com/rust-lang/const-eval/blob/master/promotion.md) +//! that represents an enum variant. +//! +//! Related issue: + +extern crate kani; +#[derive(PartialEq, Eq, kani::Arbitrary)] +pub enum Foo { + A, + B, +} + +#[kani::ensures(|result: &Foo| *result == Foo::A)] +pub fn foo_a() -> Foo { + Foo::A +} + +#[kani::proof_for_contract(foo_a)] +fn check() { + let _ = foo_a(); +} + +#[kani::proof] +#[kani::stub_verified(foo_a)] +fn check_stub() { + let val = foo_a(); + assert!(val == Foo::A) +} diff --git a/tests/kani/FunctionContracts/static_interior_mut.rs b/tests/kani/FunctionContracts/static_interior_mut.rs new file mode 100644 index 000000000000..deb20e739fb3 --- /dev/null +++ b/tests/kani/FunctionContracts/static_interior_mut.rs @@ -0,0 +1,47 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts +//! This test checks that contracts havoc static variables with interior mutability. +//! For now, we over-approximate and havoc the entire static. + +extern crate kani; + +use std::cell::UnsafeCell; + +pub struct WithMut { + regular_field: u8, + mut_field: UnsafeCell, +} + +/// Just for test purpose. +unsafe impl Sync for WithMut {} + +/// A static definition of `WithMut` +static ZERO_VAL: WithMut = WithMut { regular_field: 0, mut_field: UnsafeCell::new(0) }; + +/// The regular field should be 0. +#[kani::ensures(|result| *result == 0)] +pub fn regular_field() -> u8 { + ZERO_VAL.regular_field +} + +/// The mutable field can be anything. +#[kani::ensures(|result| *result == old(unsafe { *ZERO_VAL.mut_field.get() }))] +pub unsafe fn mut_field() -> u8 { + unsafe { *ZERO_VAL.mut_field.get() } +} + +/// This harness is duplicated in `fixme_static_interior_mut.rs`. +/// Issue <> +#[cfg(fixme)] +#[kani::proof_for_contract(regular_field)] +fn check_regular_field_is_const() { + assert_eq!(regular_field(), 0); // ** This should succeed since this field is constant. +} + +// Ensure that Kani havoc the mutable field. +#[kani::should_panic] +#[kani::proof_for_contract(mut_field)] +fn check_regular_field_is_const() { + assert_eq!(unsafe { mut_field() }, 0); // ** This must fail since Kani havoc the mutable field. +}