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

riscv aspec: unmap_page may be called with unmapped ASID 

This means we can't use gets_the, which asserts, but need find_vspace_for_asid,
which can throw.
This commit is contained in:
Gerwin Klein 2019-07-21 16:48:00 +10:00
parent ed3d2e1ec2
commit 750746296f
1 changed files with 2 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -184,7 +184,8 @@ text \<open>Unmap a mapped page if the given mapping details are still current.\
definition unmap_page :: "vmpage_size \<Rightarrow> asid \<Rightarrow> vspace_ref \<Rightarrow> obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad"
where
"unmap_page pgsz asid vptr pptr \<equiv> doE
(lev, slot) \<leftarrow> liftE $ gets_the $ vs_lookup_slot 0 asid vptr;
top_level_pt \<leftarrow> find_vspace_for_asid asid;
(lev, slot) \<leftarrow> liftE $ gets_the $ pt_lookup_slot top_level_pt vptr \<circ> ptes_of;
unlessE (pt_bits_left lev = pageBitsForSize pgsz) $ throwError InvalidRoot;
pte \<leftarrow> liftE $ get_pte slot;
unlessE (is_PagePTE pte \<and> pptr_from_pte pte = pptr) $ throwError InvalidRoot;