1(* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(GD_GPL) 9 *) 10 11theory ArchEmptyFail_AI 12imports "../EmptyFail_AI" 13begin 14 15context Arch begin global_naming ARM 16 17named_theorems EmptyFail_AI_assms 18 19crunch_ignore (empty_fail) 20 (add: invalidateLocalTLB_ASID_impl invalidateLocalTLB_VAASID_impl cleanByVA_impl 21 cleanByVA_PoU_impl invalidateByVA_impl invalidateByVA_I_impl 22 invalidate_I_PoU_impl cleanInvalByVA_impl branchFlush_impl 23 clean_D_PoU_impl cleanInvalidate_D_PoC_impl cleanInvalidateL2Range_impl 24 invalidateL2Range_impl cleanL2Range_impl flushBTAC_impl 25 writeContextID_impl isb_impl dsb_impl dmb_impl setHardwareASID_impl 26 writeTTBR0_impl cacheRangeOp setIRQTrigger_impl) 27 28crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: 29 loadWord, load_word_offs, storeWord, getRestartPC, get_mrs 30 31end 32 33global_interpretation EmptyFail_AI_load_word?: EmptyFail_AI_load_word 34 proof goal_cases 35 interpret Arch . 36 case 1 show ?case by (unfold_locales; (fact EmptyFail_AI_assms)?) 37 qed 38 39context Arch begin global_naming ARM 40 41crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: handle_fault 42 (simp: kernel_object.splits option.splits arch_cap.splits cap.splits endpoint.splits 43 bool.splits list.splits thread_state.splits split_def catch_def sum.splits 44 Let_def wp: zipWithM_x_empty_fail) 45 46crunch (empty_fail) empty_fail[wp]: 47 decode_tcb_configure, decode_bind_notification, decode_unbind_notification, 48 decode_set_priority, decode_set_mcpriority, decode_set_sched_params, 49 decode_set_tls_base 50 (simp: cap.splits arch_cap.splits split_def) 51 52lemma decode_tcb_invocation_empty_fail[wp]: 53 "empty_fail (decode_tcb_invocation a b (ThreadCap p) d e)" 54 by (simp add: decode_tcb_invocation_def split: invocation_label.splits | wp | intro conjI impI)+ 55 56crunch (empty_fail) empty_fail[wp]: find_pd_for_asid, get_master_pde, check_vp_alignment, 57 create_mapping_entries, ensure_safe_mapping, get_asid_pool, resolve_vaddr 58 (simp: kernel_object.splits arch_kernel_obj.splits option.splits pde.splits pte.splits) 59 60lemma arch_decode_ARMASIDControlMakePool_empty_fail: 61 "invocation_type label = ArchInvocationLabel ARMASIDControlMakePool 62 \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)" 63 apply (simp add: arch_decode_invocation_def Let_def) 64 apply (intro impI conjI allI) 65 apply (simp add: isPageFlushLabel_def isPDFlushLabel_def split: arch_cap.splits)+ 66 apply (rule impI) 67 apply (simp add: split_def) 68 apply wp 69 apply simp 70 apply (subst bindE_assoc[symmetric]) 71 apply (rule empty_fail_bindE) 72 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: if_split_asm) 73 by (simp add: Let_def split: cap.splits arch_cap.splits option.splits bool.splits | wp | intro conjI impI allI)+ 74 75lemma arch_decode_ARMASIDPoolAssign_empty_fail: 76 "invocation_type label = ArchInvocationLabel ARMASIDPoolAssign 77 \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)" 78 apply (simp add: arch_decode_invocation_def split_def Let_def isPageFlushLabel_def isPDFlushLabel_def 79 split: arch_cap.splits cap.splits option.splits | intro impI allI)+ 80 apply (rule empty_fail_bindE) 81 apply simp 82 apply (rule empty_fail_bindE) 83 apply ((simp | wp)+)[1] 84 apply (rule empty_fail_bindE) 85 apply ((simp | wp)+)[1] 86 apply (rule empty_fail_bindE) 87 apply ((simp | wp)+)[1] 88 apply (subst bindE_assoc[symmetric]) 89 apply (rule empty_fail_bindE) 90 subgoal by (fastforce simp: empty_fail_def whenE_def throwError_def select_def bindE_def 91 bind_def return_def returnOk_def lift_def liftE_def select_ext_def 92 gets_def get_def assert_def fail_def) 93 apply wp 94 done 95 96lemma arch_decode_invocation_empty_fail[wp]: 97 "empty_fail (arch_decode_invocation label b c d e f)" 98 apply (case_tac "invocation_type label") 99 apply (find_goal \<open>match premises in "_ = ArchInvocationLabel _" \<Rightarrow> \<open>-\<close>\<close>) 100 apply (rename_tac alabel) 101 apply (case_tac alabel; simp) 102 apply (find_goal \<open>succeeds \<open>erule arch_decode_ARMASIDControlMakePool_empty_fail\<close>\<close>) 103 apply (find_goal \<open>succeeds \<open>erule arch_decode_ARMASIDPoolAssign_empty_fail\<close>\<close>) 104 apply ((simp add: arch_decode_ARMASIDControlMakePool_empty_fail arch_decode_ARMASIDPoolAssign_empty_fail)+)[2] 105 including no_pre 106 by ((simp add: arch_decode_invocation_def Let_def split: arch_cap.splits cap.splits option.splits | (wp+) | intro conjI impI allI)+) 107 108end 109 110global_interpretation EmptyFail_AI_derive_cap?: EmptyFail_AI_derive_cap 111 proof goal_cases 112 interpret Arch . 113 case 1 show ?case by (unfold_locales; (fact EmptyFail_AI_assms)?) 114 qed 115 116context Arch begin global_naming ARM 117 118crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: maskInterrupt, empty_slot, 119 setHardwareASID, set_current_pd, finalise_cap, preemption_point, 120 cap_swap_for_delete, decode_invocation 121 (simp: Let_def catch_def split_def OR_choiceE_def mk_ef_def option.splits endpoint.splits 122 notification.splits thread_state.splits sum.splits cap.splits arch_cap.splits 123 kernel_object.splits vmpage_size.splits pde.splits bool.splits list.splits) 124 125crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: setRegister, setNextPC 126 127end 128 129global_interpretation EmptyFail_AI_rec_del?: EmptyFail_AI_rec_del 130 proof goal_cases 131 interpret Arch . 132 case 1 show ?case by (unfold_locales; (fact EmptyFail_AI_assms)?) 133 qed 134 135context Arch begin global_naming ARM 136crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: 137 cap_delete, choose_thread 138end 139 140global_interpretation EmptyFail_AI_schedule_unit?: EmptyFail_AI_schedule_unit 141 proof goal_cases 142 interpret Arch . 143 case 1 show ?case by (unfold_locales; (fact EmptyFail_AI_assms)?) 144 qed 145 146global_interpretation EmptyFail_AI_schedule_det?: EmptyFail_AI_schedule_det 147 proof goal_cases 148 interpret Arch . 149 case 1 show ?case by (unfold_locales; (fact EmptyFail_AI_assms)?) 150 qed 151 152global_interpretation EmptyFail_AI_schedule?: EmptyFail_AI_schedule 153 proof goal_cases 154 interpret Arch . 155 case 1 show ?case by (unfold_locales; (fact EmptyFail_AI_assms)?) 156 qed 157 158context Arch begin global_naming ARM 159crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: handle_event, activate_thread 160 (simp: cap.splits arch_cap.splits split_def invocation_label.splits Let_def 161 kernel_object.splits arch_kernel_obj.splits option.splits pde.splits pte.splits 162 bool.splits apiobject_type.splits aobject_type.splits notification.splits 163 thread_state.splits endpoint.splits catch_def sum.splits cnode_invocation.splits 164 page_table_invocation.splits page_invocation.splits asid_control_invocation.splits 165 asid_pool_invocation.splits arch_invocation.splits irq_state.splits syscall.splits 166 flush_type.splits page_directory_invocation.splits 167 ignore: resetTimer_impl ackInterrupt_impl) 168end 169 170global_interpretation EmptyFail_AI_call_kernel_unit?: EmptyFail_AI_call_kernel_unit 171 proof goal_cases 172 interpret Arch . 173 case 1 show ?case by (unfold_locales; (fact EmptyFail_AI_assms)?) 174 qed 175 176global_interpretation EmptyFail_AI_call_kernel_det?: EmptyFail_AI_call_kernel_det 177 proof goal_cases 178 interpret Arch . 179 case 1 show ?case by (unfold_locales; (fact EmptyFail_AI_assms)?) 180 qed 181 182global_interpretation EmptyFail_AI_call_kernel?: EmptyFail_AI_call_kernel 183 proof goal_cases 184 interpret Arch . 185 case 1 show ?case by (unfold_locales; (fact EmptyFail_AI_assms)?) 186 qed 187 188end 189