Cleanup formal description of M-extension

agra-uni-bremen · Apr 16, 2024 · 107418a · 107418a
1 parent 3aec407
commit 107418a
Showing 1 changed file with 23 additions and 15 deletions.
diff --git a/lib/LibRISCV/Semantics/RV_M/Default.hs b/lib/LibRISCV/Semantics/RV_M/Default.hs
@@ -25,63 +25,71 @@ import Data.BitVector (ones)
 import Control.Monad.Extra (whenM, ifM)
 import Data.Function (on)
 
-instrSemantics :: forall v r . (Member (Operations v) r, Member LogInstructionFetch r, Member (Decoding v) r, Member (ExprEval v) r) => Int -> RV_M -> Eff r ()
+instrSemantics :: forall v r .
+  ( Member (Operations v) r
+  , Member LogInstructionFetch r
+  , Member (Decoding v) r
+  , Member (ExprEval v) r) => Int -> RV_M -> Eff r ()
 instrSemantics width =
     let
+        fromUInt :: Integer -> Expr v
         fromUInt = FromInt width
+
+        immEqInt :: v -> Integer -> Expr v
+        immEqInt imm int = FromImm imm `Eq` fromUInt int
+
+        mask1 :: Expr v
         mask1 = FromInt width (2^width - 1)
-        extract32 = flip Extract 32
 
-        -- False if a given address is not aligned at the four-byte boundary.
-        isMisaligned :: Expr v -> Expr v
-        isMisaligned addr = (addr `And` fromUInt 0x3) `Uge` fromUInt 1
+        extract32 :: Int -> Expr v -> Expr v
+        extract32 = flip Extract 32
     in \case
     MUL -> do
-        (r1, r2, rd) <- decodeAndReadRType @v
+        (r1, r2, rd) <- decodeAndReadRType
         let
             multRes = (Mul `on` sextImm 32) r1 r2
             res = extract32 0 multRes
         writeRegister rd res
     MULH -> do
-        (r1, r2, rd) <- decodeAndReadRType @v
+        (r1, r2, rd) <- decodeAndReadRType
         let
             multRes = (Mul `on` sextImm 32) r1 r2
             res = extract32 32 multRes
         writeRegister rd res
     MULHU -> do
-        (r1, r2, rd) <- decodeAndReadRType @v
+        (r1, r2, rd) <- decodeAndReadRType
         let
             multRes = (Mul `on` zextImm 32) r1 r2
             res = extract32 32 multRes
         writeRegister rd res
     MULHSU -> do
-        (r1, r2, rd) <- decodeAndReadRType @v
+        (r1, r2, rd) <- decodeAndReadRType
         let
             multRes = sextImm 32 r1 `Mul` zextImm 32 r2
             res = extract32 32 multRes
         writeRegister rd res
     DIV -> do
         (r1, r2, rd) <- decodeAndReadRType
 
-        ifExprM (FromImm r2 `Eq` fromUInt 0)
+        ifExprM (r2 `immEqInt` 0)
             do writeRegister rd mask1
-            do ifExprM ((FromImm r1 `Eq` fromUInt (fromIntegral (minBound :: Int32))) `And` mask1)
+            do ifExprM ((r1 `immEqInt` fromIntegral (minBound :: Int32)) `And` mask1)
                 do writeRegister rd $ FromImm r1
                 do writeRegister rd $ r1 `sdiv` r2
     DIVU -> do
         (r1, r2, rd) <- decodeAndReadRType
-        ifExprM (FromImm r2 `Eq` fromUInt 0)
+        ifExprM (r2 `immEqInt` 0)
             do writeRegister rd mask1
             do writeRegister rd $ r1 `udiv` r2
     REM -> do
         (r1, r2, rd) <- decodeAndReadRType
-        ifExprM (FromImm r2 `Eq` fromUInt 0)
+        ifExprM (r2 `immEqInt` 0)
             do writeRegister rd $ FromImm r1
-            do ifExprM ((FromImm r1 `Eq` fromUInt (fromIntegral (minBound :: Int32))) `And` (FromImm r2 `Eq` fromUInt 0xFFFFFFFF))
+            do ifExprM ((r1 `immEqInt` fromIntegral (minBound :: Int32)) `And` (r2 `immEqInt` 0xFFFFFFFF))
                 do writeRegister rd $ fromUInt 0
                 do writeRegister rd $ r1 `srem` r2
     REMU -> do
         (r1, r2, rd) <- decodeAndReadRType
-        ifExprM (FromImm r2 `Eq` fromUInt 0)
+        ifExprM (r2 `immEqInt` 0)
             do writeRegister rd $ FromImm r1
             do writeRegister rd $ r1 `urem` r2