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

arm-hyp aspec: update PageMap to replace PageRemap (SELFOUR-161)

This commit is contained in:
Victor Phan 2019-09-25 16:40:32 +10:00
parent c64e054c3f
commit 12a7c2d441
3 changed files with 11 additions and 51 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

39
spec/abstract/ARM_HYP/ArchDecode_A.thy
View File

@ -147,15 +147,21 @@ case cap of
attr = args ! 2;
pd_cap = fst (extra_caps ! 0)
in doE
whenE (mapped_address \<noteq> None) $ throwError $ InvalidCapability 0;
(pd,asid) \<leftarrow> (case pd_cap of
ArchObjectCap (PageDirectoryCap pd (Some asid)) \<Rightarrow>
returnOk (pd,asid)
| _ \<Rightarrow> throwError $ InvalidCapability 1);
case mapped_address of
Some (asid', vaddr') \<Rightarrow> doE
whenE (asid' \<noteq> asid) (throwError $ InvalidCapability 1);
whenE (vaddr' \<noteq> vaddr) (throwError $ InvalidArgument 0)
odE
| None \<Rightarrow> doE
vtop \<leftarrow> returnOk (vaddr + (1 << (pageBitsForSize pgsz)) - 1);
whenE (vtop \<ge> kernel_base) $ throwError $ InvalidArgument 0
odE;
pd' \<leftarrow> lookup_error_on_failure False $ find_pd_for_asid asid;
whenE (pd' \<noteq> pd) $ throwError $ InvalidCapability 1;
vtop \<leftarrow> returnOk (vaddr + (1 << (pageBitsForSize pgsz)) - 1);
whenE (vtop \<ge> kernel_base) $ throwError $ InvalidArgument 0;
vm_rights \<leftarrow> returnOk (mask_vm_rights R (data_to_rights rights_mask));
check_vp_alignment pgsz vaddr;
entries \<leftarrow> create_mapping_entries (addrFromPPtr p)
@ -166,32 +172,7 @@ case cap of
(ArchObjectCap $ PageCap dev p R pgsz (Some (asid, vaddr)))
cte entries
odE
else throwError TruncatedMessage
else if invocation_type label = ArchInvocationLabel ARMPageRemap then
if length args > 1 \<and> length extra_caps > 0
then let rights_mask = args ! 0;
attr = args ! 1;
pd_cap = fst (extra_caps ! 0)
in doE
whenE (isIOSpaceFrame cap) $ throwError IllegalOperation;
(pd,asid) \<leftarrow> (case pd_cap of
ArchObjectCap (PageDirectoryCap pd (Some asid)) \<Rightarrow>
returnOk (pd,asid)
| _ \<Rightarrow> throwError $ InvalidCapability 1);
(asid', vaddr) \<leftarrow> (case mapped_address of
Some a \<Rightarrow> returnOk a
| _ \<Rightarrow> throwError $ InvalidCapability 0);
pd' \<leftarrow> lookup_error_on_failure False $ find_pd_for_asid asid';
whenE (pd' \<noteq> pd \<or> asid' \<noteq> asid) $ throwError $ InvalidCapability 1;
vm_rights \<leftarrow> returnOk (mask_vm_rights R $ data_to_rights rights_mask);
check_vp_alignment pgsz vaddr;
entries \<leftarrow> create_mapping_entries (addrFromPPtr p)
vaddr pgsz vm_rights
(attribs_from_word attr) pd;
ensure_safe_mapping entries;
returnOk $ InvokePage $ PageRemap asid' entries
odE
else throwError TruncatedMessage
else throwError TruncatedMessage
else if invocation_type label = ArchInvocationLabel ARMPageUnmap
then returnOk $ InvokePage $ PageUnmap cap cte
else if isPageFlushLabel (invocation_type label) then

3
spec/abstract/ARM_HYP/ArchInvocation_A.thy
View File

@ -48,9 +48,6 @@ datatype page_invocation
(page_map_cap: cap)
(page_map_ct_slot: cslot_ptr)
(page_map_entries: "pte \<times> (obj_ref list) + pde \<times> (obj_ref list)")
| PageRemap
(page_remap_asid: asid)
(page_remap_entries: "pte \<times> (obj_ref list) + pde \<times> (obj_ref list)")
| PageUnmap
(page_unmap_cap: arch_cap)
(page_unmap_cap_slot: cslot_ptr)

20
spec/abstract/ARM_HYP/Arch_A.thy
View File

@ -123,9 +123,7 @@ where
text \<open>The Page capability confers the authority to map, unmap and flush the
memory page. The remap system call is a convenience operation that ensures the
page is mapped in the same location as this cap was previously used to map it
in.\<close>
memory page.\<close>
definition
perform_page_invocation :: "page_invocation \<Rightarrow> (unit,'z::state_ext) s_monad" where
"perform_page_invocation iv \<equiv> case iv of
@ -149,22 +147,6 @@ perform_page_invocation :: "page_invocation \<Rightarrow> (unit,'z::state_ext) s
if flush then (invalidate_tlb_by_asid asid) else return ()
od
od
| PageRemap asid (Inl (pte, slots)) \<Rightarrow> do
flush \<leftarrow> pte_check_if_mapped (hd slots);
store_pte (hd slots) pte;
mapM_x (swp store_pte InvalidPTE) (tl slots);
do_machine_op $ cleanCacheRange_PoU (hd slots) (last_byte_pte (last slots))
(addrFromPPtr (hd slots));
if flush then (invalidate_tlb_by_asid asid) else return ()
od
| PageRemap asid (Inr (pde, slots)) \<Rightarrow> do
flush \<leftarrow> pde_check_if_mapped (hd slots);
store_pde (hd slots) pde;
mapM_x (swp store_pde InvalidPDE) (tl slots);
do_machine_op $ cleanCacheRange_PoU (hd slots) (last_byte_pde (last slots))
(addrFromPPtr (hd slots));
if flush then (invalidate_tlb_by_asid asid) else return ()
od
| PageUnmap cap ct_slot \<Rightarrow>
(case cap of
PageCap dev p R vp_size vp_mapped_addr \<Rightarrow> do