seL4 · axel-h · Mar 10, 2022 · Mar 10, 2022
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,
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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])
@@ -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)
@@ -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)
@@ -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)
@@ -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)
@@ -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)
@@ -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)
@@ -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 {
 
-}
+}
diff --git a/capDL-tool/camkes-adder-arm.thy.right b/capDL-tool/camkes-adder-arm.thy.right
@@ -338,7 +338,7 @@ definition adder_group_bin_pd_caps :: "cdl_cap_map" where
 definition adder_group_bin_pd :: "cdl_object" where
 "adder_group_bin_pd \<equiv> Types_D.PageDirectory \<lparr> cdl_page_directory_caps = adder_group_bin_pd_caps \<rparr>"
 
-lemma adder_group_bin_pd_object_slots: 
+lemma adder_group_bin_pd_object_slots:
   "object_slots adder_group_bin_pd = adder_group_bin_pd_caps"
   by (simp add: adder_group_bin_pd_def object_slots_def)
 
@@ -349,7 +349,7 @@ definition client_group_bin_pd_caps :: "cdl_cap_map" where
 definition client_group_bin_pd :: "cdl_object" where
 "client_group_bin_pd \<equiv> Types_D.PageDirectory \<lparr> cdl_page_directory_caps = client_group_bin_pd_caps \<rparr>"
 
-lemma client_group_bin_pd_object_slots: 
+lemma client_group_bin_pd_object_slots:
   "object_slots client_group_bin_pd = client_group_bin_pd_caps"
   by (simp add: client_group_bin_pd_def object_slots_def)
 
@@ -633,7 +633,7 @@ definition adder_adder_0_control_tcb :: "cdl_object" where
                                                          cdl_tcb_has_fault = True,
                                                          cdl_tcb_domain = 0 \<rparr>"
 
-lemma adder_adder_0_control_tcb_object_slots: 
+lemma adder_adder_0_control_tcb_object_slots:
   "object_slots adder_adder_0_control_tcb = adder_adder_0_control_tcb_caps"
   by (simp add: adder_adder_0_control_tcb_def object_slots_def)
 
@@ -649,7 +649,7 @@ definition adder_adder_0_fault_handler_tcb :: "cdl_object" where
                                                                cdl_tcb_has_fault = False,
                                                                cdl_tcb_domain = 0 \<rparr>"
 
-lemma adder_adder_0_fault_handler_tcb_object_slots: 
+lemma adder_adder_0_fault_handler_tcb_object_slots:
   "object_slots adder_adder_0_fault_handler_tcb = adder_adder_0_fault_handler_tcb_caps"
   by (simp add: adder_adder_0_fault_handler_tcb_def object_slots_def)
 
@@ -665,7 +665,7 @@ definition adder_adder_a_0000_tcb :: "cdl_object" where
                                                       cdl_tcb_has_fault = True,
                                                       cdl_tcb_domain = 0 \<rparr>"
 
-lemma adder_adder_a_0000_tcb_object_slots: 
+lemma adder_adder_a_0000_tcb_object_slots:
   "object_slots adder_adder_a_0000_tcb = adder_adder_a_0000_tcb_caps"
   by (simp add: adder_adder_a_0000_tcb_def object_slots_def)
 
@@ -681,7 +681,7 @@ definition client_client_0_control_tcb :: "cdl_object" where
                                                            cdl_tcb_has_fault = True,
                                                            cdl_tcb_domain = 0 \<rparr>"
 
-lemma client_client_0_control_tcb_object_slots: 
+lemma client_client_0_control_tcb_object_slots:
   "object_slots client_client_0_control_tcb = client_client_0_control_tcb_caps"
   by (simp add: client_client_0_control_tcb_def object_slots_def)
 
@@ -697,7 +697,7 @@ definition client_client_0_fault_handler_tcb :: "cdl_object" where
                                                                  cdl_tcb_has_fault = False,
                                                                  cdl_tcb_domain = 0 \<rparr>"
 
-lemma client_client_0_fault_handler_tcb_object_slots: 
+lemma client_client_0_fault_handler_tcb_object_slots:
   "object_slots client_client_0_fault_handler_tcb = client_client_0_fault_handler_tcb_caps"
   by (simp add: client_client_0_fault_handler_tcb_def object_slots_def)
 
@@ -721,7 +721,7 @@ definition pt_adder_group_bin_0000_caps :: "cdl_cap_map" where
 definition pt_adder_group_bin_0000 :: "cdl_object" where
 "pt_adder_group_bin_0000 \<equiv> Types_D.PageTable \<lparr> cdl_page_table_caps = pt_adder_group_bin_0000_caps \<rparr>"
 
-lemma pt_adder_group_bin_0000_object_slots: 
+lemma pt_adder_group_bin_0000_object_slots:
   "object_slots pt_adder_group_bin_0000 = pt_adder_group_bin_0000_caps"
   by (simp add: pt_adder_group_bin_0000_def object_slots_def)
 
@@ -754,7 +754,7 @@ definition pt_adder_group_bin_0003_caps :: "cdl_cap_map" where
 definition pt_adder_group_bin_0003 :: "cdl_object" where
 "pt_adder_group_bin_0003 \<equiv> Types_D.PageTable \<lparr> cdl_page_table_caps = pt_adder_group_bin_0003_caps \<rparr>"
 
-lemma pt_adder_group_bin_0003_object_slots: 
+lemma pt_adder_group_bin_0003_object_slots:
   "object_slots pt_adder_group_bin_0003 = pt_adder_group_bin_0003_caps"
   by (simp add: pt_adder_group_bin_0003_def object_slots_def)
 
@@ -778,7 +778,7 @@ definition pt_client_group_bin_0000_caps :: "cdl_cap_map" where
 definition pt_client_group_bin_0000 :: "cdl_object" where
 "pt_client_group_bin_0000 \<equiv> Types_D.PageTable \<lparr> cdl_page_table_caps = pt_client_group_bin_0000_caps \<rparr>"
 
-lemma pt_client_group_bin_0000_object_slots: 
+lemma pt_client_group_bin_0000_object_slots:
   "object_slots pt_client_group_bin_0000 = pt_client_group_bin_0000_caps"
   by (simp add: pt_client_group_bin_0000_def object_slots_def)
 
@@ -802,7 +802,7 @@ definition pt_client_group_bin_0003_caps :: "cdl_cap_map" where
 definition pt_client_group_bin_0003 :: "cdl_object" where
 "pt_client_group_bin_0003 \<equiv> Types_D.PageTable \<lparr> cdl_page_table_caps = pt_client_group_bin_0003_caps \<rparr>"
 
-lemma pt_client_group_bin_0003_object_slots: 
+lemma pt_client_group_bin_0003_object_slots:
   "object_slots pt_client_group_bin_0003 = pt_client_group_bin_0003_caps"
   by (simp add: pt_client_group_bin_0003_def object_slots_def)
 
@@ -822,7 +822,7 @@ definition adder_cnode :: "cdl_object" where
 "adder_cnode \<equiv> Types_D.CNode \<lparr> cdl_cnode_caps = adder_cnode_caps,
                                              cdl_cnode_size_bits = 4 \<rparr>"
 
-lemma adder_cnode_object_slots: 
+lemma adder_cnode_object_slots:
   "object_slots adder_cnode = adder_cnode_caps"
   by (simp add: adder_cnode_def object_slots_def)
 
@@ -840,7 +840,7 @@ definition client_cnode :: "cdl_object" where
 "client_cnode \<equiv> Types_D.CNode \<lparr> cdl_cnode_caps = client_cnode_caps,
                                               cdl_cnode_size_bits = 4 \<rparr>"
 
-lemma client_cnode_object_slots: 
+lemma client_cnode_object_slots:
   "object_slots client_cnode = client_cnode_caps"
   by (simp add: client_cnode_def object_slots_def)
 
@@ -881,7 +881,7 @@ definition p_ep :: "cdl_object" where
 
 
 
-lemmas ids = 
+lemmas ids =
 adder_adder_0_control_tcb_id_def
 adder_adder_0_fault_handler_tcb_id_def
 adder_adder_a_0000_tcb_id_def
@@ -990,7 +990,7 @@ stack__camkes_stack_client_0_fault_handler_1_client_obj_id_def
 stack__camkes_stack_client_0_fault_handler_2_client_obj_id_def
 stack__camkes_stack_client_0_fault_handler_3_client_obj_id_def
 
-lemmas cap_defs = 
+lemmas cap_defs =
 adder_group_bin_pd_caps_def
 client_group_bin_pd_caps_def
 adder_adder_0_control_tcb_caps_def
@@ -1005,7 +1005,7 @@ pt_client_group_bin_0003_caps_def
 adder_cnode_caps_def
 client_cnode_caps_def
 
-lemmas obj_defs = 
+lemmas obj_defs =
 adder_frame__camkes_ipc_buffer_adder_0_control_def
 adder_group_bin_pd_def
 client_group_bin_pd_def
@@ -1205,9 +1205,9 @@ 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>"
 
-end
+end