From 61e5a84670a403561290c1831a7fe686b62bd46f Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Fri, 18 Mar 2022 17:00:18 +1100 Subject: [PATCH] aarch64 aspec+haskell: config dependent vm_level Using value_type, we can capture both config options. Signed-off-by: Gerwin Klein --- spec/abstract/AARCH64/Arch_Structs_A.thy | 3 +-- spec/haskell/src/SEL4/Model/StateData/AARCH64.hs | 4 ++-- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/spec/abstract/AARCH64/Arch_Structs_A.thy b/spec/abstract/AARCH64/Arch_Structs_A.thy index 1c6599e56..fbd320af1 100644 --- a/spec/abstract/AARCH64/Arch_Structs_A.thy +++ b/spec/abstract/AARCH64/Arch_Structs_A.thy @@ -261,8 +261,7 @@ text \ top-level page tables, and level 1 page tables. The bottom-level page tables (level 0) contains only InvalidPTEs or PagePTEs. \ -(* 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" diff --git a/spec/haskell/src/SEL4/Model/StateData/AARCH64.hs b/spec/haskell/src/SEL4/Model/StateData/AARCH64.hs index 761ddf690..989162e0a 100644 --- a/spec/haskell/src/SEL4/Model/StateData/AARCH64.hs +++ b/spec/haskell/src/SEL4/Model/StateData/AARCH64.hs @@ -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"