arm-hyp+aarch64 spec+proof: make generic in CONFIG_DISABLE_WFI_WFE_TRAPS

The config option CONFIG_DISABLE_WFI_WFE_TRAPS influences the value of HCR_VCPU (hcrVCPU in Haskell). There is not much to make generic -- it is unfolded exactly once to compare the value in the spec to the value in C. The main part is defining hcrVCPU conditionally based on the config setting. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
seL4 · Sep 25, 2024 · e34ca85 · e34ca85
1 parent d7d306e
commit e34ca85
Show file tree

Hide file tree

Showing 9 changed files with 70 additions and 7 deletions.
diff --git a/proof/crefine/AARCH64/VSpace_C.thy b/proof/crefine/AARCH64/VSpace_C.thy
@@ -2744,7 +2744,7 @@ lemma vcpu_enable_ccorres:
    apply (rule_tac Q'="\<lambda>_. vcpu_at' v" in hoare_post_imp, fastforce)
    apply wpsimp
   apply (clarsimp simp: typ_heap_simps' Collect_const_mem cvcpu_relation_def
-                        cvcpu_regs_relation_def Let_def cvgic_relation_def hcrVCPU_def
+                        cvcpu_regs_relation_def Let_def cvgic_relation_def hcrVCPU_val
          | rule conjI | simp)+
    apply (drule (1) vcpu_at_rf_sr)
    apply (clarsimp simp: typ_heap_simps' cvcpu_relation_def cvgic_relation_def)

diff --git a/proof/crefine/AARCH64/Wellformed_C.thy b/proof/crefine/AARCH64/Wellformed_C.thy
@@ -604,8 +604,21 @@ lemma ptrFromPAddr_mask_cacheLineBits[simp]:
   "ptrFromPAddr v && mask cacheLineBits = v && mask cacheLineBits"
   by (simp add: ptrFromPAddr_def add_mask_ignore)
 
+
+text \<open>hcrVCPU interface\<close>
+
+arch_requalify_facts hcrCommon_def hcrTWE_def hcrTWI_def
+
+(* hcrVCPU can have two values, based on configuration. We only need need the numerical value
+   to match with C, no other computations depend on it *)
+schematic_goal hcrVCPU_val:
+  "hcrVCPU = ?val"
+  by (simp add: hcrVCPU_def hcrCommon_def hcrTWE_def hcrTWI_def
+                Kernel_Config.config_DISABLE_WFI_WFE_TRAPS_def)
+
 (* end of Kernel_Config interface section *)
 
+
 (* Input abbreviations for API object types *)
 (* disambiguates names *)
 

diff --git a/proof/crefine/ARM_HYP/VSpace_C.thy b/proof/crefine/ARM_HYP/VSpace_C.thy
@@ -2084,7 +2084,7 @@ lemma vcpu_enable_ccorres:
    apply (rule_tac Q'="\<lambda>_. vcpu_at' v" in hoare_post_imp, fastforce)
    apply wpsimp
   apply (clarsimp simp: typ_heap_simps' Collect_const_mem cvcpu_relation_def
-                        cvcpu_regs_relation_def Let_def cvgic_relation_def hcrVCPU_def
+                        cvcpu_regs_relation_def Let_def cvgic_relation_def hcrVCPU_val
          | rule conjI | simp)+
   apply (drule (1) vcpu_at_rf_sr)
   apply (clarsimp simp: typ_heap_simps' cvcpu_relation_def cvgic_relation_def)

diff --git a/proof/crefine/ARM_HYP/Wellformed_C.thy b/proof/crefine/ARM_HYP/Wellformed_C.thy
@@ -609,8 +609,21 @@ lemma shiftr_cacheLineBits_less_mask_word_bits:
   using shiftr_less_max_mask[where n=cacheLineBits and x=x] cacheLineBits_sanity
   by (simp add: word_bits_def)
 
+
+text \<open>hcrVCPU interface\<close>
+
+arch_requalify_facts hcrCommon_def hcrTWE_def hcrTWI_def
+
+(* hcrVCPU can have two values, based on configuration. We only need need the numerical value
+   to match with C, no other computations depend on it *)
+schematic_goal hcrVCPU_val:
+  "hcrVCPU = ?val"
+  by (simp add: hcrVCPU_def hcrCommon_def hcrTWE_def hcrTWI_def
+                Kernel_Config.config_DISABLE_WFI_WFE_TRAPS_def)
+
 (* end of Kernel_Config interface section *)
 
+
 (* Input abbreviations for API object types *)
 (* disambiguates names *)
 

diff --git a/spec/cspec/c/gen-config-thy.py b/spec/cspec/c/gen-config-thy.py
@@ -116,7 +116,7 @@
     'CONFIG_TK1_SMMU': (bool, None),
     'CONFIG_ENABLE_A9_PREFETCHER': (bool, None),
     'CONFIG_EXPORT_PMU_USER': (bool, None),
-    'CONFIG_DISABLE_WFI_WFE_TRAPS': (bool, None),
+    'CONFIG_DISABLE_WFI_WFE_TRAPS': (bool, 'config_DISABLE_WFI_WFE_TRAPS'),
     'CONFIG_SMMU_INTERRUPT_ENABLE': (bool, None),
     'CONFIG_AARCH32_FPU_ENABLE_CONTEXT_SWITCH': (bool, None),
     'CONFIG_L1_CACHE_LINE_SIZE_BITS': (nat, None),

diff --git a/spec/design/m-skel/AARCH64/MachineTypes.thy b/spec/design/m-skel/AARCH64/MachineTypes.thy
@@ -115,6 +115,7 @@ definition
   PT_Type \
   VMFaultType HypFaultType vmFaultTypeFSR VMPageSize pageBits ptTranslationBits \
   pageBitsForSize \
+  hcrCommon hcrTWE hcrTWI \
   hcrVCPU hcrNative vgicHCREN sctlrDefault sctlrEL1VM actlrDefault gicVCPUMaxNumLR \
   vcpuBits
 

diff --git a/spec/design/m-skel/ARM_HYP/MachineTypes.thy b/spec/design/m-skel/ARM_HYP/MachineTypes.thy
@@ -11,7 +11,7 @@ imports
   Word_Lib.WordSetup
   Monads.Nondet_Empty_Fail
   Monads.Nondet_Reader_Option
-  Setup_Locale
+  Lib.HaskellLib_H
   Platform
 begin
 context Arch begin arch_global_naming
@@ -136,7 +136,7 @@ definition
 
 
 (* Machine/Hardware/ARM.lhs - hardware_asid, vmfault_type and vmpage_size *)
-#INCLUDE_HASKELL SEL4/Machine/Hardware/ARM.lhs CONTEXT ARM_HYP ONLY HardwareASID VMFaultType HypFaultType VMPageSize pageBits pageBitsForSize hcrVCPU hcrNative vgicHCREN sctlrDefault actlrDefault gicVCPUMaxNumLR
+#INCLUDE_HASKELL SEL4/Machine/Hardware/ARM.lhs CONTEXT ARM_HYP ONLY HardwareASID VMFaultType HypFaultType VMPageSize pageBits pageBitsForSize hcrCommon hcrTWE hcrTWI hcrVCPU hcrNative vgicHCREN sctlrDefault actlrDefault gicVCPUMaxNumLR
 
 end
 

diff --git a/spec/haskell/src/SEL4/Machine/Hardware/AARCH64.hs b/spec/haskell/src/SEL4/Machine/Hardware/AARCH64.hs
@@ -442,7 +442,21 @@ check_export_arch_timer = error "Unimplemented - machine op"
 
 {- Constants -}
 
-hcrVCPU =  (0x80086039 :: Word) -- HCR_VCPU
+hcrCommon :: Word
+--          HCR_VM  | HCR_RW   | HCR_AMO | HCR_IMO | HCR_FMO | HCR_TSC
+hcrCommon = bit 0  .|. bit 31 .|. bit 5 .|. bit 4 .|. bit 3 .|. bit 19
+
+hcrTWE :: Word
+hcrTWE = bit 14
+
+hcrTWI :: Word
+hcrTWI = bit 13
+
+hcrVCPU :: Word -- HCR_VCPU
+hcrVCPU = if config_DISABLE_WFI_WFE_TRAPS
+          then hcrCommon
+          else hcrCommon .|. hcrTWE .|. hcrTWI
+
 hcrNative = (0x8E28103B :: Word) -- HCR_NATIVE
 sctlrEL1VM = (0x34d58820 :: Word) -- SCTLR_EL1_VM
 sctlrDefault  = (0x34d59824 :: Word) -- SCTLR_DEFAULT
@@ -455,3 +469,7 @@ gicVCPUMaxNumLR = (64 :: Int)
 -- The size of the physical address space in hyp mode can be configured on some platforms.
 config_ARM_PA_SIZE_BITS_40 :: Bool
 config_ARM_PA_SIZE_BITS_40 = error "generated from CMake config"
+
+-- Wether to trap WFI/WFE instructions or not in hyp mode
+config_DISABLE_WFI_WFE_TRAPS :: Bool
+config_DISABLE_WFI_WFE_TRAPS = error "generated from CMake config"
diff --git a/spec/haskell/src/SEL4/Machine/Hardware/ARM.lhs b/spec/haskell/src/SEL4/Machine/Hardware/ARM.lhs
@@ -875,12 +875,30 @@ FIXME ARMHYP consider moving to platform code?
 
 #ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
 
-> hcrVCPU =  (0x87039 :: Word) -- HCR_VCPU
+> hcrCommon :: Word
+> --          HCR_TSC | HCR_AMO  | HCR_IO | HCR_FMO | HCR_DC  | HCR_VM
+> hcrCommon = bit 19 .|. bit 5  .|. bit 4 .|. bit 3 .|. bit 12 .|. bit 0
+
+> hcrTWE :: Word
+> hcrTWE = bit 14
+
+> hcrTWI :: Word
+> hcrTWI = bit 13
+
+> hcrVCPU :: Word -- HCR_VCPU
+> hcrVCPU = if config_DISABLE_WFI_WFE_TRAPS
+>           then hcrCommon
+>           else hcrCommon .|. hcrTWE .|. hcrTWI
+
 > hcrNative = (0xFE8103B :: Word) -- HCR_NATIVE
 > vgicHCREN = (0x1 :: Word) -- VGIC_HCR_EN
 > sctlrDefault = (0xc5187c :: Word) -- SCTLR_DEFAULT
 > actlrDefault = (0x40 :: Word) -- ACTLR_DEFAULT
 > gicVCPUMaxNumLR = (64 :: Int)
 
+> -- Wether to trap WFI/WFE instructions or not in hyp mode
+> config_DISABLE_WFI_WFE_TRAPS :: Bool
+> config_DISABLE_WFI_WFE_TRAPS = error "generated from CMake config"
+
 #endif