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