| 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)
|
|
Also updated some of the documentation in the sail source code
|
|
This removes all type polymorphism, so we can generate optimized
bitvector code and compile to languages without parametric
polymorphism.
|
|
|
|
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.
|
|
(rather than for each argument separately)
|
|
|
|
Experimenting with porting riscv model to new typechecker
|
|
The type-checker already supports a user-defined "exception" type that can be
used in throw and try-catch expressions. This patch adds support for that to
the Lem shallow embedding by adapting the existing exception mechanisms of the
state and prompt monads. User-defined exceptions are distinguished from
builtin exception cases. For example, the state monad uses
type ex 'e =
| Exit
| Assert of string
| Throw of 'e
to distinguish between calls to "exit", failed assertions, and user-defined
exceptions, respectively. Early return is also handled using the exception
mechanism, by lifting to a monad with "either 'r exception" as the exception
type, where 'r is the expected return type and "exception" is the user-defined
exception type.
|
|
Works with the vector branch of asl_parser
|
|
|
|
Also fix bug in mono analysis with generated variables
Breaks lots of typechecking tests because it generates unnecessary
equality tests on units (and the tests don't have generic equality),
which I'll fix next.
|
|
|
|
- Add support for some internal nodes to type checker
- Add more explicit type annotations during rewriting
- Remove hardcoded rewrites for E_vector_update etc from Lem pretty-printer;
these will be resolved by the type checker during rewriting now
|
|
|
|
|
|
As discussed previously, we wanted to start refactoring the re-writer
to make it a bit less monolithic, and in the future potentially break
it into separate files for backend-specific rewrites and stuff.
- rewriter.ml now contains the generic re-writing code
- rewrites.ml contains the rewriting passes themselves
It would be nice if the generic rewriting code didn't depend on the
typechecker, because then it could be used in ASL parser on untyped
code.
|
|
Alastair's test cases revealed that using regular ints causes issues
throughout sail, where all kinds of things can internally overflow in
edge cases. This either causes crashes (e.g. int_of_string fails for
big ints) or bizarre inexplicable behaviour. This patch switches the
sail AST to use big_int rather than int, and updates everything
accordingly.
This touches everything and there may be bugs where I mistranslated
things, and also n = m will still typecheck with big_ints but fail at
runtime (ocaml seems to have decided that static typing is unnecessary
for equality...), as it needs to be changed to eq_big_int.
I also got rid of the old unused ocaml backend while I was updating
things, so as to not have to fix it.
|
|
|
|
Now constraints on type constructors are checked correctly when
checking that types are well formed using Env.wf_typ. The arity and
kind of type constructor arguments are also checked in the same way.
Also some general cleanups to the type checker code, with some
auxillary functions being moved to more appropriate files.
|
|
Possibly useful for Brian's monomorphisation code
|
|
embedding
Checks for command-line flag -undefined_gen and uses the undefined value
generator functions of the form undefined_typ to initialise registers
|
|
|
|
|
|
|
|
|
|
checking that the type variables visible in the output aren't
existential
|
|
Also added some new utility functions in ast_util
|
|
Also improves flow typing in assert statements for ASL parser
This patch does currently introduce a few test failures, probably due
to the new way literals are handled in case statements, which needs to
be investigated and fixed if possible.
|
|
|
|
Also fixed basic ocaml test suite
|
|
as GPR
This was wrongly translated as an update of the vector of references.
|
|
- Modified how sail type error messages are displayed. The
typechecker, rather than immediately outputing a string has a
datatype for error types, which are the pretty-printed using a
PPrint pretty-printer. Needs more work for all the error messages.
- Error messages now attempt to highlight the part of the file where
the error occurred, by printing the line the error is on and
highlighting where the error message is in red. Again, this needs to
be made more robust, especially when the error messages span
multiple lines.
Other things
- Improved new parser and lexer. Made the lexer & parser handling of
colons simpler and more intuitive.
- Added some more typechecking test cases
|
|
- Support tuples in lexps
- Rewrite trivial sizeofs
- Rewrite early returns more aggressively
- Support let bindings with ticked variables (binding both a type-level and
term-level variable at the same time)
|
|
syntactically correct ocaml
|
|
Also generate a function which initializes all the registers in a spec to undefined. This gives us the information we need post-rewriting to generate registers of any arbitrary type.
|
|
backed.
Ocaml doesn't support undefined values, so we need a way to remove
them from the specification in order to generate good ocaml
code. There are more subtle issues to - like if we initialize a
mutable variable with an undefined list, then the ocaml runtime has no
way of telling what it's length should be (as this information is
removed by the simple_types pass).
We therefore rewrite undefined literals with calls to functions that
create undefined types, e.g.
(bool) undefined becomes undefined_bool ()
(vector<'n,'m,dec,bit>) undefined becomes undefined_vector(sizeof 'n, sizeof 'm, undefined_bit ())
We therefore have to generate undefined_X functions for any user
defined datatype X. initial_check seems to be the logical place for
this. This is straightforward provided the user defined types are
not-recursive (and it shouldn't be too bad even if they are).
|
|
|
|
The reason you want this is to do something like (note new parser only):
*********
default Order dec
type bits 'n:Int = vector('n - 1, 'n, dec, bit)
val zeros : forall 'n. atom('n) -> bits('n)
val decode : bool -> unit
function decode b = {
let 'datasize: {|32, 64|} = if b then 32 else 64;
let imm: bits('datasize) = zeros(datasize);
()
}
*********
for the ASL decode functions, where the typechecker now knows that the
datasize variable and the length of imm are the same.
|
|
- Add some missing "wreg" effect annotations in the type checker
- Improve pretty-printing of register type definitions: In addition to a
"build" function, output an actual type definition, and some getter/setter
functions for register fields
- Fix a bug in sizeof rewriting that caused it to fail when rewriting nested
calls of functions that contained sizeof expressions
- Fix pretty-printing of user-defined union types with type variables (cf. test
case option_either.sail)
- Simplify nexps, e.g. "(8 * 8) - 1" becomes "63", in order to be able to
output more type annotations with bitvector lengths
- Add (back) some support for specifying Lem bindings in val specs using
"val extern ... foo = bar"
- Misc bug fixes
|
|
|
|
If some type-level variables in a sizeof expression in a function body cannot
be directly extracted from the parameters of the function, add a new parameter
for each unresolved parameter, and rewrite calls to the function accordingly
|
|
Tries to extract values of nexps from the (type annotations of) parameters
passed to the function. This seems to correspond to the behaviour of the
previous typechecker.
|
|
1) Added a new construct to the expression level: constraint. This is the
essentially the boolean form of sizeof. Whereas sizeof takes a nexp
and has type [:'n:], constraint takes a n_constraint and returns a
boolean. The hope is this will allow for flow typing to be represented
more explicitly in the generatated sail from ASL.
For example we could have something like:
default Order dec
val bit[64] -> unit effect pure test64
val forall 'n, ('n = 32 | 'n = 64 | 'n = 10) & 'n != 43. bit['n] -> unit effect pure test
function forall 'n. unit test addr =
{
if constraint('n = 32) then {
()
} else {
assert(constraint('n = 64), "64-bit mode");
test64(addr)
}
}
2) The other thing this example demonstrates is that flow constraints
now work with assert and not just if. Even though flow typing will
only guarantee us that 'n != 32 in the else branch, the assert gives
us 'n = 64. This is very useful as it's a common idiom in the ARM
spec to guarantee such things with an assert.
3) Added != to the n_constraint language
4) Changed the n_constraint language to add or and and as constructs
in constraints. Previously one could have a list of conjuncts each of
which were simple inequalites or set constraints, now one can do for
example:
val forall 'n, ('n = 32 | 'n = 64) & 'n in {32, 64}. bit['n] -> unit effect pure test
This has the very nice upside that every n_constraint can now be
negatated when flow-typing if statements. Note also that 'in' has been
introduced as a synonym for 'IN' in the constraint 'n in {32,64}. The
use of a block capital keyword was a bit odd there because all the
other keywords are lowercase.
|
|
|
|
|
|
|
