From 8b89160fc35881fbc876958d52e9dbee81636eb2 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Wed, 28 Jun 2023 15:11:27 -0700
Subject: [PATCH 01/14] Fix dev-documentation broken link (#2575)

Fix broken link introduced by #1138 and add a link to Coding conventions.
---
 docs/src/dev-documentation.md | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/docs/src/dev-documentation.md b/docs/src/dev-documentation.md
index d480c4340d19..639b7125ae78 100644
--- a/docs/src/dev-documentation.md
+++ b/docs/src/dev-documentation.md
@@ -9,10 +9,11 @@ we recommend looking into [these issues](https://github.com/model-checking/kani/
 
 In this chapter, we provide documentation that might be helpful for Kani
 developers (including external contributors):
- 1. [Suggested workarounds](./workarounds.md).
+ 1. [Coding conventions](./conventions.md).
  2. [Useful command-line instructions for Kani/CBMC/Git](./cheat-sheets.md).
- 3. [Development setup recommendations for working with `rustc`](./rustc-hacks.md).
- 4. [Guide for testing in Kani](./testing.md).
+ 3. [Development setup recommendations for working with `cbmc`](./cbmc-hacks.md).
+ 4. [Development setup recommendations for working with `rustc`](./rustc-hacks.md).
+ 5. [Guide for testing in Kani](./testing.md).
 
 > **NOTE**: The developer documentation is intended for Kani developers and not
 users. At present, the project is under heavy development and some items

From 713906371b45905ff44f3bc44d919755f61cda11 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Tue, 4 Jul 2023 10:50:10 -0700
Subject: [PATCH 02/14] Upgrade rust toolchain to nightly-2023-06-20 (#2551)

Change Kani's compiler and tests to adapt to changes done to the toolchain. The biggest changes were:

Implement overflow checks as part of rvalue.rs instead of intrinsics due to lowering of intrinsics to BinOp.
Add a unsupported check for handling C string literals.


Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
---
 .../codegen/intrinsic.rs                      |  70 +----------
 .../codegen_cprover_gotoc/codegen/operand.rs  |  13 ++
 .../codegen_cprover_gotoc/codegen/rvalue.rs   | 116 +++++++++++++++++-
 .../codegen/statement.rs                      |   6 +-
 .../src/codegen_cprover_gotoc/codegen/typ.rs  |  10 +-
 .../compiler_interface.rs                     |  33 ++---
 .../codegen_cprover_gotoc/context/goto_ctx.rs |   4 +-
 kani-compiler/src/kani_middle/attributes.rs   |   7 +-
 kani-compiler/src/kani_middle/coercion.rs     |  10 +-
 kani-compiler/src/kani_middle/mod.rs          |   6 +-
 kani-compiler/src/kani_middle/provide.rs      |   9 +-
 kani-compiler/src/kani_middle/reachability.rs |   8 +-
 rust-toolchain.toml                           |   2 +-
 ...igned.expected => check_unsigned.expected} |   0
 tests/cargo-kani/itoa_dep/src/main.rs         |   8 ++
 tests/expected/slice_c_str/c_str.rs           |  22 ++++
 tests/expected/slice_c_str/expected           |   7 ++
 tests/perf/format/Cargo.toml                  |  11 ++
 tests/perf/format/expected                    |   1 +
 tests/perf/format/src/lib.rs                  |  20 +++
 .../arithmetic_overflow/expected              |   6 +-
 tests/ui/code-location/expected               |   2 +-
 tests/ui/duplicates/dup_checks.rs             |  19 +++
 tests/ui/duplicates/expected                  |  49 ++++++++
 24 files changed, 325 insertions(+), 114 deletions(-)
 rename tests/cargo-kani/itoa_dep/{check_signed.expected => check_unsigned.expected} (100%)
 create mode 100644 tests/expected/slice_c_str/c_str.rs
 create mode 100644 tests/expected/slice_c_str/expected
 create mode 100644 tests/perf/format/Cargo.toml
 create mode 100644 tests/perf/format/expected
 create mode 100644 tests/perf/format/src/lib.rs
 create mode 100644 tests/ui/duplicates/dup_checks.rs
 create mode 100644 tests/ui/duplicates/expected

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index 8c6674d26f26..4bd5566f9d7c 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -5,8 +5,7 @@ use super::typ::{self, pointee_type};
 use super::PropertyClass;
 use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::{
-    arithmetic_overflow_result_type, ArithmeticOverflowResult, BinaryOperator, BuiltinFn, Expr,
-    Location, Stmt, Type, ARITH_OVERFLOW_OVERFLOWED_FIELD, ARITH_OVERFLOW_RESULT_FIELD,
+    ArithmeticOverflowResult, BinaryOperator, BuiltinFn, Expr, Location, Stmt, Type,
 };
 use rustc_middle::mir::{BasicBlock, Operand, Place};
 use rustc_middle::ty::layout::{LayoutOf, ValidityRequirement};
@@ -183,43 +182,6 @@ impl<'tcx> GotocCtx<'tcx> {
             }};
         }
 
-        // Intrinsics which encode a simple arithmetic operation with overflow check
-        macro_rules! codegen_op_with_overflow_check {
-            ($f:ident) => {{
-                let a = fargs.remove(0);
-                let b = fargs.remove(0);
-                let op_type = a.typ().clone();
-                let res = a.$f(b);
-                // add to symbol table
-                let struct_tag = self.codegen_arithmetic_overflow_result_type(op_type.clone());
-                assert_eq!(*res.typ(), struct_tag);
-
-                // store the result in a temporary variable
-                let (var, decl) = self.decl_temp_variable(struct_tag, Some(res), loc);
-                let check = self.codegen_assert(
-                    var.clone()
-                        .member(ARITH_OVERFLOW_OVERFLOWED_FIELD, &self.symbol_table)
-                        .cast_to(Type::c_bool())
-                        .not(),
-                    PropertyClass::ArithmeticOverflow,
-                    format!("attempt to compute {} which would overflow", intrinsic).as_str(),
-                    loc,
-                );
-                self.codegen_expr_to_place(
-                    p,
-                    Expr::statement_expression(
-                        vec![
-                            decl,
-                            check,
-                            var.member(ARITH_OVERFLOW_RESULT_FIELD, &self.symbol_table)
-                                .as_stmt(loc),
-                        ],
-                        op_type,
-                    ),
-                )
-            }};
-        }
-
         // Intrinsics which encode a division operation with overflow check
         macro_rules! codegen_op_with_div_overflow_check {
             ($f:ident) => {{
@@ -617,19 +579,12 @@ impl<'tcx> GotocCtx<'tcx> {
             "unaligned_volatile_load" => {
                 unstable_codegen!(self.codegen_expr_to_place(p, fargs.remove(0).dereference()))
             }
-            "unchecked_add" => codegen_op_with_overflow_check!(add_overflow_result),
+            "unchecked_add" | "unchecked_mul" | "unchecked_shl" | "unchecked_shr"
+            | "unchecked_sub" => {
+                unreachable!("Expected intrinsic `{intrinsic}` to be lowered before codegen")
+            }
             "unchecked_div" => codegen_op_with_div_overflow_check!(div),
-            "unchecked_mul" => codegen_op_with_overflow_check!(mul_overflow_result),
             "unchecked_rem" => codegen_op_with_div_overflow_check!(rem),
-            "unchecked_shl" => codegen_intrinsic_binop!(shl),
-            "unchecked_shr" => {
-                if fargs[0].typ().is_signed(self.symbol_table.machine_model()) {
-                    codegen_intrinsic_binop!(ashr)
-                } else {
-                    codegen_intrinsic_binop!(lshr)
-                }
-            }
-            "unchecked_sub" => codegen_op_with_overflow_check!(sub_overflow_result),
             "unlikely" => self.codegen_expr_to_place(p, fargs.remove(0)),
             "unreachable" => unreachable!(
                 "Expected `std::intrinsics::unreachable` to be handled by `TerminatorKind::Unreachable`"
@@ -1808,19 +1763,4 @@ impl<'tcx> GotocCtx<'tcx> {
         );
         (size_of_count_elems.result, assert_stmt)
     }
-
-    /// Codegens the struct type that CBMC produces for its arithmetic with overflow operators:
-    /// ```
-    /// struct overflow_result_<operand_type> {
-    ///     operand_type result;     // the result of the operation
-    ///     bool         overflowed; // whether the operation overflowed
-    /// }
-    /// ```
-    /// and adds the type to the symbol table
-    fn codegen_arithmetic_overflow_result_type(&mut self, operand_type: Type) -> Type {
-        let res_type = arithmetic_overflow_result_type(operand_type);
-        self.ensure_struct(res_type.tag().unwrap(), res_type.tag().unwrap(), |_, _| {
-            res_type.components().unwrap().clone()
-        })
-    }
 }
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
index a756a42b0388..23211f022b23 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
@@ -227,6 +227,19 @@ impl<'tcx> GotocCtx<'tcx> {
                         );
                     }
                 }
+                ty::Adt(def, _) if Some(def.did()) == self.tcx.lang_items().c_str() => {
+                    // TODO: Handle CString
+                    // <https://github.com/model-checking/kani/issues/2549>
+                    let loc = self.codegen_span_option(span.cloned());
+                    let typ = self.codegen_ty(lit_ty);
+                    let operation_name = "C string literal";
+                    return self.codegen_unimplemented_expr(
+                        &operation_name,
+                        typ,
+                        loc,
+                        "https://github.com/model-checking/kani/issues/2549",
+                    );
+                }
                 _ => {}
             }
         }
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index 8a652f0833e1..22b26a3489b4 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -163,6 +163,52 @@ impl<'tcx> GotocCtx<'tcx> {
         }
     }
 
+    /// Generate code for a binary operation with an overflow check.
+    fn codegen_binop_with_overflow_check(
+        &mut self,
+        op: &BinOp,
+        left_op: &Operand<'tcx>,
+        right_op: &Operand<'tcx>,
+        loc: Location,
+    ) -> Expr {
+        debug!(?op, "codegen_binop_with_overflow_check");
+        let left = self.codegen_operand(left_op);
+        let right = self.codegen_operand(right_op);
+        let ret_type = left.typ().clone();
+        let (bin_op, op_name) = match op {
+            BinOp::AddUnchecked => (BinaryOperator::OverflowResultPlus, "unchecked_add"),
+            BinOp::SubUnchecked => (BinaryOperator::OverflowResultMinus, "unchecked_sub"),
+            BinOp::MulUnchecked => (BinaryOperator::OverflowResultMult, "unchecked_mul"),
+            _ => unreachable!("Expected Add/Sub/Mul but got {op:?}"),
+        };
+        // Create CBMC result type and add to the symbol table.
+        let res_type = arithmetic_overflow_result_type(left.typ().clone());
+        let tag = res_type.tag().unwrap();
+        let struct_tag =
+            self.ensure_struct(tag, tag, |_, _| res_type.components().unwrap().clone());
+        let res = left.overflow_op(bin_op, right);
+        // store the result in a temporary variable
+        let (var, decl) = self.decl_temp_variable(struct_tag, Some(res), loc);
+        // cast into result type
+        let check = self.codegen_assert(
+            var.clone()
+                .member(ARITH_OVERFLOW_OVERFLOWED_FIELD, &self.symbol_table)
+                .cast_to(Type::c_bool())
+                .not(),
+            PropertyClass::ArithmeticOverflow,
+            format!("attempt to compute `{op_name}` which would overflow").as_str(),
+            loc,
+        );
+        Expr::statement_expression(
+            vec![
+                decl,
+                check,
+                var.member(ARITH_OVERFLOW_RESULT_FIELD, &self.symbol_table).as_stmt(loc),
+            ],
+            ret_type,
+        )
+    }
+
     /// Generate code for a binary operation with an overflow and returns a tuple (res, overflow).
     pub fn codegen_binop_with_overflow(
         &mut self,
@@ -297,7 +343,28 @@ impl<'tcx> GotocCtx<'tcx> {
             BinOp::Add | BinOp::Sub | BinOp::Mul | BinOp::Shl | BinOp::Shr => {
                 self.codegen_scalar_binop(op, e1, e2)
             }
-            BinOp::Div | BinOp::Rem | BinOp::BitXor | BinOp::BitAnd | BinOp::BitOr => {
+            // We currently rely on CBMC's UB checks for shift which isn't always accurate.
+            // We should implement the checks ourselves.
+            // See https://github.com/model-checking/kani/issues/2374
+            BinOp::ShlUnchecked => self.codegen_scalar_binop(&BinOp::Shl, e1, e2),
+            BinOp::ShrUnchecked => self.codegen_scalar_binop(&BinOp::Shr, e1, e2),
+            BinOp::AddUnchecked | BinOp::MulUnchecked | BinOp::SubUnchecked => {
+                self.codegen_binop_with_overflow_check(op, e1, e2, loc)
+            }
+            BinOp::Div | BinOp::Rem => {
+                let result = self.codegen_unchecked_scalar_binop(op, e1, e2);
+                if self.operand_ty(e1).is_integral() {
+                    let is_rem = matches!(op, BinOp::Rem);
+                    let check = self.check_div_overflow(e1, e2, is_rem, loc);
+                    Expr::statement_expression(
+                        vec![check, result.clone().as_stmt(loc)],
+                        result.typ().clone(),
+                    )
+                } else {
+                    result
+                }
+            }
+            BinOp::BitXor | BinOp::BitAnd | BinOp::BitOr => {
                 self.codegen_unchecked_scalar_binop(op, e1, e2)
             }
             BinOp::Eq | BinOp::Lt | BinOp::Le | BinOp::Ne | BinOp::Ge | BinOp::Gt => {
@@ -341,6 +408,53 @@ impl<'tcx> GotocCtx<'tcx> {
         }
     }
 
+    /// Check that a division does not overflow.
+    /// For integer types, division by zero is UB, as is MIN / -1 for signed.
+    /// Note that the compiler already inserts these checks for regular division.
+    /// However, since <https://github.com/rust-lang/rust/pull/112168>, unchecked divisions are
+    /// lowered to `BinOp::Div`. Prefer adding duplicated checks for now.
+    fn check_div_overflow(
+        &mut self,
+        dividend: &Operand<'tcx>,
+        divisor: &Operand<'tcx>,
+        is_remainder: bool,
+        loc: Location,
+    ) -> Stmt {
+        let divisor_expr = self.codegen_operand(divisor);
+        let msg = if is_remainder {
+            "attempt to calculate the remainder with a divisor of zero"
+        } else {
+            "attempt to divide by zero"
+        };
+        let div_by_zero_check = self.codegen_assert_assume(
+            divisor_expr.clone().is_zero().not(),
+            PropertyClass::ArithmeticOverflow,
+            msg,
+            loc,
+        );
+        if self.operand_ty(dividend).is_signed() {
+            let dividend_expr = self.codegen_operand(dividend);
+            let overflow_msg = if is_remainder {
+                "attempt to calculate the remainder with overflow"
+            } else {
+                "attempt to divide with overflow"
+            };
+            let overflow_expr = dividend_expr
+                .clone()
+                .eq(dividend_expr.typ().min_int_expr(self.symbol_table.machine_model()))
+                .and(divisor_expr.clone().eq(Expr::int_constant(-1, divisor_expr.typ().clone())));
+            let overflow_check = self.codegen_assert_assume(
+                overflow_expr.not(),
+                PropertyClass::ArithmeticOverflow,
+                overflow_msg,
+                loc,
+            );
+            Stmt::block(vec![overflow_check, div_by_zero_check], loc)
+        } else {
+            div_by_zero_check
+        }
+    }
+
     /// Create an initializer for a generator struct.
     fn codegen_rvalue_generator(
         &mut self,
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
index 18f510dc7a56..fbabe7e112cd 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -149,7 +149,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 "unreachable code",
                 loc,
             ),
-            TerminatorKind::Drop { place, target, unwind: _ } => {
+            TerminatorKind::Drop { place, target, unwind: _, replace: _ } => {
                 self.codegen_drop(place, target, loc)
             }
             TerminatorKind::Call { func, args, destination, target, .. } => {
@@ -161,12 +161,12 @@ impl<'tcx> GotocCtx<'tcx> {
                     if *expected { r } else { Expr::not(r) }
                 };
 
-                let msg = if let AssertKind::BoundsCheck { .. } = msg {
+                let msg = if let AssertKind::BoundsCheck { .. } = &**msg {
                     // For bounds check the following panic message is generated at runtime:
                     // "index out of bounds: the length is {len} but the index is {index}",
                     // but CBMC only accepts static messages so we don't add values to the message.
                     "index out of bounds: the length is less than or equal to the given index"
-                } else if let AssertKind::MisalignedPointerDereference { .. } = msg {
+                } else if let AssertKind::MisalignedPointerDereference { .. } = &**msg {
                     // Misaligned pointer dereference check messages is also a runtime messages.
                     // Generate a generic one here.
                     "misaligned pointer dereference: address must be a multiple of its type's alignment"
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
index 955edb615bd6..69da5f1c7ad1 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -303,7 +303,7 @@ impl<'tcx> GotocCtx<'tcx> {
             var: ty::BoundVar::from_usize(bound_vars.len() - 1),
             kind: ty::BoundRegionKind::BrEnv,
         };
-        let env_region = self.tcx.mk_re_late_bound(ty::INNERMOST, br);
+        let env_region = ty::Region::new_late_bound(self.tcx, ty::INNERMOST, br);
         let env_ty = self.tcx.closure_env_ty(def_id, substs, env_region).unwrap();
 
         let sig = sig.skip_binder();
@@ -345,7 +345,7 @@ impl<'tcx> GotocCtx<'tcx> {
             kind: ty::BoundRegionKind::BrEnv,
         };
         let env_region = ty::ReLateBound(ty::INNERMOST, br);
-        let env_ty = self.tcx.mk_mut_ref(self.tcx.mk_region_from_kind(env_region), ty);
+        let env_ty = self.tcx.mk_mut_ref(ty::Region::new_from_kind(self.tcx, env_region), ty);
 
         let pin_did = self.tcx.require_lang_item(LangItem::Pin, None);
         let pin_adt_ref = self.tcx.adt_def(pin_did);
@@ -429,7 +429,7 @@ impl<'tcx> GotocCtx<'tcx> {
             current_fn.instance().subst_mir_and_normalize_erasing_regions(
                 self.tcx,
                 ty::ParamEnv::reveal_all(),
-                value,
+                ty::EarlyBinder::bind(value),
             )
         } else {
             // TODO: confirm with rust team there is no way to monomorphize
@@ -665,8 +665,8 @@ impl<'tcx> GotocCtx<'tcx> {
             }
             _ => {
                 // This hash is documented to be the same no matter the crate context
-                let id_u64 = self.tcx.type_id_hash(t).as_u64();
-                format!("_{id_u64}").intern()
+                let id = self.tcx.type_id_hash(t).as_u128();
+                format!("_{id}").intern()
             }
         }
     }
diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
index 985cbe1efc47..a89e5035f2a2 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
@@ -27,7 +27,7 @@ use rustc_codegen_ssa::back::archive::{
 use rustc_codegen_ssa::back::metadata::create_wrapper_file;
 use rustc_codegen_ssa::traits::CodegenBackend;
 use rustc_codegen_ssa::{CodegenResults, CrateInfo};
-use rustc_data_structures::fx::FxHashMap;
+use rustc_data_structures::fx::{FxHashMap, FxIndexMap};
 use rustc_data_structures::temp_dir::MaybeTempDir;
 use rustc_errors::{ErrorGuaranteed, DEFAULT_LOCALE_RESOURCE};
 use rustc_hir::def_id::LOCAL_CRATE;
@@ -36,8 +36,8 @@ use rustc_metadata::fs::{emit_wrapper_file, METADATA_FILENAME};
 use rustc_metadata::EncodedMetadata;
 use rustc_middle::dep_graph::{WorkProduct, WorkProductId};
 use rustc_middle::mir::mono::MonoItem;
-use rustc_middle::ty::query::Providers;
-use rustc_middle::ty::{self, TyCtxt};
+use rustc_middle::query::{ExternProviders, Providers};
+use rustc_middle::ty::TyCtxt;
 use rustc_session::config::{CrateType, OutputFilenames, OutputType};
 use rustc_session::cstore::MetadataLoaderDyn;
 use rustc_session::output::out_filename;
@@ -192,7 +192,7 @@ impl CodegenBackend for GotocCodegenBackend {
         provide::provide(providers, &self.queries.lock().unwrap());
     }
 
-    fn provide_extern(&self, providers: &mut ty::query::ExternProviders) {
+    fn provide_extern(&self, providers: &mut ExternProviders) {
         provide::provide_extern(providers);
     }
 
@@ -317,10 +317,12 @@ impl CodegenBackend for GotocCodegenBackend {
         ongoing_codegen: Box<dyn Any>,
         _sess: &Session,
         _filenames: &OutputFilenames,
-    ) -> Result<(CodegenResults, FxHashMap<WorkProductId, WorkProduct>), ErrorGuaranteed> {
-        Ok(*ongoing_codegen
-            .downcast::<(CodegenResults, FxHashMap<WorkProductId, WorkProduct>)>()
-            .unwrap())
+    ) -> Result<(CodegenResults, FxIndexMap<WorkProductId, WorkProduct>), ErrorGuaranteed> {
+        match ongoing_codegen.downcast::<(CodegenResults, FxIndexMap<WorkProductId, WorkProduct>)>()
+        {
+            Ok(val) => Ok(*val),
+            Err(val) => panic!("unexpected error: {:?}", val.type_id()),
+        }
     }
 
     /// Emit output files during the link stage if it was requested.
@@ -345,12 +347,13 @@ impl CodegenBackend for GotocCodegenBackend {
     ) -> Result<(), ErrorGuaranteed> {
         let requested_crate_types = sess.crate_types();
         for crate_type in requested_crate_types {
-            let out_path = out_filename(
+            let out_fname = out_filename(
                 sess,
                 *crate_type,
                 outputs,
                 codegen_results.crate_info.local_crate_name,
             );
+            let out_path = out_fname.as_path();
             debug!(?crate_type, ?out_path, "link");
             if *crate_type == CrateType::Rlib {
                 // Emit the `rlib` that contains just one file: `<crate>.rmeta`
@@ -396,7 +399,7 @@ fn check_target(session: &Session) {
             `x86_64-apple-*` or `arm64-apple-*`, but it is {}",
             &session.target.llvm_target
         );
-        session.err(&err_msg);
+        session.err(err_msg);
     }
 
     session.abort_if_errors();
@@ -412,7 +415,7 @@ fn check_options(session: &Session) {
             let err_msg = format!(
                 "Kani requires the target architecture option `min_global_align` to be 1, but it is {align}."
             );
-            session.err(&err_msg);
+            session.err(err_msg);
         }
         _ => (),
     }
@@ -441,7 +444,7 @@ fn codegen_results(
     rustc_metadata: EncodedMetadata,
     machine: &MachineModel,
 ) -> Box<dyn Any> {
-    let work_products = FxHashMap::<WorkProductId, WorkProduct>::default();
+    let work_products = FxIndexMap::<WorkProductId, WorkProduct>::default();
     Box::new((
         CodegenResults {
             modules: vec![],
@@ -482,7 +485,7 @@ fn symbol_table_to_gotoc(tcx: &TyCtxt, base_path: &Path) -> PathBuf {
             "Failed to generate goto model:\n\tsymtab2gb failed on file {}.",
             input_filename.display()
         );
-        tcx.sess.err(&err_msg);
+        tcx.sess.err(err_msg);
         tcx.sess.abort_if_errors();
     };
     output_filename
@@ -591,7 +594,7 @@ impl<'tcx> GotoCodegenResults<'tcx> {
             msg += "\nVerification will fail if one or more of these constructs is reachable.";
             msg += "\nSee https://model-checking.github.io/kani/rust-feature-support.html for more \
             details.";
-            tcx.sess.warn(&msg);
+            tcx.sess.warn(msg);
         }
 
         if !self.concurrent_constructs.is_empty() {
@@ -602,7 +605,7 @@ impl<'tcx> GotoCodegenResults<'tcx> {
             for (construct, locations) in self.concurrent_constructs.iter() {
                 writeln!(&mut msg, "    - {construct} ({})", locations.len()).unwrap();
             }
-            tcx.sess.warn(&msg);
+            tcx.sess.warn(msg);
         }
 
         // Print some compilation stats.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
index 836444a78165..dd43c96f27ea 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
@@ -377,13 +377,13 @@ impl<'tcx> FnAbiOfHelpers<'tcx> for GotocCtx<'tcx> {
                 FnAbiRequest::OfFnPtr { sig, extra_args } => {
                     span_bug!(
                         span,
-                        "Error: {err}\n while running `fn_abi_of_fn_ptr. ({sig}, {extra_args:?})`",
+                        "Error: {err:?}\n while running `fn_abi_of_fn_ptr. ({sig}, {extra_args:?})`",
                     );
                 }
                 FnAbiRequest::OfInstance { instance, extra_args } => {
                     span_bug!(
                         span,
-                        "Error: {err}\n while running `fn_abi_of_instance. ({instance}, {extra_args:?})`",
+                        "Error: {err:?}\n while running `fn_abi_of_instance. ({instance}, {extra_args:?})`",
                     );
                 }
             }
diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs
index 24726e0f9655..6ee5136e12e5 100644
--- a/kani-compiler/src/kani_middle/attributes.rs
+++ b/kani-compiler/src/kani_middle/attributes.rs
@@ -58,8 +58,7 @@ pub(super) fn check_attributes(tcx: TyCtxt, def_id: DefId) {
                 format!(
                     "the `{}` attribute also requires the `#[kani::proof]` attribute",
                     kind.as_ref()
-                )
-                .as_str(),
+                ),
             );
         }
         match kind {
@@ -147,7 +146,7 @@ pub fn extract_harness_attributes(tcx: TyCtxt, def_id: DefId) -> HarnessAttribut
 ///
 /// TODO: Improve error message by printing the span of the harness instead of the definition.
 pub fn check_unstable_features(tcx: TyCtxt, enabled_features: &[String], def_id: DefId) {
-    if !matches!(tcx.type_of(def_id).0.kind(), TyKind::FnDef(..)) {
+    if !matches!(tcx.type_of(def_id).skip_binder().kind(), TyKind::FnDef(..)) {
         // skip closures due to an issue with rustc.
         // https://github.com/model-checking/kani/pull/2406#issuecomment-1534333862
         return;
@@ -195,7 +194,7 @@ fn expect_single<'a>(
     if attributes.len() > 1 {
         tcx.sess.span_err(
             attr.span,
-            &format!("only one '#[kani::{}]' attribute is allowed per harness", kind.as_ref()),
+            format!("only one '#[kani::{}]' attribute is allowed per harness", kind.as_ref()),
         );
     }
     attr
diff --git a/kani-compiler/src/kani_middle/coercion.rs b/kani-compiler/src/kani_middle/coercion.rs
index 3c87a8173b3f..42f3cfb0a702 100644
--- a/kani-compiler/src/kani_middle/coercion.rs
+++ b/kani-compiler/src/kani_middle/coercion.rs
@@ -16,8 +16,8 @@
 use rustc_hir::lang_items::LangItem;
 use rustc_middle::traits::{ImplSource, ImplSourceUserDefinedData};
 use rustc_middle::ty::adjustment::CustomCoerceUnsized;
-use rustc_middle::ty::TypeAndMut;
 use rustc_middle::ty::{self, ParamEnv, Ty, TyCtxt};
+use rustc_middle::ty::{TraitRef, TypeAndMut};
 use rustc_span::symbol::Symbol;
 use tracing::trace;
 
@@ -213,9 +213,11 @@ fn custom_coerce_unsize_info<'tcx>(
 ) -> CustomCoerceUnsized {
     let def_id = tcx.require_lang_item(LangItem::CoerceUnsized, None);
 
-    let trait_ref = ty::Binder::dummy(
-        tcx.mk_trait_ref(def_id, tcx.mk_substs_trait(source_ty, [target_ty.into()])),
-    );
+    let trait_ref = ty::Binder::dummy(TraitRef::new(
+        tcx,
+        def_id,
+        tcx.mk_substs_trait(source_ty, [target_ty.into()]),
+    ));
 
     match tcx.codegen_select_candidate((ParamEnv::reveal_all(), trait_ref)) {
         Ok(ImplSource::UserDefined(ImplSourceUserDefinedData { impl_def_id, .. })) => {
diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs
index fc60c0cc1a14..ba235db26805 100644
--- a/kani-compiler/src/kani_middle/mod.rs
+++ b/kani-compiler/src/kani_middle/mod.rs
@@ -51,7 +51,7 @@ pub fn check_crate_items(tcx: TyCtxt, ignore_asm: bool) {
                     `--enable-unstable --ignore-global-asm` to suppress this error \
                     (**Verification results may be impacted**).",
                 );
-                tcx.sess.err(&error_msg);
+                tcx.sess.err(error_msg);
             } else {
                 tcx.sess.warn(format!(
                     "Ignoring global ASM in crate {krate}. Verification results may be impacted.",
@@ -192,13 +192,13 @@ impl<'tcx> FnAbiOfHelpers<'tcx> for CompilerHelpers<'tcx> {
                 FnAbiRequest::OfFnPtr { sig, extra_args } => {
                     span_bug!(
                         span,
-                        "Error: {err}\n while running `fn_abi_of_fn_ptr. ({sig}, {extra_args:?})`",
+                        "Error: {err:?}\n while running `fn_abi_of_fn_ptr. ({sig}, {extra_args:?})`",
                     );
                 }
                 FnAbiRequest::OfInstance { instance, extra_args } => {
                     span_bug!(
                         span,
-                        "Error: {err}\n while running `fn_abi_of_instance. ({instance}, {extra_args:?})`",
+                        "Error: {err:?}\n while running `fn_abi_of_instance. ({instance}, {extra_args:?})`",
                     );
                 }
             }
diff --git a/kani-compiler/src/kani_middle/provide.rs b/kani-compiler/src/kani_middle/provide.rs
index a3a0a37f6a2e..bdca51f43129 100644
--- a/kani-compiler/src/kani_middle/provide.rs
+++ b/kani-compiler/src/kani_middle/provide.rs
@@ -6,13 +6,13 @@
 
 use crate::kani_middle::reachability::{collect_reachable_items, filter_crate_items};
 use crate::kani_middle::stubbing;
-use crate::kani_middle::ty::query::query_provided::collect_and_partition_mono_items;
 use crate::kani_queries::QueryDb;
 use rustc_hir::def_id::{DefId, LocalDefId};
 use rustc_interface;
 use rustc_middle::{
     mir::Body,
-    ty::{query::ExternProviders, query::Providers, TyCtxt},
+    query::{queries, ExternProviders, Providers},
+    ty::TyCtxt,
 };
 
 /// Sets up rustc's query mechanism to apply Kani's custom queries to code from
@@ -65,7 +65,10 @@ fn run_kani_mir_passes<'tcx>(
 /// This is an issue when compiling a library, since the crate metadata is
 /// generated (using this query) before code generation begins (which is
 /// when we normally run the reachability analysis).
-fn collect_and_partition_mono_items(tcx: TyCtxt, key: ()) -> collect_and_partition_mono_items {
+fn collect_and_partition_mono_items(
+    tcx: TyCtxt,
+    key: (),
+) -> queries::collect_and_partition_mono_items::ProvidedValue {
     let entry_fn = tcx.entry_fn(()).map(|(id, _)| id);
     let local_reachable = filter_crate_items(tcx, |_, def_id| {
         tcx.is_reachable_non_generic(def_id) || entry_fn == Some(def_id)
diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs
index 4d32a09f7d28..a3110426dc57 100644
--- a/kani-compiler/src/kani_middle/reachability.rs
+++ b/kani-compiler/src/kani_middle/reachability.rs
@@ -30,8 +30,8 @@ use rustc_middle::mir::{
 use rustc_middle::span_bug;
 use rustc_middle::ty::adjustment::PointerCast;
 use rustc_middle::ty::{
-    Closure, ClosureKind, ConstKind, Instance, InstanceDef, ParamEnv, Ty, TyCtxt, TyKind,
-    TypeFoldable, VtblEntry,
+    Closure, ClosureKind, ConstKind, EarlyBinder, Instance, InstanceDef, ParamEnv, Ty, TyCtxt,
+    TyKind, TypeFoldable, VtblEntry,
 };
 
 use crate::kani_middle::coercion;
@@ -243,7 +243,7 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> {
         self.instance.subst_mir_and_normalize_erasing_regions(
             self.tcx,
             ParamEnv::reveal_all(),
-            value,
+            EarlyBinder::bind(value),
         )
     }
 
@@ -483,7 +483,7 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> {
                                 let receiver_ty = tcx.subst_and_normalize_erasing_regions(
                                     substs,
                                     ParamEnv::reveal_all(),
-                                    generic_ty,
+                                    EarlyBinder::bind(generic_ty),
                                 );
                                 let sep = callee.rfind("::").unwrap();
                                 let trait_ = &callee[..sep];
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index 0015b8619839..e1e134733598 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2023-04-30"
+channel = "nightly-2023-06-20"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
diff --git a/tests/cargo-kani/itoa_dep/check_signed.expected b/tests/cargo-kani/itoa_dep/check_unsigned.expected
similarity index 100%
rename from tests/cargo-kani/itoa_dep/check_signed.expected
rename to tests/cargo-kani/itoa_dep/check_unsigned.expected
diff --git a/tests/cargo-kani/itoa_dep/src/main.rs b/tests/cargo-kani/itoa_dep/src/main.rs
index 9bda87de7339..c2d1a165a409 100644
--- a/tests/cargo-kani/itoa_dep/src/main.rs
+++ b/tests/cargo-kani/itoa_dep/src/main.rs
@@ -17,10 +17,18 @@ fn check_itoa<T: kani::Arbitrary + Integer + std::fmt::Display>() {
     assert_eq!(result, &output);
 }
 
+/// Note: We ignore this harness for now due to a performance regression.
+/// See <https://github.com/model-checking/kani/issues/2576> for more details.
 #[kani::proof]
 #[kani::unwind(10)]
 fn check_signed() {
     check_itoa::<i8>();
 }
 
+#[kani::proof]
+#[kani::unwind(10)]
+fn check_unsigned() {
+    check_itoa::<u8>();
+}
+
 fn main() {}
diff --git a/tests/expected/slice_c_str/c_str.rs b/tests/expected/slice_c_str/c_str.rs
new file mode 100644
index 000000000000..9fa2feedc6ea
--- /dev/null
+++ b/tests/expected/slice_c_str/c_str.rs
@@ -0,0 +1,22 @@
+#![feature(rustc_private)]
+#![feature(c_str_literals)]
+
+extern crate libc;
+use libc::c_char;
+
+#[kani::proof]
+fn check_c_str() {
+    assert_eq!(unsafe { *empty_c_str() }, 0);
+    let (s, len) = non_empty_c_str();
+    assert_ne!(unsafe { *s.offset(0) }, 0);
+    assert_eq!(unsafe { *s.offset(len as isize) }, 0);
+}
+
+fn empty_c_str() -> *const c_char {
+    c"".as_ptr() as *const c_char
+}
+
+/// Return a C string and its length (without the null character).
+fn non_empty_c_str() -> (*const c_char, usize) {
+    (c"hi".as_ptr() as *const c_char, 2)
+}
diff --git a/tests/expected/slice_c_str/expected b/tests/expected/slice_c_str/expected
new file mode 100644
index 000000000000..2138044e5b88
--- /dev/null
+++ b/tests/expected/slice_c_str/expected
@@ -0,0 +1,7 @@
+warning: Found the following unsupported constructs:
+- C string literal
+
+Checking harness check_c_str...
+Failed Checks: C string literal is not currently supported by Kani.
+
+VERIFICATION:- FAILED
diff --git a/tests/perf/format/Cargo.toml b/tests/perf/format/Cargo.toml
new file mode 100644
index 000000000000..3fe392e07c04
--- /dev/null
+++ b/tests/perf/format/Cargo.toml
@@ -0,0 +1,11 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "format"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
diff --git a/tests/perf/format/expected b/tests/perf/format/expected
new file mode 100644
index 000000000000..44572d1c72bf
--- /dev/null
+++ b/tests/perf/format/expected
@@ -0,0 +1 @@
+Complete - 2 successfully verified harnesses, 0 failures, 2 total
diff --git a/tests/perf/format/src/lib.rs b/tests/perf/format/src/lib.rs
new file mode 100644
index 000000000000..1986a08222ba
--- /dev/null
+++ b/tests/perf/format/src/lib.rs
@@ -0,0 +1,20 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test checks the performance of calling format.
+//! This test captures the performance regression introduced by the toolchain upgrade in <https://github.com/model-checking/kani/pull/2551>
+//! See <https://github.com/model-checking/kani/issues/2576> for more details.
+
+#[kani::proof]
+fn fmt_i8() {
+    let num: i8 = kani::any();
+    let s = format!("{num}");
+    assert!(s.len() <= 4);
+}
+
+#[kani::proof]
+fn fmt_u8() {
+    let num: u8 = kani::any();
+    let s = format!("{num}");
+    assert!(s.len() <= 3);
+}
diff --git a/tests/ui/Property-Class-UI/arithmetic_overflow/expected b/tests/ui/Property-Class-UI/arithmetic_overflow/expected
index 67fc7dd6c0cd..9b445e995385 100644
--- a/tests/ui/Property-Class-UI/arithmetic_overflow/expected
+++ b/tests/ui/Property-Class-UI/arithmetic_overflow/expected
@@ -1,11 +1,11 @@
 core::num::<impl u8>::unchecked_mul.arithmetic_overflow.1\
 Status: SUCCESS
-Description: "attempt to compute unchecked_mul which would overflow"
+Description: "attempt to compute `unchecked_mul` which would overflow"
 
 core::num::<impl u8>::unchecked_add.arithmetic_overflow.1\
 Status: SUCCESS
-Description: "attempt to compute unchecked_add which would overflow"
+Description: "attempt to compute `unchecked_add` which would overflow"
 
 core::num::<impl u8>::unchecked_sub.arithmetic_overflow.1\
 Status: SUCCESS
-Description: "attempt to compute unchecked_sub which would overflow"
+Description: "attempt to compute `unchecked_sub` which would overflow"
diff --git a/tests/ui/code-location/expected b/tests/ui/code-location/expected
index cced065e9f1a..bacda6b16a29 100644
--- a/tests/ui/code-location/expected
+++ b/tests/ui/code-location/expected
@@ -1,6 +1,6 @@
 module/mod.rs:10:5 in function module::not_empty
 main.rs:13:5 in function same_file
 /toolchains/
-alloc/src/vec/mod.rs:3018:81 in function <std::vec::Vec<i32> as std::ops::Drop>::drop
+alloc/src/vec/mod.rs:3007:81 in function <std::vec::Vec<i32> as std::ops::Drop>::drop
 
 VERIFICATION:- SUCCESSFUL
diff --git a/tests/ui/duplicates/dup_checks.rs b/tests/ui/duplicates/dup_checks.rs
new file mode 100644
index 000000000000..a1b45d52cc05
--- /dev/null
+++ b/tests/ui/duplicates/dup_checks.rs
@@ -0,0 +1,19 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+//! Test that captures how Kani implements various redundant checks
+//! for the same operation. This can be confusing for the user, since
+//! the duplicated check will always succeed, even when the first check fails.
+//! <https://github.com/model-checking/kani/issues/2579>
+
+use std::hint::black_box;
+
+#[kani::proof]
+fn check_division() {
+    black_box(kani::any::<i8>() / kani::any::<i8>());
+}
+
+#[kani::proof]
+fn check_remainder() {
+    black_box(kani::any::<i8>() % kani::any::<i8>());
+}
diff --git a/tests/ui/duplicates/expected b/tests/ui/duplicates/expected
new file mode 100644
index 000000000000..9e6b135283d6
--- /dev/null
+++ b/tests/ui/duplicates/expected
@@ -0,0 +1,49 @@
+Checking harness check_remainder...
+
+RESULTS:
+check_remainder.assertion\
+Status: FAILURE\
+Description: "attempt to calculate the remainder with a divisor of zero"
+
+check_remainder.assertion\
+Status: FAILURE\
+Description: "attempt to calculate the remainder with overflow"
+
+check_remainder.arithmetic_overflow\
+Status: SUCCESS\
+Description: "attempt to calculate the remainder with overflow"
+
+check_remainder.arithmetic_overflow\
+Status: SUCCESS\
+Description: "attempt to calculate the remainder with a divisor of zero"
+
+check_remainder.division-by-zero\
+Status: SUCCESS\
+Description: "division by zero"
+
+Failed Checks: attempt to calculate the remainder with a divisor of zero
+Failed Checks: attempt to calculate the remainder with overflow
+
+Checking harness check_division...
+check_division.assertion\
+Status: FAILURE\
+Description: "attempt to divide by zero"
+
+check_division.assertion\
+Status: FAILURE\
+Description: "attempt to divide with overflow"
+
+check_division.arithmetic_overflow\
+Status: SUCCESS\
+Description: "attempt to divide with overflow"
+
+check_division.arithmetic_overflow\
+Status: SUCCESS\
+Description: "attempt to divide by zero"
+
+check_division.division-by-zero\
+Status: SUCCESS\
+Description: "division by zero"
+
+Failed Checks: attempt to divide by zero
+Failed Checks: attempt to divide with overflow

From b35b4e6374cb8f3df523c718fccbe29c5153e4b2 Mon Sep 17 00:00:00 2001
From: Kareem Khazem <karkhaz@amazon.com>
Date: Wed, 5 Jul 2023 01:36:43 +0100
Subject: [PATCH 03/14] Remove atty and tracing-tree, update hermit-abi (#2581)

This removes dependency on atty, and tracing-tree (which depends on atty). This is in response to this security advisory:

https://rustsec.org/advisories/RUSTSEC-2021-0145

atty is removed by switching to std::io::IsTerminal. tracing-tree is removed by replacing HierarchicalLayer with a regular tracing_subscriber::fmt::layer that directs to stderr.

The PR also updates hermit-abi to 0.3.2 from 0.3.1, in response to 0.3.1 being yanked.

This PR resolves #2580.
---
 Cargo.lock                    | 84 +++++++++--------------------------
 kani-compiler/Cargo.toml      |  2 -
 kani-compiler/src/session.rs  | 11 ++---
 kani-driver/Cargo.toml        |  2 -
 kani-driver/src/call_cargo.rs |  3 +-
 kani-driver/src/session.rs    | 11 ++---
 6 files changed, 30 insertions(+), 83 deletions(-)

diff --git a/Cargo.lock b/Cargo.lock
index 4660575954f2..353da79ace78 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -87,17 +87,6 @@ version = "1.0.71"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "9c7d0618f0e0b7e8ff11427422b64564d5fb0be1940354bfe2e0529b18a9d9b8"
 
-[[package]]
-name = "atty"
-version = "0.2.14"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d9b39be18770d11421cdb1b9947a45dd3f37e93092cbf377614828a319d5fee8"
-dependencies = [
- "hermit-abi 0.1.19",
- "libc",
- "winapi",
-]
-
 [[package]]
 name = "autocfg"
 version = "1.1.0"
@@ -110,6 +99,12 @@ version = "1.3.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a"
 
+[[package]]
+name = "bitflags"
+version = "2.3.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "630be753d4e58660abd17930c71b647fe46c27ea6b63cc59e1e3851406972e42"
+
 [[package]]
 name = "bookrunner"
 version = "0.1.0"
@@ -196,7 +191,7 @@ checksum = "9a78fbdd3cc2914ddf37ba444114bc7765bbdcb55ec9cbe6fa054f0137400717"
 dependencies = [
  "anstream",
  "anstyle",
- "bitflags",
+ "bitflags 1.3.2",
  "clap_lex",
  "once_cell",
  "strsim",
@@ -332,7 +327,7 @@ version = "0.26.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "a84cda67535339806297f1b331d6dd6320470d2a0fe65381e79ee9e156dd3d13"
 dependencies = [
- "bitflags",
+ "bitflags 1.3.2",
  "crossterm_winapi",
  "libc",
  "mio",
@@ -437,15 +432,6 @@ version = "0.4.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "95505c38b4572b2d910cecb0281560f54b440a19336cbbcb27bf6ce6adc6f5a8"
 
-[[package]]
-name = "hermit-abi"
-version = "0.1.19"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "62b467343b94ba476dcb2500d242dadbb39557df889310ac77c5d99100aaac33"
-dependencies = [
- "libc",
-]
-
 [[package]]
 name = "hermit-abi"
 version = "0.2.6"
@@ -457,9 +443,9 @@ dependencies = [
 
 [[package]]
 name = "hermit-abi"
-version = "0.3.1"
+version = "0.3.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "fed44880c466736ef9a5c5b5facefb5ed0785676d0c02d612db14e54f0d84286"
+checksum = "443144c8cdadd93ebf52ddb4056d257f5b52c04d3c804e657d19eb73fc33668b"
 
 [[package]]
 name = "home"
@@ -480,25 +466,13 @@ dependencies = [
  "hashbrown 0.14.0",
 ]
 
-[[package]]
-name = "io-lifetimes"
-version = "1.0.11"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "eae7b9aee968036d54dce06cebaefd919e4472e753296daccd6d344e3e2df0c2"
-dependencies = [
- "hermit-abi 0.3.1",
- "libc",
- "windows-sys 0.48.0",
-]
-
 [[package]]
 name = "is-terminal"
-version = "0.4.7"
+version = "0.4.8"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "adcf93614601c8129ddf72e2d5633df827ba6551541c6d8c59520a371475be1f"
+checksum = "24fddda5af7e54bf7da53067d6e802dbcc381d0a8eef629df528e3ebf68755cb"
 dependencies = [
- "hermit-abi 0.3.1",
- "io-lifetimes",
+ "hermit-abi 0.3.2",
  "rustix",
  "windows-sys 0.48.0",
 ]
@@ -529,7 +503,6 @@ dependencies = [
 name = "kani-compiler"
 version = "0.31.0"
 dependencies = [
- "atty",
  "clap",
  "cprover_bindings",
  "home",
@@ -545,7 +518,6 @@ dependencies = [
  "strum_macros",
  "tracing",
  "tracing-subscriber",
- "tracing-tree",
 ]
 
 [[package]]
@@ -553,7 +525,6 @@ name = "kani-driver"
 version = "0.31.0"
 dependencies = [
  "anyhow",
- "atty",
  "cargo_metadata",
  "clap",
  "comfy-table",
@@ -573,7 +544,6 @@ dependencies = [
  "toml",
  "tracing",
  "tracing-subscriber",
- "tracing-tree",
  "which",
 ]
 
@@ -630,9 +600,9 @@ dependencies = [
 
 [[package]]
 name = "linux-raw-sys"
-version = "0.3.8"
+version = "0.4.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ef53942eb7bf7ff43a617b3e2c1c4a5ecf5944a7c1bc12d7ee39bbb15e5c1519"
+checksum = "09fc20d2ca12cb9f044c93e3bd6d32d523e6e2ec3db4f7b2939cd99026ecd3f0"
 
 [[package]]
 name = "lock_api"
@@ -890,7 +860,7 @@ version = "0.9.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "77a1a2f1f0a7ecff9c31abbe177637be0e97a0aef46cf8738ece09327985d998"
 dependencies = [
- "bitflags",
+ "bitflags 1.3.2",
  "memchr",
  "unicase",
 ]
@@ -962,7 +932,7 @@ version = "0.3.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "567664f262709473930a4bf9e51bf2ebf3348f2e748ccc50dea20646858f8f29"
 dependencies = [
- "bitflags",
+ "bitflags 1.3.2",
 ]
 
 [[package]]
@@ -1012,13 +982,12 @@ dependencies = [
 
 [[package]]
 name = "rustix"
-version = "0.37.20"
+version = "0.38.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b96e891d04aa506a6d1f318d2771bcb1c7dfda84e126660ace067c9b474bb2c0"
+checksum = "aabcb0461ebd01d6b79945797c27f8529082226cb630a9865a71870ff63532a4"
 dependencies = [
- "bitflags",
+ "bitflags 2.3.3",
  "errno",
- "io-lifetimes",
  "libc",
  "linux-raw-sys",
  "windows-sys 0.48.0",
@@ -1378,19 +1347,6 @@ dependencies = [
  "tracing-serde",
 ]
 
-[[package]]
-name = "tracing-tree"
-version = "0.2.3"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "4f9742d8df709837409dbb22aa25dd7769c260406f20ff48a2320b80a4a6aed0"
-dependencies = [
- "atty",
- "nu-ansi-term",
- "tracing-core",
- "tracing-log",
- "tracing-subscriber",
-]
-
 [[package]]
 name = "unicase"
 version = "2.6.0"
diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml
index 65f018363990..f0baa6f7047d 100644
--- a/kani-compiler/Cargo.toml
+++ b/kani-compiler/Cargo.toml
@@ -9,7 +9,6 @@ license = "MIT OR Apache-2.0"
 publish = false
 
 [dependencies]
-atty = "0.2.14"
 cbmc = { path = "../cprover_bindings", package = "cprover_bindings", optional = true }
 clap = { version = "4.1.3", features = ["cargo"] }
 home = "0.5"
@@ -25,7 +24,6 @@ strum_macros = "0.24.0"
 shell-words = "1.0.0"
 tracing = {version = "0.1", features = ["max_level_trace", "release_max_level_debug"]}
 tracing-subscriber = {version = "0.3.8", features = ["env-filter", "json", "fmt"]}
-tracing-tree = "0.2.2"
 
 # Future proofing: enable backend dependencies using feature.
 [features]
diff --git a/kani-compiler/src/session.rs b/kani-compiler/src/session.rs
index 3900aba5e82f..6061554200dc 100644
--- a/kani-compiler/src/session.rs
+++ b/kani-compiler/src/session.rs
@@ -9,11 +9,11 @@ use rustc_errors::{
     emitter::Emitter, emitter::HumanReadableErrorType, fallback_fluent_bundle, json::JsonEmitter,
     ColorConfig, Diagnostic, TerminalUrl,
 };
+use std::io::IsTerminal;
 use std::panic;
 use std::str::FromStr;
 use std::sync::LazyLock;
 use tracing_subscriber::{filter::Directive, layer::SubscriberExt, EnvFilter, Registry};
-use tracing_tree::HierarchicalLayer;
 
 /// Environment variable used to control this session log tracing.
 const LOG_ENV_VAR: &str = "KANI_LOG";
@@ -107,16 +107,13 @@ fn json_logs(filter: EnvFilter) {
 
 /// Configure global logger to use a hierarchical view.
 fn hier_logs(args: &ArgMatches, filter: EnvFilter) {
-    let use_colors = atty::is(atty::Stream::Stdout) || args.get_flag(parser::COLOR_OUTPUT);
+    let use_colors = std::io::stdout().is_terminal() || args.get_flag(parser::COLOR_OUTPUT);
     let subscriber = Registry::default().with(filter);
     let subscriber = subscriber.with(
-        HierarchicalLayer::default()
+        tracing_subscriber::fmt::layer()
             .with_writer(std::io::stderr)
-            .with_indent_lines(true)
             .with_ansi(use_colors)
-            .with_targets(true)
-            .with_verbose_exit(true)
-            .with_indent_amount(4),
+            .with_target(true),
     );
     tracing::subscriber::set_global_default(subscriber).unwrap();
 }
diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml
index 18d666830854..b6a89a72dc09 100644
--- a/kani-driver/Cargo.toml
+++ b/kani-driver/Cargo.toml
@@ -15,7 +15,6 @@ publish = false
 kani_metadata = { path = "../kani_metadata" }
 cargo_metadata = "0.15.0"
 anyhow = "1"
-atty = "0.2.14"
 console = "0.15.1"
 once_cell = "1.13.0"
 serde = { version = "1", features = ["derive"] }
@@ -32,7 +31,6 @@ strum = {version = "0.24.0"}
 strum_macros = {version = "0.24.0"}
 tracing = {version = "0.1", features = ["max_level_trace", "release_max_level_debug"]}
 tracing-subscriber = {version = "0.3.8", features = ["env-filter", "json", "fmt"]}
-tracing-tree = "0.2.2"
 rand = "0.8"
 which = "4.4.0"
 
diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs
index 30dac09eddaa..00bbe72d9865 100644
--- a/kani-driver/src/call_cargo.rs
+++ b/kani-driver/src/call_cargo.rs
@@ -14,6 +14,7 @@ use std::ffi::{OsStr, OsString};
 use std::fmt::{self, Display};
 use std::fs::{self, File};
 use std::io::BufReader;
+use std::io::IsTerminal;
 use std::path::PathBuf;
 use std::process::Command;
 use tracing::{debug, trace};
@@ -180,7 +181,7 @@ impl KaniSession {
     /// Run cargo and collect any error found.
     /// We also collect the metadata file generated during compilation if any.
     fn run_cargo(&self, cargo_cmd: Command, target: &Target) -> Result<Option<Artifact>> {
-        let support_color = atty::is(atty::Stream::Stdout);
+        let support_color = std::io::stdout().is_terminal();
         let mut artifact = None;
         if let Some(mut cargo_process) = self.run_piped(cargo_cmd)? {
             let reader = BufReader::new(cargo_process.stdout.take().unwrap());
diff --git a/kani-driver/src/session.rs b/kani-driver/src/session.rs
index 47cbb0914eaf..646b7b6ae746 100644
--- a/kani-driver/src/session.rs
+++ b/kani-driver/src/session.rs
@@ -5,6 +5,7 @@ use crate::args::common::Verbosity;
 use crate::args::VerificationArgs;
 use crate::util::render_command;
 use anyhow::{bail, Context, Result};
+use std::io::IsTerminal;
 use std::io::Write;
 use std::path::{Path, PathBuf};
 use std::process::{Child, Command, ExitStatus, Stdio};
@@ -13,7 +14,6 @@ use std::time::Instant;
 use strum_macros::Display;
 use tracing::level_filters::LevelFilter;
 use tracing_subscriber::{layer::SubscriberExt, EnvFilter, Registry};
-use tracing_tree::HierarchicalLayer;
 
 /// Environment variable used to control this session log tracing.
 /// This is the same variable used to control `kani-compiler` logs. Note that you can still control
@@ -368,16 +368,13 @@ fn init_logger(args: &VerificationArgs) {
     };
 
     // Use a hierarchical view for now.
-    let use_colors = atty::is(atty::Stream::Stdout);
+    let use_colors = std::io::stdout().is_terminal();
     let subscriber = Registry::default().with(filter);
     let subscriber = subscriber.with(
-        HierarchicalLayer::default()
+        tracing_subscriber::fmt::layer()
             .with_writer(std::io::stderr)
-            .with_indent_lines(true)
             .with_ansi(use_colors)
-            .with_targets(true)
-            .with_verbose_exit(true)
-            .with_indent_amount(4),
+            .with_target(true),
     );
     tracing::subscriber::set_global_default(subscriber).unwrap();
 }

From 08ed81193d127e63b461fa5dbd5f1b4f7d02c477 Mon Sep 17 00:00:00 2001
From: "github-actions[bot]"
 <41898282+github-actions[bot]@users.noreply.github.com>
Date: Wed, 5 Jul 2023 10:39:14 -0700
Subject: [PATCH 04/14] Automatic toolchain upgrade to nightly-2023-06-21
 (#2582)

Update Rust toolchain from nightly-2023-06-20 to nightly-2023-06-21 without any other source changes.

Co-authored-by: celinval <celinval@users.noreply.github.com>
---
 rust-toolchain.toml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index e1e134733598..0916ae1c14db 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2023-06-20"
+channel = "nightly-2023-06-21"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

From 2be57b4972fb6659c31f49e4171bccb5cc2d5288 Mon Sep 17 00:00:00 2001
From: Fabian Zaiser <fabian.zaiser@cs.ox.ac.uk>
Date: Thu, 6 Jul 2023 19:02:09 +0100
Subject: [PATCH 05/14] Add kani::spawn and an executor to the Kani library
 (#1659)

This adds an executor (scheduler for async futures) to the Kani library, thus supporting `kani::spawn` as a replacement for `tokio::spawn`.

It also includes `kani::yield_now` which is similar to `tokio::yield_now`.

Co-authored-by: Celina G. Val <celinval@amazon.com>
---
 kani-driver/src/args/common.rs        |   2 +
 library/kani/src/futures.rs           | 189 ++++++++++++++++++++++++
 library/kani/src/lib.rs               |   3 +-
 tests/kani/AsyncAwait/main.rs         |   1 +
 tests/kani/AsyncAwait/manual_spawn.rs | 203 --------------------------
 tests/kani/AsyncAwait/spawn.rs        |  33 +++++
 6 files changed, 226 insertions(+), 205 deletions(-)
 delete mode 100644 tests/kani/AsyncAwait/manual_spawn.rs
 create mode 100644 tests/kani/AsyncAwait/spawn.rs

diff --git a/kani-driver/src/args/common.rs b/kani-driver/src/args/common.rs
index b8434c76e7b8..746482c6985e 100644
--- a/kani-driver/src/args/common.rs
+++ b/kani-driver/src/args/common.rs
@@ -42,6 +42,8 @@ pub enum UnstableFeatures {
     CFfi,
     /// Enable concrete playback flow.
     ConcretePlayback,
+    /// Enable Kani's unstable async library.
+    AsyncLib,
 }
 
 impl ValidateArgs for CommonArgs {
diff --git a/library/kani/src/futures.rs b/library/kani/src/futures.rs
index aea5e03d1f0b..cd3b9ad60597 100644
--- a/library/kani/src/futures.rs
+++ b/library/kani/src/futures.rs
@@ -15,6 +15,9 @@ use std::{
 /// Whereas a clever executor like `block_on` in `futures` or `tokio` would interact with the OS scheduler
 /// to be woken up when a resource becomes available, this is not supported by Kani.
 /// As a consequence, this function completely ignores the waker infrastructure and just polls the given future in a busy loop.
+///
+/// Note that [`spawn`] is not supported with this function. Use [`block_on_with_spawn`] if you need it.
+#[crate::unstable(feature = "async-lib", issue = 2559, reason = "experimental async support")]
 pub fn block_on<T>(mut fut: impl Future<Output = T>) -> T {
     let waker = unsafe { Waker::from_raw(NOOP_RAW_WAKER) };
     let cx = &mut Context::from_waker(&waker);
@@ -41,3 +44,189 @@ const NOOP_RAW_WAKER: RawWaker = {
 
     RawWaker::new(std::ptr::null(), &RawWakerVTable::new(clone_waker, noop, noop, noop))
 };
+
+/// The global executor used by [`spawn`] and [`block_on_with_spawn`] to run tasks.
+static mut GLOBAL_EXECUTOR: Option<Scheduler> = None;
+
+type BoxFuture = Pin<Box<dyn Future<Output = ()> + Sync + 'static>>;
+
+/// Indicates to the scheduler whether it can `kani::assume` that the returned task is running.
+///
+/// This is useful if the task was picked nondeterministically using `kani::any()`.
+/// For more information, see [`SchedulingStrategy`].
+pub enum SchedulingAssumption {
+    CanAssumeRunning,
+    CannotAssumeRunning,
+}
+
+/// Trait that determines the possible sequence of tasks scheduling for a harness.
+///
+/// If your harness spawns several tasks, Kani's scheduler has to decide in what order to poll them.
+/// This order may depend on the needs of your verification goal.
+/// For example, you sometimes may wish to verify all possible schedulings, i.e. a nondeterministic scheduling strategy.
+///
+/// Nondeterministic scheduling strategies can be very slow to verify because they require Kani to check a large number of permutations of tasks.
+/// So if you want to verify a harness that uses `spawn`, but don't care about concurrency issues, you can simply use a deterministic scheduling strategy,
+/// such as [`RoundRobin`], which polls each task in turn.
+///
+/// Finally, you have the option of providing your own scheduling strategy by implementing this trait.
+/// This can be useful, for example, if you want to verify that things work correctly for a very specific task ordering.
+pub trait SchedulingStrategy {
+    /// Picks the next task to be scheduled whenever the scheduler needs to pick a task to run next, and whether it can be assumed that the picked task is still running
+    ///
+    /// Tasks are numbered `0..num_tasks`.
+    /// For example, if pick_task(4) returns (2, CanAssumeRunning) than it picked the task with index 2 and allows Kani to `assume` that this task is still running.
+    /// This is useful if the task is chosen nondeterministicall (`kani::any()`) and allows the verifier to discard useless execution branches (such as polling a completed task again).
+    ///
+    /// As a rule of thumb:
+    /// if the scheduling strategy picks the next task nondeterministically (using `kani::any()`), return CanAssumeRunning, otherwise CannotAssumeRunning.
+    /// When returning `CanAssumeRunning`, the scheduler will then assume that the picked task is still running, which cuts off "useless" paths where a completed task is polled again.
+    /// It is even necessary to make things terminate if nondeterminism is involved:
+    /// if we pick the task nondeterministically, and don't have the restriction to still running tasks, we could poll the same task over and over again.
+    ///
+    /// However, for most deterministic scheduling strategies, e.g. the round robin scheduling strategy, assuming that the picked task is still running is generally not possible
+    /// because if that task has ended, we are saying assume(false) and the verification effectively stops (which is undesirable, of course).
+    /// In such cases, return `CannotAssumeRunning` instead.
+    fn pick_task(&mut self, num_tasks: usize) -> (usize, SchedulingAssumption);
+}
+
+/// Keeps cycling through the tasks in a deterministic order
+#[derive(Default)]
+pub struct RoundRobin {
+    index: usize,
+}
+
+impl SchedulingStrategy for RoundRobin {
+    #[inline]
+    fn pick_task(&mut self, num_tasks: usize) -> (usize, SchedulingAssumption) {
+        self.index = (self.index + 1) % num_tasks;
+        (self.index, SchedulingAssumption::CannotAssumeRunning)
+    }
+}
+
+pub(crate) struct Scheduler {
+    tasks: Vec<Option<BoxFuture>>,
+    num_running: usize,
+}
+
+impl Scheduler {
+    /// Creates a scheduler with an empty task list
+    #[inline]
+    pub(crate) const fn new() -> Scheduler {
+        Scheduler { tasks: Vec::new(), num_running: 0 }
+    }
+
+    /// Adds a future to the scheduler's task list, returning a JoinHandle
+    pub(crate) fn spawn<F: Future<Output = ()> + Sync + 'static>(&mut self, fut: F) -> JoinHandle {
+        let index = self.tasks.len();
+        self.tasks.push(Some(Box::pin(fut)));
+        self.num_running += 1;
+        JoinHandle { index }
+    }
+
+    /// Runs the scheduler with the given scheduling plan until all tasks have completed
+    fn run(&mut self, mut scheduling_plan: impl SchedulingStrategy) {
+        let waker = unsafe { Waker::from_raw(NOOP_RAW_WAKER) };
+        let cx = &mut Context::from_waker(&waker);
+        while self.num_running > 0 {
+            let (index, assumption) = scheduling_plan.pick_task(self.tasks.len());
+            let task = &mut self.tasks[index];
+            if let Some(fut) = task.as_mut() {
+                match fut.as_mut().poll(cx) {
+                    std::task::Poll::Ready(()) => {
+                        self.num_running -= 1;
+                        let _prev = task.take();
+                    }
+                    std::task::Poll::Pending => (),
+                }
+            } else if let SchedulingAssumption::CanAssumeRunning = assumption {
+                crate::assume(false); // useful so that we can assume that a nondeterministically picked task is still running
+            }
+        }
+    }
+
+    /// Polls the given future and the tasks it may spawn until all of them complete
+    fn block_on<F: Future<Output = ()> + Sync + 'static>(
+        &mut self,
+        fut: F,
+        scheduling_plan: impl SchedulingStrategy,
+    ) {
+        self.spawn(fut);
+        self.run(scheduling_plan);
+    }
+}
+
+/// Result of spawning a task.
+///
+/// If you `.await` a JoinHandle, this will wait for the spawned task to complete.
+pub struct JoinHandle {
+    index: usize,
+}
+
+impl Future for JoinHandle {
+    type Output = ();
+
+    fn poll(self: Pin<&mut Self>, cx: &mut Context<'_>) -> std::task::Poll<Self::Output> {
+        if unsafe { GLOBAL_EXECUTOR.as_mut().unwrap().tasks[self.index].is_some() } {
+            std::task::Poll::Pending
+        } else {
+            cx.waker().wake_by_ref(); // For completeness. But Kani currently ignores wakers.
+            std::task::Poll::Ready(())
+        }
+    }
+}
+
+/// Spawns a task on the current global executor (which is set by [`block_on_with_spawn`])
+///
+/// This function can only be called inside a future passed to [`block_on_with_spawn`].
+#[crate::unstable(feature = "async-lib", issue = 2559, reason = "experimental async support")]
+pub fn spawn<F: Future<Output = ()> + Sync + 'static>(fut: F) -> JoinHandle {
+    unsafe {
+        GLOBAL_EXECUTOR
+            .as_mut()
+            .expect("`spawn` should only be called within `block_on_with_spawn`")
+            .spawn(fut)
+    }
+}
+
+/// Polls the given future and the tasks it may spawn until all of them complete
+///
+/// Contrary to [`block_on`], this allows `spawn`ing other futures
+#[crate::unstable(feature = "async-lib", issue = 2559, reason = "experimental async support")]
+pub fn block_on_with_spawn<F: Future<Output = ()> + Sync + 'static>(
+    fut: F,
+    scheduling_plan: impl SchedulingStrategy,
+) {
+    unsafe {
+        assert!(GLOBAL_EXECUTOR.is_none(), "`block_on_with_spawn` should not be nested");
+        GLOBAL_EXECUTOR = Some(Scheduler::new());
+        GLOBAL_EXECUTOR.as_mut().unwrap().block_on(fut, scheduling_plan);
+        GLOBAL_EXECUTOR = None;
+    }
+}
+
+/// Suspends execution of the current future, to allow the scheduler to poll another future
+///
+/// Specifically, it returns a future that isn't ready until the second time it is polled.
+#[crate::unstable(feature = "async-lib", issue = 2559, reason = "experimental async support")]
+pub fn yield_now() -> impl Future<Output = ()> {
+    struct YieldNow {
+        yielded: bool,
+    }
+
+    impl Future for YieldNow {
+        type Output = ();
+
+        fn poll(mut self: Pin<&mut Self>, cx: &mut Context<'_>) -> std::task::Poll<Self::Output> {
+            if self.yielded {
+                cx.waker().wake_by_ref(); // For completeness. But Kani currently ignores wakers.
+                std::task::Poll::Ready(())
+            } else {
+                self.yielded = true;
+                std::task::Poll::Pending
+            }
+        }
+    }
+
+    YieldNow { yielded: false }
+}
diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs
index 71faf63feaaf..5ab09d69f9bb 100644
--- a/library/kani/src/lib.rs
+++ b/library/kani/src/lib.rs
@@ -26,8 +26,7 @@ pub use concrete_playback::concrete_playback_run;
 pub fn concrete_playback_run<F: Fn()>(_: Vec<Vec<u8>>, _: F) {
     unreachable!("Concrete playback does not work during verification")
 }
-
-pub use futures::block_on;
+pub use futures::{block_on, block_on_with_spawn, spawn, yield_now, RoundRobin};
 
 /// Creates an assumption that will be valid after this statement run. Note that the assumption
 /// will only be applied for paths that follow the assumption. If the assumption doesn't hold, the
diff --git a/tests/kani/AsyncAwait/main.rs b/tests/kani/AsyncAwait/main.rs
index e8821c998c16..aa1964bfc479 100644
--- a/tests/kani/AsyncAwait/main.rs
+++ b/tests/kani/AsyncAwait/main.rs
@@ -2,6 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
 // compile-flags: --edition 2018
+// kani-flags: -Z async-lib
 
 // Tests that the language constructs `async { ... }` blocks, `async fn`, and `.await` work correctly.
 
diff --git a/tests/kani/AsyncAwait/manual_spawn.rs b/tests/kani/AsyncAwait/manual_spawn.rs
deleted file mode 100644
index 8888bc5caea1..000000000000
--- a/tests/kani/AsyncAwait/manual_spawn.rs
+++ /dev/null
@@ -1,203 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-//
-// compile-flags: --edition 2018
-// kani-flags: --enable-unstable --mir-linker
-
-//! This file tests a hand-written spawn infrastructure and executor.
-//! This should be replaced with code from the Kani library as soon as the executor can get merged.
-//! Tracking issue: https://github.com/model-checking/kani/issues/1685
-
-use std::{
-    future::Future,
-    pin::Pin,
-    sync::{
-        atomic::{AtomicI64, Ordering},
-        Arc,
-    },
-    task::{Context, RawWaker, RawWakerVTable, Waker},
-};
-
-/// A dummy waker, which is needed to call [`Future::poll`]
-const NOOP_RAW_WAKER: RawWaker = {
-    #[inline]
-    unsafe fn clone_waker(_: *const ()) -> RawWaker {
-        NOOP_RAW_WAKER
-    }
-
-    #[inline]
-    unsafe fn noop(_: *const ()) {}
-
-    RawWaker::new(std::ptr::null(), &RawWakerVTable::new(clone_waker, noop, noop, noop))
-};
-
-static mut GLOBAL_EXECUTOR: Scheduler = Scheduler::new();
-const MAX_TASKS: usize = 16;
-
-type BoxFuture = Pin<Box<dyn Future<Output = ()> + Sync + 'static>>;
-
-/// Indicates to the scheduler whether it can `assume` that the returned task is running.
-/// This is useful if the task was picked nondeterministically using `any()`.
-pub enum SchedulingOptimization {
-    CanAssumeRunning,
-    CannotAssumeRunning,
-}
-
-/// Allows to parameterize how the scheduler picks the next task to poll in `spawnable_block_on`
-pub trait SchedulingStrategy {
-    /// Picks the next task to be scheduled whenever the scheduler needs to pick a task to run next, and whether it can be assumed that the picked task is still running
-    ///
-    /// Tasks are numbered `0..num_tasks`.
-    /// For example, if pick_task(4) returns `(2, CanAssumeRunning)` than it picked the task with index 2 and allows Kani to `assume` that this task is still running.
-    /// This is useful if the task is chosen nondeterministicall (`kani::any()`) and allows the verifier to discard useless execution branches (such as polling a completed task again).
-    fn pick_task(&mut self, num_tasks: usize) -> (usize, SchedulingOptimization);
-}
-
-/// Keeps cycling through the tasks in a deterministic order
-#[derive(Default)]
-pub struct RoundRobin {
-    index: usize,
-}
-
-impl SchedulingStrategy for RoundRobin {
-    fn pick_task(&mut self, num_tasks: usize) -> (usize, SchedulingOptimization) {
-        self.index = (self.index + 1) % num_tasks;
-        (self.index, SchedulingOptimization::CannotAssumeRunning)
-    }
-}
-
-pub struct Scheduler {
-    /// Using a Vec instead of an array makes the runtime increase by a factor of 200.
-    tasks: [Option<BoxFuture>; MAX_TASKS],
-    num_tasks: usize,
-    num_running: usize,
-}
-
-impl Scheduler {
-    /// Creates a scheduler with an empty task list
-    pub const fn new() -> Scheduler {
-        const INIT: Option<BoxFuture> = None;
-        Scheduler { tasks: [INIT; MAX_TASKS], num_tasks: 0, num_running: 0 }
-    }
-
-    /// Adds a future to the scheduler's task list, returning a JoinHandle
-    pub fn spawn<F: Future<Output = ()> + Sync + 'static>(&mut self, fut: F) -> JoinHandle {
-        let index = self.num_tasks;
-        self.tasks[index] = Some(Box::pin(fut));
-        self.num_tasks += 1;
-        assert!(self.num_tasks < MAX_TASKS, "more than {} tasks", MAX_TASKS);
-        self.num_running += 1;
-        JoinHandle { index }
-    }
-
-    /// Runs the scheduler with the given scheduling plan until all tasks have completed
-    pub fn run(&mut self, mut scheduling_plan: impl SchedulingStrategy) {
-        let waker = unsafe { Waker::from_raw(NOOP_RAW_WAKER) };
-        let cx = &mut Context::from_waker(&waker);
-        while self.num_running > 0 {
-            let (index, can_assume_running) = scheduling_plan.pick_task(self.num_tasks);
-            let task = &mut self.tasks[index];
-            if let Some(fut) = task.as_mut() {
-                match fut.as_mut().poll(cx) {
-                    std::task::Poll::Ready(()) => {
-                        self.num_running -= 1;
-                        let _prev = std::mem::replace(task, None);
-                    }
-                    std::task::Poll::Pending => (),
-                }
-            } else if let SchedulingOptimization::CanAssumeRunning = can_assume_running {
-                #[cfg(kani)]
-                kani::assume(false); // useful so that we can assume that a nondeterministically picked task is still running
-            }
-        }
-    }
-
-    /// Polls the given future and the tasks it may spawn until all of them complete.
-    pub fn block_on<F: Future<Output = ()> + Sync + 'static>(
-        &mut self,
-        fut: F,
-        scheduling_plan: impl SchedulingStrategy,
-    ) {
-        self.spawn(fut);
-        self.run(scheduling_plan);
-    }
-}
-
-/// Result of spawning a task.
-///
-/// If you `.await` a JoinHandle, this will wait for the spawned task to complete.
-pub struct JoinHandle {
-    index: usize,
-}
-
-impl Future for JoinHandle {
-    type Output = ();
-
-    fn poll(self: Pin<&mut Self>, cx: &mut Context<'_>) -> std::task::Poll<Self::Output> {
-        if unsafe { GLOBAL_EXECUTOR.tasks[self.index].is_some() } {
-            std::task::Poll::Pending
-        } else {
-            cx.waker().wake_by_ref(); // For completeness. But Kani currently ignores wakers.
-            std::task::Poll::Ready(())
-        }
-    }
-}
-
-#[inline] // to work around linking issue
-pub fn spawn<F: Future<Output = ()> + Sync + 'static>(fut: F) -> JoinHandle {
-    unsafe { GLOBAL_EXECUTOR.spawn(fut) }
-}
-
-/// Polls the given future and the tasks it may spawn until all of them complete
-///
-/// Contrary to block_on, this allows `spawn`ing other futures
-pub fn spawnable_block_on<F: Future<Output = ()> + Sync + 'static>(
-    fut: F,
-    scheduling_plan: impl SchedulingStrategy,
-) {
-    unsafe {
-        GLOBAL_EXECUTOR.block_on(fut, scheduling_plan);
-    }
-}
-
-struct YieldNow {
-    yielded: bool,
-}
-
-impl Future for YieldNow {
-    type Output = ();
-
-    fn poll(mut self: Pin<&mut Self>, cx: &mut Context<'_>) -> std::task::Poll<Self::Output> {
-        if self.yielded {
-            cx.waker().wake_by_ref(); // For completeness. But Kani currently ignores wakers.
-            std::task::Poll::Ready(())
-        } else {
-            self.yielded = true;
-            std::task::Poll::Pending
-        }
-    }
-}
-
-/// Suspends execution of the current future, to allow the scheduler to poll another future
-pub fn yield_now() -> impl Future<Output = ()> {
-    YieldNow { yielded: false }
-}
-
-#[kani::proof]
-#[kani::unwind(4)]
-fn arc_spawn_deterministic_test() {
-    let x = Arc::new(AtomicI64::new(0)); // Surprisingly, Arc verified faster than Rc
-    let x2 = x.clone();
-    spawnable_block_on(
-        async move {
-            let x3 = x2.clone();
-            spawn(async move {
-                x3.fetch_add(1, Ordering::Relaxed);
-            });
-            yield_now().await;
-            x2.fetch_add(1, Ordering::Relaxed);
-        },
-        RoundRobin::default(),
-    );
-    assert_eq!(x.load(Ordering::Relaxed), 2);
-}
diff --git a/tests/kani/AsyncAwait/spawn.rs b/tests/kani/AsyncAwait/spawn.rs
new file mode 100644
index 000000000000..3bef244ef547
--- /dev/null
+++ b/tests/kani/AsyncAwait/spawn.rs
@@ -0,0 +1,33 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// compile-flags: --edition 2018
+// kani-flags: -Z async-lib
+
+//! This file tests the executor and spawn infrastructure from the Kani library.
+
+use std::sync::{
+    atomic::{AtomicI64, Ordering},
+    Arc,
+};
+
+#[kani::proof]
+#[kani::unwind(4)]
+fn round_robin_schedule() {
+    let x = Arc::new(AtomicI64::new(0)); // Surprisingly, Arc verified faster than Rc
+    let x2 = x.clone();
+    kani::block_on_with_spawn(
+        async move {
+            let x3 = x2.clone();
+            kani::spawn(async move {
+                assert_eq!(x3.load(Ordering::Relaxed), 0); // to check the order of the round-robin
+                x3.fetch_add(1, Ordering::Relaxed);
+            });
+            kani::yield_now().await;
+            assert_eq!(x2.load(Ordering::Relaxed), 1); // to check the order of the round-robin
+            x2.fetch_add(1, Ordering::Relaxed);
+        },
+        kani::RoundRobin::default(),
+    );
+    assert_eq!(x.load(Ordering::Relaxed), 2);
+}

From eefd724445dcd4a8bc04ede54ed6fb0cfc5cce1d Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Fri, 7 Jul 2023 12:33:44 -0700
Subject: [PATCH 06/14] Update rust toolchain to 2023-06-22 (#2588)

Update toolchain and remove dependency on line number since we match exact value only, this generate a lot of noise whenever we update the toolchain.
---
 rust-toolchain.toml             | 2 +-
 tests/ui/code-location/expected | 3 ++-
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index 0916ae1c14db..429669562eee 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2023-06-21"
+channel = "nightly-2023-06-22"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
diff --git a/tests/ui/code-location/expected b/tests/ui/code-location/expected
index bacda6b16a29..9af3f651fb50 100644
--- a/tests/ui/code-location/expected
+++ b/tests/ui/code-location/expected
@@ -1,6 +1,7 @@
 module/mod.rs:10:5 in function module::not_empty
 main.rs:13:5 in function same_file
 /toolchains/
-alloc/src/vec/mod.rs:3007:81 in function <std::vec::Vec<i32> as std::ops::Drop>::drop
+alloc/src/vec/mod.rs:
+in function <std::vec::Vec<i32> as std::ops::Drop>::drop
 
 VERIFICATION:- SUCCESSFUL

From 042a3039762acf48ddc2d2215bc1beb8fd5cbd20 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Fri, 7 Jul 2023 17:44:28 -0700
Subject: [PATCH 07/14] Add "kani" configuration key to enable conditional
 compilation in build scripts (#2297)

We now pass `--cfg=kani` to build scripts, which allow users to use constructs such as `if cfg!(kani)` to conditionally compile their build scripts.

The build script may have logic that is not redundant to Kani, or even unsupported. Users can now change how their build works based on conditional compilation.

Co-authored-by: Kareem Khazem <karkhaz@amazon.com>
---
 kani-driver/src/call_cargo.rs                 | 21 +++++++++++++---
 kani-driver/src/concrete_playback/playback.rs |  7 +++---
 kani-driver/src/session.rs                    |  8 ++++++
 tests/cargo-ui/verbose-cmds/expected          |  2 +-
 .../build-rs-conditional/Cargo.toml           |  9 +++++++
 .../build-rs-conditional/build.rs             | 11 ++++++++
 .../build-rs-conditional/build_rs.sh          | 25 +++++++++++++++++++
 .../build-rs-conditional/config.yml           |  4 +++
 .../build-rs-conditional/expected             | 16 ++++++++++++
 .../build-rs-conditional/src/lib.rs           | 24 ++++++++++++++++++
 10 files changed, 119 insertions(+), 8 deletions(-)
 create mode 100644 tests/script-based-pre/build-rs-conditional/Cargo.toml
 create mode 100644 tests/script-based-pre/build-rs-conditional/build.rs
 create mode 100755 tests/script-based-pre/build-rs-conditional/build_rs.sh
 create mode 100644 tests/script-based-pre/build-rs-conditional/config.yml
 create mode 100644 tests/script-based-pre/build-rs-conditional/expected
 create mode 100644 tests/script-based-pre/build-rs-conditional/src/lib.rs

diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs
index 00bbe72d9865..82186e96a44e 100644
--- a/kani-driver/src/call_cargo.rs
+++ b/kani-driver/src/call_cargo.rs
@@ -5,7 +5,7 @@ use crate::args::VerificationArgs;
 use crate::call_single_file::to_rustc_arg;
 use crate::project::Artifact;
 use crate::session::KaniSession;
-use crate::util;
+use crate::{session, util};
 use anyhow::{bail, Context, Result};
 use cargo_metadata::diagnostic::{Diagnostic, DiagnosticLevel};
 use cargo_metadata::{Message, Metadata, MetadataCommand, Package, Target};
@@ -79,8 +79,7 @@ impl KaniSession {
             cargo_args.push(format!("--features={}", features.join(",")).into());
         }
 
-        cargo_args.push("--target".into());
-        cargo_args.push(build_target.into());
+        cargo_args.append(&mut cargo_config_args());
 
         cargo_args.push("--target-dir".into());
         cargo_args.push(target_dir.into());
@@ -111,7 +110,8 @@ impl KaniSession {
         for package in packages {
             for verification_target in package_targets(&self.args, package) {
                 let mut cmd = Command::new("cargo");
-                cmd.args(&cargo_args)
+                cmd.arg(session::toolchain_shorthand())
+                    .args(&cargo_args)
                     .args(vec!["-p", &package.name])
                     .args(&verification_target.to_args())
                     .args(&pkg_args)
@@ -252,6 +252,19 @@ impl KaniSession {
     }
 }
 
+pub fn cargo_config_args() -> Vec<OsString> {
+    [
+        "--target",
+        env!("TARGET"),
+        // Propagate `--cfg=kani` to build scripts.
+        "-Zhost-config",
+        "-Ztarget-applies-to-host",
+        "--config=host.rustflags=[\"--cfg=kani\"]",
+    ]
+    .map(OsString::from)
+    .to_vec()
+}
+
 /// Print the compiler message following the coloring schema.
 fn print_msg(diagnostic: &Diagnostic, use_rendered: bool) -> Result<()> {
     if use_rendered {
diff --git a/kani-driver/src/concrete_playback/playback.rs b/kani-driver/src/concrete_playback/playback.rs
index 0a71d64fe50f..bb060cea58bd 100644
--- a/kani-driver/src/concrete_playback/playback.rs
+++ b/kani-driver/src/concrete_playback/playback.rs
@@ -5,6 +5,7 @@
 
 use crate::args::common::Verbosity;
 use crate::args::playback_args::{CargoPlaybackArgs, KaniPlaybackArgs, MessageFormat};
+use crate::call_cargo::cargo_config_args;
 use crate::call_single_file::base_rustc_flags;
 use crate::session::{lib_playback_folder, InstallType};
 use crate::{session, util};
@@ -113,8 +114,7 @@ fn cargo_test(install: &InstallType, args: CargoPlaybackArgs) -> Result<()> {
     }
 
     cargo_args.append(&mut args.cargo.to_cargo_args());
-    cargo_args.push("--target".into());
-    cargo_args.push(env!("TARGET").into());
+    cargo_args.append(&mut cargo_config_args());
 
     // These have to be the last arguments to cargo test.
     if !args.playback.test_args.is_empty() {
@@ -124,7 +124,8 @@ fn cargo_test(install: &InstallType, args: CargoPlaybackArgs) -> Result<()> {
 
     // Arguments that will only be passed to the target package.
     let mut cmd = Command::new("cargo");
-    cmd.args(&cargo_args)
+    cmd.arg(session::toolchain_shorthand())
+        .args(&cargo_args)
         .env("RUSTC", &install.kani_compiler()?)
         // Use CARGO_ENCODED_RUSTFLAGS instead of RUSTFLAGS is preferred. See
         // https://doc.rust-lang.org/cargo/reference/environment-variables.html
diff --git a/kani-driver/src/session.rs b/kani-driver/src/session.rs
index 646b7b6ae746..d0834cae2122 100644
--- a/kani-driver/src/session.rs
+++ b/kani-driver/src/session.rs
@@ -291,6 +291,14 @@ pub fn base_folder() -> Result<PathBuf> {
         .to_path_buf())
 }
 
+/// Return the shorthand for the toolchain used by this Kani version.
+///
+/// This shorthand can be used to select the exact toolchain version that matches the one used to
+/// build the current Kani version.
+pub fn toolchain_shorthand() -> String {
+    format!("+{}", env!("RUSTUP_TOOLCHAIN"))
+}
+
 impl InstallType {
     pub fn new() -> Result<Self> {
         // Case 1: We've checked out the development repo and we're built under `target/kani`
diff --git a/tests/cargo-ui/verbose-cmds/expected b/tests/cargo-ui/verbose-cmds/expected
index a15f3ba25b6e..f883ef972cb3 100644
--- a/tests/cargo-ui/verbose-cmds/expected
+++ b/tests/cargo-ui/verbose-cmds/expected
@@ -1,5 +1,5 @@
 CARGO_ENCODED_RUSTFLAGS=
-cargo rustc
+cargo +nightly
 Running: `goto-cc
 Running: `goto-instrument
 Checking harness dummy_harness...
diff --git a/tests/script-based-pre/build-rs-conditional/Cargo.toml b/tests/script-based-pre/build-rs-conditional/Cargo.toml
new file mode 100644
index 000000000000..136bae92250e
--- /dev/null
+++ b/tests/script-based-pre/build-rs-conditional/Cargo.toml
@@ -0,0 +1,9 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "build-rs-conditional"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]
+
diff --git a/tests/script-based-pre/build-rs-conditional/build.rs b/tests/script-based-pre/build-rs-conditional/build.rs
new file mode 100644
index 000000000000..0b083ff95f02
--- /dev/null
+++ b/tests/script-based-pre/build-rs-conditional/build.rs
@@ -0,0 +1,11 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Verify that build scripts can check if they are running under `kani`.
+
+fn main() {
+    if cfg!(kani) {
+        println!("cargo:rustc-env=RUNNING_KANI=Yes");
+    } else {
+        println!("cargo:rustc-env=RUNNING_KANI=No");
+    }
+}
diff --git a/tests/script-based-pre/build-rs-conditional/build_rs.sh b/tests/script-based-pre/build-rs-conditional/build_rs.sh
new file mode 100755
index 000000000000..f08fcf10cb79
--- /dev/null
+++ b/tests/script-based-pre/build-rs-conditional/build_rs.sh
@@ -0,0 +1,25 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+set +e
+
+TMP_DIR="/tmp/build-rs"
+
+rm -rf ${TMP_DIR}
+cp -r . ${TMP_DIR}
+pushd ${TMP_DIR} > /dev/null
+
+
+echo "[TEST] Run verification..."
+cargo kani --concrete-playback=inplace -Z concrete-playback
+
+echo "[TEST] Run playback..."
+cargo kani playback -Z concrete-playback --lib -- check_kani
+
+echo "[TEST] Run test..."
+cargo test --lib
+
+# Cleanup
+popd > /dev/null
+rm -r ${TMP_DIR}
diff --git a/tests/script-based-pre/build-rs-conditional/config.yml b/tests/script-based-pre/build-rs-conditional/config.yml
new file mode 100644
index 000000000000..e34ed0cb5689
--- /dev/null
+++ b/tests/script-based-pre/build-rs-conditional/config.yml
@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: build_rs.sh
+expected: expected
diff --git a/tests/script-based-pre/build-rs-conditional/expected b/tests/script-based-pre/build-rs-conditional/expected
new file mode 100644
index 000000000000..55f309077721
--- /dev/null
+++ b/tests/script-based-pre/build-rs-conditional/expected
@@ -0,0 +1,16 @@
+[TEST] Run verification...
+Checking harness verify::check_kani...
+Complete - 1 successfully verified harnesses, 0 failures, 1 total
+
+[TEST] Run playback...
+running 1 test\
+test verify::kani_concrete_playback_check_kani_\
+\
+test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 1 filtered out
+
+[TEST] Run test...
+running 1 test\
+test test::check_not_kani ... ok\
+\
+test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out
+
diff --git a/tests/script-based-pre/build-rs-conditional/src/lib.rs b/tests/script-based-pre/build-rs-conditional/src/lib.rs
new file mode 100644
index 000000000000..70df880fdc8b
--- /dev/null
+++ b/tests/script-based-pre/build-rs-conditional/src/lib.rs
@@ -0,0 +1,24 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! This tests ensures that build scripts are able to conditionally check if they are running under
+//! Kani (in both verification and playback mode).
+
+#[cfg(kani)]
+mod verify {
+    /// Running `cargo kani` should verify that "RUNNING_KANI" is equals to "Yes"
+    #[kani::proof]
+    fn check_kani() {
+        assert_eq!(env!("RUNNING_KANI"), "Yes");
+        // Add a dummy cover so playback generates a test that should succeed.
+        kani::cover!(kani::any());
+    }
+}
+
+#[cfg(test)]
+mod test {
+    /// Running `cargo test` should check that "RUNNING_KANI" is "No".
+    #[test]
+    fn check_not_kani() {
+        assert_eq!(env!("RUNNING_KANI"), "No");
+    }
+}

From ca66814dead93899859b014d5c61070116a44992 Mon Sep 17 00:00:00 2001
From: "github-actions[bot]"
 <41898282+github-actions[bot]@users.noreply.github.com>
Date: Mon, 10 Jul 2023 10:00:42 -0700
Subject: [PATCH 08/14] Automatic toolchain upgrade to nightly-2023-06-23
 (#2591)

Update Rust toolchain from nightly-2023-06-22 to nightly-2023-06-23 without any other source changes.
---
 rust-toolchain.toml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index 429669562eee..8db43261ba02 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2023-06-22"
+channel = "nightly-2023-06-23"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

From bb53ec2e4eb6937a5d45774d73307d74c74aa82d Mon Sep 17 00:00:00 2001
From: Kareem Khazem <karkhaz@amazon.com>
Date: Mon, 10 Jul 2023 18:41:39 +0100
Subject: [PATCH 09/14] Clean up benchmark directories after building (#2583)

This commit makes benchcomp delete fresh copies of benchmark directories after running the benchmark suite, by default. This is to save disk space, especially on CI machines which do not have enough disk space to run the perf suite. The new behavior can be turned off with the new --no-cleanup-run-dirs flag.
---
 tools/benchcomp/benchcomp/cmd_args.py  | 7 +++++++
 tools/benchcomp/benchcomp/entry/run.py | 8 +++++++-
 2 files changed, 14 insertions(+), 1 deletion(-)

diff --git a/tools/benchcomp/benchcomp/cmd_args.py b/tools/benchcomp/benchcomp/cmd_args.py
index 6a8e47d42250..d8b7e735824f 100644
--- a/tools/benchcomp/benchcomp/cmd_args.py
+++ b/tools/benchcomp/benchcomp/cmd_args.py
@@ -138,6 +138,13 @@ def _get_args_dict():
                         "help":
                             "do not make a fresh copy of the benchmark "
                             "directories before running each variant",
+                    }, {
+                        "flags": ["--keep-temps"],
+                        "action": "store_false",
+                        "dest": "cleanup_directory",
+                        "help":
+                            "do not delete fresh copies of benchmark "
+                            "directories after running each variant",
                     }],
                 },
                 "collate": {
diff --git a/tools/benchcomp/benchcomp/entry/run.py b/tools/benchcomp/benchcomp/entry/run.py
index d95ce8ab0d3a..a870e7e9a1b0 100644
--- a/tools/benchcomp/benchcomp/entry/run.py
+++ b/tools/benchcomp/benchcomp/entry/run.py
@@ -39,6 +39,7 @@ class _SingleInvocation:
     command_line: str
     directory: pathlib.Path
 
+    cleanup_directory: bool
     env: dict = dataclasses.field(default_factory=dict)
     timeout: int = None
     memout: int = None
@@ -85,6 +86,9 @@ def __call__(self):
                 encoding="utf-8") as handle:
             yaml.dump(suite, handle, default_flow_style=False)
 
+        if self.cleanup_directory and self.copy_benchmarks_dir:
+            shutil.rmtree(self.working_copy)
+
 
 @dataclasses.dataclass
 class _Run:
@@ -95,6 +99,7 @@ class _Run:
     out_dir: str
     out_symlink: str
     copy_benchmarks_dir: bool
+    cleanup_directory: bool
     result: dict = None
 
     def __call__(self):
@@ -110,6 +115,7 @@ def __call__(self):
                     suite_id, variant_id,
                     parse, suite_yaml_out_dir=out_path,
                     copy_benchmarks_dir=self.copy_benchmarks_dir,
+                    cleanup_directory=self.cleanup_directory,
                     **config)
                 invoke()
 
@@ -137,6 +143,6 @@ def get_default_out_prefix():
 def main(args):
     run = _Run(
         args.config, args.out_prefix, args.out_dir, args.out_symlink,
-        args.copy_benchmarks_dir)
+        args.copy_benchmarks_dir, args.cleanup_directory)
     run()
     return run

From f26b1cf928b88ad9eb424e0459d09a4c095abbb3 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
Date: Mon, 10 Jul 2023 16:41:38 -0400
Subject: [PATCH 10/14] Bump CBMC version to 5.87.0 (#2598)

---
 kani-dependencies | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/kani-dependencies b/kani-dependencies
index 0c2264b0f9b2..498182678d6f 100644
--- a/kani-dependencies
+++ b/kani-dependencies
@@ -1,4 +1,4 @@
-CBMC_VERSION="5.86.0"
+CBMC_VERSION="5.87.0"
 # If you update this version number, remember to bump it in `src/setup.rs` too
 CBMC_VIEWER_VERSION="3.8"
 KISSAT_VERSION="3.0.0"

From 634924bccdd23a54f659cb7c88ba21d2e487690d Mon Sep 17 00:00:00 2001
From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
Date: Mon, 10 Jul 2023 18:05:58 -0400
Subject: [PATCH 11/14] Update dependencies (#2599)

---
 Cargo.lock | 148 +++++++++++++++++++++++++++--------------------------
 1 file changed, 75 insertions(+), 73 deletions(-)

diff --git a/Cargo.lock b/Cargo.lock
index 353da79ace78..7b28de987528 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -174,9 +174,9 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
 
 [[package]]
 name = "clap"
-version = "4.3.8"
+version = "4.3.11"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d9394150f5b4273a1763355bd1c2ec54cc5a2593f790587bcd6b2c947cfa9211"
+checksum = "1640e5cc7fb47dbb8338fd471b105e7ed6c3cb2aeb00c2e067127ffd3764a05d"
 dependencies = [
  "clap_builder",
  "clap_derive",
@@ -185,13 +185,12 @@ dependencies = [
 
 [[package]]
 name = "clap_builder"
-version = "4.3.8"
+version = "4.3.11"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9a78fbdd3cc2914ddf37ba444114bc7765bbdcb55ec9cbe6fa054f0137400717"
+checksum = "98c59138d527eeaf9b53f35a77fcc1fad9d883116070c63d5de1c7dc7b00c72b"
 dependencies = [
  "anstream",
  "anstyle",
- "bitflags 1.3.2",
  "clap_lex",
  "once_cell",
  "strsim",
@@ -206,7 +205,7 @@ dependencies = [
  "heck",
  "proc-macro2",
  "quote",
- "syn 2.0.22",
+ "syn 2.0.25",
 ]
 
 [[package]]
@@ -432,15 +431,6 @@ version = "0.4.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "95505c38b4572b2d910cecb0281560f54b440a19336cbbcb27bf6ce6adc6f5a8"
 
-[[package]]
-name = "hermit-abi"
-version = "0.2.6"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ee512640fe35acbfb4bb779db6f0d80704c2cacfa2e39b601ef3e3f47d1ae4c7"
-dependencies = [
- "libc",
-]
-
 [[package]]
 name = "hermit-abi"
 version = "0.3.2"
@@ -468,11 +458,11 @@ dependencies = [
 
 [[package]]
 name = "is-terminal"
-version = "0.4.8"
+version = "0.4.9"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "24fddda5af7e54bf7da53067d6e802dbcc381d0a8eef629df528e3ebf68755cb"
+checksum = "cb0889898416213fab133e1d33a0e5858a48177452750691bde3666d0fdbaf8b"
 dependencies = [
- "hermit-abi 0.3.2",
+ "hermit-abi",
  "rustix",
  "windows-sys 0.48.0",
 ]
@@ -488,9 +478,9 @@ dependencies = [
 
 [[package]]
 name = "itoa"
-version = "1.0.6"
+version = "1.0.8"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "453ad9f582a441959e5f0d088b02ce04cfe8d51a8eaf077f12ac6d3e94164ca6"
+checksum = "62b02a5381cc465bd3041d84623d0fa3b66738b52b8e2fc3bab8ad63ab032f4a"
 
 [[package]]
 name = "kani"
@@ -563,7 +553,7 @@ dependencies = [
  "proc-macro-error",
  "proc-macro2",
  "quote",
- "syn 2.0.22",
+ "syn 2.0.25",
 ]
 
 [[package]]
@@ -626,7 +616,7 @@ version = "0.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "8263075bb86c5a1b1427b5ae862e8889656f126e9f77c484496e8b47cf5c5558"
 dependencies = [
- "regex-automata",
+ "regex-automata 0.1.10",
 ]
 
 [[package]]
@@ -750,11 +740,11 @@ dependencies = [
 
 [[package]]
 name = "num_cpus"
-version = "1.15.0"
+version = "1.16.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "0fac9e2da13b5eb447a6ce3d392f23a29d8694bff781bf03a16cd9ac8697593b"
+checksum = "4161fcb6d602d4d2081af7c3a45852d875a03dd337a6bfdd6e06407b61342a43"
 dependencies = [
- "hermit-abi 0.2.6",
+ "hermit-abi",
  "libc",
 ]
 
@@ -800,7 +790,7 @@ dependencies = [
  "libc",
  "redox_syscall",
  "smallvec",
- "windows-targets 0.48.0",
+ "windows-targets 0.48.1",
 ]
 
 [[package]]
@@ -811,9 +801,9 @@ checksum = "8835116a5c179084a830efb3adc117ab007512b535bc1a21c991d3b32a6b44dd"
 
 [[package]]
 name = "pin-project-lite"
-version = "0.2.9"
+version = "0.2.10"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e0a7ae3ac2f1173085d398531c705756c94a4c56843785df85a60c1a0afac116"
+checksum = "4c40d25201921e5ff0c862a505c6557ea88568a4e3ace775ab55e93f2f4f9d57"
 
 [[package]]
 name = "ppv-lite86"
@@ -847,9 +837,9 @@ dependencies = [
 
 [[package]]
 name = "proc-macro2"
-version = "1.0.63"
+version = "1.0.64"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7b368fba921b0dce7e60f5e04ec15e565b3303972b42bcfde1d0713b881959eb"
+checksum = "78803b62cbf1f46fde80d7c0e803111524b9877184cfe7c3033659490ac7a7da"
 dependencies = [
  "unicode-ident",
 ]
@@ -867,9 +857,9 @@ dependencies = [
 
 [[package]]
 name = "quote"
-version = "1.0.28"
+version = "1.0.29"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1b9ab9c7eadfd8df19006f1cf1a4aed13540ed5cbc047010ece5826e10825488"
+checksum = "573015e8ab27661678357f27dc26460738fd2b6c86e46f386fde94cb5d913105"
 dependencies = [
  "proc-macro2",
 ]
@@ -937,13 +927,14 @@ dependencies = [
 
 [[package]]
 name = "regex"
-version = "1.8.4"
+version = "1.9.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d0ab3ca65655bb1e41f2a8c8cd662eb4fb035e67c3f78da1d61dffe89d07300f"
+checksum = "b2eae68fc220f7cf2532e4494aded17545fce192d59cd996e0fe7887f4ceb575"
 dependencies = [
  "aho-corasick",
  "memchr",
- "regex-syntax 0.7.2",
+ "regex-automata 0.3.2",
+ "regex-syntax 0.7.3",
 ]
 
 [[package]]
@@ -955,6 +946,17 @@ dependencies = [
  "regex-syntax 0.6.29",
 ]
 
+[[package]]
+name = "regex-automata"
+version = "0.3.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "83d3daa6976cffb758ec878f108ba0e062a45b2d6ca3a2cca965338855476caf"
+dependencies = [
+ "aho-corasick",
+ "memchr",
+ "regex-syntax 0.7.3",
+]
+
 [[package]]
 name = "regex-syntax"
 version = "0.6.29"
@@ -963,9 +965,9 @@ checksum = "f162c6dd7b008981e4d40210aca20b4bd0f9b60ca9271061b07f78537722f2e1"
 
 [[package]]
 name = "regex-syntax"
-version = "0.7.2"
+version = "0.7.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "436b050e76ed2903236f032a59761c1eb99e1b0aead2c257922771dab1fc8c78"
+checksum = "2ab07dc67230e4a4718e70fd5c20055a4334b121f1f9db8fe63ef39ce9b8c846"
 
 [[package]]
 name = "rustc-demangle"
@@ -982,9 +984,9 @@ dependencies = [
 
 [[package]]
 name = "rustix"
-version = "0.38.2"
+version = "0.38.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "aabcb0461ebd01d6b79945797c27f8529082226cb630a9865a71870ff63532a4"
+checksum = "ac5ffa1efe7548069688cd7028f32591853cd7b5b756d41bcffd2353e4fc75b4"
 dependencies = [
  "bitflags 2.3.3",
  "errno",
@@ -995,15 +997,15 @@ dependencies = [
 
 [[package]]
 name = "rustversion"
-version = "1.0.12"
+version = "1.0.13"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "4f3208ce4d8448b3f3e7d168a73f5e0c43a61e32930de3bceeccedb388b6bf06"
+checksum = "dc31bd9b61a32c31f9650d18add92aa83a49ba979c143eefd27fe7177b05bd5f"
 
 [[package]]
 name = "ryu"
-version = "1.0.13"
+version = "1.0.14"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f91339c0467de62360649f8d3e185ca8de4224ff281f66000de5eb2a77a79041"
+checksum = "fe232bdf6be8c8de797b22184ee71118d63780ea42ac85b61d1baa6d3b782ae9"
 
 [[package]]
 name = "same-file"
@@ -1031,29 +1033,29 @@ dependencies = [
 
 [[package]]
 name = "serde"
-version = "1.0.164"
+version = "1.0.171"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9e8c8cf938e98f769bc164923b06dce91cea1751522f46f8466461af04c9027d"
+checksum = "30e27d1e4fd7659406c492fd6cfaf2066ba8773de45ca75e855590f856dc34a9"
 dependencies = [
  "serde_derive",
 ]
 
 [[package]]
 name = "serde_derive"
-version = "1.0.164"
+version = "1.0.171"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d9735b638ccc51c28bf6914d90a2e9725b377144fc612c49a611fddd1b631d68"
+checksum = "389894603bd18c46fa56231694f8d827779c0951a667087194cf9de94ed24682"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.22",
+ "syn 2.0.25",
 ]
 
 [[package]]
 name = "serde_json"
-version = "1.0.99"
+version = "1.0.100"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "46266871c240a00b8f503b877622fe33430b3c7d963bdc0f2adc511e54a1eae3"
+checksum = "0f1e14e89be7aa4c4b78bdbdc9eb5bf8517829a600ae8eaa39a6e1d960b5185c"
 dependencies = [
  "itoa",
  "ryu",
@@ -1071,9 +1073,9 @@ dependencies = [
 
 [[package]]
 name = "serde_test"
-version = "1.0.164"
+version = "1.0.171"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "797c38160e2546a56e1e3439496439597e938669673ffd8af02a12f070da648f"
+checksum = "b6480a2f4e1449ec9757ea143362ad5cea79bc7f1cb7711c06e1c5d03b6b5a3a"
 dependencies = [
  "serde",
 ]
@@ -1138,9 +1140,9 @@ dependencies = [
 
 [[package]]
 name = "smallvec"
-version = "1.10.0"
+version = "1.11.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a507befe795404456341dfab10cef66ead4c041f62b8b11bbb92bffe5d0953e0"
+checksum = "62bb4feee49fdd9f707ef802e22365a35de4b7b299de4763d44bfea899442ff9"
 
 [[package]]
 name = "std"
@@ -1198,9 +1200,9 @@ dependencies = [
 
 [[package]]
 name = "syn"
-version = "2.0.22"
+version = "2.0.25"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "2efbeae7acf4eabd6bcdcbd11c92f45231ddda7539edc7806bd1a04a03b24616"
+checksum = "15e3fc8c0c74267e2df136e5e5fb656a464158aa57624053375eb9c8c6e25ae2"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -1209,22 +1211,22 @@ dependencies = [
 
 [[package]]
 name = "thiserror"
-version = "1.0.40"
+version = "1.0.43"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "978c9a314bd8dc99be594bc3c175faaa9794be04a5a5e153caba6915336cebac"
+checksum = "a35fc5b8971143ca348fa6df4f024d4d55264f3468c71ad1c2f365b0a4d58c42"
 dependencies = [
  "thiserror-impl",
 ]
 
 [[package]]
 name = "thiserror-impl"
-version = "1.0.40"
+version = "1.0.43"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f9456a42c5b0d803c8cd86e73dd7cc9edd429499f37a3550d286d5e86720569f"
+checksum = "463fe12d7993d3b327787537ce8dd4dfa058de32fc2b195ef3cde03dc4771e8f"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.22",
+ "syn 2.0.25",
 ]
 
 [[package]]
@@ -1239,9 +1241,9 @@ dependencies = [
 
 [[package]]
 name = "toml"
-version = "0.7.5"
+version = "0.7.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1ebafdf5ad1220cb59e7d17cf4d2c72015297b75b19a10472f99b89225089240"
+checksum = "c17e963a819c331dcacd7ab957d80bc2b9a9c1e71c804826d2f283dd65306542"
 dependencies = [
  "serde",
  "serde_spanned",
@@ -1260,9 +1262,9 @@ dependencies = [
 
 [[package]]
 name = "toml_edit"
-version = "0.19.11"
+version = "0.19.12"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "266f016b7f039eec8a1a80dfe6156b633d208b9fccca5e4db1d6775b0c4e34a7"
+checksum = "c500344a19072298cd05a7224b3c0c629348b78692bf48466c5238656e315a78"
 dependencies = [
  "indexmap",
  "serde",
@@ -1291,7 +1293,7 @@ checksum = "5f4f31f56159e98206da9efd823404b79b6ef3143b4a7ab76e67b1751b25a4ab"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.22",
+ "syn 2.0.25",
 ]
 
 [[package]]
@@ -1358,9 +1360,9 @@ dependencies = [
 
 [[package]]
 name = "unicode-ident"
-version = "1.0.9"
+version = "1.0.10"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b15811caf2415fb889178633e7724bad2509101cde276048e013b9def5e51fa0"
+checksum = "22049a19f4a68748a168c0fc439f9516686aa045927ff767eca0a85101fb6e73"
 
 [[package]]
 name = "unicode-width"
@@ -1474,7 +1476,7 @@ version = "0.48.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "677d2418bec65e3338edb076e806bc1ec15693c5d0104683f2efe857f61056a9"
 dependencies = [
- "windows-targets 0.48.0",
+ "windows-targets 0.48.1",
 ]
 
 [[package]]
@@ -1494,9 +1496,9 @@ dependencies = [
 
 [[package]]
 name = "windows-targets"
-version = "0.48.0"
+version = "0.48.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7b1eb6f0cd7c80c79759c929114ef071b87354ce476d9d94271031c0497adfd5"
+checksum = "05d4b17490f70499f20b9e791dcf6a299785ce8af4d709018206dc5b4953e95f"
 dependencies = [
  "windows_aarch64_gnullvm 0.48.0",
  "windows_aarch64_msvc 0.48.0",
@@ -1593,9 +1595,9 @@ checksum = "1a515f5799fe4961cb532f983ce2b23082366b898e52ffbce459c86f67c8378a"
 
 [[package]]
 name = "winnow"
-version = "0.4.7"
+version = "0.4.9"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ca0ace3845f0d96209f0375e6d367e3eb87eb65d27d445bdc9f1843a26f39448"
+checksum = "81a2094c43cc94775293eaa0e499fbc30048a6d824ac82c0351a8c0bf9112529"
 dependencies = [
  "memchr",
 ]

From 5bd66d7a352f65ef818c72df954cc01625d2dc26 Mon Sep 17 00:00:00 2001
From: "github-actions[bot]"
 <41898282+github-actions[bot]@users.noreply.github.com>
Date: Tue, 11 Jul 2023 16:13:40 -0400
Subject: [PATCH 12/14] Automatic toolchain upgrade to nightly-2023-06-24
 (#2600)

Co-authored-by: celinval <celinval@users.noreply.github.com>
---
 rust-toolchain.toml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index 8db43261ba02..1935a8e3142a 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2023-06-23"
+channel = "nightly-2023-06-24"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

From ef055290267fd7a857eec7744e480288e98c8172 Mon Sep 17 00:00:00 2001
From: "Felipe R. Monteiro" <rms.felipe@gmail.com>
Date: Tue, 11 Jul 2023 17:11:47 -0400
Subject: [PATCH 13/14] Adds posix_memalign to the list of supported builtins
 (#2601)

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
---
 cprover_bindings/src/goto_program/builtin.rs |  5 +++
 tests/kani/LibC/posix_memalign.rs            | 46 ++++++++++++++++++++
 2 files changed, 51 insertions(+)
 create mode 100644 tests/kani/LibC/posix_memalign.rs

diff --git a/cprover_bindings/src/goto_program/builtin.rs b/cprover_bindings/src/goto_program/builtin.rs
index dc703ce83edc..258691b9ade4 100644
--- a/cprover_bindings/src/goto_program/builtin.rs
+++ b/cprover_bindings/src/goto_program/builtin.rs
@@ -47,6 +47,7 @@ pub enum BuiltinFn {
     Memset,
     Nearbyint,
     Nearbyintf,
+    Posixmemalign,
     Pow,
     Powf,
     Powi,
@@ -109,6 +110,7 @@ impl ToString for BuiltinFn {
             Memset => "memset",
             Nearbyint => "nearbyint",
             Nearbyintf => "nearbyintf",
+            Posixmemalign => "posix_memalign",
             Pow => "pow",
             Powf => "powf",
             Powi => "__builtin_powi",
@@ -173,6 +175,7 @@ impl BuiltinFn {
             Memset => vec![Type::void_pointer(), Type::c_int(), Type::size_t()],
             Nearbyint => vec![Type::double()],
             Nearbyintf => vec![Type::float()],
+            Posixmemalign => vec![Type::void_pointer(), Type::size_t(), Type::size_t()],
             Powf => vec![Type::float(), Type::float()],
             Powi => vec![Type::double(), Type::c_int()],
             Powif => vec![Type::float(), Type::c_int()],
@@ -234,6 +237,7 @@ impl BuiltinFn {
             Memset => Type::void_pointer(),
             Nearbyint => Type::double(),
             Nearbyintf => Type::float(),
+            Posixmemalign => Type::c_int(),
             Pow => Type::double(),
             Powf => Type::float(),
             Powi => Type::double(),
@@ -296,6 +300,7 @@ impl BuiltinFn {
             Memset,
             Nearbyint,
             Nearbyintf,
+            Posixmemalign,
             Pow,
             Powf,
             Powi,
diff --git a/tests/kani/LibC/posix_memalign.rs b/tests/kani/LibC/posix_memalign.rs
new file mode 100644
index 000000000000..dc4aa5aeaae0
--- /dev/null
+++ b/tests/kani/LibC/posix_memalign.rs
@@ -0,0 +1,46 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+//! Check support for `posix_memalign`.
+
+#![feature(rustc_private)]
+#![feature(allocator_api)]
+extern crate libc;
+
+use std::alloc::{Allocator, Layout, System};
+use std::ptr;
+
+#[repr(C, align(32))]
+struct MyStruct {
+    data: [u128; 10],
+}
+
+#[kani::proof]
+fn alloc_zeroed() {
+    let layout = Layout::new::<MyStruct>();
+    let ptr = System.allocate_zeroed(layout).unwrap();
+    assert_eq!(unsafe { ptr.as_ref()[0] }, 0);
+}
+
+// Source rust/src/libstd/sys/unix/alloc.rs
+unsafe fn aligned_malloc(layout: &Layout) -> *mut u8 {
+    let mut out = ptr::null_mut();
+    let ret = libc::posix_memalign(&mut out, layout.align(), layout.size());
+    if ret != 0 { ptr::null_mut() } else { out as *mut u8 }
+}
+
+#[kani::proof]
+fn aligned_malloc_main() {
+    let mut layout = Layout::from_size_align(0, 1);
+    let _mem = unsafe { aligned_malloc(&layout.unwrap()) };
+}
+
+#[kani::proof]
+fn posix_memalign_incorrect_alignment() {
+    let mut out = ptr::null_mut();
+    let small_page_size = 1;
+    let size = 4;
+    assert_eq!(unsafe { libc::posix_memalign(&mut out, small_page_size, size) }, libc::EINVAL);
+    let incorrect_page_size = 13;
+    assert_eq!(unsafe { libc::posix_memalign(&mut out, incorrect_page_size, size) }, libc::EINVAL);
+}

From 06c0fbe60d793f8b47fadc5fc5a83932e96f2389 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
Date: Wed, 12 Jul 2023 12:14:28 -0400
Subject: [PATCH 14/14] Bump Kani version to 0.32.0 (#2602)

---
 CHANGELOG.md                   | 14 ++++++++++++++
 Cargo.lock                     | 18 +++++++++---------
 Cargo.toml                     |  2 +-
 cprover_bindings/Cargo.toml    |  2 +-
 kani-compiler/Cargo.toml       |  2 +-
 kani-driver/Cargo.toml         |  2 +-
 kani_metadata/Cargo.toml       |  2 +-
 library/kani/Cargo.toml        |  2 +-
 library/kani_macros/Cargo.toml |  2 +-
 library/std/Cargo.toml         |  2 +-
 tools/build-kani/Cargo.toml    |  2 +-
 11 files changed, 32 insertions(+), 18 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 37f29f7df732..659057b2a987 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -4,6 +4,20 @@ 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.32.0]
+
+## What's Changed
+
+* Add kani::spawn and an executor to the Kani library by @fzaiser in https://github.com/model-checking/kani/pull/1659
+* Add "kani" configuration key to enable conditional compilation in build scripts by @celinval in https://github.com/model-checking/kani/pull/2297
+* Adds posix_memalign to the list of supported builtins by @feliperodri in https://github.com/model-checking/kani/pull/2601
+* Upgrade rust toolchain to nightly-2023-06-20 by @celinval in https://github.com/model-checking/kani/pull/2551
+* Update rust toolchain to 2023-06-22 by @celinval in https://github.com/model-checking/kani/pull/2588
+* Automatic toolchain upgrade to nightly-2023-06-24 by @github-actions in https://github.com/model-checking/kani/pull/2600
+* Bump CBMC version to 5.87.0 by @adpaco-aws in https://github.com/model-checking/kani/pull/2598
+
+**Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.31.0...kani-0.32.0
+
 ## [0.31.0]
 
 ## What's Changed
diff --git a/Cargo.lock b/Cargo.lock
index 7b28de987528..0847cd2f318a 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -120,7 +120,7 @@ dependencies = [
 
 [[package]]
 name = "build-kani"
-version = "0.31.0"
+version = "0.32.0"
 dependencies = [
  "anyhow",
  "cargo_metadata",
@@ -264,7 +264,7 @@ dependencies = [
 
 [[package]]
 name = "cprover_bindings"
-version = "0.31.0"
+version = "0.32.0"
 dependencies = [
  "lazy_static",
  "linear-map",
@@ -484,14 +484,14 @@ checksum = "62b02a5381cc465bd3041d84623d0fa3b66738b52b8e2fc3bab8ad63ab032f4a"
 
 [[package]]
 name = "kani"
-version = "0.31.0"
+version = "0.32.0"
 dependencies = [
  "kani_macros",
 ]
 
 [[package]]
 name = "kani-compiler"
-version = "0.31.0"
+version = "0.32.0"
 dependencies = [
  "clap",
  "cprover_bindings",
@@ -512,7 +512,7 @@ dependencies = [
 
 [[package]]
 name = "kani-driver"
-version = "0.31.0"
+version = "0.32.0"
 dependencies = [
  "anyhow",
  "cargo_metadata",
@@ -539,7 +539,7 @@ dependencies = [
 
 [[package]]
 name = "kani-verifier"
-version = "0.31.0"
+version = "0.32.0"
 dependencies = [
  "anyhow",
  "home",
@@ -548,7 +548,7 @@ dependencies = [
 
 [[package]]
 name = "kani_macros"
-version = "0.31.0"
+version = "0.32.0"
 dependencies = [
  "proc-macro-error",
  "proc-macro2",
@@ -558,7 +558,7 @@ dependencies = [
 
 [[package]]
 name = "kani_metadata"
-version = "0.31.0"
+version = "0.32.0"
 dependencies = [
  "cprover_bindings",
  "serde",
@@ -1146,7 +1146,7 @@ checksum = "62bb4feee49fdd9f707ef802e22365a35de4b7b299de4763d44bfea899442ff9"
 
 [[package]]
 name = "std"
-version = "0.31.0"
+version = "0.32.0"
 dependencies = [
  "kani",
 ]
diff --git a/Cargo.toml b/Cargo.toml
index e87c98d5241a..bb0dffcfaf1f 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani-verifier"
-version = "0.31.0"
+version = "0.32.0"
 edition = "2021"
 description = "A bit-precise model checker for Rust."
 readme = "README.md"
diff --git a/cprover_bindings/Cargo.toml b/cprover_bindings/Cargo.toml
index aad7ccc3c858..938b93606fd2 100644
--- a/cprover_bindings/Cargo.toml
+++ b/cprover_bindings/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "cprover_bindings"
-version = "0.31.0"
+version = "0.32.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false
diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml
index f0baa6f7047d..f23fc40e4b8c 100644
--- a/kani-compiler/Cargo.toml
+++ b/kani-compiler/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani-compiler"
-version = "0.31.0"
+version = "0.32.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false
diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml
index b6a89a72dc09..a4385206f83f 100644
--- a/kani-driver/Cargo.toml
+++ b/kani-driver/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani-driver"
-version = "0.31.0"
+version = "0.32.0"
 edition = "2021"
 description = "Build a project with Kani and run all proof harnesses"
 license = "MIT OR Apache-2.0"
diff --git a/kani_metadata/Cargo.toml b/kani_metadata/Cargo.toml
index 1f71406bbad3..7b908e068fa5 100644
--- a/kani_metadata/Cargo.toml
+++ b/kani_metadata/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani_metadata"
-version = "0.31.0"
+version = "0.32.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false
diff --git a/library/kani/Cargo.toml b/library/kani/Cargo.toml
index 2dfd1e5e5291..8d44bb760367 100644
--- a/library/kani/Cargo.toml
+++ b/library/kani/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani"
-version = "0.31.0"
+version = "0.32.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false
diff --git a/library/kani_macros/Cargo.toml b/library/kani_macros/Cargo.toml
index bfcdcb64afc0..78b8fbb529da 100644
--- a/library/kani_macros/Cargo.toml
+++ b/library/kani_macros/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani_macros"
-version = "0.31.0"
+version = "0.32.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false
diff --git a/library/std/Cargo.toml b/library/std/Cargo.toml
index 3ed8810f0c1d..3cad55b31167 100644
--- a/library/std/Cargo.toml
+++ b/library/std/Cargo.toml
@@ -5,7 +5,7 @@
 # Note: this package is intentionally named std to make sure the names of
 # standard library symbols are preserved
 name = "std"
-version = "0.31.0"
+version = "0.32.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false
diff --git a/tools/build-kani/Cargo.toml b/tools/build-kani/Cargo.toml
index eb4f686bc9f3..22a3d5d864e8 100644
--- a/tools/build-kani/Cargo.toml
+++ b/tools/build-kani/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "build-kani"
-version = "0.31.0"
+version = "0.32.0"
 edition = "2021"
 description = "Builds Kani, Sysroot and release bundle."
 license = "MIT OR Apache-2.0"