| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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 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).
|
|
|
|
Split the variable (tuple) type into an input and output type. They are
meant to be the same, but due to the way function types are
instantiated, unification can fail in the case of existential types, as
in the added test case (when trying to generate Lem definitions from
it). The output of the loop will be checked against the expected type,
though, due to a type annotation outside the loop added by the rewrite
pass for variable updates.
|
|
|
|
|
|
... instead of a tuple assignment. This makes the rewrite independent
of the tuple assignment rewrite and allows it to be moved after the
latter (nesting vector concat lexps into tuple lexps is an idiom in ASL,
but the other way around doesn't make sense).
|
|
In particular, don't add annotations for types with existentially
quantified variables that only occur in constraints, not in the type,
e.g. {'i1 'i2, 'i1 == div('i2, 8). int('i1)}. These seem to confuse the
type checker when pulled out into the source AST.
|
|
sail -i now starts an interactive toplevel with a few additional
options set by default:
- It applies the "interpreter" rewrites to any files passed on the command
line.
- It also applies those rewrites after the :l/:load command
- Registers previously started in a disabled state, as the interactive shell
made no default decision as to how to handle undefined (which is the initial
value for all registers). Now -i implies -undefined_gen
- Better help text for :fix_registers
- Nullary interactive actions generate Sail functions that round-trip through pretty
printing and parsing (bugfix)
The -interact_custom flag has the same behavior as the previous -i flag
This commit also improves the c/ocaml/interpreter test harness so it
cleans up temporary files which could cause issues with stale files
when switching ocaml versions
|
|
Allows clients of sail as a library to define custom symbols for $ifdef
and $ifndef
Iterate vector concat assignment and tuple assignment to handle unusual
nesting cases when compiling to C. These rewrites should really be one
rewrite anyway though!
Don't add type annotations when introducing tuple patterns during
rewriting. I guess not adding them could also cause an error in some
circumstances, but if that's the case it could probably be fixed by
tweaking some rules in the type-checker.
|
|
In the new version of the ASL-generated Sail, some vector operators are
also overloaded for integers to match idioms of ASL (e.g. i[31:0], where
i is an integer), so check in the monomorphisation rewrites that we use
bitvector helper functions only for actual bitvectors.
|
|
... instead of dying with "Syntax error".
|
|
... that match the names in lib/real.sail.
Also fix the lem mapping for abs_int_atom and a Lem syntax error with
nested record updates.
|
|
Check that indices are within bounds, not just in the right
(increasing/decreasing) order.
|
|
|
|
Asserting constraints from the loop condition in the body is fine for
while-loops, but doesn't make sense for until-loops.
|
|
|
|
|
|
|
|
From:
No type variable 'ex14#
to:
Type error:
[../and_let_bool.sail]:6:19-50
6 | and_bool(let y : bool = x in not_bool(y), x)
| ^-----------------------------^
| The type variable 'ex14# would leak into an outer scope.
|
| Try adding a type annotation to this expression.
| This error was caused by:
| [../and_let_bool.sail]:6:23-24
| 6 | and_bool(let y : bool = x in not_bool(y), x)
| | ^
| | Type variable 'ex14# was introduced here
|
|
|
Allows ASL-to-Sail translation to automatically patch lexp bounds check
errors.
|
