From 42ff16ed4cb84a10b0557e3c96a2f956d99717dd Mon Sep 17 00:00:00 2001 From: Matthew Brecknell Date: Tue, 14 Mar 2017 19:26:23 +1100 Subject: [PATCH] x64: fix sorry proofs in ArchAInvsPre_AI The canonical_address constant (but not its definition) is now exported to generic theories, and used in do_user_op. On ARM, all virtual addresses are canonical. --- proof/invariant-abstract/ADT_AI.thy | 8 +- proof/invariant-abstract/AInvs.thy | 3 +- proof/invariant-abstract/AInvsPre.thy | 2 +- proof/invariant-abstract/ARM/ArchAInvsPre.thy | 2 +- .../ARM/ArchInvariants_AI.thy | 5 + proof/invariant-abstract/Invariants_AI.thy | 1 + proof/invariant-abstract/X64/ArchADT_AI.thy | 2 +- proof/invariant-abstract/X64/ArchAInvsPre.thy | 152 +++++++----------- .../X64/ArchInvariants_AI.thy | 34 ++++ .../invariant-abstract/X64/ArchVSpace_AI.thy | 1 - 10 files changed, 107 insertions(+), 103 deletions(-) diff --git a/proof/invariant-abstract/ADT_AI.thy b/proof/invariant-abstract/ADT_AI.thy index b96462217..4e6cc7086 100644 --- a/proof/invariant-abstract/ADT_AI.thy +++ b/proof/invariant-abstract/ADT_AI.thy @@ -220,10 +220,14 @@ definition ,(ds \ ptrFromPAddr) |` {pa. \va. conv va = Some pa \ AllowRead \ rights va} ) )); do_machine_op (user_memory_update - ((um' |` {pa. \va. conv va = Some pa \ AllowWrite \ rights va} + ((um' |` {pa. \va. canonical_address va + \ conv va = Some pa + \ AllowWrite \ rights va} \ addrFromPPtr) |` (- dom ds))); do_machine_op (device_memory_update - ((ds' |` {pa. \va. conv va = Some pa \ AllowWrite \ rights va} + ((ds' |` {pa. \va. canonical_address va + \ conv va = Some pa + \ AllowWrite \ rights va} \ addrFromPPtr) |` (dom ds))); return (e, tc') od" diff --git a/proof/invariant-abstract/AInvs.thy b/proof/invariant-abstract/AInvs.thy index d66cf0828..c59d11ea6 100644 --- a/proof/invariant-abstract/AInvs.thy +++ b/proof/invariant-abstract/AInvs.thy @@ -115,8 +115,7 @@ lemma do_user_op_invs: restrict_map_def invs_def cur_tcb_def split: option.splits if_split_asm) apply (frule ptable_rights_imp_frame) - apply fastforce - apply simp + apply fastforce+ apply (clarsimp simp: valid_state_def device_frame_in_device_region) done diff --git a/proof/invariant-abstract/AInvsPre.thy b/proof/invariant-abstract/AInvsPre.thy index 1fe7ec519..9b86cde6b 100644 --- a/proof/invariant-abstract/AInvsPre.thy +++ b/proof/invariant-abstract/AInvsPre.thy @@ -16,7 +16,7 @@ locale AInvsPre = fixes state_ext_type1 :: "('a :: state_ext) itself" assumes ptable_rights_imp_frame: "\ (s :: 'a state) t x y. - valid_state s \ + valid_state s \ canonical_address x \ ptable_rights t s x \ {} \ ptable_lift t s x = Some (addrFromPPtr y) \ in_user_frame y s \ in_device_frame y s" diff --git a/proof/invariant-abstract/ARM/ArchAInvsPre.thy b/proof/invariant-abstract/ARM/ArchAInvsPre.thy index d0275a8bc..f4ceaad3a 100644 --- a/proof/invariant-abstract/ARM/ArchAInvsPre.thy +++ b/proof/invariant-abstract/ARM/ArchAInvsPre.thy @@ -202,7 +202,7 @@ named_theorems AInvsPre_asms lemma (* ptable_rights_imp_frame *)[AInvsPre_asms]: - assumes "valid_state s" + assumes "valid_state s" "canonical_address x" shows "ptable_rights t s x \ {} \ ptable_lift t s x = Some (addrFromPPtr y) \ in_user_frame y s \ in_device_frame y s" diff --git a/proof/invariant-abstract/ARM/ArchInvariants_AI.thy b/proof/invariant-abstract/ARM/ArchInvariants_AI.thy index 444a6bcd5..b76d82528 100644 --- a/proof/invariant-abstract/ARM/ArchInvariants_AI.thy +++ b/proof/invariant-abstract/ARM/ArchInvariants_AI.thy @@ -75,6 +75,11 @@ lemmas a_type_simps = a_type_def[split_simps kernel_object.split arch_kernel_obj definition "vmsz_aligned ref sz \ is_aligned ref (pageBitsForSize sz)" +(* There are no non-canonical addresses on 32-bit ARM. *) +definition canonical_address :: "obj_ref \ bool" +where + "canonical_address p \ True" + definition "wellformed_mapdata sz \ \(asid, vref). 0 < asid \ asid \ 2^asid_bits - 1 diff --git a/proof/invariant-abstract/Invariants_AI.thy b/proof/invariant-abstract/Invariants_AI.thy index 84f9b410f..b31ee6725 100644 --- a/proof/invariant-abstract/Invariants_AI.thy +++ b/proof/invariant-abstract/Invariants_AI.thy @@ -45,6 +45,7 @@ requalify_consts ASIDPoolObj + canonical_address vs_lookup1 vs_lookup_trans vs_refs diff --git a/proof/invariant-abstract/X64/ArchADT_AI.thy b/proof/invariant-abstract/X64/ArchADT_AI.thy index 69fd4ea9c..e644dcf70 100644 --- a/proof/invariant-abstract/X64/ArchADT_AI.thy +++ b/proof/invariant-abstract/X64/ArchADT_AI.thy @@ -234,7 +234,7 @@ text {* @{text get_page_info} takes the architecture-specific part of the kernel heap, a reference to the page directory, and a virtual memory address. It returns a tuple containing - (a) the physical address, where the associated page table starts, + (a) the physical address, where the associated page starts, (b) the page table's size in bits, and (c) the page attributes (cachable, XNever, etc) (d) the access rights (a subset of @{term "{AllowRead, AllowWrite}"}). diff --git a/proof/invariant-abstract/X64/ArchAInvsPre.thy b/proof/invariant-abstract/X64/ArchAInvsPre.thy index 0ad7ec955..9882fc5d8 100644 --- a/proof/invariant-abstract/X64/ArchAInvsPre.thy +++ b/proof/invariant-abstract/X64/ArchAInvsPre.thy @@ -115,18 +115,15 @@ lemma get_page_info_gpd_kmaps: get_page_info (\obj. get_arch_obj (kheap s obj)) (x64_global_pml4 (arch_state s)) p = Some (b, a, attr, r)\ \ p \ kernel_mappings" - apply (clarsimp simp: valid_global_objs_def valid_arch_state_def) - apply (thin_tac "Ball x y" for x y) - apply (clarsimp simp add: obj_at_def valid_ao_at_def) - apply (clarsimp simp: empty_table_def kernel_mappings_slots_eq) - apply (drule_tac x="ucast (p >> pml4_shift_bits)" in spec) - apply (rule ccontr, simp) - apply (clarsimp simp: get_page_info_def get_pml4_entry_def get_arch_obj_def - get_pdpt_info_def get_pdpt_entry_def get_pd_info_def get_pd_entry_def - get_pt_info_def get_pt_entry_def - split: option.splits arch_kernel_obj.splits kernel_object.splits - pml4e.splits pdpte.splits pde.splits pte.splits) - sorry + apply (clarsimp simp: valid_global_objs_def valid_arch_state_def + obj_at_def valid_ao_at_def + empty_table_def kernel_mappings_slots_eq) + apply (drule_tac x="ucast (p >> pml4_shift_bits)" in spec; clarsimp) + apply (rule ccontr) + apply (clarsimp simp: get_page_info_def get_pml4_entry_def get_arch_obj_def + bit_simps ucast_ucast_mask9 + split: option.splits pml4e.splits arch_kernel_obj.splits) + done lemma get_vspace_of_thread_reachable: "get_vspace_of_thread (kheap s) (arch_state s) t \ x64_global_pml4 (arch_state s) @@ -145,60 +142,29 @@ lemma is_aligned_ptrFromPAddrD: done lemma some_get_page_info_umapsD: - "\get_page_info (\obj. get_arch_obj (kheap s obj)) pd_ref p = Some (b, a, attr, r); - (\\ pd_ref) s; p \ kernel_mappings; valid_arch_objs s; pspace_aligned s; + "\get_page_info (\obj. get_arch_obj (kheap s obj)) pml4_ref p = Some (b, a, attr, r); + (\\ pml4_ref) s; p \ kernel_mappings; valid_arch_objs s; pspace_aligned s; + canonical_address p; valid_asid_table (x64_asid_table (arch_state s)) s; valid_objs s\ - \ (\sz. pageBitsForSize sz = a \ is_aligned b a \ - typ_at (AArch (AIntData sz)) (ptrFromPAddr b) s)" - apply (clarsimp simp: get_page_info_def get_pd_entry_def get_arch_obj_def + \ \sz. pageBitsForSize sz = a \ is_aligned b a \ data_at sz (ptrFromPAddr b) s" + apply (clarsimp simp: get_page_info_def get_pdpt_info_def get_pd_info_def get_pt_info_def + get_pml4_entry_def get_pdpt_entry_def get_pd_entry_def get_pt_entry_def + get_arch_obj_def valid_asid_table_def bit_simps kernel_mappings_slots_eq - split: option.splits Structures_A.kernel_object.splits - arch_kernel_obj.splits) - apply (frule (1) valid_arch_objsD[rotated 2]) - apply (simp add: obj_at_def) - sorry (* - apply (simp add: valid_arch_obj_def) - apply (drule bspec, simp) - apply (simp split: pde.splits) - apply (rename_tac rs pd pt_ref rights w) - apply (subgoal_tac - "((rs, pd_ref) \1 - (VSRef (ucast (ucast (p >> 20))) (Some APageDirectory) # rs, - ptrFromPAddr pt_ref)) s") - prefer 2 - apply (rule vs_lookup1I[rotated 2], simp) - apply (simp add: obj_at_def) - apply (simp add: vs_refs_def pde_ref_def image_def graph_of_def) - apply (rule exI, rule conjI, simp+) - apply (frule (1) vs_lookup_step) - apply (drule (2) stronger_arch_objsD[where ref="x # xs" for x xs]) - apply clarsimp - apply (case_tac ao, simp_all add: a_type_simps obj_at_def)[1] - apply (simp add: get_pt_info_def get_pt_entry_def) - apply (drule_tac x="(ucast ((p >> 12) && mask 8))" in spec) - apply (clarsimp simp: obj_at_def valid_arch_obj_def - split: pte.splits) - apply (clarsimp simp: pspace_aligned_def) - apply (drule_tac x = "(ptrFromPAddr b)" in bspec, fastforce) - apply (drule is_aligned_ptrFromPAddrD) - apply simp - apply (clarsimp simp:a_type_simps) - apply (clarsimp simp: pspace_aligned_def) - apply (drule_tac x = "(ptrFromPAddr b)" in bspec, fastforce) - apply (drule is_aligned_ptrFromPAddrD) - apply simp - apply (clarsimp simp:a_type_simps) - apply (clarsimp simp: pspace_aligned_def obj_at_def) - apply (drule_tac x = "(ptrFromPAddr b)" in bspec, fastforce) - apply (drule is_aligned_ptrFromPAddrD) - apply simp - apply (clarsimp simp:a_type_simps) - apply (clarsimp simp: pspace_aligned_def obj_at_def) - apply (drule_tac x = "(ptrFromPAddr b)" in bspec, fastforce) - apply (drule is_aligned_ptrFromPAddrD) - apply simp - apply (clarsimp simp:a_type_simps) - done *) + split: option.splits kernel_object.splits arch_kernel_obj.splits + pml4e.splits pdpte.splits pde.splits pte.splits) + apply (all \drule (2) vs_lookup_step_alt[OF _ _ vs_refs_pml4I], + simp add: ucast_ucast_mask9, fastforce\) + prefer 3 subgoal + by (rule exI[of _ X64HugePage]; frule (3) valid_arch_objs_entryD; + clarsimp simp: bit_simps vmsz_aligned_def) + apply (all \drule (2) vs_lookup_step_alt[OF _ _ vs_refs_pdptI], fastforce\) + prefer 2 subgoal + by (rule exI[of _ X64LargePage]; frule (3) valid_arch_objs_entryD; + clarsimp simp: bit_simps vmsz_aligned_def) + apply (drule (2) vs_lookup_step_alt[OF _ _ vs_refs_pdI], fastforce) + by (rule exI[of _ X64SmallPage]; frule (3) valid_arch_objs_entryD; + clarsimp simp: bit_simps vmsz_aligned_def) lemma user_mem_dom_cong: "kheap s = kheap s' \ dom (user_mem s) = dom (user_mem s')" @@ -216,52 +182,49 @@ lemma device_frame_in_device_region: global_naming Arch named_theorems AInvsPre_asms -lemma (* ptable_rights_imp_user_frame *)[AInvsPre_asms]: - assumes "valid_state s" +lemma ptable_rights_imp_frame[AInvsPre_asms]: + assumes "valid_state s" "canonical_address x" shows "ptable_rights t s x \ {} \ ptable_lift t s x = Some (addrFromPPtr y) \ - in_user_frame y s" - sorry (* - apply (clarsimp simp: ptable_rights_def ptable_lift_def in_user_frame_def + in_user_frame y s \ in_device_frame y s" + apply (rule ccontr) + using assms + apply (clarsimp simp: ptable_lift_def ptable_rights_def + in_user_frame_def in_device_frame_def split: option.splits) - apply (rename_tac b a r) apply (case_tac "x \ kernel_mappings") - apply (frule (1) some_get_page_info_kmapsD) - using assms - apply (clarsimp simp add: valid_state_def) - using assms - apply (clarsimp simp add: valid_state_def) - apply simp + apply (frule (2) some_get_page_info_kmapsD; fastforce simp: valid_state_def) apply (frule some_get_page_info_umapsD) - apply (rule get_vspace_of_thread_reachable) - apply clarsimp - apply (frule get_page_info_gpd_kmaps[rotated 2]) - using assms - apply (simp_all add: valid_state_def valid_pspace_def - valid_arch_state_def) - apply clarsimp - apply (frule is_aligned_add_helper[OF _ and_mask_less', - THEN conjunct2, of _ _ x]) + apply (rule get_vspace_of_thread_reachable) + apply clarsimp + apply (frule get_page_info_gpd_kmaps[rotated 2]) + apply (simp_all add: valid_state_def valid_pspace_def + valid_arch_state_def) + apply (clarsimp simp: data_at_def)+ + apply (drule_tac x=sz in spec)+ + apply (rename_tac p_addr attr rghts sz) + apply (frule is_aligned_add_helper[OF _ and_mask_less', THEN conjunct2, of _ _ x]) apply (simp only: pbfs_less_wb'[simplified word_bits_def]) - apply (clarsimp simp: ptrFromPAddr_def Platform.X64.addrFromPPtr_def - field_simps) - apply (rule_tac x=sz in exI) + apply (clarsimp simp: data_at_def ptrFromPAddr_def addrFromPPtr_def field_simps) + apply (subgoal_tac "p_addr + (pptrBase + (x && mask (pageBitsForSize sz))) + && ~~ mask (pageBitsForSize sz) = p_addr + pptrBase") + apply simp apply (subst add.assoc[symmetric]) apply (subst is_aligned_add_helper) apply (erule aligned_add_aligned) - apply (case_tac sz, simp_all add: physMappingOffset_def - kernelBase_addr_def physBase_def is_aligned_def)[1] - apply (case_tac sz, simp_all add: word_bits_conv)[1] + apply (case_tac sz; simp add: is_aligned_def pptrBase_def bit_simps) + apply simp apply (rule and_mask_less') - apply (case_tac sz, simp_all add: word_bits_conv)[1] + apply (case_tac sz; simp add: bit_simps) apply simp - done *) + done + end interpretation AInvsPre?: AInvsPre proof goal_cases interpret Arch . - case 1 show ?case apply (intro_locales; (unfold_locales, fact AInvsPre_asms)?) sorry + case 1 show ?case by (intro_locales; (unfold_locales; fact AInvsPre_asms)?) qed requalify_facts @@ -269,5 +232,4 @@ requalify_facts X64.device_mem_dom_cong X64.device_frame_in_device_region - end diff --git a/proof/invariant-abstract/X64/ArchInvariants_AI.thy b/proof/invariant-abstract/X64/ArchInvariants_AI.thy index 61000936a..dbd31845f 100644 --- a/proof/invariant-abstract/X64/ArchInvariants_AI.thy +++ b/proof/invariant-abstract/X64/ArchInvariants_AI.thy @@ -2973,6 +2973,40 @@ lemma valid_arch_obj_default': unfolding default_arch_object_def by (cases aobject_type; simp) +lemma valid_arch_obj_entryD: + shows valid_arch_obj_pml4eD: "\valid_arch_obj (PageMapL4 pm) s; pm i = pml4e; i \ kernel_mapping_slots\ \ valid_pml4e pml4e s" + and valid_arch_obj_pdpteD: "\valid_arch_obj (PDPointerTable pdpt) s; pdpt i = pdpte\ \ valid_pdpte pdpte s" + and valid_arch_obj_pdeD : "\valid_arch_obj (PageDirectory pd) s; pd i = pde\ \ valid_pde pde s" + and valid_arch_obj_pteD : "\valid_arch_obj (PageTable pt) s; pt i = pte\ \ valid_pte pte s" + by fastforce+ + +lemmas valid_arch_objsD_alt' + = valid_arch_objsD[simplified obj_at_def, simplified] + +lemmas valid_arch_objs_entryD + = valid_arch_obj_entryD[OF valid_arch_objsD_alt'] + +lemmas vs_lookup_step_alt + = vs_lookup_step[OF _ vs_lookup1I[OF _ _ refl], simplified obj_at_def, simplified] + +lemma pdpte_graph_ofI: + "\pdpt x = pdpte; pdpte_ref pdpte = Some v\ \ (x, v) \ graph_of (pdpte_ref \ pdpt)" + by (rule graph_ofI, simp) + +lemma vs_refs_pdptI: + "\pdpt ((ucast (r :: machine_word)) :: 9 word) = PageDirectoryPDPTE x a b; + \n \ 9. n < 64 \ \ r !! n\ + \ (VSRef r (Some APDPointerTable), ptrFromPAddr x) \ vs_refs (ArchObj (PDPointerTable pdpt))" + apply (simp add: vs_refs_def) + apply (rule image_eqI[rotated]) + apply (erule pdpte_graph_ofI) + apply (simp add: pdpte_ref_def) + apply (simp add: ucast_ucast_mask) + apply (rule word_eqI) + apply (simp add: word_size) + apply (rule ccontr, auto) + done + end (* diff --git a/proof/invariant-abstract/X64/ArchVSpace_AI.thy b/proof/invariant-abstract/X64/ArchVSpace_AI.thy index 72210c3c1..de1c497a6 100644 --- a/proof/invariant-abstract/X64/ArchVSpace_AI.thy +++ b/proof/invariant-abstract/X64/ArchVSpace_AI.thy @@ -35,7 +35,6 @@ lemma do_machine_op_lift_invs: abbreviation "canonicalise x \ (scast ((ucast x) :: 48 word)) :: 64 word" -(* FIXME x64: this needs canonical_address shenanigans *) lemma pptr_base_shift_cast_le: fixes x :: "9 word" shows "((pptr_base >> pml4_shift_bits) && mask ptTranslationBits \ ucast x) =