adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

aarch64 haskell: adjust syntax for translator 

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
This commit is contained in:
Rafal Kolanski 2022-02-17 14:28:56 +11:00 committed by Gerwin Klein
parent 512fa574db
commit 715212dd41
4 changed files with 23 additions and 23 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
spec/haskell/src/SEL4/Machine/RegisterSet/AARCH64.hs
View File

@ -18,12 +18,12 @@ import Data.Helpers
import Control.Monad.State(State, gets, modify)
-- note on aliases: NextIP = ELR_EL1, X30 = LR, TPIDR_EL0 = TLS_BASE
data Register
= X0 | X1 | X2 | X3 | X4 | X5 | X6 | X7 | X8 | X9
| X10 | X11 | X12 | X13 | X14 | X15 | X16 | X17 | X18 | X19
| X20 | X21 | X22 | X23 | X24 | X25 | X26 | X27 | X28 | X29 | X30 {-LR-}
| SP_EL0 | NextIP {-ELR_EL1-} | SPSR_EL1 | FaultIP | TPIDR_EL0 {-TLS_BASE-}
| TPIDRRO_EL0
| X20 | X21 | X22 | X23 | X24 | X25 | X26 | X27 | X28 | X29 | X30
| SP_EL0 | NextIP | SPSR_EL1 | FaultIP | TPIDR_EL0 | TPIDRRO_EL0
deriving (Eq, Enum, Bounded, Ord, Ix, Show)
type Word = Data.Word.Word64
@ -49,8 +49,8 @@ gpRegisters = [X9 .. X15] ++ [X19 .. X28] ++ [TPIDR_EL0, TPIDRRO_EL0]
exceptionMessage :: [Register] -- see fault_messages[] in C
exceptionMessage = [FaultIP, SP_EL0, SPSR_EL1]
syscallMessage :: [Register] -- see fault_messages[] in C
syscallMessage = [X0 .. X7] ++ [FaultIP, SP_EL0, NextIP {-ELR_EL1-}, SPSR_EL1]
syscallMessage :: [Register] -- see fault_messages[] in C; note NextIP = ELR_EL1
syscallMessage = [X0 .. X7] ++ [FaultIP, SP_EL0, NextIP, SPSR_EL1]
tlsBaseRegister :: Register
tlsBaseRegister = TPIDR_EL0

2
spec/haskell/src/SEL4/Model/StateData/AARCH64.hs
View File

@ -42,7 +42,7 @@ data KernelState = ARMKernelState {
armKSGlobalUserVSpace :: PPtr PTE,
armHSCurVCPU :: Maybe (PPtr VCPU, Bool),
armKSGICVCPUNumListRegs :: Int
}
}
-- counting from 0 at bottom, i.e. number of levels = maxPTLevel + 1;
-- maxPTLevel = level of top-level root table

8
spec/haskell/src/SEL4/Object/ObjectType/AARCH64.hs
View File

@ -215,10 +215,10 @@ decodeInvocation label args capIndex slot cap extraCaps =
performInvocation :: ArchInv.Invocation -> KernelP [Word]
performInvocation i =
case i of ArchInv.InvokeVCPU iv -> do
withoutPreemption $ performARMVCPUInvocation iv
-- FIXME AARCH64 SMMU: SID/CB control invocations, SID/CB invocations
_ -> performARMMMUInvocation i
case i of
ArchInv.InvokeVCPU iv -> withoutPreemption $ performARMVCPUInvocation iv
-- FIXME AARCH64 SMMU: SID/CB control invocations, SID/CB invocations
_ -> performARMMMUInvocation i
{- Helper Functions -}

26
spec/haskell/src/SEL4/Object/Structures/AARCH64.hs
View File

@ -52,19 +52,6 @@ minUntypedSizeBits = 4
maxUntypedSizeBits :: Int
maxUntypedSizeBits = 47
{- Kernel Objects -}
data ArchKernelObject
= KOASIDPool ASIDPool
| KOPTE PTE
| KOVCPU VCPU
deriving Show
archObjSize :: ArchKernelObject -> Int
archObjSize (KOASIDPool _) = pageBits
archObjSize (KOPTE _) = pteBits
archObjSize (KOVCPU _) = vcpuBits
{- Threads -}
@ -163,3 +150,16 @@ makeVCPUObject =
, vcpuVTimer = VirtTimer 0
}
{- Kernel Objects -}
data ArchKernelObject
= KOASIDPool ASIDPool
| KOPTE PTE
| KOVCPU VCPU
deriving Show
archObjSize :: ArchKernelObject -> Int
archObjSize (KOASIDPool _) = pageBits
archObjSize (KOPTE _) = pteBits
archObjSize (KOVCPU _) = vcpuBits