arm+arm-hyp+riscv64 spec: update other arches for semi-lazy FPU changes

These architectures do not have FPU enabled and so just need minor updates to match the changed interface. Signed-off-by: Corey Lewis <[email protected]>
seL4 · Dec 19, 2024 · 3086f30 · 3086f30
1 parent d500de0
commit 3086f30
Show file tree

Hide file tree

Showing 24 changed files with 96 additions and 15 deletions.
diff --git a/spec/abstract/ARM/ArchTcb_A.thy b/spec/abstract/ARM/ArchTcb_A.thy
@@ -34,5 +34,11 @@ definition
 where
   "arch_post_modify_registers cur t \<equiv> return ()"
 
+definition arch_post_set_flags :: "obj_ref \<Rightarrow> tcb_flags \<Rightarrow> (unit, 'a::state_ext) s_monad" where
+  "arch_post_set_flags t flags \<equiv> return ()"
+
+definition arch_prepare_set_domain :: "obj_ref \<Rightarrow> domain \<Rightarrow> unit det_ext_monad" where
+  "arch_prepare_set_domain t new_dom \<equiv> return ()"
+
 end
 end
diff --git a/spec/abstract/ARM/Arch_A.thy b/spec/abstract/ARM/Arch_A.thy
@@ -45,6 +45,9 @@ definition
      set_vm_root thread
    od"
 
+definition arch_prepare_next_domain :: "(unit,'z::state_ext) s_monad" where
+  "arch_prepare_next_domain \<equiv> return ()"
+
 definition
   arch_activate_idle_thread :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where
   "arch_activate_idle_thread t \<equiv> return ()"

diff --git a/spec/abstract/ARM/Arch_Structs_A.thy b/spec/abstract/ARM/Arch_Structs_A.thy
@@ -12,7 +12,7 @@ chapter "ARM-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

diff --git a/spec/abstract/ARM/Init_A.thy b/spec/abstract/ARM/Init_A.thy
@@ -74,6 +74,7 @@ definition
     tcb_fault = None,
     tcb_bound_notification = None,
     tcb_mcpriority = minBound,
+    tcb_flags = {},
     tcb_arch = init_arch_tcb
   \<rparr>,
   init_globals_frame \<mapsto> ArchObj (DataPage False ARMSmallPage), \<comment> \<open>same reason as why we kept the definition of @{term init_globals_frame}\<close>

diff --git a/spec/abstract/ARM_HYP/ArchTcb_A.thy b/spec/abstract/ARM_HYP/ArchTcb_A.thy
@@ -41,5 +41,11 @@ definition
 where
   "arch_post_modify_registers cur t \<equiv> return ()"
 
+definition arch_post_set_flags :: "obj_ref \<Rightarrow> tcb_flags \<Rightarrow> (unit, 'a::state_ext) s_monad" where
+  "arch_post_set_flags t flags \<equiv> return ()"
+
+definition arch_prepare_set_domain :: "obj_ref \<Rightarrow> domain \<Rightarrow> unit det_ext_monad" where
+  "arch_prepare_set_domain t new_dom \<equiv> return ()"
+
 end
 end
diff --git a/spec/abstract/ARM_HYP/Arch_A.thy b/spec/abstract/ARM_HYP/Arch_A.thy
@@ -46,6 +46,9 @@ definition
      set_vm_root t
    od"
 
+definition arch_prepare_next_domain :: "(unit,'z::state_ext) s_monad" where
+  "arch_prepare_next_domain \<equiv> return ()"
+
 definition
   arch_activate_idle_thread :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where
   "arch_activate_idle_thread t \<equiv> return ()"

diff --git a/spec/abstract/ARM_HYP/Arch_Structs_A.thy b/spec/abstract/ARM_HYP/Arch_Structs_A.thy
@@ -12,7 +12,7 @@ chapter "ARM-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

diff --git a/spec/abstract/ARM_HYP/Init_A.thy b/spec/abstract/ARM_HYP/Init_A.thy
@@ -76,6 +76,7 @@ definition
     tcb_fault = None,
     tcb_bound_notification = None,
     tcb_mcpriority = minBound,
+    tcb_flags = {},
     tcb_arch = init_arch_tcb
   \<rparr>,
   us_global_pd_ptr \<mapsto> us_global_pd)"

diff --git a/spec/abstract/RISCV64/ArchTcb_A.thy b/spec/abstract/RISCV64/ArchTcb_A.thy
@@ -24,5 +24,11 @@ definition arch_post_modify_registers :: "obj_ref \<Rightarrow> obj_ref \<Righta
   where
   "arch_post_modify_registers cur t \<equiv> return ()"
 
+definition arch_post_set_flags :: "obj_ref \<Rightarrow> tcb_flags \<Rightarrow> (unit, 'a::state_ext) s_monad" where
+  "arch_post_set_flags t flags \<equiv> return ()"
+
+definition arch_prepare_set_domain :: "obj_ref \<Rightarrow> domain \<Rightarrow> unit det_ext_monad" where
+  "arch_prepare_set_domain t new_dom \<equiv> return ()"
+
 end
 end
diff --git a/spec/abstract/RISCV64/Arch_A.thy b/spec/abstract/RISCV64/Arch_A.thy
@@ -36,6 +36,9 @@ definition arch_switch_to_idle_thread :: "(unit,'z::state_ext) s_monad"
     set_vm_root thread
   od"
 
+definition arch_prepare_next_domain :: "(unit,'z::state_ext) s_monad" where
+  "arch_prepare_next_domain \<equiv> return ()"
+
 definition arch_activate_idle_thread :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad"
   where
   "arch_activate_idle_thread t \<equiv> return ()"

diff --git a/spec/abstract/RISCV64/Arch_Structs_A.thy b/spec/abstract/RISCV64/Arch_Structs_A.thy
@@ -8,7 +8,7 @@ chapter "RISCV64-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

diff --git a/spec/abstract/RISCV64/Init_A.thy b/spec/abstract/RISCV64/Init_A.thy
@@ -111,6 +111,7 @@ definition init_kheap :: kheap
          tcb_fault = None,
          tcb_bound_notification = None,
          tcb_mcpriority = minBound,
+         tcb_flags = {},
          tcb_arch = init_arch_tcb
          \<rparr>,
       riscv_global_pt_ptr \<mapsto> init_global_pt

diff --git a/spec/design/skel/ARM/ArchStructures_H.thy b/spec/design/skel/ARM/ArchStructures_H.thy
@@ -15,9 +15,11 @@ context Arch begin arch_global_naming (H)
 #INCLUDE_SETTINGS keep_constructor=asidpool
 #INCLUDE_SETTINGS keep_constructor=arch_tcb
 
-#INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs CONTEXT ARM_H decls_only
+#INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs CONTEXT ARM_H decls_only \
+  NOT ArchTcbFlag archTcbFlagToWord
 #INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs CONTEXT ARM_H instanceproofs
-#INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs CONTEXT ARM_H bodies_only
+#INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs CONTEXT ARM_H bodies_only \
+  NOT archTcbFlagToWord
 
 datatype arch_kernel_object_type =
     PDET

diff --git a/spec/design/skel/ARM/Arch_Structs_B.thy b/spec/design/skel/ARM/Arch_Structs_B.thy
@@ -4,16 +4,22 @@
  * SPDX-License-Identifier: GPL-2.0-only
  *)
 
-(* Architecture-specific data types shared by spec and abstract. *)
+(* Architecture-specific data types shared by design and abstract specs. *)
 
 chapter "Common, Architecture-Specific Data Types"
 
 theory Arch_Structs_B
-imports Main Setup_Locale
+imports
+  Setup_Locale
+  Lib.HaskellLib_H
+  MachineExports
 begin
+
 context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL SEL4/Model/StateData/ARM.lhs CONTEXT ARM_H ONLY ArmVSpaceRegionUse
 
+#INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs CONTEXT ARM_H ONLY ArchTcbFlag archTcbFlagToWord
+
 end
 end
diff --git a/spec/design/skel/ARM_HYP/ArchStructures_H.thy b/spec/design/skel/ARM_HYP/ArchStructures_H.thy
@@ -15,9 +15,11 @@ context Arch begin arch_global_naming (H)
 #INCLUDE_SETTINGS keep_constructor=asidpool
 #INCLUDE_SETTINGS keep_constructor=arch_tcb
 
-#INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs CONTEXT ARM_HYP_H decls_only NOT VPPIEventIRQ VirtTimer
+#INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs CONTEXT ARM_HYP_H decls_only NOT VPPIEventIRQ VirtTimer \
+  NOT ArchTcbFlag archTcbFlagToWord
 #INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs CONTEXT ARM_HYP_H instanceproofs NOT VPPIEventIRQ VirtTimer
-#INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs CONTEXT ARM_HYP_H bodies_only NOT makeVCPUObject
+#INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs CONTEXT ARM_HYP_H bodies_only NOT makeVCPUObject \
+  NOT archTcbFlagToWord
 
 (* we define makeVCPUObject_def manually because we want a total function vgicLR *)
 defs makeVCPUObject_def:

diff --git a/spec/design/skel/ARM_HYP/Arch_Structs_B.thy b/spec/design/skel/ARM_HYP/Arch_Structs_B.thy
@@ -4,16 +4,21 @@
  * SPDX-License-Identifier: GPL-2.0-only
  *)
 
-(* Architecture-specific data types shared by spec and abstract. *)
+(* Architecture-specific data types shared by design and abstract specs. *)
 
 chapter "Common, Architecture-Specific Data Types"
 
 theory Arch_Structs_B
-imports Main Setup_Locale
+imports
+  Setup_Locale
+  Lib.HaskellLib_H
+  MachineExports
 begin
 context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL SEL4/Model/StateData/ARM.lhs CONTEXT ARM_HYP_H ONLY ArmVSpaceRegionUse
 
+#INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs CONTEXT ARM_HYP_H ONLY ArchTcbFlag archTcbFlagToWord
+
 end
 end
diff --git a/spec/design/skel/RISCV64/ArchStructures_H.thy b/spec/design/skel/RISCV64/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/RISCV64.hs CONTEXT RISCV64_H decls_only
+#INCLUDE_HASKELL SEL4/Object/Structures/RISCV64.hs CONTEXT RISCV64_H decls_only \
+  NOT ArchTcbFlag archTcbFlagToWord
 #INCLUDE_HASKELL SEL4/Object/Structures/RISCV64.hs CONTEXT RISCV64_H instanceproofs
-#INCLUDE_HASKELL SEL4/Object/Structures/RISCV64.hs CONTEXT RISCV64_H bodies_only
+#INCLUDE_HASKELL SEL4/Object/Structures/RISCV64.hs CONTEXT RISCV64_H bodies_only \
+  NOT archTcbFlagToWord
 
 datatype arch_kernel_object_type =
     PTET

diff --git a/spec/design/skel/RISCV64/Arch_Structs_B.thy b/spec/design/skel/RISCV64/Arch_Structs_B.thy
@@ -4,18 +4,23 @@
  * SPDX-License-Identifier: GPL-2.0-only
  *)
 
-(* Architecture-specific data types shared by spec and abstract. *)
+(* Architecture-specific data types shared by design and abstract specs. *)
 
 chapter "Common, Architecture-Specific Data Types"
 
 theory Arch_Structs_B
-imports Setup_Locale
+imports
+  Setup_Locale
+  Lib.HaskellLib_H
+  MachineExports
 begin
 
 context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL SEL4/Model/StateData/RISCV64.hs CONTEXT RISCV64_H ONLY RISCVVSpaceRegionUse
 
+#INCLUDE_HASKELL SEL4/Object/Structures/RISCV64.hs CONTEXT RISCV64_H ONLY ArchTcbFlag archTcbFlagToWord
+
 end
 
 end
diff --git a/spec/haskell/src/SEL4/Kernel/Thread/ARM.lhs b/spec/haskell/src/SEL4/Kernel/Thread/ARM.lhs
@@ -65,3 +65,7 @@ There is nothing special about idle thread activation on ARM.
 > activateIdleThread :: PPtr TCB -> Kernel ()
 > activateIdleThread _ = return ()
 
+There is nothing special that needs to be done before calling nextDomain on ARM.
+
+> prepareNextDomain :: Kernel ()
+> prepareNextDomain = return ()
diff --git a/spec/haskell/src/SEL4/Kernel/Thread/RISCV64.hs b/spec/haskell/src/SEL4/Kernel/Thread/RISCV64.hs
@@ -30,3 +30,6 @@ switchToIdleThread = do
 
 activateIdleThread :: PPtr TCB -> Kernel ()
 activateIdleThread _ = return ()
+
+prepareNextDomain :: Kernel ()
+prepareNextDomain = return ()
diff --git a/spec/haskell/src/SEL4/Object/Structures/ARM.lhs b/spec/haskell/src/SEL4/Object/Structures/ARM.lhs
@@ -136,6 +136,11 @@ present on all platforms is stored here.
 > atcbContextGet :: ArchTCB -> UserContext
 > atcbContextGet = atcbContext
 
+> type ArchTcbFlag = ()
+
+> archTcbFlagToWord :: ArchTcbFlag -> Word
+> archTcbFlagToWord _ = error "ARM does not have any arch specific flags"
+
 \subsection{ASID Pools}
 
 An ASID pool is an array of pointers to page directories. This is used to implement virtual ASIDs on ARM; it is not accessed by the hardware.

diff --git a/spec/haskell/src/SEL4/Object/Structures/RISCV64.hs b/spec/haskell/src/SEL4/Object/Structures/RISCV64.hs
@@ -73,6 +73,10 @@ atcbContextSet uc atcb = atcb { atcbContext = uc }
 atcbContextGet :: ArchTCB -> UserContext
 atcbContextGet = atcbContext
 
+type ArchTcbFlag = ()
+
+archTcbFlagToWord :: ArchTcbFlag -> Word
+archTcbFlagToWord _ = error "ARM does not have any arch specific flags"
 
 {- ASID Pools -}
 

diff --git a/spec/haskell/src/SEL4/Object/TCB/ARM.lhs b/spec/haskell/src/SEL4/Object/TCB/ARM.lhs
@@ -23,6 +23,7 @@ There are presently no ARM-specific register subsets defined, but in future this
 > import SEL4.Model
 > import SEL4.Object.Structures
 > import SEL4.Object.Instances()
+> import SEL4.API.Types
 > import SEL4.API.Failures
 > import SEL4.API.Invocation.ARM
 > import SEL4.Machine.RegisterSet(setRegister, UserMonad, VPtr(..))
@@ -66,3 +67,8 @@ There are presently no ARM-specific register subsets defined, but in future this
 > postModifyRegisters :: PPtr TCB -> PPtr TCB -> UserMonad ()
 > postModifyRegisters cur ptr = return ()
 
+> postSetFlags :: PPtr TCB -> TcbFlags -> Kernel ()
+> postSetFlags t flags = return ()
+
+> prepareSetDomain :: PPtr TCB -> Domain -> Kernel ()
+> prepareSetDomain t newDom = return ()
diff --git a/spec/haskell/src/SEL4/Object/TCB/RISCV64.hs b/spec/haskell/src/SEL4/Object/TCB/RISCV64.hs
@@ -18,6 +18,7 @@ import Prelude hiding (Word)
 import SEL4.Machine(PPtr)
 import SEL4.Model
 import SEL4.Object.Structures
+import SEL4.API.Types
 import SEL4.API.Failures
 import SEL4.API.Invocation.RISCV64
 import SEL4.Machine.RegisterSet(setRegister, UserMonad, VPtr(..))
@@ -41,3 +42,9 @@ getSanitiseRegisterInfo _ = return False
 
 postModifyRegisters :: PPtr TCB -> PPtr TCB -> UserMonad ()
 postModifyRegisters _ _ = return ()
+
+postSetFlags :: PPtr TCB -> TcbFlags -> Kernel ()
+postSetFlags t flags = return ()
+
+prepareSetDomain :: PPtr TCB -> Domain -> Kernel ()
+prepareSetDomain t newDom = return ()