| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
This makes it consistent with the C backend, and also makes it easier to compare traces across execution re-runs.
|
|
If we have an nexp that we can't print, look for an equivalent type
variable before looking for a constant - the constant may only be valid
locally (e.g., under an if) while the type variable will be valid
throughout the function.
Fixes a problem with aget_Mem on aarch64.
|
|
redundant files.
|
|
|
|
|
|
|
|
|
|
|
|
Use nondeterministic choice by default instead of a deterministic bitstream
generator in the state, which is slightly awkward to reason about, because
every use of undefined_boolS changes the state. The previous behaviour can be
implemented as Sail code, if desired.
Also add a default implementation of internal_pick that nondeterministically
chooses an element from a list.
|
|
By default generated functions are non-static, using the -static flag makes them static which is useful for measuring coverage using generated code. Some utility helper functions will always be static, but the compiled versions of sail functions won't be unless this flag is set.
|
|
(probably still some pattern matching to do, but I don't think the models
use that)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Makes sure equality comparisons for variants are compiled correctly. Needed for CHERI and mips, which have structs containing
variants. Also make sure that struct equality works for structs containing other structs.
|
|
Add a test case in test/c/eq_struct.sail. Ensure that the macro EQUAL(type) will always give a valid equality function for any
builtin type in sail.h.
|
|
Non bitvector literals for decreasing vectors were not being reversed
correctly, so the list of capability registers was effectively in
reverse order.
Added a test case to test/c/ based on this aspect of CHERI
|
|
to notice if they are dead or inline them if appropriate, cleaning up coverage reports and potentially improving execution speed.
|
|
cleanly
|
|
We should test before the first iteration in case 'to' starts out as
less than 'from'.
|
|
|
|
The code to do this is rather ugly. It would be nice to have a generic
callgraph representation we could just query and not use the rewriter
in a weird way to extract this info.
|
|
|
|
Uses simple method of printing the entire record, in lieu of any decent
record update syntax.
|
|
|
|
|
|
|
|
targets using this.
|
|
Makes the generated undefined functions smaller, easier to read, and
avoids excessive memory usage in Coq (e.g., for large AST types).
|
|
|
|
|
|
This is now directly supported from SAIL so we can call the SAIL __SetConfig function
instead.
|
|
|
|
Registers can now be marked as configuration registers, for example:
register configuration CFG_RVBAR = 0x1300000
They work like ordinary registers except they can only be set by
functions with the 'configuration' effect and have no effect when
read. They also have an initialiser, like a let-binding. Internally
there is a new reg_dec constructor DEC_config. They are intended to
represent configuration parameters for the model, which can change
between runs, but don't change during execution. Currently they'll
only work when compiled to C. Internally registers can now have custom
effects for reads and writes rather than just rreg and wreg, so the
type signatures of Env.add_register and Env.get_register have changed,
as well as the Register lvar, so in the type checker we now write:
Env.add_register id read_effect write_effect typ
rather than
Env.add_register id typ
For the corresponding change to ASL parser there's a function
is_config in asl_to_sail.ml which controls what becomes a
configuration register for ARM. Some things we have to keep as
let-bindings because Sail can't handle them changing at runtime -
e.g. the length of vectors in other top-level definitions. Luckily
__SetConfig doesn't (yet) try to change those options.
Together these changes allow us to translate the ASL __SetConfig
function, which means we should get command-line option compatibility
with ArchEx for running the ARM conformance tests.
|
|
Necessary to prevent redundant clauses that Coq will reject
(There's still a problem if you use a variable rather than a wildcard,
see the test)
|
|
quite likely to exceed representable range of signed 64-bit integer (e.g. address starting 0x9...). Also make clear which values are displayed in hex vs. decimal.
|
|
|
|
|
|
Remember and use fallthrough clauses instead of dropping them when the last
clause in a group has a guard
|
|
|
|
|
