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 */
26define objsize_l2cnode 16384;
27/* Size of DCB: */
28define objsize_dispatcher 1024;
29/* Size of (x86_64) VNode: */
30define objsize_vnode 4096; /* BASE_PAGE_SIZE */
31/* Size of ARMv7 VNodes */
32define objsize_vnode_arm_l1 16384;
33define objsize_vnode_arm_l2 1024;
34/* size of a kernel control block */
35define objsize_kcb 65536; /* OBJSIZE_KCB */
36/* size of a mapping cap:
37 * if mappings are zero-sized they mess up range queries */
38define 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
45cap Null is_never_copy {
46    /* Null/invalid object type */
47};
48
49cap 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) */
71cap PhysAddr from_self inherit Memory;
72
73cap Mapping abstract {
74    "struct capability" cap;
75    eq "struct cte" ptable;
76    /* We currently never use the offset into the source capability, so remove
77     * it to make room for a more expressive way of referring to the pte */
78    /* uint32 offset; */
79    eq uint16 entry;
80    uint16 pte_count;
81
82    address { get_address(cap) };
83    size { objsize_mapping };
84};
85
86cap VNode abstract {
87    address genpaddr base;  /* Base address of VNode */
88    size { objsize_vnode };
89};
90
91/** The following caps are similar to the previous one **/
92
93/* RAM memory object */
94cap RAM from PhysAddr from_self inherit Memory;
95
96/* Abstract CNode, need to define size */
97cap CNode abstract {
98    address lpaddr cnode;               /* Base address of CNode */
99    caprights rightsmask;               /* Cap access rights */
100};
101
102/* Level 1 CNode table, resizable */
103cap L1CNode from RAM inherit CNode {
104    size gensize allocated_bytes;       /* Allocated size of L1 CNode in bytes */
105};
106
107/* Level 2 CNode table, resolves 8 bits of cap address */
108cap L2CNode from RAM inherit CNode {
109    size { objsize_l2cnode };                 /* Size of L2 CNode in bytes (16kB) */
110};
111
112cap FCNode {
113     /* Foreign CNode capability */
114
115     eq genpaddr cnode;	    /* Base address of CNode */
116     eq uint8 bits;    	    /* Number of bits this CNode resolves */
117     caprights rightsmask;
118     eq coreid core_id;     /* The core the cap is local on */
119     uint8 guard_size; 	    /* Number of bits in guard */
120     caddr guard;           /* Bitmask already resolved when reaching this CNode */
121};
122
123/** Dispatcher is interesting is several ways. **/
124
125/**
126  XXX: The whole multi_retype stuff is hack in hamlet that should be removed as
127  soon as parts of an object can be retyped individually. -MN
128**/
129
130cap Dispatcher from RAM {
131    /* Dispatcher */
132
133    /**
134      The Dispatcher is a special case that can be retyped several
135      times to an end-point
136    **/
137    /** Note: This must be the first statement */
138    can_retype_multiple;
139
140    /**
141      We allow the use of unknow structures. However, equality will
142      be defined by address, not by structure.
143    **/
144    "struct dcb" dcb;       /* Pointer to kernel DCB */
145
146    address { mem_to_phys(dcb) };
147    size { objsize_dispatcher };
148};
149
150cap EndPoint from Dispatcher {
151    /* IDC endpoint */
152
153    "struct dcb" listener;  /* Dispatcher listening on this endpoint */
154    lvaddr epoffset;        /* Offset of endpoint buffer in disp frame */
155    uint32 epbuflen;        /* Length of endpoint buffer in words */
156
157    address { mem_to_phys(listener) };
158
159    /** XXX
160       Preferable definitions for address and size would be as below. These
161       should be used as soon as the whole multi retype hack stuff is fixed:
162
163       address { mem_to_phys(listener + epoffset) };
164       size { epbuflen };
165
166       -MN
167    **/
168};
169
170/** Then, we go back to routine **/
171
172cap Frame from RAM from_self inherit Memory;
173
174cap Frame_Mapping from Frame inherit Mapping;
175
176cap DevFrame from PhysAddr from_self inherit Memory;
177
178cap DevFrame_Mapping from DevFrame inherit Mapping;
179
180cap Kernel is_always_copy {
181    /* Capability to a kernel */
182};
183
184
185/* x86_64-specific capabilities: */
186
187/* PML4 */
188cap VNode_x86_64_pml4 from RAM inherit VNode;
189
190cap VNode_x86_64_pml4_Mapping from VNode_x86_64_pml4 inherit Mapping;
191
192/* PDPT */
193cap VNode_x86_64_pdpt from RAM inherit VNode;
194
195cap VNode_x86_64_pdpt_Mapping from VNode_x86_64_pdpt inherit Mapping;
196
197/* Page directory */
198cap VNode_x86_64_pdir from RAM inherit VNode;
199
200cap VNode_x86_64_pdir_Mapping from VNode_x86_64_pdir inherit Mapping;
201
202/* Page table */
203cap VNode_x86_64_ptable from RAM inherit VNode;
204
205cap VNode_x86_64_ptable_Mapping from VNode_x86_64_ptable inherit Mapping;
206
207
208/* x86_32-specific capabilities: */
209
210/* PDPT */
211cap VNode_x86_32_pdpt from RAM inherit VNode;
212
213cap VNode_x86_32_pdpt_Mapping from VNode_x86_32_pdpt inherit Mapping;
214
215/* Page directory */
216cap VNode_x86_32_pdir from RAM inherit VNode;
217
218cap VNode_x86_32_pdir_Mapping from VNode_x86_32_pdir inherit Mapping;
219
220/* Page table */
221cap VNode_x86_32_ptable from RAM inherit VNode;
222
223cap VNode_x86_32_ptable_Mapping from VNode_x86_32_ptable inherit Mapping;
224
225/* ARM specific capabilities: */
226
227/* L1 Page Table */
228cap VNode_ARM_l1 from RAM inherit VNode {
229    size { objsize_vnode_arm_l1 };
230};
231
232cap VNode_ARM_l1_Mapping from VNode_ARM_l1 inherit Mapping;
233
234/* L2 Page Table */
235cap VNode_ARM_l2 from RAM inherit VNode {
236    size { objsize_vnode_arm_l2 };
237};
238
239cap VNode_ARM_l2_Mapping from VNode_ARM_l2 inherit Mapping;
240
241/* ARM AArch64-specific capabilities: */
242
243/* L0 Page Table */
244cap VNode_AARCH64_l0 from RAM inherit VNode;
245
246cap VNode_AARCH64_l0_Mapping from VNode_AARCH64_l0 inherit Mapping;
247
248/* L1 Page Table */
249cap VNode_AARCH64_l1 from RAM inherit VNode;
250
251cap VNode_AARCH64_l1_Mapping from VNode_AARCH64_l1 inherit Mapping;
252
253/* L2 Page Table */
254cap VNode_AARCH64_l2 from RAM inherit VNode;
255
256cap VNode_AARCH64_l2_Mapping from VNode_AARCH64_l2 inherit Mapping;
257
258/* L3 Page Table */
259cap VNode_AARCH64_l3 from RAM inherit VNode;
260
261cap VNode_AARCH64_l3_Mapping from VNode_AARCH64_l3 inherit Mapping;
262
263/** IRQTable and IO are slightly different **/
264
265cap IRQTable is_always_copy {
266    /* IRQ Routing table */
267    /**
268       When testing two IRQTable caps for is_copy, we always return True: all
269       IRQ entries originate from a single, primitive Cap. Grand'pa Cap, sort
270       of.
271    **/
272};
273
274cap IRQDest {
275	/* IRQ Destination capability.
276       Represents a slot in a CPUs int vector table.
277       Can be connected to a LMP endpoint to recv this interrupt. */
278    eq uint64 cpu;
279    eq uint64 vector;
280};
281
282cap IRQSrc from_self {
283	/* IRQ Source capability.
284       Represents an interrupt source. It contains a range of interrupt
285       source numbers. */ 
286	eq uint64 vec_start;
287	eq uint64 vec_end;
288};
289
290cap IO {
291    /* Legacy IO capability */
292    eq uint16 start;
293    eq uint16 end;          /* Granted IO range */
294};
295
296/* IPI notify caps */
297cap Notify_IPI {
298    eq coreid coreid;
299    eq uint16 chanid;
300};
301
302/* ID capability, system-wide unique */
303cap ID {
304    eq coreid coreid; /* core cap was created */
305    eq uint32 core_local_id; /* per core unique id */
306};
307
308cap PerfMon is_always_copy {
309};
310
311/** KernelControlBlock represents a struct kcb which contains all the pointers
312 *  to core-local global state of the kernel.
313 **/
314cap KernelControlBlock from RAM {
315    "struct kcb" kcb;
316
317    address { mem_to_phys(kcb) };
318    /* base page size for now so we can map the kcb in boot driver */
319    size { objsize_kcb };
320};
321
322cap IPI is_always_copy {};
323
324cap ProcessManager is_always_copy {
325    // Capability to act as process manager, i.e. create new domain caps.
326};
327
328cap Domain from ProcessManager {
329    eq coreid coreid;  /* Core where the domain was created. */
330    eq uint32 core_local_id;  /* Core-local ID of the domain. */
331};