1#!/usr/bin/env python 2# -*- coding: utf-8 -*- 3 4# 5# Copyright 2017, Data61 6# Commonwealth Scientific and Industrial Research Organisation (CSIRO) 7# ABN 41 687 119 230. 8# 9# This software may be distributed and modified according to the terms of 10# the BSD 2-Clause license. Note that NO WARRANTY is provided. 11# See "LICENSE_BSD2.txt" for details. 12# 13# @TAG(DATA61_BSD) 14# 15 16''' 17The jinja2 template code runs in a very restricted environment during 18rendering. For example, you can't call functions like `map`. To expose certain 19functions to the template code we need to explicitly pass these in during 20rendering. This module encapsulates extra context elements we want to make 21available to the template code. 22''' 23 24from __future__ import absolute_import, division, print_function, \ 25 unicode_literals 26from camkes.internal.seven import cmp, filter, map, zip 27 28from functools import partial 29import capdl 30import code 31import collections 32import copy 33import inspect 34import itertools 35import functools 36import numbers 37import \ 38 orderedset, os, pdb, re, six, sys, textwrap, math 39from capdl.Object import ObjectType, ObjectRights, ARMIRQMode 40from capdl.Allocator import Cap 41from capdl import page_sizes 42 43# Depending on what kernel branch we are on, we may or may not have ASIDs. 44# There are separate python-capdl branches for this, but this import allows us 45# to easily interoperate with both. 46try: 47 from capdl.Allocator import seL4_ASID_Pool 48except ImportError: 49 seL4_ASID_Pool = None 50 51import camkes.ast as AST 52from camkes.internal.Counter import Counter 53from camkes.templates import macros, TemplateError 54 55 56def new_context(entity, assembly, render_state, state_key, outfile_name, 57 **kwargs): 58 '''Create a new default context for rendering.''' 59 60 obj_space = render_state.obj_space if render_state else None 61 cap_space = render_state.cspaces[state_key] if state_key and render_state else None 62 addr_space = render_state.addr_spaces[state_key] if state_key and render_state else None 63 64 return dict(list(__builtins__.items()) + list(ObjectType.__members__.items()) + list(ObjectRights.__members__.items()) + list(ARMIRQMode.__members__.items()) + list({ 65 # Kernel object allocator 66 'alloc_obj': ( 67 lambda name, type, label=entity.label(), **kwargs: 68 alloc_obj((entity.label(), obj_space), obj_space, 69 '%s_%s' % (entity.label(), name), type, label, 70 **kwargs)) 71 if obj_space else None, 72 73 # Cap allocator 74 'alloc_cap': None if cap_space is None else \ 75 (lambda name, obj, **kwargs: alloc_cap((entity.label(), 76 cap_space), cap_space, name, obj, **kwargs)), 77 78 'Cap': Cap, 79 80 # The CNode root of your CSpace. Should only be necessary in cases 81 # where you need to allocate a cap to it. 82 'my_cnode': None if cap_space is None else cap_space.cnode, 83 84 # Batched object and cap allocation for when you don't need a reference 85 # to the object. Probably best not to look directly at this one. When 86 # you see `set y = alloc('foo', bar, moo)` in template code, think: 87 # set x = alloc_obj('foo_obj', bar) 88 # set y = alloc_cap('foo_cap', x, moo) 89 'alloc': None if cap_space is None else \ 90 (lambda name, type, label=entity.label(), **kwargs: 91 alloc_cap((entity.label(), cap_space), cap_space, name, 92 alloc_obj((entity.label(), obj_space), obj_space, '%s_%s' % 93 (entity.label(), name), type, label, **kwargs), 94 **kwargs)), 95 96 # Functionality for templates to inform us that they've emitted a C 97 # variable that's intended to map to a shared variable. It is 98 # (deliberately) left to the template authors to ensure global names 99 # (gnames) only collide when intended; i.e. when they should map to the 100 # same shared variable. The local name (lname) will later be used by us 101 # to locate the relevant ELF frame(s) to remap. Note that we assume 102 # address spaces and CSpaces are 1-to-1. 103 'register_shared_variable': None if cap_space is None else \ 104 (lambda global_name, symbol, size, frame_size=None, paddr=None, 105 perm='RWX', cached=True, label=entity.parent.label(), with_mapping_caps=None: 106 register_shared_variable( 107 addr_space, obj_space, global_name, symbol, size, cap_space, 108 frame_size, paddr, perm, cached, label, with_mapping_caps)), 109 110 'get_shared_variable_backing_frames': None if cap_space is None else \ 111 (lambda global_name, size, frame_size=None, label=entity.parent.label(): 112 get_shared_variable_backing_frames( 113 obj_space, global_name, size, frame_size, label)), 114 115 # Get the object-label mapping for our verification models. 116 'object_label_mapping': (lambda: object_label_mapping(obj_space)), 117 118 # Function for templates to inform us that they would like certain 119 # 'fill' information to get placed into the provided symbol. Provided 120 # symbol should be page size and aligned. The 'fill' parameter is 121 # an arbitrary string that will be set as the 'fill' parameter on the 122 # capDL frame object. The meaning of fill is completely dependent 123 # on the underlying loader 124 'register_fill_frame': (lambda symbol, fill, size=4096: 125 register_fill_frame(addr_space, symbol, fill, size, obj_space, entity.label())), 126 127 'register_stack_symbol': (lambda symbol, size: 128 register_stack_symbol(addr_space, symbol, size, obj_space, entity.label())), 129 130 'register_ipc_symbol': (lambda symbol, frame: 131 register_ipc_symbol(addr_space, symbol, frame)), 132 133 'register_dma_pool': (lambda symbol, page_size, caps: 134 register_dma_pool(addr_space, symbol, page_size, caps, cap_space)), 135 136 # A `self`-like reference to the current AST object. It would be nice 137 # to actually call this `self` to lead to more pythonic templates, but 138 # `self` inside template blocks refers to the jinja2 parser. 139 'me': entity, 140 141 # The AST assembly's configuration. 142 'configuration': assembly.configuration, 143 144 # The AST assembly's composition 145 'composition': assembly.composition, 146 147 # Cross-template variable passing helpers. These are quite low-level. 148 # Avoid calling them unless necessary. 149 'stash': partial(stash, entity.label()), 150 'pop': partial(pop, entity.label()), 151 'guard': partial(guard, entity.label()), 152 153 # If the previous group of functions are considered harmful, these are 154 # to be considered completely off limits. These expose a mechanism for 155 # passing data between unrelated templates (_stash and _pop) and a way 156 # of running arbitrary Python statements and expressions. They come 157 # with significant caveats. E.g. _stash and _pop will likely not behave 158 # as expected with the template cache enabled. 159 '_stash': partial(stash, ''), 160 '_pop': partial(pop, ''), 161 'exec': _exec, 162 163 # Helpers for creating unique symbols within templates. 164 'c_symbol': partial(symbol, '_camkes_%(tag)s_%(counter)d'), 165 'isabelle_symbol': partial(symbol, '%(tag)s%(counter)d\'', 's'), 166 167 # Expose some library functions 168 'assert': _assert, 169 'itertools': itertools, 170 'functools': functools, 171 'lambda': lambda s: eval('lambda %s' % s), 172 'numbers': numbers, 173 'os': os, 174 'pdb': pdb, 175 'raise': _raise, 176 're': re, 177 'six': six, 178 'set': orderedset.OrderedSet, 179 'textwrap': textwrap, 180 'copy': copy, 181 'zip': zip, 182 'math': math, 183 'enumerate': enumerate, 184 185 # Allocation pools. In general, do not touch these in templates, but 186 # interact with them through the alloc* functions. They are only in the 187 # context to allow unanticipated template extensions. 188 'obj_space': obj_space, 189 'cap_space': cap_space, 190 191 # Debugging functions 192 'breakpoint': _breakpoint, 193 'sys': sys, 194 195 # Work around for Jinja's bizarre scoping rules. 196 'Counter': Counter, 197 198 # Return a list of distinct elements. Normally you would just do this 199 # as list(set(xs)), but this turns out to be non-deterministic in the 200 # template environment for some reason. 201 'uniq': lambda xs: functools.reduce(lambda ys, z: ys if z in ys else (ys + [z]), xs, []), 202 203 # Functional helpers. 204 'flatMap': lambda f, xs: list(itertools.chain.from_iterable(map(f, xs))), 205 'flatten': lambda xss: list(itertools.chain.from_iterable(xss)), 206 207 # Macros for common operations. 208 'macros': macros, 209 210 # Macro shorthands for mangling Isabelle identifiers. 211 'isabelle_identifier': macros.isabelle_ident, 212 'isabelle_component': macros.isabelle_ADL_ident('component'), 213 'isabelle_instance': macros.isabelle_ADL_ident('instance'), 214 'isabelle_connector': macros.isabelle_ADL_ident('connector'), 215 'isabelle_connection': macros.isabelle_ADL_ident('connection'), 216 'isabelle_procedure': macros.isabelle_ADL_ident('procedure'), 217 'isabelle_event': macros.isabelle_ADL_ident('event'), 218 'isabelle_dataport': 219 lambda name: macros.isabelle_ADL_ident('dataport')( 220 # hack to fix up names for sized buffer types e.g. 'Buf(4096)' -> 'Buf_4096' 221 re.sub(r'\((.*)\)', r'_\1', name)), 222 223 'isabelle_capdl_identifier': macros.isabelle_ident, 224 225 # Add extra policy edges to help the cdl-refine verification. 226 'add_policy_extra': lambda x, auth, y: render_state.policy_extra.add((x, auth, y)), 227 'get_policy_extra': lambda: set(render_state.policy_extra), 228 229 # This function abstracts away the differences between the RT kernel's 230 # seL4_Recv and the master kernel's seL4_Recv. Namely, the RT kernel's 231 # seL4_Recv takes an extra reply object cap. 232 # 233 # seL4_Recv is distinct from seL4_Wait, in that a seL4_Recv() call 234 # expects to potentially get a reply cap from the sender. 235 'generate_seL4_Recv': generate_seL4_Recv, 236 237 # This function is similar to generate_seL4_Recv, in that it also 238 # abstracts away the differences between the RT and master kernels. 239 # This function specifically abstracts away the differences between 240 # seL4_SignalRecv (on master) and seL4_NBSendRecv (on RT). 241 'generate_seL4_SignalRecv': generate_seL4_SignalRecv, 242 243 # This function is similar to generate_seL4_Recv as well, but it 244 # abstracts away the differences between seL4_ReplyRecv between the 245 # RT and master branches. 246 'generate_seL4_ReplyRecv': generate_seL4_ReplyRecv, 247 248 # Give template authors access to AST types just in case. Templates 249 # should never be constructing objects of these types, but they may 250 # need to do `isinstance` testing. 251 'camkes': collections.namedtuple('camkes', ['ast'])(AST), 252 253 # Expose CapDL module for `isinstance` testing. 254 'capdl': capdl, 255 256 # Give the template authors a mechanism for writing C-style include 257 # guards. Use the following idiom to guard an include target: 258 # /*- if 'template.filename' not in included' -*/ 259 # /*- do included.add('template.filename') -*/ 260 # ... my template ... 261 # /*- endif -*/ 262 'included': set(), 263 264 # Expose an exception class templates can use to throw errors related 265 # to invalid input specification. 266 'TemplateError': TemplateError, 267 268 # Output filename (mainly needed by Isabelle templates) 269 # Currently only supported for misc templates. 270 'outfile_name': outfile_name, 271 272 # FIXME: these are currently used in cdl-refine.thy, 273 # but should be done in a cleaner way. 274 'is_IRQ_object': lambda obj: isinstance(obj, capdl.IRQ), 275 'is_ASIDPool_object': lambda obj: isinstance(obj, capdl.ASIDPool), 276 }.items()) + list(kwargs.items())) 277 278 279# For all three of these functions below, for the 'badge_var_name' variable, 280# be sure that you pass in an ampersand character prefixed to the argument if 281# your badge variable isn't a pointer. 282 283 284def generate_seL4_Recv(options, ep_cap, badge_var_name, reply_cap): 285 if options.realtime: 286 return 'seL4_Recv(%s, %s, %s)' % (ep_cap, badge_var_name, reply_cap) 287 else: 288 return 'seL4_Recv(%s, %s)' % (ep_cap, badge_var_name) 289 290 291def generate_seL4_SignalRecv(options, res_msginfo_var_name, dest_ntfn_cap, dest_msginfo_var_name, src_ep_cap, badge_var_name, reply_cap): 292 if options.realtime: 293 return '%s = seL4_NBSendRecv(%s, %s, %s, %s, %s)' % (res_msginfo_var_name, dest_ntfn_cap, dest_msginfo_var_name, src_ep_cap, badge_var_name, reply_cap) 294 else: 295 return 'seL4_Signal(%s); %s = seL4_Recv(%s, %s)' % (dest_ntfn_cap, res_msginfo_var_name, src_ep_cap, badge_var_name) 296 297 298def generate_seL4_ReplyRecv(options, src_ep_cap, dest_msginfo_var_name, badge_var_name, reply_cap): 299 if options.realtime: 300 return 'seL4_ReplyRecv(%s, %s, %s, %s)' % (src_ep_cap, dest_msginfo_var_name, badge_var_name, reply_cap) 301 else: 302 return 'seL4_ReplyRecv(%s, %s, %s)' % (src_ep_cap, dest_msginfo_var_name, badge_var_name) 303 304 305def _assert(condition, msg=None): 306 '''Hack to reify assert as a callable''' 307 if msg is not None: 308 assert condition, msg 309 else: 310 assert condition 311 return '' 312 313 314def _exec(statement): 315 '''Hack to reify exec as a callable''' 316 # Jinja seems to invoke this through a variable level of indirection. 317 # Search up our stack for the caller's context, identifiable by their 'me' 318 # variable. This is a bit fragile, but since _exec should only be a tool of 319 # last resort, I think it's acceptable. 320 stack_frames = inspect.stack() 321 caller = None 322 for i, f in enumerate(stack_frames): 323 if 'me' in f[0].f_locals: 324 # Found it. 325 caller = i 326 break 327 if caller is None: 328 raise Exception('_exec: failed to find caller\'s context') 329 six.exec_(statement, stack_frames[caller][0].f_globals, 330 stack_frames[caller][0].f_locals) 331 return '' 332 333 334def _raise(exception): 335 '''Hack to reify raise as a callable''' 336 if isinstance(exception, Exception): 337 raise exception 338 else: 339 assert hasattr(exception, '__call__') 340 raise exception() 341 return '' 342 343 344def _breakpoint(): 345 '''Debugging function to be called from templates. This drops you into the 346 Python interpreter with a brief attempt to align your locals() with the 347 template's.''' 348 kwargs = { 349 'banner': 'Breakpoint triggered', 350 } 351 352 # Try and locate the stack frame containing the template context. This is a 353 # bit error prone, but it's nice if we can find it because then we can fake 354 # the template context to the interpreter prompt. 355 for f in inspect.stack(): 356 if 'context' in f[0].f_locals: 357 kwargs['local'] = f[0].f_globals.copy() 358 kwargs['local'].update(f[0].f_locals['context']) 359 break 360 361 code.interact(**kwargs) 362 363 # It's possible the template called this from inside a /*? ?*/ block, so 364 # make sure we don't mess up the output: 365 return '' 366 367 368# Functionality for carrying variables between related templates. The idea is 369# that one template performs stash('foo', 'bar') to save 'bar' and the other 370# template performs pop('foo') to retrieve 'bar'. This pattern relies on the 371# order of instantiation of templates. To avoid this, use the guard function 372# below. See the templates for examples. 373store = {} 374 375 376def stash(client, key, value): 377 if client not in store: 378 store[client] = {} 379 store[client][key] = value 380 return '' 381 382 383def pop(client, key): 384 if client not in store or key not in store[client]: 385 return None 386 value = store[client][key] 387 del store[client][key] 388 if not store[client]: 389 del store[client] 390 return value 391 392 393def guard(client, func, key, **kwargs): 394 '''Retrieve the value for key from the stash. If it does not exist, call 395 func to get a value. In either event re-stash the resulting value under the 396 same key and return it.''' 397 value = pop(client, key) 398 if value is None: 399 value = func(**kwargs) 400 stash(client, key, value) 401 return value 402 403 404symbol_counter = 0 405 406 407def symbol(pattern, default_tag='', tag=None): 408 '''Allocate a symbol to be used in a template. This is useful for avoiding 409 colliding with user symbols.''' 410 global symbol_counter 411 s = pattern % { 412 'counter': symbol_counter, 413 'tag': tag or default_tag, 414 } 415 symbol_counter += 1 416 return s 417 418 419def alloc_obj(client, space, name, type, label=None, **kwargs): 420 '''Guarded allocation of an object. That is, if the object we're trying to 421 allocate already exists, just return it. Otherwise allocate and save the 422 object.''' 423 return guard(client, space.alloc, '%s_obj' % name, type=type, name=name, 424 label=label, **kwargs) 425 426 427def alloc_cap(client, space, name, obj, **kwargs): 428 '''Guarded cap allocation. Works similarly to alloc_obj above.''' 429 cap = guard(client, space.alloc, '%s_cap' % name, name=name, obj=obj, **kwargs) 430 431 if obj is None: 432 # The caller was allocating a free slot. No rights are relevant. 433 return cap 434 435 # Upgrade the cap's rights if required. This can occur in a situation where 436 # we have connected an outgoing interface of a component instance to an 437 # incoming interface of the same component. alloc will be called twice on 438 # the EP with different permissions and we want to take the union of them. 439 if not space.cnode[cap].read and kwargs.get('read', False): 440 space.cnode[cap].read = True 441 if not space.cnode[cap].write and kwargs.get('write', False): 442 space.cnode[cap].write = True 443 if not space.cnode[cap].grant and kwargs.get('grant', False): 444 space.cnode[cap].grant = True 445 if not space.cnode[cap].grantreply and kwargs.get('grantreply', False): 446 space.cnode[cap].grantreply = True 447 448 return cap 449 450 451def calc_frame_size(size, frame_size, arch): 452 if not frame_size: 453 for sz in reversed(page_sizes(arch)): 454 if size >= sz and size % sz == 0: 455 frame_size = sz 456 break 457 assert frame_size, "Shared variable size: %d is not a valid page size multiple" % size 458 return frame_size 459 460 461def register_shared_variable(addr_space, obj_space, global_name, symbol, size, cap_space, 462 frame_size=None, paddr=None, perm='RWX', cached=True, label=None, with_mapping_caps=None): 463 ''' 464 Create a reservation for a shared memory region between multiple 465 components. 466 467 global_name: a global key that is used to link up the reservations 468 across multiple components. 469 symbol: the name of the local symbol to be backed by the 470 mapping frames. 471 size: the size of the region. Needs to be a multiple of the 472 smallest page size. 473 cap_space: the component's cspace. This is potentially used if the mapping caps 474 need to be moved to the component. In this case, with_mapping_caps needs 475 to be set when register_shared_variable is called. 476 frame_size: the size of frames to use to back the region. `size` 477 must be a multiple of `frame_size`. If `frame_size` 478 is not specified, the largest frame size that divides 479 evenly into `size` will be used. 480 paddr: the starting physical address of the frames. Only one 481 caller needs to specify this. If multiple callers 482 specify different values, the result is undefined. 483 perm, cached: page mapping options. These are only applied to the 484 caller's mapping 485 label: integrity label of the frame objects. In the default 486 `Context`, this defaults to the current entity name. 487 with_mapping_caps: An array to return mapping caps if the component needs the 488 caps for the mapping to be moved into their own cspace. 489 ''' 490 assert addr_space 491 size = int(size) 492 frame_size = calc_frame_size(size, frame_size, obj_space.spec.arch) 493 num_frames = size//frame_size 494 495 # If these frames have been allocated already then the allocator will return them. 496 # Therefore calls to register_shared_variable with the same global_name have to have the same size. 497 frames = [obj_space.alloc(ObjectType.seL4_FrameObject, 498 name='%s_%d_obj' % (global_name, i), 499 size=frame_size, 500 label=label) 501 for i in range(num_frames)] 502 if paddr is not None: 503 for f in frames: 504 f.paddr = paddr 505 paddr += frame_size 506 507 read = 'R' in perm 508 write = 'W' in perm 509 grant = 'X' in perm 510 511 if with_mapping_caps is not None: 512 # If we need the caps in our cspace, then we need to allocate them and call set_mapping_deferred on the cap 513 # set_mapping_deferred will result in the correct mapping info being set when the spec is being generated. 514 slots = [cap_space.alloc(frame, read=read, write=write, grant=grant, 515 cached=cached) for frame in frames] 516 caps = [cap_space.cnode[slot] for slot in slots] 517 [cap.set_mapping_deferred() for cap in caps] 518 with_mapping_caps.extend(slots) 519 else: 520 caps = [Cap(frame, read=read, write=write, grant=grant, cached=cached) for frame in frames] 521 sizes = [frame_size] * num_frames 522 addr_space.add_symbol_with_caps(symbol, sizes, caps) 523 # Return code to: 524 # 1. page-align the shared variable; 525 # 2. make it visible in the final ELF; and 526 # 3. Check that it is page-sized. 527 return 'extern typeof(%(sym)s) %(sym)s ALIGN(%(frame_size)d) VISIBLE;\n' \ 528 'static_assert(sizeof(%(sym)s) <= %(size)d,\n' \ 529 ' "typeof(%(sym)s) size greater than dataport size.");\n' \ 530 'static_assert(sizeof(%(sym)s) %% %(frame_size)d == 0,\n' \ 531 ' "%(sym)s not page-sized. Template bug in its declaration? ' \ 532 'Suggested formulation: `char %(sym)s[ROUND_UP_UNSAFE(sizeof(...), ' \ 533 'PAGE_SIZE_4K)];`");' % {'sym': symbol, 'size': size, 'frame_size': frame_size} 534 535 536def get_shared_variable_backing_frames(obj_space, global_name, size, frame_size=None, label=None): 537 ''' 538 Return the objects for the frame mapping. 539 global_name, size and frame_size need to be the same as was provided to register_shared_variable 540 It is possible to call this in a component that does not call register_shared_variable if the component 541 doesn't want a mapping itself, but requires caps for its cspace. 542 ''' 543 size = int(size) 544 frame_size = calc_frame_size(size, frame_size, obj_space.spec.arch) 545 num_frames = size//frame_size 546 return [obj_space.alloc(ObjectType.seL4_FrameObject, 547 name='%s_%d_obj' % (global_name, i), 548 size=frame_size, 549 label=label) 550 for i in range(num_frames)] 551 552 553def register_fill_frame(addr_space, symbol, fill, size, obj_space, label): 554 ''' 555 Take a symbol and create a collection of 4K frames that can comfortably store 556 a region in the bootinfo. 557 558 Return a static_assert checking that the symbol is of the correct size 559 ''' 560 assert addr_space 561 number_frames = size//4096 562 frames = [] 563 for i in range(number_frames): 564 fill_str = ['%d %d %s %d' % (0, 4096 if (size - (i * 4096)) >= 565 4096 else (size - (i * 4096)), fill, i * 4096)] 566 name = '%s_%s_%d_obj' % (symbol, label, i) 567 frames.append(obj_space.alloc(ObjectType.seL4_FrameObject, 568 name=name, label=label, fill=fill_str, size=4096)) 569 caps = [Cap(frame, read=True, write=False, grant=False) for frame in frames] 570 sizes = [4096] * number_frames 571 addr_space.add_symbol_with_caps(symbol, sizes, caps) 572 return 'static_assert(sizeof(%(sym)s) == %(size)s,\n' \ 573 ' "%(sym)s not page sized. Templage bug in its declaration?");' \ 574 % {'sym': symbol, 'size': size} 575 576 577def register_stack_symbol(addr_space, symbol, size, obj_space, label): 578 ''' 579 Create a stack of `size` with a guard page on each side. This allocates the frames internally 580 from the obj_space that is passed in as the frame objects shouldn't be needed anywhere else. 581 Stack frames are read, write mappings. 582 ''' 583 assert addr_space 584 number_frames = size//4096 585 frames = [obj_space.alloc(ObjectType.seL4_FrameObject, name='stack_%s_%d_%s_obj' % (symbol, i, label), label=label, size=4096) 586 for i in range(number_frames)] 587 # We create 2 additional mappings with None caps that are for the guard pages. 588 sizes = [4096] * (number_frames + 2) 589 caps = [None] + [Cap(frame, read=True, write=True, grant=False) for frame in frames] + [None] 590 addr_space.add_symbol_with_caps(symbol, sizes, caps) 591 592 593def register_ipc_symbol(addr_space, symbol, frame): 594 ''' 595 Register an IPC buffer symbol with a cap to the frame that is passed in. 596 The frame needs to be passed in instead of allocated internally because caps 597 to the frame are needed by other objects such as the TCB for the thread. 598 It is left to the caller to manage references to the Frame passed in. 599 ''' 600 assert addr_space 601 # We create 3*4K mappings with None on each side of the IPC buffer for guard pages 602 caps = [None, Cap(frame, read=True, write=True, grant=False), None] 603 sizes = [4096] * 3 604 addr_space.add_symbol_with_caps(symbol, sizes, caps) 605 606 607def register_dma_pool(addr_space, symbol, page_size, caps, cap_space): 608 ''' 609 Register a DMA pool symbol region in the AddressSpaceAllocator. 610 We pass in a list of slots and a cap_space allocator with the page size 611 to specify the size and caps of the DMA region. 612 ''' 613 assert addr_space 614 addr_space.add_symbol_with_caps( 615 symbol, [page_size] * len(caps), [cap_space.cnode[i] for i in caps]) 616 617 618def object_label_mapping(obj_space): 619 '''Return a list of all objects and the integrity labels for them.''' 620 return ((obj, label) 621 for label, objs in obj_space.labels.items() 622 for obj in objs) 623