| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
Also updated some of the documentation in the sail source code
|
|
Uses the typechecker tests for now. Also fix two minor bugs in pretty-printer
and rewriter uncovered by the tests.
|
|
|
|
- Remove vector start indices
- Library refactoring: Definitions in sail_operators.lem now use Bitvector
type class and work for both bit list and machine word representations
- Add Lem bindings to AArch64 and RISC-V preludes
TODO: Merge specialised machine word operations from sail_operators_mwords into
sail_operators.
|
|
This removes all type polymorphism, so we can generate optimized
bitvector code and compile to languages without parametric
polymorphism.
|
|
typechecking bug
|
|
|
|
|
|
// is a comment
as well as
/* is a comment */
|
|
Fix a typechecking bug involving constraints attached to type synonyms
within existentials.
|
|
|
|
|
|
|
|
|
|
(no vector type start position, comment syntax)
|
|
Changed -mono-split to -mono_split to be consistent with other options
that use underscores, -mono-split still works but gives a warning
message, just so nothing breaks immediately because of this.
Removed this sil commands since they really don't do anything right
now.
|
|
|
|
Fixed test cases for ocaml backend and interpreter
|
|
|
|
This change allows the AST to be type-checked after sizeof
re-writing. It modifies the unification algorithm to better support
checking multiplication in constraints, by using division and modulus
SMT operators if they are defined.
Also made sure the typechecker doesn't re-introduce E_constraint
nodes, otherwise re-checking after sizeof-rewriting will re-introduce
constraint nodes.
|
|
Also drop redundant unit expressions when concatenating with an empty block.
|
|
In particular, there is an ASL pattern with single-branch if-expressions
containing an early return (and an empty else-branch), e.g.
{
...
if (error) then return(Fault) else ();
...
return(Success);
}
The rewriting pass now tries to fold the rest of the block into the
else-branch, since it is unreachable after the then-branch, e.g.
{
...
if (error) then return(Fault) else {
...
return(Success);
}
}
In combination with other rewriting rules, this allows the rewriting pass to
pull out the early returns if *all* branches end in a return statement. If it
is possible to pull out the return all the way, i.e., so that the function body
is a single return statement, then the return can be removed. If that is not
possible, then the function body is left as it was originally.
|
|
Use Tarjan's algorithm for finding strongly connected components (and finding a
topological sorting of components at the same time), in order to properly take
into account mutually recursive functions. The sorting is stable, i.e.,
definitions are only moved when necessary. Exceptions to this are statements
that do not have any dependencies: default bitvector order declarations,
operator fixity declarations, and top-level comments. These are moved to the
beginning (like with the previous sorting implementation).
Any dependency cycles that are found are additionally printed to the console in
dot-format, for easy visualisation with graphviz.
|
|
We add the generated ARM no_vector spec from the public v8.3 XML
release, mostly so that we can add end-to-end test cases for sail
using it. This kind of large example is very useful for thoroughly
testing the sail compiler and interpreter.
|
|
|
|
|
|
|
|
Currently doesn't try to compile to lem or use the MIPS spec
All the failing tests have been removed because I intend to handle
them differently - they were very fragile before because there was no
indication of why they failed, so as sail evolved they tended to start
failing for the wrong reasons and not testing what they were supposed
to.
|
|
Monomorphisation sometimes produces pattern guard with let-bindings, e.g.
| ... if (let regsize = size_itself(regsize) in eq(regsize, 32)) -> ...
Previously, the rewriting pass for let-bindings (and pattern guards) pulled
these out of the guard condition and into the same scope as the case
expression, which potentially clashed with let-bindings for the same variables
in that case expression. The rewriter now leaves let-bindings in place within
pure if-conditions, solving this problem.
|
|
Keep track of which type variables have been bound in the function declaration,
and allow those to be pretty-printed
|
|
|
|
|
|
|
|
(rather than for each argument separately)
|
|
|
|
Previously we only did top-level literal pattern to guard conversion, this
does it throughout any pattern
|
|
|
|
|
|
Otherwise the type checker can't figure it out when we substitute
|
|
|
|
|
|
|
|
|
|
New testcase for bitfield syntax
Updated to work with latest lem and linksem
|
|
|
