Skip to content

Commit

Permalink
Update to CBMC version 6.1.1 (#2995)
Browse files Browse the repository at this point in the history
Updates to match changes to the GOTO binary format.

Resolves: #2952, #2972, #3287, #3391

This includes 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: #3099
  • Loading branch information
tautschnig authored Jul 31, 2024
1 parent 39c6bc1 commit e4078b4
Show file tree
Hide file tree
Showing 38 changed files with 152 additions and 102 deletions.
15 changes: 14 additions & 1 deletion cprover_bindings/src/env.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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()),
Expand All @@ -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()
}
10 changes: 5 additions & 5 deletions cprover_bindings/src/irep/goto_binary_serde.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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
),
));
}
Expand Down
4 changes: 2 additions & 2 deletions cprover_bindings/src/irep/irep_id.rs
Original file line number Diff line number Diff line change
Expand Up @@ -366,7 +366,7 @@ pub enum IrepId {
Div,
Power,
FactorialPower,
PrettyName,
CPrettyName,
CClass,
CField,
CInterface,
Expand Down Expand Up @@ -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",
Expand Down
2 changes: 1 addition & 1 deletion cprover_bindings/src/irep/to_irep.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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![
Expand Down
1 change: 1 addition & 0 deletions cprover_bindings/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,7 @@
#![feature(f16)]

mod env;
pub use env::global_dead_object;
pub mod goto_program;
pub mod irep;
mod machine_model;
Expand Down
3 changes: 0 additions & 3 deletions kani-compiler/src/args.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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)]
Expand Down
59 changes: 55 additions & 4 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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(
Expand Down Expand Up @@ -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();
Expand Down
31 changes: 29 additions & 2 deletions kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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)]
Expand All @@ -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
Expand All @@ -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 {
Expand All @@ -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,
Expand Down Expand Up @@ -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
Expand Down
6 changes: 3 additions & 3 deletions kani-dependencies
Original file line number Diff line number Diff line change
@@ -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"
Expand Down
8 changes: 0 additions & 8 deletions kani-driver/src/args/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
39 changes: 27 additions & 12 deletions kani-driver/src/call_cbmc.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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());
}

Expand All @@ -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
Expand Down
2 changes: 2 additions & 0 deletions kani-driver/src/call_goto_instrument.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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
];
Expand Down Expand Up @@ -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(),
];
Expand Down
Loading

0 comments on commit e4078b4

Please sign in to comment.