Update to CBMC version 6.1.1

.github/workflows/release.yml

@@ -103,12 +103,16 @@ 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/get-pip.py -o get-pip.py
+ curl -s https://bootstrap.pypa.io/pip/3.7/get-pip.py -o get-pip.py
  python3 get-pip.py --force-reinstall
  rm get-pip.py
 

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
@@ -82,5 +82,16 @@ pub fn additional_env_symbols() -> Vec<Symbol> {
  Location::none(),
  )
  .with_is_extern(true),
+ Symbol::static_variable(
+ "__CPROVER_dead_object",
+ "__CPROVER_dead_object",
+ Type::void_pointer(),
+ Location::none(),
+ )
+ .with_is_extern(true),
  ]
 }
+
+pub fn global_dead_object(symbol_table: &SymbolTable) -> Expr {
+ symbol_table.lookup("__CPROVER_dead_object").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

@@ -364,7 +364,7 @@ pub enum IrepId {
  Div,
  Power,
  FactorialPower,
- PrettyName,
+ CPrettyName,
  CClass,
  CField,
  CInterface,
@@ -1238,7 +1238,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

@@ -30,6 +30,7 @@
 //! 1. [irep::IrepId::Empty] and [irep::IrepId::Nil] behaves like \[null\].
 
 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

@@ -76,17 +76,38 @@ impl<'tcx> GotocCtx<'tcx> {
  self.codegen_set_discriminant(dest_ty, dest_expr, *variant_index, location)
  }
  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(
@@ -425,6 +446,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<usize>,
  /// 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<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 {
@@ -47,13 +67,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,
@@ -107,6 +130,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: usize) -> 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="0"
+CBMC_VERSION="6.0.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

@@ -255,14 +255,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

@@ -160,30 +160,39 @@ impl KaniSession {
  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
+ 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 +201,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(),
  ];

kani-driver/src/call_single_file.rs

@@ -143,10 +143,6 @@ impl KaniSession {
  flags.push("--ub-check=ptr_to_ref_cast".into())
  }
 
- if self.args.ignore_locals_lifetime {
- flags.push("--ignore-storage-markers".into())
- }
-
  flags.extend(self.args.common_args.unstable_features.as_arguments().map(str::to_string));
 
  // This argument will select the Kani flavour of the compiler. It will be removed before

kani-driver/src/cbmc_output_parser.rs

@@ -329,6 +329,7 @@ pub enum CheckStatus {
  Satisfied, // for `cover` properties only
  Success,
  Undetermined,
+ Unknown,
  Unreachable,
  Uncovered, // for `code_coverage` properties only
  Unsatisfiable, // for `cover` properties only
@@ -344,6 +345,9 @@ impl std::fmt::Display for CheckStatus {
  CheckStatus::Failure => style("FAILURE").red(),
  CheckStatus::Unreachable => style("UNREACHABLE").yellow(),
  CheckStatus::Undetermined => style("UNDETERMINED").yellow(),
+ // CBMC 6+ uses UNKNOWN when another property of undefined behavior failed, making it
+ // impossible to definitively conclude whether other properties hold or not.
+ CheckStatus::Unknown => style("UNDETERMINED").yellow(),
  CheckStatus::Unsatisfiable => style("UNSATISFIABLE").yellow(),
  };
  write!(f, "{check_str}")

scripts/ci/Dockerfile.bundle-test-ubuntu-18-04

@@ -18,7 +18,7 @@ RUN apt-get update && \
 
 RUN update-alternatives --install /usr/bin/python3 python3 /usr/bin/python3.7 1
 
-RUN curl -s https://bootstrap.pypa.io/get-pip.py -o get-pip.py && \
+RUN curl -s https://bootstrap.pypa.io/pip/3.7/get-pip.py -o get-pip.py && \
  python3 get-pip.py --force-reinstall && \
  rm get-pip.py