| Age | Commit message (Collapse) | Author |
|---|
|
|
|
sail_new_tc
|
|
* 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
|
|
|
|
|
|
|
|
|
|
|
|
Added code to solve basic constraints without passing them to Z3. This
results in roughly another 5x speedup.
|
|
Filter the possible casts by only attempting those which reasonably
match the surrounding type environment. This results in about a 5x
performance improvement.
|
|
|
|
|
|
|
|
monomorphisation
|
|
|
|
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
|
|
|
|
sail.ml
Current REMS install script and Jenkins CI server is on an older ocaml
which doesn't have this function in String.
|
|
|
|
|
|
|
|
|
|
|
|
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
|
|
(e.g., for some ARM decoding functions)
|
|
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
|
|
Seems to work for CHERI-MIPS, but still a few things to be done, e.g.
collecting let bindings for variables bound in bitvector patterns
|
|
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.
|
|
Added a new feature for implicit casts - now allowable implicit casts
can be specified by the user via a valspec such as
val cast forall Type 'a, Type 'b. 'a -> 'b effect pure cast_anything
with a new AST constructor to represent this as VS_cast_spec. This
constructor is removed and replaced with the standard val spec by the
old typechecker for backwards compatability, so it's only used by the
new typechecker, and won't appear in the ast once it reaches the
backends.
Also added Num as a synonym for the Nat kind in the parser, via the
confusingly named NatNum token (Num by itself was already taken for a
numeric constant).
|
|
|
|
(Previously it used the last branch's type!)
|
|
Can now typecheck:
* register fields in expressions, e.g. CP0Status.IM
* register fields in l-expressions, e.g. CP0Cause.CE := 0b00
* functions without valspecs, provided their types are easily inferable
Still need to be able to treat a register-typed register as a vector
for most of mips model to typecheck, as well as bitvector patterns,
but it's like 90% there.
|
|
|
|
Added support for implicit casting to the bi-directional type
checker. The casts can be any user-specified function, and in princple
don't have to be hardcoded. This allows us to typecheck definitions such as
function bit[64] rGPR idx = {
if idx == 0 then 0 else GPR[idx]
}
in the MIPS spec, which involves lots of casting from integers to
bitvectors, as well as casting from a named register to it's value
(implicit dereferencing).
|
|
|
|
Added support for:
* Register type declarations
* Undefined literals
* Exit statement
* Toplevel let statements
* Vector literals i.e. [a, b, c]
* Binary bitvector literals
* Hex bitvector literals
Patched the parser so you can actually write 2**'n - 1 in a nexp. The
parser rules for nexps are a bit strange, and there didn't seem to be
anyway to write this before without it causing a parse error.
Can now typecheck up to line 332 of mips_prelude in mips/, but need to
add support for the implict passing of registers by names to go any
further, which should be fun...
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
Added basic support for vector types, and fixed various bugs. Also
added some basic tests for these features in test/typecheck.
|
