| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Currently uses the -c2 option
Now generates a sail_state struct which is passed as a pointer to all
generated functions. This contains all registers, letbindings, and the
exception state. (Letbindings must be included as they can contain
pointers to registers). This should make it possible to use sail models
in a multi-threaded program by creating multiple sail_states, provided a
suitable set of thread-safe memory builtins are provided. Currently the
sail_state cannot be passed to the memory builtins.
For foo.sail, now generate a foo.c, foo.h, and (optionally) a foo_emu.c.
foo_emu.c wraps the generated library into an emulator that behaves the
same as the one we previously generated.
The sail_assert and sail_match_failure builtins are now in a separate
file, as they must exist even when the RTS is not used.
Name mangling can be controlled via the exports and exports_mangled
fields of the configuration struct (currently not exposed outside of
OCaml). exports allows specifying a name in C for any Sail identifier
(before name mangling) and exports_mangled allows specifiying a name for
a mangled Sail identifier - this is primarily useful for generic
functions and data structures which have been specialised.
|
|
Useful for tracking down non-determinism
|
|
This is useful because an arbitrary vector of a fixed size N can be represented symbolically as a
vector of N symbolic values, whereas an arbitrary vector of arbitrary size cannot be easily
represented.
|
|
|
|
|
|
Means we can avoid the use of -undefined_gen for Sail->SMT
|
|
|
|
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.
|
|
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
|
|
Previously path conditionals for a node were defined as the path
conditional of the immediate dominator (+ a guard for explicit guard
nodes after conditional branches), whereas now they are the path
conditional of the immediate dominator plus an expression
encapsulating all the guards between the immediate dominator and the
node. This is needed as the previous method was incorrect for certain
control flow graphs.
This slows down the generated SMT massively, because it causes the
path conditionals to become huge when the immediate dominator is far
away from the node in question. It also changes computing path
conditionals from O(n) to O(n^2) which is not ideal as our inlined
graphs can become massive. Need to figure out a better way to generate
minimal path conditionals between the immediate dominator and the
node.
I upped the timeout for the SMT tests from 20s to 300s each but this
may still cause a failure in Jenkins because that machine is slow.
|
|
Jib_compile now has an option that lets it generate real value
literals (VL_real), which we don't want for backends (i.e. C), which
don't support them. Reals are encoded as actual reals in SMT, as there
isn't really any nice way to encode them as bitvectors. Currently we
just have the pure real functions, functions between integers and
reals (i.e. floor, to_real, etc) are not supported for now.
Strings are likewise encoded as SMTLIB strings, for similar reasons.
Jib_smt has ctx.use_real and ctx.use_string which are set when we
generate anything real or string related, so we can keep the logic as
Arrays+Bitvectors for most Sail that doesn't require either.
|
|
|
|
|
|
Fixes C backend optimizations that were disabled due to changes in the
IR while working on the SMT generation.
Also add a -Oaarch64_fast option that optimizes any integer within a
struct to be an int64_t, which is safe for the ARM v8.5 spec and
improves performance significantly (reduces Linux boot times by 4-5
minutes). Eventually this should probably be a directive that can be
attached to any arbitrary struct/type.
Fixes the -c_specialize option for ARM v8.5. However this only gives a
very small performance improvment for a very large increase in
compilation time however.
|
|
Need to get these working again before we can thing about merging back
into sail2
|
|
Get rid of separate V_op and V_unary constructors. jib.ott now defines
the valid operations for V_call including zero/sign extension, in such
a way that the operation ctyp can be inferred. Overall this makes the
IR less ad-hoc, and means we can share more code between SMT and C.
string_of_cval no longer used by c_backend, which now uses sgen_cval
following other sgen_ functions in the code generator, meaning
string_of_cval doesn't have to produce valid C code anymore and so can
be used for backend-agnostic debug and error messages.
|
|
|
|
|
|
|
|
Generates much better SMT that assigning each field one-by-one
starting with an undefined struct.
|
|
|
|
Had to change the hundreds and hundreds of places such values were
used. However this now lets us automatically prove cheri-concentrate
properties. Such as showing
function prop_cap_round_trip(cap: bits(128)) -> bool = {
let cap_rt = capToBits(capBitsToCapability(true, cap));
cap == cap_rt
}
is always true.
|
|
Currently only works with CVC4, test cases are in test/smt. Can prove
that RISC-V add instruction actually adds values in registers and
that's about it for now.
|
|
- Rename DeIid to Operator. It corresponds to operator <string> in the
syntax. The previous name is from when it was called deinfix in
sail1.
- Removed things that weren't actually common from
pretty_print_common.ml, e.g. printing identifiers is backend
specific. The doc_id function here was only used for a very specific
use case in pretty_print_lem, so I simplified it and renamed it to
doc_sia_id, as it is always used for a SIA.Id whatever that is.
- There is some support for anonymous records in constructors, e.g.
union Foo ('a : Type) = {
MkFoo : { field1 : 'a, field2 : int }
}
somewhat similar to the enum syntax in Rust. I'm not sure when this
was added, but there were a few odd things about it. It was
desugared in the preprocessor, rather than initial_check, and the
desugaring generated incorrect code for polymorphic anonymous
records as above.
I moved the code to initial_check, so the pre-processor now just
deals with pre-processor things and not generating types, and I
fixed the code to work with polymorphic types. This revealed some
issues in the C backend w.r.t. polymorphic structs, which is the
bulk of this commit. I also added some tests for this feature.
- OCaml backend can now generate a valid string_of function for
polymorphic structs, previously this would cause the ocaml to fail
to compile.
- Some cleanup in the Sail ott definition
- Add support for E_var in interpreter previously this would just
cause the interpreter to fail
|
|
Previously the specialization would remove any polymorphic union
constructor that was never created anywhere in the
specification. While this wasn't usually problematic, it does leave an
edge case where such a constructor could be matched upon in a pattern,
and then the resulting match would fail to compile as it would be
matching on a constructor kind that doesn't exists.
This should fix that issue by chaging the V_ctor_kind value into an
F_ctor_kind fragment. Previously a polymorphic constructor-kind would
have been represented by its mangled name, e.g.
V_ctor_kind "zSome_unit"
would now be represented as
V_ctor_kind ("Some", unifiers, ty)
where ty is a monomorphic version of the original constructor's type
such that
ctyp_unify original_ty ty = unifiers
and the mangled name we generate is
zencode_string ("Some_" ^ string_of_list "_" string_of_ctyp unifiers)
|
|
Allows us to track the last version of the return variable when the AST
in in SSA form.
|
|
Add a test case to ensure variable types in l-expressions remain the
same with flow-sensitive constraints.
|
|
Remove unused experimental optimizations
|
|
Add a function Jib_optimize.inline which can inline functions. To make
this more efficient, we can make identifiers unique on a per-function
basis.
|
|
Avoids duplication between l-expressions and expressions. Also means that
special variables like current_exception and have_exception are treated
normally by functions such as instr_reads and instr_writes etc. Furthermore
we can now easily annotate Jib identifiers in ways that were not previously
possible with plain sail ids.
|
|
Add a CL_void l-expression so we don't have redundant unit-typed
variables everywhere, and add an optimization in Jib_optimize called
optimize_unit which introduces these.
Remove the basic control-flow graph in Jib_util and add a new mutable
control-flow graph type in Jib_ssa which allows the IR to be converted
into SSA form. The mutable graph allows for more efficient updates,
and includes both back and forwards references making it much more
convenient to traverse.
Having an SSA representation should make some optimizations much
simpler, and is also probably more natural for SMT generation where
variables have to be defined once using declare-const anyway.
Debug option -ddump_flow_graphs now outputs SSA'd graphs of the
functions in a specification.
|
|
For a Int-parameterised struct F('x: Int) = ... the optimizer would
attempt to optimize field access in cases where 'x was known to
constrain the types of the struct fields only locally. Which would
create a type error in the generated C. Now we always use the type
from the global struct type.
However, we previously weren't using struct type quantifiers to
optimize the field representation, which we now do.
Also rename some utility functions to better match the List
functions in the OCaml stdlib.
|
|
Main change is splitting apart the Sail->IR compilation stage and the
C code generation and optimization phase. Rather than variously
calling the intermediate language either bytecode (when it's not
really) or simply IR, we give it a name: Jib (a type of Sail). Most of
the types are still prefixed by c/C, and I don't think it's worth
changing this.
The various parts of the C backend are now in the src/jib/ subdirectory
src/jib/anf.ml - Sail->ANF translation
src/jib/jib_util.ml - various Jib AST processing and helper functions (formerly bytecode_util)
src/jib/jib_compile.ml - Sail->Jib translation (using Sail->ANF)
src/jib/c_backend.ml - Jib->C code generator and optimizations
Further, bytecode.ott is now jib.ott and generates jib.ml (which still
lives in src/ for now)
The optimizations in c_backend.ml should eventually be moved in a
separate jib_optimization file.
The Sail->Jib compilation can be parameterised by two functions - one
is a custom ANF->ANF optimization pass that can be specified on a per
Jib backend basis, and the other is the rule for translating Sail
types in Jib types. This can be more or less precise depending on how
precise we want to be about bit-widths etc, i.e. we only care about <64
and >64 for C, but for SMT generation we would want to be as precise
as possible.
Additional improvements:
The Jib IR is now agnostic about whether arguments are allocated on
the heap vs the stack and this is handled by the C code generator.
jib.ott now has some more comments explaining various parts of the Jib
AST.
A Set module and comparison function for ctyps is defined, and some
functions now return ctyp sets rather than lists to avoid repeated
work.
|
