From 5e4df460e29843aab4bdaa5000561d1f6f1c09f7 Mon Sep 17 00:00:00 2001 From: Miki Tanaka Date: Tue, 16 May 2017 21:27:26 +1000 Subject: [PATCH] ainvs: adjust generic theories for ARM fix --- proof/invariant-abstract/CNodeInv_AI.thy | 9 ++-- proof/invariant-abstract/CSpace_AI.thy | 10 +++++ proof/invariant-abstract/Detype_AI.thy | 12 ++++-- proof/invariant-abstract/Finalise_AI.thy | 4 +- proof/invariant-abstract/InterruptAcc_AI.thy | 2 + proof/invariant-abstract/Invariants_AI.thy | 26 +++++++++++- proof/invariant-abstract/Ipc_AI.thy | 43 ++++++++++++++++++-- proof/invariant-abstract/KHeapPre_AI.thy | 18 ++------ proof/invariant-abstract/KHeap_AI.thy | 17 +++++++- proof/invariant-abstract/Retype_AI.thy | 7 ++-- proof/invariant-abstract/VSpacePre_AI.thy | 4 +- 11 files changed, 112 insertions(+), 40 deletions(-) diff --git a/proof/invariant-abstract/CNodeInv_AI.thy b/proof/invariant-abstract/CNodeInv_AI.thy index c0a5025a0..ed8a9ac1a 100644 --- a/proof/invariant-abstract/CNodeInv_AI.thy +++ b/proof/invariant-abstract/CNodeInv_AI.thy @@ -1860,11 +1860,10 @@ lemma cap_swap_irq_handlers[wp]: crunch vspace_objs [wp]: cap_swap "valid_vspace_objs" +crunch valid_global_objs [wp]: cap_swap "valid_global_objs" + +crunch valid_global_vspace_mappings [wp]: cap_swap "valid_global_vspace_mappings" (* -crunch arch_objs [wp]: cap_swap "valid_arch_objs" - -crunch arch_objs [wp]: cap_move "valid_arch_objs" - crunch arch_objs [wp]: empty_slot "valid_arch_objs" *) @@ -1983,7 +1982,7 @@ lemma cap_swap_invs[wp]: cte_wp_at_caps_of_state simp del: split_paired_Ex split_paired_All | rule conjI - | fastforce dest!: valid_reply_caps_of_stateD)+ + | clarsimp dest!: valid_reply_caps_of_stateD)+ done lemma cap_swap_fd_invs[wp]: diff --git a/proof/invariant-abstract/CSpace_AI.thy b/proof/invariant-abstract/CSpace_AI.thy index ff34a1eaf..d1d707e2a 100644 --- a/proof/invariant-abstract/CSpace_AI.thy +++ b/proof/invariant-abstract/CSpace_AI.thy @@ -3954,6 +3954,12 @@ crunch empty_table_at[wp]: cap_insert "obj_at (empty_table S) p" simp: empty_table_caps_of) +crunch valid_global_objs[wp]: cap_insert "valid_global_objs" + (wp: crunch_wps) + +crunch global_vspace_mappings[wp]: cap_insert "valid_global_vspace_mappings" + (wp: crunch_wps) + crunch v_ker_map[wp]: cap_insert "valid_kernel_mappings" (wp: crunch_wps) @@ -4637,6 +4643,10 @@ lemmas setup_reply_master_valid_vso_at[wp] = valid_vso_at_lift [OF setup_reply_master_typ_at setup_reply_master_arch_ko_at] +crunch valid_global_objs[wp]: setup_reply_master "valid_global_objs" + +crunch global_vspace_mappings[wp]: setup_reply_master "valid_global_vspace_mappings" + crunch v_ker_map[wp]: setup_reply_master "valid_kernel_mappings" crunch eq_ker_map[wp]: setup_reply_master "equal_kernel_mappings" diff --git a/proof/invariant-abstract/Detype_AI.thy b/proof/invariant-abstract/Detype_AI.thy index fd000d609..a18d6d336 100644 --- a/proof/invariant-abstract/Detype_AI.thy +++ b/proof/invariant-abstract/Detype_AI.thy @@ -416,11 +416,13 @@ lemma unique_table_refs: split: if_split) apply blast done - - + lemma valid_pspace: "valid_pspace s" using invs by (simp add: invs_def valid_state_def) - + +lemma valid_global_objs: "valid_global_objs s" + using invs by (clarsimp simp: invs_def valid_state_def) + lemma cap_is_valid: "valid_cap cap s" by (rule cte_wp_valid_cap[OF cap invs_valid_objs[OF invs]]) @@ -465,8 +467,10 @@ locale detype_locale_gen_2 = detype_locale_gen_1 cap ptr s "valid_vspace_objs (detype (untyped_range cap) s)" "valid_arch_caps (detype (untyped_range cap) s)" "valid_kernel_mappings (detype (untyped_range cap) s)" + "valid_global_objs (detype (untyped_range cap) s)" "valid_asid_map (detype (untyped_range cap) s)" - "equal_kernel_mappings (detype (untyped_range cap) s)" + "valid_global_vspace_mappings (detype (untyped_range cap) s)" + "equal_kernel_mappings (detype (untyped_range cap) s)" "pspace_in_kernel_window (detype (untyped_range cap) s)" "valid_machine_state (clear_um (untyped_range cap) (detype (untyped_range cap) s))" "pspace_respects_device_region (clear_um (untyped_range cap) (detype (untyped_range cap) s))" diff --git a/proof/invariant-abstract/Finalise_AI.thy b/proof/invariant-abstract/Finalise_AI.thy index b34800464..c5d6a8e09 100644 --- a/proof/invariant-abstract/Finalise_AI.thy +++ b/proof/invariant-abstract/Finalise_AI.thy @@ -692,12 +692,12 @@ lemma tcb_cap_valid_imp_NullCap: apply (clarsimp simp: ran_tcb_cap_cases valid_ipc_buffer_cap_def split: Structures_A.thread_state.split_asm) done - +(* moved to Invariants_AI lemma a_type_arch_live: "a_type ko = AArch tp \ \ live0 ko" by (simp add: a_type_def split: Structures_A.kernel_object.split_asm) - +*) lemma pred_tcb_at_def2: "pred_tcb_at proj P t \ \s. \tcb. ko_at (TCB tcb) t s \ P (proj (tcb_to_itcb tcb))" by (rule eq_reflection, rule ext) (fastforce simp: pred_tcb_at_def obj_at_def) diff --git a/proof/invariant-abstract/InterruptAcc_AI.thy b/proof/invariant-abstract/InterruptAcc_AI.thy index e68d45257..e17162c24 100644 --- a/proof/invariant-abstract/InterruptAcc_AI.thy +++ b/proof/invariant-abstract/InterruptAcc_AI.thy @@ -53,6 +53,8 @@ definition all_invs_but_valid_irq_states_for where valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and + valid_global_objs and + valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and diff --git a/proof/invariant-abstract/Invariants_AI.thy b/proof/invariant-abstract/Invariants_AI.thy index 3c41b2f67..b61be6aba 100644 --- a/proof/invariant-abstract/Invariants_AI.thy +++ b/proof/invariant-abstract/Invariants_AI.thy @@ -26,7 +26,6 @@ requalify_consts is_nondevice_page_cap state_hyp_refs_of hyp_refs_of - arch_live hyp_live wellformed_acap @@ -45,8 +44,10 @@ requalify_consts valid_arch_objs valid_vspace_objs valid_arch_caps + valid_global_objs valid_kernel_mappings equal_kernel_mappings + valid_global_vspace_mappings pspace_in_kernel_window ASIDPoolObj @@ -84,6 +85,7 @@ requalify_facts physical_arch_cap_has_ref wellformed_arch_default valid_arch_obj_default' + valid_vspace_obj_default' vs_lookup1_stateI2 vs_lookup_pages1_stateI2 typ_at_pg @@ -624,6 +626,11 @@ where | Notification ntfn => live0 ko | ArchObj ao => hyp_live ko" +lemma a_type_arch_live: + "a_type ko = AArch tp \ \ live0 ko" + by (simp add: a_type_def + split: Structures_A.kernel_object.split_asm) + fun zobj_refs :: "cap \ obj_ref set" where @@ -895,9 +902,11 @@ where (* and valid_arch_objs *) and valid_vspace_objs and valid_arch_caps + and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map + and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region @@ -975,8 +984,9 @@ abbreviation(input) and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_machine_state and valid_irq_states and valid_irq_node and valid_irq_handlers and valid_vspace_objs (* and valid_arch_objs *) - and valid_arch_caps and valid_kernel_mappings + and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map + and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb" @@ -2539,6 +2549,14 @@ lemma valid_arch_cap_update [iff]: "valid_arch_caps (f s) = valid_arch_caps s" by (simp add: valid_arch_caps_def) +lemma valid_global_objs_update [iff]: + "valid_global_objs (f s) = valid_global_objs s" + by (simp add: valid_global_objs_def arch) + +lemma valid_global_vspace_mappings_update [iff]: + "valid_global_vspace_mappings (f s) = valid_global_vspace_mappings s" + by (simp add: valid_global_vspace_mappings_def arch) + lemma pspace_in_kernel_window_update [iff]: "pspace_in_kernel_window (f s) = pspace_in_kernel_window s" by (simp add: pspace_in_kernel_window_def arch pspace) @@ -3183,6 +3201,10 @@ lemma cur_tcb_arch [iff]: "cur_tcb (arch_state_update f s) = cur_tcb s" by (simp add: cur_tcb_def) +lemma invs_valid_global_objs[elim!]: + "invs s \ valid_global_objs s" + by (clarsimp simp: invs_def valid_state_def) + lemma get_irq_slot_real_cte: "\invs\ get_irq_slot irq \real_cte_at\" apply (simp add: get_irq_slot_def) diff --git a/proof/invariant-abstract/Ipc_AI.thy b/proof/invariant-abstract/Ipc_AI.thy index 435247d15..d4bb5e2ac 100644 --- a/proof/invariant-abstract/Ipc_AI.thy +++ b/proof/invariant-abstract/Ipc_AI.thy @@ -235,6 +235,10 @@ locale Ipc_AI = "\ ft t. make_arch_fault_msg ft t \cap_refs_in_kernel_window :: 'state_ext state \ bool\" assumes make_arch_fault_msg_valid_objs[wp]: "\ ft t. make_arch_fault_msg ft t \valid_objs :: 'state_ext state \ bool\" + assumes make_arch_fault_msg_valid_global_objs[wp]: + "\ ft t. make_arch_fault_msg ft t \valid_global_objs :: 'state_ext state \ bool\" + assumes make_arch_fault_msg_valid_global_vspace_mappings[wp]: + "\ ft t. make_arch_fault_msg ft t \valid_global_vspace_mappings :: 'state_ext state \ bool\" assumes make_arch_fault_msg_valid_ioc[wp]: "\ ft t. make_arch_fault_msg ft t \valid_ioc :: 'state_ext state \ bool\" assumes make_arch_fault_msg_vms[wp]: @@ -273,6 +277,11 @@ locale Ipc_AI = \valid_objs and cte_wp_at P (t, ref) and tcb_at t :: 'state_ext state \ bool\ do_ipc_transfer st ep b gr rt \\rv. cte_wp_at P (t, ref)\" + assumes setup_caller_cap_valid_global_objs[wp]: + "\send recv. + \valid_global_objs :: 'state_ext state \ bool\ + setup_caller_cap send recv + \\rv. valid_global_objs\" assumes handle_arch_fault_reply_typ_at[wp]: "\ P T p x4 t label msg. \\s::'state_ext state. P (typ_at T p s)\ @@ -970,8 +979,16 @@ lemma transfer_caps_loop_valid_arch_caps[wp]: apply clarsimp done +crunch valid_global_objs [wp]: set_extra_badge valid_global_objs +lemma transfer_caps_loop_valid_global_objs[wp]: + "\ep buffer n caps slots mi. + \valid_global_objs :: 'state_ext state \ bool\ + transfer_caps_loop ep buffer n caps slots mi + \\rv. valid_global_objs\" + by (wp transfer_caps_loop_pres cap_insert_valid_global_objs) + crunch valid_kernel_mappings [wp]: set_extra_badge valid_kernel_mappings @@ -1015,6 +1032,16 @@ lemma transfer_caps_loop_only_idle[wp]: \\rv. only_idle\" by (wp transfer_caps_loop_pres | simp)+ +crunch valid_global_vspace_mappings [wp]: set_extra_badge valid_global_vspace_mappings + + +lemma transfer_caps_loop_valid_global_pd_mappings[wp]: + "\ep buffer n caps slots mi. + \valid_global_vspace_mappings :: 'state_ext state \ bool\ + transfer_caps_loop ep buffer n caps slots mi + \\rv. valid_global_vspace_mappings\" + by (wp transfer_caps_loop_pres) + crunch pspace_in_kernel_window [wp]: set_extra_badge pspace_in_kernel_window @@ -1121,7 +1148,8 @@ lemma transfer_caps_loop_invs[wp]: \ transfer_caps_srcs caps s\ transfer_caps_loop ep buffer n caps slots mi \\rv. invs\" - unfolding invs_def valid_state_def valid_pspace_def by (wpsimp wp: valid_irq_node_typ transfer_caps_loop_valid_vspace_objs) + unfolding invs_def valid_state_def valid_pspace_def + by (wpsimp wp: valid_irq_node_typ transfer_caps_loop_valid_vspace_objs) end @@ -1672,14 +1700,17 @@ lemma copy_mrs_irq_handlers[wp]: context Ipc_AI begin crunch irq_handlers[wp]: do_ipc_transfer "valid_irq_handlers :: 'state_ext state \ bool" - (wp: crunch_wps hoare_vcg_const_Ball_lift simp: zipWithM_x_mapM crunch_simps ball_conj_distrib ) + (wp: crunch_wps hoare_vcg_const_Ball_lift simp: zipWithM_x_mapM crunch_simps ball_conj_distrib) -crunch vspace_objs[wp]: transfer_caps_loop "valid_vspace_objs :: 'state_ext state \ bool" - (wp: crunch_wps transfer_caps_loop_valid_vspace_objs simp: zipWithM_x_mapM crunch_simps) +crunch valid_global_objs[wp]: do_ipc_transfer "valid_global_objs :: 'state_ext state \ bool" + (wp: crunch_wps simp: zipWithM_x_mapM ignore: make_arch_fault_msg) crunch vspace_objs[wp]: do_ipc_transfer "valid_vspace_objs :: 'state_ext state \ bool" (wp: crunch_wps transfer_caps_loop_valid_vspace_objs simp: zipWithM_x_mapM crunch_simps) +crunch valid_global_vspace_mappings[wp]: do_ipc_transfer "valid_global_vspace_mappings :: 'state_ext state \ bool" + (wp: crunch_wps transfer_caps_loop_valid_vspace_objs simp: zipWithM_x_mapM crunch_simps) + crunch arch_caps[wp]: do_ipc_transfer "valid_arch_caps :: 'state_ext state \ bool" (wp: crunch_wps hoare_vcg_const_Ball_lift transfer_caps_loop_valid_arch_caps simp: zipWithM_x_mapM crunch_simps ball_conj_distrib ) @@ -1718,6 +1749,8 @@ context Ipc_AI begin crunch only_idle [wp]: do_ipc_transfer "only_idle :: 'state_ext state \ bool" (wp: crunch_wps simp: crunch_simps) +crunch valid_global_vspace_mappings [wp]: set_extra_badge valid_global_vspace_mappings + crunch pspace_in_kernel_window[wp]: do_ipc_transfer "pspace_in_kernel_window :: 'state_ext state \ bool" (wp: crunch_wps simp: crunch_simps) @@ -2448,6 +2481,8 @@ crunch eq_ker_map[wp]: setup_caller_cap "equal_kernel_mappings" crunch asid_map [wp]: setup_caller_cap "valid_asid_map" +crunch global_pd_mappings[wp]: setup_caller_cap "valid_global_vspace_mappings" + crunch pspace_in_kernel_window[wp]: setup_caller_cap "pspace_in_kernel_window" lemma setup_caller_cap_cap_refs_in_window[wp]: diff --git a/proof/invariant-abstract/KHeapPre_AI.thy b/proof/invariant-abstract/KHeapPre_AI.thy index b1c9f99f4..c322c058a 100644 --- a/proof/invariant-abstract/KHeapPre_AI.thy +++ b/proof/invariant-abstract/KHeapPre_AI.thy @@ -73,7 +73,7 @@ lemma arch_obj_pred_a_type[intro, simp]: "arch_obj_pred (\ko. a_type ko lemma arch_obj_pred_arch_obj_l[intro, simp]: "arch_obj_pred (\ko. ArchObj ako = ko)" and - arch_obj_pred_arch_obj_r[intro, simp]: "arch_obj_pred (\ko. ko = ArchObj ako)" +arch_obj_pred_arch_obj_r[intro, simp]: "arch_obj_pred (\ko. ko = ArchObj ako)" by (auto simp add: arch_obj_pred_defs) lemma arch_obj_pred_fun_lift: "arch_obj_pred (\ko. F (arch_obj_fun_lift P N ko))" @@ -109,27 +109,15 @@ declare locale arch_only_obj_pred = fixes P :: "kernel_object \ bool" - assumes arch_only: "arch_obj_pred P" - -(**) - -(* -lemma "arch_obj_pred P \ vspace_obj_pred P" - apply (clarsimp simp add: arch_obj_pred_def vspace_obj_pred_def) - apply (erule_tac x=ko in allE) - apply (simp add: non_vspace_obj_def) - apply -*) + assumes arch_only: "arch_obj_pred P" locale vspace_only_obj_pred = fixes P :: "kernel_object \ bool" fixes vspace_obj_pred :: "(kernel_object \ bool) \ bool" assumes vspace_only: "vspace_obj_pred P" -(**) - lemma set_object_typ_at: - "\\s. typ_at (a_type ko) p s \ P (typ_at T p' s)\ + "\\s. typ_at (a_type ko) p s \ P (typ_at T p' s)\ set_object p ko \\rv s. P (typ_at T p' s)\" apply (simp add: set_object_def) apply wp diff --git a/proof/invariant-abstract/KHeap_AI.thy b/proof/invariant-abstract/KHeap_AI.thy index 62a93d81a..7c9c3e857 100644 --- a/proof/invariant-abstract/KHeap_AI.thy +++ b/proof/invariant-abstract/KHeap_AI.thy @@ -27,9 +27,11 @@ requalify_facts vs_lookup_vspace_obj_at_lift vs_lookup_pages_vspace_obj_at_lift valid_arch_caps_lift_weak + valid_global_objs_lift_weak valid_asid_map_lift valid_kernel_mappings_lift equal_kernel_mappings_lift + valid_global_vspace_mappings_lift valid_machine_state_lift valid_vso_at_lift valid_vso_at_lift_aobj_at @@ -1253,7 +1255,7 @@ lemma set_object_non_pagetable: apply (clarsimp simp: obj_at_def) by (rule vspace_obj_predE) - +(* lemma set_object_vspace_objs_non_pagetable: "\valid_vspace_objs and K (non_vspace_obj ko) and obj_at non_vspace_obj p\ set_object p ko @@ -1262,7 +1264,7 @@ lemma set_object_vspace_objs_non_pagetable: apply (rule hoare_pre) apply (rule valid_vspace_objs_lift_weak) apply (wpsimp wp: set_object_non_pagetable)+ - done + done*) lemma set_object_memory[wp]: "\\s. P (underlying_memory (machine_state s))\ @@ -1311,6 +1313,13 @@ by (rule vs_lookup_vspace_obj_at_lift; wp vsobj_at; simp) lemma vs_lookup_pages[wp]: "\\s. P (vs_lookup_pages s)\ f \\_ s. P (vs_lookup_pages s)\" by (rule vs_lookup_pages_vspace_obj_at_lift; wp vsobj_at; simp) +lemma valid_global_objs[wp]: "\valid_global_objs\ f \\_. valid_global_objs\" +by (rule valid_global_objs_lift_weak, (wp vsobj_at)+) + +lemma valid_global_vspace_mappings[wp]: + "\valid_global_vspace_mappings\ f \\_. valid_global_vspace_mappings\" +by (rule valid_global_vspace_mappings_lift, (wp vsobj_at)+) + lemma valid_asid_map[wp]: "\valid_asid_map\ f \\_. valid_asid_map\" by (rule valid_asid_map_lift, (wp vsobj_at)+) @@ -1692,6 +1701,10 @@ crunch reply_masters[wp]: do_machine_op "valid_reply_masters" crunch valid_irq_handlers[wp]: do_machine_op "valid_irq_handlers" +crunch valid_global_objs[wp]: do_machine_op "valid_global_objs" + +crunch valid_global_vspace_mappings[wp]: do_machine_op "valid_global_vspace_mappings" + crunch valid_arch_caps[wp]: do_machine_op "valid_arch_caps" diff --git a/proof/invariant-abstract/Retype_AI.thy b/proof/invariant-abstract/Retype_AI.thy index 7a9db3bea..d1213203c 100644 --- a/proof/invariant-abstract/Retype_AI.thy +++ b/proof/invariant-abstract/Retype_AI.thy @@ -22,7 +22,6 @@ abbreviation "down_aligned_area ptr sz \ {(ptr && ~~ mask sz) + (2 ^ sz - context begin interpretation Arch . requalify_facts global_refs_kheap - valid_vspace_obj_default' (* move to invariants_AI? *) requalify_consts clearMemory clearMemoryVM @@ -1123,9 +1122,9 @@ abbreviation(input) and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_vspace_objs - and valid_irq_states + and valid_irq_states and valid_global_objs and valid_arch_caps and valid_kernel_mappings - and valid_asid_map + and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and valid_ioc and valid_machine_state" @@ -1150,6 +1149,7 @@ locale Retype_AI_dmo_eq_kernel_restricted = crunch only_idle[wp]: do_machine_op "only_idle" crunch valid_global_refs[wp]: do_machine_op "valid_global_refs" +crunch global_mappings[wp]: do_machine_op "valid_global_vspace_mappings" crunch valid_kernel_mappings[wp]: do_machine_op "valid_kernel_mappings" crunch cap_refs_in_kernel_window[wp]: do_machine_op "cap_refs_in_kernel_window" @@ -1627,7 +1627,6 @@ lemma valid_obj_default_object: apply (clarsimp simp add: wellformed_arch_default) done - lemma valid_vspace_obj_default: assumes tyunt: "ty \ Structures_A.apiobject_type.Untyped" shows "ArchObj ao = default_object ty dev us \ valid_vspace_obj ao s'" diff --git a/proof/invariant-abstract/VSpacePre_AI.thy b/proof/invariant-abstract/VSpacePre_AI.thy index 670e2a783..d10561593 100644 --- a/proof/invariant-abstract/VSpacePre_AI.thy +++ b/proof/invariant-abstract/VSpacePre_AI.thy @@ -103,8 +103,8 @@ lemma hoare_name_pre_state2: by (auto simp: valid_def intro: hoare_name_pre_state) lemma pd_casting_shifting: - "size x + 3 < len_of TYPE('a) \ - ucast (ucast x << 3 >> 3 :: ('a :: len) word) = x" + "size x + n < len_of TYPE('a) \ + ucast (ucast x << n >> n :: ('a :: len) word) = x" apply (rule word_eqI) apply (simp add: nth_ucast nth_shiftr nth_shiftl word_size) done