Merge branch 'master' into pr/tcb-bound-notification

.github/workflows/push.yml

@@ -23,3 +23,6 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - uses: seL4/ci-actions/link-check@master
+        with:
+          # produces 403 for link checkers now:
+          exclude_urls: ".*haskellstack.org.*"

CHANGES → CHANGES.md

@@ -1,40 +1,71 @@
-<--
+<!--
      Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 
      SPDX-License-Identifier: BSD-2-Clause
 -->
 
-Revision history for capDL
+# Version history for capDL
 
-This file should be word wrapped to 120 characters
+<!-- This file should be word wrapped to 120 characters -->
 
 ---
-Upcoming release
 
-## Changes
+## Upcoming release
 
+### Changes
+
+* add support for SMC capability
+* enable MCS build; use `seL4_TCB_SetAffinity` only for non-MCS kernels
+* allow `SchedControlCap` to refer to a secondary core
+* minimal update for seL4 AArch64 VSpace API change, removing `seL4_ARM_PageGlobalDirectoryObject`
+* `object_sizes`: add include for deprecated constants, because some definitions
+  that `object_sizes` depends on are now found in a `deprecated.h` header file.
+* Clean up and clarify `arm11` usage in capDL despite ARMv6 removal
+* `cdl_utils`: remove `simpleeval` python dependency
+* Run GitHub tests with python 3.9
+* added vulnerability reporting policy
+
+#### capdl-loader
+
+* use `seL4_BootInfoFrameSize` instead of hard-coded page size
+* python + loader: Add support for generating fault handler caps with specific
+  rights. Behaviour is unchanged (`seL4_AllRights`) if no rights are provided.
+* ensure heap is aligned
+
+#### capDL-tool
+
+* update to LTS Haskell 20.25, ghc-9.2.8
+* fix several cases in `validObjPars`: `Period`, `IOAPIC`, `MSIHandle`, `CBNumber`
+
+### Upgrade Notes
+
+* existing capDL specs should continue to work
+* AArch64 VSpace changes may allow simplification of some capDL specs
 
-## Upgrade Notes
 ---
-0.2.1 2021-06-10
+
+## 0.2.1 2021-06-10
+
 Using seL4 version 12.1.0
 
-## Changes
+### Changes
 
 * Added page-upper-directory caps to the valid TCB check for platforms like QEMU arm-virt as they use different paging
   structures.
 * Added const qualifiers to the capdl-loader-app to avoid compiler warnings against other libraries.
 * Improved the README for the capdl-loader-app.
 
-## Upgrade Notes
+### Upgrade Notes
 
 * None to be aware of. This is not a source-breaking or binary-breaking release.
 
 ---
-capdl-0.2.0 2020-10-27
+
+## capdl-0.2.0 2020-10-27
+
 Using seL4 version 12.0.0
 
-## Changes
+### Changes
 
 * Convert to SPDX license tags. This includes marking all documentation files CC-BY-SA-4.0.
 
@@ -53,12 +84,12 @@ Using seL4 version 12.0.0
 * Add TCB Resume field to capDL object and support raw TCB object creation.
 * Add GitHub actions scripts. These scripts replicate internal CI checks directly on GitHub
 
-### capDL-tool
+#### capDL-tool
 
 * rework validObjCap and check TCB slots, which allows vcpus for all architectures.
 * convert CapDL language specification to Markdown.
 
-### Capdl-loader-app
+#### Capdl-loader-app
 
 * Improve log output.
 * Initialise libc in debug builds.
@@ -72,18 +103,20 @@ Using seL4 version 12.0.0
 * Fix issue where large DTB images inside BootInfo would overlap reserved memory address used to initialise frames.
 * Remove CONFIG_CAPDL_LOADER_ALLOW_NO_CSPACE config option as it has been unused for a while.
 
-### Capdl-linker:
+#### Capdl-linker
 
 * Optimize spec generation performance:
   - Sort elf symbols by their vaddr.
   - Replace linear search with binary when looking for virtual addresses.
 * Fix Python syntax warnings when `capdl_linker.py` is invoked.
 
 ---
-0.1.0 2019-11-19
+
+## 0.1.0 2019-11-19
+
 Using seL4 version 11.0.0
 
-## Changes
+### Changes
 
 * Add GrantReply access right for endpoint capabilities.
   - This is a new right available on seL4 Endpoint object capabilities.

cdl_utils/capdl_linker.py

@@ -8,17 +8,16 @@
 from capdl.Object import register_object_sizes, Untyped
 from capdl.Allocator import ASIDTableAllocator, BestFitAllocator
 from capdl import ELF, lookup_architecture, TCB, valid_architectures
+from importlib.metadata import version
 from jinja2 import Environment, BaseLoader, FileSystemLoader
 import sys
 import argparse
 import pickle
 import logging
 import os
 import tempfile
-import pkg_resources
 import yaml
 import six
-pkg_resources.require("jinja2>=2.10")
 
 
 CSPACE_TEMPLATE_FILE = os.path.join(os.path.dirname(__file__), "templates/cspace.template.c")
@@ -29,6 +28,10 @@ def manifest(cap_symbols, region_symbols, architecture, targets):
     Generates a c file from CSPACE_TEMPLATE_FILE with some runtime information
     about CSpace slots and special address ranges
     """
+    jinja2_version = version("jinja2")
+    if jinja2_version < "2.10":
+        raise Warning("Jinja2 should be >= 2.10")
+
     temp_file = open(CSPACE_TEMPLATE_FILE, 'r').read()
     template = Environment(loader=BaseLoader).from_string(temp_file)
 

python-capdl-tool/capdl/ELF.py

@@ -149,7 +149,6 @@ def get_pages(self, infer_asid=True, pd=None, use_large_frames=True, addr_space=
         existing_pages = []
         if addr_space:
             # Update symbols with their vaddrs in the AddressSpaceAllocator if we were given one
-            existing_pages = []
             for (symbol, (sizes, caps)) in iteritems(addr_space.get_symbols_and_clear()):
                 assert self.get_symbol_size(symbol) >= sum(sizes), \
                     "Symbol (%s:%d) must have same or greater size than supplied cap range (%d)" % (