Override carrying_mul_add in cg_llvm

model-checking · Feb 20, 2025 · 929ca0c · 929ca0c
1 parent 17ab595
commit 929ca0c
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 2 deletions.
diff --git a/core/src/intrinsics/fallback.rs b/core/src/intrinsics/fallback.rs
@@ -100,8 +100,8 @@ impl const CarryingMulAdd for i128 {
     fn carrying_mul_add(self, b: i128, c: i128, d: i128) -> (u128, i128) {
         let (low, high) = wide_mul_u128(self as u128, b as u128);
         let mut high = high as i128;
-        high = high.wrapping_add((self >> 127) * b);
-        high = high.wrapping_add(self * (b >> 127));
+        high = high.wrapping_add(i128::wrapping_mul(self >> 127, b));
+        high = high.wrapping_add(i128::wrapping_mul(self, b >> 127));
         let (low, carry) = u128::overflowing_add(low, c as u128);
         high = high.wrapping_add((carry as i128) + (c >> 127));
         let (low, carry) = u128::overflowing_add(low, d as u128);

diff --git a/core/tests/intrinsics.rs b/core/tests/intrinsics.rs
@@ -153,6 +153,7 @@ fn carrying_mul_add_fallback_i32() {
 
 #[test]
 fn carrying_mul_add_fallback_u128() {
+    assert_eq!(fallback_cma::<u128>(u128::MAX, u128::MAX, 0, 0), (1, u128::MAX - 1));
     assert_eq!(fallback_cma::<u128>(1, 1, 1, 1), (3, 0));
     assert_eq!(fallback_cma::<u128>(0, 0, u128::MAX, u128::MAX), (u128::MAX - 1, 1));
     assert_eq!(
@@ -178,8 +179,17 @@ fn carrying_mul_add_fallback_u128() {
 
 #[test]
 fn carrying_mul_add_fallback_i128() {
+    assert_eq!(fallback_cma::<i128>(-1, -1, 0, 0), (1, 0));
     let r = fallback_cma::<i128>(-1, -1, -1, -1);
     assert_eq!(r, (u128::MAX, -1));
     let r = fallback_cma::<i128>(1, -1, 1, 1);
     assert_eq!(r, (1, 0));
+    assert_eq!(
+        fallback_cma::<i128>(i128::MAX, i128::MAX, i128::MAX, i128::MAX),
+        (u128::MAX, i128::MAX / 2),
+    );
+    assert_eq!(
+        fallback_cma::<i128>(i128::MIN, i128::MIN, i128::MAX, i128::MAX),
+        (u128::MAX - 1, -(i128::MIN / 2)),
+    );
 }