Merge branch 'main' into issue-3383-contract-playback

.github/workflows/cbmc-latest.yml

@@ -38,14 +38,24 @@ jobs:
           repository: diffblue/cbmc
           path: cbmc
 
-      - name: Build CBMC
+      - name: Build CBMC (Linux)
+        if: ${{ startsWith(matrix.os, 'ubuntu') }}
         working-directory: ./cbmc
         run: |
           cmake -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical"
           cmake --build build -- -j 4
           # Prepend the bin directory to $PATH
           echo "${GITHUB_WORKSPACE}/cbmc/build/bin" >> $GITHUB_PATH
 
+      - name: Build CBMC (macOS)
+        if: ${{ startsWith(matrix.os, 'macos') }}
+        working-directory: ./cbmc
+        run: |
+          cmake -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical" -DCMAKE_CXX_COMPILER=$(which clang++)
+          cmake --build build -- -j 4
+          # Prepend the bin directory to $PATH
+          echo "${GITHUB_WORKSPACE}/cbmc/build/bin" >> $GITHUB_PATH
+
       - name: Execute Kani regressions
         working-directory: ./kani
         run: ./scripts/kani-regression.sh

cprover_bindings/src/env.rs

@@ -8,7 +8,7 @@
 //! c.f. CBMC code [src/ansi-c/ansi_c_internal_additions.cpp].
 //! One possible invocation of this insertion in CBMC can be found in \[ansi_c_languaget::parse\].
 
-use super::goto_program::{Expr, Location, Symbol, Type};
+use super::goto_program::{Expr, Location, Symbol, SymbolTable, Type};
 use super::MachineModel;
 use num::bigint::BigInt;
 fn int_constant<T>(name: &str, value: T) -> Symbol
@@ -71,6 +71,8 @@ pub fn machine_model_symbols(mm: &MachineModel) -> Vec<Symbol> {
     ]
 }
 
+const DEAD_OBJECT_IDENTIFIER: &str = "__CPROVER_dead_object";
+
 pub fn additional_env_symbols() -> Vec<Symbol> {
     vec![
         Symbol::builtin_function("__CPROVER_initialize", vec![], Type::empty()),
@@ -82,5 +84,16 @@ pub fn additional_env_symbols() -> Vec<Symbol> {
             Location::none(),
         )
         .with_is_extern(true),
+        Symbol::static_variable(
+            DEAD_OBJECT_IDENTIFIER,
+            DEAD_OBJECT_IDENTIFIER,
+            Type::void_pointer(),
+            Location::none(),
+        )
+        .with_is_extern(true),
     ]
 }
+
+pub fn global_dead_object(symbol_table: &SymbolTable) -> Expr {
+    symbol_table.lookup(DEAD_OBJECT_IDENTIFIER).unwrap().to_expr()
+}

cprover_bindings/src/irep/goto_binary_serde.rs

@@ -11,7 +11,7 @@ use std::io::{self, BufReader};
 use std::io::{BufWriter, Bytes, Error, ErrorKind, Read, Write};
 use std::path::Path;
 
-/// Writes a symbol table to a file in goto binary format in version 5.
+/// Writes a symbol table to a file in goto binary format in version 6.
 ///
 /// In CBMC, the serialization rules are defined in :
 /// - src/goto-programs/write_goto_binary.h
@@ -26,7 +26,7 @@ pub fn write_goto_binary_file(filename: &Path, source: &crate::goto_program::Sym
     serializer.write_file(irep_symbol_table);
 }
 
-/// Reads a symbol table from a file expected to be in goto binary format in version 5.
+/// Reads a symbol table from a file expected to be in goto binary format in version 6.
 //
 /// In CBMC, the deserialization rules are defined in :
 /// - src/goto-programs/read_goto_binary.h
@@ -540,7 +540,7 @@ where
         assert!(written == 4);
 
         // Write goto binary version
-        self.write_usize_varenc(5);
+        self.write_usize_varenc(6);
     }
 
     /// Writes the symbol table using the GOTO binary file format to the byte stream.
@@ -921,12 +921,12 @@ where
 
         // Read goto binary version
         let goto_binary_version = self.read_usize_varenc()?;
-        if goto_binary_version != 5 {
+        if goto_binary_version != 6 {
             return Err(Error::new(
                 ErrorKind::Other,
                 format!(
                     "Unsupported GOTO binary version: {}. Supported version: {}",
-                    goto_binary_version, 5
+                    goto_binary_version, 6
                 ),
             ));
         }

cprover_bindings/src/irep/irep_id.rs

@@ -366,7 +366,7 @@ pub enum IrepId {
     Div,
     Power,
     FactorialPower,
-    PrettyName,
+    CPrettyName,
     CClass,
     CField,
     CInterface,
@@ -1242,7 +1242,7 @@ impl Display for IrepId {
             IrepId::Div => "/",
             IrepId::Power => "**",
             IrepId::FactorialPower => "factorial_power",
-            IrepId::PrettyName => "pretty_name",
+            IrepId::CPrettyName => "#pretty_name",
             IrepId::CClass => "#class",
             IrepId::CField => "#field",
             IrepId::CInterface => "#interface",

cprover_bindings/src/irep/to_irep.rs

@@ -132,7 +132,7 @@ impl ToIrep for DatatypeComponent {
         match self {
             DatatypeComponent::Field { name, typ } => Irep::just_named_sub(linear_map![
                 (IrepId::Name, Irep::just_string_id(name.to_string())),
-                (IrepId::PrettyName, Irep::just_string_id(name.to_string())),
+                (IrepId::CPrettyName, Irep::just_string_id(name.to_string())),
                 (IrepId::Type, typ.to_irep(mm)),
             ]),
             DatatypeComponent::Padding { name, bits } => Irep::just_named_sub(linear_map![

cprover_bindings/src/lib.rs

@@ -33,6 +33,7 @@
 #![feature(f16)]
 
 mod env;
+pub use env::global_dead_object;
 pub mod goto_program;
 pub mod irep;
 mod machine_model;

kani-compiler/src/args.rs

@@ -74,9 +74,6 @@ pub struct Arguments {
     /// Enable specific checks.
     #[clap(long)]
     pub ub_check: Vec<ExtraChecks>,
-    /// Ignore storage markers.
-    #[clap(long)]
-    pub ignore_storage_markers: bool,
 }
 
 #[derive(Debug, Clone, Copy, AsRefStr, EnumString, VariantNames, PartialEq, Eq)]

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

@@ -75,18 +75,68 @@ impl<'tcx> GotocCtx<'tcx> {
                 .goto_expr;
                 self.codegen_set_discriminant(dest_ty, dest_expr, *variant_index, location)
             }
+            // StorageLive and StorageDead are modelled via CBMC's internal means of detecting
+            // accesses to dangling pointers, which uses demonic non-determinism. That is, CBMC
+            // non-deterministically chooses a single object's address to be tracked in a
+            // pointer-typed global instrumentation variable __CPROVER_dead_object. Any dereference
+            // entails a check that the pointer being dereferenced is not equal to the pointer held
+            // in __CPROVER_dead_object. We use this to bridge the difference between Rust and MIR
+            // semantics as follows:
+            //
+            // 1. (At the time of writing) MIR declares all function-local variables at function
+            //    scope, irrespective of the scope/block that Rust code originally used.
+            // 2. In MIR, StorageLive and StorageDead markers are inserted at the beginning and end
+            //    of the Rust block to record the Rust-level lifetime of the object.
+            // 3. We translate MIR declarations into GOTO declarations, implying that we will have
+            //    a single object per function for a local variable, even when Rust had a variable
+            //    declared in a sub-scope of the function where said scope was entered multiple
+            //    times (e.g., a loop body).
+            // 4. To enable detection of use of dangling pointers, we now use
+            //    __CPROVER_dead_object, unless the address of the local object is never taken
+            //    (implying that there cannot be a use of a dangling pointer with respect to said
+            //    object). We update __CPROVER_dead_object as follows:
+            //    * StorageLive is set to NULL when __CPROVER_dead_object pointed to the object
+            //    (re-)entering scope, or else is left unchanged.
+            //    * StorageDead non-deterministically updates (or leaves unchanged)
+            //    __CPROVER_dead_object to point to the object going out of scope. (This is the
+            //    same update approach as used within CBMC.)
+            //
+            // This approach will also work when there are multiple occurrences of StorageLive (or
+            // StorageDead) on a path, or across control-flow branches, and even when StorageDead
+            // occurs without a preceding StorageLive.
             StatementKind::StorageLive(var_id) => {
-                if self.queries.args().ignore_storage_markers {
+                if !self.current_fn().is_address_taken_local(*var_id) {
                     Stmt::skip(location)
                 } else {
-                    Stmt::decl(self.codegen_local(*var_id, location), None, location)
+                    let global_dead_object = cbmc::global_dead_object(&self.symbol_table);
+                    Stmt::assign(
+                        global_dead_object.clone(),
+                        global_dead_object
+                            .clone()
+                            .eq(self
+                                .codegen_local(*var_id, location)
+                                .address_of()
+                                .cast_to(global_dead_object.typ().clone()))
+                            .ternary(global_dead_object.typ().null(), global_dead_object),
+                        location,
+                    )
                 }
             }
             StatementKind::StorageDead(var_id) => {
-                if self.queries.args().ignore_storage_markers {
+                if !self.current_fn().is_address_taken_local(*var_id) {
                     Stmt::skip(location)
                 } else {
-                    Stmt::dead(self.codegen_local(*var_id, location), location)
+                    let global_dead_object = cbmc::global_dead_object(&self.symbol_table);
+                    Stmt::assign(
+                        global_dead_object.clone(),
+                        Type::bool().nondet().ternary(
+                            self.codegen_local(*var_id, location)
+                                .address_of()
+                                .cast_to(global_dead_object.typ().clone()),
+                            global_dead_object,
+                        ),
+                        location,
+                    )
                 }
             }
             StatementKind::Intrinsic(NonDivergingIntrinsic::CopyNonOverlapping(
@@ -424,6 +474,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 .branches()
                 .map(|(c, bb)| {
                     Expr::int_constant(c, switch_ty.clone())
+                        .with_location(loc)
                         .switch_case(Stmt::goto(bb_label(bb), loc))
                 })
                 .collect();

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

@@ -7,9 +7,9 @@ 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};
+use stable_mir::mir::{visit::Location, visit::MirVisitor, Body, Local, LocalDecl, Rvalue};
 use stable_mir::CrateDef;
-use std::collections::HashMap;
+use std::collections::{HashMap, HashSet};
 
 /// This structure represents useful data about the function we are currently compiling.
 #[derive(Debug)]
@@ -26,6 +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 used in a reference or address-of expression.
+    address_taken_locals: HashSet<Local>,
     /// The symbol name of the current function
     name: String,
     /// A human readable pretty name for the current function
@@ -34,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<Local>,
+}
+
+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 {
@@ -46,13 +66,16 @@ impl<'tcx> CurrentFnCtx<'tcx> {
             .iter()
             .filter_map(|info| info.local().map(|local| (local, (&info.name).into())))
             .collect::<HashMap<_, _>>();
+        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,
+            address_taken_locals: visitor.address_taken_locals,
             name,
             readable_name,
             temp_var_counter: 0,
@@ -106,6 +129,10 @@ impl<'tcx> CurrentFnCtx<'tcx> {
     pub fn local_name(&self, local: Local) -> Option<InternedString> {
         self.local_names.get(&local).copied()
     }
+
+    pub fn is_address_taken_local(&self, local: Local) -> bool {
+        self.address_taken_locals.contains(&local)
+    }
 }
 
 /// Utility functions

kani-dependencies

@@ -1,6 +1,6 @@
-CBMC_MAJOR="5"
-CBMC_MINOR="95"
-CBMC_VERSION="5.95.1"
+CBMC_MAJOR="6"
+CBMC_MINOR="1"
+CBMC_VERSION="6.1.1"
 
 # If you update this version number, remember to bump it in `src/setup.rs` too
 CBMC_VIEWER_MAJOR="3"

kani-driver/src/args/mod.rs

@@ -245,14 +245,6 @@ pub struct VerificationArgs {
     #[arg(long, hide_short_help = true, requires("enable_unstable"))]
     pub ignore_global_asm: bool,
 
-    /// Ignore lifetimes of local variables. This effectively extends their
-    /// lifetimes to the function scope, and hence may cause Kani to miss
-    /// undefined behavior resulting from using the variable after it dies.
-    /// This option may impact the soundness of the analysis and may cause false
-    /// proofs and/or counterexamples
-    #[arg(long, hide_short_help = true, requires("enable_unstable"))]
-    pub ignore_locals_lifetime: bool,
-
     /// Write the GotoC symbol table to a file in JSON format instead of goto binary format.
     #[arg(long, hide_short_help = true)]
     pub write_json_symtab: bool,