| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Don't include length and indexing order in Regval_vector constructor, as
these can get in the way of proofs without providing any value.
|
|
If, for example, we have a bidirectional encoding-decoding mapping as in
sail-riscv, but want to translate only the decoder to a theorem prover,
this commit allows us to stub out the the encoder by splicing in dummy
definitions.
|
|
|
|
The val spec generation for partially evaluated function copies did not
pick up type variables originally declared using the new "constant"
syntax, as well as some implicit existential variables (e.g. in "bool")
that were not declared originally but appear and get bound during
instantiation. Change the code to just recreate the list of type
variables from scratch from the new type. This will lose "constant"
annotations, but the new list of type variables should be correct.
|
|
When considering whether to add a cast, now also consider the updated
environment within an if branch / match clause to compare against the
outer environment. This picks up not only constraints on type variables
added by an if condition or pattern guard (e.g. "if (size == 16) ..."),
but also constraints depending on those (e.g. in "bits('width)" where
"'width == 'size * 8"). Fixes a type error observed when generating Lem
for sail-arm (in aget__Mem).
|
|
... with one field per register *type*, instead of one field per
register. The fields store functions from register name to value.
This leads to dramatically reduced processing time for the register
state record in HOL4.
|
|
|
|
Means we can avoid the use of -undefined_gen for Sail->SMT
|
|
|
|
|
|
Also don't include the toplevel files in the library, and move
load_files and descatter into process_file where they can be called
|
|
Also make the Error type private, so it's only constructed through the
functions we expose in reporting.mli
|
|
Split the dynamic context into the ctx struct, and the static
configuration into a module which parameterises the sail->jib
compilation step rather than just having a giant ctx struct.
|
|
sail2_instr_kinds was in the folder with the old lem interpreter for
some reason, rather than with all the other sail2*.lem files
|
|
|
|
: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.
|
