Skip to content

Commit

Permalink
ARMv6 (arm11) is no longer supported by seL4
Browse files Browse the repository at this point in the history
Signed-off-by: Axel Heider <axelheider@gmx.de>
  • Loading branch information
axel-h committed Mar 10, 2022
1 parent ed23384 commit 9ea20e5
Show file tree
Hide file tree
Showing 19 changed files with 55 additions and 48 deletions.
6 changes: 3 additions & 3 deletions capDL-tool/CapDL/DumpParser.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
7 changes: 4 additions & 3 deletions capDL-tool/CapDL/Model.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -84,7 +84,8 @@ data Cap
| VCPUCap {
capObj :: ObjID }

-- arch specific caps, ARM11, IA32, X86_64 and AARCH64 merged
-- arch specific caps, AARCH32, AARCH64, ARM_HYP, IA32, X86_64, RISCV32,
-- RISCV64 merged
| FrameCap {
capObj :: ObjID,
capRights :: CapRights,
Expand Down Expand Up @@ -182,7 +183,7 @@ data KernelObject a
| RTReply
| VCPU

-- arch specific objects, ARM11, IA32, X86_64, AARCH64 and RISCV mixed
-- arch specific objects, AARCH32, AARCH64, ARM_HYP, IA32, X86_64, RISCV mixed
| ASIDPool { slots :: CapMap a,
capAsidHigh :: Maybe Word }
| PT { slots :: CapMap a }
Expand Down
2 changes: 1 addition & 1 deletion capDL-tool/CapDL/ParserUtils.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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 "aarch32" AARCH32 <|> keyw "x86_64" X86_64 <|> keyw "aarch64" AARCH64 <|> keyw "riscv" RISCV

object_type :: MapParser KOType
object_type =
Expand Down
2 changes: 1 addition & 1 deletion capDL-tool/CapDL/PrintC.hs
Original file line number Diff line number Diff line change
Expand Up @@ -56,7 +56,7 @@ memberArch arch =
where
a = case arch of
IA32 -> "IA32"
ARM11 -> "ARM"
AARCH32 -> "AARCH32"
X86_64 -> "X86_64"
AARCH64 -> "AARCH64"
RISCV -> "RISCV"
Expand Down
4 changes: 2 additions & 2 deletions capDL-tool/CapDL/PrintIsabelle.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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 $+$
Expand Down Expand Up @@ -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"
2 changes: 1 addition & 1 deletion capDL-tool/CapDL/PrintUtils.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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"

Expand Down
10 changes: 5 additions & 5 deletions capDL-tool/CapDL/State.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion capDL-tool/camkes-adder-arm.cdl
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
31 changes: 15 additions & 16 deletions capDL-tool/camkes-adder-arm.right
Original file line number Diff line number Diff line change
@@ -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])
Expand Down Expand Up @@ -205,19 +204,19 @@ objects {
1: adder_group_bin_pd
4: adder_frame__camkes_ipc_buffer_adder_0_control (RW)
}

adder_adder_0_fault_handler_tcb {
0: adder_cnode (guard_size: 28)
1: adder_group_bin_pd
4: adder_frame__camkes_ipc_buffer_adder_0_fault_handler (RW)
}

adder_adder_a_0000_tcb {
0: adder_cnode (guard_size: 28)
1: adder_group_bin_pd
4: adder_frame__camkes_ipc_buffer_adder_a_0000 (RW)
}

adder_cnode {
1: adder_adder_0_control_tcb
2: adder_fault_ep (badge: 1, RWP)
Expand All @@ -230,24 +229,24 @@ objects {
9: adder_post_init_ep (RW)
10: p_ep (R)
}

adder_group_bin_pd {
0: pt_adder_group_bin_0000
1: pt_adder_group_bin_0003
}

client_client_0_control_tcb {
0: client_cnode (guard_size: 28)
1: client_group_bin_pd
4: client_frame__camkes_ipc_buffer_client_0_control (RW)
}

client_client_0_fault_handler_tcb {
0: client_cnode (guard_size: 28)
1: client_group_bin_pd
4: client_frame__camkes_ipc_buffer_client_0_fault_handler (RW)
}

client_cnode {
1: client_client_0_control_tcb
2: client_fault_ep (badge: 1, RWP)
Expand All @@ -258,12 +257,12 @@ objects {
7: client_post_init_ep (RW)
8: p_ep (badge: 1, WP)
}

client_group_bin_pd {
0: pt_client_group_bin_0000
1: pt_client_group_bin_0003
}

pt_adder_group_bin_0000 {
16: frame_adder_group_bin_0000 (RWX)
32: frame_adder_group_bin_0001 (RWX)
Expand All @@ -281,7 +280,7 @@ objects {
224: frame_adder_group_bin_0023 (RWX)
240: frame_adder_group_bin_0047 (RWX)
}

pt_adder_group_bin_0003 {
0: frame_adder_group_bin_0025 (RWX)
16: frame_adder_group_bin_0049 (RWX)
Expand All @@ -308,7 +307,7 @@ objects {
93: adder_frame__camkes_ipc_buffer_adder_0_fault_handler (RW)
95: s_data_0_obj (RWX, uncached)
}

pt_client_group_bin_0000 {
16: frame_client_group_bin_0000 (RWX)
32: frame_client_group_bin_0001 (RWX)
Expand All @@ -326,7 +325,7 @@ objects {
224: frame_client_group_bin_0016 (RWX)
240: frame_client_group_bin_0036 (RWX)
}

pt_client_group_bin_0003 {
0: frame_client_group_bin_0018 (RWX)
16: frame_client_group_bin_0037 (RWX)
Expand All @@ -344,9 +343,9 @@ objects {
80: client_frame__camkes_ipc_buffer_client_0_fault_handler (RW)
82: s_data_0_obj (RWX, uncached)
}

} cdt {

} irq maps {

}
}
2 changes: 1 addition & 1 deletion capDL-tool/camkes-adder-arm.thy.right
Original file line number Diff line number Diff line change
Expand Up @@ -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>"
Expand Down
14 changes: 11 additions & 3 deletions capDL-tool/doc/capDL.md
Original file line number Diff line number Diff line change
Expand Up @@ -152,7 +152,9 @@ in section [Modules](#modules).

### Modules

arch ::= 'arch' ('ia32' | 'arm11')
arch ::= 'arch' ('aarch32' | 'aarch64'
| 'ia32' | 'x86_64' |
| 'riscv32' | 'riscv64')

module ::= arch (obj_decls | cap_decls | irq_decls | cdt_decls)+

Expand Down Expand Up @@ -205,7 +207,10 @@ architecture the system is intended for.
objects :: Map ObjID Object
}

data Arch = IA32 | ARM11
data Arch = AARCH32 | AARCH64
| IA32 | X86_64
| RISCV


Objects are described by the following data type. We are mainly
interested in what capabilities an object contains. We also store
Expand Down Expand Up @@ -380,7 +385,10 @@ A list of ranges `name[r1,r2,..r3]` refers to the union of the ranges

### Module

arch ::= 'arch' ('ia32' | 'arm11')
arch ::= 'arch' ('aarch32' | 'aarch64'
| 'ia32' | 'x86_64' |
| 'riscv32' | 'riscv64')

module ::= arch (obj_decls | cap_decls)+

A module maps to a full `Model` in the data model. Its `Arch` component
Expand Down
2 changes: 1 addition & 1 deletion capDL-tool/example-arm.cdl
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
* SPDX-License-Identifier: BSD-2-Clause
*/

arch arm11
arch aarch32

objects {

Expand Down
2 changes: 1 addition & 1 deletion capDL-tool/example-arm.right
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
arch arm11
arch aarch32

objects {

Expand Down
2 changes: 1 addition & 1 deletion capDL-tool/hello-dump.cdl
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@
* SPDX-License-Identifier: BSD-2-Clause
*/

arch arm11
arch aarch32

objects {

Expand Down
2 changes: 1 addition & 1 deletion capDL-tool/hello-dump.right
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
arch arm11
arch aarch32

objects {

Expand Down
2 changes: 1 addition & 1 deletion capDL-tool/tools/capdl.vim
Original file line number Diff line number Diff line change
Expand Up @@ -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 aarch32 aarch64 ia32 x86_64 riscv32 riscv64
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
Expand Down
4 changes: 2 additions & 2 deletions python-capdl-tool/capdl/PageCollection.py
Original file line number Diff line number Diff line change
Expand Up @@ -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 = {}
Expand Down Expand Up @@ -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)
Expand Down
4 changes: 2 additions & 2 deletions python-capdl-tool/capdl/Spec.py
Original file line number Diff line number Diff line change
Expand Up @@ -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()

Expand Down Expand Up @@ -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
Expand Down
3 changes: 1 addition & 2 deletions python-capdl-tool/capdl/util.py
Original file line number Diff line number Diff line change
Expand Up @@ -151,7 +151,7 @@ def __init__(self, hyp=False):
self.hyp = hyp

def capdl_name(self):
return "arm11"
return "aarch32"

def levels(self):
return [
Expand Down Expand Up @@ -244,7 +244,6 @@ def normalised_map():
'aarch32': 'aarch32',
'aarch64': 'aarch64',
'arm': 'aarch32',
'arm11': 'aarch32',
'arm_hyp': 'arm_hyp',
'ia32': 'ia32',
'x86': 'ia32',
Expand Down

0 comments on commit 9ea20e5

Please sign in to comment.