From ecbdb14bf4264cb2012a614f51626a61f30d2eb8 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Tue, 28 Jan 2025 16:42:33 -0500 Subject: [PATCH 1/4] Toolchain upgrade to nightly-2025-01-28 (#3855) Resolves https://github.com/model-checking/kani/issues/3854. This upgrade requires changes to remove `RunCompiler` due to the following changes: - https://github.com/rust-lang/rust/commit/a77776cc1d Remove RunCompiler By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Signed-off-by: Felipe R. Monteiro --- kani-compiler/src/kani_compiler.rs | 15 ++++++++------- kani-compiler/src/main.rs | 5 ++--- kani-compiler/src/session.rs | 2 +- rust-toolchain.toml | 2 +- 4 files changed, 12 insertions(+), 12 deletions(-) diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index 253a9b88a52c..e4bfba3113b0 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/kani-compiler/src/kani_compiler.rs @@ -3,7 +3,7 @@ //! This module defines all compiler extensions that form the Kani compiler. //! -//! The [KaniCompiler] can be used across multiple rustc driver runs ([RunCompiler::run()]), +//! The [KaniCompiler] can be used across multiple rustc driver runs ([`rustc_driver::run_compiler`]), //! which is used to implement stubs. //! //! In the first run, [KaniCompiler::config] will implement the compiler configuration and it will @@ -25,7 +25,7 @@ use crate::kani_queries::QueryDb; use crate::session::init_session; use clap::Parser; use rustc_codegen_ssa::traits::CodegenBackend; -use rustc_driver::{Callbacks, Compilation, RunCompiler}; +use rustc_driver::{Callbacks, Compilation, run_compiler}; use rustc_interface::Config; use rustc_middle::ty::TyCtxt; use rustc_session::config::ErrorOutputType; @@ -34,7 +34,7 @@ use std::sync::{Arc, Mutex}; use tracing::debug; /// Run the Kani flavour of the compiler. -/// This may require multiple runs of the rustc driver ([RunCompiler::run]). +/// This may require multiple runs of the rustc driver ([`rustc_driver::run_compiler`]). pub fn run(args: Vec) { let mut kani_compiler = KaniCompiler::new(); kani_compiler.run(args); @@ -96,10 +96,7 @@ impl KaniCompiler { /// actually invoke the rust compiler multiple times. pub fn run(&mut self, args: Vec) { debug!(?args, "run_compilation_session"); - let queries = self.queries.clone(); - let mut compiler = RunCompiler::new(&args, self); - compiler.set_make_codegen_backend(Some(Box::new(move |_cfg| backend(queries)))); - compiler.run(); + run_compiler(&args, self); } } @@ -108,6 +105,10 @@ impl Callbacks for KaniCompiler { /// Configure the [KaniCompiler] `self` object during the [CompilationStage::Init]. fn config(&mut self, config: &mut Config) { let mut args = vec!["kani-compiler".to_string()]; + config.make_codegen_backend = Some(Box::new({ + let queries = self.queries.clone(); + move |_cfg| backend(queries) + })); args.extend(config.opts.cg.llvm_args.iter().cloned()); let args = Arguments::parse_from(args); init_session(&args, matches!(config.opts.error_format, ErrorOutputType::Json { .. })); diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs index 65424f6d46bf..c8a56d3ef062 100644 --- a/kani-compiler/src/main.rs +++ b/kani-compiler/src/main.rs @@ -50,7 +50,7 @@ mod kani_middle; mod kani_queries; mod session; -use rustc_driver::{RunCompiler, TimePassesCallbacks}; +use rustc_driver::{TimePassesCallbacks, run_compiler}; use std::env; /// Main function. Configure arguments and run the compiler. @@ -63,8 +63,7 @@ fn main() { kani_compiler::run(rustc_args); } else { let mut callbacks = TimePassesCallbacks::default(); - let compiler = RunCompiler::new(&rustc_args, &mut callbacks); - compiler.run(); + run_compiler(&rustc_args, &mut callbacks); } } diff --git a/kani-compiler/src/session.rs b/kani-compiler/src/session.rs index f448afb801cc..5b4990790a10 100644 --- a/kani-compiler/src/session.rs +++ b/kani-compiler/src/session.rs @@ -57,7 +57,7 @@ static JSON_PANIC_HOOK: LazyLock) + Sync + let mut emitter = JsonEmitter::new( Box::new(io::BufWriter::new(io::stderr())), #[allow(clippy::arc_with_non_send_sync)] - Lrc::new(SourceMap::new(FilePathMapping::empty())), + Some(Lrc::new(SourceMap::new(FilePathMapping::empty()))), fallback_bundle, false, HumanReadableErrorType::Default, diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 9ae762092eb2..3741e551a5b8 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2025-01-24" +channel = "nightly-2025-01-28" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] From cc07375c43da544f202c44b298642f9bcdaef4f9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9mi=20Delmas?= Date: Tue, 28 Jan 2025 16:32:53 -0600 Subject: [PATCH 2/4] Allow multiple annotations, but check for duplicate targets. (#3808) Resolves #3804. Enables multiple `stub_verified(TARGET)` annotations on a harness, but still detect and report duplicate targets. Adds positive and negative tests. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Remi Delmas Co-authored-by: Celina G. Val Co-authored-by: Felipe R. Monteiro --- kani-compiler/src/kani_middle/attributes.rs | 32 ++++++++++++++++--- .../missing_contract_for_replace.expected | 2 +- .../multiple_replace_fail.expected | 1 + .../multiple_replace_fail.rs | 31 ++++++++++++++++++ .../multiple_replace_pass.expected | 1 + .../multiple_replace_pass.rs | 30 +++++++++++++++++ 6 files changed, 92 insertions(+), 5 deletions(-) create mode 100644 tests/expected/function-contract/multiple_replace_fail.expected create mode 100644 tests/expected/function-contract/multiple_replace_fail.rs create mode 100644 tests/expected/function-contract/multiple_replace_pass.expected create mode 100644 tests/expected/function-contract/multiple_replace_pass.rs diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 6d366f432e2a..bdd6db831d6c 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -394,7 +394,7 @@ impl<'tcx> KaniAttributes<'tcx> { attrs.iter().for_each(|attr| self.check_proof_attribute(kind, attr)) } KaniAttributeKind::StubVerified => { - expect_single(self.tcx, kind, &attrs); + self.check_stub_verified(); } KaniAttributeKind::FnMarker | KaniAttributeKind::CheckedWith @@ -591,15 +591,29 @@ impl<'tcx> KaniAttributes<'tcx> { } } - fn handle_stub_verified(&self, harness: &mut HarnessAttributes) { + fn check_stub_verified(&self) { let dcx = self.tcx.dcx(); + let mut seen = HashSet::new(); for (name, def_id, span) in self.interpret_stub_verified_attribute() { + if seen.contains(&name) { + dcx.struct_span_warn( + span, + format!("Multiple occurrences of `stub_verified({})`.", name), + ) + .with_span_note( + self.tcx.def_span(def_id), + format!("Use a single `stub_verified({})` annotation.", name), + ) + .emit(); + } else { + seen.insert(name); + } if KaniAttributes::for_item(self.tcx, def_id).contract_attributes().is_none() { dcx.struct_span_err( span, format!( - "Failed to generate verified stub: Function `{}` has no contract.", - self.item_name(), + "Target function in `stub_verified({})` has no contract.", + name, ), ) .with_span_note( @@ -612,6 +626,16 @@ impl<'tcx> KaniAttributes<'tcx> { .emit(); return; } + } + } + + /// Adds the verified stub names to the `harness.verified_stubs`. + /// + /// This method must be called after `check_stub_verified`, to ensure that + /// the target names are known and have contracts, and there are no + /// duplicate target names. + fn handle_stub_verified(&self, harness: &mut HarnessAttributes) { + for (name, _, _) in self.interpret_stub_verified_attribute() { harness.verified_stubs.push(name.to_string()) } } diff --git a/tests/expected/function-contract/missing_contract_for_replace.expected b/tests/expected/function-contract/missing_contract_for_replace.expected index 29f3fa955307..198838feca03 100644 --- a/tests/expected/function-contract/missing_contract_for_replace.expected +++ b/tests/expected/function-contract/missing_contract_for_replace.expected @@ -1,4 +1,4 @@ -error: Failed to generate verified stub: Function `harness` has no contract. +error: Target function in `stub_verified(no_contract)` has no contract. | 8 | #[kani::stub_verified(no_contract)] | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/tests/expected/function-contract/multiple_replace_fail.expected b/tests/expected/function-contract/multiple_replace_fail.expected new file mode 100644 index 000000000000..5e828259fcb6 --- /dev/null +++ b/tests/expected/function-contract/multiple_replace_fail.expected @@ -0,0 +1 @@ +warning: Multiple occurrences of `stub_verified(one)`. diff --git a/tests/expected/function-contract/multiple_replace_fail.rs b/tests/expected/function-contract/multiple_replace_fail.rs new file mode 100644 index 000000000000..ecd3c099b2ab --- /dev/null +++ b/tests/expected/function-contract/multiple_replace_fail.rs @@ -0,0 +1,31 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#[kani::ensures(|result : &u32| *result == 1)] +fn one() -> u32 { + 1 +} + +#[kani::proof_for_contract(one)] +fn check_one() { + let _ = one(); +} + +#[kani::ensures(|result : &u32| *result == 1)] +fn one_too() -> u32 { + 1 +} + +#[kani::proof_for_contract(one_too)] +fn check_one_too() { + let _ = one_too(); +} + +#[kani::proof] +#[kani::stub_verified(one)] +#[kani::stub_verified(one)] +#[kani::stub_verified(one_too)] +fn main() { + assert_eq!(one(), one_too()); +} diff --git a/tests/expected/function-contract/multiple_replace_pass.expected b/tests/expected/function-contract/multiple_replace_pass.expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/expected/function-contract/multiple_replace_pass.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/multiple_replace_pass.rs b/tests/expected/function-contract/multiple_replace_pass.rs new file mode 100644 index 000000000000..bd3cb81e136a --- /dev/null +++ b/tests/expected/function-contract/multiple_replace_pass.rs @@ -0,0 +1,30 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#[kani::ensures(|result : &u32| *result == 1)] +fn one() -> u32 { + 1 +} + +#[kani::proof_for_contract(one)] +fn check_one() { + let _ = one(); +} + +#[kani::ensures(|result : &u32| *result == 1)] +fn one_too() -> u32 { + 1 +} + +#[kani::proof_for_contract(one_too)] +fn check_one_too() { + let _ = one_too(); +} + +#[kani::proof] +#[kani::stub_verified(one)] +#[kani::stub_verified(one_too)] +fn main() { + assert_eq!(one(), one_too()); +} From ad91bfacd691d8a2f9c20f6b75c09923a061d60e Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Tue, 28 Jan 2025 16:58:42 -0600 Subject: [PATCH 3/4] Move documentation of kani_core modules to right places (#3851) Resolves #3815 [Documentations](https://github.com/model-checking/kani/blob/main/library/kani_core/src/mem.rs#L3) of `kani_core` modules doesn't show up correctly on https://model-checking.github.io/kani/crates/doc/kani/mem/index.html. This PR move the comments to the right place so that they will show up correctly. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- library/kani_core/src/float.rs | 2 +- library/kani_core/src/lib.rs | 50 +++++++++++++++++++++++++++++++ library/kani_core/src/mem.rs | 40 +++---------------------- library/kani_core/src/mem_init.rs | 15 ++-------- 4 files changed, 57 insertions(+), 50 deletions(-) diff --git a/library/kani_core/src/float.rs b/library/kani_core/src/float.rs index 44475af80a51..55fe71dbf24d 100644 --- a/library/kani_core/src/float.rs +++ b/library/kani_core/src/float.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -//! This module contains functions useful for float-related checks +// This module contains functions useful for float-related checks. #[allow(clippy::crate_in_macro_def)] #[macro_export] diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index 3ba2f459470e..37a05821bd33 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -67,14 +67,64 @@ macro_rules! kani_lib { kani_core::generate_models!(); pub mod float { + //! This module contains functions useful for float-related checks kani_core::generate_float!(std); } pub mod mem { + //! This module contains functions useful for checking unsafe memory access. + //! + //! Given the following validity rules provided in the Rust documentation: + //! (accessed Feb 6th, 2024) + //! + //! 1. A null pointer is never valid, not even for accesses of size zero. + //! 2. For a pointer to be valid, it is necessary, but not always sufficient, that the pointer + //! be dereferenceable: the memory range of the given size starting at the pointer must all be + //! within the bounds of a single allocated object. Note that in Rust, every (stack-allocated) + //! variable is considered a separate allocated object. + //! ~~Even for operations of size zero, the pointer must not be pointing to deallocated memory, + //! i.e., deallocation makes pointers invalid even for zero-sized operations.~~ + //! ZST access is not OK for any pointer. + //! See: + //! 3. However, casting any non-zero integer literal to a pointer is valid for zero-sized + //! accesses, even if some memory happens to exist at that address and gets deallocated. + //! This corresponds to writing your own allocator: allocating zero-sized objects is not very + //! hard. The canonical way to obtain a pointer that is valid for zero-sized accesses is + //! `NonNull::dangling`. + //! 4. All accesses performed by functions in this module are non-atomic in the sense of atomic + //! operations used to synchronize between threads. + //! This means it is undefined behavior to perform two concurrent accesses to the same location + //! from different threads unless both accesses only read from memory. + //! Notice that this explicitly includes `read_volatile` and `write_volatile`: + //! Volatile accesses cannot be used for inter-thread synchronization. + //! 5. The result of casting a reference to a pointer is valid for as long as the underlying + //! object is live and no reference (just raw pointers) is used to access the same memory. + //! That is, reference and pointer accesses cannot be interleaved. + //! + //! Kani is able to verify #1 and #2 today. + //! + //! For #3, we are overly cautious, and Kani will only consider zero-sized pointer access safe if + //! the address matches `NonNull::<()>::dangling()`. + //! The way Kani tracks provenance is not enough to check if the address was the result of a cast + //! from a non-zero integer literal. + //! kani_core::kani_mem!(std); } mod mem_init { + //! This module provides instrumentation for tracking memory initialization of raw pointers. + //! + //! Currently, memory initialization is tracked on per-byte basis, so each byte of memory pointed to + //! by raw pointers could be either initialized or uninitialized. Padding bytes are always + //! considered uninitialized when read as data bytes. Each type has a type layout to specify which + //! bytes are considered to be data and which -- padding. This is determined at compile time and + //! statically injected into the program (see `Layout`). + //! + //! Compiler automatically inserts calls to `is_xxx_initialized` and `set_xxx_initialized` at + //! appropriate locations to get or set the initialization status of the memory pointed to. + //! + //! Note that for each harness, tracked object and tracked offset are chosen non-deterministically, + //! so calls to `is_xxx_initialized` should be only used in assertion contexts. kani_core::kani_mem_init!(std); } }; diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs index c09d67ca51ff..baf90ed98158 100644 --- a/library/kani_core/src/mem.rs +++ b/library/kani_core/src/mem.rs @@ -1,41 +1,9 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -//! This module contains functions useful for checking unsafe memory access. -//! -//! Given the following validity rules provided in the Rust documentation: -//! (accessed Feb 6th, 2024) -//! -//! 1. A null pointer is never valid, not even for accesses of size zero. -//! 2. For a pointer to be valid, it is necessary, but not always sufficient, that the pointer -//! be dereferenceable: the memory range of the given size starting at the pointer must all be -//! within the bounds of a single allocated object. Note that in Rust, every (stack-allocated) -//! variable is considered a separate allocated object. -//! ~~Even for operations of size zero, the pointer must not be pointing to deallocated memory, -//! i.e., deallocation makes pointers invalid even for zero-sized operations.~~ -//! ZST access is not OK for any pointer. -//! See: -//! 3. However, casting any non-zero integer literal to a pointer is valid for zero-sized -//! accesses, even if some memory happens to exist at that address and gets deallocated. -//! This corresponds to writing your own allocator: allocating zero-sized objects is not very -//! hard. The canonical way to obtain a pointer that is valid for zero-sized accesses is -//! `NonNull::dangling`. -//! 4. All accesses performed by functions in this module are non-atomic in the sense of atomic -//! operations used to synchronize between threads. -//! This means it is undefined behavior to perform two concurrent accesses to the same location -//! from different threads unless both accesses only read from memory. -//! Notice that this explicitly includes `read_volatile` and `write_volatile`: -//! Volatile accesses cannot be used for inter-thread synchronization. -//! 5. The result of casting a reference to a pointer is valid for as long as the underlying -//! object is live and no reference (just raw pointers) is used to access the same memory. -//! That is, reference and pointer accesses cannot be interleaved. -//! -//! Kani is able to verify #1 and #2 today. -//! -//! For #3, we are overly cautious, and Kani will only consider zero-sized pointer access safe if -//! the address matches `NonNull::<()>::dangling()`. -//! The way Kani tracks provenance is not enough to check if the address was the result of a cast -//! from a non-zero integer literal. -//! + +// This module contains functions useful for checking unsafe memory access. +// For full documentation, see the usage of `kani_core::kani_mem!(std);` in library/kani_core/src/lib.rs + // TODO: This module is currently tightly coupled with CBMC's memory model, and it needs some // refactoring to be used with other backends. diff --git a/library/kani_core/src/mem_init.rs b/library/kani_core/src/mem_init.rs index 935f14d71c5d..3fafcb1d8388 100644 --- a/library/kani_core/src/mem_init.rs +++ b/library/kani_core/src/mem_init.rs @@ -1,19 +1,8 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -//! This module provides instrumentation for tracking memory initialization of raw pointers. -//! -//! Currently, memory initialization is tracked on per-byte basis, so each byte of memory pointed to -//! by raw pointers could be either initialized or uninitialized. Padding bytes are always -//! considered uninitialized when read as data bytes. Each type has a type layout to specify which -//! bytes are considered to be data and which -- padding. This is determined at compile time and -//! statically injected into the program (see `Layout`). -//! -//! Compiler automatically inserts calls to `is_xxx_initialized` and `set_xxx_initialized` at -//! appropriate locations to get or set the initialization status of the memory pointed to. -//! -//! Note that for each harness, tracked object and tracked offset are chosen non-deterministically, -//! so calls to `is_xxx_initialized` should be only used in assertion contexts. +// This module provides instrumentation for tracking memory initialization of raw pointers. +// For full documentation, see the usage of `kani_core::kani_mem_init!(std);` in library/kani_core/src/lib.rs // Definitions in this module are not meant to be visible to the end user, only the compiler. #![allow(dead_code)] From 53013f35d8a78db685e2ce6cf95b0146df148ecb Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 29 Jan 2025 00:24:15 -0800 Subject: [PATCH 4/4] Fix missing function declaration issue (#3862) In cases where a function pointer is created, but its value is never used, Kani crashes due to missing function declaration. For now, collect any instance that has its address taken even if its never used. Fixes #3799 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- kani-compiler/src/kani_middle/reachability.rs | 16 +++++++++++ tests/kani/CodegenMisc/missing_mut_fn.rs | 27 +++++++++++++++++++ 2 files changed, 43 insertions(+) create mode 100644 tests/kani/CodegenMisc/missing_mut_fn.rs diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index dea7cca60844..2267af56a684 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -470,6 +470,22 @@ impl MirVisitor for MonoItemsFnCollector<'_, '_> { self.super_terminator(terminator, location); } + + /// Collect any function definition that may occur as a type. + /// + /// The codegen stage will require the definition to be available. + /// This is a conservative approach, since there are cases where the function is never + /// actually used, so we don't need the body. + /// + /// Another alternative would be to lazily declare functions, but it would require a bigger + /// change to codegen. + fn visit_ty(&mut self, ty: &Ty, _: Location) { + if let TyKind::RigidTy(RigidTy::FnDef(def, args)) = ty.kind() { + let instance = Instance::resolve(def, &args).unwrap(); + self.collect_instance(instance, true); + } + self.super_ty(ty); + } } fn extract_unsize_coercion(tcx: TyCtxt, orig_ty: Ty, dst_trait: Ty) -> (Ty, Ty) { diff --git a/tests/kani/CodegenMisc/missing_mut_fn.rs b/tests/kani/CodegenMisc/missing_mut_fn.rs new file mode 100644 index 000000000000..ae7bfe753bf0 --- /dev/null +++ b/tests/kani/CodegenMisc/missing_mut_fn.rs @@ -0,0 +1,27 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Ensure Kani can codegen code with a pointer to a function that is never used +//! See for more details. +fn foo(_func: &mut F) {} +fn foo_dyn(_func: &mut dyn Fn()) {} + +#[kani::proof] +fn check_foo() { + fn f() {} + + foo(&mut f); +} + +#[kani::proof] +fn check_foo_dyn() { + fn f() {} + + foo_dyn(&mut f); +} + +#[kani::proof] +fn check_foo_unused() { + fn f() {} + + let ptr = &mut f; +}