1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7(* Author: Andrew Boyton, 2012 8 Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au> 9 Rafal Kolanski <rafal.kolanski at nicta.com.au> 10*) 11 12chapter "A simplified version of the actual capDL specification." 13 14theory Types_D 15imports "HOL-Word.Word" 16begin 17 18(* 19 * Objects are named by 32 bit words. 20 * This name may correspond to the memory address of the object. 21 *) 22type_synonym cdl_object_id = "32 word" 23 24type_synonym cdl_object_set = "cdl_object_id set" 25 26(* The type we use to represent object sizes. *) 27type_synonym cdl_size_bits = nat 28 29(* An index into a CNode, TCB, or other kernel object that contains caps. *) 30type_synonym cdl_cnode_index = nat 31 32(* A reference to a capability slot. *) 33type_synonym cdl_cap_ref = "cdl_object_id \<times> cdl_cnode_index" 34 35(* The possible access-control rights that exist in the system. *) 36datatype cdl_right = AllowRead | AllowWrite | AllowGrant 37 38 39(* 40 * Kernel capabilities. 41 * 42 * Such capabilities (or "caps") give the holder particular rights to 43 * a kernel object or system hardware. 44 * 45 * Caps have attributes such as the object they point to, the rights 46 * they give the holder, or how the holder is allowed to interact with 47 * the target object. 48 * 49 * This is a simplified, cut-down version of this datatype for 50 * demonstration purposes. 51 *) 52datatype cdl_cap = 53 NullCap 54 | EndpointCap cdl_object_id "cdl_right set" 55 | CNodeCap cdl_object_id 56 | TcbCap cdl_object_id 57 58(* A mapping from capability identifiers to capabilities. *) 59type_synonym cdl_cap_map = "cdl_cnode_index \<Rightarrow> cdl_cap option" 60 61translations 62 (type) "cdl_cap_map" <= (type) "nat \<Rightarrow> cdl_cap option" 63 (type) "cdl_cap_ref" <= (type) "cdl_object_id \<times> nat" 64 65(* A user cap pointer. *) 66type_synonym cdl_cptr = "32 word" 67 68(* Kernel objects *) 69record cdl_tcb = 70 cdl_tcb_caps :: cdl_cap_map 71 cdl_tcb_fault_endpoint :: cdl_cptr 72 73record cdl_cnode = 74 cdl_cnode_caps :: cdl_cap_map 75 cdl_cnode_size_bits :: cdl_size_bits 76 77(* 78 * Kernel objects. 79 * 80 * These are in-memory objects that may, over the course of the system 81 * execution, be created or deleted by users. 82 * 83 * Again, a simplified version of the real datatype. 84 *) 85datatype cdl_object = 86 Endpoint 87 | Tcb cdl_tcb 88 | CNode cdl_cnode 89 90(* 91 * The current state of the system. 92 * 93 * The state record contains the following primary pieces of information: 94 * 95 * objects: 96 * The objects that currently exist in the system. 97 * 98 * current_thread: 99 * The currently running thread. Operations will always be performed 100 * on behalf of this thread. 101 * 102 * ghost_state: (Used for separation logic) 103 * Which fields are owned by an object. 104 * In capDL this is all of the fields (or none of them). 105 * In any concrete state, this will be all of the fields. 106 *) 107 108 109(* The ghost state tracks which components (fields and slots) are owned by an object. 110 * Fields + slots are encoded as None + Some nat. 111 *) 112type_synonym cdl_heap = "cdl_object_id \<Rightarrow> cdl_object option" 113type_synonym cdl_component = "nat option" 114type_synonym cdl_components = "cdl_component set" 115type_synonym cdl_ghost_state = "cdl_object_id \<Rightarrow> cdl_components" 116 117translations 118 (type) "cdl_heap" <= (type) "cdl_object_id \<Rightarrow> cdl_object option" 119 (type) "cdl_ghost_state" <= (type) "cdl_object_id \<Rightarrow> nat option set" 120 121record cdl_state = 122 cdl_objects :: "cdl_heap" 123 cdl_current_thread :: "cdl_object_id option" 124 cdl_ghost_state :: "cdl_ghost_state" 125 126 127(* Kernel objects types. *) 128datatype cdl_object_type = 129 EndpointType 130 | TcbType 131 | CNodeType 132 133(* Return the type of an object. *) 134definition 135 object_type :: "cdl_object \<Rightarrow> cdl_object_type" 136where 137 "object_type x \<equiv> 138 case x of 139 Endpoint \<Rightarrow> EndpointType 140 | Tcb _ \<Rightarrow> TcbType 141 | CNode _ \<Rightarrow> CNodeType" 142 143(* 144 * Getters and setters for various data types. 145 *) 146 147(* Capability getters / setters *) 148 149definition cap_objects :: "cdl_cap \<Rightarrow> cdl_object_id set" 150where 151 "cap_objects cap \<equiv> 152 case cap of 153 TcbCap x \<Rightarrow> {x} 154 | CNodeCap x \<Rightarrow> {x} 155 | EndpointCap x _ \<Rightarrow> {x}" 156 157definition cap_has_object :: "cdl_cap \<Rightarrow> bool" 158where 159 "cap_has_object cap \<equiv> 160 case cap of 161 NullCap \<Rightarrow> False 162 | _ \<Rightarrow> True" 163 164definition cap_object :: "cdl_cap \<Rightarrow> cdl_object_id" 165where 166 "cap_object cap \<equiv> 167 if cap_has_object cap 168 then THE obj_id. cap_objects cap = {obj_id} 169 else undefined " 170 171lemma cap_object_simps: 172 "cap_object (TcbCap x) = x" 173 "cap_object (CNodeCap x) = x" 174 "cap_object (EndpointCap x j) = x" 175 by (simp_all add:cap_object_def cap_objects_def cap_has_object_def) 176 177definition 178 cap_rights :: "cdl_cap \<Rightarrow> cdl_right set" 179where 180 "cap_rights c \<equiv> case c of 181 EndpointCap _ x \<Rightarrow> x 182 | _ \<Rightarrow> UNIV" 183 184definition 185 update_cap_rights :: "cdl_right set \<Rightarrow> cdl_cap \<Rightarrow> cdl_cap" 186where 187 "update_cap_rights r c \<equiv> case c of 188 EndpointCap f1 _ \<Rightarrow> EndpointCap f1 r 189 | _ \<Rightarrow> c" 190 191(* Kernel object getters / setters *) 192definition 193 object_slots :: "cdl_object \<Rightarrow> cdl_cap_map" 194where 195 "object_slots obj \<equiv> case obj of 196 CNode x \<Rightarrow> cdl_cnode_caps x 197 | Tcb x \<Rightarrow> cdl_tcb_caps x 198 | _ \<Rightarrow> Map.empty" 199 200definition 201 update_slots :: "cdl_cap_map \<Rightarrow> cdl_object \<Rightarrow> cdl_object" 202where 203 "update_slots new_val obj \<equiv> case obj of 204 CNode x \<Rightarrow> CNode (x\<lparr>cdl_cnode_caps := new_val\<rparr>) 205 | Tcb x \<Rightarrow> Tcb (x\<lparr>cdl_tcb_caps := new_val\<rparr>) 206 | _ \<Rightarrow> obj" 207 208(* Adds new caps to an object. It won't overwrite on a collision. *) 209definition 210 add_to_slots :: "cdl_cap_map \<Rightarrow> cdl_object \<Rightarrow> cdl_object" 211where 212 "add_to_slots new_val obj \<equiv> update_slots (new_val ++ (object_slots obj)) obj" 213 214definition 215 slots_of :: "cdl_heap \<Rightarrow> cdl_object_id \<Rightarrow> cdl_cap_map" 216where 217 "slots_of h \<equiv> \<lambda>obj_id. 218 case h obj_id of 219 None \<Rightarrow> Map.empty 220 | Some obj \<Rightarrow> object_slots obj" 221 222 223definition 224 has_slots :: "cdl_object \<Rightarrow> bool" 225where 226 "has_slots obj \<equiv> case obj of 227 CNode _ \<Rightarrow> True 228 | Tcb _ \<Rightarrow> True 229 | _ \<Rightarrow> False" 230 231definition 232 object_at :: "(cdl_object \<Rightarrow> bool) \<Rightarrow> cdl_object_id \<Rightarrow> cdl_heap \<Rightarrow> bool" 233where 234 "object_at P p s \<equiv> \<exists>object. s p = Some object \<and> P object" 235 236abbreviation 237 "ko_at k \<equiv> object_at ((=) k)" 238 239end 240