| 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.
|
|
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.
|
|
|
|
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
|
|
|
|
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)
|
|
|
|
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.
|
