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

capdl: update PageMap to replace PageRemap (SELFOUR-161)

This commit is contained in:
Victor Phan 2019-09-26 16:53:08 +10:00
parent 1522b8bdb4
commit c143029f25
4 changed files with 3 additions and 42 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
spec/capDL/Intents_D.thy
View File

@ -155,14 +155,6 @@ datatype cdl_page_table_intent =
datatype cdl_page_intent =
(* Map: (target), (pd), vaddr, rights, attr *)
PageMapIntent word32 "cdl_right set" cdl_raw_vmattrs
(*
* Remap: (target), (pd), rights, attr
*
* Note that Remap differs from the abstract spec. This is to
* prevent Remap() from taking place after all rights to the PD
* are long-gone.
*)
| PageRemapIntent"cdl_right set" cdl_raw_vmattrs
(* Unmap: (target) *)
| PageUnmapIntent
(* FlushCaches: (target) *)

1
spec/capDL/Invocations_D.thy
View File

@ -81,7 +81,6 @@ datatype flush =
datatype cdl_page_invocation =
PageMap cdl_cap cdl_cap cdl_cap_ref "cdl_cap_ref list"
| PageRemap cdl_cap "cdl_cap_ref list"
| PageUnmap "cdl_mapped_addr option" cdl_object_id "cdl_cap_ref" nat
| PageFlushCaches flush
| PageGetAddress

1
spec/capDL/PageTableUnmap_D.thy
View File

@ -250,7 +250,6 @@ text \<open>
Should only be used on bounded revokes.
* PageTableUnmap pt_cap_ref
* PageRemap _ frame_cap_ref _
* PageUnmap frame_cap_ref \<Rightarrow>
* revoke_cap_simple (target_tcb, tcb_replycap_slot)
\<close>

35
spec/capDL/PageTable_D.thy
View File

@ -43,7 +43,7 @@ where
\<comment> \<open>
Map the given PageTable into the given PageDirectory at the given
virtual address.
The concrete implementation only allows a PageTable to be mapped
once at any point in time, but we don't enforce that here.
\<close>
@ -95,7 +95,7 @@ where
\<comment> \<open>
Map the given Page into the given PageDirectory or PageTable at
the given virtual address.
The concrete implementation only allows a Page to be mapped
once at any point in time, but we don't enforce that here.
\<close>
@ -109,7 +109,7 @@ where
| _ \<Rightarrow> throw;
\<comment> \<open>Collect mapping from target cap.\<close>
(frame, sz,dev) \<leftarrow> returnOk $ (case target of FrameCap dev p R sz m mp \<Rightarrow> (p,sz,dev));
(frame,sz,dev) \<leftarrow> returnOk $ (case target of FrameCap dev p R sz m mp \<Rightarrow> (p,sz,dev));
target_slots \<leftarrow> cdl_page_mapping_entries vaddr sz pd_object_id;
@ -129,31 +129,6 @@ where
(returnOk $ PageUnmap asid frame target_ref sz) \<sqinter> throw
odE
\<comment> \<open>Change the rights on a given mapping.\<close>
| PageRemapIntent rights attrs \<Rightarrow>
doE
\<comment> \<open>Ensure user has a right to the PD.\<close>
pd \<leftarrow> throw_on_none $ get_index caps 0;
pd_object_id \<leftarrow>
case (fst pd) of
PageDirectoryCap x _ _ \<Rightarrow> returnOk x
| _ \<Rightarrow> throw;
pd_object \<leftarrow> liftE $ get_object pd_object_id;
\<comment> \<open>Find all of our children caps.\<close>
pd_slots \<leftarrow> liftE $ gets $ all_pd_pt_slots pd_object pd_object_id;
target_slots \<leftarrow> liftE $ select {M. set M \<subseteq> pd_slots \<and> distinct M};
\<comment> \<open>Calculate rights.\<close>
new_rights \<leftarrow> returnOk $ validate_vm_rights $ cap_rights target \<inter> rights;
\<comment> \<open>Collect mapping from target cap.\<close>
(frame, sz, dev) \<leftarrow> returnOk $ (case target of FrameCap dev p R sz m mp \<Rightarrow> (p,sz,dev));
returnOk $ PageRemap (FrameCap False frame new_rights sz Fake None) target_slots
odE \<sqinter> throw
\<comment> \<open>Flush the caches associated with this page.\<close>
| PageFlushCachesIntent \<Rightarrow>
(returnOk $ PageFlushCaches Unify) \<sqinter> (returnOk $ PageFlushCaches Clean) \<sqinter>
@ -221,10 +196,6 @@ where
set_cap frame_cap_ref (reset_mem_mapping cap)
od
| PageRemap pseudo_frame_cap target_slots \<Rightarrow>
mapM_x (swp set_cap pseudo_frame_cap) target_slots
| PageFlushCaches flush \<Rightarrow> return ()
| PageGetAddress \<Rightarrow>