From cb9581a4166b36112b2649a506b2ea884da53bcc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?S=C3=B6ren=20Tempel?= <tempel@uni-bremen.de>
Date: Thu, 18 Apr 2024 17:31:45 +0200
Subject: [PATCH] Cleanup handling of signed overflow

---
 lib/LibRISCV/Semantics/RV_M/Default.hs | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

diff --git a/lib/LibRISCV/Semantics/RV_M/Default.hs b/lib/LibRISCV/Semantics/RV_M/Default.hs
index 1c9260d..8f73f21 100644
--- a/lib/LibRISCV/Semantics/RV_M/Default.hs
+++ b/lib/LibRISCV/Semantics/RV_M/Default.hs
@@ -43,6 +43,13 @@ instrSemantics width =
 
         extract32 :: Int -> Expr v -> Expr v
         extract32 = flip Extract 32
+
+        mostNegative :: Integer
+        mostNegative = 2^(width - 1)
+
+        -- Signed division overflow occurs when the most-negative integer is divided by -1.
+        sdivOverflow :: v -> v -> Expr v
+        sdivOverflow n divisor = (n `immEqInt` mostNegative) `And` (divisor `immEqInt` (-1))
     in \case
     MUL -> do
         (r1, r2, rd) <- decodeAndReadRType
@@ -70,10 +77,9 @@ instrSemantics width =
         writeRegister rd res
     DIV -> do
         (r1, r2, rd) <- decodeAndReadRType
-
         ifExprM (r2 `immEqInt` 0)
             do writeRegister rd mask1
-            do ifExprM ((r1 `immEqInt` fromIntegral (minBound :: Int32)) `And` mask1)
+            do ifExprM (sdivOverflow r1 r2)
                 do writeRegister rd $ FromImm r1
                 do writeRegister rd $ r1 `sdiv` r2
     DIVU -> do
@@ -85,7 +91,7 @@ instrSemantics width =
         (r1, r2, rd) <- decodeAndReadRType
         ifExprM (r2 `immEqInt` 0)
             do writeRegister rd $ FromImm r1
-            do ifExprM ((r1 `immEqInt` fromIntegral (minBound :: Int32)) `And` (r2 `immEqInt` 0xFFFFFFFF))
+            do ifExprM (sdivOverflow r1 r2)
                 do writeRegister rd $ fromUInt 0
                 do writeRegister rd $ r1 `srem` r2
     REMU -> do