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

aarch64 aspec+haskell: config dependent vm_level 

Using value_type, we can capture both config options.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2022-03-18 17:00:18 +11:00 committed by Gerwin Klein
parent 47c0ec4bdc
commit 61e5a84670
2 changed files with 3 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
spec/abstract/AARCH64/Arch_Structs_A.thy
View File

@ -261,8 +261,7 @@ text \<open>
top-level page tables, and level 1 page tables. The bottom-level page tables (level 0)
contains only InvalidPTEs or PagePTEs.
\<close>
(* FIXME AARCH64: this depends on config_ARM_PA_SIZE_BITS_40 *)
type_synonym vm_level = 5
value_type vm_level = "if config_ARM_PA_SIZE_BITS_40 then 4 else (5::int)"
definition asid_pool_level :: vm_level where
"asid_pool_level = maxBound"

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

@ -12,7 +12,7 @@ module SEL4.Model.StateData.AARCH64 where
import Prelude hiding (Word)
import SEL4.Machine
import SEL4.Machine.Hardware.AARCH64 (PTE(..))
import SEL4.Machine.Hardware.AARCH64 (PTE(..), config_ARM_PA_SIZE_BITS_40)
import SEL4.Object.Structures.AARCH64
import Data.Array
@ -47,7 +47,7 @@ data KernelState = ARMKernelState {
-- counting from 0 at bottom, i.e. number of levels = maxPTLevel + 1;
-- maxPTLevel = level of top-level root table
maxPTLevel :: Int
maxPTLevel = 3
maxPTLevel = if config_ARM_PA_SIZE_BITS_40 then 2 else 3
newKernelState :: PAddr -> (KernelState, [PAddr])
newKernelState _ = error "No initial state defined for AARCH64"