From d7fd88727a888129806cf880b0fbc23b328e7341 Mon Sep 17 00:00:00 2001 From: Sophie Taylor Date: Tue, 9 Feb 2016 13:34:35 +1100 Subject: [PATCH] SELFOUR-420: Verification of maxIRQ check in handle_interrupt. --- proof/access-control/Syscall_AC.thy | 7 +- proof/crefine/Syscall_C.thy | 220 +++++++++++++++--- proof/drefine/Interrupt_DR.thy | 6 + proof/infoflow/ADT_IF.thy | 12 +- proof/infoflow/FinalCaps.thy | 1 + proof/infoflow/IRQMasks_IF.thy | 54 ++++- proof/infoflow/Noninterference.thy | 50 ++-- proof/infoflow/Scheduler_IF.thy | 20 +- proof/infoflow/Syscall_IF.thy | 11 +- proof/invariant-abstract/Deterministic_AI.thy | 8 +- proof/invariant-abstract/Interrupt_AI.thy | 25 +- proof/invariant-abstract/Syscall_AI.thy | 2 +- proof/refine/Interrupt_R.thy | 72 +++--- proof/refine/PageTableDuplicates.thy | 2 +- spec/abstract/Interrupt_A.thy | 37 +-- spec/capDL/Interrupt_D.thy | 4 +- spec/design/Interrupt_H.thy | 49 ++-- spec/design/m-skel/ARM/MachineTypes.thy | 3 + spec/design/version | 4 +- spec/machine/ARM/MachineTypes.thy | 3 + 20 files changed, 421 insertions(+), 169 deletions(-) diff --git a/proof/access-control/Syscall_AC.thy b/proof/access-control/Syscall_AC.thy index 527a750f2..a0f256fbc 100644 --- a/proof/access-control/Syscall_AC.thy +++ b/proof/access-control/Syscall_AC.thy @@ -491,7 +491,7 @@ lemma handle_interrupt_pas_refined: handle_interrupt irq \\rv. pas_refined aag\" 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 \\rv. integrity aag X st\" 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 \\rv. integrity aag X st\" 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]: "\\s :: det_ext state. P (arch_state s)\ handle_interrupt irq \\_ s. P (arch_state s)\" 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)+ diff --git a/proof/crefine/Syscall_C.thy b/proof/crefine/Syscall_C.thy index 39d1c2637..21a8a92e7 100644 --- a/proof/crefine/Syscall_C.thy +++ b/proof/crefine/Syscall_C.thy @@ -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 \ ('b::len) word" + and uc' :: "'b word \ ('c::len) sword" + shows + "\is_up uc; is_up uc'\ \ is_up (uc' \ uc)" + unfolding is_up_def by (simp add: Word.target_size Word.source_size) + + + lemma is_up_compose: + shows + "\is_up uc; is_up uc'\ \ is_up (uc' \ uc)" + unfolding is_up_def by (simp add: Word.target_size Word.source_size) + + lemma uint_is_up_compose: + fixes uc :: "('a::len) word \ ('b::len) word" + and uc' :: "'b word \ ('c::len) sword" + assumes "uc = ucast" + and "uc' = ucast" + and " uuc = uc' \ uc" + shows + "\ is_up uc; is_up uc' \ \ 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 \ ('b::len) word" + and uc' :: "'b word \ ('c::len) sword" + assumes "uc = ucast" + and "uc' = ucast" + and " uuc = uc' \ uc" + shows + "\ is_up uc; is_up uc' \ \ P (uint (uuc b)) \ 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 \ ('b::len) sword" + shows "\uc = ucast; len_of TYPE('a) < len_of TYPE('b) \ \ is_up uc = (\ 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 \ ('b::len) word" + and uc' :: "'b word \ ('c::len) sword" + shows + "\uc = ucast; uc' = ucast; len_of TYPE('a) < len_of TYPE('c)\ \ \ is_down (uc' \ uc) " + unfolding is_down_def + by (simp add: Word.target_size Word.source_size) + + + + + lemma sint_ucast_uint: + fixes uc :: "('a::len) word \ ('b::len) word" + and uc' :: "'b word \ ('c::len) sword" + assumes "uc = ucast" and " uc' = ucast" and "uuc=uc' \ uc " and "len_of TYPE('a) < len_of TYPE('c signed)" + shows + "\ is_up uc; is_up uc'\ \ 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 \ ('b::len) word" + and uc' :: "'b word \ ('c::len) sword" + and uuc :: "'a word \ 'c sword" + assumes "uc = ucast" and " uc' = ucast" and "uuc=uc' \ uc " and "len_of TYPE('a) < len_of TYPE('c )" + shows "\is_up uc; is_up uc'\ \ P (uint b) \ 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 \ ('b::len) word" + and uc' :: "'b word \ ('c::len) sword" + assumes "uc = ucast" and " uc' = ucast" and "uuc=uc' \ uc " and "len_of TYPE('a) < len_of TYPE('c )" + shows "\is_up uc; is_up uc'\ \ P (uint(uuc b)) \ 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 \ 16 word" + and uc' :: "16 word\ 32 sword" + and b :: irq + shows + "(Kernel_C.maxIRQ) (ucast :: irq \ 16 word)) b \ 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) \ uint b"; (simp only: Kernel_C.maxIRQ_def)?) + apply (subgoal_tac "sint (ucast Kernel_C.maxIRQ :: 32 sword) \ uint b"; (simp only: Kernel_C.maxIRQ_def)?) + apply (simp ) + apply (subst uint_is_up_compose[where uc="(ucast :: irq \ 16 word)" and uc' = "(ucast :: 16 word \ 32 sword)",symmetric]; + (simp add: is_up_def target_size source_size )?) + apply fastforce + apply (subst sint_ucast_uint_pred[where uc="(ucast :: irq \ 16 word)" and uc' = "(ucast :: 16 word \ 32 sword)"]; + (simp add: is_up_def target_size source_size )?) + apply fastforce +done + + lemma validIRQcastingLess: "Kernel_C.maxIRQ 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: "(\ (Kernel_C.maxIRQ) (ucast :: irq \ 16 word)) b) \ \ (scast Kernel_C.maxIRQ < b)" + apply (subgoal_tac "sint (ucast Kernel_C.maxIRQ :: 32 sword) \ 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 \ ucast" , simplified]; + (simp add: is_up_def target_size source_size)?) + apply (subst (asm) uint_is_up_compose[where 'b = 16 and uuc="ucast \ 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 \ 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 \ 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 \ 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 \ ucast maxIRQ)) + (invs') (UNIV \ \\irq = ucast irq\) [] (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=\ and P'="{s. ret__int_' s = 0 \ cap_get_tag cap \ 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 diff --git a/proof/drefine/Interrupt_DR.thy b/proof/drefine/Interrupt_DR.thy index ae345143d..9227f80da 100755 --- a/proof/drefine/Interrupt_DR.thy +++ b/proof/drefine/Interrupt_DR.thy @@ -281,6 +281,12 @@ lemma handle_interrupt_corres: "dcorres dc \ (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) diff --git a/proof/infoflow/ADT_IF.thy b/proof/infoflow/ADT_IF.thy index 7b84790d9..4ab616415 100644 --- a/proof/infoflow/ADT_IF.thy +++ b/proof/infoflow/ADT_IF.thy @@ -1132,10 +1132,9 @@ lemma handle_preemption_if_irq_masks: "\(\s. P (irq_masks_of_state s)) and domain_sep_inv False st\ handle_preemption_if tc \\_ s. P (irq_masks_of_state s)\" - apply(simp add: handle_preemption_if_def | wp handle_interrupt_irq_masks)+ - apply(rule_tac Q="\_ s. P (irq_masks_of_state s) \ 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="\rv s. P (irq_masks_of_state s) \ domain_sep_inv False st s \ (\x. rv = Some x \ x \ 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 \ \\s. domain_time s > 0\ handle_interrupt e - \\r s. domain_time s = 0 \ scheduler_action s = choose_new_thread\" - apply(simp add: handle_interrupt_def) + \\r s. domain_time s = 0 \ scheduler_action s = choose_new_thread\" + apply(simp add: handle_interrupt_def split del: split_if) + apply (rule hoare_pre) apply (wp) apply(case_tac "st \ IRQTimer") apply((wp hoare_vcg_imp_lift' | simp | wpc)+)[1] diff --git a/proof/infoflow/FinalCaps.thy b/proof/infoflow/FinalCaps.thy index 73422818e..7e7687720 100644 --- a/proof/infoflow/FinalCaps.thy +++ b/proof/infoflow/FinalCaps.thy @@ -3153,6 +3153,7 @@ lemma handle_recv_silc_inv: lemma handle_interrupt_silc_inv: "\silc_inv aag st\ handle_interrupt irq \\_. silc_inv aag st\" unfolding handle_interrupt_def + apply (rule hoare_if) apply(wp | wpc | simp | wp_once hoare_drop_imps)+ done diff --git a/proof/infoflow/IRQMasks_IF.thy b/proof/infoflow/IRQMasks_IF.thy index eeaf0c029..bd46b213a 100644 --- a/proof/infoflow/IRQMasks_IF.thy +++ b/proof/infoflow/IRQMasks_IF.thy @@ -83,14 +83,18 @@ crunch irq_masks[wp]: machine_op_lift "\s. P (irq_masks s)" lemma handle_interrupt_irq_masks: notes no_irq[wp del] + shows - "\(\s. P (irq_masks_of_state s)) and domain_sep_inv False st\ + "\(\s. P (irq_masks_of_state s)) and domain_sep_inv False st and K (irq \ maxIRQ)\ handle_interrupt irq \\rv s. P (irq_masks_of_state s)\" - 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 "\s. P (irq_masks_of_state s)" @@ -396,12 +400,27 @@ crunch irq_masks[wp]: handle_vm_fault "\s. P (irq_masks_of_state s)" lemma dmo_getActiveIRQ_irq_masks[wp]: "\(\s. P (irq_masks_of_state s))\ do_machine_op getActiveIRQ - \\x s. P (irq_masks_of_state s)\" + \\rv s. P (irq_masks_of_state s) \" 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]: + "\\\ + do_machine_op getActiveIRQ + \(\rv s. (\x. rv = Some x \ x \ maxIRQ)) \" + 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]: "\(\s. P (irq_masks_of_state s)) and domain_sep_inv False st and invs\ handle_yield \\rv s. P (irq_masks_of_state s)\" +lemma handle_yield_irq_masks_of_state[wp]: + "\(\s. P (irq_masks_of_state s)) and domain_sep_inv False st and invs\ + handle_yield + \\rv s. P (irq_masks_of_state s)\" apply (simp add: handle_yield_def) apply wp apply simp @@ -412,9 +431,20 @@ lemma handle_event_irq_masks: handle_event ev \ \ rv s. P (irq_masks_of_state s) \" 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="\rv s. P (irq_masks_of_state s) \ domain_sep_inv False st s \ (\x. rv = Some x \ x \ 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 "\s. P (irq_masks_of_state s)" @@ -428,8 +458,8 @@ lemma call_kernel_irq_masks: \ \ rv s. P (irq_masks_of_state s) \" apply(simp add: call_kernel_def) apply (wp handle_interrupt_irq_masks[where st=st])+ - apply(rule_tac Q="\_ s. P (irq_masks_of_state s) \ domain_sep_inv False st s" in hoare_strengthen_post) - apply(wp | simp)+ + apply (rule_tac Q="\rv s. P (irq_masks_of_state s) \ domain_sep_inv False st s \ (\x. rv = Some x \ x \ maxIRQ)" in hoare_strengthen_post) + apply (wp | simp)+ apply(rule_tac Q="\ x s. P (irq_masks_of_state s) \ 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)+ diff --git a/proof/infoflow/Noninterference.thy b/proof/infoflow/Noninterference.thy index ad9b85783..d4fab35c6 100644 --- a/proof/infoflow/Noninterference.thy +++ b/proof/infoflow/Noninterference.thy @@ -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]: "\\_. True\ getActiveIRQ \\rv s. \x. rv = Some x \ x \ maxIRQ\" + 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: "(\x. y = Some x \ P x) = ((\x. y = Some x) \ 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) (\r r'. r = uc \ 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 (\s. irq_masks_of_state st = irq_masks_of_state s) and (\s. ct_idle s \ 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="\\" and Q'="\\"]) - 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="\\" and Q'="\\"]) + 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: "\\\ 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 (\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 diff --git a/proof/infoflow/Scheduler_IF.thy b/proof/infoflow/Scheduler_IF.thy index 49c8b3b33..bf6d6cb82 100644 --- a/proof/infoflow/Scheduler_IF.thy +++ b/proof/infoflow/Scheduler_IF.thy @@ -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 \ 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 \ 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 \ 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 diff --git a/proof/infoflow/Syscall_IF.thy b/proof/infoflow/Syscall_IF.thy index 4ce2e257b..3978e6ef0 100644 --- a/proof/infoflow/Syscall_IF.thy +++ b/proof/infoflow/Syscall_IF.thy @@ -907,13 +907,20 @@ declare gts_st_tcb_at[wp del] lemma handle_interrupt_globals_equiv: "\globals_equiv (st :: det_ext state) and invs\ handle_interrupt irq \\r. globals_equiv st\" 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 diff --git a/proof/invariant-abstract/Deterministic_AI.thy b/proof/invariant-abstract/Deterministic_AI.thy index f80d2e279..1d7700b17 100644 --- a/proof/invariant-abstract/Deterministic_AI.thy +++ b/proof/invariant-abstract/Deterministic_AI.thy @@ -4117,10 +4117,10 @@ interpretation timer_tick_extended: is_extended "timer_tick" done lemma handle_interrupt_valid_list[wp]: - "\valid_list\ handle_interrupt irq \\_.valid_list\" - unfolding handle_interrupt_def - apply (wp get_cap_wp | wpc | simp add: get_irq_slot_def get_irq_state_def)+ - done + "\valid_list \ handle_interrupt irq \\_.valid_list\" + 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 diff --git a/proof/invariant-abstract/Interrupt_AI.thy b/proof/invariant-abstract/Interrupt_AI.thy index 56c16e6ee..8861869c4 100644 --- a/proof/invariant-abstract/Interrupt_AI.thy +++ b/proof/invariant-abstract/Interrupt_AI.thy @@ -203,13 +203,15 @@ lemma get_irq_slot_ex_cte: apply clarsimp done + lemma maskInterrupt_invs: - "\invs and (\s. interrupt_states s irq \ IRQInactive)\ + "\invs and (\s. \b \ interrupt_states s irq \ IRQInactive)\ do_machine_op (maskInterrupt b irq) \\rv. invs\" 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]: "\invs\ handle_interrupt irq \\_. invs\" - 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="\rv. invs and (\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 \ No newline at end of file diff --git a/proof/invariant-abstract/Syscall_AI.thy b/proof/invariant-abstract/Syscall_AI.thy index e5f997877..6fbe85e6c 100644 --- a/proof/invariant-abstract/Syscall_AI.thy +++ b/proof/invariant-abstract/Syscall_AI.thy @@ -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)+ diff --git a/proof/refine/Interrupt_R.thy b/proof/refine/Interrupt_R.thy index a774d5476..ee2824bde 100644 --- a/proof/refine/Interrupt_R.thy +++ b/proof/refine/Interrupt_R.thy @@ -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 (\s. intStateIRQTable (ksInterruptState s) irq \ 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="\rv. einvs" - and R'="\rv. invs' and (\s. rv \ IRQInactive)"]) + and R'="\rv. invs' and (\s. rv \ 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="\rv. einvs and valid_cap rv" and R'="\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]: "\invs'\ handleInterrupt irq \\rv. invs'\" 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="\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: "\st_tcb_at' runnable' t\ handleInterrupt irq \\_. st_tcb_at' runnable' t\" 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)+ diff --git a/proof/refine/PageTableDuplicates.thy b/proof/refine/PageTableDuplicates.thy index f27a8e738..c01e800ab 100644 --- a/proof/refine/PageTableDuplicates.thy +++ b/proof/refine/PageTableDuplicates.thy @@ -2519,7 +2519,7 @@ lemma handleInterrupt_valid_duplicates'[wp]: "\\s. vs_valid_duplicates' (ksPSpace s)\ handleInterrupt irq \\r s. vs_valid_duplicates' (ksPSpace s)\" 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)+ diff --git a/spec/abstract/Interrupt_A.thy b/spec/abstract/Interrupt_A.thy index 6516a56a7..595b3575e 100644 --- a/spec/abstract/Interrupt_A.thy +++ b/spec/abstract/Interrupt_A.thy @@ -82,22 +82,27 @@ definition timer_tick :: "unit det_ext_monad" where definition handle_interrupt :: "irq \ (unit,'z::state_ext) s_monad" where - "handle_interrupt irq \ do - st \ get_irq_state irq; - case st of - IRQSignal \ do - slot \ get_irq_slot irq; - cap \ get_cap slot; - when (is_ntfn_cap cap \ AllowSend \ cap_rights cap) - $ send_signal (obj_ref_of cap) (cap_ep_badge cap); - do_machine_op $ maskInterrupt True irq + "handle_interrupt irq \ + if (irq > maxIRQ) then do_machine_op $ do + maskInterrupt True irq; + ackInterrupt irq od - | IRQTimer \ do - do_extended_op timer_tick; - do_machine_op resetTimer - od - | IRQInactive \ fail (* not meant to be able to get IRQs from inactive lines *); - do_machine_op $ ackInterrupt irq - od" + else do + st \ get_irq_state irq; + case st of + IRQSignal \ do + slot \ get_irq_slot irq; + cap \ get_cap slot; + when (is_ntfn_cap cap \ AllowSend \ cap_rights cap) + $ send_signal (obj_ref_of cap) (cap_ep_badge cap); + do_machine_op $ maskInterrupt True irq + od + | IRQTimer \ do + do_extended_op timer_tick; + do_machine_op resetTimer + od + | IRQInactive \ fail (* not meant to be able to get IRQs from inactive lines *); + do_machine_op $ ackInterrupt irq + od" end diff --git a/spec/capDL/Interrupt_D.thy b/spec/capDL/Interrupt_D.thy index e688c0969..818b47c66 100644 --- a/spec/capDL/Interrupt_D.thy +++ b/spec/capDL/Interrupt_D.thy @@ -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 \ unit k_monad" where - "handle_interrupt irq \ + "handle_interrupt irq \ if (irq > maxIRQ) then return () else do irq_slot \ gets $ get_irq_slot irq; c \ gets $ opt_cap irq_slot; diff --git a/spec/design/Interrupt_H.thy b/spec/design/Interrupt_H.thy index b01f86a2e..a59216722 100644 --- a/spec/design/Interrupt_H.thy +++ b/spec/design/Interrupt_H.thy @@ -128,28 +128,35 @@ defs initInterruptController_def: odE)" defs handleInterrupt_def: -"handleInterrupt irq\ (do - st \ getIRQState irq; - (case st of - IRQSignal \ (do - slot \ getIRQSlot irq; - cap \ getSlotCap slot; - (case cap of - NotificationCap _ _ True _ \ - sendSignal (capNtfnPtr cap) (capNtfnBadge cap) - | _ \ doMachineOp $ debugPrint $ - [] @ show irq - ); - doMachineOp $ maskInterrupt True irq +"handleInterrupt irq\ ( + if (irq > maxIRQ) then doMachineOp $ ((do + maskInterrupt True irq; + ackInterrupt irq + od) + ) + else (do + st \ getIRQState irq; + (case st of + IRQSignal \ (do + slot \ getIRQSlot irq; + cap \ getSlotCap slot; + (case cap of + NotificationCap _ _ True _ \ + sendSignal (capNtfnPtr cap) (capNtfnBadge cap) + | _ \ doMachineOp $ debugPrint $ + [] @ show irq + ); + doMachineOp $ maskInterrupt True irq + od) + | IRQTimer \ (do + timerTick; + doMachineOp resetTimer od) - | IRQTimer \ (do - timerTick; - doMachineOp resetTimer - od) - | IRQInactive \ haskell_fail $ [] @ show irq - ); - doMachineOp $ ackInterrupt irq -od)" + | IRQInactive \ haskell_fail $ [] @ show irq + ); + doMachineOp $ ackInterrupt irq + od) +)" defs isIRQActive_def: "isIRQActive irq\ liftM (\x. x \IRQInactive) $ getIRQState irq" diff --git a/spec/design/m-skel/ARM/MachineTypes.thy b/spec/design/m-skel/ARM/MachineTypes.thy index 1407a663a..222d29970 100644 --- a/spec/design/m-skel/ARM/MachineTypes.thy +++ b/spec/design/m-skel/ARM/MachineTypes.thy @@ -67,6 +67,9 @@ record consts irq_oracle :: "nat \ 10 word" +axiomatization irq_oracle_max_irqInst where + irq_oracle_max_irq: "\ n. (irq_oracle n) <= maxIRQ" + text {* The machine monad is used for operations on the state defined above. *} diff --git a/spec/design/version b/spec/design/version index a6e3183ba..32ad60825 100644 --- a/spec/design/version +++ b/spec/design/version @@ -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 diff --git a/spec/machine/ARM/MachineTypes.thy b/spec/machine/ARM/MachineTypes.thy index b0b4109d6..73c14d67c 100644 --- a/spec/machine/ARM/MachineTypes.thy +++ b/spec/machine/ARM/MachineTypes.thy @@ -181,6 +181,9 @@ record consts irq_oracle :: "nat \ 10 word" +axiomatization irq_oracle_max_irqInst where + irq_oracle_max_irq: "\ n. (irq_oracle n) <= maxIRQ" + text {* The machine monad is used for operations on the state defined above. *}