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

riscv aspec: fix addr conversions in set_vm_root 

global_pt needs addrFromKPPtr, because it is an address that lives in the
kernel image, other pt's need addrFromPPtr because they are standard
kernel-virtual addresses.
This commit is contained in:
Gerwin Klein 2019-07-20 21:02:52 +10:00
parent e44423d6bb
commit d4f3d7122c
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
spec/abstract/RISCV64/ArchVSpace_A.thy
View File

@ -95,12 +95,12 @@ definition set_vm_root :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad"
ArchObjectCap (PageTableCap pt (Some (asid, _))) \<Rightarrow> doE
pt' \<leftarrow> find_vspace_for_asid asid;
whenE (pt \<noteq> pt') $ throwError InvalidRoot;
liftE $ do_machine_op $ setVSpaceRoot pt (ucast asid)
liftE $ do_machine_op $ setVSpaceRoot (addrFromPPtr pt) (ucast asid)
odE
| _ \<Rightarrow> throwError InvalidRoot) <catch>
(\<lambda>_. do
global_pt \<leftarrow> gets global_pt;
do_machine_op $ setVSpaceRoot (addrFromPPtr global_pt) 0
do_machine_op $ setVSpaceRoot (addrFromKPPtr global_pt) 0
od)
od"