| Age | Commit message (Collapse) | Author |
|---|
|
Recent patches have made the rewriter more strict about performing
type correct rewrites. This is mostly a good thing but did cause some
problems with the ocaml backend.
Currently the sizeof rewriter doesn't seem to preserve type
correctness - I suspect this is because when it resolves the sizeofs,
it generates constraints that are true, but not in a form where the
typechecker can see that they are true. I disabled the re-check after
the sizeof rewriting pass to fix this. Maybe we don't want to do this
anyway because it's slow.
Changes to function clauses with guards + monomorphisation changed how
the typechecker handles literal patterns. I added a rewriting pass to
rewrite literals to guarded equality checks, which is run before
generating ocaml.
The rewriter currently uses Env.empty in a view places. This can cause
bugs because Env.empty is a totally unitialised environment that
doesn't satisfy invariants we expect of an environment. This should be
changed to initial_env and it shouldn't be exported, I fixed a few
cases where this caused things to go wrong, but it should probably not
be exported from Type_check.ml.
|
|
|
|
steps
Parser now has syntax for mutual recusion blocks
mutual {
... fundefs ...
}
which is used for parsing and pretty printing
DEF_internal_mutrec. It's stripped away by the initial_check, so the
typechecker never sees DEF_internal_mutrec. Maybe this could change,
as forcing mutual recursion to be explicit would probably be a good
thing.
Added record syntax to the new parser
New option -dmagic_hash is similar to GHC's -XMagicHash in that it
allows for identifiers to contain the special hash character, which is
used to introduce new autogenerated variables in a way that doesn't
clash with existing names.
Option -sil compiles sail down to the intermediate language defined in
sil.ott (not complete yet).
|
|
|
|
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.
|
|
numbers below 129
|
|
|
|
|
|
What does this mean? Basically undefined values can't be created for
types that contain free type variables, so for example: undefined :
list(int) is good, but undefined : list('a) is bad. The reason we want
to do this is because we can't compile them away statically, and this
leads to situations where type-checkable code fails in the rewriter
and gives horribly confusing error messages that don't relate to code
the user wrote at all.
As an example the following used to typecheck, but fail in the
rewriter with a confusing error message, whereas now the typechecker
should reject all cases which would trigger that failure in rewriting.
val test : forall ('a:Type). list('a) -> unit effect {wreg, undef}
function test xs = {
xs_mut = xs;
xs_mut = undefined; (* We don't know what kind of undefined 'a is *)
()
}
There's a slight hitch, namely that in the undefined_type functions
created by the -undefined_gen option, we do want to allow functions
that have polymorphic undefined values, so that we can generate
undefined generators for polymorphic datatypes such as:
union option ('a:Type) = {
Some : 'a,
None
}
These functions are always have a specific form that allows the
rewriter to succesfully remove the polymorphic undefined value for the
'a argument for Sone. As such there's a flag in the typechecking
environment for polymorphic undefineds that is enabled when it sees a
function with the undefined_ name prefix.
Also: Fixed some test cases that were broken due to escape effect being added to assert.
|
|
Translates atom('n) types into itself('n) types that won't be erased
Also exports more rewriting functions
|
|
|
|
|
|
|
|
(and fix up monomorphisation)
|
|
With -ddump_rewrite_ast, pretty-print Sail code after each rewriting step in
addition to dumping the AST.
|
|
Menhir pretty printer can now print enough sail to be useful with ASL parser
Fixity declarations are now preserved in the AST
Menhir parser now runs without the Pre-lexer
Ocaml backend now supports variant typedefs, as the machinery to
generate arbitrary instances of variant types has been added to the
-undefined_gen flag
|
|
New option -memo_z3 memoizes calls to the Z3 solver, and saves these
results between calls to sail. This greatly increases the performance
of sail when re-checking large specifications by about an order of
magnitude. For example:
time sail -no_effects prelude.sail aarch64_no_vector.sail
real 0m4.391s
user 0m0.856s
sys 0m0.464s
After running with -memo_z3 once, running again gives:
time sail -memo_z3 -no_effects prelude.sail aarch64_no_vector.sail
real 0m0.457s
user 0m0.448s
sys 0m0.008s
Both the old and the new parser should now have better error messages
where the location of the parse error is displayed visually in the
error message and highlighted.
|
|
mono-experiments
|
|
|
|
mono-experiments
# Conflicts:
# src/gen_lib/sail_values.lem
|
|
- Add back support for bit list representation of bit vectors, for backwards
compatibility in order to ease integration with the interpreter. For this
purpose, split out a file sail_operators.lem from sail_values.lem, and add a
variant sail_operators_mwords.lem for the machine word representation of
bitvectors. Currently, Sail is hardcoded to use machine words for the
sequential state monad, and bit lists for the free monad, but this could be
turned into a command line flag.
- Add a prelude_wrappers.sail file for glueing the Sail prelude to the Lem
library. The wrappers make use of sizeof expressions to extract type
information from bitvectors (length, start index) in order to pass it to the
Lem functions.
- Add early return support to the free monad, using a new constructor "Return
of 'r". As with the sequential monad, functions with early return are
wrapped into "catch_early_return", which extracts the return value at the end
of the function execution.
|
|
|
|
|
|
Basically we needed to make the rewriting step for E_sizeof and
E_constraint more aggressively try to rewrite those expressions from
variables in scope, without adding new parameters to pass the type
variables at runtime, as this can break in the presence of existential
quantification. Still some cleanup to do in this code, but tests on
the arm spec show that it now introduces the minimal amount of new
parameters.
|
|
Also: Merge remote-tracking branch 'origin/sail_new_tc' into experiments
|
|
Make state monad parametric in register state, and generate a record with
registers from the Sail spec
|
|
Conflicts:
src/pretty_print_common.ml
|
|
Added a copy of the current parser/lexer in parser2.mly and
lexer2.mll. They can be used with the -new_parser flag. Currently they
are just copies of the existing files.
|
|
|
|
|
|
number of files
|
|
|
|
|
|
Modified initial_check.ml so it no longer requires type_internal. It's
still needs cleaned up in a few ways. Most of the things it's trying
to do could be done nicer if we took some time to re-factor it, and
some of the things should just be handled by the main typechecker,
leaving it as a think layer between the parse_ast and the ast.
Now that's done everything can be switched to the new typechecker and
the _new suffixes were deleted from everything except the
monomorphisation pass because I don't know the status of that.
|
|
sail_new_tc
|
|
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.
|
|
Initial typecheck still uses previous typechecker
|
|
|
|
sail_new_tc
|
|
|
|
|
|
|
|
Added vector concatenation patterns. Currently slightly more
restrictive than before as each subvector's length must be inferrable
from just that particular subvector - this may require additional type
annotations in certain vector patterns. How exactly weird vector
patterns, such as incrementing and decrementing vectors appearing in
the same pattern, as well as patterns with funny start indexes should
be dealt with correctly is unclear. It's probably best to be as
restrictive as possible to avoid unsoundness bugs.
Added a new option -ddump_tc_ast which dumps the (new) typechecked AST
to stdout. Also added a new option -dno_cast which disables implicit
casting in the typechecker. These options can be used in conjunction
to dump the typechecked ast (which has all implicit casts resolved),
and then re-typecheck it as a way to check that the typechecker is
indeed resolving all casts correctly, and is reconstructing a fully
type correct AST. The run_tests.sh script in test/typecheck has been
modified to do this.
Removed the dependency on Type_internal.ml from
pretty_print_sail.ml. This means that we can no longer pretty print
certain internal constructs produced by the old typechecker, but on
the plus side it means that the sail pretty printer is type system
agnostic and works with any annotation AST, irregardless of the type
of annotations. Also fixed a few bugs where certain constructs would
be pretty printed incorrectly.
|
|
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
|
