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

Updated proof with new fastpath changes removing setCurrentASID and armv_contextSwitch_fp

This commit is contained in:
Joel Beeren 2015-05-21 17:33:02 +10:00 committed by Gerwin Klein
parent 075349ec40
commit 002cf370bb
24 changed files with 310 additions and 390 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
proof/access-control/Arch_AC.thy
View File

@ -59,13 +59,17 @@ lemma integrity_arm_next_asid [iff]:
declare dmo_mol_respects [wp]
crunch respects[wp]: set_current_asid "integrity X aag st"
(simp: invalidateTLB_ASID_def setHardwareASID_def ignore: do_machine_op)
crunch respects[wp]: arm_context_switch "integrity X aag st"
(simp: dmo_bind_valid dsb_def isb_def writeTTBR0_def invalidateTLB_ASID_def
setHardwareASID_def setCurrentPD_def
ignore: do_machine_op)
crunch respects[wp]: find_pd_for_asid "integrity X aag st"
crunch respects[wp]: set_vm_root "integrity X aag st"
(wp: crunch_wps simp: setCurrentPD_def crunch_simps ignore: do_machine_op)
(wp: crunch_wps
simp: setCurrentPD_def isb_def dsb_def writeTTBR0_def dmo_bind_valid crunch_simps
ignore: do_machine_op)
crunch respects[wp]: set_vm_root_for_flush "integrity X aag st"
(wp: crunch_wps simp: setCurrentPD_def crunch_simps ignore: do_machine_op)

29
proof/crefine/Arch_C.thy
View File

@ -2134,33 +2134,8 @@ lemma setVMRootForFlush_ccorres2:
rule ccorres_rhs_assoc2,
rule ccorres_symb_exec_r)
apply simp
apply (subst bind_assoc[symmetric])
apply (rule ccorres_split_nothrow_call_novcg)
apply (rule ccorres_Call)
apply (rule armv_contextSwitch_impl[unfolded armv_contextSwitch_body_def])
apply simp
apply (rule ccorres_rhs_assoc)
apply (rule ccorres_symb_exec_r)
apply simp
apply (ctac(no_vcg) add:setCurrentPD_ccorres)
apply (rule ccorres_call)
apply (ctac(no_vcg) add: setCurrentASID_ccorres)
apply simp
unfolding xfdc_def apply simp
apply simp
apply (wp dmo_setCurrentPD_invs_no_cicd')
apply simp
apply vcg
apply simp
apply (rule conseqPre)
apply vcg
apply (rule subsetI)
apply simp
apply simp
apply simp
apply simp
apply ceqv
apply (ctac add:ccorres_return_C)
apply (ctac (no_vcg) add: armv_contextSwitch_ccorres)
apply (ctac add: ccorres_return_C)
apply wp
apply (simp add: true_def from_bool_def)
apply vcg

83
proof/crefine/Fastpath_C.thy
View File

@ -958,60 +958,6 @@ lemma ccorres_bind_assoc_rev:
(do x \<leftarrow> a1; y \<leftarrow> a2 x; a3 y od) c"
by (simp add: bind_assoc)
lemma armv_contextSwitch_fp_ccorres:
"ccorres dc xfdc \<top>
(UNIV \<inter> {s. cap_pd_' s = pde_Ptr (ptrFromPAddr pd)}
\<inter> {s. hw_asid_' s = ucast hw_asid}) []
(do x \<leftarrow> doMachineOp (setCurrentPD pd);
doMachineOp (setHardwareASID hw_asid)
od)
(Call armv_contextSwitch_fp_'proc)"
proof -
(* these are obtained from the locale here to avoid nasty parameter passing
everywhere else *)
obtain DSB setHWASID_no_DSB where
setCurrentPD_fp_ccorres: "\<forall> pd.
ccorres dc xfdc \<top> (UNIV \<inter> \<lbrace>\<acute>pd_addr = pd\<rbrace>) []
(doMachineOp (setCurrentPD pd))
(Call setCurrentPD_fp_'proc)"
and setHardwareASID_fp_ccorres: "\<forall>hw_asid.
ccorres dc xfdc \<top> (UNIV \<inter> \<lbrace>\<acute>asid___unsigned_char = ucast hw_asid\<rbrace>) []
(doMachineOp (setHWASID_no_DSB hw_asid))
(Call setHardwareASID_fp_'proc)"
and DSB_fp_ccorres: "ccorres dc xfdc \<top> UNIV []
(doMachineOp DSB) (Call dsb_fp_'proc)"
and do_eq: "\<forall>hw_asid pd.
(do (x :: unit) \<leftarrow> DSB; setCurrentPD pd; setHWASID_no_DSB hw_asid od)
= (do setCurrentPD pd; setHardwareASID hw_asid od)"
using setCurrentPD_setHardwareASID_dsb_fp_ccorres
by auto
have dmo_split:
"(do x \<leftarrow> doMachineOp (setCurrentPD pd);
doMachineOp (setHardwareASID hw_asid)
od) = (do doMachineOp DSB; doMachineOp (setCurrentPD pd);
doMachineOp (setHWASID_no_DSB hw_asid) od)"
apply (simp add: doMachineOp_bind[symmetric]
setCurrentPD_empty_fail setHardwareASID_empty_fail
do_eq[rule_format, simplified, symmetric])
apply (rule ext)
apply (simp add: doMachineOp_def exec_gets exec_modify split_def bind_assoc
bind_select_f_bind[symmetric]
| rule select_bind_eq)+
apply (simp add: simpler_modify_def)
done
show ?thesis
apply (cinit' lift: cap_pd_' hw_asid_')
apply (simp only: dmo_split, simp)
apply (ctac(no_vcg) add: DSB_fp_ccorres)
apply csymbr
apply (simp only:)
apply (ctac(no_vcg) add: setCurrentPD_fp_ccorres[rule_format])
apply (ctac add: setHardwareASID_fp_ccorres[rule_format, unfolded dc_def])
apply wp
apply (simp add: Collect_const_mem addrFromPPtr_def)
done
qed
lemma monadic_rewrite_gets_l:
"(\<And>x. monadic_rewrite F E (P x) (g x) m)
\<Longrightarrow> monadic_rewrite F E (\<lambda>s. P (f s) s) (gets f >>= (\<lambda>x. g x)) m"
@ -1021,14 +967,14 @@ lemma pd_at_asid_inj':
"pd_at_asid' pd asid s \<Longrightarrow> pd_at_asid' pd' asid s \<Longrightarrow> pd' = pd"
by (clarsimp simp: pd_at_asid'_def obj_at'_def)
lemma setCurrentASID_setCurrentHWASID_rewrite:
lemma armv_contextSwitch_HWASID_fp_rewrite:
"monadic_rewrite True False
(pd_has_hwasid pd and pd_at_asid' pd asid and
(\<lambda>s. asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) pd
= set_option (pde_stored_asid v)))
(setCurrentASID asid)
(doMachineOp (setHardwareASID (the (pde_stored_asid v))))"
apply (simp add: setCurrentASID_def getHWASID_def
(armv_contextSwitch pd asid)
(doMachineOp (armv_contextSwitch_HWASID pd (the (pde_stored_asid v))))"
apply (simp add: getHWASID_def armv_contextSwitch_def
bind_assoc loadHWASID_def
findPDForASIDAssert_def
checkPDAt_def checkPDUniqueToASID_def
@ -1104,18 +1050,14 @@ lemma switchToThread_fp_ccorres:
catch_throwError)
apply (rule ccorres_stateAssert)
apply (rule ccorres_False[where P'=UNIV])
apply (simp add: catch_liftE bind_assoc armv_contextSwitch_def
apply (simp add: catch_liftE bind_assoc
del: Collect_const cong: call_ignore_cong)
apply (rule monadic_rewrite_ccorres_assemble[rotated])
apply (rule monadic_rewrite_bind_tail)
apply (rule monadic_rewrite_bind_head)
apply (rule_tac pd=pd and v=v
in setCurrentASID_setCurrentHWASID_rewrite)
apply (simp add: pd_has_hwasid_def)
apply (wp doMachineOp_pd_at_asid')
apply (rule ccorres_bind_assoc_rev)
apply (ctac(no_vcg) add: armv_contextSwitch_fp_ccorres)
apply (simp add: storeWordUser_def bind_assoc case_option_If2
apply (rule monadic_rewrite_bind_head)
apply (rule_tac pd=pd and v=v
in armv_contextSwitch_HWASID_fp_rewrite)
apply (ctac(no_vcg) add: armv_contextSwitch_HWASID_ccorres)
apply (simp add: storeWordUser_def bind_assoc case_option_If2
split_def
del: Collect_const)
apply (rule ccorres_symb_exec_l[OF _ gets_inv _ empty_fail_gets])
@ -1148,7 +1090,6 @@ lemma switchToThread_fp_ccorres:
apply wp
apply (simp add: obj_at'_weakenE[OF _ TrueI])
apply (wp hoare_drop_imps)[1]
apply (wp doMachineOp_no_0')[1]
apply (simp add: bind_assoc checkPDNotInASIDMap_def
checkPDASIDMapMembership_def)
apply (rule ccorres_stateAssert)
@ -4075,7 +4016,7 @@ lemma setVMRoot_isolatable:
apply (simp add: setVMRoot_def getThreadVSpaceRoot_def
locateSlot_conv getSlotCap_def
cap_case_isPageDirectoryCap if_bool_simps
whenE_def liftE_def setCurrentASID_def
whenE_def liftE_def
checkPDNotInASIDMap_def stateAssert_def2
checkPDASIDMapMembership_def armv_contextSwitch_def
cong: if_cong)
@ -4340,7 +4281,7 @@ lemma oblivious_setVMRoot_schact:
apply (simp add: setVMRoot_def getThreadVSpaceRoot_def locateSlot_conv
getSlotCap_def getCTE_def armv_contextSwitch_def)
apply (safe intro!: oblivious_bind oblivious_bindE oblivious_catch
| simp_all add: liftE_def setCurrentASID_def getHWASID_def
| simp_all add: liftE_def getHWASID_def
findPDForASID_def liftME_def loadHWASID_def
findPDForASIDAssert_def checkPDAt_def
checkPDUniqueToASID_def

50
proof/crefine/Machine_C.thy
View File

@ -31,10 +31,10 @@ assumes resetTimer_ccorres:
(doMachineOp resetTimer)
(Call resetTimer_'proc)"
assumes setCurrentPD_ccorres:
assumes writeTTBR0_ccorres:
"ccorres dc xfdc \<top> (\<lbrace>\<acute>addr = pd\<rbrace>) []
(doMachineOp (setCurrentPD pd))
(Call setCurrentPD_'proc)"
(doMachineOp (writeTTBR0 pd))
(Call writeTTBR0_'proc)"
assumes setHardwareASID_ccorres:
"ccorres dc xfdc \<top> (\<lbrace>\<acute>hw_asid = hw_asid\<rbrace>) []
@ -174,34 +174,7 @@ assumes cleanCacheRange_PoU_spec:
(* The following are fastpath specific assumptions.
We might want to move them somewhere else. *)
(*
The setCurrentPD_fp function is a fastpath specific implementation of
setCurrentPD, making stronger assumptions on the assembly level.
It has the same outside interface as @{text setCurrentPD}.
The setHardwareASID_fp function is similar to regular setHardwareASID,
but does not perform a data synchronisation barrier, which is performed
explicitly via dsb_fp. The fastpath requires these functions taken
together to have the same effect, in fact with a slight ordering change.
*)
assumes setCurrentPD_setHardwareASID_dsb_fp_ccorres:
"\<exists>DSB setHWASID_no_DSB.
(\<forall>pd.
ccorres dc xfdc \<top> (\<lbrace>\<acute>pd_addr = pd\<rbrace>) []
(doMachineOp (setCurrentPD pd))
(Call setCurrentPD_fp_'proc))
\<and> (\<forall>hw_asid.
ccorres dc xfdc \<top> (\<lbrace>\<acute>asid___unsigned_char = ucast hw_asid\<rbrace>) []
(doMachineOp (setHWASID_no_DSB hw_asid))
(Call setHardwareASID_fp_'proc))
\<and> ccorres dc xfdc \<top> UNIV []
(doMachineOp DSB) (Call dsb_fp_'proc)
\<and> (\<forall>hw_asid pd.
(do (x :: unit) \<leftarrow> DSB; setCurrentPD pd; setHWASID_no_DSB hw_asid od)
= (do setCurrentPD pd; setHardwareASID hw_asid od))"
(* likewise clearExMonitor_fp is an inline-friendly version of clearExMonitor *)
(* clearExMonitor_fp is an inline-friendly version of clearExMonitor *)
assumes clearExMonitor_fp_ccorres:
"ccorres dc xfdc (\<lambda>_. True) UNIV [] (doMachineOp MachineOps.clearExMonitor)
(Call clearExMonitor_fp_'proc)"
@ -694,6 +667,21 @@ lemma cleanCaches_PoU_ccorres:
apply clarsimp
done
lemma setCurrentPD_ccorres:
"ccorres dc xfdc \<top> (\<lbrace>\<acute>addr = pd\<rbrace>) []
(doMachineOp (setCurrentPD pd))
(Call setCurrentPD_'proc)"
apply cinit'
apply (simp add: setCurrentPD_def doMachineOp_bind empty_fail_dsb empty_fail_isb
writeTTBR0_empty_fail)
apply (ctac (no_vcg) add: dsb_ccorres)
apply (ctac (no_vcg) add: writeTTBR0_ccorres)
apply (ctac (no_vcg) add: isb_ccorres)
apply wp
apply clarsimp
done
end
end

75
proof/crefine/VSpace_C.thy
View File

@ -1431,15 +1431,30 @@ lemma getHWASID_ccorres:
apply (auto simp: all_invs_but_ct_idle_or_in_cur_domain'_def)
done
lemma setCurrentASID_ccorres:
lemma armv_contextSwitch_HWASID_ccorres:
"ccorres dc xfdc \<top> (UNIV \<inter> {s. cap_pd_' s = pde_Ptr pd} \<inter> {s. hw_asid_' s = hwasid}) []
(doMachineOp (armv_contextSwitch_HWASID pd hwasid)) (Call armv_contextSwitch_HWASID_'proc)"
apply (cinit' lift: cap_pd_' hw_asid_')
apply (simp add: armv_contextSwitch_HWASID_def doMachineOp_bind setCurrentPD_empty_fail
setHardwareASID_empty_fail )
apply csymbr
apply (ctac (no_vcg) add: setCurrentPD_ccorres)
apply (fold dc_def)
apply (ctac (no_vcg) add: setHardwareASID_ccorres)
apply wp
apply clarsimp
done
lemma armv_contextSwitch_ccorres:
"ccorres dc xfdc (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asid \<le> mask asid_bits))
(UNIV \<inter> {s. asid_' s = asid}) []
(setCurrentASID asid) (Call setCurrentASID_'proc)"
apply (cinit lift: asid_')
(UNIV \<inter> {s. cap_pd_' s = pde_Ptr pd} \<inter> {s. asid_' s = asid} ) []
(armv_contextSwitch pd asid) (Call armv_contextSwitch_'proc)"
apply (cinit lift: cap_pd_' asid_')
apply simp
apply (ctac(no_vcg) add: getHWASID_ccorres)
apply (fold dc_def)
apply (ctac add: setHardwareASID_ccorres)
apply (ctac (no_vcg)add: armv_contextSwitch_HWASID_ccorres)
apply wp
apply clarsimp
done
@ -1545,26 +1560,7 @@ lemma setVMRoot_ccorres:
apply vcg
apply wp
apply (simp add: whenE_def returnOk_def)
apply (unfold armv_contextSwitch_def)
apply (rule ccorres_call)
apply (rule ccorres_Call)
apply (rule armv_contextSwitch_impl [unfolded armv_contextSwitch_body_def])
apply simp
apply (rule ccorres_rhs_assoc)
apply (rule ccorres_symb_exec_r)
apply (ctac(no_vcg) add: setCurrentPD_ccorres)
apply (ctac add: setCurrentASID_ccorres[unfolded dc_def])
apply (wp dmo_setCurrentPD_invs_no_cicd')
apply simp
apply vcg
apply simp
apply (rule conseqPre)
apply vcg
apply (rule subsetI)
apply simp
apply simp
apply simp
apply simp
apply (ctac add: armv_contextSwitch_ccorres[unfolded dc_def])
apply (simp add: checkPDNotInASIDMap_def checkPDASIDMapMembership_def)
apply (rule ccorres_stateAssert)
apply (rule ccorres_rhs_assoc)+
@ -1640,33 +1636,8 @@ lemma setVMRootForFlush_ccorres:
rule ccorres_rhs_assoc2,
rule ccorres_symb_exec_r)
apply simp
apply (subst bind_assoc[symmetric])
apply (rule ccorres_split_nothrow_call_novcg)
apply (rule ccorres_Call)
apply (rule armv_contextSwitch_impl[unfolded armv_contextSwitch_body_def])
apply simp
apply (rule ccorres_rhs_assoc)
apply (rule ccorres_symb_exec_r)
apply simp
apply (ctac(no_vcg) add:setCurrentPD_ccorres)
apply (rule ccorres_call)
apply (ctac(no_vcg) add: setCurrentASID_ccorres)
apply simp
unfolding xfdc_def apply simp
apply simp
apply (wp dmo_setCurrentPD_invs_no_cicd')
apply simp
apply vcg
apply simp
apply (rule conseqPre)
apply vcg
apply (rule subsetI)
apply simp
apply simp
apply simp
apply simp
apply ceqv
apply (ctac add:ccorres_return_C)
apply (ctac (no_vcg)add: armv_contextSwitch_ccorres)
apply (ctac add: ccorres_return_C)
apply wp
apply (simp add: true_def from_bool_def)
apply vcg

2
proof/drefine/Arch_DR.thy
View File

@ -1339,7 +1339,7 @@ done
lemma set_vm_root_for_flush_dwp[wp]:
"\<lbrace>\<lambda>ps. transform ps = cs\<rbrace> set_vm_root_for_flush word1 word2 \<lbrace>\<lambda>r s. transform s = cs\<rbrace>"
apply (simp add:set_vm_root_for_flush_def)
apply (wp do_machine_op_wp|clarsimp simp:set_current_asid_def get_hw_asid_def)+
apply (wp do_machine_op_wp|clarsimp simp:arm_context_switch_def get_hw_asid_def)+
apply (wpc)
apply wp
apply (rule hoare_conjI,rule hoare_drop_imp)

2
proof/drefine/CNode_DR.thy
View File

@ -1409,7 +1409,7 @@ lemma delete_asid_pool_idle [wp]:
apply (rule mapM_wp)
apply wp
apply (rule_tac Q = "\<lambda>r s. P (idle_thread s)" in hoare_strengthen_post)
apply (clarsimp simp:load_hw_asid_def find_free_hw_asid_def invalidate_asid_entry_def set_current_asid_def get_hw_asid_def | wp | wpc)+
apply (clarsimp simp:load_hw_asid_def find_free_hw_asid_def invalidate_asid_entry_def arm_context_switch_def get_hw_asid_def | wp | wpc)+
apply fastforce
apply wp
apply clarsimp

8
proof/drefine/Finalise_DR.thy
View File

@ -577,7 +577,7 @@ done
lemma set_current_pd_dwp[wp]:
" \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> setCurrentPD (Platform.addrFromPPtr x) \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>"
by (clarsimp simp:setCurrentPD_def,wp)
by (clarsimp simp:setCurrentPD_def writeTTBR0_def isb_def dsb_def,wp)
lemma set_hardware_asid_dwp[wp]:
" \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> setHardwareASID hw_asid \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>"
@ -688,7 +688,7 @@ lemma dcorres_set_vm_root:
apply simp
apply (rule hoare_pre)
apply (wp hoare_whenE_wp do_machine_op_wp [OF allI] hoare_drop_imps find_pd_for_asid_inv
| wpc | simp add: set_current_asid_def get_hw_asid_def load_hw_asid_def if_apply_def2)+
| wpc | simp add: arm_context_switch_def get_hw_asid_def load_hw_asid_def if_apply_def2)+
done
lemma dcorres_delete_asid_pool:
@ -780,7 +780,7 @@ lemma dcorres_flush_page:
apply (simp add:load_hw_asid_def)
apply wp
apply (clarsimp simp:set_vm_root_for_flush_def)
apply (wp do_machine_op_wp|clarsimp simp:set_current_asid_def get_hw_asid_def)+
apply (wp do_machine_op_wp|clarsimp simp:arm_context_switch_def get_hw_asid_def)+
apply (wpc)
apply wp
apply (rule hoare_conjI,rule hoare_drop_imp)
@ -804,7 +804,7 @@ lemma dcorres_flush_table:
apply (clarsimp simp:load_hw_asid_def)
apply wp
apply (clarsimp simp:set_vm_root_for_flush_def)
apply (wp do_machine_op_wp|clarsimp simp:set_current_asid_def get_hw_asid_def)+
apply (wp do_machine_op_wp|clarsimp simp:arm_context_switch_def get_hw_asid_def)+
apply wpc
apply wp
apply (rule hoare_conjI,rule hoare_drop_imp)

56
proof/infoflow/Arch_IF.thy
View File

@ -57,7 +57,8 @@ lemma irq_state_clearExMonitor[wp]: "\<lbrace> \<lambda>s. P (irq_state s) \<rbr
crunch irq_state_of_state[wp]: schedule "\<lambda>(s::det_state). P (irq_state_of_state s)"
(wp: dmo_wp modify_wp crunch_wps hoare_whenE_wp
simp: invalidateTLB_ASID_def setHardwareASID_def setCurrentPD_def
machine_op_lift_def machine_rest_lift_def crunch_simps storeWord_def)
machine_op_lift_def machine_rest_lift_def crunch_simps storeWord_def
dsb_def isb_def writeTTBR0_def)
crunch irq_state_of_state[wp]: reply_from_kernel "\<lambda>s. P (irq_state_of_state s)"
@ -696,40 +697,31 @@ lemma dmo_mol_irq_state_of_state[wp]:
apply(wp dmo_wp | simp)+
done
lemma set_current_asid_reads_respects:
"reads_respects aag l \<top> (set_current_asid asid)"
unfolding set_current_asid_def
lemma arm_context_switch_reads_respects:
"reads_respects aag l \<top> (arm_context_switch pd asid)"
unfolding arm_context_switch_def
apply(rule equiv_valid_guard_imp)
apply(rule reads_respects_unobservable_unit_return)
apply (wp do_machine_op_mol_states_equiv_for get_hw_asid_states_equiv_for get_hw_asid_cur_thread | simp add: setHardwareASID_def)+
apply (wp do_machine_op_mol_states_equiv_for get_hw_asid_states_equiv_for get_hw_asid_cur_thread
| simp add: setCurrentPD_def dsb_def isb_def writeTTBR0_def dmo_bind_valid setHardwareASID_def)+
done
lemma gets_arm_global_pd_bind_setCurrentPD_reads_respects:
"reads_respects aag l \<top> ( do global_pd \<leftarrow> gets (arm_global_pd \<circ> arch_state);
do_machine_op
(machine_op_lift (setCurrentPD_impl (addrFromPPtr global_pd)))
od)"
apply(rule reads_respects_unobservable_unit_return)
apply (wp do_machine_op_mol_states_equiv_for)+
done
lemma set_current_asid_states_equiv_for:
"invariant (set_current_asid asid) (states_equiv_for P Q R S X st)"
unfolding set_current_asid_def
apply (wp do_machine_op_mol_states_equiv_for get_hw_asid_states_equiv_for | simp add: setHardwareASID_def)+
lemma arm_context_switch_states_equiv_for:
"invariant (arm_context_switch pd asid) (states_equiv_for P Q R S X st)"
unfolding arm_context_switch_def
apply (wp do_machine_op_mol_states_equiv_for get_hw_asid_states_equiv_for | simp add: setHardwareASID_def dmo_bind_valid setCurrentPD_def dsb_def isb_def writeTTBR0_def)+
done
crunch states_equiv_for: find_pd_for_asid "states_equiv_for P Q R S X st"
lemma set_vm_root_states_equiv_for:
"invariant (set_vm_root thread) (states_equiv_for P Q R S X st)"
unfolding set_vm_root_def catch_def fun_app_def setCurrentPD_def
unfolding set_vm_root_def catch_def fun_app_def setCurrentPD_def isb_def dsb_def writeTTBR0_def
apply (wp_once hoare_drop_imps
|wp do_machine_op_mol_states_equiv_for hoare_vcg_all_lift set_current_asid_states_equiv_for hoare_whenE_wp | wpc | simp)+
|wp do_machine_op_mol_states_equiv_for hoare_vcg_all_lift arm_context_switch_states_equiv_for hoare_whenE_wp | wpc | simp add: dmo_bind_valid)+
apply(rule hoare_post_imp_R)
apply(rule valid_validE_R)
apply(wp find_pd_for_asid_states_equiv_for hoare_drop_imps set_current_asid_states_equiv_for do_machine_op_mol_states_equiv_for hoare_whenE_wp | simp | wpc)+
apply(wp find_pd_for_asid_states_equiv_for hoare_drop_imps arm_context_switch_states_equiv_for do_machine_op_mol_states_equiv_for hoare_whenE_wp | simp | wpc)+
apply(rule hoare_post_imp_R)
apply(rule valid_validE_R)
apply(wp find_pd_for_asid_states_equiv_for get_cap_wp | simp)+
@ -780,7 +772,7 @@ lemma set_vm_root_for_flush_reads_respects:
unfolding set_vm_root_for_flush_def fun_app_def setCurrentPD_def
apply(rule equiv_valid_guard_imp)
apply (wp_once hoare_drop_imps
|wp set_current_asid_reads_respects dmo_mol_reads_respects
|wp arm_context_switch_reads_respects dmo_mol_reads_respects
hoare_vcg_all_lift gets_cur_thread_ev get_cap_rev
|wpc)+
apply (clarsimp simp: reads_equiv_def)
@ -1645,16 +1637,20 @@ lemma get_hw_asid_globals_equiv[wp]:
apply(wp store_hw_asid_globals_equiv find_free_hw_asid_globals_equiv load_hw_asid_wp | wpc | simp)+
done
lemma set_current_asid_globals_equiv[wp]:
"\<lbrace>globals_equiv s\<rbrace> set_current_asid asid \<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
unfolding set_current_asid_def setHardwareASID_def
apply(wp dmo_mol_globals_equiv get_hw_asid_globals_equiv)
lemma arm_context_switch_globals_equiv[wp]:
"\<lbrace>globals_equiv s\<rbrace> arm_context_switch pd asid \<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
unfolding arm_context_switch_def setHardwareASID_def
apply(wp dmo_mol_globals_equiv get_hw_asid_globals_equiv
| simp add: dmo_bind_valid setCurrentPD_def writeTTBR0_def isb_def dsb_def )+
done
lemma set_vm_root_globals_equiv[wp]:
"\<lbrace>globals_equiv s\<rbrace> set_vm_root tcb \<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
unfolding set_vm_root_def fun_app_def setCurrentPD_def
apply(wp dmo_mol_globals_equiv set_current_asid_globals_equiv whenE_inv| wpc)+
apply (clarsimp simp:set_vm_root_def fun_app_def setCurrentPD_def dsb_def
isb_def writeTTBR0_def dmo_bind_valid)
apply(wp dmo_mol_globals_equiv arm_context_switch_globals_equiv whenE_inv
| wpc
| clarsimp simp: dmo_bind_valid isb_def dsb_def writeTTBR0_def)+
apply(wp hoare_vcg_all_lift | wp_once hoare_drop_imps | clarsimp)+
done
@ -1873,7 +1869,7 @@ lemma valid_ko_at_arm_arch[simp]:
valid_ko_at_arm (s\<lparr>arch_state := A\<rparr>) = valid_ko_at_arm s"
by (simp add: valid_ko_at_arm_def)
crunch valid_ko_at_arm[wp]: set_current_asid "valid_ko_at_arm"
crunch valid_ko_at_arm[wp]: arm_context_switch "valid_ko_at_arm"
(wp: find_pd_for_asid_assert_wp)
lemma set_vm_root_valid_ko_at_arm[wp]:

4
proof/infoflow/Scheduler_IF.thy
View File

@ -688,10 +688,10 @@ lemma midstrength_scheduler_affects_equiv_unobservable:
lemma dmo_mol_exclusive_state[wp]:
"invariant (do_machine_op (machine_op_lift mop)) (\<lambda>s. P (exclusive_state (machine_state s)))"
by(wp mol_exclusive_state dmo_wp | simp add: split_def)+
by(wp mol_exclusive_state dmo_wp | simp add: split_def dmo_bind_valid writeTTBR0_def isb_def dsb_def )+
crunch exclusive_state[wp]: set_vm_root "\<lambda>s. P (exclusive_state (machine_state s))"
(ignore: do_machine_op simp: invalidateTLB_ASID_def setHardwareASID_def setCurrentPD_def crunch_simps)
(ignore: do_machine_op simp: invalidateTLB_ASID_def setHardwareASID_def setCurrentPD_def dsb_def isb_def writeTTBR0_def dmo_bind_valid crunch_simps)
lemmas set_vm_root_scheduler_affects_equiv[wp] = scheduler_affects_equiv_unobservable[OF set_vm_root_states_equiv_for set_vm_root_cur_domain _ _ _ set_vm_root_idle_thread set_vm_root_exclusive_state]

2
proof/invariant-abstract/EmptyFail_AI.thy
View File

@ -142,7 +142,7 @@ crunch_ignore (empty_fail)
invalidateByVA_I_impl invalidate_I_PoU_impl cleanInvalByVA_impl branchFlush_impl
clean_D_PoU_impl cleanInvalidate_D_PoC_impl cleanInvalidateL2Range_impl
invalidateL2Range_impl cleanL2Range_impl flushBTAC_impl writeContextID_impl
isb_impl dsb_impl dmb_impl setHardwareASID_impl setCurrentPD_impl do_extended_op
isb_impl dsb_impl dmb_impl setHardwareASID_impl writeTTBR0_impl do_extended_op
cacheRangeOp)
crunch (empty_fail) empty_fail[wp]: set_object, gets_the, get_register, get_cap

2
proof/invariant-abstract/Finalise_AI.thy
View File

@ -1617,7 +1617,7 @@ lemma flush_table_empty:
flush_table ac aa b word
\<lbrace>\<lambda>rv s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace>"
apply (clarsimp simp: flush_table_def set_vm_root_def)
apply (wp do_machine_op_obj_at set_current_asid_empty hoare_whenE_wp
apply (wp do_machine_op_obj_at arm_context_switch_empty hoare_whenE_wp
| wpc
| simp
| wps)+

22
proof/invariant-abstract/Machine_AI.thy
View File

@ -69,9 +69,6 @@ lemma ef_machine_op_lift [simp]:
by (simp add: machine_op_lift_def)
lemma no_fail_setCurrentPD: "no_fail \<top> (setCurrentPD w)"
by (simp add: setCurrentPD_def)
lemma no_fail_setNextPC: "no_fail \<top> (setNextPC pc)"
by (simp add: setNextPC_def setRegister_def)
@ -97,6 +94,14 @@ lemma no_fail_dsb: "no_fail \<top> dsb"
lemma no_fail_dmb: "no_fail \<top> dmb"
by (simp add: dmb_def)
lemma no_fail_writeTTBR0: "no_fail \<top> (writeTTBR0 w)"
by (simp add: writeTTBR0_def)
lemma no_fail_setCurrentPD: "no_fail \<top> (setCurrentPD w)"
apply (simp add: setCurrentPD_def)
apply (rule no_fail_pre, wp no_fail_dsb no_fail_writeTTBR0 no_fail_isb, simp)
done
lemma no_fail_cleanByVA: "no_fail \<top> (cleanByVA w p)"
by (simp add: cleanByVA_def)
@ -422,10 +427,9 @@ lemma no_irq_writeContextID: "no_irq writeContextID"
lemma no_irq_setHardwareASID: "no_irq (setHardwareASID hw_asid)"
by (simp add: setHardwareASID_def)
lemma no_irq_setCurrentPD: "no_irq (setCurrentPD pd)"
by (simp add: setCurrentPD_def)
lemma no_irq_writeTTBR0: "no_irq (writeTTBR0 pd)"
by (simp add: writeTTBR0_def)
lemma no_irq_gets [simp]:
"no_irq (gets f)"
by (simp add: no_irq_def)
@ -527,6 +531,10 @@ lemma no_irq_modify:
apply (clarsimp simp: in_monad)
done
lemma no_irq_setCurrentPD: "no_irq (setCurrentPD pd)"
apply (clarsimp simp: setCurrentPD_def)
apply (wp no_irq_dsb no_irq_writeTTBR0 no_irq_isb)
done
lemma no_irq_clearExMonitor: "no_irq clearExMonitor"
apply (simp add: clearExMonitor_def)

4
proof/invariant-abstract/Schedule_AI.thy
View File

@ -112,8 +112,8 @@ lemma dmo_kheap_arch_state[wp]:
lemma set_vm_root_kheap_arch_state[wp]:
"\<lbrace>\<lambda>s. P (kheap s) (arm_globals_frame (arch_state s))\<rbrace> set_vm_root a
\<lbrace>\<lambda>_ s. P (kheap s) (arm_globals_frame (arch_state s))\<rbrace>" (is "valid ?P _ _")
apply (simp add: set_vm_root_def set_current_asid_def)
apply (wp | wpcw | simp add: set_current_asid_def get_hw_asid_def
apply (simp add: set_vm_root_def arm_context_switch_def)
apply (wp | wpcw | simp add: arm_context_switch_def get_hw_asid_def
store_hw_asid_def find_pd_for_asid_assert_def find_free_hw_asid_def
invalidate_hw_asid_entry_def invalidate_asid_def load_hw_asid_def)+
apply (simp add: whenE_def, intro conjI impI)

97
proof/invariant-abstract/VSpace_AI.thy
View File

@ -882,7 +882,7 @@ crunch arm_asid_table_inv[wp]: invalidate_asid_entry
crunch st_tcb_at_P [wp]: find_free_hw_asid "\<lambda>s. P (st_tcb_at Q p s)"
crunch st_tcb_at [wp]: set_current_asid "\<lambda>s. P (st_tcb_at Q p s)"
crunch st_tcb_at [wp]: arm_context_switch "\<lambda>s. P (st_tcb_at Q p s)"
crunch st_tcb_at [wp]: find_pd_for_asid "\<lambda>s. P (st_tcb_at Q p s)"
@ -973,7 +973,7 @@ lemma svmrff_asid_mapped [wp]:
"\<lbrace>valid_asid asid\<rbrace>
set_vm_root_for_flush pd asid
\<lbrace>\<lambda>rv. valid_asid asid\<rbrace>"
apply (simp add: set_vm_root_for_flush_def set_current_asid_def
apply (simp add: set_vm_root_for_flush_def arm_context_switch_def
get_hw_asid_def store_hw_asid_def find_free_hw_asid_def
load_hw_asid_def
cong: if_cong option.case_cong)
@ -1021,10 +1021,10 @@ lemma store_hw_asid_asid_map [wp]:
done
lemma set_current_asid_asid_map [wp]:
lemma arm_context_switch_asid_map [wp]:
"\<lbrace>valid_asid_map and K (asid \<le> mask asid_bits)\<rbrace>
set_current_asid asid \<lbrace>\<lambda>_. valid_asid_map\<rbrace>"
apply (simp add: set_current_asid_def get_hw_asid_def)
arm_context_switch pd asid \<lbrace>\<lambda>_. valid_asid_map\<rbrace>"
apply (simp add: arm_context_switch_def get_hw_asid_def)
apply (wp load_hw_asid_wp|wpc|simp)+
done
@ -1681,19 +1681,20 @@ lemma get_hw_asid_invs [wp]:
apply simp
done
lemma set_current_asid_invs [wp]:
"\<lbrace>invs and K (a \<le> mask asid_bits)\<rbrace> set_current_asid a \<lbrace>\<lambda>_. invs\<rbrace>"
apply (simp add: set_current_asid_def)
lemma arm_context_switch_invs [wp]:
"\<lbrace>invs and K (a \<le> mask asid_bits)\<rbrace> arm_context_switch pd a \<lbrace>\<lambda>_. invs\<rbrace>"
apply (simp add: arm_context_switch_def)
apply (wp dmo_invs)
apply (rule hoare_post_imp[rotated])
apply (rule get_hw_asid_invs[simplified])
apply safe
apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p = underlying_memory m p"
in use_valid)
apply ((clarsimp simp: setHardwareASID_def machine_op_lift_def
machine_rest_lift_def split_def | wp)+)[3]
apply ((clarsimp simp: setHardwareASID_def setCurrentPD_def writeTTBR0_def
isb_def dsb_def machine_op_lift_def
machine_rest_lift_def split_def | wp)+)[3]
apply(erule use_valid)
apply(wp | simp add: no_irq_setHardwareASID)+
apply(wp | simp add: no_irq_setHardwareASID no_irq_setCurrentPD)+
done
(* FIXME: move *)
@ -1706,63 +1707,33 @@ lemma invs_valid_irq_states[elim!]:
"invs s \<Longrightarrow> valid_irq_states s"
by(auto simp: invs_def valid_state_def)
lemmas setCurrentPD_irq_masks = no_irq[OF no_irq_setCurrentPD]
lemmas setHardwareASID_irq_masks = no_irq[OF no_irq_setHardwareASID]
lemma dmo_setCurrentPD_invs[wp]: "\<lbrace>invs\<rbrace> do_machine_op (setCurrentPD addr) \<lbrace>\<lambda>y. invs\<rbrace>"
apply (wp dmo_invs)
apply safe
apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p = underlying_memory m p"
in use_valid)
apply ((clarsimp simp: setCurrentPD_def writeTTBR0_def dsb_def isb_def machine_op_lift_def
machine_rest_lift_def split_def | wp)+)[3]
apply(erule (1) use_valid[OF _ setCurrentPD_irq_masks])
done
lemma svr_invs [wp]:
"\<lbrace>invs\<rbrace> set_vm_root t' \<lbrace>\<lambda>_. invs\<rbrace>"
apply (simp add: set_vm_root_def)
apply (rule hoare_pre)
apply (wp dmo_invs hoare_whenE_wp find_pd_for_asid_inv hoare_vcg_all_lift
| wpc | simp)+
apply (rule_tac Q="\<top>\<top>" in hoare_post_imp)
apply safe
apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p =
underlying_memory m p"
in use_valid)
apply (clarsimp simp: setCurrentPD_def machine_op_lift_def
machine_rest_lift_def split_def)
apply ((wp | simp)+)[3]
apply(erule use_valid, wp no_irq_setCurrentPD, assumption)
apply(wp dmo_invs | clarsimp)+
apply (simp add: whenE_def)
apply (intro conjI impI)
apply wp
apply (simp add: returnOk_E')
apply (simp add: whenE_def)
apply (intro conjI[rotated] impI)
apply wp
apply (simp add: throwError_R')
apply wp
apply (wp hoare_whenE_wp find_pd_for_asid_inv hoare_vcg_all_lift | wpc | simp add: split_def)+
apply (rule_tac Q'="\<lambda>_ s. invs s \<and> x2 \<le> mask asid_bits" in hoare_post_imp_R)
prefer 2
apply safe
apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p = underlying_memory m p"
in use_valid)
apply (clarsimp simp: setCurrentPD_def machine_op_lift_def
machine_rest_lift_def split_def)
apply ((wp | clarsimp simp: split_def)+)[3]
apply(erule use_valid, wp no_irq_setCurrentPD, assumption)
apply(wp | clarsimp simp: split_def)+
apply (rule_tac Q="\<lambda>c s. invs s \<and> s \<turnstile> c \<and>
(\<forall>m. \<forall>x\<in>fst (setCurrentPD (Platform.addrFromPPtr
(arm_global_pd (arch_state s))) m).
(\<forall>p. in_user_frame p s \<or>
underlying_memory (snd x) p = underlying_memory m p) \<and>
(m = machine_state s \<longrightarrow>
(\<forall>irq. interrupt_states s irq = IRQInactive \<longrightarrow>
irq_masks (snd x) irq \<or>
irq_masks (snd x) irq =
irq_masks (machine_state s) irq)))"
in hoare_strengthen_post)
apply simp
apply (rule valid_validE_R)
apply (wp find_pd_for_asid_inv | simp add: split_def)+
apply (rule_tac Q="\<lambda>c s. invs s \<and> s \<turnstile> c" in hoare_strengthen_post)
apply wp
apply (clarsimp simp: valid_cap_def mask_def)
apply(simp add: invs_valid_objs)
apply safe
apply (clarsimp simp add: invs_def valid_state_def valid_pspace_def)
apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p = underlying_memory m p"
in use_valid)
apply ((clarsimp simp: setCurrentPD_def machine_op_lift_def
machine_rest_lift_def split_def valid_irq_states_def | wp)+)[3]
apply(subst snd_conv)
apply(erule use_valid, wp no_irq_setCurrentPD, assumption)
done
lemma svr_st_tcb [wp]:
@ -3273,13 +3244,7 @@ lemma set_vm_root_for_flush_invs:
"\<lbrace>invs and K (asid \<le> mask asid_bits)\<rbrace>
set_vm_root_for_flush pd asid \<lbrace>\<lambda>_. invs\<rbrace>"
apply (simp add: set_vm_root_for_flush_def)
apply (wp dmo_invs hoare_drop_imps hoare_vcg_all_lift |wpc|simp)+
apply safe
apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p = underlying_memory x p"
in use_valid)
apply ((clarsimp simp: setCurrentPD_def machine_op_lift_def
machine_rest_lift_def split_def | wp)+)[3]
apply(erule use_valid, wp no_irq_setCurrentPD, assumption)
apply (wp hoare_drop_imps hoare_vcg_all_lift |wpc|simp)+
done
lemma flush_table_invs[wp]:

3
proof/refine/CNodeInv_R.thy
View File

@ -9614,12 +9614,13 @@ lemma invokeCNode_invs' [wp]:
declare withoutPreemption_lift [wp]
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_invalidateTLB_ASID no_irq_setHardwareASID
no_irq_setCurrentPD no_irq_invalidateTLB_VAASID
no_irq_cleanByVA_PoU
simp: crunch_simps ignore: getObject setObject)
simp: crunch_simps armv_contextSwitch_HWASID_def ignore: getObject setObject)
lemma finaliseSlot_IRQInactive':
"s \<turnstile> \<lbrace>valid_irq_states'\<rbrace> finaliseSlot' a b

4
proof/refine/PageTableDuplicates.thy
View File

@ -1697,7 +1697,7 @@ lemma lookupPTSlot_aligned:
crunch valid_arch_state'[wp]:
flushPage valid_arch_state'
(wp: crunch_wps simp: crunch_simps unless_def
(wp: crunch_wps getHWASID_valid_arch' simp: crunch_simps unless_def
ignore:getObject updateObject setObject)
crunch valid_arch_state'[wp]:
@ -1768,7 +1768,7 @@ crunch ko_wp_at'[wp]:
ignore:getObject updateObject setObject)
crunch ko_wp_at'[wp]:
setCurrentASID "\<lambda>s. ko_wp_at' P p s"
armv_contextSwitch "\<lambda>s. ko_wp_at' P p s"
(wp: crunch_wps simp: crunch_simps unless_def
ignore:getObject updateObject setObject)

150
proof/refine/VSpace_R.thy
View File

@ -482,7 +482,7 @@ lemma get_hw_asid_corres:
apply simp
done
lemma set_current_asid_corres:
lemma arm_context_switch_corres:
"corres dc
(pd_at_asid a pd and K (a \<noteq> 0 \<and> a \<le> mask asid_bits)
and unique_table_refs o caps_of_state
@ -491,15 +491,15 @@ lemma set_current_asid_corres:
and pspace_aligned and pspace_distinct
and valid_arch_state)
(pspace_aligned' and pspace_distinct' and no_0_obj')
(set_current_asid a) (setCurrentASID a)"
apply (simp add: set_current_asid_def setCurrentASID_def)
(arm_context_switch pd a) (armv_contextSwitch pd a)"
apply (simp add: arm_context_switch_def armv_contextSwitch_def armv_contextSwitch_HWASID_def)
apply (rule corres_guard_imp)
apply (rule corres_split_eqr [OF _ get_hw_asid_corres[where pd=pd]])
apply (rule corres_machine_op)
apply (rule corres_no_failI)
apply (rule no_fail_setHardwareASID)
apply fastforce
apply (wp | simp)+
apply (rule corres_rel_imp)
apply (rule corres_underlying_trivial)
apply (rule no_fail_pre)
apply (wp no_fail_setCurrentPD no_fail_setHardwareASID no_irq_setCurrentPD | clarsimp)+
done
lemma hv_corres:
@ -651,6 +651,25 @@ lemma find_pd_for_asid_pd_at_asid_again:
apply clarsimp+
done
lemmas setCurrentPD_no_fails = no_fail_dsb no_fail_isb no_fail_writeTTBR0
lemmas setCurrentPD_no_irqs = no_irq_dsb no_irq_isb no_irq_writeTTBR0
lemma setCurrentPD_corres:
"corres dc \<top> \<top> (do_machine_op (setCurrentPD addr)) (doMachineOp (setCurrentPD addr))"
apply (simp add: setCurrentPD_def)
apply (rule corres_machine_op)
apply (rule corres_guard_imp)
apply (rule corres_split_eqr)
apply (rule corres_split_eqr)
apply (rule corres_rel_imp)
apply (wp
| rule corres_underlying_trivial
| rule setCurrentPD_no_fails
| rule setCurrentPD_no_irqs
| simp add: dc_def)+
done
lemma set_vm_root_corres:
"corres dc (tcb_at t and valid_arch_state and valid_objs and valid_asid_map
and unique_table_refs o caps_of_state and valid_vs_lookup
@ -662,18 +681,14 @@ lemma set_vm_root_corres:
proof -
have P: "corres dc \<top> \<top>
(do global_pd \<leftarrow> gets (arm_global_pd \<circ> arch_state);
do_machine_op (setCurrentPD (Platform.addrFromPPtr global_pd))
do_machine_op (MachineOps.setCurrentPD (Platform.addrFromPPtr global_pd))
od)
(do globalPD \<leftarrow> gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp (setCurrentPD (addrFromPPtr globalPD))
od)"
apply (rule corres_guard_imp)
apply (rule corres_split_eqr)
apply (rule corres_machine_op)
apply (rule corres_rel_imp)
apply (rule corres_underlying_trivial)
apply (rule no_fail_setCurrentPD)
apply simp
apply (rule setCurrentPD_corres)
apply (subst corres_gets)
apply (clarsimp simp: state_relation_def arch_state_relation_def)
apply (wp | simp)+
@ -695,7 +710,7 @@ proof -
done
show ?thesis
unfolding set_vm_root_def setVMRoot_def locateSlot_def
getThreadVSpaceRoot_def armv_contextSwitch_def
getThreadVSpaceRoot_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
@ -738,12 +753,8 @@ proof -
apply (simp add: lookup_failure_map_def)
apply simp
apply simp
apply (rule corres_split)
apply (rule_tac pd=pd' in set_current_asid_corres)
apply (rule corres_machine_op)
apply (rule corres_underlying_trivial)
apply (rule no_fail_setCurrentPD)
apply (wp | simp | wp_once hoare_drop_imps)+
apply (rule arm_context_switch_corres)
apply (wp | simp | wp_once hoare_drop_imps)+
apply (simp add: whenE_def split del: split_if, wp)[1]
apply (rule find_pd_for_asid_pd_at_asid_again)
apply wp
@ -1085,7 +1096,7 @@ lemma set_vm_root_for_flush_corres:
(pspace_aligned' and pspace_distinct' and no_0_obj')
(set_vm_root_for_flush pd asid)
(setVMRootForFlush pd asid)"
proof -
proof -
have X: "corres op = (pd_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask asid_bits)
and valid_asid_map and valid_vs_lookup
and valid_arch_objs and valid_global_objs
@ -1093,22 +1104,16 @@ proof -
and valid_arch_state
and pspace_aligned and pspace_distinct)
(pspace_aligned' and pspace_distinct' and no_0_obj')
(do y \<leftarrow> do_machine_op (setCurrentPD (Platform.addrFromPPtr pd));
y \<leftarrow> set_current_asid asid;
(do arm_context_switch pd asid;
return True
od)
(do y \<leftarrow> doMachineOp (setCurrentPD (addrFromPPtr pd));
y \<leftarrow> setCurrentASID asid;
(do armv_contextSwitch pd asid;
return True
od)"
apply (rule corres_guard_imp)
apply (rule corres_split [OF _ corres_machine_op [where r=dc]])
apply (rule corres_split [OF _ set_current_asid_corres[where pd=pd]])
apply (rule corres_trivial, simp)
apply wp
apply (rule corres_Id, rule refl, simp)
apply (rule no_fail_setCurrentPD)
apply (wp | simp)+
apply (rule corres_split [OF _ arm_context_switch_corres])
apply (rule corres_trivial)
apply (wp | simp)+
done
show ?thesis
apply (simp add: set_vm_root_for_flush_def setVMRootForFlush_def getThreadVSpaceRoot_def locateSlot_def)
@ -1128,7 +1133,7 @@ proof -
capPDBasePtr (capCap rv') = pd")
apply (case_tac rv, simp_all add: isCap_simps)[1]
apply (case_tac arch_cap, auto)[1]
apply (case_tac rv, simp_all add: isCap_simps X[simplified])[1]
apply (case_tac rv, simp_all add: isCap_simps [simplified] X[simplified])[1]
apply (case_tac arch_cap, auto simp: X[simplified] split: option.splits)[1]
apply (simp add: cte_map_def objBits_simps tcb_cnode_index_def tcbVTableSlot_def to_bl_1)
apply wp
@ -1139,7 +1144,7 @@ proof -
done
qed
crunch typ_at' [wp]: setCurrentASID "\<lambda>s. P (typ_at' T p s)"
crunch typ_at' [wp]: armv_contextSwitch "\<lambda>s. P (typ_at' T p s)"
(simp: crunch_simps)
crunch typ_at' [wp]: findPDForASID "\<lambda>s. P (typ_at' T p s)"
@ -2642,9 +2647,9 @@ lemma pap_corres:
apply (clarsimp simp: cte_wp_at_ctes_of valid_apinv'_def)
done
lemma setCurrentASID_obj_at [wp]:
"\<lbrace>\<lambda>s. P (obj_at' P' t s)\<rbrace> setCurrentASID a \<lbrace>\<lambda>rv s. P (obj_at' P' t s)\<rbrace>"
apply (simp add: setCurrentASID_def getHWASID_def)
lemma armv_contextSwitch_obj_at [wp]:
"\<lbrace>\<lambda>s. P (obj_at' P' t s)\<rbrace> armv_contextSwitch pd a \<lbrace>\<lambda>rv s. P (obj_at' P' t s)\<rbrace>"
apply (simp add: armv_contextSwitch_def armv_contextSwitch_HWASID_def getHWASID_def)
apply (wp doMachineOp_obj_at|wpc|simp)+
done
@ -2744,28 +2749,61 @@ lemma getHWASID_invs_no_cicd':
apply simp
done
lemma setCurrentASID_invs [wp]:
"\<lbrace>invs'\<rbrace> setCurrentASID asid \<lbrace>\<lambda>rv. invs'\<rbrace>"
apply (simp add: setCurrentASID_def)
apply (wp dmo_invs' no_irq_setHardwareASID)
lemmas armv_ctxt_sw_defs = armv_contextSwitch_HWASID_def setHardwareASID_def setCurrentPD_def
writeTTBR0_def isb_def dsb_def
lemma dmo_armv_contextSwitch_HWASID_invs'[wp]:
"\<lbrace>invs'\<rbrace> doMachineOp (armv_contextSwitch_HWASID pd hwasid) \<lbrace>\<lambda>_. invs'\<rbrace>"
apply (wp dmo_invs')
apply (simp add: armv_contextSwitch_HWASID_def)
apply (wp no_irq_setCurrentPD no_irq_setHardwareASID)
apply safe
apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p = underlying_memory m p"
in use_valid)
apply (simp add: machine_op_lift_def machine_rest_lift_def split_def armv_ctxt_sw_defs
| wp)+
done
lemma dmo_armv_contextSwitch_HWASID_invs_no_cicd':
"\<lbrace>invs_no_cicd'\<rbrace> doMachineOp (armv_contextSwitch_HWASID pd hwasid) \<lbrace>\<lambda>_. invs_no_cicd'\<rbrace>"
apply (wp dmo_invs_no_cicd')
apply (simp add: armv_contextSwitch_HWASID_def)
apply (wp no_irq_setCurrentPD no_irq_setHardwareASID)
apply safe
apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p = underlying_memory m p"
in use_valid)
apply (simp add: machine_op_lift_def machine_rest_lift_def split_def armv_ctxt_sw_defs
| wp)+
done
lemma no_irq_armv_contextSwitch_HWASID:
"no_irq (armv_contextSwitch_HWASID pd hwasid)"
apply (simp add: armv_contextSwitch_HWASID_def)
apply (wp no_irq_setCurrentPD no_irq_setHardwareASID)
done
lemma armv_contextSwitch_invs [wp]:
"\<lbrace>invs'\<rbrace> armv_contextSwitch pd asid \<lbrace>\<lambda>rv. invs'\<rbrace>"
apply (simp add: armv_contextSwitch_def)
apply (wp dmo_invs' no_irq_armv_contextSwitch_HWASID)
apply (rule hoare_post_imp[rotated], wp)
apply clarsimp
apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p = underlying_memory m p"
in use_valid)
apply (clarsimp simp: setHardwareASID_def machine_op_lift_def
machine_rest_lift_def split_def | wp)+
apply (simp add: machine_op_lift_def machine_rest_lift_def split_def armv_ctxt_sw_defs
| wp)+
done
lemma setCurrentASID_invs_no_cicd':
"\<lbrace>invs_no_cicd'\<rbrace> setCurrentASID asid \<lbrace>\<lambda>rv. invs_no_cicd'\<rbrace>"
apply (simp add: setCurrentASID_def)
apply (wp dmo_invs_no_cicd' no_irq_setHardwareASID)
lemma armv_contextSwitch_invs_no_cicd':
"\<lbrace>invs_no_cicd'\<rbrace> armv_contextSwitch pd asid \<lbrace>\<lambda>rv. invs_no_cicd'\<rbrace>"
apply (simp add: armv_contextSwitch_def armv_contextSwitch_HWASID_def)
apply (wp dmo_invs_no_cicd' no_irq_setHardwareASID no_irq_setCurrentPD)
apply (rule hoare_post_imp[rotated], wp getHWASID_invs_no_cicd')
apply clarsimp
apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p = underlying_memory m p"
in use_valid)
apply (clarsimp simp: setHardwareASID_def machine_op_lift_def
machine_rest_lift_def split_def | wp)+
apply (clarsimp simp: machine_op_lift_def machine_rest_lift_def split_def armv_ctxt_sw_defs | wp)+
done
lemma dmo_setCurrentPD_invs'[wp]:
@ -2774,7 +2812,7 @@ lemma dmo_setCurrentPD_invs'[wp]:
apply clarsimp
apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p = underlying_memory m p"
in use_valid)
apply (clarsimp simp: setCurrentPD_def machine_op_lift_def
apply (clarsimp simp: setCurrentPD_def machine_op_lift_def writeTTBR0_def dsb_def isb_def
machine_rest_lift_def split_def | wp)+
done
@ -2784,24 +2822,26 @@ lemma dmo_setCurrentPD_invs_no_cicd':
apply clarsimp
apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p = underlying_memory m p"
in use_valid)
apply (clarsimp simp: setCurrentPD_def machine_op_lift_def
apply (clarsimp simp: setCurrentPD_def machine_op_lift_def writeTTBR0_def dsb_def isb_def
machine_rest_lift_def split_def | wp)+
done
lemma setVMRoot_invs [wp]:
"\<lbrace>invs'\<rbrace> setVMRoot p \<lbrace>\<lambda>rv. invs'\<rbrace>"
apply (simp add: setVMRoot_def getThreadVSpaceRoot_def armv_contextSwitch_def)
apply (simp add: setVMRoot_def getThreadVSpaceRoot_def)
apply (rule hoare_pre)
apply (wp hoare_drop_imps | wpcw
| simp add: whenE_def checkPDNotInASIDMap_def armv_contextSwitch_def split del: split_if)+
| simp add: whenE_def checkPDNotInASIDMap_def split del: split_if)+
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)
apply (rule hoare_pre)
apply (wp dmo_setCurrentPD_invs_no_cicd' hoare_drop_imps setCurrentASID_invs_no_cicd' | wpcw
| simp add: whenE_def checkPDNotInASIDMap_def armv_contextSwitch_def split del: split_if)+
apply (wp hoare_drop_imps armv_contextSwitch_invs_no_cicd' getHWASID_invs_no_cicd'
dmo_setCurrentPD_invs_no_cicd'
| wpcw
| simp add: whenE_def checkPDNotInASIDMap_def split del: split_if)+
done
crunch nosch [wp]: setVMRoot "\<lambda>s. P (ksSchedulerAction s)"

28
spec/abstract/ArchVSpace_A.thy
View File

@ -283,14 +283,20 @@ get_hw_asid :: "asid \<Rightarrow> (hardware_asid,'z::state_ext) s_monad" where
od)
od"
text {* Set the current virtual ASID by setting the hardware ASID to one
associated with it. *}
abbreviation
"arm_context_switch_hwasid pd hwasid \<equiv> do
setCurrentPD $ addrFromPPtr pd;
setHardwareASID hwasid
od"
definition
set_current_asid :: "asid \<Rightarrow> (unit,'z::state_ext) s_monad" where
"set_current_asid asid \<equiv> do
hw_asid \<leftarrow> get_hw_asid asid;
do_machine_op $ setHardwareASID hw_asid
od"
arm_context_switch :: "word32 \<Rightarrow> asid \<Rightarrow> (unit, 'z::state_ext) s_monad"
where
"arm_context_switch pd asid \<equiv> do
hwasid \<leftarrow> get_hw_asid asid;
do_machine_op $ arm_context_switch_hwasid pd hwasid
od"
text {* Switch into the address space of a given thread or the global address
space if none is correctly configured. *}
@ -303,10 +309,7 @@ definition
ArchObjectCap (PageDirectoryCap pd (Some asid)) \<Rightarrow> doE
pd' \<leftarrow> find_pd_for_asid asid;
whenE (pd \<noteq> pd') $ throwError InvalidRoot;
liftE $ do
do_machine_op $ setCurrentPD $ addrFromPPtr pd;
set_current_asid asid
od
liftE $ arm_context_switch pd asid
odE
| _ \<Rightarrow> throwError InvalidRoot) <catch>
(\<lambda>_. do
@ -368,8 +371,7 @@ set_vm_root_for_flush :: "word32 \<Rightarrow> asid \<Rightarrow> (bool,'z::stat
ArchObjectCap (PageDirectoryCap cur_pd (Some _)) \<Rightarrow> return (cur_pd \<noteq> pd)
| _ \<Rightarrow> return True);
(if not_is_pd then do
do_machine_op $ setCurrentPD $ addrFromPPtr pd;
set_current_asid asid;
arm_context_switch pd asid;
return True
od
else return False)

6
spec/design/ArchVSpaceDecls_H.thy
View File

@ -128,6 +128,9 @@ unmapPage :: "vmpage_size \<Rightarrow> asid \<Rightarrow> vptr \<Rightarrow> ma
consts
checkMappingPPtr :: "machine_word \<Rightarrow> vmpage_size \<Rightarrow> (machine_word) + (machine_word) \<Rightarrow> ( lookup_failure , unit ) kernel_f"
consts
armv_contextSwitch_HWASID :: "machine_word \<Rightarrow> hardware_asid \<Rightarrow> unit machine_monad"
consts
armv_contextSwitch :: "machine_word \<Rightarrow> asid \<Rightarrow> unit kernel"
@ -176,9 +179,6 @@ findFreeHWASID :: "hardware_asid kernel"
consts
getHWASID :: "asid \<Rightarrow> hardware_asid kernel"
consts
setCurrentASID :: "asid \<Rightarrow> unit kernel"
consts
doFlush :: "flush_type \<Rightarrow> vptr \<Rightarrow> vptr \<Rightarrow> paddr \<Rightarrow> unit machine_monad"

19
spec/design/ArchVSpace_H.thy
View File

@ -666,10 +666,16 @@ defs checkMappingPPtr_def:
odE)
)"
defs armv_contextSwitch_HWASID_def:
"armv_contextSwitch_HWASID pd hwasid \<equiv> (do
setCurrentPD $ addrFromPPtr pd;
setHardwareASID hwasid
od)"
defs armv_contextSwitch_def:
"armv_contextSwitch pd asid \<equiv> (do
doMachineOp $ setCurrentPD $ addrFromPPtr pd;
setCurrentASID asid
hwasid \<leftarrow> getHWASID asid;
doMachineOp $ armv_contextSwitch_HWASID pd hwasid
od)"
defs setVMRoot_def:
@ -707,8 +713,7 @@ defs setVMRootForFlush_def:
if isArchObjectCap v8 \<and> isPageDirectoryCap (capCap v8) \<and> capPDMappedASID (capCap v8) \<noteq> None \<and> capPDBasePtr (capCap v8) = pd
then let cur_pd = pd in return False
else (do
doMachineOp $ setCurrentPD $ addrFromPPtr pd;
setCurrentASID asid;
armv_contextSwitch pd asid;
return True
od)
)
@ -855,12 +860,6 @@ defs getHWASID_def:
)
od)"
defs setCurrentASID_def:
"setCurrentASID asid\<equiv> (do
hw_asid \<leftarrow> getHWASID asid;
doMachineOp $ setHardwareASID hw_asid
od)"
defs doFlush_def:
"doFlush x0 vstart vend pstart\<equiv> (case x0 of
Clean \<Rightarrow>

2
spec/design/skel/Hardware_H.thy
View File

@ -14,7 +14,7 @@ imports
State_H
begin
#INCLUDE_HASKELL SEL4/Machine/Hardware/ARM.lhs NOT getMemoryRegions getDeviceRegions getKernelDevices loadWord storeWord storeWordVM getActiveIRQ ackInterrupt maskInterrupt configureTimer resetTimer debugPrint getRestartPC setNextPC clearMemory clearMemoryVM initMemory freeMemory setCurrentPD setGlobalPD setTTBCR setHardwareASID invalidateTLB invalidateTLB_ASID invalidateTLB_VAASID cleanByVA cleanByVA_PoU invalidateByVA invalidateByVA_I invalidate_I_PoU cleanInvalByVA branchFlush clean_D_PoU cleanInvalidate_D_PoC cleanInvalidate_D_PoU cleanInvalidateL2Range invalidateL2Range cleanL2Range isb dsb dmb getIFSR getDFSR getFAR HardwareASID wordFromPDE wordFromPTE VMFaultType VMPageSize pageBits pageBitsForSize toPAddr cacheLineBits cacheLine lineStart cacheRangeOp cleanCacheRange_PoC cleanInvalidateCacheRange_RAM cleanCacheRange_RAM cleanCacheRange_PoU invalidateCacheRange_RAM invalidateCacheRange_I branchFlushRange cleanCaches_PoU cleanInvalidateL1Caches addrFromPPtr ptrFromPAddr
#INCLUDE_HASKELL SEL4/Machine/Hardware/ARM.lhs NOT getMemoryRegions getDeviceRegions getKernelDevices loadWord storeWord storeWordVM getActiveIRQ ackInterrupt maskInterrupt configureTimer resetTimer debugPrint getRestartPC setNextPC clearMemory clearMemoryVM initMemory freeMemory writeTTBR0 setCurrentPD setGlobalPD setTTBCR setHardwareASID invalidateTLB invalidateTLB_ASID invalidateTLB_VAASID cleanByVA cleanByVA_PoU invalidateByVA invalidateByVA_I invalidate_I_PoU cleanInvalByVA branchFlush clean_D_PoU cleanInvalidate_D_PoC cleanInvalidate_D_PoU cleanInvalidateL2Range invalidateL2Range cleanL2Range isb dsb dmb getIFSR getDFSR getFAR HardwareASID wordFromPDE wordFromPTE VMFaultType VMPageSize pageBits pageBitsForSize toPAddr cacheLineBits cacheLine lineStart cacheRangeOp cleanCacheRange_PoC cleanInvalidateCacheRange_RAM cleanCacheRange_RAM cleanCacheRange_PoU invalidateCacheRange_RAM invalidateCacheRange_I branchFlushRange cleanCaches_PoU cleanInvalidateL1Caches addrFromPPtr ptrFromPAddr
#INCLUDE_HASKELL SEL4/Machine/Hardware/ARM.lhs instanceproofs NOT HardwareASID VMFaultType VMPageSize

27
spec/design/version
View File

@ -1,3 +1,26 @@
Built from git repo at ../../../seL4/haskell by kleing
Built from git repo at /home/jbeeren/nfshome/work/fp/seL4/haskell by jbeeren
eff5683 add support for XN attribute in Haskell
Generated from changeset:
a3c1a39 Minor change to haskell implementation of armv_contextSwitch
Warning - uncomitted changes used:
M src/SEL4/Kernel/VSpace/ARM.lhs
?? ../api/
?? ../arch/
?? ../kernel.elf
?? ../kernel.elf.strip
?? ../kernel.o
?? ../kernel_all.c
?? ../kernel_all.c_pp
?? ../kernel_final.c
?? ../kernel_final.s
?? ../linker.lds_pp
?? ../parsetab.py
?? ../plat/
?? ../sources_list_updated
?? ../src/arch/arm/armv/armv6/machine_asm.o
?? ../src/arch/arm/halt.o
?? ../src/arch/arm/head.o
?? ../src/arch/arm/idle.o
?? ../src/arch/arm/traps.o

15
spec/machine/MachineOps.thy
View File

@ -184,10 +184,11 @@ definition
where "resetTimer \<equiv> machine_op_lift resetTimer_impl"
consts
setCurrentPD_impl :: "paddr \<Rightarrow> unit machine_rest_monad"
writeTTBR0_impl :: "paddr \<Rightarrow> unit machine_rest_monad"
definition
setCurrentPD :: "paddr \<Rightarrow> unit machine_monad"
where "setCurrentPD pd \<equiv> machine_op_lift (setCurrentPD_impl pd)"
writeTTBR0 :: "paddr \<Rightarrow> unit machine_monad"
where "writeTTBR0 pd \<equiv> machine_op_lift (writeTTBR0_impl pd)"
consts
setHardwareASID_impl :: "hardware_asid \<Rightarrow> unit machine_rest_monad"
@ -218,7 +219,13 @@ definition
where "dmb \<equiv> machine_op_lift dmb_impl"
definition
setCurrentPD :: "paddr \<Rightarrow> unit machine_monad"
where "setCurrentPD pd \<equiv> do
dsb;
writeTTBR0 pd;
isb
od"
consts
invalidateTLB_impl :: "unit machine_rest_monad"