arm-hyp: rename addressTranslateS1CPR
renamed to: addressTranslateS1 Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
This commit is contained in:
Rafal Kolanski
Rafal Kolanski
parent
08a6e13892
commit
f04a6319cc
|
|
@ -1800,7 +1800,7 @@ proof -
|
|||
apply (csymbr)
|
||||
apply csymbr
|
||||
apply (ctac(no_vcg) add: getRestartPC_ccorres)
|
||||
apply (ctac(no_vcg) add: addressTranslateS1CPR_ccorres)
|
||||
apply (ctac(no_vcg) add: addressTranslateS1_ccorres)
|
||||
apply (rule ccorres_stateAssert)
|
||||
apply csymbr
|
||||
apply (ctac(no_vcg) add: setMR_ccorres_dc)
|
||||
|
|
|
|||
|
|
@ -100,10 +100,10 @@ assumes writeTPIDRURO_ccorres:
|
|||
(doMachineOp (setTPIDRURO reg))
|
||||
(Call writeTPIDRURO_'proc)"
|
||||
|
||||
assumes addressTranslateS1CPR_ccorres:
|
||||
assumes addressTranslateS1_ccorres:
|
||||
"ccorres (=) ret__unsigned_long_' \<top> (\<lbrace>\<acute>vaddr = vaddr \<rbrace>) []
|
||||
(doMachineOp (addressTranslateS1CPR vaddr))
|
||||
(Call addressTranslateS1CPR_'proc)"
|
||||
(doMachineOp (addressTranslateS1 vaddr))
|
||||
(Call addressTranslateS1_'proc)"
|
||||
|
||||
assumes invalidateLocalTLB_ccorres:
|
||||
"ccorres dc xfdc \<top> UNIV []
|
||||
|
|
|
|||
|
|
@ -500,7 +500,7 @@ lemma handleVMFault_ccorres:
|
|||
apply csymbr
|
||||
apply csymbr
|
||||
apply (ctac (no_vcg) add: getHDFAR_ccorres pre: ccorres_liftE_Seq)
|
||||
apply (ctac (no_vcg) add: addressTranslateS1CPR_ccorres pre: ccorres_liftE_Seq)
|
||||
apply (ctac (no_vcg) add: addressTranslateS1_ccorres pre: ccorres_liftE_Seq)
|
||||
apply csymbr
|
||||
apply (ctac (no_vcg) add: getHSR_ccorres pre: ccorres_liftE_Seq)
|
||||
apply csymbr
|
||||
|
|
@ -517,7 +517,7 @@ lemma handleVMFault_ccorres:
|
|||
apply csymbr
|
||||
apply csymbr
|
||||
apply (ctac (no_vcg) pre: ccorres_liftE_Seq)
|
||||
apply (ctac (no_vcg) add: addressTranslateS1CPR_ccorres pre: ccorres_liftE_Seq)
|
||||
apply (ctac (no_vcg) add: addressTranslateS1_ccorres pre: ccorres_liftE_Seq)
|
||||
apply csymbr
|
||||
apply (ctac (no_vcg) add: getHSR_ccorres pre: ccorres_liftE_Seq)
|
||||
apply csymbr
|
||||
|
|
|
|||
|
|
@ -37,7 +37,7 @@ context Arch begin global_naming ARM_HYP
|
|||
crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: handle_fault
|
||||
(simp: kernel_object.splits option.splits arch_cap.splits cap.splits endpoint.splits
|
||||
bool.splits list.splits thread_state.splits split_def catch_def sum.splits
|
||||
Let_def wp: zipWithM_x_empty_fail empty_fail_addressTranslateS1CPR)
|
||||
Let_def wp: zipWithM_x_empty_fail empty_fail_addressTranslateS1)
|
||||
|
||||
crunch (empty_fail) empty_fail[wp]:
|
||||
decode_tcb_configure, decode_bind_notification, decode_unbind_notification,
|
||||
|
|
@ -189,7 +189,7 @@ crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: handle_event, activate_t
|
|||
page_table_invocation.splits page_invocation.splits asid_control_invocation.splits
|
||||
asid_pool_invocation.splits arch_invocation.splits irq_state.splits syscall.splits
|
||||
flush_type.splits page_directory_invocation.splits
|
||||
ignore: resetTimer_impl ackInterrupt_impl addressTranslateS1CPR_impl)
|
||||
ignore: resetTimer_impl ackInterrupt_impl addressTranslateS1_impl)
|
||||
end
|
||||
|
||||
global_interpretation EmptyFail_AI_call_kernel_unit?: EmptyFail_AI_call_kernel_unit
|
||||
|
|
|
|||
|
|
@ -218,7 +218,7 @@ lemma as_user_getRestart_invs[wp]: "\<lbrace>P\<rbrace> as_user t getRestartPC \
|
|||
lemma make_arch_fault_msg_invs[wp, Ipc_AI_assms]: "make_arch_fault_msg f t \<lbrace>invs\<rbrace>"
|
||||
apply (cases f)
|
||||
apply simp_all
|
||||
apply (wpsimp simp: do_machine_op_bind addressTranslateS1CPR_def)
|
||||
apply (wpsimp simp: do_machine_op_bind addressTranslateS1_def)
|
||||
done
|
||||
|
||||
lemma make_fault_message_inv[wp, Ipc_AI_assms]:
|
||||
|
|
@ -409,17 +409,17 @@ lemma transfer_caps_loop_valid_vspace_objs[wp, Ipc_AI_assms]:
|
|||
| assumption | simp split del: if_split)+
|
||||
done
|
||||
|
||||
lemma addressTranslateS1CPR_vms[wp]: "do_machine_op (addressTranslateS1CPR pc) \<lbrace> valid_machine_state \<rbrace>"
|
||||
lemma addressTranslateS1_vms[wp]: "do_machine_op (addressTranslateS1 pc) \<lbrace> valid_machine_state \<rbrace>"
|
||||
by (wpsimp wp: hoare_vcg_all_lift hoare_vcg_disj_lift dmo_machine_state_lift
|
||||
addressTranslateS1CPR_underlying_memory
|
||||
addressTranslateS1_underlying_memory
|
||||
simp: valid_machine_state_def)
|
||||
|
||||
lemma dmo_addressTranslateS1CPR_valid_irq_state[wp]:
|
||||
"do_machine_op (addressTranslateS1CPR pc) \<lbrace>valid_irq_states\<rbrace>"
|
||||
by (wpsimp simp: addressTranslateS1CPR_def do_machine_op_bind wp: dmo_valid_irq_states)
|
||||
lemma dmo_addressTranslateS1_valid_irq_state[wp]:
|
||||
"do_machine_op (addressTranslateS1 pc) \<lbrace>valid_irq_states\<rbrace>"
|
||||
by (wpsimp simp: addressTranslateS1_def do_machine_op_bind wp: dmo_valid_irq_states)
|
||||
|
||||
lemma dmo_addressTranslateS1CPR_cap_refs_respects_device_region[wp]:
|
||||
"do_machine_op (addressTranslateS1CPR pc) \<lbrace>cap_refs_respects_device_region\<rbrace>"
|
||||
lemma dmo_addressTranslateS1_cap_refs_respects_device_region[wp]:
|
||||
"do_machine_op (addressTranslateS1 pc) \<lbrace>cap_refs_respects_device_region\<rbrace>"
|
||||
by (wpsimp wp: cap_refs_respects_device_region_dmo)
|
||||
|
||||
crunch aligned [wp, Ipc_AI_assms]: make_arch_fault_msg "pspace_aligned"
|
||||
|
|
@ -478,9 +478,9 @@ context Arch begin global_naming ARM_HYP
|
|||
|
||||
named_theorems Ipc_AI_cont_assms
|
||||
|
||||
lemma dmo_addressTranslateS1CPR_pspace_respects_device_region[wp]:
|
||||
"do_machine_op (addressTranslateS1CPR pc) \<lbrace>pspace_respects_device_region\<rbrace>"
|
||||
by (wpsimp simp: addressTranslateS1CPR_def do_machine_op_bind wp: device_region_dmos)
|
||||
lemma dmo_addressTranslateS1_pspace_respects_device_region[wp]:
|
||||
"do_machine_op (addressTranslateS1 pc) \<lbrace>pspace_respects_device_region\<rbrace>"
|
||||
by (wpsimp simp: addressTranslateS1_def do_machine_op_bind wp: device_region_dmos)
|
||||
|
||||
crunch pspace_respects_device_region[wp]: make_fault_msg "pspace_respects_device_region"
|
||||
(wp: as_user_inv getRestartPC_inv mapM_wp' simp: getRegister_def ignore: do_machine_op)
|
||||
|
|
|
|||
|
|
@ -70,10 +70,10 @@ lemma getHSR_invs[wp]:
|
|||
"valid invs (do_machine_op getHSR) (\<lambda>_. invs)"
|
||||
by (simp add: getHSR_def do_machine_op_def split_def select_f_returns | wp)+
|
||||
|
||||
lemma addressTranslateS1CPR_invs[wp]:
|
||||
"valid invs (do_machine_op (addressTranslateS1CPR w)) (\<lambda>_. invs)"
|
||||
lemma addressTranslateS1_invs[wp]:
|
||||
"valid invs (do_machine_op (addressTranslateS1 w)) (\<lambda>_. invs)"
|
||||
apply (wp dmo_invs)
|
||||
apply (clarsimp simp add: addressTranslateS1CPR_def machine_rest_lift_def in_monad
|
||||
apply (clarsimp simp add: addressTranslateS1_def machine_rest_lift_def in_monad
|
||||
machine_op_lift_def select_f_def)
|
||||
done
|
||||
|
||||
|
|
|
|||
|
|
@ -102,7 +102,7 @@ declare glob_vs_refs_arch_def[simp]
|
|||
definition
|
||||
"glob_vs_refs \<equiv> arch_obj_fun_lift glob_vs_refs_arch {}"
|
||||
|
||||
crunch_ignore (add: writeContextIDAndPD_impl addressTranslateS1CPR_impl
|
||||
crunch_ignore (add: writeContextIDAndPD_impl addressTranslateS1_impl
|
||||
setSCTLR_impl setHCR_impl
|
||||
set_gic_vcpu_ctrl_vmcr_impl
|
||||
set_gic_vcpu_ctrl_apr_impl
|
||||
|
|
@ -2021,7 +2021,7 @@ lemma dmo_ackInterrupt[wp]: "\<lbrace>invs\<rbrace> do_machine_op (ackInterrupt
|
|||
(* FIXME move to Machine_AI? *)
|
||||
|
||||
crunch device_state_inv[wp]: writeContextIDAndPD "\<lambda>ms. P (device_state ms)"
|
||||
crunch device_state_inv[wp]: addressTranslateS1CPR "\<lambda>ms. P (device_state ms)"
|
||||
crunch device_state_inv[wp]: addressTranslateS1 "\<lambda>ms. P (device_state ms)"
|
||||
crunch device_state_inv[wp]: getSCTLR,get_gic_vcpu_ctrl_hcr,set_gic_vcpu_ctrl_hcr "\<lambda>ms. P (device_state ms)"
|
||||
crunch device_state_inv[wp]: writeVCPUHardwareReg, readVCPUHardwareReg "\<lambda>ms. P (device_state ms)"
|
||||
crunch device_state_inv[wp]: setSCTLR,setHCR,getSCTLR,get_gic_vcpu_ctrl_vmcr,set_gic_vcpu_ctrl_vmcr "\<lambda>ms. P (device_state ms)"
|
||||
|
|
@ -2030,7 +2030,7 @@ crunch device_state_inv[wp]:
|
|||
"\<lambda>ms. P (device_state ms)"
|
||||
|
||||
crunch underlying_memory: setSCTLR,getSCTLR,setHCR "\<lambda>m'. underlying_memory m' p = um"
|
||||
crunch underlying_memory: dsb,isb,writeContextIDAndPD,addressTranslateS1CPR "\<lambda>m'. underlying_memory m' p = um"
|
||||
crunch underlying_memory: dsb,isb,writeContextIDAndPD,addressTranslateS1 "\<lambda>m'. underlying_memory m' p = um"
|
||||
crunch underlying_memory: get_gic_vcpu_ctrl_vmcr,set_gic_vcpu_ctrl_vmcr "\<lambda>m'. underlying_memory m' p = um"
|
||||
crunch underlying_memory: get_gic_vcpu_ctrl_apr,set_gic_vcpu_ctrl_apr "\<lambda>m'. underlying_memory m' p = um"
|
||||
crunch underlying_memory: get_gic_vcpu_ctrl_lr,set_gic_vcpu_ctrl_lr "\<lambda>m'. underlying_memory m' p = um"
|
||||
|
|
|
|||
|
|
@ -466,8 +466,8 @@ lemma no_irq_debugPrint: "no_irq (debugPrint $ xs)"
|
|||
lemma no_irq_writeContextIDAndPD: "no_irq (writeContextIDAndPD asid w)"
|
||||
by (simp add: writeContextIDAndPD_def)
|
||||
|
||||
lemma no_irq_addressTranslateS1CPR: "no_irq (addressTranslateS1CPR w)"
|
||||
apply (clarsimp simp add: addressTranslateS1CPR_def no_irq_def, wp)
|
||||
lemma no_irq_addressTranslateS1: "no_irq (addressTranslateS1 w)"
|
||||
apply (clarsimp simp add: addressTranslateS1_def no_irq_def, wp)
|
||||
apply (simp only: atomize_all)
|
||||
apply (wp no_irq_machine_op_lift[simplified no_irq_def], simp)
|
||||
done
|
||||
|
|
@ -770,9 +770,9 @@ lemma empty_fail_setHCR[simp, intro!]:
|
|||
"empty_fail (setHCR w)"
|
||||
by (simp add: setHCR_def)
|
||||
|
||||
lemma empty_fail_addressTranslateS1CPR[simp, intro!]:
|
||||
"empty_fail (addressTranslateS1CPR w)"
|
||||
by (simp add: addressTranslateS1CPR_def)
|
||||
lemma empty_fail_addressTranslateS1[simp, intro!]:
|
||||
"empty_fail (addressTranslateS1 w)"
|
||||
by (simp add: addressTranslateS1_def)
|
||||
|
||||
lemma empty_fail_writeContextIDAndPD[simp, intro!]:
|
||||
"empty_fail (writeContextIDAndPD asid w)"
|
||||
|
|
|
|||
|
|
@ -31,13 +31,13 @@ lemma no_fail_writeContextIDAndPD[wp]: "no_fail \<top> (writeContextIDAndPD a w)
|
|||
|
||||
(* Move to Machine_AI *)
|
||||
crunches
|
||||
get_gic_vcpu_ctrl_apr, get_gic_vcpu_ctrl_lr, addressTranslateS1CPR, getHDFAR, getHSR,
|
||||
get_gic_vcpu_ctrl_apr, get_gic_vcpu_ctrl_lr, addressTranslateS1, getHDFAR, getHSR,
|
||||
writeVCPUHardwareReg, readVCPUHardwareReg, get_gic_vcpu_ctrl_vmcr, get_gic_vcpu_ctrl_hcr,
|
||||
set_gic_vcpu_ctrl_hcr, set_gic_vcpu_ctrl_vmcr, setHCR, setSCTLR,
|
||||
set_gic_vcpu_ctrl_lr, set_gic_vcpu_ctrl_apr
|
||||
for (no_fail) no_fail[wp, intro!, simp]
|
||||
(wp: no_fail_machine_op_lift crunch_wps
|
||||
ignore: get_gic_vcpu_ctrl_lr_impl bind addressTranslateS1CPR_impl writeVCPUHardwareReg_impl
|
||||
ignore: get_gic_vcpu_ctrl_lr_impl bind addressTranslateS1_impl writeVCPUHardwareReg_impl
|
||||
set_gic_vcpu_ctrl_hcr_impl set_gic_vcpu_ctrl_vmcr_impl setHCR_impl setSCTLR_impl
|
||||
set_gic_vcpu_ctrl_lr_impl set_gic_vcpu_ctrl_apr_impl)
|
||||
|
||||
|
|
|
|||
|
|
@ -1589,18 +1589,18 @@ lemma makeFaultMessage_corres:
|
|||
apply (rule makeArchFaultMessage_corres)
|
||||
done
|
||||
|
||||
lemma dmo_addressTranslateS1CPR_invs'[wp]:
|
||||
"doMachineOp (addressTranslateS1CPR pc) \<lbrace>invs'\<rbrace>"
|
||||
apply (wp dmo_invs' no_irq_addressTranslateS1CPR no_irq)
|
||||
lemma dmo_addressTranslateS1_invs'[wp]:
|
||||
"doMachineOp (addressTranslateS1 pc) \<lbrace>invs'\<rbrace>"
|
||||
apply (wp dmo_invs' no_irq_addressTranslateS1 no_irq)
|
||||
apply clarsimp
|
||||
apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p = underlying_memory m p"
|
||||
in use_valid)
|
||||
apply (clarsimp simp: addressTranslateS1CPR_def machine_op_lift_def
|
||||
apply (clarsimp simp: addressTranslateS1_def machine_op_lift_def
|
||||
machine_rest_lift_def split_def | wp)+
|
||||
done
|
||||
|
||||
lemma dmo_addressTranslateS1CPR_valid_ipc_buffer_ptr'[wp]:
|
||||
"doMachineOp (addressTranslateS1CPR pc) \<lbrace>valid_ipc_buffer_ptr' p\<rbrace>"
|
||||
lemma dmo_addressTranslateS1_valid_ipc_buffer_ptr'[wp]:
|
||||
"doMachineOp (addressTranslateS1 pc) \<lbrace>valid_ipc_buffer_ptr' p\<rbrace>"
|
||||
by (wpsimp wp: hoare_valid_ipc_buffer_ptr_typ_at')
|
||||
|
||||
crunch inv[wp]: makeArchFaultMessage invs'
|
||||
|
|
@ -1846,7 +1846,7 @@ crunch irq_handlers'[wp]: doIPCTransfer "valid_irq_handlers'"
|
|||
|
||||
crunch irq_states'[wp]: doIPCTransfer "valid_irq_states'"
|
||||
(wp: crunch_wps no_irq no_irq_mapM no_irq_storeWord no_irq_loadWord
|
||||
no_irq_case_option no_irq_addressTranslateS1CPR
|
||||
no_irq_case_option no_irq_addressTranslateS1
|
||||
simp: crunch_simps zipWithM_x_mapM)
|
||||
|
||||
crunch pde_mappings'[wp]: doIPCTransfer "valid_pde_mappings'"
|
||||
|
|
@ -2934,13 +2934,13 @@ lemma cteDeleteOne_reply_cap_to'[wp]:
|
|||
apply (clarsimp simp: cte_wp_at_ctes_of isCap_simps)
|
||||
done
|
||||
|
||||
lemma dmo_addressTranslateS1CPR_valid_machine_state'[wp]:
|
||||
"doMachineOp (addressTranslateS1CPR pc) \<lbrace>valid_machine_state'\<rbrace>"
|
||||
lemma dmo_addressTranslateS1_valid_machine_state'[wp]:
|
||||
"doMachineOp (addressTranslateS1 pc) \<lbrace>valid_machine_state'\<rbrace>"
|
||||
by (wpsimp simp: valid_machine_state'_def
|
||||
pointerInUserData_def
|
||||
pointerInDeviceData_def
|
||||
wp: dmo_lift' hoare_vcg_all_lift
|
||||
addressTranslateS1CPR_underlying_memory
|
||||
addressTranslateS1_underlying_memory
|
||||
hoare_vcg_disj_lift)
|
||||
|
||||
crunches setupCallerCap, possibleSwitchTo, asUser, doIPCTransfer
|
||||
|
|
|
|||
|
|
@ -1989,7 +1989,7 @@ lemma hvmf_invs_lift:
|
|||
\<lbrace>P\<rbrace> handleVMFault t flt \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>"
|
||||
unfolding handleVMFault_def
|
||||
by (wpsimp wp: dmo_machine_rest_lift asUser_inv
|
||||
simp: getHSR_def getHDFAR_def addressTranslateS1CPR_def
|
||||
simp: getHSR_def getHDFAR_def addressTranslateS1_def
|
||||
doMachineOp_bind getRestartPC_def getRegister_def)
|
||||
|
||||
lemma hvmf_invs_etc:
|
||||
|
|
|
|||
|
|
@ -20,7 +20,7 @@ fun make_arch_fault_msg :: "arch_fault \<Rightarrow> obj_ref \<Rightarrow> (data
|
|||
where
|
||||
"make_arch_fault_msg (VMFault vptr archData) thread = do
|
||||
pc \<leftarrow> as_user thread getRestartPC;
|
||||
upc \<leftarrow> do_machine_op (addressTranslateS1CPR pc);
|
||||
upc \<leftarrow> do_machine_op (addressTranslateS1 pc);
|
||||
return (5, (upc && ~~ mask pageBits || pc && mask pageBits) # vptr # archData) od"
|
||||
| "make_arch_fault_msg (VCPUFault hsr) thread = return (7, [hsr])"
|
||||
| "make_arch_fault_msg (VPPIEvent irq) thread = return (8, [ucast irq])"
|
||||
|
|
|
|||
|
|
@ -176,7 +176,7 @@ handle_vm_fault :: "word32 \<Rightarrow> vmfault_type \<Rightarrow> (unit,'z::st
|
|||
where
|
||||
"handle_vm_fault thread ARMDataAbort = doE
|
||||
addr \<leftarrow> liftE $ do_machine_op getHDFAR;
|
||||
uaddr \<leftarrow> liftE $ do_machine_op (addressTranslateS1CPR addr);
|
||||
uaddr \<leftarrow> liftE $ do_machine_op (addressTranslateS1 addr);
|
||||
fault \<leftarrow> liftE $ do_machine_op getHSR;
|
||||
let faddr = (uaddr && complement (mask pageBits)) || (addr && mask pageBits)
|
||||
in
|
||||
|
|
@ -185,7 +185,7 @@ odE"
|
|||
|
|
||||
"handle_vm_fault thread ARMPrefetchAbort = doE
|
||||
pc \<leftarrow> liftE $ as_user thread $ getRestartPC;
|
||||
upc \<leftarrow> liftE $ do_machine_op (addressTranslateS1CPR pc);
|
||||
upc \<leftarrow> liftE $ do_machine_op (addressTranslateS1 pc);
|
||||
fault \<leftarrow> liftE $ do_machine_op getHSR;
|
||||
let faddr = (upc && complement (mask pageBits)) || (pc && mask pageBits)
|
||||
in
|
||||
|
|
|
|||
|
|
@ -11,7 +11,7 @@ imports
|
|||
begin
|
||||
context Arch begin global_naming ARM_HYP_H
|
||||
|
||||
#INCLUDE_HASKELL SEL4/Machine/Hardware/ARM.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 setGlobalPD setTTBCR setHardwareASID invalidateLocalTLB invalidateLocalTLB_ASID invalidateLocalTLB_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 paddrBase pptrBase pptrTop paddrTop kernelELFPAddrBase kernelELFBase kernelELFBaseOffset pptrBaseOffset cacheLineBits cacheLine lineStart cacheRangeOp cleanCacheRange_PoC cleanInvalidateCacheRange_RAM cleanCacheRange_RAM cleanCacheRange_PoU invalidateCacheRange_RAM invalidateCacheRange_I branchFlushRange cleanCaches_PoU cleanInvalidateL1Caches addrFromPPtr ptrFromPAddr addrFromKPPtr initIRQController MachineData hapFromVMRights wordsFromPDE wordsFromPTE writeContextIDAndPD hcrVCPU hcrNative vgicHCREN sctlrDefault actlrDefault gicVCPUMaxNumLR 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 setCurrentPDPL2 readVCPUHardwareReg setIRQTrigger writeVCPUHardwareReg getTPIDRURO setTPIDRURO get_cntv_cval_64 set_cntv_cval_64 set_cntv_off_64 get_cntv_off_64 read_cntpct
|
||||
#INCLUDE_HASKELL SEL4/Machine/Hardware/ARM.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 setGlobalPD setTTBCR setHardwareASID invalidateLocalTLB invalidateLocalTLB_ASID invalidateLocalTLB_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 paddrBase pptrBase pptrTop paddrTop kernelELFPAddrBase kernelELFBase kernelELFBaseOffset pptrBaseOffset cacheLineBits cacheLine lineStart cacheRangeOp cleanCacheRange_PoC cleanInvalidateCacheRange_RAM cleanCacheRange_RAM cleanCacheRange_PoU invalidateCacheRange_RAM invalidateCacheRange_I branchFlushRange cleanCaches_PoU cleanInvalidateL1Caches addrFromPPtr ptrFromPAddr addrFromKPPtr initIRQController MachineData hapFromVMRights wordsFromPDE wordsFromPTE writeContextIDAndPD hcrVCPU hcrNative vgicHCREN sctlrDefault actlrDefault gicVCPUMaxNumLR getHSR setHCR getHDFAR addressTranslateS1 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 setCurrentPDPL2 readVCPUHardwareReg setIRQTrigger writeVCPUHardwareReg getTPIDRURO setTPIDRURO get_cntv_cval_64 set_cntv_cval_64 set_cntv_off_64 get_cntv_off_64 read_cntpct
|
||||
|
||||
end
|
||||
|
||||
|
|
|
|||
|
|
@ -23,7 +23,7 @@ This module defines the encoding of arch-specific faults.
|
|||
> import SEL4.Object.TCB(asUser)
|
||||
> import Data.Bits
|
||||
#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
|
||||
> import SEL4.Machine.Hardware.ARM(addressTranslateS1CPR)
|
||||
> import SEL4.Machine.Hardware.ARM(addressTranslateS1)
|
||||
#endif
|
||||
|
||||
\end{impdetails}
|
||||
|
|
@ -39,7 +39,7 @@ in handleVMFault?
|
|||
#ifndef CONFIG_ARM_HYPERVISOR_SUPPORT
|
||||
> return (5, pc:fromVPtr vptr:archData)
|
||||
#else
|
||||
> upc <- doMachineOp (addressTranslateS1CPR $ VPtr pc)
|
||||
> upc <- doMachineOp (addressTranslateS1 $ VPtr pc)
|
||||
> let faddr = (upc .&. complement (mask pageBits)) .|.
|
||||
> (VPtr pc .&. mask pageBits)
|
||||
> return (5, fromVPtr faddr:fromVPtr vptr:archData)
|
||||
|
|
|
|||
|
|
@ -738,7 +738,7 @@ Hypervisor mode requires extra translation here.
|
|||
> handleVMFault _ ARMDataAbort = do
|
||||
#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
|
||||
> addr <- withoutFailure $ doMachineOp getHDFAR
|
||||
> uaddr <- withoutFailure $ doMachineOp (addressTranslateS1CPR addr)
|
||||
> uaddr <- withoutFailure $ doMachineOp (addressTranslateS1 addr)
|
||||
> let faddr = (uaddr .&. complement (mask pageBits)) .|.
|
||||
> (addr .&. mask pageBits)
|
||||
> fault <- withoutFailure $ doMachineOp getHSR
|
||||
|
|
@ -752,7 +752,7 @@ Hypervisor mode requires extra translation here.
|
|||
> handleVMFault thread ARMPrefetchAbort = do
|
||||
> pc <- withoutFailure $ asUser thread $ getRestartPC
|
||||
#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
|
||||
> upc <- withoutFailure $ doMachineOp (addressTranslateS1CPR $ VPtr pc)
|
||||
> upc <- withoutFailure $ doMachineOp (addressTranslateS1 $ VPtr pc)
|
||||
> let faddr = (upc .&. complement (mask pageBits)) .|.
|
||||
> (VPtr pc .&. mask pageBits)
|
||||
> fault <- withoutFailure $ doMachineOp getHSR
|
||||
|
|
|
|||
|
|
@ -507,8 +507,8 @@ implementation assumes the monitor is not modelled in our simulator.
|
|||
> getHDFAR :: MachineMonad VPtr
|
||||
> getHDFAR = error "FIXME ARMHYP machine callback unimplemented"
|
||||
|
||||
> addressTranslateS1CPR :: VPtr -> MachineMonad VPtr
|
||||
> addressTranslateS1CPR = error "FIXME ARMHYP machine callback unimplemented"
|
||||
> addressTranslateS1 :: VPtr -> MachineMonad VPtr
|
||||
> addressTranslateS1 = error "FIXME ARMHYP machine callback unimplemented"
|
||||
|
||||
> getSCTLR :: MachineMonad Word
|
||||
> getSCTLR = error "FIXME ARMHYP machine callback unimplemented"
|
||||
|
|
|
|||
|
|
@ -539,14 +539,14 @@ where
|
|||
"setHCR w \<equiv> machine_op_lift (setHCR_impl w)"
|
||||
|
||||
consts'
|
||||
addressTranslateS1CPR_impl :: "machine_word \<Rightarrow> unit machine_rest_monad"
|
||||
addressTranslateS1CPR_val :: "machine_word \<Rightarrow> machine_state \<Rightarrow> machine_word"
|
||||
addressTranslateS1_impl :: "machine_word \<Rightarrow> unit machine_rest_monad"
|
||||
addressTranslateS1_val :: "machine_word \<Rightarrow> machine_state \<Rightarrow> machine_word"
|
||||
definition
|
||||
addressTranslateS1CPR :: "machine_word \<Rightarrow> machine_word machine_monad"
|
||||
addressTranslateS1 :: "machine_word \<Rightarrow> machine_word machine_monad"
|
||||
where
|
||||
"addressTranslateS1CPR w \<equiv> do
|
||||
machine_op_lift (addressTranslateS1CPR_impl w);
|
||||
gets (addressTranslateS1CPR_val w)
|
||||
"addressTranslateS1 w \<equiv> do
|
||||
machine_op_lift (addressTranslateS1_impl w);
|
||||
gets (addressTranslateS1_val w)
|
||||
od"
|
||||
|
||||
definition
|
||||
|
|
|
|||
Loading…
Reference in New Issue