| Age | Commit message (Collapse) | Author |
|---|
|
(both off by default)
|
|
|
|
|
|
|
|
|
|
|
|
While the backends will usually manage to find the constant size anyway,
this ensures that implicit arguments will be filled in with the constant
value too. (For example, this was affecting isla execution in one corner
case because the slice_mask primitive didn't see that the size was
constant.)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This can be useful to reference things that aren't defined by sail.
|
|
This is for a bug I encountered while moving some docs over from the ISA
spec into sail documentation comments.
|
|
Also fix a few shellcheck warnings related to printf while doing so.
|
|
Both /.gitignore and /lib/coq/.gitignore ignored some files in /lib/coq.
This commit removes /lib/coq/.gitignore and moves all ignore-statements
to /.gitignore . This should simplify the maintenance of gitignore files.
The situation with /test/mono/.gitignore is analogous.
|
|
- add tests for a couple of related rewrites
- accept same range of constants for sign extension in the rewrite as for
the zero extension version (to make the test simpler)
|
|
|
|
|
|
|
|
|
|
|
|
Avoids generating an assert expression with an escape effect.
Mirrors existing case for `if cond { throw(...); };`.
No longer requires `-non_lexical_flow`.
|
|
(currently supported in nl_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
|
|
|
|
|
|
|
|
Location info fixes changed the location reported for an expected type error very slightly
|
|
|
|
|
|
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.
|
|
|
|
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.
|
|
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.
|
|
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.
|
|
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
|
|
|
|
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.
|
