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