Merge branch 'main' into docs/loop-contracts

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<String>) {
     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<String>) {
         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 { .. }));

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())
         }
     }

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) {

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);
     }
 }
 

kani-compiler/src/session.rs

@@ -57,7 +57,7 @@ static JSON_PANIC_HOOK: LazyLock<Box<dyn Fn(&panic::PanicHookInfo<'_>) + 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,

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]

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:
+            //! <https://doc.rust-lang.org/std/ptr/index.html> (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: <https://github.com/rust-lang/unsafe-code-guidelines/issues/472>
+            //! 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);
         }
     };

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:
-//! <https://doc.rust-lang.org/std/ptr/index.html> (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: <https://github.com/rust-lang/unsafe-code-guidelines/issues/472>
-//! 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.
 

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)]

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"]

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)]
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

tests/expected/function-contract/multiple_replace_fail.expected

@@ -0,0 +1 @@
+warning: Multiple occurrences of `stub_verified(one)`.

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());
+}

tests/expected/function-contract/multiple_replace_pass.expected

@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL

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());
+}