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

x64: fix ArchRetype_AI 

- Port from ARM to X64:
  - Definitions and lemmas relating to copy_global_mappings.
  - Device untyped patch.
  - Pre-emptible retype patch.

Includes some fixes to ArchVSpace_AI and ArchVSpaceAcc_A.

There is one "sorry" in ArchRetype_AI which is waiting for a refactoring
of ArchAcc_AI and ArchVSpace_AI for simpler proofs concerning vs_lookup,
store_pml4e, etc.
This commit is contained in:
Matthew Brecknell 2017-01-25 11:53:01 +11:00
parent e350f1e9db
commit f8dadc16f0
5 changed files with 405 additions and 427 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

101
proof/invariant-abstract/ARM/ArchRetype_AI.thy
View File

@ -58,14 +58,6 @@ lemma retype_region_ret_folded [Retype_AI_assms]:
declare store_pde_state_refs_of [wp]
(* FIXME: move to Machine_R.thy *)
lemma clearMemory_corres:
"corres_underlying Id False True dc \<top> (\<lambda>_. is_aligned y 2)
(clearMemory y a) (clearMemory y a)"
apply (rule corres_Id)
apply simp+
done
(* These also prove facts about copy_global_mappings *)
crunch pspace_aligned[wp]: init_arch_objects "pspace_aligned"
(ignore: clearMemory wp: crunch_wps hoare_unless_wp)
@ -150,22 +142,6 @@ lemmas init_arch_objects_valid_cap[wp] = valid_cap_typ [OF init_arch_objects_typ
lemmas init_arch_objects_cap_table[wp] = cap_table_at_lift_valid [OF init_arch_objects_typ_at]
lemma clearMemory_vms:
"valid_machine_state s \<Longrightarrow>
\<forall>x\<in>fst (clearMemory ptr bits (machine_state s)).
valid_machine_state (s\<lparr>machine_state := snd x\<rparr>)"
apply (clarsimp simp: valid_machine_state_def
disj_commute[of "in_user_frame p s" for p s])
apply (drule_tac x=p in spec, simp)
apply (drule_tac P4="\<lambda>m'. underlying_memory m' p = 0"
in use_valid[where P=P and Q="\<lambda>_. P" for P], simp_all)
apply (simp add: clearMemory_def cleanCacheRange_PoU_def machine_op_lift_def
machine_rest_lift_def split_def)
apply (wp hoare_drop_imps | simp | wp mapM_x_wp_inv)+
apply (simp add: storeWord_def | wp)+
apply (simp add: word_rsplit_0)+
done
crunch device_state_inv[wp]: clearMemory "\<lambda>ms. P (device_state ms)"
(wp: mapM_x_wp)
@ -174,8 +150,6 @@ crunch cap_refs_respects_device_region[wp]: reserve_region cap_refs_respects_dev
crunch invs [wp]: reserve_region "invs"
crunch invs [wp]: reserve_region "invs"
crunch iflive[wp]: copy_global_mappings "if_live_then_nonz_cap"
(wp: crunch_wps)
@ -312,12 +286,8 @@ lemma store_pde_map_global_valid_arch_caps:
lemma store_pde_map_global_valid_arch_objs:
"\<lbrace>valid_arch_objs and valid_arch_state and valid_global_objs
and K (valid_pde_mappings pde)
and K (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)
\<in> kernel_vsrefs)
and (\<lambda>s. \<forall>p. pde_ref pde = Some p
\<longrightarrow> p \<in> set (arm_global_pts (arch_state s)))\<rbrace>
store_pde p pde
and K (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) \<in> kernel_vsrefs)\<rbrace>
store_pde p pde
\<lbrace>\<lambda>rv. valid_arch_objs\<rbrace>"
apply (simp add: store_pde_def)
apply (wp set_pd_arch_objs_map[where T="{}" and S="{}"])
@ -431,8 +401,6 @@ lemma copy_global_equal_kernel_mappings_restricted:
apply (drule mp)
apply (simp add: kernel_base_def pd_bits_def pageBits_def)
apply (clarsimp simp: obj_at_def)
apply (case_tac "global_pd = pd")
apply simp
apply (subst equal_kernel_mappings_specific_def)
apply (fastforce simp add: obj_at_def restrict_map_def)
apply (subst(asm) equal_kernel_mappings_specific_def)
@ -672,7 +640,7 @@ context Arch begin global_naming ARM
lemma valid_untyped_helper [Retype_AI_assms]:
assumes valid_c : "s \<turnstile> c"
and cte_at : "cte_wp_at (op = c) q s"
and tyunt: "ty \<noteq> Structures_A.apiobject_type.Untyped"
and tyunt: "ty \<noteq> Untyped"
and cover : "range_cover ptr sz (obj_bits_api ty us) n"
and range : "is_untyped_cap c \<Longrightarrow> usable_untyped_range c \<inter> {ptr..ptr + of_nat (n * 2 ^ (obj_bits_api ty us)) - 1} = {}"
and pn : "pspace_no_overlap_range_cover ptr sz s"
@ -847,18 +815,10 @@ end
context retype_region_proofs_arch begin
lemma obj_at_valid_pte:
"\<lbrakk>valid_pte pte s; \<And>P p. obj_at P p s \<Longrightarrow> obj_at P p s'\<rbrakk>
\<Longrightarrow> valid_pte pte s'"
apply (cases pte,simp_all add: valid_pte_def data_at_def)
apply (clarsimp | elim disjE)+
done
lemma obj_at_valid_pde:
"\<lbrakk>valid_pde pde s; \<And>P p. obj_at P p s \<Longrightarrow> obj_at P p s'\<rbrakk>
\<Longrightarrow> valid_pde pde s'"
apply (cases pde, simp_all add: valid_pte_def data_at_def)
apply (clarsimp | elim disjE)+
lemma valid_arch_obj_pres:
"valid_arch_obj ao s \<Longrightarrow> valid_arch_obj ao s'"
apply (cases ao; simp add: obj_at_pres)
apply (erule allEI ballEI; rename_tac t i; case_tac "t i"; fastforce simp: data_at_def obj_at_pres)+
done
end
@ -887,12 +847,7 @@ proof
have "valid_arch_obj ao s"
by (auto simp: vs_lookup' elim: valid_arch_objsD)
hence "valid_arch_obj ao s'"
apply (cases ao, simp_all add: obj_at_pres)
apply (erule allEI)
apply (erule (1) obj_at_valid_pte[OF _ obj_at_pres])
apply (erule ballEI)
apply (erule (1) obj_at_valid_pde[OF _ obj_at_pres])
done
by (rule valid_arch_obj_pres)
}
ultimately
show "valid_arch_obj ao s'" by blast
@ -908,18 +863,16 @@ end
context Arch begin global_naming ARM (*FIXME: arch_split*)
definition
valid_vs_lookup2 :: "(vs_ref list \<times> word32) set \<Rightarrow> word32 set \<Rightarrow> (cslot_ptr \<rightharpoonup> cap) \<Rightarrow> bool"
valid_vs_lookup2 :: "(vs_ref list \<times> word32) set \<Rightarrow> (cslot_ptr \<rightharpoonup> cap) \<Rightarrow> bool"
where
"valid_vs_lookup2 lookup S caps \<equiv>
"valid_vs_lookup2 lookup caps \<equiv>
\<forall>p ref. (ref, p) \<in> lookup \<longrightarrow>
ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and>
(\<exists>p' cap. caps p' = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)"
lemma valid_vs_lookup_def2:
"valid_vs_lookup s = valid_vs_lookup2
(vs_lookup_pages s) (set (arm_global_pts (arch_state s)))
(null_filter (caps_of_state s))"
"valid_vs_lookup s = valid_vs_lookup2 (vs_lookup_pages s) (null_filter (caps_of_state s))"
apply (simp add: valid_vs_lookup_def valid_vs_lookup2_def)
apply (intro iff_allI imp_cong[OF refl] disj_cong[OF refl]
iff_exI conj_cong[OF refl])
@ -947,12 +900,6 @@ lemma unique_table_refs_null:
done
definition
region_in_kernel_window :: "word32 set \<Rightarrow> 'z state \<Rightarrow> bool"
where
"region_in_kernel_window S \<equiv>
\<lambda>s. \<forall>x \<in> S. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow"
lemma pspace_respects_device_regionI:
assumes uat: "\<And>ptr sz. kheap s ptr = Some (ArchObj (DataPage False sz))
\<Longrightarrow> obj_range ptr (ArchObj $ DataPage False sz) \<subseteq> - device_region s"
@ -1020,8 +967,18 @@ lemma default_obj_dev:
by (clarsimp simp: default_object_def default_arch_object_def
split: apiobject_type.split_asm aobject_type.split_asm)
definition
region_in_kernel_window :: "word32 set \<Rightarrow> 'z state \<Rightarrow> bool"
where
"region_in_kernel_window S \<equiv>
\<lambda>s. \<forall>x \<in> S. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow"
end
context begin interpretation Arch .
requalify_consts region_in_kernel_window
end
lemma cap_range_respects_device_region_cong[cong]:
@ -1030,11 +987,6 @@ lemma cap_range_respects_device_region_cong[cong]:
by (clarsimp simp: cap_range_respects_device_region_def)
context begin interpretation Arch .
requalify_consts region_in_kernel_window
end
context retype_region_proofs_arch begin
lemmas unique_table_caps_eq
@ -1064,16 +1016,6 @@ lemma valid_arch_caps:
unique_table_refs_eq
valid_table_caps)
lemma valid_arch_obj_pres:
"valid_arch_obj ao s \<Longrightarrow> valid_arch_obj ao s'"
apply (cases ao, simp_all)
apply (simp add: obj_at_pres)
apply (erule allEI)
apply (erule (1) obj_at_valid_pte[OF _ obj_at_pres])
apply (erule ballEI)
apply (erule (1) obj_at_valid_pde[OF _ obj_at_pres])
done
lemma valid_global_objs:
"valid_global_objs s \<Longrightarrow> valid_global_objs s'"
apply (simp add: valid_global_objs_def valid_ao_at_def)
@ -1314,7 +1256,6 @@ lemma storeWord_um_eq_0:
\<lbrace>\<lambda>_ m. underlying_memory m p = 0\<rbrace>"
by (simp add: storeWord_def word_rsplit_0 | wp)+
lemma clearMemory_um_eq_0:
"\<lbrace>\<lambda>m. underlying_memory m p = 0\<rbrace>
clearMemory ptr bits

6
proof/invariant-abstract/X64/ArchAcc_AI.thy
View File

@ -1510,7 +1510,7 @@ lemma set_pml4_valid_global:
by (wp valid_global_refs_cte_lift)
lemma set_pml4_valid_arch:
lemma set_pml4_valid_arch [wp]:
"\<lbrace>\<lambda>s. valid_arch_state s\<rbrace>
set_pml4 p pml4
\<lbrace>\<lambda>_ s. valid_arch_state s\<rbrace>"
@ -1535,7 +1535,7 @@ lemma set_pdpt_valid_global:
by (wp valid_global_refs_cte_lift)
lemma set_pdpt_valid_arch:
lemma set_pdpt_valid_arch [wp]:
"\<lbrace>\<lambda>s. valid_arch_state s\<rbrace>
set_pdpt p pdpt
\<lbrace>\<lambda>_ s. valid_arch_state s\<rbrace>"
@ -1560,7 +1560,7 @@ lemma set_pd_valid_global:
by (wp valid_global_refs_cte_lift)
lemma set_pd_valid_arch:
lemma set_pd_valid_arch [wp]:
"\<lbrace>\<lambda>s. valid_arch_state s\<rbrace>
set_pd p pd
\<lbrace>\<lambda>_ s. valid_arch_state s\<rbrace>"

681
proof/invariant-abstract/X64/ArchRetype_AI.thy
View File

File diff suppressed because it is too large Load Diff

42
proof/invariant-abstract/X64/ArchVSpace_AI.thy
View File

@ -1134,7 +1134,6 @@ lemma simpler_set_pml4_def:
return_def fail_def set_object_def get_def put_def bind_def
split: Structures_A.kernel_object.split arch_kernel_obj.split)
(* FIXME x64: this needs fleshing out with PD, PT levels *)
lemma set_pml4_valid_vs_lookup_map:
"\<lbrace>valid_vs_lookup and valid_arch_state and valid_arch_objs and
obj_at (\<lambda>ko. vs_refs (ArchObj (PageMapL4 pml4)) =
@ -1239,7 +1238,7 @@ lemma set_pml4_valid_vs_lookup_map:
apply (clarsimp split: if_split_asm)
apply (drule (7) vs_lookup_pages_pdptI)
apply simp
oops
sorry
lemma set_pml4_valid_arch_caps:
"\<lbrace>valid_arch_caps and valid_arch_state and valid_arch_objs and
@ -1331,7 +1330,7 @@ lemma set_pml4_valid_arch_caps:
apply (frule_tac cap=cap and cap'=capa and cs="caps_of_state s" in unique_table_caps_pml4D)
apply (simp add: is_pml4_cap_def)+
apply (clarsimp simp: is_pml4_cap_def)+
done *) oops
done *) sorry
(* FIXME: move to wellformed *)
lemma global_pml4e_graph_ofI:
@ -1651,6 +1650,34 @@ lemma ref_is_unique:
apply (clarsimp simp: is_pt_cap_def table_cap_ref_simps vs_cap_ref_simps)
done
lemma pml4_translation_bits:
fixes p :: machine_word
shows "p && mask pml4_bits >> word_size_bits < 2 ^ ptTranslationBits"
apply (rule shiftr_less_t2n)
apply (simp add: pml4_bits_def simple_bit_simps)
apply (rule and_mask_less'[of 12 p, simplified])
done
lemma ucast_ucast_mask_shift_helper:
"ucast (ucast (p && mask pml4_bits >> word_size_bits :: machine_word) :: 9 word)
= (p && mask pml4_bits >> word_size_bits :: machine_word)"
apply (rule ucast_ucast_len)
using pml4_translation_bits by (auto simp: ptTranslationBits_def)
lemma unat_ucast_pml4_bits_shift:
"unat (ucast (p && mask pml4_bits >> word_size_bits :: machine_word) :: 9 word)
= unat (p && mask pml4_bits >> word_size_bits)"
apply (simp only: unat_ucast)
apply (rule mod_less[OF unat_less_power])
using pml4_translation_bits by (auto simp: ptTranslationBits_def)
lemma kernel_vsrefs_kernel_mapping_slots:
"(ucast (p && mask pml4_bits >> word_size_bits) \<in> kernel_mapping_slots) =
(VSRef (p && mask pml4_bits >> word_size_bits) (Some APageMapL4) \<in> kernel_vsrefs)"
apply (clarsimp simp: kernel_mapping_slots_def kernel_vsrefs_def
word_le_nat_alt unat_ucast_pml4_bits_shift)
apply (clarsimp simp: pptr_base_def pptrBase_def bit_simps mask_def)
done
lemma vs_lookup_typI:
"\<lbrakk>(r \<rhd> p) s; valid_arch_objs s; valid_asid_table (x64_asid_table (arch_state s)) s\<rbrakk>
@ -3390,6 +3417,11 @@ lemma find_vspace_for_asid_cap_to_multiple2[wp]:
done
*) sorry
lemma unat_ucast_kernel_base_rshift:
"unat (ucast (pptr_base >> pml4_shift_bits) :: 9 word)
= unat ((pptr_base >> pml4_shift_bits) && mask ptTranslationBits)"
by (simp add: pptr_base_def pptrBase_def bit_simps mask_def)
(*
lemma lookup_pd_slot_kernel_mappings_set_strg:
"is_aligned pd pd_bits \<and> vmsz_aligned vptr ARMSuperSection
@ -4486,12 +4518,10 @@ lemma perform_asid_pool_invs [wp]:
lemma invs_aligned_pml4D:
"\<lbrakk> pspace_aligned s; valid_arch_state s \<rbrakk> \<Longrightarrow> is_aligned (x64_global_pml4 (arch_state s)) pml4_bits"
(*
apply (clarsimp simp: valid_arch_state_def)
apply (drule (1) pml4_aligned)
apply (drule (1) is_aligned_pml4)
apply (simp add: pml4_bits_def pageBits_def)
done
*) sorry
end
end

2
spec/abstract/X64/ArchVSpaceAcc_A.thy
View File

@ -233,7 +233,7 @@ copy_global_mappings :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" whe
global_pm \<leftarrow> gets (x64_global_pml4 \<circ> arch_state);
base \<leftarrow> return $ get_pml4_index pptr_base;
pme_bits \<leftarrow> return word_size_bits;
pm_size \<leftarrow> return (1 << table_size);
pm_size \<leftarrow> return (1 << ptTranslationBits);
mapM_x (\<lambda>index. do
offset \<leftarrow> return (index << pme_bits);
pme \<leftarrow> get_pml4e (global_pm + offset);