1/*
2 * Copyright 2017, Data61
3 * Commonwealth Scientific and Industrial Research Organisation (CSIRO)
4 * ABN 41 687 119 230.
5 *
6 * This software may be distributed and modified according to the terms of
7 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
8 * See "LICENSE_BSD2.txt" for details.
9 *
10 * @TAG(DATA61_BSD)
11 */
12
13/* This template is meant to be used for components that are themselves dynamic systems
14 * and need to create seL4 objects dynamically at run time. This is *not* the standard
15 * use case for CAmkES and should only be used as a last resort if what you want is
16 * really not possible any other way. This template is also highly experimental and
17 * unsupported / undocumented */
18
19/*- if configuration[me.name].get('simple') -*/
20
21#include <autoconf.h>
22#include <sel4camkes/gen_config.h>
23#include <assert.h>
24#include <sel4/types.h>
25#include <sel4/sel4.h>
26#include <sel4utils/mapping.h>
27#include <stddef.h>
28#include <stdint.h>
29#include <camkes/error.h>
30#include <camkes/tls.h>
31#include <vka/kobject_t.h>
32
33#include <simple/simple.h>
34
35/*- set self_cnode = alloc_cap('cnode', my_cnode, write=true) -*/
36/*- set self_pd = alloc_cap('my_pd_cap', my_pd, write=true) -*/
37
38/*- if options.realtime -*/
39/*- if 'sched_ctrl' in configuration[me.name].keys() -*/
40    /*- set sched_control = alloc('sched_control', type=seL4_SchedControl, core=configuration[me.name].get('sched_ctrl')) -*/
41/*- endif -*/
42/*- endif -*/
43
44/*- set extrabi_list = [] -*/
45/*- for value in configuration[me.name].get('simple_extra_bootinfo',[]) -*/
46    /*- set name = value.strip('"') -*/
47    /*- set symbol = 'extra_bootinfo_frame_%d' % loop.index0 -*/
48    struct {
49        char content[PAGE_SIZE_4K];
50    } /*? symbol ?*/ ALIGN(PAGE_SIZE_4K) SECTION("align_12bit");
51    /*- do register_fill_frame(symbol, 'CDL_FrameFill_BootInfo %s' % name, 4096) -*/
52    /*- do extrabi_list.append((name, symbol)) -*/
53/*- endfor -*/
54
55/*# Find any untyped pools #*/
56/*- set untyped_obj_list = [] -*/
57/*- for attribute, value in configuration[me.name].items() -*/
58    /*- set r = re.match('simple_untyped(\\d+)_pool$', attribute) -*/
59    /*- if r is not none -*/
60        /*- set bits = int(r.group(1)) -*/
61        /*- for i in six.moves.range(value) -*/
62            /*- if not macros.min_untyped_size(options.architecture) <= bits <= macros.max_untyped_size(options.architecture) -*/
63                /*? raise(TemplateError('illegal untyped size')) ?*/
64            /*- endif -*/
65            /*- set untyped = alloc('simple_untyped_%d_pool_%d' % (bits, i), seL4_UntypedObject, size_bits=bits) -*/
66            /*- do untyped_obj_list.append((untyped, bits)) -*/
67        /*- endfor -*/
68    /*- endif -*/
69/*- endfor -*/
70
71/*# Find any configuration IO ports #*/
72/*- set ioports = [] -*/
73/*- set ioport_list = configuration[me.name].get('ioports') -*/
74/*- if ioport_list is not none -*/
75    /*- set ioport_list = ioport_list.strip('"').split(',') -*/
76    /*- for ioport in ioport_list -*/
77        /*- set start, end = ioport.split(':') -*/
78        /*- set start = int(start, 0) -*/
79        /*- set end = int(end, 0) -*/
80        /*- set ioport_cap = alloc("ioport%d_%d" % (start, end), seL4_IA32_IOPort, start_port=start, end_port=end + 1) -*/
81        /*- do ioports.append( (ioport_cap, start, end) ) -*/
82    /*- endfor -*/
83/*- endif -*/
84
85/*# Find any configuration mmio regions #*/
86/*- set mmio_regions = [] -*/
87/*- set mmio_region_list = configuration[me.name].get('mmios') -*/
88/*- if mmio_region_list is not none -*/
89    /*- for mmio_region in mmio_region_list -*/
90        /*- set paddr, size, bits = mmio_region.split(':') -*/
91        /*- do mmio_regions.append( (int(paddr, 0), int(size, 0),int(bits, 0)) ) -*/
92    /*- endfor -*/
93/*- endif -*/
94
95/*# Allocates capabilities for all the MMIO regions #*/
96/*- set mmio_caps_len = [] -*/
97/*# Map size to seL4 object. The arm HYP kernel has different sizes for
98    some objects. But as they do not overlap we can just include both
99    and rely on the component author to get it right #*/
100/*- set bits_to_frame_type = { 12:seL4_FrameObject, 20:seL4_ARM_SectionObject, 21:seL4_ARM_SectionObject } -*/
101/*- do mmio_caps_len.append(0) -*/
102/*- for paddr, size, bits in mmio_regions -*/
103    /*- set mmio_key = '0x%x_0x%x' % (paddr, size) -*/
104    static seL4_CPtr mmio_cap_lookup_/*? mmio_key ?*/[] = {
105    /*- for frame_offset in six.moves.range(0, size, 2 ** bits) -*/
106        /*- set frames = paddr + frame_offset -*/
107        /*- set temp_object=alloc_obj('mmio_frame_%d' % frames, bits_to_frame_type[bits], paddr=frames) -*/
108        /*- set temp_cap = alloc_cap('mmio_frame_%d' % frames, temp_object, read=true, write=true) -*/
109        /*? temp_cap ?*/,
110        /*- do mmio_caps_len.append(mmio_caps_len.pop() + 1) -*/
111    /*- endfor -*/
112    };
113/*- endfor -*/
114
115/*# Find an allocate untyped MMIO capabilities #*/
116/*- set untyped_mmio = [] -*/
117/*- set ut_mmio_list = configuration[me.name].get('untyped_mmios') -*/
118/*- if ut_mmio_list is not none -*/
119    /*- for ut_mmio in ut_mmio_list -*/
120        /*- set paddr, size_bits = ut_mmio.split(':') -*/
121        /*- set paddr = int(paddr, 0) -*/
122        /*- set size_bits = int(size_bits, 0) -*/
123        /*- set cap = alloc('untyped_cap_0x%x' % paddr, seL4_UntypedObject, paddr = paddr, size_bits = size_bits) -*/
124        /*- do untyped_mmio.append( (paddr, size_bits, cap) ) -*/
125    /*- endfor -*/
126/*- endif -*/
127
128/*# Allocate any IOSpace caps #*/
129/*- set iospaces = [] -*/
130/*- set iospace_list = configuration[me.name].get('iospaces') -*/
131/*- if iospace_list is not none -*/
132    /*- set iospace_list = iospace_list.strip('"').split(',') -*/
133    /*- for iospace in iospace_list -*/
134        /*- set domain, bus, dev, fun = iospace.split(':') -*/
135        /*- set domain = int(domain, 0) -*/
136        /*- set bus = int(bus, 0) -*/
137        /*- set dev = int(dev, 0) -*/
138        /*- set fun = int(fun, 0) -*/
139        /*- set pciid = bus * 256 + dev * 8 + fun -*/
140        /*- set devid = domain * 65536 + pciid -*/
141        /*- set iospace_cap = alloc('iospace_%d' % devid, seL4_IA32_IOSpace, domainID=domain, bus=bus, dev=dev, fun=fun) -*/
142        /*- do iospaces.append((devid, iospace_cap)) -*/
143    /*- endfor -*/
144/*- endif -*/
145
146/*# Allocate any SMMU caps #*/
147/*- for smmu in configuration[me.name].get('smmu',[]) -*/
148    /*- set smmu_cap = alloc('smmu_%d' % smmu, seL4_ARM_IOSpace, iospace=smmu) -*/
149    /*- do iospaces.append((smmu, smmu_cap)) -*/
150/*- endfor -*/
151
152/*# Allocate asid pool cap #*/
153/*- if configuration and configuration[me.name].get('asid_pool') -*/
154    /*- set asidpool = alloc('asid_pool', seL4_ASID_Pool) -*/
155/*- endif -*/
156
157/*- set irq_notification_object = alloc_obj('irq_notification_obj', seL4_NotificationObject) -*/
158/*- set irq_notification = alloc_cap('irq_notification_obj', irq_notification_object, read=True) -*/
159/*- set irqs = [] -*/
160/*- set irq_list = configuration[me.name].get('irqs') -*/
161/*- if irq_list is not none -*/
162    /*- for irq in irq_list -*/
163        /*- set irq_cap = alloc('irq_%d' % irq, seL4_IRQHandler, number=irq, notification=my_cnode[irq_notification]) -*/
164        /*- do irqs.append( (irq, irq_cap) ) -*/
165    /*- endfor -*/
166/*- endif -*/
167
168/*# No cap allocation from here on! We assume all caps exist so we can guess our cnode size from the
169 * holding slot #*/
170/*- set holding_slot = alloc_cap('temporary_simple_slot', None) -*/
171
172/*# We need to have a known cspace size to instantiate a simple. This logic is
173    more complicated than it strictly needs to be since in practice camkes will
174    always have an 'auto' size, but it does not hurt to be general here #*/
175/*- if cap_space.cnode.size_bits == 'auto' -*/
176    /*- set size_bits = configuration[me.name].get('cnode_size_bits') -*/
177    /*- if size_bits is not none -*/
178        /*- set cnodesize = size_bits -*/
179    /*- else -*/
180        /*# We will determine the size at run time #*/
181        /*- set cnodesize = None -*/
182    /*- endif -*/
183/*- else -*/
184    /*- set cnodesize = cap_space.cnode.size_bits -*/
185/*- endif -*/
186
187/* Static declaration for our cap information. We will populate this when we make
188 * the simple */
189typedef struct camkes_untyped {
190    seL4_CPtr cptr;
191    uintptr_t paddr;
192    int size_bits;
193    int device;
194} camkes_untyped_t;
195typedef struct camkes_simple_data {
196/*- if cnodesize is none -*/
197    int cnodesizebits;
198/*- endif -*/
199    camkes_untyped_t untyped[/*? len(untyped_obj_list) + len(untyped_mmio) ?*/];
200    seL4_CPtr inittcb;
201    seL4_CPtr initsc;
202} camkes_simple_data_t;
203static camkes_simple_data_t simple_data;
204static bool camkes_simple_init = false;
205
206static int simple_camkes_untyped_count(void *data) {
207    return /*? len(untyped_obj_list) + len(untyped_mmio) ?*/;
208}
209
210static int simple_camkes_cap_count(void *data) {
211    /*# untypeds + mmio +ioports + cnode + pd + iospaces + holding #*/
212    return /*? len(untyped_obj_list) + mmio_caps_len[0] + len(ioports) + len(iospaces) + len(untyped_mmio) + 3 ?*/;
213}
214
215static seL4_CPtr simple_camkes_nth_untyped(void *data, int n, size_t *size_bits, uintptr_t *paddr, bool *device) {
216    camkes_simple_data_t *camkes = (camkes_simple_data_t *)data;
217    if (size_bits) {
218        *size_bits = (size_t)camkes->untyped[n].size_bits;
219    }
220    if (paddr) {
221        *paddr = camkes->untyped[n].paddr;
222    }
223    if (device) {
224        *device = camkes->untyped[n].device;
225    }
226    return camkes->untyped[n].cptr;
227}
228
229static seL4_Error simple_camkes_get_frame_cap(void *data, void *paddr, int size_bits, cspacepath_t *path) {
230    /*- if len(mmio_regions) > 0 -*/
231        /*- for paddr, size, bits in mmio_regions -*/
232            /*- set mmio_key = '0x%x_0x%x' % (paddr, size) -*/
233            if ((uintptr_t)paddr >= (uintptr_t)/*? paddr ?*/ && (uintptr_t)paddr < (uintptr_t)/*? paddr ?*/ + (uintptr_t)/*? size ?*/ && size_bits == /*? bits ?*/) {
234                return seL4_CNode_Copy(path->root, path->capPtr, path->capDepth, /*? self_cnode ?*/, mmio_cap_lookup_/*? mmio_key ?*/[((uintptr_t)paddr - (uintptr_t)/*? paddr ?*/) >> /*? bits ?*/], CONFIG_WORD_SIZE, seL4_AllRights);
235            }
236        /*- endfor -*/
237    /*- endif -*/
238    return seL4_FailedLookup;
239}
240
241static seL4_CPtr simple_camkes_nth_cap(void *data, int n) {
242    camkes_simple_data_t *camkes = (camkes_simple_data_t *)data;
243    switch(n) {
244    case 0:
245        return /*? self_cnode ?*/;
246    case 1:
247        return /*? self_pd ?*/;
248    /*- if len(untyped_obj_list) > 0 -*/
249        case 2 ... /*? len(untyped_obj_list) + 1 ?*/:
250            return camkes->untyped[n - 2].cptr;
251    /*- endif -*/
252    /*- set mmio_counter = [] -*/
253    /*- do mmio_counter.append(0) -*/
254    /*- for paddr, size, bits in mmio_regions -*/
255        /*- set mmio_key = '0x%x_0x%x' % (paddr, size) -*/
256        /*- set mmio_range_len = len(list(six.moves.range(0, size, 2 ** bits))) -*/
257        case /*? 2 + len(untyped_obj_list) + mmio_counter[0] ?*/ ... /*? 2 + len(untyped_obj_list) + mmio_counter[0] + mmio_range_len - 1 ?*/:
258            return mmio_cap_lookup_/*? mmio_key ?*/[n - /*? 2 + len(untyped_obj_list) + mmio_counter[0] ?*/];
259        /*- do mmio_counter.append(mmio_counter.pop() + mmio_range_len) -*/
260    /*- endfor -*/
261    /*- for cap, start, end in ioports -*/
262        case /*? 2 + len(untyped_obj_list) + mmio_caps_len[0] + loop.index0 ?*/:
263            return /*? cap ?*/;
264    /*- endfor -*/
265    /*- for devid, cap in iospaces -*/
266        case /*? 2 + len(untyped_obj_list) + mmio_caps_len[0] + len(ioports) + loop.index0 ?*/:
267            return /*? cap ?*/;
268    /*- endfor -*/
269    /*- for paddr, size, cap in untyped_mmio -*/
270        case /*? 2 + len(untyped_obj_list) + mmio_caps_len[0] + len(ioports) + len(iospaces) + loop.index0 ?*/:
271            return /*? cap ?*/;
272    /*- endfor -*/
273    case /*? len(untyped_obj_list) + mmio_caps_len[0] + len(ioports) + len(iospaces) + len(untyped_mmio) + 2 ?*/:
274        /*# The last cap we report is the magic holding slot we allocated.
275         * technically this slot is probably free since we should have
276         * deleted whatever was there. But this should also be the largest
277         * cptr allocated, so is convenient to return it as the last cap #*/
278        return /*? holding_slot ?*/;
279    default:
280        assert(!"Invalid cap requested");
281    }
282    return 0;
283}
284
285static seL4_CPtr simple_camkes_init_cap(void *data, seL4_CPtr cap) {
286    camkes_simple_data_t *camkes = (camkes_simple_data_t *)data;
287    switch(cap) {
288    case seL4_CapInitThreadCNode:
289        return /*? self_cnode ?*/;
290    case seL4_CapInitThreadPD:
291        return /*? self_pd ?*/;
292    case seL4_CapInitThreadTCB:
293        return camkes->inittcb;
294    /*- if options.realtime -*/
295    case seL4_CapInitThreadSC:
296        return camkes->initsc;
297    /*- endif -*/
298    default:
299        assert(!"Unsupported init_cap requested");
300    }
301    return 0;
302}
303
304static uint8_t simple_camkes_cnode_size(void *data) {
305    /*- if cnodesize is none -*/
306        camkes_simple_data_t *camkes = (camkes_simple_data_t *)data;
307        return camkes->cnodesizebits;
308    /*- else -*/
309        return /*? cnodesize ?*/;
310    /*- endif -*/
311}
312
313static seL4_Error simple_camkes_get_IOPort_cap(void *data, uint16_t start_port, uint16_t end_port, seL4_Word root, seL4_Word dest, seL4_Word depth) {
314    assert(start_port <= end_port);
315    seL4_CPtr cap = seL4_CapNull;
316    /*- for cap, start, end in ioports -*/
317        if (start_port >= /*? start ?*/ && end_port <= /*? end ?*/) {
318            cap = /*? cap ?*/;
319        }
320    /*- endfor -*/
321    if (cap == seL4_CapNull) {
322        ERR(camkes_error, ((camkes_error_t){
323                .type = CE_ALLOCATION_FAILURE,
324                .instance = "/*? me.name ?*/",
325                .description = "unable to find IO port cap",
326            }), ({
327                return seL4_FailedLookup;
328            }));
329        return seL4_FailedLookup;
330    }
331    return seL4_CNode_Copy(root, dest, depth, /*? self_cnode ?*/, cap, CONFIG_WORD_SIZE, seL4_AllRights);
332}
333
334#ifdef CONFIG_IOMMU
335static seL4_Error simple_camkes_get_iospace(void *data, uint16_t domainID, uint16_t deviceID, cspacepath_t *path) {
336    /*- if len(iospaces) > 0 -*/
337        uint32_t devid = ((uint32_t)domainID << 16) | (uint32_t)deviceID;
338        seL4_CPtr cap;
339        switch(devid) {
340        /*- for devid, cap in iospaces -*/
341            case /*? devid ?*/:
342                cap = /*? cap ?*/;
343                break;
344        /*- endfor -*/
345            default:
346                return seL4_FailedLookup;
347        }
348        return seL4_CNode_Copy(path->root, path->capPtr, path->capDepth, /*? self_cnode ?*/, cap, CONFIG_WORD_SIZE, seL4_AllRights);
349    /*- else -*/
350        return seL4_FailedLookup;
351    /*- endif -*/
352}
353#endif
354
355#ifdef CONFIG_TK1_SMMU
356static seL4_Error simple_camkes_get_iospace_cap_count(void *data, int *count) {
357    if (count) {
358        *count = /*? len(iospaces) ?*/;
359    }
360    return seL4_NoError;
361}
362
363static seL4_CPtr simple_camkes_get_iospace_nth_cap(void *data, int n) {
364    /*- if len(iospaces) > 0 -*/
365        switch (n) {
366        /*- for smmu, cap in iospaces -*/
367            case /*? loop.index0 ?*/:
368                return /*? cap ?*/;
369        /*- endfor -*/
370        default:
371            return 0;
372        }
373    /*- else -*/
374        return 0;
375    /*- endif -*/
376}
377#endif
378
379static void simple_camkes_print(void *data) {
380    printf("camkes is too cool to print out simple information\n");
381}
382
383static seL4_Error simple_camkes_set_ASID(void *data, seL4_CPtr vspace) {
384    /*- if configuration[me.name].get('asid_pool') -*/
385#ifdef CONFIG_ARCH_X86
386        return seL4_X86_ASIDPool_Assign(/*? asidpool ?*/, vspace);
387#elif CONFIG_ARCH_ARM
388        return seL4_ARM_ASIDPool_Assign(/*? asidpool ?*/, vspace);
389#endif
390    /*- else -*/
391        return seL4_FailedLookup;
392    /*- endif -*/
393}
394
395static seL4_Error simple_camkes_get_irq(void *data, int irq, seL4_CNode cnode, seL4_Word index, uint8_t depth) {
396    /*- if len(irqs) > 0 -*/
397        switch(irq) {
398        /*- for irq,cap in irqs -*/
399            case /*? irq ?*/:
400                return seL4_CNode_Copy(cnode, index, depth, /*? self_cnode ?*/, /*? cap ?*/, CONFIG_WORD_SIZE, seL4_AllRights);
401        /*- endfor -*/
402            default:
403                return seL4_FailedLookup;
404        }
405    /*- else -*/
406        return seL4_FailedLookup;
407    /*- endif -*/
408}
409
410static uintptr_t make_frame_get_paddr(seL4_CPtr untyped) {
411    int type;
412    int error;
413    uintptr_t ret;
414    type = seL4_ARCH_4KPage;
415#ifdef CONFIG_KERNEL_STABLE
416    error = seL4_Untyped_RetypeAtOffset(untyped, type, 0, 12, /*? self_cnode ?*/, 0, 0, /*? holding_slot ?*/, 1);
417#else
418    error = seL4_Untyped_Retype(untyped, type, 12, /*? self_cnode ?*/, 0, 0, /*? holding_slot ?*/, 1);
419#endif
420    ERR_IF(error != seL4_NoError, camkes_error, ((camkes_error_t){
421            .type = CE_SYSCALL_FAILED,
422            .instance = "/*? me.name ?*/",
423            .description = "failed to retype an untyped while trying to determine its physical address",
424            .syscall = UntypedRetype,
425            .error = error,
426        }), ({
427            return (uintptr_t)NULL;
428        }));
429    seL4_ARCH_Page_GetAddress_t res = seL4_ARCH_Page_GetAddress(/*? holding_slot ?*/);
430    ret = res.paddr;
431    ERR_IF(ret == 0, camkes_error, ((camkes_error_t){
432            .type = CE_SYSCALL_FAILED,
433            .instance = "/*? me.name ?*/",
434            .description = "failed to retrieve the physical address of a temporary frame",
435            .syscall = ARCHPageGetAddress,
436            .error = res.error,
437        }), ({
438            return (uintptr_t)NULL;
439        }));
440    seL4_CNode_Delete(/*? self_cnode ?*/, /*? holding_slot ?*/, CONFIG_WORD_SIZE);
441    return ret;
442}
443
444static void camkes_make_arch_simple(arch_simple_t *simple) {
445    simple->irq = &simple_camkes_get_irq;
446#ifdef CONFIG_IOMMU
447    simple->iospace = &simple_camkes_get_iospace;
448#endif
449/*- if options.architecture in ('ia32', 'x86_64') -*/
450    simple->IOPort_cap = &simple_camkes_get_IOPort_cap;
451/*- endif -*/
452}
453
454static ssize_t camkes_get_extended_bootinfo(void *data, seL4_Word type, void *dest, ssize_t max_len) {
455    seL4_BootInfoHeader *mapping = NULL;
456    /*- for name, symbol in extrabi_list -*/
457    if (type == /*? name ?*/) {
458        mapping = (seL4_BootInfoHeader*)&/*? symbol ?*/.content[0];
459    }
460    /*- endfor -*/
461    if (mapping && mapping->len != -1) {
462        ssize_t len = MIN(mapping->len, max_len);
463        memcpy(dest, mapping, len);
464        return len;
465    }
466    return -1;
467}
468
469static UNUSED seL4_CPtr camkes_simple_sched_ctrl(void *data, int core) {
470    /*- if options.realtime -*/
471    /*- if 'sched_ctrl' in configuration[me.name].keys() -*/
472    if (core == /*? configuration[me.name].get('sched_ctrl') ?*/) {
473        return /*? sched_control ?*/;
474    }
475    /*- endif -*/
476    /*- endif -*/
477    return seL4_CapNull;
478}
479
480static int camkes_simple_core_count(void *data) {
481    return CONFIG_MAX_NUM_NODES;
482}
483
484void camkes_make_simple(simple_t *simple) {
485    if (!camkes_simple_init) {
486        /*- if cnodesize is none -*/
487            /* Guess the size of our cnode by rounding */
488            /*# If there is no size specified in the configuration then we assume the cnode
489                will be as small as possible to hold all the capabilities that are currently
490                defined #*/
491            simple_data.cnodesizebits = CONFIG_WORD_SIZE - __builtin_clz(/*? holding_slot ?*/) + 1;
492        /*- endif -*/
493        /*# Find untyped physical addresses. We only care if the untyped is at least a page size #*/
494        /*- for u in untyped_obj_list -*/
495            /*- if u[1] >= 12 -*/
496                simple_data.untyped[/*? loop.index0 ?*/] = (camkes_untyped_t) {.cptr = /*? u[0] ?*/, .paddr = make_frame_get_paddr(/*? u[0] ?*/), .size_bits = /*? u[1] ?*/, .device = false};
497            /*- endif -*/
498        /*- endfor -*/
499        /*- for paddr, size_bits, cap in untyped_mmio -*/
500            simple_data.untyped[/*? loop.index0 + len(untyped_obj_list) ?*/] = (camkes_untyped_t){.cptr = /*? cap ?*/, .paddr = /*? paddr ?*/, .size_bits = /*? size_bits ?*/, .device = true};
501        /*- endfor -*/
502        camkes_simple_init = true;
503    }
504    /* Assume we are called from init */
505    simple_data.inittcb = camkes_get_tls()->tcb_cap;
506    simple_data.initsc = camkes_get_tls()->sc_cap;
507    simple->data = &simple_data;
508    simple->frame_info = /*&simple_camkes_get_frame_info*/NULL;
509    simple->frame_cap = &simple_camkes_get_frame_cap;
510    simple->frame_mapping = /*&simple_camkes_get_frame_mapping*/NULL;
511    simple->ASID_assign = &simple_camkes_set_ASID;
512    simple->cap_count = &simple_camkes_cap_count;
513    simple->nth_cap = &simple_camkes_nth_cap;
514    simple->init_cap = &simple_camkes_init_cap;
515    simple->cnode_size = &simple_camkes_cnode_size;
516    simple->untyped_count = &simple_camkes_untyped_count;
517    simple->nth_untyped = &simple_camkes_nth_untyped;
518    simple->userimage_count = /*&simple_camkes_userimage_count*/NULL;
519    simple->nth_userimage = /*&simple_camkes_nth_userimage*/NULL;
520    simple->extended_bootinfo = &camkes_get_extended_bootinfo;
521#ifdef CONFIG_KERNEL_MCS
522    simple->sched_ctrl = &camkes_simple_sched_ctrl;
523    simple->core_count = &camkes_simple_core_count;
524#endif
525#ifdef CONFIG_TK1_SMMU
526    simple->arch_simple.iospace_cap_count = simple_camkes_get_iospace_cap_count;
527    simple->arch_simple.iospace_get_nth_cap = simple_camkes_get_iospace_nth_cap;
528#endif
529    simple->print = &simple_camkes_print;
530
531    camkes_make_arch_simple(&simple->arch_simple);
532}
533
534/*- endif -*/
535