These combinator rules do something like what wp_pre does now.
They were helpful in the ancient past, but now that wp_pre exists it is
much better to just use automation.
The run_tests script already has a -l/--list option to list all tests.
This adds a -L/--dry-run option to list the requested tests, which makes it
easier to figure out what tests -r/-x etc would select.
Also clarify in --help that -v adds more info to -l.
Abandon post-processing. There's some fragility somewhere that requires
process_stmt to see exactly the statements that go out, so it needs to run
last.
To handle initialiser elements, re-run process_stmt over the initialiser
statements that are created by process_decl. That's repeating some steps,
but it seems to work.
Waiting on input from Michael N about how crazy this is, but for now we're
pushing it to testing.
Two kinds of function calls were escaping the analysis. The first is simple,
the ReturnFnCall statement type, which was a silly omission from before.
Function calls inside initialiser statements are a more difficult problem.
The simplest solution was to move the VER-881 calculation into a
post-processing phase once those function calls have been moved to statement
positions.
- remove separate abstract set_/get_register implementation, directly use machine op
- make interface aware that user_context does not always need to equal
(register => machine_word)
- introduce FPU state on x64
This scans for statement-level function calls which will have complex
lvalue translations, either because their lvalues are compound
expressions or because their function return type will be promoted to
be stored. It treats them like expression-level function calls, with
an additional call statement added (saving to a ret_ variable) and
the complex lvalue step treated like an assignment.
When given a theorem, find_names finds other names the theorem appears
under, via matching on the whole proposition. It will not identify
unnamed theorems.
This patch adds a generic "post_cap_deletion" step that is called by
finalise_slot. Previous to this, the only caps which had actions
required at this stage were IRQHandlerCaps -- it was required that the
IRQ bitmap be updated after the cap itself was removed (as the
invariants state that for any existing IRQHandlerCap, the corresponding
bit in the IRQ bitmap must be set).
By genericising this, we add the capacity for new, arch-specific post
cap deletion actions to occur in the future.
Including version information in the spec document is tricky, because
Isabelle will rebuild the session whenever it sees that session inputs
(including document sources) have changed. Since ASpec is close to the
root of our session hierarchy, frequently changing version information
causes excessive rebuilds during development.
This commit avoids excessive rebuilding by building the document (with
version information) in a separate ASpecDoc session. The ASpecDoc
session is identical to the previous version of the ASpec session, but
is not the parent of any other sessions. The ASpec session is used as
the basis for other sessions, but has document-only inputs removed, and
also has document builds disabled.
This partially reverts a recent change which adds these.
Unfortunately, including the ARCH and git-id files in the ROOT file
causes frequent rebuilds during development. For example, adding a
commit that changes only CRefine would cause a change in the git-id
file, which would in turn trigger a rebuild of ASpec and everything that
depends on it. Because the git-id file also noted uncommitted changes,
these would also trigger an ASpec rebuild. Similarly, switching to a
different L4V_ARCH would cause the ARCH file to change, also triggering
an ASpec rebuild.
Since Isabelle makes it difficult to include this information in the
document without adding these files to the ROOT file, this commit is
removing this information until we find a better way.
message_info structs have 20 bit labels. On 32-bit systems, the label
does not need to be masked as there are no extra padding bits in the
struct, but this is not true for 64-bit systems. As a result, the
haskell needs to mask msgLabelBits (=20) when extracting the label in
messageInfoFromWord.
It's just a parser tweak for crunch, and runs multiple crunch commands
with the same sections (wps, ignores, etc).
Also update the comments a little, and move them closer to the anchor of
command clicks (the @{command_keyword} antiquotation).
Thomas Sewell
Japheth Lim
Gerwin Klein
Michael Sproul
Rafal Kolanski
Joel Beeren
Matthew Brecknell
Miki Tanaka
Matthew Fernandez