Codegen storage markers as assignments to __CPROVER_dead_object

This changes our handling of storage markers to be marking is-alive
only rather than treating StorageLive as creating a new object. That is,
object instances are now tied to their Mir-provided declarations (which,
at present, only appear once per function). To still account for when
Rust scopes deem an object to be alive, we use StorageLive and
StorageDead to update `__CPROVER_dead_object`. This (global) variable is
used by CBMC's pointer checks to track when a pointer may not be safe to
dereference for it could be pointing to an object that no longer is in
scope.

Resolves: model-checking#3099

kani-compiler/src/codegen_cprover_gotoc/codegen/mod.rs

@@ -23,5 +23,4 @@ pub(super) mod typ;
 
 pub use assert::PropertyClass;
 pub use block::bb_label;
-pub use block::reverse_postorder;
 pub use typ::TypeExt;

kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs

@@ -77,7 +77,7 @@ impl<'tcx> GotocCtx<'tcx> {
             }
             StatementKind::StorageLive(var_id) => {
                 if self.queries.args().ignore_storage_markers
-                    || !self.current_fn().is_inner_local(*var_id)
+                    || !self.current_fn().is_address_taken_local(*var_id)
                 {
                     Stmt::skip(location)
                 } else {
@@ -103,7 +103,7 @@ impl<'tcx> GotocCtx<'tcx> {
             }
             StatementKind::StorageDead(var_id) => {
                 if self.queries.args().ignore_storage_markers
-                    || !self.current_fn().is_inner_local(*var_id)
+                    || !self.current_fn().is_address_taken_local(*var_id)
                 {
                     Stmt::skip(location)
                 } else {

kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs

@@ -1,14 +1,13 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-use crate::codegen_cprover_gotoc::codegen::reverse_postorder;
 use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::Stmt;
 use cbmc::InternedString;
 use rustc_middle::ty::Instance as InstanceInternal;
 use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::Instance;
-use stable_mir::mir::{Body, Local, LocalDecl, StatementKind};
+use stable_mir::mir::{visit::Location, visit::MirVisitor, Body, Local, LocalDecl, Rvalue};
 use stable_mir::CrateDef;
 use std::collections::{HashMap, HashSet};
 
@@ -27,9 +26,8 @@ pub struct CurrentFnCtx<'tcx> {
     locals: Vec<LocalDecl>,
     /// A list of pretty names for locals that corrspond to user variables.
     local_names: HashMap<Local, InternedString>,
-    /// Collection of variables that are local to an inner block within this function and never
-    /// escapte that block.
-    inner_locals_not_escaping_block: HashSet<usize>,
+    /// Collection of variables that are used in a reference or address-of expression.
+    address_taken_locals: HashSet<usize>,
     /// The symbol name of the current function
     name: String,
     /// A human readable pretty name for the current function
@@ -38,6 +36,24 @@ pub struct CurrentFnCtx<'tcx> {
     temp_var_counter: u64,
 }
 
+struct AddressTakenLocalsCollector {
+    /// Locals that appear in `Rvalue::Ref` or `Rvalue::AddressOf` expressions.
+    address_taken_locals: HashSet<usize>,
+}
+
+impl MirVisitor for AddressTakenLocalsCollector {
+    fn visit_rvalue(&mut self, rvalue: &Rvalue, _location: Location) {
+        match rvalue {
+            Rvalue::Ref(_, _, p) | Rvalue::AddressOf(_, p) => {
+                if p.projection.is_empty() {
+                    self.address_taken_locals.insert(p.local);
+                }
+            }
+            _ => (),
+        }
+    }
+}
+
 /// Constructor
 impl<'tcx> CurrentFnCtx<'tcx> {
     pub fn new(instance: Instance, gcx: &GotocCtx<'tcx>, body: &Body) -> Self {
@@ -51,38 +67,16 @@ impl<'tcx> CurrentFnCtx<'tcx> {
             .iter()
             .filter_map(|info| info.local().map(|local| (local, (&info.name).into())))
             .collect::<HashMap<_, _>>();
-        let mut inner_locals_not_escaping_block: HashSet<usize> = HashSet::new();
-        // let mut marked_dead: HashMap<usize, usize> = HashMap::new();
-        // reverse_postorder(&body).for_each(|bb| {
-        //     body.blocks[bb].statements.iter().for_each(|s| {
-        //         if let StatementKind::StorageDead(var_id) = s.kind {
-        //             *marked_dead.entry(var_id).or_default() += 1
-        //         }
-        //     })
-        // });
-        reverse_postorder(&body).for_each(|bb| {
-            inner_locals_not_escaping_block.extend(body.blocks[bb].statements.iter().filter_map(
-                |s| match s.kind {
-                    StatementKind::StorageLive(var_id) => {
-                        Some(var_id)
-                        // if marked_dead.get(&var_id) == Some(&1) {
-                        //     Some(var_id)
-                        // } else {
-                        //     None
-                        // }
-                    }
-                    _ => None,
-                },
-            ))
-        });
+        let mut visitor = AddressTakenLocalsCollector { address_taken_locals: HashSet::new() };
+        visitor.visit_body(body);
         Self {
             block: vec![],
             instance,
             instance_internal,
             krate: instance.def.krate().name,
             locals,
             local_names,
-            inner_locals_not_escaping_block,
+            address_taken_locals: visitor.address_taken_locals,
             name,
             readable_name,
             temp_var_counter: 0,
@@ -137,8 +131,8 @@ impl<'tcx> CurrentFnCtx<'tcx> {
         self.local_names.get(&local).copied()
     }
 
-    pub fn is_inner_local(&self, local: usize) -> bool {
-        self.inner_locals_not_escaping_block.contains(&local)
+    pub fn is_address_taken_local(&self, local: usize) -> bool {
+        self.address_taken_locals.contains(&local)
     }
 }
 

tests/expected/dead-invalid-access-via-raw/main.expected

@@ -1,7 +1,5 @@
 SUCCESS\
 address must be a multiple of its type's alignment
-FAILURE\
-unsafe { *raw_ptr } == 10
 SUCCESS\
 pointer NULL
 SUCCESS\

tests/kani/Spurious/storage_fixme.rs → tests/kani/StorageMarkers/main.rs

@@ -3,7 +3,7 @@
 // Modifications Copyright Kani Contributors
 // See GitHub history for details.
 
-// Our handling of storage markers causes spurious failures in this test.
+// Our handling of storage markers used to cause spurious failures in this test.
 // https://github.com/model-checking/kani/issues/3099
 // The code is extracted from the implementation of `BTreeMap` which is where we
 // originally saw the spurious failures while trying to enable storage markers