From ac823d33a3540d71ecdb115395013373f8e6e55c Mon Sep 17 00:00:00 2001
From: Qinheping Hu <qinhh@amazon.com>
Date: Thu, 18 Jul 2024 18:37:27 -0500
Subject: [PATCH 01/20] Upgrade toolchain to 2024-07-18 (#3355)

Resolves #3353

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
---
 .../src/codegen_cprover_gotoc/compiler_interface.rs         | 6 ++----
 rust-toolchain.toml                                         | 2 +-
 2 files changed, 3 insertions(+), 5 deletions(-)

diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
index abb69a655472..ff98880ac4d7 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
@@ -24,9 +24,7 @@ use kani_metadata::artifact::convert_type;
 use kani_metadata::UnsupportedFeature;
 use kani_metadata::{ArtifactType, HarnessMetadata, KaniMetadata};
 use kani_metadata::{AssignsContract, CompilerArtifactStub};
-use rustc_codegen_ssa::back::archive::{
-    get_native_object_symbols, ArArchiveBuilder, ArchiveBuilder,
-};
+use rustc_codegen_ssa::back::archive::{ArArchiveBuilder, ArchiveBuilder, DEFAULT_OBJECT_READER};
 use rustc_codegen_ssa::back::metadata::create_wrapper_file;
 use rustc_codegen_ssa::traits::CodegenBackend;
 use rustc_codegen_ssa::{CodegenResults, CrateInfo};
@@ -402,7 +400,7 @@ impl CodegenBackend for GotocCodegenBackend {
             debug!(?crate_type, ?out_path, "link");
             if *crate_type == CrateType::Rlib {
                 // Emit the `rlib` that contains just one file: `<crate>.rmeta`
-                let mut builder = Box::new(ArArchiveBuilder::new(sess, get_native_object_symbols));
+                let mut builder = Box::new(ArArchiveBuilder::new(sess, &DEFAULT_OBJECT_READER));
                 let tmp_dir = TempFileBuilder::new().prefix("kani").tempdir().unwrap();
                 let path = MaybeTempDir::new(tmp_dir, sess.opts.cg.save_temps);
                 let (metadata, _metadata_position) = create_wrapper_file(
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index bd69934d573c..c04db242fd5b 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-07-17"
+channel = "nightly-2024-07-18"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

From 96d1147fc3b59bf71ac6618aca957ac6ba40073a Mon Sep 17 00:00:00 2001
From: Artem Agvanian <nartagva@amazon.com>
Date: Fri, 19 Jul 2024 08:56:01 -0700
Subject: [PATCH 02/20] Support for disabling automatically generated pointer
 checks to avoid reinstrumentation (#3344)

Recently added memory initialization checks (see #3300 for an overview)
code suffers from re-instrumentation due to automatically added pointer
checks to the instrumentation code.

This PR adds an internal `kanitool::disable_checks` attribute to disable
automatically generated CBMC checks inside internal instrumentation.
This, in turn, relies on CBMC pragmas
(https://www.cprover.org/cprover-manual/properties/#usinggotoinstrument).

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
---
 cprover_bindings/src/goto_program/location.rs | 35 +++++++---
 cprover_bindings/src/irep/to_irep.rs          | 46 ++++++++++---
 .../src/codegen_cprover_gotoc/codegen/span.rs | 68 +++++++++++++++++++
 kani-compiler/src/kani_middle/attributes.rs   | 14 +++-
 library/kani/src/mem_init.rs                  | 17 ++++-
 .../alloc-zeroed.rs                           | 22 ++++++
 .../mem-init-reinstrumentation/config.yml     |  4 ++
 .../mem-init-reinstrumentation.expected       |  1 +
 .../mem-init-reinstrumentation.sh             | 20 ++++++
 9 files changed, 204 insertions(+), 23 deletions(-)
 create mode 100644 tests/script-based-pre/mem-init-reinstrumentation/alloc-zeroed.rs
 create mode 100644 tests/script-based-pre/mem-init-reinstrumentation/config.yml
 create mode 100644 tests/script-based-pre/mem-init-reinstrumentation/mem-init-reinstrumentation.expected
 create mode 100755 tests/script-based-pre/mem-init-reinstrumentation/mem-init-reinstrumentation.sh

diff --git a/cprover_bindings/src/goto_program/location.rs b/cprover_bindings/src/goto_program/location.rs
index 4097d075276d..9a2a046f6387 100644
--- a/cprover_bindings/src/goto_program/location.rs
+++ b/cprover_bindings/src/goto_program/location.rs
@@ -19,6 +19,7 @@ pub enum Location {
         start_col: Option<u64>,
         end_line: u64,
         end_col: Option<u64>,
+        pragmas: &'static [&'static str], // CBMC `#pragma check` statements per location.
     },
     /// Location for Statements that use Property Class and Description - Assert, Assume, Cover etc.
     Property {
@@ -28,6 +29,7 @@ pub enum Location {
         col: Option<u64>,
         comment: InternedString,
         property_class: InternedString,
+        pragmas: &'static [&'static str], // CBMC `#pragma check` statements per location.
     },
     /// Covers cases where Location Details are unknown or set as None but Property Class is needed.
     PropertyUnknownLocation { comment: InternedString, property_class: InternedString },
@@ -99,6 +101,7 @@ impl Location {
         start_col: Option<T>,
         end_line: T,
         end_col: Option<T>,
+        pragmas: &'static [&'static str],
     ) -> Location
     where
         T: TryInto<u64>,
@@ -117,6 +120,7 @@ impl Location {
             start_col: start_col_into,
             end_line: end_line_into,
             end_col: end_col_into,
+            pragmas,
         }
     }
 
@@ -128,6 +132,7 @@ impl Location {
         col: Option<T>,
         comment: U,
         property_name: U,
+        pragmas: &'static [&'static str],
     ) -> Location
     where
         T: TryInto<u64>,
@@ -140,7 +145,7 @@ impl Location {
         let function = function.intern();
         let property_class = property_name.into();
         let comment = comment.into();
-        Location::Property { file, function, line, col, comment, property_class }
+        Location::Property { file, function, line, col, comment, property_class, pragmas }
     }
 
     /// Create a Property type Location from an already existing Location type
@@ -157,17 +162,25 @@ impl Location {
                 None,
                 comment.into(),
                 property_name.into(),
+                &[],
+            ),
+            Location::Loc {
+                file,
+                function,
+                start_line,
+                start_col,
+                end_line: _,
+                end_col: _,
+                pragmas,
+            } => Location::property_location(
+                file.into(),
+                function.intern(),
+                start_line,
+                start_col,
+                comment.into(),
+                property_name.into(),
+                pragmas,
             ),
-            Location::Loc { file, function, start_line, start_col, end_line: _, end_col: _ } => {
-                Location::property_location(
-                    file.into(),
-                    function.intern(),
-                    start_line,
-                    start_col,
-                    comment.into(),
-                    property_name.into(),
-                )
-            }
             Location::Property { .. } => location,
             Location::PropertyUnknownLocation { .. } => location,
             // This converts None type Locations to PropertyUnknownLocation type which inserts Property Class and Description
diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs
index 4b5c86350172..d1e84669121d 100644
--- a/cprover_bindings/src/irep/to_irep.rs
+++ b/cprover_bindings/src/irep/to_irep.rs
@@ -389,15 +389,32 @@ impl ToIrep for Location {
                 (IrepId::Function, Irep::just_string_id(function_name.to_string())),
             ])
             .with_named_sub_option(IrepId::Line, line.map(Irep::just_int_id)),
-            Location::Loc { file, function, start_line, start_col, end_line: _, end_col: _ } => {
-                Irep::just_named_sub(linear_map![
-                    (IrepId::File, Irep::just_string_id(file.to_string())),
-                    (IrepId::Line, Irep::just_int_id(*start_line)),
-                ])
-                .with_named_sub_option(IrepId::Column, start_col.map(Irep::just_int_id))
-                .with_named_sub_option(IrepId::Function, function.map(Irep::just_string_id))
-            }
-            Location::Property { file, function, line, col, property_class, comment } => {
+            Location::Loc {
+                file,
+                function,
+                start_line,
+                start_col,
+                end_line: _,
+                end_col: _,
+                pragmas,
+            } => Irep::just_named_sub(linear_map![
+                (IrepId::File, Irep::just_string_id(file.to_string())),
+                (IrepId::Line, Irep::just_int_id(*start_line)),
+            ])
+            .with_named_sub_option(IrepId::Column, start_col.map(Irep::just_int_id))
+            .with_named_sub_option(IrepId::Function, function.map(Irep::just_string_id))
+            .with_named_sub_option(
+                IrepId::Pragma,
+                Some(Irep::just_named_sub(
+                    pragmas
+                        .iter()
+                        .map(|pragma| {
+                            (IrepId::from_string(*pragma), Irep::just_id(IrepId::EmptyString))
+                        })
+                        .collect(),
+                )),
+            ),
+            Location::Property { file, function, line, col, property_class, comment, pragmas } => {
                 Irep::just_named_sub(linear_map![
                     (IrepId::File, Irep::just_string_id(file.to_string())),
                     (IrepId::Line, Irep::just_int_id(*line)),
@@ -409,6 +426,17 @@ impl ToIrep for Location {
                     IrepId::PropertyClass,
                     Irep::just_string_id(property_class.to_string()),
                 )
+                .with_named_sub_option(
+                    IrepId::Pragma,
+                    Some(Irep::just_named_sub(
+                        pragmas
+                            .iter()
+                            .map(|pragma| {
+                                (IrepId::from_string(*pragma), Irep::just_id(IrepId::EmptyString))
+                            })
+                            .collect(),
+                    )),
+                )
             }
             Location::PropertyUnknownLocation { property_class, comment } => {
                 Irep::just_named_sub(linear_map![
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs
index aadb4fbebed9..41a3da11324b 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs
@@ -5,9 +5,31 @@
 
 use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::Location;
+use lazy_static::lazy_static;
+use rustc_ast::Attribute;
 use rustc_smir::rustc_internal;
 use rustc_span::Span;
 use stable_mir::ty::Span as SpanStable;
+use std::collections::HashMap;
+
+lazy_static! {
+    /// Pragmas key-value store to prevent CBMC from generating automatic checks.
+    /// This list is taken from https://github.com/diffblue/cbmc/blob/develop/regression/cbmc/pragma_cprover_enable_all/main.c.
+    static ref PRAGMAS: HashMap<&'static str, &'static str> =
+        [("bounds", "disable:bounds-check"),
+         ("pointer", "disable:pointer-check"),
+         ("div-by-zero", "disable:div-by-zero-check"),
+         ("float-div-by-zero", "disable:float-div-by-zero-check"),
+         ("enum-range", "disable:enum-range-check"),
+         ("signed-overflow", "disable:signed-overflow-check"),
+         ("unsigned-overflow", "disable:unsigned-overflow-check"),
+         ("pointer-overflow", "disable:pointer-overflow-check"),
+         ("float-overflow", "disable:float-overflow-check"),
+         ("conversion", "disable:conversion-check"),
+         ("undefined-shift", "disable:undefined-shift-check"),
+         ("nan", "disable:nan-check"),
+         ("pointer-primitive", "disable:pointer-primitive-check")].iter().copied().collect();
+}
 
 impl<'tcx> GotocCtx<'tcx> {
     pub fn codegen_span(&self, sp: &Span) -> Location {
@@ -15,6 +37,36 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     pub fn codegen_span_stable(&self, sp: SpanStable) -> Location {
+        // Attribute to mark functions as where automatic pointer checks should not be generated.
+        let should_skip_ptr_checks_attr = vec![
+            rustc_span::symbol::Symbol::intern("kanitool"),
+            rustc_span::symbol::Symbol::intern("disable_checks"),
+        ];
+        let pragmas: &'static [&str] = {
+            let disabled_checks: Vec<_> = self
+                .current_fn
+                .as_ref()
+                .map(|current_fn| {
+                    let instance = current_fn.instance();
+                    self.tcx
+                        .get_attrs_by_path(instance.def.def_id(), &should_skip_ptr_checks_attr)
+                        .collect()
+                })
+                .unwrap_or_default();
+            disabled_checks
+                .iter()
+                .map(|attr| {
+                    let arg = parse_word(attr).expect(
+                        "incorrect value passed to `disable_checks`, expected a single identifier",
+                    );
+                    *PRAGMAS.get(arg.as_str()).expect(format!(
+                        "attempting to disable an unexisting check, the possible options are {:?}",
+                        PRAGMAS.keys()
+                    ).as_str())
+                })
+                .collect::<Vec<_>>()
+                .leak() // This is to preserve `Location` being Copy, but could blow up the memory utilization of compiler. 
+        };
         let loc = sp.get_lines();
         Location::new(
             sp.get_filename().to_string(),
@@ -23,6 +75,7 @@ impl<'tcx> GotocCtx<'tcx> {
             Some(loc.start_col),
             loc.end_line,
             Some(loc.end_col),
+            pragmas,
         )
     }
 
@@ -39,3 +92,18 @@ impl<'tcx> GotocCtx<'tcx> {
         self.codegen_span(&topmost)
     }
 }
+
+/// Extracts the single argument from the attribute provided as a string.
+/// For example, `disable_checks(foo)` return `Some("foo")`
+fn parse_word(attr: &Attribute) -> Option<String> {
+    // Vector of meta items , that contain the arguments given the attribute
+    let attr_args = attr.meta_item_list()?;
+    // Only extracts one string ident as a string
+    if attr_args.len() == 1 {
+        attr_args[0].ident().map(|ident| ident.to_string())
+    }
+    // Return none if there are no attributes or if there's too many attributes
+    else {
+        None
+    }
+}
diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs
index 84ec8d627c59..9eb6d3d6ee4e 100644
--- a/kani-compiler/src/kani_middle/attributes.rs
+++ b/kani-compiler/src/kani_middle/attributes.rs
@@ -74,6 +74,9 @@ enum KaniAttributeKind {
     /// We use this attribute to properly instantiate `kani::any_modifies` in
     /// cases when recursion is present given our contracts instrumentation.
     Recursion,
+    /// Used to mark functions where generating automatic pointer checks should be disabled. This is
+    /// used later to automatically attach pragma statements to locations.
+    DisableChecks,
 }
 
 impl KaniAttributeKind {
@@ -93,7 +96,8 @@ impl KaniAttributeKind {
             | KaniAttributeKind::CheckedWith
             | KaniAttributeKind::Modifies
             | KaniAttributeKind::InnerCheck
-            | KaniAttributeKind::IsContractGenerated => false,
+            | KaniAttributeKind::IsContractGenerated
+            | KaniAttributeKind::DisableChecks => false,
         }
     }
 
@@ -382,6 +386,10 @@ impl<'tcx> KaniAttributes<'tcx> {
                 KaniAttributeKind::InnerCheck => {
                     self.inner_check();
                 }
+                KaniAttributeKind::DisableChecks => {
+                    // Ignored here, because it should be an internal attribute. Actual validation
+                    // happens when pragmas are generated.
+                }
             }
         }
     }
@@ -490,6 +498,10 @@ impl<'tcx> KaniAttributes<'tcx> {
                 | KaniAttributeKind::InnerCheck
                 | KaniAttributeKind::ReplacedWith => {
                     self.tcx.dcx().span_err(self.tcx.def_span(self.item), format!("Contracts are not supported on harnesses. (Found the kani-internal contract attribute `{}`)", kind.as_ref()));
+                },
+                KaniAttributeKind::DisableChecks => {
+                    // Internal attribute which shouldn't exist here.
+                    unreachable!()
                 }
             };
             harness
diff --git a/library/kani/src/mem_init.rs b/library/kani/src/mem_init.rs
index a09e515d7e17..88847e9c4f3c 100644
--- a/library/kani/src/mem_init.rs
+++ b/library/kani/src/mem_init.rs
@@ -50,6 +50,7 @@ impl MemoryInitializationState {
     ///
     /// Such definition is necessary since both tracked object and tracked offset are chosen
     /// non-deterministically.
+    #[kanitool::disable_checks(pointer)]
     pub fn get<const LAYOUT_SIZE: usize>(
         &mut self,
         ptr: *const u8,
@@ -61,7 +62,7 @@ impl MemoryInitializationState {
             && self.tracked_offset >= offset
             && self.tracked_offset < offset + LAYOUT_SIZE
         {
-            !layout[(self.tracked_offset - offset) % LAYOUT_SIZE] || self.value
+            !layout[self.tracked_offset - offset] || self.value
         } else {
             true
         }
@@ -73,6 +74,7 @@ impl MemoryInitializationState {
     ///
     /// Such definition is necessary since both tracked object and tracked offset are chosen
     /// non-deterministically.
+    #[kanitool::disable_checks(pointer)]
     pub fn set<const LAYOUT_SIZE: usize>(
         &mut self,
         ptr: *const u8,
@@ -85,7 +87,7 @@ impl MemoryInitializationState {
             && self.tracked_offset >= offset
             && self.tracked_offset < offset + LAYOUT_SIZE
         {
-            self.value = layout[(self.tracked_offset - offset) % LAYOUT_SIZE] && value;
+            self.value = layout[self.tracked_offset - offset] && value;
         }
     }
 
@@ -95,6 +97,7 @@ impl MemoryInitializationState {
     ///
     /// Such definition is necessary since both tracked object and tracked offset are chosen
     /// non-deterministically.
+    #[kanitool::disable_checks(pointer)]
     pub fn get_slice<const LAYOUT_SIZE: usize>(
         &mut self,
         ptr: *const u8,
@@ -119,6 +122,7 @@ impl MemoryInitializationState {
     ///
     /// Such definition is necessary since both tracked object and tracked offset are chosen
     /// non-deterministically.
+    #[kanitool::disable_checks(pointer)]
     pub fn set_slice<const LAYOUT_SIZE: usize>(
         &mut self,
         ptr: *const u8,
@@ -142,6 +146,7 @@ impl MemoryInitializationState {
 static mut MEM_INIT_STATE: MemoryInitializationState = MemoryInitializationState::new();
 
 /// Set tracked object and tracked offset to a non-deterministic value.
+#[kanitool::disable_checks(pointer)]
 #[rustc_diagnostic_item = "KaniInitializeMemoryInitializationState"]
 fn initialize_memory_initialization_state() {
     unsafe {
@@ -152,6 +157,7 @@ fn initialize_memory_initialization_state() {
 }
 
 /// Get initialization state of `num_elts` items laid out according to the `layout` starting at address `ptr`.
+#[kanitool::disable_checks(pointer)]
 #[rustc_diagnostic_item = "KaniIsPtrInitialized"]
 fn is_ptr_initialized<const LAYOUT_SIZE: usize, T>(
     ptr: *const T,
@@ -165,6 +171,7 @@ fn is_ptr_initialized<const LAYOUT_SIZE: usize, T>(
 }
 
 /// Set initialization state to `value` for `num_elts` items laid out according to the `layout` starting at address `ptr`.
+#[kanitool::disable_checks(pointer)]
 #[rustc_diagnostic_item = "KaniSetPtrInitialized"]
 fn set_ptr_initialized<const LAYOUT_SIZE: usize, T>(
     ptr: *const T,
@@ -181,6 +188,7 @@ fn set_ptr_initialized<const LAYOUT_SIZE: usize, T>(
 }
 
 /// Get initialization state of `num_elts` items laid out according to the `layout` starting at address `ptr`.
+#[kanitool::disable_checks(pointer)]
 #[rustc_diagnostic_item = "KaniIsSliceChunkPtrInitialized"]
 fn is_slice_chunk_ptr_initialized<const LAYOUT_SIZE: usize, T>(
     ptr: *const T,
@@ -195,6 +203,7 @@ fn is_slice_chunk_ptr_initialized<const LAYOUT_SIZE: usize, T>(
 }
 
 /// Set initialization state to `value` for `num_elts` items laid out according to the `layout` starting at address `ptr`.
+#[kanitool::disable_checks(pointer)]
 #[rustc_diagnostic_item = "KaniSetSliceChunkPtrInitialized"]
 fn set_slice_chunk_ptr_initialized<const LAYOUT_SIZE: usize, T>(
     ptr: *const T,
@@ -212,6 +221,7 @@ fn set_slice_chunk_ptr_initialized<const LAYOUT_SIZE: usize, T>(
 }
 
 /// Get initialization state of the slice, items of which are laid out according to the `layout` starting at address `ptr`.
+#[kanitool::disable_checks(pointer)]
 #[rustc_diagnostic_item = "KaniIsSlicePtrInitialized"]
 fn is_slice_ptr_initialized<const LAYOUT_SIZE: usize, T>(
     ptr: *const [T],
@@ -225,6 +235,7 @@ fn is_slice_ptr_initialized<const LAYOUT_SIZE: usize, T>(
 }
 
 /// Set initialization state of the slice, items of which are laid out according to the `layout` starting at address `ptr` to `value`.
+#[kanitool::disable_checks(pointer)]
 #[rustc_diagnostic_item = "KaniSetSlicePtrInitialized"]
 fn set_slice_ptr_initialized<const LAYOUT_SIZE: usize, T>(
     ptr: *const [T],
@@ -241,6 +252,7 @@ fn set_slice_ptr_initialized<const LAYOUT_SIZE: usize, T>(
 }
 
 /// Get initialization state of the string slice, items of which are laid out according to the `layout` starting at address `ptr`.
+#[kanitool::disable_checks(pointer)]
 #[rustc_diagnostic_item = "KaniIsStrPtrInitialized"]
 fn is_str_ptr_initialized<const LAYOUT_SIZE: usize>(
     ptr: *const str,
@@ -254,6 +266,7 @@ fn is_str_ptr_initialized<const LAYOUT_SIZE: usize>(
 }
 
 /// Set initialization state of the string slice, items of which are laid out according to the `layout` starting at address `ptr` to `value`.
+#[kanitool::disable_checks(pointer)]
 #[rustc_diagnostic_item = "KaniSetStrPtrInitialized"]
 fn set_str_ptr_initialized<const LAYOUT_SIZE: usize>(
     ptr: *const str,
diff --git a/tests/script-based-pre/mem-init-reinstrumentation/alloc-zeroed.rs b/tests/script-based-pre/mem-init-reinstrumentation/alloc-zeroed.rs
new file mode 100644
index 000000000000..891a97fd8c22
--- /dev/null
+++ b/tests/script-based-pre/mem-init-reinstrumentation/alloc-zeroed.rs
@@ -0,0 +1,22 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z uninit-checks
+
+use std::alloc::{alloc_zeroed, Layout};
+use std::slice::from_raw_parts;
+
+#[kani::proof]
+fn alloc_zeroed_to_slice() {
+    let layout = Layout::from_size_align(32, 8).unwrap();
+    unsafe {
+        // This returns initialized memory, so any further accesses are valid.
+        let ptr = alloc_zeroed(layout);
+        *ptr = 0x41;
+        *ptr.add(1) = 0x42;
+        *ptr.add(2) = 0x43;
+        *ptr.add(3) = 0x44;
+        *ptr.add(16) = 0x00;
+        let _slice1 = from_raw_parts(ptr, 16);
+        let _slice2 = from_raw_parts(ptr.add(16), 16);
+    }
+}
diff --git a/tests/script-based-pre/mem-init-reinstrumentation/config.yml b/tests/script-based-pre/mem-init-reinstrumentation/config.yml
new file mode 100644
index 000000000000..ef61a9171954
--- /dev/null
+++ b/tests/script-based-pre/mem-init-reinstrumentation/config.yml
@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: mem-init-reinstrumentation.sh
+expected: mem-init-reinstrumentation.expected
diff --git a/tests/script-based-pre/mem-init-reinstrumentation/mem-init-reinstrumentation.expected b/tests/script-based-pre/mem-init-reinstrumentation/mem-init-reinstrumentation.expected
new file mode 100644
index 000000000000..59b64322ad50
--- /dev/null
+++ b/tests/script-based-pre/mem-init-reinstrumentation/mem-init-reinstrumentation.expected
@@ -0,0 +1 @@
+success: no pointer checks are detected in initialized memory instrumentaiton
diff --git a/tests/script-based-pre/mem-init-reinstrumentation/mem-init-reinstrumentation.sh b/tests/script-based-pre/mem-init-reinstrumentation/mem-init-reinstrumentation.sh
new file mode 100755
index 000000000000..f859864d1c9a
--- /dev/null
+++ b/tests/script-based-pre/mem-init-reinstrumentation/mem-init-reinstrumentation.sh
@@ -0,0 +1,20 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+set -u
+
+KANI_OUTPUT=`kani -Z uninit-checks alloc-zeroed.rs`
+echo "$KANI_OUTPUT" | egrep -q "kani::mem_init::.*pointer_dereference"
+INSTRUMENTATION_DETECTED=$?
+
+if [[ $INSTRUMENTATION_DETECTED == 0 ]]; then
+    echo "failed: pointer checks are detected in initialized memory instrumentaiton"
+    exit 1
+elif [[ $INSTRUMENTATION_DETECTED == 1 ]]; then
+    echo "success: no pointer checks are detected in initialized memory instrumentaiton"
+    exit 0
+else 
+    echo "failed: error occured when runnning egrep"
+    exit 0
+fi

From 03679923d1f1a862021532a66e1ab43248f36e56 Mon Sep 17 00:00:00 2001
From: Artem Agvanian <nartagva@amazon.com>
Date: Fri, 19 Jul 2024 13:53:08 -0700
Subject: [PATCH 03/20] Add support for global transformations (#3348)

This PR adds basic support for global transformations, which will be
useful to implement full support of #3324

Changes:
- Add edge annotations to the call graph
- Implement global transformation pass infrastructure
- Implement `dump_mir` as a global transformation pass

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: Celina G. Val <celinval@amazon.com>
---
 .../compiler_interface.rs                     |  30 +-
 kani-compiler/src/kani_middle/mod.rs          |  43 +--
 kani-compiler/src/kani_middle/reachability.rs | 304 +++++++++++-------
 .../kani_middle/transform/dump_mir_pass.rs    |  69 ++++
 .../src/kani_middle/transform/mod.rs          |  59 +++-
 5 files changed, 336 insertions(+), 169 deletions(-)
 create mode 100644 kani-compiler/src/kani_middle/transform/dump_mir_pass.rs

diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
index ff98880ac4d7..986cd00e32a5 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
@@ -7,14 +7,14 @@ use crate::args::ReachabilityType;
 use crate::codegen_cprover_gotoc::GotocCtx;
 use crate::kani_middle::analysis;
 use crate::kani_middle::attributes::{is_test_harness_description, KaniAttributes};
+use crate::kani_middle::check_reachable_items;
 use crate::kani_middle::codegen_units::{CodegenUnit, CodegenUnits};
 use crate::kani_middle::metadata::gen_test_metadata;
 use crate::kani_middle::provide;
 use crate::kani_middle::reachability::{
     collect_reachable_items, filter_const_crate_items, filter_crate_items,
 };
-use crate::kani_middle::transform::BodyTransformation;
-use crate::kani_middle::{check_reachable_items, dump_mir_items};
+use crate::kani_middle::transform::{BodyTransformation, GlobalPasses};
 use crate::kani_queries::QueryDb;
 use cbmc::goto_program::Location;
 use cbmc::irep::goto_binary_serde::write_goto_binary_file;
@@ -87,11 +87,33 @@ impl GotocCodegenBackend {
         check_contract: Option<InternalDefId>,
         mut transformer: BodyTransformation,
     ) -> (GotocCtx<'tcx>, Vec<MonoItem>, Option<AssignsContract>) {
-        let items = with_timer(
+        let (items, call_graph) = with_timer(
             || collect_reachable_items(tcx, &mut transformer, starting_items),
             "codegen reachability analysis",
         );
-        dump_mir_items(tcx, &mut transformer, &items, &symtab_goto.with_extension("kani.mir"));
+
+        // Retrieve all instances from the currently codegened items.
+        let instances = items
+            .iter()
+            .filter_map(|item| match item {
+                MonoItem::Fn(instance) => Some(*instance),
+                MonoItem::Static(static_def) => {
+                    let instance: Instance = (*static_def).into();
+                    instance.has_body().then_some(instance)
+                }
+                MonoItem::GlobalAsm(_) => None,
+            })
+            .collect();
+
+        // Apply all transformation passes, including global passes.
+        let mut global_passes = GlobalPasses::new(&self.queries.lock().unwrap(), tcx);
+        global_passes.run_global_passes(
+            &mut transformer,
+            tcx,
+            starting_items,
+            instances,
+            call_graph,
+        );
 
         // Follow rustc naming convention (cx is abbrev for context).
         // https://rustc-dev-guide.rust-lang.org/conventions.html#naming-conventions
diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs
index 17b08b687e30..3c300e9da52c 100644
--- a/kani-compiler/src/kani_middle/mod.rs
+++ b/kani-compiler/src/kani_middle/mod.rs
@@ -4,9 +4,7 @@
 //! and transformations.
 
 use std::collections::HashSet;
-use std::path::Path;
 
-use crate::kani_middle::transform::BodyTransformation;
 use crate::kani_queries::QueryDb;
 use rustc_hir::{def::DefKind, def_id::LOCAL_CRATE};
 use rustc_middle::span_bug;
@@ -15,18 +13,14 @@ use rustc_middle::ty::layout::{
     LayoutOfHelpers, TyAndLayout,
 };
 use rustc_middle::ty::{self, Instance as InstanceInternal, Ty as TyInternal, TyCtxt};
-use rustc_session::config::OutputType;
 use rustc_smir::rustc_internal;
 use rustc_span::source_map::respan;
 use rustc_span::Span;
 use rustc_target::abi::call::FnAbi;
 use rustc_target::abi::{HasDataLayout, TargetDataLayout};
-use stable_mir::mir::mono::{Instance, MonoItem};
+use stable_mir::mir::mono::MonoItem;
 use stable_mir::ty::{FnDef, RigidTy, Span as SpanStable, TyKind};
 use stable_mir::CrateDef;
-use std::fs::File;
-use std::io::BufWriter;
-use std::io::Write;
 
 use self::attributes::KaniAttributes;
 
@@ -92,41 +86,6 @@ pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem])
     tcx.dcx().abort_if_errors();
 }
 
-/// Print MIR for the reachable items if the `--emit mir` option was provided to rustc.
-pub fn dump_mir_items(
-    tcx: TyCtxt,
-    transformer: &mut BodyTransformation,
-    items: &[MonoItem],
-    output: &Path,
-) {
-    /// Convert MonoItem into a DefId.
-    /// Skip stuff that we cannot generate the MIR items.
-    fn get_instance(item: &MonoItem) -> Option<Instance> {
-        match item {
-            // Exclude FnShims and others that cannot be dumped.
-            MonoItem::Fn(instance) => Some(*instance),
-            MonoItem::Static(def) => {
-                let instance: Instance = (*def).into();
-                instance.has_body().then_some(instance)
-            }
-            MonoItem::GlobalAsm(_) => None,
-        }
-    }
-
-    if tcx.sess.opts.output_types.contains_key(&OutputType::Mir) {
-        // Create output buffer.
-        let out_file = File::create(output).unwrap();
-        let mut writer = BufWriter::new(out_file);
-
-        // For each def_id, dump their MIR
-        for instance in items.iter().filter_map(get_instance) {
-            writeln!(writer, "// Item: {} ({})", instance.name(), instance.mangled_name()).unwrap();
-            let body = transformer.body(tcx, instance);
-            let _ = body.dump(&mut writer, &instance.name());
-        }
-    }
-}
-
 /// Structure that represents the source location of a definition.
 /// TODO: Use `InternedString` once we move it out of the cprover_bindings.
 /// <https://github.com/model-checking/kani/issues/2435>
diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs
index 279dcf8cc107..d2c9d50515c4 100644
--- a/kani-compiler/src/kani_middle/reachability.rs
+++ b/kani-compiler/src/kani_middle/reachability.rs
@@ -22,6 +22,7 @@ use rustc_data_structures::fingerprint::Fingerprint;
 use rustc_data_structures::fx::FxHashSet;
 use rustc_data_structures::stable_hasher::{HashStable, StableHasher};
 use rustc_middle::ty::{TyCtxt, VtblEntry};
+use rustc_session::config::OutputType;
 use rustc_smir::rustc_internal;
 use stable_mir::mir::alloc::{AllocId, GlobalAlloc};
 use stable_mir::mir::mono::{Instance, InstanceKind, MonoItem, StaticDef};
@@ -32,6 +33,12 @@ use stable_mir::mir::{
 use stable_mir::ty::{Allocation, ClosureKind, ConstantKind, RigidTy, Ty, TyKind};
 use stable_mir::CrateItem;
 use stable_mir::{CrateDef, ItemKind};
+use std::fmt::{Display, Formatter};
+use std::{
+    collections::{HashMap, HashSet},
+    fs::File,
+    io::{BufWriter, Write},
+};
 
 use crate::kani_middle::coercion;
 use crate::kani_middle::coercion::CoercionBase;
@@ -42,7 +49,7 @@ pub fn collect_reachable_items(
     tcx: TyCtxt,
     transformer: &mut BodyTransformation,
     starting_points: &[MonoItem],
-) -> Vec<MonoItem> {
+) -> (Vec<MonoItem>, CallGraph) {
     // For each harness, collect items using the same collector.
     // I.e.: This will return any item that is reachable from one or more of the starting points.
     let mut collector = MonoItemsCollector::new(tcx, transformer);
@@ -62,7 +69,7 @@ pub fn collect_reachable_items(
     // order of the errors and warnings is stable.
     let mut sorted_items: Vec<_> = collector.collected.into_iter().collect();
     sorted_items.sort_by_cached_key(|item| to_fingerprint(tcx, item));
-    sorted_items
+    (sorted_items, collector.call_graph)
 }
 
 /// Collect all (top-level) items in the crate that matches the given predicate.
@@ -118,7 +125,24 @@ where
             }
         }
     }
-    roots
+    roots.into_iter().map(|root| root.item).collect()
+}
+
+/// Reason for introducing an edge in the call graph.
+#[derive(Clone, Copy, Debug, Eq, PartialEq, Hash)]
+enum CollectionReason {
+    DirectCall,
+    IndirectCall,
+    VTableMethod,
+    Static,
+    StaticDrop,
+}
+
+/// A destination of the edge in the call graph.
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
+struct CollectedItem {
+    item: MonoItem,
+    reason: CollectionReason,
 }
 
 struct MonoItemsCollector<'tcx, 'a> {
@@ -130,8 +154,8 @@ struct MonoItemsCollector<'tcx, 'a> {
     collected: FxHashSet<MonoItem>,
     /// Items enqueued for visiting.
     queue: Vec<MonoItem>,
-    #[cfg(debug_assertions)]
-    call_graph: debug::CallGraph,
+    /// Call graph used for dataflow analysis.
+    call_graph: CallGraph,
 }
 
 impl<'tcx, 'a> MonoItemsCollector<'tcx, 'a> {
@@ -140,8 +164,7 @@ impl<'tcx, 'a> MonoItemsCollector<'tcx, 'a> {
             tcx,
             collected: FxHashSet::default(),
             queue: vec![],
-            #[cfg(debug_assertions)]
-            call_graph: debug::CallGraph::default(),
+            call_graph: CallGraph::default(),
             transformer,
         }
     }
@@ -167,17 +190,17 @@ impl<'tcx, 'a> MonoItemsCollector<'tcx, 'a> {
                         vec![]
                     }
                 };
-                #[cfg(debug_assertions)]
                 self.call_graph.add_edges(to_visit, &next_items);
 
-                self.queue
-                    .extend(next_items.into_iter().filter(|item| !self.collected.contains(item)));
+                self.queue.extend(next_items.into_iter().filter_map(
+                    |CollectedItem { item, .. }| (!self.collected.contains(&item)).then_some(item),
+                ));
             }
         }
     }
 
     /// Visit a function and collect all mono-items reachable from its instructions.
-    fn visit_fn(&mut self, instance: Instance) -> Vec<MonoItem> {
+    fn visit_fn(&mut self, instance: Instance) -> Vec<CollectedItem> {
         let _guard = debug_span!("visit_fn", function=?instance).entered();
         let body = self.transformer.body(self.tcx, instance);
         let mut collector =
@@ -187,19 +210,24 @@ impl<'tcx, 'a> MonoItemsCollector<'tcx, 'a> {
     }
 
     /// Visit a static object and collect drop / initialization functions.
-    fn visit_static(&mut self, def: StaticDef) -> Vec<MonoItem> {
+    fn visit_static(&mut self, def: StaticDef) -> Vec<CollectedItem> {
         let _guard = debug_span!("visit_static", ?def).entered();
         let mut next_items = vec![];
 
         // Collect drop function.
         let static_ty = def.ty();
         let instance = Instance::resolve_drop_in_place(static_ty);
-        next_items.push(instance.into());
+        next_items
+            .push(CollectedItem { item: instance.into(), reason: CollectionReason::StaticDrop });
 
         // Collect initialization.
         let alloc = def.eval_initializer().unwrap();
         for (_, prov) in alloc.provenance.ptrs {
-            next_items.extend(collect_alloc_items(prov.0).into_iter());
+            next_items.extend(
+                collect_alloc_items(prov.0)
+                    .into_iter()
+                    .map(|item| CollectedItem { item, reason: CollectionReason::Static }),
+            );
         }
 
         next_items
@@ -213,7 +241,7 @@ impl<'tcx, 'a> MonoItemsCollector<'tcx, 'a> {
 
 struct MonoItemsFnCollector<'a, 'tcx> {
     tcx: TyCtxt<'tcx>,
-    collected: FxHashSet<MonoItem>,
+    collected: FxHashSet<CollectedItem>,
     body: &'a Body,
 }
 
@@ -251,7 +279,9 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> {
                 }
             });
             trace!(methods=?methods.clone().collect::<Vec<_>>(), "collect_vtable_methods");
-            self.collected.extend(methods);
+            self.collected.extend(
+                methods.map(|item| CollectedItem { item, reason: CollectionReason::VTableMethod }),
+            );
         }
 
         // Add the destructor for the concrete type.
@@ -282,7 +312,12 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> {
         };
         if should_collect && should_codegen_locally(&instance) {
             trace!(?instance, "collect_instance");
-            self.collected.insert(instance.into());
+            let reason = if is_direct_call {
+                CollectionReason::DirectCall
+            } else {
+                CollectionReason::IndirectCall
+            };
+            self.collected.insert(CollectedItem { item: instance.into(), reason });
         }
     }
 
@@ -290,7 +325,11 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> {
     fn collect_allocation(&mut self, alloc: &Allocation) {
         debug!(?alloc, "collect_allocation");
         for (_, id) in &alloc.provenance.ptrs {
-            self.collected.extend(collect_alloc_items(id.0).into_iter())
+            self.collected.extend(
+                collect_alloc_items(id.0)
+                    .into_iter()
+                    .map(|item| CollectedItem { item, reason: CollectionReason::Static }),
+            )
         }
     }
 }
@@ -366,7 +405,8 @@ impl<'a, 'tcx> MirVisitor for MonoItemsFnCollector<'a, 'tcx> {
             }
             Rvalue::ThreadLocalRef(item) => {
                 trace!(?item, "visit_rvalue thread_local");
-                self.collected.insert(MonoItem::Static(StaticDef::try_from(item).unwrap()));
+                let item = MonoItem::Static(StaticDef::try_from(item).unwrap());
+                self.collected.insert(CollectedItem { item, reason: CollectionReason::Static });
             }
             _ => { /* not interesting */ }
         }
@@ -485,128 +525,150 @@ fn collect_alloc_items(alloc_id: AllocId) -> Vec<MonoItem> {
     items
 }
 
-#[cfg(debug_assertions)]
-#[allow(dead_code)]
-mod debug {
-
-    use std::fmt::{Display, Formatter};
-    use std::{
-        collections::{HashMap, HashSet},
-        fs::File,
-        io::{BufWriter, Write},
-    };
-
-    use rustc_session::config::OutputType;
-
-    use super::*;
+/// Call graph with edges annotated with the reason why they were added to the graph.
+#[derive(Debug, Default)]
+pub struct CallGraph {
+    /// Nodes of the graph.
+    nodes: HashSet<Node>,
+    /// Edges of the graph.
+    edges: HashMap<Node, Vec<CollectedNode>>,
+    /// Since the graph is directed, we also store back edges.
+    back_edges: HashMap<Node, Vec<CollectedNode>>,
+}
 
-    #[derive(Debug, Default)]
-    pub struct CallGraph {
-        // Nodes of the graph.
-        nodes: HashSet<Node>,
-        edges: HashMap<Node, Vec<Node>>,
-        back_edges: HashMap<Node, Vec<Node>>,
+/// Newtype around MonoItem.
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
+struct Node(pub MonoItem);
+
+/// Newtype around CollectedItem.
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
+struct CollectedNode(pub CollectedItem);
+
+impl CallGraph {
+    /// Add a new node into a graph.
+    fn add_node(&mut self, item: MonoItem) {
+        let node = Node(item);
+        self.nodes.insert(node.clone());
+        self.edges.entry(node.clone()).or_default();
+        self.back_edges.entry(node).or_default();
     }
 
-    #[derive(Clone, Debug, Eq, PartialEq, Hash)]
-    struct Node(pub MonoItem);
-
-    impl CallGraph {
-        pub fn add_node(&mut self, item: MonoItem) {
-            let node = Node(item);
-            self.nodes.insert(node.clone());
-            self.edges.entry(node.clone()).or_default();
-            self.back_edges.entry(node).or_default();
-        }
+    /// Add a new edge "from" -> "to".
+    fn add_edge(&mut self, from: MonoItem, to: MonoItem, collection_reason: CollectionReason) {
+        let from_node = Node(from.clone());
+        let to_node = Node(to.clone());
+        self.add_node(from.clone());
+        self.add_node(to.clone());
+        self.edges
+            .get_mut(&from_node)
+            .unwrap()
+            .push(CollectedNode(CollectedItem { item: to, reason: collection_reason }));
+        self.back_edges
+            .get_mut(&to_node)
+            .unwrap()
+            .push(CollectedNode(CollectedItem { item: from, reason: collection_reason }));
+    }
 
-        /// Add a new edge "from" -> "to".
-        pub fn add_edge(&mut self, from: MonoItem, to: MonoItem) {
-            let from_node = Node(from.clone());
-            let to_node = Node(to.clone());
-            self.add_node(from);
-            self.add_node(to);
-            self.edges.get_mut(&from_node).unwrap().push(to_node.clone());
-            self.back_edges.get_mut(&to_node).unwrap().push(from_node);
+    /// Add multiple new edges for the "from" node.
+    fn add_edges(&mut self, from: MonoItem, to: &[CollectedItem]) {
+        self.add_node(from.clone());
+        for CollectedItem { item, reason } in to {
+            self.add_edge(from.clone(), item.clone(), *reason);
         }
+    }
 
-        /// Add multiple new edges for the "from" node.
-        pub fn add_edges(&mut self, from: MonoItem, to: &[MonoItem]) {
-            self.add_node(from.clone());
-            for item in to {
-                self.add_edge(from.clone(), item.clone());
+    /// Print the graph in DOT format to a file.
+    /// See <https://graphviz.org/doc/info/lang.html> for more information.
+    fn dump_dot(&self, tcx: TyCtxt) -> std::io::Result<()> {
+        if let Ok(target) = std::env::var("KANI_REACH_DEBUG") {
+            debug!(?target, "dump_dot");
+            let outputs = tcx.output_filenames(());
+            let base_path = outputs.path(OutputType::Metadata);
+            let path = base_path.as_path().with_extension("dot");
+            let out_file = File::create(path)?;
+            let mut writer = BufWriter::new(out_file);
+            writeln!(writer, "digraph ReachabilityGraph {{")?;
+            if target.is_empty() {
+                self.dump_all(&mut writer)?;
+            } else {
+                // Only dump nodes that led the reachability analysis to the target node.
+                self.dump_reason(&mut writer, &target)?;
             }
+            writeln!(writer, "}}")?;
         }
 
-        /// Print the graph in DOT format to a file.
-        /// See <https://graphviz.org/doc/info/lang.html> for more information.
-        pub fn dump_dot(&self, tcx: TyCtxt) -> std::io::Result<()> {
-            if let Ok(target) = std::env::var("KANI_REACH_DEBUG") {
-                debug!(?target, "dump_dot");
-                let outputs = tcx.output_filenames(());
-                let base_path = outputs.path(OutputType::Metadata);
-                let path = base_path.as_path().with_extension("dot");
-                let out_file = File::create(path)?;
-                let mut writer = BufWriter::new(out_file);
-                writeln!(writer, "digraph ReachabilityGraph {{")?;
-                if target.is_empty() {
-                    self.dump_all(&mut writer)?;
-                } else {
-                    // Only dump nodes that led the reachability analysis to the target node.
-                    self.dump_reason(&mut writer, &target)?;
-                }
-                writeln!(writer, "}}")?;
-            }
+        Ok(())
+    }
 
-            Ok(())
+    /// Write all notes to the given writer.
+    fn dump_all<W: Write>(&self, writer: &mut W) -> std::io::Result<()> {
+        tracing::info!(nodes=?self.nodes.len(), edges=?self.edges.len(), "dump_all");
+        for node in &self.nodes {
+            writeln!(writer, r#""{node}""#)?;
+            for succ in self.edges.get(node).unwrap() {
+                let reason = succ.0.reason;
+                writeln!(writer, r#""{node}" -> "{succ}" [label={reason:?}] "#)?;
+            }
         }
+        Ok(())
+    }
 
-        /// Write all notes to the given writer.
-        fn dump_all<W: Write>(&self, writer: &mut W) -> std::io::Result<()> {
-            tracing::info!(nodes=?self.nodes.len(), edges=?self.edges.len(), "dump_all");
-            for node in &self.nodes {
-                writeln!(writer, r#""{node}""#)?;
-                for succ in self.edges.get(node).unwrap() {
-                    writeln!(writer, r#""{node}" -> "{succ}" "#)?;
-                }
+    /// Write all notes that may have led to the discovery of the given target.
+    fn dump_reason<W: Write>(&self, writer: &mut W, target: &str) -> std::io::Result<()> {
+        let mut queue: Vec<Node> =
+            self.nodes.iter().filter(|item| item.to_string().contains(target)).cloned().collect();
+        let mut visited: HashSet<Node> = HashSet::default();
+        tracing::info!(target=?queue, nodes=?self.nodes.len(), edges=?self.edges.len(), "dump_reason");
+        while let Some(to_visit) = queue.pop() {
+            if !visited.contains(&to_visit) {
+                visited.insert(to_visit.clone());
+                queue.extend(
+                    self.back_edges
+                        .get(&to_visit)
+                        .unwrap()
+                        .iter()
+                        .map(|item| Node::from(item.clone())),
+                );
             }
-            Ok(())
         }
 
-        /// Write all notes that may have led to the discovery of the given target.
-        fn dump_reason<W: Write>(&self, writer: &mut W, target: &str) -> std::io::Result<()> {
-            let mut queue = self
-                .nodes
-                .iter()
-                .filter(|item| item.to_string().contains(target))
-                .collect::<Vec<_>>();
-            let mut visited: HashSet<&Node> = HashSet::default();
-            tracing::info!(target=?queue, nodes=?self.nodes.len(), edges=?self.edges.len(), "dump_reason");
-            while let Some(to_visit) = queue.pop() {
-                if !visited.contains(to_visit) {
-                    visited.insert(to_visit);
-                    queue.extend(self.back_edges.get(to_visit).unwrap());
-                }
+        for node in &visited {
+            writeln!(writer, r#""{node}""#)?;
+            let edges = self.edges.get(node).unwrap();
+            for succ in edges.iter().filter(|item| {
+                let node = Node::from((*item).clone());
+                visited.contains(&node)
+            }) {
+                let reason = succ.0.reason;
+                writeln!(writer, r#""{node}" -> "{succ}" [label={reason:?}] "#)?;
             }
+        }
+        Ok(())
+    }
+}
 
-            for node in &visited {
-                writeln!(writer, r#""{node}""#)?;
-                for succ in
-                    self.edges.get(node).unwrap().iter().filter(|item| visited.contains(item))
-                {
-                    writeln!(writer, r#""{node}" -> "{succ}" "#)?;
-                }
-            }
-            Ok(())
+impl Display for Node {
+    fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
+        match &self.0 {
+            MonoItem::Fn(instance) => write!(f, "{}", instance.name()),
+            MonoItem::Static(def) => write!(f, "{}", def.name()),
+            MonoItem::GlobalAsm(asm) => write!(f, "{asm:?}"),
         }
     }
+}
 
-    impl Display for Node {
-        fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
-            match &self.0 {
-                MonoItem::Fn(instance) => write!(f, "{}", instance.name()),
-                MonoItem::Static(def) => write!(f, "{}", def.name()),
-                MonoItem::GlobalAsm(asm) => write!(f, "{asm:?}"),
-            }
+impl Display for CollectedNode {
+    fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
+        match &self.0.item {
+            MonoItem::Fn(instance) => write!(f, "{}", instance.name()),
+            MonoItem::Static(def) => write!(f, "{}", def.name()),
+            MonoItem::GlobalAsm(asm) => write!(f, "{asm:?}"),
         }
     }
 }
+
+impl From<CollectedNode> for Node {
+    fn from(value: CollectedNode) -> Self {
+        Node(value.0.item)
+    }
+}
diff --git a/kani-compiler/src/kani_middle/transform/dump_mir_pass.rs b/kani-compiler/src/kani_middle/transform/dump_mir_pass.rs
new file mode 100644
index 000000000000..9393ec0d88c9
--- /dev/null
+++ b/kani-compiler/src/kani_middle/transform/dump_mir_pass.rs
@@ -0,0 +1,69 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Global transformation pass, which does not modify bodies but dumps MIR whenever the appropriate debug flag is passed.
+
+use crate::kani_middle::reachability::CallGraph;
+use crate::kani_middle::transform::GlobalPass;
+use crate::kani_queries::QueryDb;
+use kani_metadata::ArtifactType;
+use rustc_middle::ty::TyCtxt;
+use rustc_session::config::OutputType;
+use stable_mir::mir::mono::{Instance, MonoItem};
+use std::fs::File;
+use std::io::BufWriter;
+use std::io::Write;
+
+use super::BodyTransformation;
+
+/// Dump all MIR bodies.
+#[derive(Debug)]
+pub struct DumpMirPass {
+    enabled: bool,
+}
+
+impl DumpMirPass {
+    pub fn new(tcx: TyCtxt) -> Self {
+        Self { enabled: tcx.sess.opts.output_types.contains_key(&OutputType::Mir) }
+    }
+}
+
+impl GlobalPass for DumpMirPass {
+    fn is_enabled(&self, _query_db: &QueryDb) -> bool {
+        self.enabled
+    }
+
+    fn transform(
+        &mut self,
+        tcx: TyCtxt,
+        _call_graph: &CallGraph,
+        starting_items: &[MonoItem],
+        instances: Vec<Instance>,
+        transformer: &mut BodyTransformation,
+    ) {
+        // Create output buffer.
+        let file_path = {
+            let base_path = tcx.output_filenames(()).path(OutputType::Object);
+            let base_name = base_path.as_path();
+            let entry_point = (starting_items.len() == 1).then_some(starting_items[0].clone());
+            // If there is a single entry point, use it as a file name.
+            if let Some(MonoItem::Fn(starting_instance)) = entry_point {
+                let mangled_name = starting_instance.mangled_name();
+                let file_stem =
+                    format!("{}_{mangled_name}", base_name.file_stem().unwrap().to_str().unwrap());
+                base_name.with_file_name(file_stem).with_extension(ArtifactType::SymTabGoto)
+            } else {
+                // Otherwise, use the object output path from the compiler.
+                base_name.with_extension(ArtifactType::SymTabGoto)
+            }
+        };
+        let out_file = File::create(file_path.with_extension("kani.mir")).unwrap();
+        let mut writer = BufWriter::new(out_file);
+
+        // For each def_id, dump their MIR.
+        for instance in instances.iter() {
+            writeln!(writer, "// Item: {} ({})", instance.name(), instance.mangled_name()).unwrap();
+            let _ = transformer.body(tcx, *instance).dump(&mut writer, &instance.name());
+        }
+    }
+}
diff --git a/kani-compiler/src/kani_middle/transform/mod.rs b/kani-compiler/src/kani_middle/transform/mod.rs
index 26a95978fcaf..5b497b09619d 100644
--- a/kani-compiler/src/kani_middle/transform/mod.rs
+++ b/kani-compiler/src/kani_middle/transform/mod.rs
@@ -17,6 +17,7 @@
 //! For all instrumentation passes, always use exhaustive matches to ensure soundness in case a new
 //! case is added.
 use crate::kani_middle::codegen_units::CodegenUnit;
+use crate::kani_middle::reachability::CallGraph;
 use crate::kani_middle::transform::body::CheckType;
 use crate::kani_middle::transform::check_uninit::UninitPass;
 use crate::kani_middle::transform::check_values::ValidValuePass;
@@ -24,8 +25,9 @@ use crate::kani_middle::transform::contracts::AnyModifiesPass;
 use crate::kani_middle::transform::kani_intrinsics::IntrinsicGeneratorPass;
 use crate::kani_middle::transform::stubs::{ExternFnStubPass, FnStubPass};
 use crate::kani_queries::QueryDb;
+use dump_mir_pass::DumpMirPass;
 use rustc_middle::ty::TyCtxt;
-use stable_mir::mir::mono::Instance;
+use stable_mir::mir::mono::{Instance, MonoItem};
 use stable_mir::mir::Body;
 use std::collections::HashMap;
 use std::fmt::Debug;
@@ -34,6 +36,7 @@ pub(crate) mod body;
 mod check_uninit;
 mod check_values;
 mod contracts;
+mod dump_mir_pass;
 mod kani_intrinsics;
 mod stubs;
 
@@ -90,7 +93,8 @@ impl BodyTransformation {
         transformer
     }
 
-    /// Retrieve the body of an instance.
+    /// Retrieve the body of an instance. This does not apply global passes, but will retrieve the
+    /// body after global passes running if they were previously applied.
     ///
     /// Note that this assumes that the instance does have a body since existing consumers already
     /// assume that. Use `instance.has_body()` to check if an instance has a body.
@@ -152,6 +156,23 @@ pub(crate) trait TransformPass: Debug {
     fn transform(&mut self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body);
 }
 
+/// A trait to represent transformation passes that operate on the whole codegen unit.
+pub(crate) trait GlobalPass: Debug {
+    fn is_enabled(&self, query_db: &QueryDb) -> bool
+    where
+        Self: Sized;
+
+    /// Run a transformation pass on the whole codegen unit.
+    fn transform(
+        &mut self,
+        tcx: TyCtxt,
+        call_graph: &CallGraph,
+        starting_items: &[MonoItem],
+        instances: Vec<Instance>,
+        transformer: &mut BodyTransformation,
+    );
+}
+
 /// The transformation result.
 /// We currently only cache the body of functions that were instrumented.
 #[derive(Clone, Debug)]
@@ -159,3 +180,37 @@ enum TransformationResult {
     Modified(Body),
     NotModified,
 }
+
+pub struct GlobalPasses {
+    /// The passes that operate on the whole codegen unit, they run after all previous passes are
+    /// done.
+    global_passes: Vec<Box<dyn GlobalPass>>,
+}
+
+impl GlobalPasses {
+    pub fn new(queries: &QueryDb, tcx: TyCtxt) -> Self {
+        let mut global_passes = GlobalPasses { global_passes: vec![] };
+        global_passes.add_global_pass(queries, DumpMirPass::new(tcx));
+        global_passes
+    }
+
+    fn add_global_pass<P: GlobalPass + 'static>(&mut self, query_db: &QueryDb, pass: P) {
+        if pass.is_enabled(&query_db) {
+            self.global_passes.push(Box::new(pass))
+        }
+    }
+
+    /// Run all global passes and store the results in a cache that can later be queried by `body`.
+    pub fn run_global_passes(
+        &mut self,
+        transformer: &mut BodyTransformation,
+        tcx: TyCtxt,
+        starting_items: &[MonoItem],
+        instances: Vec<Instance>,
+        call_graph: CallGraph,
+    ) {
+        for global_pass in self.global_passes.iter_mut() {
+            global_pass.transform(tcx, &call_graph, starting_items, instances.clone(), transformer);
+        }
+    }
+}

From 9f230baeeaf59ffdf44cdf73d627e9f67d4606e1 Mon Sep 17 00:00:00 2001
From: Qinheping Hu <qinhh@amazon.com>
Date: Mon, 22 Jul 2024 03:14:49 -0500
Subject: [PATCH 04/20] Upgrade toolchain to 2024-07-19 (#3364)

Resolves #3358

Related upstream commits:
- https://github.com/rust-lang/rust/commit/21dc49c587 ptr::metadata:
avoid references to extern types
---
 .../codegen_cprover_gotoc/codegen/rvalue.rs   | 28 +++++++++++++++----
 rust-toolchain.toml                           |  2 +-
 2 files changed, 24 insertions(+), 6 deletions(-)

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index e01ffbe462ba..f84708b9bdd5 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -703,8 +703,10 @@ impl<'tcx> GotocCtx<'tcx> {
                         if meta.typ().sizeof(&self.symbol_table) == 0 {
                             data_cast
                         } else {
-                            let vtable_expr =
-                                meta.member("_vtable_ptr", &self.symbol_table).cast_to(
+                            let vtable_expr = meta
+                                .member("_vtable_ptr", &self.symbol_table)
+                                .member("pointer", &self.symbol_table)
+                                .cast_to(
                                     typ.lookup_field_type("vtable", &self.symbol_table).unwrap(),
                                 );
                             dynamic_fat_ptr(typ, data_cast, vtable_expr, &self.symbol_table)
@@ -835,13 +837,29 @@ impl<'tcx> GotocCtx<'tcx> {
                             dst_goto_typ.lookup_components(&self.symbol_table).unwrap();
                         assert_eq!(dst_components.len(), 2);
                         assert_eq!(dst_components[0].name(), "_vtable_ptr");
-                        assert!(dst_components[0].typ().is_pointer());
+                        assert!(dst_components[0].typ().is_struct_like());
                         assert_eq!(dst_components[1].name(), "_phantom");
                         self.assert_is_rust_phantom_data_like(&dst_components[1].typ());
+                        // accessing pointer type of _vtable_ptr, which is wrapped in NonNull
+                        let vtable_ptr_typ = dst_goto_typ
+                            .lookup_field_type("_vtable_ptr", &self.symbol_table)
+                            .unwrap()
+                            .lookup_components(&self.symbol_table)
+                            .unwrap()[0]
+                            .typ();
                         Expr::struct_expr(
-                            dst_goto_typ,
+                            dst_goto_typ.clone(),
                             btree_string_map![
-                                ("_vtable_ptr", vtable_expr.cast_to(dst_components[0].typ())),
+                                (
+                                    "_vtable_ptr",
+                                    Expr::struct_expr_from_values(
+                                        dst_goto_typ
+                                            .lookup_field_type("_vtable_ptr", &self.symbol_table)
+                                            .unwrap(),
+                                        vec![vtable_expr.clone().cast_to(vtable_ptr_typ)],
+                                        &self.symbol_table
+                                    )
+                                ),
                                 (
                                     "_phantom",
                                     Expr::struct_expr(
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index c04db242fd5b..adc62ae8e8db 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-07-18"
+channel = "nightly-2024-07-19"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

From bf1126a7b2db230fc7497f10d87f0e438a2c95b7 Mon Sep 17 00:00:00 2001
From: "github-actions[bot]"
 <41898282+github-actions[bot]@users.noreply.github.com>
Date: Mon, 22 Jul 2024 12:26:53 +0200
Subject: [PATCH 05/20] Automatic toolchain upgrade to nightly-2024-07-20
 (#3366)

Update Rust toolchain from nightly-2024-07-19 to nightly-2024-07-20
without any other source changes.
This is an automatically generated pull request. If any of the CI checks
fail, manual intervention is required. In such a case, review the
changes at https://github.com/rust-lang/rust from
https://github.com/rust-lang/rust/commit/5affbb17153bc69a9d5d8d2faa4e399a014a211e
up to
https://github.com/rust-lang/rust/commit/9057c3ffec44926d5e149dc13ff3ce1613b69cce.
---
 rust-toolchain.toml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index adc62ae8e8db..a7a9ca6ca0e5 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-07-19"
+channel = "nightly-2024-07-20"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

From d6806795e0f501090787b0860126870dd79f7157 Mon Sep 17 00:00:00 2001
From: "github-actions[bot]"
 <41898282+github-actions[bot]@users.noreply.github.com>
Date: Mon, 22 Jul 2024 11:05:55 +0000
Subject: [PATCH 06/20] Automatic cargo update to 2024-07-22 (#3365)

Dependency upgrade resulting from `cargo update`.
---
 Cargo.lock | 42 +++++++++++++++++++++---------------------
 1 file changed, 21 insertions(+), 21 deletions(-)

diff --git a/Cargo.lock b/Cargo.lock
index fe420de27a88..0fd31f73278b 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -169,7 +169,7 @@ dependencies = [
  "heck",
  "proc-macro2",
  "quote",
- "syn 2.0.71",
+ "syn 2.0.72",
 ]
 
 [[package]]
@@ -482,7 +482,7 @@ dependencies = [
  "proc-macro-error",
  "proc-macro2",
  "quote",
- "syn 2.0.71",
+ "syn 2.0.72",
 ]
 
 [[package]]
@@ -801,9 +801,9 @@ dependencies = [
 
 [[package]]
 name = "redox_syscall"
-version = "0.5.2"
+version = "0.5.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c82cf8cff14456045f55ec4241383baeff27af886adb72ffb2162f99911de0fd"
+checksum = "2a908a6e00f1fdd0dfd9c0eb08ce85126f6d8bbda50017e74bc4a4b7d4a926a4"
 dependencies = [
  "bitflags",
 ]
@@ -924,7 +924,7 @@ checksum = "e0cd7e117be63d3c3678776753929474f3b04a43a080c744d6b0ae2a8c28e222"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.71",
+ "syn 2.0.72",
 ]
 
 [[package]]
@@ -1030,7 +1030,7 @@ dependencies = [
  "proc-macro2",
  "quote",
  "rustversion",
- "syn 2.0.71",
+ "syn 2.0.72",
 ]
 
 [[package]]
@@ -1045,9 +1045,9 @@ dependencies = [
 
 [[package]]
 name = "syn"
-version = "2.0.71"
+version = "2.0.72"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b146dcf730474b4bcd16c311627b31ede9ab149045db4d6088b3becaea046462"
+checksum = "dc4b9b9bf2add8093d3f2c0204471e951b2285580335de42f9d2534f3ae7a8af"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -1068,22 +1068,22 @@ dependencies = [
 
 [[package]]
 name = "thiserror"
-version = "1.0.62"
+version = "1.0.63"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f2675633b1499176c2dff06b0856a27976a8f9d436737b4cf4f312d4d91d8bbb"
+checksum = "c0342370b38b6a11b6cc11d6a805569958d54cfa061a29969c3b5ce2ea405724"
 dependencies = [
  "thiserror-impl",
 ]
 
 [[package]]
 name = "thiserror-impl"
-version = "1.0.62"
+version = "1.0.63"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d20468752b09f49e909e55a5d338caa8bedf615594e9d80bc4c565d30faf798c"
+checksum = "a4558b58466b9ad7ca0f102865eccc95938dca1a74a856f2b57b6629050da261"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.71",
+ "syn 2.0.72",
 ]
 
 [[package]]
@@ -1098,9 +1098,9 @@ dependencies = [
 
 [[package]]
 name = "toml"
-version = "0.8.14"
+version = "0.8.15"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6f49eb2ab21d2f26bd6db7bf383edc527a7ebaee412d17af4d40fdccd442f335"
+checksum = "ac2caab0bf757388c6c0ae23b3293fdb463fee59434529014f85e3263b995c28"
 dependencies = [
  "serde",
  "serde_spanned",
@@ -1119,9 +1119,9 @@ dependencies = [
 
 [[package]]
 name = "toml_edit"
-version = "0.22.15"
+version = "0.22.16"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d59a3a72298453f564e2b111fa896f8d07fabb36f51f06d7e875fc5e0b5a3ef1"
+checksum = "278f3d518e152219c994ce877758516bca5e118eaed6996192a774fb9fbf0788"
 dependencies = [
  "indexmap",
  "serde",
@@ -1149,7 +1149,7 @@ checksum = "34704c8d6ebcbc939824180af020566b01a7c01f80641264eba0999f6c2b6be7"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.71",
+ "syn 2.0.72",
 ]
 
 [[package]]
@@ -1384,9 +1384,9 @@ checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec"
 
 [[package]]
 name = "winnow"
-version = "0.6.13"
+version = "0.6.14"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "59b5e5f6c299a3c7890b876a2a587f3115162487e704907d9b6cd29473052ba1"
+checksum = "374ec40a2d767a3c1b4972d9475ecd557356637be906f2cb3f7fe17a6eb5e22f"
 dependencies = [
  "memchr",
 ]
@@ -1414,5 +1414,5 @@ checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.71",
+ "syn 2.0.72",
 ]

From 59371f358d1fff009846dc9554a7f9c72415d93e Mon Sep 17 00:00:00 2001
From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com>
Date: Mon, 22 Jul 2024 10:22:01 -0700
Subject: [PATCH 07/20] Bump tests/perf/s2n-quic from `71f8d9f` to `f568f26`
 (#3368)

Bumps [tests/perf/s2n-quic](https://github.com/aws/s2n-quic) from
`71f8d9f` to `f568f26`.
<details>
<summary>Commits</summary>
<ul>
<li><a
href="https://github.com/aws/s2n-quic/commit/f568f269ee5c9896f4936089c26dfbb3f87f4dab"><code>f568f26</code></a>
feat(s2n-quic-dc): return from ConfirmComplete when no dc version
negotiated ...</li>
<li><a
href="https://github.com/aws/s2n-quic/commit/518c0a9d76b388c85e86f021165f06f641a9f91f"><code>518c0a9</code></a>
fix(s2n-quic-dc): reorder wire version to preserve wire invariants (<a
href="https://redirect.github.com/aws/s2n-quic/issues/2277">#2277</a>)</li>
<li><a
href="https://github.com/aws/s2n-quic/commit/59564ffbcce0c6d6a42af45b3587f49cb249d6ea"><code>59564ff</code></a>
feat(s2n-quic-dc): add ClientConfirm subscriber (<a
href="https://redirect.github.com/aws/s2n-quic/issues/2274">#2274</a>)</li>
<li><a
href="https://github.com/aws/s2n-quic/commit/fcd9a1b2c0e4b5c76726b291316161eec259792b"><code>fcd9a1b</code></a>
feat(s2n-quic-dc): import 7/18 version (<a
href="https://redirect.github.com/aws/s2n-quic/issues/2275">#2275</a>)</li>
<li><a
href="https://github.com/aws/s2n-quic/commit/2c95dd95c03ca85005c3f0e1fba33574d45012b3"><code>2c95dd9</code></a>
feat(s2n-quic-dc): Periodically re-handshake existing path secrets (<a
href="https://redirect.github.com/aws/s2n-quic/issues/2276">#2276</a>)</li>
<li><a
href="https://github.com/aws/s2n-quic/commit/d55d258ab4981a0318f3a84aa7872f45b502092a"><code>d55d258</code></a>
feat(s2n-quic-transport): Support de-duplicating concurrent connections
to th...</li>
<li><a
href="https://github.com/aws/s2n-quic/commit/b3eb094898a1175dbc1213d4db3ff5a0d70931e0"><code>b3eb094</code></a>
fix(s2n-quic): implement Debug and Default for the disabled event
Subscriber ...</li>
<li>See full diff in <a
href="https://github.com/aws/s2n-quic/compare/71f8d9f5aafbf59f31ad85eeb7b4b67a7564a685...f568f269ee5c9896f4936089c26dfbb3f87f4dab">compare
view</a></li>
</ul>
</details>
<br />


Dependabot will resolve any conflicts with this PR as long as you don't
alter it yourself. You can also trigger a rebase manually by commenting
`@dependabot rebase`.

[//]: # (dependabot-automerge-start)
[//]: # (dependabot-automerge-end)

---

<details>
<summary>Dependabot commands and options</summary>
<br />

You can trigger Dependabot actions by commenting on this PR:
- `@dependabot rebase` will rebase this PR
- `@dependabot recreate` will recreate this PR, overwriting any edits
that have been made to it
- `@dependabot merge` will merge this PR after your CI passes on it
- `@dependabot squash and merge` will squash and merge this PR after
your CI passes on it
- `@dependabot cancel merge` will cancel a previously requested merge
and block automerging
- `@dependabot reopen` will reopen this PR if it is closed
- `@dependabot close` will close this PR and stop Dependabot recreating
it. You can achieve the same result by closing it manually
- `@dependabot show <dependency name> ignore conditions` will show all
of the ignore conditions of the specified dependency
- `@dependabot ignore this major version` will close this PR and stop
Dependabot creating any more for this major version (unless you reopen
the PR or upgrade to it yourself)
- `@dependabot ignore this minor version` will close this PR and stop
Dependabot creating any more for this minor version (unless you reopen
the PR or upgrade to it yourself)
- `@dependabot ignore this dependency` will close this PR and stop
Dependabot creating any more for this dependency (unless you reopen the
PR or upgrade to it yourself)


</details>

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
---
 tests/perf/s2n-quic | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/perf/s2n-quic b/tests/perf/s2n-quic
index 71f8d9f5aafb..f568f269ee5c 160000
--- a/tests/perf/s2n-quic
+++ b/tests/perf/s2n-quic
@@ -1 +1 @@
-Subproject commit 71f8d9f5aafbf59f31ad85eeb7b4b67a7564a685
+Subproject commit f568f269ee5c9896f4936089c26dfbb3f87f4dab

From 5d6bf6974055b53c1878ff1718c98c0ab4f98aed Mon Sep 17 00:00:00 2001
From: "github-actions[bot]"
 <41898282+github-actions[bot]@users.noreply.github.com>
Date: Mon, 22 Jul 2024 18:16:24 +0000
Subject: [PATCH 08/20] Automatic toolchain upgrade to nightly-2024-07-21
 (#3367)

Update Rust toolchain from nightly-2024-07-20 to nightly-2024-07-21
without any other source changes.
This is an automatically generated pull request. If any of the CI checks
fail, manual intervention is required. In such a case, review the
changes at https://github.com/rust-lang/rust from
https://github.com/rust-lang/rust/commit/9057c3ffec44926d5e149dc13ff3ce1613b69cce
up to
https://github.com/rust-lang/rust/commit/5069856495870486134dd2ca0b0e2516308c5c2a.
---
 rust-toolchain.toml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index a7a9ca6ca0e5..27c29bb820e2 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-07-20"
+channel = "nightly-2024-07-21"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

From 7ad4d1cc3109defea1131876f427f13599243ed8 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
Date: Mon, 22 Jul 2024 16:18:06 -0400
Subject: [PATCH 09/20] Enable an `#[safety_constraint(...)]` attribute helper
 for the `Arbitrary` and `Invariant` macros (#3283)

This PR enables an `#[safety_constraint(...)]` attribute helper for the
`#[derive(Arbitrary)]` and `#[derive(Invariant)]` macro.

For the `Invariant` derive macro, this allows users to derive more
sophisticated invariants for their data types by annotating individual
named fields with the `#[safety_constraint(<cond>)]` attribute, where
`<cond>` represents the predicate to be evaluated for the corresponding
field. In addition, the implementation always checks `#field.is_safe()`
for each field.

For example, let's say we are working with the `Point` type from #3250
```rs
#[derive(kani::Invariant)]
struct Point<X, Y> {
    x: X,
    y: Y,
}
```

and we need to extend it to only allow positive values for both `x` and
`y`.
With the `[safety_constraint(...)]` attribute, we can achieve this
without explicitly writing the `impl Invariant for ...` as follows:

```rs
#[derive(kani::Invariant)]
struct PositivePoint {
    #[safety_constraint(*x >= 0)]
    x: i32,
    #[safety_constraint(*y >= 0)]
    y: i32,
}
```

For the `Arbitrary` derive macro, this allows users to derive more
sophisticated `kani::any()` generators that respect the specified
invariants. In other words, the `kani::any()` will assume any invariants
specified through the `#[safety_constraint(...)]` attribute helper.
Going back to the `PositivePoint` example, we'd expect this harness to
be successful:

```rs
#[kani::proof]
fn check_invariant_helper_ok() {
    let pos_point: PositivePoint = kani::any();
    assert!(pos_point.x >= 0);
    assert!(pos_point.y >= 0);
}
```

The PR includes tests to ensure it's working as expected, in addition to
UI tests checking for cases where the arguments provided to the macro
are incorrect. Happy to add any other cases that you feel are missing.

Related #3095
---
 library/kani_macros/src/derive.rs             | 202 ++++++++++++++++--
 library/kani_macros/src/lib.rs                | 112 +++++++++-
 .../safety_constraint_helper/expected         |  17 ++
 .../safety_constraint_helper.rs               |  31 +++
 .../attrs_cfg_guard/attrs_cfg_guard.rs        |  24 +++
 .../derive-invariant/attrs_cfg_guard/expected |   9 +
 .../attrs_mixed/attrs_mixed.rs                |  24 +++
 .../derive-invariant/attrs_mixed/expected     |   9 +
 .../safety_constraint_helper/expected         |  13 ++
 .../safety_constraint_helper.rs               |  43 ++++
 .../safety_constraint_helper_funs/expected    |  13 ++
 .../safety_constraint_helper_funs.rs          |  48 +++++
 .../expected                                  |   0
 .../safety_invariant_fail.rs}                 |   0
 .../safety_invariant_fail_mut/expected        |  11 +
 .../safety_invariant_fail_mut.rs              |  28 +++
 .../ui/derive-invariant/helper-empty/expected |   6 +
 .../helper-empty/helper-empty.rs              |  17 ++
 .../derive-invariant/helper-no-expr/expected  |   6 +
 .../helper-no-expr/helper-no-expr.rs          |  17 ++
 .../helper-side-effect/expected               |   9 +
 .../helper-side-effect/helper-side-effect.rs  |  22 ++
 .../helper-wrong-expr/expected                |   9 +
 .../helper-wrong-expr/helper-wrong-expr.rs    |  18 ++
 24 files changed, 668 insertions(+), 20 deletions(-)
 create mode 100644 tests/expected/derive-arbitrary/safety_constraint_helper/expected
 create mode 100644 tests/expected/derive-arbitrary/safety_constraint_helper/safety_constraint_helper.rs
 create mode 100644 tests/expected/derive-invariant/attrs_cfg_guard/attrs_cfg_guard.rs
 create mode 100644 tests/expected/derive-invariant/attrs_cfg_guard/expected
 create mode 100644 tests/expected/derive-invariant/attrs_mixed/attrs_mixed.rs
 create mode 100644 tests/expected/derive-invariant/attrs_mixed/expected
 create mode 100644 tests/expected/derive-invariant/safety_constraint_helper/expected
 create mode 100644 tests/expected/derive-invariant/safety_constraint_helper/safety_constraint_helper.rs
 create mode 100644 tests/expected/derive-invariant/safety_constraint_helper_funs/expected
 create mode 100644 tests/expected/derive-invariant/safety_constraint_helper_funs/safety_constraint_helper_funs.rs
 rename tests/expected/derive-invariant/{invariant_fail => safety_invariant_fail}/expected (100%)
 rename tests/expected/derive-invariant/{invariant_fail/invariant_fail.rs => safety_invariant_fail/safety_invariant_fail.rs} (100%)
 create mode 100644 tests/expected/derive-invariant/safety_invariant_fail_mut/expected
 create mode 100644 tests/expected/derive-invariant/safety_invariant_fail_mut/safety_invariant_fail_mut.rs
 create mode 100644 tests/ui/derive-invariant/helper-empty/expected
 create mode 100644 tests/ui/derive-invariant/helper-empty/helper-empty.rs
 create mode 100644 tests/ui/derive-invariant/helper-no-expr/expected
 create mode 100644 tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs
 create mode 100644 tests/ui/derive-invariant/helper-side-effect/expected
 create mode 100644 tests/ui/derive-invariant/helper-side-effect/helper-side-effect.rs
 create mode 100644 tests/ui/derive-invariant/helper-wrong-expr/expected
 create mode 100644 tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs

diff --git a/library/kani_macros/src/derive.rs b/library/kani_macros/src/derive.rs
index 4e99590fc6a3..a7aaa8ae334e 100644
--- a/library/kani_macros/src/derive.rs
+++ b/library/kani_macros/src/derive.rs
@@ -28,11 +28,30 @@ pub fn expand_derive_arbitrary(item: proc_macro::TokenStream) -> proc_macro::Tok
     let (impl_generics, ty_generics, where_clause) = generics.split_for_impl();
 
     let body = fn_any_body(&item_name, &derive_item.data);
-    let expanded = quote! {
-        // The generated implementation.
-        impl #impl_generics kani::Arbitrary for #item_name #ty_generics #where_clause {
-            fn any() -> Self {
-                #body
+
+    // Get the safety constraints (if any) to produce type-safe values
+    let safety_conds_opt = safety_conds(&item_name, &derive_item.data);
+
+    let expanded = if let Some(safety_cond) = safety_conds_opt {
+        let field_refs = field_refs(&item_name, &derive_item.data);
+        quote! {
+            // The generated implementation.
+            impl #impl_generics kani::Arbitrary for #item_name #ty_generics #where_clause {
+                fn any() -> Self {
+                    let obj = #body;
+                    #field_refs
+                    kani::assume(#safety_cond);
+                    obj
+                }
+            }
+        }
+    } else {
+        quote! {
+            // The generated implementation.
+            impl #impl_generics kani::Arbitrary for #item_name #ty_generics #where_clause {
+                fn any() -> Self {
+                    #body
+                }
             }
         }
     };
@@ -75,6 +94,103 @@ fn fn_any_body(ident: &Ident, data: &Data) -> TokenStream {
     }
 }
 
+/// Parse the condition expressions in `#[safety_constraint(<cond>)]` attached to struct
+/// fields and, it at least one was found, generate a conjunction to be assumed.
+///
+/// For example, if we're deriving implementations for the struct
+/// ```
+/// #[derive(Arbitrary)]
+/// #[derive(Invariant)]
+/// struct PositivePoint {
+///     #[safety_constraint(*x >= 0)]
+///     x: i32,
+///     #[safety_constraint(*y >= 0)]
+///     y: i32,
+/// }
+/// ```
+/// this function will generate the `TokenStream`
+/// ```
+/// *x >= 0 && *y >= 0
+/// ```
+/// which can be passed to `kani::assume` to constrain the values generated
+/// through the `Arbitrary` impl so that they are type-safe by construction.
+fn safety_conds(ident: &Ident, data: &Data) -> Option<TokenStream> {
+    match data {
+        Data::Struct(struct_data) => safety_conds_inner(ident, &struct_data.fields),
+        Data::Enum(_) => None,
+        Data::Union(_) => None,
+    }
+}
+
+/// Generates an expression resulting from the conjunction of conditions
+/// specified as safety constraints for each field. See `safety_conds` for more details.
+fn safety_conds_inner(ident: &Ident, fields: &Fields) -> Option<TokenStream> {
+    match fields {
+        Fields::Named(ref fields) => {
+            let conds: Vec<TokenStream> =
+                fields.named.iter().filter_map(|field| parse_safety_expr(ident, field)).collect();
+            if !conds.is_empty() { Some(quote! { #(#conds)&&* }) } else { None }
+        }
+        Fields::Unnamed(_) => None,
+        Fields::Unit => None,
+    }
+}
+
+/// Generates the sequence of expressions to initialize the variables used as
+/// references to the struct fields.
+///
+/// For example, if we're deriving implementations for the struct
+/// ```
+/// #[derive(Arbitrary)]
+/// #[derive(Invariant)]
+/// struct PositivePoint {
+///     #[safety_constraint(*x >= 0)]
+///     x: i32,
+///     #[safety_constraint(*y >= 0)]
+///     y: i32,
+/// }
+/// ```
+/// this function will generate the `TokenStream`
+/// ```
+/// let x = &obj.x;
+/// let y = &obj.y;
+/// ```
+/// which allows us to refer to the struct fields without using `self`.
+/// Note that the actual stream is generated in the `field_refs_inner` function.
+fn field_refs(ident: &Ident, data: &Data) -> TokenStream {
+    match data {
+        Data::Struct(struct_data) => field_refs_inner(ident, &struct_data.fields),
+        Data::Enum(_) => unreachable!(),
+        Data::Union(_) => unreachable!(),
+    }
+}
+
+/// Generates the sequence of expressions to initialize the variables used as
+/// references to the struct fields. See `field_refs` for more details.
+fn field_refs_inner(_ident: &Ident, fields: &Fields) -> TokenStream {
+    match fields {
+        Fields::Named(ref fields) => {
+            let field_refs: Vec<TokenStream> = fields
+                .named
+                .iter()
+                .map(|field| {
+                    let name = &field.ident;
+                    quote_spanned! {field.span()=>
+                        let #name = &obj.#name;
+                    }
+                })
+                .collect();
+            if !field_refs.is_empty() {
+                quote! { #( #field_refs )* }
+            } else {
+                quote! {}
+            }
+        }
+        Fields::Unnamed(_) => quote! {},
+        Fields::Unit => quote! {},
+    }
+}
+
 /// Generate an item initialization where an item can be a struct or a variant.
 /// For named fields, this will generate: `Item { field1: kani::any(), field2: kani::any(), .. }`
 /// For unnamed fields, this will generate: `Item (kani::any(), kani::any(), ..)`
@@ -115,6 +231,42 @@ fn init_symbolic_item(ident: &Ident, fields: &Fields) -> TokenStream {
     }
 }
 
+/// Extract, parse and return the expression `cond` (i.e., `Some(cond)`) in the
+/// `#[safety_constraint(<cond>)]` attribute helper associated with a given field.
+/// Return `None` if the attribute isn't specified.
+fn parse_safety_expr(ident: &Ident, field: &syn::Field) -> Option<TokenStream> {
+    let name = &field.ident;
+    let mut safety_helper_attr = None;
+
+    // Keep the helper attribute if we find it
+    for attr in &field.attrs {
+        if attr.path().is_ident("safety_constraint") {
+            safety_helper_attr = Some(attr);
+        }
+    }
+
+    // Parse the arguments in the `#[safety_constraint(...)]` attribute
+    if let Some(attr) = safety_helper_attr {
+        let expr_args: Result<syn::Expr, syn::Error> = attr.parse_args();
+
+        // Check if there was an error parsing the arguments
+        if let Err(err) = expr_args {
+            abort!(Span::call_site(), "Cannot derive impl for `{}`", ident;
+            note = attr.span() =>
+            "safety constraint in field `{}` could not be parsed: {}", name.as_ref().unwrap().to_string(), err
+            )
+        }
+
+        // Return the expression associated to the safety constraint
+        let safety_expr = expr_args.unwrap();
+        Some(quote_spanned! {field.span()=>
+            #safety_expr
+        })
+    } else {
+        None
+    }
+}
+
 /// Generate the body of the function `any()` for enums. The cases are:
 /// 1. For zero-variants enumerations, this will encode a `panic!()` statement.
 /// 2. For one or more variants, the code will be something like:
@@ -176,10 +328,14 @@ pub fn expand_derive_invariant(item: proc_macro::TokenStream) -> proc_macro::Tok
     let (impl_generics, ty_generics, where_clause) = generics.split_for_impl();
 
     let body = is_safe_body(&item_name, &derive_item.data);
+    let field_refs = field_refs(&item_name, &derive_item.data);
+
     let expanded = quote! {
         // The generated implementation.
         impl #impl_generics kani::Invariant for #item_name #ty_generics #where_clause {
             fn is_safe(&self) -> bool {
+                let obj = self;
+                #field_refs
                 #body
             }
         }
@@ -199,7 +355,7 @@ fn add_trait_bound_invariant(mut generics: Generics) -> Generics {
 
 fn is_safe_body(ident: &Ident, data: &Data) -> TokenStream {
     match data {
-        Data::Struct(struct_data) => struct_safe_conjunction(ident, &struct_data.fields),
+        Data::Struct(struct_data) => struct_invariant_conjunction(ident, &struct_data.fields),
         Data::Enum(_) => {
             abort!(Span::call_site(), "Cannot derive `Invariant` for `{}` enum", ident;
                 note = ident.span() =>
@@ -215,21 +371,35 @@ fn is_safe_body(ident: &Ident, data: &Data) -> TokenStream {
     }
 }
 
-/// Generates an expression that is the conjunction of `is_safe` calls for each field in the struct.
-fn struct_safe_conjunction(_ident: &Ident, fields: &Fields) -> TokenStream {
+/// Generates an expression that is the conjunction of safety constraints for each field in the struct.
+fn struct_invariant_conjunction(ident: &Ident, fields: &Fields) -> TokenStream {
     match fields {
         // Expands to the expression
+        // `true && <safety_cond1> && <safety_cond2> && ..`
+        // where `safety_condN` is
+        //  - `self.fieldN.is_safe() && <cond>` if a condition `<cond>` was
+        //    specified through the `#[safety_constraint(<cond>)]` helper attribute, or
+        //  - `self.fieldN.is_safe()` otherwise
+        //
+        // Therefore, if `#[safety_constraint(<cond>)]` isn't specified for any field, this expands to
         // `true && self.field1.is_safe() && self.field2.is_safe() && ..`
         Fields::Named(ref fields) => {
-            let safe_calls = fields.named.iter().map(|field| {
-                let name = &field.ident;
-                quote_spanned! {field.span()=>
-                    self.#name.is_safe()
-                }
-            });
+            let safety_conds: Vec<TokenStream> = fields
+                .named
+                .iter()
+                .map(|field| {
+                    let name = &field.ident;
+                    let default_expr = quote_spanned! {field.span()=>
+                        #name.is_safe()
+                    };
+                    parse_safety_expr(ident, field)
+                        .map(|expr| quote! { #expr && #default_expr})
+                        .unwrap_or(default_expr)
+                })
+                .collect();
             // An initial value is required for empty structs
-            safe_calls.fold(quote! { true }, |acc, call| {
-                quote! { #acc && #call }
+            safety_conds.iter().fold(quote! { true }, |acc, cond| {
+                quote! { #acc && #cond }
             })
         }
         Fields::Unnamed(ref fields) => {
diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs
index b10b8a74cdc5..4e3a8d6f9f5b 100644
--- a/library/kani_macros/src/lib.rs
+++ b/library/kani_macros/src/lib.rs
@@ -100,16 +100,120 @@ pub fn unstable_feature(attr: TokenStream, item: TokenStream) -> TokenStream {
     attr_impl::unstable(attr, item)
 }
 
-/// Allow users to auto generate Arbitrary implementations by using `#[derive(Arbitrary)]` macro.
+/// Allow users to auto generate `Arbitrary` implementations by using
+/// `#[derive(Arbitrary)]` macro.
+///
+/// When using `#[derive(Arbitrary)]` on a struct, the `#[safety_constraint(<cond>)]`
+/// attribute can be added to its fields to indicate a type safety invariant
+/// condition `<cond>`. Since `kani::any()` is always expected to produce
+/// type-safe values, **adding `#[safety_constraint(...)]` to any fields will further
+/// constrain the objects generated with `kani::any()`**.
+///
+/// For example, the `check_positive` harness in this code is expected to
+/// pass:
+///
+/// ```rs
+/// #[derive(kani::Arbitrary)]
+/// struct AlwaysPositive {
+///     #[safety_constraint(*inner >= 0)]
+///     inner: i32,
+/// }
+///
+/// #[kani::proof]
+/// fn check_positive() {
+///     let val: AlwaysPositive = kani::any();
+///     assert!(val.inner >= 0);
+/// }
+/// ```
+///
+/// Therefore, using the `#[safety_constraint(...)]` attribute can lead to vacuous
+/// results when the values are over-constrained. For example, in this code
+/// the `check_positive` harness will pass too:
+///
+/// ```rs
+/// #[derive(kani::Arbitrary)]
+/// struct AlwaysPositive {
+///     #[safety_constraint(*inner >= 0 && *inner < i32::MIN)]
+///     inner: i32,
+/// }
+///
+/// #[kani::proof]
+/// fn check_positive() {
+///     let val: AlwaysPositive = kani::any();
+///     assert!(val.inner >= 0);
+/// }
+/// ```
+///
+/// Unfortunately, we made a mistake when specifying the condition because
+/// `*inner >= 0 && *inner < i32::MIN` is equivalent to `false`. This results
+/// in the relevant assertion being unreachable:
+///
+/// ```
+/// Check 1: check_positive.assertion.1
+///         - Status: UNREACHABLE
+///         - Description: "assertion failed: val.inner >= 0"
+///         - Location: src/main.rs:22:5 in function check_positive
+/// ```
+///
+/// As usual, we recommend users to defend against these behaviors by using
+/// `kani::cover!(...)` checks and watching out for unreachable assertions in
+/// their project's code.
 #[proc_macro_error]
-#[proc_macro_derive(Arbitrary)]
+#[proc_macro_derive(Arbitrary, attributes(safety_constraint))]
 pub fn derive_arbitrary(item: TokenStream) -> TokenStream {
     derive::expand_derive_arbitrary(item)
 }
 
-/// Allow users to auto generate Invariant implementations by using `#[derive(Invariant)]` macro.
+/// Allow users to auto generate `Invariant` implementations by using
+/// `#[derive(Invariant)]` macro.
+///
+/// When using `#[derive(Invariant)]` on a struct, the `#[safety_constraint(<cond>)]`
+/// attribute can be added to its fields to indicate a type safety invariant
+/// condition `<cond>`. This will ensure that the gets additionally checked when
+/// using the `is_safe()` method generated by the `#[derive(Invariant)]` macro.
+///
+/// For example, the `check_positive` harness in this code is expected to
+/// fail:
+///
+/// ```rs
+/// #[derive(kani::Invariant)]
+/// struct AlwaysPositive {
+///     #[safety_constraint(*inner >= 0)]
+///     inner: i32,
+/// }
+///
+/// #[kani::proof]
+/// fn check_positive() {
+///     let val = AlwaysPositive { inner: -1 };
+///     assert!(val.is_safe());
+/// }
+/// ```
+///
+/// This is not too surprising since the type safety invariant that we indicated
+/// is not being taken into account when we create the `AlwaysPositive` object.
+///
+/// As mentioned, the `is_safe()` methods generated by the
+/// `#[derive(Invariant)]` macro check the corresponding `is_safe()` method for
+/// each field in addition to any type safety invariants specified through the
+/// `#[safety_constraint(...)]` attribute.
+///
+/// For example, for the `AlwaysPositive` struct from above, we will generate
+/// the following implementation:
+///
+/// ```rs
+/// impl kani::Invariant for AlwaysPositive {
+///     fn is_safe(&self) -> bool {
+///         let obj = self;
+///         let inner = &obj.inner;
+///         true && *inner >= 0 && inner.is_safe()
+///     }
+/// }
+/// ```
+///
+/// Note: the assignments to `obj` and `inner` are made so that we can treat the
+/// fields as if they were references.
 #[proc_macro_error]
-#[proc_macro_derive(Invariant)]
+#[proc_macro_derive(Invariant, attributes(safety_constraint))]
 pub fn derive_invariant(item: TokenStream) -> TokenStream {
     derive::expand_derive_invariant(item)
 }
diff --git a/tests/expected/derive-arbitrary/safety_constraint_helper/expected b/tests/expected/derive-arbitrary/safety_constraint_helper/expected
new file mode 100644
index 000000000000..f35f18084911
--- /dev/null
+++ b/tests/expected/derive-arbitrary/safety_constraint_helper/expected
@@ -0,0 +1,17 @@
+Check 1: check_invariant_helper_ok.assertion.1\
+         - Status: SUCCESS\
+         - Description: "assertion failed: pos_point.x >= 0"
+
+Check 2: check_invariant_helper_ok.assertion.2\
+         - Status: SUCCESS\
+         - Description: "assertion failed: pos_point.y >= 0"
+
+Check 1: check_invariant_helper_fail.assertion.1\
+         - Status: FAILURE\
+         - Description: "assertion failed: pos_point.x >= 0"
+
+Check 2: check_invariant_helper_fail.assertion.2\
+         - Status: FAILURE\
+         - Description: "assertion failed: pos_point.y >= 0"
+
+Complete - 2 successfully verified harnesses, 0 failures, 2 total.
diff --git a/tests/expected/derive-arbitrary/safety_constraint_helper/safety_constraint_helper.rs b/tests/expected/derive-arbitrary/safety_constraint_helper/safety_constraint_helper.rs
new file mode 100644
index 000000000000..5b608aa2a3c0
--- /dev/null
+++ b/tests/expected/derive-arbitrary/safety_constraint_helper/safety_constraint_helper.rs
@@ -0,0 +1,31 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that the `#[safety_constraint(...)]` attribute helper adds the conditions provided to
+//! the attribute to the derived `Arbitrary` implementation.
+
+extern crate kani;
+use kani::Invariant;
+
+#[derive(kani::Arbitrary)]
+struct PositivePoint {
+    #[safety_constraint(*x >= 0)]
+    x: i32,
+    #[safety_constraint(*y >= 0)]
+    y: i32,
+}
+
+#[kani::proof]
+fn check_invariant_helper_ok() {
+    let pos_point: PositivePoint = kani::any();
+    assert!(pos_point.x >= 0);
+    assert!(pos_point.y >= 0);
+}
+
+#[kani::proof]
+#[kani::should_panic]
+fn check_invariant_helper_fail() {
+    let pos_point: PositivePoint = PositivePoint { x: kani::any(), y: kani::any() };
+    assert!(pos_point.x >= 0);
+    assert!(pos_point.y >= 0);
+}
diff --git a/tests/expected/derive-invariant/attrs_cfg_guard/attrs_cfg_guard.rs b/tests/expected/derive-invariant/attrs_cfg_guard/attrs_cfg_guard.rs
new file mode 100644
index 000000000000..546695bf3731
--- /dev/null
+++ b/tests/expected/derive-invariant/attrs_cfg_guard/attrs_cfg_guard.rs
@@ -0,0 +1,24 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that the `#[safety_constraint(...)]` attribute helper is picked up
+//! when it's used with `cfg_attr(kani, ...)]`.
+
+extern crate kani;
+use kani::Invariant;
+
+#[derive(kani::Arbitrary)]
+#[derive(kani::Invariant)]
+struct PositivePoint {
+    #[cfg_attr(kani, safety_constraint(*x >= 0))]
+    x: i32,
+    #[cfg_attr(kani, safety_constraint(*y >= 0))]
+    y: i32,
+}
+
+#[kani::proof]
+fn check_safety_constraint_cfg() {
+    let pos_point: PositivePoint = kani::any();
+    assert!(pos_point.x >= 0);
+    assert!(pos_point.y >= 0);
+}
diff --git a/tests/expected/derive-invariant/attrs_cfg_guard/expected b/tests/expected/derive-invariant/attrs_cfg_guard/expected
new file mode 100644
index 000000000000..edb3e256975d
--- /dev/null
+++ b/tests/expected/derive-invariant/attrs_cfg_guard/expected
@@ -0,0 +1,9 @@
+Check 1: check_safety_constraint_cfg.assertion.1\
+         - Status: SUCCESS\
+         - Description: "assertion failed: pos_point.x >= 0"
+
+Check 2: check_safety_constraint_cfg.assertion.2\
+         - Status: SUCCESS\
+         - Description: "assertion failed: pos_point.y >= 0"
+
+Complete - 1 successfully verified harnesses, 0 failures, 1 total.
diff --git a/tests/expected/derive-invariant/attrs_mixed/attrs_mixed.rs b/tests/expected/derive-invariant/attrs_mixed/attrs_mixed.rs
new file mode 100644
index 000000000000..ff58ff846c67
--- /dev/null
+++ b/tests/expected/derive-invariant/attrs_mixed/attrs_mixed.rs
@@ -0,0 +1,24 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that in the `#[safety_constraint(...)]` attribute helper it is
+//! possible to refer to other struct fields, not just the one associated with
+//! the attribute.
+
+extern crate kani;
+use kani::Invariant;
+
+#[derive(kani::Arbitrary)]
+#[derive(kani::Invariant)]
+struct PositivePoint {
+    #[safety_constraint(*x >= 0 && *y >= 0)]
+    x: i32,
+    y: i32,
+}
+
+#[kani::proof]
+fn check_safety_constraint_cfg() {
+    let pos_point: PositivePoint = kani::any();
+    assert!(pos_point.x >= 0);
+    assert!(pos_point.y >= 0);
+}
diff --git a/tests/expected/derive-invariant/attrs_mixed/expected b/tests/expected/derive-invariant/attrs_mixed/expected
new file mode 100644
index 000000000000..edb3e256975d
--- /dev/null
+++ b/tests/expected/derive-invariant/attrs_mixed/expected
@@ -0,0 +1,9 @@
+Check 1: check_safety_constraint_cfg.assertion.1\
+         - Status: SUCCESS\
+         - Description: "assertion failed: pos_point.x >= 0"
+
+Check 2: check_safety_constraint_cfg.assertion.2\
+         - Status: SUCCESS\
+         - Description: "assertion failed: pos_point.y >= 0"
+
+Complete - 1 successfully verified harnesses, 0 failures, 1 total.
diff --git a/tests/expected/derive-invariant/safety_constraint_helper/expected b/tests/expected/derive-invariant/safety_constraint_helper/expected
new file mode 100644
index 000000000000..31b6de54c647
--- /dev/null
+++ b/tests/expected/derive-invariant/safety_constraint_helper/expected
@@ -0,0 +1,13 @@
+Check 1: check_invariant_helper_ok.assertion.1\
+         - Status: SUCCESS\
+         - Description: "assertion failed: pos_point.is_safe()"
+
+Check 1: check_invariant_helper_ok_manual.assertion.1\
+         - Status: SUCCESS\
+         - Description: "assertion failed: pos_point.is_safe()"
+
+Check 1: check_invariant_helper_fail.assertion.1\
+         - Status: FAILURE\
+         - Description: "assertion failed: pos_point.is_safe()"
+
+Complete - 3 successfully verified harnesses, 0 failures, 3 total.
diff --git a/tests/expected/derive-invariant/safety_constraint_helper/safety_constraint_helper.rs b/tests/expected/derive-invariant/safety_constraint_helper/safety_constraint_helper.rs
new file mode 100644
index 000000000000..44a218f8fa63
--- /dev/null
+++ b/tests/expected/derive-invariant/safety_constraint_helper/safety_constraint_helper.rs
@@ -0,0 +1,43 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that the `#[safety_constraint(...)]` attribute helper adds the conditions provided to
+//! the attribute to the derived `Invariant` implementation.
+
+extern crate kani;
+use kani::Invariant;
+
+#[derive(kani::Arbitrary)]
+#[derive(kani::Invariant)]
+struct PositivePoint {
+    #[safety_constraint(*x >= 0)]
+    x: i32,
+    #[safety_constraint(*y >= 0)]
+    y: i32,
+}
+
+#[kani::proof]
+fn check_invariant_helper_ok() {
+    let pos_point: PositivePoint = kani::any();
+    assert!(pos_point.is_safe());
+}
+
+#[kani::proof]
+#[kani::should_panic]
+fn check_invariant_helper_fail() {
+    // In this case, we build the struct from unconstrained arbitrary values
+    // that do not respect `PositivePoint`'s safety constraints.
+    let pos_point: PositivePoint = PositivePoint { x: kani::any(), y: kani::any() };
+    assert!(pos_point.is_safe());
+}
+
+#[kani::proof]
+fn check_invariant_helper_ok_manual() {
+    // In this case, we build the struct from unconstrained arbitrary values
+    // that do not respect `PositivePoint`'s safety constraints. However, we
+    // manually constrain them later.
+    let pos_point: PositivePoint = PositivePoint { x: kani::any(), y: kani::any() };
+    kani::assume(pos_point.x >= 0);
+    kani::assume(pos_point.y >= 0);
+    assert!(pos_point.is_safe());
+}
diff --git a/tests/expected/derive-invariant/safety_constraint_helper_funs/expected b/tests/expected/derive-invariant/safety_constraint_helper_funs/expected
new file mode 100644
index 000000000000..31b6de54c647
--- /dev/null
+++ b/tests/expected/derive-invariant/safety_constraint_helper_funs/expected
@@ -0,0 +1,13 @@
+Check 1: check_invariant_helper_ok.assertion.1\
+         - Status: SUCCESS\
+         - Description: "assertion failed: pos_point.is_safe()"
+
+Check 1: check_invariant_helper_ok_manual.assertion.1\
+         - Status: SUCCESS\
+         - Description: "assertion failed: pos_point.is_safe()"
+
+Check 1: check_invariant_helper_fail.assertion.1\
+         - Status: FAILURE\
+         - Description: "assertion failed: pos_point.is_safe()"
+
+Complete - 3 successfully verified harnesses, 0 failures, 3 total.
diff --git a/tests/expected/derive-invariant/safety_constraint_helper_funs/safety_constraint_helper_funs.rs b/tests/expected/derive-invariant/safety_constraint_helper_funs/safety_constraint_helper_funs.rs
new file mode 100644
index 000000000000..a2c4600eb208
--- /dev/null
+++ b/tests/expected/derive-invariant/safety_constraint_helper_funs/safety_constraint_helper_funs.rs
@@ -0,0 +1,48 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that functions can be called in the `#[safety_constraint(...)]` attribute helpers.
+//! This is like the `invariant_helper` test but using a function instead
+//! of passing in a predicate.
+
+extern crate kani;
+use kani::Invariant;
+
+#[derive(kani::Arbitrary)]
+#[derive(kani::Invariant)]
+struct PositivePoint {
+    #[safety_constraint(is_coordinate_safe(x))]
+    x: i32,
+    #[safety_constraint(is_coordinate_safe(y))]
+    y: i32,
+}
+
+fn is_coordinate_safe(val: &i32) -> bool {
+    *val >= 0
+}
+
+#[kani::proof]
+fn check_invariant_helper_ok() {
+    let pos_point: PositivePoint = kani::any();
+    assert!(pos_point.is_safe());
+}
+
+#[kani::proof]
+#[kani::should_panic]
+fn check_invariant_helper_fail() {
+    // In this case, we build the struct from unconstrained arbitrary values
+    // that do not respect `PositivePoint`'s safety constraints.
+    let pos_point: PositivePoint = PositivePoint { x: kani::any(), y: kani::any() };
+    assert!(pos_point.is_safe());
+}
+
+#[kani::proof]
+fn check_invariant_helper_ok_manual() {
+    // In this case, we build the struct from unconstrained arbitrary values
+    // that do not respect `PositivePoint`'s safety constraints. However, we
+    // manually constrain them later.
+    let pos_point: PositivePoint = PositivePoint { x: kani::any(), y: kani::any() };
+    kani::assume(pos_point.x >= 0);
+    kani::assume(pos_point.y >= 0);
+    assert!(pos_point.is_safe());
+}
diff --git a/tests/expected/derive-invariant/invariant_fail/expected b/tests/expected/derive-invariant/safety_invariant_fail/expected
similarity index 100%
rename from tests/expected/derive-invariant/invariant_fail/expected
rename to tests/expected/derive-invariant/safety_invariant_fail/expected
diff --git a/tests/expected/derive-invariant/invariant_fail/invariant_fail.rs b/tests/expected/derive-invariant/safety_invariant_fail/safety_invariant_fail.rs
similarity index 100%
rename from tests/expected/derive-invariant/invariant_fail/invariant_fail.rs
rename to tests/expected/derive-invariant/safety_invariant_fail/safety_invariant_fail.rs
diff --git a/tests/expected/derive-invariant/safety_invariant_fail_mut/expected b/tests/expected/derive-invariant/safety_invariant_fail_mut/expected
new file mode 100644
index 000000000000..0853a68fa79e
--- /dev/null
+++ b/tests/expected/derive-invariant/safety_invariant_fail_mut/expected
@@ -0,0 +1,11 @@
+Check 1: check_invariant_fail_mut.assertion.1\
+         - Status: SUCCESS\
+         - Description: "assertion failed: pos_point.is_safe()"
+
+Check 2: check_invariant_fail_mut.assertion.2\
+         - Status: FAILURE\
+         - Description: "assertion failed: pos_point.is_safe()"
+
+VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected)
+
+Complete - 1 successfully verified harnesses, 0 failures, 1 total.
diff --git a/tests/expected/derive-invariant/safety_invariant_fail_mut/safety_invariant_fail_mut.rs b/tests/expected/derive-invariant/safety_invariant_fail_mut/safety_invariant_fail_mut.rs
new file mode 100644
index 000000000000..dc659ec66dd6
--- /dev/null
+++ b/tests/expected/derive-invariant/safety_invariant_fail_mut/safety_invariant_fail_mut.rs
@@ -0,0 +1,28 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that a verification failure is triggered if we check the invariant
+//! after mutating an object to violate it.
+
+extern crate kani;
+use kani::Invariant;
+
+#[derive(kani::Arbitrary)]
+#[derive(kani::Invariant)]
+struct PositivePoint {
+    #[safety_constraint(*x >= 0)]
+    x: i32,
+    #[safety_constraint(*y >= 0)]
+    y: i32,
+}
+
+#[kani::proof]
+#[kani::should_panic]
+fn check_invariant_fail_mut() {
+    let mut pos_point: PositivePoint = kani::any();
+    assert!(pos_point.is_safe());
+    // Set the `x` field to an unsafe value
+    pos_point.x = -1;
+    // The object's invariant isn't preserved anymore so the next check fails
+    assert!(pos_point.is_safe());
+}
diff --git a/tests/ui/derive-invariant/helper-empty/expected b/tests/ui/derive-invariant/helper-empty/expected
new file mode 100644
index 000000000000..d8590a9d22b8
--- /dev/null
+++ b/tests/ui/derive-invariant/helper-empty/expected
@@ -0,0 +1,6 @@
+error: Cannot derive impl for `PositivePoint`
+   |
+| #[derive(kani::Invariant)]
+   |          ^^^^^^^^^^^^^^^
+   |
+note: safety constraint in field `x` could not be parsed: expected attribute arguments in parentheses: #[safety_constraint(...)]
diff --git a/tests/ui/derive-invariant/helper-empty/helper-empty.rs b/tests/ui/derive-invariant/helper-empty/helper-empty.rs
new file mode 100644
index 000000000000..3086603cf5db
--- /dev/null
+++ b/tests/ui/derive-invariant/helper-empty/helper-empty.rs
@@ -0,0 +1,17 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check the compilation error for the `#[safety_constraint(...)]` attribute helper when an
+//! argument isn't provided.
+
+extern crate kani;
+use kani::Invariant;
+
+#[derive(kani::Arbitrary)]
+#[derive(kani::Invariant)]
+struct PositivePoint {
+    #[safety_constraint]
+    x: i32,
+    #[safety_constraint(*y >= 0)]
+    y: i32,
+}
diff --git a/tests/ui/derive-invariant/helper-no-expr/expected b/tests/ui/derive-invariant/helper-no-expr/expected
new file mode 100644
index 000000000000..e9ac7e3e1124
--- /dev/null
+++ b/tests/ui/derive-invariant/helper-no-expr/expected
@@ -0,0 +1,6 @@
+error: Cannot derive impl for `PositivePoint`
+   |
+| #[derive(kani::Invariant)]
+   |          ^^^^^^^^^^^^^^^
+   |
+note: safety constraint in field `x` could not be parsed: unexpected end of input, expected an expression
diff --git a/tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs b/tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs
new file mode 100644
index 000000000000..080c94371257
--- /dev/null
+++ b/tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs
@@ -0,0 +1,17 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check the compilation error for the `#[safety_constraint(...)]` attribute helper when the
+//! argument is not a proper expression.
+
+extern crate kani;
+use kani::Invariant;
+
+#[derive(kani::Arbitrary)]
+#[derive(kani::Invariant)]
+struct PositivePoint {
+    #[safety_constraint()]
+    x: i32,
+    #[safety_constraint(*y >= 0)]
+    y: i32,
+}
diff --git a/tests/ui/derive-invariant/helper-side-effect/expected b/tests/ui/derive-invariant/helper-side-effect/expected
new file mode 100644
index 000000000000..20b3d17efd38
--- /dev/null
+++ b/tests/ui/derive-invariant/helper-side-effect/expected
@@ -0,0 +1,9 @@
+error[E0596]: cannot borrow `*x` as mutable, as it is behind a `&` reference
+   |
+|     #[safety_constraint({*(x.as_mut()) = 0; true})]
+   |                            ^ `x` is a `&` reference, so the data it refers to cannot be borrowed as mutable
+   |
+help: consider specifying this binding's type
+   |
+|     x: &mut std::boxed::Box<i32>: Box<i32>,
+   |      +++++++++++++++++++++++++++
diff --git a/tests/ui/derive-invariant/helper-side-effect/helper-side-effect.rs b/tests/ui/derive-invariant/helper-side-effect/helper-side-effect.rs
new file mode 100644
index 000000000000..e80f2ff25796
--- /dev/null
+++ b/tests/ui/derive-invariant/helper-side-effect/helper-side-effect.rs
@@ -0,0 +1,22 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that side effect expressions in the `#[safety_constraint(...)]`
+//! attribute helpers are not allowed.
+
+extern crate kani;
+use kani::Invariant;
+
+#[derive(kani::Arbitrary)]
+#[derive(kani::Invariant)]
+struct PositivePoint {
+    #[safety_constraint({*(x.as_mut()) = 0; true})]
+    x: Box<i32>,
+    y: i32,
+}
+
+#[kani::proof]
+fn check_invariant_helper_ok() {
+    let pos_point: PositivePoint = kani::any();
+    assert!(pos_point.is_safe());
+}
diff --git a/tests/ui/derive-invariant/helper-wrong-expr/expected b/tests/ui/derive-invariant/helper-wrong-expr/expected
new file mode 100644
index 000000000000..3f661bce9cbb
--- /dev/null
+++ b/tests/ui/derive-invariant/helper-wrong-expr/expected
@@ -0,0 +1,9 @@
+error[E0308]: mismatched types
+   |
+|     #[safety_constraint(x >= 0)]
+   |                              ^ expected `&i32`, found integer
+   |
+help: consider dereferencing the borrow
+   |
+|     #[safety_constraint(*x >= 0)]
+   |
diff --git a/tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs b/tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs
new file mode 100644
index 000000000000..66b42e02fd68
--- /dev/null
+++ b/tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs
@@ -0,0 +1,18 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check the compilation error for the `#[safety_constraint(...)]` attribute helper when the
+//! argument cannot be evaluated in the struct's context.
+
+extern crate kani;
+use kani::Invariant;
+
+#[derive(kani::Arbitrary)]
+#[derive(kani::Invariant)]
+struct PositivePoint {
+    // Note: `x` is a reference in this context, we should refer to `*x`
+    #[safety_constraint(x >= 0)]
+    x: i32,
+    #[safety_constraint(*y >= 0)]
+    y: i32,
+}

From ea0f54a6ddf9e1d449c6c96662e02bc339c6bb0c Mon Sep 17 00:00:00 2001
From: Jacob Salzberg <jsalzbergedu@yahoo.com>
Date: Tue, 23 Jul 2024 14:25:24 -0400
Subject: [PATCH 10/20] Test that boxed fn parameters are implemented. (#3361)

This regression test ensures that issue #2874 does not reoccur, which
was last encountered in commit 9190831.

Resolves #2874

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: Jacob Salzberg <salzber@amazon.com>
Co-authored-by: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com>
---
 tests/kani/Closure/boxed_closure.rs | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)
 create mode 100644 tests/kani/Closure/boxed_closure.rs

diff --git a/tests/kani/Closure/boxed_closure.rs b/tests/kani/Closure/boxed_closure.rs
new file mode 100644
index 000000000000..4071978d28b1
--- /dev/null
+++ b/tests/kani/Closure/boxed_closure.rs
@@ -0,0 +1,22 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// compile-flags: -Zmir-opt-level=2
+
+// The main function of this test moves an integer into a closure,
+// boxes the value, then passes the closure to a function that calls it.
+// This test covers the issue
+// https://github.com/model-checking/kani/issues/2874 .
+
+fn call_boxed_closure(f: Box<dyn Fn() -> ()>) -> () {
+    f()
+}
+
+// #[kani::proof]
+fn main() {
+    let x = 1;
+    let closure = move || {
+        let _ = x;
+        ()
+    };
+    call_boxed_closure(Box::new(closure));
+}

From dfd05f7d3082526e1d555385b98662b64ccf0930 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Tue, 23 Jul 2024 13:57:44 -0700
Subject: [PATCH 11/20] Fix contract handling of promoted constants and
 constant static (#3305)

When verifying contracts, CBMC initializes all static variables to
non-deterministic values, except for those with constant types or with
types / values annotated with `ID_C_no_nondet_initialization`.

Kani compiler never set these flags, which caused spurious failures when
verification depended on promoted constants or constant static
variables. This fix changes that.

First, I did a bit of refactoring since we may need to set this `Symbol`
property at a later time for static variables.
I also got rid of the initialization function, since the allocation
initialization can be done directly from an expression.

Then, I added the new property to the `Symbol` type. In CBMC, this is a
property of the type or expression. However, I decided to add it to
`Symbol` to avoid having to add this attribute to all variants of `Type`
and `Expr`.

Resolves #3228
---
 cprover_bindings/src/goto_program/symbol.rs   |  26 +++++
 .../src/goto_program/symbol_table.rs          |   5 +
 cprover_bindings/src/irep/to_irep.rs          |   4 +
 .../codegen_cprover_gotoc/codegen/operand.rs  | 105 +++++++++---------
 .../codegen_cprover_gotoc/codegen/rvalue.rs   |   8 +-
 .../codegen/statement.rs                      |   5 +-
 .../codegen/static_var.rs                     |  16 ++-
 .../codegen_cprover_gotoc/context/goto_ctx.rs |  84 ++++++++------
 kani-compiler/src/kani_middle/mod.rs          |  34 +++++-
 .../uninit/access-static-padding.expected     |  12 ++
 .../expected/uninit/access-static-padding.rs  |  34 ++++++
 tests/kani/CodegenStatic/main.rs              |   2 +-
 tests/kani/CodegenStatic/struct.rs            |  20 +++-
 .../fixme_static_interior_mut.rs              |  35 ++++++
 .../FunctionContracts/fixme_static_mut.rs     |  46 ++++++++
 .../FunctionContracts/promoted_constants.rs   |  54 +++++++++
 .../promoted_constants_enum.rs                |  32 ++++++
 .../FunctionContracts/static_interior_mut.rs  |  47 ++++++++
 18 files changed, 461 insertions(+), 108 deletions(-)
 create mode 100644 tests/expected/uninit/access-static-padding.expected
 create mode 100644 tests/expected/uninit/access-static-padding.rs
 create mode 100644 tests/kani/FunctionContracts/fixme_static_interior_mut.rs
 create mode 100644 tests/kani/FunctionContracts/fixme_static_mut.rs
 create mode 100644 tests/kani/FunctionContracts/promoted_constants.rs
 create mode 100644 tests/kani/FunctionContracts/promoted_constants_enum.rs
 create mode 100644 tests/kani/FunctionContracts/static_interior_mut.rs

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:
 /// <https://github.com/diffblue/cbmc/blob/develop/src/util/symbol.h>
+///
+/// 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<T: Into<InternedString>>(&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<T: Into<InternedString>>(&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<String>,
         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<T, F>(
+        &mut self,
+        name: T,
+        is_file_local: bool,
+        is_const: bool,
+        t: Type,
+        loc: Location,
+        init: F,
+    ) -> &mut Symbol
+    where
+        T: Into<InternedString> + 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<Stmt>,
-        T: Into<InternedString>,
-    >(
+    ///
+    /// This will add the symbol to the Symbol Table if not inserted yet.
+    pub fn ensure_global_var<T: Into<InternedString> + 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 <https://doc.rust-lang.org/reference/interior-mutability.html> 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<Self::Break> {
+        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<T>(orig: *const T) -> bool
+where
+    [(); size_of::<T>()]:,
+{
+    let buf = orig as *const [u8; size_of::<T>()];
+    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 N: usize> {
 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<u8>,
+}
+
+/// 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<u32> = 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: <https://github.com/model-checking/kani/issues/3228>
+
+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: <https://github.com/model-checking/kani/issues/3228>
+
+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<u8>,
+}
+
+/// 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.
+}

From 5a5044a3e8744c6a14730b101292c5b2fec10689 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 23 Jul 2024 23:40:46 +0200
Subject: [PATCH 12/20] Bump CBMC Viewer to 3.9 (#3373)

This is in preparation of updating to CBMC 6, which emits some
properties in ways that CBMC Viewer 3.8 did not adequately parse.
---
 kani-dependencies                   | 4 ++--
 scripts/setup/macos/install_deps.sh | 4 ++--
 src/setup.rs                        | 2 +-
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/kani-dependencies b/kani-dependencies
index 200755839284..844d83c23dc7 100644
--- a/kani-dependencies
+++ b/kani-dependencies
@@ -4,7 +4,7 @@ CBMC_VERSION="5.95.1"
 
 # If you update this version number, remember to bump it in `src/setup.rs` too
 CBMC_VIEWER_MAJOR="3"
-CBMC_VIEWER_MINOR="8"
-CBMC_VIEWER_VERSION="3.8"
+CBMC_VIEWER_MINOR="9"
+CBMC_VIEWER_VERSION="3.9"
 
 KISSAT_VERSION="3.1.1"
diff --git a/scripts/setup/macos/install_deps.sh b/scripts/setup/macos/install_deps.sh
index 429eb200541a..179bf8c1237f 100755
--- a/scripts/setup/macos/install_deps.sh
+++ b/scripts/setup/macos/install_deps.sh
@@ -4,10 +4,10 @@
 
 set -eux
 
-# Github promises weekly build image updates, so we can skip the update step and
+# Github promises weekly build image updates, so we could skip the update step and
 # worst case we should only be 1-2 weeks behind upstream brew.
 # https://docs.github.com/en/actions/using-github-hosted-runners/about-github-hosted-runners#supported-software
-#brew update
+brew update
 
 # Install Python separately to workround recurring homebrew CI issue.
 # See https://github.com/actions/runner-images/issues/9471 for more details.
diff --git a/src/setup.rs b/src/setup.rs
index 730679f06c10..58387f7031b7 100644
--- a/src/setup.rs
+++ b/src/setup.rs
@@ -189,7 +189,7 @@ fn setup_python_deps(kani_dir: &Path) -> Result<()> {
     let pyroot = kani_dir.join("pyroot");
 
     // TODO: this is a repetition of versions from kani/kani-dependencies
-    let pkg_versions = &["cbmc-viewer==3.8"];
+    let pkg_versions = &["cbmc-viewer==3.9"];
 
     Command::new("python3")
         .args(["-m", "pip", "install", "--target"])

From 1b1a9b6714038382bc9a592da056dd202e57d8e4 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 24 Jul 2024 17:53:45 +0200
Subject: [PATCH 13/20] Import apply_closure into kani_core (#3375)

This enables use of `|result|` when verifying the standard library.
---
 library/kani_core/src/lib.rs | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs
index 68a8e79658f1..a07ba7ca8ec4 100644
--- a/library/kani_core/src/lib.rs
+++ b/library/kani_core/src/lib.rs
@@ -384,6 +384,13 @@ macro_rules! kani_intrinsics {
             #[doc(hidden)]
             #[rustc_diagnostic_item = "KaniInitContracts"]
             pub fn init_contracts() {}
+
+            /// This should only be used within contracts. The intent is to
+            /// perform type inference on a closure's argument
+            #[doc(hidden)]
+            pub fn apply_closure<T, U: Fn(&T) -> bool>(f: U, x: &T) -> bool {
+                f(x)
+            }
         }
     };
 }

From f37944524306a2708c2f352b76d627d44ec70894 Mon Sep 17 00:00:00 2001
From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com>
Date: Wed, 24 Jul 2024 16:12:30 -0400
Subject: [PATCH 14/20] Bump tests/perf/s2n-quic from `f568f26` to `75afd77`
 (#3378)

---
 tests/perf/s2n-quic | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/perf/s2n-quic b/tests/perf/s2n-quic
index f568f269ee5c..75afd77dfa88 160000
--- a/tests/perf/s2n-quic
+++ b/tests/perf/s2n-quic
@@ -1 +1 @@
-Subproject commit f568f269ee5c9896f4936089c26dfbb3f87f4dab
+Subproject commit 75afd77dfa88d696900f12ee747409ddb208a745

From d66f0c22ea43b3d88b843746f8975372ef22f722 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 24 Jul 2024 22:54:14 +0200
Subject: [PATCH 15/20] compiletest: ensure extra arguments are appended at the
 end (#3379)

We must not mix arguments to be passed to Kani with those parsed by
compiletest. Will enable use of `--cbmc-args` to increase CBMC's
verbosity as needed for certain tests.
---
 tools/compiletest/src/runtest.rs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tools/compiletest/src/runtest.rs b/tools/compiletest/src/runtest.rs
index 7925ed83e6e5..50f1e3035ac8 100644
--- a/tools/compiletest/src/runtest.rs
+++ b/tools/compiletest/src/runtest.rs
@@ -272,14 +272,14 @@ impl<'test> TestCx<'test> {
             .arg("kani")
             .arg("--target-dir")
             .arg(self.output_base_dir().join("target"))
-            .current_dir(parent_dir)
-            .args(&self.config.extra_args);
+            .current_dir(parent_dir);
         if test {
             cargo.arg("--tests");
         }
         if "expected" != self.testpaths.file.file_name().unwrap() {
             cargo.args(["--harness", function_name]);
         }
+        cargo.args(&self.config.extra_args);
 
         let proc_res = self.compose_and_run(cargo);
         self.verify_output(&proc_res, &self.testpaths.file);

From ae3bdb2b1879a7831944e016578fae7ebd72a00f Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 24 Jul 2024 23:28:43 +0200
Subject: [PATCH 16/20] Prepare CBMC v6+ build on Ubuntu 18.04 (#3377)

Use PPA with GCC-9 to build CBMC v6+ on Ubuntu 18.04 (to have full C++17
support) and build static binaries so that they can still be used on
systems that might have libstdc++ from said PPA.
---
 .github/workflows/release.yml        | 6 +++++-
 scripts/setup/ubuntu/install_cbmc.sh | 3 ++-
 2 files changed, 7 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
index 9fb35033d2d1..72ef4e2de889 100644
--- a/.github/workflows/release.yml
+++ b/.github/workflows/release.yml
@@ -104,10 +104,14 @@ jobs:
           apt-get install -y software-properties-common apt-utils
           add-apt-repository ppa:git-core/ppa
           add-apt-repository ppa:deadsnakes/ppa
+          add-apt-repository ppa:ubuntu-toolchain-r/test
           apt-get update
           apt-get install -y \
-            build-essential bash-completion curl lsb-release sudo g++ gcc flex \
+            build-essential bash-completion curl lsb-release sudo g++-9 gcc-9 flex \
             bison make patch git python3.7 python3.7-dev python3.7-distutils
+          update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-9 110 \
+            --slave /usr/bin/g++ g++ /usr/bin/g++-9
+          ln -sf cpp-9 /usr/bin/cpp
           update-alternatives --install /usr/bin/python3 python3 /usr/bin/python3.7 1
           curl -s https://bootstrap.pypa.io/pip/3.7/get-pip.py -o get-pip.py
           python3 get-pip.py --force-reinstall
diff --git a/scripts/setup/ubuntu/install_cbmc.sh b/scripts/setup/ubuntu/install_cbmc.sh
index f37aafcd6327..31015ab9de7a 100755
--- a/scripts/setup/ubuntu/install_cbmc.sh
+++ b/scripts/setup/ubuntu/install_cbmc.sh
@@ -42,7 +42,8 @@ pushd "${WORK_DIR}"
 mkdir build
 git submodule update --init
 
-cmake -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical"
+cmake -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical" \
+  -DBUILD_SHARED_LIBS=OFF -DCMAKE_EXE_LINKER_FLAGS=-static
 make -C build -j$(nproc)
 cpack -G DEB --config build/CPackConfig.cmake
 sudo dpkg -i ./cbmc-*.deb

From abcb54e7d5447e7385371438d546fa26eca9ea2d Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 25 Jul 2024 09:27:10 +0200
Subject: [PATCH 17/20] Maintain test execution performance with newer CaDiCaL
 versions (#3381)

CBMC using CaDiCaL 1.9.2 and later have substantially worse performance
on these tests than CaDiCaL 1.7.2, which CBMC 5.95.1 uses. Using MiniSat
will make sure performance remains consistent.
---
 tests/kani/FloatingPoint/main.rs                              | 1 +
 tests/kani/Intrinsics/Math/Rounding/Ceil/ceilf64.rs           | 2 ++
 tests/kani/Intrinsics/Math/Rounding/Floor/floorf64.rs         | 2 ++
 tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf32.rs | 2 ++
 tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf64.rs | 2 ++
 tests/kani/Intrinsics/Math/Rounding/RInt/rintf32.rs           | 2 ++
 tests/kani/Intrinsics/Math/Rounding/RInt/rintf64.rs           | 2 ++
 tests/kani/Intrinsics/Math/Rounding/Round/roundf32.rs         | 2 ++
 tests/kani/Intrinsics/Math/Rounding/Round/roundf64.rs         | 2 ++
 tests/kani/Intrinsics/Math/Rounding/Trunc/truncf64.rs         | 2 ++
 10 files changed, 19 insertions(+)

diff --git a/tests/kani/FloatingPoint/main.rs b/tests/kani/FloatingPoint/main.rs
index f8ebccdac02a..93a29f169f27 100644
--- a/tests/kani/FloatingPoint/main.rs
+++ b/tests/kani/FloatingPoint/main.rs
@@ -26,6 +26,7 @@ macro_rules! test_floats {
 }
 
 #[kani::proof]
+#[kani::solver(minisat)]
 fn main() {
     assert!(1.1 == 1.1 * 1.0);
     assert!(1.1 != 1.11 / 1.0);
diff --git a/tests/kani/Intrinsics/Math/Rounding/Ceil/ceilf64.rs b/tests/kani/Intrinsics/Math/Rounding/Ceil/ceilf64.rs
index 09c630aa94a7..642d984a7e2b 100644
--- a/tests/kani/Intrinsics/Math/Rounding/Ceil/ceilf64.rs
+++ b/tests/kani/Intrinsics/Math/Rounding/Ceil/ceilf64.rs
@@ -45,6 +45,7 @@ fn test_conc_sci() {
 }
 
 #[kani::proof]
+#[kani::solver(minisat)]
 fn test_towards_inf() {
     let x: f64 = kani::any();
     kani::assume(!x.is_nan());
@@ -53,6 +54,7 @@ fn test_towards_inf() {
 }
 
 #[kani::proof]
+#[kani::solver(minisat)]
 fn test_diff_one() {
     let x: f64 = kani::any();
     kani::assume(!x.is_nan());
diff --git a/tests/kani/Intrinsics/Math/Rounding/Floor/floorf64.rs b/tests/kani/Intrinsics/Math/Rounding/Floor/floorf64.rs
index 0560a2c55064..54ad74c33430 100644
--- a/tests/kani/Intrinsics/Math/Rounding/Floor/floorf64.rs
+++ b/tests/kani/Intrinsics/Math/Rounding/Floor/floorf64.rs
@@ -45,6 +45,7 @@ fn test_conc_sci() {
 }
 
 #[kani::proof]
+#[kani::solver(minisat)]
 fn test_towards_neg_inf() {
     let x: f64 = kani::any();
     kani::assume(!x.is_nan());
@@ -53,6 +54,7 @@ fn test_towards_neg_inf() {
 }
 
 #[kani::proof]
+#[kani::solver(minisat)]
 fn test_diff_one() {
     let x: f64 = kani::any();
     kani::assume(!x.is_nan());
diff --git a/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf32.rs b/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf32.rs
index 25e02f45a943..7ffdb5f28747 100644
--- a/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf32.rs
+++ b/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf32.rs
@@ -50,6 +50,7 @@ fn test_conc_sci() {
 }
 
 #[kani::proof]
+#[kani::solver(minisat)]
 fn test_towards_nearest() {
     let x: f32 = kani::any();
     kani::assume(!x.is_nan());
@@ -88,6 +89,7 @@ fn test_towards_nearest() {
 }
 
 #[kani::proof]
+#[kani::solver(minisat)]
 fn test_diff_half_one() {
     let x: f32 = kani::any();
     kani::assume(!x.is_nan());
diff --git a/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf64.rs b/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf64.rs
index 589a44a4d1ac..bf656512562e 100644
--- a/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf64.rs
+++ b/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf64.rs
@@ -50,6 +50,7 @@ fn test_conc_sci() {
 }
 
 #[kani::proof]
+#[kani::solver(minisat)]
 fn test_towards_nearest() {
     let x: f64 = kani::any();
     kani::assume(!x.is_nan());
@@ -88,6 +89,7 @@ fn test_towards_nearest() {
 }
 
 #[kani::proof]
+#[kani::solver(minisat)]
 fn test_diff_half_one() {
     let x: f64 = kani::any();
     kani::assume(!x.is_nan());
diff --git a/tests/kani/Intrinsics/Math/Rounding/RInt/rintf32.rs b/tests/kani/Intrinsics/Math/Rounding/RInt/rintf32.rs
index 79a0a4f9be2c..53d9d7d5fc73 100644
--- a/tests/kani/Intrinsics/Math/Rounding/RInt/rintf32.rs
+++ b/tests/kani/Intrinsics/Math/Rounding/RInt/rintf32.rs
@@ -55,6 +55,7 @@ fn test_conc_sci() {
 }
 
 #[kani::proof]
+#[kani::solver(minisat)]
 fn test_towards_nearest() {
     let x: f32 = kani::any();
     kani::assume(!x.is_nan());
@@ -93,6 +94,7 @@ fn test_towards_nearest() {
 }
 
 #[kani::proof]
+#[kani::solver(minisat)]
 fn test_diff_half_one() {
     let x: f32 = kani::any();
     kani::assume(!x.is_nan());
diff --git a/tests/kani/Intrinsics/Math/Rounding/RInt/rintf64.rs b/tests/kani/Intrinsics/Math/Rounding/RInt/rintf64.rs
index 8c8ea583a2d5..de608e7cdb9f 100644
--- a/tests/kani/Intrinsics/Math/Rounding/RInt/rintf64.rs
+++ b/tests/kani/Intrinsics/Math/Rounding/RInt/rintf64.rs
@@ -55,6 +55,7 @@ fn test_conc_sci() {
 }
 
 #[kani::proof]
+#[kani::solver(minisat)]
 fn test_towards_nearest() {
     let x: f64 = kani::any();
     kani::assume(!x.is_nan());
@@ -93,6 +94,7 @@ fn test_towards_nearest() {
 }
 
 #[kani::proof]
+#[kani::solver(minisat)]
 fn test_diff_half_one() {
     let x: f64 = kani::any();
     kani::assume(!x.is_nan());
diff --git a/tests/kani/Intrinsics/Math/Rounding/Round/roundf32.rs b/tests/kani/Intrinsics/Math/Rounding/Round/roundf32.rs
index 8a8780878925..04893727dcfa 100644
--- a/tests/kani/Intrinsics/Math/Rounding/Round/roundf32.rs
+++ b/tests/kani/Intrinsics/Math/Rounding/Round/roundf32.rs
@@ -39,6 +39,7 @@ fn test_conc_sci() {
 }
 
 #[kani::proof]
+#[kani::solver(minisat)]
 fn test_towards_closer() {
     let x: f32 = kani::any();
     kani::assume(!x.is_nan());
@@ -61,6 +62,7 @@ fn test_towards_closer() {
 }
 
 #[kani::proof]
+#[kani::solver(minisat)]
 fn test_diff_half_one() {
     let x: f32 = kani::any();
     kani::assume(!x.is_nan());
diff --git a/tests/kani/Intrinsics/Math/Rounding/Round/roundf64.rs b/tests/kani/Intrinsics/Math/Rounding/Round/roundf64.rs
index ddafc45a2e9e..cd61e9607646 100644
--- a/tests/kani/Intrinsics/Math/Rounding/Round/roundf64.rs
+++ b/tests/kani/Intrinsics/Math/Rounding/Round/roundf64.rs
@@ -39,6 +39,7 @@ fn test_conc_sci() {
 }
 
 #[kani::proof]
+#[kani::solver(minisat)]
 fn test_towards_closer() {
     let x: f64 = kani::any();
     kani::assume(!x.is_nan());
@@ -61,6 +62,7 @@ fn test_towards_closer() {
 }
 
 #[kani::proof]
+#[kani::solver(minisat)]
 fn test_diff_half_one() {
     let x: f64 = kani::any();
     kani::assume(!x.is_nan());
diff --git a/tests/kani/Intrinsics/Math/Rounding/Trunc/truncf64.rs b/tests/kani/Intrinsics/Math/Rounding/Trunc/truncf64.rs
index 5fcc8c80606d..a8a80672e36b 100644
--- a/tests/kani/Intrinsics/Math/Rounding/Trunc/truncf64.rs
+++ b/tests/kani/Intrinsics/Math/Rounding/Trunc/truncf64.rs
@@ -38,6 +38,7 @@ fn test_conc_sci() {
 }
 
 #[kani::proof]
+#[kani::solver(minisat)]
 fn test_towards_zero() {
     let x: f64 = kani::any();
     kani::assume(!x.is_nan());
@@ -50,6 +51,7 @@ fn test_towards_zero() {
 }
 
 #[kani::proof]
+#[kani::solver(minisat)]
 fn test_diff_one() {
     let x: f64 = kani::any();
     kani::assume(!x.is_nan());

From 114beea036b95b82ee7a5ca051b078aa3408919e Mon Sep 17 00:00:00 2001
From: Artem Agvanian <nartagva@amazon.com>
Date: Thu, 25 Jul 2024 10:14:25 -0700
Subject: [PATCH 18/20] Better explanations and extra functionality in
 `MutableBody` (#3382)

`MutableBody` is the core data structure for MIR manipulation in
instrumentation passes. However, its public methods have limited
documentation and unclear semantics. This slowed down the development of
instrumentation passes.

This PR aims to fix that by:
- Clarifying how source instruction shifts when the methods are called;
- Adding functionality for inserting basic blocks;
- Expanding the support for different terminator types.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
---
 .../src/kani_middle/transform/body.rs         | 159 ++++++++++++------
 .../kani_middle/transform/check_uninit/mod.rs |  18 +-
 .../transform/check_uninit/uninit_visitor.rs  |   2 +-
 .../src/kani_middle/transform/check_values.rs |  44 ++---
 .../kani_middle/transform/kani_intrinsics.rs  |  16 +-
 5 files changed, 146 insertions(+), 93 deletions(-)

diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs
index d82dda80cc05..d3f2afc15d31 100644
--- a/kani-compiler/src/kani_middle/transform/body.rs
+++ b/kani-compiler/src/kani_middle/transform/body.rs
@@ -88,16 +88,20 @@ impl MutableBody {
 
     pub fn new_str_operand(&mut self, msg: &str, span: Span) -> Operand {
         let literal = MirConst::from_str(msg);
-        Operand::Constant(ConstOperand { span, user_ty: None, const_: literal })
+        self.new_const_operand(literal, span)
     }
 
-    pub fn new_const_operand(&mut self, val: u128, uint_ty: UintTy, span: Span) -> Operand {
+    pub fn new_uint_operand(&mut self, val: u128, uint_ty: UintTy, span: Span) -> Operand {
         let literal = MirConst::try_from_uint(val, uint_ty).unwrap();
+        self.new_const_operand(literal, span)
+    }
+
+    fn new_const_operand(&mut self, literal: MirConst, span: Span) -> Operand {
         Operand::Constant(ConstOperand { span, user_ty: None, const_: literal })
     }
 
     /// Create a raw pointer of `*mut type` and return a new local where that value is stored.
-    pub fn new_cast_ptr(
+    pub fn insert_ptr_cast(
         &mut self,
         from: Operand,
         pointee_ty: Ty,
@@ -108,13 +112,13 @@ impl MutableBody {
         assert!(from.ty(self.locals()).unwrap().kind().is_raw_ptr());
         let target_ty = Ty::new_ptr(pointee_ty, mutability);
         let rvalue = Rvalue::Cast(CastKind::PtrToPtr, from, target_ty);
-        self.new_assignment(rvalue, source, position)
+        self.insert_assignment(rvalue, source, position)
     }
 
     /// Add a new assignment for the given binary operation.
     ///
     /// Return the local where the result is saved.
-    pub fn new_binary_op(
+    pub fn insert_binary_op(
         &mut self,
         bin_op: BinOp,
         lhs: Operand,
@@ -123,13 +127,13 @@ impl MutableBody {
         position: InsertPosition,
     ) -> Local {
         let rvalue = Rvalue::BinaryOp(bin_op, lhs, rhs);
-        self.new_assignment(rvalue, source, position)
+        self.insert_assignment(rvalue, source, position)
     }
 
     /// Add a new assignment.
     ///
-    /// Return  local where the result is saved.
-    pub fn new_assignment(
+    /// Return the local where the result is saved.
+    pub fn insert_assignment(
         &mut self,
         rvalue: Rvalue,
         source: &mut SourceInstruction,
@@ -146,9 +150,10 @@ impl MutableBody {
     /// Add a new assert to the basic block indicated by the given index.
     ///
     /// The new assertion will have the same span as the source instruction, and the basic block
-    /// will be split. The source instruction will be adjusted to point to the first instruction in
-    /// the new basic block.
-    pub fn add_check(
+    /// will be split. If `InsertPosition` is `InsertPosition::Before`, `source` will point to the
+    /// same instruction as before. If `InsertPosition` is `InsertPosition::After`, `source` will
+    /// point to the new terminator.
+    pub fn insert_check(
         &mut self,
         tcx: TyCtxt,
         check_type: &CheckType,
@@ -183,7 +188,7 @@ impl MutableBody {
                     unwind: UnwindAction::Terminate,
                 };
                 let terminator = Terminator { kind, span };
-                self.split_bb(source, position, terminator);
+                self.insert_terminator(source, position, terminator);
             }
             CheckType::Panic | CheckType::NoCore => {
                 tcx.sess
@@ -199,10 +204,11 @@ impl MutableBody {
 
     /// Add a new call to the basic block indicated by the given index.
     ///
-    /// The new call will have the same span as the source instruction, and the basic block
-    /// will be split. The source instruction will be adjusted to point to the first instruction in
-    /// the new basic block.
-    pub fn add_call(
+    /// The new call will have the same span as the source instruction, and the basic block will be
+    /// split. If `InsertPosition` is `InsertPosition::Before`, `source` will point to the same
+    /// instruction as before. If `InsertPosition` is `InsertPosition::After`, `source` will point
+    /// to the new terminator.
+    pub fn insert_call(
         &mut self,
         callee: &Instance,
         source: &mut SourceInstruction,
@@ -222,13 +228,14 @@ impl MutableBody {
             unwind: UnwindAction::Terminate,
         };
         let terminator = Terminator { kind, span };
-        self.split_bb(source, position, terminator);
+        self.insert_terminator(source, position, terminator);
     }
 
-    /// Split a basic block and use the new terminator in the basic block that was split.
-    ///
-    /// The source is updated to point to the same instruction which is now in the new basic block.
-    pub fn split_bb(
+    /// Split a basic block and use the new terminator in the basic block that was split. If
+    /// `InsertPosition` is `InsertPosition::Before`, `source` will point to the same instruction as
+    /// before. If `InsertPosition` is `InsertPosition::After`, `source` will point to the new
+    /// terminator.
+    fn split_bb(
         &mut self,
         source: &mut SourceInstruction,
         position: InsertPosition,
@@ -245,6 +252,7 @@ impl MutableBody {
     }
 
     /// Split a basic block right before the source location.
+    /// `source` will point to the same instruction as before after the function is done.
     fn split_bb_before(&mut self, source: &mut SourceInstruction, new_term: Terminator) {
         let new_bb_idx = self.blocks.len();
         let (idx, bb) = match source {
@@ -268,6 +276,7 @@ impl MutableBody {
     }
 
     /// Split a basic block right after the source location.
+    /// `source` will point to the new terminator after the function is done.
     fn split_bb_after(&mut self, source: &mut SourceInstruction, mut new_term: Terminator) {
         let new_bb_idx = self.blocks.len();
         match source {
@@ -275,39 +284,69 @@ impl MutableBody {
             // and move the remaining statements into the new one.
             SourceInstruction::Statement { idx, bb } => {
                 let (orig_idx, orig_bb) = (*idx, *bb);
-                *idx = 0;
-                *bb = new_bb_idx;
                 let old_term = mem::replace(&mut self.blocks[orig_bb].terminator, new_term);
                 let bb_stmts = &mut self.blocks[orig_bb].statements;
                 let remaining = bb_stmts.split_off(orig_idx + 1);
                 let new_bb = BasicBlock { statements: remaining, terminator: old_term };
                 self.blocks.push(new_bb);
+                // Update the source to point at the terminator.
+                *source = SourceInstruction::Terminator { bb: orig_bb };
             }
             // Make the terminator at `source` point at the new block,
             // the terminator of which is a simple Goto instruction.
             SourceInstruction::Terminator { bb } => {
-                let current_terminator = &mut self.blocks.get_mut(*bb).unwrap().terminator;
-                // Kani can only instrument function calls like this.
-                match (&mut current_terminator.kind, &mut new_term.kind) {
-                    (
-                        TerminatorKind::Call { target: Some(target_bb), .. },
-                        TerminatorKind::Call { target: Some(new_target_bb), .. },
-                    ) => {
-                        // Set the new terminator to point where previous terminator pointed.
-                        *new_target_bb = *target_bb;
-                        // Point the current terminator to the new terminator's basic block.
-                        *target_bb = new_bb_idx;
-                        // Update the current poisition.
-                        *bb = new_bb_idx;
-                        self.blocks.push(BasicBlock { statements: vec![], terminator: new_term });
-                    }
-                    _ => unimplemented!("Kani can only split blocks after calls."),
-                };
+                let current_term = &mut self.blocks.get_mut(*bb).unwrap().terminator;
+                let target_bb = get_mut_target_ref(current_term);
+                let new_target_bb = get_mut_target_ref(&mut new_term);
+                // Set the new terminator to point where previous terminator pointed.
+                *new_target_bb = *target_bb;
+                // Point the current terminator to the new terminator's basic block.
+                *target_bb = new_bb_idx;
+                // Update the source to point at the terminator.
+                *bb = new_bb_idx;
+                self.blocks.push(BasicBlock { statements: vec![], terminator: new_term });
             }
         };
     }
 
-    /// Insert statement before or after the source instruction and update the source as needed.
+    /// Insert basic block before or after the source instruction and update `source` accordingly. If
+    /// `InsertPosition` is `InsertPosition::Before`, `source` will point to the same instruction as
+    /// before. If `InsertPosition` is `InsertPosition::After`, `source` will point to the
+    /// terminator of the newly inserted basic block.
+    pub fn insert_bb(
+        &mut self,
+        mut bb: BasicBlock,
+        source: &mut SourceInstruction,
+        position: InsertPosition,
+    ) {
+        // Splitting adds 1 block, so the added block index is len + 1;
+        let split_bb_idx = self.blocks().len();
+        let inserted_bb_idx = self.blocks().len() + 1;
+        // Update the terminator of the basic block to point at the remaining part of the split
+        // basic block.
+        let target = get_mut_target_ref(&mut bb.terminator);
+        *target = split_bb_idx;
+        let new_term = Terminator {
+            kind: TerminatorKind::Goto { target: inserted_bb_idx },
+            span: source.span(&self.blocks),
+        };
+        self.split_bb(source, position, new_term);
+        self.blocks.push(bb);
+    }
+
+    pub fn insert_terminator(
+        &mut self,
+        source: &mut SourceInstruction,
+        position: InsertPosition,
+        terminator: Terminator,
+    ) {
+        self.split_bb(source, position, terminator);
+    }
+
+    /// Insert statement before or after the source instruction and update the source as needed. If
+    /// `InsertPosition` is `InsertPosition::Before`, `source` will point to the same instruction as
+    /// before. If `InsertPosition` is `InsertPosition::After`, `source` will point to the
+    /// newly inserted statement.
     pub fn insert_stmt(
         &mut self,
         new_stmt: Statement,
@@ -338,22 +377,18 @@ impl MutableBody {
                     SourceInstruction::Terminator { bb } => {
                         // Create a new basic block, as we need to append a statement after the terminator.
                         let current_terminator = &mut self.blocks.get_mut(*bb).unwrap().terminator;
-                        // Kani can only instrument function calls in this way.
-                        match &mut current_terminator.kind {
-                            TerminatorKind::Call { target: Some(target_bb), .. } => {
-                                *source = SourceInstruction::Statement { idx: 0, bb: new_bb_idx };
-                                let new_bb = BasicBlock {
-                                    statements: vec![new_stmt],
-                                    terminator: Terminator {
-                                        kind: TerminatorKind::Goto { target: *target_bb },
-                                        span,
-                                    },
-                                };
-                                *target_bb = new_bb_idx;
-                                self.blocks.push(new_bb);
-                            }
-                            _ => unimplemented!("Kani can only insert statements after calls."),
+                        // Update target of the terminator.
+                        let target_bb = get_mut_target_ref(current_terminator);
+                        *source = SourceInstruction::Statement { idx: 0, bb: new_bb_idx };
+                        let new_bb = BasicBlock {
+                            statements: vec![new_stmt],
+                            terminator: Terminator {
+                                kind: TerminatorKind::Goto { target: *target_bb },
+                                span,
+                            },
                         };
+                        *target_bb = new_bb_idx;
+                        self.blocks.push(new_bb);
                     }
                 }
             }
@@ -574,3 +609,15 @@ pub trait MutMirVisitor {
         }
     }
 }
+
+fn get_mut_target_ref(terminator: &mut Terminator) -> &mut BasicBlockIdx {
+    match &mut terminator.kind {
+        TerminatorKind::Assert { target, .. }
+        | TerminatorKind::Drop { target, .. }
+        | TerminatorKind::Goto { target }
+        | TerminatorKind::Call { target: Some(target), .. } => target,
+        _ => unimplemented!(
+            "Kani can only insert instructions after terminators that have a `target` field."
+        ),
+    }
+}
diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs
index 4f94f94d17f1..f46c143f16d1 100644
--- a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs
+++ b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs
@@ -230,7 +230,7 @@ impl UninitPass {
                     *pointee_info.ty(),
                 );
                 collect_skipped(&operation, body, skip_first);
-                body.add_call(
+                body.insert_call(
                     &is_ptr_initialized_instance,
                     source,
                     operation.position(),
@@ -257,7 +257,7 @@ impl UninitPass {
                 let layout_operand =
                     mk_layout_operand(body, source, operation.position(), &element_layout);
                 collect_skipped(&operation, body, skip_first);
-                body.add_call(
+                body.insert_call(
                     &is_ptr_initialized_instance,
                     source,
                     operation.position(),
@@ -276,7 +276,7 @@ impl UninitPass {
         // Make sure all non-padding bytes are initialized.
         collect_skipped(&operation, body, skip_first);
         let ptr_operand_ty = ptr_operand.ty(body.locals()).unwrap();
-        body.add_check(
+        body.insert_check(
             tcx,
             &self.check_type,
             source,
@@ -345,7 +345,7 @@ impl UninitPass {
                     *pointee_info.ty(),
                 );
                 collect_skipped(&operation, body, skip_first);
-                body.add_call(
+                body.insert_call(
                     &set_ptr_initialized_instance,
                     source,
                     operation.position(),
@@ -372,7 +372,7 @@ impl UninitPass {
                 let layout_operand =
                     mk_layout_operand(body, source, operation.position(), &element_layout);
                 collect_skipped(&operation, body, skip_first);
-                body.add_call(
+                body.insert_call(
                     &set_ptr_initialized_instance,
                     source,
                     operation.position(),
@@ -408,8 +408,8 @@ impl UninitPass {
             span,
             user_ty: None,
         }));
-        let result = body.new_assignment(rvalue, source, position);
-        body.add_check(tcx, &self.check_type, source, position, result, reason);
+        let result = body.insert_assignment(rvalue, source, position);
+        body.insert_check(tcx, &self.check_type, source, position, result, reason);
     }
 }
 
@@ -432,7 +432,7 @@ pub fn mk_layout_operand(
     layout_byte_mask: &[bool],
 ) -> Operand {
     Operand::Move(Place {
-        local: body.new_assignment(
+        local: body.insert_assignment(
             Rvalue::Aggregate(
                 AggregateKind::Array(Ty::bool_ty()),
                 layout_byte_mask
@@ -531,7 +531,7 @@ fn inject_memory_init_setup(
     )
     .unwrap();
 
-    new_body.add_call(
+    new_body.insert_call(
         &memory_initialization_init,
         &mut source,
         InsertPosition::Before,
diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs
index 4c768aa2ee81..10a93b727a77 100644
--- a/kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs
+++ b/kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs
@@ -57,7 +57,7 @@ impl MemoryInitOp {
                         Operand::Copy(place) | Operand::Move(place) => place,
                         Operand::Constant(_) => unreachable!(),
                     };
-                    body.new_assignment(
+                    body.insert_assignment(
                         Rvalue::AddressOf(Mutability::Not, place.clone()),
                         source,
                         self.position(),
diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs
index a7d0f14d270f..a81f76d25393 100644
--- a/kani-compiler/src/kani_middle/transform/check_values.rs
+++ b/kani-compiler/src/kani_middle/transform/check_values.rs
@@ -85,13 +85,13 @@ impl ValidValuePass {
         for operation in instruction.operations {
             match operation {
                 SourceOp::BytesValidity { ranges, target_ty, rvalue } => {
-                    let value = body.new_assignment(rvalue, &mut source, InsertPosition::Before);
+                    let value = body.insert_assignment(rvalue, &mut source, InsertPosition::Before);
                     let rvalue_ptr = Rvalue::AddressOf(Mutability::Not, Place::from(value));
                     for range in ranges {
                         let result = build_limits(body, &range, rvalue_ptr.clone(), &mut source);
                         let msg =
                             format!("Undefined Behavior: Invalid value of type `{target_ty}`",);
-                        body.add_check(
+                        body.insert_check(
                             tcx,
                             &self.check_type,
                             &mut source,
@@ -106,7 +106,7 @@ impl ValidValuePass {
                         let result = build_limits(body, &range, rvalue.clone(), &mut source);
                         let msg =
                             format!("Undefined Behavior: Invalid value of type `{pointee_ty}`",);
-                        body.add_check(
+                        body.insert_check(
                             tcx,
                             &self.check_type,
                             &mut source,
@@ -139,8 +139,8 @@ impl ValidValuePass {
             span,
             user_ty: None,
         }));
-        let result = body.new_assignment(rvalue, source, InsertPosition::Before);
-        body.add_check(tcx, &self.check_type, source, InsertPosition::Before, result, reason);
+        let result = body.insert_assignment(rvalue, source, InsertPosition::Before);
+        body.insert_check(tcx, &self.check_type, source, InsertPosition::Before, result, reason);
     }
 }
 
@@ -771,24 +771,25 @@ pub fn build_limits(
     let span = source.span(body.blocks());
     debug!(?req, ?rvalue_ptr, ?span, "build_limits");
     let primitive_ty = uint_ty(req.size.bytes());
-    let start_const = body.new_const_operand(req.valid_range.start, primitive_ty, span);
-    let end_const = body.new_const_operand(req.valid_range.end, primitive_ty, span);
+    let start_const = body.new_uint_operand(req.valid_range.start, primitive_ty, span);
+    let end_const = body.new_uint_operand(req.valid_range.end, primitive_ty, span);
     let orig_ptr = if req.offset != 0 {
-        let start_ptr = move_local(body.new_assignment(rvalue_ptr, source, InsertPosition::Before));
-        let byte_ptr = move_local(body.new_cast_ptr(
+        let start_ptr =
+            move_local(body.insert_assignment(rvalue_ptr, source, InsertPosition::Before));
+        let byte_ptr = move_local(body.insert_ptr_cast(
             start_ptr,
             Ty::unsigned_ty(UintTy::U8),
             Mutability::Not,
             source,
             InsertPosition::Before,
         ));
-        let offset_const = body.new_const_operand(req.offset as _, UintTy::Usize, span);
-        let offset = move_local(body.new_assignment(
+        let offset_const = body.new_uint_operand(req.offset as _, UintTy::Usize, span);
+        let offset = move_local(body.insert_assignment(
             Rvalue::Use(offset_const),
             source,
             InsertPosition::Before,
         ));
-        move_local(body.new_binary_op(
+        move_local(body.insert_binary_op(
             BinOp::Offset,
             byte_ptr,
             offset,
@@ -796,9 +797,9 @@ pub fn build_limits(
             InsertPosition::Before,
         ))
     } else {
-        move_local(body.new_assignment(rvalue_ptr, source, InsertPosition::Before))
+        move_local(body.insert_assignment(rvalue_ptr, source, InsertPosition::Before))
     };
-    let value_ptr = body.new_cast_ptr(
+    let value_ptr = body.insert_ptr_cast(
         orig_ptr,
         Ty::unsigned_ty(primitive_ty),
         Mutability::Not,
@@ -806,13 +807,18 @@ pub fn build_limits(
         InsertPosition::Before,
     );
     let value = Operand::Copy(Place { local: value_ptr, projection: vec![ProjectionElem::Deref] });
-    let start_result =
-        body.new_binary_op(BinOp::Ge, value.clone(), start_const, source, InsertPosition::Before);
+    let start_result = body.insert_binary_op(
+        BinOp::Ge,
+        value.clone(),
+        start_const,
+        source,
+        InsertPosition::Before,
+    );
     let end_result =
-        body.new_binary_op(BinOp::Le, value, end_const, source, InsertPosition::Before);
+        body.insert_binary_op(BinOp::Le, value, end_const, source, InsertPosition::Before);
     if req.valid_range.wraps_around() {
         // valid >= start || valid <= end
-        body.new_binary_op(
+        body.insert_binary_op(
             BinOp::BitOr,
             move_local(start_result),
             move_local(end_result),
@@ -821,7 +827,7 @@ pub fn build_limits(
         )
     } else {
         // valid >= start && valid <= end
-        body.new_binary_op(
+        body.insert_binary_op(
             BinOp::BitAnd,
             move_local(start_result),
             move_local(end_result),
diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs
index c4534bf11b4d..d6475465d1b1 100644
--- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs
+++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs
@@ -136,11 +136,11 @@ impl IntrinsicGeneratorPass {
                     user_ty: None,
                 }));
                 let result =
-                    new_body.new_assignment(rvalue, &mut terminator, InsertPosition::Before);
+                    new_body.insert_assignment(rvalue, &mut terminator, InsertPosition::Before);
                 let reason = format!(
                     "Kani currently doesn't support checking validity of `{target_ty}`. {msg}"
                 );
-                new_body.add_check(
+                new_body.insert_check(
                     tcx,
                     &self.check_type,
                     &mut terminator,
@@ -212,7 +212,7 @@ impl IntrinsicGeneratorPass {
                             InsertPosition::Before,
                             &layout,
                         );
-                        new_body.add_call(
+                        new_body.insert_call(
                             &is_ptr_initialized_instance,
                             &mut terminator,
                             InsertPosition::Before,
@@ -242,7 +242,7 @@ impl IntrinsicGeneratorPass {
                             InsertPosition::Before,
                             &element_layout,
                         );
-                        new_body.add_call(
+                        new_body.insert_call(
                             &is_ptr_initialized_instance,
                             &mut terminator,
                             InsertPosition::Before,
@@ -256,14 +256,14 @@ impl IntrinsicGeneratorPass {
                             span,
                             user_ty: None,
                         }));
-                        let result = new_body.new_assignment(
+                        let result = new_body.insert_assignment(
                             rvalue,
                             &mut terminator,
                             InsertPosition::Before,
                         );
                         let reason: &str = "Kani does not support reasoning about memory initialization of pointers to trait objects.";
 
-                        new_body.add_check(
+                        new_body.insert_check(
                             tcx,
                             &self.check_type,
                             &mut terminator,
@@ -282,11 +282,11 @@ impl IntrinsicGeneratorPass {
                     user_ty: None,
                 }));
                 let result =
-                    new_body.new_assignment(rvalue, &mut terminator, InsertPosition::Before);
+                    new_body.insert_assignment(rvalue, &mut terminator, InsertPosition::Before);
                 let reason = format!(
                     "Kani currently doesn't support checking memory initialization of `{target_ty}`. {msg}"
                 );
-                new_body.add_check(
+                new_body.insert_check(
                     tcx,
                     &self.check_type,
                     &mut terminator,

From b18698f0e01b9d7d678a0ced8c2553a8d56e7767 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Thu, 25 Jul 2024 10:58:31 -0700
Subject: [PATCH 19/20] Add missing functionalities to kani_core (#3384)

  - Add Arbitrary for array
  - Add Arbitrary for tuples
  - Add missing changes from modifies slices (#3295)

Note that for adding `any_array` I had to cleanup the unnecessary usage
of constant parameters from `kani::any_raw`.
---
 library/kani/src/arbitrary.rs                 | 24 +----
 library/kani/src/concrete_playback.rs         | 12 +--
 library/kani/src/lib.rs                       | 17 ++--
 library/kani/src/vec.rs                       |  2 -
 library/kani_core/src/arbitrary.rs            | 70 ++++++++------
 library/kani_core/src/lib.rs                  | 93 +++++++++++++------
 .../verify_std_cmd/verify_core.rs             | 75 +++++++++++++++
 .../verify_std_cmd/verify_std.expected        |  8 +-
 .../verify_std_cmd/verify_std.sh              | 42 +--------
 9 files changed, 209 insertions(+), 134 deletions(-)
 create mode 100644 tests/script-based-pre/verify_std_cmd/verify_core.rs

diff --git a/library/kani/src/arbitrary.rs b/library/kani/src/arbitrary.rs
index 424ca2485d57..ef6e2ef23dd4 100644
--- a/library/kani/src/arbitrary.rs
+++ b/library/kani/src/arbitrary.rs
@@ -16,12 +16,7 @@ where
     Self: Sized,
 {
     fn any() -> Self;
-    fn any_array<const MAX_ARRAY_LENGTH: usize>() -> [Self; MAX_ARRAY_LENGTH]
-    // the requirement defined in the where clause must appear on the `impl`'s method `any_array`
-    // but also on the corresponding trait's method
-    where
-        [(); std::mem::size_of::<[Self; MAX_ARRAY_LENGTH]>()]:,
-    {
+    fn any_array<const MAX_ARRAY_LENGTH: usize>() -> [Self; MAX_ARRAY_LENGTH] {
         [(); MAX_ARRAY_LENGTH].map(|_| Self::any())
     }
 }
@@ -33,20 +28,10 @@ macro_rules! trivial_arbitrary {
             #[inline(always)]
             fn any() -> Self {
                 // This size_of call does not use generic_const_exprs feature. It's inside a macro, and Self isn't generic.
-                unsafe { crate::any_raw_internal::<Self, { std::mem::size_of::<Self>() }>() }
+                unsafe { crate::any_raw_internal::<Self>() }
             }
-            fn any_array<const MAX_ARRAY_LENGTH: usize>() -> [Self; MAX_ARRAY_LENGTH]
-            where
-                // `generic_const_exprs` requires all potential errors to be reflected in the signature/header.
-                // We must repeat the expression in the header, to make sure that if the body can fail the header will also fail.
-                [(); { std::mem::size_of::<[$type; MAX_ARRAY_LENGTH]>() }]:,
-            {
-                unsafe {
-                    crate::any_raw_internal::<
-                        [Self; MAX_ARRAY_LENGTH],
-                        { std::mem::size_of::<[Self; MAX_ARRAY_LENGTH]>() },
-                    >()
-                }
+            fn any_array<const MAX_ARRAY_LENGTH: usize>() -> [Self; MAX_ARRAY_LENGTH] {
+                unsafe { crate::any_raw_internal::<[Self; MAX_ARRAY_LENGTH]>() }
             }
         }
     };
@@ -128,7 +113,6 @@ nonzero_arbitrary!(NonZeroIsize, isize);
 impl<T, const N: usize> Arbitrary for [T; N]
 where
     T: Arbitrary,
-    [(); std::mem::size_of::<[T; N]>()]:,
 {
     fn any() -> Self {
         T::any_array()
diff --git a/library/kani/src/concrete_playback.rs b/library/kani/src/concrete_playback.rs
index 711b9b005624..aa6cd7e4018d 100644
--- a/library/kani/src/concrete_playback.rs
+++ b/library/kani/src/concrete_playback.rs
@@ -47,19 +47,17 @@ pub fn concrete_playback_run<F: Fn()>(mut local_concrete_vals: Vec<Vec<u8>>, pro
 /// # Safety
 ///
 /// The semantics of this function require that SIZE_T equals the size of type T.
-pub(crate) unsafe fn any_raw_internal<T, const SIZE_T: usize>() -> T {
+pub(crate) unsafe fn any_raw_internal<T: Copy>() -> T {
+    let sz = size_of::<T>();
     let mut next_concrete_val: Vec<u8> = Vec::new();
     CONCRETE_VALS.with(|glob_concrete_vals| {
         let mut_ref_glob_concrete_vals = &mut *glob_concrete_vals.borrow_mut();
-        next_concrete_val = if SIZE_T > 0 {
+        next_concrete_val = if sz > 0 {
             mut_ref_glob_concrete_vals.pop().expect("Not enough det vals found")
         } else {
             vec![]
         };
     });
-    let next_concrete_val_len = next_concrete_val.len();
-    let bytes_t: [u8; SIZE_T] = next_concrete_val.try_into().expect(&format!(
-        "Expected {SIZE_T} bytes instead of {next_concrete_val_len} bytes in the following det vals vec"
-    ));
-    std::mem::transmute_copy::<[u8; SIZE_T], T>(&bytes_t)
+    assert_eq!(next_concrete_val.len(), sz, "Expected {sz} bytes in the following det vals vec");
+    unsafe { *(next_concrete_val.as_ptr() as *mut T) }
 }
diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs
index 7487cc26b186..3cf46bd7af07 100644
--- a/library/kani/src/lib.rs
+++ b/library/kani/src/lib.rs
@@ -7,11 +7,10 @@
 // Used for rustc_diagnostic_item.
 // Note: We could use a kanitool attribute instead.
 #![feature(rustc_attrs)]
-// This is required for the optimized version of `any_array()`
-#![feature(generic_const_exprs)]
-#![allow(incomplete_features)]
 // Used to model simd.
 #![feature(repr_simd)]
+#![feature(generic_const_exprs)]
+#![allow(incomplete_features)]
 // Features used for tests only.
 #![cfg_attr(test, feature(core_intrinsics, portable_simd))]
 // Required for `rustc_diagnostic_item` and `core_intrinsics`
@@ -21,6 +20,9 @@
 #![feature(f16)]
 #![feature(f128)]
 
+// Allow us to use `kani::` to access crate features.
+extern crate self as kani;
+
 pub mod arbitrary;
 #[cfg(feature = "concrete_playback")]
 mod concrete_playback;
@@ -48,6 +50,7 @@ pub use invariant::Invariant;
 pub fn concrete_playback_run<F: Fn()>(_: Vec<Vec<u8>>, _: F) {
     unreachable!("Concrete playback does not work during verification")
 }
+
 pub use futures::{block_on, block_on_with_spawn, spawn, yield_now, RoundRobin};
 
 /// Creates an assumption that will be valid after this statement run. Note that the assumption
@@ -246,21 +249,21 @@ pub fn any_where<T: Arbitrary, F: FnOnce(&T) -> bool>(f: F) -> T {
 /// Note that SIZE_T must be equal the size of type T in bytes.
 #[inline(never)]
 #[cfg(not(feature = "concrete_playback"))]
-pub(crate) unsafe fn any_raw_internal<T, const SIZE_T: usize>() -> T {
+pub(crate) unsafe fn any_raw_internal<T: Copy>() -> T {
     any_raw_inner::<T>()
 }
 
 #[inline(never)]
 #[cfg(feature = "concrete_playback")]
-pub(crate) unsafe fn any_raw_internal<T, const SIZE_T: usize>() -> T {
-    concrete_playback::any_raw_internal::<T, SIZE_T>()
+pub(crate) unsafe fn any_raw_internal<T: Copy>() -> T {
+    concrete_playback::any_raw_internal::<T>()
 }
 
 /// This low-level function returns nondet bytes of size T.
 #[rustc_diagnostic_item = "KaniAnyRaw"]
 #[inline(never)]
 #[allow(dead_code)]
-fn any_raw_inner<T>() -> T {
+fn any_raw_inner<T: Copy>() -> T {
     kani_intrinsic()
 }
 
diff --git a/library/kani/src/vec.rs b/library/kani/src/vec.rs
index 626d152f02d4..a3ec05a9c953 100644
--- a/library/kani/src/vec.rs
+++ b/library/kani/src/vec.rs
@@ -6,7 +6,6 @@ use crate::{any, any_where, Arbitrary};
 pub fn any_vec<T, const MAX_LENGTH: usize>() -> Vec<T>
 where
     T: Arbitrary,
-    [(); std::mem::size_of::<[T; MAX_LENGTH]>()]:,
 {
     let real_length: usize = any_where(|sz| *sz <= MAX_LENGTH);
     match real_length {
@@ -26,7 +25,6 @@ where
 pub fn exact_vec<T, const EXACT_LENGTH: usize>() -> Vec<T>
 where
     T: Arbitrary,
-    [(); std::mem::size_of::<[T; EXACT_LENGTH]>()]:,
 {
     let boxed_array: Box<[T; EXACT_LENGTH]> = Box::new(any());
     <[T]>::into_vec(boxed_array)
diff --git a/library/kani_core/src/arbitrary.rs b/library/kani_core/src/arbitrary.rs
index a8271ad758cf..7cfb649b11a0 100644
--- a/library/kani_core/src/arbitrary.rs
+++ b/library/kani_core/src/arbitrary.rs
@@ -8,6 +8,7 @@
 //!
 //! TODO: Use this inside kani library so that we dont have to maintain two copies of the same proc macro for arbitrary.
 #[macro_export]
+#[allow(clippy::crate_in_macro_def)]
 macro_rules! generate_arbitrary {
     ($core:path) => {
         use core_path::marker::{PhantomData, PhantomPinned};
@@ -18,13 +19,7 @@ macro_rules! generate_arbitrary {
             Self: Sized,
         {
             fn any() -> Self;
-            #[cfg(kani_sysroot)]
-            fn any_array<const MAX_ARRAY_LENGTH: usize>() -> [Self; MAX_ARRAY_LENGTH]
-            // the requirement defined in the where clause must appear on the `impl`'s method `any_array`
-            // but also on the corresponding trait's method
-            where
-                [(); core_path::mem::size_of::<[Self; MAX_ARRAY_LENGTH]>()]:,
-            {
+            fn any_array<const MAX_ARRAY_LENGTH: usize>() -> [Self; MAX_ARRAY_LENGTH] {
                 [(); MAX_ARRAY_LENGTH].map(|_| Self::any())
             }
         }
@@ -36,22 +31,10 @@ macro_rules! generate_arbitrary {
                     #[inline(always)]
                     fn any() -> Self {
                         // This size_of call does not use generic_const_exprs feature. It's inside a macro, and Self isn't generic.
-                        unsafe { any_raw_internal::<Self, { core_path::mem::size_of::<Self>() }>() }
+                        unsafe { crate::kani::any_raw_internal::<Self>() }
                     }
-                    // Disable this for standard library since we cannot enable generic constant expr.
-                    #[cfg(kani_sysroot)]
-                    fn any_array<const MAX_ARRAY_LENGTH: usize>() -> [Self; MAX_ARRAY_LENGTH]
-                    where
-                        // `generic_const_exprs` requires all potential errors to be reflected in the signature/header.
-                        // We must repeat the expression in the header, to make sure that if the body can fail the header will also fail.
-                        [(); { core_path::mem::size_of::<[$type; MAX_ARRAY_LENGTH]>() }]:,
-                    {
-                        unsafe {
-                            any_raw_internal::<
-                                [Self; MAX_ARRAY_LENGTH],
-                                { core_path::mem::size_of::<[Self; MAX_ARRAY_LENGTH]>() },
-                            >()
-                        }
+                    fn any_array<const MAX_ARRAY_LENGTH: usize>() -> [Self; MAX_ARRAY_LENGTH] {
+                        unsafe { crate::kani::any_raw_internal::<[Self; MAX_ARRAY_LENGTH]>() }
                     }
                 }
             };
@@ -134,6 +117,15 @@ macro_rules! generate_arbitrary {
             }
         }
 
+        impl<T, const N: usize> Arbitrary for [T; N]
+        where
+            T: Arbitrary,
+        {
+            fn any() -> Self {
+                T::any_array::<N>()
+            }
+        }
+
         impl<T> Arbitrary for Option<T>
         where
             T: Arbitrary,
@@ -165,15 +157,33 @@ macro_rules! generate_arbitrary {
             }
         }
 
-        #[cfg(kani_sysroot)]
-        impl<T, const N: usize> Arbitrary for [T; N]
-        where
-            T: Arbitrary,
-            [(); core_path::mem::size_of::<[T; N]>()]:,
-        {
+        arbitrary_tuple!(A);
+        arbitrary_tuple!(A, B);
+        arbitrary_tuple!(A, B, C);
+        arbitrary_tuple!(A, B, C, D);
+        arbitrary_tuple!(A, B, C, D, E);
+        arbitrary_tuple!(A, B, C, D, E, F);
+        arbitrary_tuple!(A, B, C, D, E, F, G);
+        arbitrary_tuple!(A, B, C, D, E, F, G, H);
+        arbitrary_tuple!(A, B, C, D, E, F, G, H, I);
+        arbitrary_tuple!(A, B, C, D, E, F, G, H, I, J);
+        arbitrary_tuple!(A, B, C, D, E, F, G, H, I, J, K);
+        arbitrary_tuple!(A, B, C, D, E, F, G, H, I, J, K, L);
+    };
+}
+
+/// This macro implements `kani::Arbitrary` on a tuple whose elements
+/// already implement `kani::Arbitrary` by running `kani::any()` on
+/// each index of the tuple.
+#[allow(clippy::crate_in_macro_def)]
+#[macro_export]
+macro_rules! arbitrary_tuple {
+    ($($type:ident),*) => {
+        impl<$($type : Arbitrary),*>  Arbitrary for ($($type,)*) {
+            #[inline(always)]
             fn any() -> Self {
-                T::any_array()
+                ($(crate::kani::any::<$type>(),)*)
             }
         }
-    };
+    }
 }
diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs
index a07ba7ca8ec4..016c805e8f8e 100644
--- a/library/kani_core/src/lib.rs
+++ b/library/kani_core/src/lib.rs
@@ -60,6 +60,7 @@ macro_rules! kani_lib {
 /// such as core in rust's std library itself.
 ///
 /// TODO: Use this inside kani library so that we dont have to maintain two copies of the same intrinsics.
+#[allow(clippy::crate_in_macro_def)]
 #[macro_export]
 macro_rules! kani_intrinsics {
     ($core:tt) => {
@@ -180,7 +181,7 @@ macro_rules! kani_intrinsics {
         /// under all possible `NonZeroU8` input values, i.e., all possible `u8` values except zero.
         ///
         /// ```rust
-        /// let inputA = kani::any::<std::num::NonZeroU8>();
+        /// let inputA = kani::any::<core::num::NonZeroU8>();
         /// fn_under_verification(inputA);
         /// ```
         ///
@@ -247,21 +248,21 @@ macro_rules! kani_intrinsics {
         /// Note that SIZE_T must be equal the size of type T in bytes.
         #[inline(never)]
         #[cfg(not(feature = "concrete_playback"))]
-        pub(crate) unsafe fn any_raw_internal<T, const SIZE_T: usize>() -> T {
+        pub(crate) unsafe fn any_raw_internal<T: Copy>() -> T {
             any_raw_inner::<T>()
         }
 
         #[inline(never)]
         #[cfg(feature = "concrete_playback")]
-        pub(crate) unsafe fn any_raw_internal<T, const SIZE_T: usize>() -> T {
-            concrete_playback::any_raw_internal::<T, SIZE_T>()
+        pub(crate) unsafe fn any_raw_internal<T: Copy>() -> T {
+            concrete_playback::any_raw_internal::<T>()
         }
 
         /// This low-level function returns nondet bytes of size T.
         #[rustc_diagnostic_item = "KaniAnyRaw"]
         #[inline(never)]
         #[allow(dead_code)]
-        pub fn any_raw_inner<T>() -> T {
+        pub fn any_raw_inner<T: Copy>() -> T {
             kani_intrinsic()
         }
 
@@ -269,7 +270,7 @@ macro_rules! kani_intrinsics {
         /// supported by Kani display.
         ///
         /// During verification this will get replaced by `assert(false)`. For concrete executions, we just
-        /// invoke the regular `std::panic!()` function. This function is used by our standard library
+        /// invoke the regular `core::panic!()` function. This function is used by our standard library
         /// overrides, but not the other way around.
         #[inline(never)]
         #[rustc_diagnostic_item = "KaniPanic"]
@@ -294,6 +295,8 @@ macro_rules! kani_intrinsics {
         }
 
         pub mod internal {
+            use crate::kani::Arbitrary;
+            use core::ptr;
 
             /// Helper trait for code generation for `modifies` contracts.
             ///
@@ -301,7 +304,7 @@ macro_rules! kani_intrinsics {
             #[doc(hidden)]
             pub trait Pointer<'a> {
                 /// Type of the pointed-to data
-                type Inner;
+                type Inner: ?Sized;
 
                 /// Used for checking assigns contracts where we pass immutable references to the function.
                 ///
@@ -309,56 +312,52 @@ macro_rules! kani_intrinsics {
                 /// argument, for instance one of type `&mut _`, in the `modifies` clause which would move it.
                 unsafe fn decouple_lifetime(&self) -> &'a Self::Inner;
 
-                /// used for havocking on replecement of a `modifies` clause.
-                unsafe fn assignable(self) -> &'a mut Self::Inner;
+                unsafe fn assignable(self) -> *mut Self::Inner;
             }
 
-            impl<'a, 'b, T> Pointer<'a> for &'b T {
+            impl<'a, 'b, T: ?Sized> Pointer<'a> for &'b T {
                 type Inner = T;
                 unsafe fn decouple_lifetime(&self) -> &'a Self::Inner {
-                    $core::mem::transmute(*self)
+                    core::mem::transmute(*self)
                 }
 
-                #[allow(clippy::transmute_ptr_to_ref)]
-                unsafe fn assignable(self) -> &'a mut Self::Inner {
-                    $core::mem::transmute(self as *const T)
+                unsafe fn assignable(self) -> *mut Self::Inner {
+                    core::mem::transmute(self as *const T)
                 }
             }
 
-            impl<'a, 'b, T> Pointer<'a> for &'b mut T {
+            impl<'a, 'b, T: ?Sized> Pointer<'a> for &'b mut T {
                 type Inner = T;
 
                 #[allow(clippy::transmute_ptr_to_ref)]
                 unsafe fn decouple_lifetime(&self) -> &'a Self::Inner {
-                    $core::mem::transmute::<_, &&'a T>(self)
+                    core::mem::transmute::<_, &&'a T>(self)
                 }
 
-                unsafe fn assignable(self) -> &'a mut Self::Inner {
-                    $core::mem::transmute(self)
+                unsafe fn assignable(self) -> *mut Self::Inner {
+                    self as *mut T
                 }
             }
 
-            impl<'a, T> Pointer<'a> for *const T {
+            impl<'a, T: ?Sized> Pointer<'a> for *const T {
                 type Inner = T;
                 unsafe fn decouple_lifetime(&self) -> &'a Self::Inner {
                     &**self as &'a T
                 }
 
-                #[allow(clippy::transmute_ptr_to_ref)]
-                unsafe fn assignable(self) -> &'a mut Self::Inner {
-                    $core::mem::transmute(self)
+                unsafe fn assignable(self) -> *mut Self::Inner {
+                    core::mem::transmute(self)
                 }
             }
 
-            impl<'a, T> Pointer<'a> for *mut T {
+            impl<'a, T: ?Sized> Pointer<'a> for *mut T {
                 type Inner = T;
                 unsafe fn decouple_lifetime(&self) -> &'a Self::Inner {
                     &**self as &'a T
                 }
 
-                #[allow(clippy::transmute_ptr_to_ref)]
-                unsafe fn assignable(self) -> &'a mut Self::Inner {
-                    $core::mem::transmute(self)
+                unsafe fn assignable(self) -> *mut Self::Inner {
+                    self
                 }
             }
 
@@ -391,6 +390,48 @@ macro_rules! kani_intrinsics {
             pub fn apply_closure<T, U: Fn(&T) -> bool>(f: U, x: &T) -> bool {
                 f(x)
             }
+
+            /// Recieves a reference to a pointer-like object and assigns kani::any_modifies to that object.
+            /// Only for use within function contracts and will not be replaced if the recursive or function stub
+            /// replace contracts are not used.
+            #[rustc_diagnostic_item = "KaniWriteAny"]
+            #[inline(never)]
+            #[doc(hidden)]
+            pub unsafe fn write_any<T: ?Sized>(_pointer: *mut T) {
+                // This function should not be reacheable.
+                // Users must include `#[kani::recursion]` in any function contracts for recursive functions;
+                // otherwise, this might not be properly instantiate. We mark this as unreachable to make
+                // sure Kani doesn't report any false positives.
+                unreachable!()
+            }
+
+            /// Fill in a slice with kani::any.
+            /// Intended as a post compilation replacement for write_any
+            #[rustc_diagnostic_item = "KaniWriteAnySlice"]
+            #[inline(always)]
+            pub unsafe fn write_any_slice<T: Arbitrary>(slice: *mut [T]) {
+                (*slice).fill_with(T::any)
+            }
+
+            /// Fill in a pointer with kani::any.
+            /// Intended as a post compilation replacement for write_any
+            #[rustc_diagnostic_item = "KaniWriteAnySlim"]
+            #[inline(always)]
+            pub unsafe fn write_any_slim<T: Arbitrary>(pointer: *mut T) {
+                ptr::write(pointer, T::any())
+            }
+
+            /// Fill in a str with kani::any.
+            /// Intended as a post compilation replacement for write_any.
+            /// Not yet implemented
+            #[rustc_diagnostic_item = "KaniWriteAnyStr"]
+            #[inline(always)]
+            pub unsafe fn write_any_str(_s: *mut str) {
+                //TODO: strings introduce new UB
+                //(*s).as_bytes_mut().fill_with(u8::any)
+                //TODO: String validation
+                unimplemented!("Kani does not support creating arbitrary `str`")
+            }
         }
     };
 }
diff --git a/tests/script-based-pre/verify_std_cmd/verify_core.rs b/tests/script-based-pre/verify_std_cmd/verify_core.rs
new file mode 100644
index 000000000000..28cf113a9210
--- /dev/null
+++ b/tests/script-based-pre/verify_std_cmd/verify_core.rs
@@ -0,0 +1,75 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+/// Dummy code that gets injected into `core` for basic tests for `verify-std` subcommand.
+#[cfg(kani)]
+kani_core::kani_lib!(core);
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+pub mod verify {
+    use crate::kani;
+    use core::num::NonZeroU8;
+
+    #[kani::proof]
+    pub fn harness() {
+        kani::assert(true, "yay");
+    }
+
+    #[kani::proof_for_contract(fake_function)]
+    fn dummy_proof() {
+        fake_function(true);
+    }
+
+    /// Add a `rustc_diagnostic_item` to ensure this works.
+    /// See <https://github.com/model-checking/kani/issues/3251> for more details.
+    #[kani::requires(x == true)]
+    #[rustc_diagnostic_item = "fake_function"]
+    fn fake_function(x: bool) -> bool {
+        x
+    }
+
+    #[kani::proof_for_contract(dummy_read)]
+    fn check_dummy_read() {
+        let val: char = kani::any();
+        assert_eq!(unsafe { dummy_read(&val) }, val);
+    }
+
+    /// Ensure we can verify constant functions.
+    #[kani::requires(kani::mem::can_dereference(ptr))]
+    #[rustc_diagnostic_item = "dummy_read"]
+    const unsafe fn dummy_read<T: Copy>(ptr: *const T) -> T {
+        *ptr
+    }
+
+    #[kani::proof_for_contract(swap_tuple)]
+    fn check_swap_tuple() {
+        let initial: (char, NonZeroU8) = kani::any();
+        let _swapped = swap_tuple(initial);
+    }
+
+    #[kani::ensures(| result | result.0 == second && result.1 == first)]
+    fn swap_tuple((first, second): (char, NonZeroU8)) -> (NonZeroU8, char) {
+        (second, first)
+    }
+
+    #[kani::proof_for_contract(add_one)]
+    fn check_add_one() {
+        let mut initial: [u32; 4] = kani::any();
+        unsafe { add_one(&mut initial) };
+    }
+
+    /// Function with a more elaborated contract that uses `old` and `modifies`.
+    #[kani::modifies(inout)]
+    #[kani::requires(kani::mem::can_dereference(inout)
+    && unsafe { inout.as_ref_unchecked().iter().all(| i | * i < u32::MAX) })]
+    #[kani::requires(kani::mem::can_write(inout))]
+    #[kani::ensures(| result | {
+    let (orig, i) = old({
+    let i = kani::any_where(| i: & usize | * i < unsafe { inout.len() });
+    (unsafe { inout.as_ref_unchecked()[i] }, i)});
+    unsafe { inout.as_ref_unchecked()[i] > orig }
+    })]
+    unsafe fn add_one(inout: *mut [u32]) {
+        inout.as_mut_unchecked().iter_mut().for_each(|e| *e += 1)
+    }
+}
diff --git a/tests/script-based-pre/verify_std_cmd/verify_std.expected b/tests/script-based-pre/verify_std_cmd/verify_std.expected
index aa30da375dd3..22e8fb2e6375 100644
--- a/tests/script-based-pre/verify_std_cmd/verify_std.expected
+++ b/tests/script-based-pre/verify_std_cmd/verify_std.expected
@@ -9,7 +9,13 @@ VERIFICATION:- SUCCESSFUL
 Checking harness verify::check_dummy_read...
 VERIFICATION:- SUCCESSFUL
 
+Checking harness verify::check_add_one...
+VERIFICATION:- SUCCESSFUL
+
+Checking harness verify::check_swap_tuple...
+VERIFICATION:- SUCCESSFUL
+
 Checking harness num::verify::check_non_zero...
 VERIFICATION:- SUCCESSFUL
 
-Complete - 4 successfully verified harnesses, 0 failures, 4 total.
+Complete - 6 successfully verified harnesses, 0 failures, 6 total.
diff --git a/tests/script-based-pre/verify_std_cmd/verify_std.sh b/tests/script-based-pre/verify_std_cmd/verify_std.sh
index 3253ad29756e..91454c4b65e7 100755
--- a/tests/script-based-pre/verify_std_cmd/verify_std.sh
+++ b/tests/script-based-pre/verify_std_cmd/verify_std.sh
@@ -21,47 +21,7 @@ STD_PATH="${SYSROOT}/lib/rustlib/src/rust/library"
 cp -r "${STD_PATH}" "${TMP_DIR}"
 
 # Insert a small harness in one of the standard library modules.
-CORE_CODE='
-#[cfg(kani)]
-kani_core::kani_lib!(core);
-
-#[cfg(kani)]
-#[unstable(feature = "kani", issue = "none")]
-pub mod verify {
-    use crate::kani;
-
-    #[kani::proof]
-    pub fn harness() {
-        kani::assert(true, "yay");
-    }
-
-    #[kani::proof_for_contract(fake_function)]
-    fn dummy_proof() {
-        fake_function(true);
-    }
-
-    /// Add a `rustc_diagnostic_item` to ensure this works.
-    /// See <https://github.com/model-checking/kani/issues/3251> for more details.
-    #[kani::requires(x == true)]
-    #[rustc_diagnostic_item = "fake_function"]
-    fn fake_function(x: bool) -> bool {
-        x
-    }
-
-    #[kani::proof_for_contract(dummy_read)]
-    fn check_dummy_read() {
-        let val: char = kani::any();
-        assert_eq!(unsafe { dummy_read(&val) }, val);
-    }
-
-    /// Ensure we can verify constant functions.
-    #[kani::requires(kani::mem::can_dereference(ptr))]
-    #[rustc_diagnostic_item = "dummy_read"]
-    const unsafe fn dummy_read<T: Copy>(ptr: *const T) -> T {
-        *ptr
-    }
-}
-'
+CORE_CODE=$(cat verify_core.rs)
 
 STD_CODE='
 #[cfg(kani)]

From 70bd0215da3183db04796c93f070d805cc93343b Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Fri, 26 Jul 2024 11:04:59 -0700
Subject: [PATCH 20/20] Add two new CI workflows to check Kani against
 `verify-rust-std` (#3386)

This PR adds the following workflows:
1. `verify-std-check`: This workflow will run either in a PR or via
workflow call. It pulls the `main` branch of `verify-rust-std`
repository, and see if it can verify the repo with the new Kani version
from HEAD.
   - If verification succeeds, the workflow will succeed.
   - If the verification fails and this is a PR, the workflow will compare
the verification result against the base of the PR. The workflow will
succeed if the results match*.
2. `verify-std-update`: This workflow will run the `verify-std-check`
workflow. If it succeeds, it will update the `verify-rust-std` branch
from HEAD. This workflow will fail if `features/verify-rust-std` branch
diverges, and a merge is required.

The motivation for this PR is to help us identify any changes to Kani
that may break the Rust verification repository, and to keep the
`verify-rust-std` up to date as much as possible.

* The fallback logic is needed since toolchain upgrades can potentially
break the std verification. This will happen in cases where the new
toolchain version is incompatible with the library version from the
`verify-rust-std`. Those cases should not interfere with Kani
development, and they should be fixed when we update the
`verify-rust-std` repo.
---
 .github/workflows/verify-std-check.yml  | 86 +++++++++++++++++++++++++
 .github/workflows/verify-std-update.yml | 35 ++++++++++
 2 files changed, 121 insertions(+)
 create mode 100644 .github/workflows/verify-std-check.yml
 create mode 100644 .github/workflows/verify-std-update.yml

diff --git a/.github/workflows/verify-std-check.yml b/.github/workflows/verify-std-check.yml
new file mode 100644
index 000000000000..667be6b340c5
--- /dev/null
+++ b/.github/workflows/verify-std-check.yml
@@ -0,0 +1,86 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+#
+# This workflow will try to build and run the `verify-rust-std` repository.
+#
+# This check should be optional, but it has been added to help provide
+# visibility to when a PR may break the `verify-rust-std` repository.
+#
+# We expect toolchain updates to potentially break this workflow in cases where
+# the version tracked in the `verify-rust-std` is not compatible with newer
+# versions of the Rust toolchain.
+#
+# Changes unrelated to the toolchain should match the current status of main.
+
+name: Check Std Verification
+on:
+  pull_request:
+  workflow_call:
+
+env:
+  RUST_BACKTRACE: 1
+
+jobs:
+  verify-std:
+    runs-on: ${{ matrix.os }}
+    strategy:
+      matrix:
+        # Kani does not support windows.
+        os: [ ubuntu-22.04, macos-14 ]
+    steps:
+      - name: Checkout Library
+        uses: actions/checkout@v4
+        with:
+          repository: model-checking/verify-rust-std
+          path: verify-rust-std
+          submodules: true
+
+      - name: Checkout `Kani`
+        uses: actions/checkout@v4
+        with:
+          path: kani
+
+      - name: Setup Kani Dependencies
+        uses: ./kani/.github/actions/setup
+        with:
+          os: ${{ matrix.os }}
+          kani_dir: kani
+
+      - name: Build Kani
+        working-directory: kani
+        run: |
+          cargo build-dev
+          echo "$(pwd)/scripts" >> $GITHUB_PATH
+
+      - name: Run verification with HEAD
+        id: check-head
+        working-directory: verify-rust-std
+        continue-on-error: true
+        run: |
+          kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \
+            -Z mem-predicates -Z ptr-to-ref-cast-checks
+
+      # If the head failed, check if it's a new failure.
+      - name: Checkout base
+        working-directory: kani
+        if: steps.check-head.outcome != 'success' && github.event_name == 'pull_request'
+        run: |
+          BASE_REF=${{ github.event.pull_request.base.sha }}
+          git checkout ${BASE_REF}
+          cargo build-dev
+
+      - name: Run verification with BASE
+        id: check-base
+        if: steps.check-head.outcome != 'success' && github.event_name == 'pull_request'
+        working-directory: verify-rust-std
+        continue-on-error: true
+        run: |
+          kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \
+            -Z mem-predicates -Z ptr-to-ref-cast-checks
+
+      - name: Compare PR results
+        if: steps.check-head.outcome != 'success' && steps.check-head.output != github.check-base.output
+        run: |
+          echo "New failure introduced by this change"
+          exit 1
+
diff --git a/.github/workflows/verify-std-update.yml b/.github/workflows/verify-std-update.yml
new file mode 100644
index 000000000000..518f80ecd1b8
--- /dev/null
+++ b/.github/workflows/verify-std-update.yml
@@ -0,0 +1,35 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+#
+# This workflow will try to update the verify std branch.
+
+name: Update "features/verify-rust-std"
+on:
+  schedule:
+    - cron: "30 3 * * *" # Run this every day at 03:30 UTC
+  workflow_dispatch:     # Allow manual dispatching.
+
+env:
+  RUST_BACKTRACE: 1
+
+jobs:
+  # First ensure the HEAD is compatible with the `verify-rust-std` repository.
+  verify-std:
+    name: Verify Std
+    permissions: { }
+    uses: ./.github/workflows/verify-std-check.yml
+
+  # Push changes to the features branch.
+  update-branch:
+    needs: verify-std
+    permissions:
+      contents: write
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout Kani
+        uses: actions/checkout@v4
+
+      - name: Update feature branch
+        run: |
+          git push origin HEAD:features/verify-rust-std
+