{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

-- | Implements the default (concrete) interpreter for the 'Operations' effect.
module LibRISCV.Effects.Operations.Default.Interpreter (
    ArchState (..),
    mkArchState,
    dumpState,
    defaultInstructions,
) where

import Control.Monad.Freer (type (~>))
import Control.Monad.IO.Class (MonadIO (..))
import Data.Array.IO (IOUArray)
import Data.BitVector (BV, bitVec)
import Data.Int (Int32)
import Data.Word (Word16, Word32, Word8)
import LibRISCV (Address)
import qualified LibRISCV.Effects.Operations.Default.Machine.Memory as MEM
import qualified LibRISCV.Effects.Operations.Default.Machine.Register as REG
import LibRISCV.Effects.Operations.Language (
    Operations (..),
    Size (Byte, Half, Word),
 )
import Numeric (showHex)

-- | Representation of the concrete architectural state of the interpreter.
data ArchState = ArchState
    { ArchState -> RegisterFile IOUArray Int32
getReg :: REG.RegisterFile IOUArray Int32
    -- ^ Register file implementation of the architectural state.
    , ArchState -> Memory IOUArray Word8
getMem :: MEM.Memory IOUArray Word8
    -- ^ Memory implementation of the architectural state.
    }

-- | Create a new t'ArchState' based on a memory start address and a memory size.
mkArchState :: Address -> Word32 -> IO ArchState
mkArchState :: Word32 -> Word32 -> IO ArchState
mkArchState Word32
memStart Word32
memSize = do
    RegisterFile IOUArray Int32
reg <- Int32 -> IO (RegisterFile IOUArray Int32)
forall (t :: * -> * -> *) a.
MArray t a IO =>
a -> IO (RegisterFile t a)
REG.mkRegFile Int32
0
    Memory IOUArray Word8
mem <- Word32 -> Word32 -> IO (Memory IOUArray Word8)
forall (t :: * -> * -> *) a.
MArray t a IO =>
Word32 -> Word32 -> IO (Memory t a)
MEM.mkMemory Word32
memStart Word32
memSize
    ArchState -> IO ArchState
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ArchState -> IO ArchState) -> ArchState -> IO ArchState
forall a b. (a -> b) -> a -> b
$ RegisterFile IOUArray Int32 -> Memory IOUArray Word8 -> ArchState
ArchState RegisterFile IOUArray Int32
reg Memory IOUArray Word8
mem

-- | Write a textual representation of the t'ArchState' to standard output.
dumpState :: ArchState -> IO ()
dumpState :: ArchState -> IO ()
dumpState ArchState{getReg :: ArchState -> RegisterFile IOUArray Int32
getReg = RegisterFile IOUArray Int32
r} =
    (Int32 -> ShowS) -> RegisterFile IOUArray Int32 -> IO String
forall (t :: * -> * -> *) a.
MArray t a IO =>
(a -> ShowS) -> RegisterFile t a -> IO String
REG.dumpRegs (Word32 -> ShowS
forall a. Integral a => a -> ShowS
showHex (Word32 -> ShowS) -> (Int32 -> Word32) -> Int32 -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral @Int32 @Word32) RegisterFile IOUArray Int32
r IO String -> (String -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= String -> IO ()
putStr

-- | Implements concrete interpretation of the 'Operations' effect based on a 'BV' value representation.
defaultInstructions :: (MonadIO m) => ArchState -> Operations BV ~> m
defaultInstructions :: forall (m :: * -> *). MonadIO m => ArchState -> Operations BV ~> m
defaultInstructions (ArchState RegisterFile IOUArray Int32
regFile Memory IOUArray Word8
mem) =
    IO x -> m x
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO x -> m x)
-> (Operations BV x -> IO x) -> Operations BV x -> m x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
        ReadRegister BV
idx -> Int -> Int32 -> BV
forall a. Integral a => Int -> a -> BV
bitVec Int
32 (Int32 -> x) -> IO Int32 -> IO x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RegisterFile IOUArray Int32 -> RegIdx -> IO Int32
forall (t :: * -> * -> *) a.
MArray t a IO =>
RegisterFile t a -> RegIdx -> IO a
REG.readRegister RegisterFile IOUArray Int32
regFile (Int -> RegIdx
forall a. Enum a => Int -> a
toEnum (Int -> RegIdx) -> Int -> RegIdx
forall a b. (a -> b) -> a -> b
$ BV -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral BV
idx)
        WriteRegister BV
idx BV
reg -> RegisterFile IOUArray Int32 -> RegIdx -> Int32 -> IO ()
forall (t :: * -> * -> *) a.
MArray t a IO =>
RegisterFile t a -> RegIdx -> a -> IO ()
REG.writeRegister RegisterFile IOUArray Int32
regFile (Int -> RegIdx
forall a. Enum a => Int -> a
toEnum (Int -> RegIdx) -> Int -> RegIdx
forall a b. (a -> b) -> a -> b
$ BV -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral BV
idx) (BV -> Int32
forall a b. (Integral a, Num b) => a -> b
fromIntegral BV
reg)
        Load Size
size BV
addr -> case Size
size of
            Size
Byte -> Int -> Word8 -> BV
forall a. Integral a => Int -> a -> BV
bitVec Int
8 (Word8 -> x) -> IO Word8 -> IO x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Memory IOUArray Word8 -> Word32 -> IO Word8
forall (t :: * -> * -> *) a.
MArray t a IO =>
Memory t a -> Word32 -> IO a
MEM.loadByte Memory IOUArray Word8
mem (BV -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral BV
addr)
            Size
Half -> Int -> Word16 -> BV
forall a. Integral a => Int -> a -> BV
bitVec Int
16 (Word16 -> x) -> IO Word16 -> IO x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Memory IOUArray Word8 -> Word32 -> IO Word16
forall (t :: * -> * -> *) a b.
(MArray t a IO, HalfStorage b a) =>
Memory t a -> Word32 -> IO b
MEM.loadHalf Memory IOUArray Word8
mem (BV -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral BV
addr) :: IO Word16)
            Size
Word -> Int -> BV -> BV
forall a. Integral a => Int -> a -> BV
bitVec Int
32 (BV -> x) -> IO BV -> IO x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> * -> *) a b.
(MArray t a IO, WordStorage b a) =>
Memory t a -> Word32 -> IO b
MEM.loadWord @_ @_ @BV Memory IOUArray Word8
mem (BV -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral BV
addr)
        Store Size
size BV
addr BV
w -> case Size
size of
            Size
Byte -> Memory IOUArray Word8 -> Word32 -> Word8 -> IO ()
forall (t :: * -> * -> *) a.
MArray t a IO =>
Memory t a -> Word32 -> a -> IO ()
MEM.storeByte Memory IOUArray Word8
mem (BV -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral BV
addr) (BV -> Word8
forall a b. (Integral a, Num b) => a -> b
fromIntegral BV
w)
            Size
Half -> Memory IOUArray Word8 -> Word32 -> BV -> IO ()
forall (t :: * -> * -> *) a b.
(MArray t a IO, HalfStorage b a) =>
Memory t a -> Word32 -> b -> IO ()
MEM.storeHalf Memory IOUArray Word8
mem (BV -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral BV
addr) BV
w
            Size
Word -> Memory IOUArray Word8 -> Word32 -> BV -> IO ()
forall (t :: * -> * -> *) a b.
(MArray t a IO, WordStorage b a) =>
Memory t a -> Word32 -> b -> IO ()
MEM.storeWord Memory IOUArray Word8
mem (BV -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral BV
addr) BV
w
        WritePC BV
w -> RegisterFile IOUArray Int32 -> Word32 -> IO ()
forall (t :: * -> * -> *) a. RegisterFile t a -> Word32 -> IO ()
REG.writePC RegisterFile IOUArray Int32
regFile (BV -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral BV
w)
        Operations BV x
ReadPC -> Int -> Word32 -> BV
forall a. Integral a => Int -> a -> BV
bitVec Int
32 (Word32 -> x) -> IO Word32 -> IO x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RegisterFile IOUArray Int32 -> IO Word32
forall (t :: * -> * -> *) a. RegisterFile t a -> IO Word32
REG.readPC RegisterFile IOUArray Int32
regFile
        Exception BV
pc String
msg -> String -> IO x
forall a. HasCallStack => String -> a
error (String -> IO x) -> String -> IO x
forall a b. (a -> b) -> a -> b
$ String
"[0x" String -> ShowS
forall a. [a] -> [a] -> [a]
++ BV -> ShowS
forall a. Integral a => a -> ShowS
showHex BV
pc String
"" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"] " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
msg
        Ecall BV
pc -> String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"ecall at 0x" String -> ShowS
forall a. [a] -> [a] -> [a]
++ BV -> ShowS
forall a. Integral a => a -> ShowS
showHex BV
pc String
""
        Ebreak BV
pc -> String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"ebreak at 0x" String -> ShowS
forall a. [a] -> [a] -> [a]
++ BV -> ShowS
forall a. Integral a => a -> ShowS
showHex BV
pc String
""