| Age | Commit message (Collapse) | Author |
|---|
|
|
|
This refactoring is intended to allow this type to have more than just a
list of definitions in future.
|
|
sail -i now starts an interactive toplevel with a few additional
options set by default:
- It applies the "interpreter" rewrites to any files passed on the command
line.
- It also applies those rewrites after the :l/:load command
- Registers previously started in a disabled state, as the interactive shell
made no default decision as to how to handle undefined (which is the initial
value for all registers). Now -i implies -undefined_gen
- Better help text for :fix_registers
- Nullary interactive actions generate Sail functions that round-trip through pretty
printing and parsing (bugfix)
The -interact_custom flag has the same behavior as the previous -i flag
This commit also improves the c/ocaml/interpreter test harness so it
cleans up temporary files which could cause issues with stale files
when switching ocaml versions
|
|
This allows read_mem and read_reg effects to be handled by GDB
|
|
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")
}
}
}
|
|
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.
|
|
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.
|
|
Can now use C-c C-s to start an interactive Sail process, C-c C-l to
load a file, and C-c C-q to kill the sail process. Type errors are
highlighted in the emacs buffer (like with merlin for OCaml) with a
tooltip for the type-error, as well as being displayed in the
minibuffer. Need to add a C-c C-x command like merlin to jump to the
error, and figure out how to handle multiple files nicely, as well as
hooking the save function like tuareg/merlin, but this is already
enough to make working with small examples quite a bit more pleasant.
|
|
Work on improving the formatting and quality of error messages
When sail is invoked with sail -i, any type errors now drop the user
down to the interactive prompt, with the interactive environment being
the environment at the point the type error occurred, this means the
typechecker state can be interactively queried in the interpreter to help
diagnose type errors.
|
