| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Make destructuring existentials less arcane by allowing them to be destructured via type patterns (typ_pat in ast.ml). This allows the following code for example:
val mk_square : unit -> {'n 'm, 'n = 'm. vector('n, dec, vector('m, dec, bit))}
function test (() : unit) -> unit = {
let matrix as vector('width, _, 'height) = mk_square ();
_prove(constraint('width = 'height));
()
}
where 'width we become 'n from mk_square, and 'height becomes 'm. The old syntax
let vector as 'length = ...
or even
let 'vector = ...
still works under this new scheme in a uniform way, so this is backwards compatible
The way this works is when a kind identifier in a type pattern is bound against a type, e.g. 'height being bound against vector('m, dec, bit) in the example, then we get a constraint that 'height is equal to the first and only n-expression in the type, in this case 'm. If the type has two or more n-expressions (or zero) then this is a type error.
|
|
Can now use C-style include declarations to include files within other sail files. This is done in such a way that all the location information is preserved in error messages. As an example:
$include "aarch64/prelude.sail"
$define SYM
$ifndef SYM
$include <../util.sail>
$endif
would include the file aarch64/prelude.sail relative to the file where the include is contained. It then defines a symbol SYM and includes another file if it is not defined. The <../util.sail> include will be accessed relative to $SAIL_DIR/lib, so $SAIL_DIR/lib/../util.sail in this case.
This can be used with the standard C trick of
$ifndef ONCE
$define ONCE
val f : unit -> unit
$endif
so no matter how many sail files include the above file, the valspec for f will only appear once.
Currently we just have $include, $define, $ifdef and $ifndef (with $else and $endif). We're using $ rather than # because # is already used in internal identifiers, although this could be switched.
|
|
Currently doesn't try to compile to lem or use the MIPS spec
All the failing tests have been removed because I intend to handle
them differently - they were very fragile before because there was no
indication of why they failed, so as sail evolved they tended to start
failing for the wrong reasons and not testing what they were supposed
to.
|
|
|
|
|
|
For example:
bitfield cr : vector(8, dec, bit) = {
CR0 : 7 .. 4,
LT : 7,
CR1 : 3 .. 2,
CR2 : 1,
CR3 : 0,
}
The difference this creates a newtype wrapper around the vector type,
then generates getters and setters for all the fields once, rather
than having to handle this construct separately in every backend.
|
|
|
|
|
|
Breaks parsing ambiguities by removing = as an identifier in the old parser
and requiring parentheses for some expressions in the new parser
|
|
|
|
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.
|
|
For example,
val test = { ocaml: "test_ocaml" } : unit -> unit
will only be external for OCaml. For other backends, it will have to be
defined.
|
|
For example:
val test = { ocaml: "test_ocaml", lem: "test_lem" } : unit -> unit
val main : unit -> unit
function main () = {
test ();
}
for a backend not explicitly provided, the extern name would be simply
"test" in this case, i.e. the string version of the id.
Also fixed some bugs in the ocaml backend.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
also rename NC_nat_set_bounded to NC_set (it was an int set not a nat set anyway)
|
|
just LB_val in AST
also rename functions in rewriter.ml appropriately.
|
|
|
|
|
|
|
|
to translate exceptions in ASL. See test/typecheck/pass/trycatch.sail.
|
|
|
|
Also fixed substitution functions so as to not substitute captured kind identifiers
|
|
|
|
|
|
Fixed some bugs in the initial check that caused valid code to fail to
parse
Add a nid utility function that creates an id n-expression, similar to
nvar, nconstant etc
|
|
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
|
|
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.
|
|
Also added some additional helper functions in type_check_new.mli and changed real literals slightly
|
|
|
|
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
|
|
annotated patterns and lexps
Added get_enum to type checker interface
|
|
* Experimented with using list<bit> to clean up manually monomorphised code in MIPS tlb
* Added option -dtc_verbose to control verbosity of new typechecker
* Allowed functions with val specs to omit their type declarations
|
|
This introduces some shift/reduce and reduce/reduce conflicts, but I don't think these matter.
|
|
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
|
|
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).
|
|
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...
|
|
# Conflicts:
# src/lem_interp/interp.lem
# src/lem_interp/interp_inter_imp.lem
# src/lem_interp/interp_interface.lem
# src/parser.mly
# src/pretty_print_lem.ml
|
|
|
|
data and invent rmemt and wmvt effects for them. Extend the interpreter context to include lists of tagged memory read and write functions. The memory model must round down the address to the nearest capability aligned address when reading/writing tags. Remove TAGw which is no longer needed as a result.
|
|
|
|
Add div to library functions
|
|
TODO: add an event for a return so that rewriters can find and remove them as needed for OCaml and Lem
|
