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

Signed-off-by: Corey Lewis <[email protected]>
seL4 · Sep 27, 2024 · 31b2feb · 31b2feb
1 parent 0fc72fd
commit 31b2feb
Show file tree

Hide file tree

Showing 18 changed files with 74 additions and 0 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
@@ -282,6 +282,11 @@ qualify ARM_A (in Arch)
 record arch_tcb =
  tcb_context       :: user_context
 
+type_synonym arch_tcb_flag = unit
+
+definition word_from_arch_tcb_flag :: "arch_tcb_flag \<Rightarrow> machine_word" where
+  "word_from_arch_tcb_flag flag \<equiv> undefined"
+
 end_qualify
 
 context Arch begin arch_global_naming (A)

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
@@ -338,6 +338,11 @@ record arch_state =
   arm_kernel_vspace :: ARM_HYP_A.arm_vspace_region_uses
   arm_us_global_pd  :: obj_ref
 
+type_synonym arch_tcb_flag = unit
+
+definition word_from_arch_tcb_flag :: "arch_tcb_flag \<Rightarrow> machine_word" where
+  "word_from_arch_tcb_flag flag \<equiv> undefined"
+
 end_qualify
 
 context Arch begin arch_global_naming (A)

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
@@ -274,6 +274,11 @@ text \<open> Arch-specific part of a TCB: this must have at least a field for us
 record arch_tcb =
   tcb_context :: user_context
 
+type_synonym arch_tcb_flag = unit
+
+definition word_from_arch_tcb_flag :: "arch_tcb_flag \<Rightarrow> machine_word" where
+  "word_from_arch_tcb_flag flag \<equiv> undefined"
+
 end_qualify
 
 context Arch begin arch_global_naming (A)

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/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 ()