harness: tftp test: actually check that we got the file contents we expect
[barrelfish] / capabilities / caps.hl
1 /*
2  * Copyright (c) 2009, 2010, 2012, 2015, 2016, ETH Zurich.
3  * Copyright (c) 2015, 2016 Hewlett Packard Enterprise Development LP.
4  * All rights reserved.
5  *
6  * This file is distributed under the terms in the attached LICENSE file.
7  * If you do not find this file, copies can be found by writing to:
8  * ETH Zurich D-INFK, Universitaetstr. 6, CH-8092 Zurich. Attn: Systems Group.
9  */
10
11 /**
12     Hamlet input file.
13
14     This file defines the Barrelfish capability type system.
15
16     (Meta-)Comments about the syntax are enclosed between /** ... **/
17     Comments of the Hamlet language are enclosed between /* ... */
18 **/
19
20 /** We can define some constants using the "define" construct **/
21
22 /* XXX: these must match the corresponding OBJBITS definitions in
23  * barrelfish_kpi/capabilities.h */
24
25 /* Size of L2 CNode: L2 resolves 8 bits of Cap address space */
26 define objsize_l2cnode 16384;
27 /* Size of DCB: */
28 define objsize_dispatcher 1024;
29 /* Size of (x86_64) VNode: */
30 define objsize_vnode 4096; /* BASE_PAGE_SIZE */
31 /* Size of ARMv7 VNodes */
32 define objsize_vnode_arm_l1 16384;
33 define objsize_vnode_arm_l2 1024;
34 /* size of a kernel control block */
35 define objsize_kcb 65536; /* OBJSIZE_KCB */
36 /* size of a mapping cap:
37  * if mappings are zero-sized they mess up range queries */
38 define objsize_mapping 1;
39
40 /**
41     The capabilities of the whole system are listed thereafter.
42     The minimal definition consists of a name and an empty body.
43 **/
44
45 cap Null is_never_copy {
46     /* Null/invalid object type */
47 };
48
49 cap Memory abstract {
50     /**
51       For a populated cap, we need to give the type and name of each
52       of its fields, such as:
53       "genpaddr base;" for instance
54
55       In order to implement various comparisons, we need to specify a address
56       and size for each type that is backed by memory. The size may be
57       specified directly with "size" or as "size_bits".
58
59       Additional equality fields can be specified with an "eq" prefix, as in
60       "eq genpaddr base;"
61     **/
62
63     address genpaddr base;  /* Physical base address of Memory object */
64     pasid pasid;            /* Physical Address Space ID */
65     size gensize bytes;     /* Size of region in bytes */
66 };
67
68
69
70 /* Physical address range (root of cap tree) */
71 cap PhysAddr from_self inherit Memory;
72
73 cap Mapping abstract {
74     "struct capability" cap;
75     eq lvaddr pte;
76     uint32 offset;
77     uint16 pte_count;
78
79     address { get_address(cap) };
80     size { objsize_mapping };
81 };
82
83 cap VNode abstract {
84     address genpaddr base;  /* Base address of VNode */
85     size { objsize_vnode };
86 };
87
88 /** The following caps are similar to the previous one **/
89
90 /* RAM memory object */
91 cap RAM from PhysAddr from_self inherit Memory;
92
93 /* Abstract CNode, need to define size */
94 cap CNode abstract {
95     address lpaddr cnode;               /* Base address of CNode */
96     caprights rightsmask;               /* Cap access rights */
97 };
98
99 /* Level 1 CNode table, resizable */
100 cap L1CNode from RAM inherit CNode {
101     size gensize allocated_bytes;       /* Allocated size of L1 CNode in bytes */
102 };
103
104 /* Level 2 CNode table, resolves 8 bits of cap address */
105 cap L2CNode from RAM inherit CNode {
106     size { objsize_l2cnode };                 /* Size of L2 CNode in bytes (16kB) */
107 };
108
109 cap FCNode {
110      /* Foreign CNode capability */
111
112      eq genpaddr cnode;     /* Base address of CNode */
113      eq uint8 bits;         /* Number of bits this CNode resolves */
114      caprights rightsmask;
115      eq coreid core_id;     /* The core the cap is local on */
116      uint8 guard_size;      /* Number of bits in guard */
117      caddr guard;           /* Bitmask already resolved when reaching this CNode */
118 };
119
120 /** Dispatcher is interesting is several ways. **/
121
122 /**
123   XXX: The whole multi_retype stuff is hack in hamlet that should be removed as
124   soon as parts of an object can be retyped individually. -MN
125 **/
126
127 cap Dispatcher from RAM {
128     /* Dispatcher */
129
130     /**
131       The Dispatcher is a special case that can be retyped several
132       times to an end-point
133     **/
134     /** Note: This must be the first statement */
135     can_retype_multiple;
136
137     /**
138       We allow the use of unknow structures. However, equality will
139       be defined by address, not by structure.
140     **/
141     "struct dcb" dcb;       /* Pointer to kernel DCB */
142
143     address { mem_to_phys(dcb) };
144     size { objsize_dispatcher };
145 };
146
147 cap EndPoint from Dispatcher {
148     /* IDC endpoint */
149
150     "struct dcb" listener;  /* Dispatcher listening on this endpoint */
151     lvaddr epoffset;        /* Offset of endpoint buffer in disp frame */
152     uint32 epbuflen;        /* Length of endpoint buffer in words */
153
154     address { mem_to_phys(listener) };
155
156     /** XXX
157        Preferable definitions for address and size would be as below. These
158        should be used as soon as the whole multi retype hack stuff is fixed:
159
160        address { mem_to_phys(listener + epoffset) };
161        size { epbuflen };
162
163        -MN
164     **/
165 };
166
167 /** Then, we go back to routine **/
168
169 cap Frame from RAM from_self inherit Memory;
170
171 cap Frame_Mapping from Frame inherit Mapping;
172
173 cap DevFrame from PhysAddr from_self inherit Memory;
174
175 cap DevFrame_Mapping from DevFrame inherit Mapping;
176
177 cap Kernel is_always_copy {
178     /* Capability to a kernel */
179 };
180
181
182 /* x86_64-specific capabilities: */
183
184 /* PML4 */
185 cap VNode_x86_64_pml4 from RAM inherit VNode;
186
187 cap VNode_x86_64_pml4_Mapping from VNode_x86_64_pml4 inherit Mapping;
188
189 /* PDPT */
190 cap VNode_x86_64_pdpt from RAM inherit VNode;
191
192 cap VNode_x86_64_pdpt_Mapping from VNode_x86_64_pdpt inherit Mapping;
193
194 /* Page directory */
195 cap VNode_x86_64_pdir from RAM inherit VNode;
196
197 cap VNode_x86_64_pdir_Mapping from VNode_x86_64_pdir inherit Mapping;
198
199 /* Page table */
200 cap VNode_x86_64_ptable from RAM inherit VNode;
201
202 cap VNode_x86_64_ptable_Mapping from VNode_x86_64_ptable inherit Mapping;
203
204
205 /* x86_32-specific capabilities: */
206
207 /* PDPT */
208 cap VNode_x86_32_pdpt from RAM inherit VNode;
209
210 cap VNode_x86_32_pdpt_Mapping from VNode_x86_32_pdpt inherit Mapping;
211
212 /* Page directory */
213 cap VNode_x86_32_pdir from RAM inherit VNode;
214
215 cap VNode_x86_32_pdir_Mapping from VNode_x86_32_pdir inherit Mapping;
216
217 /* Page table */
218 cap VNode_x86_32_ptable from RAM inherit VNode;
219
220 cap VNode_x86_32_ptable_Mapping from VNode_x86_32_ptable inherit Mapping;
221
222 /* ARM specific capabilities: */
223
224 /* L1 Page Table */
225 cap VNode_ARM_l1 from RAM inherit VNode {
226     size { objsize_vnode_arm_l1 };
227 };
228
229 cap VNode_ARM_l1_Mapping from VNode_ARM_l1 inherit Mapping;
230
231 /* L2 Page Table */
232 cap VNode_ARM_l2 from RAM inherit VNode {
233     size { objsize_vnode_arm_l2 };
234 };
235
236 cap VNode_ARM_l2_Mapping from VNode_ARM_l2 inherit Mapping;
237
238 /* ARM AArch64-specific capabilities: */
239
240 /* L0 Page Table */
241 cap VNode_AARCH64_l0 from RAM inherit VNode;
242
243 cap VNode_AARCH64_l0_Mapping from VNode_AARCH64_l0 inherit Mapping;
244
245 /* L1 Page Table */
246 cap VNode_AARCH64_l1 from RAM inherit VNode;
247
248 cap VNode_AARCH64_l1_Mapping from VNode_AARCH64_l1 inherit Mapping;
249
250 /* L2 Page Table */
251 cap VNode_AARCH64_l2 from RAM inherit VNode;
252
253 cap VNode_AARCH64_l2_Mapping from VNode_AARCH64_l2 inherit Mapping;
254
255 /* L3 Page Table */
256 cap VNode_AARCH64_l3 from RAM inherit VNode;
257
258 cap VNode_AARCH64_l3_Mapping from VNode_AARCH64_l3 inherit Mapping;
259
260 /** IRQTable and IO are slightly different **/
261
262 cap IRQTable is_always_copy {
263     /* IRQ Routing table */
264     /**
265        When testing two IRQTable caps for is_copy, we always return True: all
266        IRQ entries originate from a single, primitive Cap. Grand'pa Cap, sort
267        of.
268     **/
269 };
270
271 cap IRQDest {
272         /* IRQ Destination capability.
273        Represents a slot in a CPUs int vector table.
274        Can be connected to a LMP endpoint to recv this interrupt. */
275     eq uint64 cpu;
276     eq uint64 vector;
277 };
278
279 cap IRQSrc from_self {
280         /* IRQ Source capability.
281        Represents an interrupt source. It contains a range of interrupt
282        source numbers. */ 
283         eq uint64 vec_start;
284         eq uint64 vec_end;
285 };
286
287 cap IO {
288     /* Legacy IO capability */
289     eq uint16 start;
290     eq uint16 end;          /* Granted IO range */
291 };
292
293 /* IPI notify caps */
294 cap Notify_IPI {
295     eq coreid coreid;
296     eq uint16 chanid;
297 };
298
299 /* ID capability, system-wide unique */
300 cap ID {
301     eq coreid coreid; /* core cap was created */
302     eq uint32 core_local_id; /* per core unique id */
303 };
304
305 cap PerfMon is_always_copy {
306 };
307
308 /** KernelControlBlock represents a struct kcb which contains all the pointers
309  *  to core-local global state of the kernel.
310  **/
311 cap KernelControlBlock from RAM {
312     "struct kcb" kcb;
313
314     address { mem_to_phys(kcb) };
315     /* base page size for now so we can map the kcb in boot driver */
316     size { objsize_kcb };
317 };
318
319 cap IPI is_always_copy {};