| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
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.
|
|
|
|
Defined in terms of tdiv so we don't have to add it to backends that
don't already have it
|
|
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.
|
|
This will constant-fold letbindings such as
let LOG2_TAG_GRANULE : int(4) = 4
let TAG_GRANULE : int = (1 << LOG2_TAG_GRANULE)
which is useful for the translation to Lem if TAG_GRANULE is used in
bitvector lengths.
|
|
- Handle more combinations of patterns and expressions in constant
propagation
- Remove dead code after throw() in monomorphisation
- Use correct val specs and environments when analysing and
pretty-printing function clauses
|
|
This check is used in the guarded pattern rewrite step, which would
previously generate some impossible matches (e.g. matching expression
"true" against pattern "false").
|
|
|
|
Add casts for function arguments using the constraints in the
environment of the function clause (not just assertions within the
function body). Also pass in the global typing environment for
comparison with the environment within the function clause (and make a
corresponding change in the Lem pretty-printer so that it uses the right
environments).
|
|
|
