Merge branch 'main' into issue-2690-ptr-access

CHANGELOG.md

@@ -4,6 +4,21 @@ This file contains notable changes (e.g. breaking changes, major changes, etc.)
 
 This file was introduced starting Kani 0.23.0, so it only contains changes from version 0.23.0 onwards.
 
+## [0.48.0]
+
+### Major Changes
+* We fixed a soundness bug that in some cases may cause Kani to not detect a use-after-free issue in https://github.com/model-checking/kani/pull/3063
+
+### What's Changed
+* Fix `codegen_atomic_binop` for `atomic_ptr` by @qinheping in https://github.com/model-checking/kani/pull/3047
+* Retrieve info for recursion tracker reliably by @feliperodri in https://github.com/model-checking/kani/pull/3045
+* Add `--use-local-toolchain` to Kani setup by @jaisnan in https://github.com/model-checking/kani/pull/3056
+* Replace internal reverse_postorder by a stable one by @celinval in https://github.com/model-checking/kani/pull/3064
+* Add option to override `--crate-name` from `kani` by @adpaco-aws in https://github.com/model-checking/kani/pull/3054
+* Rust toolchain upgraded to 2024-03-11 by @adpaco-ws @celinval @zyadh
+
+**Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.47.0...kani-0.48.0
+
 ## [0.47.0]
 
 ### What's Changed

Cargo.lock

@@ -141,11 +141,11 @@ dependencies = [
 
 [[package]]
 name = "build-kani"
-version = "0.47.0"
+version = "0.48.0"
 dependencies = [
  "anyhow",
  "cargo_metadata",
- "clap 4.5.1",
+ "clap 4.5.2",
  "which",
 ]
 
@@ -204,19 +204,19 @@ dependencies = [
 
 [[package]]
 name = "clap"
-version = "4.5.1"
+version = "4.5.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c918d541ef2913577a0f9566e9ce27cb35b6df072075769e0b26cb5a554520da"
+checksum = "b230ab84b0ffdf890d5a10abdbc8b83ae1c4918275daea1ab8801f71536b2651"
 dependencies = [
  "clap_builder",
  "clap_derive",
 ]
 
 [[package]]
 name = "clap_builder"
-version = "4.5.1"
+version = "4.5.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9f3e7391dad68afb0c2ede1bf619f579a3dc9c2ec67f089baa397123a2f3d1eb"
+checksum = "ae129e2e766ae0ec03484e609954119f123cc1fe650337e155d03b022f24f7b4"
 dependencies = [
  "anstream",
  "anstyle",
@@ -292,7 +292,7 @@ dependencies = [
 
 [[package]]
 name = "cprover_bindings"
-version = "0.47.0"
+version = "0.48.0"
 dependencies = [
  "lazy_static",
  "linear-map",
@@ -472,16 +472,16 @@ checksum = "b1a46d1a171d865aa5f83f92695765caa047a9b4cbae2cbf37dbd613a793fd4c"
 
 [[package]]
 name = "kani"
-version = "0.47.0"
+version = "0.48.0"
 dependencies = [
  "kani_macros",
 ]
 
 [[package]]
 name = "kani-compiler"
-version = "0.47.0"
+version = "0.48.0"
 dependencies = [
- "clap 4.5.1",
+ "clap 4.5.2",
  "cprover_bindings",
  "home",
  "itertools",
@@ -492,19 +492,19 @@ dependencies = [
  "serde",
  "serde_json",
  "shell-words",
- "strum 0.26.1",
- "strum_macros 0.26.1",
+ "strum 0.26.2",
+ "strum_macros 0.26.2",
  "tracing",
  "tracing-subscriber",
 ]
 
 [[package]]
 name = "kani-driver"
-version = "0.47.0"
+version = "0.48.0"
 dependencies = [
  "anyhow",
  "cargo_metadata",
- "clap 4.5.1",
+ "clap 4.5.2",
  "comfy-table",
  "console",
  "glob",
@@ -517,8 +517,8 @@ dependencies = [
  "rustc-demangle",
  "serde",
  "serde_json",
- "strum 0.26.1",
- "strum_macros 0.26.1",
+ "strum 0.26.2",
+ "strum_macros 0.26.2",
  "tempfile",
  "toml",
  "tracing",
@@ -528,7 +528,7 @@ dependencies = [
 
 [[package]]
 name = "kani-verifier"
-version = "0.47.0"
+version = "0.48.0"
 dependencies = [
  "anyhow",
  "clap 2.34.0",
@@ -538,7 +538,7 @@ dependencies = [
 
 [[package]]
 name = "kani_macros"
-version = "0.47.0"
+version = "0.48.0"
 dependencies = [
  "proc-macro-error",
  "proc-macro2",
@@ -548,13 +548,13 @@ dependencies = [
 
 [[package]]
 name = "kani_metadata"
-version = "0.47.0"
+version = "0.48.0"
 dependencies = [
- "clap 4.5.1",
+ "clap 4.5.2",
  "cprover_bindings",
  "serde",
- "strum 0.26.1",
- "strum_macros 0.26.1",
+ "strum 0.26.2",
+ "strum_macros 0.26.2",
 ]
 
 [[package]]
@@ -896,7 +896,7 @@ checksum = "b62dbe01f0b06f9d8dc7d49e05a0785f153b00b2c227856282f671e0318c9b15"
 dependencies = [
  "aho-corasick",
  "memchr",
- "regex-automata 0.4.5",
+ "regex-automata 0.4.6",
  "regex-syntax 0.8.2",
 ]
 
@@ -911,9 +911,9 @@ dependencies = [
 
 [[package]]
 name = "regex-automata"
-version = "0.4.5"
+version = "0.4.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5bb987efffd3c6d0d8f5f89510bb458559eab11e4f869acb20bf845e016259cd"
+checksum = "86b83b8b9847f9bf95ef68afb0b8e6cdb80f498442f5179a29fad448fcc1eaea"
 dependencies = [
  "aho-corasick",
  "memchr",
@@ -1079,7 +1079,7 @@ checksum = "e6ecd384b10a64542d77071bd64bd7b231f4ed5940fba55e98c3de13824cf3d7"
 
 [[package]]
 name = "std"
-version = "0.47.0"
+version = "0.48.0"
 dependencies = [
  "kani",
 ]
@@ -1115,9 +1115,9 @@ checksum = "290d54ea6f91c969195bdbcd7442c8c2a2ba87da8bf60a7ee86a235d4bc1e125"
 
 [[package]]
 name = "strum"
-version = "0.26.1"
+version = "0.26.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "723b93e8addf9aa965ebe2d11da6d7540fa2283fcea14b3371ff055f7ba13f5f"
+checksum = "5d8cec3501a5194c432b2b7976db6b7d10ec95c253208b45f83f7136aa985e29"
 
 [[package]]
 name = "strum_macros"
@@ -1134,9 +1134,9 @@ dependencies = [
 
 [[package]]
 name = "strum_macros"
-version = "0.26.1"
+version = "0.26.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7a3417fc93d76740d974a01654a09777cb500428cc874ca9f45edfe0c4d4cd18"
+checksum = "c6cf59daf282c0a494ba14fd21610a0325f9f90ec9d1231dea26bcb1d696c946"
 dependencies = [
  "heck",
  "proc-macro2",
@@ -1219,9 +1219,9 @@ dependencies = [
 
 [[package]]
 name = "toml"
-version = "0.8.10"
+version = "0.8.11"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9a9aad4a3066010876e8dcf5a8a06e70a558751117a145c6ce2b82c2e2054290"
+checksum = "af06656561d28735e9c1cd63dfd57132c8155426aa6af24f36a00a351f88c48e"
 dependencies = [
  "serde",
  "serde_spanned",
@@ -1240,9 +1240,9 @@ dependencies = [
 
 [[package]]
 name = "toml_edit"
-version = "0.22.6"
+version = "0.22.7"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "2c1b5fd4128cc8d3e0cb74d4ed9a9cc7c7284becd4df68f5f940e1ad123606f6"
+checksum = "18769cd1cec395d70860ceb4d932812a0b4d06b1a4bb336745a4d21b9496e992"
 dependencies = [
  "indexmap",
  "serde",

Cargo.toml

@@ -3,7 +3,7 @@
 
 [package]
 name = "kani-verifier"
-version = "0.47.0"
+version = "0.48.0"
 edition = "2021"
 description = "A bit-precise model checker for Rust."
 readme = "README.md"

cprover_bindings/Cargo.toml

@@ -3,7 +3,7 @@
 
 [package]
 name = "cprover_bindings"
-version = "0.47.0"
+version = "0.48.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false

cprover_bindings/src/goto_program/stmt.rs

@@ -57,6 +57,8 @@ pub enum StmtBody {
  Break,
  /// `continue;`
  Continue,
+ /// End-of-life of a local variable
+ Dead(Expr),
  /// `lhs.typ lhs = value;` or `lhs.typ lhs;`
  Decl {
  lhs: Expr, // SymbolExpr
@@ -232,6 +234,11 @@ impl Stmt {
  BuiltinFn::CProverCover.call(vec![cond], loc).as_stmt(loc)
  }
 
+ /// Local variable goes out of scope
+ pub fn dead(symbol: Expr, loc: Location) -> Self {
+ stmt!(Dead(symbol), loc)
+ }
+
  /// `lhs.typ lhs = value;` or `lhs.typ lhs;`
  pub fn decl(lhs: Expr, value: Option<Expr>, loc: Location) -> Self {
  assert!(lhs.is_symbol());

cprover_bindings/src/irep/to_irep.rs

@@ -438,6 +438,7 @@ impl ToIrep for StmtBody {
  }
  StmtBody::Break => code_irep(IrepId::Break, vec![]),
  StmtBody::Continue => code_irep(IrepId::Continue, vec![]),
+ StmtBody::Dead(symbol) => code_irep(IrepId::Dead, vec![symbol.to_irep(mm)]),
  StmtBody::Decl { lhs, value } => {
  if value.is_some() {
  code_irep(

kani-compiler/Cargo.toml

@@ -3,7 +3,7 @@
 
 [package]
 name = "kani-compiler"
-version = "0.47.0"
+version = "0.48.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false

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

@@ -474,6 +474,11 @@ impl<'tcx> GotocCtx<'tcx> {
  let binop_stmt = codegen_intrinsic_binop!(sub);
  self.add_finite_args_checks(intrinsic, fargs_clone, binop_stmt, span)
  }
+ "is_val_statically_known" => {
+ // Returning false is sound according do this intrinsic's documentation:
+ // https://doc.rust-lang.org/nightly/std/intrinsics/fn.is_val_statically_known.html
+ self.codegen_expr_to_place_stable(place, Expr::c_false())
+ }
  "likely" => self.codegen_expr_to_place_stable(place, fargs.remove(0)),
  "log10f32" => unstable_codegen!(codegen_simple_intrinsic!(Log10f)),
  "log10f64" => unstable_codegen!(codegen_simple_intrinsic!(Log10)),
@@ -506,6 +511,7 @@ impl<'tcx> GotocCtx<'tcx> {
  "ptr_offset_from" => self.codegen_ptr_offset_from(fargs, place, loc),
  "ptr_offset_from_unsigned" => self.codegen_ptr_offset_from_unsigned(fargs, place, loc),
  "raw_eq" => self.codegen_intrinsic_raw_eq(instance, fargs, place, loc),
+ "retag_box_to_raw" => self.codegen_retag_box_to_raw(fargs, place, loc),
  "rintf32" => codegen_simple_intrinsic!(Rintf),
  "rintf64" => codegen_simple_intrinsic!(Rint),
  "rotate_left" => codegen_intrinsic_binop!(rol),
@@ -1259,6 +1265,19 @@ impl<'tcx> GotocCtx<'tcx> {
  self.codegen_expr_to_place_stable(p, e)
  }
 
+ // This is an operation that is primarily relevant for stacked borrow
+ // checks. For Kani, we simply return the pointer.
+ fn codegen_retag_box_to_raw(
+ &mut self,
+ mut fargs: Vec<Expr>,
+ p: &Place,
+ _loc: Location,
+ ) -> Stmt {
+ assert_eq!(fargs.len(), 1, "raw_box_to_box expected one argument");
+ let arg = fargs.remove(0);
+ self.codegen_expr_to_place_stable(p, arg)
+ }
+
  fn vtable_info(
  &mut self,
  info: VTableInfo,

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

@@ -381,7 +381,7 @@ impl<'tcx> GotocCtx<'tcx> {
  }
 
  /// Codegen for a local
- fn codegen_local(&mut self, l: Local) -> Expr {
+ pub fn codegen_local(&mut self, l: Local) -> Expr {
  let local_ty = self.local_ty_stable(l);
  // Check if the local is a function definition (see comment above)
  if let Some(fn_def) = self.codegen_local_fndef(local_ty) {

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

@@ -725,7 +725,7 @@ impl<'tcx> GotocCtx<'tcx> {
  .bytes(),
  Type::size_t(),
  ),
- NullOp::DebugAssertions => Expr::c_false(),
+ NullOp::UbCheck(_) => Expr::c_false(),
  }
  }
  Rvalue::ShallowInitBox(ref operand, content_ty) => {

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

@@ -75,8 +75,10 @@ impl<'tcx> GotocCtx<'tcx> {
  .goto_expr;
  self.codegen_set_discriminant(dest_ty, dest_expr, *variant_index, location)
  }
- StatementKind::StorageLive(_) => Stmt::skip(location), // TODO: fix me
- StatementKind::StorageDead(_) => Stmt::skip(location), // TODO: fix me
+ StatementKind::StorageLive(var_id) => {
+ Stmt::decl(self.codegen_local(*var_id), None, location)
+ }
+ StatementKind::StorageDead(var_id) => Stmt::dead(self.codegen_local(*var_id), location),
  StatementKind::Intrinsic(NonDivergingIntrinsic::CopyNonOverlapping(
  CopyNonOverlapping { src, dst, count },
  )) => {

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

@@ -542,6 +542,9 @@ impl<'tcx> GotocCtx<'tcx> {
  ty::Float(k) => match k {
  FloatTy::F32 => Type::float(),
  FloatTy::F64 => Type::double(),
+ // `F16` and `F128` are not yet handled.
+ // Tracked here: <https://github.com/model-checking/kani/issues/3069>
+ FloatTy::F16 | FloatTy::F128 => unimplemented!(),
  },
  ty::Adt(def, _) if def.repr().simd() => self.codegen_vector(ty),
  ty::Adt(def, subst) => {
@@ -1346,6 +1349,9 @@ impl<'tcx> GotocCtx<'tcx> {
 
  Primitive::F32 => self.tcx.types.f32,
  Primitive::F64 => self.tcx.types.f64,
+ // `F16` and `F128` are not yet handled.
+ // Tracked here: <https://github.com/model-checking/kani/issues/3069>
+ Primitive::F16 | Primitive::F128 => unimplemented!(),
  Primitive::Pointer(_) => Ty::new_ptr(
  self.tcx,
  ty::TypeAndMut { ty: self.tcx.types.u8, mutbl: Mutability::Not },

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -397,7 +397,7 @@ impl CodegenBackend for GotocCodegenBackend {
  let path = MaybeTempDir::new(tmp_dir, sess.opts.cg.save_temps);
  let (metadata, _metadata_position) = create_wrapper_file(
  sess,
- b".rmeta".to_vec(),
+ ".rmeta".to_string(),
  codegen_results.metadata.raw_data(),
  );
  let metadata = emit_wrapper_file(sess, &metadata, &path, METADATA_FILENAME);