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

x64 aspec: remove syntax warning

This commit is contained in:
Gerwin Klein 2018-07-15 15:22:12 +01:00
parent 8f1122270c
commit 469b88ea30
1 changed files with 18 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -140,32 +140,33 @@ page is mapped in the same location as this cap was previously used to map it
in. *} in. *}
definition definition
perform_page_invocation :: "page_invocation \<Rightarrow> (unit,'z::state_ext) s_monad" where perform_page_invocation :: "page_invocation \<Rightarrow> (unit,'z::state_ext) s_monad" where
"perform_page_invocation iv \<equiv> (case iv of "perform_page_invocation iv \<equiv> case iv of
PageMap cap ct_slot entries vspace \<Rightarrow> do PageMap cap ct_slot entries vspace \<Rightarrow> do
set_cap cap ct_slot; set_cap cap ct_slot;
(case entries case entries of
of (VMPTE pte, slot) \<Rightarrow> store_pte slot pte (VMPTE pte, slot) \<Rightarrow> store_pte slot pte
| (VMPDE pde, slot) \<Rightarrow> store_pde slot pde | (VMPDE pde, slot) \<Rightarrow> store_pde slot pde
| (VMPDPTE pdpte, slot) \<Rightarrow> store_pdpte slot pdpte); | (VMPDPTE pdpte, slot) \<Rightarrow> store_pdpte slot pdpte;
asid <- case cap of ArchObjectCap (PageCap _ _ _ _ _ (Some (as, _))) \<Rightarrow> return as asid \<leftarrow> case cap of
| _ \<Rightarrow> fail; ArchObjectCap (PageCap _ _ _ _ _ (Some (as, _))) \<Rightarrow> return as
| _ \<Rightarrow> fail;
invalidate_page_structure_cache_asid (addrFromPPtr vspace) asid invalidate_page_structure_cache_asid (addrFromPPtr vspace) asid
od od
| PageRemap entries asid vspace \<Rightarrow> do | PageRemap entries asid vspace \<Rightarrow> do
(case entries case entries of
of (VMPTE pte, slot) \<Rightarrow> store_pte slot pte (VMPTE pte, slot) \<Rightarrow> store_pte slot pte
| (VMPDE pde, slot) \<Rightarrow> store_pde slot pde | (VMPDE pde, slot) \<Rightarrow> store_pde slot pde
| (VMPDPTE pdpte, slot) \<Rightarrow> store_pdpte slot pdpte); | (VMPDPTE pdpte, slot) \<Rightarrow> store_pdpte slot pdpte;
invalidate_page_structure_cache_asid (addrFromPPtr vspace) asid invalidate_page_structure_cache_asid (addrFromPPtr vspace) asid
od od
| PageUnmap cap ct_slot \<Rightarrow> | PageUnmap cap ct_slot \<Rightarrow>
(case cap (case cap of
of PageCap dev base rights map_type sz mapped \<Rightarrow> PageCap dev base rights map_type sz mapped \<Rightarrow>
case mapped of (case mapped of
Some _ \<Rightarrow> case map_type of Some _ \<Rightarrow> (case map_type of
VMVSpaceMap \<Rightarrow> perform_page_invocation_unmap cap ct_slot VMVSpaceMap \<Rightarrow> perform_page_invocation_unmap cap ct_slot
| _ \<Rightarrow> fail | _ \<Rightarrow> fail)
| None \<Rightarrow> return () | None \<Rightarrow> return ())
| _ \<Rightarrow> fail) | _ \<Rightarrow> fail)
(* | PageIOMap asid cap ct_slot entries \<Rightarrow> undefined *) (* | PageIOMap asid cap ct_slot entries \<Rightarrow> undefined *)
| PageGetAddr ptr \<Rightarrow> do | PageGetAddr ptr \<Rightarrow> do
@ -174,7 +175,7 @@ perform_page_invocation :: "page_invocation \<Rightarrow> (unit,'z::state_ext) s
msg_transferred \<leftarrow> set_mrs ct Nothing [paddr]; msg_transferred \<leftarrow> set_mrs ct Nothing [paddr];
msg_info \<leftarrow> return $ MI msg_transferred 0 0 0; msg_info \<leftarrow> return $ MI msg_transferred 0 0 0;
set_message_info ct msg_info set_message_info ct msg_info
od)" od"
text {* PageTable capabilities confer the authority to map and unmap page tables. *} text {* PageTable capabilities confer the authority to map and unmap page tables. *}
definition definition