adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

arm-hyp execspec/machine: callbacks and variuos vcpu functions 

- defined callback axiomatisations
This commit is contained in:
Miki Tanaka 2016-12-06 21:12:57 +11:00 committed by Alejandro Gomez-Londono
parent c079f39e3b
commit bb9d8df8e8
2 changed files with 170 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
spec/design/skel/ARM_HYP/Hardware_H.thy
View File

@ -15,7 +15,7 @@ imports
begin
context Arch begin global_naming ARM_HYP_H
#INCLUDE_HASKELL SEL4/Machine/Hardware/ARM_HYP.lhs Platform=Platform.ARM_HYP CONTEXT ARM_HYP_H NOT getMemoryRegions getDeviceRegions getKernelDevices loadWord storeWord storeWordVM getActiveIRQ ackInterrupt maskInterrupt configureTimer resetTimer debugPrint getRestartPC setNextPC clearMemory clearMemoryVM initMemory freeMemory writeTTBR0 setCurrentPD setGlobalPD setTTBCR setHardwareASID invalidateTLB invalidateTLB_ASID invalidateTLB_VAASID cleanByVA cleanByVA_PoU invalidateByVA invalidateByVA_I invalidate_I_PoU cleanInvalByVA branchFlush clean_D_PoU cleanInvalidate_D_PoC cleanInvalidate_D_PoU cleanInvalidateL2Range invalidateL2Range cleanL2Range isb dsb dmb getIFSR getDFSR getFAR HardwareASID wordFromPDE wordFromPTE VMFaultType HypFaultType VMPageSize pageBits pageBitsForSize toPAddr cacheLineBits cacheLine lineStart cacheRangeOp cleanCacheRange_PoC cleanInvalidateCacheRange_RAM cleanCacheRange_RAM cleanCacheRange_PoU invalidateCacheRange_RAM invalidateCacheRange_I branchFlushRange cleanCaches_PoU cleanInvalidateL1Caches addrFromPPtr ptrFromPAddr initIRQController MachineData hapFromVMRights wordsFromPDE wordsFromPTE
#INCLUDE_HASKELL SEL4/Machine/Hardware/ARM_HYP.lhs Platform=Platform.ARM_HYP CONTEXT ARM_HYP_H NOT getMemoryRegions getDeviceRegions getKernelDevices loadWord storeWord storeWordVM getActiveIRQ ackInterrupt maskInterrupt configureTimer resetTimer debugPrint getRestartPC setNextPC clearMemory clearMemoryVM initMemory freeMemory writeTTBR0 setCurrentPD setGlobalPD setTTBCR setHardwareASID invalidateTLB invalidateTLB_ASID invalidateTLB_VAASID cleanByVA cleanByVA_PoU invalidateByVA invalidateByVA_I invalidate_I_PoU cleanInvalByVA branchFlush clean_D_PoU cleanInvalidate_D_PoC cleanInvalidate_D_PoU cleanInvalidateL2Range invalidateL2Range cleanL2Range isb dsb dmb getIFSR getDFSR getFAR HardwareASID wordFromPDE wordFromPTE VMFaultType HypFaultType VMPageSize pageBits pageBitsForSize toPAddr cacheLineBits cacheLine lineStart cacheRangeOp cleanCacheRange_PoC cleanInvalidateCacheRange_RAM cleanCacheRange_RAM cleanCacheRange_PoU invalidateCacheRange_RAM invalidateCacheRange_I branchFlushRange cleanCaches_PoU cleanInvalidateL1Caches addrFromPPtr ptrFromPAddr initIRQController MachineData hapFromVMRights wordsFromPDE wordsFromPTE writeContextIDAndPD getHSR setHCR getHDFAR addressTranslateS1CPR getSCTLR setSCTLR getACTLR setACTLR get_gic_vcpu_ctrl_hcr set_gic_vcpu_ctrl_hcr get_gic_vcpu_ctrl_vmcr set_gic_vcpu_ctrl_vmcr get_gic_vcpu_ctrl_apr set_gic_vcpu_ctrl_apr get_gic_vcpu_ctrl_vtr get_gic_vcpu_ctrl_eisr0 get_gic_vcpu_ctrl_eisr1 get_gic_vcpu_ctrl_misr get_gic_vcpu_ctrl_lr set_gic_vcpu_ctrl_lr
end

170
spec/machine/ARM_HYP/MachineOps.thy
View File

@ -282,7 +282,6 @@ definition
where "initIRQController \<equiv> machine_op_lift initIRQController_impl"
consts'
writeContextID_impl :: "unit machine_rest_monad"
definition
@ -486,7 +485,176 @@ definition
"freeMemory ptr bits \<equiv>
mapM_x (\<lambda>p. storeWord p 0) [ptr, ptr + word_size .e. ptr + 2 ^ bits - 1]"
section "ARMHYP specific definitions"
consts'
writeContextIDAndPD_impl :: "hardware_asid \<Rightarrow> machine_word \<Rightarrow> unit machine_rest_monad"
definition
writeContextIDAndPD :: "hardware_asid \<Rightarrow> machine_word \<Rightarrow> unit machine_monad"
where "writeContextIDAndPD a b \<equiv> machine_op_lift (writeContextIDAndPD_impl a b)"
consts'
HSR_val :: "machine_state \<Rightarrow> machine_word"
HDFAR_val :: "machine_state \<Rightarrow> machine_word"
SCTLR_val :: "machine_state \<Rightarrow> machine_word"
ACTLR_val :: "machine_state \<Rightarrow> machine_word"
definition
getHSR :: "machine_word machine_monad"
where "getHSR \<equiv> gets HSR_val" (* ARMHYP machine callback *)
definition
getHDFAR :: "machine_word machine_monad"
where "getHDFAR \<equiv> gets HDFAR_val" (* ARMHYP machine callback *)
consts'
setHCR_impl :: "machine_word \<Rightarrow> unit machine_rest_monad"
definition
setHCR :: "machine_word \<Rightarrow> unit machine_monad"
where
"setHCR w \<equiv> machine_op_lift (setHCR_impl w)"
consts'
addressTranslateS1CPR_impl :: "machine_word \<Rightarrow> unit machine_rest_monad"
addressTranslateS1CPR_val :: "machine_state \<Rightarrow> machine_word"
definition
addressTranslateS1CPR :: "machine_word \<Rightarrow> machine_word machine_monad"
where
"addressTranslateS1CPR w \<equiv> do
machine_op_lift (addressTranslateS1CPR_impl w);
gets addressTranslateS1CPR_val
od"
consts'
getSCTLR_impl :: "machine_word machine_rest_monad"
definition
getSCTLR :: "machine_word machine_monad"
where "getSCTLR \<equiv> gets SCTLR_val"
consts'
setSCTLR_impl :: "machine_word \<Rightarrow> unit machine_rest_monad"
definition
setSCTLR :: "machine_word \<Rightarrow> unit machine_monad"
where
"setSCTLR w \<equiv> machine_op_lift (setSCTLR_impl w)"
consts'
getACTLR_impl :: "machine_word machine_rest_monad"
definition
getACTLR :: "machine_word machine_monad"
where
"getACTLR \<equiv> gets ACTLR_val"
consts'
setACTLR_impl :: "machine_word \<Rightarrow> unit machine_rest_monad"
definition
setACTLR :: "machine_word \<Rightarrow> unit machine_monad"
where
"setACTLR w \<equiv> machine_op_lift (setACTLR_impl w)"
definition
vgic_irq_active :: "machine_word"
where
"vgic_irq_active \<equiv> 2 << 28"
definition
vgic_irq_mask :: "machine_word"
where
"vgic_irq_mask \<equiv> 3 << 28"
consts' (* ARMHYP is this okay? *)
get_gic_vcpu_ctrl_hcr_impl :: "machine_word machine_rest_monad"
gic_vcpu_ctrl_hcr_val :: "machine_state \<Rightarrow> machine_word"
definition
get_gic_vcpu_ctrl_hcr :: "machine_word machine_monad"
where
"get_gic_vcpu_ctrl_hcr \<equiv> gets gic_vcpu_ctrl_hcr_val"
consts'
set_gic_vcpu_ctrl_hcr_impl :: "machine_word \<Rightarrow> unit machine_rest_monad"
definition
set_gic_vcpu_ctrl_hcr :: "machine_word \<Rightarrow> unit machine_monad"
where
"set_gic_vcpu_ctrl_hcr w \<equiv> machine_op_lift (set_gic_vcpu_ctrl_hcr_impl w)"
consts'
get_gic_vcpu_ctrl_vmcr_impl :: "machine_word machine_rest_monad"
gic_vcpu_ctrl_vmcr_val :: "machine_state \<Rightarrow> machine_word"
definition
get_gic_vcpu_ctrl_vmcr :: "machine_word machine_monad"
where
"get_gic_vcpu_ctrl_vmcr \<equiv> gets gic_vcpu_ctrl_vmcr_val"
consts'
set_gic_vcpu_ctrl_vmcr_impl :: "machine_word \<Rightarrow> unit machine_rest_monad"
definition
set_gic_vcpu_ctrl_vmcr :: "machine_word \<Rightarrow> unit machine_monad"
where
"set_gic_vcpu_ctrl_vmcr w \<equiv> machine_op_lift (set_gic_vcpu_ctrl_vmcr_impl w)"
consts'
get_gic_vcpu_ctrl_apr_impl :: "machine_word machine_rest_monad"
gic_vcpu_ctrl_apr_val :: "machine_state \<Rightarrow> machine_word"
definition
get_gic_vcpu_ctrl_apr :: "machine_word machine_monad"
where
"get_gic_vcpu_ctrl_apr \<equiv> gets gic_vcpu_ctrl_apr_val"
consts'
set_gic_vcpu_ctrl_apr_impl :: "machine_word \<Rightarrow> unit machine_rest_monad"
definition
set_gic_vcpu_ctrl_apr :: "machine_word \<Rightarrow> unit machine_monad"
where
"set_gic_vcpu_ctrl_apr w \<equiv> machine_op_lift (set_gic_vcpu_ctrl_apr_impl w)"
consts'
get_gic_vcpu_ctrl_vtr_impl :: "machine_word machine_rest_monad"
gic_vcpu_ctrl_vtr_val :: "machine_state \<Rightarrow> machine_word"
definition
get_gic_vcpu_ctrl_vtr :: "machine_word machine_monad"
where
"get_gic_vcpu_ctrl_vtr \<equiv> gets gic_vcpu_ctrl_vtr_val"
consts'
set_gic_vcpu_ctrl_vtr_impl :: "machine_word \<Rightarrow> unit machine_rest_monad"
definition
set_gic_vcpu_ctrl_vtr :: "machine_word \<Rightarrow> unit machine_monad"
where
"set_gic_vcpu_ctrl_vtr w \<equiv> machine_op_lift (set_gic_vcpu_ctrl_vtr_impl w)"
consts'
get_gic_vcpu_ctrl_eisr1_impl :: "machine_word machine_rest_monad"
gic_vcpu_ctrl_eisr1_val :: "machine_state \<Rightarrow> machine_word"
definition
get_gic_vcpu_eisr1_vtr :: "machine_word machine_monad"
where
"get_gic_vcpu_eisr1_vtr \<equiv> gets gic_vcpu_ctrl_eisr1_val"
consts'
get_gic_vcpu_ctrl_misr_impl :: "machine_word machine_rest_monad"
gic_vcpu_ctrl_misr_val :: "machine_state \<Rightarrow> machine_word"
definition
get_gic_vcpu_ctrl_misr :: "machine_word machine_monad"
where
"get_gic_vcpu_ctrl_misr \<equiv> gets gic_vcpu_ctrl_misr_val"
consts'
get_gic_vcpu_ctrl_lr_impl :: "nat \<Rightarrow> unit machine_rest_monad"
gic_vcpu_ctrl_lr_val :: "machine_state \<Rightarrow> machine_word"
definition
get_gic_vcpu_ctrl_lr :: "nat \<Rightarrow> machine_word machine_monad"
where
"get_gic_vcpu_ctrl_lr n \<equiv> do
machine_op_lift (get_gic_vcpu_ctrl_lr_impl n);
gets gic_vcpu_ctrl_lr_val
od"
consts'
set_gic_vcpu_ctrl_lr_impl :: "nat \<Rightarrow> machine_word \<Rightarrow> unit machine_rest_monad"
definition
set_gic_vcpu_ctrl_lr :: "nat \<Rightarrow> machine_word \<Rightarrow> unit machine_monad"
where
"set_gic_vcpu_ctrl_lr n w \<equiv> machine_op_lift (set_gic_vcpu_ctrl_lr_impl n w)"
section "User Monad"