{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QualifiedDo #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}

module LibRISCV.Semantics.RV_M.Default where

import Control.Monad.Freer
import Data.Function (on)
import LibRISCV.Effects.Decoding.Language (Decoding)
import LibRISCV.Effects.Expressions.Expr
import LibRISCV.Effects.Expressions.Language (ExprEval, ifExprM)
import LibRISCV.Effects.Logging.Language (LogInstructionFetch)
import LibRISCV.Effects.Operations.Language (Operations (..))
import LibRISCV.Internal.Decoder.Opcodes (RV_M (..))
import LibRISCV.Semantics.Utils

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 Int
width =
    let
        fromUInt :: Integer -> Expr v
        fromUInt :: Integer -> Expr v
fromUInt = Int -> Integer -> Expr v
forall a. Int -> Integer -> Expr a
FromInt Int
width

        immEqInt :: v -> Integer -> Expr v
        immEqInt :: v -> Integer -> Expr v
immEqInt v
imm Integer
int = v -> Expr v
forall a. a -> Expr a
FromImm v
imm Expr v -> Expr v -> Expr v
forall a. Expr a -> Expr a -> Expr a
`Eq` Integer -> Expr v
fromUInt Integer
int

        mask1 :: Expr v
        mask1 :: Expr v
mask1 = Int -> Integer -> Expr v
forall a. Int -> Integer -> Expr a
FromInt Int
width (Integer
2 Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Int
width Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)

        extract32 :: Int -> Expr v -> Expr v
        extract32 :: Int -> Expr v -> Expr v
extract32 = (Int -> Int -> Expr v -> Expr v) -> Int -> Int -> Expr v -> Expr v
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> Int -> Expr v -> Expr v
forall a. Int -> Int -> Expr a -> Expr a
Extract Int
32

        mostNegative :: Integer
        mostNegative :: Integer
mostNegative = Integer
2 Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ (Int
width Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)

        -- Signed division overflow occurs when the most-negative integer is divided by -1.
        sdivOverflow :: v -> v -> Expr v
        sdivOverflow :: v -> v -> Expr v
sdivOverflow v
n v
divisor = (v
n v -> Integer -> Expr v
`immEqInt` Integer
mostNegative) Expr v -> Expr v -> Expr v
forall a. Expr a -> Expr a -> Expr a
`And` (v
divisor v -> Integer -> Expr v
`immEqInt` (-Integer
1))
     in
        \case
            RV_M
MUL -> do
                (v
r1, v
r2, v
rd) <- Eff r (v, v, v)
forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadRType
                let
                    multRes :: Expr v
multRes = (Expr v -> Expr v -> Expr v
forall a. Expr a -> Expr a -> Expr a
Mul (Expr v -> Expr v -> Expr v) -> (v -> Expr v) -> v -> v -> Expr v
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Int -> v -> Expr v
forall a. Int -> a -> Expr a
sextImm Int
32) v
r1 v
r2
                    res :: Expr v
res = Int -> Expr v -> Expr v
extract32 Int
0 Expr v
multRes
                v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
rd Expr v
res
            RV_M
MULH -> do
                (v
r1, v
r2, v
rd) <- Eff r (v, v, v)
forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadRType
                let
                    multRes :: Expr v
multRes = (Expr v -> Expr v -> Expr v
forall a. Expr a -> Expr a -> Expr a
Mul (Expr v -> Expr v -> Expr v) -> (v -> Expr v) -> v -> v -> Expr v
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Int -> v -> Expr v
forall a. Int -> a -> Expr a
sextImm Int
32) v
r1 v
r2
                    res :: Expr v
res = Int -> Expr v -> Expr v
extract32 Int
32 Expr v
multRes
                v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
rd Expr v
res
            RV_M
MULHU -> do
                (v
r1, v
r2, v
rd) <- Eff r (v, v, v)
forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadRType
                let
                    multRes :: Expr v
multRes = (Expr v -> Expr v -> Expr v
forall a. Expr a -> Expr a -> Expr a
Mul (Expr v -> Expr v -> Expr v) -> (v -> Expr v) -> v -> v -> Expr v
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Int -> v -> Expr v
forall a. Int -> a -> Expr a
zextImm Int
32) v
r1 v
r2
                    res :: Expr v
res = Int -> Expr v -> Expr v
extract32 Int
32 Expr v
multRes
                v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
rd Expr v
res
            RV_M
MULHSU -> do
                (v
r1, v
r2, v
rd) <- Eff r (v, v, v)
forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadRType
                let
                    multRes :: Expr v
multRes = Int -> v -> Expr v
forall a. Int -> a -> Expr a
sextImm Int
32 v
r1 Expr v -> Expr v -> Expr v
forall a. Expr a -> Expr a -> Expr a
`Mul` Int -> v -> Expr v
forall a. Int -> a -> Expr a
zextImm Int
32 v
r2
                    res :: Expr v
res = Int -> Expr v -> Expr v
extract32 Int
32 Expr v
multRes
                v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
rd Expr v
res
            RV_M
DIV -> do
                (v
r1, v
r2, v
rd) <- Eff r (v, v, v)
forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadRType
                Expr v -> Eff r () -> Eff r () -> Eff r ()
forall v (r :: [* -> *]) v'.
Member (ExprEval v) r =>
Expr v -> Eff r v' -> Eff r v' -> Eff r v'
ifExprM
                    (v
r2 v -> Integer -> Expr v
`immEqInt` Integer
0)
                    do v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
rd Expr v
mask1
                    do
                        Expr v -> Eff r () -> Eff r () -> Eff r ()
forall v (r :: [* -> *]) v'.
Member (ExprEval v) r =>
Expr v -> Eff r v' -> Eff r v' -> Eff r v'
ifExprM
                            (v -> v -> Expr v
sdivOverflow v
r1 v
r2)
                            do v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
rd (Expr v -> Eff r ()) -> Expr v -> Eff r ()
forall a b. (a -> b) -> a -> b
$ v -> Expr v
forall a. a -> Expr a
FromImm v
r1
                            do v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
rd (Expr v -> Eff r ()) -> Expr v -> Eff r ()
forall a b. (a -> b) -> a -> b
$ v
r1 v -> v -> Expr v
forall {a}. a -> a -> Expr a
`sdiv` v
r2
            RV_M
DIVU -> do
                (v
r1, v
r2, v
rd) <- Eff r (v, v, v)
forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadRType
                Expr v -> Eff r () -> Eff r () -> Eff r ()
forall v (r :: [* -> *]) v'.
Member (ExprEval v) r =>
Expr v -> Eff r v' -> Eff r v' -> Eff r v'
ifExprM
                    (v
r2 v -> Integer -> Expr v
`immEqInt` Integer
0)
                    do v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
rd Expr v
mask1
                    do v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
rd (Expr v -> Eff r ()) -> Expr v -> Eff r ()
forall a b. (a -> b) -> a -> b
$ v
r1 v -> v -> Expr v
forall {a}. a -> a -> Expr a
`udiv` v
r2
            RV_M
REM -> do
                (v
r1, v
r2, v
rd) <- Eff r (v, v, v)
forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadRType
                Expr v -> Eff r () -> Eff r () -> Eff r ()
forall v (r :: [* -> *]) v'.
Member (ExprEval v) r =>
Expr v -> Eff r v' -> Eff r v' -> Eff r v'
ifExprM
                    (v
r2 v -> Integer -> Expr v
`immEqInt` Integer
0)
                    do v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
rd (Expr v -> Eff r ()) -> Expr v -> Eff r ()
forall a b. (a -> b) -> a -> b
$ v -> Expr v
forall a. a -> Expr a
FromImm v
r1
                    do
                        Expr v -> Eff r () -> Eff r () -> Eff r ()
forall v (r :: [* -> *]) v'.
Member (ExprEval v) r =>
Expr v -> Eff r v' -> Eff r v' -> Eff r v'
ifExprM
                            (v -> v -> Expr v
sdivOverflow v
r1 v
r2)
                            do v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
rd (Expr v -> Eff r ()) -> Expr v -> Eff r ()
forall a b. (a -> b) -> a -> b
$ Integer -> Expr v
fromUInt Integer
0
                            do v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
rd (Expr v -> Eff r ()) -> Expr v -> Eff r ()
forall a b. (a -> b) -> a -> b
$ v
r1 v -> v -> Expr v
forall {a}. a -> a -> Expr a
`srem` v
r2
            RV_M
REMU -> do
                (v
r1, v
r2, v
rd) <- Eff r (v, v, v)
forall v (r :: [* -> *]).
(Member (Decoding v) r, Member (Operations v) r) =>
Eff r (v, v, v)
decodeAndReadRType
                Expr v -> Eff r () -> Eff r () -> Eff r ()
forall v (r :: [* -> *]) v'.
Member (ExprEval v) r =>
Expr v -> Eff r v' -> Eff r v' -> Eff r v'
ifExprM
                    (v
r2 v -> Integer -> Expr v
`immEqInt` Integer
0)
                    do v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
rd (Expr v -> Eff r ()) -> Expr v -> Eff r ()
forall a b. (a -> b) -> a -> b
$ v -> Expr v
forall a. a -> Expr a
FromImm v
r1
                    do v -> Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
v -> Expr v -> Eff r ()
writeRegister v
rd (Expr v -> Eff r ()) -> Expr v -> Eff r ()
forall a b. (a -> b) -> a -> b
$ v
r1 v -> v -> Expr v
forall {a}. a -> a -> Expr a
`urem` v
r2