| Age | Commit message (Collapse) | Author |
|---|
|
mono-experiments
|
|
|
|
to translate exceptions in ASL. See test/typecheck/pass/trycatch.sail.
|
|
Conflicts:
src/pretty_print_common.ml
|
|
|
|
|
|
Add a test case with the MIPS spec using the TLB stub.
Use the sequential monad for Lem testing for now; the free monad (in
"prompt.lem") has not been updated for machine words yet.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
considering possible casts
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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
|
|
- Fixed a bug where some l-expressions which wrote registers wern't
picking up register writes.
- Can now write to registers with record types. e.g. ARM's ProcState
record from ASL.
|
|
See test/typecheck/pass/cons_pattern.sail for an example.
Also cleaned up the propagating effects code by making some of the
variable names less verbose
|
|
|
|
Introduces a when keyword for case statements, as the Pat_when constructor for pexp's in the AST. This allows us to write things like:
typedef T = const union { int C1; int C2 }
function int test ((int) x, (T) y) =
switch y {
case (C1(z)) when z == 0 -> 0
case (C1(z)) when z != 0 -> x quot z
case (C2(z)) -> z
}
this should make translation from ASL's patterns much more straightforward
|
|
|
|
|
|
This introduces some shift/reduce and reduce/reduce conflicts, but I don't think these matter.
|
|
|
|
* Fixed a bug where non-polymorphic function return types could be incorrect
* Added support for LEXP_memory AST node
* Flow typing constraint generation for all inequality operators
* Better support for increasing vector indices in field access expressions
|
|
|
|
|
|
Also:
- Added support for foreach loops
- Started work on type unions
- Flow typing can now generate constraints, in addition to restricting range-typed variables
- Various bugfixes
- Better unification for nexps with multiplication
|
|
|
|
|
|
|
|
|
|
Now the test suite generates lem for all the typechecker tests, and
tests if the generated lem typechecks. For a lot of the cases the
answer is currently no.
|
|
Added the following constructs to the new type checker:
* Added records, and record field accessors
* Added assert statements
* Added nondet blocks
* More simple flow typing tests
|
|
Added preliminary support for flow types, so we can typecheck things
like:
default Order inc
val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range
val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range
val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom
val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range
overload (deinfix +) [add_range]
overload (deinfix -) [sub_range]
overload (deinfix <) [lt_atom_range; lt_range_atom]
function ([|63|]) branch (([|63|]) x) =
{
y := x;
if (y < 32)
then {
y := 31;
y + 32
}
else y - 32
}
Currently how this works is that the if condition is lifted to a typ
modifying function that applies to the type of the variables appearing
in the condition provided it satisfies some ad-hoc conditions.
As can be seen above, it does require that the initial environment for
the typechecker is set up with the correct definitions
|
|
Commented out some buggy re-sugaring logic from pretty_print_common
where it re-sugared vectors incorrectly
Fixed a bug where the type checker forgot to preserve type signatures
in top-level letbinds
|
|
Other things:
* Cleaned up several files a bit
* Fixed a bug in the parser where (deinfix |) got parsed as (definfix ||)
* Turned of the irritating auto-indent in sail-mode.el
|
|
Also added some additional tests in test/typecheck
|
|
|
|
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.
|
|
New typechecker has no builtin overloaded operators - instead can now
write something in SAIL like:
overload (deinfix +) [id1; id2; id3]
to set up functions id1, id2, and id3 as overloadings for the +
operator. Any identifier can be overloaded, not just infix ones. This
is done in a backwards compatible way, so the old typechecker removes
the DEF_overload nodes from the ast so the various backends never see
it.
|
