x64: CR3 and machine op updates for Meltdown
This commit is contained in:
Matthew Brecknell
Joel Beeren
parent
a3de401c09
commit
f649240cde
|
|
@ -1828,14 +1828,14 @@ proof -
|
|||
|
||||
moreover
|
||||
{
|
||||
assume "s' \<Turnstile>\<^sub>c pml4_Ptr (symbol_table ''x64KSGlobalPML4'')"
|
||||
assume "s' \<Turnstile>\<^sub>c pml4_Ptr (symbol_table ''x64KSSKIMPML4'')"
|
||||
moreover
|
||||
from sr ptr_refs have "ptr_span (pd_Ptr (symbol_table ''x64KSGlobalPML4''))
|
||||
from sr ptr_refs have "ptr_span (pd_Ptr (symbol_table ''x64KSSKIMPML4''))
|
||||
\<inter> {ptr..ptr + 2 ^ bits - 1} = {}"
|
||||
by (fastforce simp: rf_sr_def cstate_relation_def Let_def)
|
||||
ultimately
|
||||
have "hrs_htd (hrs_htd_update (typ_region_bytes ptr bits) (t_hrs_' (globals s')))
|
||||
\<Turnstile>\<^sub>t pml4_Ptr (symbol_table ''x64KSGlobalPML4'')"
|
||||
\<Turnstile>\<^sub>t pml4_Ptr (symbol_table ''x64KSSKIMPML4'')"
|
||||
using al wb
|
||||
apply (cases "t_hrs_' (globals s')")
|
||||
apply (simp add: hrs_htd_update_def hrs_htd_def h_t_valid_typ_region_bytes upto_intvl_eq)
|
||||
|
|
|
|||
|
|
@ -728,21 +728,21 @@ lemma liftM_getObject_return_tcb:
|
|||
"ko_at' v p s \<Longrightarrow> liftM f (getObject p) s = return (f (v::tcb)) s"
|
||||
by (simp add: liftM_def bind_def getObject_return_tcb return_def objBits_defs)
|
||||
|
||||
lemma getCurrentCR3_isolatable:
|
||||
"thread_actions_isolatable idx (getCurrentCR3)"
|
||||
by (clarsimp simp: getCurrentCR3_def gets_isolatable)
|
||||
lemma getCurrentUserCR3_isolatable:
|
||||
"thread_actions_isolatable idx (getCurrentUserCR3)"
|
||||
by (clarsimp simp: getCurrentUserCR3_def gets_isolatable)
|
||||
|
||||
lemma setCurrentCR3_isolatable:
|
||||
"thread_actions_isolatable idx (setCurrentCR3 f)"
|
||||
apply (clarsimp simp: setCurrentCR3_def)
|
||||
lemma setCurrentUserCR3_isolatable:
|
||||
"thread_actions_isolatable idx (setCurrentUserCR3 f)"
|
||||
apply (clarsimp simp: setCurrentUserCR3_def)
|
||||
apply (intro modify_isolatable doMachineOp_isolatable
|
||||
thread_actions_isolatable_bind[OF _ _ hoare_pre(1)])
|
||||
apply wpsimp+
|
||||
done
|
||||
|
||||
lemma setCurrentVSpaceRoot_isolatable:
|
||||
"thread_actions_isolatable idx (setCurrentVSpaceRoot a f)"
|
||||
by (clarsimp simp: setCurrentVSpaceRoot_def setCurrentCR3_isolatable)
|
||||
lemma setCurrentUserVSpaceRoot_isolatable:
|
||||
"thread_actions_isolatable idx (setCurrentUserVSpaceRoot a f)"
|
||||
by (clarsimp simp: setCurrentUserVSpaceRoot_def setCurrentUserCR3_isolatable)
|
||||
|
||||
lemma setVMRoot_isolatable:
|
||||
"thread_actions_isolatable idx (setVMRoot t)"
|
||||
|
|
@ -757,9 +757,9 @@ lemma setVMRoot_isolatable:
|
|||
thread_actions_isolatable_catch[OF _ _ hoare_pre(1)]
|
||||
thread_actions_isolatable_if thread_actions_isolatable_returns
|
||||
thread_actions_isolatable_fail
|
||||
getCurrentCR3_isolatable setCurrentCR3_isolatable
|
||||
getCurrentUserCR3_isolatable setCurrentUserCR3_isolatable
|
||||
gets_isolatable getCTE_isolatable
|
||||
setCurrentVSpaceRoot_isolatable
|
||||
setCurrentUserVSpaceRoot_isolatable
|
||||
findVSpaceForASID_isolatable doMachineOp_isolatable
|
||||
| simp add: projectKO_opt_asidpool
|
||||
| wp getASID_wp typ_at_lifts)+
|
||||
|
|
@ -979,13 +979,13 @@ lemma oblivious_modifyArchState_schact[simp]:
|
|||
lemma oblivious_setVMRoot_schact:
|
||||
"oblivious (ksSchedulerAction_update f) (setVMRoot t)"
|
||||
apply (simp add: setVMRoot_def getThreadVSpaceRoot_def locateSlot_conv
|
||||
getSlotCap_def getCTE_def )
|
||||
getSlotCap_def getCTE_def)
|
||||
by (safe intro!: oblivious_bind oblivious_bindE oblivious_catch oblivious_mapM_x
|
||||
| simp_all add: liftE_def
|
||||
findVSpaceForASID_def liftME_def
|
||||
findVSpaceForASIDAssert_def checkPML4At_def
|
||||
getCurrentCR3_def setCurrentCR3_def
|
||||
invalidateASID_def setCurrentVSpaceRoot_def
|
||||
getCurrentUserCR3_def setCurrentUserCR3_def
|
||||
invalidateASID_def setCurrentUserVSpaceRoot_def
|
||||
split: if_split capability.split arch_capability.split option.split)+
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -62,6 +62,10 @@ assumes invalidateTranslationSingleASID_ccorres:
|
|||
(doMachineOp (invalidateTranslationSingleASID vptr asid))
|
||||
(Call invalidateTranslationSingleASID_'proc)"
|
||||
|
||||
assumes invalidateASID_ccorres:
|
||||
"ccorres dc xfdc \<top> (UNIV \<inter> \<lbrace>\<acute>vspace = pml4e_Ptr vspace\<rbrace> \<inter> \<lbrace>\<acute>asid = asid\<rbrace>) []
|
||||
(doMachineOp (invalidateASID vspace asid)) (Call invalidateASID_'proc)"
|
||||
|
||||
(* The following are fastpath specific assumptions.
|
||||
We might want to move them somewhere else. *)
|
||||
|
||||
|
|
|
|||
|
|
@ -2195,7 +2195,7 @@ proof (intro impI allI)
|
|||
|
||||
moreover
|
||||
from rf szb al
|
||||
have "ptr_span (pml4_Ptr (symbol_table ''x64KSGlobalPML4'')) \<inter> {ptr ..+ 2 ^ ptBits} = {}"
|
||||
have "ptr_span (pml4_Ptr (symbol_table ''x64KSSKIMPML4'')) \<inter> {ptr ..+ 2 ^ ptBits} = {}"
|
||||
apply (clarsimp simp: valid_global_refs'_def Let_def
|
||||
valid_refs'_def ran_def rf_sr_def cstate_relation_def)
|
||||
apply (erule disjoint_subset)
|
||||
|
|
@ -2375,7 +2375,7 @@ proof (intro impI allI)
|
|||
|
||||
moreover
|
||||
from rf szb al
|
||||
have "ptr_span (pml4_Ptr (symbol_table ''x64KSGlobalPML4'')) \<inter> {ptr ..+ 2 ^ pdBits} = {}"
|
||||
have "ptr_span (pml4_Ptr (symbol_table ''x64KSSKIMPML4'')) \<inter> {ptr ..+ 2 ^ pdBits} = {}"
|
||||
apply (clarsimp simp: valid_global_refs'_def Let_def
|
||||
valid_refs'_def ran_def rf_sr_def cstate_relation_def)
|
||||
apply (erule disjoint_subset)
|
||||
|
|
@ -2555,7 +2555,7 @@ proof (intro impI allI)
|
|||
|
||||
moreover
|
||||
from rf szb al
|
||||
have "ptr_span (pml4_Ptr (symbol_table ''x64KSGlobalPML4'')) \<inter> {ptr ..+ 2 ^ pdptBits} = {}"
|
||||
have "ptr_span (pml4_Ptr (symbol_table ''x64KSSKIMPML4'')) \<inter> {ptr ..+ 2 ^ pdptBits} = {}"
|
||||
apply (clarsimp simp: valid_global_refs'_def Let_def
|
||||
valid_refs'_def ran_def rf_sr_def cstate_relation_def)
|
||||
apply (erule disjoint_subset)
|
||||
|
|
@ -2735,7 +2735,7 @@ proof (intro impI allI)
|
|||
|
||||
moreover
|
||||
from rf szb al
|
||||
have "ptr_span (pml4_Ptr (symbol_table ''x64KSGlobalPML4'')) \<inter> {ptr ..+ 2 ^ pml4Bits} = {}"
|
||||
have "ptr_span (pml4_Ptr (symbol_table ''x64KSSKIMPML4'')) \<inter> {ptr ..+ 2 ^ pml4Bits} = {}"
|
||||
apply (clarsimp simp: valid_global_refs'_def Let_def
|
||||
valid_refs'_def ran_def rf_sr_def cstate_relation_def)
|
||||
apply (erule disjoint_subset)
|
||||
|
|
@ -7265,7 +7265,7 @@ lemma ccorres_typ_region_bytes_dummy:
|
|||
apply (frule typ_bytes_cpspace_relation_clift_devicedata)
|
||||
apply (simp add: invs_pspace_aligned')+
|
||||
apply (frule typ_bytes_cpspace_relation_clift_gptr[where
|
||||
ptr'="pml4_Ptr (symbol_table ''x64KSGlobalPML4'')"])
|
||||
ptr'="pml4_Ptr (symbol_table ''x64KSSKIMPML4'')"])
|
||||
apply (simp add: invs_pspace_aligned')+
|
||||
apply (frule typ_bytes_cpspace_relation_clift_gptr[where
|
||||
ptr'="ptr_coerce x :: (cte_C[256]) ptr" for x])
|
||||
|
|
|
|||
|
|
@ -1149,7 +1149,7 @@ lemma cstate_relation_only_t_hrs:
|
|||
intStateIRQNode_' s = intStateIRQNode_' t;
|
||||
intStateIRQTable_' s = intStateIRQTable_' t;
|
||||
x86KSASIDTable_' s = x86KSASIDTable_' t;
|
||||
x64KSCurrentCR3_' s = x64KSCurrentCR3_' t;
|
||||
x64KSCurrentUserCR3_' s = x64KSCurrentUserCR3_' t;
|
||||
phantom_machine_state_' s = phantom_machine_state_' t;
|
||||
ghost'state_' s = ghost'state_' t;
|
||||
ksDomScheduleIdx_' s = ksDomScheduleIdx_' t;
|
||||
|
|
@ -1173,7 +1173,7 @@ lemma rf_sr_upd:
|
|||
"intStateIRQNode_'(globals x) = intStateIRQNode_' (globals y)"
|
||||
"intStateIRQTable_'(globals x) = intStateIRQTable_' (globals y)"
|
||||
"x86KSASIDTable_' (globals x) = x86KSASIDTable_' (globals y)"
|
||||
"x64KSCurrentCR3_' (globals x) = x64KSCurrentCR3_' (globals y)"
|
||||
"x64KSCurrentUserCR3_' (globals x) = x64KSCurrentUserCR3_' (globals y)"
|
||||
"phantom_machine_state_' (globals x) = phantom_machine_state_' (globals y)"
|
||||
"ghost'state_' (globals x) = ghost'state_' (globals y)"
|
||||
"ksDomScheduleIdx_' (globals x) = ksDomScheduleIdx_' (globals y)"
|
||||
|
|
@ -1198,7 +1198,7 @@ lemma rf_sr_upd_safe[simp]:
|
|||
and dt: "ksDomainTime_' (globals (g y)) = ksDomainTime_' (globals y)"
|
||||
and arch:
|
||||
"x86KSASIDTable_' (globals (g y)) = x86KSASIDTable_' (globals y)"
|
||||
"x64KSCurrentCR3_' (globals (g y)) = x64KSCurrentCR3_' (globals y)"
|
||||
"x64KSCurrentUserCR3_' (globals (g y)) = x64KSCurrentUserCR3_' (globals y)"
|
||||
"phantom_machine_state_' (globals (g y)) = phantom_machine_state_' (globals y)"
|
||||
and gs: "ghost'state_' (globals (g y)) = ghost'state_' (globals y)"
|
||||
and wu: "(ksWorkUnitsCompleted_' (globals (g y))) = (ksWorkUnitsCompleted_' (globals y))"
|
||||
|
|
@ -2266,10 +2266,8 @@ lemma cap_lift_Some_CapD:
|
|||
"\<And>c'. cap_lift c = Some (Cap_io_port_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_io_port_cap"
|
||||
by (auto simp: cap_lifts cap_lift_defs)
|
||||
|
||||
lemma rf_sr_x64KSGlobalPML4:
|
||||
"(s, s') \<in> rf_sr
|
||||
\<Longrightarrow> x64KSGlobalPML4 (ksArchState s)
|
||||
= symbol_table ''x64KSGlobalPML4''"
|
||||
lemma rf_sr_x64KSSKIMPML4:
|
||||
"(s, s') \<in> rf_sr \<Longrightarrow> x64KSSKIMPML4 (ksArchState s) = symbol_table ''x64KSSKIMPML4''"
|
||||
by (clarsimp simp: rf_sr_def cstate_relation_def Let_def carch_state_relation_def carch_globals_def)
|
||||
|
||||
lemma ghost_assertion_size_logic':
|
||||
|
|
|
|||
|
|
@ -21,9 +21,18 @@ crunch ksCurDomain[wp]: switchToIdleThread "\<lambda>s. P (ksCurDomain s)"
|
|||
crunch valid_pspace'[wp]: switchToIdleThread, switchToThread valid_pspace'
|
||||
(simp: whenE_def ignore: getObject)
|
||||
|
||||
lemma valid_arch_state'_currentCR3_inv[simp]: "valid_arch_state' s \<Longrightarrow>
|
||||
valid_arch_state' (s\<lparr>ksArchState := x64KSCurrentCR3_update (\<lambda>_. param_a) (ksArchState s)\<rparr>)"
|
||||
by (clarsimp simp: valid_arch_state'_def)
|
||||
lemma setCurrentUserCR3_valid_arch_state'[wp]:
|
||||
"\<lbrace>valid_arch_state' and K (valid_cr3' c)\<rbrace> setCurrentUserCR3 c \<lbrace>\<lambda>_. valid_arch_state'\<rbrace>"
|
||||
by (wpsimp simp: setCurrentUserCR3_def valid_arch_state'_def)
|
||||
|
||||
lemma setVMRoot_valid_arch_state':
|
||||
"\<lbrace>valid_arch_state'\<rbrace> setVMRoot t \<lbrace>\<lambda>_. valid_arch_state'\<rbrace>"
|
||||
apply (simp add: setVMRoot_def getThreadVSpaceRoot_def setCurrentUserVSpaceRoot_def)
|
||||
apply (wp hoare_whenE_wp getCurrentUserCR3_wp findVSpaceForASID_vs_at_wp
|
||||
| wpcw
|
||||
| clarsimp simp: if_apply_def2 asid_wf_0
|
||||
| strengthen valid_cr3'_makeCR3)+
|
||||
done
|
||||
|
||||
crunch valid_arch_state'[wp]: switchToThread valid_arch_state'
|
||||
(wp: crunch_wps simp: crunch_simps)
|
||||
|
|
|
|||
|
|
@ -95,7 +95,7 @@ begin
|
|||
(* relates fixed adresses *)
|
||||
definition
|
||||
"carch_globals s \<equiv>
|
||||
(x64KSGlobalPML4 s = symbol_table ''x64KSGlobalPML4'')"
|
||||
(x64KSSKIMPML4 s = symbol_table ''x64KSSKIMPML4'')"
|
||||
|
||||
(* FIXME x64: DON'T DELETE!
|
||||
keep this for a rainy day, if we find out that leaving the asid map out of the state relation
|
||||
|
|
@ -108,13 +108,17 @@ where
|
|||
Some asidpoolptr \<Rightarrow> case (ksPSpace s) asidpoolptr of None \<Rightarrow> None |
|
||||
Some (KOArch (KOASIDPool (ASIDPool pool))) \<Rightarrow> pool (asid && mask asidLowBits)"
|
||||
|
||||
(* The C kernel stores and performs operations on the current CR3 as a word.
|
||||
This means that we need to reason about bits which the bitfield generator ignores.
|
||||
We therefore encode an invariant about those extra bits here. *)
|
||||
definition
|
||||
ccr3_relation :: "X64_H.cr3 \<Rightarrow> cr3_C \<Rightarrow> bool"
|
||||
ccr3_relation :: "X64_H.cr3 \<Rightarrow> machine_word \<Rightarrow> bool"
|
||||
where
|
||||
"ccr3_relation c ccr3 \<equiv>
|
||||
let ccr3' = cr3_lift ccr3 in
|
||||
case c of
|
||||
CR3 pad as \<Rightarrow> pad = (pml4_base_address_CL ccr3') \<and> as = (pcid_CL ccr3')"
|
||||
"ccr3_relation hcr3 ccr3 \<equiv>
|
||||
case hcr3 of
|
||||
CR3 addr pcid \<Rightarrow> addr = ccr3 && (mask 39 << 12)
|
||||
\<and> pcid = ccr3 && mask 12
|
||||
\<and> 1 << 63 = ccr3 && (~~ mask 51)"
|
||||
|
||||
definition
|
||||
carch_state_relation :: "Arch.kernel_state \<Rightarrow> globals \<Rightarrow> bool"
|
||||
|
|
@ -122,14 +126,7 @@ where
|
|||
"carch_state_relation astate cstate \<equiv>
|
||||
x64KSKernelVSpace astate = x64KSKernelVSpace_C \<and>
|
||||
array_relation (op = \<circ> option_to_ptr) (2^asid_high_bits - 1) (x64KSASIDTable astate) (x86KSASIDTable_' cstate) \<and>
|
||||
(*
|
||||
Changes to the C kernel to mitigate Meltdown have removed x64KSCurrentCR3.
|
||||
We temporarily remove it from the C state relation to keep existing proofs working.
|
||||
But for x64 verification, this ultimately needs to be replaced with a relation on
|
||||
the new state that has been added, and the specs updated accordingly.
|
||||
|
||||
ccr3_relation (x64KSCurrentCR3 astate) (x64KSCurrentCR3_' cstate) \<and>
|
||||
*)
|
||||
ccr3_relation (x64KSCurrentUserCR3 astate) (x64KSCurrentUserCR3_' cstate) \<and>
|
||||
(* FIXME x64: Still needed: relation for IOPort bitmap *)
|
||||
carch_globals astate"
|
||||
|
||||
|
|
@ -882,9 +879,8 @@ where
|
|||
h_t_valid (hrs_htd (t_hrs_' cstate)) c_guard
|
||||
(ptr_coerce (intStateIRQNode_' cstate) :: (cte_C[256]) ptr) \<and>
|
||||
{ptr_val (intStateIRQNode_' cstate) ..+ 2 ^ (8 + cte_level_bits)} \<subseteq> kernel_data_refs \<and>
|
||||
h_t_valid (hrs_htd (t_hrs_' cstate)) c_guard
|
||||
(pml4_Ptr (symbol_table ''x64KSGlobalPML4'')) \<and>
|
||||
ptr_span (pml4_Ptr (symbol_table ''x64KSGlobalPML4'')) \<subseteq> kernel_data_refs \<and>
|
||||
h_t_valid (hrs_htd (t_hrs_' cstate)) c_guard (pml4_Ptr (symbol_table ''x64KSSKIMPML4'')) \<and>
|
||||
ptr_span (pml4_Ptr (symbol_table ''x64KSSKIMPML4'')) \<subseteq> kernel_data_refs \<and>
|
||||
htd_safe domain (hrs_htd (t_hrs_' cstate)) \<and>
|
||||
kernel_data_refs = (- domain) \<and>
|
||||
globals_list_distinct (- kernel_data_refs) symbol_table globals_list \<and>
|
||||
|
|
|
|||
|
|
@ -931,16 +931,15 @@ lemma findVSpaceForASID_ccorres:
|
|||
asid_map_asid_map_none_def asid_map_asid_map_vspace_def
|
||||
asid_map_asid_map_vspace_lift_def
|
||||
split: if_splits)
|
||||
apply simp+
|
||||
apply (simp add: mask_2pm1)+
|
||||
done
|
||||
|
||||
(* FIXME x64: there is no USGlobalPML4 in x64, do we need this?
|
||||
lemma ccorres_pre_gets_armUSGlobalPD_ksArchState:
|
||||
lemma ccorres_pre_gets_x64KSSKIMPML4_ksArchState:
|
||||
assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c"
|
||||
shows "ccorres r xf
|
||||
(\<lambda>s. (\<forall>rv. armUSGlobalPD (ksArchState s) = rv \<longrightarrow> P rv s))
|
||||
(P' (ptr_val ((Ptr ::(32 word \<Rightarrow> (pde_C[2048]) ptr)) (symbol_table ''armUSGlobalPD''))))
|
||||
hs (gets (armUSGlobalPD \<circ> ksArchState) >>= (\<lambda>rv. f rv)) c"
|
||||
(\<lambda>s. (\<forall>rv. x64KSSKIMPML4 (ksArchState s) = rv \<longrightarrow> P rv s))
|
||||
(P' (ptr_val (pml4_Ptr (symbol_table ''x64KSSKIMPML4''))))
|
||||
hs (gets (x64KSSKIMPML4 \<circ> ksArchState) >>= (\<lambda>rv. f rv)) c"
|
||||
apply (rule ccorres_guard_imp)
|
||||
apply (rule ccorres_symb_exec_l)
|
||||
defer
|
||||
|
|
@ -954,9 +953,9 @@ lemma ccorres_pre_gets_armUSGlobalPD_ksArchState:
|
|||
apply (rule cc)
|
||||
apply clarsimp
|
||||
apply assumption
|
||||
apply (drule rf_sr_armUSGlobalPD)
|
||||
apply (drule rf_sr_x64KSSKIMPML4)
|
||||
apply simp
|
||||
done *)
|
||||
done
|
||||
|
||||
(* FIXME move *)
|
||||
lemma ccorres_from_vcg_might_throw:
|
||||
|
|
@ -994,27 +993,24 @@ end
|
|||
|
||||
context kernel_m begin
|
||||
|
||||
|
||||
(* FIXME: move *)
|
||||
(* FIXME x64: needed?
|
||||
lemma ccorres_h_t_valid_armUSGlobalPD:
|
||||
lemma ccorres_h_t_valid_x64KSSKIMPML4:
|
||||
"ccorres r xf P P' hs f (f' ;; g') \<Longrightarrow>
|
||||
ccorres r xf P P' hs f
|
||||
(Guard C_Guard {s'. s' \<Turnstile>\<^sub>c (Ptr::(32 word \<Rightarrow> (pde_C[2048]) ptr)) (symbol_table ''armUSGlobalPD'')} f';;
|
||||
g')"
|
||||
(Guard C_Guard {s'. s' \<Turnstile>\<^sub>c pml4_Ptr (symbol_table ''x64KSSKIMPML4'')} f';; g')"
|
||||
apply (rule ccorres_guard_imp2)
|
||||
apply (rule ccorres_move_c_guards[where P = \<top>])
|
||||
apply clarsimp
|
||||
apply assumption
|
||||
apply simp
|
||||
by (simp add:rf_sr_def cstate_relation_def Let_def) *)
|
||||
by (clarsimp simp add: rf_sr_def cstate_relation_def Let_def)
|
||||
|
||||
lemma ccorres_pre_gets_x64KSCurrentCR3_ksArchState:
|
||||
lemma ccorres_pre_gets_x64KSCurrentUserCR3_ksArchState:
|
||||
assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c"
|
||||
shows "ccorres r xf
|
||||
(\<lambda>s. (\<forall>rv. x64KSCurrentCR3 (ksArchState s) = rv \<longrightarrow> P rv s))
|
||||
(\<lambda>s. (\<forall>rv. x64KSCurrentUserCR3 (ksArchState s) = rv \<longrightarrow> P rv s))
|
||||
{s. \<forall>rv. s \<in> P' rv }
|
||||
hs (gets (x64KSCurrentCR3 \<circ> ksArchState) >>= (\<lambda>rv. f rv)) c"
|
||||
hs (gets (x64KSCurrentUserCR3 \<circ> ksArchState) >>= (\<lambda>rv. f rv)) c"
|
||||
apply (rule ccorres_guard_imp)
|
||||
apply (rule ccorres_symb_exec_l)
|
||||
defer
|
||||
|
|
@ -1093,149 +1089,232 @@ lemma ccorres_name_pre_C:
|
|||
apply simp
|
||||
done
|
||||
|
||||
lemma kpptr_to_paddr_spec:
|
||||
"\<forall>s. \<Gamma> \<turnstile> {s}
|
||||
Call kpptr_to_paddr_'proc
|
||||
\<lbrace> \<acute>ret__unsigned_long = X64_H.addrFromKPPtr (ptr_val (pptr_' s)) \<rbrace>"
|
||||
apply vcg
|
||||
apply (simp add: X64_H.addrFromKPPtr_def X64.addrFromKPPtr_def X64.kpptrBase_def)
|
||||
done
|
||||
|
||||
(* A version of ccr3_relation in which the most significant bit is cleared.
|
||||
This reflects the behaviour of getCurrentUserCR3, which clears that bit. *)
|
||||
definition
|
||||
ccr3_relation'' :: "machine_word \<Rightarrow> machine_word \<Rightarrow> cr3_C \<Rightarrow> bool"
|
||||
where
|
||||
"ccr3_relation'' addr pcid ccr3 \<equiv>
|
||||
let ccr3' = cr3_C.words_C ccr3.[0] in
|
||||
addr = ccr3' && (mask 39 << 12)
|
||||
\<and> pcid = ccr3' && mask 12
|
||||
\<and> ccr3' && (~~ mask 51) = 0"
|
||||
|
||||
definition
|
||||
ccr3_relation' :: "X64_H.cr3 \<Rightarrow> cr3_C \<Rightarrow> bool"
|
||||
where
|
||||
"ccr3_relation' hcr3 \<equiv> case hcr3 of CR3 addr pcid \<Rightarrow> ccr3_relation'' addr pcid"
|
||||
|
||||
lemmas ccr3_relation_defs =
|
||||
ccr3_relation_def ccr3_relation'_def ccr3_relation''_def
|
||||
|
||||
(* The C kernel performs some operations on CR3s as words rather than bitfields.
|
||||
When we need to reason about the bits that the bitfield-generated specs ignore,
|
||||
we'll use the following stronger specs for cr3_new and makeCR3. *)
|
||||
lemma cr3_new_spec':
|
||||
"\<forall>s. \<Gamma> \<turnstile> {s} Call cr3_new_'proc
|
||||
{t. globals t = globals s \<and> ccr3_relation''
|
||||
(pml4_base_address_' s && (mask 39 << 12))
|
||||
(pcid_' s && mask 12)
|
||||
(ret__struct_cr3_C_' t) }"
|
||||
apply (hoare_rule HoarePartial.ProcNoRec1)
|
||||
apply (rule allI, rule conseqPre, vcg)
|
||||
apply (clarsimp simp: mask_def ccr3_relation''_def Let_def word_ao_dist word_bw_assocs)
|
||||
done
|
||||
|
||||
lemma makeCR3_spec:
|
||||
"\<forall>s. \<Gamma> \<turnstile> {s} Call makeCR3_'proc
|
||||
{t. globals t = globals s \<and> ccr3_relation''
|
||||
(addr_' s && (mask 39 << 12))
|
||||
(pcid___unsigned_long_' s && mask 12)
|
||||
(ret__struct_cr3_C_' t) }"
|
||||
apply (rule allI, rule conseqPre, vcg exspec=cr3_new_spec')
|
||||
apply clarsimp
|
||||
done
|
||||
|
||||
lemma getCurrentUserCR3_ccorres:
|
||||
"ccorres ccr3_relation' ret__struct_cr3_C_' \<top> UNIV hs
|
||||
getCurrentUserCR3 (Call getCurrentUserCR3_'proc)"
|
||||
apply (rule ccorres_from_vcg, rule allI, rule conseqPre, vcg)
|
||||
apply (clarsimp simp: gets_def get_def return_def bind_def getCurrentUserCR3_def)
|
||||
apply (clarsimp simp: ccr3_relation_defs Let_def cr3_lift_def
|
||||
rf_sr_def cstate_relation_def carch_state_relation_def
|
||||
split: X64_H.cr3.splits)
|
||||
apply (drule_tac x="x64KSCurrentUserCR3_' (globals x) && ~~ mask 51"
|
||||
and f="\<lambda>x. x && mask 63" in arg_cong)
|
||||
apply (simp add: mask_def word_bw_assocs word_ao_dist)
|
||||
done
|
||||
|
||||
lemma setCurrentUserCR3_ccorres:
|
||||
"ccorres dc xfdc
|
||||
\<top> (UNIV \<inter> \<lbrace>ccr3_relation'' addr asid \<acute>cr3\<rbrace>)
|
||||
hs
|
||||
(setCurrentUserCR3 (CR3 addr asid))
|
||||
(Call setCurrentUserCR3_'proc)"
|
||||
(is "ccorres _ _ _ (UNIV \<inter> ?P') _ _ _")
|
||||
apply cinit
|
||||
apply (rule ccorres_from_vcg[where P=\<top> and P'="?P'"])
|
||||
apply (rule allI, rule conseqPre, vcg)
|
||||
apply (clarsimp simp: modify_def bind_def get_def put_def)
|
||||
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def)
|
||||
apply (clarsimp simp: carch_state_relation_def carch_globals_def cmachine_state_relation_def)
|
||||
apply (clarsimp simp: ccr3_relation_defs Let_def word_ao_dist mask_def)
|
||||
apply simp
|
||||
done
|
||||
|
||||
lemma setCurrentUserVSpaceRoot_ccorres:
|
||||
"ccorres dc xfdc (K (asid_wf asid)) (UNIV \<inter> \<lbrace>\<acute>addr = addr\<rbrace> \<inter> \<lbrace>\<acute>pcid___unsigned_long = asid\<rbrace>) hs
|
||||
(setCurrentUserVSpaceRoot addr asid)
|
||||
(Call setCurrentUserVSpaceRoot_'proc)"
|
||||
apply cinit
|
||||
apply (simp add: makeCR3_def)
|
||||
apply (rule ccorres_symb_exec_r)
|
||||
apply (ctac add: setCurrentUserCR3_ccorres)
|
||||
apply vcg
|
||||
apply (rule conseqPre, vcg)
|
||||
apply clarsimp
|
||||
apply (simp add: asid_wf_def, drule less_mask_eq)
|
||||
apply (clarsimp simp: ccr3_relation_defs Let_def mask_def bit_simps asid_bits_def)
|
||||
done
|
||||
|
||||
(* FIXME: move *)
|
||||
lemma invs_cicd_valid_objs' [elim!]:
|
||||
"all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> valid_objs' s"
|
||||
by (simp add: all_invs_but_ct_idle_or_in_cur_domain'_def valid_pspace'_def)
|
||||
|
||||
lemma setVMRoot_ccorres:
|
||||
"ccorres dc xfdc
|
||||
(all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' thread)
|
||||
(UNIV \<inter> {s. tcb_' s = tcb_ptr_to_ctcb_ptr thread}) []
|
||||
(setVMRoot thread) (Call setVMRoot_'proc)"
|
||||
(UNIV \<inter> {s. tcb_' s = tcb_ptr_to_ctcb_ptr thread}) hs
|
||||
(setVMRoot thread) (Call setVMRoot_'proc)"
|
||||
supply Collect_const[simp del]
|
||||
apply (cinit lift: tcb_')
|
||||
sorry (* FIXME x64: waiting for bit size changes, and subsequent changes to Ctac_lemmas_C
|
||||
apply (rule ccorres_move_array_assertion_tcb_ctes)
|
||||
apply (rule ccorres_move_c_guard_tcb_ctes)
|
||||
apply (simp add: getThreadVSpaceRoot_def locateSlot_conv)
|
||||
apply (ctac)
|
||||
apply (simp add: getThreadVSpaceRoot_def locateSlot_conv cap_case_isPML4Cap
|
||||
makeCR3_def bit_simps asid_bits_def)
|
||||
apply (ctac, rename_tac vRootCap vRootCap')
|
||||
apply (csymbr, rename_tac vRootTag)
|
||||
apply csymbr
|
||||
apply csymbr
|
||||
apply (simp add: if_1_0_0 cap_get_tag_isCap_ArchObject2 del: Collect_const)
|
||||
apply (simp add: cap_get_tag_isCap_ArchObject2)
|
||||
apply (rule ccorres_Cond_rhs_Seq)
|
||||
apply (simp add: cap_case_isPageDirectoryCap cong: if_cong)
|
||||
apply (rule ccorres_cond_true_seq)
|
||||
apply (rule ccorres_rhs_assoc)
|
||||
apply (simp add: throwError_def catch_def dc_def[symmetric])
|
||||
apply (rule ccorres_rhs_assoc)+
|
||||
apply (rule ccorres_h_t_valid_armUSGlobalPD)
|
||||
apply (rule ccorres_cond_true_seq, ccorres_rewrite)
|
||||
apply (rule ccorres_rhs_assoc)
|
||||
apply (rule ccorres_h_t_valid_x64KSSKIMPML4)
|
||||
apply csymbr
|
||||
apply (rule ccorres_pre_gets_armUSGlobalPD_ksArchState[unfolded comp_def])
|
||||
apply (rule ccorres_pre_gets_x64KSSKIMPML4_ksArchState[unfolded comp_def])
|
||||
apply (rule ccorres_add_return2)
|
||||
apply (ctac (no_vcg) add: setCurrentPD_ccorres)
|
||||
apply (rule ccorres_split_throws)
|
||||
apply (rule ccorres_return_void_C)
|
||||
apply vcg
|
||||
apply wp
|
||||
apply (rule ccorres_rhs_assoc)+
|
||||
apply (ctac (no_vcg) add: setCurrentUserVSpaceRoot_ccorres)
|
||||
apply (rule ccorres_return_void_C)
|
||||
apply (rule hoare_post_taut[where P=\<top>])
|
||||
apply (rule ccorres_rhs_assoc)
|
||||
apply (csymbr, rename_tac is_mapped)
|
||||
apply csymbr
|
||||
apply csymbr
|
||||
apply (rule_tac P="to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift threadRoot))
|
||||
= (capPDMappedASID (capCap rv) \<noteq> None)"
|
||||
in ccorres_gen_asm2)
|
||||
apply (simp add: if_1_0_0 to_bool_def del: Collect_const)
|
||||
apply (rule_tac P="to_bool (capPML4IsMapped_CL (cap_pml4_cap_lift vRootCap'))
|
||||
= (capPML4MappedASID (capCap vRootCap) \<noteq> None)"
|
||||
in ccorres_gen_asm2)
|
||||
apply (clarsimp simp: to_bool_def dc_def[symmetric])
|
||||
apply (rule ccorres_Cond_rhs_Seq)
|
||||
apply (simp add: cap_case_isPageDirectoryCap cong: if_cong)
|
||||
apply (simp add: throwError_def catch_def)
|
||||
apply (rule ccorres_rhs_assoc)+
|
||||
apply (rule ccorres_h_t_valid_armUSGlobalPD)
|
||||
apply (simp add: throwError_def catch_def dc_def[symmetric], ccorres_rewrite)
|
||||
apply (rule ccorres_rhs_assoc)
|
||||
apply (rule ccorres_h_t_valid_x64KSSKIMPML4)
|
||||
apply csymbr
|
||||
apply (rule ccorres_pre_gets_armUSGlobalPD_ksArchState[unfolded comp_def])
|
||||
apply (rule ccorres_pre_gets_x64KSSKIMPML4_ksArchState[unfolded comp_def])
|
||||
apply (rule ccorres_add_return2)
|
||||
apply (ctac (no_vcg) add: setCurrentPD_ccorres)
|
||||
apply (rule ccorres_split_throws)
|
||||
apply (rule ccorres_return_void_C [unfolded dc_def])
|
||||
apply vcg
|
||||
apply wp
|
||||
apply (simp add: cap_case_isPageDirectoryCap)
|
||||
apply (simp add: catch_def)
|
||||
apply csymbr
|
||||
apply csymbr
|
||||
apply csymbr
|
||||
apply (simp add: liftE_bindE)
|
||||
apply (simp add: bindE_bind_linearise bind_assoc liftE_def)
|
||||
apply (rule_tac f'=lookup_failure_rel and r'="\<lambda>pdeptrc pdeptr. pdeptr = pde_Ptr pdeptrc"
|
||||
apply (ctac (no_vcg) add: setCurrentUserVSpaceRoot_ccorres)
|
||||
apply (rule ccorres_return_void_C)
|
||||
apply (rule hoare_post_taut[where P=\<top>])
|
||||
apply (simp add: catch_def bindE_bind_linearise bind_assoc liftE_def)
|
||||
apply (csymbr, rename_tac pml4_ptr, csymbr)
|
||||
apply (csymbr, rename_tac asid', csymbr)
|
||||
apply (rule_tac f'=lookup_failure_rel
|
||||
and r'="\<lambda>pml4_ptr pml4_ptr'. pml4_ptr' = pml4e_Ptr pml4_ptr"
|
||||
and xf'=find_ret_'
|
||||
in ccorres_split_nothrow_case_sum)
|
||||
in ccorres_split_nothrow_case_sum)
|
||||
apply (ctac add: findVSpaceForASID_ccorres)
|
||||
apply ceqv
|
||||
apply (rule_tac P="capPDBasePtr_CL (cap_page_directory_cap_lift threadRoot)
|
||||
= capPDBasePtr (capCap rv)"
|
||||
apply (rename_tac vspace vspace')
|
||||
apply (rule_tac P="capPML4BasePtr_CL (cap_pml4_cap_lift vRootCap')
|
||||
= capPML4BasePtr (capCap vRootCap)"
|
||||
in ccorres_gen_asm2)
|
||||
apply (simp del: Collect_const)
|
||||
apply simp
|
||||
apply (rule ccorres_Cond_rhs_Seq)
|
||||
apply (simp add: whenE_def throwError_def
|
||||
checkPML4NotInASIDMap_def checkPML4ASIDMapMembership_def)
|
||||
apply (rule ccorres_stateAssert)
|
||||
apply (rule ccorres_pre_gets_armUSGlobalPD_ksArchState[unfolded o_def])
|
||||
apply (rule ccorres_rhs_assoc)+
|
||||
apply (rule ccorres_h_t_valid_armUSGlobalPD)
|
||||
apply (simp add: whenE_def throwError_def dc_def[symmetric], ccorres_rewrite)
|
||||
apply (rule ccorres_rhs_assoc)
|
||||
apply (rule ccorres_h_t_valid_x64KSSKIMPML4)
|
||||
apply csymbr
|
||||
apply (rule ccorres_pre_gets_x64KSSKIMPML4_ksArchState[unfolded comp_def])
|
||||
apply (rule ccorres_add_return2)
|
||||
apply (ctac(no_vcg) add: setCurrentPD_ccorres)
|
||||
apply (rule ccorres_split_throws)
|
||||
apply (rule ccorres_return_void_C[unfolded dc_def])
|
||||
apply vcg
|
||||
apply wp
|
||||
apply (ctac (no_vcg) add: setCurrentUserVSpaceRoot_ccorres)
|
||||
apply (rule ccorres_return_void_C)
|
||||
apply (rule hoare_post_taut[where P=\<top>])
|
||||
apply (simp add: whenE_def returnOk_def)
|
||||
apply (ctac (no_vcg) add: armv_contextSwitch_ccorres[unfolded dc_def])
|
||||
apply (rule ccorres_move_c_guard_tcb)
|
||||
apply (rule ccorres_symb_exec_l3)
|
||||
apply (rename_tac tcb)
|
||||
apply (rule_tac P="ko_at' tcb thread" in ccorres_cross_over_guard)
|
||||
apply (ctac add: vcpu_switch_ccorres[unfolded dc_def]) (* c *)
|
||||
apply wp
|
||||
apply (wp getObject_tcb_wp)
|
||||
apply simp
|
||||
apply clarsimp
|
||||
apply (wp hoare_drop_imp hoare_vcg_ex_lift armv_contextSwitch_invs_no_cicd' valid_case_option_post_wp')
|
||||
apply (simp add: checkPML4NotInASIDMap_def checkPML4ASIDMapMembership_def)
|
||||
apply (rule ccorres_stateAssert)
|
||||
apply (rule ccorres_rhs_assoc)+
|
||||
apply (rule ccorres_pre_gets_armUSGlobalPD_ksArchState[unfolded o_def])
|
||||
apply (rule ccorres_h_t_valid_armUSGlobalPD)
|
||||
apply (csymbr, rename_tac base_addr)
|
||||
apply (rule ccorres_symb_exec_r)
|
||||
apply (ctac add: getCurrentUserCR3_ccorres, rename_tac currentCR3 currentCR3')
|
||||
apply (rule ccorres_if_bind, rule ccorres_if_lhs; simp add: dc_def[symmetric])
|
||||
apply (rule ccorres_cond_true)
|
||||
apply (ctac add: setCurrentUserCR3_ccorres)
|
||||
apply (rule ccorres_cond_false)
|
||||
apply (rule ccorres_return_Skip)
|
||||
apply (simp, rule hoare_post_taut[where P=\<top>])
|
||||
apply vcg
|
||||
apply vcg
|
||||
apply (rule conseqPre, vcg, clarsimp)
|
||||
apply (rule ccorres_cond_true_seq, simp add: dc_def[symmetric], ccorres_rewrite)
|
||||
apply (rule ccorres_rhs_assoc)
|
||||
apply (rule ccorres_h_t_valid_x64KSSKIMPML4)
|
||||
apply csymbr
|
||||
apply (rule ccorres_pre_gets_x64KSSKIMPML4_ksArchState[unfolded comp_def])
|
||||
apply (rule ccorres_add_return2)
|
||||
apply (ctac(no_vcg) add: setCurrentPD_ccorres)
|
||||
apply (rule ccorres_split_throws)
|
||||
apply (rule ccorres_return_void_C[unfolded dc_def])
|
||||
apply vcg
|
||||
apply wp
|
||||
apply simp
|
||||
apply (wp hoare_drop_imps)[1]
|
||||
apply (simp add: Collect_const_mem)
|
||||
apply (ctac (no_vcg) add: setCurrentUserVSpaceRoot_ccorres)
|
||||
apply (rule ccorres_return_void_C)
|
||||
apply (rule hoare_post_taut[where P=\<top>])
|
||||
apply (simp add: asid_wf_0, rule wp_post_tautE)
|
||||
apply (vcg exspec=findVSpaceForASID_modifies)
|
||||
apply (simp add: getSlotCap_def)
|
||||
apply (wp getCTE_wp')
|
||||
apply (clarsimp simp add: if_1_0_0 simp del: Collect_const)
|
||||
apply (wpsimp wp: getSlotCap_wp)
|
||||
apply vcg
|
||||
apply (clarsimp simp: Collect_const_mem word_sle_def)
|
||||
apply (clarsimp simp: Collect_const_mem)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: all_invs_but_ct_idle_or_in_cur_domain'_def)
|
||||
apply (frule cte_wp_at_valid_objs_valid_cap', clarsimp+)
|
||||
apply (auto simp: isCap_simps valid_cap'_def mask_def dest!: tcb_ko_at')[1]
|
||||
apply (rule_tac x=ta in exI, auto split: option.splits)[1]
|
||||
apply (frule (2) sym_refs_tcb_vcpu', clarsimp)
|
||||
apply (clarsimp simp: obj_at'_def typ_at'_def ko_wp_at'_def projectKOs)
|
||||
apply (clarsimp simp: ptr_val_tcb_ptr_mask'
|
||||
size_of_def cte_level_bits_def
|
||||
tcbVTableSlot_def tcb_cnode_index_defs
|
||||
ccap_rights_relation_def cap_rights_to_H_def
|
||||
to_bool_def true_def allRights_def
|
||||
mask_def[where n="Suc 0"]
|
||||
cte_at_tcb_at_16' addrFromPPtr_def)
|
||||
apply (frule cte_at_tcb_at_32', drule cte_at_cte_wp_atD)
|
||||
apply (clarsimp simp: cte_level_bits_def tcbVTableSlot_def)
|
||||
apply (rule_tac x="cteCap cte" in exI)
|
||||
apply (rule conjI, erule cte_wp_at_weakenE', simp)
|
||||
apply (clarsimp simp: invs_cicd_no_0_obj' invs_cicd_arch_state')
|
||||
apply (frule cte_wp_at_valid_objs_valid_cap'; clarsimp simp: invs_cicd_valid_objs')
|
||||
apply (clarsimp simp: isCap_simps valid_cap'_def mask_def asid_wf_def)
|
||||
apply (clarsimp simp: tcb_cnode_index_defs cte_level_bits_def tcbVTableSlot_def
|
||||
cte_at_tcb_at_32' to_bool_def)
|
||||
apply (clarsimp simp: cap_get_tag_isCap_ArchObject2
|
||||
dest!: isCapDs)
|
||||
apply (clarsimp simp: cap_get_tag_isCap_ArchObject[symmetric]
|
||||
cap_lift_page_directory_cap cap_to_H_def
|
||||
cap_page_directory_cap_lift_def
|
||||
to_bool_def
|
||||
elim!: ccap_relationE split: if_split_asm)
|
||||
apply (rename_tac s'')
|
||||
apply (drule_tac s=s'' in obj_at_cslift_tcb, assumption)
|
||||
apply (clarsimp simp: typ_heap_simps)
|
||||
apply (clarsimp simp: ctcb_relation_def carch_tcb_relation_def)
|
||||
done *)
|
||||
cap_lift_pml4_cap cap_to_H_def
|
||||
cap_pml4_cap_lift_def
|
||||
to_bool_def mask_def
|
||||
ccr3_relation_defs Let_def
|
||||
cr3_lift_def word_bw_assocs
|
||||
elim!: ccap_relationE
|
||||
split: if_split_asm X64_H.cr3.splits)
|
||||
apply (rename_tac t t')
|
||||
apply (rule conjI; clarsimp)
|
||||
apply (drule_tac t="cr3_C.words_C (ret__struct_cr3_C_' t').[0]" in sym)
|
||||
apply (simp add: word_bw_assocs)
|
||||
apply (frule (1) word_combine_masks[where m="0x7FFFFFFFFF000" and m'="0xFFF"]; simp add: word_ao_dist2[symmetric])
|
||||
apply (frule (1) word_combine_masks[where m="0x7FFFFFFFFFFFF" and m'="0x7FF8000000000000"]; simp)
|
||||
apply (match premises in H: \<open>cr3_C.words_C _.[0] && _ = 0\<close> \<Rightarrow> \<open>insert H; word_bitwise\<close>)
|
||||
done
|
||||
|
||||
(* FIXME: move *)
|
||||
lemma invs'_invs_no_cicd:
|
||||
"invs' s \<Longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s"
|
||||
by (clarsimp simp add: invs'_def all_invs_but_ct_idle_or_in_cur_domain'_def valid_state'_def newKernelState_def)
|
||||
(* FIXME: remove *)
|
||||
lemmas invs'_invs_no_cicd = invs_invs_no_cicd'
|
||||
|
||||
lemma ccorres_seq_IF_False:
|
||||
"ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (IF False THEN x ELSE y FI ;; c) = ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (y ;; c)"
|
||||
|
|
|
|||
|
|
@ -1324,16 +1324,16 @@ lemma pml4e_at_shifting_magic:
|
|||
|
||||
lemma le_user_vtop_less_pptr_base[simp]:
|
||||
"x \<le> user_vtop \<Longrightarrow> x < pptr_base"
|
||||
apply (clarsimp simp: user_vtop_def pptr_base_def pptrBase_def)
|
||||
apply (clarsimp simp: user_vtop_def pptrUserTop_def pptr_base_def pptrBase_def)
|
||||
by (word_bitwise; simp)
|
||||
|
||||
lemma le_user_vtop_canonical_address[simp]:
|
||||
"x \<le> user_vtop \<Longrightarrow> canonical_address x"
|
||||
by (clarsimp simp: user_vtop_def canonical_address_range mask_def)
|
||||
by (clarsimp simp: user_vtop_def pptrUserTop_def canonical_address_range mask_def)
|
||||
|
||||
lemma le_user_vtop_and_user_vtop_eq:
|
||||
"x && ~~ mask pml4_shift_bits \<le> user_vtop \<Longrightarrow> x && user_vtop = x"
|
||||
apply (clarsimp simp add: user_vtop_def bit_simps)
|
||||
apply (clarsimp simp add: user_vtop_def pptrUserTop_def bit_simps)
|
||||
by (word_bitwise; simp)
|
||||
|
||||
lemma and_not_mask_pml4_not_kernel_mapping_slots:
|
||||
|
|
|
|||
|
|
@ -18,11 +18,15 @@ named_theorems EmptyFail_AI_assms
|
|||
|
||||
crunch_ignore (empty_fail)
|
||||
(add: invalidateTLBEntry_impl invalidateTranslationSingleASID_impl
|
||||
resetCR3_impl invalidateASID_impl ioapicMapPinToVector_impl updateIRQState_impl
|
||||
invalidateASID_impl ioapicMapPinToVector_impl updateIRQState_impl
|
||||
in8_impl in16_impl in32_impl out8_impl out16_impl out32_impl)
|
||||
|
||||
lemma invalidateLocalPageStructureCacheASID_ef[simp,wp]:
|
||||
"empty_fail (invalidateLocalPageStructureCacheASID vs asid)"
|
||||
by (simp add: invalidateLocalPageStructureCacheASID_def)
|
||||
|
||||
crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]:
|
||||
loadWord, load_word_offs, storeWord, getRestartPC, get_mrs, invalidate_local_page_structure_cache_asid
|
||||
loadWord, load_word_offs, storeWord, getRestartPC, get_mrs, invalidate_page_structure_cache_asid
|
||||
|
||||
end
|
||||
|
||||
|
|
|
|||
|
|
@ -721,7 +721,7 @@ lemma flush_table_empty:
|
|||
| rule hoare_pre)+
|
||||
done
|
||||
|
||||
crunch empty[wp]: flush_all, invalidate_local_page_structure_cache_asid, lookup_pt_slot, set_vm_root,
|
||||
crunch empty[wp]: flush_all, invalidate_page_structure_cache_asid, lookup_pt_slot, set_vm_root,
|
||||
invalidate_asid_entry
|
||||
"\<lambda>s. obj_at (empty_table (set (x64_global_pdpts (arch_state s)))) word s"
|
||||
(wp: crunch_wps simp: crunch_simps)
|
||||
|
|
@ -1002,10 +1002,12 @@ lemma replaceable_reset_pml4:
|
|||
crunch caps_of_state [wp]: arch_finalise_cap "\<lambda>s. P (caps_of_state s)"
|
||||
(wp: crunch_wps simp: crunch_simps)
|
||||
|
||||
crunch obj_at[wp]: invalidate_local_page_structure_cache_asid, invalidate_asid_entry "\<lambda>s. P' (obj_at P p s)"
|
||||
crunch obj_at[wp]: invalidate_page_structure_cache_asid, invalidate_asid_entry
|
||||
"\<lambda>s. P' (obj_at P p s)"
|
||||
(wp: hoare_whenE_wp simp: crunch_simps)
|
||||
|
||||
crunch x64_global_pdpts[wp]: invalidate_local_page_structure_cache_asid, invalidate_asid_entry "\<lambda>s. P' (x64_global_pdpts (arch_state s))"
|
||||
crunch x64_global_pdpts[wp]: invalidate_page_structure_cache_asid, invalidate_asid_entry
|
||||
"\<lambda>s. P' (x64_global_pdpts (arch_state s))"
|
||||
(wp: hoare_whenE_wp simp: crunch_simps)
|
||||
|
||||
lemma delete_asid_empty_table_pml4:
|
||||
|
|
@ -1230,8 +1232,8 @@ lemma replaceable_or_arch_update_pg:
|
|||
apply (auto simp: is_cap_simps is_arch_update_def cap_master_cap_simps)
|
||||
done
|
||||
|
||||
crunch valid_cap: invalidate_local_page_structure_cache_asid, invalidate_asid_entry "valid_cap cap"
|
||||
crunch valid_objs[wp]: invalidate_local_page_structure_cache_asid, invalidate_asid_entry "valid_objs"
|
||||
crunch valid_cap: invalidate_page_structure_cache_asid, invalidate_asid_entry "valid_cap cap"
|
||||
crunch valid_objs[wp]: invalidate_page_structure_cache_asid, invalidate_asid_entry "valid_objs"
|
||||
crunch valid_asid_table[wp]: do_machine_op
|
||||
"\<lambda>s. valid_asid_table (x64_asid_table (arch_state s)) s"
|
||||
|
||||
|
|
@ -1577,10 +1579,10 @@ lemma delete_asid_pool_unmapped2:
|
|||
apply fastforce
|
||||
done
|
||||
|
||||
crunch x64_global_pml4[wp]: invalidate_asid_entry, invalidate_local_page_structure_cache_asid
|
||||
crunch x64_global_pml4[wp]: invalidate_asid_entry, invalidate_page_structure_cache_asid
|
||||
"\<lambda>s. P (x64_global_pml4(arch_state s))"
|
||||
|
||||
crunch global_refs_invs[wp]: invalidate_local_page_structure_cache_asid
|
||||
crunch global_refs_invs[wp]: invalidate_page_structure_cache_asid
|
||||
"\<lambda>s. P (global_refs s)"
|
||||
|
||||
lemma page_table_pte_atE:
|
||||
|
|
|
|||
|
|
@ -994,6 +994,13 @@ where
|
|||
"valid_global_pdpts \<equiv> \<lambda>s.
|
||||
\<forall>p \<in> set (x64_global_pdpts (arch_state s)). typ_at (AArch APDPointerTable) p s"
|
||||
|
||||
definition
|
||||
valid_cr3 :: "cr3 \<Rightarrow> bool"
|
||||
where
|
||||
"valid_cr3 r \<equiv> is_aligned (cr3_base_address r) asid_bits
|
||||
\<and> cr3_base_address r \<le> mask (pml4_shift_bits + asid_bits)
|
||||
\<and> asid_wf (cr3_pcid r)"
|
||||
|
||||
(* arch_live/hyp_live stub *)
|
||||
|
||||
definition
|
||||
|
|
@ -1037,9 +1044,12 @@ definition
|
|||
valid_arch_state :: "'z::state_ext state \<Rightarrow> bool"
|
||||
where
|
||||
"valid_arch_state \<equiv> \<lambda>s.
|
||||
valid_asid_table (x64_asid_table (arch_state s)) s \<and>
|
||||
page_map_l4_at (x64_global_pml4 (arch_state s)) s \<and>
|
||||
valid_global_pts s \<and> valid_global_pds s \<and> valid_global_pdpts s"
|
||||
valid_asid_table (x64_asid_table (arch_state s)) s
|
||||
\<and> page_map_l4_at (x64_global_pml4 (arch_state s)) s
|
||||
\<and> valid_global_pts s
|
||||
\<and> valid_global_pds s
|
||||
\<and> valid_global_pdpts s
|
||||
\<and> valid_cr3 (x64_current_cr3 (arch_state s))"
|
||||
|
||||
definition
|
||||
vs_cap_ref_arch :: "arch_cap \<Rightarrow> vs_ref list option"
|
||||
|
|
|
|||
|
|
@ -132,20 +132,20 @@ lemma init_irq_ptrs_eq:
|
|||
done
|
||||
|
||||
lemma in_kernel_base:
|
||||
"\<lbrakk>m < 0x3FFFFFFF; n \<le> 0x3FFFFFFF\<rbrakk>
|
||||
"\<lbrakk>m < 0x7FFFFFFF; n \<le> 0x7FFFFFFF\<rbrakk>
|
||||
\<Longrightarrow> (\<forall>y\<in>{kernel_base + m .. n + kernel_base}.
|
||||
kernel_base \<le> y \<and> y \<le> kernel_base + 0x3FFFFFFF)"
|
||||
kernel_base \<le> y \<and> y \<le> kernel_base + 0x7FFFFFFF)"
|
||||
apply (clarsimp)
|
||||
apply (intro conjI)
|
||||
apply (rule ccontr,simp add:not_le)
|
||||
apply (rule ccontr, simp add:not_le)
|
||||
apply (drule(1) le_less_trans)
|
||||
apply (cut_tac is_aligned_no_wrap'[where ptr=kernel_base and off=m and sz=30, simplified])
|
||||
apply (cut_tac is_aligned_no_wrap'[where ptr=kernel_base and off=m and sz=31, simplified])
|
||||
apply (drule less_le_trans[of _ kernel_base kernel_base])
|
||||
apply (simp add: pptr_base_def pptrBase_def kernel_base_def)
|
||||
apply simp
|
||||
apply (simp add:kernel_base_def is_aligned_def)
|
||||
apply (rule ccontr, simp add:not_less)
|
||||
apply (drule less_le_trans[where z = "0x40000000"])
|
||||
apply (drule less_le_trans[where z = "0x80000000"])
|
||||
apply simp
|
||||
apply simp
|
||||
apply (erule order_trans)
|
||||
|
|
@ -156,7 +156,7 @@ lemma in_kernel_base:
|
|||
done
|
||||
|
||||
lemma in_kernel_base_in_pptr_base:
|
||||
"\<lbrakk>m < 0x3FFFFFFF; n \<le> 0x3FFFFFFF\<rbrakk>
|
||||
"\<lbrakk>m < 0x7FFFFFFF; n \<le> 0x7FFFFFFF\<rbrakk>
|
||||
\<Longrightarrow> (\<forall>y\<in>{kernel_base + m .. n + kernel_base}.
|
||||
pptr_base \<le> y \<and> y \<le> pptr_base + 0x7FFFFFFFFF)"
|
||||
apply (frule (1) in_kernel_base; erule ballEI; clarsimp)
|
||||
|
|
@ -292,7 +292,8 @@ lemma invs_A:
|
|||
apply (rule conjI)
|
||||
apply (clarsimp simp: valid_asid_table_def state_defs)
|
||||
apply (simp add: valid_global_pts_def valid_global_pds_def valid_global_pdpts_def
|
||||
valid_arch_state_def state_defs obj_at_def a_type_def)
|
||||
valid_arch_state_def state_defs obj_at_def a_type_def
|
||||
valid_cr3_def asid_wf_0)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: valid_irq_node_def obj_at_def state_defs
|
||||
is_cap_table_def wf_empty_bits
|
||||
|
|
|
|||
|
|
@ -298,7 +298,7 @@ lemma flush_table_valid_vspace_objs'[wp]:
|
|||
"\<lbrace>valid_vspace_objs'\<rbrace> flush_table a b c d \<lbrace>\<lambda>rv. valid_vspace_objs'\<rbrace>"
|
||||
by (wp mapM_x_wp' | wpc | simp add: flush_table_def | rule hoare_pre)+
|
||||
|
||||
crunch valid_vspace_objs'[wp]: invalidate_local_page_structure_cache_asid valid_vspace_objs'
|
||||
crunch valid_vspace_objs'[wp]: invalidate_page_structure_cache_asid valid_vspace_objs'
|
||||
|
||||
crunch kheap[wp]: get_cap "\<lambda>s. P (kheap s)"
|
||||
(wp: crunch_wps simp: crunch_simps)
|
||||
|
|
|
|||
|
|
@ -920,18 +920,22 @@ lemma arch_state_update_invs:
|
|||
|
||||
lemma valid_ioports_cr3_update[iff]:
|
||||
"valid_ioports (s\<lparr>arch_state := arch_state s\<lparr>x64_current_cr3 := c\<rparr>\<rparr>) = valid_ioports s"
|
||||
crunch global_pml4[wp]: set_current_cr3 "\<lambda>s. P (x64_global_pml4 (arch_state s))"
|
||||
|
||||
by (clarsimp simp: valid_ioports_def all_ioports_issued_def issued_ioports_def)
|
||||
|
||||
lemma set_current_cr3_invs[wp]:
|
||||
"\<lbrace>invs\<rbrace> set_current_cr3 c \<lbrace>\<lambda>rv. invs\<rbrace>"
|
||||
"\<lbrace>invs and K (valid_cr3 c)\<rbrace> set_current_cr3 c \<lbrace>\<lambda>rv. invs\<rbrace>"
|
||||
apply (wpsimp simp: set_current_cr3_def; erule arch_state_update_invs)
|
||||
by (auto simp: valid_global_refs_def global_refs_def valid_arch_state_def valid_table_caps_def
|
||||
valid_global_objs_def valid_kernel_mappings_def second_level_tables_def)
|
||||
|
||||
lemma set_current_vspace_root_invs[wp]:
|
||||
"\<lbrace>invs\<rbrace> set_current_vspace_root vspace asid \<lbrace>\<lambda>rv. invs\<rbrace>"
|
||||
apply (simp add: set_current_vspace_root_def)
|
||||
apply (wp)
|
||||
lemma valid_cr3_make_cr3:
|
||||
"asid_wf asid \<Longrightarrow> valid_cr3 (make_cr3 addr asid)"
|
||||
apply (clarsimp simp: valid_cr3_def make_cr3_def cr3_addr_mask_def bit_simps
|
||||
is_aligned_andI2[OF is_aligned_shift])
|
||||
apply (rule order.trans[OF word_and_le1])
|
||||
apply (simp add: mask_def asid_bits_def)
|
||||
done
|
||||
|
||||
lemma set_current_vspace_root_invs[wp]:
|
||||
|
|
@ -949,9 +953,14 @@ lemma asid_wf_0:
|
|||
lemma svr_invs [wp]:
|
||||
"\<lbrace>invs\<rbrace> set_vm_root t' \<lbrace>\<lambda>_. invs\<rbrace>"
|
||||
apply (simp add: set_vm_root_def)
|
||||
apply (wp hoare_whenE_wp get_cap_wp
|
||||
| wpc
|
||||
| simp add: split_def if_apply_def2 cong: if_cong)+
|
||||
apply (wp hoare_whenE_wp
|
||||
| wpc
|
||||
| simp add: split_def if_apply_def2 cong: conj_cong if_cong
|
||||
| strengthen valid_cr3_make_cr3)+
|
||||
apply (strengthen drop_imp)
|
||||
apply (wpsimp wp: get_cap_wp simp: asid_wf_0)+
|
||||
apply (drule (1) cte_wp_valid_cap[OF _ invs_valid_objs])
|
||||
apply (simp add: valid_cap_def)
|
||||
done
|
||||
|
||||
crunch pred_tcb_at[wp]: set_current_vspace_root "pred_tcb_at proj P t"
|
||||
|
|
@ -1692,11 +1701,7 @@ lemma not_in_global_refs_vs_lookup:
|
|||
apply blast
|
||||
done
|
||||
|
||||
crunch device_state_inv[wp]: invalidateASID,resetCR3 "\<lambda>s. P (device_state s)"
|
||||
|
||||
lemma resetCR3_underlying_memory[wp]:
|
||||
"\<lbrace>\<lambda>m'. underlying_memory m' p = um\<rbrace> resetCR3 \<lbrace>\<lambda>_ m'. underlying_memory m' p = um\<rbrace>"
|
||||
by (simp add: resetCR3_def machine_op_lift_underlying_memory)
|
||||
crunch device_state_inv[wp]: invalidateASID "\<lambda>s. P (device_state s)"
|
||||
|
||||
lemma invalidateASID_underlying_memory[wp]:
|
||||
"\<lbrace>\<lambda>m'. underlying_memory m' p = um\<rbrace> invalidateASID vspace asid \<lbrace>\<lambda>_ m'. underlying_memory m' p = um\<rbrace>"
|
||||
|
|
@ -1705,7 +1710,6 @@ lemma invalidateASID_underlying_memory[wp]:
|
|||
lemma no_irq_invalidateASID: "no_irq (invalidateASID vpsace asid)"
|
||||
by (clarsimp simp: invalidateASID_def)
|
||||
|
||||
lemmas resetCR3_irq_masks = no_irq[OF no_irq_resetCR3]
|
||||
lemmas invalidateASID_irq_masks = no_irq[OF no_irq_invalidateASID]
|
||||
|
||||
lemma flush_all_invs[wp]:
|
||||
|
|
@ -1812,7 +1816,7 @@ lemma vs_lookup_pages_current_cr3[iff]:
|
|||
vs_lookup_pages s"
|
||||
by (simp add: vs_lookup_pages_arch_update)
|
||||
|
||||
crunch vs_lookup_pages[wp]: invalidate_local_page_structure_cache_asid "\<lambda>s. P (vs_lookup_pages s)"
|
||||
crunch vs_lookup_pages[wp]: invalidate_page_structure_cache_asid "\<lambda>s. P (vs_lookup_pages s)"
|
||||
(simp: crunch_simps wp: crunch_wps)
|
||||
|
||||
lemma vs_ref_pages_simps:
|
||||
|
|
@ -2568,7 +2572,13 @@ lemma vs_lookup1_archD:
|
|||
\<and> ko_at (ArchObj ko) p s \<and> (r,p') \<in> vs_refs_arch ko"
|
||||
by (clarsimp dest!: vs_lookup1D simp: obj_at_def vs_refs_def split: kernel_object.splits)
|
||||
|
||||
crunch invs[wp]: invalidate_local_page_structure_cache_asid invs
|
||||
lemma dmo_invalidateLocalPageStructureCacheASID[wp]:
|
||||
"\<lbrace>invs\<rbrace> do_machine_op (invalidateLocalPageStructureCacheASID vs asid) \<lbrace>\<lambda>rv. invs\<rbrace>"
|
||||
by (simp add: invalidateLocalPageStructureCacheASID_def do_machine_op_lift_invs)
|
||||
|
||||
lemma invalidate_page_structure_cache_asid_invs[wp]:
|
||||
"\<lbrace>invs\<rbrace> invalidate_page_structure_cache_asid vs asid \<lbrace>\<lambda>rv. invs\<rbrace>"
|
||||
by (wpsimp simp: invalidate_page_structure_cache_asid_def)
|
||||
|
||||
lemma unmap_pd_invs[wp]:
|
||||
"\<lbrace>invs and K (vaddr < pptr_base \<and> canonical_address vaddr)\<rbrace>
|
||||
|
|
@ -3931,7 +3941,7 @@ lemma perform_io_port_invocation_invs[wp]:
|
|||
done
|
||||
|
||||
lemma user_vtop_mask: "user_vtop = mask 47"
|
||||
by (simp add: user_vtop_def mask_def)
|
||||
by (simp add: user_vtop_def pptrUserTop_def mask_def)
|
||||
|
||||
lemma user_vtop_le: "p && user_vtop \<le> mask 47"
|
||||
by (simp add: user_vtop_mask word_and_le1)
|
||||
|
|
|
|||
|
|
@ -317,9 +317,6 @@ lemma no_irq_modify:
|
|||
lemma no_irq_invalidateTLBEntry: "no_irq (invalidateTLBEntry a)"
|
||||
by (clarsimp simp: invalidateTLBEntry_def)
|
||||
|
||||
lemma no_irq_resetCR3: "no_irq resetCR3"
|
||||
by (clarsimp simp: resetCR3_def)
|
||||
|
||||
lemma no_irq_storeWord: "no_irq (storeWord w p)"
|
||||
apply (simp add: storeWord_def)
|
||||
apply (wp no_irq_modify)
|
||||
|
|
@ -353,6 +350,13 @@ lemma no_irq_out16: "no_irq (out16 irq b)"
|
|||
lemma no_irq_out32: "no_irq (out32 irq b)"
|
||||
by (wp | clarsimp simp: out32_def)+
|
||||
|
||||
lemma no_irq_invalidateLocalPageStructureCacheASID:
|
||||
"no_irq (invalidateLocalPageStructureCacheASID vspace asid)"
|
||||
by (wpsimp simp: invalidateLocalPageStructureCacheASID_def)
|
||||
|
||||
lemmas invalidateLocalPageStructureCacheASID_irq_masks =
|
||||
no_irq[OF no_irq_invalidateLocalPageStructureCacheASID]
|
||||
|
||||
lemma getActiveIRQ_le_maxIRQ':
|
||||
"\<lbrace>\<lambda>s. \<forall>irq > maxIRQ. irq_masks s irq\<rbrace>
|
||||
getActiveIRQ in_kernel
|
||||
|
|
@ -423,10 +427,6 @@ lemma hwASIDInvalidate_ef[simp,wp]: "empty_fail (hwASIDInvalidate b a)"
|
|||
lemma updateIRQState_ef[simp,wp]: "empty_fail (updateIRQState b c)"
|
||||
by (simp add: updateIRQState_def)
|
||||
|
||||
(* FIXME x64: move *)
|
||||
lemma resetCR3_ef[simp,wp]: "empty_fail (resetCR3)"
|
||||
by (simp add: resetCR3_def)
|
||||
|
||||
(* FIXME x64: move *)
|
||||
lemma writeCR3_ef[simp,wp]: "empty_fail (writeCR3 a b)"
|
||||
by (simp add: writeCR3_def)
|
||||
|
|
|
|||
|
|
@ -1535,7 +1535,7 @@ crunch typ_at'[wp]: copyGlobalMappings "\<lambda>s. P (typ_at' T p s)"
|
|||
lemmas copyGlobalMappings_typ_ats[wp] = typ_at_lifts [OF copyGlobalMappings_typ_at']
|
||||
|
||||
lemma corres_gets_global_pml4 [corres]:
|
||||
"corres (op =) \<top> \<top> (gets (x64_global_pml4 \<circ> arch_state)) (gets (x64KSGlobalPML4 \<circ> ksArchState))"
|
||||
"corres (op =) \<top> \<top> (gets (x64_global_pml4 \<circ> arch_state)) (gets (x64KSSKIMPML4 \<circ> ksArchState))"
|
||||
by (simp add: state_relation_def arch_state_relation_def)
|
||||
|
||||
lemma copy_global_mappings_corres [@lift_corres_args, corres]:
|
||||
|
|
@ -1547,7 +1547,7 @@ lemma copy_global_mappings_corres [@lift_corres_args, corres]:
|
|||
apply (fold word_size_bits_def)
|
||||
apply corressimp
|
||||
apply (rule_tac P="page_map_l4_at global_pm and ?apre" and
|
||||
P'="page_map_l4_at' globalPM and page_map_l4_at' pm"
|
||||
P'="page_map_l4_at' skimPM and page_map_l4_at' pm"
|
||||
in corresK_mapM_x[OF order_refl])
|
||||
apply (corressimp simp: objBits_def mask_def wp: get_pde_wp getPDE_wp)+
|
||||
apply(rule conjI)
|
||||
|
|
|
|||
|
|
@ -587,7 +587,7 @@ lemma vs_refs_pages_pml4I:
|
|||
done
|
||||
|
||||
lemma userVTop_conv[simp]: "userVTop = user_vtop"
|
||||
by (simp add: userVTop_def user_vtop_def)
|
||||
by (simp add: userVTop_def user_vtop_def X64.pptrUserTop_def)
|
||||
|
||||
lemma find_vspace_for_asid_lookup_slot [wp]:
|
||||
"\<lbrace>pspace_aligned and valid_vspace_objs\<rbrace>
|
||||
|
|
@ -1881,7 +1881,7 @@ lemma decode_page_inv_wf[wp]:
|
|||
dest!: diminished_capMaster)
|
||||
apply (rule conjI)
|
||||
apply (erule is_aligned_addrFromPPtr_n, case_tac vmpage_size, simp_all add: bit_simps)[1]
|
||||
apply (simp add: user_vtop_def X64.pptrBase_def)
|
||||
apply (simp add: user_vtop_def X64.pptrBase_def X64.pptrUserTop_def)
|
||||
apply (word_bitwise)
|
||||
apply (cases "invocation_type label = ArchInvocationLabel X64PageRemap")
|
||||
apply (simp add: split_def invs_valid_objs' split del: if_split
|
||||
|
|
@ -1940,7 +1940,7 @@ lemma decode_page_table_inv_wf[wp]:
|
|||
apply (clarsimp simp: diminished_valid' [symmetric])
|
||||
apply (clarsimp simp: valid_cap'_def bit_simps is_aligned_addrFromPPtr_n
|
||||
invs_valid_objs' and_not_mask[symmetric])
|
||||
apply (clarsimp simp: mask_def X64.pptrBase_def user_vtop_def)
|
||||
apply (clarsimp simp: mask_def X64.pptrBase_def X64.pptrUserTop_def user_vtop_def)
|
||||
apply word_bitwise
|
||||
apply auto
|
||||
done
|
||||
|
|
@ -1972,7 +1972,7 @@ lemma decode_page_directory_inv_wf[wp]:
|
|||
apply (clarsimp simp: diminished_valid' [symmetric])
|
||||
apply (clarsimp simp: valid_cap'_def bit_simps is_aligned_addrFromPPtr_n
|
||||
invs_valid_objs' and_not_mask[symmetric])
|
||||
apply (clarsimp simp: mask_def X64.pptrBase_def user_vtop_def)
|
||||
apply (clarsimp simp: mask_def X64.pptrBase_def X64.pptrUserTop_def user_vtop_def)
|
||||
apply word_bitwise
|
||||
apply auto
|
||||
done
|
||||
|
|
@ -2004,7 +2004,7 @@ lemma decode_pdpt_inv_wf[wp]:
|
|||
apply (clarsimp simp: diminished_valid' [symmetric])
|
||||
apply (clarsimp simp: valid_cap'_def bit_simps is_aligned_addrFromPPtr_n
|
||||
invs_valid_objs' and_not_mask[symmetric])
|
||||
apply (clarsimp simp: mask_def X64.pptrBase_def user_vtop_def)
|
||||
apply (clarsimp simp: mask_def X64.pptrBase_def X64.pptrUserTop_def user_vtop_def)
|
||||
apply word_bitwise
|
||||
apply auto
|
||||
done
|
||||
|
|
|
|||
|
|
@ -9724,8 +9724,8 @@ crunch irq_states' [wp]: capSwapForDelete valid_irq_states'
|
|||
|
||||
crunch irq_states' [wp]: finaliseCap valid_irq_states'
|
||||
(wp: crunch_wps hoare_unless_wp getASID_wp no_irq
|
||||
no_irq_hwASIDInvalidate no_irq_writeCR3
|
||||
no_irq_invalidateASID
|
||||
no_irq_hwASIDInvalidate no_irq_writeCR3 no_irq_invalidateASID
|
||||
no_irq_invalidateLocalPageStructureCacheASID
|
||||
simp: crunch_simps o_def ignore: getObject setObject)
|
||||
|
||||
lemma finaliseSlot_IRQInactive':
|
||||
|
|
|
|||
|
|
@ -3218,7 +3218,7 @@ lemma storePDE_setCTE_commute:
|
|||
lemma setCTE_gets_globalPML4_commute:
|
||||
"monad_commute
|
||||
(cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and pspace_aligned')
|
||||
(setCTE src cte) (gets (x64KSGlobalPML4 \<circ> ksArchState))"
|
||||
(setCTE src cte) (gets (x64KSSKIMPML4 \<circ> ksArchState))"
|
||||
apply (simp add:setCTE_def2)
|
||||
apply (rule monad_commute_guard_imp)
|
||||
apply (rule commute_commute[OF monad_commute_split[where Q = "\<lambda>r. \<top>"]])
|
||||
|
|
@ -3235,7 +3235,7 @@ lemma placeNewObject_gets_globalPML4_commute:
|
|||
(pspace_distinct' and pspace_aligned' and
|
||||
K (us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us)) and
|
||||
pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) )
|
||||
(placeNewObject ptr val us) (gets (x64KSGlobalPML4 \<circ> ksArchState))"
|
||||
(placeNewObject ptr val us) (gets (x64KSSKIMPML4 \<circ> ksArchState))"
|
||||
apply (rule commute_name_pre_state)
|
||||
apply (rule monad_commute_guard_imp)
|
||||
apply (rule_tac commute_rewrite[where Q = "\<lambda>s.
|
||||
|
|
|
|||
|
|
@ -1050,10 +1050,10 @@ definition
|
|||
where
|
||||
"global_refs' \<equiv> \<lambda>s.
|
||||
{ksIdleThread s} \<union>
|
||||
table_refs' (x64KSGlobalPML4 (ksArchState s)) \<union>
|
||||
(\<Union>pt \<in> set (x64KSGlobalPDs (ksArchState s)). table_refs' pt) \<union>
|
||||
(\<Union>pt \<in> set (x64KSGlobalPTs (ksArchState s)). table_refs' pt) \<union>
|
||||
(\<Union>pt \<in> set (x64KSGlobalPDPTs (ksArchState s)). table_refs' pt) \<union>
|
||||
table_refs' (x64KSSKIMPML4 (ksArchState s)) \<union>
|
||||
(\<Union>pt \<in> set (x64KSSKIMPDs (ksArchState s)). table_refs' pt) \<union>
|
||||
(\<Union>pt \<in> set (x64KSSKIMPTs (ksArchState s)). table_refs' pt) \<union>
|
||||
(\<Union>pt \<in> set (x64KSSKIMPDPTs (ksArchState s)). table_refs' pt) \<union>
|
||||
range (\<lambda>irq :: irq. irq_node' s + 32 * ucast irq)"
|
||||
|
||||
definition
|
||||
|
|
@ -1080,6 +1080,13 @@ where
|
|||
"valid_asid_table' table \<equiv> \<lambda>s. dom table \<subseteq> {0 .. 2^asid_high_bits - 1}
|
||||
\<and> 0 \<notin> ran table"
|
||||
|
||||
primrec
|
||||
valid_cr3' :: "cr3 \<Rightarrow> bool"
|
||||
where
|
||||
"valid_cr3' (CR3 addr pcid) = (is_aligned addr asid_bits
|
||||
\<and> addr \<le> mask (pml4ShiftBits + asid_bits)
|
||||
\<and> asid_wf pcid)"
|
||||
|
||||
definition
|
||||
valid_global_pts' :: "machine_word list \<Rightarrow> kernel_state \<Rightarrow> bool"
|
||||
where
|
||||
|
|
@ -1100,10 +1107,11 @@ definition
|
|||
where
|
||||
"valid_arch_state' \<equiv> \<lambda>s.
|
||||
valid_asid_table' (x64KSASIDTable (ksArchState s)) s \<and>
|
||||
page_map_l4_at' (x64KSGlobalPML4 (ksArchState s)) s \<and>
|
||||
valid_global_pds' (x64KSGlobalPDs (ksArchState s)) s \<and>
|
||||
valid_global_pdpts' (x64KSGlobalPDPTs (ksArchState s)) s \<and>
|
||||
valid_global_pts' (x64KSGlobalPTs (ksArchState s)) s"
|
||||
valid_cr3' (x64KSCurrentUserCR3 (ksArchState s)) \<and>
|
||||
page_map_l4_at' (x64KSSKIMPML4 (ksArchState s)) s \<and>
|
||||
valid_global_pds' (x64KSSKIMPDs (ksArchState s)) s \<and>
|
||||
valid_global_pdpts' (x64KSSKIMPDPTs (ksArchState s)) s \<and>
|
||||
valid_global_pts' (x64KSSKIMPTs (ksArchState s)) s"
|
||||
|
||||
definition
|
||||
irq_issued' :: "irq \<Rightarrow> kernel_state \<Rightarrow> bool"
|
||||
|
|
|
|||
|
|
@ -154,7 +154,7 @@ lemma none_in_new_cap_addrs:
|
|||
apply simp+
|
||||
done
|
||||
|
||||
crunch arch_inv[wp]: createNewObjects "\<lambda>s. P (x64KSGlobalPML4 (ksArchState s))"
|
||||
crunch arch_inv[wp]: createNewObjects "\<lambda>s. P (x64KSSKIMPML4 (ksArchState s))"
|
||||
(simp: crunch_simps zipWithM_x_mapM wp: crunch_wps hoare_unless_wp)
|
||||
|
||||
crunch arch_inv[wp]: resetUntypedCap "\<lambda>s. P (ksArchState s)"
|
||||
|
|
@ -165,7 +165,7 @@ crunch arch_inv[wp]: resetUntypedCap "\<lambda>s. P (ksArchState s)"
|
|||
|
||||
lemma is_aligned_x64KSGlobalPD:
|
||||
"valid_arch_state' s
|
||||
\<Longrightarrow> is_aligned (x64KSGlobalPML4 (ksArchState s)) pml4Bits"
|
||||
\<Longrightarrow> is_aligned (x64KSSKIMPML4 (ksArchState s)) pml4Bits"
|
||||
by (clarsimp simp: valid_arch_state'_def page_map_l4_at'_def)
|
||||
|
||||
lemma new_CapTable_bound:
|
||||
|
|
|
|||
|
|
@ -475,11 +475,11 @@ definition
|
|||
where
|
||||
"arch_state_relation \<equiv> {(s, s') .
|
||||
x64_asid_table s = x64KSASIDTable s' o ucast
|
||||
\<and> x64_global_pml4 s = x64KSGlobalPML4 s'
|
||||
\<and> x64_global_pdpts s = x64KSGlobalPDPTs s'
|
||||
\<and> x64_global_pds s = x64KSGlobalPDs s'
|
||||
\<and> x64_global_pts s = x64KSGlobalPTs s'
|
||||
\<and> cr3_relation (x64_current_cr3 s) (x64KSCurrentCR3 s')
|
||||
\<and> x64_global_pml4 s = x64KSSKIMPML4 s'
|
||||
\<and> x64_global_pdpts s = x64KSSKIMPDPTs s'
|
||||
\<and> x64_global_pds s = x64KSSKIMPDs s'
|
||||
\<and> x64_global_pts s = x64KSSKIMPTs s'
|
||||
\<and> cr3_relation (x64_current_cr3 s) (x64KSCurrentUserCR3 s')
|
||||
\<and> x64_kernel_vspace s = x64KSKernelVSpace s'
|
||||
\<and> x64_allocated_io_ports s = x64KSAllocatedIOPorts s'}"
|
||||
|
||||
|
|
|
|||
|
|
@ -293,22 +293,16 @@ lemma no_fail_writeCR3[wp]: "no_fail \<top> (writeCR3 a b)"
|
|||
by (simp add: writeCR3_def)
|
||||
|
||||
lemma set_current_cr3_corres [corres]:
|
||||
"cr3_relation c c' \<Longrightarrow> corres dc \<top> \<top> (set_current_cr3 c) (setCurrentCR3 c')"
|
||||
apply (clarsimp simp add: set_current_cr3_def setCurrentCR3_def cr3_relation_def)
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_split_nor)
|
||||
apply (rule corres_machine_op)
|
||||
apply (rule corres_Id, rule refl, simp)
|
||||
apply (rule no_fail_writeCR3)
|
||||
apply (rule corres_modify')
|
||||
apply (clarsimp simp: state_relation_def arch_state_relation_def cr3_relation_def)
|
||||
apply (simp add: dc_def)
|
||||
apply wpsimp+
|
||||
"cr3_relation c c' \<Longrightarrow> corres dc \<top> \<top> (set_current_cr3 c) (setCurrentUserCR3 c')"
|
||||
apply (clarsimp simp add: set_current_cr3_def setCurrentUserCR3_def cr3_relation_def)
|
||||
apply (rule corres_modify')
|
||||
apply (clarsimp simp: state_relation_def arch_state_relation_def cr3_relation_def)
|
||||
apply simp
|
||||
done
|
||||
|
||||
lemma get_current_cr3_corres [corres]:
|
||||
"corres cr3_relation \<top> \<top> (get_current_cr3) (getCurrentCR3)"
|
||||
apply (simp add: getCurrentCR3_def get_current_cr3_def)
|
||||
"corres cr3_relation \<top> \<top> (get_current_cr3) (getCurrentUserCR3)"
|
||||
apply (simp add: getCurrentUserCR3_def get_current_cr3_def)
|
||||
by (clarsimp simp: state_relation_def arch_state_relation_def)
|
||||
|
||||
lemma set_vm_root_corres [corres]:
|
||||
|
|
@ -325,13 +319,15 @@ proof -
|
|||
(do global_pml4 \<leftarrow> gets (x64_global_pml4 \<circ> arch_state);
|
||||
set_current_vspace_root (X64.addrFromKPPtr global_pml4) 0
|
||||
od)
|
||||
(do globalPML4 \<leftarrow> gets (x64KSGlobalPML4 \<circ> ksArchState);
|
||||
X64_H.setCurrentVSpaceRoot (addrFromKPPtr globalPML4) 0
|
||||
(do globalPML4 \<leftarrow> gets (x64KSSKIMPML4 \<circ> ksArchState);
|
||||
X64_H.setCurrentUserVSpaceRoot (addrFromKPPtr globalPML4) 0
|
||||
od)"
|
||||
apply (simp add: X64_H.setCurrentVSpaceRoot_def set_current_vspace_root_def)
|
||||
apply (simp add: X64_H.setCurrentUserVSpaceRoot_def set_current_vspace_root_def
|
||||
make_cr3_def makeCR3_def)
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_split_eqr)
|
||||
apply (rule set_current_cr3_corres, simp add: cr3_relation_def addrFromKPPtr_def)
|
||||
apply (rule set_current_cr3_corres,
|
||||
simp add: cr3_relation_def cr3_addr_mask_def addrFromKPPtr_def bit_simps)
|
||||
apply (subst corres_gets)
|
||||
apply (clarsimp simp: state_relation_def arch_state_relation_def)
|
||||
apply (wp | simp)+
|
||||
|
|
@ -342,8 +338,8 @@ proof -
|
|||
set_current_vspace_root (X64.addrFromKPPtr global_pml4) 0
|
||||
od))
|
||||
(throwError Fault_H.lookup_failure.InvalidRoot <catch>
|
||||
(\<lambda>_ . do globalPML4 \<leftarrow> gets (x64KSGlobalPML4 \<circ> ksArchState);
|
||||
setCurrentVSpaceRoot (addrFromKPPtr globalPML4) 0
|
||||
(\<lambda>_ . do globalPML4 \<leftarrow> gets (x64KSSKIMPML4 \<circ> ksArchState);
|
||||
setCurrentUserVSpaceRoot (addrFromKPPtr globalPML4) 0
|
||||
od))"
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_split_catch [where f=lfr])
|
||||
|
|
@ -354,6 +350,7 @@ proof -
|
|||
show ?thesis
|
||||
unfolding set_vm_root_def setVMRoot_def getThreadVSpaceRoot_def locateSlot_conv
|
||||
catchFailure_def withoutFailure_def throw_def
|
||||
make_cr3_def makeCR3_def
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_split' [where r'="op = \<circ> cte_map"])
|
||||
apply (simp add: tcbVTableSlot_def cte_map_def objBits_def cte_level_bits_def
|
||||
|
|
@ -379,9 +376,9 @@ proof -
|
|||
apply (simp only: liftE_bindE)
|
||||
apply (rule corres_split'[OF get_current_cr3_corres])
|
||||
apply (rule corres_whenE[OF _ _ dc_simp])
|
||||
apply (case_tac cur_cr3; case_tac curCR3; clarsimp simp: cr3_relation_def)
|
||||
apply (case_tac cur_cr3; case_tac curCR3; clarsimp simp: cr3_relation_def cr3_addr_mask_def)
|
||||
apply (rule iffD2[OF corres_liftE_rel_sum, OF set_current_cr3_corres])
|
||||
apply (simp add: cr3_relation_def)
|
||||
apply (simp add: cr3_relation_def cr3_addr_mask_def)
|
||||
apply wp
|
||||
apply wpsimp
|
||||
apply simp
|
||||
|
|
@ -840,22 +837,24 @@ crunch valid_arch'[wp]: storePDE, storePTE, storePDPTE, storePML4E valid_arch_st
|
|||
crunch cur_tcb'[wp]: storePDE, storePTE, storePDPTE, storePML4E cur_tcb'
|
||||
(ignore: setObject)
|
||||
|
||||
lemma getCurrentCR3_inv: "\<lbrace>P\<rbrace> getCurrentCR3 \<lbrace>\<lambda>_. P\<rbrace>"
|
||||
by (simp add: getCurrentCR3_def)
|
||||
lemma getCurrentUserCR3_inv[wp]: "\<lbrace>P\<rbrace> getCurrentUserCR3 \<lbrace>\<lambda>_. P\<rbrace>"
|
||||
by (simp add: getCurrentUserCR3_def)
|
||||
|
||||
lemma invalidate_local_page_structure_cache_asid_corres:
|
||||
lemma invalidatePageStructureCacheASID_corres' [corres]:
|
||||
assumes "vspace' = vspace" "asid' = asid"
|
||||
shows
|
||||
"corres dc \<top> \<top>
|
||||
(invalidate_local_page_structure_cache_asid a b)
|
||||
(X64_H.invalidateLocalPageStructureCacheASID a b)"
|
||||
apply (simp add: invalidate_local_page_structure_cache_asid_def
|
||||
X64_H.invalidateLocalPageStructureCacheASID_def)
|
||||
by (corressimp corres: get_current_cr3_corres set_current_cr3_corres
|
||||
wp: get_current_cr3_inv getCurrentCR3_inv
|
||||
simp: cr3_relation_def)
|
||||
(invalidate_page_structure_cache_asid vspace asid)
|
||||
(X64_H.invalidatePageStructureCacheASID vspace' asid')"
|
||||
by (corressimp simp: invalidate_page_structure_cache_asid_def
|
||||
X64_H.invalidatePageStructureCacheASID_def
|
||||
invalidateLocalPageStructureCacheASID_def
|
||||
assms ucast_id
|
||||
corres: corres_machine_op
|
||||
wp: no_fail_machine_op_lift)
|
||||
|
||||
lemmas invalidatePageStructureCacheASID_corres = invalidate_local_page_structure_cache_asid_corres
|
||||
[folded invalidatePageStructureCacheASID_def]
|
||||
lemmas invalidatePageStructureCacheASID_corres =
|
||||
invalidatePageStructureCacheASID_corres'[OF refl refl]
|
||||
|
||||
(* FIXME x64: move *)
|
||||
lemma flush_table_pde_at[wp]: "\<lbrace>pde_at p\<rbrace> flush_table a b c d \<lbrace>\<lambda>_. pde_at p\<rbrace>"
|
||||
|
|
@ -1201,7 +1200,7 @@ proof -
|
|||
apply (rule corres_split[OF _ store_pte_corres'])
|
||||
apply (rule corres_split[where r'="op ="])
|
||||
apply simp
|
||||
apply (rule invalidate_local_page_structure_cache_asid_corres)
|
||||
apply (rule invalidatePageStructureCacheASID_corres)
|
||||
apply (case_tac cap; clarsimp simp add: is_pg_cap_def)
|
||||
apply (case_tac m; clarsimp)
|
||||
apply (rule corres_fail[where P=\<top> and P'=\<top>])
|
||||
|
|
@ -1215,7 +1214,7 @@ proof -
|
|||
apply (rule corres_split[OF _ store_pde_corres'])
|
||||
apply (rule corres_split[where r'="op ="])
|
||||
apply simp
|
||||
apply (rule invalidate_local_page_structure_cache_asid_corres)
|
||||
apply (rule invalidatePageStructureCacheASID_corres)
|
||||
apply (case_tac cap; clarsimp simp add: is_pg_cap_def)
|
||||
apply (case_tac m; clarsimp)
|
||||
apply (rule corres_fail[where P=\<top> and P'=\<top>])
|
||||
|
|
@ -1229,7 +1228,7 @@ proof -
|
|||
apply (rule corres_split[OF _ store_pdpte_corres'])
|
||||
apply (rule corres_split[where r'="op ="])
|
||||
apply simp
|
||||
apply (rule invalidate_local_page_structure_cache_asid_corres)
|
||||
apply (rule invalidatePageStructureCacheASID_corres)
|
||||
apply (case_tac cap; clarsimp simp add: is_pg_cap_def)
|
||||
apply (case_tac m; clarsimp)
|
||||
apply (rule corres_fail[where P=\<top> and P'=\<top>])
|
||||
|
|
@ -1252,19 +1251,19 @@ proof -
|
|||
apply (clarsimp simp: mapping_map_simps)
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_split[OF _ store_pte_corres'])
|
||||
apply (rule invalidate_local_page_structure_cache_asid_corres)
|
||||
apply (rule invalidatePageStructureCacheASID_corres)
|
||||
apply (wpsimp simp: invs_pspace_aligned')+
|
||||
apply (frule (1) mapping_map_pde, clarsimp)
|
||||
apply (clarsimp simp: mapping_map_simps)
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_split[OF _ store_pde_corres'])
|
||||
apply (rule invalidate_local_page_structure_cache_asid_corres)
|
||||
apply (rule invalidatePageStructureCacheASID_corres)
|
||||
apply (wpsimp simp: invs_pspace_aligned')+
|
||||
apply (frule (1) mapping_map_pdpte, clarsimp)
|
||||
apply (clarsimp simp: mapping_map_simps)
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_split[OF _ store_pdpte_corres'])
|
||||
apply (rule invalidate_local_page_structure_cache_asid_corres)
|
||||
apply (rule invalidatePageStructureCacheASID_corres)
|
||||
apply (wpsimp simp: invs_pspace_aligned')+
|
||||
-- "PageUnmap"
|
||||
apply (clarsimp simp: performPageInvocation_def perform_page_invocation_def
|
||||
|
|
@ -1549,13 +1548,12 @@ lemma unmap_pd_corres:
|
|||
notes liftE_get_pdpte_corres = get_pdpte_corres'[THEN corres_liftE_rel_sum[THEN iffD2]]
|
||||
shows "corres dc
|
||||
(invs and valid_etcbs and page_directory_at pd and
|
||||
K (0 < asid \<and> is_aligned vptr pdpt_shift_bits \<and> vptr < pptr_base \<and> canonical_address vptr \<and> asid \<le> mask asid_bits))
|
||||
K (0 < asid \<and> is_aligned vptr pdpt_shift_bits \<and> vptr < pptr_base \<and> canonical_address vptr \<and> asid_wf asid))
|
||||
(valid_arch_state' and pspace_aligned' and pspace_distinct'
|
||||
and no_0_obj' and cur_tcb' and valid_objs')
|
||||
(unmap_pd asid vptr pd)
|
||||
(unmapPageDirectory asid' vptr' pd')"
|
||||
apply (clarsimp simp: assms unmap_pd_def unmapPageDirectory_def flushPD_def
|
||||
invalidatePageStructureCacheASID_def
|
||||
ignoreFailure_def const_def)
|
||||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_split_catch[where E="\<top>\<top>" and E'="\<top>\<top>"], simp)
|
||||
|
|
@ -1570,7 +1568,7 @@ lemma unmap_pd_corres:
|
|||
split: X64_A.pdpte.splits)
|
||||
apply simp
|
||||
apply (rule corres_split_nor[OF _ flush_all_corres[OF refl refl]])
|
||||
apply (rule corres_split[OF invalidate_local_page_structure_cache_asid_corres
|
||||
apply (rule corres_split[OF invalidatePageStructureCacheASID_corres
|
||||
store_pdpte_corres'])
|
||||
apply ((wpsimp wp: get_pdpte_wp simp: pdpte_at_def)+)[8]
|
||||
apply (wpsimp wp: hoare_drop_imps)
|
||||
|
|
@ -1844,14 +1842,14 @@ lemma pap_corres:
|
|||
valid_apinv'_def cte_wp_at'_def)
|
||||
qed
|
||||
|
||||
lemma setCurrentCR3_obj_at [wp]:
|
||||
"\<lbrace>\<lambda>s. P (obj_at' P' t s)\<rbrace> setCurrentCR3 c \<lbrace>\<lambda>rv s. P (obj_at' P' t s)\<rbrace>"
|
||||
apply (simp add: setCurrentCR3_def)
|
||||
lemma setCurrentUserCR3_obj_at [wp]:
|
||||
"\<lbrace>\<lambda>s. P (obj_at' P' t s)\<rbrace> setCurrentUserCR3 c \<lbrace>\<lambda>rv s. P (obj_at' P' t s)\<rbrace>"
|
||||
apply (simp add: setCurrentUserCR3_def)
|
||||
apply (wp doMachineOp_obj_at|wpc|simp)+
|
||||
done
|
||||
|
||||
lemmas getCurrentCR3_obj_at [wp]
|
||||
= getCurrentCR3_inv[of "\<lambda>s. P (obj_at' P' t s)" for P P' t]
|
||||
lemmas getCurrentUserCR3_obj_at [wp]
|
||||
= getCurrentUserCR3_inv[of "\<lambda>s. P (obj_at' P' t s)" for P P' t]
|
||||
|
||||
crunch obj_at[wp]: setVMRoot "\<lambda>s. P (obj_at' P' t s)"
|
||||
(simp: crunch_simps)
|
||||
|
|
@ -1888,45 +1886,51 @@ lemma valid_ioports_cr3_update[elim!]:
|
|||
"valid_ioports' s \<Longrightarrow> valid_ioports' (s\<lparr>ksArchState := x64KSCurrentCR3_update (\<lambda>_. c) (ksArchState s)\<rparr>)"
|
||||
by (clarsimp simp: valid_ioports'_simps)
|
||||
|
||||
lemma setCurrentCR3_invs' [wp]: "\<lbrace>invs'\<rbrace> setCurrentCR3 c \<lbrace>\<lambda>rv. invs'\<rbrace>"
|
||||
unfolding setCurrentCR3_def
|
||||
apply (wpsimp wp:)
|
||||
lemma setCurrentUserCR3_invs' [wp]:
|
||||
"\<lbrace>invs' and K (valid_cr3' c)\<rbrace> setCurrentUserCR3 c \<lbrace>\<lambda>rv. invs'\<rbrace>"
|
||||
unfolding setCurrentUserCR3_def
|
||||
apply wpsimp
|
||||
by (clarsimp simp: invs'_def valid_state'_def valid_global_refs'_def global_refs'_def
|
||||
valid_arch_state'_def valid_machine_state'_def ct_not_inQ_def
|
||||
ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def)
|
||||
|
||||
lemma getCurrentCR3_invs' [wp]: "\<lbrace>invs'\<rbrace> getCurrentCR3 \<lbrace>\<lambda>rv. invs'\<rbrace>"
|
||||
unfolding getCurrentCR3_def
|
||||
by (wpsimp)
|
||||
lemma setCurrentUserCR3_invs_no_cicd' [wp]:
|
||||
"\<lbrace>invs_no_cicd' and K (valid_cr3' c)\<rbrace> setCurrentUserCR3 c \<lbrace>\<lambda>rv. invs_no_cicd'\<rbrace>"
|
||||
unfolding setCurrentUserCR3_def
|
||||
apply wpsimp
|
||||
by (clarsimp simp: all_invs_but_ct_idle_or_in_cur_domain'_def valid_state'_def
|
||||
valid_global_refs'_def global_refs'_def
|
||||
valid_arch_state'_def valid_machine_state'_def ct_not_inQ_def
|
||||
ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def)
|
||||
|
||||
lemma setCurrentCR3_invs_no_cicd' [wp]: "\<lbrace>invs_no_cicd'\<rbrace> setCurrentCR3 c \<lbrace>\<lambda>rv. invs_no_cicd'\<rbrace>"
|
||||
unfolding setCurrentCR3_def
|
||||
apply (wpsimp wp:)
|
||||
by (clarsimp simp: all_invs_but_ct_idle_or_in_cur_domain'_def valid_state'_def valid_global_refs'_def global_refs'_def
|
||||
valid_arch_state'_def valid_machine_state'_def ct_not_inQ_def
|
||||
ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def)
|
||||
|
||||
lemma getCurrentCR3_invs_no_cicd' [wp]: "\<lbrace>invs_no_cicd'\<rbrace> getCurrentCR3 \<lbrace>\<lambda>rv. invs_no_cicd'\<rbrace>"
|
||||
unfolding getCurrentCR3_def
|
||||
by (wpsimp)
|
||||
lemma valid_cr3'_makeCR3:
|
||||
"asid_wf asid \<Longrightarrow> valid_cr3' (makeCR3 addr asid)"
|
||||
apply (clarsimp simp: valid_cr3'_def makeCR3_def bit_simps
|
||||
is_aligned_andI2[OF is_aligned_shift])
|
||||
apply (rule order.trans[OF word_and_le1])
|
||||
apply (simp add: mask_def asid_bits_def)
|
||||
done
|
||||
|
||||
lemma getCurrentUserCR3_wp:
|
||||
"\<lbrace> \<lambda>s. Q (x64KSCurrentUserCR3 (ksArchState s)) s \<rbrace> getCurrentUserCR3 \<lbrace> Q \<rbrace>"
|
||||
by (wpsimp simp: getCurrentUserCR3_def)
|
||||
|
||||
lemma setVMRoot_invs [wp]:
|
||||
"\<lbrace>invs'\<rbrace> setVMRoot p \<lbrace>\<lambda>rv. invs'\<rbrace>"
|
||||
apply (simp add: setVMRoot_def getThreadVSpaceRoot_def setCurrentVSpaceRoot_def )
|
||||
apply (rule hoare_pre)
|
||||
apply (wp hoare_whenE_wp | wpcw | clarsimp cong: if_cong)+
|
||||
apply (rule_tac Q'="\<lambda>rv. invs'" in hoare_post_imp_R)
|
||||
apply (wpsimp)+
|
||||
apply (simp add: setVMRoot_def getThreadVSpaceRoot_def setCurrentUserVSpaceRoot_def)
|
||||
apply (wp hoare_whenE_wp getCurrentUserCR3_wp findVSpaceForASID_vs_at_wp
|
||||
| wpcw
|
||||
| clarsimp simp: if_apply_def2 asid_wf_0
|
||||
| strengthen valid_cr3'_makeCR3)+
|
||||
done
|
||||
|
||||
lemma setVMRoot_invs_no_cicd':
|
||||
"\<lbrace>invs_no_cicd'\<rbrace> setVMRoot p \<lbrace>\<lambda>rv. invs_no_cicd'\<rbrace>"
|
||||
apply (simp add: setVMRoot_def getThreadVSpaceRoot_def setCurrentVSpaceRoot_def)
|
||||
apply (rule hoare_pre)
|
||||
apply (wp hoare_whenE_wp | wpcw | clarsimp cong: if_cong)+
|
||||
apply (rule_tac Q'="\<lambda>rv. invs_no_cicd'" in hoare_post_imp_R)
|
||||
apply (wpsimp)+
|
||||
apply (simp add: setVMRoot_def getThreadVSpaceRoot_def setCurrentUserVSpaceRoot_def)
|
||||
apply (wp hoare_whenE_wp getCurrentUserCR3_wp findVSpaceForASID_vs_at_wp
|
||||
| wpcw
|
||||
| clarsimp simp: if_apply_def2 asid_wf_0
|
||||
| strengthen valid_cr3'_makeCR3)+
|
||||
done
|
||||
|
||||
crunch nosch [wp]: setVMRoot "\<lambda>s. P (ksSchedulerAction s)"
|
||||
|
|
@ -2861,11 +2865,14 @@ lemma dmo_invalidateASID_invs'[wp]:
|
|||
machine_rest_lift_def split_def | wp)+
|
||||
done
|
||||
|
||||
lemma x64KSCurrentCR3_update_inv[simp]:
|
||||
"invs' s \<Longrightarrow> invs' (s\<lparr>ksArchState := x64KSCurrentCR3_update (\<lambda>_. c) (ksArchState s)\<rparr>)"
|
||||
by (clarsimp simp: invs'_def valid_state'_def valid_global_refs'_def global_refs'_def
|
||||
valid_arch_state'_def valid_machine_state'_def ct_not_inQ_def
|
||||
ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def)
|
||||
lemma dmo_invalidateLocalPageStructureCacheASID_invs'[wp]:
|
||||
"\<lbrace>invs'\<rbrace> doMachineOp (invalidateLocalPageStructureCacheASID vspace asid) \<lbrace>\<lambda>_. invs'\<rbrace>"
|
||||
apply (wpsimp wp: dmo_invs' invalidateLocalPageStructureCacheASID_irq_masks)
|
||||
apply (drule_tac P4="\<lambda>m'. underlying_memory m' p = underlying_memory m p"
|
||||
in use_valid[where P=P and Q="\<lambda>_. P" for P])
|
||||
apply (simp add: invalidateLocalPageStructureCacheASID_def machine_op_lift_def
|
||||
machine_rest_lift_def split_def | wp)+
|
||||
done
|
||||
|
||||
crunch invs'[wp]: unmapPageTable, unmapPageDirectory, unmapPDPT "invs'"
|
||||
(ignore: getObject setObject storePDE storePDPTE storePML4E doMachineOp
|
||||
|
|
|
|||
|
|
@ -214,10 +214,6 @@ definition
|
|||
|
||||
section "Basic Operations"
|
||||
|
||||
text {* The kernel window is mapped into every virtual address space from the
|
||||
@{term kernel_base} pointer upwards. This function copies the mappings which
|
||||
create the kernel window into a new page directory object. *}
|
||||
|
||||
definition
|
||||
get_pt_index :: "vspace_ref \<Rightarrow> machine_word" where
|
||||
"get_pt_index vptr \<equiv> (vptr >> pt_shift_bits) && mask ptTranslationBits"
|
||||
|
|
@ -234,6 +230,10 @@ definition
|
|||
get_pml4_index :: "vspace_ref \<Rightarrow> machine_word" where
|
||||
"get_pml4_index vptr \<equiv> (vptr >> pml4_shift_bits) && mask ptTranslationBits"
|
||||
|
||||
text {* The kernel window is mapped into every virtual address space from the
|
||||
@{term pptr_base} pointer upwards. This function copies the mappings which
|
||||
create the kernel window into a new page directory object. *}
|
||||
|
||||
definition
|
||||
copy_global_mappings :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where
|
||||
"copy_global_mappings new_pm \<equiv> do
|
||||
|
|
|
|||
|
|
@ -157,21 +157,14 @@ where
|
|||
definition
|
||||
set_current_cr3 :: "cr3 \<Rightarrow> (unit,'z::state_ext) s_monad"
|
||||
where
|
||||
"set_current_cr3 c \<equiv> do
|
||||
modify (\<lambda>s. s \<lparr>arch_state := (arch_state s) \<lparr>x64_current_cr3 := c\<rparr>\<rparr>);
|
||||
do_machine_op $ writeCR3 (cr3_base_address c) (cr3_pcid c)
|
||||
od"
|
||||
"set_current_cr3 c \<equiv>
|
||||
modify (\<lambda>s. s \<lparr>arch_state := (arch_state s) \<lparr>x64_current_cr3 := c\<rparr>\<rparr>)"
|
||||
|
||||
definition
|
||||
invalidate_local_page_structure_cache_asid :: "obj_ref \<Rightarrow> asid \<Rightarrow> (unit, 'z::state_ext) s_monad"
|
||||
invalidate_page_structure_cache_asid :: "obj_ref \<Rightarrow> asid \<Rightarrow> (unit, 'z::state_ext) s_monad"
|
||||
where
|
||||
"invalidate_local_page_structure_cache_asid vspace asid \<equiv> do
|
||||
cur_cr3 \<leftarrow> get_current_cr3;
|
||||
set_current_cr3 (cr3 vspace asid);
|
||||
set_current_cr3 cur_cr3
|
||||
od"
|
||||
|
||||
abbreviation "invalidate_page_structure_cache_asid \<equiv> invalidate_local_page_structure_cache_asid"
|
||||
"invalidate_page_structure_cache_asid vspace asid \<equiv>
|
||||
do_machine_op $ invalidateLocalPageStructureCacheASID vspace (ucast asid)"
|
||||
|
||||
definition
|
||||
getCurrentVSpaceRoot :: "(obj_ref, 'z::state_ext) s_monad"
|
||||
|
|
@ -181,10 +174,18 @@ where
|
|||
return $ cr3_base_address cur
|
||||
od"
|
||||
|
||||
definition
|
||||
"cr3_addr_mask \<equiv> mask pml4_shift_bits << asid_bits"
|
||||
|
||||
definition
|
||||
make_cr3 :: "obj_ref \<Rightarrow> asid \<Rightarrow> cr3"
|
||||
where
|
||||
"make_cr3 vspace asid \<equiv> cr3 (vspace && cr3_addr_mask) asid"
|
||||
|
||||
definition
|
||||
set_current_vspace_root :: "obj_ref \<Rightarrow> asid \<Rightarrow> (unit, 'z::state_ext) s_monad"
|
||||
where
|
||||
"set_current_vspace_root vspace asid \<equiv> set_current_cr3 $ cr3 vspace asid"
|
||||
"set_current_vspace_root vspace asid \<equiv> set_current_cr3 $ make_cr3 vspace asid"
|
||||
|
||||
text {* Switch into the address space of a given thread or the global address
|
||||
space if none is correctly configured. *}
|
||||
|
|
@ -198,8 +199,8 @@ definition
|
|||
pml4' \<leftarrow> find_vspace_for_asid asid;
|
||||
whenE (pml4 \<noteq> pml4') $ throwError InvalidRoot;
|
||||
cur_cr3 \<leftarrow> liftE $ get_current_cr3;
|
||||
whenE (cur_cr3 \<noteq> cr3 (addrFromPPtr pml4) asid) $
|
||||
liftE $ set_current_cr3 $ cr3 (addrFromPPtr pml4) asid
|
||||
whenE (cur_cr3 \<noteq> make_cr3 (addrFromPPtr pml4) asid) $
|
||||
liftE $ set_current_cr3 $ make_cr3 (addrFromPPtr pml4) asid
|
||||
odE
|
||||
| _ \<Rightarrow> throwError InvalidRoot) <catch>
|
||||
(\<lambda>_. do
|
||||
|
|
|
|||
|
|
@ -52,17 +52,15 @@ datatype arch_cap =
|
|||
(* cr3 Stuff *)
|
||||
datatype cr3 = cr3 obj_ref asid
|
||||
|
||||
primrec cr3_base_address where
|
||||
"cr3_base_address (cr3 v0 _) = v0"
|
||||
primrec
|
||||
cr3_base_address :: "cr3 \<Rightarrow> obj_ref"
|
||||
where
|
||||
"cr3_base_address (cr3 addr _) = addr"
|
||||
|
||||
primrec cr3_base_address_update where
|
||||
"cr3_base_address_update f (cr3 v0 v1) = (cr3 (f v0) v1)"
|
||||
|
||||
primrec cr3_pcid where
|
||||
"cr3_pcid (cr3 _ v1) = v1"
|
||||
|
||||
primrec cr3_pcid_update where
|
||||
"cr3_pcid_update f (cr3 v0 v1) = (cr3 v0 (f v1))"
|
||||
primrec
|
||||
cr3_pcid :: "cr3 \<Rightarrow> asid"
|
||||
where
|
||||
"cr3_pcid (cr3 _ pcid) = pcid"
|
||||
|
||||
section {* Architecture-specific objects *}
|
||||
|
||||
|
|
|
|||
|
|
@ -121,13 +121,13 @@ definition
|
|||
(* Virtual address space available to users. *)
|
||||
definition
|
||||
user_vtop :: "machine_word" where
|
||||
"user_vtop = 0x00007fffffffffff"
|
||||
"user_vtop = Platform.X64.pptrUserTop"
|
||||
|
||||
text {* The lowest virtual address in the kernel window. The kernel reserves the
|
||||
virtual addresses from here up in every virtual address space. *}
|
||||
definition
|
||||
kernel_base :: "vspace_ref" where
|
||||
"kernel_base \<equiv> 0xffffffffc0000000"
|
||||
"kernel_base \<equiv> 0xffffffff80000000"
|
||||
|
||||
definition
|
||||
idle_thread_ptr :: vspace_ref where
|
||||
|
|
|
|||
|
|
@ -118,7 +118,7 @@ definition
|
|||
device_state = empty,
|
||||
machine_state_rest = undefined \<rparr>"
|
||||
|
||||
#INCLUDE_HASKELL SEL4/Machine/Hardware/X64.lhs CONTEXT X64 ONLY HardwareASID VMFaultType HypFaultType VMPageSize VMMapType pageBits ptTranslationBits pageBitsForSize
|
||||
#INCLUDE_HASKELL SEL4/Machine/Hardware/X64.lhs CONTEXT X64 ONLY VMFaultType HypFaultType VMPageSize VMMapType pageBits ptTranslationBits pageBitsForSize
|
||||
|
||||
end
|
||||
|
||||
|
|
@ -128,7 +128,7 @@ end
|
|||
|
||||
context Arch begin global_naming X64
|
||||
|
||||
#INCLUDE_HASKELL SEL4/Machine/Hardware/X64.lhs CONTEXT X64 instanceproofs ONLY HardwareASID VMFaultType HypFaultType VMPageSize VMMapType
|
||||
#INCLUDE_HASKELL SEL4/Machine/Hardware/X64.lhs CONTEXT X64 instanceproofs ONLY VMFaultType HypFaultType VMPageSize VMMapType
|
||||
|
||||
end
|
||||
end
|
||||
|
|
|
|||
|
|
@ -16,7 +16,7 @@ begin
|
|||
|
||||
context Arch begin global_naming X64_H
|
||||
|
||||
#INCLUDE_HASKELL SEL4/Machine/Hardware/X64.lhs Platform=Platform.X64 CONTEXT X64_H NOT getMemoryRegions getDeviceRegions getKernelDevices loadWord storeWord storeWordVM getActiveIRQ ackInterrupt maskInterrupt configureTimer resetTimer debugPrint getRestartPC setNextPC clearMemory clearMemoryVM initMemory freeMemory setCurrentPD setGlobalPD setHardwareASID wordFromPDE wordFromPTE VMFaultType HypFaultType VMMapType VMPageSize pageBits pageBitsForSize toPAddr addrFromPPtr ptrFromPAddr setCurrentCR3 getCurrentCR3 invalidateTLB invalidateTLBEntry mfence wordFromPML4E wordFromPDPTE firstValidIODomain numIODomainIDBits hwASIDInvalidate getFaultAddress irqIntOffset maxPCIBus maxPCIDev maxPCIFunc numIOAPICs ioapicIRQLines ioapicMapPinToVector irqStateIRQIOAPICNew irqStateIRQMSINew updateIRQState X64IRQState in8 out8 in16 out16 in32 out32 invalidatePageStructureCache resetCR3 physBase archSetCurrentVSpaceRoot writeCR3 invalidateASID invalidateTranslationSingleASID invalidatePageStructureCacheASID ptTranslationBits
|
||||
#INCLUDE_HASKELL SEL4/Machine/Hardware/X64.lhs Platform=Platform.X64 CONTEXT X64_H NOT getMemoryRegions getDeviceRegions getKernelDevices loadWord storeWord storeWordVM getActiveIRQ ackInterrupt maskInterrupt configureTimer resetTimer debugPrint getRestartPC setNextPC clearMemory clearMemoryVM initMemory freeMemory wordFromPDE wordFromPTE VMFaultType HypFaultType VMMapType VMPageSize pageBits pageBitsForSize toPAddr addrFromPPtr ptrFromPAddr setCurrentUserCR3 getCurrentUserCR3 invalidateTLB invalidateTLBEntry mfence wordFromPML4E wordFromPDPTE firstValidIODomain numIODomainIDBits hwASIDInvalidate getFaultAddress irqIntOffset maxPCIBus maxPCIDev maxPCIFunc numIOAPICs ioapicIRQLines ioapicMapPinToVector irqStateIRQIOAPICNew irqStateIRQMSINew updateIRQState X64IRQState in8 out8 in16 out16 in32 out32 invalidatePageStructureCache writeCR3 invalidateASID invalidateTranslationSingleASID invalidateLocalPageStructureCacheASID ptTranslationBits
|
||||
|
||||
end
|
||||
|
||||
|
|
@ -26,7 +26,7 @@ end
|
|||
|
||||
context Arch begin global_naming X64_H
|
||||
|
||||
#INCLUDE_HASKELL SEL4/Machine/Hardware/X64.lhs CONTEXT X64_H instanceproofs NOT HardwareASID VMFaultType VMPageSize VMPageEntry VMMapType HypFaultType
|
||||
#INCLUDE_HASKELL SEL4/Machine/Hardware/X64.lhs CONTEXT X64_H instanceproofs NOT VMFaultType VMPageSize VMPageEntry VMMapType HypFaultType
|
||||
|
||||
#INCLUDE_HASKELL SEL4/Machine/Hardware/X64.lhs CONTEXT X64_H ONLY wordFromPDE wordFromPTE wordFromPML4E wordFromPDPTE
|
||||
|
||||
|
|
|
|||
|
|
@ -64,13 +64,13 @@ When a new page directory is created, the kernel copies all of the global mappin
|
|||
|
||||
> copyGlobalMappings :: PPtr PML4E -> Kernel ()
|
||||
> copyGlobalMappings newPM = do
|
||||
> globalPM <- gets (x64KSGlobalPML4 . ksArchState)
|
||||
> skimPM <- gets (x64KSSKIMPML4 . ksArchState)
|
||||
> let base = getPML4Index pptrBase
|
||||
> let pml4eBits = objBits (undefined :: PML4E) -- = 3, size of word
|
||||
> let pmSize = 1 `shiftL` ptTranslationBits -- 512 entries in table
|
||||
> forM_ [base .. pmSize - 1] $ \index -> do
|
||||
> let offset = PPtr index `shiftL` pml4eBits
|
||||
> pml4e <- getObject $ globalPM + offset
|
||||
> pml4e <- getObject $ skimPM + offset
|
||||
> storePML4E (newPM + offset) pml4e
|
||||
|
||||
> createMappingEntries :: PAddr -> VPtr ->
|
||||
|
|
@ -414,35 +414,19 @@ This helper function checks that the mapping installed at a given PT or PD slot
|
|||
|
||||
\subsection{Address Space Switching}
|
||||
|
||||
> getCurrentCR3 :: Kernel CR3
|
||||
> getCurrentCR3 = gets (x64KSCurrentCR3 . ksArchState)
|
||||
> getCurrentUserCR3 :: Kernel CR3
|
||||
> getCurrentUserCR3 = gets (x64KSCurrentUserCR3 . ksArchState)
|
||||
|
||||
> setCurrentCR3 :: CR3 -> Kernel ()
|
||||
> setCurrentCR3 cr3 = do
|
||||
> modify (\s -> s { ksArchState = (ksArchState s) { x64KSCurrentCR3 = cr3 }})
|
||||
> doMachineOp $ writeCR3 (cr3BaseAddress cr3) $ fromASID $ cr3pcid cr3
|
||||
|
||||
> invalidateLocalPageStructureCacheASID :: PAddr -> ASID -> Kernel ()
|
||||
> invalidateLocalPageStructureCacheASID ptr asid = do
|
||||
> curCR3 <- getCurrentCR3
|
||||
> setCurrentCR3 (CR3 ptr asid)
|
||||
> setCurrentCR3 curCR3
|
||||
> setCurrentUserCR3 :: CR3 -> Kernel ()
|
||||
> setCurrentUserCR3 cr3 =
|
||||
> modify (\s -> s { ksArchState = (ksArchState s) { x64KSCurrentUserCR3 = cr3 }})
|
||||
|
||||
> invalidatePageStructureCacheASID :: PAddr -> ASID -> Kernel ()
|
||||
> invalidatePageStructureCacheASID p a = invalidateLocalPageStructureCacheASID p a
|
||||
> invalidatePageStructureCacheASID p a = doMachineOp $ invalidateLocalPageStructureCacheASID p (fromASID a)
|
||||
|
||||
> getCurrentVSpaceRoot :: Kernel PAddr
|
||||
> getCurrentVSpaceRoot = do
|
||||
> cur <- getCurrentCR3
|
||||
> return $ cr3BaseAddress cur
|
||||
> setCurrentUserVSpaceRoot :: PAddr -> ASID -> Kernel ()
|
||||
> setCurrentUserVSpaceRoot vspace asid = setCurrentUserCR3 $ makeCR3 vspace asid
|
||||
|
||||
> setCurrentVSpaceRoot :: PAddr -> ASID -> Kernel ()
|
||||
> setCurrentVSpaceRoot vspace asid = setCurrentCR3 $ CR3 vspace asid
|
||||
|
||||
> -- FIXME x64: Currently we don't have global state for the CR3 so
|
||||
> -- we can't test whether or not we should write to it. We should
|
||||
> -- add global state to remember the CR3 and actually avoid the write/flush
|
||||
> -- when we can.
|
||||
> setVMRoot :: PPtr TCB -> Kernel ()
|
||||
> setVMRoot tcb = do
|
||||
> threadRootSlot <- getThreadVSpaceRoot tcb
|
||||
|
|
@ -451,16 +435,16 @@ This helper function checks that the mapping installed at a given PT or PD slot
|
|||
> (case threadRoot of
|
||||
> ArchObjectCap (PML4Cap {
|
||||
> capPML4MappedASID = Just asid,
|
||||
> capPML4BasePtr = pd }) -> do
|
||||
> pd' <- findVSpaceForASID asid
|
||||
> when (pd /= pd') $ throw InvalidRoot
|
||||
> curCR3 <- withoutFailure $ getCurrentCR3
|
||||
> when (curCR3 /= CR3 (addrFromPPtr pd) asid) $
|
||||
> withoutFailure $ setCurrentCR3 $ CR3 (addrFromPPtr pd) asid
|
||||
> capPML4BasePtr = pml4 }) -> do
|
||||
> pml4' <- findVSpaceForASID asid
|
||||
> when (pml4 /= pml4') $ throw InvalidRoot
|
||||
> curCR3 <- withoutFailure $ getCurrentUserCR3
|
||||
> when (curCR3 /= makeCR3 (addrFromPPtr pml4) asid) $
|
||||
> withoutFailure $ setCurrentUserCR3 $ makeCR3 (addrFromPPtr pml4) asid
|
||||
> _ -> throw InvalidRoot)
|
||||
> (\_ -> do
|
||||
> globalPML4 <- gets (x64KSGlobalPML4 . ksArchState)
|
||||
> setCurrentVSpaceRoot (addrFromKPPtr globalPML4) 0)
|
||||
> skimPML4 <- gets (x64KSSKIMPML4 . ksArchState)
|
||||
> setCurrentUserVSpaceRoot (addrFromKPPtr skimPML4) 0)
|
||||
|
||||
\subsection{Helper Functions}
|
||||
|
||||
|
|
@ -1186,7 +1170,7 @@ Checking virtual address for page size dependent alignment:
|
|||
> asid <- case cap of
|
||||
> ArchObjectCap (PageCap _ _ _ _ _ (Just (as, _))) -> return as
|
||||
> _ -> fail "impossible"
|
||||
> invalidateLocalPageStructureCacheASID (addrFromPPtr vspace) asid
|
||||
> invalidatePageStructureCacheASID (addrFromPPtr vspace) asid
|
||||
>
|
||||
> performPageInvocation (PageRemap entries asid vspace) = do
|
||||
> case entries of
|
||||
|
|
@ -1194,7 +1178,7 @@ Checking virtual address for page size dependent alignment:
|
|||
> (VMPDE pde, VMPDEPtr slot) -> storePDE slot pde
|
||||
> (VMPDPTE pdpte, VMPDPTEPtr slot) -> storePDPTE slot pdpte
|
||||
> _ -> fail "impossible"
|
||||
> invalidateLocalPageStructureCacheASID (addrFromPPtr vspace) asid
|
||||
> invalidatePageStructureCacheASID (addrFromPPtr vspace) asid
|
||||
>
|
||||
> performPageInvocation (PageUnmap cap ctSlot) = do
|
||||
> case capVPMappedAddress cap of
|
||||
|
|
|
|||
|
|
@ -214,8 +214,3 @@ The constant "nullPointer" is a physical pointer guaranteed to be invalid.
|
|||
> nullPointer :: PPtr a
|
||||
> nullPointer = PPtr 0
|
||||
|
||||
|
||||
> physBase :: PAddr
|
||||
> physBase = Arch.physBase
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -254,9 +254,6 @@ caches must be done separately.
|
|||
> writeCR3 :: PAddr -> Word64 -> MachineMonad ()
|
||||
> writeCR3 vspace asid = Platform.writeCR3 vspace asid
|
||||
|
||||
> resetCR3 :: MachineMonad ()
|
||||
> resetCR3 = Platform.resetCR3
|
||||
|
||||
\subsubsection{Memory Barriers}
|
||||
|
||||
> mfence :: MachineMonad ()
|
||||
|
|
@ -279,6 +276,9 @@ caches must be done separately.
|
|||
> invalidateTranslationSingleASID :: VPtr -> Word64 -> MachineMonad ()
|
||||
> invalidateTranslationSingleASID vspace asid = Platform.invalidateTranslationSingleASID vspace asid
|
||||
|
||||
> invalidateLocalPageStructureCacheASID :: PAddr -> Word64 -> MachineMonad ()
|
||||
> invalidateLocalPageStructureCacheASID paddr asid = liftIO $ Platform.invalidateLocalPageStructureCacheASID paddr asid
|
||||
|
||||
\subsubsection{Page Table Structure}
|
||||
|
||||
The x64 architecture defines a four-level hardware-walked page table. The kernel must write entries to this table in the defined format to construct address spaces for user-level tasks.
|
||||
|
|
@ -559,10 +559,13 @@ Page entries -- any of PTEs, PDEs or PDPTEs.
|
|||
> x64WriteThrough, x64PAT, x64CacheDisabled :: Bool }
|
||||
|
||||
> pptrBase :: VPtr
|
||||
> pptrBase = Platform.pptrBase
|
||||
> pptrBase = VPtr Platform.pptrBase
|
||||
|
||||
> physBase :: PAddr
|
||||
> physBase = toPAddr Platform.physBase
|
||||
> kpptrBase :: VPtr
|
||||
> kpptrBase = VPtr Platform.kpptrBase
|
||||
|
||||
> pptrUserTop :: VPtr
|
||||
> pptrUserTop = Platform.pptrUserTop
|
||||
|
||||
> -- This firstValidIODomain and numIODomainBits calculated as part of the boot code.
|
||||
> -- Right now, for simplicity, we assume it is constant
|
||||
|
|
@ -575,7 +578,6 @@ Page entries -- any of PTEs, PDEs or PDPTEs.
|
|||
> hwASIDInvalidate :: Word -> Word64 -> MachineMonad ()
|
||||
> hwASIDInvalidate = invalidateASID
|
||||
|
||||
|
||||
> getFaultAddress :: MachineMonad VPtr
|
||||
> getFaultAddress = do
|
||||
> cbptr <- ask
|
||||
|
|
|
|||
|
|
@ -15,7 +15,7 @@ module SEL4.Machine.Hardware.X64.PC99 where
|
|||
import SEL4.Machine.RegisterSet
|
||||
import Foreign.Ptr
|
||||
import Data.Bits
|
||||
import Data.Word(Word8, Word16)
|
||||
import Data.Word(Word8, Word16, Word64)
|
||||
import Data.Ix
|
||||
|
||||
data CallbackData
|
||||
|
|
@ -30,20 +30,23 @@ instance Bounded IRQ where
|
|||
newtype PAddr = PAddr { fromPAddr :: Word }
|
||||
deriving (Integral, Real, Show, Eq, Num, Bits, FiniteBits, Ord, Enum, Bounded)
|
||||
|
||||
pptrUserTop :: VPtr
|
||||
pptrUserTop = VPtr 0x00007fffffffffff
|
||||
|
||||
-- FIXME: The following kernelBase and physBase are not correct
|
||||
kernelBase :: VPtr
|
||||
kernelBase = VPtr 0xe0000000
|
||||
|
||||
physBase = 0x10000000
|
||||
physMappingOffset = 0xe0000000 - physBase
|
||||
pptrBase :: Word
|
||||
pptrBase = 0xffffff8000000000
|
||||
|
||||
kpptrBase :: Word
|
||||
kpptrBase = 0xffffffff80000000
|
||||
|
||||
ptrFromPAddr :: PAddr -> PPtr a
|
||||
ptrFromPAddr (PAddr addr) = PPtr $ addr + physMappingOffset
|
||||
ptrFromPAddr (PAddr addr) = PPtr $ addr + pptrBase
|
||||
|
||||
addrFromPPtr :: PPtr a -> PAddr
|
||||
addrFromPPtr (PPtr ptr) = PAddr $ ptr - physMappingOffset
|
||||
addrFromPPtr (PPtr ptr) = PAddr $ ptr - pptrBase
|
||||
|
||||
addrFromKPPtr :: PPtr a -> PAddr
|
||||
addrFromKPPtr (PPtr ptr) = PAddr $ ptr - kpptrBase
|
||||
|
||||
pageColourBits :: Int
|
||||
pageColourBits = 0 -- qemu has no cache
|
||||
|
|
@ -132,16 +135,15 @@ foreign import ccall unsafe "qemu_store_word_phys"
|
|||
-- PC99 stubs
|
||||
|
||||
writeCR3 = error "Unimplemented"
|
||||
resetCR3 = error "Unimplemented"
|
||||
|
||||
invalidateTLB = error "Unimplemented"
|
||||
mfence = error "Unimplemented"
|
||||
addrFromKPPtr = error "Unimplemented" -- FIXME two kernel windows
|
||||
pptrBase = error "Unimplemented" -- FIXME two kernel windows
|
||||
hwASIDInvalidate = error "Unimplemented"
|
||||
invalidateASID = error "Unimplemented"
|
||||
invalidateTranslationSingleASID = error "unimplemented"
|
||||
invalidateTranslationSingleASID = error "Unimplemented"
|
||||
|
||||
invalidateLocalPageStructureCacheASID :: PAddr -> Word64 -> IO ()
|
||||
invalidateLocalPageStructureCacheASID = error "Unimplemented"
|
||||
|
||||
getFaultAddress :: Ptr CallbackData -> IO VPtr
|
||||
getFaultAddress _ = error "Unimplemented" -- FIXME: should read CR2
|
||||
|
|
|
|||
|
|
@ -34,12 +34,12 @@ This module contains the architecture-specific kernel global data for the X86-64
|
|||
> gdteBits = 3
|
||||
|
||||
> data KernelState = X64KernelState {
|
||||
> x64KSASIDTable :: Array ASID (Maybe (PPtr ASIDPool)),
|
||||
> x64KSGlobalPML4 :: PPtr PML4E,
|
||||
> x64KSGlobalPDPTs :: [PPtr PDPTE],
|
||||
> x64KSGlobalPDs :: [PPtr PDE],
|
||||
> x64KSGlobalPTs :: [PPtr PTE],
|
||||
> x64KSCurrentCR3 :: CR3,
|
||||
> x64KSASIDTable :: Array ASID (Maybe (PPtr ASIDPool)),
|
||||
> x64KSSKIMPML4 :: PPtr PML4E,
|
||||
> x64KSSKIMPDPTs :: [PPtr PDPTE],
|
||||
> x64KSSKIMPDs :: [PPtr PDE],
|
||||
> x64KSSKIMPTs :: [PPtr PTE],
|
||||
> x64KSCurrentUserCR3 :: CR3,
|
||||
> x64KSKernelVSpace :: PPtr Word -> X64VSpaceRegionUse,
|
||||
> x64KSAllocatedIOPorts :: Array IOPort Bool}
|
||||
|
||||
|
|
|
|||
|
|
@ -151,4 +151,8 @@ ASIDs are mapped to address space roots by a global two-level table. The actual
|
|||
> cr3pcid :: ASID }
|
||||
> deriving (Show, Eq)
|
||||
|
||||
> makeCR3 :: PAddr -> ASID -> CR3
|
||||
> makeCR3 vspace asid = CR3 vspace' asid
|
||||
> where
|
||||
> vspace' = vspace .&. (mask pml4ShiftBits `shiftL` asidBits)
|
||||
|
||||
|
|
|
|||
|
|
@ -314,11 +314,13 @@ where
|
|||
"invalidateASID vspace asid \<equiv> machine_op_lift (invalidateASID_impl vspace asid)"
|
||||
|
||||
consts'
|
||||
resetCR3_impl :: "unit machine_rest_monad"
|
||||
invalidateLocalPageStructureCacheASID_impl :: "machine_word \<Rightarrow> machine_word \<Rightarrow> unit machine_rest_monad"
|
||||
|
||||
definition
|
||||
resetCR3 :: "unit machine_monad" where
|
||||
"resetCR3 \<equiv> machine_op_lift resetCR3_impl "
|
||||
invalidateLocalPageStructureCacheASID :: "machine_word \<Rightarrow> machine_word \<Rightarrow> unit machine_monad"
|
||||
where
|
||||
"invalidateLocalPageStructureCacheASID vspace asid \<equiv>
|
||||
machine_op_lift (invalidateLocalPageStructureCacheASID_impl vspace asid)"
|
||||
|
||||
(* FIXME x64: VT-d
|
||||
definition
|
||||
|
|
|
|||
|
|
@ -32,6 +32,14 @@ definition
|
|||
pptrBase :: word64 where
|
||||
"pptrBase = 0xffffff8000000000"
|
||||
|
||||
definition
|
||||
kpptrBase :: word64 where
|
||||
"kpptrBase = 0xffffffff80000000"
|
||||
|
||||
definition
|
||||
pptrUserTop :: word64 where
|
||||
"pptrUserTop = 0x00007fffffffffff"
|
||||
|
||||
definition
|
||||
cacheLineBits :: nat where
|
||||
"cacheLineBits = 5"
|
||||
|
|
@ -50,7 +58,7 @@ definition
|
|||
|
||||
definition
|
||||
addrFromKPPtr :: "word64 \<Rightarrow> paddr" where
|
||||
"addrFromKPPtr pptr \<equiv> undefined"
|
||||
"addrFromKPPtr pptr \<equiv> pptr - kpptrBase"
|
||||
|
||||
definition
|
||||
pageColourBits :: "nat" where
|
||||
|
|
|
|||
Loading…
Reference in New Issue