| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Previous merge commit caused some code that was generating
register.field = value
to instead generate
temp = register
temp.field = value
register = temp
This was caused by rewriter changes affecting the ANF form, and the Jib
compilation was sensitive to small changes in the ANF form when
compiling l-expressions. Rather than applying a band-aid fix in the
rewriter this commit re-factors the ANF translation of l-expressions to
ensure that the jib compilation is more robust and able to consistently
generate the correct l-expressions without introducing additional
read-modify-write expressions in the code.
|
|
See sailcov/README.md for a short description
Fix many location info bugs discovered by eyeballing output
|
|
|
|
Will call:
void sail_branch_reached(int branch_id, char *source_file, int l1, int c1, int l2, int c2);
on each branch caused by a match or if statement in the source code
For each branch that is taken, will call:
void sail_branch_taken(int branch_id, char *source_file, int l1, int c1, int l2, int c2)
Every branch gets a unique identifier, and the functions are called with
the source file location and line/character information for the start
and end of each match case or then/else branch. sail_branch_reached is
given the location info for the whole match statement.
|
|
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.
|
|
The have_exception flag wasn't being cleared until after the handler,
resulting in false exception reporting.
|
|
|
|
Useful for tracking down non-determinism
|
|
|
|
Instead handle it specially in c_backend, leaving the type information in the IR available for other consumers
|
|
execution
|
|
|
|
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.
|
|
|
|
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
|
|
|
|
|
|
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
|
|
|
|
|
|
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.
|
|
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.
|
|
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.
|
|
Add an Assumption event that is true whenever a property's type
quantifier is true, rather than wrapping body in a if-statement that
ends up creating a dead branch.
|
|
SMT query now expressed as a logical expression over events, so e.g.
let default_query =
Q_or [Q_and [Q_all Assertion; Q_all Return; Q_not (Q_exist Match)]; Q_exist Overflow]
Checks either an overflow occurred, or the function returned true,
while all assertions held, and no match failures occurred. Currently
there is only the default query but the plan is to make this
user-specifiable in the $property/$counterexample directives.
|
|
|
|
Add a new AE_write_ref constructor in the ANF representation to
make writes to register references explicit in Jib_compile
|
|
|
|
|
|
Generates much better SMT that assigning each field one-by-one
starting with an undefined struct.
|
|
|
|
|
|
Currently only supports pure termination measures for loops with effects.
The user syntax uses separate termination measure declarations, as in the
previous recursive termination measures, which are rewritten into the
loop AST nodes before type checking (because it would be rather difficult
to calculate the correct environment to type check the separate declaration
in).
|
|
|
|
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.
|
|
Most such patterns are re-written away by various re-writing steps,
but for those that arn't they are fairly easy to handle by just having
as patterns directly in the ANF-patterns.
Fixes #39
|
|
Add a test case to ensure variable types in l-expressions remain the
same with flow-sensitive constraints.
|
|
Remove unused experimental optimizations
|
