diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index a3ddd7cac76f..da72a203d7dc 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -131,7 +131,7 @@ impl<'tcx> GotocCtx<'tcx> { // First try to generate the constant without allocating memory. let expr = self.try_codegen_constant(alloc, ty, loc).unwrap_or_else(|| { debug!("codegen_allocation try_fail"); - let mem_var = self.codegen_const_allocation(alloc, None, loc); + let mem_var = self.codegen_const_allocation(alloc, None, loc, true); mem_var .cast_to(Type::unsigned_int(8).to_pointer()) .cast_to(self.codegen_ty_stable(ty).to_pointer()) @@ -282,7 +282,7 @@ impl<'tcx> GotocCtx<'tcx> { let GlobalAlloc::Memory(data) = GlobalAlloc::from(alloc_id) else { unreachable!() }; - let mem_var = self.codegen_const_allocation(&data, None, loc); + let mem_var = self.codegen_const_allocation(&data, None, loc, false); // Extract identifier for static variable. // codegen_allocation_auto_imm_name returns the *address* of @@ -323,7 +323,7 @@ impl<'tcx> GotocCtx<'tcx> { let GlobalAlloc::Memory(data) = GlobalAlloc::from(alloc_id) else { unreachable!() }; - let mem_var = self.codegen_const_allocation(&data, None, loc); + let mem_var = self.codegen_const_allocation(&data, None, loc, false); let inner_typ = self.codegen_ty_stable(inner_ty); let len = data.bytes.len() / inner_typ.sizeof(&self.symbol_table) as usize; let data_expr = mem_var.cast_to(inner_typ.to_pointer()); @@ -394,7 +394,7 @@ impl<'tcx> GotocCtx<'tcx> { // crates do not conflict. The name alone is insufficient because Rust // allows different versions of the same crate to be used. let name = format!("{}::{alloc_id:?}", self.full_crate_name()); - self.codegen_const_allocation(&alloc, Some(name), loc) + self.codegen_const_allocation(&alloc, Some(name), loc, false) } alloc @ GlobalAlloc::VTable(..) => { // This is similar to GlobalAlloc::Memory but the type is opaque to rust and it @@ -404,7 +404,7 @@ impl<'tcx> GotocCtx<'tcx> { unreachable!() }; let name = format!("{}::{alloc_id:?}", self.full_crate_name()); - self.codegen_const_allocation(&alloc, Some(name), loc) + self.codegen_const_allocation(&alloc, Some(name), loc, false) } GlobalAlloc::TypeId { ty: _ } => todo!(), }; @@ -486,6 +486,7 @@ impl<'tcx> GotocCtx<'tcx> { alloc: &Allocation, name: Option, loc: Location, + is_definitely_const: bool, ) -> Expr { debug!(?name, ?alloc, "codegen_const_allocation"); let alloc_name = match self.alloc_map.get(alloc) { @@ -497,6 +498,7 @@ impl<'tcx> GotocCtx<'tcx> { alloc_name.clone(), loc, has_interior_mutabity, + is_definitely_const, ); alloc_name } @@ -517,7 +519,7 @@ impl<'tcx> GotocCtx<'tcx> { // The memory behind this allocation isn't constant, but codegen_alloc_in_memory (which codegen_const_allocation calls) // uses alloc's mutability field to set the const-ness of the allocation in CBMC's symbol table, // so we can reuse the code and without worrying that the allocation is set as immutable. - self.codegen_const_allocation(alloc, name, loc) + self.codegen_const_allocation(alloc, name, loc, false) } /// Insert an allocation into the goto symbol table, and generate an init value. @@ -530,6 +532,7 @@ impl<'tcx> GotocCtx<'tcx> { name: String, loc: Location, has_interior_mutabity: bool, + is_definitely_const: bool, ) { debug!(?name, ?alloc, "codegen_alloc_in_memory"); let struct_name = &format!("{name}::struct"); @@ -583,7 +586,7 @@ impl<'tcx> GotocCtx<'tcx> { let _var = self.ensure_global_var_init( &name, false, //TODO is this correct? - alloc.mutability == Mutability::Not && !has_interior_mutabity, + (is_definitely_const || alloc.mutability == Mutability::Not) && !has_interior_mutabity, alloc_typ_ref.clone(), loc, init_fn, 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 786f4f03ae36..2c87d87b3bd0 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs @@ -24,6 +24,7 @@ impl GotocCtx<'_> { symbol_name, self.codegen_span_stable(def.span()), is_interior_mut(self.tcx, def.ty()), + false, ); } diff --git a/tests/expected/function-contract/const_block.expected b/tests/expected/function-contract/const_block.expected new file mode 100644 index 000000000000..c5753d840eb0 --- /dev/null +++ b/tests/expected/function-contract/const_block.expected @@ -0,0 +1,11 @@ +assertion\ + - Status: SUCCESS\ + - Description: "|result| *result == Enum::Second"\ + +assertion\ + - Status: SUCCESS\ + - Description: "|result| *result == Enum::First"\ + +VERIFICATION:- SUCCESSFUL + +Complete - 5 successfully verified harnesses, 0 failures, 5 total. diff --git a/tests/expected/function-contract/const_block.rs b/tests/expected/function-contract/const_block.rs new file mode 100644 index 000000000000..e61f5899b053 --- /dev/null +++ b/tests/expected/function-contract/const_block.rs @@ -0,0 +1,74 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z function-contracts + +//! Checking that constant blocks are correctly verified in contracts. +//! See https://github.com/model-checking/kani/issues/3905 + +#![feature(ptr_alignment_type)] + +use std::mem; +use std::ptr::{Alignment, NonNull}; + +#[derive(PartialEq)] +enum Enum { + First, + Second, +} + +#[kani::ensures(|result| *result == Enum::First)] +const fn first() -> Enum { + const { Enum::First } +} + +#[kani::ensures(|result| *result == Enum::Second)] +const fn second() -> Enum { + Enum::Second +} + +#[kani::proof_for_contract(first)] +pub fn check_first() { + let _ = first(); +} + +#[kani::proof_for_contract(second)] +pub fn check_second() { + let _ = second(); +} + +#[kani::ensures(|result| result.as_usize().is_power_of_two())] +pub const fn Align_of() -> Alignment { + // This can't actually panic since type alignment is always a power of two. + const { Alignment::new(mem::align_of::()).unwrap() } +} + +#[kani::ensures(|result| result.as_usize().is_power_of_two())] +pub const fn Align_of_no_const() -> Alignment { + // This can't actually panic since type alignment is always a power of two. + Alignment::new(mem::align_of::()).unwrap() +} + +#[kani::proof_for_contract(Align_of)] +pub fn check_of_i32() { + let _ = Align_of::(); +} + +#[kani::proof_for_contract(Align_of_no_const)] +pub fn check_of_i32_no_const() { + let _ = Align_of_no_const::(); +} + +#[kani::requires(true)] +pub const unsafe fn byte_add_n(s: NonNull, count: usize) -> NonNull { + unsafe { NonNull::new_unchecked(s.as_ptr().byte_add(count)) } +} + +#[kani::proof_for_contract(byte_add_n)] +pub fn non_null_byte_add_dangling_proof() { + let ptr = NonNull::::dangling(); + assert!(ptr.as_ptr().addr() == 4); + assert!(ptr.as_ptr().addr() <= (isize::MAX as usize)); + unsafe { + let _ = byte_add_n(ptr, 0); + } +} diff --git a/tests/expected/function-contract/valid_ptr.expected b/tests/expected/function-contract/valid_ptr.expected index 38f31a63d5ca..0c43cd901cc9 100644 --- a/tests/expected/function-contract/valid_ptr.expected +++ b/tests/expected/function-contract/valid_ptr.expected @@ -4,9 +4,7 @@ Failed Checks: |result| kani::mem::can_dereference(result.0) VERIFICATION:- FAILED Checking harness pre_condition::harness_invalid_ptr... -Failed Checks: assertion failed: unsafe { read_ptr(ptr) } == -20 Failed Checks: Kani does not support reasoning about pointer to unallocated memory -Failed Checks: dereference failure: pointer outside object bounds VERIFICATION:- FAILED Checking harness pre_condition::harness_stack_ptr... diff --git a/tests/kani/FunctionContracts/modify_slice_elem_fixme.rs b/tests/kani/FunctionContracts/modify_slice_elem.rs similarity index 93% rename from tests/kani/FunctionContracts/modify_slice_elem_fixme.rs rename to tests/kani/FunctionContracts/modify_slice_elem.rs index 385db9983d88..15c0f6db9655 100644 --- a/tests/kani/FunctionContracts/modify_slice_elem_fixme.rs +++ b/tests/kani/FunctionContracts/modify_slice_elem.rs @@ -4,6 +4,7 @@ //! //! This started failing with the 2025-04-05 toolchain upgrade //! Tracking issue: https://github.com/model-checking/kani/issues/4029 +//! Was fixed with https://github.com/model-checking/kani/pull/4233 //! //! Note that this test used to crash while parsing the annotations. // kani-flags: -Zfunction-contracts