diff --git a/capDL-tool/CapDL/DumpParser.hs b/capDL-tool/CapDL/DumpParser.hs index b558f409..b7a64f09 100644 --- 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 index c57412d1..8efe0d0a 100644 --- 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, @@ -185,7 +185,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 index 5ebcfa63..a1080ba8 100644 --- 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 index 4d71ee9b..d3245191 100644 --- 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 index 535946a6..be5da76b 100644 --- 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 index b629d75d..5c60d268 100644 --- a/capDL-tool/CapDL/PrintUtils.hs +++ b/capDL-tool/CapDL/PrintUtils.hs @@ -379,9 +379,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 index 7da1a830..4d502972 100644 --- a/capDL-tool/CapDL/State.hs +++ b/capDL-tool/CapDL/State.hs @@ -405,8 +405,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 (ARMIOSpaceCap {}) = True validCapArch AARCH64 (PUDCap {}) = True @@ -451,8 +451,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 @@ -487,7 +487,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 index ceda1b02..45afadd3 100644 --- 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 index 13cd50e0..69030872 100644 --- 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 index a4340bae..01d0e8e2 100644 --- 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 \ Map.empty" definition state :: "cdl_state" where -"state \ \ cdl_arch = ARM11, cdl_objects = objects, +"state \ \ 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 \" diff --git a/capDL-tool/doc/capDL.md b/capDL-tool/doc/capDL.md index 36bd76e1..5b49bf89 100644 --- 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 index 329eb4fb..c56986b6 100644 --- 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 index a7e700ec..88f48422 100644 --- 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 index 69638ef0..65256d6a 100644 --- 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 index 2317f9ec..4a884408 100644 --- 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 index 75253585..6b5f0533 100644 --- 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 "\" syn match CapDLIRQ "\\( 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 index 2be2fc5a..31368c20 100644 --- 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 index de926d25..64b36a68 100644 --- 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 index d13d5775..07f5ca44 100644 --- 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 = { # : [arch_obj_ctor, ] - 'aarch32': [lambda: ARM32Arch(), ['arm', 'arm11']], + 'aarch32': [lambda: ARM32Arch(), ['arm']], 'arm_hyp': [lambda: ARM32Arch(hyp=True), []], 'aarch64': [lambda: AARCH64Arch(), []], 'ia32': [lambda: IA32Arch(), ['x86']],