Machine.hs

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, UndecidableInstances, ScopedTypeVariables, Rank2Types #-}
module Spec.Machine where
import Spec.CSRField
import qualified Spec.CSR as CSR
import Spec.Decode
import Utility.Utility
import Data.Int
import Data.Word
import Data.Bits
import Control.Monad
import Control.Monad.Trans
import Control.Monad.Trans.Maybe
import Prelude
import Debug.Trace

-- Note that this is ordered: User < Supervisor < Machine
data PrivMode = User | Supervisor | Machine deriving (Eq, Ord, Show)
data AccessType = Instruction | Load | Store deriving (Eq, Show)

data SourceType = VirtualMemory | Fetch | Execute deriving (Eq,Show)

decodePrivMode 0 = User
decodePrivMode 1 = Supervisor
decodePrivMode 3 = Machine
decodePrivMode _ = error "Invalid privilege mode"

encodePrivMode User = 0
encodePrivMode Supervisor = 1
encodePrivMode Machine = 3

data Platform = Platform {
  -- The existential on p and t is per-function, rather than a type variable of
  -- Platform, both for semantic clarity and because Having it as a type
  -- variable of Platform would break lifting.
  dirtyHardware :: forall p t. (RiscvMachine p t) => p Bool,
  readPlatformCSR :: forall p t. (RiscvMachine p t) => CSR.CSR -> p MachineInt,
  writePlatformCSRField :: forall p t. (RiscvMachine p t) => CSRField -> MachineInt -> p MachineInt
  -- writeMISA :: forall p t. (RiscvMachine p t) => MachineInt -> p MachineInt
}

class (Monad p, MachineWidth t) => RiscvMachine p t | p -> t where
  getRegister :: Register -> p t
  setRegister :: Register -> t -> p ()
  -- TODO: Another typeclass parameter for floating-point width?
  getFPRegister :: FPRegister -> p Int32
  setFPRegister :: FPRegister -> Int32 -> p ()
  loadByte :: SourceType -> t -> p Int8
  loadHalf :: SourceType -> t -> p Int16
  loadWord :: SourceType -> t -> p Int32
  loadDouble :: SourceType -> t -> p Int64
  storeByte :: SourceType -> t -> Int8 -> p ()
  storeHalf :: SourceType -> t -> Int16 -> p ()
  storeWord :: SourceType -> t -> Int32 -> p ()
  storeDouble :: SourceType -> t -> Int64 -> p ()
  makeReservation :: t -> p ()
  checkReservation :: t -> p Bool
  clearReservation :: t -> p ()
  getCSRField :: CSRField -> p MachineInt
  unsafeSetCSRField :: (Integral s) => CSRField -> s -> p ()
  getPC :: p t
  setPC :: t -> p ()
  getPrivMode :: p PrivMode
  setPrivMode :: PrivMode -> p ()
  commit :: p ()
  endCycle :: forall z. p z
  flushTLB :: p ()
  fence :: MachineInt -> MachineInt -> p ()
  getPlatform :: p Platform


cacheAccess :: forall p t. (RiscvMachine p t) => AccessType -> MachineInt -> p (MachineInt, MachineInt,  Int) -> p MachineInt
cacheAccess accessType addr getPA = do --remove TLB tracking, the only people that model stalled TLB entries seem to be doing it in an axiomatic memory model fashion
      (pa, _pte, _level) <- getPA
      return pa

getXLEN :: forall p t s. (RiscvMachine p t, Integral s) => p s
getXLEN = do
            mxl <- getCSRField MXL
            case mxl of
                1 -> return 32
                2 -> return 64

hardwareDirtyBit :: (RiscvMachine p t) => p Bool
hardwareDirtyBit = do
  p <- getPlatform
  r <- dirtyHardware p
  return r

getCSR_InstRet :: (RiscvMachine p t) => p MachineInt
getCSR_InstRet = do
  p <- getPlatform
  r <- readPlatformCSR p CSR.InstRet
  return r

getCSR_Time :: (RiscvMachine p t) => p MachineInt
getCSR_Time = do
  p <- getPlatform
  readPlatformCSR p CSR.Time

getCSR_Cycle :: (RiscvMachine p t) => p MachineInt
getCSR_Cycle = do
  p <- getPlatform
  readPlatformCSR p CSR.Cycle

setCSRField :: (RiscvMachine p t, Integral s) => CSRField -> s -> p ()
setCSRField field value = do
  let ty = fieldType field
  if (ty == WLRL || ty == WARL) then do
    p <- getPlatform
    v <- (writePlatformCSRField p) field (fromIntegral value)
    unsafeSetCSRField field v
  else unsafeSetCSRField field value

instance (RiscvMachine p t) => RiscvMachine (MaybeT p) t where
  getRegister r = lift (getRegister r)
  setRegister r v = lift (setRegister r v)
  getFPRegister r = lift (getFPRegister r)
  setFPRegister r v = lift (setFPRegister r v)
  loadByte s a = lift (loadByte s a)
  loadHalf s a = lift (loadHalf s a)
  loadWord s a = lift (loadWord s a)
  loadDouble s a = lift (loadDouble s a)
  storeByte s a v = lift (storeByte s a v)
  storeHalf s a v = lift (storeHalf s a v)
  storeWord s a v = lift (storeWord s a v)
  storeDouble s a v = lift (storeDouble s a v)
  makeReservation a = lift (makeReservation a)
  checkReservation a = lift (checkReservation a)
  clearReservation a = lift (clearReservation a)
  getCSRField f = lift (getCSRField f)
  unsafeSetCSRField f v = lift (unsafeSetCSRField f v)
  getPC = lift getPC
  setPC v = lift (setPC v)
  getPrivMode = lift getPrivMode
  setPrivMode m = lift (setPrivMode m)
  commit = lift commit
  endCycle = MaybeT (return Nothing) -- b is of type (MaybeT p) a
  flushTLB = lift flushTLB
  fence a b = lift (fence a b)
  getPlatform = lift getPlatform

raiseExceptionWithInfo :: forall a p t. (RiscvMachine p t) => MachineInt -> MachineInt -> MachineInt -> p a
raiseExceptionWithInfo isInterrupt exceptionCode info =  do
  pc <- getPC
  mode <- getPrivMode
  medeleg <- getCSRField MEDeleg
  mideleg <- getCSRField MIDeleg
  let delegatedException = isInterrupt == 0 && (testBit medeleg ((fromIntegral:: MachineInt -> Int) exceptionCode))
  let delegatedInterrupt = isInterrupt /= 0 && (testBit mideleg ((fromIntegral ::MachineInt -> Int) exceptionCode))
  if (mode < Machine) && (delegatedException || delegatedInterrupt)
    then do
    -- Delegate to S-mode.
    addr <- getCSRField STVecBase
    setPrivMode Supervisor
    setCSRField STVal info
    setCSRField SPP (encodePrivMode mode)
    setCSRField SEPC pc
    setCSRField SCauseInterrupt isInterrupt
    setCSRField SCauseCode exceptionCode
    sie <- getCSRField SIE
    setCSRField SPIE sie
    setCSRField SIE 0
    setPC ((fromIntegral:: MachineInt -> t) addr * 4)
    else do
    -- Handle in M-mode.
    addr <- getCSRField MTVecBase
    setPrivMode Machine
    setCSRField MTVal info
    setCSRField MPP (encodePrivMode mode)
    mie <- getCSRField MIE
    setCSRField MPIE mie
    setCSRField MIE 0
    setCSRField MEPC pc
    setCSRField MCauseInterrupt isInterrupt
    setCSRField MCauseCode exceptionCode
    setPC ((fromIntegral:: MachineInt -> t) addr * 4)
  endCycle

raiseException :: forall a p t. (RiscvMachine p t) => MachineInt -> MachineInt -> p a
raiseException isInterrupt exceptionCode = raiseExceptionWithInfo isInterrupt exceptionCode 0