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

arm-hyp abstract: (Fix) Correctly defining setCurrentPD

This commit is contained in:
Alejandro Gomez-Londono 2017-04-05 17:43:04 +10:00 committed by Alejandro Gomez-Londono
parent cd8a45c220
commit 8ace5b721d
3 changed files with 10 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
spec/abstract/ARM_HYP/ArchVSpaceAcc_A.thy
View File

@ -88,6 +88,11 @@ definition
set_object ptr (ArchObj (PageDirectory pd))
od"
definition
set_current_pd :: "paddr \<Rightarrow> unit machine_monad"
where
"set_current_pd pd \<equiv> setCurrentPDPL2 pd"
text {* The following function takes a pointer to a PDE in kernel memory
and returns the actual PDE. *}
definition

2
spec/abstract/ARM_HYP/ArchVSpace_A.thy
View File

@ -588,7 +588,7 @@ definition
| _ \<Rightarrow> throwError InvalidRoot) <catch>
(\<lambda>_. do
global_us_pd \<leftarrow> gets (arm_us_global_pd o arch_state);
do_machine_op $ setCurrentPD $ addrFromPPtr global_us_pd
do_machine_op $ set_current_pd $ addrFromPPtr global_us_pd
od)
od"

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

@ -157,14 +157,11 @@ definition
dmb :: "unit machine_monad"
where "dmb \<equiv> machine_op_lift dmb_impl"
consts'
setCurrentPDPL2_impl :: "paddr \<Rightarrow> unit machine_rest_monad"
definition
setCurrentPD :: "paddr \<Rightarrow> unit machine_monad"
where "setCurrentPD pd \<equiv> do
dsb;
writeTTBR0 pd;
isb
od"
setCurrentPDPL2 :: "paddr \<Rightarrow> unit machine_monad"
where "setCurrentPDPL2 pd \<equiv> machine_op_lift (setCurrentPDPL2_impl pd)"
consts'
invalidateTLB_impl :: "unit machine_rest_monad"