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

aspec: generate proper kernel reply for PageGetAddr 

The previous spec was trying to set message registers manually
when instead it should have just returned the list of data words
that forms the reply. This correctly modeled the currently wrong
behaviour in C, which seL4/seL4#243 fixes.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2021-08-22 13:42:25 +10:00 committed by Ryan Barry
parent 94da7bca1b
commit 8effcb0e42
4 changed files with 63 additions and 56 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

51
spec/abstract/ARM/Arch_A.thy
View File

@ -121,7 +121,7 @@ where
text \<open>The Page capability confers the authority to map, unmap and flush the text \<open>The Page capability confers the authority to map, unmap and flush the
memory page.\<close> memory page.\<close>
definition definition
perform_page_invocation :: "page_invocation \<Rightarrow> (unit,'z::state_ext) s_monad" where perform_page_invocation :: "page_invocation \<Rightarrow> (data list,'z::state_ext) s_monad" where
"perform_page_invocation iv \<equiv> case iv of "perform_page_invocation iv \<equiv> case iv of
PageMap asid cap ct_slot entries \<Rightarrow> do PageMap asid cap ct_slot entries \<Rightarrow> do
set_cap cap ct_slot; set_cap cap ct_slot;
@ -141,8 +141,9 @@ perform_page_invocation :: "page_invocation \<Rightarrow> (unit,'z::state_ext) s
do_machine_op $ cleanCacheRange_PoU (hd slots) (last_byte_pde (last slots)) do_machine_op $ cleanCacheRange_PoU (hd slots) (last_byte_pde (last slots))
(addrFromPPtr (hd slots)); (addrFromPPtr (hd slots));
if flush then (invalidate_tlb_by_asid asid) else return () if flush then (invalidate_tlb_by_asid asid) else return ()
od od;
od return []
od
| PageUnmap cap ct_slot \<Rightarrow> | PageUnmap cap ct_slot \<Rightarrow>
(case cap of (case cap of
PageCap dev p R vp_size vp_mapped_addr \<Rightarrow> do PageCap dev p R vp_size vp_mapped_addr \<Rightarrow> do
@ -150,10 +151,11 @@ perform_page_invocation :: "page_invocation \<Rightarrow> (unit,'z::state_ext) s
Some (asid, vaddr) \<Rightarrow> unmap_page vp_size asid vaddr p Some (asid, vaddr) \<Rightarrow> unmap_page vp_size asid vaddr p
| None \<Rightarrow> return (); | None \<Rightarrow> return ();
cap \<leftarrow> liftM the_arch_cap $ get_cap ct_slot; cap \<leftarrow> liftM the_arch_cap $ get_cap ct_slot;
set_cap (ArchObjectCap $ update_map_data cap None) ct_slot set_cap (ArchObjectCap $ update_map_data cap None) ct_slot;
return []
od od
| _ \<Rightarrow> fail) | _ \<Rightarrow> fail)
| PageFlush typ start end pstart pd asid \<Rightarrow> | PageFlush typ start end pstart pd asid \<Rightarrow> do
when (start < end) $ do when (start < end) $ do
root_switched \<leftarrow> set_vm_root_for_flush pd asid; root_switched \<leftarrow> set_vm_root_for_flush pd asid;
do_machine_op $ do_flush typ start end pstart; do_machine_op $ do_flush typ start end pstart;
@ -161,12 +163,12 @@ perform_page_invocation :: "page_invocation \<Rightarrow> (unit,'z::state_ext) s
tcb \<leftarrow> gets cur_thread; tcb \<leftarrow> gets cur_thread;
set_vm_root tcb set_vm_root tcb
od od
od od;
| PageGetAddr ptr \<Rightarrow> do return []
ct \<leftarrow> gets cur_thread; od
n_msg \<leftarrow> set_mrs ct None [addrFromPPtr ptr]; | PageGetAddr ptr \<Rightarrow>
set_message_info ct $ MI n_msg 0 0 0 return [addrFromPPtr ptr]
od" "
text \<open>PageTable capabilities confer the authority to map and unmap page text \<open>PageTable capabilities confer the authority to map and unmap page
tables.\<close> tables.\<close>
@ -195,15 +197,26 @@ case iv of PageTableMap cap ct_slot pde pd_slot \<Rightarrow> do
text \<open>Top level system call despatcher for all ARM-specific system calls.\<close> text \<open>Top level system call despatcher for all ARM-specific system calls.\<close>
definition definition
arch_perform_invocation :: "arch_invocation \<Rightarrow> (data list,'z::state_ext) p_monad" where arch_perform_invocation :: "arch_invocation \<Rightarrow> (data list,'z::state_ext) p_monad" where
"arch_perform_invocation i \<equiv> liftE $ do "arch_perform_invocation i \<equiv> liftE $
case i of case i of
InvokePageTable oper \<Rightarrow> perform_page_table_invocation oper InvokePageTable oper \<Rightarrow> do
| InvokePageDirectory oper \<Rightarrow> perform_page_directory_invocation oper perform_page_table_invocation oper;
| InvokePage oper \<Rightarrow> perform_page_invocation oper return []
| InvokeASIDControl oper \<Rightarrow> perform_asid_control_invocation oper od
| InvokeASIDPool oper \<Rightarrow> perform_asid_pool_invocation oper; | InvokePageDirectory oper \<Rightarrow> do
return $ [] perform_page_directory_invocation oper;
od" return []
od
| InvokePage oper \<Rightarrow> perform_page_invocation oper
| InvokeASIDControl oper \<Rightarrow> do
perform_asid_control_invocation oper;
return []
od
| InvokeASIDPool oper \<Rightarrow> do
perform_asid_pool_invocation oper;
return []
od
"
end end

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

@ -122,7 +122,7 @@ where
text \<open>The Page capability confers the authority to map, unmap and flush the text \<open>The Page capability confers the authority to map, unmap and flush the
memory page.\<close> memory page.\<close>
definition definition
perform_page_invocation :: "page_invocation \<Rightarrow> (unit,'z::state_ext) s_monad" where perform_page_invocation :: "page_invocation \<Rightarrow> (data list,'z::state_ext) s_monad" where
"perform_page_invocation iv \<equiv> case iv of "perform_page_invocation iv \<equiv> case iv of
PageMap asid cap ct_slot entries \<Rightarrow> do PageMap asid cap ct_slot entries \<Rightarrow> do
set_cap cap ct_slot; set_cap cap ct_slot;
@ -142,8 +142,9 @@ perform_page_invocation :: "page_invocation \<Rightarrow> (unit,'z::state_ext) s
do_machine_op $ cleanCacheRange_PoU (hd slots) (last_byte_pde (last slots)) do_machine_op $ cleanCacheRange_PoU (hd slots) (last_byte_pde (last slots))
(addrFromPPtr (hd slots)); (addrFromPPtr (hd slots));
if flush then (invalidate_tlb_by_asid asid) else return () if flush then (invalidate_tlb_by_asid asid) else return ()
od od;
od return []
od
| PageUnmap cap ct_slot \<Rightarrow> | PageUnmap cap ct_slot \<Rightarrow>
(case cap of (case cap of
PageCap dev p R vp_size vp_mapped_addr \<Rightarrow> do PageCap dev p R vp_size vp_mapped_addr \<Rightarrow> do
@ -151,10 +152,11 @@ perform_page_invocation :: "page_invocation \<Rightarrow> (unit,'z::state_ext) s
Some (asid, vaddr) \<Rightarrow> unmap_page vp_size asid vaddr p Some (asid, vaddr) \<Rightarrow> unmap_page vp_size asid vaddr p
| None \<Rightarrow> return (); | None \<Rightarrow> return ();
cap \<leftarrow> liftM the_arch_cap $ get_cap ct_slot; cap \<leftarrow> liftM the_arch_cap $ get_cap ct_slot;
set_cap (ArchObjectCap $ update_map_data cap None) ct_slot set_cap (ArchObjectCap $ update_map_data cap None) ct_slot;
return []
od od
| _ \<Rightarrow> fail) | _ \<Rightarrow> fail)
| PageFlush typ start end pstart pd asid \<Rightarrow> | PageFlush typ start end pstart pd asid \<Rightarrow> do
when (start < end) $ do when (start < end) $ do
root_switched \<leftarrow> set_vm_root_for_flush pd asid; root_switched \<leftarrow> set_vm_root_for_flush pd asid;
do_machine_op $ do_flush typ start end pstart; do_machine_op $ do_flush typ start end pstart;
@ -162,12 +164,12 @@ perform_page_invocation :: "page_invocation \<Rightarrow> (unit,'z::state_ext) s
tcb \<leftarrow> gets cur_thread; tcb \<leftarrow> gets cur_thread;
set_vm_root tcb set_vm_root tcb
od od
od od;
| PageGetAddr ptr \<Rightarrow> do return []
ct \<leftarrow> gets cur_thread; od
n_msg \<leftarrow> set_mrs ct None [addrFromPPtr ptr]; | PageGetAddr ptr \<Rightarrow>
set_message_info ct $ MI n_msg 0 0 0 return [addrFromPPtr ptr]
od" "
text \<open>PageTable capabilities confer the authority to map and unmap page text \<open>PageTable capabilities confer the authority to map and unmap page
tables.\<close> tables.\<close>
@ -200,7 +202,7 @@ definition
case i of case i of
InvokePageTable oper \<Rightarrow> do perform_page_table_invocation oper; return [] od InvokePageTable oper \<Rightarrow> do perform_page_table_invocation oper; return [] od
| InvokePageDirectory oper \<Rightarrow> do perform_page_directory_invocation oper; return [] od | InvokePageDirectory oper \<Rightarrow> do perform_page_directory_invocation oper; return [] od
| InvokePage oper \<Rightarrow> do perform_page_invocation oper; return [] od | InvokePage oper \<Rightarrow> perform_page_invocation oper
| InvokeASIDControl oper \<Rightarrow> do perform_asid_control_invocation oper; return [] od | InvokeASIDControl oper \<Rightarrow> do perform_asid_control_invocation oper; return [] od
| InvokeASIDPool oper \<Rightarrow> do perform_asid_pool_invocation oper; return [] od | InvokeASIDPool oper \<Rightarrow> do perform_asid_pool_invocation oper; return [] od
| InvokeVCPU oper \<Rightarrow> perform_vcpu_invocation oper" | InvokeVCPU oper \<Rightarrow> perform_vcpu_invocation oper"

18
spec/abstract/RISCV64/Arch_A.thy
View File

@ -102,22 +102,16 @@ definition perform_pg_inv_map :: "arch_cap \<Rightarrow> cslot_ptr \<Rightarrow>
do_machine_op sfence do_machine_op sfence
od" od"
definition perform_pg_inv_get_addr :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" definition perform_pg_inv_get_addr :: "obj_ref \<Rightarrow> (data list,'z::state_ext) s_monad"
where where
"perform_pg_inv_get_addr ptr \<equiv> do "perform_pg_inv_get_addr ptr \<equiv> return [addrFromPPtr ptr]"
paddr \<leftarrow> return $ fromPAddr $ addrFromPPtr ptr;
ct \<leftarrow> gets cur_thread;
msg_transferred \<leftarrow> set_mrs ct Nothing [paddr];
msg_info \<leftarrow> return $ MI msg_transferred 0 0 0;
set_message_info ct msg_info
od"
text \<open>The Frame capability confers the authority to map and unmap memory.\<close> text \<open>The Frame capability confers the authority to map and unmap memory.\<close>
definition perform_page_invocation :: "page_invocation \<Rightarrow> (unit,'z::state_ext) s_monad" definition perform_page_invocation :: "page_invocation \<Rightarrow> (data list,'z::state_ext) s_monad"
where where
"perform_page_invocation iv \<equiv> case iv of "perform_page_invocation iv \<equiv> case iv of
PageMap cap ct_slot (pte,slot) \<Rightarrow> perform_pg_inv_map cap ct_slot pte slot PageMap cap ct_slot (pte,slot) \<Rightarrow> do perform_pg_inv_map cap ct_slot pte slot; return [] od
| PageUnmap cap ct_slot \<Rightarrow> perform_pg_inv_unmap cap ct_slot | PageUnmap cap ct_slot \<Rightarrow> do perform_pg_inv_unmap cap ct_slot; return [] od
| PageGetAddr ptr \<Rightarrow> perform_pg_inv_get_addr ptr" | PageGetAddr ptr \<Rightarrow> perform_pg_inv_get_addr ptr"
@ -161,7 +155,7 @@ definition arch_perform_invocation :: "arch_invocation \<Rightarrow> (data list,
where where
"arch_perform_invocation i \<equiv> liftE $ case i of "arch_perform_invocation i \<equiv> liftE $ case i of
InvokePageTable oper \<Rightarrow> arch_no_return $ perform_page_table_invocation oper InvokePageTable oper \<Rightarrow> arch_no_return $ perform_page_table_invocation oper
| InvokePage oper \<Rightarrow> arch_no_return $ perform_page_invocation oper | InvokePage oper \<Rightarrow> perform_page_invocation oper
| InvokeASIDControl oper \<Rightarrow> arch_no_return $ perform_asid_control_invocation oper | InvokeASIDControl oper \<Rightarrow> arch_no_return $ perform_asid_control_invocation oper
| InvokeASIDPool oper \<Rightarrow> arch_no_return $ perform_asid_pool_invocation oper" | InvokeASIDPool oper \<Rightarrow> arch_no_return $ perform_asid_pool_invocation oper"

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

@ -133,7 +133,7 @@ where
text \<open>The Page capability confers the authority to map, unmap and flush the text \<open>The Page capability confers the authority to map, unmap and flush the
memory page.\<close> memory page.\<close>
definition definition
perform_page_invocation :: "page_invocation \<Rightarrow> (unit,'z::state_ext) s_monad" where perform_page_invocation :: "page_invocation \<Rightarrow> (data list,'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;
@ -144,25 +144,23 @@ perform_page_invocation :: "page_invocation \<Rightarrow> (unit,'z::state_ext) s
asid \<leftarrow> case cap of asid \<leftarrow> case cap of
ArchObjectCap (PageCap _ _ _ _ _ (Some (as, _))) \<Rightarrow> return as ArchObjectCap (PageCap _ _ _ _ _ (Some (as, _))) \<Rightarrow> return as
| _ \<Rightarrow> fail; | _ \<Rightarrow> fail;
invalidate_page_structure_cache_asid (addrFromPPtr vspace) asid invalidate_page_structure_cache_asid (addrFromPPtr vspace) asid;
return []
od od
| PageUnmap cap ct_slot \<Rightarrow> | PageUnmap cap ct_slot \<Rightarrow>
(case cap of (case cap of
PageCap dev base rights map_type sz mapped \<Rightarrow> PageCap dev base rights map_type sz mapped \<Rightarrow> do
(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 ();
return []
od
| _ \<Rightarrow> fail) | _ \<Rightarrow> fail)
\<^cancel>\<open>| PageIOMap asid cap ct_slot entries \<Rightarrow> undefined\<close> \<^cancel>\<open>| PageIOMap asid cap ct_slot entries \<Rightarrow> undefined\<close>
| PageGetAddr ptr \<Rightarrow> do | PageGetAddr ptr \<Rightarrow>
paddr \<leftarrow> return $ fromPAddr $ addrFromPPtr ptr; return [addrFromPPtr ptr]"
ct \<leftarrow> gets cur_thread;
msg_transferred \<leftarrow> set_mrs ct Nothing [paddr];
msg_info \<leftarrow> return $ MI msg_transferred 0 0 0;
set_message_info ct msg_info
od"
text \<open>PageTable capabilities confer the authority to map and unmap page tables.\<close> text \<open>PageTable capabilities confer the authority to map and unmap page tables.\<close>
definition definition
@ -286,7 +284,7 @@ definition
InvokePageTable oper \<Rightarrow> arch_no_return $ perform_page_table_invocation oper InvokePageTable oper \<Rightarrow> arch_no_return $ perform_page_table_invocation oper
| InvokePageDirectory oper \<Rightarrow> arch_no_return $ perform_page_directory_invocation oper | InvokePageDirectory oper \<Rightarrow> arch_no_return $ perform_page_directory_invocation oper
| InvokePDPT oper \<Rightarrow> arch_no_return $ perform_pdpt_invocation oper | InvokePDPT oper \<Rightarrow> arch_no_return $ perform_pdpt_invocation oper
| InvokePage oper \<Rightarrow> arch_no_return $ perform_page_invocation oper | InvokePage oper \<Rightarrow> perform_page_invocation oper
| InvokeASIDControl oper \<Rightarrow> arch_no_return $ perform_asid_control_invocation oper | InvokeASIDControl oper \<Rightarrow> arch_no_return $ perform_asid_control_invocation oper
| InvokeASIDPool oper \<Rightarrow> arch_no_return $ perform_asid_pool_invocation oper | InvokeASIDPool oper \<Rightarrow> arch_no_return $ perform_asid_pool_invocation oper
| InvokeIOPort oper \<Rightarrow> perform_io_port_invocation oper | InvokeIOPort oper \<Rightarrow> perform_io_port_invocation oper