Release snapshot

.gitignore

@@ -0,0 +1,2 @@
+# Ignore python bytecode
+**.pyc

.hgignore

@@ -0,0 +1,18 @@
+syntax: regexp
+
+\.pyc$
+\.out$
+\.swp$
+
+# Generated parser database.
+parsetab\.py$
+
+# Generated test files.
+^tests/\.stable[12]$
+
+# Generated C parser input
+^include/isabelle/.*_pp
+
+# Generate docs
+^docs/.*\.html$
+^docs/contents\.js$

Kconfig

@@ -0,0 +1,246 @@
+#
+# Copyright 2014, NICTA
+#
+# This software may be distributed and modified according to the terms of
+# the BSD 2-Clause license. Note that NO WARRANTY is provided.
+# See "LICENSE_BSD2.txt" for details.
+#
+# @TAG(NICTA_BSD)
+#
+
+menu "CAmkES Options"
+
+    config CAMKES_DEFAULT_STACK_SIZE
+    int "Component stack size"
+    default 16384
+    range 1 1073741824 # <-- 2^30
+    help
+        Stack size to allocate per-component, in bytes. Note that this value
+        should be page-aligned. If not, it will be rounded up.
+
+    config CAMKES_USE_EXTERNAL_OBJDUMP
+    bool "Call out to objdump for ELF information"
+    default n
+    help
+        Instead of using the internal ELF parsing functionality, call out to
+        your toolchain's objdump to perform required operations. This is much
+        more fragile than using internal functionality, but can provide a
+        performance boost in compilation times.
+
+    choice
+    prompt "Compilation cache"
+    default CAMKES_CACHE_OFF
+    help
+        Select the mode of operation of the compilation cache. This cache
+        stores results of previous code generation using the same configuration
+        and uses this to speed up subsequent invocations.
+
+    config CAMKES_CACHE_OFF
+    bool "off"
+
+    config CAMKES_CACHE_READWRITE
+    bool "read/write"
+
+    config CAMKES_CACHE_READONLY
+    bool "read-only"
+
+    config CAMKES_CACHE_WRITEONLY
+    bool "write-only"
+
+    endchoice
+
+    config CAMKES_CPP
+    bool "Pre-process with CPP"
+    default n
+    help
+        Run CPP on the input specification(s) before parsing them into an AST.
+        This can allow you to write parameterised specs in the case of more
+        complex systems.
+
+    config CAMKES_DEBUG_MALLOC
+    bool "Enable allocation debugging"
+    default n
+    help
+        This option instruments memory allocation functions to catch heap
+        corruption. Use this for debugging dynamic memory problems.
+
+    config CAMKES_DEBUG_POST_RENDER_EDIT
+    bool "Allow editing each template after rendering"
+    default n
+    help
+        After each template is rendered, you will be prompted as to whether you
+        want to edit the rendered output before the runner exits. If you choose
+        to do so, the output will be opened in the editor determined by the
+        value of your environment variable EDITOR.
+
+    config CAMKES_SYSLIB
+    string "Name of C stdlib syscall backing library"
+    default sel4muslccamkes
+    help
+        This option sets the name of the backing library which will be linked with camkes
+        components. This defaults to sel4muslcsys, which is a minimal syscall library for
+        muslc.
+
+    config CAMKES_OPTIMISATION_RPC_LOCK_ELISION
+    bool "Optimisation: RPC lock elision"
+    default y
+    help
+        Detect when it is safe to exclude locking operations in the seL4RPC connector and
+        automatically do so. This is an optimisation that can improve the performance of
+        this connector.
+
+    config CAMKES_OPTIMISATION_CALL_LEAVE_REPLY_CAP
+    bool "Optimisation: Leave reply cap in place"
+    default y
+    help
+        Detect scenarios where a reply cap obtained when in an seL4RPCCall
+        connector can never be overwritten, and operate on it in place instead
+        of saving it to a free cap slot. This is an optimisation that can
+        improve the performance of the seL4RPCCall connector. Under the right
+        conditions, with this optimisation enabled, it is possible to hit the
+        IPC fastpath on return.
+
+    config CAMKES_OPTIMISATION_SPECIALISE_SYSCALL_STUBS
+    bool "Optimisation: Specialise syscall stubs"
+    default y
+    help
+        Detect when glue code overhead could be reduced with a custom syscall
+        stub and generate and use this instead of the libsel4 stubs. This does
+        not affect whether a given IPC will hit the fastpath, but it does
+        reduce the userlevel overhead of these system calls. In ideal
+        conditions this will give you RPC as fast as native seL4 IPC. This only
+        has an effect on ARM.
+
+    config CAMKES_PROVIDE_TCB_CAPS
+    bool "Verification: Provide TCB caps"
+    default y
+    help
+        Hand out TCB caps to components. These caps are used by the component
+        to exit cleanly by suspending. Disabling this option leaves components
+        with an empty slot in place of their TCB cap. This means they will cap
+        fault when attempting to exit. The advantage is that your resulting
+        CapDL specification contains no TCB caps and is thus easier to reason
+        about.
+
+    config CAMKES_SUPPORT_INIT
+    bool "Verification: Support init infrastructure"
+    default y
+    help
+        Support the pre_init, post_init and interface init functions as part of
+        component startup. These functions allow extra functionality, but
+        introduce some endpoint caps for synchronisation. You probably want
+        this option enabled unless you are targetting verification.
+
+    config CAMKES_CONNECTOR_TIMING
+    bool "Enable collection of timing data for connectors"
+    default n
+    help
+        Enable timing points within connector templates that take cycle counter
+        values as they are passed. This timing data can then be retrieved after
+        execution.
+
+    config CAMKES_DEFAULT_PRIORITY
+    int "Default thread priority"
+    # Default to one less than max prio to avoid interleaving our output with
+    # the CapDL initialiser.
+    default 254
+    range 1 255
+    help
+        Default priority for component threads if this is not overridden via an
+        attribute. Generally you want to set this as high as possible due to
+        the suboptimal seL4 scheduler.
+
+    choice
+    prompt "Profiler"
+    default CAMKES_PROFILER_NONE
+    help
+        Select the profiling tool to use when instantiating templates. Enabling
+        a profiler can help you diagnose performance bottlenecks in the
+        compilation process. The available profilers are "internal" (basic
+        timing information), "native" (cProfile), "aggregate" (single
+        cProfile measurement across entire execution) and "heartbeat" (just a
+        debugging print out pulse to show progress).
+
+    config CAMKES_PROFILER_NONE
+    bool "none"
+
+    config CAMKES_PROFILER_INTERNAL
+    bool "internal"
+
+    config CAMKES_PROFILER_NATIVE
+    bool "native"
+
+    config CAMKES_PROFILER_AGGREGATE
+    bool "aggregate"
+
+    config CAMKES_PROFILER_HEARTBEAT
+    bool "heartbeat"
+
+    endchoice
+
+    config CAMKES_PYTHON_OPTIMIZE
+    bool "Enable Python optimisations (-O)"
+    # Note that you cannot enable -OO (strip docstrings as well) because PLY
+    # needs them.
+    default n
+    help
+        Pass -O to Python when running CAmkES. This causes Python to produce
+        optimised bytecode that runs significantly faster. Note that this
+        option will disable assertions and therefore it is not recommended to
+        enable it if you are working on the internals of CAmkES itself.
+
+    config CAMKES_PLY_OPTIMIZE
+    bool "Enable PLY optimisations"
+    default n
+    help
+        Run the CAmkES parsing library, PLY, in an optimised configuration.
+        With this enabled, docstrings and regexs are compiled during an
+        execution and then re-used during following executions rather than
+        re-compiling. This option significantly hampers PLY's diagnostics so it
+        is not recommended to enable this if you are working on the internals
+        of CAmkES itself.
+
+    config CAMKES_DISABLE_PYTHON_IMPORT_CHECKS
+    bool "Disable Python import checks"
+    default n
+    help
+        Disable sanity checks that Python modules we are about to import are
+        available. These checks are designed to warn new users that they do not
+        have the required dependencies. If you have an established installation
+        and want to speed up your build times you should select this option.
+
+    choice
+    prompt "Python interpreter"
+    default CAMKES_PYTHON_INTERPRETER_CPYTHON
+    help
+        Select the Python interpreter used for executing CAmkES. The default
+        CPython interpreter should be acceptable for any normal use, but you
+        may find PyPy provides better build system performance under some
+        circumstances. To use PyPy, obviously you need it installed. The other
+        interpreters are for profiling or dynamic analysis.
+
+    config CAMKES_PYTHON_INTERPRETER_CPYTHON
+    bool "CPython (default)"
+
+    config CAMKES_PYTHON_INTERPRETER_PYPY
+    bool "PyPy"
+
+    config CAMKES_PYTHON_INTERPRETER_FIGLEAF
+    bool "Figleaf"
+
+    config CAMKES_PYTHON_INTERPRETER_COVERAGE
+    bool "Coverage"
+
+    endchoice
+
+    config CAMKES_LABEL_MAPPING
+    bool "Generate policy label mapping"
+    default n
+    help
+        Enable this option to generate a mapping from labels to kernel objects
+        during compilation. A label per-CAmkES entity (component instance or
+        connection) is generated and they are intended to form the input domain
+        of a function mapping these to final policy labels. The final labels
+        are then used to reason about the security properties of a system.
+
+endmenu

LICENSE_BSD2.txt

@@ -0,0 +1,31 @@
+Files described as being under the "BSD 2-Clause" license fall under the
+following license.
+
+-----------------------------------------------------------------------
+
+Copyright (c) 2014 National ICT Australia and other contributors.
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright
+   notice, this list of conditions and the following disclaimer in the
+   documentation and/or other materials provided with the distribution.
+
+THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' AND
+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR CONTRIBUTORS BE LIABLE
+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
+LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
+OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
+SUCH DAMAGE.
+

README

@@ -0,0 +1,26 @@
+#
+# Copyright 2014, NICTA
+#
+# This software may be distributed and modified according to the terms of
+# the BSD 2-Clause license. Note that NO WARRANTY is provided.
+# See "LICENSE_BSD2.txt" for details.
+#
+# @TAG(NICTA_BSD)
+#
+
+This repository contains various CAmkES tools.
+
+ camkes/     Implementation of the tools themselves
+  ast/       Abstract Syntax Tree objects
+  lint/      AST correctness checker
+  parser/    Grammar import and export
+  runner/    Template instantiator
+  templates/ Templates themselves
+ docs/       User and developer information about the tools
+ examples/   Some examples of how to use the parser
+ grammars/   Formal specifications of different CAmkES grammars
+ misc/       Some 'useful' odds and ends
+ tests/      Test suite for the parser
+ tools/      Scripts to ease development on the parser
+
+If you don't know where to begin, docs/index.html is a good start.