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

x64: spec+refine: plumb call through perform_ioport_invocation

This commit is contained in:
Joel Beeren 2018-05-23 11:16:01 +10:00
parent 648938513f
commit df1c4b1e45
3 changed files with 60 additions and 69 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

76
proof/refine/X64/Arch_R.thy
View File

@ -1465,27 +1465,22 @@ lemma corresK_machine_op[corresK]: "corres_underlyingK Id False True F r P Q x x
by (erule corres_machine_op)
lemma port_in_corres[corres]:
"no_fail \<top> a \<Longrightarrow> corres dc (einvs and ct_active) (invs' and ct_active') (port_in a) (portIn a)"
"no_fail \<top> a \<Longrightarrow> corres (op =) \<top> \<top> (port_in a) (portIn a)"
apply (clarsimp simp: port_in_def portIn_def)
apply (rule corres_guard_imp)
apply (rule corres_split_eqr[OF _ gct_corres])
apply (rule corres_split_eqr)
apply (rule corres_split_eqr[OF set_mi_corres set_mrs_corres])
apply wpsimp+
apply (rule corres_machine_op[OF corres_Id], simp+)
apply wpsimp+
done
apply (rule corres_split_eqr)
apply wpsimp
apply (rule corres_machine_op[OF corres_Id], simp+)
by wpsimp+
lemma port_out_corres[@lift_corres_args, corres]:
"no_fail \<top> (a w) \<Longrightarrow> corres dc (einvs and ct_active) (invs' and ct_active')
(port_out a w) (portOut a w)"
"no_fail \<top> (a w) \<Longrightarrow> corres (op =) \<top> \<top> (port_out a w) (portOut a w)"
apply (clarsimp simp: port_out_def portOut_def)
apply (rule corres_guard_imp)
apply (rule corres_split_eqr[OF _ gct_corres])
apply (rule corres_split_eqr[OF set_mi_corres])
apply wpsimp+
apply (rule corres_machine_op[OF corres_Id], simp+)
apply wpsimp+
apply (rule corres_split_eqr)
apply wpsimp
apply (rule corres_machine_op[OF corres_Id], simp+)
apply wpsimp+
done
(* FIXME x64: move *)
@ -1518,7 +1513,7 @@ lemma perform_port_inv_corres:
\<Longrightarrow> corres (intr \<oplus> (op =))
(einvs and ct_active and valid_arch_inv ai)
(invs' and ct_active' and valid_arch_inv' ai')
(liftE (do perform_io_port_invocation x; return [] od))
(liftE (perform_io_port_invocation x))
(performX64PortInvocation ai')"
apply (clarsimp simp: perform_io_port_invocation_def performX64PortInvocation_def
archinv_relation_def ioport_invocation_map_def)
@ -1619,38 +1614,45 @@ lemma inv_arch_corres:
apply (subst arch_ioport_inv_case_simp; simp)
apply (clarsimp simp: archinv_relation_def)
apply (clarsimp simp: performX64MMUInvocation_def)
apply (rule corres_split' [where r'=dc])
prefer 2
apply (rule corres_trivial)
apply simp
apply (cases ai)
apply (clarsimp simp: archinv_relation_def performX64MMUInvocation_def)
apply (erule corres_guard_imp [OF perform_page_table_corres])
apply (fastforce simp: valid_arch_inv_def)
apply (fastforce simp: valid_arch_inv'_def)
apply (clarsimp simp: archinv_relation_def)
apply (erule corres_guard_imp [OF perform_page_directory_corres])
apply (fastforce simp: valid_arch_inv_def)
apply (fastforce simp: valid_arch_inv'_def)
apply (clarsimp simp: archinv_relation_def)
apply (erule corres_guard_imp [OF perform_pdpt_corres])
apply (cases ai)
apply (clarsimp simp: archinv_relation_def performX64MMUInvocation_def)
apply (rule corres_guard_imp, rule corres_split_nor, rule corres_trivial, simp)
apply (rule perform_page_table_corres; wpsimp)
apply wpsimp+
apply (fastforce simp: valid_arch_inv_def)
apply (fastforce simp: valid_arch_inv'_def)
apply (clarsimp simp: archinv_relation_def)
apply (erule corres_guard_imp [OF perform_page_corres])
apply (rule corres_guard_imp, rule corres_split_nor, rule corres_trivial, simp)
apply (rule perform_page_directory_corres; wpsimp)
apply wpsimp+
apply (fastforce simp: valid_arch_inv_def)
apply (fastforce simp: valid_arch_inv'_def)
apply (clarsimp simp: archinv_relation_def)
apply (rule corres_guard_imp [OF pac_corres], rule refl)
apply (rule corres_guard_imp, rule corres_split_nor, rule corres_trivial, simp)
apply (rule perform_pdpt_corres; wpsimp)
apply wpsimp+
apply (fastforce simp: valid_arch_inv_def)
apply (fastforce simp: valid_arch_inv'_def)
apply (clarsimp simp: archinv_relation_def)
apply (rule corres_guard_imp [OF pap_corres], rule refl)
apply (rule corres_guard_imp, rule corres_split_nor, rule corres_trivial, simp)
apply (rule perform_page_corres; wpsimp)
apply wpsimp+
apply (fastforce simp: valid_arch_inv_def)
apply (fastforce simp: valid_arch_inv'_def)
apply clarsimp
apply clarsimp
apply wp+
apply (clarsimp simp: archinv_relation_def)
apply (rule corres_guard_imp, rule corres_split_nor, rule corres_trivial, simp)
apply (rule pac_corres; wpsimp)
apply wpsimp+
apply (fastforce simp: valid_arch_inv_def)
apply (fastforce simp: valid_arch_inv'_def)
apply (clarsimp simp: archinv_relation_def)
apply (rule corres_guard_imp, rule corres_split_nor, rule corres_trivial, simp)
apply (rule pap_corres; wpsimp)
apply wpsimp+
apply (fastforce simp: valid_arch_inv_def)
apply (fastforce simp: valid_arch_inv'_def)
apply clarsimp
apply clarsimp
done
lemma asid_pool_typ_at_ext':

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

@ -251,25 +251,21 @@ case iv of PDPTMap cap ct_slot pml4e pml4_slot vspace \<Rightarrow> do
| _ \<Rightarrow> fail"
definition
port_out :: "('a word \<Rightarrow> unit machine_monad) \<Rightarrow> ('a word) \<Rightarrow> (unit,'z::state_ext) s_monad" where
port_out :: "('a word \<Rightarrow> unit machine_monad) \<Rightarrow> ('a word) \<Rightarrow> (data list,'z::state_ext) s_monad" where
"port_out f w = do
ct \<leftarrow> gets cur_thread;
do_machine_op $ f w;
set_message_info ct $ MI 0 0 0 0
return []
od"
definition
port_in :: "(data machine_monad) \<Rightarrow> (unit,'z::state_ext) s_monad" where
port_in :: "(data machine_monad) \<Rightarrow> (data list,'z::state_ext) s_monad" where
"port_in f = do
ct \<leftarrow> gets cur_thread;
res \<leftarrow> do_machine_op f;
set_mrs ct None [res];
msg_info \<leftarrow> return $ MI 1 0 0 0;
set_message_info ct msg_info
return [res]
od"
definition
perform_io_port_invocation :: "io_port_invocation \<Rightarrow> (unit,'z::state_ext) s_monad" where
perform_io_port_invocation :: "io_port_invocation \<Rightarrow> (data list,'z::state_ext) s_monad" where
"perform_io_port_invocation i \<equiv> (
case i of (IOPortInvocation port port_data) \<Rightarrow> (
case port_data of
@ -292,21 +288,24 @@ where
cap_insert (ArchObjectCap (IOPortCap f l)) control_slot dest_slot
od"
abbreviation
arch_no_return :: "(unit, 'z::state_ext) s_monad \<Rightarrow> (data list, 'z::state_ext) s_monad"
where
"arch_no_return oper \<equiv> do oper; return [] od"
text {* Top level system call despatcher for all x64-specific system calls. *}
definition
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
InvokePageTable oper \<Rightarrow> perform_page_table_invocation oper
| InvokePageDirectory oper \<Rightarrow> perform_page_directory_invocation oper
| InvokePDPT oper \<Rightarrow> perform_pdpt_invocation oper
| InvokePage oper \<Rightarrow> perform_page_invocation oper
| InvokeASIDControl oper \<Rightarrow> perform_asid_control_invocation oper
| InvokeASIDPool oper \<Rightarrow> perform_asid_pool_invocation oper
InvokePageTable oper \<Rightarrow> arch_no_return $ perform_page_table_invocation oper
| InvokePageDirectory oper \<Rightarrow> arch_no_return $ perform_page_directory_invocation oper
| InvokePDPT oper \<Rightarrow> arch_no_return $ perform_pdpt_invocation oper
| InvokePage oper \<Rightarrow> arch_no_return $ perform_page_invocation oper
| InvokeASIDControl oper \<Rightarrow> arch_no_return $ perform_asid_control_invocation oper
| InvokeASIDPool oper \<Rightarrow> arch_no_return $ perform_asid_pool_invocation oper
| InvokeIOPort oper \<Rightarrow> perform_io_port_invocation oper
| InvokeIOPortControl oper \<Rightarrow> perform_ioport_control_invocation oper;
return $ []
od"
| InvokeIOPortControl oper \<Rightarrow> arch_no_return $ perform_ioport_control_invocation oper"
end
end

16
spec/haskell/src/SEL4/Object/IOPort/X64.lhs
View File

@ -115,25 +115,16 @@ This module defines IO port routines, specific to x64.
> decodeX64PortInvocation _ _ _ _ _ = fail "Unreachable"
> portIn f = do
> ct <- getCurThread
> res <- doMachineOp $ f
> setMRs ct Nothing [res]
> msgInfo <- return $ MI {
> msgLength = 1,
> msgExtraCaps = 0,
> msgCapsUnwrapped = 0,
> msgLabel = 0 }
> setMessageInfo ct msgInfo
> return [res]
> portOut f w = do
> ct <- getCurThread
> doMachineOp $ f w
> setMessageInfo ct $ MI 0 0 0 0
> return []
>
> performX64PortInvocation :: ArchInv.Invocation -> KernelP [Word]
> performX64PortInvocation (InvokeIOPort (IOPortInvocation port port_data)) = withoutPreemption $ do
> performX64PortInvocation (InvokeIOPort (IOPortInvocation port port_data)) = withoutPreemption $
> case port_data of
> ArchInv.IOPortIn8 -> portIn $ in8 port
> ArchInv.IOPortIn16 -> portIn $ in16 port
@ -141,7 +132,6 @@ This module defines IO port routines, specific to x64.
> ArchInv.IOPortOut8 w -> portOut (out8 port) w
> ArchInv.IOPortOut16 w -> portOut (out16 port) w
> ArchInv.IOPortOut32 w -> portOut (out32 port) w
> return $ []
> performX64PortInvocation (InvokeIOPortControl (IOPortControlIssue f l destSlot srcSlot)) =
> withoutPreemption $ do