| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
