ARMv6 (arm11) is no longer supported by seL4

Signed-off-by: Axel Heider <[email protected]>
seL4 · Jun 8, 2022 · b212b1d · b212b1d
1 parent 57a6d94
commit b212b1d
Show file tree

Hide file tree

Showing 19 changed files with 35 additions and 39 deletions.
diff --git a/capDL-tool/CapDL/DumpParser.hs b/capDL-tool/CapDL/DumpParser.hs
@@ -121,9 +121,9 @@ sizeOf _ (Obj ARMIODevice_T _ _) = 1
 sizeOf IA32 (Obj TCB_T _ _) = 2^10
 sizeOf IA32 (Obj PD_T _ _) = 4 * 2^10
 sizeOf IA32 (Obj PT_T _ _) = 4 * 2^10
-sizeOf ARM11 (Obj TCB_T _ _) = 512
-sizeOf ARM11 (Obj PD_T _ _) = 16 * 2^10
-sizeOf ARM11 (Obj PT_T _ _) = 2^10
+sizeOf AARCH32 (Obj TCB_T _ _) = 512
+sizeOf AARCH32 (Obj PD_T _ _) = 16 * 2^10
+sizeOf AARCH32 (Obj PT_T _ _) = 2^10
 sizeOf _ _ = 0
 
 consecutive :: Arch -> (Name, KO) -> Maybe (Name, KO) -> Word -> Bool

diff --git a/capDL-tool/CapDL/Model.hs b/capDL-tool/CapDL/Model.hs
@@ -18,7 +18,7 @@ import Data.Word
 import Control.Lens
 
 -- Supported architectures:
-data Arch = IA32 | ARM11 | X86_64 | AARCH64 | RISCV deriving (Eq, Show)
+data Arch = IA32 | X86_64 | AARCH32 | AARCH64 | RISCV deriving (Eq, Show)
 
 -- Access rights of capabilities. Not all capability types support all rights.
 data Rights = Read
@@ -84,7 +84,7 @@ data Cap
         | VCPUCap {
             capObj :: ObjID }
 
-        -- arch specific caps, ARM11, IA32, X86_64 and AARCH64 merged
+        -- arch specific caps, AARCH32, AARCH64, IA32, X86_64, RISCV merged
         | FrameCap {
             capObj :: ObjID,
             capRights :: CapRights,
@@ -182,7 +182,7 @@ data KernelObject a
     | RTReply
     | VCPU
 
--- arch specific objects, ARM11, IA32, X86_64, AARCH64 and RISCV mixed
+-- arch specific objects, IA32, X86_64, AARCH32, AARCH64, RISCV mixed
     | ASIDPool { slots :: CapMap a,
                  capAsidHigh :: Maybe Word }
     | PT { slots :: CapMap a }

diff --git a/capDL-tool/CapDL/ParserUtils.hs b/capDL-tool/CapDL/ParserUtils.hs
@@ -107,7 +107,7 @@ parse_either a b =
 parse_arch :: MapParser Arch
 parse_arch = do
     reserved "arch"
-    keyw "ia32" IA32 <|> keyw "arm11" ARM11 <|> keyw "x86_64" X86_64 <|> keyw "aarch64" AARCH64 <|> keyw "riscv" RISCV
+    keyw "ia32" IA32 <|> keyw "x86_64" X86_64 <|> keyw "aarch32" AARCH32 <|> keyw "aarch64" AARCH64 <|> keyw "riscv" RISCV
 
 object_type :: MapParser KOType
 object_type =

diff --git a/capDL-tool/CapDL/PrintC.hs b/capDL-tool/CapDL/PrintC.hs
@@ -56,8 +56,8 @@ memberArch arch =
     where
         a = case arch of
             IA32 -> "IA32"
-            ARM11 -> "ARM"
             X86_64 -> "X86_64"
+            AARCH32 -> "AARCH32"
             AARCH64 -> "AARCH64"
             RISCV -> "RISCV"
 

diff --git a/capDL-tool/CapDL/PrintIsabelle.hs b/capDL-tool/CapDL/PrintIsabelle.hs
@@ -507,7 +507,7 @@ printFooter :: Doc
 printFooter = text "end"
 
 printIsabelle :: String -> ObjectSizeMap -> Model Word -> Doc
-printIsabelle name objSizeMap (Model (arch@ARM11) ms irqNode cdt untypedCovers) =
+printIsabelle name objSizeMap (Model (arch@AARCH32) ms irqNode cdt untypedCovers) =
     printHeader name $+$ text "" $+$
 
     printObjIDs objSizeMap objAddrs ms irqNode $+$
@@ -535,4 +535,4 @@ printIsabelle name objSizeMap (Model (arch@ARM11) ms irqNode cdt untypedCovers)
                           Map.toList ms
 
 printIsabelle _ _ _ =
-    error "Currently only the ARM11 architecture is supported when parsing to Isabelle"
+    error "Currently only the AARCH32 architecture is supported when parsing to Isabelle"
diff --git a/capDL-tool/CapDL/PrintUtils.hs b/capDL-tool/CapDL/PrintUtils.hs
@@ -374,9 +374,9 @@ same (name1, obj1) (name2, obj2) =
     then sameName name1 name2 && slots obj1 == slots obj2
     else sameName name1 name2
 
-prettyArch ARM11 = text "arm11"
 prettyArch IA32  = text "ia32"
 prettyArch X86_64 = text "x86_64"
+prettyArch AARCH32 = text "aarch32"
 prettyArch AARCH64 = text "aarch64"
 prettyArch RISCV = text "riscv"
 

diff --git a/capDL-tool/CapDL/State.hs b/capDL-tool/CapDL/State.hs
@@ -406,8 +406,8 @@ validCapArch X86_64 (IOPortsCap {}) = True
 validCapArch X86_64 IOSpaceMasterCap = True
 validCapArch X86_64 (IOSpaceCap {}) = True
 validCapArch X86_64 (IOPTCap {}) = True
-validCapArch ARM11 (ARMIOSpaceCap {}) = True
-validCapArch ARM11 (ARMIRQHandlerCap {}) = True
+validCapArch AARCH32 (ARMIOSpaceCap {}) = True
+validCapArch AARCH32 (ARMIRQHandlerCap {}) = True
 validCapArch AARCH64 (ARMIRQHandlerCap {}) = True
 validCapArch AARCH64 (PUDCap {}) = True
 validCapArch AARCH64 (PGDCap {}) = True
@@ -450,8 +450,8 @@ validObjArch _ (SC {}) = True
 validObjArch _ (RTReply {}) = True
 validObjArch RISCV (VCPU {}) = False
 validObjArch _ (VCPU {}) = True
-validObjArch ARM11 (ARMIODevice {}) = True
-validObjArch ARM11 (ARMIrq {}) = True
+validObjArch AARCH32 (ARMIODevice {}) = True
+validObjArch AARCH32 (ARMIrq {}) = True
 validObjArch IA32 (IOPorts {}) = True
 validObjArch IA32 (IODevice {}) = True
 validObjArch IA32 (IOPT {}) = True
@@ -484,7 +484,7 @@ validTCBSlotCap arch slot cap
     | slot == tcbVTableSlot
         = case arch of
                 IA32 -> is _PDCap cap
-                ARM11 -> is _PDCap cap
+                AARCH32 -> is _PDCap cap
                 X86_64 -> is _PML4Cap cap
                 AARCH64 -> is _PGDCap cap || is _PUDCap cap
                 RISCV -> is _PTCap cap

diff --git a/capDL-tool/camkes-adder-arm.cdl b/capDL-tool/camkes-adder-arm.cdl
@@ -6,7 +6,7 @@
  * SPDX-License-Identifier: BSD-2-Clause
  */
 
-arch arm11
+arch aarch32
 
 objects {
 adder_adder_0_control_tcb = tcb (addr: 0x14b000,ip: 0x17a24,sp: 0x149000,prio: 254,max_prio: 254,affinity: 0,init: [1],fault_ep: 0x00000002)

diff --git a/capDL-tool/camkes-adder-arm.right b/capDL-tool/camkes-adder-arm.right
@@ -1,5 +1,4 @@
-arch arm11
-
+arch aarch32
 objects {
 
   adder_adder_0_control_tcb = tcb (addr: 1355776, ip: 96804, sp: 1347584, prio: 254, max_prio: 254, affinity: 0, fault_ep: 2, dom: 0, init: [1])

diff --git a/capDL-tool/camkes-adder-arm.thy.right b/capDL-tool/camkes-adder-arm.thy.right
@@ -1205,7 +1205,7 @@ definition cdt :: "cdl_cdt" where
 "cdt \<equiv> Map.empty"
 
 definition state :: "cdl_state" where
-"state \<equiv> \<lparr> cdl_arch = ARM11, cdl_objects = objects,
+"state \<equiv> \<lparr> cdl_arch = aarch32, cdl_objects = objects,
                          cdl_cdt = cdt, cdl_current_thread = undefined, cdl_irq_node = irqs,
                          cdl_asid_table = asid_table,
                          cdl_current_domain = undefined \<rparr>"

diff --git a/capDL-tool/doc/capDL.md b/capDL-tool/doc/capDL.md
@@ -152,7 +152,7 @@ in section [Modules](#modules).
 
 ### Modules
 
-      arch ::= 'arch' ('ia32' | 'arm11')
+      arch ::= 'arch' ('ia32' | 'x86_64' | 'aarch32' | 'aarch64' | 'riscv' )
 
       module ::= arch (obj_decls | cap_decls | irq_decls | cdt_decls)+
 
@@ -205,7 +205,8 @@ architecture the system is intended for.
                       objects :: Map ObjID Object
                   }
 
-    data Arch = IA32 | ARM11
+    data Arch = IA32 | X86_64 | AARCH32 | AARCH64 | RISCV
+
 
 Objects are described by the following data type. We are mainly
 interested in what capabilities an object contains. We also store
@@ -380,7 +381,8 @@ A list of ranges `name[r1,r2,..r3]` refers to the union of the ranges
 
 ### Module
 
-      arch ::= 'arch' ('ia32' | 'arm11')
+      arch ::= 'arch' ('ia32' | 'x86_64' | 'aarch32' | 'aarch64' | 'riscv')
+
       module ::= arch (obj_decls | cap_decls)+
 
 A module maps to a full `Model` in the data model. Its `Arch` component

diff --git a/capDL-tool/example-arm.cdl b/capDL-tool/example-arm.cdl
@@ -4,7 +4,7 @@
  * SPDX-License-Identifier: BSD-2-Clause
  */
 
-arch arm11
+arch aarch32
 
 objects {
 

diff --git a/capDL-tool/example-arm.right b/capDL-tool/example-arm.right
@@ -1,4 +1,4 @@
-arch arm11
+arch aarch32
 
 objects {
 

diff --git a/capDL-tool/hello-dump.cdl b/capDL-tool/hello-dump.cdl
@@ -6,7 +6,7 @@
  * SPDX-License-Identifier: BSD-2-Clause
  */
 
-arch arm11
+arch aarch32
 
 objects {
 

diff --git a/capDL-tool/hello-dump.right b/capDL-tool/hello-dump.right
@@ -1,4 +1,4 @@
-arch arm11
+arch aarch32
 
 objects {
 

diff --git a/capDL-tool/tools/capdl.vim b/capDL-tool/tools/capdl.vim
@@ -16,7 +16,7 @@
 " Note that this supports CPP commands in your CapDL as well.
 "
 
-syn keyword CapDLKeyword arch caps objects arm11 ia32
+syn keyword CapDLKeyword arch caps objects ia32 x86_64 aarch32 aarch64 riscv
 syn match CapDLIRQMap "\<irq maps\>"
 syn match CapDLIRQ "\<irq\>\( maps\)\@!"
 syn keyword CapDLObject notification asid_pool cnode ep frame io_device io_ports io_pt pd pt tcb ut

diff --git a/python-capdl-tool/capdl/PageCollection.py b/python-capdl-tool/capdl/PageCollection.py
@@ -28,7 +28,7 @@ def consume(iterator):
 
 
 class PageCollection(object):
-    def __init__(self, name='', arch='arm11', infer_asid=True, vspace_root=None):
+    def __init__(self, name='', arch='aarch32', infer_asid=True, vspace_root=None):
         self.name = name
         self.arch = arch
         self._pages = {}
@@ -145,7 +145,7 @@ def get_spec(self, existing_frames={}):
         return spec
 
 
-def create_address_space(regions, name='', arch='arm11'):
+def create_address_space(regions, name='', arch='aarch32'):
     assert isinstance(regions, list)
 
     pages = PageCollection(name, arch)

diff --git a/python-capdl-tool/capdl/Spec.py b/python-capdl-tool/capdl/Spec.py
@@ -16,7 +16,7 @@ class Spec(object):
     A CapDL specification.
     """
 
-    def __init__(self, arch='arm11'):
+    def __init__(self, arch='aarch32'):
         self.arch = arch
         self.objs = set()
 
@@ -48,7 +48,7 @@ def __repr__(self):
                'caps {\n%(caps)s\n}\n\n' \
                'irq maps {\n%(irqs)s\n}' % {
 
-                   # Architecture; arm11 or ia32
+                   # Architecture; aarch32 or ia32
                    'arch': self.arch.capdl_name(),
 
                    # Kernel objects

diff --git a/python-capdl-tool/capdl/util.py b/python-capdl-tool/capdl/util.py
@@ -151,7 +151,7 @@ def __init__(self, hyp=False):
         self.hyp = hyp
 
     def capdl_name(self):
-        return "arm11"
+        return "aarch32"
 
     def levels(self):
         return [
@@ -239,14 +239,9 @@ def ipc_buffer_size(self):
         return 512
 
 
-# Support for ARMv6 has been removed from seL4 in early 2022. However, support
-# for "arm11" is kept here, because this name is used in the CapDL specification
-# for AARCH32 configurations. Updating this is a low priority task, because it
-# is a lot of work with not much gain (except cleaning up legacy), Also, keeping
-# the name there isn't causing any issues.
 CAPDL_SUPPORTED_ARCHITECTURES = {
     # <name>:  [arch_obj_ctor, <alias_list>]
-    'aarch32': [lambda: ARM32Arch(),         ['arm', 'arm11']],
+    'aarch32': [lambda: ARM32Arch(),         ['arm']],
     'arm_hyp': [lambda: ARM32Arch(hyp=True), []],
     'aarch64': [lambda: AARCH64Arch(),       []],
     'ia32':    [lambda: IA32Arch(),          ['x86']],