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

CRefine for XN

This commit is contained in:
Gerwin Klein 2014-11-26 17:18:47 +11:00
parent 29eb636d31
commit 0466161f2d
4 changed files with 124 additions and 193 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

80
proof/crefine/Arch_C.thy
View File

@ -900,7 +900,8 @@ definition
definition
"vm_attribs_relation attr attr' \<equiv>
armParityEnabled_CL (vm_attributes_lift attr') = from_bool (armParityEnabled attr)
\<and> armPageCacheable_CL (vm_attributes_lift attr') = from_bool (armPageCacheable attr)"
\<and> armPageCacheable_CL (vm_attributes_lift attr') = from_bool (armPageCacheable attr)
\<and> armExecuteNever_CL (vm_attributes_lift attr') = from_bool (armExecuteNever attr)"
lemma framesize_from_H_eqs:
"(framesize_from_H vsz = scast Kernel_C.ARMSmallPage) = (vsz = ARMSmallPage)"
@ -922,8 +923,8 @@ lemma cpde_relation_pde_case:
"cpde_relation pde cpde
\<Longrightarrow> (case pde of InvalidPDE \<Rightarrow> P
| PageTablePDE _ _ _ \<Rightarrow> Q
| SectionPDE _ _ _ _ _ _ \<Rightarrow> R
| SuperSectionPDE _ _ _ _ _ \<Rightarrow> S)
| SectionPDE _ _ _ _ _ _ _ \<Rightarrow> R
| SuperSectionPDE _ _ _ _ _ _ \<Rightarrow> S)
= (if pde_get_tag cpde = scast pde_pde_invalid then P
else if (pde_get_tag cpde = scast pde_pde_coarse)
\<or> (pde_get_tag cpde \<noteq> scast pde_pde_section) then Q
@ -943,14 +944,14 @@ lemma pde_pde_section_size_0_1:
apply simp
done
lemma pde_bits_from_cacheable_simps:
"shared_bit_from_cacheable (case b of True \<Rightarrow> of_nat 1::word32 | False \<Rightarrow> of_nat 0) = (s_from_cacheable b :: word32)"
"tex_bits_from_cacheable (case b of True \<Rightarrow> of_nat 1::word32 | False \<Rightarrow> of_nat 0) = (tex_from_cacheable b :: word32)"
"iwb_from_cacheable (case b of True \<Rightarrow> of_nat 1 | False \<Rightarrow> of_nat 0) = b_from_cacheable b"
apply (simp_all add:shared_bit_from_cacheable_def s_from_cacheable_def
tex_bits_from_cacheable_def tex_from_cacheable_def iwb_from_cacheable_def b_from_cacheable_def)
apply (case_tac b,simp+)+
done
lemma pde_bits_from_cacheable_simps [simp]:
"shared_bit_from_cacheable (from_bool b) = s_from_cacheable b"
"tex_bits_from_cacheable (from_bool b) = tex_from_cacheable b"
"iwb_from_cacheable (from_bool b) = b_from_cacheable b"
by (simp_all add: shared_bit_from_cacheable_def s_from_cacheable_def
tex_bits_from_cacheable_def tex_from_cacheable_def
iwb_from_cacheable_def b_from_cacheable_def
split: bool.splits)
lemma createSafeMappingEntries_PDE_ccorres:
"ccorres (syscall_error_rel \<currency> (\<lambda>rv rv'. isRight rv \<and> cpde_relation (fst (theRight rv)) (fst rv')
@ -996,15 +997,14 @@ lemma createSafeMappingEntries_PDE_ccorres:
apply (clarsimp simp: if_1_0_0)
apply (clarsimp simp: typ_heap_simps vm_attribs_relation_def
from_bool_mask_simp[unfolded mask_def, simplified])
apply (intro conjI)
apply (rule conjI)
apply (simp add: gen_framesize_to_H_def vm_page_size_defs)
apply (clarsimp simp: pde_get_tag_alt cpde_relation_pde_case
pde_tag_defs fst_throwError_returnOk
pde_range_relation_def ptr_range_to_list_def
exception_defs isRight_def from_bool_def[where b=True]
syscall_error_rel_def syscall_error_to_H_cases)
apply (simp add: cpde_relation_def from_bool_def pde_bits_from_cacheable_simps
of_bool_from_bool)
apply (clarsimp simp: cpde_relation_def true_def false_def)
apply (rule ccorres_Cond_rhs)
apply (simp del: Collect_const)
apply (rule ccorres_rhs_assoc)+
@ -1014,6 +1014,7 @@ lemma createSafeMappingEntries_PDE_ccorres:
apply csymbr
apply csymbr
apply csymbr
apply csymbr
apply (simp add: mapME_x_sequenceE bindE_assoc)
apply (simp add:ARMSuperSectionBits_def word_0_sle_from_less
ARMSectionBits_def)
@ -1091,14 +1092,12 @@ lemma createSafeMappingEntries_PDE_ccorres:
apply (clarsimp simp:ARMSuperSectionBits_def
ARMSectionBits_def word_0_sle_from_less)
apply (rule conjI)
apply (clarsimp simp: cpde_relation_def vm_page_size_defs
of_bool_from_bool from_bool_def Let_def
pde_bits_from_cacheable_simps)
apply (simp add: cpde_relation_def true_def false_def)
apply (simp add: split: split_if)
done
lemma pte_case_isLargePagePTE:
"(case pte of LargePagePTE _ _ _ _ \<Rightarrow> P | _ \<Rightarrow> Q)
"(case pte of LargePagePTE _ _ _ _ _ \<Rightarrow> P | _ \<Rightarrow> Q)
= (if isLargePagePTE pte then P else Q)"
by (simp add: isLargePagePTE_def split: Hardware_H.pte.split)
@ -1143,6 +1142,12 @@ lemma lookupPTSlot_le_0x3C:
apply (simp add: word_bits_def)
done
lemma pte_get_tag_exhaust:
"pte_get_tag pte = 0 \<or> pte_get_tag pte = 1"
apply (simp add: pte_get_tag_def)
apply word_bitwise
done
lemma createSafeMappingEntries_PTE_ccorres:
"ccorres (syscall_error_rel \<currency> (\<lambda>rv rv'. isLeft rv \<and> cpte_relation (fst (theLeft rv)) (fst rv')
\<and> pte_range_relation (snd (theLeft rv)) (snd rv')))
@ -1172,6 +1177,7 @@ lemma createSafeMappingEntries_PTE_ccorres:
apply csymbr
apply csymbr
apply csymbr
apply csymbr
apply (rule ccorres_symb_exec_r)
apply (simp only: lookupError_injection)
apply (ctac add: ccorres_injection_handler_csum1
@ -1189,7 +1195,8 @@ lemma createSafeMappingEntries_PTE_ccorres:
apply (drule obj_at_ko_at', clarsimp)
apply (erule cmap_relationE1[OF rf_sr_cpte_relation], erule ko_at_projectKO_opt)
apply (clarsimp simp: typ_heap_simps cpte_relation_def Let_def)
apply (simp add: isLargePagePTE_def pte_lift_def Let_def pte_tag_defs
apply (simp add: isLargePagePTE_def pte_pte_large_lift_def pte_lift_def Let_def
pte_tag_defs pte_pte_invalid_def
split: Hardware_H.pte.split_asm split_if_asm)
apply ceqv
apply (simp add: pte_case_isLargePagePTE if_to_top_of_bindE del: Collect_const)
@ -1233,6 +1240,7 @@ lemma createSafeMappingEntries_PTE_ccorres:
apply csymbr
apply csymbr
apply csymbr
apply csymbr
apply (rule ccorres_symb_exec_r)
apply (ctac add: ccorres_injection_handler_csum1
@ -1263,7 +1271,7 @@ lemma createSafeMappingEntries_PTE_ccorres:
apply (drule obj_at_ko_at', clarsimp)
apply (erule cmap_relationE1[OF rf_sr_cpte_relation],
erule ko_at_projectKO_opt)
apply (auto simp: typ_heap_simps cpte_relation_def
apply (auto simp: typ_heap_simps cpte_relation_def pte_pte_invalid_def
Let_def pte_lift_def pte_tag_defs
intro: typ_heap_simps split: split_if_asm)[1]
apply (wp getObject_inv loadObject_default_inv | simp)+
@ -1272,7 +1280,9 @@ lemma createSafeMappingEntries_PTE_ccorres:
apply (simp add: upto_enum_step_def upto_enum_word
split: split_if)
apply (rule conseqPre, vcg)
apply clarsimp
apply (clarsimp simp: pte_tag_defs)
using pte_get_tag_exhaust
apply blast
apply wp
apply (simp add: upto_enum_step_def upto_enum_word
word_bits_def
@ -1290,7 +1300,9 @@ lemma createSafeMappingEntries_PTE_ccorres:
in HoarePartial.reannotateWhileNoGuard)
apply (rule HoarePartial.While[OF order_refl])
apply (rule conseqPre, vcg)
apply clarsimp
apply (clarsimp simp: pte_tag_defs)
using pte_get_tag_exhaust
apply blast
apply clarsimp
apply vcg
apply simp
@ -1318,8 +1330,8 @@ lemma createSafeMappingEntries_PTE_ccorres:
from_bool_mask_simp[unfolded mask_def, simplified])
apply (clarsimp simp: typ_heap_simps pte_range_relation_def
ptr_range_to_list_def upto_enum_word)
apply (simp add: cpte_relation_def Let_def pde_bits_from_cacheable_simps
of_bool_from_bool from_bool_def)
apply (simp add: cpte_relation_def true_def false_def pte_tag_defs)
using pte_get_tag_exhaust
apply auto[1]
done
@ -1360,8 +1372,6 @@ lemma word_add_format:
"(-1::32 word) + b + c = b + (c - 1)"
by simp
thm pteCheckIfMapped_body_def
lemma pteCheckIfMapped_ccorres:
"ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_' \<top>
(UNIV \<inter> {s. pte___ptr_to_struct_pte_C_' s = Ptr slot}) []
@ -1375,8 +1385,10 @@ lemma pteCheckIfMapped_ccorres:
apply clarsimp
apply (rule conseqPre, vcg)
apply (clarsimp simp: typ_heap_simps' return_def)
apply (case_tac rv, simp_all add: to_bool_def cpte_relation_invalid isInvalidPTE_def
split: split_if)
apply (case_tac rv, simp_all add: to_bool_def isInvalidPTE_def pte_tag_defs pte_pte_invalid_def
cpte_relation_def pte_pte_large_lift_def pte_get_tag_def
pte_lift_def Let_def
split: split_if_asm)
done
lemma cpde_relation_invalid:
@ -2198,8 +2210,8 @@ lemma is_aligned_no_overflow3:
lemma pte_get_tag_alt:
"pte_lift v = Some pteC
\<Longrightarrow> pte_get_tag v = (case pteC of Pte_pte_invalid \<Rightarrow> scast pte_pte_invalid
| Pte_pte_small _ \<Rightarrow> scast pte_pte_small
\<Longrightarrow> pte_get_tag v = (case pteC of
Pte_pte_small _ \<Rightarrow> scast pte_pte_small
| Pte_pte_large _ \<Rightarrow> scast pte_pte_large)"
by (auto simp add: pte_lift_def Let_def split: split_if_asm)
@ -2255,22 +2267,22 @@ lemma resolveVAddr_ccorres:
apply (vcg, clarsimp)
apply ceqv
apply (rule ccorres_pre_getObject_pte)
apply csymbr+
apply (rule ccorres_abstract_cleanup)
apply (rule_tac P'="{s. \<exists>v. cslift s (pte_Ptr (lookup_pt_slot_no_fail (ptrFromPAddr word1)
vaddr)) = Some v
\<and> cpte_relation rva v
\<and> ret__unsigned_long = pte_get_tag v}"
\<and> cpte_relation rva v}"
in ccorres_from_vcg_might_throw[where P=\<top>])
apply (rule allI, rule conseqPre, vcg)
apply clarsimp
using pte_get_tag_exhaust
apply (fastforce simp: pte_get_tag_alt pte_tag_defs cpte_relation_def
fst_return typ_heap_simps framesize_from_H_simps
pte_pte_large_lift_def pte_pte_small_lift_def
pte_pte_invalid_def
intro: resolve_ret_rel_Some
split: pte.splits)
apply (rule guard_is_UNIVI)
apply (clarsimp simp: typ_heap_simps)
apply fastforce
apply fastforce
apply (drule_tac A="{s. isPageTablePDE rv \<longrightarrow> s \<Turnstile>\<^sub>c pde_Ptr (lookup_pd_slot pd vaddr)
\<and> pde_get_tag (the (cslift s (pde_Ptr (lookup_pd_slot pd vaddr)))) = scast pde_pde_coarse

1
proof/crefine/Refine_C.thy
View File

@ -23,7 +23,6 @@ crunch ksQ[wp]: handleVMFault "\<lambda>s. P (ksReadyQueues s)"
context kernel_m
begin
(* Levity: added (20090419 09:44:42) *)
declare liftE_handle [simp]
lemma schedule_sch_act_wf:

108
proof/crefine/StateRelation_C.thy
View File

@ -44,66 +44,6 @@ definition
(addr_fun ` (dom as) = dom cs) \<and>
(\<forall>x \<in> dom as. rel (the (as x)) (the (cs (addr_fun x))))"
(*
C globals. Those marked with a ! are in the heap
- handled in the error return
current_syscall_error :: syscall_error_C
current_lookup_fault :: lookup_fault_C
current_fault :: fault_C
- handled in the state relation
ksSchedulerAction :: tcb_C ptr
intStateIRQNode :: cte_C ptr
ksCurThread :: tcb_C ptr
ksIdleThread :: tcb_C ptr
ksReadyQueues :: tcb_queue_C[256]
ksWorkUnitsCompleted :: word32
intStateIRQTable :: word32[64]
- kernel init (not looked at yet)
initFreeL2Slots :: slot_list_C ptr
initFreeL1Slots :: word32[8]
initFreeMemory :: free_list_C ptr
initBootMemory :: free_list_C ptr
initRegions :: boot_region_C[255]
initHeapPtr :: unit ptr
initL1Node :: cte_C ptr
initHeap :: word8[ty8192]
armKSGlobalPTsOffset :: word32 ??
kernel_device_array :: kernel_device_C[3]
memory_regions :: region_list_C
kernel_devices :: kernel_devices_C
device_regions :: device_list_C
n_initRegions :: word32
main_memory :: region_C
devices :: device_C[42]
epit1 :: epit_map_C ptr
avic :: avic_map_C ptr
- Unhandled
-- Generic
+ Danger Will Robinson! This looks nasty.
current_message :: inline_message_C
-- Arch
armKSGlobalsFrame :: word32[1024]
armKSGlobalPD :: pde_C[4096]
armKSGlobalPTs :: pte_C[1024]
-- Unknown
+ Seems to be a typo
platform_interrupt_t :: word32
+ These seem to be read-only
exceptionMessage :: word32[3]
syscallMessage :: word32[12]
frameRegisters :: word32[11]
msgRegisters :: word32[6]
gpRegisters :: word32[6]
*)
definition
asid_map_pd_to_hwasids :: "(asid \<rightharpoonup> hw_asid \<times> obj_ref) \<Rightarrow> (obj_ref \<Rightarrow> hw_asid set)"
@ -438,7 +378,7 @@ where
\<lparr> pde_pde_coarse_CL.address_CL = frame,
P_CL = of_bool parity,
Domain_CL = domain \<rparr>)
| SectionPDE frame parity domain cacheable global rights \<Rightarrow>
| SectionPDE frame parity domain cacheable global xn rights \<Rightarrow>
cpde' = Some (Pde_pde_section
\<lparr> pde_pde_section_CL.address_CL = frame,
size_CL = 0,
@ -449,11 +389,11 @@ where
AP_CL = ap_from_vm_rights rights,
P_CL = of_bool parity,
Domain_CL = domain,
XN_CL = 0,
XN_CL = of_bool xn,
C_CL = 0,
B_CL = b_from_cacheable cacheable
\<rparr>)
| SuperSectionPDE frame parity cacheable global rights \<Rightarrow>
| SuperSectionPDE frame parity cacheable global xn rights \<Rightarrow>
cpde' = Some (Pde_pde_section
\<lparr> pde_pde_section_CL.address_CL = frame,
size_CL = 1,
@ -464,7 +404,7 @@ where
AP_CL = ap_from_vm_rights rights,
P_CL = of_bool parity,
Domain_CL = 0,
XN_CL = 0,
XN_CL = of_bool xn,
C_CL = 0,
B_CL = b_from_cacheable cacheable
\<rparr>))"
@ -476,20 +416,32 @@ where
(let cpte' = pte_lift cpte in
case pte of
InvalidPTE \<Rightarrow>
cpte' = Some (Pte_pte_invalid)
| LargePagePTE frame cacheable global rights \<Rightarrow>
cpte' = Some (Pte_pte_large
\<lparr> pte_pte_large_CL.address_CL = 0,
XN_CL = 0,
TEX_CL = 0,
nG_CL = 0,
S_CL = 0,
APX_CL = 0,
AP_CL = 0,
C_CL = 0,
B_CL = 0,
reserved_CL = 0
\<rparr>)
| LargePagePTE frame cacheable global xn rights \<Rightarrow>
cpte' = Some (Pte_pte_large
\<lparr> pte_pte_large_CL.address_CL = frame,
XN_CL = 0,
XN_CL = of_bool xn,
TEX_CL = tex_from_cacheable cacheable,
nG_CL = of_bool (~global),
S_CL = s_from_cacheable cacheable,
APX_CL = 0,
AP_CL = ap_from_vm_rights rights,
C_CL = 0,
B_CL = b_from_cacheable cacheable
B_CL = b_from_cacheable cacheable,
reserved_CL = 1
\<rparr>)
| SmallPagePTE frame cacheable global rights \<Rightarrow>
| SmallPagePTE frame cacheable global xn rights \<Rightarrow>
cpte' = Some (Pte_pte_small
\<lparr> address_CL = frame,
nG_CL = of_bool (~global),
@ -498,9 +450,25 @@ where
TEX_CL = tex_from_cacheable cacheable,
AP_CL = ap_from_vm_rights rights,
C_CL = 0,
B_CL = b_from_cacheable cacheable
B_CL = b_from_cacheable cacheable,
XN_CL = of_bool xn
\<rparr>))"
(* Invalid PTEs map to large PTEs with reserved bit 0 *)
lemma pte_0:
"index (pte_C.words_C cpte) 0 = 0 \<Longrightarrow> pte_lift cpte = Some (Pte_pte_large
\<lparr> pte_pte_large_CL.address_CL = 0,
XN_CL = 0,
TEX_CL = 0,
nG_CL = 0,
S_CL = 0,
APX_CL = 0,
AP_CL = 0,
C_CL = 0,
B_CL = 0,
reserved_CL = 0
\<rparr>)"
by (simp add: pte_lift_def pte_get_tag_def pte_pte_large_def)
definition
casid_pool_relation :: "asidpool \<Rightarrow> asid_pool_C \<Rightarrow> bool"

128
proof/crefine/VSpace_C.thy
View File

@ -35,6 +35,7 @@ lemma empty_fail_findPDForASIDAssert[iff]:
apply (intro empty_fail_bind, simp_all split: sum.split)
done
(* FIXME: move *)
lemma mask_AND_less_0:
"\<lbrakk>x && mask n = 0; m \<le> n\<rbrakk> \<Longrightarrow> x && mask m = 0"
apply (case_tac "len_of TYPE('a) \<le> n")
@ -937,6 +938,7 @@ lemma ccorres_pre_getObject_asidpool:
apply simp
done
(* FIXME: move *)
lemma ccorres_from_vcg_throws_nofail:
"\<forall>\<sigma>. \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> srel} c {},
{s. \<not>snd (a \<sigma>) \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> srel \<and> arrel rv (axf s))} \<Longrightarrow>
@ -2091,53 +2093,6 @@ lemma ccorres_pre_getObject_pte:
apply simp
done
(*
lemma checkMappingPPtr_ccorres:
"ccorres (K dc \<currency> dc) (liftxf errstate (from_bool \<circ> Not \<circ> to_bool) (K ()) ret__int_')
no_0_obj'
(UNIV \<inter> {s. pteptr_' s = (case tabPtr of Inl ptr' \<Rightarrow> Ptr ptr' | _ \<Rightarrow> NULL)}
\<inter> {s. pdeptr_' s = (case tabPtr of Inr ptr' \<Rightarrow> Ptr ptr' | _ \<Rightarrow> NULL)}
\<inter> {s. pptr_' s = Ptr ptr}) []
(checkMappingPPtr ptr tabPtr) (Call checkMappingPPtr_'proc)"
apply (cinit lift: pteptr_' pdeptr_' pptr_')
apply csymbr
apply wpc
apply (simp add: liftE_bindE del: Collect_const)
apply (rule ccorres_pre_getObject_pte)
apply (rule_tac P="tabPtr \<noteq> Inl 0" in ccorres_gen_asm)
apply simp
apply (rule_tac P="\<top>"
and P'="{s. \<exists>rv'. cslift s (Ptr (theLeft tabPtr)) = Some rv'
\<and> cpte_relation rv rv'}"
in ccorres_from_vcg_split_throws)
apply vcg
apply (rule conseqPre, vcg)
apply (clarsimp simp: typ_heap_simps')
apply (auto simp: cpte_relation_def Let_def pte_lift_def pte_tag_defs
throwError_def return_def from_bool_def exception_defs
unlessE_def returnOk_def pte_pte_large_lift_def
pte_pte_small_lift_def
split: Hardware_H.pte.split_asm split_if_asm split_if)[1]
apply (simp add: liftE_bindE Collect_False del: Collect_const)
apply (rule ccorres_pre_getObject_pde)
apply (rule_tac P="tabPtr \<noteq> Inr 0" in ccorres_gen_asm)
apply simp
apply (rule_tac P="\<top>"
and P'="{s. \<exists>rv'. cslift s (Ptr (theRight tabPtr)) = Some rv'
\<and> cpde_relation rv rv'}"
in ccorres_from_vcg_split_throws)
apply vcg
apply (rule conseqPre, vcg)
apply (clarsimp simp: typ_heap_simps')
apply (simp add: cpde_relation_def Let_def pde_lift_def pde_tag_defs
throwError_def return_def from_bool_def exception_defs
unlessE_def returnOk_def pde_pde_section_lift_def
split: Hardware_H.pde.split_asm split_if_asm split_if)[1]
apply (clarsimp simp: Collect_const_mem typ_heap_simps')
apply auto
done
*)
lemmas unfold_checkMapping_return
= from_bool_0[where 'a=32, folded exception_defs]
to_bool_def
@ -2239,7 +2194,26 @@ lemma is_aligned_cache_preconds:
apply (drule_tac x=6 and y=5 in is_aligned_weaken, simp)+
apply (simp add: is_aligned_mask)
done
lemma pte_pte_invalid_new_spec:
"\<forall>s. \<Gamma> \<turnstile> {s}
\<acute>ret__struct_pte_C :== PROC pte_pte_invalid_new()
\<lbrace> pte_lift \<acute>ret__struct_pte_C = Some (Pte_pte_large
\<lparr> pte_pte_large_CL.address_CL = 0,
XN_CL = 0,
TEX_CL = 0,
nG_CL = 0,
S_CL = 0,
APX_CL = 0,
AP_CL = 0,
C_CL = 0,
B_CL = 0,
reserved_CL = 0
\<rparr>)\<rbrace>"
apply vcg
apply (clarsimp simp: pte_lift_def pte_get_tag_def pte_pte_large_def fupdate_def)
done
lemma unmapPage_ccorres:
"ccorres dc xfdc (invs' and (\<lambda>_. asid \<le> mask asid_bits \<and> vmsz_aligned' vptr sz
\<and> vptr < kernelBase))
@ -2271,7 +2245,7 @@ lemma unmapPage_ccorres:
apply (clarsimp simp: typ_heap_simps')
apply (simp add: cpte_relation_def Let_def pte_lift_def
isSmallPagePTE_def pte_tag_defs
pte_pte_small_lift_def
pte_pte_small_lift_def pte_pte_invalid_def
split: split_if_asm pte.split_asm)
apply (rule ceqv_refl)
apply (simp add: unfold_checkMapping_return liftE_liftM
@ -2281,8 +2255,7 @@ lemma unmapPage_ccorres:
apply csymbr
apply (rule ccorres_split_nothrow_novcg_dc)
apply (rule storePTE_Basic_ccorres)
apply (simp add: cpte_relation_def Let_def
pte_lift_pte_invalid)
apply (simp add: cpte_relation_def Let_def)
apply csymbr
apply simp
apply (ctac add: cleanByVA_PoU_ccorres[unfolded dc_def])
@ -2313,7 +2286,7 @@ lemma unmapPage_ccorres:
apply (clarsimp simp: typ_heap_simps')
apply (simp add: cpte_relation_def Let_def pte_lift_def
isLargePagePTE_def pte_tag_defs
pte_pte_large_lift_def
pte_pte_large_lift_def pte_pte_invalid_def
split: split_if_asm pte.split_asm)
apply (rule ceqv_refl)
apply (simp add: liftE_liftM dc_def[symmetric]
@ -2321,7 +2294,6 @@ lemma unmapPage_ccorres:
Collect_False unfold_checkMapping_return word_sle_def
del: Collect_const)
apply (ccorres_remove_UNIV_guard)
apply (rule ccorres_rhs_assoc2)
apply (rule ccorres_split_nothrow_novcg)
apply (rule_tac F="\<top>\<top>" in ccorres_mapM_x_while)
@ -2329,8 +2301,7 @@ lemma unmapPage_ccorres:
apply (rule ccorres_guard_imp2)
apply csymbr
apply (rule storePTE_Basic_ccorres)
apply (simp add: cpte_relation_def Let_def
pte_lift_pte_invalid)
apply (simp add: cpte_relation_def Let_def)
apply clarsimp
apply (simp add: upto_enum_step_def
upto_enum_word
@ -2861,7 +2832,8 @@ lemma makeUserPDE_spec:
"\<forall>s. \<Gamma> \<turnstile>
\<lbrace>s. (\<acute>page_size = scast Kernel_C.ARMSection \<or> \<acute>page_size = scast Kernel_C.ARMSuperSection) \<and>
\<acute>vm_rights < 4 \<and> vmsz_aligned' (\<acute>paddr) (gen_framesize_to_H \<acute>page_size) \<and>
\<acute>parity && 1 = \<acute>parity \<and> \<acute>domain && 0xF = \<acute>domain \<and> \<acute>cacheable && 1 = \<acute>cacheable\<rbrace>
\<acute>parity && 1 = \<acute>parity \<and> \<acute>domain && 0xF = \<acute>domain \<and> \<acute>cacheable && 1 = \<acute>cacheable \<and>
\<acute>nonexecutable && 1 = \<acute>nonexecutable\<rbrace>
Call makeUserPDE_'proc
\<lbrace> pde_lift \<acute>ret__struct_pde_C = Some (Pde_pde_section \<lparr>
pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr,
@ -2873,7 +2845,7 @@ lemma makeUserPDE_spec:
AP_CL = ap_from_vm_rights (vmrights_to_H \<^bsup>s\<^esup>vm_rights),
P_CL = \<^bsup>s\<^esup>parity,
Domain_CL = \<^bsup>s\<^esup>domain,
XN_CL = 0,
XN_CL = \<^bsup>s\<^esup>nonexecutable,
C_CL = 0,
B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable
\<rparr>) \<rbrace>"
@ -2922,7 +2894,7 @@ lemma makeUserPTE_spec:
"\<forall>s. \<Gamma> \<turnstile>
\<lbrace>s. (\<acute>page_size = scast Kernel_C.ARMSmallPage \<or> \<acute>page_size = scast Kernel_C.ARMLargePage) \<and>
\<acute>vm_rights < 4 \<and> vmsz_aligned' \<acute>paddr (gen_framesize_to_H \<acute>page_size) \<and>
\<acute>cacheable && 1 = \<acute>cacheable\<rbrace>
\<acute>cacheable && 1 = \<acute>cacheable \<and> \<acute>nonexecutable && 1 = \<acute>nonexecutable\<rbrace>
Call makeUserPTE_'proc
\<lbrace> pte_lift \<acute>ret__struct_pte_C = Some (if \<^bsup>s\<^esup>page_size = scast Kernel_C.ARMSmallPage
then Pte_pte_small
@ -2933,18 +2905,20 @@ lemma makeUserPTE_spec:
TEX_CL = tex_bits_from_cacheable \<^bsup>s\<^esup>cacheable,
AP_CL = ap_from_vm_rights (vmrights_to_H \<^bsup>s\<^esup>vm_rights),
C_CL = 0,
B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable
B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable,
XN_CL = \<^bsup>s\<^esup>nonexecutable
\<rparr>
else Pte_pte_large
\<lparr> pte_pte_large_CL.address_CL = \<^bsup>s\<^esup>paddr,
XN_CL = 0,
XN_CL = \<^bsup>s\<^esup>nonexecutable,
TEX_CL = tex_bits_from_cacheable \<^bsup>s\<^esup>cacheable,
nG_CL = 1,
S_CL = shared_bit_from_cacheable \<^bsup>s\<^esup>cacheable,
APX_CL = 0,
AP_CL = ap_from_vm_rights (vmrights_to_H \<^bsup>s\<^esup>vm_rights),
C_CL = 0,
B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable
B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable,
reserved_CL = 1
\<rparr>)\<rbrace>"
apply vcg
apply (clarsimp simp:vmsz_aligned'_def)
@ -2968,11 +2942,14 @@ lemma makeUserPTE_spec:
iwb_from_cacheable_def dest!:mask_eq1_nochoice is_aligned_neg_mask_eq)+)[2]
done
term vm_attributes_lift
lemma vmAttributesFromWord_spec:
"\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. True\<rbrace> Call vmAttributesFromWord_'proc
\<lbrace> vm_attributes_lift \<acute>ret__struct_vm_attributes_C =
\<lparr> armParityEnabled_CL = (\<^bsup>s\<^esup>w >> 1) && 1,
armPageCacheable_CL = \<^bsup>s\<^esup>w && 1 \<rparr> \<rbrace>"
\<lparr> armExecuteNever_CL = (\<^bsup>s\<^esup>w >> 2) && 1,
armParityEnabled_CL = (\<^bsup>s\<^esup>w >> 1) && 1,
armPageCacheable_CL = \<^bsup>s\<^esup>w && 1 \<rparr> \<rbrace>"
by (vcg, simp add: vm_attributes_lift_def word_sless_def word_sle_def)
lemma cap_to_H_PDCap_tag:
@ -3208,29 +3185,6 @@ lemma pte_case_isInvalidPTE:
by (cases pte, simp_all add: isInvalidPTE_def)
lemma cpte_relation_invalid:
"cpte_relation pte pte' \<Longrightarrow>
(pte_get_tag pte' = scast pte_pte_invalid) = isInvalidPTE pte"
apply (simp add: cpte_relation_def Let_def isInvalidPTE_def)
apply (case_tac pte)
apply (simp add: Let_def isInvalidPTE_def)
apply (case_tac "pte_get_tag pte'=scast pte_pte_invalid", simp add: pte_lift_def)
apply (case_tac "pte_get_tag pte'=scast pte_pte_large", simp add: pte_lift_def)
apply (case_tac "pte_get_tag pte'=scast pte_pte_small", simp add: pte_lift_def)
apply (simp add: pte_lift_def)
apply (simp add: cpte_relation_def Let_def isInvalidPTE_def)
apply (case_tac "pte_get_tag pte'=scast pte_pte_invalid", simp add: pte_lift_def)
apply (case_tac "pte_get_tag pte'=scast pte_pte_large", simp add: pte_lift_def)
apply (case_tac "pte_get_tag pte'=scast pte_pte_small", simp add: pte_lift_def)
apply (simp add: pte_lift_def)
apply (simp add: cpte_relation_def Let_def isInvalidPTE_def)
apply (case_tac "pte_get_tag pte'=scast pte_pte_invalid", simp add: pte_lift_def)
apply (case_tac "pte_get_tag pte'=scast pte_pte_large", simp add: pte_lift_def)
apply (case_tac "pte_get_tag pte'=scast pte_pte_small", simp add: pte_lift_def)
apply (simp add: pte_lift_def)
done
lemma flushTable_ccorres:
"ccorres dc xfdc (invs' and cur_tcb' and (\<lambda>_. asid \<le> mask asid_bits))
(UNIV \<inter> {s. pd_' s = pde_Ptr pd} \<inter> {s. asid_' s = asid}
@ -3250,8 +3204,6 @@ lemma flushTable_ccorres:
apply (clarsimp simp: pde_stored_asid_def to_bool_def split: split_if)
apply (rule ccorres_Guard_Seq ccorres_rhs_assoc)+
(* why csymbr does not work here? ... *)
(* Now we can csymbr *)
apply csymbr
apply (simp add: word_sle_def mapM_discarded whileAnno_def Collect_False
del: Collect_const)