Use parentheses in the assert_eq macros to avoid chained comparison operators error (model-checking#1202)

Author: zhassan-aws

library/std/src/lib.rs

@@ -63,20 +63,24 @@ macro_rules! assert {
 #[macro_export]
 macro_rules! assert_eq {
     ($left:expr, $right:expr $(,)?) => ({
-        assert!($left == $right);
+        // Add parentheses around the operands to avoid a "comparison operators
+        // cannot be chained" error, but exclude the parentheses in the message
+        kani::assert(($left) == ($right), concat!("assertion failed: ", stringify!($left == $right)));
     });
     ($left:expr, $right:expr, $($arg:tt)+) => ({
-        assert!($left == $right, $($arg)+);
+        assert!(($left) == ($right), $($arg)+);
     });
 }
 
 #[macro_export]
 macro_rules! assert_ne {
     ($left:expr, $right:expr $(,)?) => ({
-        assert!($left != $right);
+        // Add parentheses around the operands to avoid a "comparison operators
+        // cannot be chained" error, but exclude the parentheses in the message
+        kani::assert(($left) != ($right), concat!("assertion failed: ", stringify!($left != $right)));
     });
     ($left:expr, $right:expr, $($arg:tt)+) => ({
-        assert!($left != $right, $($arg)+);
+        assert!(($left) != ($right), $($arg)+);
     });
 }
 

tests/expected/assert-eq-chained/expected

@@ -0,0 +1,13 @@
+Status: SUCCESS\
+Description: "assertion failed: x > 3 == true"
+
+Status: SUCCESS\
+Description: "assertion failed: x == 1 == false"
+
+Status: SUCCESS\
+Description: "assertion failed: x < 10 != false"
+
+Status: FAILURE\
+Description: "assertion failed: x == 7 != false"
+
+VERIFICATION:- FAILED

tests/expected/assert-eq-chained/main.rs

@@ -0,0 +1,14 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This test checks that chained operators work with Kani's overridden assert_eq
+// macros
+
+#[kani::proof]
+fn check_chained_operators() {
+    let x = 5;
+    assert_eq!(x > 3, true);
+    debug_assert_eq!(x == 1, false);
+    assert_ne!(x < 10, false);
+    debug_assert_ne!(x == 7, false); // fails
+}