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

x64: commented out some IOSpace stuff, added machine op definitions.

This commit is contained in:
Joel Beeren 2016-10-05 12:02:46 +11:00
parent 80bc041b49
commit 1edc9ced5f
3 changed files with 7 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -73,11 +73,11 @@ datatype page_invocation
| PageUnmap
(page_unmap_cap: arch_cap)
(page_unmap_cap_slot: cslot_ptr)
| PageIOMap
(* | PageIOMap
(page_iomap_cap: cap)
(page_iomap_ct_clot: cslot_ptr)
(page_iomap_asid: iopte)
(page_iomap_entries: "obj_ref") (*FIXME: double check plz*)
(page_iomap_entries: "obj_ref") (*FIXME: double check plz*)*)
| PageGetAddr
(page_get_paddr: obj_ref)

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

@ -164,7 +164,7 @@ perform_page_invocation :: "page_invocation \<Rightarrow> (unit,'z::state_ext) s
(case mapped of Some (asid, vaddr) \<Rightarrow> unmap_page sz asid vaddr base
| None \<Rightarrow> return ())
| _ \<Rightarrow> fail)
| PageIOMap asid cap ct_slot entries \<Rightarrow> undefined (* FIXME unimplemented *)
(* | PageIOMap asid cap ct_slot entries \<Rightarrow> undefined (* FIXME unimplemented *)*)
| PageGetAddr ptr \<Rightarrow> do
paddr \<leftarrow> return $ fromPAddr $ addrFromPPtr ptr;
ct \<leftarrow> gets cur_thread;

5
spec/machine/X64/MachineOps.thy
View File

@ -255,10 +255,13 @@ mfence :: "unit machine_monad"
where
"mfence \<equiv> undefined"
consts'
invalidateTLBEntry_impl :: "word64 \<Rightarrow> unit machine_rest_monad"
definition
invalidateTLBEntry :: "word64 \<Rightarrow> unit machine_monad"
where
"invalidateTLBEntry vptr \<equiv> undefined vptr"
"invalidateTLBEntry vptr \<equiv> machine_op_lift (invalidateTLBEntry_impl vptr)"
definition
firstValidIODomain :: "word16"