| Age | Commit message (Collapse) | Author |
|---|
|
- add liftRS support to tactics
- define uint and sint in terms of functions without proof terms
- eq_vec correctness
- lemma that rounding up integers using reals is the obvious integer calculation
- another proof irrelevance tactic
- try lemmas in the sail hintdb both before and after goal processing
|
|
- break up goals more in unbool
- remove intuition from guess_ex_solver because it can be too expensive
- flip goals around because the side that evars appears on has changed
- generalise the and/or tactics
- make a couple of tactics more specific/robust
|
|
Includes removing an explicit use of a lemma generated by abstract, which
was causing problems with different versions of Coq because the names
change.
|
|
Mostly from making the aarch64 model compile again
- switch order some arithmetic lemmas
- move list membership rewrites alongside other comparisons to enable more
rewriting
- copy hypotheses used in other types/definitions so that they can be
rewritten
- lift boolean existentials out of implications in hypotheses so they can
be used as witnesses without proving the condition
- add negation to solve_bool_with_Z
- add some new bool solving for goals from and_boolMP/or_boolMP
|
|
(plus test, as it wasn't covered before)
|
|
- ArithFact takes a boolean predicate
- defined in terms of ArithFactP, which takes a Prop predicate,
and is used directly for existentials
- used abstract in more definitions with direct proofs
- beef up solve_bool_with_Z to handle more equalities, andb and orb
|
|
|
|
|
|
Means we can avoid the use of -undefined_gen for Sail->SMT
|
|
|
|
|
|
(which might not be present).
|
|
|
|
- add state versions of foreach combinators
- support dependent sumbool pattern matching (i.e., those where the
property is actually used)
- add rewriting congruence rules, state monad lifting rules,
and invariant proof rules for these
|
|
|
|
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
|
|
|
|
|
|
Some builtins need properly implementing still
Use modified spinlock implementation from hafnium with stdatomic,
rather than assembly
|
|
|
