aarch64+x64 squash: PR suggestions

Use bit in haskell and share simple datatypes and functions between abstract and exec spec. Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
seL4 · Dec 18, 2024 · 5ce4598 · 5ce4598
1 parent adf1d90
commit 5ce4598
Show file tree

Hide file tree

Showing 14 changed files with 67 additions and 51 deletions.
diff --git a/spec/abstract/AARCH64/Arch_Structs_A.thy b/spec/abstract/AARCH64/Arch_Structs_A.thy
@@ -9,7 +9,7 @@ chapter "AARCH64-Specific Data Types"
 
 theory Arch_Structs_A
 imports
-  "ExecSpec.Arch_Structs_B"
+  ExecSpec.Arch_Structs_B
   ExceptionTypes_A
   VMRights_A
   ExecSpec.Arch_Kernel_Config_Lemmas
@@ -370,14 +370,6 @@ record arch_tcb =
   tcb_context :: user_context
   tcb_vcpu    :: "obj_ref option"
 
-datatype arch_tcb_flag
-  = FpuDisabled
-
-definition word_from_arch_tcb_flag :: "arch_tcb_flag \<Rightarrow> machine_word" where
-  "word_from_arch_tcb_flag flag \<equiv>
-     case flag of
-       FpuDisabled \<Rightarrow> bit 0"
-
 end_qualify
 
 context Arch begin arch_global_naming (A)

diff --git a/spec/abstract/Structures_A.thy b/spec/abstract/Structures_A.thy
@@ -13,6 +13,7 @@ chapter "Basic Data Structures"
 
 theory Structures_A
 imports
+  ExecSpec.Structs_B
   Arch_Structs_A
   "ExecSpec.MachineExports"
 begin
@@ -23,7 +24,6 @@ arch_requalify_types (A)
   arch_kernel_obj
   arch_state
   arch_tcb
-  arch_tcb_flag
   aa_type
 
 arch_requalify_consts (A)
@@ -47,7 +47,6 @@ arch_requalify_consts (A)
   untyped_min_bits
   untyped_max_bits
   msg_label_bits
-  word_from_arch_tcb_flag
 
 text \<open>
   User mode can request these objects to be created by retype:
@@ -369,18 +368,10 @@ datatype thread_state
 
 type_synonym priority = word8
 
-datatype tcb_flag
-  = ArchFlag arch_tcb_flag
-
-definition word_from_tcb_flag :: "tcb_flag \<Rightarrow> machine_word" where
-  "word_from_tcb_flag flag \<equiv>
-     case flag of
-       ArchFlag arch_flag \<Rightarrow> word_from_arch_tcb_flag arch_flag"
-
 type_synonym tcb_flags = "tcb_flag set"
 
 definition word_to_tcb_flags :: "machine_word \<Rightarrow> tcb_flags" where
-  "word_to_tcb_flags w \<equiv> {flag. word_from_tcb_flag flag && w \<noteq> 0}"
+  "word_to_tcb_flags w \<equiv> {flag. tcbFlagToWord flag && w \<noteq> 0}"
 
 record tcb =
  tcb_ctable        :: cap

diff --git a/spec/abstract/X64/Arch_Structs_A.thy b/spec/abstract/X64/Arch_Structs_A.thy
@@ -8,7 +8,7 @@ chapter "x64-Specific Data Types"
 
 theory Arch_Structs_A
 imports
-  "ExecSpec.Arch_Structs_B"
+  ExecSpec.Arch_Structs_B
   ExceptionTypes_A
   VMRights_A
   ExecSpec.Arch_Kernel_Config_Lemmas
@@ -312,7 +312,7 @@ record arch_state =
   x64_num_ioapics           :: "64 word"
   x64_ioapic_nirqs          :: "machine_word \<Rightarrow> 8 word"
   x64_irq_state             :: "8 word \<Rightarrow> X64_A.X64IRQState"
-  x64_current_fpu_owner :: "obj_ref option"
+  x64_current_fpu_owner     :: "obj_ref option"
 
 (* FIXME x64-vtd:
   x64_num_io_domain_bits    :: "16 word"
@@ -410,14 +410,6 @@ text \<open> Arch-specific part of a TCB: this must have at least a field for us
 record arch_tcb =
   tcb_context :: user_context
 
-datatype arch_tcb_flag
-  = FpuDisabled
-
-definition word_from_arch_tcb_flag :: "arch_tcb_flag \<Rightarrow> machine_word" where
-  "word_from_arch_tcb_flag flag \<equiv>
-     case flag of
-       FpuDisabled \<Rightarrow> bit 0"
-
 end_qualify
 
 context Arch begin arch_global_naming (A)

diff --git a/spec/design/skel/AARCH64/ArchStructures_H.thy b/spec/design/skel/AARCH64/ArchStructures_H.thy
@@ -18,11 +18,11 @@ context Arch begin arch_global_naming (H)
 #INCLUDE_SETTINGS keep_constructor=arch_tcb
 
 #INCLUDE_HASKELL SEL4/Object/Structures/AARCH64.hs CONTEXT AARCH64_H decls_only \
-  NOT VPPIEventIRQ VirtTimer
+  NOT VPPIEventIRQ VirtTimer ArchTcbFlag archTcbFlagToWord
 #INCLUDE_HASKELL SEL4/Object/Structures/AARCH64.hs CONTEXT AARCH64_H instanceproofs \
   NOT VPPIEventIRQ VirtTimer
 #INCLUDE_HASKELL SEL4/Object/Structures/AARCH64.hs CONTEXT AARCH64_H bodies_only \
-  NOT makeVCPUObject
+  NOT makeVCPUObject archTcbFlagToWord
 
 (* we define makeVCPUObject_def manually because we want a total function vgicLR *)
 defs makeVCPUObject_def:

diff --git a/spec/design/skel/AARCH64/Arch_Structs_B.thy b/spec/design/skel/AARCH64/Arch_Structs_B.thy
@@ -10,7 +10,9 @@
 chapter "Common, Architecture-Specific Data Types"
 
 theory Arch_Structs_B
-imports Setup_Locale
+imports
+  Setup_Locale
+  MachineExports
 begin
 
 context Arch begin arch_global_naming (H)
@@ -19,6 +21,8 @@ context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL SEL4/API/Invocation/AARCH64.hs CONTEXT AARCH64_H ONLY FlushType
 
+#INCLUDE_HASKELL SEL4/Object/Structures/AARCH64.hs CONTEXT AARCH64_H ONLY ArchTcbFlag archTcbFlagToWord
+
 end
 
 end
diff --git a/spec/design/skel/Structs_B.thy b/spec/design/skel/Structs_B.thy
@@ -0,0 +1,24 @@
+(*
+ * Copyright 2024, Proofcraft Pty Ltd
+ *
+ * SPDX-License-Identifier: GPL-2.0-only
+ *)
+
+(* Generic data types shared by spec and abstract. *)
+
+chapter "Common, Generic Data Types"
+
+theory Structs_B
+imports Arch_Structs_B
+begin
+
+arch_requalify_types (H)
+  arch_tcb_flag
+
+arch_requalify_consts (H)
+  archTcbFlagToWord
+
+#INCLUDE_SETTINGS keep_constructor = tcb_flag
+#INCLUDE_HASKELL SEL4/Object/Structures.lhs ONLY TcbFlag tcbFlagToWord
+
+end
diff --git a/spec/design/skel/Structures_H.thy b/spec/design/skel/Structures_H.thy
@@ -12,6 +12,7 @@ chapter "Kernel Data Structures"
 
 theory Structures_H
 imports
+  Structs_B
   Config_H
   State_H
   Fault_H
@@ -24,20 +25,18 @@ arch_requalify_types (H)
   arch_kernel_object
   asid
   arch_tcb
-  arch_tcb_flag
 
 arch_requalify_consts (H)
   archObjSize
   nullPointer
   newArchTCB
-  archTcbFlagToWord
   fromPPtr
   PPtr
   atcbContextGet
   atcbContextSet
 
-#INCLUDE_HASKELL SEL4/Object/Structures.lhs decls_only NOT isNullCap isUntypedCap isIRQControlCap isReplyCap isDomainCap isNotificationCap
-#INCLUDE_HASKELL SEL4/Object/Structures.lhs bodies_only NOT kernelObjectTypeName isNullCap isUntypedCap isIRQControlCap isReplyCap isDomainCap isNotificationCap
+#INCLUDE_HASKELL SEL4/Object/Structures.lhs decls_only NOT isNullCap isUntypedCap isIRQControlCap isReplyCap isDomainCap isNotificationCap TcbFlag tcbFlagToWord
+#INCLUDE_HASKELL SEL4/Object/Structures.lhs bodies_only NOT kernelObjectTypeName isNullCap isUntypedCap isIRQControlCap isReplyCap isDomainCap isNotificationCap tcbFlagToWord
 
 
 end
diff --git a/spec/design/skel/X64/ArchStructures_H.thy b/spec/design/skel/X64/ArchStructures_H.thy
@@ -16,9 +16,11 @@ context Arch begin arch_global_naming (H)
 #INCLUDE_SETTINGS keep_constructor=asidpool
 #INCLUDE_SETTINGS keep_constructor=arch_tcb
 
-#INCLUDE_HASKELL SEL4/Object/Structures/X64.lhs CONTEXT X64_H decls_only
+#INCLUDE_HASKELL SEL4/Object/Structures/X64.lhs CONTEXT X64_H decls_only \
+  NOT ArchTcbFlag archTcbFlagToWord
 #INCLUDE_HASKELL SEL4/Object/Structures/X64.lhs CONTEXT X64_H instanceproofs
-#INCLUDE_HASKELL SEL4/Object/Structures/X64.lhs CONTEXT X64_H bodies_only
+#INCLUDE_HASKELL SEL4/Object/Structures/X64.lhs CONTEXT X64_H bodies_only \
+  NOT archTcbFlagToWord
 
 datatype arch_kernel_object_type =
     PDET

diff --git a/spec/design/skel/X64/Arch_Structs_B.thy b/spec/design/skel/X64/Arch_Structs_B.thy
@@ -9,13 +9,17 @@
 chapter "Common, Architecture-Specific Data Types"
 
 theory Arch_Structs_B
-imports Main Setup_Locale
+imports
+  Setup_Locale
+  MachineExports
 begin
 
 context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL SEL4/Model/StateData/X64.lhs CONTEXT X64_H ONLY X64VSpaceRegionUse
 
+#INCLUDE_HASKELL SEL4/Object/Structures/X64.lhs CONTEXT X64_H ONLY ArchTcbFlag archTcbFlagToWord
+
 end (* context X64 *)
 
 end
diff --git a/spec/haskell/src/SEL4/Object/Structures.lhs b/spec/haskell/src/SEL4/Object/Structures.lhs
@@ -501,12 +501,12 @@ Various operations on the free index of an Untyped cap.
 
 > type TcbFlags = Word
 
-> data TcbFlag
->     = NoFlag
->     | ArchFlag ArchTcbFlag
+> noFlag :: TcbFlags
+> noFlag = 0x0
+
+> data TcbFlag = ArchFlag ArchTcbFlag
 
 > tcbFlagToWord :: TcbFlag -> Word
-> tcbFlagToWord NoFlag = 0x0
 > tcbFlagToWord (ArchFlag archFlag) = archTcbFlagToWord archFlag
 
 > isFlagSet :: TcbFlag -> TcbFlags -> Bool

diff --git a/spec/haskell/src/SEL4/Object/Structures/AARCH64.hs b/spec/haskell/src/SEL4/Object/Structures/AARCH64.hs
@@ -73,7 +73,7 @@ atcbContextGet = atcbContext
 data ArchTcbFlag = FpuDisabled
 
 archTcbFlagToWord :: ArchTcbFlag -> Word
-archTcbFlagToWord (FpuDisabled) = 0x1
+archTcbFlagToWord (FpuDisabled) = bit 0
 
 
 {- ASID Pools -}

diff --git a/spec/haskell/src/SEL4/Object/Structures/X64.lhs b/spec/haskell/src/SEL4/Object/Structures/X64.lhs
@@ -124,7 +124,7 @@ present on all platforms is stored here.
 > data ArchTcbFlag = FpuDisabled
 
 > archTcbFlagToWord :: ArchTcbFlag -> Word
-> archTcbFlagToWord (FpuDisabled) = 0x1
+> archTcbFlagToWord (FpuDisabled) = bit 0
 
 \subsection{ASID Pools}
 

diff --git a/spec/machine/AARCH64/MachineOps.thy b/spec/machine/AARCH64/MachineOps.thy
@@ -175,9 +175,9 @@ definition setFPUState :: "fpu_state \<Rightarrow> unit user_monad" where
   "setFPUState fc \<equiv> modify (\<lambda>s. UserContext fc (user_regs s))"
 
 \<comment> \<open>This function touches the CPACR_EL1 register, which is used to enable/disable the FPU for EL0
-   and EL1 and is generally controlled by the VM. seL4 only modifies it by unconditionally enabling
-   it when disabling a VCPU, it instead toggles CPTR_EL2 to enable or disable the FPU for native
-   tasks.\<close>
+   and EL1 and is generally controlled by the VM. seL4 only modifies it when unconditionally enabling
+   it while disabling a VCPU, and seL4 instead toggles CPTR_EL2 to enable or disable the FPU for
+   native tasks.\<close>
 \<comment> \<open>FIXME FPU: The underlying register is saved and restored when switching between VCPUs, so this
      will probably need to be moved out of machine\_rest\_monad.\<close>
 consts' enableFpuEL01_impl :: "unit machine_rest_monad"

diff --git a/spec/machine/X64/MachineOps.thy b/spec/machine/X64/MachineOps.thy
@@ -278,11 +278,19 @@ definition writeFpuState :: "fpu_state \<Rightarrow> unit machine_monad" where
      machine_op_lift $ writeFpuState_impl val
    od"
 
+consts' enableFpu_impl :: "unit machine_rest_monad"
 definition enableFpu :: "unit machine_monad" where
-  "enableFpu \<equiv> modify (\<lambda>s. s\<lparr>fpu_enabled := True \<rparr>)"
+  "enableFpu ≡ do
+     machine_op_lift enableFpu_impl;
+     modify (λs. s⦇fpu_enabled := True ⦈)
+   od"
 
+consts' disableFpu_impl :: "unit machine_rest_monad"
 definition disableFpu :: "unit machine_monad" where
-  "disableFpu \<equiv> modify (\<lambda>s. s\<lparr>fpu_enabled := False \<rparr>)"
+  "disableFpu ≡ do
+     machine_op_lift disableFpu_impl;
+     modify (λs. s⦇fpu_enabled := False ⦈)
+   od"
 
 definition isFpuEnable :: "bool machine_monad" where
   "isFpuEnable \<equiv> gets fpu_enabled"