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

crefine: add abbreviations for global page table addresses

This commit is contained in:
Matthew Brecknell 2019-05-02 17:11:58 +10:00
parent 976eca1a28
commit 206ee07c58
15 changed files with 54 additions and 52 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
proof/crefine/ARM/Detype_C.thy
View File

@ -1726,14 +1726,13 @@ proof -
}
moreover
{
assume "s' \<Turnstile>\<^sub>c (Ptr::(32 word \<Rightarrow> (pde_C[4096]) ptr)) (symbol_table ''armKSGlobalPD'')"
assume "s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr"
moreover
from sr ptr_refs have "ptr_span (pd_Ptr (symbol_table ''armKSGlobalPD''))
from sr ptr_refs have "ptr_span armKSGlobalPD_Ptr
\<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 (Ptr::(32 word \<Rightarrow> (pde_C[4096]) ptr)) (symbol_table ''armKSGlobalPD'')"
have "hrs_htd (hrs_htd_update (typ_region_bytes ptr bits) (t_hrs_' (globals s'))) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr"
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)

3
proof/crefine/ARM/Retype_C.thy
View File

@ -5828,8 +5828,7 @@ lemma ccorres_typ_region_bytes_dummy:
apply (simp add: invs_pspace_aligned')+
apply (frule typ_bytes_cpspace_relation_clift_devicedata)
apply (simp add: invs_pspace_aligned')+
apply (frule typ_bytes_cpspace_relation_clift_gptr[where
ptr'="pd_Ptr (symbol_table ''armKSGlobalPD'')"])
apply (frule typ_bytes_cpspace_relation_clift_gptr[where ptr'="armKSGlobalPD_Ptr"])
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])

4
proof/crefine/ARM/SR_lemmas_C.thy
View File

@ -2037,9 +2037,7 @@ lemma cap_get_tag_isCap_ArchObject2:
simp add: isArchCap_tag_def2 cap_tag_defs)+
lemma rf_sr_armKSGlobalPD:
"(s, s') \<in> rf_sr
\<Longrightarrow> armKSGlobalPD (ksArchState s)
= symbol_table ''armKSGlobalPD''"
"(s, s') \<in> rf_sr \<Longrightarrow> armKSGlobalPD (ksArchState s) = ptr_val armKSGlobalPD_Ptr"
by (clarsimp simp: rf_sr_def cstate_relation_def Let_def carch_state_relation_def carch_globals_def)
lemma ghost_assertion_size_logic':

15
proof/crefine/ARM/StateRelation_C.thy
View File

@ -113,11 +113,17 @@ locale kernel = kernel_all_substitute + state_rel
context state_rel
begin
abbreviation armKSGlobalPD_Ptr :: "(pde_C[4096]) ptr" where
"armKSGlobalPD_Ptr \<equiv> pd_Ptr (symbol_table ''armKSGlobalPD'')"
abbreviation armKSGlobalPT_Ptr :: "(pte_C[256]) ptr" where
"armKSGlobalPT_Ptr \<equiv> pt_Ptr (symbol_table ''armKSGlobalPT'')"
(* relates fixed adresses *)
definition
"carch_globals s \<equiv>
(armKSGlobalPD s = symbol_table ''armKSGlobalPD'') \<and>
(armKSGlobalPTs s = [symbol_table ''armKSGlobalPT''])"
(armKSGlobalPD s = ptr_val armKSGlobalPD_Ptr) \<and>
(armKSGlobalPTs s = [ptr_val armKSGlobalPT_Ptr])"
definition
carch_state_relation :: "Arch.kernel_state \<Rightarrow> globals \<Rightarrow> bool"
@ -722,9 +728,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
(pd_Ptr (symbol_table ''armKSGlobalPD'')) \<and>
ptr_span (pd_Ptr (symbol_table ''armKSGlobalPD'')) \<subseteq> kernel_data_refs \<and>
h_t_valid (hrs_htd (t_hrs_' cstate)) c_guard armKSGlobalPD_Ptr \<and>
ptr_span armKSGlobalPD_Ptr \<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>

8
proof/crefine/ARM/VSpace_C.thy
View File

@ -1019,8 +1019,8 @@ lemma ccorres_pre_gets_armKSGlobalPD_ksArchState:
assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c"
shows "ccorres r xf
(\<lambda>s. (\<forall>rv. armKSGlobalPD (ksArchState s) = rv \<longrightarrow> P rv s))
(P' (ptr_val ((Ptr ::(32 word \<Rightarrow> (pde_C[4096]) ptr)) (symbol_table ''armKSGlobalPD''))))
hs (gets (armKSGlobalPD \<circ> ksArchState) >>= (\<lambda>rv. f rv)) c"
(P' (ptr_val armKSGlobalPD_Ptr))
hs (gets (armKSGlobalPD \<circ> ksArchState) >>= (\<lambda>rv. f rv)) c"
apply (rule ccorres_guard_imp)
apply (rule ccorres_symb_exec_l)
defer
@ -1388,9 +1388,7 @@ lemma armv_contextSwitch_ccorres:
(* FIXME: move *)
lemma ccorres_h_t_valid_armKSGlobalPD:
"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[4096]) ptr)) (symbol_table ''armKSGlobalPD'')} f';;
g')"
ccorres r xf P P' hs f (Guard C_Guard {s'. s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr} f';; g')"
apply (rule ccorres_guard_imp2)
apply (rule ccorres_move_c_guards[where P = \<top>])
apply clarsimp

7
proof/crefine/ARM_HYP/Detype_C.thy
View File

@ -1833,14 +1833,13 @@ proof -
}
moreover
{
assume "s' \<Turnstile>\<^sub>c (Ptr::(32 word \<Rightarrow> (pde_C[2048]) ptr)) (symbol_table ''armUSGlobalPD'')"
assume "s' \<Turnstile>\<^sub>c armUSGlobalPD_Ptr"
moreover
from sr ptr_refs have "ptr_span (pd_Ptr (symbol_table ''armUSGlobalPD''))
from sr ptr_refs have "ptr_span armUSGlobalPD_Ptr
\<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 (Ptr::(32 word \<Rightarrow> (pde_C[2048]) ptr)) (symbol_table ''armUSGlobalPD'')"
have "hrs_htd (hrs_htd_update (typ_region_bytes ptr bits) (t_hrs_' (globals s'))) \<Turnstile>\<^sub>t armUSGlobalPD_Ptr"
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)

3
proof/crefine/ARM_HYP/Retype_C.thy
View File

@ -7139,8 +7139,7 @@ lemma ccorres_typ_region_bytes_dummy:
apply (simp add: invs_pspace_aligned')+
apply (frule typ_bytes_cpspace_relation_clift_vcpu)
apply (simp add: invs_pspace_aligned')+
apply (frule typ_bytes_cpspace_relation_clift_gptr[where
ptr'="pd_Ptr (symbol_table ''armUSGlobalPD'')"])
apply (frule typ_bytes_cpspace_relation_clift_gptr[where ptr'="armUSGlobalPD_Ptr"])
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])

3
proof/crefine/ARM_HYP/SR_lemmas_C.thy
View File

@ -2182,8 +2182,7 @@ lemma cap_get_tag_isCap_ArchObject2:
lemma rf_sr_armUSGlobalPD:
"(s, s') \<in> rf_sr
\<Longrightarrow> armUSGlobalPD (ksArchState s)
= symbol_table ''armUSGlobalPD''"
\<Longrightarrow> armUSGlobalPD (ksArchState s) = ptr_val armUSGlobalPD_Ptr"
by (clarsimp simp: rf_sr_def cstate_relation_def Let_def carch_state_relation_def carch_globals_def)
lemma ghost_assertion_size_logic':

10
proof/crefine/ARM_HYP/StateRelation_C.thy
View File

@ -109,10 +109,13 @@ locale kernel = kernel_all_substitute + state_rel
context state_rel
begin
abbreviation armUSGlobalPD_Ptr :: "(pde_C[2048]) ptr" where
"armUSGlobalPD_Ptr \<equiv> pd_Ptr (symbol_table ''armUSGlobalPD'')"
(* relates fixed adresses *)
definition
"carch_globals s \<equiv>
(armUSGlobalPD s = symbol_table ''armUSGlobalPD'')"
armUSGlobalPD s = ptr_val armUSGlobalPD_Ptr"
(* FIXME ARMHYP is this the right place? MOVE? *)
definition
@ -749,9 +752,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
(pd_Ptr (symbol_table ''armUSGlobalPD'')) \<and>
ptr_span (pd_Ptr (symbol_table ''armUSGlobalPD'')) \<subseteq> kernel_data_refs \<and>
h_t_valid (hrs_htd (t_hrs_' cstate)) c_guard armUSGlobalPD_Ptr \<and>
ptr_span armUSGlobalPD_Ptr \<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>

8
proof/crefine/ARM_HYP/VSpace_C.thy
View File

@ -1100,8 +1100,8 @@ lemma ccorres_pre_gets_armUSGlobalPD_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"
(P' (ptr_val armUSGlobalPD_Ptr)) hs
(gets (armUSGlobalPD \<circ> ksArchState) >>= (\<lambda>rv. f rv)) c"
apply (rule ccorres_guard_imp)
apply (rule ccorres_symb_exec_l)
defer
@ -1473,9 +1473,7 @@ lemma armv_contextSwitch_ccorres:
(* FIXME: move *)
lemma ccorres_h_t_valid_armUSGlobalPD:
"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')"
ccorres r xf P P' hs f (Guard C_Guard {s'. s' \<Turnstile>\<^sub>c armUSGlobalPD_Ptr} f';; g')"
apply (rule ccorres_guard_imp2)
apply (rule ccorres_move_c_guards[where P = \<top>])
apply clarsimp

7
proof/crefine/X64/Detype_C.thy
View File

@ -1794,14 +1794,13 @@ proof -
moreover
{
assume "s' \<Turnstile>\<^sub>c pml4_Ptr (symbol_table ''x64KSSKIMPML4'')"
assume "s' \<Turnstile>\<^sub>c x64KSSKIMPML4_Ptr"
moreover
from sr ptr_refs have "ptr_span (pd_Ptr (symbol_table ''x64KSSKIMPML4''))
from sr ptr_refs have "ptr_span x64KSSKIMPML4_Ptr
\<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 ''x64KSSKIMPML4'')"
have "hrs_htd (hrs_htd_update (typ_region_bytes ptr bits) (t_hrs_' (globals s'))) \<Turnstile>\<^sub>t x64KSSKIMPML4_Ptr"
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)

3
proof/crefine/X64/Retype_C.thy
View File

@ -7365,8 +7365,7 @@ lemma ccorres_typ_region_bytes_dummy:
apply (simp add: invs_pspace_aligned')+
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 ''x64KSSKIMPML4'')"])
apply (frule typ_bytes_cpspace_relation_clift_gptr[where ptr'="x64KSSKIMPML4_Ptr"])
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])

2
proof/crefine/X64/SR_lemmas_C.thy
View File

@ -2261,7 +2261,7 @@ lemma cap_lift_Some_CapD:
by (auto simp: cap_lifts cap_lift_defs)
lemma rf_sr_x64KSSKIMPML4:
"(s, s') \<in> rf_sr \<Longrightarrow> x64KSSKIMPML4 (ksArchState s) = symbol_table ''x64KSSKIMPML4''"
"(s, s') \<in> rf_sr \<Longrightarrow> x64KSSKIMPML4 (ksArchState s) = ptr_val x64KSSKIMPML4_Ptr"
by (clarsimp simp: rf_sr_def cstate_relation_def Let_def carch_state_relation_def carch_globals_def)
lemma ghost_assertion_size_logic':

19
proof/crefine/X64/StateRelation_C.thy
View File

@ -92,11 +92,20 @@ locale kernel = kernel_all_substitute + state_rel
context state_rel
begin
abbreviation x64KSSKIMPML4_Ptr :: "(pml4e_C[512]) ptr" where
"x64KSSKIMPML4_Ptr \<equiv> pml4_Ptr (symbol_table ''x64KSSKIMPML4'')"
abbreviation x64KSSKIMPDPT_Ptr :: "(pdpte_C[512]) ptr" where
"x64KSSKIMPDPT_Ptr \<equiv> pdpt_Ptr (symbol_table ''x64KSSKIMPDPT'')"
abbreviation x64KSSKIMPD_Ptr :: "(pde_C[512]) ptr" where
"x64KSSKIMPD_Ptr \<equiv> pd_Ptr (symbol_table ''x64KSSKIMPD'')"
(* relates fixed adresses *)
definition
"carch_globals s \<equiv> (x64KSSKIMPML4 s = symbol_table ''x64KSSKIMPML4'')
\<and> (x64KSSKIMPDPTs s = [symbol_table ''x64KSSKIMPDPT''])
\<and> (x64KSSKIMPDs s = [symbol_table ''x64KSSKIMPD''])
"carch_globals s \<equiv> (x64KSSKIMPML4 s = ptr_val x64KSSKIMPML4_Ptr)
\<and> (x64KSSKIMPDPTs s = [ptr_val x64KSSKIMPDPT_Ptr])
\<and> (x64KSSKIMPDs s = [ptr_val x64KSSKIMPD_Ptr])
\<and> (x64KSSKIMPTs s = [])"
(* FIXME x64: DON'T DELETE!
@ -929,8 +938,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 ''x64KSSKIMPML4'')) \<and>
ptr_span (pml4_Ptr (symbol_table ''x64KSSKIMPML4'')) \<subseteq> kernel_data_refs \<and>
h_t_valid (hrs_htd (t_hrs_' cstate)) c_guard x64KSSKIMPML4_Ptr \<and>
ptr_span x64KSSKIMPML4_Ptr \<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>

7
proof/crefine/X64/VSpace_C.thy
View File

@ -1017,8 +1017,8 @@ 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. 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"
(P' (ptr_val x64KSSKIMPML4_Ptr))
hs (gets (x64KSSKIMPML4 \<circ> ksArchState) >>= (\<lambda>rv. f rv)) c"
apply (rule ccorres_guard_imp)
apply (rule ccorres_symb_exec_l)
defer
@ -1069,8 +1069,7 @@ context kernel_m begin
(* FIXME: move *)
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 pml4_Ptr (symbol_table ''x64KSSKIMPML4'')} f';; g')"
ccorres r xf P P' hs f (Guard C_Guard {s'. s' \<Turnstile>\<^sub>c x64KSSKIMPML4_Ptr} f';; g')"
apply (rule ccorres_guard_imp2)
apply (rule ccorres_move_c_guards[where P = \<top>])
apply clarsimp