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 11(* 12Refinement for handleEvent and syscalls 13*) 14 15theory ArchSyscall_AI 16imports 17 "../Syscall_AI" 18begin 19 20context Arch begin global_naming ARM 21 22named_theorems Syscall_AI_assms 23 24declare arch_get_sanitise_register_info_invs[Syscall_AI_assms] 25crunch pred_tcb_at[wp,Syscall_AI_assms]: handle_arch_fault_reply, arch_get_sanitise_register_info "pred_tcb_at proj P t" 26crunch invs[wp,Syscall_AI_assms]: handle_arch_fault_reply "invs" 27crunch cap_to[wp,Syscall_AI_assms]: handle_arch_fault_reply "ex_nonz_cap_to c" 28crunch it[wp,Syscall_AI_assms]: handle_arch_fault_reply, arch_get_sanitise_register_info "\<lambda>s. P (idle_thread s)" 29crunch caps[wp,Syscall_AI_assms]: handle_arch_fault_reply, arch_get_sanitise_register_info "\<lambda>s. P (caps_of_state s)" 30crunch cur_thread[wp,Syscall_AI_assms]: handle_arch_fault_reply, arch_get_sanitise_register_info "\<lambda>s. P (cur_thread s)" 31crunch valid_objs[wp,Syscall_AI_assms]: handle_arch_fault_reply, arch_get_sanitise_register_info "valid_objs" 32crunch cte_wp_at[wp,Syscall_AI_assms]: handle_arch_fault_reply, arch_get_sanitise_register_info "\<lambda>s. P (cte_wp_at P' p s)" 33declare arch_get_sanitise_register_info_ex_nonz_cap_to[Syscall_AI_assms] 34 make_fault_message_inv[Syscall_AI_assms] 35 36 37crunch typ_at[wp, Syscall_AI_assms]: invoke_irq_control "\<lambda>s. P (typ_at T p s)" 38 39lemma obj_refs_cap_rights_update[simp, Syscall_AI_assms]: 40 "obj_refs (cap_rights_update rs cap) = obj_refs cap" 41 by (simp add: cap_rights_update_def acap_rights_update_def 42 split: cap.split arch_cap.split) 43 44(* FIXME: move to TCB *) 45lemma table_cap_ref_mask_cap [Syscall_AI_assms]: 46 "table_cap_ref (mask_cap R cap) = table_cap_ref cap" 47 by (clarsimp simp add:mask_cap_def table_cap_ref_def acap_rights_update_def 48 cap_rights_update_def split:cap.splits arch_cap.splits) 49 50lemma diminished_no_cap_to_obj_with_diff_ref [Syscall_AI_assms]: 51 "\<lbrakk> cte_wp_at (diminished cap) p s; valid_arch_caps s \<rbrakk> 52 \<Longrightarrow> no_cap_to_obj_with_diff_ref cap S s" 53 apply (clarsimp simp: cte_wp_at_caps_of_state valid_arch_caps_def) 54 apply (frule(1) unique_table_refs_no_cap_asidD) 55 apply (clarsimp simp add: no_cap_to_obj_with_diff_ref_def 56 table_cap_ref_mask_cap diminished_def Ball_def) 57 done 58 59lemma getDFSR_invs[wp]: 60 "valid invs (do_machine_op getDFSR) (\<lambda>_. invs)" 61 by (simp add: getDFSR_def do_machine_op_def split_def select_f_returns | wp)+ 62 63lemma getFAR_invs[wp]: 64 "valid invs (do_machine_op getFAR) (\<lambda>_. invs)" 65 by (simp add: getFAR_def do_machine_op_def split_def select_f_returns | wp)+ 66 67lemma getIFSR_invs[wp]: 68 "valid invs (do_machine_op getIFSR) (\<lambda>_. invs)" 69 by (simp add: getIFSR_def do_machine_op_def split_def select_f_returns | wp)+ 70 71lemma hv_invs[wp, Syscall_AI_assms]: "\<lbrace>invs\<rbrace> handle_vm_fault t' flt \<lbrace>\<lambda>r. invs\<rbrace>" 72 apply (cases flt, simp_all) 73 apply (wp|simp)+ 74 done 75 76lemma handle_vm_fault_valid_fault[wp, Syscall_AI_assms]: 77 "\<lbrace>\<top>\<rbrace> handle_vm_fault thread ft -,\<lbrace>\<lambda>rv s. valid_fault rv\<rbrace>" 78 apply (cases ft, simp_all) 79 apply (wp no_irq_getDFSR no_irq_getIFSR| simp add: valid_fault_def)+ 80 done 81 82lemma hvmf_active [Syscall_AI_assms]: 83 "\<lbrace>st_tcb_at active t\<rbrace> handle_vm_fault t w \<lbrace>\<lambda>rv. st_tcb_at active t\<rbrace>" 84 apply (cases w, simp_all) 85 apply (wp | simp)+ 86 done 87 88lemma hvmf_ex_cap[wp, Syscall_AI_assms]: 89 "\<lbrace>ex_nonz_cap_to p\<rbrace> handle_vm_fault t b \<lbrace>\<lambda>rv. ex_nonz_cap_to p\<rbrace>" 90 apply (cases b, simp_all) 91 apply (wp | simp)+ 92 done 93 94lemma hh_invs[wp, Syscall_AI_assms]: 95 "\<lbrace>invs and ct_active and st_tcb_at active thread and ex_nonz_cap_to thread\<rbrace> 96 handle_hypervisor_fault thread fault 97 \<lbrace>\<lambda>rv. invs\<rbrace>" 98 by (cases fault; wpsimp simp: valid_fault_def) 99 100end 101 102global_interpretation Syscall_AI?: Syscall_AI 103 proof goal_cases 104 interpret Arch . 105 case 1 show ?case by (unfold_locales; (fact Syscall_AI_assms)?) 106 qed 107 108end 109