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

arm-hyp ainvs: update for PageMap replacing PageRemap (SELFOUR-161)

This commit is contained in:
Victor Phan 2019-09-25 17:15:16 +10:00
parent 558b2e8f37
commit 10127117ee
4 changed files with 81 additions and 200 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

73
proof/invariant-abstract/ARM_HYP/ArchArch_AI.thy
View File

@ -1082,7 +1082,7 @@ lemma sts_valid_slots_inv[wp]:
lemma sts_valid_page_inv[wp]:
"\<lbrace>valid_page_inv page_invocation\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_page_inv page_invocation\<rbrace>"
by (cases page_invocation,
(wp hoare_vcg_const_Ball_lift hoare_vcg_ex_lift hoare_vcg_imp_lift sts_typ_ats
(wp hoare_vcg_const_Ball_lift hoare_vcg_ex_lift hoare_vcg_disj_lift sts_typ_ats
| clarsimp simp: valid_page_inv_def same_refs_def
| wps)+)
@ -1583,13 +1583,12 @@ lemma arch_decode_inv_wf[wp]:
apply (cases "invocation_type label = ArchInvocationLabel ARMPageMap")
apply (rename_tac word rights vmpage_size option)
apply simp
apply (rule hoare_pre)
apply ((wp whenE_throwError_wp check_vp_wpR hoare_vcg_const_imp_lift_R
create_mapping_entries_parent_for_refs find_pd_for_asid_pd_at_asid
create_mapping_entries_valid_slots create_mapping_entries_same_refs_ex
find_pd_for_asid_lookup_pd_wp
| wpc
| simp add: valid_arch_inv_def valid_page_inv_def is_pg_cap_def)+)
apply (wpsimp wp: whenE_throwError_wp check_vp_wpR create_mapping_entries_parent_for_refs
find_pd_for_asid_pd_at_asid create_mapping_entries_valid_slots
create_mapping_entries_same_refs_ex hoare_vcg_ex_lift_R hoare_vcg_disj_lift_R
hoare_vcg_const_imp_lift_R find_pd_for_asid_lookup_pd_wp
simp: valid_arch_inv_def valid_page_inv_def is_pg_cap_def
cte_wp_at_caps_of_state[where P="\<lambda>c. same_refs rv c s" for rv s])
apply (clarsimp simp: neq_Nil_conv)
apply (frule diminished_cte_wp_at_valid_cap[where p="(a, b)" for a b], clarsimp)
apply (frule diminished_cte_wp_at_valid_cap[where p=slot], clarsimp)
@ -1598,54 +1597,15 @@ lemma arch_decode_inv_wf[wp]:
linorder_not_le aligned_sum_less_kernel_base
dest!: diminished_pd_capD)
apply (clarsimp simp: cap_rights_update_def acap_rights_update_def
split: cap.splits arch_cap.splits)
apply (rename_tac page_size)
apply (rule conjI, fastforce)
apply (cases slot)
apply (clarsimp simp: valid_cap_simps cap_aligned_def valid_kernel_mappings_def
aligned_sum_less_kernel_base asid_bits_def mask_def
is_arch_update_def cap_master_cap_simps is_arch_cap_def)
apply (rule conjI, fastforce)
apply (rule conjI, fastforce)
apply (rule conjI, fastforce)
apply (rule conjI, fastforce)
apply (rule conjI, fastforce)
apply (rule conjI, fastforce)
apply (rule conjI, fastforce)
apply (rule conjI, fastforce)
apply (rule conjI)
apply (fastforce simp: data_at_def split: if_splits)
apply (rule conjI, fastforce simp: vmsz_aligned_def is_aligned_addrFromPPtr_n)
apply (rule conjI, fastforce)
apply (rule conjI)
apply (clarsimp simp: vs_cap_ref_def split: vmpage_size.split)
apply (rule conjI, fastforce)
apply (fastforce intro: diminished_pd_self)
apply (cases "invocation_type label = ArchInvocationLabel ARMPageRemap")
apply (rename_tac word rights vmpage_size option)
apply simp
apply (rule hoare_pre)
apply ((wp whenE_throwError_wp check_vp_wpR hoare_vcg_const_imp_lift_R
create_mapping_entries_parent_for_refs
find_pd_for_asid_lookup_pd_wp
| wpc
| simp add: valid_arch_inv_def valid_page_inv_def
| (simp add: cte_wp_at_caps_of_state,
wp create_mapping_entries_same_refs_ex hoare_vcg_ex_lift_R))+)[1]
apply (clarsimp simp: valid_cap_def cap_aligned_def neq_Nil_conv)
apply (frule diminished_cte_wp_at_valid_cap[where p="(a, b)" for a b], clarsimp)
apply (clarsimp simp: cte_wp_at_caps_of_state mask_cap_def
diminished_def[where cap="ArchObjectCap (PageCap x y z v w)" for x y z v w])
apply (clarsimp simp: cap_rights_update_def acap_rights_update_def
split: cap.splits arch_cap.splits)
apply (rename_tac page_size)
apply (cases slot)
apply (clarsimp simp: valid_cap_simps cap_aligned_def valid_kernel_mappings_def
aligned_sum_less_kernel_base asid_bits_def mask_def
is_arch_update_def cap_master_cap_simps is_arch_cap_def)
apply (fastforce intro!: is_aligned_addrFromPPtr_n diminished_pd_self
simp: data_at_def vmsz_aligned_def
split: if_splits)
split: cap.splits arch_cap.splits if_splits)
apply (rename_tac page_size mapped_data)
apply (intro conjI allI impI;
(clarsimp simp: invs_implies valid_cap_simps cap_aligned_def valid_kernel_mappings_def
aligned_sum_less_kernel_base[symmetric] asid_bits_def mask_def
is_arch_update_def cap_master_cap_simps is_arch_cap_def data_at_def
vmsz_aligned_def is_aligned_addrFromPPtr_n vs_cap_ref_def
split: if_splits vmpage_size.split
| fastforce)+)
apply (cases "invocation_type label = ArchInvocationLabel ARMPageUnmap")
apply simp
apply (rule hoare_pre, wp)
@ -1683,7 +1643,6 @@ lemma arch_decode_inv_wf[wp]:
split: if_split|
rule_tac x="fst p" in hoare_imp_eq_substR|
wp_once hoare_vcg_ex_lift_R)+)[1]
apply (rule_tac Q'="\<lambda>a b. ko_at (ArchObj (PageDirectory pd))
(a + (args ! 0 >> 21 << 3) && ~~ mask pd_bits) b \<longrightarrow>
pd (ucast (a + (args ! 0 >> 21 << 3) && mask pd_bits >> 3)) =

32
proof/invariant-abstract/ARM_HYP/ArchInvariants_AI.thy
View File

@ -384,6 +384,38 @@ where
PageTablePDE ptr\<Rightarrow> Some (ptrFromPAddr ptr)
| _ \<Rightarrow> None"
text
\<open>Virtual address space look-ups
In the invariants, (ref \<unrhd> p) is a predicate on states which asserts the existence of a path through
the current virtual address space mappings, that is rooted in the global ASID table.
The ref is of type "vs_ref list", and represents the path through through the virtual address space
mappings. For example, it may look like this:
[VSRef r3 (Some APageTable), VSRef r2 (Some APageDirectory), VSRef r1 (Some AASIDPool), VSRef r0 None]
In this case:
r0 is the index of an entry in the global ASID table,
r1 is the index of an entry in the ASIDPool pointed to by r0,
r2 is the index of a page directory entry in the page directory mapped to the ASID formed by r0 and r1,
r3 is the index of a page table entry in the page table pointed to by r2.
Then, ((ref \<unrhd> p) s) is an assertion that: in state s, p is a pointer (in the kernel address space)
to a Page object mapped into the page table entry r3.
In this example, r0 and r1 are the high and low bits of the ASID. Similarly, r2 and r3 form parts of
the virtual address to which the page is mapped in this address space.
Note that the path is ordered bottom-up, from the object under consideration, up to the global ASID
table entry from which it can be traced.
A "vs_ref list" need not always trace from a Page object, so for example, ([VSRef r0 None] \<unrhd> p) s)
means: in state s, p is a pointer to an ASIDPool object, which was found in entry r0 of the global
ASID table.
There are also assertions of the form (ref \<rhd> p) which are similar, but don't trace any deeper than
page directory entries.\<close>
datatype vs_ref = VSRef word32 "aa_type option"
definition

104
proof/invariant-abstract/ARM_HYP/ArchVSpaceEntries_AI.thy
View File

@ -720,8 +720,6 @@ definition
"page_inv_duplicates_valid iv \<equiv> case iv of
PageMap asid cap ct_slot entries \<Rightarrow>
page_inv_entries_safe entries
| PageRemap asid entries \<Rightarrow>
page_inv_entries_safe entries
| _ \<Rightarrow> \<top>"
lemma pte_range_interD:
@ -1445,80 +1443,34 @@ lemma decode_mmu_invocation_valid_pdpt[wp]:
apply simp
done
show ?thesis
apply (simp add: decode_mmu_invocation_def
Let_def split_def get_master_pde_def
split del: if_split
cong: arch_cap.case_cong if_cong cap.case_cong
option.case_cong)
apply (rule hoare_pre)
apply ((wp get_pde_wp
ensure_safe_mapping_ensures[THEN hoare_post_imp_R]
create_mapping_entries_safe check_vp_wpR
find_pd_for_asid_aligned_pd_bits
[unfolded vspace_bits_defs,simplified]
| wpc
| simp add: invocation_duplicates_valid_def unlessE_def whenE_def
pti_duplicates_valid_def page_inv_duplicates_valid_def
mask_lower_twice vspace_bits_defs bitwise
not_le sz if_apply_def2
del: hoare_True_E_R
split del: if_split
| simp only: obj_at_def)+)
apply (rule_tac Q'="\<lambda>rv. \<exists>\<rhd> rv and K (is_aligned rv pd_bits) and
(\<exists>\<rhd> (lookup_pd_slot rv (args ! 0) && ~~ mask pd_bits)) and
valid_vspace_objs and pspace_aligned and valid_pdpt_objs"
and f="find_pd_for_asid p" for p
in hoare_post_imp_R)
apply (wp | simp)+
apply (fastforce simp:pd_bits_def pageBits_def pde_bits_def)
apply ((wp get_pde_wp
ensure_safe_mapping_ensures[THEN hoare_post_imp_R]
create_mapping_entries_safe check_vp_wpR
find_pd_for_asid_aligned_pd_bits
[unfolded pd_bits_def pageBits_def,simplified]
| wpc
| simp add: invocation_duplicates_valid_def unlessE_def whenE_def
pti_duplicates_valid_def page_inv_duplicates_valid_def
mask_lower_twice pd_bits_def bitwise pageBits_def
not_le sz if_apply_def2
del: hoare_True_E_R
split del: if_split
| simp only: obj_at_def)+)
apply (rule_tac Q'="\<lambda>rv. \<exists>\<rhd> rv and K (is_aligned rv pd_bits) and
(\<exists>\<rhd> (lookup_pd_slot rv (snd pa) && ~~ mask pd_bits)) and
valid_vspace_objs and pspace_aligned and valid_pdpt_objs and
K ((snd pa) < kernel_base)"
and f="find_pd_for_asid p" for p
in hoare_post_imp_R)
apply (wp| simp)+
apply (auto simp:pd_bits_def pageBits_def)[1]
apply ((wp get_pde_wp
ensure_safe_mapping_ensures[THEN hoare_post_imp_R]
create_mapping_entries_safe check_vp_wpR
find_pd_for_asid_aligned_pd_bits
[unfolded pd_bits_def pageBits_def,simplified]
| wpc
| simp add: invocation_duplicates_valid_def unlessE_def whenE_def
pti_duplicates_valid_def page_inv_duplicates_valid_def
mask_lower_twice pd_bits_def bitwise pageBits_def
not_le sz if_apply_def2
del: hoare_True_E_R
split del: if_split
| simp only: obj_at_def)+)
apply (simp add: vspace_bits_defs)
apply (rule hoare_post_imp_R[where P=\<top>])
apply (rule hoare_True_E_R)
apply (auto simp: bitwise)[1]
apply ((wp
| wpc
| simp add: invocation_duplicates_valid_def unlessE_def whenE_def
pti_duplicates_valid_def page_inv_duplicates_valid_def
if_apply_def2
del: hoare_True_E_R
split del: if_split
| simp only: obj_at_def)+)
apply (auto simp:valid_cap_simps)
done
supply if_split[split del]
apply (simp add: decode_mmu_invocation_def)
\<comment> \<open>Handle the easy cases first (trivial because of the post-condition invocation_duplicates_valid)\<close>
apply (cases "invocation_type label \<notin> {ArchInvocationLabel ARMPageTableMap,
ArchInvocationLabel ARMPageMap}")
apply (wpsimp simp: invocation_duplicates_valid_def page_inv_duplicates_valid_def
pti_duplicates_valid_def Let_def
cong: if_cong)
\<comment> \<open>Handle the two interesting cases now\<close>
apply (clarsimp; erule disjE; cases cap;
simp add: isPDFlushLabel_def isPageFlushLabel_def throwError_R')
\<comment> \<open>PageTableMap\<close>
apply (wpsimp simp: Let_def get_master_pde_def
wp: get_pde_wp hoare_drop_imps hoare_vcg_if_lift_ER)
apply (clarsimp simp: invocation_duplicates_valid_def pti_duplicates_valid_def
mask_lower_twice bitwise obj_at_def vspace_bits_defs if_apply_def2
split: if_splits)
apply wp
\<comment> \<open>PageMap\<close>
apply (rename_tac dev pg_ptr rights sz pg_map)
apply (wpsimp simp: Let_def invocation_duplicates_valid_def page_inv_duplicates_valid_def
wp: ensure_safe_mapping_ensures[THEN hoare_post_imp_R]
check_vp_wpR hoare_vcg_if_lift_ER find_pd_for_asid_lookup_pd_wp)
apply (fastforce simp: invs_psp_aligned page_directory_at_aligned_pd_bits word_not_le sz
valid_cap_def valid_arch_cap_def lookup_pd_slot_eq
split: if_splits)
apply wp
done
qed
lemma returnOk_lift :

72
proof/invariant-abstract/ARM_HYP/ArchVSpace_AI.thy
View File

@ -1871,9 +1871,10 @@ definition
definition
"valid_page_inv pinv \<equiv> case pinv of
"valid_page_inv pg_inv \<equiv> case pg_inv of
PageMap asid cap ptr m \<Rightarrow>
cte_wp_at (is_arch_update cap and ((=) None \<circ> vs_cap_ref)) ptr
cte_wp_at (is_arch_update cap) ptr
and (cte_wp_at (\<lambda>c. vs_cap_ref c = None) ptr or (\<lambda>s. cte_wp_at (\<lambda>c. same_refs m c s) ptr s))
and cte_wp_at is_pg_cap ptr
and (\<lambda>s. same_refs m cap s)
and valid_slots m
@ -1881,11 +1882,6 @@ definition
and K (is_pg_cap cap \<and> empty_refs m \<and> asid \<le> mask asid_bits \<and> asid \<noteq> 0)
and (\<lambda>s. \<exists>slot. cte_wp_at (parent_for_refs m) slot s)
and (\<lambda>s. \<exists>pd. vspace_at_asid asid pd s)
| PageRemap asid m \<Rightarrow>
valid_slots m and K (empty_refs m \<and> asid \<le> mask asid_bits \<and> asid \<noteq> 0)
and (\<lambda>s. \<exists>slot. cte_wp_at (parent_for_refs m) slot s)
and (\<lambda>s. \<exists>slot. cte_wp_at (\<lambda>cap. same_refs m cap s) slot s)
and (\<lambda>s. \<exists>pd. vspace_at_asid asid pd s)
| PageUnmap cap ptr \<Rightarrow>
\<lambda>s. \<exists>dev r R sz m. cap = PageCap dev r R sz m \<and>
case_option True (valid_unmap sz) m \<and>
@ -5694,6 +5690,7 @@ lemma perform_page_invs [wp]:
apply (clarsimp simp: is_cap_simps is_arch_update_def
cap_master_cap_simps
dest!: cap_master_cap_eqDs)
apply (clarsimp simp: same_refs_def)
apply clarsimp
apply (rule conjI)
apply (rule_tac x=aa in exI, rule_tac x=ba in exI)
@ -5713,7 +5710,7 @@ lemma perform_page_invs [wp]:
split: Structures_A.cap.splits arch_cap.splits)
apply (rule conjI)
apply (erule exEI)
apply clarsimp
apply (clarsimp simp: same_refs_def)
apply (rule conjI)
apply clarsimp
apply (rule_tac x=aa in exI, rule_tac x=ba in exI)
@ -5744,65 +5741,6 @@ lemma perform_page_invs [wp]:
apply (drule_tac x=sl in imageI[where f="\<lambda>x. x && ~~ mask pd_bits"])
apply (drule (1) subsetD)
apply (clarsimp simp: cap_range_def)
\<comment> \<open>PageRemap\<close>
apply (rule hoare_pre)
apply (wp get_master_pte_wp get_master_pde_wp hoare_vcg_ex_lift mapM_x_swp_store_pde_invs_unmap
| wpc | simp add: pte_check_if_mapped_def pde_check_if_mapped_def
| (rule hoare_vcg_conj_lift, rule_tac slots=x2a in store_pde_invs_unmap'))+
apply (clarsimp simp: valid_page_inv_def cte_wp_at_caps_of_state
valid_slots_def empty_refs_def neq_Nil_conv
split: sum.splits)
apply (clarsimp simp: parent_for_refs_def same_refs_def is_cap_simps cap_asid_def split:option.splits)
apply (rule conjI, fastforce)
apply (rule conjI)
apply clarsimp
apply (rule_tac x=ac in exI, rule_tac x=bc in exI, rule_tac x=capa in exI)
apply (clarsimp simp: vspace_bits_defs)
apply (erule (2) ref_is_unique[OF _ _ reachable_page_table_not_global])
apply ((simp add: invs_def valid_state_def valid_arch_state_def
valid_arch_caps_def valid_pspace_def valid_objs_caps)+)[9]
apply fastforce
apply( frule valid_global_refsD2)
apply (clarsimp simp: cap_range_def parent_for_refs_def simp del: cap_asid_simps)+
(*
apply (simp_all add: invs_def valid_state_def valid_arch_state_def
valid_arch_caps_def valid_pspace_def valid_objs_caps)[9]
apply fastforce
apply( frule valid_global_refsD2)
apply (clarsimp simp: cap_range_def parent_for_refs_def)+ *)
apply (rule conjI, rule impI)
apply (rule exI, rule exI, rule exI)
apply (erule conjI)
apply clarsimp
apply (rule conjI, rule impI)
apply (rule_tac x=ac in exI, rule_tac x=bc in exI, rule_tac x=capa in exI)
apply (clarsimp simp: same_refs_def pde_ref_def pde_ref_pages_def
valid_pde_def invs_def valid_state_def valid_pspace_def)
apply (drule valid_objs_caps)
apply (clarsimp simp: valid_caps_def)
apply (drule spec, drule spec, drule_tac x=capa in spec, drule (1) mp)
apply (case_tac aa, (clarsimp simp add: data_at_pg_cap)+)[1]
(* subgoal for _ _ aa by ((cases aa, simp_all);
((clarsimp simp: valid_cap_def obj_at_def a_type_def is_ep_def
is_ntfn_def is_cap_table_def is_tcb_def
is_pg_cap_def vspace_bits_defs
split: cap.splits Structures_A.kernel_object.splits
if_split_asm
arch_kernel_obj.splits option.splits
arch_cap.splits))) *)
apply (clarsimp simp: pde_at_def obj_at_def a_type_def simp del: cap_asid_simps)
apply (rule conjI)
apply clarsimp
apply (drule_tac ptr="(ab,bb)" in
valid_global_refsD[OF invs_valid_global_refs caps_of_state_cteD])
apply simp+
apply force
apply (erule ballEI)
apply (clarsimp simp del: cap_asid_simps)
(* apply (drule_tac ptr="(ab,bb)" in
valid_global_refsD[OF invs_valid_global_refs caps_of_state_cteD]) *)
apply simp+
apply force
\<comment> \<open>PageUnmap\<close>
apply (rename_tac arch_cap cslot_ptr)
apply (rule hoare_pre)