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

page_map_unmap_cancel : cdl spec changed and drefine fixed.

This commit is contained in:
Gao Xin 2014-09-05 14:48:22 +10:00
parent a5f2cab271
commit 77dd554227
13 changed files with 990 additions and 772 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

525
proof/drefine/Arch_DR.thy
View File

@ -12,20 +12,16 @@ theory Arch_DR
imports Untyped_DR
begin
definition
"transform_pd_slot_ref x
= (x && ~~ mask pd_bits,
unat ((x && mask pd_bits) >> 2))"
definition
"transform_pt_slot_ref x
= (x && ~~ mask pt_bits,
unat ((x && mask pt_bits) >> 2))"
definition
"make_arch_duplicate cap \<equiv> case cap of
cdl_cap.PageTableCap oid _ mp \<Rightarrow> cdl_cap.PageTableCap oid Fake None
| cdl_cap.FrameCap oid rghts sz _ mp \<Rightarrow> cdl_cap.FrameCap oid rghts sz Fake None"
definition
"get_pt_mapped_addr cap \<equiv>
case cap of (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) \<Rightarrow> transform_mapping asid
| _ \<Rightarrow> None"
definition
"transform_page_table_inv invok \<equiv> case invok of
ArchInvocation_A.PageTableMap cap slot pde slot' \<Rightarrow>
@ -36,10 +32,8 @@ definition
(transform_cslot_ptr slot) (transform_pd_slot_ref slot'))
else None
| ArchInvocation_A.PageTableUnmap cap slot \<Rightarrow>
if is_pt_cap cap then Some
(cdl_page_table_invocation.PageTableUnmap
(obj_ref_of cap) (transform_cslot_ptr slot))
else None"
Some (cdl_page_table_invocation.PageTableUnmap (get_pt_mapped_addr cap)
(obj_ref_of cap) (transform_cslot_ptr slot))"
definition flush_type_map :: "ArchInvocation_A.flush_type \<Rightarrow> flush"
where "flush_type_map f \<equiv> case f of
@ -55,6 +49,7 @@ where "transform_page_dir_inv invok \<equiv> case invok of
|ArchInvocation_A.page_directory_invocation.PageDirectoryNothing \<Rightarrow>
Some (cdl_page_directory_invocation.PageDirectoryNothing) "
definition transform_page_inv :: "ArchInvocation_A.page_invocation \<Rightarrow> cdl_page_invocation option"
where "transform_page_inv invok \<equiv> case invok of
ArchInvocation_A.page_invocation.PageMap asid cap ct_slot entries \<Rightarrow>
@ -68,9 +63,10 @@ where "transform_page_inv invok \<equiv> case invok of
(sum_case (transform_pte \<circ> fst) (transform_pde \<circ> fst) entries)
(sum_case (\<lambda>pair. [ (transform_pt_slot_ref \<circ> hd \<circ> snd) pair])
(\<lambda>pair. [(transform_pd_slot_ref \<circ> hd \<circ> snd) pair]) entries))
| ArchInvocation_A.page_invocation.PageUnmap (arch_cap.PageCap a _ _ _) ref \<Rightarrow>
Some (cdl_page_invocation.PageUnmap a (transform_cslot_ptr ref))
| ArchInvocation_A.page_invocation.PageFlush flush _ _ _ _ _ \<Rightarrow> Some (cdl_page_invocation.PageFlushCaches (flush_type_map flush))
| ArchInvocation_A.page_invocation.PageUnmap (arch_cap.PageCap a _ sz asid) ref \<Rightarrow>
Some (cdl_page_invocation.PageUnmap (transform_mapping asid) a (transform_cslot_ptr ref) (pageBitsForSize sz))
| ArchInvocation_A.page_invocation.PageFlush flush _ _ _ _ _ \<Rightarrow>
Some (cdl_page_invocation.PageFlushCaches (flush_type_map flush))
| ArchInvocation_A.page_invocation.PageGetAddr base \<Rightarrow> Some (cdl_page_invocation.PageGetAddress)
| _ \<Rightarrow> None"
@ -87,7 +83,7 @@ where "translate_arch_invocation invo \<equiv> case invo of
(transform_cslot_ptr parent)
{frame..frame + 2 ^ pageBits - 1}
(transform_cslot_ptr slot)
(transform_asid base)))
(fst $ transform_asid base)))
| arch_invocation.InvokeASIDPool oper \<Rightarrow>
Some (case oper of ArchInvocation_A.Assign asid pool_ptr ct_slot
\<Rightarrow> cdl_invocation.InvokeAsidPool
@ -148,54 +144,6 @@ lemma get_pde_sp:
lemmas less_kernel_base_mapping_slots = less_kernel_base_mapping_slots_both[where x=0, simplified]
lemma unat_pd_bits_less_4096_helper[simp]:
"\<And>x. unat (x && mask pd_bits >> 2 :: word32) < 4096"
apply (rule order_less_le_trans[where y="2^12"])
apply (rule unat_less_power[rotated])
apply (rule shiftr_less_t2n)
apply (rule order_less_le_trans, rule and_mask_less')
apply (simp_all add: pd_bits_def pageBits_def word_bits_conv)
done
lemma dcorres_lookup_pd_slot:
"is_aligned pd 14
\<Longrightarrow> (cdl_lookup_pd_slot pd vptr = transform_pd_slot_ref (lookup_pd_slot pd vptr))"
apply (clarsimp simp:cdl_lookup_pd_slot_def
transform_pd_slot_ref_def lookup_pd_slot_def)
by (simp add:vaddr_segment_nonsense vaddr_segment_nonsense2)
lemma pd_at_cdl_pd_at:
"\<lbrakk>valid_idle s ; ucast (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots;
kheap s (ptr && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory fun))\<rbrakk>
\<Longrightarrow> opt_cap (transform_pd_slot_ref ptr) (transform s) =
Some (transform_pde (fun (of_nat (unat (ptr && mask pd_bits >> 2)))))"
apply (clarsimp simp:opt_cap_def transform_pd_slot_ref_def transform_def
slots_of_def opt_object_def transform_objects_def
valid_idle_def restrict_map_def object_slots_def
transform_page_directory_contents_def unat_map_def
st_tcb_def2 dest!:get_tcb_SomeD split:option.splits)
apply (simp add: below_kernel_base)
apply (auto simp:transform_page_directory_contents_def unat_map_def)
done
lemma dcorres_get_pde:
"dcorres (\<lambda>r r'. r = transform_pde r') \<top>
(valid_idle and K (ucast (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots))
(cdl_get_pde (transform_pd_slot_ref ptr)) (get_pde ptr)"
apply (simp add:cdl_get_pde_def
get_pde_def gets_def gets_the_def
get_pd_def get_object_def bind_assoc)
apply (rule dcorres_absorb_get_l)
apply (rule dcorres_absorb_get_r)
apply (clarsimp simp:assert_def assert_opt_def
corres_free_fail
split:Structures_A.kernel_object.splits
arch_kernel_obj.splits)
apply (drule(2) pd_at_cdl_pd_at)
apply (simp add:ucast_nat_def)
done
lemma dcorres_lookup_pt_slot:
"dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) \<top>
( valid_arch_objs
@ -270,7 +218,7 @@ lemma create_mapping_entries_dcorres:
\<top>
(page_directory_at pd_ptr and valid_idle and valid_arch_objs and pspace_aligned
and (\<exists>\<rhd> (lookup_pd_slot pd_ptr vptr && ~~ mask pd_bits)))
(cdl_create_mapping_entries vptr (pageBitsForSize pgsz) pd_ptr \<sqinter> Monads_D.throw)
(cdl_page_mapping_entries vptr (pageBitsForSize pgsz) pd_ptr)
(create_mapping_entries base vptr pgsz vm_rights attrib pd_ptr)"
proof -
@ -296,8 +244,7 @@ proof -
apply (simp add: liftME_def[symmetric] o_def transform_pte_def
lookup_error_injection dc_def[symmetric])
apply (rule dcorres_injection_handler_rhs)
apply (rule corres_alternate1)
apply (simp add:liftE_bindE cdl_create_mapping_entries_def)
apply (simp add:liftE_bindE cdl_page_mapping_entries_def)
apply (rule corres_dummy_returnOk_r)
apply (rule corres_guard_imp)
apply (rule corres_splitEE[OF dcorres_returnOk])
@ -318,8 +265,7 @@ proof -
apply (simp add: liftME_def[symmetric] o_def transform_pte_def
lookup_error_injection dc_def[symmetric])
apply (rule dcorres_injection_handler_rhs)
apply (rule corres_alternate1)
apply (simp add:liftE_bindE cdl_create_mapping_entries_def)
apply (simp add:liftE_bindE cdl_page_mapping_entries_def)
apply (rule corres_dummy_returnOk_r)
apply (rule corres_guard_imp)
apply (rule corres_splitEE)
@ -343,8 +289,7 @@ proof -
show ?case using ARMSection.prems
apply (simp add: liftME_def[symmetric] o_def transform_pte_def
lookup_error_injection dc_def[symmetric])
apply (simp add:liftE_bindE cdl_create_mapping_entries_def)
apply (rule corres_alternate1)
apply (simp add:liftE_bindE cdl_page_mapping_entries_def)
apply (rule corres_guard_imp)
apply (rule_tac F = "is_aligned pd_ptr 14" in corres_gen_asm2)
apply (rule dcorres_returnOk)
@ -360,8 +305,7 @@ proof -
using pd_aligned
apply (simp add: liftME_def[symmetric] o_def transform_pte_def
lookup_error_injection dc_def[symmetric])
apply (simp add:liftE_bindE cdl_create_mapping_entries_def)
apply (rule corres_alternate1)
apply (simp add:liftE_bindE cdl_page_mapping_entries_def)
apply (rule corres_guard_imp)
apply (rule_tac F = "is_aligned pd_ptr 14" in corres_gen_asm2)
apply (rule dcorres_returnOk)
@ -758,166 +702,170 @@ next
get_index_def transform_cap_list_def
dc_def[symmetric]
split: cap.split arch_cap.split option.split)
apply (clarsimp simp: gets_bind_alternative
gets_the_def bind_assoc corres_symb_exec_in_gets
assert_opt_def)
apply (clarsimp simp: neq_Nil_conv valid_cap_simps obj_at_def
opt_object_page_directory invs_valid_idle label_to_flush_type_def InvocationLabels_H.isPageFlush_def
dest!: a_type_pdD)+
apply (rule_tac r'=dc and P'="?I" and Q'="\<lambda>rv. ?I and (\<exists>\<rhd> (lookup_pd_slot rv a && ~~ mask pd_bits))"
in corres_alternative_throw_splitE[OF _ _ returnOk_wp[where x="()"], simplified])
apply (rule corres_from_rdonly, simp_all)[1]
apply (wp | simp)+
apply (rule hoare_strengthen_post, rule hoare_post_taut)
apply (case_tac r, auto simp add: in_monad in_alternative)[1]
apply (simp add: corres_whenE_throwError_split_rhs corres_alternate2
check_vp_alignment_def unlessE_whenE)
apply (clarsimp simp add: liftE_bindE[symmetric])
apply (rule corres_alternative_throw_splitE)
apply (rule corres_guard_imp,
rule create_mapping_entries_dcorres[OF refl])
apply (clarsimp simp: neq_Nil_conv cap_aligned_def
pd_bits_def pageBits_def)
apply (simp add: vmsz_aligned_def)
apply (simp only: linorder_not_le, erule order_le_less_trans[rotated])
apply simp
apply simp
apply (clarsimp simp: neq_Nil_conv valid_cap_simps dest!:page_directory_at_rev)
apply auto[1]
apply (rule corres_from_rdonly[where P=\<top> and P'=\<top>], simp_all)[1]
apply (wp | simp)+
apply (rule validE_cases_valid, rule hoare_pre)
apply (wp | simp)+
apply (clarsimp simp add: in_monad in_alternative conj_disj_distribR[symmetric])
apply (simp add: conj_disj_distribR cong: conj_cong)
apply (simp add: arch_invocation_relation_def translate_arch_invocation_def
transform_page_inv_def update_cap_rights_def
update_mapping_cap_status_def Types_D.cap_rights_def
mask_vm_rights_def transform_mapping_def)
apply wp
apply (rule hoare_pre, wp, simp)
apply (rule hoare_pre, wp, auto)[1]
apply (wp | simp add: whenE_def split del: split_if)+
apply (rule hoare_pre, wp, simp)
apply clarsimp
apply (clarsimp simp: gets_bind_alternative
gets_the_def bind_assoc corres_symb_exec_in_gets
assert_opt_def)
apply (rule_tac F="v \<noteq> None" in corres_req)
apply (clarsimp simp: neq_Nil_conv valid_cap_simps obj_at_def
opt_object_page_directory invs_valid_idle
dest!: a_type_pdD)
apply (clarsimp simp: gets_bind_alternative corres_symb_exec_in_gets)
apply (rule_tac r'=dc and P'="?I" and Q'="\<lambda>rv. ?I and (\<exists>\<rhd> (lookup_pd_slot rv b && ~~ mask pd_bits))"
in corres_alternative_throw_splitE[OF _ _ returnOk_wp[where x="()"], simplified])
apply (rule corres_from_rdonly, simp_all)[1]
apply (wp | simp)+
apply (rule hoare_strengthen_post, rule hoare_post_taut)
apply (case_tac r, auto simp add: in_monad in_alternative)[1]
apply (simp add: corres_whenE_throwError_split_rhs corres_alternate2
check_vp_alignment_def unlessE_whenE)
apply (clarsimp simp add: liftE_bindE[symmetric])
apply (rule_tac F="b < kernel_base" in corres_req)
apply (clarsimp simp: valid_cap_simps)
apply (rule corres_alternative_throw_splitE)
apply (rule corres_guard_imp,
rule create_mapping_entries_dcorres_select[OF refl])
apply (clarsimp simp: neq_Nil_conv cap_aligned_def
pd_bits_def pageBits_def)
apply (simp add: vmsz_aligned_def)
apply simp
apply (fastforce simp: opt_object_def)
apply (clarsimp simp: neq_Nil_conv valid_cap_simps)
apply auto[1]
apply (rule corres_from_rdonly[where P=\<top> and P'=\<top>], simp_all)[1]
apply (wp | simp)+
apply (rule validE_cases_valid, rule hoare_pre)
apply (wp | simp)+
apply (clarsimp simp add: in_monad in_alternative conj_disj_distribR[symmetric])
apply (simp add: conj_disj_distribR cong: conj_cong)
apply (simp add: arch_invocation_relation_def translate_arch_invocation_def
transform_page_inv_def update_cap_rights_def
update_mapping_cap_status_def Types_D.cap_rights_def
mask_vm_rights_def)
apply wp
apply (rule hoare_pre, wp, simp)
apply (rule hoare_pre, wp, auto)[1]
apply (wp | simp add: whenE_def split del: split_if)+
apply (rule hoare_pre, wp, simp)
apply (rule corres_alternate1)
apply (simp add: returnOk_def arch_invocation_relation_def cap_object_simps
translate_arch_invocation_def transform_page_inv_def)
apply (clarsimp)
apply (rule corres_from_rdonly)
apply (clarsimp)
apply (wp, clarsimp)
apply ( simp only: Let_unfold, wp, clarsimp, rule valid_validE, wp whenE_inv, clarsimp, wp)
apply (assumption)
apply (rule validE_cases_valid, rule hoare_pre)
apply (wp | simp add: Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_inv_def)+
apply (clarsimp simp: in_monad in_alternative conj_disj_distribR[symmetric])
apply (safe)
apply blast
apply (metis flush.exhaust)
apply (rule corres_from_rdonly)
apply (clarsimp)
apply (wp, clarsimp)
apply ( simp only: Let_unfold, wp, clarsimp, rule valid_validE, wp whenE_inv, clarsimp, wp)
apply (assumption)
apply (rule validE_cases_valid, rule hoare_pre)
apply (wp | simp add: Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_inv_def)+
apply (clarsimp simp: in_monad in_alternative conj_disj_distribR[symmetric])
apply (safe)
apply blast
apply (metis flush.exhaust)
apply (rule corres_from_rdonly)
apply (clarsimp)
apply (wp, clarsimp)
apply ( simp only: Let_unfold, wp, clarsimp, rule valid_validE, wp whenE_inv, clarsimp, wp)
apply (assumption)
apply (rule validE_cases_valid, rule hoare_pre)
apply (wp | simp add: Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_inv_def)+
apply (clarsimp simp: in_monad in_alternative conj_disj_distribR[symmetric])
apply (safe)
apply blast
apply (metis flush.exhaust)
apply (rule corres_from_rdonly)
apply (clarsimp)
apply (wp, clarsimp)
apply ( simp only: Let_unfold, wp, clarsimp, rule valid_validE, wp whenE_inv, clarsimp, wp)
apply (assumption)
apply (rule validE_cases_valid, rule hoare_pre)
apply (wp | simp add: Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_inv_def)+
apply (clarsimp simp: in_monad in_alternative conj_disj_distribR[symmetric])
apply (safe)
apply blast
apply (metis flush.exhaust)
apply (simp_all add: InvocationLabels_H.isPageFlush_def)+
apply (rule dcorres_returnOk', clarsimp simp: arch_invocation_relation_def
translate_arch_invocation_def transform_page_inv_def)+
apply (clarsimp simp: gets_bind_alternative
gets_the_def bind_assoc corres_symb_exec_in_gets
assert_opt_def)
apply (clarsimp simp: neq_Nil_conv valid_cap_simps obj_at_def
opt_object_page_directory invs_valid_idle label_to_flush_type_def InvocationLabels_H.isPageFlush_def
dest!: a_type_pdD)+
apply (rule_tac r'=dc and P'="?I" and Q'="\<lambda>rv. ?I and (\<exists>\<rhd> (lookup_pd_slot rv a && ~~ mask pd_bits))"
in corres_alternative_throw_splitE[OF _ _ returnOk_wp[where x="()"], simplified])
apply (rule corres_from_rdonly, simp_all)[1]
apply (wp | simp)+
apply (rule hoare_strengthen_post, rule hoare_post_taut)
apply (case_tac r, auto simp add: in_monad in_alternative)[1]
apply (simp add: corres_whenE_throwError_split_rhs corres_alternate2
check_vp_alignment_def unlessE_whenE)
apply (clarsimp simp add: liftE_bindE[symmetric])
apply (rule corres_alternative_throw_splitE)
apply (rule corres_alternate1)
apply (rule corres_guard_imp,
rule create_mapping_entries_dcorres[OF refl])
apply (clarsimp simp: neq_Nil_conv cap_aligned_def
pd_bits_def pageBits_def)
apply (simp add: vmsz_aligned_def)
apply (simp only: linorder_not_le, erule order_le_less_trans[rotated])
apply simp
apply simp
apply (clarsimp simp: neq_Nil_conv valid_cap_simps dest!:page_directory_at_rev)
apply auto[1]
apply (rule corres_from_rdonly[where P=\<top> and P'=\<top>], simp_all)[1]
apply (wp | simp)+
apply (rule validE_cases_valid, rule hoare_pre)
apply (wp | simp)+
apply (clarsimp simp add: in_monad in_alternative conj_disj_distribR[symmetric])
apply (simp add: conj_disj_distribR cong: conj_cong)
apply (simp add: arch_invocation_relation_def translate_arch_invocation_def
transform_page_inv_def update_cap_rights_def
update_mapping_cap_status_def Types_D.cap_rights_def
mask_vm_rights_def transform_mapping_def)
apply wp
apply (rule hoare_pre, wp, simp)
apply (rule hoare_pre, wp, auto)[1]
apply (wp | simp add: whenE_def split del: split_if)+
apply (rule hoare_pre, wp, simp)
apply clarsimp
apply (clarsimp simp: gets_bind_alternative
gets_the_def bind_assoc corres_symb_exec_in_gets
assert_opt_def)
apply (rule_tac F="v \<noteq> None" in corres_req)
apply (clarsimp simp: neq_Nil_conv valid_cap_simps obj_at_def
opt_object_page_directory invs_valid_idle
dest!: a_type_pdD)
apply (clarsimp simp: gets_bind_alternative corres_symb_exec_in_gets)
apply (rule_tac r'=dc and P'="?I" and Q'="\<lambda>rv. ?I and (\<exists>\<rhd> (lookup_pd_slot rv b && ~~ mask pd_bits))"
in corres_alternative_throw_splitE[OF _ _ returnOk_wp[where x="()"], simplified])
apply (rule corres_from_rdonly, simp_all)[1]
apply (wp | simp)+
apply (rule hoare_strengthen_post, rule hoare_post_taut)
apply (case_tac r, auto simp add: in_monad in_alternative)[1]
apply (simp add: corres_whenE_throwError_split_rhs corres_alternate2
check_vp_alignment_def unlessE_whenE)
apply (clarsimp simp add: liftE_bindE[symmetric])
apply (rule_tac F="b < kernel_base" in corres_req)
apply (clarsimp simp: valid_cap_simps)
apply (rule corres_alternative_throw_splitE)
apply (rule corres_guard_imp,
rule create_mapping_entries_dcorres_select[OF refl])
apply (clarsimp simp: neq_Nil_conv cap_aligned_def
pd_bits_def pageBits_def)
apply (simp add: vmsz_aligned_def)
apply simp
apply (fastforce simp: opt_object_def)
apply (clarsimp simp: neq_Nil_conv valid_cap_simps)
apply auto[1]
apply (rule corres_from_rdonly[where P=\<top> and P'=\<top>], simp_all)[1]
apply (wp | simp)+
apply (rule validE_cases_valid, rule hoare_pre)
apply (wp | simp)+
apply (clarsimp simp add: in_monad in_alternative conj_disj_distribR[symmetric])
apply (simp add: conj_disj_distribR cong: conj_cong)
apply (simp add: arch_invocation_relation_def translate_arch_invocation_def
transform_page_inv_def update_cap_rights_def
update_mapping_cap_status_def Types_D.cap_rights_def
mask_vm_rights_def)
apply wp
apply (rule hoare_pre, wp, simp)
apply (rule hoare_pre, wp, auto)[1]
apply (wp | simp add: whenE_def split del: split_if)+
apply (rule hoare_pre, wp, simp)
apply (rule corres_alternate1)
apply (simp add: returnOk_def arch_invocation_relation_def cap_object_simps
translate_arch_invocation_def transform_page_inv_def)
apply (clarsimp)
apply (rule corres_from_rdonly)
apply (clarsimp)
apply (wp, clarsimp)
apply ( simp only: Let_unfold, wp, clarsimp, rule valid_validE, wp whenE_inv, clarsimp, wp)
apply (assumption)
apply (rule validE_cases_valid, rule hoare_pre)
apply (wp | simp add: Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_inv_def)+
apply (clarsimp simp: in_monad in_alternative conj_disj_distribR[symmetric])
apply (safe)
apply blast
apply (metis flush.exhaust)
apply (rule corres_from_rdonly)
apply (clarsimp)
apply (wp, clarsimp)
apply ( simp only: Let_unfold, wp, clarsimp, rule valid_validE, wp whenE_inv, clarsimp, wp)
apply (assumption)
apply (rule validE_cases_valid, rule hoare_pre)
apply (wp | simp add: Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_inv_def)+
apply (clarsimp simp: in_monad in_alternative conj_disj_distribR[symmetric])
apply (safe)
apply blast
apply (metis flush.exhaust)
apply (rule corres_from_rdonly)
apply (clarsimp)
apply (wp, clarsimp)
apply ( simp only: Let_unfold, wp, clarsimp, rule valid_validE, wp whenE_inv, clarsimp, wp)
apply (assumption)
apply (rule validE_cases_valid, rule hoare_pre)
apply (wp | simp add: Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_inv_def)+
apply (clarsimp simp: in_monad in_alternative conj_disj_distribR[symmetric])
apply (safe)
apply blast
apply (metis flush.exhaust)
apply (rule corres_from_rdonly)
apply (clarsimp)
apply (wp, clarsimp)
apply ( simp only: Let_unfold, wp, clarsimp, rule valid_validE, wp whenE_inv, clarsimp, wp)
apply (assumption)
apply (rule validE_cases_valid, rule hoare_pre)
apply (wp | simp add: Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_inv_def)+
apply (clarsimp simp: in_monad in_alternative conj_disj_distribR[symmetric])
apply (safe)
apply blast
apply (metis flush.exhaust)
apply (clarsimp simp: InvocationLabels_H.isPageFlush_def)+
apply (rule corres_returnOk,clarsimp simp:arch_invocation_relation_def
translate_arch_invocation_def transform_page_inv_def |
clarsimp simp: InvocationLabels_H.isPageFlush_def)+
done
next
case (PageTableCap ptr asid)
thus ?case
apply (simp add: Decode_D.decode_invocation_def
decode_invocation_def arch_decode_invocation_def
transform_cap_simps
transform_cap_simps
split del: split_if)
apply (clarsimp simp: get_page_table_intent_def transform_intent_def
option_map_Some_eq2 throw_opt_def
option_map_Some_eq2 throw_opt_def cdl_get_pt_mapped_addr_def
decode_page_table_invocation_def
transform_intent_page_table_map_def
split del: split_if split: invocation_label.split_asm list.split_asm)
split del: split_if
split: invocation_label.split_asm list.split_asm)
apply (simp add: transform_cap_simps throw_on_none_def transform_cap_list_def
get_index_def split_beta alternative_refl
corres_whenE_throwError_split_rhs corres_alternate2
split: cap.split arch_cap.split option.split cdl_frame_cap_type.splits)
apply (clarsimp simp: dc_def[symmetric] liftE_bindE gets_the_def bind_assoc
corres_symb_exec_in_gets gets_bind_alternative)
get_index_def split_beta alternative_refl
transform_mapping_def corres_whenE_throwError_split_rhs corres_alternate2
split: cap.split arch_cap.split option.split cdl_frame_cap_type.splits)
apply (clarsimp simp: dc_def[symmetric] liftE_bindE
gets_the_def bind_assoc transform_mapping_def
corres_symb_exec_in_gets gets_bind_alternative)
(* apply (rule_tac F="v \<noteq> None" in corres_req)
apply (clarsimp simp: neq_Nil_conv valid_cap_simps obj_at_def
opt_object_page_directory invs_valid_idle
@ -959,11 +907,13 @@ next
apply (wp | simp)+
apply (simp add: whenE_def split del: split_if)
apply (rule hoare_pre, wp, simp)
apply (clarsimp simp: is_final_cap'_def
is_final_cap_def split:list.splits)
apply (simp add: liftE_bindE is_final_cap_def corres_symb_exec_in_gets
unlessE_whenE corres_whenE_throwError_split_rhs
corres_alternate2)
apply (rule corres_alternate1, simp add: returnOk_def)
apply (clarsimp simp: arch_invocation_relation_def translate_arch_invocation_def
apply (clarsimp simp: arch_invocation_relation_def translate_arch_invocation_def get_pt_mapped_addr_def
transform_page_table_inv_def cap_object_simps is_cap_simps)
done
next
@ -976,8 +926,9 @@ next
isPDFlush_def
split del: split_if)
apply (clarsimp simp: get_page_directory_intent_def transform_intent_def
option_map_Some_eq2 throw_opt_def
decode_page_directory_invocation_def split: invocation_label.split_asm cdl_intent.splits InvocationLabels_H.invocation_label.splits)
option_map_Some_eq2 throw_opt_def decode_page_directory_invocation_def
split: invocation_label.split_asm cdl_intent.splits
InvocationLabels_H.invocation_label.splits)
apply (clarsimp simp: neq_Nil_conv valid_cap_simps obj_at_def
Let_unfold opt_object_page_directory invs_valid_idle label_to_flush_type_def InvocationLabels_H.isPDFlush_def InvocationLabels_H.isPageFlush_def
dest!: a_type_pdD)+
@ -993,15 +944,19 @@ next
apply (wp resolve_vaddr_inv | simp add: transform_page_dir_inv_def Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_dir_inv_def in_monad in_alternative conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
apply (rule_tac x="Inl undefined" in exI)
apply (wp resolve_vaddr_inv | simp add: flush_type_map_def transform_page_dir_inv_def Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_dir_inv_def in_monad in_alternative conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
apply (wp resolve_vaddr_inv | simp add: flush_type_map_def transform_page_dir_inv_def
Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_dir_inv_def in_monad in_alternative conj_disj_distribR[symmetric]
split: option.splits | rule impI conjI)+
apply (rule validE_cases_valid, rule hoare_pre, wp)
apply (clarsimp split: option.splits, safe)
apply (wp)
apply (clarsimp simp: whenE_def)
apply (intro conjI impI)
apply (wp resolve_vaddr_inv | simp add: transform_page_dir_inv_def Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_dir_inv_def in_monad in_alternative conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
apply (wp resolve_vaddr_inv
| simp add: transform_page_dir_inv_def Let_unfold arch_invocation_relation_def
translate_arch_invocation_def transform_page_dir_inv_def in_monad in_alternative
conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
apply (rule_tac x="Inl undefined" in exI)
apply (wp resolve_vaddr_inv | simp add: flush_type_map_def transform_page_dir_inv_def Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_dir_inv_def in_monad in_alternative conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
@ -1329,22 +1284,18 @@ lemma invoke_page_table_corres:
apply (drule valid_idle_has_null_cap[rotated -1])
apply (clarsimp simp:invs_def valid_state_def)+
apply (clarsimp simp:kernel_vsrefs_kernel_mapping_slots)
apply (clarsimp simp: is_pt_cap_def bind_assoc)
apply (clarsimp simp: get_pt_mapped_addr_def bind_assoc)
apply (rule dcorres_expand_pfx)
apply (clarsimp simp:valid_pti_def)
apply (clarsimp simp:valid_pti_def transform_mapping_def is_pt_cap_def)
apply (case_tac asid)
apply (clarsimp simp: liftM_def)
apply (rule corres_guard_imp)
apply (rule corres_dummy_return_pr[where b = "()"])
apply (rule corres_dummy_return_pr[where b = "()"])
unfolding K_bind_def
apply (rule corres_split[OF corres_split[where r'="\<lambda>rv. \<top>" and P=\<top> and P'=\<top>, OF _ corres_alternate2] dcorres_unmap_page_table_empty])
apply (rule corres_split[OF _ get_cap_corres])
apply (rule_tac P="\<lambda>y s. cte_wp_at (op = x) (a,b) s \<and> s = s'" in set_cap_corres_stronger)
apply clarsimp
apply (drule cte_wp_at_eqD2, simp)
apply (clarsimp simp:is_arch_diminished_def transform_mapping_def update_map_data_def)
apply (wp get_cap_cte_wp_at_rv | clarsimp)+
apply (rule corres_split[OF _ get_cap_corres])
apply (rule_tac P="\<lambda>y s. cte_wp_at (op = x) (a,b) s \<and> s = s'" in set_cap_corres_stronger)
apply clarsimp
apply (drule cte_wp_at_eqD2, simp)
apply (clarsimp simp:is_arch_diminished_def transform_mapping_def update_map_data_def)
apply (wp get_cap_cte_wp_at_rv | clarsimp)+
apply (clarsimp simp:cte_wp_at_def is_arch_diminished_def is_arch_cap_def is_pt_cap_def)
apply (clarsimp simp:invs_def valid_state_def not_idle_thread_def)
apply (frule valid_idle_has_null_cap,simp+)
@ -1357,7 +1308,7 @@ lemma invoke_page_table_corres:
corres_split[OF _ corres_alternate1[OF dcorres_clear_object_caps_pt]])
apply (rule dcorres_symb_exec_r)
apply (rule corres_split[OF _ get_cap_corres])
apply (rule_tac P="\<lambda>y s. cte_wp_at (op=xa) (a,b) s \<and>
apply (rule_tac P="\<lambda>y s. cte_wp_at (op=xb) (a,b) s \<and>
caps_of_state s' = caps_of_state s" in set_cap_corres_stronger)
apply (clarsimp simp:cte_wp_at_caps_of_state)
apply (clarsimp simp:is_arch_diminished_def transform_mapping_def update_map_data_def)
@ -1677,7 +1628,7 @@ lemma invoke_page_corres:
(invoke_page ip) (perform_page_invocation ip')"
apply (clarsimp simp:invoke_page_def)
apply (case_tac ip')
apply (simp_all add:perform_page_invocation_def)
apply (simp_all add:perform_page_invocation_def)
apply (simp_all add:perform_page_invocation_def transform_page_inv_def)
apply (rule dcorres_expand_pfx)
apply (clarsimp simp:valid_page_inv_def)
@ -1768,10 +1719,8 @@ lemma invoke_page_corres:
cte_wp_at_caps_of_state page_inv_duplicates_valid_def)
-- "PageUnmap"
apply (rule dcorres_expand_pfx)
apply (clarsimp simp: valid_page_inv_def liftM_def
apply (clarsimp simp: valid_page_inv_def transform_mapping_def liftM_def
split:arch_cap.splits option.splits)
apply (simp add:alternative_bind_distrib)
apply (rule corres_alternate2)
apply (rule corres_guard_imp)
apply (rule corres_split[OF _ get_cap_corres])
apply (rule_tac P="\<lambda>y s. cte_wp_at (op = x) (a,b) s \<and> s = s'" in set_cap_corres_stronger)
@ -1780,6 +1729,42 @@ lemma invoke_page_corres:
apply (clarsimp simp:is_arch_diminished_def transform_mapping_def update_map_data_def
dest!:diminished_page_is_page)
apply (wp get_cap_cte_wp_at_rv | clarsimp)+
(*
apply (rule corres_dummy_return_l)
apply (rule corres_split[OF _ store_pte_set_cap_corres])
apply (rule corres_dummy_return_l)
apply (rule_tac corres_split[OF _ dcorres_store_invalid_pte_tail_large_page])
apply (rule wp_to_dcorres[where Q=\<top>])
apply (wp do_machine_op_wp mapM_wp' set_cap_idle
store_pte_page_inv_entries_safe set_cap_page_inv_entries_safe
| clarsimp simp:cleanCacheRange_PoU_def)+
apply (rule dcorres_expand_pfx)
apply (clarsimp simp:mapM_singleton mapM_x_mapM valid_page_inv_def)
apply (rule corres_guard_imp)
apply (rule corres_dummy_return_l)
apply (rule corres_split[OF _ store_pde_set_cap_corres])
apply (rule corres_dummy_return_l)
apply (rule_tac corres_split[OF _ dcorres_store_invalid_pde_tail_super_section])
apply (rule wp_to_dcorres[where Q=\<top>])
apply (wp do_machine_op_wp mapM_wp' set_cap_idle
set_cap_page_inv_entries_safe store_pde_page_inv_entries_safe
| clarsimp simp:cleanCacheRange_PoU_def valid_slots_def
)+
apply (clarsimp simp:invs_def valid_state_def
cte_wp_at_caps_of_state page_inv_duplicates_valid_def)
apply (rule dcorres_expand_pfx)
apply (clarsimp simp: valid_page_inv_def liftM_def
transform_mapping_def
split:arch_cap.splits option.splits)
apply (rule corres_guard_imp)
apply (rule corres_split[OF _ get_cap_corres])
apply (rule_tac P="\<lambda>y s. cte_wp_at (op = x) (a,b) s \<and> s = s'" in set_cap_corres_stronger)
apply clarsimp
apply (drule cte_wp_at_eqD2, simp)
apply (clarsimp simp:is_arch_diminished_def transform_mapping_def update_map_data_def
dest!:diminished_page_is_page)
apply (wp get_cap_cte_wp_at_rv | clarsimp)+
*)
apply (clarsimp simp:cte_wp_at_def is_arch_diminished_def is_arch_cap_def is_pt_cap_def
dest!:diminished_page_is_page)
apply (clarsimp simp:invs_def valid_state_def not_idle_thread_def)
@ -1787,10 +1772,11 @@ lemma invoke_page_corres:
apply (rule sym)
apply (simp add:get_cap_caps_of_state)+
apply (rule corres_guard_imp)
apply (rule corres_split[OF _ corres_alternate1[OF dcorres_unmap_page]])
apply (rule corres_split[OF _ dcorres_unmap_page])
apply (rule corres_split[OF _ get_cap_corres])
apply (rule_tac P="\<lambda>y s. cte_wp_at (op=x) (a,b) s \<and>
caps_of_state s' = caps_of_state s" in set_cap_corres_stronger)
caps_of_state s' = caps_of_state s"
in set_cap_corres_stronger)
apply (clarsimp simp:cte_wp_at_caps_of_state)
apply (clarsimp simp:is_arch_diminished_def transform_mapping_def update_map_data_def
dest!:diminished_page_is_page)
@ -1809,6 +1795,7 @@ lemma invoke_page_corres:
apply (frule valid_idle_has_null_cap, (simp add: valid_idle_def)+)
apply (rule sym)
apply (simp add:get_cap_caps_of_state)+
-- "PageFlush"
apply (clarsimp simp:invoke_page_def)
apply (clarsimp simp: when_def split: if_splits)
@ -1830,7 +1817,7 @@ lemma invoke_page_corres:
apply simp
apply (rule corres_split[OF set_message_info_corres set_mrs_corres_no_recv_buffer[unfolded dc_def]])
apply (wp | simp add: not_idle_thread_def)+
apply (auto simp: ct_active_not_idle_etc[unfolded not_idle_thread_def] )
apply (auto simp: invs_valid_idle ct_active_not_idle_etc[unfolded not_idle_thread_def] )
done
declare tl_drop_1[simp]
@ -1841,6 +1828,23 @@ lemma valid_etcbs_clear_um_detype:
obj_at_kh_def obj_at_def detype_def detype_ext_def clear_um_def)
lemma unat_map_upd:
"unat_map (Some \<circ> transform_asid_table_entry \<circ> arm_asid_table
as (asid_high_bits_of base \<mapsto> frame)) =
unat_map (Some \<circ> transform_asid_table_entry \<circ> arm_asid_table as)
(unat (asid_high_bits_of base) \<mapsto> AsidPoolCap frame 0)"
apply (rule ext)
apply (clarsimp simp:unat_map_def asid_high_bits_of_def
transform_asid_table_entry_def)
apply (intro impI conjI)
apply (subgoal_tac "x<256")
apply (clarsimp simp:unat_map_def asid_high_bits_of_def asid_low_bits_def
transform_asid_table_entry_def transform_asid_def)
apply (drule_tac x="of_nat x" in unat_cong)
apply (subst (asm) word_unat.Abs_inverse)
apply (clarsimp simp:unats_def unat_ucast)+
done
lemma invoke_asid_control_corres:
assumes "arch_invocation_relation (cdl_invocation.InvokeAsidControl asid_inv)
(arch_invocation.InvokeASIDControl asid_inv')"
@ -1861,8 +1865,9 @@ proof -
fix s s' frame cnode_ref cref base cap idx
note retype_dc = retype_region_dcorres[where type="ArchObject ASIDPoolObj",
unfolded translate_object_type_def, simplified]
note insert_dc = insert_cap_child_corres[where cap="cap.ArchObjectCap (arch_cap.ASIDPoolCap x y)",
simplified transform_cap_simps, standard]
note insert_dc = insert_cap_child_corres
[where cap="cap.ArchObjectCap (arch_cap.ASIDPoolCap x y)",
simplified transform_cap_simps ,standard]
note [simp del] = untyped_range.simps usable_untyped_range.simps atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex
@ -1890,7 +1895,6 @@ proof -
apply (cases asid_inv, clarsimp)
apply (drule sym)
apply (drule sym)
apply (drule sym)
apply clarsimp
apply (rule corres_guard_imp)
apply (rule corres_split [OF _ delete_objects_dcorres])
@ -1904,22 +1908,15 @@ proof -
apply (rule corres_split [OF _ retype_dc[where ptr = frame and sz = pageBits ]])
apply (simp add:retype_addrs_def obj_bits_api_def default_arch_object_def
retype_transform_obj_ref_def)
apply (rule corres_split[OF _ insert_dc, where R="\<lambda>rv. \<top>"])
apply (rule corres_split[OF _ insert_dc[unfolded fun_app_def],
where R="\<lambda>rv. \<top>"])
apply (rule corres_assert_rhs[where P'=\<top>])
apply (simp add: gets_fold_into_modify dc_def[symmetric])
apply (clarsimp simp:simpler_modify_def put_def bind_def corres_underlying_def)
apply (clarsimp simp:transform_def transform_objects_def transform_cdt_def
transform_current_thread_def)
apply (clarsimp simp:transform_asid_table_def fun_upd_def[symmetric])
apply (rule ext)
apply (subgoal_tac "ab<256")
apply (clarsimp simp:unat_map_def asid_high_bits_of_def asid_low_bits_def
transform_asid_table_entry_def transform_asid_def)
apply (drule_tac x="of_nat x" in unat_cong)
apply (subst (asm) word_unat.Abs_inverse)
apply (clarsimp simp:unats_def unat_ucast)+
apply (clarsimp simp:transform_asid_def asid_high_bits_of_def asid_low_bits_def)
apply (rule unat_lt2p[where 'a=8, simplified])
apply (clarsimp simp:transform_asid_table_def transform_asid_def
fun_upd_def[symmetric] unat_map_upd)
apply wp
apply (rule_tac Q="\<lambda>rv s. cte_wp_at (\<lambda>c. \<exists>idx. c = (cap.UntypedCap frame pageBits idx))
cref s

10
proof/drefine/CNode_DR.thy
View File

@ -1348,7 +1348,7 @@ lemma dcorres_recycle_asid_pool_caps:
apply (rule dcorres_absorb_get_r)
apply (clarsimp split:split_if)
apply (intro conjI)
apply (clarsimp simp:bind_assoc)
apply (clarsimp simp:bind_assoc transform_asid_def)
apply (rule corres_alternate1)
apply (rule corres_guard_imp)
apply (rule corres_split[OF _ dcorres_delete_asid_pool])
@ -1358,7 +1358,7 @@ lemma dcorres_recycle_asid_pool_caps:
apply (rule dcorres_absorb_get_l)
apply (rule corres_guard_imp)
apply (rule corres_split[where r'=dc and P=\<top> and P'=\<top> and R="\<lambda>s. \<top>" and R'="\<lambda>s. \<top>"])
apply clarsimp
apply (clarsimp simp:transform_asid_def)
apply (clarsimp simp:KHeap_D.set_object_def set_object_def simpler_modify_def
get_def put_def bind_def return_def)
apply (clarsimp simp:corres_underlying_def transform_def transform_current_thread_def
@ -1538,10 +1538,8 @@ lemma opt_cap_pd_Some:
apply (clarsimp simp:opt_cap_def slots_of_def
object_slots_def transform_objects_def restrict_map_def not_idle_thread_def)
apply (simp add:opt_object_page_directory object_slots_def)
apply (clarsimp simp:transform_page_directory_contents_def transform_pde_def unat_map_def below_kernel_base)
apply (clarsimp simp:ucast_def)
apply (simp add: word_of_int_nat[OF uint_ge_0,simplified] unat_def)
apply (simp add:mask_pd_bits_less)
apply (clarsimp simp:transform_page_directory_contents_def
transform_pde_def unat_map_def below_kernel_base)
done
lemma inj_neq:"\<lbrakk>inj f;a\<noteq> b\<rbrakk> \<Longrightarrow> f a\<noteq> f b"

927
proof/drefine/Finalise_DR.thy
View File

File diff suppressed because it is too large Load Diff

2
proof/drefine/Refine_D.thy
View File

@ -64,4 +64,4 @@ lemma dcorres_call_kernel:
apply (clarsimp simp: ct_in_state_def st_tcb_at_def obj_at_def valid_sched_def)
done
end
end

15
proof/drefine/StateTranslation_D.thy
View File

@ -1,4 +1,3 @@
(*
* Copyright 2014, NICTA
*
@ -335,7 +334,7 @@ definition
| ARMPageTableMap \<Rightarrow>
Option.map PageTableIntent
(transform_intent_page_table_map args)
| ARMPageTableUnmap \<Rightarrow> Some (PageTableIntent PageTableUnmapIntent)
| ARMPageTableUnmap \<Rightarrow> Some (PageTableIntent PageTableUnmapIntent)
| ARMPageMap \<Rightarrow>
Option.map PageIntent
(transform_intent_page_map args)
@ -355,8 +354,8 @@ definition
| ARMASIDControlMakePool \<Rightarrow>
Option.map AsidControlIntent
(transform_cnode_index_and_depth AsidControlMakePoolIntent args)
| ARMASIDPoolAssign \<Rightarrow> Some (AsidPoolIntent AsidPoolAssignIntent)
| DomainSetSet \<Rightarrow> Option.map DomainIntent (transform_intent_domain args)"
| ARMASIDPoolAssign \<Rightarrow> Some (AsidPoolIntent (AsidPoolAssignIntent 0))
| Domainsetset \<Rightarrow> Option.map DomainIntent (transform_intent_domain args)"
lemmas transform_intent_tcb_defs =
transform_intent_tcb_read_registers_def
@ -560,9 +559,9 @@ where
"transform_asid asid = (unat (asid_high_bits_of asid), unat (ucast asid :: 10 word))"
definition
transform_mapping :: "(asid \<times> vspace_ref) option \<Rightarrow> cdl_asid option"
transform_mapping :: "(asid \<times> vspace_ref) option \<Rightarrow> cdl_mapped_addr option"
where
" transform_mapping mp = option_map (transform_asid \<circ> fst) mp"
" transform_mapping mp = option_map (\<lambda>x. (transform_asid (fst x),snd x)) mp"
(*
* Transform a cap in the abstract spec to an equivalent
@ -603,7 +602,7 @@ where
ARM_Structs_A.ASIDControlCap \<Rightarrow>
Types_D.AsidControlCap
| ARM_Structs_A.ASIDPoolCap ptr asid \<Rightarrow>
Types_D.AsidPoolCap ptr (transform_asid asid)
Types_D.AsidPoolCap ptr (fst $ (transform_asid asid))
| ARM_Structs_A.PageCap ptr cap_rights_ sz mp \<Rightarrow>
Types_D.FrameCap ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp)
| ARM_Structs_A.PageTableCap ptr mp \<Rightarrow>
@ -1083,7 +1082,7 @@ definition
where
"transform_asid_table_entry p \<equiv> case p of
None \<Rightarrow> Types_D.NullCap
| Some p \<Rightarrow> Types_D.AsidPoolCap p (0, 0)"
| Some p \<Rightarrow> Types_D.AsidPoolCap p 0"
definition
transform_asid_table :: "'z::state_ext state \<Rightarrow> cdl_cap_map"

15
proof/drefine/Syscall_DR.thy
View File

@ -496,16 +496,20 @@ lemma transform_intent_arch_cap_None:
apply wp
apply (clarsimp | rule conjI)+
apply (case_tac "excaps ! 0")
apply (clarsimp simp:transform_intent_def transform_intent_page_remap_def split:list.split_asm)
apply (clarsimp simp:transform_intent_def
transform_intent_page_remap_def split:list.split_asm)
apply ((clarsimp simp:transform_intent_def | wp)+)
apply (case_tac "invocation_type label")
apply (simp_all)
apply (intro conjI impI | wp)+
apply (clarsimp | rule conjI)+
apply (clarsimp simp:transform_intent_def transform_intent_page_table_map_def split:list.split_asm)
apply (clarsimp simp:transform_intent_def | wp)+
apply (intro conjI impI | wp)+
apply (clarsimp simp:transform_intent_def transform_intent_page_table_map_def split:list.split_asm)
apply (clarsimp simp:transform_intent_def transform_intent_page_table_map_def
split:list.split_asm)
apply (intro conjI impI | wp)+
apply ((clarsimp simp:transform_intent_def
split:list.split_asm
| wp)+)[1]
apply (case_tac "invocation_type label")
apply (simp_all add: isPDFlush_def)
apply (wp)
@ -611,7 +615,6 @@ lemma ct_running_not_idle_etc:
done
lemma dcorres_set_eobject_tcb:
"\<lbrakk> \<exists>tcb'. (transform_tcb (machine_state s') p' tcb' etcb = Tcb tcb \<and> kheap s' p' = Some (TCB tcb'));
p' \<noteq> idle_thread s'; kheap s' p' \<noteq> None; ekheap s' p' \<noteq> None \<rbrakk> \<Longrightarrow>

8
spec/capDL/Asid_D.thy
View File

@ -41,7 +41,7 @@ where
ensure_empty target_slot;
returnOk $ MakePool (set_available_range untyped_cap {}) untyped_cap_ref
(cap_objects untyped_cap) target_slot (base, 0)
(cap_objects untyped_cap) target_slot base
odE \<sqinter> throw"
definition
@ -49,7 +49,7 @@ definition
cdl_asid_pool_intent \<Rightarrow> cdl_asid_pool_invocation except_monad"
where
"decode_asid_pool_invocation target target_ref caps intent \<equiv> case intent of
AsidPoolAssignIntent \<Rightarrow>
AsidPoolAssignIntent vaddr \<Rightarrow>
doE
(pd_cap, pd_cap_ref) \<leftarrow> throw_on_none $ get_index caps 0;
(case pd_cap of
@ -57,7 +57,7 @@ where
| _ \<Rightarrow> throw);
base \<leftarrow> (case target of
AsidPoolCap p base \<Rightarrow> returnOk $ fst base
AsidPoolCap p base \<Rightarrow> returnOk $ base
| _ \<Rightarrow> throw);
offset \<leftarrow> liftE $ select {x. x < 2 ^ asid_low_bits};
returnOk $ Assign (base, offset) pd_cap_ref (cap_object target, offset)
@ -86,7 +86,7 @@ where
(* Update the asid table. *)
asid_table \<leftarrow> gets cdl_asid_table;
asid_table' \<leftarrow> return $ asid_table (fst base \<mapsto> AsidPoolCap frame (0, 0));
asid_table' \<leftarrow> return $ asid_table (base \<mapsto> AsidPoolCap frame 0);
modify (\<lambda>s. s \<lparr>cdl_asid_table := asid_table'\<rparr>)
od"

19
spec/capDL/CSpace_D.thy
View File

@ -105,11 +105,11 @@ where
* Delete an ASID pool.
*)
definition
delete_asid_pool :: "cdl_asid \<Rightarrow> cdl_object_id \<Rightarrow> unit k_monad"
delete_asid_pool :: "cdl_cnode_index \<Rightarrow> cdl_object_id \<Rightarrow> unit k_monad"
where
"delete_asid_pool base ptr \<equiv> do
asid_table \<leftarrow> gets cdl_asid_table;
asid_table' \<leftarrow> return $ asid_table (fst base \<mapsto> NullCap);
asid_table' \<leftarrow> return $ asid_table (base \<mapsto> NullCap);
modify (\<lambda>s. s \<lparr>cdl_asid_table := asid_table'\<rparr>)
od \<sqinter> return ()"
@ -124,7 +124,7 @@ where
asid_table \<leftarrow> gets cdl_asid_table;
case asid_table (fst asid) of
Some NullCap \<Rightarrow> return ()
| Some (AsidPoolCap p _) \<Rightarrow> set_cap (p, snd asid) NullCap
| Some (AsidPoolCap p _) \<Rightarrow> set_cap (p, (snd asid)) NullCap
| _ \<Rightarrow> fail
od \<sqinter> return ()"
@ -209,15 +209,15 @@ where
return (NullCap, None)
od
else return (NullCap, None))"
| "finalise_cap (PageTableCap ptr x asid) final = (
| "finalise_cap (PageTableCap ptr x (Some asid)) final = (
if (final \<and> x = Real) then do
unmap_page_table ptr;
unmap_page_table asid ptr;
return (NullCap, None)
od
else return (NullCap, None))"
| "finalise_cap (FrameCap ptr _ _ x asid) final = (
| "finalise_cap (FrameCap ptr _ s x (Some asid)) final = (
if x = Real then do
unmap_page ptr;
unmap_page asid ptr s;
return (NullCap, None)
od
else return (NullCap, None))"
@ -235,8 +235,7 @@ lemma fast_finalise_def2:
assert (result = (NullCap, None))
od"
apply (cases cap, simp_all add: liftM_def assert_def can_fast_finalise_def)
apply (case_tac option)
apply simp+
apply (case_tac option,simp+)+
done
(*
@ -541,7 +540,7 @@ where
delete_asid_pool base ptr;
clear_object_caps ptr;
asid_table \<leftarrow> gets cdl_asid_table;
asid_table' \<leftarrow> return $ asid_table (fst base \<mapsto> AsidPoolCap ptr (0, 0));
asid_table' \<leftarrow> return $ asid_table (base \<mapsto> AsidPoolCap ptr 0);
modify (\<lambda>s. s \<lparr>cdl_asid_table := asid_table'\<rparr>);
return cap
od \<sqinter> return cap

2
spec/capDL/Intents_D.thy
View File

@ -165,7 +165,7 @@ datatype cdl_asid_control_intent =
datatype cdl_asid_pool_intent =
(* Assign: (target), (vroot) *)
AsidPoolAssignIntent
AsidPoolAssignIntent word32
datatype cdl_async_endpoint_intent =
SendAsyncMessageIntent word32

8
spec/capDL/Invocations_D.thy
View File

@ -63,11 +63,11 @@ datatype cdl_reply_invocation =
datatype cdl_page_table_invocation =
(* PageTableMap <real_pt_cap> <pt_cap> <pt_cap_ref> <pd_target_slot> *)
PageTableMap cdl_cap cdl_cap cdl_cap_ref cdl_cap_ref
(* PageTableUnmap <pt_cap_ref> <pt_cap_ref> *)
| PageTableUnmap cdl_object_id cdl_cap_ref
(* PageTableUnmap <mapped_addr option> <pt_obj_id> <pt_cap_ref> *)
| PageTableUnmap "cdl_mapped_addr option" cdl_object_id cdl_cap_ref
datatype cdl_asid_control_invocation =
MakePool cdl_cap cdl_cap_ref "cdl_object_id set" cdl_cap_ref cdl_asid
MakePool cdl_cap cdl_cap_ref "cdl_object_id set" cdl_cap_ref nat
datatype cdl_asid_pool_invocation =
Assign cdl_asid cdl_cap_ref cdl_cap_ref
@ -78,7 +78,7 @@ datatype flush =
datatype cdl_page_invocation =
PageMap cdl_cap cdl_cap cdl_cap_ref "cdl_cap_ref list"
| PageRemap cdl_cap "cdl_cap_ref list"
| PageUnmap cdl_object_id cdl_cap_ref
| PageUnmap "cdl_mapped_addr option" cdl_object_id "cdl_cap_ref" nat
| PageFlushCaches flush
| PageGetAddress

110
spec/capDL/PageTableUnmap_D.thy
View File

@ -213,29 +213,92 @@ where
od) s"
by auto
definition cdl_get_pde :: "(word32 \<times> nat)\<Rightarrow> cdl_cap k_monad"
where "cdl_get_pde ptr \<equiv>
KHeap_D.get_cap ptr"
definition cdl_lookup_pd_slot :: "word32 \<Rightarrow> word32 \<Rightarrow> word32 \<times> nat "
where "cdl_lookup_pd_slot pd vptr \<equiv> (pd, unat (vptr >> 20))"
definition cdl_lookup_pt_slot :: "word32 \<Rightarrow> word32 \<Rightarrow> (word32 \<times> nat) except_monad"
where "cdl_lookup_pt_slot pd vptr \<equiv>
doE pd_slot \<leftarrow> returnOk (cdl_lookup_pd_slot pd vptr);
pdcap \<leftarrow> liftE $ cdl_get_pde pd_slot;
(case pdcap of cdl_cap.PageTableCap ref Fake None
\<Rightarrow> ( doE pt \<leftarrow> returnOk ref;
pt_index \<leftarrow> returnOk ((vptr >> 12) && 0xFF);
returnOk (pt,unat pt_index)
odE)
| _ \<Rightarrow> Monads_D.throw)
odE"
definition
cdl_find_pd_for_asid :: "cdl_mapped_addr \<Rightarrow> cdl_object_id except_monad"
where
"cdl_find_pd_for_asid maddr \<equiv> doE
asid_table \<leftarrow> liftE $ gets cdl_asid_table;
asid_pool \<leftarrow> returnOk $ asid_table (fst (fst maddr));
pd_cap_ref \<leftarrow> (case asid_pool of Some (AsidPoolCap ptr _) \<Rightarrow> returnOk (ptr, (snd \<circ> fst) maddr)
| _ \<Rightarrow> throw );
pd_cap \<leftarrow> liftE $ get_cap pd_cap_ref;
case pd_cap of (PageDirectoryCap pd _ _) \<Rightarrow> returnOk pd
| _ \<Rightarrow> throw
odE "
definition cdl_page_mapping_entries :: "32 word \<Rightarrow> nat \<Rightarrow> 32 word
\<Rightarrow> ((32 word \<times> nat) list) except_monad"
where "cdl_page_mapping_entries vptr pgsz pd \<equiv>
if pgsz = 12 then doE
p \<leftarrow> cdl_lookup_pt_slot pd vptr;
returnOk [p]
odE
else if pgsz = 16 then doE
p \<leftarrow> cdl_lookup_pt_slot pd vptr;
returnOk [p]
odE
else if pgsz = 20 then doE
p \<leftarrow> returnOk $ (cdl_lookup_pd_slot pd vptr);
returnOk [p]
odE
else if pgsz = 24 then doE
p \<leftarrow> returnOk $ (cdl_lookup_pd_slot pd vptr);
returnOk [p]
odE
else throw"
definition
cdl_page_table_mapped :: "cdl_mapped_addr \<Rightarrow> cdl_object_id \<Rightarrow> (cdl_cap_ref option) k_monad"
where
"cdl_page_table_mapped maddr pt_id \<equiv> doE
pd \<leftarrow> cdl_find_pd_for_asid maddr;
pd_slot \<leftarrow> returnOk (cdl_lookup_pd_slot pd (snd maddr));
pdcap \<leftarrow> liftE $ cdl_get_pde pd_slot;
(case pdcap of
cdl_cap.PageTableCap ref Fake None \<Rightarrow>
(returnOk $ if ref = pt_id then Some pd_slot else None)
| _ \<Rightarrow> returnOk None )
odE <catch> (K (return None))"
text {*
Unmap a frame.
We can't deterministically calculate what will be unmapped without
modelling the complexities of ASIDs and keeping track in each frame
cap which ASID/slot it was used to provide a mapping in.
Instead, we just non-deterministically choose a bunch of mappings
to remove. This is painful, but less painful than forcing users to
deal with the complexities of ASIDs.
Unmap a frame.
*}
definition
unmap_page :: "cdl_object_id \<Rightarrow> unit k_monad"
"might_throw \<equiv> (returnOk ()) \<sqinter> throw"
definition
unmap_page :: "cdl_mapped_addr \<Rightarrow> cdl_object_id \<Rightarrow> nat \<Rightarrow> unit k_monad"
where
"unmap_page frame_id \<equiv>
do
all_mappings \<leftarrow> gets $ slots_with (\<lambda>x. \<exists>rights sz asid.
x = FrameCap frame_id rights sz Fake asid);
y \<leftarrow> select {M. set M \<subseteq> all_mappings \<and> distinct M};
mapM_x delete_cap_simple y
od"
"unmap_page maddr frame_id pgsz \<equiv>
doE
pd \<leftarrow> cdl_find_pd_for_asid maddr;
pslots \<leftarrow> cdl_page_mapping_entries (snd maddr) pgsz pd;
might_throw;
liftE $ mapM_x delete_cap_simple pslots;
returnOk ()
odE <catch> (K $ return ())"
text {*
@ -245,14 +308,13 @@ text {*
non-deterministically choose a bunch of page-tables to unmap.
*}
definition
unmap_page_table :: "cdl_object_id \<Rightarrow> unit k_monad"
unmap_page_table :: "cdl_mapped_addr \<Rightarrow> cdl_object_id \<Rightarrow> unit k_monad"
where
"unmap_page_table pt_id \<equiv>
"unmap_page_table maddr pt_id\<equiv>
do
all_mappings \<leftarrow> gets $ slots_with (\<lambda>x. \<exists>rights.
x = PageTableCap pt_id Fake rights);
y \<leftarrow> select {M. set M \<subseteq> all_mappings \<and> distinct M};
mapM_x delete_cap_simple y
pt_slot \<leftarrow> cdl_page_table_mapped maddr pt_id;
case pt_slot of (Some slot) \<Rightarrow> delete_cap_simple slot
| None \<Rightarrow> return ()
od"

109
spec/capDL/PageTable_D.thy
View File

@ -29,47 +29,10 @@ where
"all_pd_pt_slots pd pd_id state \<equiv> {(pd_id, y). y \<in> dom (object_slots pd)}
\<union> {(x, y). \<exists> a b c. (object_slots pd) a = Some (PageTableCap x b c) \<and> x \<in> dom (cdl_objects state)}"
definition cdl_get_pde :: "(word32 \<times> nat)\<Rightarrow> cdl_cap k_monad"
where "cdl_get_pde ptr \<equiv>
KHeap_D.get_cap ptr"
definition cdl_lookup_pd_slot :: "word32 \<Rightarrow> word32 \<Rightarrow> word32 \<times> nat "
where "cdl_lookup_pd_slot pd vptr \<equiv> (pd, unat (vptr >> 20))"
definition cdl_lookup_pt_slot :: "word32 \<Rightarrow> word32 \<Rightarrow> (word32 \<times> nat) except_monad"
where "cdl_lookup_pt_slot pd vptr \<equiv>
doE pd_slot \<leftarrow> returnOk (cdl_lookup_pd_slot pd vptr);
pdcap \<leftarrow> liftE $ cdl_get_pde pd_slot;
(case pdcap of cdl_cap.PageTableCap ref Fake None
\<Rightarrow> ( doE pt \<leftarrow> returnOk ref;
pt_index \<leftarrow> returnOk ((vptr >> 12) && 0xFF);
returnOk (pt,unat pt_index)
odE)
| _ \<Rightarrow> Monads_D.throw)
odE"
definition cdl_create_mapping_entries :: "32 word \<Rightarrow> nat \<Rightarrow> 32 word
\<Rightarrow> ((32 word \<times> nat) list) except_monad"
where "cdl_create_mapping_entries vptr pgsz pd \<equiv>
if pgsz = 12 then doE
p \<leftarrow> cdl_lookup_pt_slot pd vptr;
returnOk [p]
odE
else if pgsz = 16 then doE
p \<leftarrow> cdl_lookup_pt_slot pd vptr;
returnOk [p]
odE
else if pgsz = 20 then doE
p \<leftarrow> returnOk $ (cdl_lookup_pd_slot pd vptr);
returnOk [p]
odE
else if pgsz = 24 then doE
p \<leftarrow> returnOk $ (cdl_lookup_pd_slot pd vptr);
returnOk [p]
odE
else throw"
definition
"cdl_get_pt_mapped_addr cap \<equiv>
case cap of PageTableCap pid ctype maddr \<Rightarrow> maddr
| _ \<Rightarrow> None"
(* Decode a page table intent into an invocation. *)
definition
@ -84,24 +47,28 @@ where
* The concrete implementation only allows a PageTable to be mapped
* once at any point in time, but we don't enforce that here.
*)
PageTableMapIntent vaddr attr \<Rightarrow>
PageTableMapIntent vaddr attr \<Rightarrow>
doE
case cdl_get_pt_mapped_addr target of Some a \<Rightarrow> throw
| None \<Rightarrow> returnOk ();
(* Ensure that a PD was passed in. *)
pd \<leftarrow> throw_on_none $ get_index caps 0;
(pd_object_id, asid) \<leftarrow>
case (fst pd) of
PageDirectoryCap x _ asid \<Rightarrow> returnOk (x, asid)
PageDirectoryCap x _ (Some asid) \<Rightarrow> returnOk (x, asid)
| _ \<Rightarrow> throw;
target_slot \<leftarrow> returnOk $ cdl_lookup_pd_slot pd_object_id vaddr;
returnOk $ PageTableMap (PageTableCap (cap_object target) Real asid)
returnOk $ PageTableMap (PageTableCap (cap_object target) Real (Some (asid,vaddr && ~~ mask 20)))
(PageTableCap (cap_object target) Fake None) target_ref target_slot
odE \<sqinter> throw
(* Unmap this PageTable. *)
| PageTableUnmapIntent \<Rightarrow>
(returnOk $ PageTableUnmap (cap_object target) target_ref) \<sqinter> throw
| PageTableUnmapIntent \<Rightarrow> (
case target of PageTableCap pid ctype maddr \<Rightarrow>
(returnOk $ PageTableUnmap maddr pid target_ref)
| _ \<Rightarrow> throw
) \<sqinter> throw
"
(* Decode a page table intent into an invocation. *)
@ -138,25 +105,29 @@ where
pd \<leftarrow> throw_on_none $ get_index caps 0;
(pd_object_id, asid) \<leftarrow>
case (fst pd) of
PageDirectoryCap x _ asid \<Rightarrow> returnOk (x, asid)
PageDirectoryCap x _ (Some asid) \<Rightarrow> returnOk (x, asid)
| _ \<Rightarrow> throw;
(* Collect mapping from target cap. *)
(frame, sz) \<leftarrow> returnOk $ (case target of FrameCap p R sz m mp \<Rightarrow> (p,sz));
target_slots \<leftarrow> cdl_create_mapping_entries vaddr sz pd_object_id;
target_slots \<leftarrow> cdl_page_mapping_entries vaddr sz pd_object_id;
(* Calculate rights. *)
new_rights \<leftarrow> returnOk $ validate_vm_rights $ cap_rights target \<inter> rights;
(* Return the map intent. *)
returnOk $ PageMap (FrameCap frame (cap_rights target) sz Real asid)
returnOk $ PageMap (FrameCap frame (cap_rights target) sz Real (Some (asid,vaddr)))
(FrameCap frame new_rights sz Fake None) target_ref target_slots
odE \<sqinter> throw
(* Unmap this PageTable. *)
| PageUnmapIntent \<Rightarrow>
(returnOk $ PageUnmap (cap_object target) target_ref) \<sqinter> throw
| PageUnmapIntent \<Rightarrow> doE
(frame, asid, sz) \<leftarrow> (case target of
FrameCap p R sz m mp \<Rightarrow> returnOk (p, mp , sz)
| _ \<Rightarrow> throw);
(returnOk $ PageUnmap asid frame target_ref sz) \<sqinter> throw
odE
(* Change the rights on a given mapping. *)
| PageRemapIntent rights attrs \<Rightarrow>
@ -188,7 +159,9 @@ where
(returnOk $ PageFlushCaches Unify) \<sqinter> (returnOk $ PageFlushCaches Clean) \<sqinter>
(returnOk $ PageFlushCaches CleanInvalidate ) \<sqinter> (returnOk $ PageFlushCaches Invalidate)
\<sqinter> throw
| PageGetAddressIntent \<Rightarrow> returnOk PageGetAddress
"
(* Invoke a page table. *)
@ -200,6 +173,7 @@ where
| PageDirectoryNothing => return ()
"
definition "option_exec f \<equiv> \<lambda>x. case x of Some a \<Rightarrow> f a | None \<Rightarrow> return ()"
(* Invoke a page table. *)
definition
@ -215,12 +189,16 @@ where
*)
insert_cap_orphan pt_cap pd_target_slot
od
| PageTableUnmap obj pt_cap_ref \<Rightarrow>
do unmap_page_table obj;
clear_object_caps obj \<sqinter> return ();
cap \<leftarrow> get_cap pt_cap_ref;
set_cap pt_cap_ref (reset_mem_mapping cap)
| PageTableUnmap mapped_addr pt_id pt_cap_ref \<Rightarrow> do
(case mapped_addr of Some maddr \<Rightarrow> do
unmap_page_table maddr pt_id;
clear_object_caps pt_id \<sqinter> return ()
od
| _ \<Rightarrow> return ());
cap \<leftarrow> get_cap pt_cap_ref;
set_cap pt_cap_ref (reset_mem_mapping cap)
od
"
(* Invoke a page. *)
@ -235,16 +213,18 @@ where
mapM_x (swp set_cap pseudo_frame_cap) target_slots
od
| PageUnmap mapped_addr frame_id frame_cap_ref pgsz \<Rightarrow> do
(case mapped_addr of
Some maddr \<Rightarrow> unmap_page maddr frame_id pgsz
| _ \<Rightarrow> return ());
cap \<leftarrow> get_cap frame_cap_ref;
set_cap frame_cap_ref (reset_mem_mapping cap)
od
| PageRemap pseudo_frame_cap target_slots \<Rightarrow>
mapM_x (swp set_cap pseudo_frame_cap) target_slots
| PageUnmap obj frame_cap_ref \<Rightarrow>
do
unmap_page obj \<sqinter> return ();
cap \<leftarrow> get_cap frame_cap_ref;
set_cap frame_cap_ref (reset_mem_mapping cap)
od
| PageFlushCaches flush \<Rightarrow> return ()
| PageGetAddress \<Rightarrow>
@ -252,6 +232,7 @@ where
ct \<leftarrow> gets_the cdl_current_thread;
corrupt_tcb_intent ct
od
"
end

12
spec/capDL/Types_D.thy
View File

@ -60,6 +60,9 @@ type_synonym cdl_cap_ref = "cdl_object_id \<times> cdl_cnode_index"
(* A virtual ASID. *)
type_synonym cdl_asid = "cdl_cnode_index \<times> cdl_cnode_index"
(* mapped address *)
type_synonym cdl_mapped_addr = "(cdl_asid \<times> word32)"
(* Number of bits in a word. *)
definition
word_bits
@ -126,11 +129,11 @@ datatype cdl_cap =
| IrqHandlerCap cdl_irq
(* Virtual memory capabilties *)
| FrameCap cdl_object_id "cdl_right set" nat cdl_frame_cap_type "cdl_asid option"
| PageTableCap cdl_object_id cdl_frame_cap_type "cdl_asid option"
| FrameCap cdl_object_id "cdl_right set" nat cdl_frame_cap_type "cdl_mapped_addr option"
| PageTableCap cdl_object_id cdl_frame_cap_type "cdl_mapped_addr option"
| PageDirectoryCap cdl_object_id cdl_frame_cap_type "cdl_asid option"
| AsidControlCap
| AsidPoolCap cdl_object_id cdl_asid
| AsidPoolCap cdl_object_id "cdl_cnode_index"
(* x86-specific capabilities *)
| IOPortsCap cdl_object_id "cdl_io_port set"
@ -216,7 +219,6 @@ type_synonym cdl_heap = "cdl_object_id \<Rightarrow> cdl_object option"
translations
(type) "cdl_heap" <=(type) "32 word \<Rightarrow> cdl_object option"
(*
* The current state of the system.
*
@ -644,7 +646,7 @@ where
| TcbType \<Rightarrow> TcbCap (pick id_set)
| CNodeType \<Rightarrow> CNodeCap (pick id_set) 0 0 sz
| UntypedType \<Rightarrow> UntypedCap id_set id_set
| AsidPoolType \<Rightarrow> AsidPoolCap (pick id_set) (0, 0)
| AsidPoolType \<Rightarrow> AsidPoolCap (pick id_set) 0
| PageTableType \<Rightarrow> PageTableCap (pick id_set) Real None
| PageDirectoryType \<Rightarrow> PageDirectoryCap (pick id_set) Real None
| FrameType frame_size \<Rightarrow> FrameCap (pick id_set) {Read, Write} frame_size Real None"