| Age | Commit message (Collapse) | Author |
|---|
|
:fixed_registers command
|
|
accordingly
|
|
The following is therefore always forbidden
```
scattered union U
enum E = A | B | C
union clause U = Ctor : E
```
We attempt to detect when this occurs and include a hint indicating the
likely reason why a 'Undefined type E' error might occur in this
circumstance
|
|
|
|
Ensure we give a nice error message that explains that recursive types are forbidden
```
Type error:
[struct_rec.sail]:3:10-11
3 | field : S
| ^
| Undefined type S
| This error was caused by:
| [struct_rec.sail]:2:0-4:1
| 2 |struct S = {
| |^-----------
| 4 |}
| |^
| | Recursive types are not allowed
```
The theorem prover backends create a special register_value union that
can be recursive, so we make sure to special case that.
|
|
This allows read_mem and read_reg effects to be handled by GDB
|
|
The following now works to run sail on every HVC call with hafnium
function gdb_init() -> unit = {
// Connect to QEMU via GDB
sail_gdb_qemu("");
sail_gdb_symbol_file("hafnium.elf.sym");
sail_gdb_send("break-insert sync_lower_exception")
}
function gdb() -> unit = {
gdb_init();
while true do {
sail_gdb_send("exec-continue");
sail_gdb_sync()
}
}
|
|
|
|
Currently the -is option allows a list of interactive commands to be
passed to the interactive toplevel, however this is only capable of
executing a sequential list of instructions which is quite limiting.
This commit allows sail interactive commands to be invoked from sail
functions running in the interpreter which can be freely interleaved
with ordinary sail code, for example one could test an assertion at each
QEMU/GDB breakpoint like so:
$include <aarch64.sail>
function main() -> unit = {
sail_gdb_start("target-select remote localhost:1234");
while true do {
sail_gdb_continue(); // Run until breakpoint
sail_gdb_sync(); // Sync register state with QEMU
if not(my_assertion()) {
print_endline("Assertion failed")
}
}
}
|
|
GDB/MI
After starting QEMU with -s -S we can run :gdb_qemu in isail to
connect to it using a gdb-multiarch child process, which we
communicate with via the gdb/mi interface.
:gdb_send command sends a command to gdb and waits for it to
respond. The idea is we will have a :gdb_sync command that will sync
the register state of the running QEMU session with the Sail
interpreter after a breakpoint, then we can run Sail code to test the
state of the machine by hooking memory reads into approprate gdb
commands.
|
|
SMT seems sensitive to gensym counter being reset between definitions,
but it shouldn't care due to unique_per_function_ids... need to
investigate further. Only causes a single test to fail so must be
subtle. Diffing between the bad/good versions reveals a few lines of
generated SMT go missing when the gensym counter is reset.
|
|
Lem definitions from Sail2_values are used in the C and SMT backends
as the definition of what the Sail builtins mean for constant folding
and other operations, but due to Lem renaming issues (we think) if any
part of Sail that RMEM relies on transitively depends on a Lem file
(that is affected by renaming?) it causes issues with inconsistent
assumptions over cmi files.
interactive.ml contains a reference to an AST and an environment which
are used as the implicit state that the interactive toplevel
uses. Commit 8182b700 added an implicit IR reference to the toplevel
which essentially added a dependency on sail2_values.lem by way of
jib.lem. This moves that to a separate file which should solve the
issue.
|
|
|
|
Make it so that jib_compile.ml never relies on specific string encodings
for various constructs in C. Previously this happened when
monomorphisation occured for union constructors and fields, i.e.
x.foo -> x.zfoo_bitsz632z7
Now identifiers that can be modified are represented as (id, ctyp list)
tuples, so we can keep the types
x.foo -> x.foo::<bits(32)>
This then enables us to do jib IR -> jib IR rewrites that modify types
In particular there is now a rewrite that removes tuples as an IR->IR
pass rather than doing it ad-hoc in the C code generation, although this
is not on by default
Note that this change seems to have triggered an Ott bug so jib.lem is
now checked in and not generated from Ott
|
|
Rather than having a global symbol generating function gensym used
throughout the C backend, instead 'generate' them as needed like:
let (gensym, reset_gensym_counter) = symbol_generator "gs"
This just makes things a bit neater and means we can reset the counter
between definitions in jib_compile without worrying about other modules
relying on global uniqueness
|
|
|
|
|
|
|
|
can use Interactive.register_command to set up a new interactive
command, which allows commands to be set up near where the
functionality they interact with is defined, e.g. the ast slicing
commands are registered in Slice.ml. Also allows help messages to be
generated in a consistent way.
|
|
- requires fixpoint definitions containing proofs to be processed in proof
mode (due to a bug in Coq), so change libraries and pretty printing to
do that
- adjust some lemmas to avoid extra evars
|
|
|
|
|
|
|
|
bitvectors in C
Assumes a Sail C library that has functions with the right types to
support this. Currently lib/int128 supports the -Ofixed_int option,
which was previously -Oint128.
Add a version of Sail C library that can be built with -nostdlib and
-ffreestanding, assuming the above options. Currently just a header
file without any implementation, but with the right types
|
|
It only produces them when necessary (because some types do not have
decidable equality due to embedded proofs).
Also add trivial instance for the unit type.
|
|
- in particular at monadic interfaces (i.e., sufficient for instruction
ast types)
- see commented out part of test/coq/pass/ast_with_dep_tuple.sail for an
example that's not currently supported
- generate definitions for type-level Bool definitions (i.e., predicates)
|
|
|
|
-coq_alt_modules2 <filename> provide additional alternative modules to open only in main (non-_types) Coq output, and suppress default definitions of MR and M monads
|
|
|
|
|
|
|
|
|
|
|
|
Also don't require a previously declared default vector indexing order
in vector_dec.sail.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Remove P_record as it's never been implemented in
parser/typechecker/rewriter, and is not likely to be. This also means
we can get rid of some ugliness with the fpat and mfpat types. Stubs
for P_or and P_not are left as they still may get added to ASL and we
might want to support them, although there are good reasons to keep
our patterns simple.
The lem warning for while -> while0 for ocaml doesn't matter because
it's only used in lem, and the 32-bit number warning is just noise.
|
|
Mostly in the Coq backend, plus a few testcases that use bitvector
builtins on poly-vectors (which works on some backends, but not Coq).
Also handle some additional list inclusion proofs in Coq.
|
|
|
|
Fixes #53
|
|
Loops measures are now abstracted over the variables so that they can be
used in proofs. Add total Hoare logic rules for until.
|
|
This reverts commit 3fb4cf236c0d4b15831576faa45c763853632568.
|
|
|
