1(* 2 * Copyright 2018, Data61, CSIRO 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(DATA61_GPL) 9 *) 10 11(* 12Arch Functions for cancelling IPC. 13*) 14 15chapter {* Arch IPC Cancelling *} 16 17 18theory ArchIpcCancel_A 19imports "../CSpaceAcc_A" 20begin 21 22context Arch begin global_naming X64_A 23 24definition 25 set_ioport_mask :: "io_port \<Rightarrow> io_port \<Rightarrow> bool \<Rightarrow> (unit, 'z::state_ext) s_monad" 26where 27 "set_ioport_mask f l val \<equiv> do 28 allocated_ports \<leftarrow> gets (x64_allocated_io_ports \<circ> arch_state); 29 ap' \<leftarrow> return (\<lambda>p. if p \<ge> f \<and> p \<le> l then val else allocated_ports p); 30 modify (\<lambda>s. s \<lparr> arch_state := (arch_state s) \<lparr> x64_allocated_io_ports := ap' \<rparr>\<rparr>) 31 od" 32 33definition 34 free_ioport_range :: "io_port \<Rightarrow> io_port \<Rightarrow> (unit, 'z::state_ext) s_monad" 35where 36 "free_ioport_range f l \<equiv> set_ioport_mask f l False" 37 38text {* Actions to be taken after a cap is deleted *} 39definition 40 arch_post_cap_deletion :: "arch_cap \<Rightarrow> (unit, 'z::state_ext) s_monad" 41where 42 "arch_post_cap_deletion ac \<equiv> case ac of 43 IOPortCap f l \<Rightarrow> free_ioport_range f l 44 | _ \<Rightarrow> return ()" 45 46text {* Arch specific generic object references not covered by generic references *} 47datatype arch_gen_obj_ref = IOPortRef io_port 48 49definition 50 arch_gen_obj_refs :: "arch_cap \<Rightarrow> arch_gen_obj_ref set" 51where 52 "arch_gen_obj_refs ac \<equiv> case ac of 53 IOPortCap f l \<Rightarrow> IOPortRef ` {f} 54 | _ \<Rightarrow> {}" 55 56definition 57 arch_cap_cleanup_opt :: "arch_cap \<Rightarrow> cap" 58where 59 "arch_cap_cleanup_opt ac \<equiv> case ac of IOPortCap f l \<Rightarrow> ArchObjectCap (IOPortCap f l) | _ \<Rightarrow> NullCap" 60 61end 62end 63