| Age | Commit message (Collapse) | Author |
|---|
|
Can now properly typecheck register declarations and assignments. Also
better support for assignments to mutable variables. Assignment to
immutable let bound variables is disallowed as it should be, and casts
when assiging to existing bound variables should be handled properly.
Added additional tests for these new features, and a new option
-just_check that allows the new checker to be run without the old.
|
|
Started work on a bi-directional type checking algorithm for sail
based on Mark and Neel's typechecker for minisail in idl
repository. It's a bit different though, because we are working with
the unmodified sail AST, and not in let normal-form.
Currently, we can check a fragment of sail that includes pattern
matching (in both function clauses and switch statements), numeric
constraints (but not set constraints), function application, casts
between numeric types, assignments to local mutable variables,
sequential blocks, and (implicit) let expressions.
For example, we can correctly typecheck the following program:
val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus
val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id
val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id
val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch
function forall Nat 'N, 'N >= 63. [|10:'N|] branch x =
{
switch x {
case ([|10:30|]) y -> y
case ([:31:]) _ -> sizeof 'N
case ([|31:40|]) _ -> plus(60,3)
}
}
and branch (([|51:63|]) _) = ten_id(sizeof 'N)
The typechecker has been set up so it can produce derivation trees for
the typing judgements and constraints, so for the above program we
have:
Checking function branch
Adding local binding x :: range<10, 'N>
| Check { switch x { case (range<10, 30>) y -> y case (atom<31>) _ -> sizeof 'N case (range<31, 40>) _ -> plus(60, 3)} } <= range<10, 'N>
| | Check switch x { case (range<10, 30>) y -> y case (atom<31>) _ -> sizeof 'N case (range<31, 40>) _ -> plus(60, 3)} <= range<10, 'N>
| | | Infer x => range<10, 'N>
| | Subset 'N >= 63 |- {'fv1 | 10 <= 'fv1 & 'fv1 <= 30} {'fv0 | 10 <= 'fv0 & 'fv0 <= 'N}
| | Adding local binding y :: range<10, 30>
| | | Check y <= range<10, 'N>
| | | | Infer y => range<10, 30>
| | | Subset 'N >= 63 |- {'fv4 | 10 <= 'fv4 & 'fv4 <= 30} {'fv3 | 10 <= 'fv3 & 'fv3 <= 'N}
| | Subset 'N >= 63 |- {'fv7 | 31 <= 'fv7 & 'fv7 <= 31} {'fv6 | 10 <= 'fv6 & 'fv6 <= 'N}
| | | Check sizeof 'N <= range<10, 'N>
| | | | Infer sizeof 'N => atom<'N>
| | | Subset 'N >= 63 |- {'fv10 | 'N <= 'fv10 & 'fv10 <= 'N} {'fv9 | 10 <= 'fv9 & 'fv9 <= 'N}
| | Subset 'N >= 63 |- {'fv13 | 31 <= 'fv13 & 'fv13 <= 40} {'fv12 | 10 <= 'fv12 & 'fv12 <= 'N}
| | | Check plus(60, 3) <= range<10, 'N>
| | | | | Infer 60 => atom<60>
| | | | | Infer 3 => atom<3>
| | | | Infer plus(60, 3) => atom<((60 - 20) + (20 + 3))>
| | | Subset 'N >= 63 |- {'fv20 | ((60 - 20) + (20 + 3)) <= 'fv20 & 'fv20 <= ((60 - 20) + (20 + 3))} {'fv19 | 10 <= 'fv19 & 'fv19 <= 'N}
Subset 'N >= 63 |- {'fv23 | 51 <= 'fv23 & 'fv23 <= 63} {'fv22 | 10 <= 'fv22 & 'fv22 <= 'N}
| Check ten_id(sizeof 'N) <= range<10, 'N>
| | | Infer sizeof 'N => atom<'N>
| | Prove 'N >= 63 |- 'N >= 10
| | Infer ten_id(sizeof 'N) => atom<'N>
| Subset 'N >= 63 |- {'fv28 | 'N <= 'fv28 & 'fv28 <= 'N} {'fv27 | 10 <= 'fv27 & 'fv27 <= 'N}
Judgements are displayed in the order they occur - inference steps go
inwards bottom up, while checking steps go outwards top-down. The
subtyping rules from Mark and Neel's check_sub rule all are verified
using the Z3 constraint solver.
I have been a set of tests in test/typecheck which aim to exhaustively
test all the code paths in the typechecker, adding new tests everytime
I add support for a new construct.
The new checker is turned on using the -new_typecheck option, and can
be tested (from the toplevel sail directory) by running:
test/typecheck/run_tests.sh -new_typecheck
(currently passes 32/32)
and compared to the old typechecker by
test/typecheck/run_tests.sh
(currently passes 21/32)
|
|
|
|
|
|
|
|
same time with the types both have in common factored out into separate file, rename one mips shallow embedding _extras file as required by this
|
|
instruction state, factor out interpreter/shallow embedding value conversion
|
|
state monad, library fixes
|
|
|
|
|
|
|
|
|
|
letbound variables
|
|
sail_impl_base, add sail_impl_base.outcome, add interp_inter_imp auxiliary functions, make prompt use sail_impl_base.outcome
|
|
|
|
|
|
well as items of kind Type.
Syntax for the feature is:
def Nat id = nexp
Note: some useful nexps may not parse properly.
All typedef forms can also be used as def Type ... if desired, but this is not required.
|
|
processing
|
|
|
|
correct now, fixes, pp
|
|
functions, and state definition
|
|
|
|
|
|
|
|
|
|
output of such
|
|
|
|
Events are eamem to signal the memory address to write to and wmv to pass the value to write
|
|
function for good unification, especially for rewriting
|
|
Also stop rewriting code in the pretty printer, instead move it all into a new general rewriting pass
|
|
|
|
|
|
instruction
|
|
|
|
will be reflected in short hand type syntax, inc is still the default if undeclared
So:
default order dec
register bit[32] t (* Declares t as a decreasing vector, starting at 31 on the left and decreasing to 0 *)
default order inc
register bit[32] o (* Declares o as an increasing vector, starting at 0 on the left and increasing to 31 *)
It is presently possible to change the default mid-file; this is almost certainly bad and I will turn it into an error soon.
|
|
interpreter.
An alias can be read within the interpreter, but not written to. Exits aren't yet taken in the interpreter.
|
|
Used by the Power XML extraction tool.
|
|
This is necessary to avoid a parse error. It might make sense to merge
this list and the one in type_internal.ml somehow, to avoid duplication
and similar bugs in the future.
|
|
from 0 to 32 etc, doesn't change order yet.).
|
|
|
|
ast, and extending the interpreter to expect annotations.
Annotations and locations are still not used by the interpreter.
|
|
(in limited circumstances at the moment due to which expressions are actually checked, so test files should not yet be changed)
|
|
definition environment. Skipping function definition, let bind, and expression checking for this commit (to come).
|
|
|
|
|
|
Tests compile and run properly. There is a lot of hackery going
on to workaround the rough edges of new Lem. Use at your own
risk (you need the "library-format" branch of lem).
|
|
|
|
and rules for lem ast generation; created a new directory for the lem interpreter and moved the Lem ast to it.
|
|
|
|
|
