| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
It previously installed fine via the build-essential package, so no idea
what changed! Plus 20.04 works fine with just build-essential
|
|
|
|
Add opam PPA when building on Ubuntu to get opam v2.
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Add static to more C functions
|
|
|
|
|
|
Otherwise the C emulator doesn't build.
|
|
This simplifies some of the code.
|
|
|
|
|
|
Colours can be tweaked for aesthetics by setting hue and saturation
individually or there is an --alt-colo[u]rs flag which switches to a
yellow/blue mode that should be better for red/green colourblindness.
|
|
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.
|
|
|
|
Location info fixes changed the location reported for an expected type error very slightly
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
