Releases: rems-project/sail
0.17.1
0.17
CHANGES:
Performance improvements
This release is primarily intended to fix performance issues. Overall
the Sail to C compilation can be almost 10x faster, and consumes
significantly less memory.
Order parameters deprecated
The order parameter on the bitvector and vector types no longer does
anything. The default Order <ord> statement now sets the bitvector
and vector ordering globally. In practice only POWER uses increasing
bit order, and there is never a valid reason to mix them in a
specification. Overall they added significant complexity to the
language for no real gain. Over subsequent releases a warning will be
added before they are eventually removed from the syntax.
String append pattern rework
For a while string append patterns x ^ y have been marked with a
special non-executable effect that forbids them from being used. Now
the implementation has been removed due to the deleterious effect
the generated code has on performance. Such clauses are now eagerly
removed from the syntax tree during rewriting pending a revised
implementation.
SystemVerilog backend (EXPERIMENTAL)
Sail can now produce SystemVerilog output using the -sv flag. Note
that this is not intended to be human readable or produce a
synthesizable design, but is instead intended to be used with
SystemVerilog verification tools like JasperGold.
0.16
CHANGES:
New documentation backend
A new documentation backend for integrating with Asciidoctor has been
added.
Automatic formatting (EXPERIMENTAL)
The sail -fmt option can be used to automatically format Sail
source. This currently misses some features and can produce ugly
output in some known cases, so is not ready for serious usage yet.
Fixes
Various bugfixes including:
Various mapping issues such as:
- Issue 244: #244
As well as other minor issues
The val cast syntax and support for implict casts is now entirely
removed, as mentioned in the previous release changes. The flags are
still allowed (to avoid breaking Makefiles) but no longer do anything.
The pattern completeness checker has been improved and is now context
sensitive in some cases.
0.15
CHANGES:
More modular codebase and dune build system
The Sail internals have been refactored into seperate packages for
each Sail backend (c/lem/coq and so on). The shared parts of Sail are
now contained in a separate libsail OCaml library. The main Sail
executable links together all the Sail backends into a single
executable.
With this architecture new backends can be implemented outside the
main Sail repository as plugins, and loaded via sail -plugin.
The Sail build system has been transitioned from the legacy ocamlbuild
system to dune.
This has been a significant refactoring of the core Sail codebase, and
while all efforts have been taken to ensure backwards-compatibility
and minimize any potential breakage, it is possible there exists some.
New pattern completeness checker
Sail now has a new pattern completeness checker that can generate
counterexamples for incomplete patterns. It is designed to be less
noisy, as it only issues warnings when it can guarantee that the
pattern is incomplete.
Implicit casts now forbidden by default
Previously they were only forbidden by the -dno_cast flag (which is
used by both sail-riscv and sail-arm). This behavior is now the
default and this flag is ignored. The -allow_deprecated_casts flag
must be used to enable this now. Implicit casts will be fully removed
in the next Sail release.
New concurrency interface (EXPERIMENTAL)
This release contains a new way of interfacing with external
concurrency models by way of user defined effects. See
lib/concurrency_interface for an example. This is currently
experimental and not fully supported in all backends. Definition of
new effects is currently only allowed with the $sail_internal
directive (see below).
No more explicit effect annotations (DEPRECATION)
Explicit effect annotations are now deprecated and do nothing. This
change relates to the previous change to allow custom outcomes in the
event monad, as the effect system no-longer corresponded in any
meaningful way with whether functions would become monadic or not in
Sail's theorem prover backends.
Function specifications (val keyword) can now be marked as pure. If
this is done, the functions must have no side-effects. The
requirements for a function to be pure in this sense are stricter than
they were previously - a pure function must not:
- Throw an exception
- Exit (either explicitly or by failing an assertion)
- Contain a possibly incomplete pattern match
- Read or write any register
- Call any impure function
This more strict notion of purity fixes some long-standing bugs when
generating theorem prover definitions from Sail.
Note that functions do not have to be explictly marked pure to be
considered pure. Purity will be inferred automatically. The pure
annotation is used to declare primitive functions as pure, and make it
a hard error if a function is inferred to be impure.
There are two places in the language where code must be pure:
- Top level let-bindings
let x = exp - Loop and function termination measures
Stricter typechecking for mutable variables (MINOR BREAKING)
Previously Sail allowed some assignment constructions that were a bit
complex, for example one could declare a variable and modify an
existing one in the same statement, e.g.
x: int = 1;
(x, y: int) = (2, 3);
This is now forbidden, so l-expressions can either modify existing
variables or declare new ones, but never both simultaneously. This
change is primarily to increase readability, and simplify the language
internally.
In the future we may move further towards a world where new
assignments must be declared with a var keyword, like the let
keyword.
Variable declarations are now forbidden in places where their scope is
not syntactically obvious, for example:
val f : (unit, int) -> unit
...
f(x: int = 3, x)
The breakage caused by this change should be minor as we hope
well-written Sail specifications do not declare variables in this way.
GCC style error message formatting
Error messages are now formatted as per:
https://www.gnu.org/prep/standards/standards.html#Errors
which should allow better editor integration
sail_internal directive
A new directive $sail_internal has been introduced. When placed in a
file this allows the use of experimental or unstable functionality. It
also allows the use of various identifiers that are ordinarily
forbidden. Its primary purpose is to allow the Sail library to be
implemented using new unstable features that may change, without them
being exposed (and therefore relied upon) by downstream users.
As such, any Sail file using this directive may become broken at any
point.