| Age | Commit message (Collapse) | Author |
|---|
|
Means we can avoid the use of -undefined_gen for Sail->SMT
|
|
|
|
|
|
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.
|
|
|
|
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")
}
}
}
|
|
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
|
|
|
|
|
|
|
|
|
|
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
|
|
|
|
|
|
|
|
|
|
|
|
for 'exception.sail' test that deliberately exits with uncaught exception.
|
|
|
|
|
|
|
|
|
|
|
|
Insert coercions for AV_cval if neccessary
Simplify any n in 2 ^ n, to make sure we can always evaluate 2 ^ n when
n is a constant before passing it to the SMT solver.
|
|
Add a test case for this
|
|
|
|
Clean up ott grammar a bit
|
|
|
|
|
|
|
|
|
|
Allow conversion between int(n) and int in smt_conversion
|
|
|
|
Also add a $suppress_warnings directive that ensures that no warnings
are generated for a specific file.
|
|
We want to ensure simplication can treat these separately so we
don't accidentally simplify away dependencies between reads and write
addresses.
|
|
Add path conditions to memory events
Allow simplication of generated SMT based on constructor kinds
|
|
Only change that should be needed for 99.9% of uses is to change
vector('n, 'ord, bit) to bitvector('n, 'ord), and adding
$ifndef FEATURE_BITVECTOR_TYPE
type bitvector('n, dec) = vector('n, dec, bit)
$endif
for to support any Sail before this
Currently I have all C, Typechecking, and SMT tests passing, as well
as the RISC-V spec building OCaml and C completely unmodified.
|
|
|
|
Expose AST -> Jib compilation function for SMT, and smt_header function
Functorise the optimiser so it can output the SMT definitions to
any data structure
|
|
Generate addresses, kinds, and values separately for read and write
events.
Add an mli interface for jib_smt.ml
|
|
Allows us to mix generated SMT for two separate threads without name
clashes, however we do want to be able to share datatypes so they are
not prefixed. Currently the pretty-printer adds the prefix but we may
want a smt_def -> smt_def renaming function instead.
|
|
Since we have __deref to desugar *x in this file (as it's the one file
everything includes) we might as well add a __bitfield_deref here too,
for the bitfield setters.
Make sure undefined_nat can be used in C
Both -memo_z3 and -no_memo_z3 were listed as default options, now only
-no_memo_z3 is listed as the default.
|
|
|
|
Generate SMT where the memory reads and writes are totally
unconstrained, allowing additional constraints to be added that
restrict the possible reads and writes based on some memory model.
|
|
|
|
|
