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

Partial progress on using array assertions.

This commit is contained in:
Thomas Sewell 2015-10-13 00:11:13 +11:00
parent 1fdbbe787e
commit 6fa0909124
18 changed files with 1236 additions and 462 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

157
lib/LemmaBucket_C.thy
View File

@ -13,6 +13,7 @@ imports
TypHeapLib
Aligned
WordLemmaBucket
"../tools/c-parser/umm_heap/ArrayAssertion"
begin
declare word_neq_0_conv [simp del]
@ -548,26 +549,6 @@ lemma coerce_heap_update_to_heap_updates:
apply simp
done
lemma array_tag_n_eq:
"(array_tag_n n :: ('a :: c_type['b :: finite]) field_desc typ_desc) =
TypDesc (TypAggregate
(map (\<lambda>n. DTPair (adjust_ti (typ_info_t TYPE('a)) (\<lambda>x. index x n)
(\<lambda>x f. Arrays.update f n x)) (replicate n CHR ''1'')) [0..<n]))
(typ_name (typ_uinfo_t TYPE('a)) @ ''_array_'' @ nat_to_bin_string (card (UNIV :: 'b :: finite set)))"
apply (induct n)
apply (simp add: typ_info_array array_tag_def eval_nat_numeral array_tag_n.simps empty_typ_info_def)
apply (simp add: typ_info_array array_tag_def eval_nat_numeral array_tag_n.simps empty_typ_info_def)
apply (simp add: ti_typ_combine_def Let_def)
done
lemma typ_info_array':
"typ_info_t TYPE ('a :: c_type['b :: finite]) =
TypDesc (TypAggregate
(map (\<lambda>n. DTPair (adjust_ti (typ_info_t TYPE('a)) (\<lambda>x. index x n)
(\<lambda>x f. Arrays.update f n x)) (replicate n CHR ''1'')) [0..<(card (UNIV :: 'b :: finite set))]))
(typ_name (typ_uinfo_t TYPE('a)) @ ''_array_'' @ nat_to_bin_string (card (UNIV :: 'b :: finite set)))"
by (simp add: typ_info_array array_tag_def array_tag_n_eq)
lemma update_ti_list_array':
"\<lbrakk> update_ti_list_t (map f [0 ..< n]) xs v = y;
\<forall>n. size_td_pair (f n) = v3; length xs = v3 * n;
@ -711,6 +692,32 @@ lemma heap_update_Array:
apply simp
done
lemma from_bytes_Array_element:
fixes p :: "('a::mem_type['b::finite]) ptr"
assumes less: "of_nat n < card (UNIV :: 'b set)"
assumes len: "length bs = size_of TYPE('a) * CARD('b)"
shows
"index (from_bytes bs :: 'a['b]) n
= from_bytes (take (size_of TYPE('a)) (drop (n * size_of TYPE('a)) bs))"
using less
apply (simp add: from_bytes_def size_of_def typ_info_array')
apply (subst update_ti_list_array'[OF refl])
apply simp
apply (simp add: len size_of_def)
apply (clarsimp simp: update_ti_s_adjust_ti)
apply (rule refl)
apply (simp add: split_upt_on_n[OF less])
apply (rule trans, rule foldr_does_nothing_to_xf[where xf="\<lambda>s. index s n"])
apply simp+
apply (subst foldr_does_nothing_to_xf[where xf="\<lambda>s. index s n"])
apply simp
apply (simp add: mult.commute)
apply (frule Suc_leI)
apply (drule_tac k="size_of TYPE('a)" in mult_le_mono2)
apply (rule upd_rf)
apply (simp add: size_of_def len mult.commute)
done
lemma heap_access_Array_element':
fixes p :: "('a::mem_type['b::finite]) ptr"
assumes less: "of_nat n < card (UNIV :: 'b set)"
@ -719,26 +726,14 @@ lemma heap_access_Array_element':
= h_val hp (array_ptr_index p False n)"
using less
apply (simp add: array_ptr_index_def CTypesDefs.ptr_add_def h_val_def)
apply (simp add: from_bytes_def size_of_def typ_info_array')
apply (subst update_ti_list_array'[OF refl])
apply simp
apply simp
apply (clarsimp simp: update_ti_s_adjust_ti)
apply (rule refl)
apply (simp add: split_upt_on_n[OF less])
apply (rule trans, rule foldr_does_nothing_to_xf[where xf="\<lambda>s. index s n"])
apply simp+
apply (subst foldr_does_nothing_to_xf[where xf="\<lambda>s. index s n"])
apply simp
apply (simp add: from_bytes_Array_element)
apply (simp add: drop_heap_list_le take_heap_list_le)
apply (subst take_heap_list_le)
apply (simp add: le_diff_conv2)
apply (drule Suc_leI)
apply (drule mult_le_mono2, simp)
apply (erule order_trans, simp)
apply (simp add: field_simps)
apply (rule upd_rf)
apply (simp add: size_of_def)
apply (drule_tac k="size_of TYPE('a)" in mult_le_mono2)
apply (simp add: mult.commute)
apply simp
done
lemmas heap_access_Array_element
@ -867,12 +862,6 @@ lemma fourthousand_size:
lemmas heap_update_Array_element
= heap_update_Array_element'[OF refl _ fourthousand_size]
lemma map_td_list_map:
"map_td_list f = map (map_td_pair f)"
apply (rule ext)
apply (induct_tac x, simp_all)
done
lemma typ_slice_list_cut:
"\<lbrakk> (\<forall>x \<in> set xs. size_td (dt_fst x) = m); m \<noteq> 0; n < (length xs * m) \<rbrakk>
\<Longrightarrow> typ_slice_list xs n =
@ -1114,4 +1103,88 @@ lemma heap_update_list_base':"heap_update_list p [] = id"
lemma hrs_mem_update_id3: "hrs_mem_update id = id"
unfolding hrs_mem_update_def by simp
abbreviation
ptr_span :: "'a::mem_type ptr \<Rightarrow> word32 set" where
"ptr_span p \<equiv> {ptr_val p ..+ size_of TYPE('a)}"
abbreviation (input)
cptr_type :: "('a :: c_type) ptr \<Rightarrow> 'a itself"
where
"cptr_type p \<equiv> TYPE('a)"
lemma ptr_retyp_valid_footprint_disjoint2:
"\<lbrakk>valid_footprint (ptr_retyp (q::'b::mem_type ptr) d) p s; {p..+size_td s} \<inter> {ptr_val q..+size_of TYPE('b)} = {} \<rbrakk>
\<Longrightarrow> valid_footprint d p s"
apply(clarsimp simp: valid_footprint_def Let_def)
apply (drule spec, drule (1) mp)
apply(subgoal_tac "p + of_nat y \<in> {p..+size_td s}")
apply (subst (asm) ptr_retyp_d)
apply clarsimp
apply fast
apply (clarsimp simp add: ptr_retyp_d_eq_fst split: split_if_asm)
apply fast
apply (erule intvlI)
done
lemma ptr_retyp_disjoint2:
"\<lbrakk>ptr_retyp (p::'a::mem_type ptr) d,g \<Turnstile>\<^sub>t q;
{ptr_val p..+size_of TYPE('a)} \<inter> {ptr_val q..+size_of TYPE('b)} = {} \<rbrakk>
\<Longrightarrow> d,g \<Turnstile>\<^sub>t (q::'b::mem_type ptr)"
apply(clarsimp simp: h_t_valid_def)
apply(erule ptr_retyp_valid_footprint_disjoint2)
apply(simp add: size_of_def)
apply fast
done
lemma ptr_retyp_disjoint_iff:
"{ptr_val p..+size_of TYPE('a)} \<inter> {ptr_val q..+size_of TYPE('b)} = {}
\<Longrightarrow> ptr_retyp (p::'a::mem_type ptr) d,g \<Turnstile>\<^sub>t q = d,g \<Turnstile>\<^sub>t (q::'b::mem_type ptr)"
apply rule
apply (erule (1) ptr_retyp_disjoint2)
apply (erule (1) ptr_retyp_disjoint)
done
lemma h_t_valid_ptr_retyp_eq:
"\<not> cptr_type p <\<^sub>\<tau> cptr_type p' \<Longrightarrow> h_t_valid (ptr_retyp p td) g p'
= (if ptr_span p \<inter> ptr_span p' = {} then h_t_valid td g p'
else field_of_t p' p \<and> g p')"
apply (clarsimp simp: ptr_retyp_disjoint_iff split: split_if)
apply (cases "g p'")
apply (rule iffI)
apply (rule ccontr, drule h_t_valid_neq_disjoint, rule ptr_retyp_h_t_valid, simp+)
apply (simp add: Int_commute)
apply (clarsimp simp: field_of_t_def field_of_def)
apply (drule sub_h_t_valid[where p=p, rotated], rule ptr_retyp_h_t_valid, simp, simp)
apply (erule(1) h_t_valid_guard_subst)
apply (simp add: h_t_valid_def)
done
lemma field_lookup_list_Some_again:
"dt_snd (xs ! i) = f
\<Longrightarrow> i < length xs
\<Longrightarrow> f \<notin> dt_snd ` set ((take i xs))
\<Longrightarrow> field_lookup_list xs [f] n
= Some (dt_fst (xs ! i), n + listsum (map (size_td o dt_fst) (take i xs)))"
apply (induct xs arbitrary: i n, simp_all)
apply (case_tac x1, simp)
apply (case_tac i, auto split: split_if)
done
lemma field_lookup_array:
"n < CARD('b) \<Longrightarrow> field_lookup (typ_info_t TYPE(('a :: c_type)['b :: finite]))
[replicate n (CHR ''1'')] i = Some (adjust_ti (typ_info_t TYPE('a))
(\<lambda>x. x.[n]) (\<lambda>x f. Arrays.update f n x), i + n * size_of TYPE ('a))"
apply (simp add: typ_info_array array_tag_def array_tag_n_eq)
apply (subst field_lookup_list_Some_again[where i=n],
auto simp add: take_map o_def listsum_triv size_of_def)
done
lemma array_not_sub_type:
"\<not> TYPE(('a :: c_type)['b :: finite]) <\<^sub>\<tau> TYPE('a)"
sorry
lemma field_of_t_array:
"field_of_t p' p = (\<exists>i. p' = array_ptr_index p True i)"
sorry
end

4
proof/crefine/CSpace_C.thy
View File

@ -3192,6 +3192,8 @@ lemma cap_get_capPtr_spec:
mask_def objBits_simps cap_lift_domain_cap
dest!: sym [where t = "cap_get_tag cap" for cap]
split: vmpage_size.splits)+
sorry (*
weak array assertion with zero width?
(* XXX: slow. there should be a rule for this *)
apply (case_tac "cap_lift cap", simp_all, case_tac "a",
auto simp: cap_lift_def cap_tag_defs Let_def
@ -3201,7 +3203,7 @@ lemma cap_get_capPtr_spec:
cap_zombie_cap_lift_def cap_page_table_cap_lift_def
cap_page_directory_cap_lift_def cap_asid_pool_cap_lift_def
Let_def cap_untyped_cap_lift_def split: split_if_asm)
done
done *)
lemma ccap_relation_get_capPtr_not_physical:
"\<lbrakk> ccap_relation hcap ccap; capClass hcap \<noteq> PhysicalClass \<rbrakk> \<Longrightarrow>

21
proof/crefine/CSpace_RAB_C.thy
View File

@ -527,15 +527,18 @@ next
apply (frule(2) gm)
apply (simp add: word_less_nat_alt word_le_nat_alt less_mask_eq)
apply (intro impI conjI allI, simp_all)
apply (simp add: cap_simps)
apply (frule iffD1 [OF cap_get_tag_CNodeCap])
apply (simp add: cap_get_tag_isCap)
apply (erule ssubst [where t = cap])
apply simp
apply (simp add: mask_def)
apply (subgoal_tac "capCNodeBits cap \<noteq> 0")
apply (clarsimp simp: linorder_not_less cap_simps)
apply (clarsimp simp: isCap_simps valid_cap'_def)
apply (simp add: cap_simps)
apply (frule iffD1 [OF cap_get_tag_CNodeCap])
apply (simp add: cap_get_tag_isCap)
apply (erule ssubst [where t = cap])
apply simp
apply (simp add: mask_def)
apply (subgoal_tac "capCNodeBits cap \<noteq> 0")
apply (clarsimp simp: linorder_not_less cap_simps)
apply (clarsimp simp: isCap_simps valid_cap'_def)
thm valid_cap'_def
apply (rule disjCI2)
defer
apply (clarsimp simp: linorder_not_less cap_simps)
apply (clarsimp simp: isCap_simps valid_cap'_def)
apply simp

110
proof/crefine/Detype_C.thy
View File

@ -1398,6 +1398,92 @@ lemma untyped_cap_rf_sr_ptr_bits_domain:
apply blast
done
lemma aligned_ranges_subset_or_disjoint_coroll:
"\<lbrakk> is_aligned (p :: 'a :: len word) n; is_aligned (p' :: 'a :: len word) n';
p && ~~ mask n' \<noteq> p'; p' && ~~ mask n \<noteq> p \<rbrakk>
\<Longrightarrow> {p .. p + 2 ^ n - 1} \<inter> {p' .. p' + 2 ^ n' - 1} = {}"
using aligned_ranges_subset_or_disjoint
apply (simp only: mask_in_range)
apply (subgoal_tac "p \<in> {p .. p + 2 ^ n - 1} \<and> p' \<in> {p' .. p' + 2 ^ n' - 1}")
apply blast
apply simp
done
lemma neg_mask_twice:
"x && ~~ mask n && ~~ mask m = x && ~~ mask (max n m)"
by (metis word_bw_assocs neg_mask_combine)
lemma multiple_mask_trivia: "n \<ge> m
\<Longrightarrow> (x && ~~ mask n) + (x && mask n && ~~ mask m) = x && ~~ mask m"
apply (rule trans[rotated], rule_tac w="mask n" in word_plus_and_or_coroll2)
apply (simp add: word_bw_assocs word_bw_comms word_bw_lcs neg_mask_twice
max_absorb2)
done
lemma distinct_aligned_addresses_accumulate:
"is_aligned p n \<Longrightarrow> is_aligned ptr bits
\<Longrightarrow> n \<ge> m \<Longrightarrow> n < size p \<Longrightarrow> m \<le> bits
\<Longrightarrow> (\<forall>y<2 ^ (n - m). p + (y << m) \<notin> {ptr..ptr + 2 ^ bits - 1})
\<Longrightarrow> {p .. p + 2 ^ n - 1} \<inter> {ptr..ptr + 2 ^ bits - 1} = {}"
apply safe
apply (simp only: mask_in_range[symmetric])
apply (drule_tac x="(x && mask n) >> m" in spec)
apply (simp add: shiftr_shiftl1 word_bw_assocs)
apply (drule mp, rule shiftr_less_t2n)
apply (subst add_diff_inverse, simp, rule and_mask_less', simp add: word_size)
apply (clarsimp simp: multiple_mask_trivia word_bw_assocs neg_mask_twice max_absorb2)
done
lemma offs_in_intvl_iff:
"(p + x \<in> {p ..+ n}) = (unat x < n)"
apply (simp add: intvl_def, safe)
apply (erule order_le_less_trans[rotated], simp add: unat_of_nat)
apply (rule exI, erule conjI[rotated])
apply simp
done
lemma objBits_koTypeOf:
fixes v :: "'a :: pspace_storable" shows
"objBits v = objBitsT (koType TYPE('a))"
using project_inject[where v=v, THEN iffD2, OF refl]
project_koType[THEN iffD1, OF exI[where x=v]]
by (simp add: objBits_def objBitsT_koTypeOf[symmetric])
lemma cmap_array_typ_region_bytes:
"ptrf = (Ptr :: _ \<Rightarrow> 'b ptr)
\<Longrightarrow> carray_map_relation bits' amap (h_t_valid htd c_guard) ptrf
\<Longrightarrow> is_aligned ptr bits
\<Longrightarrow> typ_uinfo_t TYPE('b :: c_type) \<noteq> typ_uinfo_t TYPE(8 word)
\<Longrightarrow> size_of TYPE('b) = 2 ^ bits'
\<Longrightarrow> objBitsT (koType TYPE('a :: pspace_storable)) \<le> bits
\<Longrightarrow> objBitsT (koType TYPE('a :: pspace_storable)) \<le> bits'
\<Longrightarrow> bits' < word_bits
\<Longrightarrow> carray_map_relation bits' (restrict_map (amap :: _ \<Rightarrow> 'a option) (- {ptr ..+ 2 ^ bits}))
(h_t_valid (typ_region_bytes ptr bits htd) c_guard) ptrf"
apply (clarsimp simp: carray_map_relation_def h_t_valid_typ_region_bytes)
apply (case_tac "h_t_valid htd c_guard (ptrf p)", simp_all)
apply (clarsimp simp: objBits_koTypeOf)
apply (drule spec, drule(1) iffD2, clarsimp)
apply (rule iffI[rotated])
apply clarsimp
apply (drule equals0D, erule notE, erule IntI[rotated])
apply (simp only: upto_intvl_eq is_aligned_neg_mask2 mask_in_range[symmetric])
apply (simp only: upto_intvl_eq, rule distinct_aligned_addresses_accumulate,
simp_all add: upto_intvl_eq[symmetric] word_size word_bits_def)
apply clarsimp
apply (drule_tac x="p + (y << objBitsT (koType TYPE('a)))" in spec)+
apply (simp add: is_aligned_add[OF is_aligned_weaken is_aligned_shiftl])
apply (simp add: is_aligned_add_helper shiftl_less_t2n word_bits_def)
apply clarsimp
apply (drule_tac x=p in spec)
apply (clarsimp simp: objBits_koTypeOf)
apply auto
done
lemma map_comp_restrict_map:
"(f \<circ>\<^sub>m (restrict_map m S)) = (restrict_map (f \<circ>\<^sub>m m) S)"
by (rule ext, simp add: restrict_map_def map_comp_def)
lemma deleteObjects_ccorres':
notes if_cong[cong]
shows
@ -1439,7 +1525,7 @@ proof -
and cte: "cte_wp_at' (\<lambda>cte. cteCap cte = UntypedCap ptr bits idx) p s"
and desc_range: "descendants_range' (UntypedCap ptr bits idx) p (ctes_of s)"
and invs: "invs' s" and "ct_active' s"
and "sch_act_simple s" and wb: "bits < word_bits"
and "sch_act_simple s" and wb: "bits < word_bits" and b2: "2 \<le> bits"
and "deletionIsSafe ptr bits s"
and sr: "(s, s') \<in> rf_sr"
and safe_asids:
@ -1500,7 +1586,15 @@ proof -
done
note cmaptcb = cmap_relation_tcb [OF sr]
note cmap_array_helper = arg_cong2[where f=carray_map_relation, OF refl map_comp_restrict_map]
have trivia: "size_of TYPE(pte_C[256]) = 2 ^ ptBits"
"size_of TYPE(pde_C[4096]) = 2 ^ pdBits"
by (auto simp: ptBits_def pageBits_def pdBits_def)
note cmap_array = cmap_array_typ_region_bytes[where 'a=pte, OF refl _ al _ trivia(1)]
cmap_array_typ_region_bytes[where 'a=pde, OF refl _ al _ trivia(2)]
note cmap_array = cmap_array[simplified, simplified objBitsT_simps b2
ptBits_def pdBits_def pageBits_def word_bits_def, simplified]
have cs: "cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s))
(t_hrs_' (globals s'))"
using sr
@ -1517,7 +1611,8 @@ proof -
simp_all add: objBits_simps archObjSize_def pageBits_def projectKOs
heap_to_page_data_restrict)[1])+ -- "waiting ..."
apply (simp add: map_to_ctes_delete' cmap_relation_restrict_both_proj
cmap_relation_restrict_both)
cmap_relation_restrict_both cmap_array_helper hrs_htd_update
ptBits_def pdBits_def pageBits_def cmap_array)
apply (intro conjI)
apply (frule cmap_relation_restrict_both_proj
[where f = tcb_ptr_to_ctcb_ptr])
@ -1645,8 +1740,7 @@ proof -
\<Turnstile>\<^sub>t (Ptr::(32 word \<Rightarrow> (pde_C[4096]) ptr)) (symbol_table ''armKSGlobalPD'')"
using al wb
apply (cases "t_hrs_' (globals s')")
apply (simp add: hrs_htd_update_def hrs_htd_def h_t_valid_typ_region_bytes upto_intvl_eq
ptr_span_def)
apply (simp add: hrs_htd_update_def hrs_htd_def h_t_valid_typ_region_bytes upto_intvl_eq)
done
}
@ -1716,6 +1810,9 @@ proof -
apply simp
done
have s_ksPSpace_adjust: "ksPSpace_update ?psu s = s\<lparr>ksPSpace := ?psu (ksPSpace s)\<rparr>"
by simp
from psp_in_sr
have msu_in_sr:
"(ksMachineState_update (underlying_memory_update ?mmu)
@ -1724,7 +1821,8 @@ proof -
apply (simp add: rf_sr_def)
apply (clarsimp simp add: cstate_relation_def Let_def)
apply (rule conjI[rotated])
apply (simp add: cmachine_state_relation_def)
apply (simp add: cmachine_state_relation_def
s_ksPSpace_adjust)
apply (clarsimp simp add: cpspace_relation_def h2pd_eq)
done

10
proof/crefine/Finalise_C.thy
View File

@ -1330,13 +1330,19 @@ lemma pageTableMapped_ccorres:
apply csymbr
apply (rule_tac xf'=pde_' and r'=cpde_relation in ccorres_split_nothrow_novcg)
apply (rule ccorres_add_return2, rule ccorres_pre_getObject_pde)
apply (rule_tac P="ko_at' x (lookup_pd_slot rv vaddr) and no_0_obj'"
apply (rule_tac P="ko_at' x (lookup_pd_slot rv vaddr) and no_0_obj'
and page_directory_at' rv"
in ccorres_from_vcg[where P'=UNIV])
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: return_def lookup_pd_slot_def Let_def)
apply (drule(1) page_directory_at_rf_sr)
apply (erule cmap_relationE1[OF rf_sr_cpde_relation],
erule ko_at_projectKO_opt)
apply (clarsimp simp: typ_heap_simps' shiftl_t2n field_simps)
apply (erule clift_array_assertion_imp, simp+)
apply (rule_tac x=0 in exI, simp add: unat_def[symmetric])
apply (rule unat_le_helper, simp)
apply ((thin_tac P for P)+, word_bitwise)
apply ceqv
apply (rule_tac P="rv \<noteq> 0" in ccorres_gen_asm)
apply csymbr+
@ -2027,4 +2033,4 @@ lemma finaliseCap_ccorres:
done
end
end
end

2
proof/crefine/IpcCancel_C.thy
View File

@ -143,7 +143,7 @@ lemma tcbEPDequeue_spec:
apply assumption
apply simp
apply (frule c_guard_clift)
apply (simp add: typ_heap_simps)
apply (simp add: typ_heap_simps')
apply (intro allI conjI impI)
apply (clarsimp simp add: typ_heap_simps h_t_valid_clift_Some_iff)
apply (clarsimp simp: typ_heap_simps h_t_valid_clift_Some_iff

72
proof/crefine/Ipc_C.thy
View File

@ -890,12 +890,34 @@ lemmas ccorres_pre_stateAssert =
declare setRegister_ccorres[corres]
lemma storeWordUser_array_ipcBuffer_ccorres:
"ccorres dc xfdc (valid_ipc_buffer_ptr' ptr and valid_pspace' and (\<lambda>s. off < 2 ^ msg_align_bits))
(UNIV \<inter> {s. ptr' s = Ptr ptr} \<inter> {s. off = of_int (n' s) * 4}
\<inter> {s. n'' s = Suc (nat (n' s))} \<inter> {s. w' s = w}) hs
(storeWordUser (ptr + off) w)
(Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>(\<lambda>s. ptr_add (ptr' s) (n' s))\<rbrace>
(Guard gname \<lbrace>array_assertion \<acute>(\<lambda>s. ptr' s) \<acute>(\<lambda>s. n'' s) (hrs_htd \<acute>t_hrs)\<rbrace>
(Basic (\<lambda>s. globals_update (t_hrs_'_update
(hrs_mem_update (heap_update (ptr_add (ptr' s) (n' s)) (w' s)))) s))))"
apply (rule ccorres_guard_imp2)
apply (rule ccorres_second_Guard)
apply (rule storeWordUser_ccorres)
apply (clarsimp simp: Collect_const_mem)
apply (subst valid_ipc_buffer_ptr_array, simp+)
defer
apply simp
defer
apply (clarsimp simp: valid_ipc_buffer_ptr'_def msg_align_bits
is_aligned_add[OF is_aligned_weaken]
is_aligned_mult_triv2[where n=2, simplified])
sorry
lemma setMR_ccorres:
notes if_cong[cong]
shows
"ccorres (\<lambda>r r'. r = unat (r' && mask msgLengthBits)) ret__unsigned_'
(valid_pspace' and (\<lambda>_. offset < msgMaxLength
\<and> is_aligned (option_to_0 buf) msg_align_bits))
(valid_pspace' and case_option \<top> valid_ipc_buffer_ptr' buf
and (\<lambda>s. offset < msgMaxLength))
(UNIV \<inter> {s. offset_' s = of_nat offset} \<inter> {s. reg_' s = v}
\<inter> {s. receiver_' s = tcb_ptr_to_ctcb_ptr thread}
\<inter> {s. receiveIPCBuffer_' s = option_to_ptr buf}) []
@ -914,15 +936,17 @@ lemma setMR_ccorres:
apply (rule ccorres_return_C, simp+)[1]
apply (simp add: option_to_ptr_def option_to_0_def Collect_True
ccorres_cond_iffs
del: Collect_const)
apply (simp add: storeWordUser_def bind_assoc del: Collect_const)
apply (rule ccorres_pre_stateAssert)
del: Collect_const ptr_add_def')
apply (rule ccorres_cond_true)
apply (ctac add: storeWord_ccorres[simplified])
apply (rule ccorres_split_nothrow_novcg)
apply (rule storeWordUser_array_ipcBuffer_ccorres)
apply ceqv
apply (rule ccorres_return_C, simp+)[1]
apply wp
apply (simp del: Collect_const)
apply vcg
apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem)
apply (simp add: msgLengthBits_def msgMaxLength_def
unat_arith_simps less_mask_eq unat_of_nat
del: Collect_const)
apply ctac
apply (rule ccorres_return_C, simp+)[1]
apply wp
@ -930,26 +954,14 @@ lemma setMR_ccorres:
apply (vcg exspec=setRegister_modifies)
apply (simp add: Collect_const_mem option_to_0_def)
apply (intro impI conjI allI, simp_all)
apply (rule aligned_add_aligned[where n=msg_align_bits])
apply simp
apply (rule is_aligned_mult_triv2
[where n=2, simplified, folded word_size_def])
apply (simp add: msg_align_bits)
apply (simp add: msgRegisters_unfold n_msgRegisters_def
msgLengthBits_def mask_def)
apply (simp add: word_size_def)
apply (clarsimp simp: word_size_def field_simps pointerInUserData_c_guard)
apply (simp add: unat_of_nat32 msgMaxLength_unfold word_bits_def
unat_add_lem[THEN iffD1] less_mask_eq msgLengthBits_def
word_less_nat_alt)
apply (clarsimp simp: word_size_def field_simps pointerInUserData_h_t_valid)
apply (clarsimp simp: pointerInUserData_def typ_at_to_obj_at_arches
mask_out_sub_mask)
apply (subst(asm) less_mask_eq)
apply (simp add: word_size_def pageBits_def msgMaxLength_unfold)
apply (simp add: unat_add_lem[THEN iffD1] word_less_nat_alt
unat_mult_lem[THEN iffD1] unat_of_nat32 word_bits_def)
apply clarsimp
apply (simp add: msg_align_bits word_size_def msgMaxLength_def
length_msgRegisters n_msgRegisters_def)
apply (simp add: unat_word_ariths
word_less_nat_alt unat_of_nat)
apply (simp add: msgRegisters_unfold n_msgRegisters_def
msgLengthBits_def mask_def)
apply (simp add: word_size_def)
apply (clarsimp simp: valid_ipc_buffer_ptr'_def)
apply (simp add: unat_of_nat32 word_bits_def msgMaxLength_unfold
word_le_nat_alt msgRegisters_ccorres n_msgRegisters_def)
apply (simp add: unat_of_nat32 msgMaxLength_unfold word_bits_def
@ -960,8 +972,8 @@ lemma setMR_ccorres:
lemma setMR_ccorres_dc:
"ccorres dc xfdc
(valid_pspace' and (\<lambda>_. offset < msgMaxLength
\<and> is_aligned (option_to_0 buf) msg_align_bits))
(valid_pspace' and case_option \<top> valid_ipc_buffer_ptr' buf
and (\<lambda>s. offset < msgMaxLength))
(UNIV \<inter> {s. offset_' s = of_nat offset} \<inter> {s. reg_' s = v}
\<inter> {s. receiver_' s = tcb_ptr_to_ctcb_ptr thread}
\<inter> {s. receiveIPCBuffer_' s = option_to_ptr buf}) []

18
proof/crefine/PSpace_C.thy
View File

@ -94,9 +94,12 @@ lemma setObject_ccorres_helper:
done
lemma carray_map_relation_upd_triv:
"f x = Some (v :: 'a :: pspace_storable)
\<Longrightarrow> carray_map_relation n (f (x \<mapsto> y)) hp ptrf = carray_map_relation n f hp ptrf"
by (simp add: carray_map_relation_def objBits_def objBitsT_koTypeOf[symmetric]
koTypeOf_injectKO
del: objBitsT_koTypeOf)
lemma storePTE_Basic_ccorres':
"\<lbrakk> cpte_relation pte pte' \<rbrakk> \<Longrightarrow>
@ -117,7 +120,8 @@ lemma storePTE_Basic_ccorres':
apply (rule conjI)
apply (clarsimp simp: cpspace_relation_def typ_heap_simps
update_pte_map_to_ptes
update_pte_map_tos)
update_pte_map_tos
carray_map_relation_upd_triv)
apply (case_tac "f x", simp)
@ -127,7 +131,8 @@ lemma storePTE_Basic_ccorres':
carch_state_relation_def
cmachine_state_relation_def
Let_def typ_heap_simps
cteCaps_of_def update_pte_map_tos)
cteCaps_of_def update_pte_map_tos
)
done
@ -174,7 +179,8 @@ lemma storePDE_Basic_ccorres':
apply (rule conjI)
apply (clarsimp simp: cpspace_relation_def typ_heap_simps
update_pde_map_to_pdes
update_pde_map_tos)
update_pde_map_tos
carray_map_relation_upd_triv)
apply (erule cmap_relation_updI,
erule ko_at_projectKO_opt, simp+)
apply (simp add: cready_queues_relation_def

4
proof/crefine/Recycle_C.thy
View File

@ -565,7 +565,7 @@ lemma clearMemory_setObject_PTE_ccorres:
apply (clarsimp simp: rf_sr_def Let_def cstate_relation_def typ_heap_simps)
apply (rule conjI)
apply (simp add: cpspace_relation_def typ_heap_simps update_pte_map_tos
update_pte_map_to_ptes)
update_pte_map_to_ptes carray_map_relation_upd_triv)
apply (rule cmap_relation_updI, simp_all)[1]
apply (simp add: cpte_relation_def Let_def pte_lift_def
fcp_beta pte_get_tag_def pte_tag_defs)
@ -828,7 +828,7 @@ lemma arch_recycleCap_ccorres:
apply (clarsimp simp: rf_sr_def Let_def cstate_relation_def typ_heap_simps)
apply (rule conjI)
apply (simp add: cpspace_relation_def typ_heap_simps update_pde_map_tos
update_pde_map_to_pdes)
update_pde_map_to_pdes carray_map_relation_upd_triv)
apply (rule cmap_relation_updI, simp_all)[1]
apply (simp add: cpde_relation_def Let_def pde_lift_def
fcp_beta pde_get_tag_def pde_tag_defs)

770
proof/crefine/Retype_C.thy
View File

File diff suppressed because it is too large Load Diff

21
proof/crefine/SR_lemmas_C.thy
View File

@ -509,7 +509,8 @@ lemma fst_setCTE:
(map_to_asidpools (ksPSpace s) = map_to_asidpools (ksPSpace s'));
(map_to_user_data (ksPSpace s) = map_to_user_data (ksPSpace s'));
(option_map tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s)
= option_map tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s')) \<rbrakk> \<Longrightarrow> P"
= option_map tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'));
\<forall>T p. typ_at' T p s = typ_at' T p s'\<rbrakk> \<Longrightarrow> P"
shows "P"
proof -
(* Unpack the existential and bind x, theorems in this. Yuck *)
@ -596,7 +597,12 @@ proof -
thus "(projectKO_opt (the (ksPSpace s' x)) :: user_data option) = projectKO_opt (the (ksPSpace s x))" using ko ko'
by simp
qed fact
note sta = setCTE_typ_at'[where P="\<lambda>x. x = y" for y]
show typ_at: "\<forall>T p. typ_at' T p s = typ_at' T p s'"
using use_valid[OF _ sta, OF thms(1), OF refl]
by auto
show "option_map tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s) =
option_map tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s')"
proof (rule ext)
@ -1998,6 +2004,17 @@ lemma gs_set_assn_Delete_cstate_relation:
cteDeleteOne_'proc_def cap_get_capSizeBits_'proc_def)
done
lemma update_typ_at:
assumes at: "obj_at' P p s"
and tp: "\<forall>obj. P obj \<longrightarrow> koTypeOf (injectKOS obj) = koTypeOf ko"
shows "typ_at' T p' (s \<lparr>ksPSpace := ksPSpace s(p \<mapsto> ko)\<rparr>) = typ_at' T p' s"
using at
by (auto elim!: obj_atE' simp: typ_at'_def ko_wp_at'_def
dest!: tp[rule_format]
simp: project_inject projectKO_eq split: kernel_object.splits split_if_asm,
simp_all add: objBits_def objBitsT_koTypeOf[symmetric] ps_clear_upd
del: objBitsT_koTypeOf)
end
end

43
proof/crefine/StateRelation_C.thy
View File

@ -48,6 +48,20 @@ definition
(addr_fun ` (dom as) = dom cs) \<and>
(\<forall>x \<in> dom as. rel (the (as x)) (the (cs (addr_fun x))))"
definition
carray_map_relation :: "nat \<Rightarrow> (word32 \<rightharpoonup> ('a :: pre_storable))
\<Rightarrow> ('b ptr \<Rightarrow> bool) \<Rightarrow> (word32 \<Rightarrow> 'b ptr) \<Rightarrow> bool"
where
"carray_map_relation bits as cs addr_fun \<equiv>
(\<forall>p. (is_aligned p bits \<and> (\<forall>p'. p' && ~~ mask bits = p \<and> is_aligned p' (objBits (the (as p')))
\<longrightarrow> p' \<in> dom as)) \<longleftrightarrow> cs (addr_fun p))"
definition
cvariable_array_map_relation :: "(word32 \<rightharpoonup> 'a) \<Rightarrow> ('a \<Rightarrow> nat)
\<Rightarrow> (word32 \<Rightarrow> ('c :: c_type) ptr) \<Rightarrow> heap_typ_desc \<Rightarrow> bool"
where
"cvariable_array_map_relation amap szs ptrfun htd
\<equiv> \<forall>p v. amap p = Some v \<longrightarrow> array_assertion (ptrfun p) (szs v) htd"
definition
asid_map_pd_to_hwasids :: "(asid \<rightharpoonup> hw_asid \<times> obj_ref) \<Rightarrow> (obj_ref \<Rightarrow> hw_asid set)"
@ -120,11 +134,6 @@ where
exclusive_state s = exclusive_state (phantom_machine_state_' s') \<and>
machine_state_rest s = machine_state_rest (phantom_machine_state_' s')"
(* ptr_range uses the wrong set construct for h_t_valid stuff *)
definition
ptr_span :: "'a::mem_type ptr \<Rightarrow> word32 set" where
"ptr_span p \<equiv> {ptr_val p ..+ size_of TYPE('a)}"
definition
"globals_list_id_fudge = id"
@ -513,13 +522,26 @@ abbreviation
abbreviation
"cpspace_user_data_relation ah bh ch \<equiv> cmap_relation (heap_to_page_data ah bh) (clift ch) Ptr cuser_data_relation"
abbreviation
pd_Ptr :: "32 word \<Rightarrow> (pde_C[4096]) ptr" where "pd_Ptr == Ptr"
abbreviation
"cpspace_pde_array_relation ah ch \<equiv> carray_map_relation pdBits (map_to_pdes ah) (h_t_valid (hrs_htd ch) c_guard) pd_Ptr"
abbreviation
pt_Ptr :: "32 word \<Rightarrow> (pte_C[256]) ptr" where "pt_Ptr == Ptr"
abbreviation
"cpspace_pte_array_relation ah ch \<equiv> carray_map_relation ptBits (map_to_ptes ah) (h_t_valid (hrs_htd ch) c_guard) pt_Ptr"
definition
cpspace_relation :: "(word32 \<rightharpoonup> Structures_H.kernel_object) \<Rightarrow> (word32 \<Rightarrow> word8) \<Rightarrow> heap_raw_state \<Rightarrow> bool"
where
"cpspace_relation ah bh ch \<equiv>
cpspace_cte_relation ah ch \<and> cpspace_tcb_relation ah ch \<and> cpspace_ep_relation ah ch \<and> cpspace_ntfn_relation ah ch \<and>
cpspace_pde_relation ah ch \<and> cpspace_pte_relation ah ch \<and> cpspace_asidpool_relation ah ch \<and> cpspace_user_data_relation ah bh ch"
cpspace_pde_relation ah ch \<and> cpspace_pte_relation ah ch \<and> cpspace_asidpool_relation ah ch \<and> cpspace_user_data_relation ah bh ch \<and>
cpspace_pde_array_relation ah ch \<and> cpspace_pte_array_relation ah ch"
abbreviation
"sched_queue_relation' \<equiv> tcb_queue_relation' tcbSchedNext_C tcbSchedPrev_C"
@ -546,6 +568,11 @@ where
prio \<ge> ucast minPrio \<and> prio \<le> ucast maxPrio) \<longrightarrow> aqueues (qdom, prio) = [])"
abbreviation
"cte_array_relation astate cstate
\<equiv> cvariable_array_map_relation (gsCNodes astate) (\<lambda>n. 2 ^ n)
cte_Ptr (hrs_htd (t_hrs_' cstate))"
fun
irqstate_to_C :: "irqstate \<Rightarrow> word32"
where
@ -576,9 +603,6 @@ where
ucast (fst adomSched) = dschedule_C.domain_C cdomSched \<and>
(snd adomSched) = dschedule_C.length_C cdomSched"
abbreviation
pd_Ptr :: "32 word \<Rightarrow> (pde_C[4096]) ptr" where "pd_Ptr == Ptr"
definition
cdom_schedule_relation :: "(8 word \<times> 32 word) list \<Rightarrow> (dschedule_C['b :: finite]) \<Rightarrow> bool"
where
@ -629,6 +653,7 @@ where
(ksSchedulerAction_' cstate) \<and>
carch_state_relation (ksArchState astate) cstate \<and>
cmachine_state_relation (ksMachineState astate) cstate \<and>
cte_array_relation astate cstate \<and>
apsnd fst (ghost'state_' cstate) = (gsUserPages astate, gsCNodes astate) \<and>
ghost_size_rel (ghost'state_' cstate) (gsMaxObjectSize astate) \<and>
ksWorkUnitsCompleted_' cstate = ksWorkUnitsCompleted astate \<and>

40
proof/crefine/SyscallArgs_C.thy
View File

@ -12,8 +12,7 @@ theory SyscallArgs_C
imports
TcbQueue_C
CSpace_RAB_C
StoreWord_C
DetWP
StoreWord_C DetWP
begin
declare word_neq_0_conv[simp del]
@ -733,7 +732,7 @@ lemma threadGet_tcbIpcBuffer_ccorres [corres]:
apply clarsimp
apply (clarsimp simp: return_def typ_heap_simps')
apply (clarsimp simp: obj_at'_def ctcb_relation_def)
done
done
(* FIXME: move *)
lemma ccorres_case_bools:
@ -1143,6 +1142,32 @@ lemma scast_ucast_add_one [simp]:
apply clarsimp
done
lemma valid_ipc_buffer_ptr_array:
"valid_ipc_buffer_ptr' (ptr_val p) s \<Longrightarrow> (s, s') \<in> rf_sr
\<Longrightarrow> n < 2 ^ (msg_align_bits - 2)
\<Longrightarrow> n \<noteq> 0
\<Longrightarrow> array_assertion (p :: word32 ptr) n (hrs_htd (t_hrs_' (globals s')))"
apply (clarsimp simp: valid_ipc_buffer_ptr'_def typ_at_to_obj_at_arches)
apply (drule obj_at_ko_at', clarsimp)
apply (drule rf_sr_heap_relation)
apply (erule cmap_relationE1)
apply (clarsimp simp: heap_to_page_data_def Let_def)
apply (rule conjI, rule exI, erule ko_at_projectKO_opt)
apply (rule refl)
apply (drule clift_field, rule user_data_C_words_C_fl_ti, simp)
apply (erule clift_array_assertion_imp, simp+)
apply (simp add: field_lvalue_def msg_align_bits)
apply (rule_tac x="unat (ptr_val p && mask pageBits >> 2)" in exI,
simp add: word32_shift_by_2 shiftr_shiftl1
is_aligned_andI1[OF is_aligned_weaken])
apply (simp add: add.commute word_plus_and_or_coroll2)
apply (cut_tac x="(ptr_val p && mask pageBits ) >> 2"
and n="2 ^ (pageBits - 2) - 2 ^ (msg_align_bits - 2)" in unat_le_helper)
apply (simp add: pageBits_def msg_align_bits mask_def is_aligned_mask)
apply word_bitwise
apply simp
apply (simp add: msg_align_bits pageBits_def)
done
lemma getSyscallArg_ccorres_foo:
"ccorres (\<lambda>a rv. rv = args ! n) ret__unsigned_long_'
@ -1186,7 +1211,8 @@ lemma getSyscallArg_ccorres_foo:
apply (rule ccorres_seq_skip [THEN iffD2])
apply (rule ccorres_add_return2)
apply (rule ccorres_symb_exec_l)
apply (rule_tac P="\<lambda>s. user_word_at (x!n) (ptr_val (CTypesDefs.ptr_add ipc_buffer (of_nat n + 1))) s"
apply (rule_tac P="\<lambda>s. user_word_at (x!n) (ptr_val (CTypesDefs.ptr_add ipc_buffer (of_nat n + 1))) s
\<and> valid_ipc_buffer_ptr' (ptr_val ipc_buffer) s \<and> n < msgMaxLength"
and P'=UNIV
in ccorres_from_vcg_throws)
apply (simp add: return_def split del: split_if)
@ -1198,6 +1224,10 @@ lemma getSyscallArg_ccorres_foo:
apply simp
apply (clarsimp simp: mult.commute mult.left_commute ucast_nat_def')
apply (clarsimp simp: CTypesDefs.ptr_add_def)
apply (subst valid_ipc_buffer_ptr_array, assumption+)
apply (simp add: unat_def[symmetric] msg_align_bits
msgMaxLength_def unat_arith_simps)
apply simp
apply (frule (1) user_word_at_cross_over)
apply simp
apply (clarsimp simp: mult.commute mult.left_commute ucast_nat_def)
@ -1208,7 +1238,7 @@ lemma getSyscallArg_ccorres_foo:
msgLength mi \<le> msgMaxLength \<and> scast n_msgRegisters \<le> i"
in hoare_pre(1))
apply (wp getMRs_user_word)
apply clarsimp
apply (clarsimp simp: msgMaxLength_def unat_less_helper)
apply simp
apply (clarsimp simp: sysargs_rel_def sysargs_rel_n_def)
apply (rule conjI, clarsimp simp: unat_of_nat32 word_bits_def)

21
proof/crefine/TcbQueue_C.thy
View File

@ -1101,21 +1101,6 @@ proof -
done
qed
(* FIXME: move to SR_lemmas_C *)
(* FIXME: remove old version *)
lemma update_tcb_map_tos:
fixes P :: "tcb \<Rightarrow> bool"
assumes at: "obj_at' P p s"
shows "map_to_eps (ksPSpace s(p \<mapsto> KOTCB ko)) = map_to_eps (ksPSpace s)"
and "map_to_ntfns (ksPSpace s(p \<mapsto> KOTCB ko)) = map_to_ntfns (ksPSpace s)"
and "map_to_pdes (ksPSpace s(p \<mapsto> KOTCB ko)) = map_to_pdes (ksPSpace s)"
and "map_to_ptes (ksPSpace s(p \<mapsto> KOTCB ko)) = map_to_ptes (ksPSpace s)"
and "map_to_asidpools (ksPSpace s(p \<mapsto> KOTCB ko)) = map_to_asidpools (ksPSpace s)"
and "map_to_user_data (ksPSpace s(p \<mapsto> KOTCB ko)) = map_to_user_data (ksPSpace s)"
using at
by (auto elim!: obj_atE' intro!: map_to_ctes_upd_other map_comp_eqI
simp: projectKOs projectKO_opts_defs split: kernel_object.splits split_if_asm)+
lemma rf_sr_tcb_update_no_queue:
"\<lbrakk> (s, s') \<in> rf_sr; ko_at' tcb thread s;
(cslift t :: tcb_C typ_heap) = (cslift s')(tcb_ptr_to_ctcb_ptr thread \<mapsto> ctcb);
@ -1130,7 +1115,8 @@ lemma rf_sr_tcb_update_no_queue:
\<rbrakk>
\<Longrightarrow> (s\<lparr>ksPSpace := ksPSpace s(thread \<mapsto> KOTCB tcb')\<rparr>, x\<lparr>globals := globals s'\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr"
unfolding rf_sr_def state_relation_def cstate_relation_def cpspace_relation_def
apply (clarsimp simp: Let_def update_tcb_map_tos map_to_ctes_upd_tcb_no_ctes heap_to_page_data_def)
apply (clarsimp simp: Let_def update_tcb_map_tos map_to_ctes_upd_tcb_no_ctes
heap_to_page_data_def)
apply (frule (1) cmap_relation_ko_atD)
apply (erule obj_atE')
apply (clarsimp simp: projectKOs)
@ -1179,7 +1165,8 @@ lemma rf_sr_tcb_update_not_in_queue:
\<Longrightarrow> (s\<lparr>ksPSpace := ksPSpace s(thread \<mapsto> KOTCB tcb')\<rparr>,
x\<lparr>globals := globals s'\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr"
unfolding rf_sr_def state_relation_def cstate_relation_def cpspace_relation_def
apply (clarsimp simp: Let_def update_tcb_map_tos map_to_ctes_upd_tcb_no_ctes heap_to_page_data_def)
apply (clarsimp simp: Let_def update_tcb_map_tos map_to_ctes_upd_tcb_no_ctes
heap_to_page_data_def)
apply (frule (1) cmap_relation_ko_atD)
apply (erule obj_atE')
apply (clarsimp simp: projectKOs)

100
proof/crefine/Tcb_C.thy
View File

@ -1568,6 +1568,10 @@ lemma is_aligned_the_x_strengthen:
"x \<noteq> None \<and> case_option \<top> valid_ipc_buffer_ptr' x s \<longrightarrow> is_aligned (the x) msg_align_bits"
by (clarsimp simp: valid_ipc_buffer_ptr'_def)
lemma valid_ipc_buffer_ptr_the_strengthen:
"x \<noteq> None \<and> case_option \<top> valid_ipc_buffer_ptr' x s \<longrightarrow> valid_ipc_buffer_ptr' (the x) s"
by clarsimp
lemma lookupIPCBuffer_Some_0:
"\<lbrace>\<top>\<rbrace> lookupIPCBuffer w t \<lbrace>\<lambda>rv s. rv \<noteq> Some 0\<rbrace>"
apply (simp add: lookupIPCBuffer_def
@ -1580,6 +1584,32 @@ lemma lookupIPCBuffer_Some_0:
apply (rule hoare_vcg_prop , simp add:hoare_TrueI)
done
lemma storeWordUser_array_ipcBuffer_ccorres:
"ccorres dc xfdc (valid_ipc_buffer_ptr' ptr and valid_pspace' and (\<lambda>s. off < 2 ^ msg_align_bits))
(UNIV \<inter> {s. ptr' s = Ptr ptr} \<inter> {s. off = of_int (n' s) * 4}
\<inter> {s. n'' s = Suc (nat (n' s))} \<inter> {s. w' s = w}) hs
(storeWordUser (ptr + off) w)
(Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>(\<lambda>s. ptr_add (ptr' s) (n' s))\<rbrace>
(Guard gname \<lbrace>array_assertion \<acute>(\<lambda>s. ptr' s) \<acute>(\<lambda>s. n'' s) (hrs_htd \<acute>t_hrs)\<rbrace>
(Basic (\<lambda>s. globals_update (t_hrs_'_update
(hrs_mem_update (heap_update (ptr_add (ptr' s) (n' s)) (w' s)))) s))))"
apply (rule ccorres_guard_imp2)
apply (rule ccorres_second_Guard)
apply (rule storeWordUser_ccorres)
apply (clarsimp simp: Collect_const_mem)
apply (subst valid_ipc_buffer_ptr_array, simp+)
defer
apply simp
defer
apply (clarsimp simp: valid_ipc_buffer_ptr'_def msg_align_bits
is_aligned_add[OF is_aligned_weaken]
is_aligned_mult_triv2[where n=2, simplified])
sorry
find_theorems lookupIPCBuffer valid_ipc_buffer_ptr'
lemma asUser_valid_ipc_buffer_ptr':
"\<lbrace> valid_ipc_buffer_ptr' p \<rbrace> asUser t m \<lbrace> \<lambda>rv s. valid_ipc_buffer_ptr' p s \<rbrace>"
by (simp add: valid_ipc_buffer_ptr'_def, wp, auto simp: valid_ipc_buffer_ptr'_def)
lemma invokeTCB_ReadRegisters_ccorres:
notes
min_simps [simp del]
@ -1703,26 +1733,29 @@ shows
rule_tac F="\<lambda>m s. obj_at' (\<lambda>tcb. map (tcbContext tcb) (genericTake n
(State_H.frameRegisters @ State_H.gpRegisters))
= reply) target s
\<and> is_aligned (the rva) msg_align_bits \<and> valid_pspace' s"
\<and> valid_ipc_buffer_ptr' (the rva) s
\<and> valid_pspace' s"
and i="unat n_msgRegisters"
in ccorres_mapM_x_while')
apply (clarsimp simp: less_diff_conv)
apply (intro allI impI, elim conjE exE, hypsubst, simp)
apply (simp add: less_diff_conv)
apply (rule ccorres_guard_imp2)
apply (rule ccorres_add_return,
ctac add: getRegister_ccorres_defer[where thread=target])
apply (rule storeWordUser_ccorres)
apply (rule storeWordUser_array_ipcBuffer_ccorres)
apply wp
apply (vcg exspec=getRegister_modifies)
apply (clarsimp simp: obj_at'_weakenE[OF _ TrueI]
word_size)
apply (intro conjI[rotated] impI allI)
apply (simp add: n_msgRegisters_def n_frameRegisters_def
word_less_nat_alt)
apply (subst unat_add_lem[THEN iffD1], simp_all add: unat_of_nat)[1]
apply (erule sym)
apply (simp add: option_to_ptr_def option_to_0_def
apply (simp add: n_msgRegisters_def n_frameRegisters_def
word_less_nat_alt)
apply (subst unat_add_lem[THEN iffD1], simp_all add: unat_of_nat)[1]
apply (erule sym)
apply (simp add: option_to_ptr_def option_to_0_def
msg_registers_convs upto_enum_word wordSize_def'
del: upt.simps)
del: upt.simps)
apply (simp add: option_to_ptr_def option_to_0_def)
apply (rule frame_gp_registers_convs)
apply (simp add: frame_gp_registers_convs less_diff_conv)
apply (subst iffD1 [OF unat_add_lem])
@ -1731,9 +1764,11 @@ shows
word_le_nat_alt unat_of_nat)
apply (simp add: n_frameRegisters_def n_msgRegisters_def
unat_of_nat)
apply (erule aligned_add_aligned)
apply (simp add: word32_shift_by_2 is_aligned_shiftl_self)
apply (simp add: msg_align_bits)
apply (simp add: msg_registers_convs n_msgRegisters_def
msgMaxLength_def n_frameRegisters_def
upto_enum_word_nth msg_align_bits
)
apply (simp add: unat_word_ariths word_less_nat_alt unat_of_nat)
apply (clarsimp simp: getRegister_def submonad_asUser.guarded_gets
obj_at'_weakenE[OF _ TrueI])
apply (clarsimp simp: asUser_fetch_def simpler_gets_def
@ -1802,35 +1837,38 @@ shows
apply (rule_tac F="\<lambda>m s. obj_at' (\<lambda>tcb. map (tcbContext tcb) (genericTake n
(State_H.frameRegisters @ State_H.gpRegisters))
= reply) target s
\<and> is_aligned (the rva) msg_align_bits \<and> valid_pspace' s"
\<and> valid_ipc_buffer_ptr' (the rva) s \<and> valid_pspace' s"
and i="0" in ccorres_mapM_x_while')
apply (clarsimp simp: less_diff_conv drop_zip)
apply (rule ccorres_guard_imp2)
apply (rule ccorres_add_return,
ctac add: getRegister_ccorres_defer[where thread=target])
apply (rule storeWordUser_ccorres)
apply (rule storeWordUser_array_ipcBuffer_ccorres)
apply wp
apply (vcg exspec=getRegister_modifies)
apply (clarsimp simp: obj_at'_weakenE[OF _ TrueI]
word_size)
apply (intro conjI[rotated] impI allI)
apply (simp add: n_frameRegisters_def n_msgRegisters_def
length_msgRegisters word_of_nat_less
n_gpRegisters_def)
apply (erule sym)
apply (simp add: option_to_ptr_def option_to_0_def
msg_registers_convs upto_enum_word
n_msgRegisters_def n_frameRegisters_def
n_gpRegisters_def msgMaxLength_def msgLengthBits_def
del: upt.simps upt_rec_numeral)
apply (simp add: min_def split: split_if_asm)
apply (simp add: n_frameRegisters_def n_msgRegisters_def
length_msgRegisters word_of_nat_less
n_gpRegisters_def)
apply (erule sym)
apply (simp add: option_to_ptr_def option_to_0_def
msg_registers_convs upto_enum_word
n_msgRegisters_def n_frameRegisters_def
n_gpRegisters_def msgMaxLength_def msgLengthBits_def
del: upt.simps upt_rec_numeral)
apply (simp add: min_def split: split_if_asm)
apply (simp add: option_to_ptr_def option_to_0_def)
apply (rule frame_gp_registers_convs)
apply (simp add: frame_gp_registers_convs n_msgRegisters_def n_frameRegisters_def
n_gpRegisters_def msgMaxLength_def msgLengthBits_def
unat_of_nat)
apply (erule aligned_add_aligned)
apply (simp add: word32_shift_by_2 is_aligned_shiftl_self)
apply (simp add: msg_align_bits)
apply (simp add: msg_registers_convs n_msgRegisters_def
msgMaxLength_def n_frameRegisters_def
upto_enum_word_nth msg_align_bits
)
apply (simp add: unat_word_ariths word_less_nat_alt unat_of_nat)
apply (clarsimp simp: getRegister_def submonad_asUser.guarded_gets
obj_at'_weakenE[OF _ TrueI])
apply (clarsimp simp: asUser_fetch_def simpler_gets_def
@ -1905,7 +1943,8 @@ shows
apply simp
apply (rule mapM_x_wp')
apply (rule hoare_pre)
apply (wp asUser_obj_at'[where t'=target] static_imp_wp)
apply (wp asUser_obj_at'[where t'=target] static_imp_wp
asUser_valid_ipc_buffer_ptr')
apply clarsimp
apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem
msg_registers_convs n_msgRegisters_def
@ -1914,10 +1953,11 @@ shows
word_less_nat_alt unat_of_nat)
apply (simp add: min_def split: split_if_asm)
apply (wp_once hoare_drop_imps)
apply (wp asUser_obj_at'[where t'=target] static_imp_wp)
apply (wp asUser_obj_at'[where t'=target] static_imp_wp
asUser_valid_ipc_buffer_ptr')
apply (vcg exspec=setRegister_modifies)
apply simp
apply (strengthen is_aligned_the_x_strengthen)
apply (strengthen valid_ipc_buffer_ptr_the_strengthen)
apply simp
apply (wp lookupIPCBuffer_Some_0 | wp_once hoare_drop_imps)+
apply (simp add: Collect_const_mem State_H.badgeRegister_def

272
proof/crefine/VSpace_C.thy
View File

@ -162,6 +162,28 @@ lemma rf_sr_asid_map_pd_to_hwasids:
by (simp add: rf_sr_def cstate_relation_def Let_def
carch_state_relation_def)
lemma page_directory_at_carray_map_relation:
"\<lbrakk> page_directory_at' pd s; cpspace_pde_array_relation (ksPSpace s) hp \<rbrakk>
\<Longrightarrow> clift hp (pd_Ptr pd) \<noteq> None"
apply (clarsimp simp: carray_map_relation_def h_t_valid_clift_Some_iff)
apply (drule spec, erule iffD1)
apply (clarsimp simp: page_directory_at'_def)
apply (drule_tac x="p' && mask pdBits >> 2" in spec)
apply (clarsimp simp: shiftr_shiftl1)
apply (drule mp)
apply (simp add: shiftr_over_and_dist pdBits_def pageBits_def mask_def
order_le_less_trans[OF word_and_le1])
apply (clarsimp simp: typ_at_to_obj_at_arches objBits_simps archObjSize_def
is_aligned_andI1 add.commute word_plus_and_or_coroll2
dest!: obj_at_ko_at' ko_at_projectKO_opt)
done
lemma page_directory_at_rf_sr:
"\<lbrakk> page_directory_at' pd s; (s, s') \<in> rf_sr \<rbrakk>
\<Longrightarrow> cslift s' (pd_Ptr pd) \<noteq> None"
by (clarsimp simp: rf_sr_def cstate_relation_def Let_def
cpspace_relation_def page_directory_at_carray_map_relation)
lemma pd_at_asid_cross_over:
"\<lbrakk> pd_at_asid' pd asid s; asid \<le> mask asid_bits;
(s, s') \<in> rf_sr\<rbrakk>
@ -170,6 +192,7 @@ lemma pd_at_asid_cross_over:
\<and> index ap (unat (asid && 2 ^ asid_low_bits - 1)) = pde_Ptr pd
\<and> cslift s' (pde_Ptr (pd + 0x3FC0)) = Some pde
\<and> is_aligned pd pdBits
\<and> array_assertion (pde_Ptr pd) 4096 (hrs_htd (t_hrs_' (globals s')))
\<and> (valid_pde_mappings' s \<longrightarrow> pde_get_tag pde = scast pde_pde_invalid)"
apply (clarsimp simp: pd_at_asid'_def)
apply (subgoal_tac "asid >> asid_low_bits \<le> 2 ^ asid_high_bits - 1")
@ -192,12 +215,14 @@ lemma pd_at_asid_cross_over:
split: asid_pool_C.split_asm)
apply (drule spec, drule sym [OF mp])
apply (rule_tac y=asid in word_and_le1)
apply (frule(1) page_directory_at_rf_sr)
apply (clarsimp simp: mask_2pm1[symmetric] option_to_ptr_def option_to_0_def
page_directory_at'_def typ_at_to_obj_at_arches)
apply (drule_tac x="pd_asid_slot" in spec, simp add: pd_asid_slot_def)
apply (drule obj_at_ko_at'[where 'a=pde], clarsimp)
apply (rule cmap_relationE1 [OF rf_sr_cpde_relation],
assumption, erule ko_at_projectKO_opt)
apply (subst array_ptr_valid_array_assertionI, erule h_t_valid_clift, simp+)
apply (clarsimp simp: valid_pde_mappings'_def)
apply (elim allE, drule(1) mp)
apply (simp add: valid_pde_mapping'_def valid_pde_mapping_offset'_def
@ -253,6 +278,7 @@ lemma loadHWASID_ccorres:
apply (frule(2) pd_at_asid_cross_over)
apply (clarsimp simp: asidLowBits_handy_convs word_sless_def word_sle_def)
apply (clarsimp simp: typ_heap_simps order_le_less_trans[OF word_and_le1]
array_assertion_shrink_right ptr_add_assertion_def
arg_cong[where f="\<lambda>x. 2 ^ x", OF meta_eq_to_obj_eq, OF asid_low_bits_def])
apply (clarsimp split: option.split)
apply (frule_tac x=pd in fun_cong [OF rf_sr_asid_map_pd_to_hwasids])
@ -333,6 +359,7 @@ lemma storeHWASID_ccorres:
carch_state_relation_def pd_at_asid'_def
fun_upd_def[symmetric] carch_globals_def
order_le_less_trans[OF word_and_le1]
array_assertion_shrink_right
arg_cong[where f="\<lambda>x. 2 ^ x", OF meta_eq_to_obj_eq, OF asid_low_bits_def])
apply (subgoal_tac "ucast hw_asid <s (256 :: sword32) \<and> ucast hw_asid < (256 :: sword32)
\<and> (0 :: sword32) <=s ucast hw_asid")
@ -428,7 +455,8 @@ lemma invalidateASID_ccorres:
apply (frule(2) pd_at_asid_cross_over)
apply (clarsimp simp: typ_heap_simps)
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
cpspace_relation_def)
cpspace_relation_def
array_assertion_shrink_right)
apply (clarsimp simp: typ_heap_simps cmachine_state_relation_def
carch_state_relation_def pd_at_asid'_def carch_globals_def
fun_upd_def[symmetric] order_le_less_trans[OF word_and_le1]
@ -717,30 +745,33 @@ lemma generic_frame_cap_ptr_set_capFMappedAddress_spec:
apply (clarsimp simp: cte_lift_def)
done
lemma lookupPDSlot_spec:
"\<forall>s. \<Gamma> \<turnstile> {s}
"\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. array_assertion (pd_' s) (2 ^ pageBits) (hrs_htd (\<acute>t_hrs))\<rbrace>
Call lookupPDSlot_'proc
\<lbrace> \<acute>ret__ptr_to_struct_pde_C = Ptr (lookupPDSlot (ptr_val (pd_' s)) (vptr_' s)) \<rbrace>"
apply vcg
apply (clarsimp simp: lookupPDSlot_def)
apply (simp add: ArchVSpaceAcc_A.lookup_pd_slot_def)
apply (subst array_assertion_shrink_right, assumption)
apply (rule unat_le_helper, simp)
apply (rule order_less_imp_le, rule vptr_shiftr_le_2p)
apply (simp add: Let_def word_sle_def)
apply (case_tac pd)
apply simp
apply (case_tac pd)
apply (simp add: word32_shift_by_2)
done
lemma lookupPTSlot_nofail_spec:
"\<forall>s. \<Gamma> \<turnstile> {s}
"\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. array_assertion (pt_' s) (2 ^ (ptBits - 2)) (hrs_htd (\<acute>t_hrs))\<rbrace>
Call lookupPTSlot_nofail_'proc
\<lbrace> \<acute>ret__ptr_to_struct_pte_C = Ptr (lookupPTSlot_nofail (ptr_val (pt_' s)) (vptr_' s)) \<rbrace>"
apply vcg
apply (clarsimp simp: lookupPTSlot_nofail_def)
apply (simp add: ArchVSpaceAcc_A.lookup_pt_slot_no_fail_def)
apply (subst array_assertion_shrink_right, assumption)
apply (rule order_less_imp_le, rule unat_less_helper, simp)
apply (rule order_le_less_trans, rule word_and_le1, simp add: ptBits_def pageBits_def)
apply (simp add: Let_def word_sle_def)
apply (case_tac pt)
apply simp
apply (simp add: word32_shift_by_2)
done
@ -811,8 +842,31 @@ lemma cpde_relation_pde_coarse:
apply (simp add: pde_pde_coarse_lift_def)
done
lemma page_table_at_carray_map_relation:
"\<lbrakk> page_table_at' pt s; cpspace_pte_array_relation (ksPSpace s) hp \<rbrakk>
\<Longrightarrow> clift hp (pt_Ptr pt) \<noteq> None"
apply (clarsimp simp: carray_map_relation_def h_t_valid_clift_Some_iff)
apply (drule spec, erule iffD1)
apply (clarsimp simp: page_table_at'_def)
apply (drule_tac x="p' && mask ptBits >> 2" in spec)
apply (clarsimp simp: shiftr_shiftl1)
apply (drule mp)
apply (simp add: shiftr_over_and_dist ptBits_def pageBits_def mask_def
order_le_less_trans[OF word_and_le1])
apply (clarsimp simp: typ_at_to_obj_at_arches objBits_simps archObjSize_def
is_aligned_andI1 add.commute word_plus_and_or_coroll2
dest!: obj_at_ko_at' ko_at_projectKO_opt)
done
lemma page_table_at_rf_sr:
"\<lbrakk> page_table_at' pd s; (s, s') \<in> rf_sr \<rbrakk>
\<Longrightarrow> cslift s' (Ptr pd :: (pte_C[256]) ptr) \<noteq> None"
by (clarsimp simp: rf_sr_def cstate_relation_def Let_def
cpspace_relation_def page_table_at_carray_map_relation)
lemma lookupPTSlot_ccorres:
"ccorres (lookup_failure_rel \<currency> (\<lambda>rv rv'. rv' = pte_Ptr rv)) lookupPTSlot_xf \<top>
"ccorres (lookup_failure_rel \<currency> (\<lambda>rv rv'. rv' = pte_Ptr rv)) lookupPTSlot_xf
(page_directory_at' pd)
(UNIV \<inter> \<lbrace>\<acute>pd = Ptr pd \<rbrace> \<inter> \<lbrace>\<acute>vptr = vptr \<rbrace>)
[]
(lookupPTSlot pd vptr)
@ -835,40 +889,30 @@ lemma lookupPTSlot_ccorres:
apply (simp add: lookup_fault_missing_capability_lift)
apply (simp add: mask_def)
apply (rule ccorres_rhs_assoc)+
apply csymbr
apply csymbr
apply csymbr
apply csymbr
apply (rule ccorres_abstract_cleanup)
apply (rule_tac P="ret__unsigned_long = pdeTable rv"
in ccorres_gen_asm2)
apply simp
apply (simp add: word_sle_def)
apply (simp add:liftE_bindE checkPTAt_def)
apply (rule ccorres_stateAssert)
apply (rule_tac R=\<top> and Q' = "UNIV
\<inter> {s. pt_' s = Ptr (ptrFromPAddr ret__unsigned_long)}" in ccorres_symb_exec_r)
apply (rule ccorres_tmp_lift2)
apply ceqv
apply (rule ccorres_Guard_Seq)+
apply csymbr
apply csymbr
apply csymbr
apply csymbr
apply (rule ccorres_return_CE, simp+)[1]
apply (clarsimp simp: Collect_const_mem shiftl_t2n)
apply simp
apply vcg
apply (rule conseqPre, vcg)
apply clarsimp
apply (clarsimp simp: Collect_const_mem)
apply (frule h_t_valid_clift, simp)
apply (intro conjI impI)
apply (clarsimp simp: cpde_relation_def pde_pde_coarse_lift_def
pde_lift_pde_coarse Let_def)
apply (clarsimp split: Hardware_H.pde.split_asm)
apply (drule cpde_relation_pde_coarse, simp)
done
apply (rule_tac P="page_table_at' (ptrFromPAddr (pdeTable rv))
and ko_at' rv (lookup_pd_slot pd vptr)
and K (isPageTablePDE rv)" and P'=UNIV in ccorres_from_vcg_throws)
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: returnOk_def return_def Collect_const_mem
lookup_pd_slot_def word_sle_def)
apply (frule(1) page_table_at_rf_sr, clarsimp)
apply (erule cmap_relationE1[OF rf_sr_cpde_relation], erule ko_at_projectKO_opt)
apply (clarsimp simp: typ_heap_simps cpde_relation_def Let_def isPageTablePDE_def
pde_pde_coarse_lift_def pde_pde_coarse_lift
split: pde.split_asm)
apply (subst array_ptr_valid_array_assertionI, erule h_t_valid_clift, simp+)
apply (rule unat_le_helper, rule order_trans[OF word_and_le1], simp)
apply (simp add: word32_shift_by_2)
apply (clarsimp simp: Collect_const_mem h_t_valid_clift)
apply (frule(1) page_directory_at_rf_sr, clarsimp)
apply (subst array_ptr_valid_array_assertionI, erule h_t_valid_clift, simp+)
apply (simp add: pageBits_def)
apply (clarsimp simp: cpde_relation_def pde_pde_coarse_lift_def
pde_pde_coarse_lift Let_def isPageTablePDE_def
split: Hardware_H.pde.split_asm)
done
lemma cap_case_isPageDirectoryCap:
"(case cap of capability.ArchObjectCap (arch_capability.PageDirectoryCap pd ( Some asid)) \<Rightarrow> fn pd asid
@ -1484,10 +1528,21 @@ lemma ccorres_h_t_valid_armKSGlobalPD:
apply (simp add:rf_sr_def cstate_relation_def Let_def)
done
lemma array_assertion_abs_tcb_ctes:
"\<forall>s s'. (s, s') \<in> rf_sr \<and> tcb_at' (ctcb_ptr_to_tcb_ptr (tcb s')) s \<and> (of_nat n < tcbCNodeEntries)
\<longrightarrow> array_assertion (cte_Ptr (ptr_val (tcb s') && 0xFFFFFE00)) n (hrs_htd (t_hrs_' (globals s')))"
(* going to need to assert this too, sigh *)
sorry
lemmas ccorres_move_array_assertion_tcb_ctes [corres_pre]
= ccorres_move_Guard_Seq [OF array_assertion_abs_tcb_ctes]
ccorres_move_Guard [OF array_assertion_abs_tcb_ctes]
lemma setVMRoot_ccorres:
"ccorres dc xfdc (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' thread) (UNIV \<inter> {s. tcb_' s = tcb_ptr_to_ctcb_ptr thread}) []
(setVMRoot thread) (Call setVMRoot_'proc)"
apply (cinit lift: tcb_')
apply (rule ccorres_move_array_assertion_tcb_ctes)
apply (rule ccorres_move_c_guard_cte)
apply (simp add: getThreadVSpaceRoot_def locateSlot_conv)
apply (ctac)
@ -1588,7 +1643,7 @@ lemma setVMRoot_ccorres:
apply (auto simp: isCap_simps valid_cap'_def mask_def)[1]
apply (clarsimp simp: ptr_val_tcb_ptr_mask'
size_of_def cte_level_bits_def
tcbVTableSlot_def Kernel_C.tcbVTable_def
tcbVTableSlot_def tcb_cnode_index_defs
ccap_rights_relation_def cap_rights_to_H_def
to_bool_def true_def allRights_def
mask_def[where n="Suc 0"]
@ -1607,7 +1662,6 @@ lemma invs'_invs_no_cicd:
"invs' s \<Longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s"
by (clarsimp simp add: invs'_def all_invs_but_ct_idle_or_in_cur_domain'_def valid_state'_def newKernelState_def)
lemma setVMRootForFlush_ccorres:
"ccorres (\<lambda>rv rv'. rv' = from_bool rv) ret__unsigned_long_'
(invs' and (\<lambda>s. asid \<le> mask asid_bits))
@ -1652,6 +1706,9 @@ lemma setVMRootForFlush_ccorres:
mask_def[where n="Suc 0"] true_def to_bool_def
allRights_def size_of_def cte_level_bits_def
tcbVTableSlot_def Kernel_C.tcbVTable_def invs'_invs_no_cicd)
apply (clarsimp simp: rf_sr_ksCurThread)
apply (subst array_assertion_abs_tcb_ctes, simp add: tcb_cnode_index_defs,
fastforce intro: tcb_at_invs')+
apply (clarsimp simp: rf_sr_ksCurThread ptr_val_tcb_ptr_mask' [OF tcb_at_invs'])
apply (frule cte_at_tcb_at_16'[OF tcb_at_invs'], clarsimp simp: cte_wp_at_ctes_of)
apply (rule cmap_relationE1[OF cmap_relation_cte], assumption+)
@ -2199,6 +2256,108 @@ lemma pte_pte_invalid_new_spec:
apply (clarsimp simp: pte_lift_def pte_get_tag_def pte_pte_large_def fupdate_def)
done
lemma ccorres_name_pre_C:
"(\<And>s. s \<in> P' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P {s} hs f g)
\<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs f g"
apply (rule ccorres_guard_imp)
apply (rule_tac xf'=id in ccorres_abstract, rule ceqv_refl)
apply (rule_tac P="rv' \<in> P'" in ccorres_gen_asm2)
apply assumption
apply simp
apply simp
done
lemma ccorres_second_Guard:
assumes cc: "ccorres_underlying sr \<Gamma> r xf arrel axf A C' hs a (Guard F1 S1 c)"
shows "ccorres_underlying sr \<Gamma> r xf arrel axf A (C' \<inter> S) hs a (Guard F1 S1 (Guard F S c))"
apply (rule ccorres_name_pre_C)
apply (rule ccorres_guard_imp)
apply (rule_tac xf'=id in ccorres_abstract)
apply (rule Guard_ceqv, rule impI, rule refl)
apply (rule_tac x'="{_. rv' \<in> S}" in Guard_ceqv)
apply (clarsimp simp: Collect_const_mem)
apply (rule ceqv_refl)
apply (rule_tac P="rv' = s" in ccorres_gen_asm2)
apply simp
apply (rule_tac xf'=xfdc in ccorres_abstract)
apply (rule Guard_ceqv, rule impI, rule refl)
apply (rule ceqv_Guard_UNIV[THEN iffD2])
apply (rule ceqv_refl)
apply (rule cc)
apply simp
apply simp
done
lemma clift_array_assertion_imp:
"clift hrs (p :: (('a :: wf_type)['b :: finite]) ptr) = Some v
\<Longrightarrow> htd = hrs_htd hrs
\<Longrightarrow> n \<noteq> 0
\<Longrightarrow> \<exists>i. p' = ptr_add (ptr_coerce p) (int i)
\<and> i + n \<le> CARD('b)
\<Longrightarrow> array_assertion (p' :: 'a ptr) n htd"
apply clarsimp
apply (drule h_t_valid_clift)
apply (drule array_ptr_valid_array_assertionD)
apply (drule_tac j=i in array_assertion_shrink_left, simp)
apply (erule array_assertion_shrink_right)
apply simp
done
lemma multiple_add_less_nat:
"a < (c :: nat) \<Longrightarrow> x dvd a \<Longrightarrow> x dvd c \<Longrightarrow> b < x
\<Longrightarrow> a + b < c"
apply (subgoal_tac "b < c - a")
apply simp
apply (erule order_less_le_trans)
apply (rule dvd_imp_le)
apply simp
apply simp
done
lemma large_ptSlot_array_constraint:
"is_aligned (ptSlot :: word32) 6 \<Longrightarrow> n < 16
\<Longrightarrow> \<exists>i. ptSlot = (ptSlot && ~~ mask ptBits) + of_nat i * 4 \<and> i + n \<le> 255"
apply (rule_tac x="unat ((ptSlot && mask ptBits) >> 2)" in exI)
apply (simp add: shiftl_t2n[where n=2, symmetric, THEN trans[rotated],
OF mult.commute, simplified])
apply (simp add: shiftr_shiftl1)
apply (rule conjI, rule trans,
rule word_plus_and_or_coroll2[symmetric, where w="mask ptBits"])
apply (simp, rule aligned_neg_mask[THEN sym], rule is_aligned_andI1,
erule is_aligned_weaken, simp)
apply (rule less_Suc_eq_le[THEN iffD1])
apply (rule_tac x="2 ^ 4" in multiple_add_less_nat, simp_all)[1]
apply (rule unat_less_helper, simp)
apply (rule order_less_le_trans, rule shiftr_less_t2n[where m="ptBits - 2"])
apply (rule order_le_less_trans, rule word_and_le1, simp add: mask_def ptBits_def pageBits_def)
apply (simp add: ptBits_def pageBits_def)
apply (simp add: is_aligned_def[where n=4, simplified, symmetric])
apply (rule is_aligned_shiftr, rule is_aligned_andI1, simp)
done
lemma large_pdSlot_array_constraint:
"is_aligned pd pdBits \<Longrightarrow> vmsz_aligned vptr ARMSuperSection \<Longrightarrow> n < 16
\<Longrightarrow> \<exists>i. lookup_pd_slot pd vptr = pd + of_nat i * 4 \<and> i + n \<le> 4095"
apply (rule_tac x="unat (vptr >> 20)" in exI)
apply (rule conjI)
apply (simp add: lookup_pd_slot_def shiftl_t2n)
apply (rule less_Suc_eq_le[THEN iffD1])
apply (rule_tac x="2 ^ 4" in multiple_add_less_nat, simp_all)[1]
apply (rule unat_less_helper, simp)
apply (rule order_less_le_trans, rule shiftr_less_t2n3[where m=12], simp+)
apply (simp add: is_aligned_def[where n=4, simplified, symmetric]
vmsz_aligned_def is_aligned_shiftr)
done
lemma findPDForASID_page_directory_at'_simple[wp]:
notes checkPDAt_inv[wp del]
shows "\<lbrace>\<top>\<rbrace> findPDForASID asiv
\<lbrace>\<lambda>rv s. page_directory_at' rv s\<rbrace>,-"
apply (simp add:findPDForASID_def)
apply (wp getASID_wp|simp add:checkPDAt_def | wpc)+
apply auto
done
lemma unmapPage_ccorres:
"ccorres dc xfdc (invs' and (\<lambda>s. 2 ^ pageBitsForSize sz \<le> gsMaxObjectSize s)
and (\<lambda>_. asid \<le> mask asid_bits \<and> vmsz_aligned' vptr sz
@ -2263,6 +2422,7 @@ lemma unmapPage_ccorres:
apply csymbr
apply csymbr
apply (ctac add: lookupPTSlot_ccorres)
apply (rename_tac ptSlot lookupPTSlot_ret)
apply (simp add: Collect_False dc_def[symmetric] del: Collect_const)
apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2,
rule ccorres_rhs_assoc2)
@ -2282,13 +2442,24 @@ lemma unmapPage_ccorres:
apply (ccorres_remove_UNIV_guard)
apply (rule ccorres_rhs_assoc2)
apply (rule ccorres_split_nothrow_novcg)
apply (rule_tac F="\<top>\<top>" in ccorres_mapM_x_while)
apply (rule_tac P="is_aligned ptSlot 6" in ccorres_gen_asm)
apply (rule_tac F="\<lambda>_. page_table_at' (ptSlot && ~~ mask ptBits)"
in ccorres_mapM_x_while)
apply clarsimp
apply (rule ccorres_guard_imp2)
apply csymbr
apply (rule ccorres_Guard)
apply (rule ccorres_second_Guard)
apply (rule storePTE_Basic_ccorres)
apply (simp add: cpte_relation_def Let_def)
apply clarsimp
apply (drule(1) page_table_at_rf_sr, clarsimp)
apply (simp add: clift_array_assertion_imp unat_of_nat
upto_enum_step_def large_ptSlot_array_constraint)
apply (subst clift_array_assertion_imp, assumption,
simp_all add: unat_of_nat
upto_enum_step_def)[1]
apply (simp add: large_ptSlot_array_constraint)
apply (simp add: upto_enum_step_def
upto_enum_word
del: upt.simps)
@ -2304,7 +2475,7 @@ lemma unmapPage_ccorres:
apply (rule ccorres_move_c_guard_pte, ccorres_remove_UNIV_guard)
apply (rule ccorres_move_c_guard_pte, ccorres_remove_UNIV_guard)
apply (ctac add: cleanCacheRange_PoU_ccorres[unfolded dc_def])
apply (rule_tac P="is_aligned rva 6" in hoare_gen_asm)
apply (rule_tac P="is_aligned ptSlot 6" in hoare_gen_asm)
apply (rule hoare_strengthen_post)
apply (rule hoare_vcg_conj_lift)
apply (rule_tac P="\<lambda>s. 2 ^ pageBitsForSize sz \<le> gsMaxObjectSize s"
@ -2335,7 +2506,8 @@ lemma unmapPage_ccorres:
apply (rule ccorres_split_throws)
apply (rule ccorres_return_void_C')
apply vcg
apply (wp lookupPTSlot_inv Arch_R.lookupPTSlot_aligned | simp add: K_def)+
apply (wp lookupPTSlot_inv Arch_R.lookupPTSlot_aligned
lookupPTSlot_page_table_at' | simp add: K_def)+
apply (vcg exspec=lookupPTSlot_modifies)
-- "ARMSection"
apply (rule ccorres_Cond_rhs)
@ -2403,15 +2575,21 @@ lemma unmapPage_ccorres:
apply (rule ccorres_rhs_assoc2,
rule ccorres_split_nothrow_novcg)
apply (rule_tac P="is_aligned rv pdBits" in ccorres_gen_asm)
apply (rule_tac F="\<top>\<top>" in ccorres_mapM_x_while)
apply (rule_tac F="\<lambda>_. page_directory_at' rv" in ccorres_mapM_x_while)
apply clarsimp
apply (rule ccorres_guard_imp2)
apply csymbr
apply (rule ccorres_second_Guard)
apply (rule storePDE_Basic_ccorres)
apply (simp add: cpde_relation_def Let_def
pde_lift_pde_invalid)
apply clarsimp
apply (simp add: upto_enum_step_def upto_enum_word)
apply (drule(1) page_directory_at_rf_sr, clarsimp)
apply (simp add: unat_def[symmetric] unat_of_nat
upto_enum_step_def upto_enum_word)
apply (subst clift_array_assertion_imp, assumption, simp_all)[1]
apply (rule large_pdSlot_array_constraint, simp_all)[1]
apply (simp add: vmsz_aligned'_def vmsz_aligned_def)
apply (clarsimp simp: lookup_pd_slot_def Let_def
mask_add_aligned field_simps)
apply (erule less_kernelBase_valid_pde_offset')

32
spec/cspec/Substitute.thy
View File

@ -44,7 +44,7 @@ fun suspicious_term ctxt s t = if Term.add_var_names t [] = [] then ()
val debug_trace = ref (Bound 0);
fun convert prefix src_ctxt proc (tm as Const (name, _)) (convs, ctxt) =
(term_convert prefix convs tm; (convs, ctxt))
((term_convert prefix convs tm; (convs, ctxt))
handle Option =>
let
val cname = unprefix prefix name;
@ -80,7 +80,9 @@ fun convert prefix src_ctxt proc (tm as Const (name, _)) (convs, ctxt) =
val abs_tm = list_abs (map (pair "_") lhs_argTs, tm'')
in (Termtab.insert (K true) (tm, abs_tm) convs, ctxt) end
end
end)
| convert _ _ _ (tm) _ = raise TERM ("convert: not Const", [tm])
fun prove_impl_tac ctxt ss =
SUBGOAL (fn (t, n) => let
@ -311,6 +313,29 @@ val guard_halt = com_rewrite
then (t, [(@{term DontReach}, @{term "{} :: globals myvars set"})])
else (t, []))
fun acc_ptr_adds (Const (@{const_name h_val}, _) $ m $ (Const (@{const_name ptr_add}, _) $ p $ n))
= [(p, n, true)] @ maps acc_ptr_adds [m, p, n]
| acc_ptr_adds (Const (@{const_name heap_update}, _) $ (Const (@{const_name ptr_add}, _) $ p $ n))
= [(p, n, true)] @ maps acc_ptr_adds [p, n]
| acc_ptr_adds (Const (@{const_name ptr_add}, _) $ p $ n)
= [(p, n, false)] @ maps acc_ptr_adds [p, n]
| acc_ptr_adds (f $ x) = maps acc_ptr_adds [f, x]
| acc_ptr_adds (abs as Abs (_, T, t)) = if T = @{typ "globals myvars"}
then acc_ptr_adds (betapply (abs, @{term "s :: globals myvars"}))
else acc_ptr_adds t
| acc_ptr_adds _ = []
fun mk_bool true = @{term True} | mk_bool false = @{term False}
val guard_acc_ptr_adds = com_rewrite
(fn t => (t, acc_ptr_adds t |> map (fn (p, n, strong) => let
val assn = Const (@{const_name ptr_add_assertion},
fastype_of p --> @{typ "int \<Rightarrow> bool \<Rightarrow> heap_typ_desc \<Rightarrow> bool"})
$ p $ n $ mk_bool strong
$ @{term "hrs_htd (t_hrs_' (globals (s :: globals myvars)))"}
val gd = HOLogic.mk_Collect ("s", @{typ "globals myvars"}, assn)
in (@{term MemorySafety}, gd) end)))
end
*}
@ -325,7 +350,8 @@ SubstituteSpecs.take_all_actions
o (strengthen_c_guards ["memset_body", "memcpy_body", "memzero_body"]
(Proof_Context.theory_of ctxt) s)
o guard_halt
o guard_htd_updates_with_domain)
o guard_htd_updates_with_domain
o guard_acc_ptr_adds)
@{term kernel_all_global_addresses.\<Gamma>}
(CalculateState.get_csenv @{theory} "c/kernel_all.c_pp" |> the)
[@{typ "globals myvars"}, @{typ int}, @{typ strictc_errortype}]

1
tools/c-parser/CProof.thy
View File

@ -13,6 +13,7 @@ imports
"umm_heap/SepFrame"
"Simpl/Vcg"
"umm_heap/StructSupport"
"umm_heap/ArrayAssertion"
begin
(* name generation is the only thing this theory wants, but that