From e2856c701c2ef5a0a33bb39eb046a4e8c8746f2f Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 5 Apr 2024 11:33:12 +0000
Subject: [PATCH] Update the rust toolchain to nightly-2024-04-03

Changes required due to:
- rust-lang/rust@3da115a93b Add Ord::cmp for primitives as a BinOp in MIR

Resolves: #31XX
---
 .../src/codegen_cprover_gotoc/codegen/rvalue.rs        | 10 +++++++++-
 rust-toolchain.toml                                    |  2 +-
 .../{write_invalid_fixme.rs => write_invalid.rs}       |  0
 3 files changed, 10 insertions(+), 2 deletions(-)
 rename tests/kani/ValidValues/{write_invalid_fixme.rs => write_invalid.rs} (100%)

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index 74622d41ed50..14e789930f93 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -376,7 +376,7 @@ impl<'tcx> GotocCtx<'tcx> {
             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 => {
+            BinOp::Eq | BinOp::Lt | BinOp::Le | BinOp::Ne | BinOp::Ge | BinOp::Gt | BinOp::Cmp => {
                 let op_ty = self.operand_ty_stable(e1);
                 if self.is_fat_pointer_stable(op_ty) {
                     self.codegen_comparison_fat_ptr(op, e1, e2, loc)
@@ -1465,6 +1465,14 @@ fn comparison_expr(op: &BinOp, left: Expr, right: Expr, is_float: bool) -> Expr
         }
         BinOp::Ge => left.ge(right),
         BinOp::Gt => left.gt(right),
+        BinOp::Cmp => {
+            // Implement https://doc.rust-lang.org/core/cmp/trait.Ord.html as done in cranelift,
+            // i.e., (left > right) - (left < right)
+            left.clone()
+                .gt(right.clone())
+                .cast_to(Type::c_int())
+                .sub(left.lt(right).cast_to(Type::c_int()))
+        }
         _ => unreachable!(),
     }
 }
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index eee073e29a89..31f9e45dd714 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-03-29"
+channel = "nightly-2024-04-03"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
diff --git a/tests/kani/ValidValues/write_invalid_fixme.rs b/tests/kani/ValidValues/write_invalid.rs
similarity index 100%
rename from tests/kani/ValidValues/write_invalid_fixme.rs
rename to tests/kani/ValidValues/write_invalid.rs