From f21d06d35a2428738b75b6e322fd2762391a537b Mon Sep 17 00:00:00 2001 From: Joel Beeren Date: Fri, 2 Dec 2016 15:10:51 +1100 Subject: [PATCH 01/10] AInvs: remove 32-bit references in Untyped_AI --- .../ARM/ArchInvariants_AI.thy | 2 + .../invariant-abstract/ARM/ArchRetype_AI.thy | 2 +- .../invariant-abstract/ARM/ArchUntyped_AI.thy | 12 +- proof/invariant-abstract/Untyped_AI.thy | 172 ++++++++++-------- 4 files changed, 101 insertions(+), 87 deletions(-) diff --git a/proof/invariant-abstract/ARM/ArchInvariants_AI.thy b/proof/invariant-abstract/ARM/ArchInvariants_AI.thy index fe2ff0f52..6148c49b8 100644 --- a/proof/invariant-abstract/ARM/ArchInvariants_AI.thy +++ b/proof/invariant-abstract/ARM/ArchInvariants_AI.thy @@ -373,6 +373,8 @@ definition where "vs_lookup \ \s. vs_lookup_trans s `` vs_asid_refs (arm_asid_table (arch_state s))" +definition "second_level_tables \ arch_state.arm_global_pts" + end context begin interpretation Arch . diff --git a/proof/invariant-abstract/ARM/ArchRetype_AI.thy b/proof/invariant-abstract/ARM/ArchRetype_AI.thy index 367c55616..1acf3fa94 100644 --- a/proof/invariant-abstract/ARM/ArchRetype_AI.thy +++ b/proof/invariant-abstract/ARM/ArchRetype_AI.thy @@ -658,7 +658,7 @@ requalify_consts post_retype_invs_check end definition - post_retype_invs :: "apiobject_type \ word32 list \ 'z::state_ext state \ bool" + post_retype_invs :: "apiobject_type \ machine_word list \ 'z::state_ext state \ bool" where "post_retype_invs tp refs \ if post_retype_invs_check tp diff --git a/proof/invariant-abstract/ARM/ArchUntyped_AI.thy b/proof/invariant-abstract/ARM/ArchUntyped_AI.thy index d3716e58c..76653d5c5 100644 --- a/proof/invariant-abstract/ARM/ArchUntyped_AI.thy +++ b/proof/invariant-abstract/ARM/ArchUntyped_AI.thy @@ -436,7 +436,7 @@ lemma invoke_untyped_st_tcb_at[Untyped_AI_assms]: (*FIXME: move *) done (* nonempty_table *) definition - nonempty_table :: "word32 set \ Structures_A.kernel_object \ bool" + nonempty_table :: "machine_word set \ Structures_A.kernel_object \ bool" where "nonempty_table S ko \ (a_type ko = AArch APageTable \ a_type ko = AArch APageDirectory) @@ -452,7 +452,7 @@ lemma create_cap_valid_arch_caps[wp, Untyped_AI_assms]: and valid_cap (default_cap tp oref sz dev) and (\(s::'state_ext::state_ext state). \r\obj_refs (default_cap tp oref sz dev). (\p'. \ cte_wp_at (\cap. r \ obj_refs cap) p' s) - \ \ obj_at (nonempty_table (set (arm_global_pts (arch_state s)))) r s) + \ \ obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s) and cte_wp_at (op = cap.NullCap) cref and K (tp \ ArchObject ASIDPoolObj)\ create_cap tp sz p dev (cref, oref) \\rv. valid_arch_caps\" @@ -471,7 +471,7 @@ lemma create_cap_valid_arch_caps[wp, Untyped_AI_assms]: apply (case_tac cref, fastforce) apply (simp add: obj_ref_none_no_asid) apply (rule conjI) - apply (auto simp: is_cap_simps valid_cap_def + apply (auto simp: is_cap_simps valid_cap_def second_level_tables_def obj_at_def nonempty_table_def a_type_simps)[1] apply (clarsimp simp del: imp_disjL) apply (case_tac "\x. x \ obj_refs cap") @@ -663,16 +663,16 @@ lemma mapM_copy_global_mappings_nonempty_table[wp]: (**) lemma init_arch_objects_nonempty_table[wp]: - "\(\s. \ (obj_at (nonempty_table (set (arm_global_pts (arch_state s)))) r s) + "\(\s. \ (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s) \ valid_global_objs s \ valid_arch_state s \ pspace_aligned s) and K (tp = ArchObject PageDirectoryObj \ (\pd\set refs. is_aligned pd pd_bits))\ init_arch_objects tp ptr bits us refs dev - \\rv s. \ (obj_at (nonempty_table (set (arm_global_pts (arch_state s)))) r s)\" + \\rv s. \ (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)\" apply (rule hoare_gen_asm) apply (simp add: init_arch_objects_def) apply (rule hoare_pre) - apply (wp hoare_unless_wp | wpc | simp add: create_word_objects_def reserve_region_def)+ + apply (wp hoare_unless_wp | wpc | simp add: create_word_objects_def reserve_region_def second_level_tables_def)+ done diff --git a/proof/invariant-abstract/Untyped_AI.thy b/proof/invariant-abstract/Untyped_AI.thy index e477c726b..6142459e3 100644 --- a/proof/invariant-abstract/Untyped_AI.thy +++ b/proof/invariant-abstract/Untyped_AI.thy @@ -18,6 +18,8 @@ context begin interpretation Arch . requalify_consts region_in_kernel_window + arch_default_cap + second_level_tables end primrec @@ -44,7 +46,7 @@ locale Untyped_AI_of_bl_nat_to_cref = lemma cnode_cap_bits_range: "\ cte_wp_at P p s; invs s \ \ (\c. P c \ (is_cnode_cap c \ - (\n. n > 0 \ n < 28 \ is_aligned (obj_ref_of c) (n + 4)) (bits_of c)))" + (\n. n > 0 \ n < (word_bits - 4) \ is_aligned (obj_ref_of c) (n + 4)) (bits_of c)))" apply (frule invs_valid_objs) apply (drule(1) cte_wp_at_valid_objs_valid_cap) apply clarsimp @@ -289,7 +291,7 @@ locale Untyped_AI_arch = "\ptr sz s x6 us n dev. \pspace_no_overlap ptr sz (s::'state_ext state) \ x6 \ ASIDPoolObj \ range_cover ptr sz (obj_bits_api (ArchObject x6) us) n \ ptr \ 0(*; tp = ArchObject x6*)\ \ \y\{0..kheap := foldr (\p kh. kh(p \ default_object (ArchObject x6) dev us)) (map (\p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x6) us)) [0.. \ ArchObjectCap (ARM_A.arch_default_cap x6 (ptr_add ptr (y * 2 ^ obj_bits_api (ArchObject x6) us)) us dev)" + (kheap s)\ \ ArchObjectCap (arch_default_cap x6 (ptr_add ptr (y * 2 ^ obj_bits_api (ArchObject x6) us)) us dev)" assumes init_arch_objects_descendants_range[wp]: "\x cref ty ptr n us y dev. \\(s::'state_ext state). descendants_range x cref s \ init_arch_objects ty ptr n us y dev @@ -390,20 +392,23 @@ qed lemma range_cover_stuff: - "\0 < n;n \ unat ((2::word32) ^ sz - of_nat rv >> bits); + notes unat_power_lower_machine = unat_power_lower[where 'a=machine_word_len] + notes unat_of_nat_machine = unat_of_nat_eq[where 'a=machine_word_len] + shows + "\0 < n;n \ unat ((2::machine_word) ^ sz - of_nat rv >> bits); rv \ 2^ sz; sz < word_bits; is_aligned w sz\ \ rv \ unat (alignUp (w + of_nat rv) bits - w) \ (alignUp (w + of_nat rv) bits) && ~~ mask sz = w \ - range_cover (alignUp (w + ((of_nat rv)::word32)) bits) sz bits n" + range_cover (alignUp (w + ((of_nat rv)::machine_word)) bits) sz bits n" apply (clarsimp simp: range_cover_def) proof (intro conjI) assume not_0 : "0 unat ((2::word32) ^ sz - of_nat rv >> bits)" "rv\ 2^sz" + assume bound : "n \ unat ((2::machine_word) ^ sz - of_nat rv >> bits)" "rv\ 2^sz" "sz < word_bits" assume al: "is_aligned w sz" - have space: "(2::word32) ^ sz - of_nat rv \ 2^ sz" + have space: "(2::machine_word) ^ sz - of_nat rv \ 2^ sz" apply (rule word_sub_le[OF word_of_nat_le]) - apply (clarsimp simp: bound unat_power_lower32) + apply (clarsimp simp: bound unat_power_lower_machine) done show cmp: "bits \ sz" using not_0 bound @@ -413,7 +418,7 @@ lemma range_cover_stuff: apply (drule le_trans) apply (rule word_le_nat_alt[THEN iffD1]) apply (rule le_shiftr[OF space]) - apply (subgoal_tac "(2::word32)^sz >> bits = 0") + apply (subgoal_tac "(2::machine_word)^sz >> bits = 0") apply simp apply (rule and_mask_eq_iff_shiftr_0[THEN iffD1]) apply (simp add: and_mask_eq_iff_le_mask) @@ -421,18 +426,18 @@ lemma range_cover_stuff: apply (simp add: word_bits_def mask_def power_overflow) apply (subst le_mask_iff_lt_2n[THEN iffD1]) apply (simp add: word_bits_def) - apply (simp add: word_less_nat_alt[THEN iffD2] unat_power_lower32) + apply (simp add: word_less_nat_alt[THEN iffD2] unat_power_lower_machine) done - have shiftr_t2n[simp]:"(2::word32)^sz >> bits = 2^ (sz - bits)" + have shiftr_t2n[simp]:"(2::machine_word)^sz >> bits = 2^ (sz - bits)" using bound cmp apply (case_tac "sz = 0",simp) - apply (subgoal_tac "(1::word32) << sz >> bits = 2^ (sz -bits)") + apply (subgoal_tac "(1::machine_word) << sz >> bits = 2^ (sz -bits)") apply simp apply (subst shiftl_shiftr1) apply (simp add: word_size word_bits_def shiftl_t2n word_1_and_bl)+ done - have cmp2[simp]: "alignUp (of_nat rv) bits < (2 :: word32) ^ sz" + have cmp2[simp]: "alignUp (of_nat rv) bits < (2 :: machine_word) ^ sz" using bound cmp not_0 apply - apply (case_tac "rv = 0") @@ -440,7 +445,7 @@ lemma range_cover_stuff: apply (clarsimp simp: alignUp_def2) apply (subst mask_eq_x_eq_0[THEN iffD1]) apply (simp add: and_mask_eq_iff_le_mask mask_def) - apply (simp add: p2_gt_0[where 'a=32, folded word_bits_def]) + apply (simp add: p2_gt_0[where 'a=machine_word_len, folded word_bits_def]) apply (simp add: alignUp_def3) apply (subgoal_tac "1 \ unat (2 ^ sz - of_nat rv >> bits)") prefer 2 @@ -450,11 +455,11 @@ lemma range_cover_stuff: apply (simp add: shiftr_div_2n') apply (simp add: td_gal[symmetric]) apply (subst (asm) unat_sub) - apply (simp add: word_of_nat_le unat_power_lower32) + apply (simp add: word_of_nat_le unat_power_lower_machine) apply (simp add: le_diff_conv2 word_of_nat_le unat_le_helper word_less_nat_alt) apply (rule le_less_trans[OF unat_plus_gt]) apply (rule less_le_trans[where y = "2^bits + unat (of_nat rv)"]) - apply (simp add: unat_power_lower32) + apply (simp add: unat_power_lower_machine) apply (rule le_less_trans[OF _ measure_unat]) apply (rule word_le_nat_alt[THEN iffD1]) apply (rule word_and_le2) @@ -462,10 +467,10 @@ lemma range_cover_stuff: apply (subst word_bits_def[symmetric]) apply (erule le_less_trans) apply simp - apply (simp add: unat_power_lower32) + apply (simp add: unat_power_lower_machine) done - show "n + unat (alignUp (w + ((of_nat rv)::word32)) bits && mask sz >> bits) \ 2 ^ (sz - bits)" + show "n + unat (alignUp (w + ((of_nat rv)::machine_word)) bits && mask sz >> bits) \ 2 ^ (sz - bits)" using not_0 bound cmp apply - apply (erule le_trans[OF add_le_mono]) @@ -510,37 +515,42 @@ lemma range_cover_stuff: apply (case_tac "rv = 0") apply simp apply (rule le_trans[OF _ word_le_nat_alt[THEN iffD1,OF alignUp_ge]]) - apply (subst unat_of_nat32) - apply (erule le_less_trans) - apply simp - apply (simp_all add: word_bits_def)[2] + apply (subst unat_of_nat_machine) + apply (erule le_less_trans) + apply (rule power_strict_increasing) + apply (simp_all add: word_bits_def)[4] apply (rule alignUp_is_aligned_nz[where x = "2^sz"]) - apply (rule is_aligned_weaken[OF is_aligned_triv2]) - apply (simp_all add: word_bits_def)[2] - apply (subst word_of_nat_le) - apply (subst unat_power_lower32) - apply simp+ - apply (erule of_nat_neq_0) - apply (erule le_less_trans) - apply (subst word_bits_def[symmetric]) - apply simp - done + apply (rule is_aligned_weaken[OF is_aligned_triv2]) + apply (simp_all add: word_bits_def)[2] + apply (subst word_of_nat_le) + apply (subst unat_power_lower_machine) + apply (simp add: word_bits_def)+ + apply (erule of_nat_neq_0) + apply (erule le_less_trans) + apply (rule power_strict_increasing) + apply (simp add: word_bits_def)+ + done show "alignUp (w + of_nat rv) bits && ~~ mask sz = w" using bound not_0 cmp al apply (clarsimp simp: alignUp_plus[OF is_aligned_weaken] mask_out_add_aligned[symmetric]) apply (clarsimp simp: and_not_mask) - apply (subgoal_tac "alignUp ((of_nat rv)::word32) bits >> sz = 0") + apply (subgoal_tac "alignUp ((of_nat rv)::machine_word) bits >> sz = 0") apply simp apply (simp add: le_mask_iff[symmetric] mask_def) done - show "sz < 32" by (simp add: bound(3)[unfolded word_bits_def, simplified]) - qed + qed (simp add: word_bits_def) + +context Arch begin + (*FIXME: generify proof that uses this *) + lemmas range_cover_stuff_arch = range_cover_stuff[unfolded word_bits_def, simplified] +end + lemma cte_wp_at_range_cover: "\bits < word_bits; rv\ 2^ sz; invs s; cte_wp_at (op = (cap.UntypedCap dev w sz idx)) p s; - 0 < n; n \ unat ((2::word32) ^ sz - of_nat rv >> bits)\ + 0 < n; n \ unat ((2::machine_word) ^ sz - of_nat rv >> bits)\ \ range_cover (alignUp (w + of_nat rv) bits) sz bits n" apply (clarsimp simp: cte_wp_at_caps_of_state) apply (frule(1) caps_of_state_valid) @@ -552,7 +562,7 @@ lemma cte_wp_at_range_cover: lemma le_mask_le_2p: - "\idx \ unat ((ptr::word32) && mask sz);sz < word_bits\ \ idx < 2^ sz" + "\idx \ unat ((ptr::machine_word) && mask sz);sz < word_bits\ \ idx < 2^ sz" apply (erule le_less_trans) apply (rule unat_less_helper) apply simp @@ -682,18 +692,18 @@ lemma cases_imp_eq: by blast lemma inj_16: - "\ of_nat x * 16 = of_nat y * (16 :: word32); + "\ of_nat x * 16 = of_nat y * (16 :: machine_word); x < bnd; y < bnd; bnd \ 2 ^ (word_bits - 4) \ - \ of_nat x = (of_nat y :: word32)" + \ of_nat x = (of_nat y :: machine_word)" apply (fold shiftl_t2n [where n=4, simplified, simplified mult.commute]) apply (simp only: word_bl.Rep_inject[symmetric] bl_shiftl) apply (drule(1) order_less_le_trans)+ - apply (drule of_nat_mono_maybe[rotated, where 'a=32]) + apply (drule of_nat_mono_maybe[rotated, where 'a=machine_word_len]) apply (rule power_strict_increasing) apply (simp add: word_bits_def) apply simp - apply (drule of_nat_mono_maybe[rotated, where 'a=32]) + apply (drule of_nat_mono_maybe[rotated, where 'a=machine_word_len]) apply (rule power_strict_increasing) apply (simp add: word_bits_def) apply simp @@ -705,12 +715,15 @@ lemma inj_16: lemma of_nat_shiftR: "a < 2 ^ word_bits \ - unat (of_nat (shiftR a b)::word32) = unat ((of_nat a :: word32) >> b)" + unat (of_nat (shiftR a b)::machine_word) = unat ((of_nat a :: machine_word) >> b)" apply (subst shiftr_div_2n') apply (clarsimp simp: shiftR_nat) - apply (subst unat_of_nat32) + apply (subst unat_of_nat_eq[where 'a=machine_word_len]) + apply (simp only: word_bits_def) apply (erule le_less_trans[OF div_le_dividend]) - apply (simp add: unat_of_nat32) + apply (subst unat_of_nat_eq[where 'a=machine_word_len]) + apply (simp only: word_bits_def) + apply simp done @@ -1458,17 +1471,17 @@ lemma of_nat_shift_distinct_helper: done -lemmas of_nat_shift_distinct_helper32 = of_nat_shift_distinct_helper[where 'a=32, folded word_bits_def] +lemmas of_nat_shift_distinct_helper_machine = of_nat_shift_distinct_helper[where 'a=machine_word_len, folded word_bits_def] lemma ptr_add_distinct_helper: - "\ ptr_add (p :: word32) (x * 2 ^ n) = ptr_add p (y * 2 ^ n); x \ y; + "\ ptr_add (p :: machine_word) (x * 2 ^ n) = ptr_add p (y * 2 ^ n); x \ y; x < bnd; y < bnd; n < word_bits; bnd \ 2 ^ (word_bits - n) \ \ P" apply (clarsimp simp: ptr_add_def word_unat_power[symmetric] shiftl_t2n[symmetric, simplified mult.commute]) - apply (erule(5) of_nat_shift_distinct_helper32) + apply (erule(5) of_nat_shift_distinct_helper_machine) done @@ -1628,12 +1641,12 @@ lemma retype_region_distinct_sets: apply (clarsimp simp: retype_addrs_def distinct_prop_map) apply (rule distinct_prop_distinct) apply simp - apply (subgoal_tac "of_nat y * (2::word32) ^ obj_bits_api tp us \ of_nat x * 2 ^ obj_bits_api tp us") + apply (subgoal_tac "of_nat y * (2::machine_word) ^ obj_bits_api tp us \ of_nat x * 2 ^ obj_bits_api tp us") apply (case_tac tp) defer apply (simp add:cap_range_def ptr_add_def)+ apply (clarsimp simp: ptr_add_def word_unat_power[symmetric] shiftl_t2n[simplified mult.commute, symmetric]) - apply (erule(2) of_nat_shift_distinct_helper[where 'a=32 and n = "obj_bits_api tp us"]) + apply (erule(2) of_nat_shift_distinct_helper[where 'a=machine_word_len and n = "obj_bits_api tp us"]) apply simp apply (simp add:range_cover_def) apply (erule range_cover.range_cover_n_le) @@ -2055,10 +2068,10 @@ lemma op_equal: "(\x. x = c) = (op = c)" by (rule ext) auto lemma mask_out_eq_0: - "\idx < 2^ sz;sz \ ((of_nat idx)::word32) && ~~ mask sz = 0" + "\idx < 2^ sz;sz \ ((of_nat idx)::machine_word) && ~~ mask sz = 0" apply (clarsimp simp: mask_out_sub_mask) apply (subst less_mask_eq[symmetric]) - apply (erule(1) of_nat_less_pow_32) + apply (erule(1) of_nat_power[where 'a=machine_word_len, folded word_bits_def]) apply simp done @@ -2081,7 +2094,7 @@ lemma is_aligned_neg_mask_eq': lemma neg_mask_mask_unat: "sz < word_bits \ - unat ((ptr::word32) && ~~ mask sz) + unat (ptr && mask sz) = unat ptr" + unat ((ptr::machine_word) && ~~ mask sz) + unat (ptr && mask sz) = unat ptr" apply (subst unat_plus_simple[THEN iffD1,symmetric]) apply (rule is_aligned_no_wrap'[OF is_aligned_neg_mask[OF le_refl]]) apply (rule and_mask_less') @@ -2292,7 +2305,7 @@ proof - apply - apply (erule disjE) apply (erule cte_wp_at_caps_descendants_range_inI[OF _ _ _ range_cover.sz(1) - [where 'a=32, folded word_bits_def]]) + [where 'a=machine_word_len, folded word_bits_def]]) apply (simp add: cte_wp_at_caps_of_state)+ using desc_range apply simp @@ -2314,7 +2327,7 @@ lemma ps_no_overlap[simp]: "ptr && ~~ mask sz \ ptr \ psp using misc cte_wp_at cover apply clarsimp apply (erule cte_wp_at_pspace_no_overlapI[OF _ _ _ - range_cover.sz(1)[where 'a=32, folded word_bits_def]]) + range_cover.sz(1)[where 'a=machine_word_len, folded word_bits_def]]) apply (simp add: cte_wp_at_caps_of_state) apply simp+ done @@ -2324,7 +2337,7 @@ lemma ps_no_overlap[simp]: "ptr && ~~ mask sz \ ptr \ psp apply - apply (erule disjE) apply (erule cte_wp_at_caps_no_overlapI[OF _ _ _ range_cover.sz(1) - [where 'a=32, folded word_bits_def]]) + [where 'a=machine_word_len, folded word_bits_def]]) apply (simp add: cte_wp_at_caps_of_state)+ apply (erule descendants_range_caps_no_overlapI) apply (simp add: cte_wp_at_caps_of_state)+ @@ -2390,14 +2403,14 @@ lemma ps_no_overlap[simp]: "ptr && ~~ mask sz \ ptr \ psp {ptr..ptr + of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} = {}" proof - have idx_compare''[simp]: - "unat ((ptr && mask sz) + (of_nat (length slots) * (2::word32) ^ obj_bits_api tp us)) < 2 ^ sz + "unat ((ptr && mask sz) + (of_nat (length slots) * (2::machine_word) ^ obj_bits_api tp us)) < 2 ^ sz \ ptr + of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < ptr + of_nat (length slots) * 2 ^ obj_bits_api tp us" apply (rule minus_one_helper,simp) apply (rule neq_0_no_wrap) apply (rule machine_word_plus_mono_right_split) apply (simp add: shiftl_t2n range_cover_unat[OF cover] field_simps) - apply (simp add: range_cover.sz[where 'a=32, folded word_bits_def, OF cover])+ + apply (simp add: range_cover.sz[where 'a=machine_word_len, folded word_bits_def, OF cover])+ done show ?thesis apply (clarsimp simp: mask_out_sub_mask blah) @@ -2486,14 +2499,14 @@ lemma valid_untyped_cap_inc: apply simp apply (erule disjoint_subset[rotated]) apply (frule(1) le_mask_le_2p[OF _ - range_cover.sz(1)[where 'a=32, folded word_bits_def]]) + range_cover.sz(1)[where 'a=machine_word_len, folded word_bits_def]]) apply clarsimp apply (rule word_plus_mono_right) apply (rule word_of_nat_le) - apply (simp add: unat_of_nat32 range_cover_unat field_simps) + apply (simp add: unat_of_nat_eq[where 'a=machine_word_len] range_cover_unat field_simps) apply (rule is_aligned_no_wrap'[OF is_aligned_neg_mask[OF le_refl]]) apply (simp add: word_less_nat_alt - unat_power_lower[where 'a=32, folded word_bits_def]) + unat_power_lower[where 'a=machine_word_len, folded word_bits_def]) apply (simp add: range_cover_unat range_cover.unat_of_nat_shift shiftl_t2n field_simps) apply (subst add.commute) apply (simp add: range_cover.range_cover_compare_bound) @@ -2731,16 +2744,15 @@ lemma create_cap_irq_handlers[wp]: crunch valid_arch_objs[wp]: create_cap "valid_arch_objs" (simp: crunch_simps) - locale Untyped_AI_nonempty_table = fixes state_ext_t :: "('state_ext::state_ext) itself" - fixes nonempty_table :: "word32 set \ Structures_A.kernel_object \ bool" + fixes nonempty_table :: "machine_word set \ Structures_A.kernel_object \ bool" assumes create_cap_valid_arch_caps[wp]: "\tp oref sz dev cref p.\valid_arch_caps and valid_cap (default_cap tp oref sz dev) and (\(s::'state_ext state). \r\obj_refs (default_cap tp oref sz dev). (\p'. \ cte_wp_at (\cap. r \ obj_refs cap) p' s) - \ \ obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) r s) + \ \ obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s) and cte_wp_at (op = cap.NullCap) cref and K (tp \ ArchObject ASIDPoolObj)\ create_cap tp sz p dev (cref, oref) \\rv. valid_arch_caps\" @@ -2832,7 +2844,7 @@ lemma (in Untyped_AI_nonempty_table) create_cap_invs[wp]: and real_cte_at cref and (\(s::'state_ext state). \r\obj_refs (default_cap tp oref sz dev). (\p'. \ cte_wp_at (\cap. r \ obj_refs cap) p' s) - \ \ obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) r s) + \ \ obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s) and K (p \ cref \ tp \ ArchObject ASIDPoolObj)\ create_cap tp sz p dev (cref, oref) \\rv. invs\" apply (rule hoare_pre) @@ -2865,9 +2877,9 @@ lemma create_cap_no_cap[wp]: done lemma (in Untyped_AI_nonempty_table) create_cap_nonempty_tables[wp]: - "\\s. P (obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) p s)\ + "\\s. P (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) p s)\ create_cap tp sz p' dev (cref, oref) - \\rv s. P (obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) p s)\" + \\rv s. P (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) p s)\" apply (rule hoare_pre) apply (rule hoare_use_eq [where f=arch_state, OF create_cap_arch_state]) apply (simp add: create_cap_def set_cdt_def) @@ -2912,7 +2924,7 @@ lemma (in Untyped_AI_nonempty_table) create_caps_invs_inv: real_cte_at (fst tup) s) \ (\tup \ set ((cref,oref)#list). \r \ obj_refs (default_cap tp (snd tup) sz dev). (\p'. \ cte_wp_at (\cap. r \ obj_refs cap) p' s) - \ \ obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) r s) + \ \ obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s) \ distinct (p # (map fst ((cref,oref)#list))) \ tp \ ArchObject ASIDPoolObj) \ create_cap tp sz p dev (cref,oref) @@ -2936,7 +2948,7 @@ lemma (in Untyped_AI_nonempty_table) create_caps_invs_inv: real_cte_at (fst tup) s) \ (\tup \ set list. \r \ obj_refs (default_cap tp (snd tup) sz dev). (\p'. \ cte_wp_at (\cap. r \ obj_refs cap) p' s) - \ \ obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) r s) + \ \ obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s) \ distinct (p # (map fst list)) \ tp \ ArchObject ASIDPoolObj) \" apply (rule hoare_pre) @@ -2977,7 +2989,7 @@ lemma (in Untyped_AI_nonempty_table) create_caps_invs: real_cte_at (fst tup) s) \ (\tup \ set (zip crefs orefs). \r \ obj_refs (default_cap tp (snd tup) sz dev). (\p'. \ cte_wp_at (\cap. r \ obj_refs cap) p' s) - \ \ obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) r s) + \ \ obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s) \ distinct (p # (map fst (zip crefs orefs))) \ tp \ ArchObject ASIDPoolObj \ mapM_x (create_cap tp sz p dev) (zip crefs orefs) @@ -3014,7 +3026,7 @@ lemma (in Untyped_AI_nonempty_table) create_caps_invs_empty_descendants: ex_cte_cap_wp_to is_cnode_cap (fst tup) s \ real_cte_at (fst tup) s) \ (\tup \ set (zip crefs orefs). \r \ obj_refs (default_cap tp (snd tup) sz dev). (\p'. \ cte_wp_at (\cap. r \ obj_refs cap) p' s) - \ \ obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) r s) + \ \ obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s) \ distinct (p # (map fst (zip crefs orefs))) \ tp \ ArchObject ASIDPoolObj\ mapM_x (create_cap tp sz p dev) (zip crefs orefs) @@ -3101,7 +3113,7 @@ lemma retype_region_refs_distinct[wp]: | drule subsetD [OF obj_refs_default_cap] less_two_pow_divD)+ apply (simp add: range_cover_def word_bits_def) - apply (erule range_cover.range_cover_n_le[where 'a=32, folded word_bits_def]) + apply (erule range_cover.range_cover_n_le[where 'a=machine_word_len, folded word_bits_def]) done @@ -3156,9 +3168,9 @@ lemma do_machine_op_obj_at_arch_state[wp]: by (clarsimp simp: do_machine_op_def split_def | wp)+ lemma (in Untyped_AI_nonempty_table) retype_nonempty_table[wp]: - "\\(s::('state_ext::state_ext) state). \ (obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) r s)\ + "\\(s::('state_ext::state_ext) state). \ (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)\ retype_region ptr sz us tp dev - \\rv s. \ (obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) r s)\" + \\rv s. \ (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)\" apply (simp add: retype_region_def split del: split_if) apply (rule hoare_pre) apply (wp|simp del: fun_upd_apply)+ @@ -3188,9 +3200,9 @@ lemma invs_cap_refs_in_kernel_window[elim!]: by (simp add: invs_def valid_state_def) lemma (in Untyped_AI_nonempty_table) set_cap_nonempty_tables[wp]: - "\\s. P (obj_at (nonempty_table (set (arm_global_pts (arch_state s)))) p s)\ + "\\s. P (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) p s)\ set_cap cap cref - \\rv s. P (obj_at (nonempty_table (set (arm_global_pts (arch_state s)))) p s)\" + \\rv s. P (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) p s)\" apply (rule hoare_pre) apply (rule hoare_use_eq [where f=arch_state, OF set_cap_arch]) apply (wp set_cap_obj_at_impossible) @@ -3307,7 +3319,7 @@ lemma (in invoke_untyp_invs_retype_assms) pf : done lemma (in invoke_untyp_invs_retype_assms) of_nat_length: - "(of_nat (length slots)::word32) - (1::word32) < (of_nat (length slots)::word32)" + "(of_nat (length slots)::machine_word) - (1::machine_word) < (of_nat (length slots)::machine_word)" using vslot using range_cover.range_cover_le_n_less(1)[OF cover,where p = "length slots"] apply - @@ -3347,7 +3359,7 @@ lemma (in invoke_untyp_invs_retype_assms) ps_no_overlap[simp]: using misc cte_wp_at cover apply clarsimp apply (erule(3) cte_wp_at_pspace_no_overlapI - [OF _ _ _ range_cover.sz(1)[where 'a=32, folded word_bits_def]]) + [OF _ _ _ range_cover.sz(1)[where 'a=machine_word_len, folded word_bits_def]]) done lemmas (in invoke_untyp_invs_retype_assms) ex_cte_no_overlap = invoke_untyped_proofs.ex_cte_no_overlap[OF pf] @@ -3427,7 +3439,7 @@ lemma (in invoke_untyp_invs_retype_assms) temp_simp [simp]:"ptr \ 0" done lemma (in invoke_untyp_invs_retype_assms) idx_compare''[simp]: - "unat ((ptr && mask sz) + (of_nat (length slots) * (2::word32) ^ obj_bits_api tp us)) < 2 ^ sz + "unat ((ptr && mask sz) + (of_nat (length slots) * (2::machine_word) ^ obj_bits_api tp us)) < 2 ^ sz \ ptr + of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < ptr + of_nat (length slots) * 2 ^ obj_bits_api tp us" apply (rule minus_one_helper,simp) @@ -3435,11 +3447,11 @@ lemma (in invoke_untyp_invs_retype_assms) idx_compare''[simp]: apply (rule machine_word_plus_mono_right_split) apply (simp add: shiftl_t2n range_cover_unat[OF cover] field_simps) apply (simp add: range_cover.sz - [where 'a=32, folded word_bits_def, OF cover])+ + [where 'a=machine_word_len, folded word_bits_def, OF cover])+ done lemma (in invoke_untyp_invs_retype_assms) idx_compare'''[simp]: - "\unat (of_nat (length slots) * (2::word32) ^ obj_bits_api tp us) < 2 ^ sz; + "\unat (of_nat (length slots) * (2::machine_word) ^ obj_bits_api tp us) < 2 ^ sz; ptr && ~~ mask sz = ptr\ \ ptr + of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < ptr + of_nat (length slots) * 2 ^ obj_bits_api tp us " @@ -3448,7 +3460,7 @@ lemma (in invoke_untyp_invs_retype_assms) idx_compare'''[simp]: apply (rule neq_0_no_wrap) apply (rule machine_word_plus_mono_right_split[where sz = sz]) apply (simp add: is_aligned_mask)+ - apply (simp add: range_cover.sz[where 'a=32, folded word_bits_def, OF cover])+ + apply (simp add: range_cover.sz[where 'a=machine_word_len, folded word_bits_def, OF cover])+ done lemma (in invoke_untyp_invs_retype_assms) detype_locale: From fc55c229fd26a9acfea52b08fb99bb783e46ed1d Mon Sep 17 00:00:00 2001 From: Joel Beeren Date: Fri, 2 Dec 2016 15:11:35 +1100 Subject: [PATCH 02/10] x64: allow skip proofs up to Untyped_AI, add definitions to let generic Untyped_AI pass in x64 context --- proof/invariant-abstract/X64/ArchInvariants_AI.thy | 2 ++ proof/invariant-abstract/X64/ArchRetype_AI.thy | 6 +++--- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/proof/invariant-abstract/X64/ArchInvariants_AI.thy b/proof/invariant-abstract/X64/ArchInvariants_AI.thy index 799b34c34..6e5ec7746 100644 --- a/proof/invariant-abstract/X64/ArchInvariants_AI.thy +++ b/proof/invariant-abstract/X64/ArchInvariants_AI.thy @@ -498,6 +498,8 @@ definition where "vs_lookup \ \s. vs_lookup_trans s `` vs_asid_refs (x64_asid_table (arch_state s))" +definition "second_level_tables \ arch_state.x64_global_pdpts" + end context begin interpretation Arch . diff --git a/proof/invariant-abstract/X64/ArchRetype_AI.thy b/proof/invariant-abstract/X64/ArchRetype_AI.thy index 4e7bfb4a3..61419f708 100644 --- a/proof/invariant-abstract/X64/ArchRetype_AI.thy +++ b/proof/invariant-abstract/X64/ArchRetype_AI.thy @@ -583,7 +583,7 @@ requalify_consts post_retype_invs_check end definition - post_retype_invs :: "apiobject_type \ word32 list \ 'z::state_ext state \ bool" + post_retype_invs :: "apiobject_type \ machine_word list \ 'z::state_ext state \ bool" where "post_retype_invs tp refs \ if post_retype_invs_check tp @@ -952,10 +952,10 @@ lemma unique_table_refs_null: definition - region_in_kernel_window :: "word32 set \ 'z state \ bool" + region_in_kernel_window :: "machine_word set \ 'z state \ bool" where "region_in_kernel_window S \ - \s. \x \ S. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow" + \s. \x \ S. x64_kernel_vspace (arch_state s) x = X64VSpaceKernelWindow" end From 757545b8f14e62f616197c2d3c43db468e8fa55d Mon Sep 17 00:00:00 2001 From: Joel Beeren Date: Tue, 6 Dec 2016 17:07:08 +1100 Subject: [PATCH 03/10] x64: generify up to Finalise_AI --- proof/invariant-abstract/Finalise_AI.thy | 2 +- proof/invariant-abstract/IpcCancel_AI.thy | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/proof/invariant-abstract/Finalise_AI.thy b/proof/invariant-abstract/Finalise_AI.thy index 7737d17b4..081673c9d 100644 --- a/proof/invariant-abstract/Finalise_AI.thy +++ b/proof/invariant-abstract/Finalise_AI.thy @@ -989,7 +989,7 @@ crunch tcb_at[wp]: unbind_notification "tcb_at t" locale Finalise_AI_3 = Finalise_AI_2 a b for a :: "('a :: state_ext) itself" and b :: "('b :: state_ext) itself" + - fixes replaceable_or_arch_update :: "'a state \ 32 word \ bool list \ cap \ cap \ bool" + fixes replaceable_or_arch_update :: "'a state \ machine_word \ bool list \ cap \ cap \ bool" fixes c :: "'c itself" assumes finalise_cap_invs: "\ cap slot x. diff --git a/proof/invariant-abstract/IpcCancel_AI.thy b/proof/invariant-abstract/IpcCancel_AI.thy index 2cf9a41e7..dd3e4e972 100644 --- a/proof/invariant-abstract/IpcCancel_AI.thy +++ b/proof/invariant-abstract/IpcCancel_AI.thy @@ -820,7 +820,7 @@ lemma suspend_unlive: done -definition bound_refs_of_tcb :: "'a state \ 32 word \ (32 word \ reftype) set" +definition bound_refs_of_tcb :: "'a state \ machine_word \ (machine_word \ reftype) set" where "bound_refs_of_tcb s t \ case kheap s t of Some (TCB tcb) \ tcb_bound_refs (tcb_bound_notification tcb) From 25a63548593a9b5a5a6ebf4e61c9dcd85e0fcb6c Mon Sep 17 00:00:00 2001 From: Joel Beeren Date: Tue, 13 Dec 2016 10:15:53 +1100 Subject: [PATCH 04/10] AInvs: remove references to arch specific stuff in Ipc_AI --- proof/invariant-abstract/ARM/ArchIpc_AI.thy | 4 ++-- spec/abstract/ARM/ArchCSpace_A.thy | 14 ++++++++++---- spec/abstract/ARM/Arch_Structs_A.thy | 5 +++++ spec/abstract/CSpace_A.thy | 2 ++ spec/abstract/Structures_A.thy | 8 +------- 5 files changed, 20 insertions(+), 13 deletions(-) diff --git a/proof/invariant-abstract/ARM/ArchIpc_AI.thy b/proof/invariant-abstract/ARM/ArchIpc_AI.thy index 7a0ad67d8..01a61b0d7 100644 --- a/proof/invariant-abstract/ARM/ArchIpc_AI.thy +++ b/proof/invariant-abstract/ARM/ArchIpc_AI.thy @@ -46,11 +46,11 @@ lemma update_cap_data_closedform: simp_all only: cap.simps update_cap_data_def is_ep_cap.simps if_False if_True is_ntfn_cap.simps is_cnode_cap.simps is_arch_cap_def word_size cap_ep_badge.simps badge_update_def o_def cap_rights_update_def - simp_thms cap_rights.simps Let_def split_def + simp_thms cap_rights.simps Let_def split_def badge_bits_def the_cnode_cap_def fst_conv snd_conv fun_app_def the_arch_cap_def arch_update_cap_data_def cong: if_cong) - apply auto + apply (auto simp: word_bits_def cnode_padding_bits_def cnode_guard_size_bits_def) done lemma cap_asid_PageCap_None [simp]: diff --git a/spec/abstract/ARM/ArchCSpace_A.thy b/spec/abstract/ARM/ArchCSpace_A.thy index f716a3b22..becf0aab7 100644 --- a/spec/abstract/ARM/ArchCSpace_A.thy +++ b/spec/abstract/ARM/ArchCSpace_A.thy @@ -21,16 +21,22 @@ begin context Arch begin global_naming ARM_A +definition cnode_guard_size_bits :: "nat" +where + "cnode_guard_size_bits \ 5" + +definition cnode_padding_bits :: "nat" +where + "cnode_padding_bits \ 3" + text {* On a user request to modify a cnode capability, extract new guard bits and guard. *} definition update_cnode_cap_data :: "data \ nat \ data" where "update_cnode_cap_data w \ let - pad_bits = 3; guard_bits = 18; - guard_size_bits = 5; - guard_size' = unat ((w >> pad_bits) && mask guard_size_bits); - guard'' = (w >> (pad_bits + guard_size_bits)) && mask guard_bits + guard_size' = unat ((w >> cnode_padding_bits) && mask cnode_guard_size_bits); + guard'' = (w >> (cnode_padding_bits + cnode_guard_size_bits)) && mask guard_bits in (guard_size', guard'')" text {* For some purposes capabilities to physical objects are treated diff --git a/spec/abstract/ARM/Arch_Structs_A.thy b/spec/abstract/ARM/Arch_Structs_A.thy index c74ef075f..f315d36cb 100644 --- a/spec/abstract/ARM/Arch_Structs_A.thy +++ b/spec/abstract/ARM/Arch_Structs_A.thy @@ -261,6 +261,11 @@ where | DataPage dev sz \ if dev then ADeviceData sz else AUserData sz | ASIDPool f \ AASIDPool)" + +text {* For implementation reasons the badge word has differing amounts of bits *} +definition + badge_bits :: nat where + "badge_bits \ 28" end end diff --git a/spec/abstract/CSpace_A.thy b/spec/abstract/CSpace_A.thy index bdf6dc26a..3032bc4b0 100644 --- a/spec/abstract/CSpace_A.thy +++ b/spec/abstract/CSpace_A.thy @@ -39,6 +39,8 @@ requalify_consts msg_max_extra_caps msg_align_bits update_cnode_cap_data + cnode_padding_bits + cnode_guard_size_bits end diff --git a/spec/abstract/Structures_A.thy b/spec/abstract/Structures_A.thy index c123227c5..c9d769b24 100755 --- a/spec/abstract/Structures_A.thy +++ b/spec/abstract/Structures_A.thy @@ -40,6 +40,7 @@ requalify_consts asid_high_bits asid_low_bits arch_is_frame_type + badge_bits end text {* @@ -222,13 +223,6 @@ definition | ArchObjectCap acap \ ArchObjectCap (acap_rights_update cr' acap) | _ \ cap" -text {* For implementation reasons not all bits of the badge word can be used. *} -definition - badge_bits :: nat where - "badge_bits \ 28" - -declare badge_bits_def [simp] - definition badge_update :: "badge \ cap \ cap" where "badge_update data cap \ From a1ab2d90b1a177c564d9fa4f97720f7b7c96f495 Mon Sep 17 00:00:00 2001 From: Joel Beeren Date: Tue, 13 Dec 2016 10:17:28 +1100 Subject: [PATCH 05/10] x64: fix up ArchIPC_AI --- .../X64/ArchFinalise_AI.thy | 86 +++++++++---------- proof/invariant-abstract/X64/ArchIpc_AI.thy | 80 +++++++++-------- spec/abstract/X64/ArchCSpace_A.thy | 14 ++- spec/abstract/X64/ArchVSpace_A.thy | 6 +- spec/abstract/X64/Arch_A.thy | 7 -- spec/abstract/X64/Arch_Structs_A.thy | 5 ++ 6 files changed, 104 insertions(+), 94 deletions(-) diff --git a/proof/invariant-abstract/X64/ArchFinalise_AI.thy b/proof/invariant-abstract/X64/ArchFinalise_AI.thy index df682ffca..a19a327da 100644 --- a/proof/invariant-abstract/X64/ArchFinalise_AI.thy +++ b/proof/invariant-abstract/X64/ArchFinalise_AI.thy @@ -21,12 +21,12 @@ lemma (* obj_at_not_live_valid_arch_cap_strg *) [Finalise_AI_asms]: \ obj_at (\ko. \ live ko) r s" by (clarsimp simp: valid_cap_def obj_at_def a_type_arch_live - split: arch_cap.split_asm) + split: arch_cap.split_asm split_if_asm) global_naming X64 lemma valid_global_refs_asid_table_udapte [iff]: - "valid_global_refs (s\arch_state := arm_asid_table_update f (arch_state s)\) = + "valid_global_refs (s\arch_state := x64_asid_table_update f (arch_state s)\) = valid_global_refs s" by (simp add: valid_global_refs_def global_refs_def) @@ -43,8 +43,10 @@ lemma reachable_pg_cap_update[simp]: by (simp add:reachable_pg_cap_def vs_lookup_pages_def vs_lookup_pages1_def obj_at_def) +(* FIXME x64: this needs stuff about equality between vs_lookup and vs_lookup_pages + for PageMapL4, PDPTs *) lemma vs_lookup_pages_eq: - "\valid_arch_objs s; valid_asid_table (arm_asid_table (arch_state s)) s; + "\valid_arch_objs s; valid_asid_table (x64_asid_table (arch_state s)) s; valid_cap cap s; table_cap_ref cap = Some vref; oref \ obj_refs cap\ \ (vref \ oref) s = (vref \ oref) s" apply (clarsimp simp: table_cap_ref_def @@ -54,10 +56,10 @@ lemma vs_lookup_pages_eq: apply (rule iffI[rotated, OF vs_lookup_pages_vs_lookupI], assumption) apply (simp add: valid_cap_def) apply (erule vs_lookup_vs_lookup_pagesI', clarsimp+) - done + sorry lemma nat_to_cref_unat_of_bl': - "\ length xs < 32; n = length xs \ \ + "\ length xs < word_bits; n = length xs \ \ nat_to_cref n (unat (of_bl xs :: machine_word)) = xs" apply (simp add: nat_to_cref_def word_bits_def) apply (rule nth_equalityI) @@ -72,11 +74,13 @@ lemma nat_to_cref_unat_of_bl': lemmas nat_to_cref_unat_of_bl = nat_to_cref_unat_of_bl' [OF _ refl] -lemma invs_arm_asid_table_unmap: +(* FIXME x64: this needs reevaluation - do we need the "asid_map" premise? + note delete_asid_pool for arm and x64 differ a lot *) +lemma invs_x64_asid_table_unmap: "invs s \ is_aligned base asid_low_bits \ base \ mask asid_bits - \ (\x\set [0.e.2 ^ asid_low_bits - 1]. arm_asid_map (arch_state s) (base + x) = None) - \ tab = arm_asid_table (arch_state s) - \ invs (s\arch_state := arch_state s\arm_asid_table := tab(asid_high_bits_of base := None)\\)" + \ (\x\set [0.e.2 ^ asid_low_bits - 1]. x64_asid_map (arch_state s) (base + x) = None) + \ tab = x64_asid_table (arch_state s) + \ invs (s\arch_state := arch_state s\x64_asid_table := tab(asid_high_bits_of base := None)\\)" apply (clarsimp simp: invs_def valid_state_def valid_arch_caps_def) apply (strengthen valid_asid_map_unmap valid_arch_objs_unmap_strg valid_vs_lookup_unmap_strg valid_arch_state_unmap_strg) @@ -90,33 +94,25 @@ lemma delete_asid_pool_invs[wp]: delete_asid_pool base pptr \\rv. invs\" apply (simp add: delete_asid_pool_def) - apply wp - apply (strengthen invs_arm_asid_table_unmap) - apply simp - apply (rule hoare_vcg_conj_lift, - (rule mapM_invalidate[where ptr=pptr])?, - ((wp mapM_wp' | simp add: if_apply_def2)+)[1])+ - apply wp - apply (clarsimp simp: is_aligned_mask[symmetric]) - apply (rule conjI) - apply (rule vs_lookupI) - apply (erule vs_asid_refsI) - apply simp + apply_trace wp + apply (clarsimp simp: if_apply_def2 invs_x64_asid_table_unmap[rule_format]) + thm invs_x64_asid_table_unmap[rule_format, simplified] + apply (rule invs_x64_asid_table_unmap[rule_format]) apply clarsimp - done + sorry lemma delete_asid_invs[wp]: "\invs and K (asid \ mask asid_bits)\ delete_asid asid pd \\rv. invs\" apply (simp add: delete_asid_def cong: option.case_cong) - apply (wp set_asid_pool_invs_unmap | wpc)+ - apply (simp add: invalidate_asid_entry_def invalidate_asid_def invalidate_hw_asid_entry_def) + apply_trace (wp set_asid_pool_invs_unmap hoare_vcg_all_lift dmo_wp | wpc | simp | wp_once )+ + apply (simp add:) apply (wp load_hw_asid_wp) apply (simp add: flush_space_def) apply (wp load_hw_asid_wp|wpc)+ apply (clarsimp simp del: fun_upd_apply) - apply (subgoal_tac "valid_asid_table (arm_asid_table (arch_state s)) s") + apply (subgoal_tac "valid_asid_table (x64_asid_table (arch_state s)) s") prefer 2 apply fastforce apply (clarsimp simp: valid_asid_table_def) @@ -433,7 +429,7 @@ lemma arch_finalise_cap_replaceable[wp]: "\\s. s \ cap.ArchObjectCap cap \ x = is_final_cap' (cap.ArchObjectCap cap) s \ pspace_aligned s \ valid_arch_objs s \ valid_objs s \ - valid_asid_table (arm_asid_table (arch_state s)) s\ + valid_asid_table (x64_asid_table (arch_state s)) s\ arch_finalise_cap cap x \\rv s. replaceable s sl rv (cap.ArchObjectCap cap)\" apply (simp add: arch_finalise_cap_def) @@ -589,7 +585,7 @@ context Arch begin global_naming X64 lemma fast_finalise_replaceable[wp]: "\\s. s \ cap \ x = is_final_cap' cap s - \ cte_wp_at (op = cap) sl s \ valid_asid_table (arm_asid_table (arch_state s)) s + \ cte_wp_at (op = cap) sl s \ valid_asid_table (x64_asid_table (arch_state s)) s \ valid_mdb s \ valid_objs s \ sym_refs (state_refs_of s)\ fast_finalise cap x \\rv s. cte_wp_at (replaceable s sl cap.NullCap) sl s\" @@ -1200,7 +1196,7 @@ lemma replaceable_reset_pd_strg: lemma arch_finalise_case_no_lookup: "\pspace_aligned and valid_arch_objs and valid_objs and - valid_cap (cap.ArchObjectCap acap) and (\s. valid_asid_table (arm_asid_table (arch_state s)) s) + valid_cap (cap.ArchObjectCap acap) and (\s. valid_asid_table (x64_asid_table (arch_state s)) s) and K (aobj_ref acap = Some w \ is_final)\ arch_finalise_cap acap is_final \\rv s. (\vs. vs_cap_ref (cap.ArchObjectCap acap) = Some vs \ \ (vs \ w) s)\" @@ -1274,7 +1270,7 @@ crunch valid_cap: invalidate_tlb_by_asid "valid_cap cap" crunch inv: page_table_mapped "P" crunch valid_objs[wp]: invalidate_tlb_by_asid "valid_objs" crunch valid_asid_table[wp]: do_machine_op - "\s. valid_asid_table (arm_asid_table (arch_state s)) s" + "\s. valid_asid_table (x64_asid_table (arch_state s)) s" lemma mapM_x_swp_store_invalid_pte_invs: "\invs and (\s. \slot. cte_wp_at @@ -1639,8 +1635,8 @@ lemma set_asid_pool_obj_at_ptr: lemma valid_arch_state_table_strg: "valid_arch_state s \ asid_pool_at p s \ - Some p \ arm_asid_table (arch_state s) ` (dom (arm_asid_table (arch_state s)) - {x}) \ - valid_arch_state (s\arch_state := arch_state s\arm_asid_table := arm_asid_table (arch_state s)(x \ p)\\)" + Some p \ x64_asid_table (arch_state s) ` (dom (x64_asid_table (arch_state s)) - {x}) \ + valid_arch_state (s\arch_state := arch_state s\x64_asid_table := x64_asid_table (arch_state s)(x \ p)\\)" apply (clarsimp simp: valid_arch_state_def valid_asid_table_def ran_def) apply (rule conjI, fastforce) apply (erule inj_on_fun_upd_strongerI) @@ -1648,15 +1644,15 @@ lemma valid_arch_state_table_strg: done lemma valid_table_caps_table [simp]: - "valid_table_caps (s\arch_state := arch_state s\arm_asid_table := arm_asid_table'\\) = valid_table_caps s" + "valid_table_caps (s\arch_state := arch_state s\x64_asid_table := x64_asid_table'\\) = valid_table_caps s" by (simp add: valid_table_caps_def) lemma valid_global_objs_table [simp]: - "valid_global_objs (s\arch_state := arch_state s\arm_asid_table := arm_asid_table'\\) = valid_global_objs s" + "valid_global_objs (s\arch_state := arch_state s\x64_asid_table := x64_asid_table'\\) = valid_global_objs s" by (simp add: valid_global_objs_def) lemma valid_kernel_mappings [iff]: - "valid_kernel_mappings (s\arch_state := arch_state s\arm_asid_table := arm_asid_table'\\) = valid_kernel_mappings s" + "valid_kernel_mappings (s\arch_state := arch_state s\x64_asid_table := x64_asid_table'\\) = valid_kernel_mappings s" by (simp add: valid_kernel_mappings_def) lemma vs_asid_refs_updateD: @@ -1674,7 +1670,7 @@ lemma vs_lookup1_arch [simp]: lemma vs_lookup_empty_table: "(rs \ q) (s\kheap := kheap s(p \ ArchObj (ASIDPool empty)), - arch_state := arch_state s\arm_asid_table := arm_asid_table (arch_state s)(x \ p)\\) \ + arch_state := arch_state s\x64_asid_table := x64_asid_table (arch_state s)(x \ p)\\) \ (rs \ q) s \ (rs = [VSRef (ucast x) None] \ q = p)" apply (erule vs_lookupE) apply clarsimp @@ -1707,7 +1703,7 @@ lemma vs_lookup_empty_table: lemma vs_lookup_pages_empty_table: "(rs \ q) (s\kheap := kheap s(p \ ArchObj (ASIDPool empty)), - arch_state := arch_state s\arm_asid_table := arm_asid_table (arch_state s)(x \ p)\\) \ + arch_state := arch_state s\x64_asid_table := x64_asid_table (arch_state s)(x \ p)\\) \ (rs \ q) s \ (rs = [VSRef (ucast x) None] \ q = p)" apply (subst (asm) vs_lookup_pages_def) apply (clarsimp simp: Image_def) @@ -1741,8 +1737,8 @@ lemma set_asid_pool_empty_table_objs: "\valid_arch_objs and asid_pool_at p\ set_asid_pool p empty \\rv s. valid_arch_objs - (s\arch_state := arch_state s\arm_asid_table := - arm_asid_table (arch_state s)(asid_high_bits_of word2 \ p)\\)\" + (s\arch_state := arch_state s\x64_asid_table := + x64_asid_table (arch_state s)(asid_high_bits_of word2 \ p)\\)\" apply (simp add: set_asid_pool_def set_object_def) apply (wp get_object_wp) apply (clarsimp simp: obj_at_def valid_arch_objs_def @@ -1766,8 +1762,8 @@ lemma set_asid_pool_empty_table_lookup: (\s. \p'. caps_of_state s p' = Some (ArchObjectCap (ASIDPoolCap p base)))\ set_asid_pool p empty \\rv s. valid_vs_lookup - (s\arch_state := arch_state s\arm_asid_table := - arm_asid_table (arch_state s)(asid_high_bits_of base \ p)\\)\" + (s\arch_state := arch_state s\x64_asid_table := + x64_asid_table (arch_state s)(asid_high_bits_of base \ p)\\)\" apply (simp add: set_asid_pool_def set_object_def) apply (wp get_object_wp) apply (clarsimp simp: obj_at_def valid_vs_lookup_def @@ -1788,8 +1784,8 @@ lemma set_asid_pool_empty_valid_asid_map: \ (\asid'. \ ([VSRef asid' None] \ p) s) \ (\p'. \ ([VSRef (ucast (asid_high_bits_of base)) None] \ p') s)\ set_asid_pool p empty - \\rv s. valid_asid_map (s\arch_state := arch_state s\arm_asid_table := - arm_asid_table (arch_state s)(asid_high_bits_of base \ p)\\)\" + \\rv s. valid_asid_map (s\arch_state := arch_state s\x64_asid_table := + x64_asid_table (arch_state s)(asid_high_bits_of base \ p)\\)\" apply (simp add: set_asid_pool_def set_object_def) apply (wp get_object_wp) apply (clarsimp simp: valid_asid_map_def vspace_at_asid_def @@ -1820,8 +1816,8 @@ lemma set_asid_pool_invs_table: \ (\ ([VSRef (ucast (asid_high_bits_of base)) None] \ p) s) \ (\p'. \ ([VSRef (ucast (asid_high_bits_of base)) None] \ p') s)\ set_asid_pool p empty - \\x s. invs (s\arch_state := arch_state s\arm_asid_table := - arm_asid_table (arch_state s)(asid_high_bits_of base \ p)\\)\" + \\x s. invs (s\arch_state := arch_state s\x64_asid_table := + x64_asid_table (arch_state s)(asid_high_bits_of base \ p)\\)\" apply (simp add: invs_def valid_state_def valid_pspace_def valid_arch_caps_def) apply (rule hoare_pre) apply (wp valid_irq_node_typ set_asid_pool_typ_at @@ -1857,7 +1853,7 @@ lemma delete_asid_pool_unmapped2: apply (wp delete_asid_pool_unmapped) apply (simp add: delete_asid_pool_def) apply wp - apply (rule_tac Q="\rv s. ?Q s \ asid_table = arm_asid_table (arch_state s)" + apply (rule_tac Q="\rv s. ?Q s \ asid_table = x64_asid_table (arch_state s)" in hoare_post_imp) apply (clarsimp simp: fun_upd_def[symmetric]) apply (drule vs_lookup_clear_asid_table[rule_format]) diff --git a/proof/invariant-abstract/X64/ArchIpc_AI.thy b/proof/invariant-abstract/X64/ArchIpc_AI.thy index aecd2aba4..a6f5fdc89 100644 --- a/proof/invariant-abstract/X64/ArchIpc_AI.thy +++ b/proof/invariant-abstract/X64/ArchIpc_AI.thy @@ -20,35 +20,42 @@ lemma update_cap_data_closedform: "update_cap_data pres w cap = (case cap of EndpointCap r badge rights \ - if badge = 0 \ \ pres then (EndpointCap r (w && mask 28) rights) else NullCap + if badge = 0 \ \ pres then (EndpointCap r (w && mask badge_bits) rights) else NullCap | NotificationCap r badge rights \ - if badge = 0 \ \ pres then (NotificationCap r (w && mask 28) rights) else NullCap + if badge = 0 \ \ pres then (NotificationCap r (w && mask badge_bits) rights) else NullCap | CNodeCap r bits guard \ - if word_bits < unat ((w >> 3) && mask 5) + bits + if word_bits < unat ((w >> cnode_padding_bits) && mask cnode_guard_size_bits) + bits then NullCap - else CNodeCap r bits ((\g''. drop (size g'' - unat ((w >> 3) && mask 5)) (to_bl g'')) ((w >> 8) && mask 18)) + else CNodeCap r bits ((\g''. drop (size g'' - unat ((w >> cnode_padding_bits) && mask cnode_guard_size_bits)) (to_bl g'')) ((w >> 8) && mask 18)) | ThreadCap r \ ThreadCap r | DomainCap \ DomainCap - | UntypedCap p n idx \ UntypedCap p n idx + | UntypedCap d p n idx \ UntypedCap d p n idx | NullCap \ NullCap | ReplyCap t m \ ReplyCap t m | IRQControlCap \ IRQControlCap | IRQHandlerCap irq \ IRQHandlerCap irq | Zombie r b n \ Zombie r b n - | ArchObjectCap cap \ ArchObjectCap cap)" + | ArchObjectCap cap \ + let fst = ucast w; + lst = ucast (w >> 16) + in case cap of IOPortCap old_fst old_lst \ + if (fst \ lst \ fst \ old_fst \ lst \ old_lst) + then ArchObjectCap (IOPortCap fst lst) + else NullCap + | _ \ ArchObjectCap cap)" apply (cases cap, simp_all only: cap.simps update_cap_data_def is_ep_cap.simps if_False if_True is_ntfn_cap.simps is_cnode_cap.simps is_arch_cap_def word_size cap_ep_badge.simps badge_update_def o_def cap_rights_update_def simp_thms cap_rights.simps Let_def split_def the_cnode_cap_def fst_conv snd_conv fun_app_def the_arch_cap_def - arch_update_cap_data_def + arch_update_cap_data_def cnode_padding_bits_def cnode_guard_size_bits_def cong: if_cong) - apply auto + apply (auto simp: cnode_padding_bits_def cnode_guard_size_bits_def) done lemma cap_asid_PageCap_None [simp]: - "cap_asid (ArchObjectCap (PageCap r R pgsz None)) = None" + "cap_asid (ArchObjectCap (PageCap d r R typ pgsz None)) = None" by (simp add: cap_asid_def) lemma arch_derive_cap_is_derived: @@ -190,7 +197,7 @@ lemma obj_refs_remove_rights[simp, Ipc_AI_assms]: lemma storeWord_um_inv: "\\s. underlying_memory s = um\ storeWord a v - \\_ s. is_aligned a 2 \ x \ {a,a+1,a+2,a+3} \ underlying_memory s x = um x\" + \\_ s. is_aligned a 3 \ x \ {a,a+1,a+2,a+3,a+4,a+5,a+6,a+7} \ underlying_memory s x = um x\" apply (simp add: storeWord_def is_aligned_mask) apply wp apply simp @@ -200,17 +207,17 @@ lemma store_word_offs_vms[wp, Ipc_AI_assms]: "\valid_machine_state\ store_word_offs ptr offs v \\_. valid_machine_state\" proof - have aligned_offset_ignore: - "\(l::word32) (p::word32) sz. l<4 \ p && mask 2 = 0 \ + "\(l::machine_word) (p::machine_word) sz. l p && mask word_size_bits = 0 \ p+l && ~~ mask (pageBitsForSize sz) = p && ~~ mask (pageBitsForSize sz)" proof - fix l p sz - assume al: "(p::word32) && mask 2 = 0" - assume "(l::word32) < 4" hence less: "l<2^2" by simp - have le: "2 \ pageBitsForSize sz" by (case_tac sz, simp_all) + assume al: "(p::machine_word) && mask word_size_bits = 0" + assume "(l::machine_word) < word_size" hence less: "l<2^word_size_bits" by (simp add: word_size_bits_def word_size_def) + have le: "word_size_bits \ pageBitsForSize sz" by (case_tac sz, simp_all add: bit_simps) show "?thesis l p sz" by (rule is_aligned_add_helper[simplified is_aligned_mask, THEN conjunct2, THEN mask_out_first_mask_some, - where n=2, OF al less le]) + where n=word_size_bits, OF al less le]) qed show ?thesis @@ -227,23 +234,23 @@ proof - apply (erule disjE, simp) apply (simp add: in_user_frame_def word_size_def) apply (erule exEI) - apply (subgoal_tac "(ptr + of_nat offs * 4) && ~~ mask (pageBitsForSize x) = - p && ~~ mask (pageBitsForSize x)", simp) - apply (simp only: is_aligned_mask[of _ 2]) - apply (elim disjE, simp_all) - apply (rule aligned_offset_ignore[symmetric], simp+)+ + apply (subgoal_tac "(ptr + of_nat offs * word_size) && ~~ mask (pageBitsForSize x) = + p && ~~ mask (pageBitsForSize x)", simp add: word_size_def) + apply (simp only: is_aligned_mask[of _ word_size_bits, simplified word_size_bits_def]) + apply (elim disjE, simp_all add: word_size_def) + apply (rule aligned_offset_ignore[symmetric, simplified word_size_bits_def word_size_def], simp+)+ done qed lemma is_zombie_update_cap_data[simp, Ipc_AI_assms]: "is_zombie (update_cap_data P data cap) = is_zombie cap" - by (simp add: update_cap_data_closedform is_zombie_def - split: cap.splits) + by (clarsimp simp: update_cap_data_closedform is_zombie_def Let_def + split: cap.splits arch_cap.splits) lemma valid_msg_length_strengthen [Ipc_AI_assms]: "valid_message_info mi \ unat (mi_length mi) \ msg_max_length" apply (clarsimp simp: valid_message_info_def) - apply (subgoal_tac "unat (mi_length mi) \ unat (of_nat msg_max_length :: word32)") + apply (subgoal_tac "unat (mi_length mi) \ unat (of_nat msg_max_length :: machine_word)") apply (clarsimp simp: unat_of_nat msg_max_length_def) apply (clarsimp simp: un_ui_le word_le_def) done @@ -271,18 +278,22 @@ lemma lookup_ipc_buffer_in_user_frame[wp, Ipc_AI_assms]: \case_option (\_. True) in_user_frame\" apply (simp add: lookup_ipc_buffer_def) apply (wp get_cap_wp thread_get_wp | wpc | simp)+ - apply (clarsimp simp add: obj_at_def is_tcb) - apply (subgoal_tac "in_user_frame (xa + (tcb_ipc_buffer tcb && - mask (pageBitsForSize xc))) s", simp) - apply (drule (1) cte_wp_valid_cap) + apply (clarsimp simp add: obj_at_def is_tcb split: split_if_asm) + apply (rename_tac dev p R tp sz m) + apply (subgoal_tac "in_user_frame (p + (tcb_ipc_buffer tcb && + mask (pageBitsForSize sz))) s", simp) + apply (frule (1) cte_wp_valid_cap) apply (clarsimp simp add: valid_cap_def cap_aligned_def in_user_frame_def) apply (thin_tac "case_option a b c" for a b c) - apply (rule_tac x=xc in exI) - apply (subgoal_tac "(xa + (tcb_ipc_buffer tcb && mask (pageBitsForSize xc)) && - ~~ mask (pageBitsForSize xc)) = xa", simp) - apply (rule is_aligned_add_helper[THEN conjunct2], assumption) - apply (rule and_mask_less') - apply (case_tac xc, simp_all) + apply (rule_tac x=sz in exI) + apply (subst is_aligned_add_helper[THEN conjunct2]) + apply simp + apply (simp add: and_mask_less' word_bits_def) + apply (clarsimp simp: caps_of_state_cteD'[where P="\x. True", simplified, symmetric]) + apply (drule (1) CSpace_AI.tcb_cap_slot_regular) + apply simp + apply (simp add: is_nondevice_page_cap_def case_bool_If + split: if_splits) done lemma transfer_caps_loop_cte_wp_at: @@ -302,13 +313,12 @@ lemma transfer_caps_loop_cte_wp_at: | assumption | simp split del: split_if)+ apply (wp hoare_vcg_conj_lift cap_insert_weak_cte_wp_at2) apply (erule imp) - apply (wp hoare_vcg_ball_lift + by (wp hoare_vcg_ball_lift | clarsimp simp: is_cap_simps split del:split_if | unfold derive_cap_def arch_derive_cap_def | wpc | rule conjI | case_tac slots)+ - done lemma transfer_caps_tcb_caps: fixes P t ref mi caps ep receiver recv_buf diff --git a/spec/abstract/X64/ArchCSpace_A.thy b/spec/abstract/X64/ArchCSpace_A.thy index 599898b63..4cf4888b3 100644 --- a/spec/abstract/X64/ArchCSpace_A.thy +++ b/spec/abstract/X64/ArchCSpace_A.thy @@ -21,16 +21,22 @@ begin context Arch begin global_naming X64_A +definition cnode_guard_size_bits :: "nat" +where + "cnode_guard_size_bits \ 6" + +definition cnode_padding_bits :: "nat" +where + "cnode_padding_bits \ 2" + text {* On a user request to modify a cnode capability, extract new guard bits and guard. *} definition update_cnode_cap_data :: "data \ nat \ data" where "update_cnode_cap_data w \ let - pad_bits = 2; guard_bits = 18; - guard_size_bits = 6; - guard_size' = unat ((w >> pad_bits) && mask guard_size_bits); - guard'' = (w >> (pad_bits + guard_size_bits)) && mask guard_bits + guard_size' = unat ((w >> cnode_padding_bits) && mask cnode_guard_size_bits); + guard'' = (w >> (cnode_padding_bits + cnode_guard_size_bits)) && mask guard_bits in (guard_size', guard'')" text {* For some purposes capabilities to physical objects are treated diff --git a/spec/abstract/X64/ArchVSpace_A.thy b/spec/abstract/X64/ArchVSpace_A.thy index 85dd9ff47..cdcd23ca2 100644 --- a/spec/abstract/X64/ArchVSpace_A.thy +++ b/spec/abstract/X64/ArchVSpace_A.thy @@ -378,15 +378,15 @@ where *) | IOPortCap _ _ \ returnOk c" -(* FIXME: update when IOSpace comes through *) +(* FIXME: update when IOSpace comes through, first/last ports may be wrong order *) text {* No user-modifiable data is stored in x64-specific capabilities. *} definition arch_update_cap_data :: "data \ arch_cap \ cap" where "arch_update_cap_data data c \ case c of IOPortCap first_port_old last_port_old \ - let first_port = undefined data; (* ioPortGetFirstPort *) - last_port = undefined data (* ioPortGetLastPort *) in + let first_port = (ucast data ); (* ioPortGetFirstPort *) + last_port = (ucast (data >> 16)) (* ioPortGetLastPort *) in if (first_port \ last_port \ first_port \ first_port_old \ last_port \ last_port_old) then ArchObjectCap $ IOPortCap first_port last_port else NullCap diff --git a/spec/abstract/X64/Arch_A.thy b/spec/abstract/X64/Arch_A.thy index 94b883e7b..0cea9af36 100644 --- a/spec/abstract/X64/Arch_A.thy +++ b/spec/abstract/X64/Arch_A.thy @@ -133,13 +133,6 @@ where return (pd \ InvalidPDE) od" -definition - set_message_info :: "obj_ref \ message_info \ (unit,'z::state_ext) s_monad" -where - "set_message_info thread info \ - as_user thread $ set_register msg_info_register $ - message_info_to_data info" - text {* The Page capability confers the authority to map, unmap and flush the memory page. The remap system call is a convenience operation that ensures the page is mapped in the same location as this cap was previously used to map it diff --git a/spec/abstract/X64/Arch_Structs_A.thy b/spec/abstract/X64/Arch_Structs_A.thy index eb77221e0..3581458e5 100644 --- a/spec/abstract/X64/Arch_Structs_A.thy +++ b/spec/abstract/X64/Arch_Structs_A.thy @@ -364,5 +364,10 @@ where | PDPointerTable pdpt \ APDPointerTable | PageMapL4 pm \ APageMapL4)" +text {* For implementation reasons the badge word has differing amounts of bits *} +definition + badge_bits :: nat where + "badge_bits \ 64" + end end From a7741ca35054b97700efdbf51da18c7c9640f367 Mon Sep 17 00:00:00 2001 From: Joel Beeren Date: Wed, 14 Dec 2016 16:32:58 +1100 Subject: [PATCH 06/10] AInvs: generify Tcb_AI --- proof/invariant-abstract/Tcb_AI.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proof/invariant-abstract/Tcb_AI.thy b/proof/invariant-abstract/Tcb_AI.thy index 5108dbe46..2d0b7f79e 100644 --- a/proof/invariant-abstract/Tcb_AI.thy +++ b/proof/invariant-abstract/Tcb_AI.thy @@ -1054,7 +1054,7 @@ where primrec - thread_control_target :: "tcb_invocation \ word32" + thread_control_target :: "tcb_invocation \ machine_word" where "thread_control_target (tcb_invocation.ThreadControl a b c d e f g h) = a" From b5156791a06ccf99a067ee7ad693eae0a059dc6b Mon Sep 17 00:00:00 2001 From: Joel Beeren Date: Wed, 14 Dec 2016 16:33:12 +1100 Subject: [PATCH 07/10] x64: fixup ArchTcb_AI --- .../X64/ArchCNodeInv_AI.thy | 2 +- proof/invariant-abstract/X64/ArchTcb_AI.thy | 64 +++++++++++-------- 2 files changed, 38 insertions(+), 28 deletions(-) diff --git a/proof/invariant-abstract/X64/ArchCNodeInv_AI.thy b/proof/invariant-abstract/X64/ArchCNodeInv_AI.thy index 9835869a9..8fd769564 100644 --- a/proof/invariant-abstract/X64/ArchCNodeInv_AI.thy +++ b/proof/invariant-abstract/X64/ArchCNodeInv_AI.thy @@ -112,7 +112,7 @@ lemma same_object_as_def2: \ \ cp = NullCap \ \ is_untyped_cap cp \ \ is_zombie cp \ (is_arch_cap cp \ - (case the_arch_cap cp of PageCap x rs sz v + (case the_arch_cap cp of PageCap d x rs tp sz v \ x \ x + 2 ^ pageBitsForSize sz - 1 | _ \ True)))" apply (simp add: same_object_as_def is_cap_simps split: cap.split) diff --git a/proof/invariant-abstract/X64/ArchTcb_AI.thy b/proof/invariant-abstract/X64/ArchTcb_AI.thy index 08338916e..d7ce6023f 100644 --- a/proof/invariant-abstract/X64/ArchTcb_AI.thy +++ b/proof/invariant-abstract/X64/ArchTcb_AI.thy @@ -57,23 +57,27 @@ where is_cnode_cap cap \ (is_arch_cap cap \ (is_pt_cap cap \ cap_asid cap \ None) - \ (is_pd_cap cap \ cap_asid cap \ None))" + \ (is_pd_cap cap \ cap_asid cap \ None) + \ (is_pdpt_cap cap \ cap_asid cap \ None) + \ (is_pml4_cap cap \ cap_asid cap \ None))" definition (* arch specific *) - "pt_pd_asid cap \ case cap of + "vspace_asid cap \ case cap of ArchObjectCap (PageTableCap _ (Some (asid, _))) \ Some asid - | ArchObjectCap (PageDirectoryCap _ (Some asid)) \ Some asid + | ArchObjectCap (PageDirectoryCap _ (Some (asid, _))) \ Some asid + | ArchObjectCap (PDPointerTableCap _ (Some (asid, _))) \ Some asid + | ArchObjectCap (PML4Cap _ (Some asid)) \ Some asid | _ \ None" -lemmas pt_pd_asid_simps [simp] = (* arch specific *) - pt_pd_asid_def [split_simps cap.split arch_cap.split option.split prod.split] +lemmas vspace_asid_simps [simp] = (* arch specific *) + vspace_asid_def [split_simps cap.split arch_cap.split option.split prod.split] lemma checked_insert_is_derived: (* arch specific *) "\ same_object_as new_cap old_cap; is_cnode_or_valid_arch new_cap; obj_refs new_cap = obj_refs old_cap \ table_cap_ref old_cap = table_cap_ref new_cap - \ pt_pd_asid old_cap = pt_pd_asid new_cap\ + \ vspace_asid old_cap = vspace_asid new_cap\ \ is_derived m slot new_cap old_cap" apply (cases slot) apply (frule same_object_as_cap_master) @@ -82,17 +86,18 @@ lemma checked_insert_is_derived: (* arch specific *) apply (frule same_master_cap_same_types) apply (simp add: is_derived_def) apply clarsimp - apply (auto simp: is_cap_simps cap_master_cap_def + by (auto simp: is_cap_simps cap_master_cap_def is_cnode_or_valid_arch_def vs_cap_ref_def - table_cap_ref_def pt_pd_asid_def up_ucast_inj_eq + table_cap_ref_def vspace_asid_def up_ucast_inj_eq split: cap.split_asm arch_cap.split_asm option.split_asm)[1] - done lemma is_cnode_or_valid_arch_cap_asid: (* arch specific *) "is_cnode_or_valid_arch cap \ (is_pt_cap cap \ cap_asid cap \ None) - \ (is_pd_cap cap \ cap_asid cap \ None)" + \ (is_pd_cap cap \ cap_asid cap \ None) + \ (is_pdpt_cap cap \ cap_asid cap \ None) + \ (is_pml4_cap cap \ cap_asid cap \ None)" by (auto simp add: is_cnode_or_valid_arch_def is_cap_simps) @@ -100,11 +105,11 @@ lemma checked_insert_tcb_invs[wp]: (* arch specific *) "\invs and cte_wp_at (\c. c = cap.NullCap) (target, ref) and K (is_cnode_or_valid_arch new_cap) and valid_cap new_cap and tcb_cap_valid new_cap (target, ref) - and K (is_pt_cap new_cap \ is_pd_cap new_cap + and K (is_pt_cap new_cap \ is_pd_cap new_cap \ is_pdpt_cap new_cap \ is_pml4_cap new_cap \ cap_asid new_cap \ None) and (cte_wp_at (\c. obj_refs c = obj_refs new_cap \ table_cap_ref c = table_cap_ref new_cap \ - pt_pd_asid c = pt_pd_asid new_cap) src_slot)\ + vspace_asid c = vspace_asid new_cap) src_slot)\ check_cap_at new_cap src_slot (check_cap_at (cap.ThreadCap target) slot (cap_insert new_cap src_slot (target, ref))) \\rv. invs\" @@ -170,15 +175,15 @@ by (unfold_locales; fact Tcb_AI_asms) lemma use_no_cap_to_obj_asid_strg: (* arch specific *) "(cte_at p s \ no_cap_to_obj_dr_emp cap s \ valid_cap cap s \ invs s) \ cte_wp_at (\c. obj_refs c = obj_refs cap - \ table_cap_ref c = table_cap_ref cap \ pt_pd_asid c = pt_pd_asid cap) p s" + \ table_cap_ref c = table_cap_ref cap \ vspace_asid c = vspace_asid cap) p s" apply (clarsimp simp: cte_wp_at_caps_of_state no_cap_to_obj_with_diff_ref_def simp del: split_paired_All) apply (frule caps_of_state_valid_cap, fastforce) apply (erule allE)+ apply (erule (1) impE)+ - apply (simp add: table_cap_ref_def pt_pd_asid_def split: cap.splits arch_cap.splits option.splits prod.splits) - apply (fastforce simp: table_cap_ref_def valid_cap_simps elim!: asid_low_high_bits)+ + apply (simp add: table_cap_ref_def vspace_asid_def split: cap.splits arch_cap.splits option.splits prod.splits) + apply (fastforce simp: table_cap_ref_def valid_cap_simps wellformed_mapdata_def elim!: asid_low_high_bits)+ done lemma cap_delete_no_cap_to_obj_asid[wp, Tcb_AI_asms]: @@ -195,7 +200,6 @@ lemma cap_delete_no_cap_to_obj_asid[wp, Tcb_AI_asms]: | rule obj_ref_none_no_asid)+ done - lemma tc_invs[Tcb_AI_asms]: "\invs and tcb_at a and (case_option \ (valid_cap o fst) e) @@ -207,6 +211,10 @@ lemma tc_invs[Tcb_AI_asms]: and (case_option \ (no_cap_to_obj_dr_emp o fst) e) and (case_option \ (no_cap_to_obj_dr_emp o fst) f) and (case_option \ (case_option \ (no_cap_to_obj_dr_emp o fst) o snd) g) + (* only set prio \ mcp *) + and (\s. case_option True (\pr. mcpriority_tcb_at (\mcp. pr \ mcp) (cur_thread s) s) pr) + (* only set mcp \ prev_mcp *) + and (\s. case_option True (\mcp. mcpriority_tcb_at (\m. mcp \ m) (cur_thread s) s) mcp) and K (case_option True (is_cnode_cap o fst) e) and K (case_option True (is_valid_vtable_root o fst) f) and K (case_option True (\v. case_option True @@ -214,10 +222,10 @@ lemma tc_invs[Tcb_AI_asms]: and is_arch_cap and is_cnode_or_valid_arch) o fst) (snd v)) g) and K (case_option True (\bl. length bl = word_bits) b)\ - invoke_tcb (ThreadControl a sl b pr e f g) + invoke_tcb (ThreadControl a sl b mcp pr e f g) \\rv. invs\" apply (rule hoare_gen_asm)+ - apply (simp add: split_def cong: option.case_cong) + apply (simp add: split_def set_mcpriority_def cong: option.case_cong) apply (rule hoare_vcg_precond_imp) apply wp apply ((simp only: simp_thms @@ -250,12 +258,14 @@ lemma tc_invs[Tcb_AI_asms]: | strengthen use_no_cap_to_obj_asid_strg tcb_cap_always_valid_strg[where p="tcb_cnode_index 0"] tcb_cap_always_valid_strg[where p="tcb_cnode_index (Suc 0)"])+) - apply (clarsimp simp: tcb_at_cte_at_0 tcb_at_cte_at_1[simplified] - is_cap_simps is_valid_vtable_root_def + apply (clarsimp simp: tcb_at_cte_at_0 tcb_at_cte_at_1[simplified] is_nondevice_page_cap_arch_def + is_cap_simps is_valid_vtable_root_def is_nondevice_page_cap_simps is_cnode_or_valid_arch_def tcb_cap_valid_def invs_valid_objs cap_asid_def vs_cap_ref_def - split: option.split_asm - | rule conjI)+ + split: option.split_asm )+ + apply (simp add: case_bool_If valid_ipc_buffer_cap_def is_nondevice_page_cap_simps + is_nondevice_page_cap_arch_def + split: arch_cap.splits if_splits)+ done @@ -265,7 +275,7 @@ lemma check_valid_ipc_buffer_inv: (* arch_specific *) cong: cap.case_cong arch_cap.case_cong split del: split_if) apply (rule hoare_pre) - apply (wp | simp split del: split_if | wpcw)+ + apply (wp | simp add: whenE_def split del: split_if | wpcw)+ done lemma check_valid_ipc_buffer_wp[Tcb_AI_asms]: @@ -279,7 +289,7 @@ lemma check_valid_ipc_buffer_wp[Tcb_AI_asms]: cong: cap.case_cong arch_cap.case_cong split del: split_if) apply (rule hoare_pre) - apply (wp | simp split del: split_if | wpc)+ + apply (wp | simp add: whenE_def split del: split_if | wpc)+ apply (clarsimp simp: is_cap_simps is_cnode_or_valid_arch_def valid_ipc_buffer_cap_def) done @@ -317,9 +327,9 @@ lemma no_cap_to_obj_with_diff_ref_update_cap_data[Tcb_AI_asms]: apply (simp add: no_cap_to_obj_with_diff_ref_def update_cap_objrefs) apply (clarsimp simp: update_cap_data_closedform - table_cap_ref_def + table_cap_ref_def Let_def arch_update_cap_data_def - split: cap.split) + split: cap.split arch_cap.splits) apply simp done @@ -342,7 +352,7 @@ lemma update_cap_valid[Tcb_AI_asms]: apply (simp add: word_bits_def) apply (rename_tac arch_cap) using valid_validate_vm_rights[simplified valid_vm_rights_def] - apply (case_tac arch_cap, simp_all add: acap_rights_update_def + apply (case_tac arch_cap, simp_all add: acap_rights_update_def Let_def split: option.splits prod.splits) done From 7dce5dd7c4cb8e9f755c3bfe5e7526a7e355bcf2 Mon Sep 17 00:00:00 2001 From: Joel Beeren Date: Thu, 5 Jan 2017 15:38:06 +1100 Subject: [PATCH 08/10] x64: defined a bunch of machine ops that were previously unspecified --- spec/abstract/X64/ArchDecode_A.thy | 14 +++-- spec/abstract/X64/Arch_A.thy | 8 +-- spec/machine/X64/MachineOps.thy | 91 +++++++++++++++++++++--------- 3 files changed, 76 insertions(+), 37 deletions(-) diff --git a/spec/abstract/X64/ArchDecode_A.thy b/spec/abstract/X64/ArchDecode_A.thy index 777527e94..fb1592fee 100644 --- a/spec/abstract/X64/ArchDecode_A.thy +++ b/spec/abstract/X64/ArchDecode_A.thy @@ -171,7 +171,8 @@ where ensure_port_operation_allowed cap port 1; output_data \ returnOk $ ucast $ args ! 1; returnOk $ InvokeIOPort $ IOPortInvocation port $ IOPortOut32 output_data - odE" + odE + | _ \ throwError IllegalOperation" (*X64STUB*) definition decode_io_unmap_invocation :: "data \ data list \ cslot_ptr \ arch_cap \ @@ -350,9 +351,9 @@ where odE else throwError TruncatedMessage else if invocation_type label = ArchInvocationLabel X64PageUnmap then - case map_type of + (*case map_type of VMIOSpaceMap \ decode_io_unmap_invocation label args cte cap extra_caps - | _ \ returnOk $ InvokePage $ PageUnmap cap cte + | _ \*) returnOk $ InvokePage $ PageUnmap cap cte (* FIXME x64-vtd: else if invocation_type label = ArchInvocationLabel X64PageMapIO then decode_io_map_invocation label args cte cap extra_caps @@ -475,7 +476,7 @@ where else throwError IllegalOperation | ASIDControlCap \ - if invocation_type label = ArchInvocationLabel X64ASIDPoolAssign then + if invocation_type label = ArchInvocationLabel X64ASIDControlMakePool then if length args > 1 \ length extra_caps > 1 then let index = args ! 0; depth = args ! 1; @@ -497,7 +498,7 @@ where else throwError $ InvalidCapability 1); dest_slot \ lookup_target_slot root (to_bl index) (unat depth); ensure_empty dest_slot; - returnOk $ InvokeASIDControl $ MakePool undefined undefined parent_slot base + returnOk $ InvokeASIDControl $ MakePool frame dest_slot parent_slot base odE else throwError TruncatedMessage else throwError IllegalOperation @@ -517,8 +518,9 @@ where (- dom pool \ {x. x \ 2 ^ asid_low_bits - 1 \ ucast x + base \ 0}); whenE (free_set = {}) $ throwError DeleteFirst; offset \ liftE $ select_ext (\_. free_asid_pool_select pool base) free_set; - returnOk $ InvokeASIDPool $ Assign undefined undefined pd_cap_slot + returnOk $ InvokeASIDPool $ Assign (ucast offset + base) p pd_cap_slot odE + | _ \ throwError $ InvalidCapability 1 else throwError TruncatedMessage else throwError IllegalOperation diff --git a/spec/abstract/X64/Arch_A.thy b/spec/abstract/X64/Arch_A.thy index 0cea9af36..0fff89754 100644 --- a/spec/abstract/X64/Arch_A.thy +++ b/spec/abstract/X64/Arch_A.thy @@ -27,14 +27,13 @@ definition "arch_invoke_irq_control aic \ (case aic of IssueIRQHandlerIOAPIC irq dest src ioapic pin level polarity vector \ without_preemption (do do_machine_op $ ioapicMapPinToVector ioapic pin level polarity vector; - irq_state \ do_machine_op $ irqStateIRQIOAPICNew ioapic pin level polarity - (1::machine_word) (0::machine_word); + irq_state \ return $ IRQIOAPIC ioapic pin level polarity True; do_machine_op $ updateIRQState irq irq_state; set_irq_state IRQSignal (IRQ irq); cap_insert (IRQHandlerCap (IRQ irq)) dest src od) | IssueIRQHandlerMSI irq dest src bus dev func handle \ without_preemption (do - irq_state \ do_machine_op $ irqStateIRQMSINew bus dev func handle; + irq_state \ return $ IRQMSI bus dev func handle; do_machine_op $ updateIRQState irq irq_state; set_irq_state IRQSignal (IRQ irq); cap_insert (IRQHandlerCap (IRQ irq)) dest src @@ -276,7 +275,8 @@ definition | InvokePage oper \ perform_page_invocation oper | InvokeASIDControl oper \ perform_asid_control_invocation oper | InvokeASIDPool oper \ perform_asid_pool_invocation oper - | InvokeIOPort oper \ perform_io_port_invocation oper; + | InvokeIOPort oper \ perform_io_port_invocation oper + | _ \ fail; return $ [] od" diff --git a/spec/machine/X64/MachineOps.thy b/spec/machine/X64/MachineOps.thy index e6caf767d..f75a31dec 100644 --- a/spec/machine/X64/MachineOps.thy +++ b/spec/machine/X64/MachineOps.thy @@ -250,10 +250,12 @@ definition setCurrentCR3 :: "Platform.X64.cr3 \ unit machine_monad" where "setCurrentCR3 \ undefined" +consts' + mfence_impl :: "unit machine_rest_monad" definition mfence :: "unit machine_monad" where -"mfence \ undefined" +"mfence \ machine_op_lift mfence_impl" consts' invalidateTLBEntry_impl :: "word64 \ unit machine_rest_monad" @@ -277,6 +279,7 @@ definition resetCR3 :: "unit machine_monad" where "resetCR3 \ machine_op_lift resetCR3_impl " +(* FIXME x64: VT-d definition firstValidIODomain :: "word16" where @@ -286,36 +289,44 @@ definition numIODomainIDBits :: "nat" where "numIODomainIDBits \ undefined" +*) +consts' + hwASIDInvalidate_impl :: "word64 \ unit machine_rest_monad" definition hwASIDInvalidate :: "word64 \ unit machine_monad" where -"hwASIDInvalidate asid \ undefined" +"hwASIDInvalidate asid \ machine_op_lift (hwASIDInvalidate_impl asid)" + +consts' + getFaultAddress_val :: "machine_state \ machine_word" definition getFaultAddress :: "word64 machine_monad" where -"getFaultAddress \ undefined" +"getFaultAddress \ gets getFaultAddress_val" +consts' + irqIntOffset_val :: "machine_state \ machine_word" definition irqIntOffset :: "machine_word" where -"irqIntOffset \ undefined" +"irqIntOffset \ 0x20" definition maxPCIBus :: "machine_word" where -"maxPCIBus \ undefined" +"maxPCIBus \ 0xFF" definition maxPCIDev :: "machine_word" where -"maxPCIDev \ undefined" +"maxPCIDev \ 31" definition maxPCIFunc :: "machine_word" where -"maxPCIFunc \ undefined" +"maxPCIFunc \ 7" definition numIOAPICs :: "machine_word" @@ -325,26 +336,38 @@ where definition ioapicIRQLines :: "machine_word" where -"ioapicIRQLines \ undefined" +"ioapicIRQLines \ error []" +(* FIXME x64: technically this is defined in c and should be here *) +consts' + ioapicMapPinToVector_impl :: "machine_word \ machine_word \ machine_word \ machine_word \ machine_word \ unit machine_rest_monad" definition ioapicMapPinToVector :: "machine_word \ machine_word \ machine_word \ machine_word \ machine_word \ unit machine_monad" where -"ioapicMapPinToVector ioapic pin level polarity vector \ undefined" +"ioapicMapPinToVector ioapic pin level polarity vector \ machine_op_lift (ioapicMapPinToVector_impl ioapic pin level polarity vector)" +datatype X64IRQState = + IRQFree + | IRQReserved + | IRQMSI + (MSIBus : machine_word) + (MSIDev : machine_word) + (MSIFunc : machine_word) + (MSIHandle : machine_word) + | IRQIOAPIC + (IRQioapic : machine_word) + (IRQPin : machine_word) + (IRQLevel : machine_word) + (IRQPolarity : machine_word) + (IRQMasked : bool) + + +consts' + updateIRQState_impl :: "irq \ X64IRQState \ unit machine_rest_monad" definition -"irqStateIRQIOAPICNew \ error []" - -definition -"irqStateIRQMSINew \ error []" - -datatype x64irqstate = - X64IRQState - -definition -updateIRQState :: "irq \ x64irqstate \ unit machine_monad" +updateIRQState :: "irq \ X64IRQState \ unit machine_monad" where -"updateIRQState arg1 arg2 \ error []" +"updateIRQState arg1 arg2 \ machine_op_lift (updateIRQState_impl arg1 arg2)" (*FIXME: How to deal with this directly? *) definition @@ -353,36 +376,50 @@ where "IRQ \ id" (* FIXME x64: More underspecified operations *) - +consts' + in8_impl :: "word16 \ unit machine_rest_monad" + in8_val :: "machine_state \ machine_word" definition in8 :: "word16 \ machine_word machine_monad" where -"in8 \ error []" +"in8 port \ do machine_op_lift $ in8_impl port; gets in8_val od" +consts' + in16_impl :: "word16 \ unit machine_rest_monad" + in16_val :: "machine_state \ machine_word" definition in16 :: "word16 \ machine_word machine_monad" where -"in16 \ error []" +"in16 port \ do machine_op_lift $ in16_impl port; gets in16_val od" +consts' + in32_impl :: "word16 \ unit machine_rest_monad" + in32_val :: "machine_state \ machine_word" definition in32 :: "word16 \ machine_word machine_monad" where -"in32 \ error []" +"in32 port \ do machine_op_lift $ in32_impl port; gets in32_val od" +consts' + out8_impl :: "word16 \ word8 \ unit machine_rest_monad" definition out8 :: "word16 \ word8 \ unit machine_monad" where -"out8 \ error []" +"out8 port dat \ machine_op_lift $ out8_impl port dat" +consts' + out16_impl :: "word16 \ word16 \ unit machine_rest_monad" definition out16 :: "word16 \ word16 \ unit machine_monad" where -"out16 \ error []" +"out16 port dat \ machine_op_lift $ out16_impl port dat" +consts' + out32_impl :: "word16 \ word32 \ unit machine_rest_monad" definition out32 :: "word16 \ word32 \ unit machine_monad" where -"out32 \ error []" +"out32 port dat \ machine_op_lift $ out32_impl port dat" end From 6de4a79059faf0c7d40322d223fd70eb936ebcb1 Mon Sep 17 00:00:00 2001 From: Joel Beeren Date: Thu, 5 Jan 2017 15:38:26 +1100 Subject: [PATCH 09/10] x64: ArchEmptyFail_AI now processes after spec changes --- .../X64/ArchEmptyFail_AI.thy | 72 +++++++++++++------ proof/invariant-abstract/X64/Machine_AI.thy | 55 ++++++++++++++ 2 files changed, 105 insertions(+), 22 deletions(-) diff --git a/proof/invariant-abstract/X64/ArchEmptyFail_AI.thy b/proof/invariant-abstract/X64/ArchEmptyFail_AI.thy index 4d1c4cd79..7f07d2dd5 100644 --- a/proof/invariant-abstract/X64/ArchEmptyFail_AI.thy +++ b/proof/invariant-abstract/X64/ArchEmptyFail_AI.thy @@ -17,13 +17,9 @@ context Arch begin global_naming X64 named_theorems EmptyFail_AI_assms crunch_ignore (empty_fail) - (add: invalidateTLB_ASID_impl invalidateTLB_VAASID_impl cleanByVA_impl - cleanByVA_PoU_impl invalidateByVA_impl 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 - writeTTBR0_impl cacheRangeOp) + (add: setCurrentVSpaceRoot_impl invalidateTLBEntry_impl invalidatePageStructureCache_impl + resetCR3_impl hwASIDInvalidate_impl ioapicMapPinToVector_impl updateIRQState_impl + in8_impl in16_impl in32_impl out8_impl out16_impl out32_impl) crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: loadWord, load_word_offs, storeWord, getRestartPC, get_mrs @@ -42,6 +38,18 @@ crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: handle_fault (simp: kernel_object.splits option.splits arch_cap.splits cap.splits endpoint.splits bool.splits list.splits thread_state.splits split_def catch_def sum.splits Let_def wp: zipWithM_x_empty_fail) + +lemma port_out_empty_fail[simp, intro!]: + assumes ef: "\a. empty_fail (oper a)" + shows "empty_fail (port_out oper w)" + apply (simp add: port_out_def) + by (wp | simp add: ef)+ + +lemma port_in_empty_fail[simp, intro!]: + assumes ef: "empty_fail oper" + shows "empty_fail (port_in oper)" + apply (simp add: port_in_def) + by (wp | simp add: ef)+ crunch (empty_fail) empty_fail[wp]: decode_tcb_configure, decode_bind_notification, decode_unbind_notification (simp: cap.splits arch_cap.splits split_def) @@ -49,31 +57,43 @@ crunch (empty_fail) empty_fail[wp]: decode_tcb_configure, decode_bind_notificati lemma decode_tcb_invocation_empty_fail[wp]: "empty_fail (decode_tcb_invocation a b (ThreadCap p) d e)" by (simp add: decode_tcb_invocation_def split: invocation_label.splits | wp | intro conjI impI)+ + +crunch (empty_fail) empty_fail[wp]: find_vspace_for_asid, check_vp_alignment, + ensure_safe_mapping, get_asid_pool, lookup_pt_slot, + decode_port_invocation + (simp: kernel_object.splits arch_kernel_obj.splits option.splits pde.splits pte.splits + pdpte.splits pml4e.splits vmpage_size.splits) -crunch (empty_fail) empty_fail[wp]: find_pd_for_asid, get_master_pde, check_vp_alignment, - create_mapping_entries, ensure_safe_mapping, get_asid_pool, resolve_vaddr - (simp: kernel_object.splits arch_kernel_obj.splits option.splits pde.splits pte.splits) - +lemma create_mapping_entries_empty_fail[wp]: + "empty_fail (create_mapping_entries a b c d e f)" + by (case_tac c; simp add: create_mapping_entries_def; wp) + lemma arch_decode_X64ASIDControlMakePool_empty_fail: "invocation_type label = ArchInvocationLabel X64ASIDControlMakePool \ empty_fail (arch_decode_invocation label b c d e f)" apply (simp add: arch_decode_invocation_def Let_def) apply (intro impI conjI allI) - apply (simp add: isPageFlushLabel_def isPDFlushLabel_def split: arch_cap.splits)+ - apply (rule impI) + apply (simp split: arch_cap.splits) + apply (intro conjI impI) apply (simp add: split_def) apply wp apply simp apply (subst bindE_assoc[symmetric]) apply (rule empty_fail_bindE) - subgoal by (fastforce simp: empty_fail_def whenE_def throwError_def select_ext_def bindE_def bind_def return_def returnOk_def lift_def liftE_def fail_def gets_def get_def assert_def select_def split: split_if_asm) - by (simp add: Let_def split: cap.splits arch_cap.splits option.splits | wp | intro conjI impI allI)+ + subgoal by (fastforce simp: empty_fail_def whenE_def throwError_def select_ext_def bindE_def bind_def return_def + returnOk_def lift_def liftE_def fail_def gets_def get_def assert_def select_def split: split_if_asm) + apply (simp add: Let_def split: cap.splits arch_cap.splits option.splits bool.splits | wp | intro conjI impI allI)+ + by (clarsimp simp add: decode_page_invocation_def split: arch_cap.splits | wp)+ + lemma arch_decode_X64ASIDPoolAssign_empty_fail: "invocation_type label = ArchInvocationLabel X64ASIDPoolAssign \ empty_fail (arch_decode_invocation label b c d e f)" - apply (simp add: arch_decode_invocation_def split_def Let_def isPageFlushLabel_def isPDFlushLabel_def + apply (simp add: arch_decode_invocation_def Let_def split: arch_cap.splits) + apply (intro impI allI conjI) + apply (simp add: arch_decode_invocation_def split_def Let_def split: arch_cap.splits cap.splits option.splits | intro impI allI)+ + apply clarsimp apply (rule empty_fail_bindE) apply simp apply (rule empty_fail_bindE) @@ -87,7 +107,7 @@ lemma arch_decode_X64ASIDPoolAssign_empty_fail: subgoal by (fastforce simp: empty_fail_def whenE_def throwError_def select_def bindE_def bind_def return_def returnOk_def lift_def liftE_def select_ext_def gets_def get_def assert_def fail_def) - apply wp + apply (clarsimp simp: decode_page_invocation_def | wp)+ done lemma arch_decode_invocation_empty_fail[wp]: @@ -99,7 +119,8 @@ lemma arch_decode_invocation_empty_fail[wp]: apply (find_goal \succeeds \erule arch_decode_X64ASIDControlMakePool_empty_fail\\) apply (find_goal \succeeds \erule arch_decode_X64ASIDPoolAssign_empty_fail\\) apply ((simp add: arch_decode_X64ASIDControlMakePool_empty_fail arch_decode_X64ASIDPoolAssign_empty_fail)+)[2] - by ((simp add: arch_decode_invocation_def Let_def split: arch_cap.splits cap.splits option.splits | wp | intro conjI impI allI)+) + by ((simp add: arch_decode_invocation_def decode_page_invocation_def Let_def + split: arch_cap.splits cap.splits option.splits | wp | intro conjI impI allI)+) end @@ -111,12 +132,19 @@ global_interpretation EmptyFail_AI_derive_cap?: EmptyFail_AI_derive_cap context Arch begin global_naming X64 +lemma flush_table_empty_fail[simp, wp]: "empty_fail (flush_table a b c)" + unfolding flush_table_def + apply simp + apply (wp | wpc)+ + done + crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: maskInterrupt, empty_slot, - setHardwareASID, setCurrentPD, finalise_cap, preemption_point, + finalise_cap, preemption_point, cap_swap_for_delete, decode_invocation (simp: Let_def catch_def split_def OR_choiceE_def mk_ef_def option.splits endpoint.splits notification.splits thread_state.splits sum.splits cap.splits arch_cap.splits - kernel_object.splits vmpage_size.splits pde.splits bool.splits list.splits) + kernel_object.splits vmpage_size.splits pde.splits bool.splits list.splits + forM_x_def empty_fail_mapM_x) crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: setRegister, setNextPC @@ -159,8 +187,8 @@ crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: handle_event, activate_t thread_state.splits endpoint.splits catch_def sum.splits cnode_invocation.splits page_table_invocation.splits page_invocation.splits asid_control_invocation.splits asid_pool_invocation.splits arch_invocation.splits irq_state.splits syscall.splits - flush_type.splits page_directory_invocation.splits - ignore: resetTimer_impl ackInterrupt_impl) + page_directory_invocation.splits + ignore: resetTimer_impl) end global_interpretation EmptyFail_AI_call_kernel_unit?: EmptyFail_AI_call_kernel_unit diff --git a/proof/invariant-abstract/X64/Machine_AI.thy b/proof/invariant-abstract/X64/Machine_AI.thy index 473a5338b..82462134d 100644 --- a/proof/invariant-abstract/X64/Machine_AI.thy +++ b/proof/invariant-abstract/X64/Machine_AI.thy @@ -367,6 +367,61 @@ lemma empty_fail_clearMemory [simp, intro!]: "\a b. empty_fail (clearMemory a b)" by (simp add: clearMemory_def mapM_x_mapM ef_storeWord) +(* FIXME x64: move *) +lemma setCurrentVSpaceRoot_ef[simp,wp]: "empty_fail (setCurrentVSpaceRoot a b)" + by (simp add: setCurrentVSpaceRoot_def) + +lemma getFaultAddress_ef[simp,wp]: "empty_fail getFaultAddress" + by (simp add: getFaultAddress_def) + +(* FIXME x64: move *) +lemma ioapicMapPinToVector_ef[simp,wp]: "empty_fail (ioapicMapPinToVector a b c d e)" + by (simp add: ioapicMapPinToVector_def) + +(* FIXME x64: move *) +lemma invalidateTLBEntry_ef[simp,wp]: "empty_fail (invalidateTLBEntry b)" + by (simp add: invalidateTLBEntry_def) + +(* FIXME x64: move *) +lemma hwASIDInvalidate_ef[simp,wp]: "empty_fail (hwASIDInvalidate b)" + by (simp add: hwASIDInvalidate_def) + +(* FIXME x64: move *) +lemma updateIRQState_ef[simp,wp]: "empty_fail (updateIRQState b c)" + by (simp add: updateIRQState_def) + +(* FIXME x64: move *) +lemma invalidatePageStructureCache_ef[simp,wp]: "empty_fail (invalidatePageStructureCache)" + by (simp add: invalidatePageStructureCache_def) + +(* FIXME x64: move *) +lemma resetCR3_ef[simp,wp]: "empty_fail (resetCR3)" + by (simp add: resetCR3_def) + +(* FIXME x64: move *) +lemma in8_ef[simp,wp]: "empty_fail (in8 port)" + by (simp add: in8_def) + +(* FIXME x64: move *) +lemma in16_ef[simp,wp]: "empty_fail (in16 port)" + by (simp add: in16_def) + +(* FIXME x64: move *) +lemma in32_ef[simp,wp]: "empty_fail (in32 port)" + by (simp add: in32_def) + +(* FIXME x64: move *) +lemma out8_ef[simp,wp]: "empty_fail (out8 port dat)" + by (simp add: out8_def) + +(* FIXME x64: move *) +lemma out16_ef[simp,wp]: "empty_fail (out16 port dat)" + by (simp add: out16_def) + +(* FIXME x64: move *) +lemma out32_ef[simp,wp]: "empty_fail (out32 port dat)" + by (simp add: out32_def) + end end From 47f78b30a6870dd2e00f3c991693749fa57125f6 Mon Sep 17 00:00:00 2001 From: Joel Beeren Date: Mon, 9 Jan 2017 17:12:34 +1100 Subject: [PATCH 10/10] x64: random stuff in BCorres, changed undefined to fail in decode_page_invocation --- proof/invariant-abstract/X64/ArchBCorres2_AI.thy | 8 ++++---- proof/invariant-abstract/X64/ArchInterrupt_AI.thy | 7 +++++-- spec/abstract/X64/ArchDecode_A.thy | 2 +- 3 files changed, 10 insertions(+), 7 deletions(-) diff --git a/proof/invariant-abstract/X64/ArchBCorres2_AI.thy b/proof/invariant-abstract/X64/ArchBCorres2_AI.thy index 065d01d87..0ad68929c 100644 --- a/proof/invariant-abstract/X64/ArchBCorres2_AI.thy +++ b/proof/invariant-abstract/X64/ArchBCorres2_AI.thy @@ -34,7 +34,7 @@ lemma invoke_tcb_bcorres[wp]: fixes a shows "bcorres (invoke_tcb a) (invoke_tcb a)" apply (cases a) - apply (wp | wpc | simp)+ + apply (wp | wpc | simp add: set_mcpriority_def)+ apply (rename_tac option) apply (case_tac option) apply (wp | wpc | simp)+ @@ -53,7 +53,7 @@ lemma transfer_caps_loop_bcorres[wp]: lemma invoke_irq_control_bcorres[wp]: "bcorres (invoke_irq_control a) (invoke_irq_control a)" apply (cases a) - apply (wp | simp add: arch_invoke_irq_control_def)+ + apply (wp | simp add: arch_invoke_irq_control_def | wpc)+ done lemma invoke_irq_handler_bcorres[wp]: "bcorres (invoke_irq_handler a) (invoke_irq_handler a)" @@ -75,7 +75,7 @@ lemma decode_cnode_invocation[wp]: "bcorres (decode_cnode_invocation a b c d) (d apply (wp | wpc | simp add: split_def | intro impI conjI)+ done -crunch (bcorres)bcorres[wp]: decode_set_ipc_buffer,decode_set_space,decode_set_priority,decode_bind_notification,decode_unbind_notification truncate_state +crunch (bcorres)bcorres[wp]: decode_set_ipc_buffer,decode_set_space,decode_set_priority,decode_set_mcpriority,decode_bind_notification,decode_unbind_notification truncate_state lemma decode_tcb_configure_bcorres[wp]: "bcorres (decode_tcb_configure b (cap.ThreadCap c) d e) (decode_tcb_configure b (cap.ThreadCap c) d e)" @@ -111,7 +111,7 @@ lemma handle_event_bcorres[wp]: "bcorres (handle_event e) (handle_event e)" apply (simp add: handle_send_def handle_call_def handle_recv_def handle_reply_def handle_yield_def handle_interrupt_def Let_def | intro impI conjI allI | wp | wpc)+ done -crunch (bcorres)bcorres[wp]: guarded_switch_to,switch_to_idle_thread truncate_state (ignore: storeWord clearExMonitor) +crunch (bcorres)bcorres[wp]: guarded_switch_to,switch_to_idle_thread truncate_state (ignore: storeWord) lemma choose_switch_or_idle: "((), s') \ fst (choose_thread s) \ diff --git a/proof/invariant-abstract/X64/ArchInterrupt_AI.thy b/proof/invariant-abstract/X64/ArchInterrupt_AI.thy index 90cd85b23..951d48721 100644 --- a/proof/invariant-abstract/X64/ArchInterrupt_AI.thy +++ b/proof/invariant-abstract/X64/ArchInterrupt_AI.thy @@ -19,8 +19,9 @@ named_theorems Interrupt_AI_asms lemma (* decode_irq_control_invocation_inv *)[Interrupt_AI_asms]: "\P\ decode_irq_control_invocation label args slot caps \\rv. P\" apply (simp add: decode_irq_control_invocation_def Let_def arch_check_irq_def - arch_decode_irq_control_invocation_def whenE_def, safe) - apply (wp | simp)+ + arch_decode_irq_control_invocation_def whenE_def split del: split_if) + apply (rule hoare_pre) + apply (wp | simp split del: split_if)+ done lemma (* decode_irq_control_valid *)[Interrupt_AI_asms]: @@ -78,6 +79,8 @@ lemma no_cap_to_obj_with_diff_IRQHandler_ARCH[Interrupt_AI_asms]: by (rule ext, simp add: no_cap_to_obj_with_diff_ref_def cte_wp_at_caps_of_state obj_ref_none_no_asid) + +crunch valid_cap: do_machine_op "valid_cap cap" lemma (* set_irq_state_valid_cap *)[Interrupt_AI_asms]: "\valid_cap cap\ set_irq_state IRQSignal irq \\rv. valid_cap cap\" diff --git a/spec/abstract/X64/ArchDecode_A.thy b/spec/abstract/X64/ArchDecode_A.thy index fb1592fee..fb4783e9b 100644 --- a/spec/abstract/X64/ArchDecode_A.thy +++ b/spec/abstract/X64/ArchDecode_A.thy @@ -361,7 +361,7 @@ where else if invocation_type label = ArchInvocationLabel X64PageGetAddress then returnOk $ InvokePage $ PageGetAddr p else throwError IllegalOperation - | _ \ undefined)" + | _ \ fail)" definition filter_frame_attrs :: "frame_attrs \ table_attrs" where