arch_split: Interrupt_AI [VER-578]
This commit is contained in:
Alejandro Gomez-Londono
parent
50ab074d71
commit
3ef9d3221c
|
|
@ -16,19 +16,191 @@ context Arch begin
|
|||
|
||||
named_theorems Interrupt_AI_asms
|
||||
|
||||
definition "Interrupt_AI_dummy_const \<equiv> (1 :: nat)"
|
||||
lemma (* decode_irq_control_invocation_inv *)[Interrupt_AI_asms]:
|
||||
"\<lbrace>P\<rbrace> decode_irq_control_invocation label args slot caps \<lbrace>\<lambda>rv. P\<rbrace>"
|
||||
apply (simp add: decode_irq_control_invocation_def Let_def arch_check_irq_def
|
||||
arch_decode_irq_control_invocation_def whenE_def, safe)
|
||||
apply (wp | simp)+
|
||||
done
|
||||
|
||||
lemma (* decode_irq_control_valid *)[Interrupt_AI_asms]:
|
||||
"\<lbrace>\<lambda>s. invs s \<and> (\<forall>cap \<in> set caps. s \<turnstile> cap)
|
||||
\<and> (\<forall>cap \<in> set caps. is_cnode_cap cap \<longrightarrow>
|
||||
(\<forall>r \<in> cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s))
|
||||
\<and> cte_wp_at (op = cap.IRQControlCap) slot s\<rbrace>
|
||||
decode_irq_control_invocation label args slot caps
|
||||
\<lbrace>irq_control_inv_valid\<rbrace>,-"
|
||||
apply (simp add: decode_irq_control_invocation_def Let_def split_def
|
||||
whenE_def arch_check_irq_def
|
||||
arch_decode_irq_control_invocation_def
|
||||
split del: split_if cong: if_cong)
|
||||
apply (rule hoare_pre)
|
||||
apply (wp ensure_empty_stronger | simp add: cte_wp_at_eq_simp
|
||||
| wp_once hoare_drop_imps)+
|
||||
apply (clarsimp simp: linorder_not_less word_le_nat_alt unat_ucast
|
||||
maxIRQ_def)
|
||||
apply (cut_tac mod_le[where b = "2^10" and c = "2^16" and a = "unat (args ! 0)" ,simplified])
|
||||
apply (cases caps, auto simp:unat_mask_32_16_is_mod)
|
||||
done
|
||||
|
||||
lemma get_irq_slot_different_ARCH[Interrupt_AI_asms]:
|
||||
"\<lbrace>\<lambda>s. valid_global_refs s \<and> ex_cte_cap_wp_to is_cnode_cap ptr s\<rbrace>
|
||||
get_irq_slot irq
|
||||
\<lbrace>\<lambda>rv s. rv \<noteq> ptr\<rbrace>"
|
||||
apply (simp add: get_irq_slot_def)
|
||||
apply wp
|
||||
apply (clarsimp simp: valid_global_refs_def valid_refs_def
|
||||
ex_cte_cap_wp_to_def)
|
||||
apply (elim allE, erule notE, erule cte_wp_at_weakenE)
|
||||
apply (clarsimp simp: global_refs_def is_cap_simps cap_range_def)
|
||||
done
|
||||
|
||||
lemma is_derived_use_interrupt_ARCH[Interrupt_AI_asms]:
|
||||
"(is_ntfn_cap cap \<and> interrupt_derived cap cap') \<longrightarrow> (is_derived m p cap cap')"
|
||||
apply (clarsimp simp: is_cap_simps)
|
||||
apply (clarsimp simp: interrupt_derived_def is_derived_def)
|
||||
apply (clarsimp simp: cap_master_cap_def split: cap.split_asm)
|
||||
apply (simp add: is_cap_simps is_pt_cap_def vs_cap_ref_def)
|
||||
done
|
||||
|
||||
lemma maskInterrupt_invs_ARCH[Interrupt_AI_asms]:
|
||||
"\<lbrace>invs and (\<lambda>s. \<not>b \<longrightarrow> interrupt_states s irq \<noteq> IRQInactive)\<rbrace>
|
||||
do_machine_op (maskInterrupt b irq)
|
||||
\<lbrace>\<lambda>rv. invs\<rbrace>"
|
||||
apply (simp add: do_machine_op_def split_def maskInterrupt_def)
|
||||
apply wp
|
||||
apply (clarsimp simp: in_monad invs_def valid_state_def all_invs_but_valid_irq_states_for_def
|
||||
valid_irq_states_but_def valid_irq_masks_but_def valid_machine_state_def cur_tcb_def valid_irq_states_def valid_irq_masks_def)
|
||||
done
|
||||
|
||||
lemma Interrupt_AI_trivial_result[Interrupt_AI_asms]:
|
||||
"Interrupt_AI_dummy_const > 0"
|
||||
by (simp add: Interrupt_AI_dummy_const_def)
|
||||
lemma no_cap_to_obj_with_diff_IRQHandler_ARCH[Interrupt_AI_asms]:
|
||||
"no_cap_to_obj_with_diff_ref (IRQHandlerCap irq) S = \<top>"
|
||||
by (rule ext, simp add: no_cap_to_obj_with_diff_ref_def
|
||||
cte_wp_at_caps_of_state
|
||||
obj_ref_none_no_asid)
|
||||
|
||||
lemma (* set_irq_state_valid_cap *)[Interrupt_AI_asms]:
|
||||
"\<lbrace>valid_cap cap\<rbrace> set_irq_state IRQSignal irq \<lbrace>\<lambda>rv. valid_cap cap\<rbrace>"
|
||||
apply (clarsimp simp: set_irq_state_def)
|
||||
apply (wp do_machine_op_valid_cap)
|
||||
apply (auto simp: valid_cap_def valid_untyped_def
|
||||
split: cap.splits option.splits arch_cap.splits
|
||||
split del: split_if)
|
||||
done
|
||||
|
||||
crunch valid_global_refs[Interrupt_AI_asms]: set_irq_state "valid_global_refs"
|
||||
|
||||
lemma invoke_irq_handler_invs'[Interrupt_AI_asms]:
|
||||
assumes dmo_ex_inv[wp]: "\<And>f. \<lbrace>invs and ex_inv\<rbrace> do_machine_op f \<lbrace>\<lambda>rv::unit. ex_inv\<rbrace>"
|
||||
assumes cap_insert_ex_inv[wp]: "\<And>cap src dest.
|
||||
\<lbrace>ex_inv and invs and K (src \<noteq> dest)\<rbrace>
|
||||
cap_insert cap src dest
|
||||
\<lbrace>\<lambda>_.ex_inv\<rbrace>"
|
||||
assumes cap_delete_one_ex_inv[wp]: "\<And>cap.
|
||||
\<lbrace>ex_inv and invs\<rbrace> cap_delete_one cap \<lbrace>\<lambda>_.ex_inv\<rbrace>"
|
||||
shows
|
||||
"\<lbrace>invs and ex_inv and irq_handler_inv_valid i\<rbrace> invoke_irq_handler i \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace>"
|
||||
proof -
|
||||
have
|
||||
cap_insert_invs_ex_invs[wp]: "\<And>cap src dest. \<lbrace>ex_inv and (invs and cte_wp_at (\<lambda>c. c = NullCap) dest and valid_cap cap and
|
||||
tcb_cap_valid cap dest and
|
||||
ex_cte_cap_wp_to (appropriate_cte_cap cap) dest and
|
||||
(\<lambda>s. \<forall>r\<in>obj_refs cap.
|
||||
\<forall>p'. dest \<noteq> p' \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') p' s \<longrightarrow>
|
||||
cte_wp_at (Not \<circ> is_zombie) p' s \<and> \<not> is_zombie cap) and
|
||||
(\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s) and
|
||||
(\<lambda>s. cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs cap - cap_irqs cap'. irq_issued irq s)
|
||||
src s) and
|
||||
(\<lambda>s. \<forall>t. cap = ReplyCap t False \<longrightarrow>
|
||||
st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) and
|
||||
K (\<not> is_master_reply_cap cap))\<rbrace>
|
||||
cap_insert cap src dest \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace>"
|
||||
apply wp
|
||||
apply (auto simp: cte_wp_at_caps_of_state)
|
||||
done
|
||||
show ?thesis
|
||||
apply (cases i, simp_all)
|
||||
apply (wp maskInterrupt_invs_ARCH)
|
||||
apply simp
|
||||
apply simp
|
||||
apply (rename_tac irq cap prod)
|
||||
apply (rule hoare_pre)
|
||||
apply (wp valid_cap_typ [OF cap_delete_one_typ_at])
|
||||
apply (strengthen real_cte_tcb_valid)
|
||||
apply (wp real_cte_at_typ_valid [OF cap_delete_one_typ_at])
|
||||
apply (rule_tac Q="\<lambda>rv s. is_ntfn_cap cap \<and> invs s
|
||||
\<and> cte_wp_at (is_derived (cdt s) prod cap) prod s"
|
||||
in hoare_post_imp)
|
||||
apply (clarsimp simp: is_cap_simps is_derived_def cte_wp_at_caps_of_state)
|
||||
apply (simp split: split_if_asm)
|
||||
apply (simp add: cap_master_cap_def split: cap.split_asm)
|
||||
apply (drule cte_wp_valid_cap [OF caps_of_state_cteD] | clarsimp)+
|
||||
apply (clarsimp simp: cap_master_cap_simps valid_cap_def obj_at_def is_ntfn is_tcb is_cap_table
|
||||
split: option.split_asm dest!:cap_master_cap_eqDs)
|
||||
apply (wp cap_delete_one_still_derived)
|
||||
apply simp
|
||||
apply (wp get_irq_slot_ex_cte get_irq_slot_different_ARCH hoare_drop_imps)
|
||||
apply (clarsimp simp: valid_state_def invs_def appropriate_cte_cap_def
|
||||
is_cap_simps)
|
||||
apply (erule cte_wp_at_weakenE, simp add: is_derived_use_interrupt_ARCH)
|
||||
apply (wp| simp add: )+
|
||||
done
|
||||
qed
|
||||
|
||||
lemma (* invoke_irq_control_invs *) [Interrupt_AI_asms]:
|
||||
"\<lbrace>invs and irq_control_inv_valid i\<rbrace> invoke_irq_control i \<lbrace>\<lambda>rv. invs\<rbrace>"
|
||||
apply (cases i, simp_all)
|
||||
apply (rule hoare_pre)
|
||||
apply (wp cap_insert_simple_invs
|
||||
| simp add: IRQHandler_valid is_cap_simps no_cap_to_obj_with_diff_IRQHandler_ARCH
|
||||
| strengthen real_cte_tcb_valid)+
|
||||
apply (clarsimp simp: cte_wp_at_caps_of_state
|
||||
is_simple_cap_def is_cap_simps is_pt_cap_def
|
||||
safe_parent_for_def
|
||||
ex_cte_cap_to_cnode_always_appropriate_strg)
|
||||
done
|
||||
|
||||
lemma resetTimer_invs_ARCH[Interrupt_AI_asms]:
|
||||
"\<lbrace>invs\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_. invs\<rbrace>"
|
||||
apply (wp dmo_invs)
|
||||
apply safe
|
||||
apply (drule_tac Q="%_ b. underlying_memory b p = underlying_memory m p"
|
||||
in use_valid)
|
||||
apply (simp add: resetTimer_def
|
||||
machine_op_lift_def machine_rest_lift_def split_def)
|
||||
apply wp
|
||||
apply (clarsimp+)[2]
|
||||
apply(erule use_valid, wp no_irq_resetTimer no_irq, assumption)
|
||||
done
|
||||
|
||||
lemma empty_fail_ackInterrupt_ARCH[Interrupt_AI_asms]:
|
||||
"empty_fail (ackInterrupt irq)"
|
||||
by (wp | simp add: ackInterrupt_def)+
|
||||
|
||||
lemma empty_fail_maskInterrupt_ARCH[Interrupt_AI_asms]:
|
||||
"empty_fail (maskInterrupt f irq)"
|
||||
by (wp | simp add: maskInterrupt_def)+
|
||||
|
||||
lemma (* handle_interrupt_invs *) [Interrupt_AI_asms]:
|
||||
"\<lbrace>invs\<rbrace> handle_interrupt irq \<lbrace>\<lambda>_. invs\<rbrace>"
|
||||
apply (simp add: handle_interrupt_def )
|
||||
apply (rule conjI; rule impI)
|
||||
apply (simp add: do_machine_op_bind empty_fail_ackInterrupt_ARCH empty_fail_maskInterrupt_ARCH)
|
||||
apply (wp dmo_maskInterrupt_invs maskInterrupt_invs_ARCH dmo_ackInterrupt | wpc | simp)+
|
||||
apply (wp get_cap_wp send_signal_interrupt_states )
|
||||
apply (rule_tac Q="\<lambda>rv. invs and (\<lambda>s. st = interrupt_states s irq)" in hoare_post_imp)
|
||||
apply (clarsimp simp: ex_nonz_cap_to_def invs_valid_objs)
|
||||
apply (intro allI exI, erule cte_wp_at_weakenE)
|
||||
apply (clarsimp simp: is_cap_simps)
|
||||
apply (wp hoare_drop_imps resetTimer_invs_ARCH | simp add: get_irq_state_def)+
|
||||
done
|
||||
|
||||
end
|
||||
|
||||
interpretation Interrupt_AI?: Interrupt_AI
|
||||
where Interrupt_AI_dummy_const = Arch.Interrupt_AI_dummy_const
|
||||
proof goal_cases
|
||||
interpret Arch .
|
||||
case 1 show ?case by (intro_locales; (unfold_locales, fact Interrupt_AI_asms)?)
|
||||
case 1 show ?case by (intro_locales; (unfold_locales, simp_all add: Interrupt_AI_asms)?)
|
||||
qed
|
||||
|
||||
end
|
||||
|
|
@ -16,14 +16,7 @@ theory Interrupt_AI
|
|||
imports "./$L4V_ARCH/ArchIpc_AI"
|
||||
begin
|
||||
|
||||
locale Interrupt_AI begin
|
||||
|
||||
extend_locale
|
||||
fixes Interrupt_AI_dummy_const :: nat
|
||||
assumes Interrupt_AI_trivial_asm: "Interrupt_AI_dummy_const > 0"
|
||||
|
||||
end
|
||||
|
||||
|
||||
context begin interpretation Arch .
|
||||
requalify_consts
|
||||
maxIRQ
|
||||
|
|
@ -57,6 +50,65 @@ where
|
|||
and ex_cte_cap_wp_to is_cnode_cap ptr and real_cte_at ptr
|
||||
and K (irq \<le> maxIRQ))"
|
||||
|
||||
locale Interrupt_AI =
|
||||
fixes state_ext_type1 :: "('a :: state_ext) itself"
|
||||
assumes decode_irq_control_invocation_inv[wp]:
|
||||
"\<And>(P :: 'a state \<Rightarrow> bool) args slot label caps.
|
||||
\<lbrace>P\<rbrace> decode_irq_control_invocation label args slot caps \<lbrace>\<lambda>rv. P\<rbrace>"
|
||||
assumes decode_irq_control_valid[wp]:
|
||||
"\<And>slot caps label args.
|
||||
\<lbrace>\<lambda>s :: 'a state. invs s \<and> (\<forall>cap \<in> set caps. s \<turnstile> cap)
|
||||
\<and> (\<forall>cap \<in> set caps. is_cnode_cap cap \<longrightarrow>
|
||||
(\<forall>r \<in> cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s))
|
||||
\<and> cte_wp_at (op = cap.IRQControlCap) slot s\<rbrace>
|
||||
decode_irq_control_invocation label args slot caps
|
||||
\<lbrace>irq_control_inv_valid\<rbrace>,-"
|
||||
assumes get_irq_slot_different:
|
||||
"\<And> irq ptr.
|
||||
\<lbrace>\<lambda>s :: 'a state. valid_global_refs s \<and> ex_cte_cap_wp_to is_cnode_cap ptr s\<rbrace>
|
||||
get_irq_slot irq
|
||||
\<lbrace>\<lambda>rv s. rv \<noteq> ptr\<rbrace>"
|
||||
assumes is_derived_use_interrupt:
|
||||
"\<And> cap cap' m p.
|
||||
(is_ntfn_cap cap \<and> interrupt_derived cap cap') \<longrightarrow> (is_derived m p cap cap')"
|
||||
assumes maskInterrupt_invs:
|
||||
"\<And>b irq.
|
||||
\<lbrace>invs and (\<lambda>s :: 'a state. \<not>b \<longrightarrow> interrupt_states s irq \<noteq> IRQInactive)\<rbrace>
|
||||
do_machine_op (maskInterrupt b irq)
|
||||
\<lbrace>\<lambda>rv. invs\<rbrace>"
|
||||
assumes no_cap_to_obj_with_diff_IRQHandler[simp]:
|
||||
"\<And> irq S. (no_cap_to_obj_with_diff_ref (IRQHandlerCap irq) S :: 'a state \<Rightarrow> bool)= \<top>"
|
||||
assumes set_irq_state_valid_cap[wp]:
|
||||
"\<And> cap irq.
|
||||
\<lbrace>valid_cap cap :: 'a state \<Rightarrow> bool\<rbrace>
|
||||
set_irq_state IRQSignal irq
|
||||
\<lbrace>\<lambda>rv. valid_cap cap\<rbrace>"
|
||||
assumes set_irq_state_valid_global_refs[wp]:
|
||||
"\<And> a b.
|
||||
\<lbrace>valid_global_refs :: 'a state \<Rightarrow> bool\<rbrace>
|
||||
set_irq_state a b
|
||||
\<lbrace>\<lambda>_. valid_global_refs\<rbrace>"
|
||||
assumes invoke_irq_handler_invs':
|
||||
"\<And> (ex_inv :: 'a state \<Rightarrow> bool) i.
|
||||
\<lbrakk> \<And>f. \<lbrace>invs and ex_inv\<rbrace> do_machine_op f \<lbrace>\<lambda>rv::unit. ex_inv\<rbrace>;
|
||||
\<And>cap src dest.
|
||||
\<lbrace>ex_inv and invs and K (src \<noteq> dest)\<rbrace>
|
||||
cap_insert cap src dest
|
||||
\<lbrace>\<lambda>_.ex_inv\<rbrace>;
|
||||
\<And>cap. \<lbrace>ex_inv and invs\<rbrace> cap_delete_one cap \<lbrace>\<lambda>_.ex_inv\<rbrace>
|
||||
\<rbrakk> \<Longrightarrow>
|
||||
\<lbrace>invs and ex_inv and irq_handler_inv_valid i\<rbrace> invoke_irq_handler i \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace>"
|
||||
assumes invoke_irq_control_invs[wp]:
|
||||
"\<And> i. \<lbrace>invs and irq_control_inv_valid i\<rbrace> invoke_irq_control i \<lbrace>\<lambda>rv. invs :: 'a state \<Rightarrow> bool\<rbrace>"
|
||||
assumes resetTimer_invs[wp]:
|
||||
"\<lbrace>invs :: 'a state \<Rightarrow> bool\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_. invs\<rbrace>"
|
||||
assumes empty_fail_ackInterrupt[simp, intro!]:
|
||||
"\<And> irq. empty_fail (ackInterrupt irq)"
|
||||
assumes empty_fail_maskInterrupt[simp, intro!]:
|
||||
"\<And> f irq. empty_fail (maskInterrupt f irq)"
|
||||
assumes handle_interrupt_invs [wp]:
|
||||
"\<And> irq. \<lbrace>invs :: 'a state \<Rightarrow> bool\<rbrace> handle_interrupt irq \<lbrace>\<lambda>_. invs\<rbrace>"
|
||||
|
||||
crunch inv[wp]: decode_irq_handler_invocation "P"
|
||||
(simp: crunch_simps)
|
||||
|
||||
|
|
@ -82,15 +134,6 @@ lemma decode_irq_handler_valid[wp]:
|
|||
|
||||
crunch inv[wp]: is_irq_active "P"
|
||||
|
||||
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||
lemma decode_irq_control_invocation_inv[wp]:
|
||||
"\<lbrace>P\<rbrace> decode_irq_control_invocation label args slot caps \<lbrace>\<lambda>rv. P\<rbrace>"
|
||||
apply (simp add: decode_irq_control_invocation_def Let_def arch_check_irq_def
|
||||
arch_decode_irq_control_invocation_def whenE_def, safe)
|
||||
apply (wp | simp)+
|
||||
done
|
||||
end
|
||||
|
||||
lemma unat_mask_32_16_is_mod:
|
||||
"unat ((a::word32) && mask 16) = (unat a) mod (2^16)"
|
||||
by (simp add:word_mod_2p_is_mask[symmetric] unat_word_ariths)
|
||||
|
|
@ -100,42 +143,6 @@ lemma mod_le:
|
|||
apply (subst mod_mod_cancel[symmetric],simp)
|
||||
by simp
|
||||
|
||||
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||
|
||||
lemma decode_irq_control_valid[wp]:
|
||||
"\<lbrace>\<lambda>s. invs s \<and> (\<forall>cap \<in> set caps. s \<turnstile> cap)
|
||||
\<and> (\<forall>cap \<in> set caps. is_cnode_cap cap \<longrightarrow>
|
||||
(\<forall>r \<in> cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s))
|
||||
\<and> cte_wp_at (op = cap.IRQControlCap) slot s\<rbrace>
|
||||
decode_irq_control_invocation label args slot caps
|
||||
\<lbrace>irq_control_inv_valid\<rbrace>,-"
|
||||
apply (simp add: decode_irq_control_invocation_def Let_def split_def
|
||||
whenE_def arch_check_irq_def
|
||||
arch_decode_irq_control_invocation_def
|
||||
split del: split_if cong: if_cong)
|
||||
apply (rule hoare_pre)
|
||||
apply (wp ensure_empty_stronger | simp add: cte_wp_at_eq_simp
|
||||
| wp_once hoare_drop_imps)+
|
||||
apply (clarsimp simp: linorder_not_less word_le_nat_alt unat_ucast
|
||||
maxIRQ_def)
|
||||
apply (cut_tac mod_le[where b = "2^10" and c = "2^16" and a = "unat (args ! 0)" ,simplified])
|
||||
apply (cases caps, auto simp:unat_mask_32_16_is_mod)
|
||||
done
|
||||
|
||||
lemma get_irq_slot_different:
|
||||
"\<lbrace>\<lambda>s. valid_global_refs s \<and> ex_cte_cap_wp_to is_cnode_cap ptr s\<rbrace>
|
||||
get_irq_slot irq
|
||||
\<lbrace>\<lambda>rv s. rv \<noteq> ptr\<rbrace>"
|
||||
apply (simp add: get_irq_slot_def)
|
||||
apply wp
|
||||
apply (clarsimp simp: valid_global_refs_def valid_refs_def
|
||||
ex_cte_cap_wp_to_def)
|
||||
apply (elim allE, erule notE, erule cte_wp_at_weakenE)
|
||||
apply (clarsimp simp: global_refs_def is_cap_simps cap_range_def)
|
||||
done
|
||||
|
||||
end
|
||||
|
||||
lemma is_up_8_32: "is_up (ucast :: word8 \<Rightarrow> word32)"
|
||||
by (simp add: is_up_def source_size_def target_size_def word_size)
|
||||
|
||||
|
|
@ -182,17 +189,6 @@ lemma cap_delete_one_still_derived:
|
|||
apply auto
|
||||
done
|
||||
|
||||
|
||||
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||
lemma is_derived_use_interrupt:
|
||||
"(is_ntfn_cap cap \<and> interrupt_derived cap cap') \<longrightarrow> (is_derived m p cap cap')"
|
||||
apply (clarsimp simp: is_cap_simps)
|
||||
apply (clarsimp simp: interrupt_derived_def is_derived_def)
|
||||
apply (clarsimp simp: cap_master_cap_def split: cap.split_asm)
|
||||
apply (simp add: is_cap_simps is_pt_cap_def vs_cap_ref_def)
|
||||
done (* FIXME: arch_split *)
|
||||
end
|
||||
|
||||
lemma cap_delete_one_cte_cap_to[wp]:
|
||||
"\<lbrace>ex_cte_cap_wp_to P ptr\<rbrace> cap_delete_one ptr' \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P ptr\<rbrace>"
|
||||
apply (simp add: ex_cte_cap_wp_to_def)
|
||||
|
|
@ -214,18 +210,6 @@ lemma get_irq_slot_ex_cte:
|
|||
apply clarsimp
|
||||
done
|
||||
|
||||
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||
lemma maskInterrupt_invs:
|
||||
"\<lbrace>invs and (\<lambda>s. \<not>b \<longrightarrow> interrupt_states s irq \<noteq> IRQInactive)\<rbrace>
|
||||
do_machine_op (maskInterrupt b irq)
|
||||
\<lbrace>\<lambda>rv. invs\<rbrace>"
|
||||
apply (simp add: do_machine_op_def split_def maskInterrupt_def)
|
||||
apply wp
|
||||
apply (clarsimp simp: in_monad invs_def valid_state_def all_invs_but_valid_irq_states_for_def
|
||||
valid_irq_states_but_def valid_irq_masks_but_def valid_machine_state_def cur_tcb_def valid_irq_states_def valid_irq_masks_def)
|
||||
done
|
||||
end
|
||||
|
||||
crunch pspace_aligned[wp]: set_irq_state "pspace_aligned"
|
||||
|
||||
crunch pspace_distinct[wp]: set_irq_state "pspace_distinct"
|
||||
|
|
@ -253,111 +237,12 @@ lemma IRQHandler_valid:
|
|||
"(s \<turnstile> cap.IRQHandlerCap irq) = (irq \<le> maxIRQ)"
|
||||
by (simp add: valid_cap_def cap_aligned_def word_bits_conv)
|
||||
|
||||
|
||||
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||
|
||||
lemma no_cap_to_obj_with_diff_IRQHandler[simp]:
|
||||
"no_cap_to_obj_with_diff_ref (IRQHandlerCap irq) S = \<top>"
|
||||
by (rule ext, simp add: no_cap_to_obj_with_diff_ref_def
|
||||
cte_wp_at_caps_of_state
|
||||
obj_ref_none_no_asid)
|
||||
lemma set_irq_state_valid_cap[wp]:
|
||||
"\<lbrace>valid_cap cap\<rbrace> set_irq_state IRQSignal irq \<lbrace>\<lambda>rv. valid_cap cap\<rbrace>"
|
||||
apply (clarsimp simp: set_irq_state_def)
|
||||
apply (wp do_machine_op_valid_cap)
|
||||
apply (auto simp: valid_cap_def valid_untyped_def
|
||||
split: cap.splits option.splits arch_cap.splits
|
||||
split del: split_if)
|
||||
done
|
||||
|
||||
crunch valid_global_refs[wp]: set_irq_state "valid_global_refs"
|
||||
|
||||
lemma invoke_irq_handler_invs':
|
||||
assumes dmo_ex_inv[wp]: "\<And>f. \<lbrace>invs and ex_inv\<rbrace> do_machine_op f \<lbrace>\<lambda>rv::unit. ex_inv\<rbrace>"
|
||||
assumes cap_insert_ex_inv[wp]: "\<And>cap src dest.
|
||||
\<lbrace>ex_inv and invs and K (src \<noteq> dest)\<rbrace>
|
||||
cap_insert cap src dest
|
||||
\<lbrace>\<lambda>_.ex_inv\<rbrace>"
|
||||
assumes cap_delete_one_ex_inv[wp]: "\<And>cap.
|
||||
\<lbrace>ex_inv and invs\<rbrace> cap_delete_one cap \<lbrace>\<lambda>_.ex_inv\<rbrace>"
|
||||
shows
|
||||
"\<lbrace>invs and ex_inv and irq_handler_inv_valid i\<rbrace> invoke_irq_handler i \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace>"
|
||||
proof -
|
||||
have
|
||||
cap_insert_invs_ex_invs[wp]: "\<And>cap src dest. \<lbrace>ex_inv and (invs and cte_wp_at (\<lambda>c. c = NullCap) dest and valid_cap cap and
|
||||
tcb_cap_valid cap dest and
|
||||
ex_cte_cap_wp_to (appropriate_cte_cap cap) dest and
|
||||
(\<lambda>s. \<forall>r\<in>obj_refs cap.
|
||||
\<forall>p'. dest \<noteq> p' \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') p' s \<longrightarrow>
|
||||
cte_wp_at (Not \<circ> is_zombie) p' s \<and> \<not> is_zombie cap) and
|
||||
(\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s) and
|
||||
(\<lambda>s. cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs cap - cap_irqs cap'. irq_issued irq s)
|
||||
src s) and
|
||||
(\<lambda>s. \<forall>t. cap = ReplyCap t False \<longrightarrow>
|
||||
st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) and
|
||||
K (\<not> is_master_reply_cap cap))\<rbrace>
|
||||
cap_insert cap src dest \<lbrace>\<lambda>rv s. invs s \<and> ex_inv s\<rbrace>"
|
||||
apply wp
|
||||
apply (auto simp: cte_wp_at_caps_of_state)
|
||||
done
|
||||
show ?thesis
|
||||
apply (cases i, simp_all)
|
||||
apply (wp maskInterrupt_invs)
|
||||
apply simp
|
||||
apply simp
|
||||
apply (rename_tac irq cap prod)
|
||||
apply (rule hoare_pre)
|
||||
apply (wp valid_cap_typ [OF cap_delete_one_typ_at])
|
||||
apply (strengthen real_cte_tcb_valid)
|
||||
apply (wp real_cte_at_typ_valid [OF cap_delete_one_typ_at])
|
||||
apply (rule_tac Q="\<lambda>rv s. is_ntfn_cap cap \<and> invs s
|
||||
\<and> cte_wp_at (is_derived (cdt s) prod cap) prod s"
|
||||
in hoare_post_imp)
|
||||
apply (clarsimp simp: is_cap_simps is_derived_def cte_wp_at_caps_of_state)
|
||||
apply (simp split: split_if_asm)
|
||||
apply (simp add: cap_master_cap_def split: cap.split_asm)
|
||||
apply (drule cte_wp_valid_cap [OF caps_of_state_cteD] | clarsimp)+
|
||||
apply (clarsimp simp: cap_master_cap_simps valid_cap_def obj_at_def is_ntfn is_tcb is_cap_table
|
||||
split: option.split_asm dest!:cap_master_cap_eqDs)
|
||||
apply (wp cap_delete_one_still_derived)
|
||||
apply simp
|
||||
apply (wp get_irq_slot_ex_cte get_irq_slot_different hoare_drop_imps)
|
||||
apply (clarsimp simp: valid_state_def invs_def appropriate_cte_cap_def
|
||||
is_cap_simps)
|
||||
apply (erule cte_wp_at_weakenE, simp add: is_derived_use_interrupt)
|
||||
apply (wp| simp add: )+
|
||||
done
|
||||
qed
|
||||
|
||||
lemmas invoke_irq_handler_invs[wp] = invoke_irq_handler_invs'[where ex_inv=\<top>, simplified hoare_post_taut, OF TrueI TrueI TrueI,simplified]
|
||||
|
||||
lemma invoke_irq_control_invs[wp]:
|
||||
"\<lbrace>invs and irq_control_inv_valid i\<rbrace> invoke_irq_control i \<lbrace>\<lambda>rv. invs\<rbrace>"
|
||||
apply (cases i, simp_all)
|
||||
apply (rule hoare_pre)
|
||||
apply (wp cap_insert_simple_invs
|
||||
| simp add: IRQHandler_valid is_cap_simps
|
||||
| strengthen real_cte_tcb_valid)+
|
||||
apply (clarsimp simp: cte_wp_at_caps_of_state
|
||||
is_simple_cap_def is_cap_simps is_pt_cap_def
|
||||
safe_parent_for_def
|
||||
ex_cte_cap_to_cnode_always_appropriate_strg)
|
||||
done
|
||||
|
||||
lemma resetTimer_invs[wp]:
|
||||
"\<lbrace>invs\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_. invs\<rbrace>"
|
||||
apply (wp dmo_invs)
|
||||
apply safe
|
||||
apply (drule_tac Q="%_ b. underlying_memory b p = underlying_memory m p"
|
||||
in use_valid)
|
||||
apply (simp add: resetTimer_def
|
||||
machine_op_lift_def machine_rest_lift_def split_def)
|
||||
apply wp
|
||||
apply (clarsimp+)[2]
|
||||
apply(erule use_valid, wp no_irq_resetTimer no_irq, assumption)
|
||||
done
|
||||
|
||||
end
|
||||
lemmas (in Interrupt_AI)
|
||||
invoke_irq_handler_invs[wp] = invoke_irq_handler_invs'[where ex_inv=\<top>
|
||||
, simplified hoare_post_taut
|
||||
, OF TrueI TrueI TrueI
|
||||
, simplified
|
||||
]
|
||||
|
||||
crunch interrupt_states[wp]: update_waiting_ntfn, cancel_signal, blocked_cancel_ipc "\<lambda>s. P (interrupt_states s)" (wp: mapM_x_wp_inv)
|
||||
|
||||
|
|
@ -385,26 +270,5 @@ lemma send_signal_interrupt_states[wp_unsafe]:
|
|||
apply (auto simp: pred_tcb_at_def obj_at_def receive_blocked_def)
|
||||
done
|
||||
|
||||
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||
lemma empty_fail_ackInterrupt[simp, intro!]: "empty_fail (ackInterrupt irq)"
|
||||
by (wp | simp add: ackInterrupt_def)+
|
||||
|
||||
lemma empty_fail_maskInterrupt[simp, intro!]: "empty_fail (maskInterrupt f irq)"
|
||||
by (wp | simp add: maskInterrupt_def)+
|
||||
|
||||
lemma handle_interrupt_invs[wp]:
|
||||
"\<lbrace>invs\<rbrace> handle_interrupt irq \<lbrace>\<lambda>_. invs\<rbrace>"
|
||||
apply (simp add: handle_interrupt_def )
|
||||
apply (rule conjI; rule impI)
|
||||
apply (simp add: do_machine_op_bind)
|
||||
apply (wp dmo_maskInterrupt_invs maskInterrupt_invs dmo_ackInterrupt | wpc | simp)+
|
||||
apply (wp get_cap_wp send_signal_interrupt_states )
|
||||
apply (rule_tac Q="\<lambda>rv. invs and (\<lambda>s. st = interrupt_states s irq)" in hoare_post_imp)
|
||||
apply (clarsimp simp: ex_nonz_cap_to_def invs_valid_objs)
|
||||
apply (intro allI exI, erule cte_wp_at_weakenE)
|
||||
apply (clarsimp simp: is_cap_simps)
|
||||
apply (wp hoare_drop_imps | simp add: get_irq_state_def)+
|
||||
done
|
||||
end
|
||||
|
||||
|
||||
end
|
||||
|
|
|
|||
Loading…
Reference in New Issue