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