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

X64: added dummy VMPML4E to vm_page_entry. 

needs to be reviewed
This commit is contained in:
Joel Beeren 2016-10-19 10:52:46 +11:00
parent dc3cf6b9b8
commit b8048726a6
3 changed files with 6 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -89,6 +89,8 @@ where
"ensure_safe_mapping (VMPDE (PageTablePDE _ _ _), _) = fail"
|
"ensure_safe_mapping (VMPDPTE (PageDirectoryPDPTE _ _ _), _) = fail"
|
"ensure_safe_mapping (VMPML4E _, _) = fail"
text {* Look up a thread's IPC buffer and check that the thread has the right
authority to read or (in the receiver case) write to it. *}

4
spec/abstract/X64/Arch_A.thy
View File

@ -153,11 +153,13 @@ perform_page_invocation :: "page_invocation \<Rightarrow> (unit,'z::state_ext) s
of (VMPTE pte, slot) \<Rightarrow> store_pte slot pte
| (VMPDE pde, slot) \<Rightarrow> store_pde slot pde
| (VMPDPTE pdpte, slot) \<Rightarrow> store_pdpte slot pdpte
| _ \<Rightarrow> fail
od
| PageRemap entries \<Rightarrow> (case entries
of (VMPTE pte, slot) \<Rightarrow> store_pte slot pte
| (VMPDE pde, slot) \<Rightarrow> store_pde slot pde
| (VMPDPTE pdpte, slot) \<Rightarrow> store_pdpte slot pdpte)
| (VMPDPTE pdpte, slot) \<Rightarrow> store_pdpte slot pdpte
| _ \<Rightarrow> fail)
| PageUnmap cap ct_slot \<Rightarrow>
(case cap
of PageCap dev base rights map_type sz mapped \<Rightarrow>

2
spec/abstract/X64/Arch_Structs_A.thy
View File

@ -110,7 +110,7 @@ datatype pte
(pte_rights : cap_rights)
datatype vm_page_entry = VMPTE pte | VMPDE pde | VMPDPTE pdpte
datatype vm_page_entry = VMPTE pte | VMPDE pde | VMPDPTE pdpte | VMPML4E pml4e
datatype translation_type = NotTranslated | Translated