| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
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.
|
|
Callable as either :f or :step_function
Allow // to be used as a comment in the interactive toplevel
|
|
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.
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Fixes #61
|
|
|
|
|
|
Tells the typechecker that, for example, in a block after
if (i < 0) then {
return ();
} else {
...
}
the constraint not(i < 0) holds. This is a useful pattern when
type-checking code generated from ASL.
|
|
|
|
|
|
Also uncovered a few other issues w.r.t lists
|
|
|
|
When returning a type from a letbinding we need to be careful that the
type it returns does not refer to any type variable that only exists for
the lifetime of the letbinding (because it was bound by it). Normally
this fails because any type variable bound in the inner letbinding won't
exist in the outer scope, but if it is shadowed this can cause an issue.
|
|
OCaml library
|
|
|
|
|
|
|
|
|
|
Also be more careful to avoid pattern bindings with identifiers to avoid
parsing clashes, eg `let 'bytes := ...` which is confused with the
notation for binary literals.
|
|
|
|
|
|
Useful for tracking down non-determinism
|
|
|
|
Was being overly conservative with nested structs and used an incorrect location for the error message
|
|
This is useful because an arbitrary vector of a fixed size N can be represented symbolically as a
vector of N symbolic values, whereas an arbitrary vector of arbitrary size cannot be easily
represented.
|
|
|
|
Instead handle it specially in c_backend, leaving the type information in the IR available for other consumers
|
|
(using match rather than let-and-projections because the latter would
be reduced by tactics like unfold)
|
|
|
|
execution
|
|
|
|
|
|
|
|
Now we less desugared ASL we'd like to translate some notions more idiomatically, such as bitfields
with names. However the current bitfield implementation in Sail is really ugly (entirely my fault)
This commit introduces a new flag -new_bitfields which changes the behavior of bitfields as follows
bitfield B : bits(32) = {
Field: 7..0
}
Is now treated as a struct with a single field called `bits`
register R : B
function main() -> unit = {
R[Field] = 0xFF;
assert(R[Field] == 0xFF)
}
then desugars as
R.bits[7..0] = 0xFF
and
assert(R.bits[7..0] == 0xFF)
which is much simpler, matches ASL and is probably how it should have worked all along
|
|
|
