re-establish InfoFlow; generalising ptable_xn
UserOp_IF had its own way of extracting the XN bit from page tables. This is now unified with the existing functions in ADT_AI, which also means that the proof for XN bit equality is basically the same as for pt_rights and pt_lift.
This commit is contained in:
Gerwin Klein
parent
7e7d39c24e
commit
29eb636d31
|
|
@ -60,12 +60,12 @@ lemma pd_of_thread_page_directory_at:
|
|||
lemma ptr_offset_in_ptr_range:
|
||||
"\<lbrakk> invs s; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj))
|
||||
(get_pd_of_thread (kheap s) (arch_state s) tcb) x =
|
||||
Some (a, aa, b); x \<notin> kernel_mappings;
|
||||
Some (base, sz, attr, r); x \<notin> kernel_mappings;
|
||||
get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s) \<rbrakk>
|
||||
\<Longrightarrow> ptrFromPAddr a + (x && mask aa) \<in> ptr_range (ptrFromPAddr a) aa"
|
||||
\<Longrightarrow> ptrFromPAddr base + (x && mask sz) \<in> ptr_range (ptrFromPAddr base) sz"
|
||||
apply (simp add: ptr_range_def mask_def)
|
||||
apply (rule conjI)
|
||||
apply (rule_tac b="2 ^ aa - 1" in word_plus_mono_right2)
|
||||
apply (rule_tac b="2 ^ sz - 1" in word_plus_mono_right2)
|
||||
apply (frule some_get_page_info_umapsD)
|
||||
apply (clarsimp simp: get_pd_of_thread_reachable invs_arch_objs
|
||||
invs_psp_aligned invs_valid_asid_table invs_valid_objs)+
|
||||
|
|
@ -160,14 +160,14 @@ lemma pt_in_pd_page_table_at:
|
|||
done
|
||||
|
||||
lemma get_page_info_state_objs_to_policy:
|
||||
"\<lbrakk> invs s; auth \<in> vspace_cap_rights_to_auth b;
|
||||
"\<lbrakk> invs s; auth \<in> vspace_cap_rights_to_auth r;
|
||||
get_page_info (\<lambda>obj. get_arch_obj (kheap s obj))
|
||||
(get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (a, aa, b);
|
||||
(get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r);
|
||||
get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s);
|
||||
get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj))
|
||||
(get_pd_of_thread (kheap s) (arch_state s) tcb) x =
|
||||
Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings \<rbrakk>
|
||||
\<Longrightarrow> (ptrFromPAddr word1, auth, ptrFromPAddr (a + (x && mask aa))) \<in> state_objs_to_policy s"
|
||||
\<Longrightarrow> (ptrFromPAddr word1, auth, ptrFromPAddr (base + (x && mask sz))) \<in> state_objs_to_policy s"
|
||||
apply (simp add: state_objs_to_policy_def)
|
||||
apply (rule sbta_vref)
|
||||
apply (clarsimp simp: state_vrefs_def split: option.splits)
|
||||
|
|
@ -176,10 +176,10 @@ lemma get_page_info_state_objs_to_policy:
|
|||
apply (clarsimp simp: typ_at_eq_kheap_obj)
|
||||
|
||||
apply (clarsimp simp: vs_refs_no_global_pts_def)
|
||||
apply (rule_tac x="(ucast ((x >> 12) && mask 8), ptrFromPAddr a, aa,
|
||||
vspace_cap_rights_to_auth b)" in bexI)
|
||||
apply (rule_tac x="(ucast ((x >> 12) && mask 8), ptrFromPAddr base, sz,
|
||||
vspace_cap_rights_to_auth r)" in bexI)
|
||||
apply clarsimp
|
||||
apply (rule_tac x="(ptrFromPAddr a + (x && mask aa), auth)" in image_eqI)
|
||||
apply (rule_tac x="(ptrFromPAddr base + (x && mask sz), auth)" in image_eqI)
|
||||
apply (simp add: ptrFromPAddr_def physMappingOffset_def kernelBase_addr_def physBase_def)
|
||||
apply (simp add: ptr_offset_in_ptr_range)
|
||||
|
||||
|
|
|
|||
|
|
@ -1827,12 +1827,12 @@ lemma not_in_global_refs_vs_lookup:
|
|||
small page, since the invariants tell us that the
|
||||
arm_globals_frame is only a small page *)
|
||||
lemma get_page_info_arm_globals_frame:
|
||||
"\<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) p = Some (b, a, r);
|
||||
"\<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) p = Some (base, sz, attr, r);
|
||||
get_pd_of_thread (kheap s) (arch_state s) t \<noteq> arm_global_pd (arch_state s);
|
||||
valid_arch_state s; valid_arch_objs s; valid_global_pd_mappings s;
|
||||
equal_kernel_mappings s; valid_vs_lookup s; valid_global_objs s;
|
||||
valid_global_refs s;
|
||||
b = addrFromPPtr (arm_globals_frame (arch_state s))\<rbrakk> \<Longrightarrow> r = {}"
|
||||
base = addrFromPPtr (arm_globals_frame (arch_state s))\<rbrakk> \<Longrightarrow> r = {}"
|
||||
apply(case_tac "p \<in> kernel_mappings")
|
||||
apply(blast dest: some_get_page_info_kmapsD)
|
||||
apply(clarsimp simp: get_pd_of_thread_def split: option.splits kernel_object.splits cap.splits arch_cap.splits if_splits)
|
||||
|
|
@ -1898,36 +1898,37 @@ lemma ptrFromPAddr_add_helper:
|
|||
done
|
||||
|
||||
lemma get_page_info_is_arm_globals_frame:
|
||||
notes blah[simp del] = atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
|
||||
Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex
|
||||
notes [simp del] = atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
|
||||
Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex
|
||||
shows
|
||||
"\<lbrakk>x \<in> range_of_arm_globals_frame sa; invs sa;
|
||||
get_page_info (\<lambda>obj. get_arch_obj (kheap sa obj))
|
||||
(get_pd_of_thread (kheap sa) (arch_state sa) t) xa =
|
||||
Some (a, aa, b);
|
||||
a + (xa && mask aa) = addrFromPPtr x;
|
||||
get_pd_of_thread (kheap sa) (arch_state sa) t \<noteq> arm_global_pd (arch_state sa);
|
||||
xa \<notin> kernel_mappings\<rbrakk> \<Longrightarrow>
|
||||
ptrFromPAddr a = (arm_globals_frame (arch_state sa))"
|
||||
"\<lbrakk>x \<in> range_of_arm_globals_frame s; invs s;
|
||||
get_page_info (\<lambda>obj. get_arch_obj (kheap s obj))
|
||||
(get_pd_of_thread (kheap s) (arch_state s) t) x' =
|
||||
Some (base, psz, attr, r);
|
||||
base + (x' && mask psz) = addrFromPPtr x;
|
||||
get_pd_of_thread (kheap s) (arch_state s) t \<noteq> arm_global_pd (arch_state s);
|
||||
x' \<notin> kernel_mappings\<rbrakk> \<Longrightarrow>
|
||||
ptrFromPAddr base = (arm_globals_frame (arch_state s))"
|
||||
apply(frule some_get_page_info_umapsD)
|
||||
(* following two lines clagged from ADT_AC.ptr_offset_in_ptr_range *)
|
||||
apply (clarsimp simp: get_pd_of_thread_reachable invs_arch_objs
|
||||
invs_psp_aligned invs_valid_asid_table invs_valid_objs)+
|
||||
apply(subgoal_tac "typ_at (AArch (AIntData ARMSmallPage)) (arm_globals_frame (arch_state sa)) sa")
|
||||
apply(rename_tac sz)
|
||||
apply(subgoal_tac "typ_at (AArch (AIntData ARMSmallPage)) (arm_globals_frame (arch_state s)) s")
|
||||
apply(clarsimp simp: obj_at_def)
|
||||
prefer 2
|
||||
apply(fastforce dest: invs_arch_state simp: valid_arch_state_def)
|
||||
apply(frule invs_distinct)
|
||||
apply(clarsimp simp: pspace_distinct_def)
|
||||
apply(drule_tac x="ptrFromPAddr a" in spec, drule_tac x="arm_globals_frame (arch_state sa)" in spec)
|
||||
apply(drule_tac x="ptrFromPAddr base" in spec, drule_tac x="arm_globals_frame (arch_state s)" in spec)
|
||||
apply simp
|
||||
apply(case_tac "ptrFromPAddr a = arm_globals_frame (arch_state sa)")
|
||||
apply(case_tac "ptrFromPAddr base = arm_globals_frame (arch_state s)")
|
||||
apply assumption
|
||||
apply(frule ptr_offset_in_ptr_range)
|
||||
apply (simp+)
|
||||
apply(simp add: ptr_range_def)
|
||||
apply(subgoal_tac "ptrFromPAddr a + (xa && mask (pageBitsForSize sz)) \<in> {arm_globals_frame
|
||||
(arch_state sa)..arm_globals_frame (arch_state sa) + 0xFFF}")
|
||||
apply(subgoal_tac "ptrFromPAddr base + (x' && mask (pageBitsForSize sz)) \<in> {arm_globals_frame
|
||||
(arch_state s)..arm_globals_frame (arch_state s) + 0xFFF}")
|
||||
apply(simp only: p_assoc_help)
|
||||
apply blast
|
||||
apply(drule_tac y="addrFromPPtr x" and f=ptrFromPAddr in arg_cong)
|
||||
|
|
@ -1957,8 +1958,10 @@ lemma empty_rights_in_arm_globals_frame:
|
|||
apply(erule invs_equal_kernel_mappings)
|
||||
apply blast
|
||||
apply(rule get_page_info_arm_globals_frame)
|
||||
apply (simp add: invs_arch_state invs_arch_objs invs_valid_global_pd_mappings invs_equal_kernel_mappings invs_valid_vs_lookup invs_valid_global_objs invs_valid_global_refs)+
|
||||
apply(drule get_page_info_is_arm_globals_frame, simp+)
|
||||
apply (simp add: invs_arch_state invs_arch_objs invs_valid_global_pd_mappings
|
||||
invs_equal_kernel_mappings invs_valid_vs_lookup invs_valid_global_objs
|
||||
invs_valid_global_refs)+
|
||||
apply(drule get_page_info_is_arm_globals_frame, simp+)[1]
|
||||
apply(fastforce dest: arg_cong[where f=addrFromPPtr])
|
||||
done
|
||||
|
||||
|
|
@ -3755,4 +3758,4 @@ where
|
|||
"uop_sane f \<equiv> \<forall>t pl pr pxn tcu. (f t pl pr pxn tcu) \<noteq> {} \<and>
|
||||
(\<forall>tc um es. (Some Interrupt, tc, um, es) \<notin> (f t pl pr pxn tcu))"
|
||||
|
||||
end (* a comment *)
|
||||
end
|
||||
|
|
|
|||
|
|
@ -116,12 +116,15 @@ definition
|
|||
"ptable_lift_s' s \<equiv> ptable_lift (ksCurThread s) (absKState s)"
|
||||
|
||||
definition
|
||||
"ptable_xn_s' s \<equiv> ptable_xn (ksCurThread s) (absKState s)"
|
||||
"ptable_attrs_s' s \<equiv> ptable_attrs (ksCurThread s) (absKState s)"
|
||||
|
||||
definition
|
||||
"ptable_xn_s' s \<equiv> \<lambda>addr. XNever \<in> ptable_attrs_s' s addr"
|
||||
|
||||
definition doUserOp_if :: "user_transition_if \<Rightarrow> user_context \<Rightarrow> (kernel_state, (event option \<times> user_context)) nondet_monad" where
|
||||
"doUserOp_if uop tc \<equiv>
|
||||
do pr \<leftarrow> gets ptable_rights_s';
|
||||
pxn \<leftarrow> gets ptable_xn_s';
|
||||
pxn \<leftarrow> gets (\<lambda>s x. pr x \<noteq> {} \<and> ptable_xn_s' s x);
|
||||
pl \<leftarrow> gets (\<lambda>s. ptable_lift_s' s |` {x. pr x \<noteq> {}});
|
||||
t \<leftarrow> getCurThread;
|
||||
um \<leftarrow>
|
||||
|
|
@ -199,7 +202,7 @@ lemma do_user_op_if_corres:
|
|||
apply (clarsimp elim!: state_relationE)
|
||||
apply (rule_tac r'="op=" and P=einvs and P'=invs' in corres_split)
|
||||
prefer 2
|
||||
apply (clarsimp simp: ptable_xn_s_def ptable_xn_s'_def)
|
||||
apply (clarsimp simp: ptable_attrs_s'_def ptable_attrs_s_def ptable_xn_s'_def ptable_xn_s_def)
|
||||
apply (subst absKState_correct, fastforce, assumption+)
|
||||
apply (clarsimp elim!: state_relationE)
|
||||
apply (rule_tac r'="op=" and P=einvs and P'=invs' in corres_split)
|
||||
|
|
@ -374,7 +377,7 @@ lemma do_user_op_if_corres':
|
|||
apply (rule_tac r'="op=" and P=einvs and P'=invs' in corres_split)
|
||||
prefer 2
|
||||
apply (clarsimp simp: absArchState_correct curthread_relation ptable_xn_s'_def
|
||||
ptable_xn_s_def)
|
||||
ptable_xn_s_def ptable_attrs_s_def ptable_attrs_s'_def)
|
||||
apply (subst absKState_correct, fastforce, assumption+)
|
||||
apply simp
|
||||
apply (clarsimp elim!: state_relationE)
|
||||
|
|
|
|||
|
|
@ -314,17 +314,22 @@ lemma kernelEntry_corres_C:
|
|||
|
||||
end
|
||||
|
||||
context state_rel
|
||||
begin
|
||||
|
||||
definition (in state_rel)
|
||||
definition
|
||||
"ptable_rights_s'' s \<equiv> ptable_rights (cur_thread (cstate_to_A s)) (cstate_to_A s)"
|
||||
|
||||
definition (in state_rel)
|
||||
definition
|
||||
"ptable_lift_s'' s \<equiv> ptable_lift (cur_thread (cstate_to_A s)) (cstate_to_A s)"
|
||||
|
||||
definition (in state_rel)
|
||||
"ptable_xn_s'' s \<equiv> ptable_xn (cur_thread (cstate_to_A s)) (cstate_to_A s)"
|
||||
definition
|
||||
"ptable_attrs_s'' s \<equiv> ptable_attrs (cur_thread (cstate_to_A s)) (cstate_to_A s)"
|
||||
|
||||
definition (in state_rel)
|
||||
definition
|
||||
"ptable_xn_s'' s \<equiv> \<lambda>addr. XNever \<in> ptable_attrs_s'' s addr"
|
||||
|
||||
definition
|
||||
doMachineOp_C :: "(machine_state, 'a) nondet_monad \<Rightarrow> (cstate, 'a) nondet_monad"
|
||||
where
|
||||
"doMachineOp_C mop \<equiv>
|
||||
|
|
@ -335,13 +340,13 @@ where
|
|||
return r
|
||||
od"
|
||||
|
||||
definition (in state_rel) doUserOp_C_if
|
||||
definition doUserOp_C_if
|
||||
:: "user_transition_if \<Rightarrow> user_context \<Rightarrow> (cstate, (event option \<times> user_context)) nondet_monad"
|
||||
where
|
||||
"doUserOp_C_if uop tc \<equiv>
|
||||
do
|
||||
pr \<leftarrow> gets ptable_rights_s'';
|
||||
pxn \<leftarrow> gets ptable_xn_s'';
|
||||
pxn \<leftarrow> gets (\<lambda>s x. pr x \<noteq> {} \<and> ptable_xn_s'' s x);
|
||||
pl \<leftarrow> gets (\<lambda>s. restrict_map (ptable_lift_s'' s) {x. pr x \<noteq> {}});
|
||||
t \<leftarrow> gets (\<lambda>s. cur_thread (cstate_to_A s));
|
||||
um \<leftarrow> gets (\<lambda>s. restrict_map (user_mem_C (globals s) \<circ> ptrFromPAddr)
|
||||
|
|
@ -358,11 +363,12 @@ definition (in state_rel) doUserOp_C_if
|
|||
od"
|
||||
|
||||
|
||||
definition (in state_rel)
|
||||
definition
|
||||
do_user_op_C_if
|
||||
where
|
||||
"do_user_op_C_if uop \<equiv> {(s,e,(tc,s'))| s e tc s'. ((e,tc),s') \<in> fst (split (doUserOp_C_if uop) s)}"
|
||||
|
||||
end
|
||||
|
||||
context kernel_m begin
|
||||
|
||||
|
|
@ -451,7 +457,8 @@ lemma do_user_op_if_C_corres:
|
|||
invs_def valid_state_def valid_pspace_def state_relation_def)
|
||||
apply (rule_tac r'="op=" and P'=\<top> and P="invs' and ex_abs (einvs)" in corres_split)
|
||||
prefer 2
|
||||
apply (clarsimp simp: ptable_xn_s'_def ptable_xn_s''_def cstate_to_A_def rf_sr_def)
|
||||
apply (clarsimp simp: ptable_xn_s'_def ptable_xn_s''_def ptable_attrs_s_def
|
||||
ptable_attrs_s'_def ptable_attrs_s''_def cstate_to_A_def rf_sr_def)
|
||||
apply (subst cstate_to_H_correct, simp add: invs'_def,force+)+
|
||||
apply (simp only: ex_abs_def)
|
||||
apply (elim exE conjE)
|
||||
|
|
|
|||
|
|
@ -1721,14 +1721,6 @@ lemma valid_sched_s0[simp]:
|
|||
apply (clarsimp simp: valid_idle_etcb_def etcb_at'_def ekh0_obj_def s0_ptr_defs idle_thread_ptr_def)
|
||||
done
|
||||
|
||||
lemma executable_arch_objs_s0[simp]:
|
||||
"executable_arch_objs s0_internal"
|
||||
by (clarsimp simp: executable_arch_objs_def executable_arch_obj_def
|
||||
executable_pte_def executable_pde_def s0_internal_def
|
||||
obj_at_def kh0_def kh0_obj_def s0_ptr_defs High_pt'_def Low_pt'_def
|
||||
High_pd'_def Low_pd'_def
|
||||
split: arch_kernel_obj.splits pte.splits pde.splits split_if_asm)
|
||||
|
||||
lemma einvs_s0:
|
||||
"einvs s0_internal"
|
||||
apply (simp add: valid_state_def invs_def)
|
||||
|
|
|
|||
|
|
@ -129,7 +129,7 @@ definition
|
|||
Low_pt'H :: "word8 \<Rightarrow> Hardware_H.pte "
|
||||
where
|
||||
"Low_pt'H \<equiv> (\<lambda>_. Hardware_H.InvalidPTE)
|
||||
(0 := Hardware_H.SmallPagePTE shared_page_ptr (PageCacheable \<in> {}) (Global \<in> {}) (vmrights_map vm_read_write))"
|
||||
(0 := Hardware_H.SmallPagePTE shared_page_ptr (PageCacheable \<in> {}) (Global \<in> {}) (XNever \<in> {}) (vmrights_map vm_read_write))"
|
||||
|
||||
definition
|
||||
Low_ptH :: "word32 \<Rightarrow> word32 \<Rightarrow> Structures_H.kernel_object option"
|
||||
|
|
@ -141,7 +141,9 @@ where
|
|||
|
||||
definition
|
||||
[simp]:
|
||||
"global_pdH \<equiv> (\<lambda>_. Hardware_H.InvalidPDE)( ucast (kernel_base >> 20) := Hardware_H.SectionPDE (addrFromPPtr kernel_base) (ParityEnabled \<in> {}) 0 (PageCacheable \<in> {}) (Global \<in> {}) (vmrights_map {}))"
|
||||
"global_pdH \<equiv> (\<lambda>_. Hardware_H.InvalidPDE)( ucast (kernel_base >> 20) :=
|
||||
Hardware_H.SectionPDE (addrFromPPtr kernel_base) (ParityEnabled \<in> {}) 0
|
||||
(PageCacheable \<in> {}) (Global \<in> {}) (XNever \<in> {}) (vmrights_map {}))"
|
||||
|
||||
|
||||
definition
|
||||
|
|
@ -152,7 +154,7 @@ where
|
|||
(0 := Hardware_H.PageTablePDE
|
||||
(Platform.addrFromPPtr Low_pt_ptr)
|
||||
(ParityEnabled \<in> {})
|
||||
undefined )"
|
||||
undefined)"
|
||||
|
||||
(* used addrFromPPtr because proof gives me ptrFromAddr.. TODO: check
|
||||
if it's right *)
|
||||
|
|
@ -174,7 +176,8 @@ definition
|
|||
where
|
||||
"High_pt'H \<equiv>
|
||||
(\<lambda>_. Hardware_H.InvalidPTE)
|
||||
(0 := Hardware_H.SmallPagePTE shared_page_ptr (PageCacheable \<in> {}) (Global \<in> {}) (vmrights_map vm_read_only))"
|
||||
(0 := Hardware_H.SmallPagePTE shared_page_ptr (PageCacheable \<in> {}) (Global \<in> {}) (XNever \<in> {})
|
||||
(vmrights_map vm_read_only))"
|
||||
|
||||
|
||||
definition
|
||||
|
|
|
|||
|
|
@ -20,9 +20,6 @@ begin
|
|||
datatype 'a partition = Partition 'a | PSched
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
fun scheduler_modes where
|
||||
"scheduler_modes KernelPreempted = True" |
|
||||
"scheduler_modes (KernelEntry Interrupt) = True" |
|
||||
|
|
|
|||
|
|
@ -26,31 +26,20 @@ definition ptable_lift_s where
|
|||
definition ptable_rights_s where
|
||||
"ptable_rights_s s \<equiv> ptable_rights (cur_thread s) s"
|
||||
|
||||
definition get_pt_xn :: "(obj_ref \<rightharpoonup> arch_kernel_obj) \<Rightarrow> obj_ref \<Rightarrow> word32 \<rightharpoonup> bool" where
|
||||
"get_pt_xn ahp pt_ref vptr \<equiv>
|
||||
case get_pt_entry ahp pt_ref vptr of
|
||||
Some (ARM_Structs_A.SmallPagePTE base atts _) \<Rightarrow> Some (XNever \<in> atts)
|
||||
| Some (ARM_Structs_A.LargePagePTE base atts _) \<Rightarrow> Some (XNever \<in> atts)
|
||||
| _ \<Rightarrow> None"
|
||||
|
||||
definition get_page_xn :: "(obj_ref \<rightharpoonup> arch_kernel_obj) \<Rightarrow> obj_ref \<Rightarrow> word32 \<rightharpoonup> bool" where
|
||||
"get_page_xn ahp pd_ref vptr \<equiv>
|
||||
case get_pd_entry ahp pd_ref vptr of
|
||||
Some (ARM_Structs_A.PageTablePDE p _ _) \<Rightarrow>
|
||||
get_pt_xn ahp (Platform.ptrFromPAddr p) vptr
|
||||
| Some (ARM_Structs_A.SectionPDE base atts _ _) \<Rightarrow> Some (XNever \<in> atts)
|
||||
| Some (ARM_Structs_A.SuperSectionPDE base atts _) \<Rightarrow> Some (XNever \<in> atts)
|
||||
| _ \<Rightarrow> None"
|
||||
|
||||
(* FIXME: move to ADT_AI.thy *)
|
||||
definition
|
||||
ptable_xn :: "obj_ref \<Rightarrow> 'z state \<Rightarrow> word32 \<Rightarrow> bool" where
|
||||
"ptable_xn tcb s \<equiv> \<lambda>addr.
|
||||
case_option False (\<lambda>x. x)
|
||||
(get_page_xn (\<lambda>obj. get_arch_obj (kheap s obj))
|
||||
ptable_attrs :: "obj_ref \<Rightarrow> 'z state \<Rightarrow> word32 \<Rightarrow> vm_attributes" where
|
||||
"ptable_attrs tcb s \<equiv> \<lambda>addr.
|
||||
case_option {} (fst o snd o snd)
|
||||
(get_page_info (\<lambda>obj. get_arch_obj (kheap s obj))
|
||||
(get_pd_of_thread (kheap s) (arch_state s) tcb) addr)"
|
||||
|
||||
definition
|
||||
ptable_attrs_s :: "'z state \<Rightarrow> word32 \<Rightarrow> vm_attributes" where
|
||||
"ptable_attrs_s s \<equiv> ptable_attrs (cur_thread s) s"
|
||||
|
||||
definition ptable_xn_s where
|
||||
"ptable_xn_s s \<equiv> ptable_xn (cur_thread s) s"
|
||||
"ptable_xn_s s \<equiv> \<lambda>addr. XNever \<in> ptable_attrs_s s addr"
|
||||
|
||||
definition getExMonitor :: "exclusive_monitors machine_monad" where
|
||||
"getExMonitor \<equiv> gets exclusive_state"
|
||||
|
|
@ -64,8 +53,8 @@ definition do_user_op_if where
|
|||
(* Get the page rights of each address (ReadOnly, ReadWrite, None, etc). *)
|
||||
pr \<leftarrow> gets ptable_rights_s;
|
||||
|
||||
(* Fetch the 'execute never' bits of the current thread's page directory. *)
|
||||
pxn \<leftarrow> gets ptable_xn_s;
|
||||
(* Fetch the 'execute never' bits of the current thread's page mappings. *)
|
||||
pxn \<leftarrow> gets (\<lambda>s x. pr x \<noteq> {} \<and> ptable_xn_s s x);
|
||||
|
||||
(* Get the mapping from virtual to physical addresses. *)
|
||||
pl \<leftarrow> gets (\<lambda>s. restrict_map (ptable_lift_s s) {x. pr x \<noteq> {}});
|
||||
|
|
@ -229,51 +218,98 @@ lemma requiv_ptable_rights_eq:
|
|||
apply (rule ext)
|
||||
apply (case_tac "x \<in> kernel_mappings")
|
||||
apply (clarsimp simp: ptable_rights_def split: option.splits)
|
||||
apply (intro conjI)
|
||||
apply (rule conjI)
|
||||
apply clarsimp
|
||||
apply (frule some_get_page_info_kmapsD)
|
||||
apply (fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings
|
||||
vspace_cap_rights_to_auth_def)+
|
||||
apply ((fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings
|
||||
vspace_cap_rights_to_auth_def)+)[4]
|
||||
apply clarsimp
|
||||
apply (frule some_get_page_info_kmapsD)
|
||||
apply (fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings
|
||||
vspace_cap_rights_to_auth_def)+
|
||||
apply ((fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings
|
||||
vspace_cap_rights_to_auth_def)+)[4]
|
||||
apply clarsimp
|
||||
apply (frule_tac r=ba in some_get_page_info_kmapsD)
|
||||
apply (fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings
|
||||
vspace_cap_rights_to_auth_def)+
|
||||
apply ((fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings
|
||||
vspace_cap_rights_to_auth_def)+)[4]
|
||||
|
||||
apply (case_tac "get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)
|
||||
= arm_global_pd (arch_state s)")
|
||||
apply (frule requiv_pd_of_thread_global_pd)
|
||||
apply fastforce+
|
||||
apply (fastforce+)[4]
|
||||
apply (clarsimp simp: ptable_rights_def split: option.splits)
|
||||
apply (intro conjI)
|
||||
apply (rule conjI)
|
||||
apply clarsimp
|
||||
apply (frule get_page_info_gpd_kmaps[rotated, rotated])
|
||||
apply (fastforce simp: invs_valid_global_objs invs_arch_state)+
|
||||
apply ((fastforce simp: invs_valid_global_objs invs_arch_state)+)[3]
|
||||
apply clarsimp
|
||||
apply (intro conjI)
|
||||
apply (rule conjI)
|
||||
apply clarsimp
|
||||
apply (frule get_page_info_gpd_kmaps[rotated, rotated])
|
||||
apply (fastforce simp: invs_valid_global_objs invs_arch_state)+
|
||||
apply ((fastforce simp: invs_valid_global_objs invs_arch_state)+)[3]
|
||||
apply clarsimp
|
||||
apply (frule get_page_info_gpd_kmaps[rotated, rotated])
|
||||
apply (fastforce simp: invs_valid_global_objs invs_arch_state)+
|
||||
apply ((fastforce simp: invs_valid_global_objs invs_arch_state)+)[3]
|
||||
|
||||
apply (case_tac "get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')
|
||||
= arm_global_pd (arch_state s')")
|
||||
apply (drule reads_equiv_sym)
|
||||
apply (frule requiv_pd_of_thread_global_pd)
|
||||
apply (fastforce simp: reads_equiv_def)+
|
||||
apply ((fastforce simp: reads_equiv_def)+)[5]
|
||||
|
||||
apply (simp add: ptable_rights_def)
|
||||
apply (frule requiv_get_pd_of_thread_eq)
|
||||
apply fastforce+
|
||||
apply (fastforce+)[6]
|
||||
apply (frule pd_of_thread_same_agent, simp+)
|
||||
apply (subst requiv_get_page_info_eq, simp+)
|
||||
done
|
||||
|
||||
|
||||
lemma requiv_ptable_attrs_eq:
|
||||
"\<lbrakk> reads_equiv aag s s'; pas_refined aag s; pas_refined aag s';
|
||||
is_subject aag (cur_thread s); invs s; invs s'; ptable_rights_s s x \<noteq> {} \<rbrakk>
|
||||
\<Longrightarrow> ptable_attrs_s s x = ptable_attrs_s s' x"
|
||||
apply (simp add: ptable_attrs_s_def ptable_rights_s_def)
|
||||
apply (case_tac "x \<in> kernel_mappings")
|
||||
apply (clarsimp simp: ptable_attrs_def split: option.splits)
|
||||
apply (rule conjI)
|
||||
apply clarsimp
|
||||
apply (frule some_get_page_info_kmapsD)
|
||||
apply ((fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings
|
||||
vspace_cap_rights_to_auth_def ptable_rights_def)+)[4]
|
||||
apply clarsimp
|
||||
apply (frule some_get_page_info_kmapsD)
|
||||
apply ((fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings
|
||||
vspace_cap_rights_to_auth_def ptable_rights_def)+)[4]
|
||||
|
||||
apply (case_tac "get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)
|
||||
= arm_global_pd (arch_state s)")
|
||||
apply (frule requiv_pd_of_thread_global_pd)
|
||||
apply (fastforce+)[4]
|
||||
apply (clarsimp simp: ptable_attrs_def split: option.splits)
|
||||
apply (rule conjI)
|
||||
apply clarsimp
|
||||
apply (frule get_page_info_gpd_kmaps[rotated, rotated])
|
||||
apply ((fastforce simp: invs_valid_global_objs invs_arch_state)+)[3]
|
||||
apply clarsimp
|
||||
apply (rule conjI)
|
||||
apply (frule get_page_info_gpd_kmaps[rotated, rotated])
|
||||
apply ((fastforce simp: invs_valid_global_objs invs_arch_state)+)[3]
|
||||
apply clarsimp
|
||||
apply (frule get_page_info_gpd_kmaps[rotated, rotated])
|
||||
apply ((fastforce simp: invs_valid_global_objs invs_arch_state)+)[3]
|
||||
|
||||
apply (case_tac "get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')
|
||||
= arm_global_pd (arch_state s')")
|
||||
apply (drule reads_equiv_sym)
|
||||
apply (frule requiv_pd_of_thread_global_pd)
|
||||
apply ((fastforce simp: reads_equiv_def)+)[5]
|
||||
|
||||
apply (simp add: ptable_attrs_def)
|
||||
apply (frule requiv_get_pd_of_thread_eq, simp+)[1]
|
||||
apply (frule pd_of_thread_same_agent, simp+)[1]
|
||||
apply (subst requiv_get_page_info_eq, simp+)[1]
|
||||
done
|
||||
|
||||
lemma requiv_ptable_lift_eq:
|
||||
"\<lbrakk> reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s;
|
||||
invs s'; is_subject aag (cur_thread s); ptable_rights_s s x \<noteq> {} \<rbrakk>
|
||||
|
|
@ -281,166 +317,50 @@ lemma requiv_ptable_lift_eq:
|
|||
apply (simp add: ptable_lift_s_def ptable_rights_s_def)
|
||||
apply (case_tac "x \<in> kernel_mappings")
|
||||
apply (clarsimp simp: ptable_lift_def split: option.splits)
|
||||
apply (intro conjI)
|
||||
apply (rule conjI)
|
||||
apply clarsimp
|
||||
apply (frule some_get_page_info_kmapsD)
|
||||
apply (fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings
|
||||
vspace_cap_rights_to_auth_def ptable_rights_def)+
|
||||
apply ((fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings
|
||||
vspace_cap_rights_to_auth_def ptable_rights_def)+)[4]
|
||||
apply clarsimp
|
||||
apply (frule some_get_page_info_kmapsD)
|
||||
apply (fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings
|
||||
vspace_cap_rights_to_auth_def ptable_rights_def)+
|
||||
apply ((fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings
|
||||
vspace_cap_rights_to_auth_def ptable_rights_def)+)[4]
|
||||
|
||||
apply (case_tac "get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)
|
||||
= arm_global_pd (arch_state s)")
|
||||
apply (frule requiv_pd_of_thread_global_pd)
|
||||
apply fastforce+
|
||||
apply (fastforce+)[4]
|
||||
apply (clarsimp simp: ptable_lift_def split: option.splits)
|
||||
apply (intro conjI)
|
||||
apply (rule conjI)
|
||||
apply clarsimp
|
||||
apply (frule get_page_info_gpd_kmaps[rotated, rotated])
|
||||
apply (fastforce simp: invs_valid_global_objs invs_arch_state)+
|
||||
apply ((fastforce simp: invs_valid_global_objs invs_arch_state)+)[3]
|
||||
apply clarsimp
|
||||
apply (intro conjI)
|
||||
apply (rule conjI)
|
||||
apply (frule get_page_info_gpd_kmaps[rotated, rotated])
|
||||
apply (fastforce simp: invs_valid_global_objs invs_arch_state)+
|
||||
apply ((fastforce simp: invs_valid_global_objs invs_arch_state)+)[3]
|
||||
apply clarsimp
|
||||
apply (frule get_page_info_gpd_kmaps[rotated, rotated])
|
||||
apply (fastforce simp: invs_valid_global_objs invs_arch_state)+
|
||||
apply ((fastforce simp: invs_valid_global_objs invs_arch_state)+)[3]
|
||||
|
||||
apply (case_tac "get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')
|
||||
= arm_global_pd (arch_state s')")
|
||||
apply (drule reads_equiv_sym)
|
||||
apply (frule requiv_pd_of_thread_global_pd)
|
||||
apply (fastforce simp: reads_equiv_def)+
|
||||
apply ((fastforce simp: reads_equiv_def)+)[5]
|
||||
|
||||
apply (simp add: ptable_lift_def)
|
||||
apply (frule requiv_get_pd_of_thread_eq, simp+)
|
||||
apply (frule pd_of_thread_same_agent, simp+)
|
||||
apply (subst requiv_get_page_info_eq, simp+)
|
||||
done
|
||||
|
||||
lemma requiv_get_pt_xn_eq:
|
||||
"\<lbrakk> reads_equiv aag s s'; pas_refined aag s; is_subject aag pt \<rbrakk>
|
||||
\<Longrightarrow> get_pt_xn (\<lambda>obj. get_arch_obj (kheap s obj)) pt x
|
||||
= get_pt_xn (\<lambda>obj. get_arch_obj (kheap s' obj)) pt x"
|
||||
apply (simp add: get_pt_xn_def)
|
||||
apply (subst requiv_get_pt_entry_eq, simp+)
|
||||
done
|
||||
|
||||
lemma requiv_get_page_xn_eq:
|
||||
"\<lbrakk> reads_equiv aag s s'; pas_refined aag s; is_subject aag pd;
|
||||
x \<notin> kernel_mappings \<rbrakk>
|
||||
\<Longrightarrow> get_page_xn (\<lambda>obj. get_arch_obj (kheap s obj)) pd x
|
||||
= get_page_xn (\<lambda>obj. get_arch_obj (kheap s' obj)) pd x"
|
||||
apply (simp add: get_page_xn_def)
|
||||
apply (subst requiv_get_pd_entry_eq[symmetric], simp+)
|
||||
apply (clarsimp split: option.splits pde.splits)
|
||||
apply (frule pt_in_pd_same_agent, fastforce+)
|
||||
apply (rule requiv_get_pt_xn_eq, simp+)
|
||||
done
|
||||
|
||||
lemma some_get_page_xn_kmapsD:
|
||||
"\<lbrakk>get_page_xn (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ref p = Some xn;
|
||||
p \<in> kernel_mappings; valid_global_pd_mappings s; equal_kernel_mappings s\<rbrakk>
|
||||
\<Longrightarrow> \<not> xn"
|
||||
apply (clarsimp simp: get_page_xn_def get_pd_entry_def get_arch_obj_def
|
||||
kernel_mappings_slots_eq
|
||||
split: option.splits Structures_A.kernel_object.splits
|
||||
arch_kernel_obj.splits)
|
||||
apply (erule valid_global_pd_mappingsE)
|
||||
apply (clarsimp simp: equal_kernel_mappings_def obj_at_def)
|
||||
apply (drule_tac x=pd_ref in spec,
|
||||
drule_tac x="arm_global_pd (arch_state s)" in spec, simp)
|
||||
apply (drule bspec, assumption)
|
||||
apply (clarsimp simp: valid_pd_kernel_mappings_def pde_mapping_bits_def)
|
||||
apply (drule_tac x="ucast (p >> 20)" in spec)
|
||||
apply (clarsimp simp: get_page_xn_def get_pd_entry_def get_arch_obj_def
|
||||
get_pt_xn_def get_pt_entry_def
|
||||
kernel_mappings_slots_eq
|
||||
split: option.splits Structures_A.kernel_object.splits
|
||||
arch_kernel_obj.splits
|
||||
ARM_Structs_A.pde.splits ARM_Structs_A.pte.splits)
|
||||
apply (simp add: valid_pde_kernel_mappings_def obj_at_def
|
||||
valid_pt_kernel_mappings_def)
|
||||
apply (drule_tac x="ucast ((p >> 12) && mask 8)" in spec)
|
||||
apply (clarsimp simp: valid_pte_kernel_mappings_def)
|
||||
apply (simp add: valid_pde_kernel_mappings_def obj_at_def
|
||||
valid_pt_kernel_mappings_def)
|
||||
apply (drule_tac x="ucast ((p >> 12) && mask 8)" in spec)
|
||||
apply (clarsimp simp: valid_pte_kernel_mappings_def)
|
||||
apply (simp add: valid_pde_kernel_mappings_def)
|
||||
apply (simp add: valid_pde_kernel_mappings_def)
|
||||
done
|
||||
|
||||
lemma get_pt_xn_some_get_pt_info:
|
||||
"get_pt_xn ahp pd_ref vptr = Some xn \<Longrightarrow>
|
||||
\<exists>base sz rights. get_pt_info ahp pd_ref vptr = Some (base, sz, rights)"
|
||||
by (simp add: get_pt_xn_def get_pt_info_def split: option.splits pte.splits)
|
||||
|
||||
lemma get_page_xn_some_get_page_info:
|
||||
"get_page_xn ahp pd_ref vptr = Some xn \<Longrightarrow>
|
||||
\<exists>base sz rights. get_page_info ahp pd_ref vptr = Some (base, sz, rights)"
|
||||
apply (simp add: get_page_xn_def get_page_info_def split: option.splits pde.splits)
|
||||
apply (drule get_pt_xn_some_get_pt_info)
|
||||
apply simp
|
||||
apply (frule requiv_get_pd_of_thread_eq, simp+)[1]
|
||||
apply (frule pd_of_thread_same_agent, simp+)[1]
|
||||
apply (subst requiv_get_page_info_eq, simp+)[1]
|
||||
done
|
||||
|
||||
lemma requiv_ptable_xn_eq:
|
||||
"\<lbrakk> reads_equiv aag s s'; pas_refined aag s; pas_refined aag s';
|
||||
is_subject aag (cur_thread s); invs s; invs s' \<rbrakk>
|
||||
\<Longrightarrow> ptable_xn_s s = ptable_xn_s s'"
|
||||
apply (simp add: ptable_xn_s_def)
|
||||
apply (rule ext)
|
||||
apply (case_tac "x \<in> kernel_mappings")
|
||||
apply (clarsimp simp: ptable_xn_def split: option.splits)
|
||||
apply (intro conjI)
|
||||
apply clarsimp
|
||||
apply (frule some_get_page_xn_kmapsD)
|
||||
apply (fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings)+
|
||||
apply clarsimp
|
||||
apply (frule some_get_page_xn_kmapsD)
|
||||
apply (fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings)+
|
||||
apply clarsimp
|
||||
apply (frule_tac xn=True in some_get_page_xn_kmapsD)
|
||||
apply (fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings)+
|
||||
|
||||
apply (case_tac "get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)
|
||||
= arm_global_pd (arch_state s)")
|
||||
apply (frule requiv_pd_of_thread_global_pd)
|
||||
apply fastforce+
|
||||
apply (clarsimp simp: ptable_xn_def split: option.splits)
|
||||
apply (intro conjI)
|
||||
apply clarsimp
|
||||
apply (drule get_page_xn_some_get_page_info)
|
||||
apply clarsimp
|
||||
apply (frule get_page_info_gpd_kmaps[rotated, rotated])
|
||||
apply (fastforce simp: invs_valid_global_objs invs_arch_state)+
|
||||
apply clarsimp
|
||||
apply (intro conjI)
|
||||
apply clarsimp
|
||||
apply (drule get_page_xn_some_get_page_info)
|
||||
apply clarsimp
|
||||
apply (frule get_page_info_gpd_kmaps[rotated, rotated])
|
||||
apply (fastforce simp: invs_valid_global_objs invs_arch_state)+
|
||||
apply clarsimp
|
||||
apply (drule get_page_xn_some_get_page_info)
|
||||
apply clarsimp
|
||||
apply (frule get_page_info_gpd_kmaps[rotated, rotated])
|
||||
apply (fastforce simp: invs_valid_global_objs invs_arch_state)+
|
||||
|
||||
apply (case_tac "get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')
|
||||
= arm_global_pd (arch_state s')")
|
||||
apply (drule reads_equiv_sym)
|
||||
apply (frule requiv_pd_of_thread_global_pd)
|
||||
apply (fastforce simp: reads_equiv_def)+
|
||||
|
||||
apply (simp add: ptable_xn_def)
|
||||
apply (frule requiv_get_pd_of_thread_eq)
|
||||
apply fastforce+
|
||||
apply (frule pd_of_thread_same_agent, simp+)
|
||||
apply (subst requiv_get_page_xn_eq, simp+)
|
||||
done
|
||||
is_subject aag (cur_thread s); invs s; invs s'; ptable_rights_s s x \<noteq> {} \<rbrakk>
|
||||
\<Longrightarrow> ptable_xn_s s x = ptable_xn_s s' x"
|
||||
by (simp add: ptable_xn_s_def requiv_ptable_attrs_eq)
|
||||
|
||||
lemma requiv_user_mem_eq:
|
||||
"\<lbrakk> reads_equiv aag s s'; globals_equiv s s'; invs s;
|
||||
|
|
@ -502,7 +422,7 @@ definition context_matches_state where
|
|||
"context_matches_state pl pr pxn um es s \<equiv>
|
||||
pl = ptable_lift_s s |` {x. pr x \<noteq> {}} \<and>
|
||||
pr = ptable_rights_s s \<and>
|
||||
pxn = ptable_xn_s s \<and>
|
||||
pxn = (\<lambda>x. pr x \<noteq> {} \<and> ptable_xn_s s x) \<and>
|
||||
um = (user_mem s \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x} \<and>
|
||||
es = exclusive_state (machine_state s)"
|
||||
|
||||
|
|
@ -569,16 +489,20 @@ lemma do_user_op_reads_respects_g:
|
|||
apply clarsimp
|
||||
apply (wp add: select_wp select_ev dmo_getExMonitor_reads_respects_g del: gets_ev
|
||||
| rule_tac P="pas_refined aag and invs" in gets_ev''' | simp)+
|
||||
apply (simp add: reads_equiv_g_def, intro context_conjI allI impI, safe)
|
||||
apply (simp add: requiv_ptable_rights_eq)
|
||||
apply (simp add: reads_equiv_g_def)
|
||||
apply (intro context_conjI allI impI, safe)
|
||||
apply (clarsimp simp: requiv_ptable_rights_eq)
|
||||
apply (rule ext)
|
||||
apply (case_tac "ptable_rights_s s x = {}", simp)
|
||||
apply (simp add: requiv_ptable_xn_eq)
|
||||
apply (subst expand_restrict_map_eq)
|
||||
apply (clarsimp simp: requiv_ptable_lift_eq)
|
||||
apply (simp add: requiv_cur_thread_eq)
|
||||
apply (clarsimp simp: requiv_cur_thread_eq)
|
||||
apply (subst expand_restrict_map_eq)
|
||||
apply (clarsimp simp: restrict_map_def requiv_user_mem_eq
|
||||
requiv_user_mem_eq[symmetric, OF reads_equiv_sym globals_equiv_sym])
|
||||
apply (simp add: context_matches_state_def comp_def)
|
||||
apply (clarsimp)
|
||||
apply (erule_tac x=st in allE)+
|
||||
apply (simp add: context_matches_state_def reads_equiv_sym globals_equiv_sym affects_equiv_sym comp_def)
|
||||
apply (simp add: globals_equiv_def)
|
||||
|
|
|
|||
|
|
@ -179,24 +179,6 @@ text {*
|
|||
(e.g. because the VTable entry is not set or a reference has been invalid),
|
||||
the function returns the global kernel mapping.
|
||||
|
||||
@{text get_page_info} takes the architecture-specific part of the kernel heap,
|
||||
a reference to the page directory, and a virtual memory address.
|
||||
It returns a triple containing
|
||||
(a) the physical address, where the associated page table starts,
|
||||
(b) the page table's size in bits, and
|
||||
(c) the access rights (a subset of @{term "{AllowRead, AllowWrite}"}).
|
||||
|
||||
NOTE: it should not be necessary to use these functions directly.
|
||||
For the user's convenience,
|
||||
the functions @{text ptable_lift} and @{text ptable_rights} are
|
||||
defined below using @{text get_page_info} and @{text get_pd_of_thread}.
|
||||
*}
|
||||
consts
|
||||
get_pd_of_thread :: "kheap \<Rightarrow> arch_state \<Rightarrow> obj_ref \<Rightarrow> obj_ref"
|
||||
get_page_info :: "(obj_ref \<rightharpoonup> arch_kernel_obj) \<Rightarrow> obj_ref \<Rightarrow>
|
||||
word32 \<rightharpoonup> (word32 \<times> nat \<times> vm_rights)"
|
||||
|
||||
text {*
|
||||
Looking up the page directory for a thread reference involves the following
|
||||
steps:
|
||||
|
||||
|
|
@ -207,7 +189,9 @@ text {*
|
|||
Note that the mapping data might become stale.
|
||||
Hence, we have to follow the mapping data through the ASID table.
|
||||
*}
|
||||
defs
|
||||
definition
|
||||
get_pd_of_thread :: "kheap \<Rightarrow> arch_state \<Rightarrow> obj_ref \<Rightarrow> obj_ref"
|
||||
where
|
||||
get_pd_of_thread_def:
|
||||
"get_pd_of_thread khp astate tcb_ref \<equiv>
|
||||
case khp tcb_ref of Some (TCB tcb) \<Rightarrow>
|
||||
|
|
@ -225,6 +209,7 @@ defs
|
|||
| _ \<Rightarrow> arm_global_pd astate)
|
||||
| _ \<Rightarrow> arm_global_pd astate"
|
||||
|
||||
|
||||
lemma VSRef_AASIDPool_in_vs_refs:
|
||||
"(VSRef (asid && mask asid_low_bits) (Some AASIDPool), r) \<in> vs_refs ko =
|
||||
(\<exists>apool. ko = ArchObj (arch_kernel_obj.ASIDPool apool) \<and>
|
||||
|
|
@ -488,17 +473,30 @@ done
|
|||
definition
|
||||
"get_pt_info ahp pt_ref vptr \<equiv>
|
||||
case get_pt_entry ahp pt_ref vptr of
|
||||
Some (ARM_Structs_A.SmallPagePTE base _ rights) \<Rightarrow> Some (base, 12, rights)
|
||||
| Some (ARM_Structs_A.LargePagePTE base _ rights) \<Rightarrow> Some (base, 16, rights)
|
||||
Some (ARM_Structs_A.SmallPagePTE base attrs rights) \<Rightarrow> Some (base, 12, attrs, rights)
|
||||
| Some (ARM_Structs_A.LargePagePTE base attrs rights) \<Rightarrow> Some (base, 16, attrs, rights)
|
||||
| _ \<Rightarrow> None"
|
||||
defs
|
||||
|
||||
text {*
|
||||
@{text get_page_info} takes the architecture-specific part of the kernel heap,
|
||||
a reference to the page directory, and a virtual memory address.
|
||||
It returns a tuple containing
|
||||
(a) the physical address, where the associated page table starts,
|
||||
(b) the page table's size in bits, and
|
||||
(c) the page attributes (cachable, XNever, etc)
|
||||
(d) the access rights (a subset of @{term "{AllowRead, AllowWrite}"}).
|
||||
*}
|
||||
definition
|
||||
get_page_info :: "(obj_ref \<rightharpoonup> arch_kernel_obj) \<Rightarrow> obj_ref \<Rightarrow>
|
||||
word32 \<rightharpoonup> (word32 \<times> nat \<times> vm_attributes \<times> vm_rights)"
|
||||
where
|
||||
get_page_info_def:
|
||||
"get_page_info ahp pd_ref vptr \<equiv>
|
||||
case get_pd_entry ahp pd_ref vptr of
|
||||
Some (ARM_Structs_A.PageTablePDE p _ _) \<Rightarrow>
|
||||
get_pt_info ahp (Platform.ptrFromPAddr p) vptr
|
||||
| Some (ARM_Structs_A.SectionPDE base _ _ rights) \<Rightarrow> Some (base, 20, rights)
|
||||
| Some (ARM_Structs_A.SuperSectionPDE base _ rights) \<Rightarrow> Some (base,24,rights)
|
||||
| Some (ARM_Structs_A.SectionPDE base attrs _ rights) \<Rightarrow> Some (base, 20, attrs, rights)
|
||||
| Some (ARM_Structs_A.SuperSectionPDE base attrs rights) \<Rightarrow> Some (base,24, attrs, rights)
|
||||
| _ \<Rightarrow> None"
|
||||
|
||||
|
||||
|
|
@ -586,15 +584,15 @@ by (clarsimp simp add: lookup_pt_slot_def lookup_pd_slot_def liftE_def bindE_def
|
|||
split: sum.splits split_if_asm kernel_object.splits arch_kernel_obj.splits
|
||||
ARM_Structs_A.pde.splits)
|
||||
|
||||
lemma
|
||||
lemma get_page_info_pte:
|
||||
"is_aligned pd_ref pd_bits \<Longrightarrow>
|
||||
lookup_pt_slot pd_ref vptr s = ({(Inr x,s)},False) \<Longrightarrow>
|
||||
is_aligned (x - ((vptr >> 12) && 0xFF << 2)) pt_bits \<Longrightarrow>
|
||||
get_pte x s = ({(pte,s)},False) \<Longrightarrow>
|
||||
get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ref vptr =
|
||||
(case pte of
|
||||
ARM_Structs_A.SmallPagePTE base _ rights \<Rightarrow> Some (base, 12, rights)
|
||||
| ARM_Structs_A.LargePagePTE base _ rights \<Rightarrow> Some (base, 16, rights)
|
||||
ARM_Structs_A.SmallPagePTE base attrs rights \<Rightarrow> Some (base, 12, attrs, rights)
|
||||
| ARM_Structs_A.LargePagePTE base attrs rights \<Rightarrow> Some (base, 16, attrs, rights)
|
||||
| _ \<Rightarrow> None)"
|
||||
apply (clarsimp simp add: get_page_info_def get_pd_entry_def
|
||||
split: option.splits)
|
||||
|
|
@ -616,12 +614,12 @@ apply (drule_tac x=x2 in get_pt_entry_Some_eq_get_pte[where s=s and vptr=vptr])
|
|||
apply (simp add: pt_bits_def pageBits_def mask_def)
|
||||
done
|
||||
|
||||
lemma
|
||||
lemma get_page_info_section:
|
||||
"is_aligned pd_ref pd_bits \<Longrightarrow>
|
||||
get_pde (lookup_pd_slot pd_ref vptr) s =
|
||||
({(ARM_Structs_A.SectionPDE base XX YY rights,s)},False) \<Longrightarrow>
|
||||
({(ARM_Structs_A.SectionPDE base attrs X rights, s)},False) \<Longrightarrow>
|
||||
get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ref vptr =
|
||||
Some (base, 20, rights)"
|
||||
Some (base, 20, attrs, rights)"
|
||||
apply (simp add: lookup_pd_slot_def get_page_info_def split: option.splits)
|
||||
apply (intro conjI impI allI)
|
||||
apply (drule get_pd_entry_None_iff_get_pde_fail[where s=s and vptr=vptr])
|
||||
|
|
@ -630,12 +628,12 @@ apply (drule_tac x=x2 in get_pd_entry_Some_eq_get_pde[where s=s and vptr=vptr])
|
|||
apply clarsimp
|
||||
done
|
||||
|
||||
lemma
|
||||
lemma get_page_info_super_section:
|
||||
"is_aligned pd_ref pd_bits \<Longrightarrow>
|
||||
get_pde (lookup_pd_slot pd_ref vptr) s =
|
||||
({(ARM_Structs_A.SuperSectionPDE base XX rights,s)},False) \<Longrightarrow>
|
||||
({(ARM_Structs_A.SuperSectionPDE base attrs rights,s)},False) \<Longrightarrow>
|
||||
get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ref vptr =
|
||||
Some (base, 24, rights)"
|
||||
Some (base, 24, attrs, rights)"
|
||||
apply (simp add: lookup_pd_slot_def get_page_info_def split: option.splits)
|
||||
apply (intro conjI impI allI)
|
||||
apply (drule get_pd_entry_None_iff_get_pde_fail[where s=s and vptr=vptr])
|
||||
|
|
@ -658,7 +656,7 @@ definition
|
|||
definition
|
||||
ptable_rights :: "obj_ref \<Rightarrow> 'z state \<Rightarrow> word32 \<Rightarrow> vm_rights" where
|
||||
"ptable_rights tcb s \<equiv> \<lambda>addr.
|
||||
case_option {} (snd o snd)
|
||||
case_option {} (snd o snd o snd)
|
||||
(get_page_info (\<lambda>obj. get_arch_obj (kheap s obj))
|
||||
(get_pd_of_thread (kheap s) (arch_state s) tcb) addr)"
|
||||
|
||||
|
|
|
|||
|
|
@ -98,11 +98,8 @@ lemma valid_global_pd_mappingsE:
|
|||
|
||||
(* NOTE: we could probably add "is_aligned b (pageBitsForSize sz)"
|
||||
if we assumed "valid_global_objs s", additionally. *)
|
||||
(* NOTE: we might be able to show "p && ~~ mask a = Platform.ptrFromPAddr b"
|
||||
with the help of valid_pde_kernel_mappings and WordLib.and_not_mask
|
||||
(though that is not trivial) *)
|
||||
lemma some_get_page_info_kmapsD:
|
||||
"\<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ref p = Some (b, a, r);
|
||||
"\<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ref p = Some (b, a, attr, r);
|
||||
p \<in> kernel_mappings; valid_global_pd_mappings s; equal_kernel_mappings s\<rbrakk>
|
||||
\<Longrightarrow> (\<exists>sz. pageBitsForSize sz = a) \<and> r = {}"
|
||||
apply (clarsimp simp: get_page_info_def get_pd_entry_def get_arch_obj_def
|
||||
|
|
@ -141,7 +138,7 @@ lemma some_get_page_info_kmapsD:
|
|||
lemma get_page_info_gpd_kmaps:
|
||||
"\<lbrakk>valid_global_objs s; valid_arch_state s;
|
||||
get_page_info (\<lambda>obj. get_arch_obj (kheap s obj))
|
||||
(arm_global_pd (arch_state s)) p = Some (b, a, r)\<rbrakk>
|
||||
(arm_global_pd (arch_state s)) p = Some (b, a, attr, r)\<rbrakk>
|
||||
\<Longrightarrow> p \<in> kernel_mappings"
|
||||
apply (clarsimp simp: valid_global_objs_def valid_arch_state_def)
|
||||
apply (thin_tac "Ball ?x ?y")
|
||||
|
|
@ -171,7 +168,7 @@ lemma is_aligned_ptrFromPAddrD:
|
|||
done
|
||||
|
||||
lemma some_get_page_info_umapsD:
|
||||
"\<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ref p = Some (b, a, r);
|
||||
"\<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ref p = Some (b, a, attr, r);
|
||||
(\<exists>\<rhd> pd_ref) s; p \<notin> kernel_mappings; valid_arch_objs s; pspace_aligned s;
|
||||
valid_asid_table (arm_asid_table (arch_state s)) s; valid_objs s\<rbrakk>
|
||||
\<Longrightarrow> (\<exists>sz. pageBitsForSize sz = a \<and> is_aligned b a \<and>
|
||||
|
|
|
|||
|
|
@ -1000,7 +1000,7 @@ lemma valid_list_post:
|
|||
\<Longrightarrow> valid_list_2 (t'(p := list_insert_after (t' p) src dest)) n"
|
||||
apply (insert valid_list dest neq)
|
||||
apply (simp add: valid_list_2_def t'_def n_def)
|
||||
apply (fastforce simp: distinct_list_insert_after list_remove_distinct list_remove_removed set_list_insert_after list_remove_removed)
|
||||
apply (fastforce simp: distinct_list_insert_after list_remove_distinct set_list_insert_after list_remove_removed)
|
||||
done
|
||||
|
||||
end
|
||||
|
|
@ -1118,7 +1118,7 @@ lemma next_not_child:
|
|||
apply(drule(1) next_not_child_NoneD)
|
||||
apply(rule next_not_child_NoneI)
|
||||
apply(simp add: next_sib' descendants_child no_mloop_descendants desc)
|
||||
apply(simp add: dest_no_parent descendants_of_def)
|
||||
apply(simp add: descendants_of_def)
|
||||
apply(simp add: next_sib')
|
||||
apply(simp add: finite_depth_insert_child)
|
||||
apply(simp add: next_slot_def split: split_if_asm)
|
||||
|
|
@ -1134,13 +1134,13 @@ lemma next_not_child:
|
|||
apply(intro allI impI conjI)
|
||||
apply(drule_tac a=src and b=q' and c=src in descendants_trans, simp)
|
||||
apply(simp)
|
||||
apply(simp add: descendants_of_def dest_no_parent)
|
||||
apply(simp add: descendants_of_def)
|
||||
apply(elim exE conjE)
|
||||
apply(rule_tac x=q in exI)
|
||||
apply(simp)
|
||||
apply(intro conjI impI notI allI)
|
||||
apply(simp add: desc)
|
||||
apply(simp add: dest_no_parent descendants_of_def)
|
||||
apply(simp add: descendants_of_def)
|
||||
apply(simp)
|
||||
apply(simp add: finite_depth_insert_child)
|
||||
apply(case_tac "next_not_child p t m")
|
||||
|
|
@ -1294,7 +1294,7 @@ lemma next_not_child_no_parent:
|
|||
else next_not_child p t m)"
|
||||
apply(simp)
|
||||
apply(intro conjI impI)
|
||||
apply(simp add: descendants_of_def dest_no_parent)
|
||||
apply(simp add: descendants_of_def)
|
||||
apply(simp add: no_mloop_def descendants_of_def)
|
||||
apply(subgoal_tac "next_not_child src t m = None")
|
||||
prefer 2
|
||||
|
|
@ -1312,7 +1312,7 @@ lemma next_not_child_no_parent:
|
|||
apply(simp)
|
||||
apply(drule(1) next_not_child_NoneD, rule next_not_child_NoneI)
|
||||
apply(simp add: descendants next_sib_no_parent)
|
||||
apply(simp add: descendants_of_def dest_no_parent)
|
||||
apply(simp add: descendants_of_def )
|
||||
apply(simp add: next_sib_no_parent)
|
||||
apply(simp add: finite_depth)
|
||||
apply(simp)
|
||||
|
|
@ -1326,7 +1326,7 @@ lemma next_not_child_no_parent:
|
|||
apply(simp)
|
||||
apply(intro allI conjI impI notI)
|
||||
apply(simp add: desc)
|
||||
apply(simp add: descendants_of_def dest_no_parent)
|
||||
apply(simp add: descendants_of_def)
|
||||
apply(simp add: finite_depth)
|
||||
apply(rule next_not_child_NoneI)
|
||||
apply(intro allI impI)
|
||||
|
|
@ -1360,7 +1360,7 @@ lemma next_not_child:
|
|||
else next_not_child p t m)"
|
||||
apply(simp)
|
||||
apply(intro conjI impI)
|
||||
apply(simp add: descendants_of_def dest_no_parent)
|
||||
apply(simp add: descendants_of_def)
|
||||
apply(simp add: no_mloop_def descendants_of_def)
|
||||
apply(erule conjE)
|
||||
apply(rule next_not_childI)
|
||||
|
|
@ -1379,7 +1379,7 @@ lemma next_not_child:
|
|||
apply(simp)
|
||||
apply(drule(1) next_not_child_NoneD, rule next_not_child_NoneI)
|
||||
apply(simp add: descendants next_sib)
|
||||
apply(simp add: descendants_of_def dest_no_parent no_mloop_def)
|
||||
apply(simp add: descendants_of_def no_mloop_def)
|
||||
apply(simp add: next_sib)
|
||||
apply(simp add: finite_depth)
|
||||
apply(simp)
|
||||
|
|
@ -1388,13 +1388,13 @@ lemma next_not_child:
|
|||
apply(simp add: next_sib descendants)
|
||||
apply(rule disjI2)
|
||||
apply(simp add: next_sib descendants no_mloop_descendants)
|
||||
apply(simp add: descendants_of_def dest_no_parent)
|
||||
apply(simp add: descendants_of_def)
|
||||
apply(elim exE conjE)
|
||||
apply(rule_tac x=q in exI)
|
||||
apply(simp)
|
||||
apply(intro conjI impI notI)
|
||||
apply(simp add: desc)
|
||||
apply(simp add: descendants_of_def dest_no_parent)
|
||||
apply(simp add: descendants_of_def)
|
||||
apply(simp add: finite_depth)
|
||||
apply(rule next_not_childI)
|
||||
apply(rule disjI1)
|
||||
|
|
@ -1442,7 +1442,7 @@ lemma next_slot_no_parent:
|
|||
apply(subgoal_tac "next_not_child dest t m = None")
|
||||
prefer 2
|
||||
apply((rule next_not_child_NoneI | intro allI impI
|
||||
| simp add: descendants_of_def dest_no_parent next_sib_def finite_depth dest)+)[1]
|
||||
| simp add: descendants_of_def next_sib_def finite_depth dest)+)[1]
|
||||
apply(subgoal_tac "next_not_child src t m = None")
|
||||
prefer 2
|
||||
apply((rule next_not_child_NoneI | intro allI impI |
|
||||
|
|
@ -1632,7 +1632,7 @@ lemma cte_at_next_slot:
|
|||
apply(subgoal_tac "next_not_child_dom (p, cdt_list s, cdt s)")
|
||||
prefer 2
|
||||
apply(simp add: next_not_child_termination valid_mdb_def valid_list_2_def)
|
||||
apply(simp add: next_not_child.psimps split: split_if_asm)
|
||||
apply(simp split: split_if_asm)
|
||||
apply(case_tac "cdt s p")
|
||||
apply(simp)
|
||||
apply(rule descendants_of_cte_at)
|
||||
|
|
@ -2403,7 +2403,7 @@ lemma (in mdb_empty_abs') valid_list_post:
|
|||
apply(rule distinct_list_replace_list)
|
||||
apply(simp)+
|
||||
apply(rule ccontr)
|
||||
apply(fastforce dest: int_not_emptyD simp: no_mdb_loop)
|
||||
apply(fastforce dest: int_not_emptyD)
|
||||
apply(simp)
|
||||
done
|
||||
|
||||
|
|
@ -2547,7 +2547,7 @@ lemma (in mdb_empty_abs') next_sib:
|
|||
apply(drule after_in_list_in_list)
|
||||
apply(simp add: valid_list_2_def)
|
||||
apply(simp)
|
||||
apply(intro conjI impI notI, simp add: no_mdb_loop)
|
||||
apply(intro conjI impI notI, simp)
|
||||
apply(subst list_replace_after_fst_list)
|
||||
apply(frule after_in_list_in_list)
|
||||
apply(simp add: valid_list_2_def)
|
||||
|
|
|
|||
Loading…
Reference in New Issue