From 9f306999d26a965f912fd6e70533f7272fdc2b53 Mon Sep 17 00:00:00 2001
From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
Date: Wed, 16 Aug 2023 09:35:59 -0700
Subject: [PATCH] Upgrade Rust toolchain to 2023-08-14 (#2688)

---
 .../codegen/intrinsic.rs                      | 38 +++++++++++++++++++
 .../compiler_interface.rs                     |  2 +-
 rust-toolchain.toml                           |  2 +-
 3 files changed, 40 insertions(+), 2 deletions(-)

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index 10fe28caf9bd..8fc2742f2824 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -4,6 +4,7 @@
 use super::typ::{self, pointee_type};
 use super::PropertyClass;
 use crate::codegen_cprover_gotoc::GotocCtx;
+use crate::unwrap_or_return_codegen_unimplemented_stmt;
 use cbmc::goto_program::{
     ArithmeticOverflowResult, BinaryOperator, BuiltinFn, Expr, Location, Stmt, Type,
 };
@@ -408,6 +409,7 @@ impl<'tcx> GotocCtx<'tcx> {
             ),
             "ceilf32" => codegen_simple_intrinsic!(Ceilf),
             "ceilf64" => codegen_simple_intrinsic!(Ceil),
+            "compare_bytes" => self.codegen_compare_bytes(fargs, p, loc),
             "copy" => self.codegen_copy(intrinsic, false, fargs, farg_types, Some(p), loc),
             "copy_nonoverlapping" => unreachable!(
                 "Expected `core::intrinsics::unreachable` to be handled by `StatementKind::CopyNonOverlapping`"
@@ -987,6 +989,42 @@ impl<'tcx> GotocCtx<'tcx> {
         Stmt::block(vec![src_align_check, dst_align_check, overflow_check, copy_expr], loc)
     }
 
+    /// This is an intrinsic that was added in
+    /// https://github.com/rust-lang/rust/pull/114382 that is essentially the
+    /// same as memcmp: it compares two slices up to the specified length.
+    /// The implementation is the same as the hook for `memcmp`.
+    pub fn codegen_compare_bytes(
+        &mut self,
+        mut fargs: Vec<Expr>,
+        p: &Place<'tcx>,
+        loc: Location,
+    ) -> Stmt {
+        let lhs = fargs.remove(0).cast_to(Type::void_pointer());
+        let rhs = fargs.remove(0).cast_to(Type::void_pointer());
+        let len = fargs.remove(0);
+        let (len_var, len_decl) = self.decl_temp_variable(len.typ().clone(), Some(len), loc);
+        let (lhs_var, lhs_decl) = self.decl_temp_variable(lhs.typ().clone(), Some(lhs), loc);
+        let (rhs_var, rhs_decl) = self.decl_temp_variable(rhs.typ().clone(), Some(rhs), loc);
+        let is_len_zero = len_var.clone().is_zero();
+        // We have to ensure that the pointers are valid even if we're comparing zero bytes.
+        // According to Rust's current definition (see https://github.com/model-checking/kani/issues/1489),
+        // this means they have to be non-null and aligned.
+        // But alignment is automatically satisfied because `memcmp` takes `*const u8` pointers.
+        let is_lhs_ok = lhs_var.clone().is_nonnull();
+        let is_rhs_ok = rhs_var.clone().is_nonnull();
+        let should_skip_pointer_checks = is_len_zero.and(is_lhs_ok).and(is_rhs_ok);
+        let place_expr =
+            unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(&p)).goto_expr;
+        let res = should_skip_pointer_checks.ternary(
+            Expr::int_constant(0, place_expr.typ().clone()), // zero bytes are always equal (as long as pointers are nonnull and aligned)
+            BuiltinFn::Memcmp
+                .call(vec![lhs_var, rhs_var, len_var], loc)
+                .cast_to(place_expr.typ().clone()),
+        );
+        let code = place_expr.assign(res, loc).with_location(loc);
+        Stmt::block(vec![len_decl, lhs_decl, rhs_decl, code], loc)
+    }
+
     // In some contexts (e.g., compilation-time evaluation),
     // `ptr_guaranteed_cmp` compares two pointers and returns:
     //  * 2 if the result is unknown.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
index f30ed663338a..dcdf6a8bfaf9 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
@@ -345,7 +345,7 @@ impl CodegenBackend for GotocCodegenBackend {
         codegen_results: CodegenResults,
         outputs: &OutputFilenames,
     ) -> Result<(), ErrorGuaranteed> {
-        let requested_crate_types = sess.crate_types();
+        let requested_crate_types = &codegen_results.crate_info.crate_types;
         for crate_type in requested_crate_types {
             let out_fname = out_filename(
                 sess,
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index 05c389240d94..092249141840 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-08-07"
+channel = "nightly-2023-08-14"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]