| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
Gives warnings when pattern matches are incomplete, when matches are
redundant (in certain cases), or when no unguarded patterns exist. For
example the following file:
enum Test = {A, C, D}
val test1 : Test -> string
function test1 x =
match x {
A => "match A",
B => "this will match anything, because B is unbound!",
C => "match C",
D => "match D"
}
val test2 : Test -> string
function test2 x =
match x {
A => "match A",
C => "match C"
/* No match for D */
}
val test3 : Test -> string
function test3 x =
match x {
A if false => "never match A",
C => "match C",
D => "match D"
}
val test4 : Test -> string
function test4 x =
match x {
A if true => "match A",
C if true => "match C",
D if true => "match D"
}
will produce the following warnings
Warning: Possible redundant pattern match at file "test.sail", line 10, character 5 to line 10, character 5
C => "match C",
Warning: Possible redundant pattern match at file "test.sail", line 11, character 5 to line 11, character 5
D => "match D"
Warning: Possible incomplete pattern match at file "test.sail", line 17, character 3 to line 17, character 7
match x {
Most general matched pattern is A_|C_
Warning: Possible incomplete pattern match at file "test.sail", line 26, character 3 to line 26, character 7
match x {
Most general matched pattern is C_|D_
Warning: No non-guarded patterns at file "test.sail", line 35, character 3 to line 35, character 7
match x {
warnings can be turned of with the -no_warn flag.
|
|
|
|
|
|
|
|
|
|
|
|
(makes some of the monomorphisation case splits smaller)
|
|
for terminating the test.
|
|
Only add bindings for sub-patterns if they are actually used in the pattern
guard or expression, respectively.
|
|
Seems to increase compilation speed significantly for OCaml 4.05.
|
|
|
|
Use consistent nesting of tuples when adding updated local mutable variables to
expressions. Add test case.
|
|
Can now use C-style include declarations to include files within other sail files. This is done in such a way that all the location information is preserved in error messages. As an example:
$include "aarch64/prelude.sail"
$define SYM
$ifndef SYM
$include <../util.sail>
$endif
would include the file aarch64/prelude.sail relative to the file where the include is contained. It then defines a symbol SYM and includes another file if it is not defined. The <../util.sail> include will be accessed relative to $SAIL_DIR/lib, so $SAIL_DIR/lib/../util.sail in this case.
This can be used with the standard C trick of
$ifndef ONCE
$define ONCE
val f : unit -> unit
$endif
so no matter how many sail files include the above file, the valspec for f will only appear once.
Currently we just have $include, $define, $ifdef and $ifndef (with $else and $endif). We're using $ rather than # because # is already used in internal identifiers, although this could be switched.
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
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)
|
