| Age | Commit message (Collapse) | Author |
|---|
|
c2: primop: -O: make sure to pick global or name correctly
|
|
exist as constructor or function
|
|
|
|
|
|
|
|
Accidentally broken by e1a2b0d2 because the Coq backend looks at the
wrong type to decide when a proof is needed.
|
|
Avoids generating an assert expression with an escape effect.
Mirrors existing case for `if cond { throw(...); };`.
No longer requires `-non_lexical_flow`.
|
|
Helps with Coq 8.11. Also fix BBVDIR default in test script.
|
|
|
|
- rename files to get rid of prefix
- use -Q to get package name right
- add Base.v to make package imports simpler
- add opam file for coq package
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
Otherwise the C emulator doesn't build.
|
|
This simplifies some of the code.
|
|
This was the final missing step for me to link two almost identical C files
generated from sail into the same library.
|
|
I was getting run-time failures when code generate from cheri128 and
cheri64 in the same process. This was caused because my compiler defaults
to -fcommon so it merged multiple variables (with conflicting types!).
When initializing the second set of letbindings, the first one was
overwritten (first variable was lbits, the other was uint64_t). Compiling
with -fno-common exposes this problem.
|
|
Without this I get the following linker error when trying to include both
64 and 128 bit sail-riscv code in the same binary:
duplicate symbol '_model_init' in:
libsail_wrapper128.a(sail_wrapper_128.c.o)
libsail_wrapper128.a(sail_wrapper_64.c.o)
duplicate symbol '_model_main' in:
libsail_wrapper128.a(sail_wrapper_128.c.o)
libsail_wrapper128.a(sail_wrapper_64.c.o)
duplicate symbol '_model_fini' in:
libsail_wrapper128.a(sail_wrapper_128.c.o)
libsail_wrapper128.a(sail_wrapper_64.c.o)
# Conflicts:
# src/jib/c_backend.ml
|
|
This allows me to compile sail-riscv64 and sail-riscv128 code in the same
static library.
|
|
See sailcov/README.md for a short description
Fix many location info bugs discovered by eyeballing output
|
|
Fixes the warning generated because in C -X where X is the minimum integer is
parsed as a positive integer which is then negated. This causes a (I
believe spurious) warning that the integer literal is too large for the type.
Also using INT64_C so we get either long or long long depending on
platform
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
All the code-generator options can now be controlled via a json
configuration file
Extra fields can be added to the sail_state struct using a
codegen.extra_state key in the configuration json for the code
generator
If primitives want to modify the state they can be specified via
codegen.state_primops
To import such state, codegen.extra_headers can be used to add
user-defined headers to the generated .h file
|
|
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 monomorphisation analysis decides whether to split function
arguments in the callee or in callers. The code previously used a
datastructure that can hold results of either the one case or the other,
but there might be functions that are called in different contexts
leading to different decisions. This patch changes the datastructure to
support storing all instances of either case.
|
|
If we call a function where some arguments need to be rewritten, we
might need to rewrite those parameters in the caller as well.
|
|
|
|
The have_exception flag wasn't being cleared until after the handler,
resulting in false exception reporting.
|
|
Callable as either :f or :step_function
Allow // to be used as a comment in the interactive toplevel
|
|
|
|
In particular tuple types containing bitvectors.
|
|
Also add support for intialising variables with an "undefined" literal;
make the SMT solver treat the value as arbitrary but fixed.
|
|
Supporting more ASL idioms
|
|
For example, in
let datasize = e in ...
the typechecker will generate a kid '_datasize if e has an existential
type (with one kid), and in
let 'datasize = e in ...
the typechecker will bind both 'datasize and '_datasize. If we
substitute one as part of constant propagation, this patch will make
constant propagation also substitute the other.
|
|
... and try to resolve them using constant propagation.
|
|
Ask the type checker instead of looking at the expression syntax. This
also discovers implied instantiations, e.g. if we previously knew
('N in {32, 64}) and we have an assertion ('N != 32), then we know
('N == 64).
|
|
This will propagate constant assignments in chosen branches of case
expressions after applying pattern choices, e.g. the assignment to
datasize in
match size {
[bitone, _] => datasize = 64,
...
}
when pattern [bitone, _] is chosen for size.
|
