Update to CBMC version 6.1.1

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,

kani-driver/src/call_cbmc.rs

@@ -153,37 +153,51 @@ impl KaniSession {
 
         args.push(file.to_owned().into_os_string());
 
+        // Make CBMC verbose by default to tell users about unwinding progress. This should be
+        // reviewed as CBMC's verbosity defaults evolve.
+        args.push("--verbosity".into());
+        args.push("9".into());
+
         Ok(args)
     }
 
     /// Just the flags to CBMC that enable property checking of any sort.
     pub fn cbmc_check_flags(&self) -> Vec<OsString> {
         let mut args = Vec::new();
 
-        if self.args.checks.memory_safety_on() {
-            args.push("--bounds-check".into());
-            args.push("--pointer-check".into());
+        // We assume that malloc cannot fail, see https://github.com/model-checking/kani/issues/891
+        args.push("--no-malloc-may-fail".into());
+
+        // With PR #2630 we generate the appropriate checks directly rather than relying on CBMC's
+        // checks (which are for C semantics).
+        args.push("--no-undefined-shift-check".into());
+        // With PR #647 we use Rust's `-C overflow-checks=on` instead of:
+        // --unsigned-overflow-check
+        // --signed-overflow-check
+        // So these options are deliberately skipped to avoid erroneously re-checking operations.
+        args.push("--no-signed-overflow-check".into());
+
+        if !self.args.checks.memory_safety_on() {
+            args.push("--no-bounds-check".into());
+            args.push("--no-pointer-check".into());
         }
         if self.args.checks.overflow_on() {
-            args.push("--div-by-zero-check".into());
             args.push("--float-overflow-check".into());
             args.push("--nan-check".into());
-            // With PR #647 we use Rust's `-C overflow-checks=on` instead of:
-            // --unsigned-overflow-check
-            // --signed-overflow-check
-            // So these options are deliberately skipped to avoid erroneously re-checking operations.
 
             // TODO: Implement conversion checks as an optional check.
             // They are a well defined operation in rust, but they may yield unexpected results to
             // many users. https://github.com/model-checking/kani/issues/840
             // We might want to create a transformation pass instead of enabling CBMC since Kani
             // compiler sometimes rely on the bitwise conversion of signed <-> unsigned.
             // args.push("--conversion-check".into());
+        } else {
+            args.push("--no-div-by-zero-check".into());
         }
 
-        if self.args.checks.unwinding_on() {
-            // TODO: With CBMC v6 the below can be removed as those are defaults.
-            args.push("--unwinding-assertions".into());
+        if !self.args.checks.unwinding_on() {
+            args.push("--no-unwinding-assertions".into());
+        } else {
             args.push("--no-self-loops-to-assumptions".into());
         }
 
@@ -192,7 +206,8 @@ impl KaniSession {
             // still catch any invalid dereference with --pointer-check. Thus, only enable them
             // if the user explicitly request them.
             args.push("--pointer-overflow-check".into());
-            args.push("--pointer-primitive-check".into());
+        } else {
+            args.push("--no-pointer-primitive-check".into());
         }
 
         args

kani-driver/src/call_goto_instrument.rs

@@ -93,6 +93,7 @@ impl KaniSession {
     fn add_library(&self, file: &Path) -> Result<()> {
         let args: Vec<OsString> = vec![
             "--add-library".into(),
+            "--no-malloc-may-fail".into(),
             file.to_owned().into_os_string(), // input
             file.to_owned().into_os_string(), // output
         ];
@@ -173,6 +174,7 @@ impl KaniSession {
             assigns.contracted_function_name.as_str().into(),
             "--nondet-static-exclude".into(),
             assigns.recursion_tracker.as_str().into(),
+            "--no-malloc-may-fail".into(),
             file.into(),
             file.into(),
         ];