#
cba22977 |
|
17-Jan-2020 |
Kent McLeod <Kent.Mcleod@data61.csiro.au> |
Remove trust_partner attribute from rpc connectors This was only used for an optimization that is removed.
|
#
ebf7f4a9 |
|
25-Nov-2019 |
Kent McLeod <Kent.Mcleod@data61.csiro.au> |
python3: Update template to work on python3 filter returns a generator and needs to be converted to a list to take the len.
|
#
002c1714 |
|
07-Aug-2018 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Guard multi-language connectors Prevents templates from doing any rendering if they would not be instantiated. Even if a template is not instantiated it still must be processed in its deterministic order, so this prevents issues where a template would not be able to be processed.
|
#
0a994d4e |
|
17-Jul-2018 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Rewrite seL4RPCCall to use an abstract 'connector' This is a substantial refactor that is meant to make it easier to change how different templated connections work without having to duplicate a template and change it. In theory the seL4RPCCall template could be instantiated with a different 'connector' to give it different behaviours, although the mechanism to change the used connector is not done in this change. Whilst intended to be a semantics preserving refactor there are some minor changes. Some code gets trivial changes of being split into multiple statements or moved into different blocks. The largest change is some error handling is changed to be 'less helpful' due to difficulties in getting precise information to the point where the error code now has to be generated and having nice abstractions.
|
#
8b2ec3e6 |
|
20-Jun-2017 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
Fix licenses
|
#
bacfebce |
|
27-Oct-2015 |
Matthew Fernandez <matthew.fernandez@nicta.com.au> |
Refactored parser init commit.
|
#
48646e67 |
|
21-May-2015 |
Stephen Sherratt <stephen.sherratt@nicta.com.au> |
Removed unnecessary check for assembly configuration being none.
|
#
b79167a9 |
|
20-May-2015 |
Matthew Fernandez <matthew.fernandez@nicta.com.au> |
Templates: Use explicit comparison when testing against `None`. This is slightly clearer and safer.
|
#
4ff636b6 |
|
20-May-2015 |
Adrian Danis <Adrian.Danis@nicta.com.au> |
Refactor RPCCall template Move most of the functionality of the RPCCall template into common stubs that are included into the existing RPCCall template. These common stubs can eventually be refactored and used by the other existing RPC templates as well as other custom RPC templates
|
#
76c942c8 |
|
19-May-2015 |
Adrian Danis <Adrian.Danis@nicta.com.au> |
Move variable setting out of 'if' statements in RPC templates Userspace IPC checking was broken due to variables being assigned to in an 'if' statement, which is considered a different scope.
|
#
c6db5b36 |
|
20-Apr-2015 |
Matthew Fernandez <matthew.fernandez@nicta.com.au> |
Use void function prototypes where possible for additional type checking. Closes JIRA CAMKES-371
|
#
d1b98f1a |
|
16-Apr-2015 |
Matthew Fernandez <matthew.fernandez@nicta.com.au> |
Remove AST type `Direction`. This AST object was not gaining us anything as you always needed to look at its content to do anything with it. In the templates it was inducing strange code of the form `p.direction.direction`. This commit removes the type entirely. RPC parameter directions are now represented as bare strings. This also relevant in movement towards JIRA CAMKES-334.
|
#
6116c8a1 |
|
15-Apr-2015 |
Matthew Fernandez <matthew.fernandez@nicta.com.au> |
Check at compile-time that RPC parameters typedefs are not arrays. The types of RPC parameters can be external references that are expected to be provided as visible C typedefs at compile-time. In C it is possible for a user to provide a typedef representing an array type. Such types have different behaviour to scalar typedefs, in particular the way they are transformed across function calls. Typedef-ed arrays like this are not supported as RPC parameters, due to the glue code's limited ability to introspect these types. This commit adds a best effort mechanism to induce a compile-time warning if the user has made use of such an unsupported type. Closes JIRA CAMKES-306
|
#
ea01d742 |
|
27-Mar-2015 |
Matthew Fernandez <matthew.fernandez@nicta.com.au> |
Optimisation: Use new configuration dictionary interface in the templates.
|
#
8e9582e5 |
|
29-Mar-2015 |
Matthew Fernandez <matthew.fernandez@nicta.com.au> |
Qualify input pointers as `const`. ** BREAKING CHANGE ** Functions that correspond to RPC interfaces may need `const` added to some of their arguments. This commit alters the prototypes for RPC interfaces to mark input pointers -- specifically 'refin' scalars, 'in' strings and 'in' arrays -- as `const`. The purpose of this is largely a hint to user programmers, but it can potentially enable some further compiler optimisations. An effort has been made to maintain const-ness of pointers internally for the purposes of marshalling as well. Note that `const` has not been applied to any parameter that manifests as a double pointer ('in' string arrays, 'refin' strings, 'refin' arrays). The rationale for this decision was that introducing `const` here actually makes things *more* complicated for the user. E.g. a `char**` does not naturally coerce to a `const char**`. The result is a series of confusing compilation warnings and generated code that the compiler (incorrectly) believes to be unsafe. Closes JIRA CAMKES-358
|
#
0b8982a4 |
|
26-Mar-2015 |
Matthew Fernandez <matthew.fernandez@nicta.com.au> |
Templates: Be more explicit about testing for None and []. This commit replaces the idiom 'if foo' with explicit tests for None or the empty list when that is the intention of the given code. This makes the templates a little more readable and is necessary to avoid confusion in relation to some upcoming commits.
|
#
254e175d |
|
25-Mar-2015 |
Matthew Fernandez <matthew.fernandez@nicta.com.au> |
seL4RPC/seL4RPCCall: Fix: avoid leaking memory on error in marshalling outputs. This commit avoids a situation where an error in marshalling outputs could be caused by a malicious or mistaken user implementation action, following which heap memory would be leaked. This issue has not been reported by users and it is suspected that it has not affected anyone substantially. Closes JIRA CAMKES-348
|
#
c34c34f0 |
|
23-Mar-2015 |
Matthew Fernandez <matthew.fernandez@nicta.com.au> |
Suffix TLS variables with the connection side of their host. The purpose of this commit is to avoid naming conflicts with the TLS variables from opposing sides of a connection and their accessors. As for the previous commit, this is irrelevant for the implementation, but aids verification. Again, this is expected to have no user-visible effects and no effect on the generated binaries.
|
#
f20d8559 |
|
23-Mar-2015 |
Matthew Fernandez <matthew.fernandez@nicta.com.au> |
seL4RPC/seL4RPCCall: Rename internal glue code functions to avoid collisions. This commit renames marshalling and unmarshalling functions that previously had the same name. These functions were compiled into separate binaries, so this was not an issue from an implementation perspective, but this caused problems for verification, where we see both snippets of generated code as the same translation unit. This commit is expected to have no user-visible effects and no effect on generated binaries.
|
#
d9c8786a |
|
22-Mar-2015 |
Matthew Fernandez <matthew.fernandez@nicta.com.au> |
Fix: seL4Call: Shuffle 'sizes' assignment to avoid problems with empty procedures. When procedures had no methods, we were running into issues with referencing this variable before it was assigned to.
|
#
db346b78 |
|
22-Mar-2015 |
Matthew Fernandez <matthew.fernandez@nicta.com.au> |
Fix some incorrect register constraints.
|
#
61b53199 |
|
17-Mar-2015 |
Matthew Fernandez <matthew.fernandez@nicta.com.au> |
trivial: Squash some compiler warnings.
|
#
0a8e5ab2 |
|
09-Mar-2015 |
Matthew Fernandez <matthew.fernandez@nicta.com.au> |
Support for configurable TLS. For verification we need to avoid taking the address of local variables. In the glue code this is difficult because multiple threads may be executing in the glue concurrently. The current work around for this is per-thread global variables that can have their address taken. This is added here as a configuration option with the default remaining the existing behaviour, because this structure has a non-trivial performance impact. In particular, GCC fails to determine that our use of static variables does not rely on their previous value and thus persistent stores to them can be eliminated. Experimenting with small examples suggests that this is just not an optimisation that GCC ever attempts. This is unsurprising as this pattern of variable usage is fairly unusual and would be unlikely to be encountered in handwritten code. This change should have no visible effect to unaware users.
|
#
16bfcca2 |
|
09-Mar-2015 |
Matthew Fernandez <matthew.fernandez@nicta.com.au> |
Templates: Name per-interface error handlers statically. This allows us to more straightforwardly blacklist these symbols -- which is also done in this commit -- to avoid them appearing in verification input.
|
#
4cbdb9f9 |
|
02-Mar-2015 |
Matthew Fernandez <matthew.fernandez@nicta.com.au> |
Include tls.h in all RPC templates for ease of use.
|
#
a966c58b |
|
26-Feb-2015 |
Matthew Fernandez <matthew.fernandez@nicta.com.au> |
Use ROUND_UP_UNSAFE in glue code instead of ROUND_UP. ROUND_UP_UNSAFE is an alternative to ROUND_UP that evaluates its arguments more than once and thus is sometimes unwise to call. In the context we are invoking it, it is safe to evaluate the arguments multiple times. The motivation for this switch is because the verification C parser cannot handle the GNU statement expressions used in ROUND_UP.
|
#
77eb2673 |
|
08-Feb-2015 |
Matthew Fernandez <matthew.fernandez@nicta.com.au> |
Optimisation: alloc destination space for strings on-demand. This commit removes the constant `CAMKES_STR_MAX` and references to this that were used as arguments to `malloc`. Instead we now allocate through `strdup` on-demand as we always know, in advance, the length of the string we're unmarshalling. This change is an optimisation for memory usage and not necessary for correctness, though it does have user-visible effects. Users should be aware that string arrays are now a malloced array of pointers to other malloced buffers, as opposed to a single malloced (2D) array.
|
#
6e1efeb6 |
|
09-Feb-2015 |
Matthew Fernandez <matthew.fernandez@nicta.com.au> |
Fix: add missing error check in seL4RPCCall.
|
#
553135c9 |
|
03-Feb-2015 |
Matthew Fernandez <matthew.fernandez@nicta.com.au> |
Implement 'refin' as a new parameter direction. This commit implements a new direction for RPC parameters, 'refin.' In everything except the C backend, this direction is identical to 'in.' In the C backend this generates a user function prototype that passes this parameter by pointer instead of by value. The primary use case of this is for interfaces involving C types that are typedefed structs. The cost of a function call involving such types can be decreased by passing the parameter by pointer. In generaly this should only be used as an optimisation and 'in' should remain the default direction for input parameters.
|
#
c9b4c516 |
|
04-Feb-2015 |
Matthew Fernandez <matthew.fernandez@nicta.com.au> |
seL4RPCCall: Only elide asm clobbers when explicitly trusting components. This commit introduces an extra degree of safety, wherein users are required to explicitly use an attribute to declare component instances 'trusted = "true"' if they want to elide all clobbers in the specialised asm stub. If the partner you are communicating with is not trusted it is not safe to elide these clobbers as they can overflow the message length you wre expecting and cause unexpected behaviour. To my knowledge no one had hit issues like this or were using this specialisation in the presence of untrusted components, but this is an added safety measure. In future it would be possible to introduce more broader stub optimisations to use seL4_CallWithMRs when we can detect (at generation time) that there is a payload, but it is short enough to fit in the message registers.
|
#
f9cda8f8 |
|
29-Jan-2015 |
Matthew Fernandez <matthew.fernandez@nicta.com.au> |
Implement error handling in glue code. This commit replaces previous assertion placeholders and other assumptions with a flexible error handling mechanism. For details on how to use this, refer to the accompanying documentation.
|
#
876fd9c9 |
|
30-Jan-2015 |
Matthew Fernandez <matthew.fernandez@nicta.com.au> |
Fix some issues with usage of arrays as return types. In particular, the size of the returned array was never actually returned to the caller and was simply discarded. As mentioned in 20f4072ac25eeb707f4e17c4a26501d4b59308ee, these issues are all theoretical as array return value cannot currently be specified.
|
#
20f4072a |
|
22-Jan-2015 |
Matthew Fernandez <matthew.fernandez@nicta.com.au> |
Templates: Consolidate and rewrite RPC marshalling code. This commit moves all RPC marshalling and unmarshalling code into separate template fragments that are included by the seL4RPC and seL4RPCCall templates. The marshalling and unmarshalling code is some of the most dense and edge-case-ridden template code we have, so hopefully this change will make it more readable and maintainable. Another driving factor for this change is the upcoming introduction of universal error handling in the glue code. This change should not have any user-visible effect beyond potential performance improvements and perhaps fixing latent bugs. The main internal effects of this commit are: * String arguments are treated more uniformly. In particular, whenever glue code needs to dynamically allocate space for a string, it references the constant `CAMKES_STR_MAX`. Users can refer to this to see how much information can be passed in string parameters. * Calls to `memcpy` are emitted inline, instead of calls to `camkes_marshal_*`. With LTO enabled, your compiler should have been able to inline the calls to `camkes_marshal_*` previously anyway, but most users build without LTO. This change inlines `memcpy` invocations always. * Marshalling and unmarshalling generated as separate, static functions. These operations were previously done inline in both seL4RPC and seL4RPCCall. The runtime effect of separating them into individual functions should be nil as they are static and each called precisely once, so the compiler should happily inline them. Separating them out does prepare the way for users like Adrian to provide their own event loop in future, though. * Method indicies are packed in seL4RPC. The seL4RPCCall connector previously used the smallest data type that could be used to transmit the method index, while seL4RPC just always used an `int`. In unifying the code, both now pack the method index. * Interfaces with more than 2^32 methods are supported. That is, the method index is now stored in a 64-bit type when necessary. 2^64 is the new upper limit on the number of methods you can have in an interface. Having said that, if you have more than 2^32 methods in an interface you should probably consult your doctor as pain will most certainly persist. * Arrays as return types are now supported. If you define an interface method with a return type that is an array, your C implementation will be prototyped (and must be implemented) with an additional leading `size_t` output parameter for the return type's length. Note that array return types are not currently supported during the parsing phase, so this is more future-proofing the marshalling code than extra functionality. * Method indicies for interfaces with 0 methods are handled. This is somewhat irrelevant as interfaces with 0 methods are not supported during the parsing phase, but it was a side-effect of code consistency. * The function `stpcpy` is used pervasively for string marshalling. This is a POSIX extension and only worth mentioning here because the calls to it will be removed in a future change that implements bounds checking. * Dynamically allocated memory in the glue code is freed more eagerly. Some calls to `free` have been shifted upwards, though this should only be observable if your heap already had a high occupancy.
|
#
b34eb1d5 |
|
29-Jan-2015 |
Matthew Fernandez <matthew.fernandez@nicta.com.au> |
Switch to using libutils unreachable macro.
|
#
50c5be15 |
|
15-Dec-2014 |
Matthew Fernandez <matthew.fernandez@nicta.com.au> |
Fix: Check for reference types when specialising syscall stubs. The code at these locations attempts to determine whether the arguments to an RPC call can be packed into registers and hit the kernel IPC fastpath. Unfortunately it assumed that all types of your methods were CAmkES native types, which was not necessarily true. This commit checks whether we have any reference types (C typedefs) in the method we're currently looking at specialising. Closes JIRA CAMKES-303
|
#
27f9118e |
|
15-Dec-2014 |
Matthew Fernandez <matthew.fernandez@nicta.com.au> |
Change template license headers to Jinja comments. The effect of this is that they do not appear in generated output, which was a bit confusing previously. Closes JIRA CAMKES-319 Conflicts: camkes/templates/autocorres/AsynchNativeFrom.template.thy camkes/templates/autocorres/AsynchNativeTo.template.thy camkes/templates/autocorres/RPCSimpleFrom.template.thy camkes/templates/autocorres/RPCSimpleTo.template.thy camkes/templates/autocorres/SharedDataFrom.template.thy camkes/templates/autocorres/SharedDataTo.template.thy camkes/templates/echronos/eChronosAsynch-from.template.c camkes/templates/echronos/eChronosAsynch-to.template.c camkes/templates/echronos/eChronosDirectCall-from.template.c camkes/templates/echronos/eChronosDirectCall-to.template.c camkes/templates/linker.lds camkes/templates/linux/component.template.c camkes/templates/linux/component.template.h camkes/templates/linux/linuxMQ-from.template.c camkes/templates/linux/linuxMQ-to.template.c camkes/templates/linux/linuxMQEmpty-from.template.c camkes/templates/linux/linuxMQEmpty-to.template.c camkes/templates/linux/linuxMmap-from.template.c camkes/templates/linux/linuxMmap-to.template.c
|
#
2187a516 |
|
22-Oct-2014 |
Matthew Fernandez <matthew.fernandez@nicta.com.au> |
Move Jinja macros into Python. Jinja macros have unexpected, and often unpleasant, behaviour. A non-exhaustive list of issues with them is: - They are not first class Python functions so cannot be passed within the template context to, e.g., `map`; - They can mask and inadvertently overwrite your local variables; - Certain types of references have unexpected expansions within the context of a macro; - Calling a macro within a macro is dangerous; and - You cannot call certain Python functions from within a macro. This commit transliterates the existing macros into Python, attempting to preserve all current functionality. This has involved essentially inverting their implementation such that they become C hosted within Python, rather than Python hosted within C. The macros are now unconditionally available to all templates (see Context.py). This change is intended to be transparent to template authors and CAmkES users. Conflicts: camkes/templates/echronos/eChronosAsynch-from.template.c camkes/templates/echronos/eChronosAsynch-to.template.c camkes/templates/linux/component.template.h camkes/templates/linux/linuxMQ-from.template.c camkes/templates/linux/linuxMQ-to.template.c camkes/templates/linux/linuxMQEmpty-from.template.c camkes/templates/linux/linuxMQEmpty-to.template.c camkes/templates/linux/linuxMmap-from.template.c camkes/templates/linux/linuxMmap-to.template.c camkes/templates/macros.jinja
|
#
1bca421e |
|
03-Dec-2014 |
Adrian Danis <Adrian.Danis@nicta.com.au> |
Allow the endpoints used in seL4RPCCall connections to be badged on the -to side and provide a function to retrieve the badge on the -from side
|
#
cc64bb50 |
|
21-Jul-2014 |
TrustworthySystems <gatekeeper@sel4.systems> |
Release snapshot
|