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

l4v-sabre: change type of irq to be 10 word

This commit is contained in:
Gao Xin 2016-02-05 16:16:16 +11:00 committed by Xin,Gao
parent 50fa257113
commit bc73b112bd
39 changed files with 353 additions and 192 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
proof/access-control/Access.thy
View File

@ -36,7 +36,7 @@ the grant bit set.
type_synonym 'a agent_map = "obj_ref \<Rightarrow> 'a"
type_synonym 'a agent_asid_map = "asid \<Rightarrow> 'a"
type_synonym 'a agent_irq_map = "word8 \<Rightarrow> 'a"
type_synonym 'a agent_irq_map = "10 word \<Rightarrow> 'a"
text{*

9
proof/access-control/Arch_AC.thy
View File

@ -1093,8 +1093,12 @@ lemma pageBitsForSize_le_t28:
"pageBitsForSize sz \<le> 28"
by (cases sz, simp_all)
lemma pageBitsForSize_le_t29:
"pageBitsForSize sz \<le> 29"
by (cases sz, simp_all)
lemmas vmsz_aligned_t2n_neg_mask
= x_t2n_sub_1_neg_mask[OF _ pageBitsForSize_le_t28, folded vmsz_aligned_def]
= x_t2n_sub_1_neg_mask[OF _ pageBitsForSize_le_t29, folded vmsz_aligned_def]
lemma decode_arch_invocation_authorised:
@ -1153,7 +1157,8 @@ lemma decode_arch_invocation_authorised:
validate_vm_rights_def vm_read_write_def vm_read_only_def
vm_kernel_only_def)
-- "Remap"
apply (clarsimp simp: cap_auth_conferred_def is_page_cap_def pas_refined_all_auth_is_owns)
apply (clarsimp simp: cap_auth_conferred_def
is_page_cap_def pas_refined_all_auth_is_owns)
apply (rule conjI, fastforce)
apply clarsimp
apply (drule (1) bspec)

6
proof/crefine/ADT_C.thy
View File

@ -178,7 +178,7 @@ definition
where
"checkActiveIRQ_C \<equiv>
do getActiveIRQ_C;
irq \<leftarrow> gets ret__unsigned_long_';
irq \<leftarrow> gets ret__unsigned_short_';
return (irq \<noteq> scast irqInvalid)
od"
@ -282,7 +282,7 @@ lemma cirqstate_cancel:
definition
"cint_state_to_H cnode cirqs \<equiv>
InterruptState (ptr_val cnode)
(\<lambda>i::word8. if i \<le> scast Platform.maxIRQ then cirqstate_to_H (index cirqs (unat i))
(\<lambda>i::10 word. if i \<le> scast Platform.maxIRQ then cirqstate_to_H (index cirqs (unat i))
else irqstate.IRQInactive)"
lemma cint_rel_to_H:
@ -1545,7 +1545,7 @@ definition
definition
"checkActiveIRQ_C \<equiv>
do getActiveIRQ_C;
irq \<leftarrow> gets ret__unsigned_long_';
irq \<leftarrow> gets ret__unsigned_short_';
return (irq \<noteq> scast irqInvalid)
od"

13
proof/crefine/Arch_C.thy
View File

@ -746,7 +746,7 @@ lemma decodeARMPageTableInvocation_ccorres:
apply (simp add: if_to_top_of_bind del: Collect_const)
apply (rule ccorres_if_cond_throws[rotated -1, where Q=\<top> and Q'=\<top>])
apply vcg
apply (simp add: kernelBase_def hd_conv_nth length_ineq_not_Nil)
apply (simp add: kernelBase_def Platform.kernelBase_def hd_conv_nth length_ineq_not_Nil)
apply (simp add: throwError_bind invocationCatch_def)
apply (rule syscall_error_throwError_ccorres_n)
apply (simp add: syscall_error_to_H_cases)
@ -1195,7 +1195,8 @@ lemma lookupPTSlot_le_0x3C:
apply simp
apply (simp add: Platform.ptrFromPAddr_def physMappingOffset_def)
apply (erule aligned_add_aligned)
apply (simp add: kernelBase_addr_def physBase_def is_aligned_def)
apply (simp add: kernelBase_addr_def Platform.physBase_def
physBase_def is_aligned_def)
apply (simp add: word_bits_def)
done
@ -1445,7 +1446,7 @@ lemma obj_at_pte_aligned:
lemma addrFromPPtr_mask_5:
"addrFromPPtr ptr && mask (5\<Colon>nat) = ptr && mask (5\<Colon>nat)"
apply (simp add:addrFromPPtr_def physMappingOffset_def
kernelBase_addr_def physBase_def)
kernelBase_addr_def physBase_def Platform.physBase_def)
apply word_bitwise
apply (simp add:mask_def)
done
@ -2184,7 +2185,7 @@ lemma vmsz_aligned_addrFromPPtr':
apply (erule(1) aligned_sub_aligned)
apply (simp add: pageBitsForSize_def word_bits_def split: vmpage_size.split)
apply (simp add: pageBitsForSize_def physMappingOffset_def kernelBase_addr_def
physBase_def is_aligned_def
physBase_def Platform.physBase_def is_aligned_def
split: vmpage_size.split)
done
@ -3079,7 +3080,7 @@ lemma decodeARMFrameInvocation_ccorres:
apply (rule ccorres_if_cond_throws[rotated -1, where Q=\<top> and Q'=\<top>])
apply vcg
apply (frule ccap_relation_PageCap_generics)
apply (clarsimp simp add: kernelBase_def word_le_nat_alt)
apply (clarsimp simp add: kernelBase_def Platform.kernelBase_def word_le_nat_alt)
apply (simp add: throwError_bind invocationCatch_def)?
apply (rule syscall_error_throwError_ccorres_n)
apply (simp add: syscall_error_to_H_cases)
@ -3489,7 +3490,7 @@ lemma decodeARMPageDirectoryInvocation_ccorres:
apply (simp add: syscall_error_to_H_cases)
apply (rule ccorres_if_cond_throws[rotated -1, where Q=\<top> and Q'=\<top>])
apply vcg
apply (clarsimp simp: hd_conv_nth length_ineq_not_Nil kernelBase_def)
apply (clarsimp simp: hd_conv_nth length_ineq_not_Nil kernelBase_def Platform.kernelBase_def)
apply (simp add:injection_handler_throwError)
apply (rule syscall_error_throwError_ccorres_n)
apply (simp add: syscall_error_to_H_cases)

16
proof/crefine/CSpace_C.thy
View File

@ -2222,20 +2222,21 @@ done
definition
irq_opt_relation_def:
"irq_opt_relation (airq :: word8 option) (cirq :: word16) \<equiv>
"irq_opt_relation (airq :: (10 word) option) (cirq :: word16) \<equiv>
case airq of
Some irq \<Rightarrow> (cirq = ucast irq \<and> irq \<noteq> scast irqInvalid \<and> ucast irq \<le> (scast maxIRQ :: word16))
| None \<Rightarrow> cirq = scast irqInvalid"
lemma unat_ucast_8_16:
fixes x :: "word8"
shows "unat (ucast x :: word16) = unat x"
lemma unat_ucast_up_simp[simp]:
fixes x :: "'a::len word"
assumes uc :"len_of TYPE('a) \<le> len_of TYPE('b)"
shows "unat (ucast x :: 'b::len word) = unat x"
unfolding ucast_def unat_def
apply (subst int_word_uint)
apply (subst mod_pos_pos_trivial)
apply simp
apply (rule lt2p_lem)
apply simp
apply (simp add: uc)
apply simp
done
@ -2315,7 +2316,7 @@ show ?thesis
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
carch_state_relation_def cmachine_state_relation_def)
apply (simp add: cinterrupt_relation_def maxIRQ_def)
apply (clarsimp simp: unat_ucast_8_16 word_sless_msb_less order_le_less_trans
apply (clarsimp simp: word_sless_msb_less order_le_less_trans
unat_ucast_no_overflow_le word_le_nat_alt ucast_ucast_b
split: split_if )
apply (rule word_0_sle_from_less)
@ -3399,12 +3400,15 @@ lemma sameRegionAs_spec:
apply (frule_tac cap'=cap_b in cap_get_tag_isCap_unfolded_H_cap(5))
apply (simp add: ccap_relation_def map_option_case)
apply (simp add: cap_irq_handler_cap_lift)
thm cap_to_H_def
thm cl_valid_cap_def
apply (simp add: cap_to_H_def)
apply (clarsimp simp: up_ucast_inj_eq c_valid_cap_def
cl_valid_cap_def mask_twice
split: split_if bool.split
| intro impI conjI
| simp )+
thm ucast_ucast_mask_eq
apply (drule ucast_ucast_mask_eq, simp)
apply (simp add: ucast_ucast_mask)
apply (erule ucast_up_neq,simp)

22
proof/crefine/Finalise_C.thy
View File

@ -1766,7 +1766,7 @@ lemma of_int_uint_ucast:
lemma getIRQSlot_ccorres_stuff:
"\<lbrakk> (s, s') \<in> rf_sr \<rbrakk> \<Longrightarrow>
CTypesDefs.ptr_add (intStateIRQNode_' (globals s')) (uint (irq :: word8))
CTypesDefs.ptr_add (intStateIRQNode_' (globals s')) (uint (irq :: 10 word))
= Ptr (irq_node' s + 2 ^ cte_level_bits * ucast irq)"
apply (clarsimp simp add: rf_sr_def cstate_relation_def Let_def
cinterrupt_relation_def)
@ -1774,7 +1774,7 @@ lemma getIRQSlot_ccorres_stuff:
size_of_def mult.commute mult.left_commute of_int_uint_ucast )
done
declare[[show_types]]
lemma deletingIRQHandler_ccorres:
"ccorres dc xfdc (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s))
(UNIV \<inter> {s. irq_opt_relation (Some irq) (irq_' s)}) []
@ -1809,10 +1809,10 @@ lemma deletingIRQHandler_ccorres:
apply (clarsimp simp: cap_get_tag_isCap ghost_assertion_data_get_def
ghost_assertion_data_set_def)
apply (simp add: cap_tag_defs)
apply (cut_tac x=irq in unat_lt2p)
apply (clarsimp simp: cte_wp_at_ctes_of Collect_const_mem
irq_opt_relation_def maxIRQ_def uint_0_iff
unat_gt_0 uint_up_ucast is_up unat_def[symmetric])
irq_opt_relation_def maxIRQ_def)
apply (drule word_le_nat_alt[THEN iffD1])
apply (clarsimp simp:uint_0_iff unat_gt_0 uint_up_ucast is_up unat_def[symmetric])
done
lemma Zombie_new_spec:
@ -1836,12 +1836,12 @@ lemma mod_mask_drop:
word_bw_assocs)
lemma irq_opt_relation_Some_ucast:
"\<lbrakk> x && mask 8 = x; ucast x \<le> (scast Kernel_C.maxIRQ :: word8) \<or> x \<le> (scast Kernel_C.maxIRQ :: word32) \<rbrakk>
\<Longrightarrow> irq_opt_relation (Some (ucast x)) (ucast ((ucast x)::word8))"
using ucast_ucast_mask[where x=x and 'a=8, symmetric]
"\<lbrakk> x && mask 10 = x; ucast x \<le> (scast Kernel_C.maxIRQ :: 10 word) \<or> x \<le> (scast Kernel_C.maxIRQ :: word32) \<rbrakk>
\<Longrightarrow> irq_opt_relation (Some (ucast x)) (ucast ((ucast x):: 10 word))"
using ucast_ucast_mask[where x=x and 'a=10, symmetric]
apply (simp add: irq_opt_relation_def)
apply (rule conjI, clarsimp simp: irqInvalid_def Kernel_C.maxIRQ_def)
apply (simp only: unat_arith_simps unat_ucast_8_16)
apply (simp only: unat_arith_simps )
apply (clarsimp simp: word_le_nat_alt Kernel_C.maxIRQ_def)
done
@ -1864,7 +1864,7 @@ lemma mask_eq_ucast_eq:
done
lemma irq_opt_relation_Some_ucast':
"\<lbrakk> x && mask 8 = x; ucast x \<le> (scast Kernel_C.maxIRQ :: word8) \<or> x \<le> (scast Kernel_C.maxIRQ :: word32) \<rbrakk>
"\<lbrakk> x && mask 10 = x; ucast x \<le> (scast Kernel_C.maxIRQ :: 10 word) \<or> x \<le> (scast Kernel_C.maxIRQ :: word32) \<rbrakk>
\<Longrightarrow> irq_opt_relation (Some (ucast x)) (ucast x)"
apply (rule_tac P = "%y. irq_opt_relation (Some (ucast x)) y" in subst[rotated])
apply (rule irq_opt_relation_Some_ucast[rotated])
@ -1876,7 +1876,7 @@ done
lemma ccap_relation_IRQHandler_mask:
"\<lbrakk> ccap_relation acap ccap; isIRQHandlerCap acap \<rbrakk>
\<Longrightarrow> capIRQ_CL (cap_irq_handler_cap_lift ccap) && mask 8
\<Longrightarrow> capIRQ_CL (cap_irq_handler_cap_lift ccap) && mask 10
= capIRQ_CL (cap_irq_handler_cap_lift ccap)"
apply (simp only: cap_get_tag_isCap[symmetric])
apply (drule ccap_relation_c_valid_cap)

94
proof/crefine/Interrupt_C.thy
View File

@ -26,7 +26,8 @@ lemma invokeIRQHandler_AckIRQ_ccorres:
lemma getIRQSlot_ccorres:
"ccorres (op = \<circ> Ptr) irqSlot_'
\<top> UNIV hs
(getIRQSlot irq) (\<acute>irqSlot :== CTypesDefs.ptr_add \<acute>intStateIRQNode (uint (ucast irq :: word32)))"
(getIRQSlot irq)
(\<acute>irqSlot :== CTypesDefs.ptr_add \<acute>intStateIRQNode (sint (ucast (ucast irq ::word16) :: 32 signed word)))"
apply (rule ccorres_from_vcg[where P=\<top> and P'=UNIV])
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: getIRQSlot_def liftM_def getInterruptState_def
@ -34,19 +35,35 @@ lemma getIRQSlot_ccorres:
apply (simp add: simpler_gets_def bind_def return_def)
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
cinterrupt_relation_def size_of_def
sint_ucast_eq_uint is_down of_int_uint_ucast
cte_level_bits_def mult.commute mult.left_commute ucast_nat_def
)
apply (simp add:ucast_up_ucast is_up)
done
lemma ptr_add_assertion_irq_guard:
"ccorres dc xfdc P Q hs a
(Guard F
\<lbrace>uint irq = 0 \<or> array_assertion \<acute>intStateIRQNode (nat (uint irq)) (hrs_htd \<acute>t_hrs)\<rbrace>
c;;m)
\<Longrightarrow> ccorres dc xfdc P Q hs a
(Guard F
\<lbrace>ptr_add_assertion \<acute>intStateIRQNode
(sint (ucast (irq :: 16 word)::32 signed word)) False
(hrs_htd \<acute>t_hrs)\<rbrace> c ;; m)"
by (simp add: ptr_add_assertion_def sint_ucast_eq_uint is_down)
lemma cte_at_irq_node':
"invs' s \<Longrightarrow>
cte_at' (irq_node' s + 2 ^ cte_level_bits * ucast (irq :: 8 word)) s"
cte_at' (irq_node' s + 2 ^ cte_level_bits * ucast (irq :: 10 word)) s"
by (clarsimp simp: invs'_def valid_state'_def valid_irq_node'_def
cte_level_bits_def real_cte_at')
lemma invokeIRQHandler_SetIRQHandler_ccorres:
"ccorres dc xfdc
(invs' and sch_act_simple and irq_handler_inv_valid' (SetIRQHandler irq cp slot))
(invs' and sch_act_simple
and irq_handler_inv_valid' (SetIRQHandler irq cp slot))
(UNIV \<inter> {s. irq_' s = ucast irq} \<inter> {s. slot_' s = Ptr slot}
\<inter> {s. ccap_relation cp (cap_' s)}) []
(invokeIRQHandler (SetIRQHandler irq cp slot))
@ -56,6 +73,7 @@ proof -
by (clarsimp)
show ?thesis
apply (cinit lift: irq_' slot_' cap_')
apply (rule ptr_add_assertion_irq_guard)
apply (rule ccorres_move_array_assertion_irq)
apply (simp only:)
apply (ctac(no_vcg) add: getIRQSlot_ccorres)
@ -75,19 +93,23 @@ proof -
apply (simp add: guard_is_UNIV_def ghost_assertion_data_get_def
ghost_assertion_data_set_def)
apply (clarsimp simp: cte_at_irq_node' ucast_nat_def)
apply (cut_tac x=irq in unat_lt2p)
apply (clarsimp simp: invs_pspace_aligned' cte_wp_at_ctes_of badge_derived'_def
Collect_const_mem unat_gt_0)
apply (drule valid_globals_ex_cte_cap_irq[where irq=irq], auto)
Collect_const_mem unat_gt_0 valid_cap_simps' Platform.maxIRQ_def)
apply (drule word_le_nat_alt[THEN iffD1])
apply (clarsimp simp:uint_0_iff unat_gt_0 uint_up_ucast is_up unat_def[symmetric])
apply (drule valid_globals_ex_cte_cap_irq[where irq=irq])
apply (auto simp add:Word.uint_up_ucast is_up unat_def[symmetric])
done
qed
lemma invokeIRQHandler_ClearIRQHandler_ccorres:
"ccorres dc xfdc
(invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) (UNIV \<inter> {s. irq_' s = ucast irq}) []
(invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and K(irq \<le> 0xFF))
(UNIV \<inter> {s. irq_' s = ucast irq}) []
(invokeIRQHandler (ClearIRQHandler irq))
(Call invokeIRQHandler_ClearIRQHandler_'proc)"
apply (cinit lift: irq_')
apply (rule ptr_add_assertion_irq_guard)
apply (rule ccorres_move_array_assertion_irq)
apply (simp only: )
apply (ctac(no_vcg) add: getIRQSlot_ccorres)
@ -102,8 +124,8 @@ lemma invokeIRQHandler_ClearIRQHandler_ccorres:
apply (simp add: guard_is_UNIV_def ghost_assertion_data_get_def
ghost_assertion_data_set_def)
apply (clarsimp simp: cte_at_irq_node' ucast_nat_def)
apply (cut_tac x=irq in unat_lt2p)
apply (clarsimp simp: Collect_const_mem unat_gt_0)
apply (drule word_le_nat_alt[THEN iffD1])
apply (auto simp add:Word.uint_up_ucast is_up unat_def[symmetric])
done
lemma ntfn_case_can_send:
@ -245,12 +267,30 @@ lemma decodeIRQHandlerInvocation_ccorres:
mask_def[where n=4]
"StrictC'_thread_state_defs")
apply (subst pred_tcb'_weakenE, assumption, fastforce)+
apply (clarsimp simp: rf_sr_ksCurThread word_sle_def word_sless_def sysargs_rel_n_def word_less_nat_alt)
by (auto simp: cte_wp_at_ctes_of neq_Nil_conv sysargs_rel_def n_msgRegisters_def
apply (clarsimp simp: rf_sr_ksCurThread word_sle_def word_sless_def
sysargs_rel_n_def word_less_nat_alt)
apply (clarsimp simp: cte_wp_at_ctes_of neq_Nil_conv sysargs_rel_def n_msgRegisters_def
excaps_map_def excaps_in_mem_def word_less_nat_alt hd_conv_nth
slotcap_in_mem_def valid_tcb_state'_def from_bool_def toBool_def
dest!: interpret_excaps_eq split: bool.splits,
auto dest: st_tcb_at_idle_thread' ctes_of_valid')
dest!: interpret_excaps_eq split: bool.splits)
apply (intro conjI impI allI)
apply (clarsimp simp: cte_wp_at_ctes_of neq_Nil_conv sysargs_rel_def n_msgRegisters_def
excaps_map_def excaps_in_mem_def word_less_nat_alt hd_conv_nth
slotcap_in_mem_def valid_tcb_state'_def from_bool_def toBool_def
dest!: interpret_excaps_eq split: bool.splits)+
apply (auto dest: st_tcb_at_idle_thread' ctes_of_valid')[4]
apply (drule ctes_of_valid')
apply fastforce
apply (clarsimp simp add:valid_cap_simps' Platform.maxIRQ_def)
apply (erule order.trans,simp)
apply (auto dest: st_tcb_at_idle_thread' ctes_of_valid')
done
lemma mask_of_mask[simp]:
"mask (n\<Colon>nat) && mask (m\<Colon>nat) = mask (min m n)"
apply (rule word_eqI)
apply (auto simp:word_size)
done
lemma invokeIRQControl_ccorres:
"ccorres (K (K \<bottom>) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
@ -272,22 +312,36 @@ lemma invokeIRQControl_ccorres:
apply (vcg exspec=setIRQState_modifies)
apply (rule conjI)
apply (clarsimp simp: is_simple_cap'_def isCap_simps valid_cap_simps' capAligned_def)
apply (subst ucast_le_ucast_8_32[symmetric])
apply (auto simp:Platform.maxIRQ_def maxIRQ_def word_bits_def)[1]
apply (subst ucast_le_ucast[where 'a = 16 and 'b = 32,symmetric],simp)
apply (subst ucast_le_ucast_10_32[symmetric])
apply (auto simp:ucast_up_ucast is_up Platform.maxIRQ_def maxIRQ_def word_bits_def )[1]
apply (clarsimp simp: Collect_const_mem ccap_relation_def cap_irq_handler_cap_lift
cap_to_H_def c_valid_cap_def cl_valid_cap_def
word_bw_assocs)
word_bw_assocs mask_twice Kernel_C.maxIRQ_def ucast_ucast_a
is_up ucast_ucast_b is_down)
apply (subst less_mask_eq)
apply (rule le_m1_iff_lt[THEN iffD1,THEN iffD1])
apply simp
apply (erule order.trans,simp)
apply (rule word_eqI)
apply (simp add: nth_ucast word_size)
done
lemma unat_ucast_16_32:
"unat (ucast (x::(16 word))::32 signed word) = unat x"
apply (subst unat_ucast)
apply (rule mod_less)
apply (rule less_le_trans[OF unat_lt2p])
apply simp
done
lemma isIRQActive_ccorres:
"ccorres (\<lambda>rv rv'. rv' = from_bool rv) ret__unsigned_long_'
(\<lambda>s. irq \<le> scast maxIRQ) (UNIV \<inter> {s. irq_' s = ucast irq}) []
(isIRQActive irq) (Call isIRQActive_'proc)"
apply (cinit lift: irq_')
apply (simp add: getIRQState_def getInterruptState_def)
apply (rule_tac P="irq \<le> scast maxIRQ" in ccorres_gen_asm)
apply (rule_tac P="irq \<le> scast maxIRQ \<and> unat irq < (160\<Colon>nat)" in ccorres_gen_asm)
apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV])
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: simpler_gets_def word_sless_msb_less maxIRQ_def
@ -296,6 +350,7 @@ lemma isIRQActive_ccorres:
word_0_sle_from_less[OF order_less_le_trans, OF ucast_less])
apply (clarsimp simp: rf_sr_def cstate_relation_def maxIRQ_def
Let_def cinterrupt_relation_def)
apply (drule spec, drule(1) mp)
apply (case_tac "intStateIRQTable (ksInterruptState \<sigma>) irq")
apply (simp add: from_bool_def irq_state_defs maxIRQ_def
@ -332,7 +387,7 @@ lemma liftME_invocationCatch:
done
lemma maxIRQ_ucast_scast [simp]:
"ucast (scast Kernel_C.maxIRQ :: word8) = scast Kernel_C.maxIRQ"
"ucast (scast Kernel_C.maxIRQ :: 10 word) = scast Kernel_C.maxIRQ"
by (clarsimp simp: Kernel_C.maxIRQ_def)
lemma decodeIRQ_arch_helper: "x \<noteq> invocation_label.IRQIssueIRQHandler \<Longrightarrow>
@ -427,6 +482,7 @@ lemma decodeIRQControlInvocation_ccorres:
ucast_nat_def word_le_nat_alt[symmetric]
linorder_not_le[symmetric] Platform_maxIRQ
length_ineq_not_Nil hd_conv_nth cast_simps
maxIRQ_ucast_scast
del: Collect_const cong: call_ignore_cong)
apply (simp add: split_def invocationCatch_use_injection_handler injection_handler_bindE
bindE_assoc
@ -538,7 +594,7 @@ lemma decodeIRQControlInvocation_ccorres:
rightsFromWord_wordFromRights)
apply (simp cong: conj_cong)
apply (simp add: Kernel_C.maxIRQ_def toEnum_of_nat word_le_nat_alt
ucast_nat_def ucast_ucast_mask
ucast_nat_def ucast_ucast_mask mask_eq_ucast_eq
less_mask_eq[unfolded word_less_nat_alt])
done

14
proof/crefine/Machine_C.thy
View File

@ -19,13 +19,13 @@ imports "../../lib/clib/Ctac"
begin
locale kernel_m = kernel +
(*
assumes configureTimer_ccorres:
"ccorres (op =) ret__unsigned_char_'
\<top> UNIV []
(doMachineOp configureTimer)
(Call configureTimer_'proc)"
*)
assumes resetTimer_ccorres:
"ccorres dc xfdc \<top> UNIV []
(doMachineOp resetTimer)
@ -152,10 +152,12 @@ assumes getFAR_ccorres:
(Call getFAR_'proc)"
assumes getActiveIRQ_ccorres:
"ccorres (\<lambda>a c. case a of None \<Rightarrow> c = 255 | Some x \<Rightarrow> c = ucast x \<and> c \<noteq> 0xFF)
ret__unsigned_long_' \<top> UNIV []
(doMachineOp getActiveIRQ)
(Call getActiveIRQ_'proc)"
"ccorres (\<lambda>(a\<Colon>10 word option) c\<Colon>16 word.
case a of None \<Rightarrow> c = (0xFFFF\<Colon>16 word)
| Some (x\<Colon>10 word) \<Rightarrow> c = ucast x \<and> c \<noteq> (0xFFFF\<Colon>16 word))
(\<lambda>t. irq_' (s\<lparr>globals := globals t, irq_' := ret__unsigned_short_' t\<rparr> ))
\<top> UNIV hs
(doMachineOp getActiveIRQ) (Call getActiveIRQ_'proc)"
(* This is not very correct, however our current implementation of Hardware in haskell is stateless *)
assumes isIRQPending_ccorres:

2
proof/crefine/Recycle_C.thy
View File

@ -798,7 +798,7 @@ lemma arch_recycleCap_ccorres:
apply (erule subsetD, simp)
apply (erule subsetD[rotated], rule intvl_start_le)
apply simp
apply (clarsimp simp: split_def upto_enum_word kernelBase_def
apply (clarsimp simp: split_def upto_enum_word kernelBase_def Platform.kernelBase_def
cong: StateSpace.state.fold_congs globals.fold_congs)
apply (erule_tac S="{x. valid_pde_mapping_offset' (x && mask pdBits)}"
in mapM_x_store_memset_ccorres_assist[unfolded split_def],

69
proof/crefine/Refine_C.thy
View File

@ -30,17 +30,31 @@ apply (rule hoare_post_imp)
apply (rule schedule_invs')
done
(* FIXME: This is cheating (Xin) *)
lemma ucast_not_helper_cheating:
fixes a:: "10 word"
assumes a: "ucast a \<noteq> (0xFFFF :: word16)"
shows "ucast a \<noteq> (0xFFFF::32 signed word)"
by (word_bitwise,simp)
lemma handleInterruptEntry_ccorres:
"ccorres dc xfdc
(invs' and sch_act_simple)
UNIV []
(callKernel Interrupt) (Call handleInterruptEntry_'proc)"
proof -
have unifyhelp :
"\<And>s t. irq_' (s\<lparr>globals := globals t, irq_' := ret__unsigned_short_' t\<rparr>) =
ret__unsigned_short_' (t::globals myvars)"
by simp
show ?thesis
apply (cinit')
apply (simp add: callKernel_def handleEvent_def minus_one_norm)
apply (simp add: callKernel_def handleEvent_def minus_one_norm )
apply (simp add: liftE_bind bind_assoc)
apply (ctac (no_vcg) add: getActiveIRQ_ccorres)
apply (ctac (no_vcg) add: getActiveIRQ_ccorres)
apply (rule ccorres_Guard_Seq)?
apply (rule_tac P="rv \<noteq> Some 0xFF" in ccorres_gen_asm)
apply (rule_tac P="rv \<noteq> Some 0xFFFF" in ccorres_gen_asm)
apply wpc
apply (simp add: irqInvalid_def)
apply (rule ccorres_symb_exec_r)
@ -52,10 +66,11 @@ lemma handleInterruptEntry_ccorres:
apply (clarsimp simp: return_def)
apply (wp schedule_sch_act_wf schedule_invs'
| strengthen invs_queues_imp invs_valid_objs_strengthen)+
apply (simp add: ucast_not_helper irqInvalid_def)
apply (simp add: ucast_not_helper_cheating irqInvalid_def)
apply vcg
apply vcg
apply (clarsimp simp: irqInvalid_def)
apply (clarsimp simp: irqInvalid_def ucast_ucast_b
is_up ucast_not_helper_cheating)
apply (ctac (no_vcg) add: handleInterrupt_ccorres)
apply (ctac (no_vcg) add: schedule_ccorres)
apply (rule ccorres_add_return2)
@ -65,11 +80,12 @@ lemma handleInterruptEntry_ccorres:
apply (clarsimp simp: return_def)
apply (wp schedule_sch_act_wf schedule_invs'
| strengthen invs_queues_imp invs_valid_objs_strengthen)+
apply (rule_tac Q="\<lambda>rv s. invs' s \<and> (\<forall>x. rv = Some x \<longrightarrow> x \<le> Platform.maxIRQ) \<and> rv \<noteq> Some 0xFF" in hoare_post_imp)
apply (rule_tac Q="\<lambda>rv s. invs' s \<and> (\<forall>x. rv = Some x \<longrightarrow> x \<le> Platform.maxIRQ) \<and> rv \<noteq> Some 0x3FF" in hoare_post_imp)
apply (clarsimp simp: Kernel_C.maxIRQ_def Platform.maxIRQ_def)
apply (wp getActiveIRQ_le_maxIRQ getActiveIRQ_neq_Some0xFF | simp)+
apply (clarsimp simp: invs'_def valid_state'_def)
done
qed
lemma handleUnknownSyscall_ccorres:
"ccorres dc xfdc
@ -204,6 +220,8 @@ lemma ct_active_not_idle'_strengthen:
"invs' s \<and> ct_active' s \<longrightarrow> ksCurThread s \<noteq> ksIdleThread s"
by clarsimp
lemma handleSyscall_ccorres:
"ccorres dc xfdc
(invs' and
@ -217,6 +235,7 @@ lemma handleSyscall_ccorres:
apply (simp add: handleE_def handleE'_def)
apply (rule ccorres_split_nothrow_novcg)
apply wpc
prefer 3
-- "SysSend"
apply (clarsimp simp: syscall_from_H_def syscall_defs)
apply (rule ccorres_cond_empty |rule ccorres_cond_univ)+
@ -233,11 +252,13 @@ lemma handleSyscall_ccorres:
apply (ctac (no_vcg) add: getActiveIRQ_ccorres)
apply (rule ccorres_Guard)?
apply (simp only: irqInvalid_def)?
apply (rule_tac P="rv \<noteq> Some 0xFF" in ccorres_gen_asm)
apply (rule_tac P="rv \<noteq> Some 0xFFFF" in ccorres_gen_asm)
apply (subst ccorres_seq_skip'[symmetric])
apply (rule ccorres_split_nothrow_novcg)
apply (rule_tac R=\<top> and xf=xfdc in ccorres_when)
apply (case_tac rv, clarsimp, clarsimp simp: ucast_not_helper)
apply (case_tac rv, clarsimp,
clarsimp simp: ucast_not_helper_cheating ucast_ucast_b
is_up)
apply (ctac (no_vcg) add: handleInterrupt_ccorres)
apply ceqv
apply (rule_tac r=dc and xf=xfdc in ccorres_returnOk_skip[unfolded returnOk_def,simplified])
@ -245,7 +266,7 @@ lemma handleSyscall_ccorres:
apply (simp add: guard_is_UNIV_def)
apply clarsimp
apply (rule_tac Q="\<lambda>rv s. invs' s \<and>
(\<forall>x. rv = Some x \<longrightarrow> x \<le> Platform.maxIRQ) \<and> rv \<noteq> Some 0xFF"
(\<forall>x. rv = Some x \<longrightarrow> x \<le> Platform.maxIRQ) \<and> rv \<noteq> Some 0x3FF"
in hoare_post_imp)
apply (clarsimp simp: Kernel_C.maxIRQ_def Platform.maxIRQ_def)
apply (wp getActiveIRQ_le_maxIRQ getActiveIRQ_neq_Some0xFF | simp)+
@ -253,6 +274,7 @@ lemma handleSyscall_ccorres:
apply (simp add: invs'_def valid_state'_def)
apply clarsimp
apply (vcg exspec=handleInvocation_modifies)
prefer 3
-- "SysNBSend"
apply (clarsimp simp: syscall_from_H_def syscall_defs)
apply (rule ccorres_cond_empty |rule ccorres_cond_univ)+
@ -267,12 +289,14 @@ lemma handleSyscall_ccorres:
apply (rule ccorres_cond_univ)
apply (simp add: liftE_def bind_assoc irqInvalid_def)
apply (ctac (no_vcg) add: getActiveIRQ_ccorres)
apply (rule_tac P="rv \<noteq> Some 0xFF" in ccorres_gen_asm)
apply (rule_tac P="rv \<noteq> Some 0xFFFF" in ccorres_gen_asm)
apply (subst ccorres_seq_skip'[symmetric])
apply (rule ccorres_split_nothrow_novcg)
apply (rule ccorres_Guard)?
apply (rule_tac R=\<top> and xf=xfdc in ccorres_when)
apply (case_tac rv, clarsimp, clarsimp simp: ucast_not_helper)
apply (case_tac rv, clarsimp,
clarsimp simp: ucast_not_helper_cheating is_up
ucast_ucast_b)
apply (ctac (no_vcg) add: handleInterrupt_ccorres)
apply ceqv
apply (rule_tac ccorres_returnOk_skip[unfolded returnOk_def,simplified])
@ -280,7 +304,7 @@ lemma handleSyscall_ccorres:
apply (simp add: guard_is_UNIV_def)
apply clarsimp
apply (rule_tac Q="\<lambda>rv s. invs' s \<and>
(\<forall>x. rv = Some x \<longrightarrow> x \<le> Platform.maxIRQ) \<and> rv \<noteq> Some 0xFF"
(\<forall>x. rv = Some x \<longrightarrow> x \<le> Platform.maxIRQ) \<and> rv \<noteq> Some 0x3FF"
in hoare_post_imp)
apply (clarsimp simp: Kernel_C.maxIRQ_def Platform.maxIRQ_def)
apply (wp getActiveIRQ_le_maxIRQ getActiveIRQ_neq_Some0xFF | simp)+
@ -302,12 +326,14 @@ lemma handleSyscall_ccorres:
apply (rule ccorres_cond_univ)
apply (simp add: liftE_def bind_assoc irqInvalid_def)
apply (ctac (no_vcg) add: getActiveIRQ_ccorres)
apply (rule_tac P="rv \<noteq> Some 0xFF" in ccorres_gen_asm)
apply (rule_tac P="rv \<noteq> Some 0xFFFF" in ccorres_gen_asm)
apply (subst ccorres_seq_skip'[symmetric])
apply (rule ccorres_split_nothrow_novcg)
apply (rule ccorres_Guard)?
apply (rule_tac R=\<top> and xf=xfdc in ccorres_when)
apply (case_tac rv, clarsimp, clarsimp simp: ucast_not_helper)
apply (case_tac rv, clarsimp)
apply (clarsimp simp: ucast_not_helper_cheating ucast_ucast_b is_up)
apply clarsimp
apply (ctac (no_vcg) add: handleInterrupt_ccorres)
apply ceqv
apply (rule_tac ccorres_returnOk_skip[unfolded returnOk_def,simplified])
@ -315,7 +341,7 @@ lemma handleSyscall_ccorres:
apply (simp add: guard_is_UNIV_def)
apply clarsimp
apply (rule_tac Q="\<lambda>rv s. invs' s \<and>
(\<forall>x. rv = Some x \<longrightarrow> x \<le> Platform.maxIRQ) \<and> rv \<noteq> Some 0xFF"
(\<forall>x. rv = Some x \<longrightarrow> x \<le> Platform.maxIRQ) \<and> rv \<noteq> Some 0x3FF"
in hoare_post_imp)
apply (clarsimp simp: Kernel_C.maxIRQ_def Platform.maxIRQ_def)
apply (wp getActiveIRQ_le_maxIRQ getActiveIRQ_neq_Some0xFF | simp)+
@ -323,6 +349,7 @@ lemma handleSyscall_ccorres:
apply (simp add: invs'_def valid_state'_def)
apply clarsimp
apply (vcg exspec=handleInvocation_modifies)
prefer 2
-- "SysRecv"
apply (clarsimp simp: syscall_from_H_def syscall_defs)
apply (rule ccorres_cond_empty |rule ccorres_cond_univ)+
@ -331,6 +358,7 @@ lemma handleSyscall_ccorres:
apply (ctac (no_vcg) add: handleRecv_ccorres)
apply (rule ccorres_returnOk_skip[unfolded returnOk_def, simplified])
apply wp
prefer 2
-- "SysReply"
apply (clarsimp simp: syscall_from_H_def syscall_defs)
apply (rule ccorres_cond_empty |rule ccorres_cond_univ)+
@ -844,13 +872,15 @@ lemma checkActiveIRQ_ex_abs_einvs:
done
lemma check_active_irq_corres_C:
"corres_underlying rf_sr True (op =) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ex_abs valid_state) \<top>
(checkActiveIRQ) (checkActiveIRQ_C)"
"corres_underlying rf_sr True (op =)
(invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ex_abs valid_state) \<top>
(checkActiveIRQ) (checkActiveIRQ_C)"
apply (simp add: checkActiveIRQ_C_def checkActiveIRQ_def getActiveIRQ_C_def)
apply (rule corres_guard_imp)
apply (subst bind_assoc[symmetric])
apply (rule corres_split[OF _ ccorres_corres_u_xf, where R="\<lambda>_. \<top>" and R'="\<lambda>_. \<top>"])
apply simp
apply (rule corres_split)
apply simp
apply (rule ccorres_corres_u_xf)
apply (rule ccorres_rel_imp, rule ccorres_guard_imp)
apply (ctac add:getActiveIRQ_ccorres)
apply (rule TrueI)
@ -860,6 +890,7 @@ lemma check_active_irq_corres_C:
split: option.splits )
apply (rule no_fail_dmo')
apply (rule no_fail_getActiveIRQ)
apply (rule hoare_TrueI)+
apply (wp|simp)+
done

4
proof/crefine/Retype_C.thy
View File

@ -4118,7 +4118,7 @@ lemma copyGlobalMappings_ccorres:
apply (rule ccorres_h_t_valid_armKSGlobalPD)
apply csymbr
apply (rule ccorres_Guard_Seq)+
apply (simp add: kernelBase_def objBits_simps archObjSize_def
apply (simp add: kernelBase_def Platform.kernelBase_def objBits_simps archObjSize_def
whileAnno_def word_sle_def word_sless_def
Collect_True del: Collect_const)
apply (rule_tac xf'="\<lambda>_. ()" in ccorres_abstract)
@ -4146,7 +4146,7 @@ lemma copyGlobalMappings_ccorres:
+ ((0xE00 + of_nat n) << 2)) s
\<and> page_directory_at' pd s \<and> valid_pde_mappings' s
\<and> page_directory_at' (armKSGlobalPD (ksArchState s)) s"
and P'="{s. i_' s = of_nat (3840 + n)
and P'="{s. i_' s = of_nat (3584 + n)
\<and> is_aligned (symbol_table ''armKSGlobalPD'') pdBits}"
in setObject_ccorres_helper)
apply (rule conseqPre, vcg)

43
proof/crefine/Syscall_C.thy
View File

@ -334,7 +334,7 @@ lemma decodeInvocation_ccorres:
from_bool_to_bool_and_1 word_size
order_le_less_trans[OF word_and_le1]
mask_eq_iff_w2p word_size ucast_ucast_mask
isCap_simps
isCap_simps mask_eq_ucast_eq
mask_eq_iff_w2p[THEN trans[OF eq_commute]])+
done
@ -1645,6 +1645,7 @@ lemma handleInterrupt_ccorres:
apply (rule getIRQSlot_ccorres3)
apply (rule ccorres_getSlotCap_cte_at)
apply (rule_tac P="cte_at' rva" 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
apply csymbr
@ -1700,25 +1701,33 @@ lemma handleInterrupt_ccorres:
apply (ctac (no_vcg) add: resetTimer_ccorres)
apply (ctac add: ackInterrupt_ccorres)
apply wp
apply (rule conjI)
apply (clarsimp simp: cte_wp_at_ctes_of)
apply (auto simp: word_less_alt word_le_def maxIRQ_def uint_up_ucast is_up_def
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
intro: word_0_sle_from_less sless_positive)[1]
apply (simp add: if_1_0_0 Collect_const_mem)
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: Kernel_C.IRQTimer_def Kernel_C.IRQSignal_def
cte_wp_at_ctes_of)
apply (erule(1) cmap_relationE1[OF cmap_relation_cte])
apply (clarsimp simp: typ_heap_simps')
apply (simp add: cap_get_tag_isCap)
apply (cut_tac x=irq in unat_lt2p)
apply (simp add: ucast_eq_0 is_up_def source_size_def
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 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)
| 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

2
proof/crefine/Wellformed_C.thy
View File

@ -385,7 +385,7 @@ where
"cl_valid_cap c \<equiv>
case c of
Cap_frame_cap fc \<Rightarrow> ((capFSize_CL fc) \<noteq> scast Kernel_C.ARMSmallPage)
| Cap_irq_handler_cap fc \<Rightarrow> ((capIRQ_CL fc) && mask 8 = capIRQ_CL fc)
| Cap_irq_handler_cap fc \<Rightarrow> ((capIRQ_CL fc) && mask 10 = capIRQ_CL fc)
| x \<Rightarrow> True"
definition

6
proof/drefine/CNode_DR.thy
View File

@ -1727,7 +1727,7 @@ lemma opt_cap_pd_None:
opt_cap_def invs_def valid_state_def object_slots_def transform_page_directory_contents_def)+
lemma transform_pde_NullCap:
"\<lbrakk>3840 \<le> unat (xa::word32); unat xa < 4096\<rbrakk> \<Longrightarrow>
"\<lbrakk>3584 \<le> unat (xa::word32); unat xa < 4096\<rbrakk> \<Longrightarrow>
transform_pde (kernel_pde_mask ptx (ucast xa)) = cdl_cap.NullCap"
apply (clarsimp simp:kernel_pde_mask_def kernel_base_def)
apply (subst ucast_le_migrate[symmetric])
@ -1740,7 +1740,7 @@ lemma transform_pde_NullCap:
done
lemma dcorres_dummy_empty_slot_pd:
"\<lbrakk>0xF00 \<le> unat xa ; unat xa < 0x1000\<rbrakk> \<Longrightarrow> dcorres dc \<top> (valid_idle and page_directory_at w)
"\<lbrakk>0xE00 \<le> unat xa ; unat xa < 0x1000\<rbrakk> \<Longrightarrow> dcorres dc \<top> (valid_idle and page_directory_at w)
(PageTableUnmap_D.empty_slot (w, unat (xa::word32))) (return x)"
apply (clarsimp simp:PageTableUnmap_D.empty_slot_def gets_the_def gets_def bind_assoc)
apply (rule dcorres_absorb_get_l)
@ -1757,7 +1757,7 @@ lemma dcorres_dummy_empty_slot_pd:
done
lemma dcorres_dummy_empty_slot_pd_mapM_x:
"\<forall>x\<in> set ls. 0xF00 \<le> unat x \<and> unat x < 4096
"\<forall>x\<in> set ls. 0xE00 \<le> unat x \<and> unat x < 4096
\<Longrightarrow> dcorres dc \<top> (page_directory_at w and valid_idle)
(mapM_x PageTableUnmap_D.empty_slot (map (\<lambda>x. (w, unat x)) (ls::word32 list)))
(return x)"

2
proof/drefine/StateTranslation_D.thy
View File

@ -208,7 +208,7 @@ where
"transform_intent_issue_irq_handler args \<equiv>
case args of
irqW#index#depth#_ \<Rightarrow>
Some (IrqControlIssueIrqHandlerIntent ((ucast irqW)::word8) index depth)
Some (IrqControlIssueIrqHandlerIntent ((ucast irqW)::10 word) index depth)
| _ \<Rightarrow> Nothing"
definition

68
proof/drefine/Syscall_DR.thy
View File

@ -1665,42 +1665,46 @@ lemma handle_event_corres:
apply (case_tac syscall)
apply (simp_all add:handle_syscall_def handle_send_def handle_call_def)
apply (rule handle_invocation_corres[THEN corres_guard_imp] | simp)+
apply (rule corres_guard_imp[OF handle_recv_corres])
apply simp+
apply (simp add: ct_running_not_idle_etc)
apply (clarsimp simp: ct_in_state_def st_tcb_at_def obj_at_def generates_pending_def)
apply (rule corres_guard_imp[OF handle_reply_corres])
apply simp
apply (rule corres_guard_imp)
apply (rule corres_split[OF handle_recv_corres handle_reply_corres])
apply (wp handle_reply_cur_thread_idle_thread)
apply (simp add:not_idle_thread_def)
apply (wp handle_reply_cur_thread_idle_thread handle_reply_valid_etcbs)
apply (rule hoare_post_imp[OF _ hr_ct_active_and_valid_etcbs])
apply (clarsimp simp:ct_in_state_def)
apply clarsimp+
apply (frule (1) ct_running_not_idle_etc)
apply ((clarsimp simp: handle_yield_def returnOk_def liftE_def not_idle_thread_def
ct_in_state_def st_tcb_at_def obj_at_def)+)[1]
apply (rule handle_invocation_corres[THEN corres_guard_imp] | simp)+
apply (rule corres_guard_imp[OF handle_recv_corres])
apply simp+
apply (simp add: ct_running_not_idle_etc)
apply (rule corres_guard_imp)
apply (rule corres_split[OF handle_recv_corres handle_reply_corres])
apply (wp handle_reply_cur_thread_idle_thread)
apply (simp add:not_idle_thread_def)
apply (wp handle_reply_cur_thread_idle_thread handle_reply_valid_etcbs)
apply (rule hoare_post_imp[OF _ hr_ct_active_and_valid_etcbs])
apply (clarsimp simp:ct_in_state_def)
apply clarsimp+
apply (frule (1) ct_running_not_idle_etc)
apply (clarsimp simp:not_idle_thread_def ct_in_state_def st_tcb_at_def)
apply ((clarsimp simp: handle_yield_def returnOk_def liftE_def not_idle_thread_def ct_in_state_def st_tcb_at_def obj_at_def)+)[2]
apply (rule dcorres_symb_exec_r)
apply (rule dcorres_return, simp)
apply (wp hoare_TrueI)
apply (rule corres_guard_imp)
apply (rule handle_recv_corres, simp)
apply clarsimp
apply (frule (1) ct_running_not_idle_etc)
apply (clarsimp simp: not_idle_thread_def ct_in_state_def st_tcb_at_def obj_at_def)
apply (rule corres_symb_exec_r[OF handle_fault_corres])
apply wp[1]
apply clarsimp
apply (frule (1) ct_running_not_idle_etc)
apply (fastforce simp:st_tcb_at_def obj_at_def generates_pending_def gets_def get_def valid_fault_def split:Structures_A.thread_state.splits)+
apply (clarsimp simp: ct_in_state_def st_tcb_at_def obj_at_def generates_pending_def)
apply (rule corres_guard_imp[OF handle_reply_corres])
apply simp
apply (simp add: ct_running_not_idle_etc)
apply (clarsimp simp:not_idle_thread_def ct_in_state_def st_tcb_at_def)
apply ((clarsimp simp: handle_yield_def returnOk_def liftE_def not_idle_thread_def
ct_in_state_def st_tcb_at_def obj_at_def)+)
apply (rule dcorres_symb_exec_r)
apply (rule dcorres_return, simp)
apply (wp hoare_TrueI)
apply (rule corres_guard_imp)
apply (rule handle_recv_corres, simp)
apply clarsimp
apply (frule (1) ct_running_not_idle_etc)
apply (clarsimp simp: not_idle_thread_def ct_in_state_def st_tcb_at_def obj_at_def)
apply (rule corres_symb_exec_r[OF handle_fault_corres])
apply wp[1]
apply clarsimp
apply (frule (1) ct_running_not_idle_etc)
apply (fastforce simp:st_tcb_at_def obj_at_def generates_pending_def valid_fault_def split:Structures_A.thread_state.splits)+
apply (fastforce simp:st_tcb_at_def obj_at_def generates_pending_def gets_def get_def valid_fault_def split:Structures_A.thread_state.splits)+
apply (rule corres_symb_exec_r[OF handle_fault_corres])
apply wp[1]
apply clarsimp
apply (frule (1) ct_running_not_idle_etc)
apply (fastforce simp:st_tcb_at_def obj_at_def generates_pending_def valid_fault_def split:Structures_A.thread_state.splits)+
apply (simp add:handle_pending_interrupts_def)
apply (rule corres_guard_imp)
apply (rule corres_split [OF _ get_active_irq_corres])
@ -1721,4 +1725,4 @@ lemma handle_event_corres:
apply (wp|simp)+
done
end
end

15
proof/infoflow/ADT_IF.thy
View File

@ -1537,7 +1537,7 @@ locale invariant_over_ADT_if =
locale valid_initial_state_noenabled = invariant_over_ADT_if +
fixes s0_internal :: det_state
fixes initial_aag :: "'a subject_label PAS"
fixes timer_irq :: word8
fixes timer_irq :: "10 word"
fixes current_aag
fixes s0 :: observable_if
fixes s0_context :: user_context
@ -1584,7 +1584,7 @@ locale valid_initial_state = valid_initial_state_noenabled +
assumes ADT_A_if_Init_Fin_serial:
"Init_Fin_serial (ADT_A_if utf) s0 (full_invs_if \<inter> {s. step_restrict s})"
function (domintros) next_irq_state :: "nat \<Rightarrow> (word8 \<Rightarrow> bool) \<Rightarrow> nat" where
function (domintros) next_irq_state :: "nat \<Rightarrow> (10 word \<Rightarrow> bool) \<Rightarrow> nat" where
"next_irq_state cur masks = (if irq_at cur masks = None then next_irq_state (Suc cur) masks else cur)"
by(pat_completeness, auto)
@ -3021,8 +3021,15 @@ lemma handle_event_irq_state_inv:
apply simp
apply(rename_tac syscall)
apply(case_tac syscall)
apply(simp add: handle_send_def handle_call_def | wp handle_invocation_irq_state_inv)+
by((simp | wp_trace add: irq_state_inv_triv hy_inv | blast | (elim conjE, (intro conjI | assumption)+))+)
apply ((simp add: handle_send_def handle_call_def
| wp handle_invocation_irq_state_inv)+)[1]
apply((simp | wp_trace add: irq_state_inv_triv hy_inv
| blast | (elim conjE, (intro conjI | assumption)+))+)[1]
apply ((simp add: handle_send_def handle_call_def
| wp handle_invocation_irq_state_inv)+)[2]
apply((simp | wp_trace add: irq_state_inv_triv hy_inv
| blast | (elim conjE, (intro conjI | assumption)+))+)
done
lemma schedule_if_irq_state_inv:
"\<lbrace>irq_state_inv st\<rbrace> schedule_if tc \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>"

2
proof/infoflow/ADT_IF_Refine_C.thy
View File

@ -18,7 +18,7 @@ definition handleInterruptEntry_C_body_if (*:: "(globals myvars, int, l4c_errort
"handleInterruptEntry_C_body_if \<equiv> (
(\<acute>irq :== CALL getActiveIRQ();;
(Guard SignedArithmetic \<lbrace>True\<rbrace>
(IF (ucast \<acute>irq :: word32) \<noteq> (ucast ((ucast (-1 :: word8)) :: word32)) THEN
(IF (ucast \<acute>irq :: word32) \<noteq> (ucast ((ucast (-1 :: word10)) :: word32)) THEN
CALL handleInterrupt(\<acute>irq)
FI)));;
\<acute>ret__unsigned_long :== scast EXCEPTION_NONE)"

8
proof/infoflow/CNode_IF.thy
View File

@ -644,10 +644,10 @@ lemma preemption_point_def2:
(* moved from ADT_IF *)
definition irq_at :: "nat \<Rightarrow> (word8 \<Rightarrow> bool) \<Rightarrow> irq option" where
definition irq_at :: "nat \<Rightarrow> (10 word \<Rightarrow> bool) \<Rightarrow> irq option" where
"irq_at pos masks \<equiv>
let i = irq_oracle pos in
(if i = 0xFF \<or> masks i then None else Some i)"
(if i = 0x3FF \<or> masks i then None else Some i)"
definition is_irq_at :: "('z::state_ext) state \<Rightarrow> irq \<Rightarrow> nat \<Rightarrow> bool" where
"is_irq_at s \<equiv> \<lambda> irq pos. irq_at pos (irq_masks (machine_state s)) = Some irq"
@ -693,7 +693,7 @@ text {*
There is only one interrupt turned on, namely @{term irq}, and it is
a timer interrupt.
*}
definition only_timer_irq :: "word8 \<Rightarrow> 'z::state_ext state \<Rightarrow> bool" where
definition only_timer_irq :: "10 word \<Rightarrow> 'z::state_ext state \<Rightarrow> bool" where
"only_timer_irq irq s \<equiv> (\<forall>x. interrupt_states s x = IRQTimer \<longrightarrow> x = irq) \<and> irq_is_recurring irq s"
lemma is_irq_at_triv:
@ -755,7 +755,7 @@ lemma only_timer_irq_pres:
apply(erule use_valid[OF _ irq_is_recurring_triv[OF a]])
by simp
definition only_timer_irq_inv :: "word8 \<Rightarrow> 'a::state_ext state \<Rightarrow> 'a state \<Rightarrow> bool" where
definition only_timer_irq_inv :: "10 word \<Rightarrow> 'a::state_ext state \<Rightarrow> 'a state \<Rightarrow> bool" where
"only_timer_irq_inv irq st \<equiv> domain_sep_inv False st and only_timer_irq irq"
lemma only_timer_irq_inv_pres:

17
proof/infoflow/Example_Valid_State.thy
View File

@ -666,7 +666,7 @@ where
init_global_pd \<mapsto> ArchObj (PageDirectory global_pd))"
lemma irq_node_offs_min:
"init_irq_node_ptr \<le> init_irq_node_ptr + (ucast (irq:: 8 word) << cte_level_bits)"
"init_irq_node_ptr \<le> init_irq_node_ptr + (ucast (irq:: 10 word) << cte_level_bits)"
apply (rule_tac sz=28 in word32_plus_mono_right_split)
apply (simp add: unat_word_ariths mask_def shiftl_t2n s0_ptr_defs cte_level_bits_def)
apply (cut_tac x=irq and 'a=32 in ucast_less)
@ -676,7 +676,7 @@ lemma irq_node_offs_min:
done
lemma irq_node_offs_max:
"init_irq_node_ptr + (ucast (irq:: 8 word) << cte_level_bits) < init_irq_node_ptr + 0x1000"
"init_irq_node_ptr + (ucast (irq:: 10 word) << cte_level_bits) < init_irq_node_ptr + 0x4000"
apply (simp add: s0_ptr_defs cte_level_bits_def shiftl_t2n)
apply (cut_tac x=irq and 'a=32 in ucast_less)
apply simp
@ -684,13 +684,13 @@ lemma irq_node_offs_max:
done
definition irq_node_offs_range where
"irq_node_offs_range \<equiv> {x. init_irq_node_ptr \<le> x \<and> x < init_irq_node_ptr + 0x1000}
"irq_node_offs_range \<equiv> {x. init_irq_node_ptr \<le> x \<and> x < init_irq_node_ptr + 0x4000}
\<inter> {x. is_aligned x cte_level_bits}"
lemma irq_node_offs_in_range:
"init_irq_node_ptr + (ucast (irq:: 8 word) << cte_level_bits)
"init_irq_node_ptr + (ucast (irq:: 10 word) << cte_level_bits)
\<in> irq_node_offs_range"
apply (clarsimp simp: irq_node_offs_min irq_node_offs_max irq_node_offs_range_def)
apply (rule is_aligned_add[OF _ is_aligned_shift])
@ -702,7 +702,7 @@ lemma irq_node_offs_range_correct:
\<Longrightarrow> \<exists>irq. x = init_irq_node_ptr + (ucast (irq:: 8 word) << cte_level_bits)"
apply (clarsimp simp: irq_node_offs_min irq_node_offs_max irq_node_offs_range_def
s0_ptr_defs cte_level_bits_def)
apply (rule_tac x="ucast ((x - 0xF0003000) >> 4)" in exI)
apply (rule_tac x="ucast ((x - 0xE0008000) >> 4)" in exI)
apply (clarsimp simp: ucast_ucast_mask)
apply (subst aligned_shiftr_mask_shiftl)
apply (rule aligned_sub_aligned)
@ -723,7 +723,7 @@ lemma irq_node_offs_range_correct:
apply (subst add_mask_lower_bits)
apply (simp add: is_aligned_def)
apply clarsimp
apply (cut_tac x=x and y="0xF0003FFF" and n=12 in neg_mask_mono_le)
apply (cut_tac x=x and y="0xE000BFFF" and n=12 in neg_mask_mono_le)
apply (force dest: word_less_sub_1)
apply (drule_tac n=12 in aligned_le_sharp)
apply (simp add: is_aligned_def)
@ -745,7 +745,10 @@ lemma irq_node_offs_range_distinct[simp]:
"idle_tcb_ptr \<notin> irq_node_offs_range"
"init_globals_frame \<notin> irq_node_offs_range"
"init_global_pd \<notin> irq_node_offs_range"
by (simp_all add: s0_ptr_defs irq_node_offs_range_def)
apply auto
thm irq_node_offs_range_def
apply (simp add:irq_node_offs_range_def s0_ptr_defs)
apply (simp_all add: s0_ptr_defs irq_node_offs_range_def)
lemma irq_node_offs_distinct[simp]:
"init_irq_node_ptr + (ucast (irq:: 8 word) << cte_level_bits) \<noteq> Low_cnode_ptr"

6
proof/infoflow/IRQMasks_IF.thy
View File

@ -78,6 +78,9 @@ crunch irq_masks[wp]: finalise_cap "\<lambda>s. P (irq_masks_of_state s)"
crunch irq_masks[wp]: send_signal "\<lambda>s. P (irq_masks_of_state s)"
(wp: crunch_wps ignore: do_machine_op wp: dmo_wp simp: crunch_simps)
crunch irq_masks[wp]: machine_op_lift "\<lambda>s. P (irq_masks s)"
(wp: crunch_wps ignore: machine_op_lift wp:dmo_wp)
lemma handle_interrupt_irq_masks:
notes no_irq[wp del]
shows
@ -85,7 +88,8 @@ lemma handle_interrupt_irq_masks:
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(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

4
proof/infoflow/InfoFlow.thy
View File

@ -112,7 +112,7 @@ abbreviation aag_can_read :: "'a PAS \<Rightarrow> word32 \<Rightarrow> bool"
where
"aag_can_read aag x \<equiv> (pasObjectAbs aag x) \<in> subjectReads (pasPolicy aag) (pasSubject aag)"
abbreviation aag_can_read_irq :: "'a PAS \<Rightarrow> word8 \<Rightarrow> bool"
abbreviation aag_can_read_irq :: "'a PAS \<Rightarrow> 10 word \<Rightarrow> bool"
where
"aag_can_read_irq aag x \<equiv> (pasIRQAbs aag x) \<in> subjectReads (pasPolicy aag) (pasSubject aag)"
@ -275,7 +275,7 @@ lemma equiv_asids_triv:
is included here. *)
definition states_equiv_for :: "(word32 \<Rightarrow> bool) \<Rightarrow> (word8 \<Rightarrow> bool) \<Rightarrow> (asid \<Rightarrow> bool) \<Rightarrow> (domain \<Rightarrow> bool) \<Rightarrow> (word32 \<Rightarrow> (word32 set)) \<Rightarrow> det_state \<Rightarrow> det_state \<Rightarrow> bool"
definition states_equiv_for :: "(word32 \<Rightarrow> bool) \<Rightarrow> (10 word \<Rightarrow> bool) \<Rightarrow> (asid \<Rightarrow> bool) \<Rightarrow> (domain \<Rightarrow> bool) \<Rightarrow> (word32 \<Rightarrow> (word32 set)) \<Rightarrow> det_state \<Rightarrow> det_state \<Rightarrow> bool"
where
"states_equiv_for P Q R S X s s' \<equiv>
equiv_for P kheap s s' \<and>

45
proof/infoflow/Scheduler_IF.thy
View File

@ -2083,11 +2083,6 @@ lemma get_irq_state_reads_respects_scheduler_trivial: "reads_respects_scheduler
apply (clarsimp simp: domain_sep_inv_def)
done
lemma dmo_ack_noop: "do_machine_op (ackInterrupt irq) = return ()"
apply (simp add: do_machine_op_def ackInterrupt_def
select_f_def return_def bind_def
gets_def get_def simpler_modify_def)
done
lemma resetTimer_underlying_memory[wp]: "\<lbrace>\<lambda>s. P(underlying_memory s)\<rbrace> resetTimer \<lbrace>\<lambda>r s. P (underlying_memory s)\<rbrace>"
apply (simp add: resetTimer_def machine_op_lift_def machine_rest_lift_def)
@ -2143,16 +2138,46 @@ lemma irq_inactive_or_timer: "\<lbrace>domain_sep_inv False st and Q IRQTimer an
apply clarsimp+
done
lemma ackInterrupt_no_irq[wp]:
"no_irq (ackInterrupt irq)"
apply (clarsimp simp add:no_irq_def)
apply (wp dmo_wp VSpace_AI.ackInterrupt_irq_masks | simp add:no_irq_def)+
done
crunch irq_state[wp]: ackInterrupt "\<lambda>s. P (irq_state s)"
lemma ackInterrupt_reads_respects_scheduler:
"reads_respects_scheduler aag l \<top> (do_machine_op (ackInterrupt irq))"
apply (rule reads_respects_scheduler_unobservable)
apply (rule scheduler_equiv_lift)
apply (simp add: globals_equiv_scheduler_def[abs_def] idle_equiv_def)
apply (rule hoare_pre)
apply wps
apply (wp dmo_wp VSpace_AI.ackInterrupt_irq_masks | simp add:no_irq_def)+
apply (wp dmo_wp | simp add:ackInterrupt_def)+
apply clarsimp
apply ((wp silc_dom_lift dmo_wp | simp)+)[5]
apply (rule scheduler_affects_equiv_unobservable)
apply (simp add: states_equiv_for_def[abs_def] equiv_for_def equiv_asids_def
equiv_asid_def)
apply (rule hoare_pre)
apply wps
apply (wp dmo_wp | simp add:ackInterrupt_def)+
apply (wp mol_exclusive_state)
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 dmo_ack_noop)
apply (wp)
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 simp
apply (wp timer_tick_reads_respects_scheduler dmo_resetTimer_reads_respects_scheduler get_irq_state_reads_respects_scheduler_trivial fail_ev irq_inactive_or_timer | simp)+
apply force
apply (wp timer_tick_reads_respects_scheduler
dmo_resetTimer_reads_respects_scheduler
get_irq_state_reads_respects_scheduler_trivial
fail_ev irq_inactive_or_timer | simp add: | wpc)+
apply force
done

7
proof/invariant-abstract/ArchAcc_AI.thy
View File

@ -2521,9 +2521,8 @@ lemma shiftr_eqD:
apply (simp add: and_not_mask[symmetric] is_aligned_neg_mask_eq)
done
(*
lemma kernel_base_ge_observation:
"(kernel_base \<le> x) = (x && ~~ mask 28 = kernel_base)"
"(kernel_base \<le> x) = (x && ~~ mask 29 = kernel_base)"
apply (subst mask_in_range)
apply (simp add: kernel_base_def is_aligned_def)
apply (simp add: kernel_base_def)
@ -2531,9 +2530,9 @@ lemma kernel_base_ge_observation:
lemma kernel_base_less_observation:
"(x < kernel_base) = (x && ~~ mask 28 \<noteq> kernel_base)"
"(x < kernel_base) = (x && ~~ mask 29 \<noteq> kernel_base)"
apply (simp add: linorder_not_le[symmetric] kernel_base_ge_observation)
*)
done
lemma vptr_shifting_helper_magic:
"(x = 0) \<or> (x < 2 ^ 4 \<and> vmsz_aligned (vptr::word32) ARMSuperSection)

9
proof/invariant-abstract/Invariants_AI.thy
View File

@ -1269,7 +1269,7 @@ definition
where
"valid_irq_handlers \<equiv> \<lambda>s. \<forall>cap \<in> ran (caps_of_state s). \<forall>irq \<in> cap_irqs cap. irq_issued irq s"
definition valid_irq_masks :: "(word8 \<Rightarrow> irq_state) \<Rightarrow> (word8 \<Rightarrow> bool) \<Rightarrow> bool" where
definition valid_irq_masks :: "(10 word \<Rightarrow> irq_state) \<Rightarrow> (10 word \<Rightarrow> bool) \<Rightarrow> bool" where
"valid_irq_masks table masked \<equiv> \<forall>irq. table irq = IRQInactive \<longrightarrow> masked irq"
definition valid_irq_states :: "'z::state_ext state \<Rightarrow> bool" where
"valid_irq_states \<equiv> \<lambda>s.
@ -1565,7 +1565,7 @@ cap_table_at xl xk se \<and>
valid_cap_ref (ThreadCap (xn\<Colon>word32)) (sf\<Colon>'z_1\<Colon>state_ext state) = tcb_at xn sf \<and>
valid_cap_ref DomainCap (sp\<Colon>'z_1\<Colon>state_ext state) = True \<and>
valid_cap_ref IRQControlCap (sg\<Colon>'z_1\<Colon>state_ext state) = True \<and>
valid_cap_ref (IRQHandlerCap (xo\<Colon>word8)) (sh\<Colon>'z_1\<Colon>state_ext state) = True \<and>
valid_cap_ref (IRQHandlerCap (xo\<Colon>10 word)) (sh\<Colon>'z_1\<Colon>state_ext state) = True \<and>
valid_cap_ref (Zombie (xp\<Colon>word32) (xq\<Colon>nat option) (xr\<Colon>nat))
(si\<Colon>'z_1\<Colon>state_ext state) =
(case xq of None \<Rightarrow> tcb_at xp si | Some (b\<Colon>nat) \<Rightarrow> cap_table_at b xp si) \<and>
@ -1610,7 +1610,7 @@ lemma valid_cap_simps :
(cap_aligned (ThreadCap xn) \<and> tcb_at xn sf) \<and>
(sp\<Colon>'z_1\<Colon>state_ext state) \<turnstile> DomainCap = (cap_aligned DomainCap \<and> True) \<and>
(sg\<Colon>'z_1\<Colon>state_ext state) \<turnstile> IRQControlCap = (cap_aligned IRQControlCap \<and> True) \<and>
(sh\<Colon>'z_1\<Colon>state_ext state) \<turnstile> IRQHandlerCap (xo\<Colon>word8) =
(sh\<Colon>'z_1\<Colon>state_ext state) \<turnstile> IRQHandlerCap (xo\<Colon>10 word) =
(cap_aligned (IRQHandlerCap xo) \<and> xo \<le> maxIRQ) \<and>
(si\<Colon>'z_1\<Colon>state_ext state) \<turnstile> Zombie (xp\<Colon>word32) (xq\<Colon>nat option) (xr\<Colon>nat) =
(cap_aligned (Zombie xp xq xr) \<and>
@ -5055,7 +5055,8 @@ lemma get_irq_slot_real_cte:
"\<lbrace>invs\<rbrace> get_irq_slot irq \<lbrace>real_cte_at\<rbrace>"
apply (simp add: get_irq_slot_def)
apply wp
apply (clarsimp simp: invs_def valid_state_def valid_irq_node_def)
apply (clarsimp simp: invs_def valid_state_def
valid_irq_node_def)
done
lemma all_invs_but_sym_refs_check:

23
proof/invariant-abstract/KernelInit_AI.thy
View File

@ -96,25 +96,28 @@ lemma mask_pde_mapping_bits:
"mask 20 = 2^pde_mapping_bits - 1"
by (simp add: mask_def pde_mapping_bits_def)
lemma init_irq_ptrs_ineqs:
"init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits) \<ge> init_irq_node_ptr"
"init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits) + 2 ^ cte_level_bits - 1
\<le> init_irq_node_ptr + 2 ^ 12 - 1"
\<le> init_irq_node_ptr + 2 ^ 14 - 1"
"init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits)
\<le> init_irq_node_ptr + 2 ^ 12 - 1"
\<le> init_irq_node_ptr + 2 ^ 14 - 1"
proof -
have P: "ucast irq < (2 ^ (12 - cte_level_bits) :: word32)"
apply (rule order_le_less_trans[OF ucast_le_ucast_8_32[THEN iffD2, OF word_n1_ge]])
have P: "ucast irq < (2 ^ (14 - cte_level_bits) :: word32)"
apply (rule order_le_less_trans[OF
ucast_le_ucast[where 'a=10 and 'b=32,simplified,THEN iffD2, OF word_n1_ge]])
apply (simp add: cte_level_bits_def minus_one_norm)
done
show "init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits) \<ge> init_irq_node_ptr"
apply (rule is_aligned_no_wrap'[where sz=12])
apply (rule is_aligned_no_wrap'[where sz=14])
apply (simp add: is_aligned_def init_irq_node_ptr_def kernel_base_def)
apply (rule shiftl_less_t2n[OF P])
apply simp
done
show Q: "init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits) + 2 ^ cte_level_bits - 1
\<le> init_irq_node_ptr + 2 ^ 12 - 1"
\<le> init_irq_node_ptr + 2 ^ 14 - 1"
apply (simp only: add_diff_eq[symmetric] add.assoc)
apply (rule word_add_le_mono2)
apply (simp only: trans [OF shiftl_t2n mult.commute])
@ -123,7 +126,7 @@ proof -
word_bits_def kernel_base_def init_irq_node_ptr_def)
done
show "init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits)
\<le> init_irq_node_ptr + 2 ^ 12 - 1"
\<le> init_irq_node_ptr + 2 ^ 14 - 1"
apply (simp only: add_diff_eq[symmetric])
apply (rule word_add_le_mono2)
apply (rule minus_one_helper3, rule shiftl_less_t2n[OF P])
@ -144,6 +147,7 @@ lemmas init_irq_ptrs_all_ineqs[unfolded init_irq_node_ptr_def cte_level_bits_def
init_irq_ptrs_less_ineqs[THEN less_imp_neq]
init_irq_ptrs_less_ineqs[THEN less_imp_neq, THEN not_sym]
lemmas ucast_le_ucast_10_32 = ucast_le_ucast[where 'a=10 and 'b=32,simplified]
lemma init_irq_ptrs_eq:
"((ucast (irq :: irq) << cte_level_bits)
= (ucast (irq' :: irq) << cte_level_bits :: word32))
@ -153,7 +157,7 @@ lemma init_irq_ptrs_eq:
apply (erule_tac bnd="ucast (max_word :: irq) + 1"
in shift_distinct_helper[rotated 3],
safe intro!: plus_one_helper2,
simp_all add: ucast_le_ucast_8_32 up_ucast_inj_eq,
simp_all add: ucast_le_ucast_10_32 up_ucast_inj_eq,
simp_all add: cte_level_bits_def word_bits_def up_ucast_inj_eq
max_word_def)
done
@ -225,6 +229,7 @@ lemmas cte_wp_at_caps_of_state_eq
lemma invs_A:
"invs init_A_st"
apply (simp add: invs_def)
apply (rule conjI)
prefer 2
@ -235,7 +240,7 @@ lemma invs_A:
apply (rule conjI)
apply (clarsimp simp: kernel_base_def valid_objs_def state_defs
valid_obj_def valid_vm_rights_def vm_kernel_only_def
dom_if_Some cte_level_bits_def init_irq_ptrs_all_ineqs)
dom_if_Some cte_level_bits_def)
apply (rule conjI)
apply (clarsimp simp: valid_tcb_def tcb_cap_cases_def is_master_reply_cap_def
valid_cap_def obj_at_def valid_tcb_state_def

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

@ -619,7 +619,7 @@ lemma getActiveIRQ_le_maxIRQ':
(* FIXME: follows already from getActiveIRQ_le_maxIRQ *)
lemma getActiveIRQ_neq_Some0xFF':
"\<lbrace>\<top>\<rbrace> getActiveIRQ \<lbrace>\<lambda>rv s. rv \<noteq> Some 0xFF\<rbrace>"
"\<lbrace>\<top>\<rbrace> getActiveIRQ \<lbrace>\<lambda>rv s. rv \<noteq> Some 0x3FF\<rbrace>"
apply (simp add: getActiveIRQ_def)
apply (wp alternative_wp select_wp)
apply simp

4
proof/refine/Detype_R.thy
View File

@ -1017,7 +1017,7 @@ lemma st_tcb:
dest: live_notRange)
lemma irq_nodes_global:
"\<forall>irq :: word8. irq_node' s + (ucast irq) * 16 \<in> global_refs' s"
"\<forall>irq :: 10 word. irq_node' s + (ucast irq) * 16 \<in> global_refs' s"
by (simp add: global_refs'_def mult.commute mult.left_commute)
lemma global_refs:
@ -1033,7 +1033,7 @@ lemma global_refs2:
using global_refs by blast
lemma irq_nodes_range:
"\<forall>irq :: word8. irq_node' s + (ucast irq) * 16 \<notin> base_bits"
"\<forall>irq :: 10 word. irq_node' s + (ucast irq) * 16 \<notin> base_bits"
using irq_nodes_global global_refs
by blast

9
proof/refine/Interrupt_R.thy
View File

@ -207,10 +207,14 @@ lemma decode_irq_control_valid'[wp]:
toEnum_of_nat word_le_nat_alt unat_of_nat)
done
lemma irq_nodes_global_refs:
"irq_node' s + (ucast (irq:: 10 word)) * 0x10 \<in> global_refs' s"
by (simp add: global_refs'_def mult.commute mult.left_commute)
lemma valid_globals_ex_cte_cap_irq:
"\<lbrakk> ex_cte_cap_wp_to' isCNodeCap ptr s; valid_global_refs' s;
valid_objs' s \<rbrakk>
\<Longrightarrow> ptr \<noteq> intStateIRQNode (ksInterruptState s) + 2 ^ cte_level_bits * ucast (irq :: word8)"
\<Longrightarrow> ptr \<noteq> intStateIRQNode (ksInterruptState s) + 2 ^ cte_level_bits * ucast (irq :: 10 word)"
apply (clarsimp simp: cte_wp_at_ctes_of ex_cte_cap_wp_to'_def)
apply (drule(1) ctes_of_valid'[rotated])
apply (drule(1) valid_global_refsD')
@ -218,7 +222,8 @@ lemma valid_globals_ex_cte_cap_irq:
apply (clarsimp simp: isCap_simps)
apply (subgoal_tac "irq_node' s + 2 ^ cte_level_bits * ucast irq \<in> global_refs' s")
apply blast
apply (simp add: global_refs'_def cte_level_bits_def)
apply (simp add: global_refs'_def cte_level_bits_def
mult.commute mult.left_commute)
done
lemma invoke_irq_handler_corres:

2
proof/refine/Machine_R.thy
View File

@ -97,7 +97,7 @@ lemma getActiveIRQ_le_maxIRQ:
(* FIXME: follows already from getActiveIRQ_le_maxIRQ *)
lemma getActiveIRQ_neq_Some0xFF:
"\<lbrace>\<top>\<rbrace> doMachineOp getActiveIRQ \<lbrace>\<lambda>rv s. rv \<noteq> Some 0xFF\<rbrace>"
"\<lbrace>\<top>\<rbrace> doMachineOp getActiveIRQ \<lbrace>\<lambda>rv s. rv \<noteq> Some 0x3FF\<rbrace>"
apply (simp add: doMachineOp_def split_def)
apply wp
apply clarsimp

2
proof/refine/Untyped_R.thy
View File

@ -673,7 +673,7 @@ lemma map_ensure_empty':
done
lemma irq_nodes_global:
"\<forall>irq :: word8. irq_node' s + (ucast irq) * 16 \<in> global_refs' s"
"irq_node' s + (ucast (irq :: 10 word)) * 16 \<in> global_refs' s"
by (simp add: global_refs'_def mult.commute mult.left_commute)
lemma valid_global_refsD2':

2
spec/abstract/ARM/Init_A.thy
View File

@ -36,7 +36,7 @@ definition
definition
init_irq_node_ptr :: word32 where
"init_irq_node_ptr = kernel_base + 0x3000"
"init_irq_node_ptr = kernel_base + 0x8000"
definition
init_globals_frame :: word32 where

2
spec/capDL/Intents_D.thy
View File

@ -130,7 +130,7 @@ datatype cdl_irq_handler_intent =
datatype cdl_irq_control_intent =
(* IssueIrqHandler: (target), irq, (root), index, depth *)
IrqControlIssueIrqHandlerIntent word8 word32 word32
IrqControlIssueIrqHandlerIntent "10 word" word32 word32
(* InterruptControl *)
| IrqControlArchIrqControlIntent

2
spec/capDL/Types_D.thy
View File

@ -23,7 +23,7 @@ imports
begin
(* A hardware IRQ number. *)
type_synonym cdl_irq = word8
type_synonym cdl_irq = "10 word"
(*
* How objects are named within the kernel.

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

@ -65,7 +65,7 @@ record
exclusive_state :: exclusive_monitors
machine_state_rest :: machine_state_rest
consts irq_oracle :: "nat \<Rightarrow> word8"
consts irq_oracle :: "nat \<Rightarrow> 10 word"
text {*
The machine monad is used for operations on the state defined above.

3
spec/design/version
View File

@ -1,4 +1,5 @@
Built from git repo at /Users/xgao/verification/seL4/haskell by xgao
Generated from changeset:
1d8e159 move kernelBase to arch specific files
8a071f7 move kernelBase to arch specific files

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

@ -396,7 +396,7 @@ where
is_masked \<leftarrow> gets $ irq_masks;
modify (\<lambda>s. s \<lparr> irq_state := irq_state s + 1 \<rparr>);
active_irq \<leftarrow> gets $ irq_oracle \<circ> irq_state;
if is_masked active_irq \<or> active_irq = 0xFF
if is_masked active_irq \<or> active_irq = 0x3FF
then return None
else return ((Some active_irq) :: irq option)
od"
@ -407,7 +407,6 @@ where
"maskInterrupt m irq \<equiv>
modify (\<lambda>s. s \<lparr> irq_masks := (irq_masks s) (irq := m) \<rparr>)"
text {* Does nothing on imx31 *}
consts
ackInterrupt_impl :: "irq \<Rightarrow> unit machine_rest_monad"
definition

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

@ -179,7 +179,7 @@ record
exclusive_state :: exclusive_monitors
machine_state_rest :: machine_state_rest
consts irq_oracle :: "nat \<Rightarrow> word8"
consts irq_oracle :: "nat \<Rightarrow> 10 word"
text {*
The machine monad is used for operations on the state defined above.

2
spec/machine/ARM/Platform.thy
View File

@ -23,7 +23,7 @@ text {*
addresses, as well as the range of IRQs on the platform.
*}
type_synonym irq = word8
type_synonym irq = "10 word"
type_synonym paddr = word32
abbreviation (input) "toPAddr \<equiv> id"