The low-level specification roughly maps to the code generator and template
instantiation phases of CAmkES. At this point no address space objects exist
(excepting slight infidelity with respect to page directories). The address
space objects are introduced in the "extra" objects that we append, which map
roughly to the ELF derivation and CapDL filters.
Separating the two collections of objects gives us some nice preserved
properties that can be shown over generation from an abstract input. In
particular, we can phrase some provable properties that are resilient against
things like changes in compiler optimisation levels and allocation strategies.
These theories construct a locale with holes that are filled in by generated
code. Interpreting the locale manually is quite tedious and error prone, but we
entirely automate this process during code generation. For the details of this,
see the CAmkES 'architecture-semantics' and 'label-mapping' back ends.
When isa_type_to_typ is called from a theory other than the one the type was
declared in, it would pick the wrong fully qualified name. Now the function
should be robust against a) yet undeclared types (for record decls), b)
existing types in same theory (normal case), and c) existing struct types
from other theories (e.g. from autocorres).
The observable state has been strengthened significantly years ago and
this theory has fallen into disrepair. The toplevel refinement statement
here was nicely concise for a paper, but the practical value is in the
much stronger corres statement, so instead of attempting proof
acrobatics with a new observable state, I'm retiring this theory.
Gerwin Klein
Gao Xin
Joel Beeren
Matthew Fernandez
Japheth Lim