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

module LibRISCV.Semantics.Default where

import Control.Monad.Freer
import Data.Data (Proxy (..))
import Data.Parameterized.NatRepr
import GHC.TypeLits
import LibRISCV.Effects.Decoding.Language
import LibRISCV.Effects.Expressions.Expr
import LibRISCV.Effects.Expressions.Language
import LibRISCV.Effects.Logging.Language (LogInstructionFetch, logFetched)
import LibRISCV.Effects.Operations.Language hiding (load, readRegister, store, writePC, writeRegister)
import LibRISCV.Internal.Decoder.Opcodes
import qualified LibRISCV.Semantics.RV32_I.Default as RV32_I
import qualified LibRISCV.Semantics.RV_I.Default as RV_I
import qualified LibRISCV.Semantics.RV_M.Default as RV_M
import LibRISCV.Semantics.Utils

------------------------------------------------------------------------

-- We require type annotations here to workaround a limitation of
-- GHC type inference in conjunction with freer-simple. Alternatively,
-- we could use a proxy type.
--
-- See: https://github.com/lexi-lambda/freer-simple/issues/7

instrSemantics ::
    forall v r.
    ( Member (Operations v) r
    , Member LogInstructionFetch r
    , Member (Decoding v) r
    , Member (ExprEval v) r
    ) =>
    Int ->
    v ->
    Eff r ()
instrSemantics :: forall v (r :: [* -> *]).
(Member (Operations v) r, Member LogInstructionFetch r,
 Member (Decoding v) r, Member (ExprEval v) r) =>
Int -> v -> Eff r ()
instrSemantics Int
width v
pc = do
    InstructionType
ty <- forall v b (effs :: [* -> *]).
Member (Decoding v) effs =>
Proxy v -> (InstructionType -> b) -> Eff effs b
withInstrType @v Proxy v
forall {k} (t :: k). Proxy t
Proxy InstructionType -> InstructionType
forall a. a -> a
id
    InstructionType -> Eff r ()
forall (effs :: [* -> *]).
Member LogInstructionFetch effs =>
InstructionType -> Eff effs ()
logFetched InstructionType
ty
    case InstructionType
ty of
        RV_I RV_I
inst -> Int -> v -> RV_I -> Eff r ()
forall v (r :: [* -> *]).
(Member (Operations v) r, Member LogInstructionFetch r,
 Member (Decoding v) r, Member (ExprEval v) r) =>
Int -> v -> RV_I -> Eff r ()
RV_I.instrSemantics Int
width v
pc RV_I
inst Eff r () -> Eff r () -> Eff r ()
forall a b. Eff r a -> Eff r b -> Eff r b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall v (r :: [* -> *]).
(Member (Operations v) r, Member LogInstructionFetch r,
 Member (Decoding v) r, Member (ExprEval v) r) =>
Int -> Eff r ()
buildInstruction @v Int
width
        RV32_I RV32_I
inst -> forall v (r :: [* -> *]).
(Member (Operations v) r, Member LogInstructionFetch r,
 Member (Decoding v) r, Member (ExprEval v) r) =>
RV32_I -> Eff r ()
RV32_I.instrSemantics @v RV32_I
inst Eff r () -> Eff r () -> Eff r ()
forall a b. Eff r a -> Eff r b -> Eff r b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall v (r :: [* -> *]).
(Member (Operations v) r, Member LogInstructionFetch r,
 Member (Decoding v) r, Member (ExprEval v) r) =>
Int -> Eff r ()
buildInstruction @v Int
width
        RV_M RV_M
inst -> forall v (r :: [* -> *]).
(Member (Operations v) r, Member LogInstructionFetch r,
 Member (Decoding v) r, Member (ExprEval v) r) =>
Int -> RV_M -> Eff r ()
RV_M.instrSemantics @v Int
width RV_M
inst Eff r () -> Eff r () -> Eff r ()
forall a b. Eff r a -> Eff r b -> Eff r b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall v (r :: [* -> *]).
(Member (Operations v) r, Member LogInstructionFetch r,
 Member (Decoding v) r, Member (ExprEval v) r) =>
Int -> Eff r ()
buildInstruction @v Int
width
        InstructionType
InvalidInstruction -> () -> Eff r ()
forall a. a -> Eff r a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

buildInstruction ::
    forall v r.
    ( Member (Operations v) r
    , Member LogInstructionFetch r
    , Member (Decoding v) r
    , Member (ExprEval v) r
    ) =>
    Int ->
    Eff r ()
buildInstruction :: forall v (r :: [* -> *]).
(Member (Operations v) r, Member LogInstructionFetch r,
 Member (Decoding v) r, Member (ExprEval v) r) =>
Int -> Eff r ()
buildInstruction Int
width = do
    -- fetch instruction at current PC
    v
pc <- forall v (effs :: [* -> *]).
Member (Operations v) effs =>
Eff effs v
readPC @v
    v
instrWord <- forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
Size -> Expr v -> Eff r v
load @v Size
Word (Expr v -> Eff r v) -> Expr v -> Eff r v
forall a b. (a -> b) -> a -> b
$ v -> Expr v
forall a. a -> Expr a
FromImm v
pc
    v -> Eff r ()
forall v (effs :: [* -> *]).
Member (Decoding v) effs =>
v -> Eff effs ()
setInstr v
instrWord

    -- Increment PC before execute', allows setting PC to to
    -- different values in execute' for jumps and branches.
    Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
Expr v -> Eff r ()
writePC (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
pc Expr v -> Expr v -> Expr v
forall a. Expr a -> Expr a -> Expr a
`Add` Int -> Integer -> Expr v
forall a. Int -> Integer -> Expr a
FromInt Int
width Integer
4
    Int -> v -> Eff r ()
forall v (r :: [* -> *]).
(Member (Operations v) r, Member LogInstructionFetch r,
 Member (Decoding v) r, Member (ExprEval v) r) =>
Int -> v -> Eff r ()
instrSemantics Int
width v
pc

-- | Obtain the free monad AST for a program loaded into memory, e.g. through
-- the provided ELF 'LibRISCV.Loader' implementation. The function takes one
-- argument  which corresponds to an address in memory at which program
-- execution will start. An instruction word will be loaded from this address,
-- decoded, and executed.
buildAST ::
    forall w v r.
    ( KnownNat w
    , Member (Operations v) r
    , Member LogInstructionFetch r
    , Member (Decoding v) r
    , Member (ExprEval v) r
    ) =>
    v ->
    Eff r ()
buildAST :: forall (w :: Nat) v (r :: [* -> *]).
(KnownNat w, Member (Operations v) r, Member LogInstructionFetch r,
 Member (Decoding v) r, Member (ExprEval v) r) =>
v -> Eff r ()
buildAST v
entry =
    let
        !width :: Int
width = Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (NatRepr w -> Integer
forall (n :: Nat). NatRepr n -> Integer
intValue (NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat :: NatRepr w))
     in
        Expr v -> Eff r ()
forall v (r :: [* -> *]).
(Member (ExprEval v) r, Member (Operations v) r) =>
Expr v -> Eff r ()
writePC (v -> Expr v
forall a. a -> Expr a
FromImm v
entry) Eff r () -> Eff r () -> Eff r ()
forall a b. Eff r a -> Eff r b -> Eff r b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall v (r :: [* -> *]).
(Member (Operations v) r, Member LogInstructionFetch r,
 Member (Decoding v) r, Member (ExprEval v) r) =>
Int -> Eff r ()
buildInstruction @v Int
width