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

SELFOUR-420: Verification of maxIRQ check in handle_interrupt.

This commit is contained in:
Sophie Taylor 2016-02-09 13:34:35 +11:00 committed by Sophie Taylor
parent ff270121c9
commit d7fd88727a
20 changed files with 421 additions and 169 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
proof/access-control/Syscall_AC.thy
View File

@ -491,7 +491,7 @@ lemma handle_interrupt_pas_refined:
handle_interrupt irq
\<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
apply (simp add: handle_interrupt_def)
apply (rule hoare_pre)
apply (rule conjI; rule impI;rule hoare_pre)
apply (wp send_signal_pas_refined get_cap_wp
| wpc
| simp add: get_irq_slot_def get_irq_state_def)+
@ -522,7 +522,7 @@ lemma handle_interrupt_integrity_autarch:
handle_interrupt irq
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
apply (simp add: handle_interrupt_def cong: irq_state.case_cong maskInterrupt_def ackInterrupt_def resetTimer_def )
apply (rule hoare_pre)
apply (rule conjI; rule impI; rule hoare_pre)
apply (wp_once send_signal_respects get_cap_auth_wp [where aag = aag] dmo_mol_respects
| simp add: get_irq_slot_def get_irq_state_def ackInterrupt_def resetTimer_def
| wp dmo_no_mem_respects
@ -546,7 +546,7 @@ lemma handle_interrupt_integrity:
handle_interrupt irq
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
apply (simp add: handle_interrupt_def maskInterrupt_def ackInterrupt_def resetTimer_def cong: irq_state.case_cong bind_cong)
apply (rule hoare_pre)
apply (rule conjI; rule impI; rule hoare_pre)
apply (wp_once send_signal_respects get_cap_wp dmo_mol_respects dmo_no_mem_respects
| wpc
| simp add: get_irq_slot_def get_irq_state_def ackInterrupt_def resetTimer_def)+
@ -958,6 +958,7 @@ lemma schedule_pas_refined:
lemma handle_interrupt_arch_state [wp]:
"\<lbrace>\<lambda>s :: det_ext state. P (arch_state s)\<rbrace> handle_interrupt irq \<lbrace>\<lambda>_ s. P (arch_state s)\<rbrace>"
unfolding handle_interrupt_def
apply (rule hoare_if)
apply (rule hoare_pre)
apply clarsimp
apply (wp get_cap_inv dxo_wp_weak send_signal_arch_state | wpc | simp add: get_irq_state_def)+

220
proof/crefine/Syscall_C.thy
View File

@ -1625,14 +1625,171 @@ lemma ucast_eq_0[OF refl]:
apply (drule inj_eq[where x=x and y=0], simp)
done
lemma is_up_compose':
fixes uc :: "('a::len) word \<Rightarrow> ('b::len) word"
and uc' :: "'b word \<Rightarrow> ('c::len) sword"
shows
"\<lbrakk>is_up uc; is_up uc'\<rbrakk> \<Longrightarrow> is_up (uc' \<circ> uc)"
unfolding is_up_def by (simp add: Word.target_size Word.source_size)
lemma is_up_compose:
shows
"\<lbrakk>is_up uc; is_up uc'\<rbrakk> \<Longrightarrow> is_up (uc' \<circ> uc)"
unfolding is_up_def by (simp add: Word.target_size Word.source_size)
lemma uint_is_up_compose:
fixes uc :: "('a::len) word \<Rightarrow> ('b::len) word"
and uc' :: "'b word \<Rightarrow> ('c::len) sword"
assumes "uc = ucast"
and "uc' = ucast"
and " uuc = uc' \<circ> uc"
shows
"\<lbrakk> is_up uc; is_up uc' \<rbrakk> \<Longrightarrow> uint (uuc b) = uint b"
apply (simp add: assms)
apply (frule is_up_compose)
apply (simp_all )
apply (simp only: Word.uint_up_ucast)
done
lemma uint_is_up_compose_pred:
fixes uc :: "('a::len) word \<Rightarrow> ('b::len) word"
and uc' :: "'b word \<Rightarrow> ('c::len) sword"
assumes "uc = ucast"
and "uc' = ucast"
and " uuc = uc' \<circ> uc"
shows
"\<lbrakk> is_up uc; is_up uc' \<rbrakk> \<Longrightarrow> P (uint (uuc b)) \<longleftrightarrow> P( uint b)"
apply (simp add: assms)
apply (frule is_up_compose)
apply (simp_all )
apply (simp only: Word.uint_up_ucast)
done
lemma is_down_up_sword:
fixes uc :: "('a::len) word \<Rightarrow> ('b::len) sword"
shows "\<lbrakk>uc = ucast; len_of TYPE('a) < len_of TYPE('b) \<rbrakk> \<Longrightarrow> is_up uc = (\<not> is_down uc)"
by (simp add: target_size source_size is_up_def is_down_def )
lemma is_not_down_compose:
fixes uc :: "('a::len) word \<Rightarrow> ('b::len) word"
and uc' :: "'b word \<Rightarrow> ('c::len) sword"
shows
"\<lbrakk>uc = ucast; uc' = ucast; len_of TYPE('a) < len_of TYPE('c)\<rbrakk> \<Longrightarrow> \<not> is_down (uc' \<circ> uc) "
unfolding is_down_def
by (simp add: Word.target_size Word.source_size)
lemma sint_ucast_uint:
fixes uc :: "('a::len) word \<Rightarrow> ('b::len) word"
and uc' :: "'b word \<Rightarrow> ('c::len) sword"
assumes "uc = ucast" and " uc' = ucast" and "uuc=uc' \<circ> uc " and "len_of TYPE('a) < len_of TYPE('c signed)"
shows
"\<lbrakk> is_up uc; is_up uc'\<rbrakk> \<Longrightarrow> sint (uuc b) = uint b"
apply (simp add: assms)
apply (frule is_up_compose')
apply simp_all
apply (simp add: ucast_ucast_b )
apply (rule WordLemmaBucket.sint_ucast_eq_uint )
apply (insert assms)
apply (simp add: is_down_def target_size source_size )
done
lemma sint_ucast_uint_pred:
fixes uc :: "('a::len) word \<Rightarrow> ('b::len) word"
and uc' :: "'b word \<Rightarrow> ('c::len) sword"
and uuc :: "'a word \<Rightarrow> 'c sword"
assumes "uc = ucast" and " uc' = ucast" and "uuc=uc' \<circ> uc " and "len_of TYPE('a) < len_of TYPE('c )"
shows "\<lbrakk>is_up uc; is_up uc'\<rbrakk> \<Longrightarrow> P (uint b) \<longleftrightarrow> P (sint (uuc b))"
apply (simp add: assms )
apply (insert sint_ucast_uint[where uc=uc and uc'=uc' and uuc=uuc and b = b])
apply (simp add: assms)
done
lemma sint_uucast_uint_uucast_pred:
fixes uc :: "('a::len) word \<Rightarrow> ('b::len) word"
and uc' :: "'b word \<Rightarrow> ('c::len) sword"
assumes "uc = ucast" and " uc' = ucast" and "uuc=uc' \<circ> uc " and "len_of TYPE('a) < len_of TYPE('c )"
shows "\<lbrakk>is_up uc; is_up uc'\<rbrakk> \<Longrightarrow> P (uint(uuc b)) \<longleftrightarrow> P (sint (uuc b))"
apply (simp add: assms )
apply (insert sint_ucast_uint[where uc=uc and uc'=uc' and uuc=uuc and b = b])
apply (insert uint_is_up_compose_pred[where uc=uc and uc'=uc' and uuc=uuc and b=b])
apply (simp add: assms uint_is_up_compose_pred)
done
lemma scast_maxIRQ_is_less:
fixes uc :: "irq \<Rightarrow> 16 word"
and uc' :: "16 word\<Rightarrow> 32 sword"
and b :: irq
shows
"(Kernel_C.maxIRQ) <s (ucast \<circ> (ucast :: irq \<Rightarrow> 16 word)) b \<Longrightarrow> scast Kernel_C.maxIRQ < b"
apply (simp add: maxIRQ_def word_sless_def word_sle_def, uint_arith, clarify,simp)
apply (subgoal_tac "sint (ucast Kernel_C.maxIRQ :: 32 sword) \<le> uint b"; (simp only: Kernel_C.maxIRQ_def)?)
apply (subgoal_tac "sint (ucast Kernel_C.maxIRQ :: 32 sword) \<noteq> uint b"; (simp only: Kernel_C.maxIRQ_def)?)
apply (simp )
apply (subst uint_is_up_compose[where uc="(ucast :: irq \<Rightarrow> 16 word)" and uc' = "(ucast :: 16 word \<Rightarrow> 32 sword)",symmetric];
(simp add: is_up_def target_size source_size )?)
apply fastforce
apply (subst sint_ucast_uint_pred[where uc="(ucast :: irq \<Rightarrow> 16 word)" and uc' = "(ucast :: 16 word \<Rightarrow> 32 sword)"];
(simp add: is_up_def target_size source_size )?)
apply fastforce
done
lemma validIRQcastingLess: "Kernel_C.maxIRQ <s (ucast((ucast (b :: irq))::word16)) \<Longrightarrow> Platform.maxIRQ < b"
by (simp add: Platform_maxIRQ scast_maxIRQ_is_less is_up_def target_size source_size)
lemma scast_maxIRQ_is_not_less: "(\<not> (Kernel_C.maxIRQ) <s (ucast \<circ> (ucast :: irq \<Rightarrow> 16 word)) b) \<Longrightarrow> \<not> (scast Kernel_C.maxIRQ < b)"
apply (subgoal_tac "sint (ucast Kernel_C.maxIRQ :: 32 sword) \<ge> sint (ucast (ucast b))";
(simp only: Kernel_C.maxIRQ_def word_sless_def word_sle_def )?)
apply (simp add: maxIRQ_def word_sless_def word_sle_def, uint_arith, clarify,simp)
apply (subst (asm) sint_ucast_uint[where b=b and 'c = 32 and 'b = 16 and uc=ucast and uc' = ucast and uuc = "ucast \<circ> ucast" , simplified];
(simp add: is_up_def target_size source_size)?)
apply (subst (asm) uint_is_up_compose[where 'b = 16 and uuc="ucast \<circ> ucast", simplified];
(simp add: is_up_def target_size source_size)?)
apply (simp add: maxIRQ_def word_sless_def word_sle_def, uint_arith, clarify,simp)
apply (subst (asm) (2) sint_ucast_uint_pred[where 'a = 10 and 'b = 16 and 'c = 32 and uuc = "ucast \<circ> ucast", simplified,symmetric ];
((simp add: is_up_def target_size source_size)?))
apply (subst sint_ucast_uint_pred[where 'a = 10 and 'b = 16 and 'c = 32 and uuc = "ucast \<circ> ucast", simplified,symmetric ];
((simp add: is_up_def target_size source_size)?))
apply (subst (asm) (2) uint_is_up_compose[where 'b = 16 and uuc="ucast \<circ> ucast", simplified];
(simp add: is_up_def target_size source_size)?)
apply (uint_arith)
done
lemma handleInterrupt_ccorres:
"ccorres dc xfdc
(invs' and K (irq \<le> ucast maxIRQ))
(invs')
(UNIV \<inter> \<lbrace>\<acute>irq = ucast irq\<rbrace>)
[]
(handleInterrupt irq)
(Call handleInterrupt_'proc)"
(Call handleInterrupt_'proc)"
apply (cinit lift: irq_' cong: call_ignore_cong)
apply (rule ccorres_Cond_rhs_Seq)
apply (simp add: Platform_maxIRQ del: Collect_const)
apply (drule scast_maxIRQ_is_less[simplified])
apply (simp del: Collect_const)
apply (rule ccorres_rhs_assoc)+
apply (simp del: Collect_const)
apply (subst doMachineOp_bind)
apply (rule maskInterrupt_empty_fail)
apply (rule ackInterrupt_empty_fail)
apply (ctac add: maskInterrupt_ccorres[unfolded dc_def])
apply (subst bind_return_unit[where f="doMachineOp (ackInterrupt irq)"])
apply (ctac add: ackInterrupt_ccorres[unfolded dc_def])
apply (rule ccorres_split_throws)
apply (rule ccorres_return_void_C[unfolded dc_def])
apply vcg
apply wp
apply (vcg exspec=ackInterrupt_modifies)
apply wp
apply (vcg exspec=maskInterrupt_modifies)
apply (simp add: scast_maxIRQ_is_not_less Platform_maxIRQ del: Collect_const)
apply (rule ccorres_pre_getIRQState)
apply wpc
apply simp
@ -1644,7 +1801,7 @@ lemma handleInterrupt_ccorres:
apply csymbr
apply (rule getIRQSlot_ccorres3)
apply (rule ccorres_getSlotCap_cte_at)
apply (rule_tac P="cte_at' rva" in ccorres_cross_over_guard)
apply (rule_tac P="cte_at' rv" in ccorres_cross_over_guard)
apply (rule ptr_add_assertion_irq_guard[unfolded dc_def])
apply (rule ccorres_move_array_assertion_irq ccorres_move_c_guard_cte)+
apply ctac
@ -1669,8 +1826,7 @@ lemma handleInterrupt_ccorres:
apply (simp del: Collect_const)
apply (rule ccorres_cond_true_seq)
apply (rule ccorres_rhs_assoc)+
apply csymbr
apply csymbr
apply csymbr+
apply (rule ccorres_cond_false_seq)
apply simp
apply (ctac (no_vcg) add: maskInterrupt_ccorres)
@ -1678,16 +1834,15 @@ lemma handleInterrupt_ccorres:
apply wp
apply (rule_tac P=\<top> and P'="{s. ret__int_' s = 0 \<and> cap_get_tag cap \<noteq> scast cap_notification_cap}" in ccorres_inst)
apply (clarsimp simp: isCap_simps simp del: Collect_const)
apply (case_tac rvb, simp_all del: Collect_const)[1]
prefer 3
apply metis
apply ((rule ccorres_guard_imp2,
rule ccorres_cond_false_seq, simp,
apply (case_tac rva, simp_all del: Collect_const)[1]
prefer 3
apply metis
apply ((rule ccorres_guard_imp2,
rule ccorres_cond_false_seq, simp,
rule ccorres_cond_false_seq, simp,
ctac (no_vcg) add: maskInterrupt_ccorres,
ctac (no_vcg) add: ackInterrupt_ccorres [unfolded dc_def],
wp, simp)+)
apply simp
apply (wp getSlotCap_wp)
apply simp
apply vcg
@ -1699,37 +1854,34 @@ lemma handleInterrupt_ccorres:
apply (rule ccorres_rhs_assoc)+
apply (ctac (no_vcg) add: timerTick_ccorres)
apply (ctac (no_vcg) add: resetTimer_ccorres)
apply (ctac add: ackInterrupt_ccorres)
apply (ctac add: ackInterrupt_ccorres )
apply wp
apply (simp add: sint_ucast_eq_uint is_down uint_up_ucast is_up)
apply (simp add: sint_ucast_eq_uint is_down uint_up_ucast is_up )
apply (clarsimp simp: word_sless_alt word_less_alt word_le_def maxIRQ_def uint_up_ucast is_up_def
source_size_def target_size_def word_size
sint_ucast_eq_uint is_down is_up word_0_sle_from_less)
source_size_def target_size_def word_size
sint_ucast_eq_uint is_down is_up word_0_sle_from_less)
apply (rule conjI)
apply (clarsimp simp: cte_wp_at_ctes_of ucast_up_ucast is_up)
apply (intro conjI allI)
apply (clarsimp simp add: if_1_0_0 Collect_const_mem)
apply (clarsimp simp: cte_wp_at_ctes_of )
apply (clarsimp simp add: if_1_0_0 Collect_const_mem )
apply (clarsimp simp: Kernel_C.IRQTimer_def Kernel_C.IRQSignal_def
cte_wp_at_ctes_of ucast_ucast_b is_up)
cte_wp_at_ctes_of ucast_ucast_b is_up)
apply (intro conjI impI)
apply clarsimp
apply (erule(1) cmap_relationE1[OF cmap_relation_cte])
apply (clarsimp simp: typ_heap_simps')
apply (simp add: cap_get_tag_isCap)
apply (clarsimp simp: isCap_simps)
apply (frule cap_get_tag_isCap_unfolded_H_cap)
apply (frule cap_get_tag_to_H, assumption)
apply (clarsimp simp: to_bool_def)
apply (cut_tac un_ui_le[where b = 159 and a = irq,
simplified word_size])
apply (simp add: ucast_eq_0 is_up_def source_size_def
target_size_def word_size unat_gt_0
| subst array_assertion_abs_irq[rule_format, OF conjI])+
apply clarsimp
apply (erule(1) cmap_relationE1[OF cmap_relation_cte])
apply (clarsimp simp: typ_heap_simps')
apply (simp add: cap_get_tag_isCap)
apply (clarsimp simp: isCap_simps)
apply (frule cap_get_tag_isCap_unfolded_H_cap)
apply (frule cap_get_tag_to_H, assumption)
apply (clarsimp simp: to_bool_def)
apply (cut_tac un_ui_le[where b = 159 and a = irq,
simplified word_size])
apply (simp add: ucast_eq_0 is_up_def source_size_def
target_size_def word_size unat_gt_0
| subst array_assertion_abs_irq[rule_format, OF conjI])+
apply (erule(1) rf_sr_cte_at_valid[OF ctes_of_cte_at])
apply (clarsimp simp:nat_le_iff)
done
end
end

6
proof/drefine/Interrupt_DR.thy
View File

@ -281,6 +281,12 @@ lemma handle_interrupt_corres:
"dcorres dc \<top> (invs and valid_etcbs) (Interrupt_D.handle_interrupt x) (Interrupt_A.handle_interrupt x)"
apply (clarsimp simp:Interrupt_A.handle_interrupt_def)
apply (clarsimp simp:get_irq_state_def gets_def bind_assoc)
apply (rule conjI; rule impI)
apply (subst Interrupt_D.handle_interrupt_def, simp)
apply (subst Retype_AI.do_machine_op_bind)
apply (rule maskInterrupt_empty_fail)
apply (rule ackInterrupt_empty_fail)
using corres_guard2_imp handle_interrupt_corres_branch apply blast
apply (rule dcorres_absorb_get_r)+
apply (clarsimp split:irq_state.splits simp:corres_free_fail | rule conjI)+
apply (simp add:Interrupt_D.handle_interrupt_def bind_assoc)

12
proof/infoflow/ADT_IF.thy
View File

@ -1132,10 +1132,9 @@ lemma handle_preemption_if_irq_masks:
"\<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st\<rbrace>
handle_preemption_if tc
\<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>"
apply(simp add: handle_preemption_if_def | wp handle_interrupt_irq_masks)+
apply(rule_tac Q="\<lambda>_ s. P (irq_masks_of_state s) \<and> domain_sep_inv False st s" in hoare_strengthen_post)
apply(wp | simp)+
by blast
apply(simp add: handle_preemption_if_def | wp handle_interrupt_irq_masks[where st=st])+
apply(rule_tac Q="\<lambda>rv s. P (irq_masks_of_state s) \<and> domain_sep_inv False st s \<and> (\<forall>x. rv = Some x \<longrightarrow> x \<le> maxIRQ) " in hoare_strengthen_post)
by(wp | simp)+
crunch valid_list[wp]: handle_preemption_if "valid_list"
(ignore: getActiveIRQ)
@ -1720,8 +1719,9 @@ lemma handle_interrupt_domain_time_sched_action:
"num_domains > 1 \<Longrightarrow>
\<lbrace>\<lambda>s. domain_time s > 0\<rbrace>
handle_interrupt e
\<lbrace>\<lambda>r s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace>"
apply(simp add: handle_interrupt_def)
\<lbrace>\<lambda>r s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace>"
apply(simp add: handle_interrupt_def split del: split_if)
apply (rule hoare_pre)
apply (wp)
apply(case_tac "st \<noteq> IRQTimer")
apply((wp hoare_vcg_imp_lift' | simp | wpc)+)[1]

1
proof/infoflow/FinalCaps.thy
View File

@ -3153,6 +3153,7 @@ lemma handle_recv_silc_inv:
lemma handle_interrupt_silc_inv:
"\<lbrace>silc_inv aag st\<rbrace> handle_interrupt irq \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
unfolding handle_interrupt_def
apply (rule hoare_if)
apply(wp | wpc | simp | wp_once hoare_drop_imps)+
done

54
proof/infoflow/IRQMasks_IF.thy
View File

@ -83,14 +83,18 @@ crunch irq_masks[wp]: machine_op_lift "\<lambda>s. P (irq_masks s)"
lemma handle_interrupt_irq_masks:
notes no_irq[wp del]
shows
"\<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st\<rbrace>
"\<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and K (irq \<le> maxIRQ)\<rbrace>
handle_interrupt irq
\<lbrace>\<lambda>rv s. P (irq_masks_of_state s)\<rbrace>"
apply(simp add: handle_interrupt_def)
apply(wp dmo_wp | simp add: ackInterrupt_def maskInterrupt_def when_def
split del: split_if | wpc | simp add: get_irq_state_def |wp_once hoare_drop_imp)+
apply(fastforce simp: domain_sep_inv_def)
apply (rule hoare_gen_asm)
apply(simp add: handle_interrupt_def split del: split_if)
apply (rule hoare_pre)
apply (rule hoare_if)
apply simp
apply(wp dmo_wp | simp add: ackInterrupt_def maskInterrupt_def when_def split del: split_if | wpc | simp add: get_irq_state_def | wp_once hoare_drop_imp)+
apply (fastforce simp: domain_sep_inv_def)
done
crunch irq_masks[wp]: cap_swap_for_delete "\<lambda>s. P (irq_masks_of_state s)"
@ -396,12 +400,27 @@ crunch irq_masks[wp]: handle_vm_fault "\<lambda>s. P (irq_masks_of_state s)"
lemma dmo_getActiveIRQ_irq_masks[wp]:
"\<lbrace>(\<lambda>s. P (irq_masks_of_state s))\<rbrace>
do_machine_op getActiveIRQ
\<lbrace>\<lambda>x s. P (irq_masks_of_state s)\<rbrace>"
\<lbrace>\<lambda>rv s. P (irq_masks_of_state s) \<rbrace>"
apply(rule hoare_pre, rule dmo_wp)
apply(simp add: getActiveIRQ_def | wp | simp add: no_irq_def | clarsimp)+
done
lemma dmo_getActiveIRQ_return_axiom[wp]:
"\<lbrace>\<top>\<rbrace>
do_machine_op getActiveIRQ
\<lbrace>(\<lambda>rv s. (\<forall>x. rv = Some x \<longrightarrow> x \<le> maxIRQ)) \<rbrace>"
apply (simp add: getActiveIRQ_def)
apply(rule hoare_pre, rule dmo_wp)
apply (insert irq_oracle_max_irq)
apply (wp alternative_wp select_wp dmo_getActiveIRQ_irq_masks)
apply clarsimp
done
lemma handle_yield_irq_masks_of_state[wp]: "\<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and invs\<rbrace> handle_yield \<lbrace>\<lambda>rv s. P (irq_masks_of_state s)\<rbrace>"
lemma handle_yield_irq_masks_of_state[wp]:
"\<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and invs\<rbrace>
handle_yield
\<lbrace>\<lambda>rv s. P (irq_masks_of_state s)\<rbrace>"
apply (simp add: handle_yield_def)
apply wp
apply simp
@ -412,9 +431,20 @@ lemma handle_event_irq_masks:
handle_event ev
\<lbrace> \<lambda> rv s. P (irq_masks_of_state s) \<rbrace>"
apply(case_tac ev)
apply (rename_tac syscall)
apply(case_tac syscall)
apply(simp add: handle_send_def handle_call_def | wp handle_invocation_irq_masks[where st=st] handle_interrupt_irq_masks[where st=st] hoare_vcg_all_lift | wpc | wp_once hoare_drop_imps)+
prefer 4
apply (rule hoare_pre)
apply simp
apply (wp handle_interrupt_irq_masks[where st=st] | wpc | simp )+
apply (rule_tac Q="\<lambda>rv s. P (irq_masks_of_state s) \<and> domain_sep_inv False st s \<and> (\<forall>x. rv = Some x \<longrightarrow> x \<le> maxIRQ)" in hoare_strengthen_post)
apply (wp | clarsimp)+
apply (rename_tac syscall)
apply (case_tac syscall)
apply (simp add: handle_send_def handle_call_def
| wp handle_invocation_irq_masks[where st=st] handle_interrupt_irq_masks[where st=st] hoare_vcg_all_lift
| wpc
| wp_once hoare_drop_imps)+
done
crunch irq_masks[wp]: activate_thread "\<lambda>s. P (irq_masks_of_state s)"
@ -428,8 +458,8 @@ lemma call_kernel_irq_masks:
\<lbrace> \<lambda> rv s. P (irq_masks_of_state s) \<rbrace>"
apply(simp add: call_kernel_def)
apply (wp handle_interrupt_irq_masks[where st=st])+
apply(rule_tac Q="\<lambda>_ s. P (irq_masks_of_state s) \<and> domain_sep_inv False st s" in hoare_strengthen_post)
apply(wp | simp)+
apply (rule_tac Q="\<lambda>rv s. P (irq_masks_of_state s) \<and> domain_sep_inv False st s \<and> (\<forall>x. rv = Some x \<longrightarrow> x \<le> maxIRQ)" in hoare_strengthen_post)
apply (wp | simp)+
apply(rule_tac Q="\<lambda> x s. P (irq_masks_of_state s) \<and> domain_sep_inv False st s" and F="E" for E in hoare_post_impErr)
apply(rule valid_validE)
apply(wp handle_event_irq_masks[where st=st] valid_validE[OF handle_event_domain_sep_inv] | simp)+

50
proof/infoflow/Noninterference.thy
View File

@ -3225,7 +3225,18 @@ lemma confidentiality_part_not_PSched:
apply(fastforce dest: non_PSched_steps_run_in_lock_step)
done
lemma getActiveIRQ_ret_no_dmo[wp]: "\<lbrace>\<lambda>_. True\<rbrace> getActiveIRQ \<lbrace>\<lambda>rv s. \<forall>x. rv = Some x \<longrightarrow> x \<le> maxIRQ\<rbrace>"
apply (simp add: getActiveIRQ_def)
apply(rule hoare_pre)
apply (insert irq_oracle_max_irq)
apply (wp alternative_wp select_wp dmo_getActiveIRQ_irq_masks)
apply clarsimp
done
lemma try_some_magic: "(\<forall>x. y = Some x \<longrightarrow> P x) = ((\<exists>x. y = Some x) \<longrightarrow> P (the y))"
by auto
lemma preemption_interrupt_scheduler_invisible:
"equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (\<lambda>r r'. r = uc \<and> snd r' = uc')
(einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s)
@ -3237,22 +3248,19 @@ lemma preemption_interrupt_scheduler_invisible:
apply (rule equiv_valid_2_bind_right)
apply (rule equiv_valid_2_bind_right)
apply (simp add: liftE_def bind_assoc)
apply (simp only: option.case_eq_if)
apply (rule equiv_valid_2_bind_pre[where R'="op ="])
apply simp
apply (case_tac "rv'")
prefer 2
apply simp
apply (rule equiv_valid_2_bind_pre[where R'="op =" and Q="\<top>\<top>" and Q'="\<top>\<top>"])
apply (rule return_ev2)
apply simp
apply (rule equiv_valid_2)
apply (rule handle_interrupt_reads_respects_scheduler)
apply (wp | simp)+
apply (rule return_ev2)
apply simp
apply (simp add: when_def split del: split_if)
apply (subst if_swap)
apply (simp split del: split_if)
apply (rule equiv_valid_2_bind_pre[where R'="op =" and Q="\<top>\<top>" and Q'="\<top>\<top>"])
apply (rule return_ev2)
apply simp
apply (rule equiv_valid_2)
apply (wp handle_interrupt_reads_respects_scheduler[where st=st] | simp)+
apply (rule equiv_valid_2)
apply (rule dmo_getActive_IRQ_reads_respect_scheduler)
apply (wp | simp | elim conjE | intro conjI)+
apply (wp dmo_getActiveIRQ_return_axiom[simplified try_some_magic] | simp add: imp_conjR | elim conjE | intro conjI | wp_once hoare_drop_imps)+
apply (subst thread_set_as_user)
apply (wp guarded_pas_domain_lift)
apply ((simp | wp | force)+)[7]
@ -3275,8 +3283,8 @@ lemma handle_preemption_agnostic_ret: "\<lbrace>\<top>\<rbrace> handle_preemptio
lemma handle_preemption_reads_respects_scheduler:
"reads_respects_scheduler aag l (einvs and pas_refined aag and guarded_pas_domain aag and domain_sep_inv False st and silc_inv aag st' and (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s)) (handle_preemption_if uc)"
apply (simp add: handle_preemption_if_def)
apply (wp when_ev handle_interrupt_reads_respects_scheduler
dmo_getActive_IRQ_reads_respect_scheduler | simp | wp_once hoare_drop_imps)+
apply (wp when_ev handle_interrupt_reads_respects_scheduler dmo_getActiveIRQ_return_axiom[simplified try_some_magic]
dmo_getActive_IRQ_reads_respect_scheduler | simp add: imp_conjR| wp_once hoare_drop_imps)+
apply force
done
@ -3298,8 +3306,8 @@ lemma kernel_entry_scheduler_equiv_2:
apply (rule equiv_valid_2_bind_pre[where R'="op ="])
apply (rule equiv_valid_2)
apply simp
apply (wp del: no_irq add: handle_interrupt_reads_respects_scheduler
dmo_getActive_IRQ_reads_respect_scheduler hoare_vcg_all_lift | wpc | simp | wp_once hoare_drop_imps)+
apply (wp del: no_irq add: handle_interrupt_reads_respects_scheduler[where st=st]
dmo_getActive_IRQ_reads_respect_scheduler | wpc | simp add: imp_conjR all_conj_distrib | wp_once hoare_drop_imps)+
apply (rule context_update_cur_thread_snippit)
apply (wp thread_set_invs_trivial guarded_pas_domain_lift
thread_set_pas_refined thread_set_not_state_valid_sched | simp add: tcb_cap_cases_def)+
@ -3315,15 +3323,15 @@ lemma kernel_entry_if_reads_respects_scheduler:
apply (rule bind_ev_pre)
apply wp_once
apply (rule bind_ev_pre)
apply ((wp del: no_irq add: when_ev handle_interrupt_reads_respects_scheduler dmo_getActive_IRQ_reads_respect_scheduler hoare_vcg_all_lift liftE_ev | simp | wpc | wp_once hoare_drop_imps)+)[1]
apply ((wp del: no_irq add: when_ev handle_interrupt_reads_respects_scheduler[where st=st] dmo_getActive_IRQ_reads_respect_scheduler liftE_ev | simp add: imp_conjR all_conj_distrib | wpc | wp_once hoare_drop_imps)+)[1]
apply (rule reads_respects_scheduler_cases')
prefer 3
apply (rule reads_respects_scheduler_unobservable'')
apply ((wp thread_set_scheduler_equiv | simp | elim conjE)+)[3]
apply ((wp | simp | elim conjE)+)[2]
apply (clarsimp simp: guarded_pas_domain_def)
apply (wp thread_set_invs_trivial guarded_pas_domain_lift
thread_set_pas_refined thread_set_not_state_valid_sched | simp add: tcb_cap_cases_def)+
apply ((wp thread_set_invs_trivial guarded_pas_domain_lift hoare_vcg_all_lift
thread_set_pas_refined thread_set_not_state_valid_sched | simp add: tcb_cap_cases_def)+)
apply (clarsimp simp: cur_thread_idle cur_thread_not_SilcLabel)
apply force
done

20
proof/infoflow/Scheduler_IF.thy
View File

@ -2167,16 +2167,22 @@ lemma ackInterrupt_reads_respects_scheduler:
done
lemma handle_interrupt_reads_respects_scheduler:
"reads_respects_scheduler aag l (invs and guarded_pas_domain aag and pas_refined aag and valid_sched and domain_sep_inv False st) (handle_interrupt irq)"
apply (simp add: handle_interrupt_def)
apply (wp | rule ackInterrupt_reads_respects_scheduler)+
apply (rule_tac Q="rv = IRQTimer \<or> rv = IRQInactive" in gen_asm_ev(2))
apply (elim disjE)
apply (wp timer_tick_reads_respects_scheduler
"reads_respects_scheduler aag l (invs and guarded_pas_domain aag and pas_refined aag and valid_sched and domain_sep_inv False st and K (irq \<le> maxIRQ)) (handle_interrupt irq)"
apply (simp add: handle_interrupt_def )
apply (rule conjI; rule impI )
apply (rule gen_asm_ev)
apply simp
apply (wp modify_wp | simp )+
apply (rule ackInterrupt_reads_respects_scheduler)
apply (rule_tac Q="rv = IRQTimer \<or> rv = IRQInactive" in gen_asm_ev(2))
apply (elim disjE)
apply (wp timer_tick_reads_respects_scheduler
ackInterrupt_reads_respects_scheduler
dmo_resetTimer_reads_respects_scheduler
get_irq_state_reads_respects_scheduler_trivial
fail_ev irq_inactive_or_timer | simp add: | wpc)+
fail_ev irq_inactive_or_timer | simp )+
apply force
done

11
proof/infoflow/Syscall_IF.thy
View File

@ -907,13 +907,20 @@ declare gts_st_tcb_at[wp del]
lemma handle_interrupt_globals_equiv:
"\<lbrace>globals_equiv (st :: det_ext state) and invs\<rbrace> handle_interrupt irq \<lbrace>\<lambda>r. globals_equiv st\<rbrace>"
unfolding handle_interrupt_def
apply (wp dmo_maskInterrupt_globals_equiv
apply (rule hoare_if)
apply (wp dmo_maskInterrupt_globals_equiv
dmo_return_globals_equiv
send_signal_globals_equiv
VSpace_AI.dmo_ackInterrupt
hoare_vcg_if_lift2
hoare_drop_imps
dxo_wp_weak
| wpc | simp add: ackInterrupt_def resetTimer_def invs_imps invs_valid_idle)+
Retype_IF.dmo_mol_globals_equiv
NonDetMonadLemmaBucket.no_fail_bind
NonDetMonadLemmaBucket.bind_known_operation_eq
Retype_IF.dmo_mol_globals_equiv
| wpc | simp add: Interrupt_AI.empty_fail_ackInterrupt dmo_bind_valid ackInterrupt_def resetTimer_def invs_imps invs_valid_idle)+
done

8
proof/invariant-abstract/Deterministic_AI.thy
View File

@ -4117,10 +4117,10 @@ interpretation timer_tick_extended: is_extended "timer_tick"
done
lemma handle_interrupt_valid_list[wp]:
"\<lbrace>valid_list\<rbrace> handle_interrupt irq \<lbrace>\<lambda>_.valid_list\<rbrace>"
unfolding handle_interrupt_def
apply (wp get_cap_wp | wpc | simp add: get_irq_slot_def get_irq_state_def)+
done
"\<lbrace>valid_list \<rbrace> handle_interrupt irq \<lbrace>\<lambda>_.valid_list\<rbrace>"
unfolding handle_interrupt_def ackInterrupt_def
apply (rule hoare_pre)
by (wp get_cap_wp do_machine_op_valid_list | wpc | simp add: get_irq_slot_def | wp_once hoare_drop_imps)+
crunch valid_list[wp]: handle_send,handle_reply valid_list

25
proof/invariant-abstract/Interrupt_AI.thy
View File

@ -203,13 +203,15 @@ lemma get_irq_slot_ex_cte:
apply clarsimp
done
lemma maskInterrupt_invs:
"\<lbrace>invs and (\<lambda>s. interrupt_states s irq \<noteq> IRQInactive)\<rbrace>
"\<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)
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
crunch pspace_aligned[wp]: set_irq_state "pspace_aligned"
@ -370,16 +372,23 @@ lemma send_signal_interrupt_states[wp_unsafe]:
apply (auto simp: pred_tcb_at_def obj_at_def receive_blocked_def)
done
lemma handle_interrupt_invs[wp]:
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 (wp maskInterrupt_invs | wpc)+
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
done
end

2
proof/invariant-abstract/Syscall_AI.thy
View File

@ -1253,7 +1253,7 @@ lemma he_invs[wp]:
apply (case_tac e, simp_all)
apply (rename_tac syscall)
apply (case_tac syscall, simp_all)
apply ((rule hoare_pre, wp hvmf_active hr_invs hy_inv) |
apply ((rule hoare_pre, wp hvmf_active hr_invs hy_inv ) |
wpc | wp hoare_drop_imps hoare_vcg_all_lift |
fastforce simp: tcb_at_invs ct_in_state_def valid_fault_def
elim!: st_tcb_ex_cap)+

72
proof/refine/Interrupt_R.thy
View File

@ -550,24 +550,29 @@ lemma timerTick_corres:
apply simp
done
lemmas corres_eq_trivial = corres_Id[where f = h and g = h for h, simplified]
thm corres_Id
lemma handle_interrupt_corres:
"corres dc
(einvs) (invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) irq \<noteq> IRQInactive))
(handle_interrupt irq) (handleInterrupt irq)"
(is "corres dc (einvs) ?P' ?f ?g")
apply (simp add: handle_interrupt_def handleInterrupt_def)
apply (simp add: handle_interrupt_def handleInterrupt_def )
apply (rule conjI[rotated]; rule impI)
apply (rule corres_guard_imp)
apply (rule corres_split [OF _ get_irq_state_corres,
where R="\<lambda>rv. einvs"
and R'="\<lambda>rv. invs' and (\<lambda>s. rv \<noteq> IRQInactive)"])
and R'="\<lambda>rv. invs' and (\<lambda>s. rv \<noteq> IRQInactive)"])
defer
apply (wp getIRQState_prop getIRQState_inv)
apply simp+
apply (rule corres_gen_asm2)
apply (rule corres_split'[where r'=dc, rotated])
apply (rule corres_machine_op)
apply (rule corres_Id, simp+)
apply wp
apply (wp getIRQState_prop getIRQState_inv do_machine_op_bind doMachineOp_bind | simp add: do_machine_op_bind doMachineOp_bind )+
apply (rule corres_guard_imp)
apply (rule corres_split)
apply (rule corres_machine_op, rule corres_eq_trivial ; (simp add: dc_def no_fail_maskInterrupt no_fail_bind no_fail_ackInterrupt)+)+
apply ((wp | simp)+)[4]
apply (rule corres_gen_asm2)
apply (case_tac st, simp_all add: irq_state_relation_def split: irqstate.split_asm)
apply (simp add: getSlotCap_def bind_assoc)
apply (rule corres_guard_imp)
@ -577,24 +582,29 @@ lemma handle_interrupt_corres:
where R="\<lambda>rv. einvs and valid_cap rv"
and R'="\<lambda>rv. invs' and valid_cap' (cteCap rv)"])
apply (rule corres_split'[where r'=dc])
apply (case_tac cap, simp_all add: when_False when_True doMachineOp_return)[1]
apply (case_tac xb, simp_all add: when_False doMachineOp_return )[1]
apply (clarsimp simp add: when_def doMachineOp_return)
apply (rule corres_guard_imp, rule send_signal_corres)
apply (clarsimp simp: valid_cap_def)
apply (clarsimp simp: valid_cap'_def)
apply (clarsimp simp: doMachineOp_return)
apply (rule corres_machine_op)
apply (rule corres_Id, simp+)
apply (wp | simp)+
apply (clarsimp simp: valid_cap_def valid_cap'_def do_machine_op_bind doMachineOp_bind)+
apply ( rule corres_split)
apply (rule corres_machine_op, rule corres_eq_trivial ; (simp add: no_fail_maskInterrupt no_fail_bind no_fail_ackInterrupt)+)+
apply ((wp |simp)+)
apply clarsimp
apply fastforce
apply (rule corres_guard_imp)
apply (rule corres_split)
apply simp
apply (rule corres_split [OF corres_machine_op timerTick_corres])
apply (rule corres_eq_trivial, simp+)
apply (rule corres_machine_op)
apply (rule corres_eq_trivial, (simp add: no_fail_ackInterrupt)+)
apply wp
apply clarsimp
apply clarsimp
apply fastforce
apply (rule corres_guard_imp)
apply (rule corres_split [OF corres_machine_op timerTick_corres])
apply (rule corres_Id, simp+)
apply wp
apply (clarsimp simp: invs_def valid_state_def valid_sched_def
valid_sched_action_def weak_valid_sched_action_def)+
done
lemma invs_ChooseNewThread:
@ -847,16 +857,20 @@ lemma dmo_ackInterrupt[wp]:
lemma hint_invs[wp]:
"\<lbrace>invs'\<rbrace> handleInterrupt irq \<lbrace>\<lambda>rv. invs'\<rbrace>"
apply (simp add: handleInterrupt_def getSlotCap_def
cong: irqstate.case_cong)
apply (wp dmo_maskInterrupt_True getCTE_wp'
| wpc | simp)+
cong: irqstate.case_cong)
apply (rule conjI; rule impI)
apply (wp dmo_maskInterrupt_True getCTE_wp'
| wpc | simp add: doMachineOp_bind )+
apply (rule_tac Q="\<lambda>rv. invs'" in hoare_post_imp)
apply (clarsimp simp: cte_wp_at_ctes_of ex_nonz_cap_to'_def)
apply fastforce
apply (wp threadSet_invs_trivial | simp add: inQ_def)+
apply (rule hoare_strengthen_post, rule getIRQState_inv)
apply (auto simp add: tcb_at_invs')
apply (wp hoare_post_comb_imp_conj hoare_drop_imp getIRQState_inv)
apply (assumption)
done
crunch st_tcb_at'[wp]: timerTick "st_tcb_at' P t"
(wp: threadSet_pred_tcb_no_state)
@ -864,7 +878,7 @@ crunch st_tcb_at'[wp]: timerTick "st_tcb_at' P t"
lemma handleInterrupt_runnable:
"\<lbrace>st_tcb_at' runnable' t\<rbrace> handleInterrupt irq \<lbrace>\<lambda>_. st_tcb_at' runnable' t\<rbrace>"
apply (simp add: handleInterrupt_def)
apply (rule hoare_pre)
apply (rule conjI; rule impI)
apply (wp sai_st_tcb' hoare_vcg_all_lift hoare_drop_imps
threadSet_pred_tcb_no_state getIRQState_inv haskell_fail_wp
|wpc|simp)+

2
proof/refine/PageTableDuplicates.thy
View File

@ -2519,7 +2519,7 @@ lemma handleInterrupt_valid_duplicates'[wp]:
"\<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
handleInterrupt irq \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace>"
apply (simp add: handleInterrupt_def)
apply (rule hoare_pre)
apply (rule conjI; rule impI)
apply (wp sai_st_tcb' hoare_vcg_all_lift hoare_drop_imps
threadSet_pred_tcb_no_state getIRQState_inv haskell_fail_wp
|wpc|simp)+

37
spec/abstract/Interrupt_A.thy
View File

@ -82,22 +82,27 @@ definition timer_tick :: "unit det_ext_monad" where
definition
handle_interrupt :: "irq \<Rightarrow> (unit,'z::state_ext) s_monad" where
"handle_interrupt irq \<equiv> do
st \<leftarrow> get_irq_state irq;
case st of
IRQSignal \<Rightarrow> do
slot \<leftarrow> get_irq_slot irq;
cap \<leftarrow> get_cap slot;
when (is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap)
$ send_signal (obj_ref_of cap) (cap_ep_badge cap);
do_machine_op $ maskInterrupt True irq
"handle_interrupt irq \<equiv>
if (irq > maxIRQ) then do_machine_op $ do
maskInterrupt True irq;
ackInterrupt irq
od
| IRQTimer \<Rightarrow> do
do_extended_op timer_tick;
do_machine_op resetTimer
od
| IRQInactive \<Rightarrow> fail (* not meant to be able to get IRQs from inactive lines *);
do_machine_op $ ackInterrupt irq
od"
else do
st \<leftarrow> get_irq_state irq;
case st of
IRQSignal \<Rightarrow> do
slot \<leftarrow> get_irq_slot irq;
cap \<leftarrow> get_cap slot;
when (is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap)
$ send_signal (obj_ref_of cap) (cap_ep_badge cap);
do_machine_op $ maskInterrupt True irq
od
| IRQTimer \<Rightarrow> do
do_extended_op timer_tick;
do_machine_op resetTimer
od
| IRQInactive \<Rightarrow> fail (* not meant to be able to get IRQs from inactive lines *);
do_machine_op $ ackInterrupt irq
od"
end

4
spec/capDL/Interrupt_D.thy
View File

@ -13,7 +13,7 @@
*)
theory Interrupt_D
imports Endpoint_D
imports Endpoint_D "../machine/$L4V_ARCH/Platform"
begin
(* Return the currently pending IRQ. *)
@ -113,7 +113,7 @@ where
definition
handle_interrupt :: "cdl_irq \<Rightarrow> unit k_monad"
where
"handle_interrupt irq \<equiv>
"handle_interrupt irq \<equiv> if (irq > maxIRQ) then return () else
do
irq_slot \<leftarrow> gets $ get_irq_slot irq;
c \<leftarrow> gets $ opt_cap irq_slot;

49
spec/design/Interrupt_H.thy
View File

@ -128,28 +128,35 @@ defs initInterruptController_def:
odE)"
defs handleInterrupt_def:
"handleInterrupt irq\<equiv> (do
st \<leftarrow> getIRQState irq;
(case st of
IRQSignal \<Rightarrow> (do
slot \<leftarrow> getIRQSlot irq;
cap \<leftarrow> getSlotCap slot;
(case cap of
NotificationCap _ _ True _ \<Rightarrow>
sendSignal (capNtfnPtr cap) (capNtfnBadge cap)
| _ \<Rightarrow> doMachineOp $ debugPrint $
[] @ show irq
);
doMachineOp $ maskInterrupt True irq
"handleInterrupt irq\<equiv> (
if (irq > maxIRQ) then doMachineOp $ ((do
maskInterrupt True irq;
ackInterrupt irq
od)
)
else (do
st \<leftarrow> getIRQState irq;
(case st of
IRQSignal \<Rightarrow> (do
slot \<leftarrow> getIRQSlot irq;
cap \<leftarrow> getSlotCap slot;
(case cap of
NotificationCap _ _ True _ \<Rightarrow>
sendSignal (capNtfnPtr cap) (capNtfnBadge cap)
| _ \<Rightarrow> doMachineOp $ debugPrint $
[] @ show irq
);
doMachineOp $ maskInterrupt True irq
od)
| IRQTimer \<Rightarrow> (do
timerTick;
doMachineOp resetTimer
od)
| IRQTimer \<Rightarrow> (do
timerTick;
doMachineOp resetTimer
od)
| IRQInactive \<Rightarrow> haskell_fail $ [] @ show irq
);
doMachineOp $ ackInterrupt irq
od)"
| IRQInactive \<Rightarrow> haskell_fail $ [] @ show irq
);
doMachineOp $ ackInterrupt irq
od)
)"
defs isIRQActive_def:
"isIRQActive irq\<equiv> liftM (\<lambda>x. x \<noteq>IRQInactive) $ getIRQState irq"

3
spec/design/m-skel/ARM/MachineTypes.thy
View File

@ -67,6 +67,9 @@ record
consts irq_oracle :: "nat \<Rightarrow> 10 word"
axiomatization irq_oracle_max_irqInst where
irq_oracle_max_irq: "\<forall> n. (irq_oracle n) <= maxIRQ"
text {*
The machine monad is used for operations on the state defined above.
*}

4
spec/design/version
View File

@ -1,4 +1,4 @@
Built from git repo at /home/xgao/verification/seL4/haskell by xgao
Built from git repo at /home/spacekitteh/verification/seL4/haskell by spacekitteh
Generated from changeset:
007e805 fix for asmrefine
0d0cf20 Fixed comments due to buggy haskell translator

3
spec/machine/ARM/MachineTypes.thy
View File

@ -181,6 +181,9 @@ record
consts irq_oracle :: "nat \<Rightarrow> 10 word"
axiomatization irq_oracle_max_irqInst where
irq_oracle_max_irq: "\<forall> n. (irq_oracle n) <= maxIRQ"
text {*
The machine monad is used for operations on the state defined above.
*}