1(* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(GD_GPL) 9 *) 10 11theory InterruptAcc_R 12imports TcbAcc_R 13begin 14 15lemma get_irq_slot_corres: 16 "corres (\<lambda>sl sl'. sl' = cte_map sl) \<top> \<top> (get_irq_slot irq) (getIRQSlot irq)" 17 apply (simp add: getIRQSlot_def get_irq_slot_def locateSlot_conv 18 liftM_def[symmetric]) 19 apply (simp add: getInterruptState_def) 20 apply (clarsimp simp: state_relation_def interrupt_state_relation_def) 21 apply (simp add: cte_map_def cte_level_bits_def 22 ucast_nat_def shiftl_t2n) 23 done 24 25crunch inv[wp]: get_irq_slot "P" 26crunch inv[wp]: getIRQSlot "P" 27 28context begin interpretation Arch . (*FIXME: arch_split*) 29 30lemma set_irq_state_corres: 31 "irq_state_relation state state' \<Longrightarrow> 32 corres dc \<top> \<top> (set_irq_state state irq) (setIRQState state' irq)" 33 apply (simp add: set_irq_state_def setIRQState_def 34 bind_assoc[symmetric]) 35 apply (subgoal_tac "(state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive)") 36 apply (rule corres_guard_imp) 37 apply (rule corres_split_nor) 38 apply (rule corres_machine_op) 39 apply (rule corres_Id | simp)+ 40 apply (rule no_fail_maskInterrupt) 41 apply (simp add: getInterruptState_def setInterruptState_def 42 simpler_gets_def simpler_modify_def bind_def) 43 apply (simp add: simpler_modify_def[symmetric]) 44 apply (rule corres_trivial, rule corres_modify) 45 apply (simp add: state_relation_def swp_def) 46 apply (clarsimp simp: interrupt_state_relation_def) 47 apply (wp | simp)+ 48 apply (clarsimp simp: irq_state_relation_def 49 split: irq_state.split_asm irqstate.split_asm) 50 done 51 52lemma setIRQState_invs[wp]: 53 "\<lbrace>\<lambda>s. invs' s \<and> (state \<noteq> IRQSignal \<longrightarrow> IRQHandlerCap irq \<notin> ran (cteCaps_of s)) \<and> (state \<noteq> IRQInactive \<longrightarrow> irq \<le> maxIRQ)\<rbrace> 54 setIRQState state irq 55 \<lbrace>\<lambda>rv. invs'\<rbrace>" 56 apply (simp add: setIRQState_def setInterruptState_def getInterruptState_def) 57 apply (wp dmo_maskInterrupt) 58 apply (clarsimp simp: invs'_def valid_state'_def cur_tcb'_def 59 Invariants_H.valid_queues_def valid_queues'_def 60 valid_idle'_def valid_irq_node'_def 61 valid_arch_state'_def valid_global_refs'_def 62 global_refs'_def valid_machine_state'_def 63 if_unsafe_then_cap'_def ex_cte_cap_to'_def 64 valid_irq_handlers'_def irq_issued'_def 65 cteCaps_of_def valid_irq_masks'_def 66 bitmapQ_defs valid_queues_no_bitmap_def) 67 apply (rule conjI, clarsimp) 68 apply (clarsimp simp: irqs_masked'_def ct_not_inQ_def) 69 apply (rule conjI) 70 apply fastforce 71 apply (simp add: ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def) 72 done 73 74lemma getIRQSlot_real_cte[wp]: 75 "\<lbrace>invs'\<rbrace> getIRQSlot irq \<lbrace>real_cte_at'\<rbrace>" 76 apply (simp add: getIRQSlot_def getInterruptState_def locateSlot_conv) 77 apply wp 78 apply (clarsimp simp: invs'_def valid_state'_def valid_irq_node'_def 79 cte_level_bits_def ucast_nat_def) 80 done 81 82lemma getIRQSlot_cte_at[wp]: 83 "\<lbrace>invs'\<rbrace> getIRQSlot irq \<lbrace>cte_at'\<rbrace>" 84 apply (rule hoare_strengthen_post [OF getIRQSlot_real_cte]) 85 apply (clarsimp simp: real_cte_at') 86 done 87 88lemma work_units_updated_state_relationI[intro!]: 89 "(s,s') \<in> state_relation \<Longrightarrow> 90 (work_units_completed_update (\<lambda>_. work_units_completed s + 1) s, s'\<lparr>ksWorkUnitsCompleted := ksWorkUnitsCompleted s' + 1\<rparr>) \<in> state_relation" 91 apply (simp add: state_relation_def) 92 done 93 94lemma work_units_and_irq_state_state_relationI [intro!]: 95 "(s, s') \<in> state_relation \<Longrightarrow> 96 (s \<lparr> work_units_completed := n, machine_state := machine_state s \<lparr> irq_state := f (irq_state (machine_state s)) \<rparr>\<rparr>, 97 s' \<lparr> ksWorkUnitsCompleted := n, ksMachineState := ksMachineState s' \<lparr> irq_state := f (irq_state (ksMachineState s')) \<rparr>\<rparr>) 98 \<in> state_relation" 99 by (simp add: state_relation_def swp_def) 100 101lemma preemption_corres: 102 "corres (intr \<oplus> dc) \<top> \<top> preemption_point preemptionPoint" 103 apply (simp add: preemption_point_def preemptionPoint_def) 104 by (auto simp: preemption_point_def preemptionPoint_def o_def gets_def liftE_def whenE_def getActiveIRQ_def 105 corres_underlying_def select_def bind_def get_def bindE_def select_f_def modify_def 106 alternative_def throwError_def returnOk_def return_def lift_def doMachineOp_def split_def 107 put_def getWorkUnits_def setWorkUnits_def modifyWorkUnits_def do_machine_op_def 108 109 update_work_units_def wrap_ext_bool_det_ext_ext_def work_units_limit_def workUnitsLimit_def 110 work_units_limit_reached_def OR_choiceE_def reset_work_units_def mk_ef_def 111 elim: state_relationE) 112 (* what? *) 113 (* who says our proofs are not automatic.. *) 114 115lemma preemptionPoint_inv: 116 assumes "(\<And>f s. P (ksWorkUnitsCompleted_update f s) = P s)" 117 "irq_state_independent_H P" 118 shows "\<lbrace>P\<rbrace> preemptionPoint \<lbrace>\<lambda>_. P\<rbrace>" using assms 119 apply (simp add: preemptionPoint_def setWorkUnits_def getWorkUnits_def modifyWorkUnits_def) 120 apply (wpc 121 | wp hoare_whenE_wp hoare_seq_ext [OF _ select_inv] alternative_valid hoare_drop_imps 122 | simp)+ 123 done 124 125lemma invs'_wu [simp, intro!]: 126 "invs' (ksWorkUnitsCompleted_update f s) = invs' s" 127 apply (simp add: invs'_def cur_tcb'_def valid_state'_def Invariants_H.valid_queues_def 128 valid_queues'_def valid_irq_node'_def valid_machine_state'_def 129 ct_not_inQ_def ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def 130 bitmapQ_defs valid_queues_no_bitmap_def) 131 done 132 133lemma ct_in_state'_irq_state_independent [simp, intro!]: 134 "ct_in_state' x (s\<lparr>ksMachineState := ksMachineState s 135 \<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>) = 136 ct_in_state' x s" 137 by (simp add: ct_in_state'_def irq_state_independent_H_def)+ 138 139lemma ex_cte_cap_wp_to'_irq_state_independent [simp, intro!]: 140 "ex_cte_cap_wp_to' x y (s\<lparr>ksMachineState := ksMachineState s 141 \<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>) = 142 ex_cte_cap_wp_to' x y s" 143 by (simp add: ex_cte_cap_wp_to'_def irq_state_independent_H_def)+ 144 145lemma ps_clear_irq_state_independent [simp, intro!]: 146 "ps_clear a b (s\<lparr>ksMachineState := ksMachineState s 147 \<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>) = 148 ps_clear a b s" 149 by (simp add: ps_clear_def) 150 151lemma invs'_irq_state_independent [simp, intro!]: 152 "invs' (s\<lparr>ksMachineState := ksMachineState s 153 \<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>) = 154 invs' s" 155 apply (clarsimp simp: irq_state_independent_H_def invs'_def valid_state'_def 156 valid_pspace'_def sch_act_wf_def 157 valid_queues_def sym_refs_def state_refs_of'_def 158 if_live_then_nonz_cap'_def if_unsafe_then_cap'_def 159 valid_idle'_def valid_global_refs'_def 160 valid_arch_state'_def valid_irq_node'_def 161 valid_irq_handlers'_def valid_irq_states'_def 162 irqs_masked'_def bitmapQ_defs valid_queues_no_bitmap_def 163 valid_queues'_def valid_pde_mappings'_def 164 pspace_domain_valid_def cur_tcb'_def 165 valid_machine_state'_def tcb_in_cur_domain'_def 166 ct_not_inQ_def ct_idle_or_in_cur_domain'_def 167 cong: if_cong option.case_cong) 168 apply (rule iffI[rotated]) 169 apply (clarsimp) 170 apply (case_tac "ksSchedulerAction s", simp_all) 171 apply clarsimp 172 apply (case_tac "ksSchedulerAction s", simp_all) 173 done 174 175lemma preemptionPoint_invs [wp]: 176 "\<lbrace>invs'\<rbrace> preemptionPoint \<lbrace>\<lambda>_. invs'\<rbrace>" 177 by (wp preemptionPoint_inv | clarsimp)+ 178 179end 180end 181