| Age | Commit message (Collapse) | Author |
|---|
|
These match the new ASL pattern constructors:
- !p matches if the pattern p does not match
- { p1, ... pn } matches if any of the patterns p1 ... pn match
We desugar the set pattern "{p1, ... pn}" into "p1 | (p2 | ... pn)".
ASL does not have pattern binding but Sail does. The rules at the
moment are that none of the pattern can contain patterns. This could
be relaxed by allowing "p1 | p2" to bind variables provided p1 and p2
both bind the same variables.
|
|
Makes the generated undefined functions smaller, easier to read, and
avoids excessive memory usage in Coq (e.g., for large AST types).
|
|
Registers can now be marked as configuration registers, for example:
register configuration CFG_RVBAR = 0x1300000
They work like ordinary registers except they can only be set by
functions with the 'configuration' effect and have no effect when
read. They also have an initialiser, like a let-binding. Internally
there is a new reg_dec constructor DEC_config. They are intended to
represent configuration parameters for the model, which can change
between runs, but don't change during execution. Currently they'll
only work when compiled to C. Internally registers can now have custom
effects for reads and writes rather than just rreg and wreg, so the
type signatures of Env.add_register and Env.get_register have changed,
as well as the Register lvar, so in the type checker we now write:
Env.add_register id read_effect write_effect typ
rather than
Env.add_register id typ
For the corresponding change to ASL parser there's a function
is_config in asl_to_sail.ml which controls what becomes a
configuration register for ARM. Some things we have to keep as
let-bindings because Sail can't handle them changing at runtime -
e.g. the length of vectors in other top-level definitions. Luckily
__SetConfig doesn't (yet) try to change those options.
Together these changes allow us to translate the ASL __SetConfig
function, which means we should get command-line option compatibility
with ArchEx for running the ARM conformance tests.
|
|
|
|
(involved some manual tinkering with gitignore, type_check, riscv)
|
|
- Refactor the flow typing implementation in the type-checker. This
should fix an issue involving riscv_platform. Specifically it should
now work better when an if statement contains multiple conditions
combined with and/or, only some of which imply constraints at the
type level. This change also simplifies the implementation of flow
typing, and removes some obscure features that were hardly used -
specifically, flow typing could modify types, but this was fairly
obscure and doesn't seem to affect any of our specifications. More
testing is needed to ensure that this change hasn't inadvertantly
broken anything, but it does pass all our tests and continue to
typecheck arm, riscv and cheri.
- Also adds a option for generating faster undefined functions for
enum and variant types. Previously I tried to optimise away such
functions in the C backend, because they could be slow and cause
considerable uneccessary allocation, however this was error prone
and it turns out a much simpler solution is to simply make the
functions themselves much faster, at the cost of hard-coding certain
decisions about what undefined means for these types at compile tile
(which is fine for fast emulation). This almost doubles the
performance of the generated C code.
- Add a wrapper for right shift to avoid UB when shifting by 64 or
more places.
|
|
This means that a mapping which formerly had to be pre-declared like
val name : a <-> b
...
mapping name {
x <-> y,
...
}
can now be shortened to
mapping name : a <-> b {
x <-> y,
...
}
|
|
|
|
1. Experiment with allowing some flow typing on mutable variables for
translating ASL in a more idiomatic way. I realise after updating some
of the test cases that this could have some problematic side effects
for lem translation, where mutable variables are translated into
monadic code. We'd need to ensure that whatever flow typing happens
for mutable variables also works for monadic code, including within
transformed loops. If this doesn't work out some of these changes may
need to be reverted.
2. Make the type inference for l-expressions a bit smarter. Splits the
type checking rules for l-expressions into a inference part and a
checking part like the other bi-directional rules. Should not be able
to type check slightly more l-expresions, such as nested vector slices
that may not have checked previously.
The l-expression rules for vector patterns should be simpler now, but
they are also more strict about bounds checking. Previously the bounds
checks were derived from the corresponding operations that would
appear on the RHS (i.e. LEXP_vector would get it's check from
vector_access). This meant that the l-expression bounds checks could
be weakend by weakening the checks on those operations. Now this is no
longer possible, there is a -no_lexp_bounds_check option which turns
of bounds checking in l-expressions. Currently this is on for the
generated ARM spec, but this should only be temporary.
3. Add a LEXP_vector_concat which mirrors P_vector_concat except in
l-expressions. Previously there was a hack that overloaded LEXP_tup
for this to translate some ASL patterns, but that was fairly
ugly. Adapt the rewriter and other parts of the code to handle
this. The rewriter for lexp tuple vector assignments is now a rewriter
for vector concat assignments.
4. Include a newly generated version of aarch64_no_vector
5. Update the Ocaml test suite to use builtins in lib/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
For some reason there was a desugaring rule that mapped f((x, y)) to
f(x, y) in initial_check.ml, this prevented functions and constructors
from being applied to tuples.
|
|
|
|
|
|
This commit primarily changes how existential types are bound in
letbindings. Essentially, the constraints on both numeric and
existentially quantified types are lifted into the surrounding type
context automatically, so in
```
val f : nat -> nat
let x = f(3)
```
whereas x would have had type nat by default before, it'll now have
type atom('n) with a constraint that 'n >= 0 (where 'n is some fresh
type variable). This has several advantages: x can be passed to
functions expecting an atom argument, such as a vector indexing
operation without any clunky cast functions - ex_int, ex_nat, and
ex_range are no longer required. The let 'x = something() syntax is
also less needed, and is now only really required when we specifically
want a name to refer to x's type. This changes slightly the nature of
the type pattern syntax---whereas previously it was used to cause an
existential to be destructured, it now just provides names for an
automatically destructured binding. Usually however, this just works
the same.
Also:
- Fixed an issue where the rewrite_split_fun_constr_pats rewriting
pass didn't add type paramemters for newly added type variables in
generated function parameters.
- Updated string_of_ functions in ast_util to reflect syntax changes
- Fixed a C compilation issue where elements of union type
constructors were not being coerced between big integers and 64-bit
integers where appropriate
- Type annotations in patterns now generalise, rather than restrict
the type of the pattern. This should be safer and easier to handle
in the various backends. I don't think any code we had was relying
on this behaviour anyway.
- Add inequality operator to lib/flow.sail
- Fix an issue whereby top-level let bindings with annotations were
checked incorrectly
|
|
|
|
Fix a bug in initial check which caused X() = y to expect an additional parameter.
Some tweaks to sail2 emacs mode
|
|
Added option -latex that outputs input to a latex document.
Added doc comments that can be attached to certain AST nodes - right now just valspecs and function clauses, e.g.
/*!
Documentation for main
*/
val main : unit -> unit
These comments are kept by the sail pretty printer, and used when generating latex
|
|
Previously union types could have no-argument constructors, for
example the option type was previously:
union option ('a : Type) = {
Some : 'a,
None
}
Now every union constructor must have a type, so option becomes:
union option ('a : Type) = {
Some : 'a,
None : unit
}
The reason for this is because previously these two different types of
constructors where very different in the AST, constructors with
arguments were used the E_app AST node, and no-argument constructors
used the E_id node. This was particularly awkward, because it meant
that E_id nodes could have polymorphic types, i.e. every E_id node
that was also a union constructor had to be annotated with a type
quantifier, in constrast with all other identifiers that have
unquantified types. This became an issue when monomorphising types,
because the machinery for figuring out function instantiations can't
be applied to identifier nodes. The same story occurs in patterns,
where previously unions were split across P_id and P_app nodes - now
the P_app node alone is used solely for unions.
This is a breaking change because it changes the syntax for union
constructors - where as previously option was matched as:
function is_none opt = match opt {
Some(_) => false,
None => true
}
it is now matched as
function is_none opt = match opt {
Some(_) => false,
None() => true
}
note that constructor() is syntactic sugar for constructor(()), i.e. a
one argument constructor with unit as it's value. This is exactly the
same as for functions where a unit-function can be called as f() and
not as f(()). (This commit also makes exit() work consistently in the
same way) An attempt to pattern match a variable with the same name as
a union-constructor now gives an error as a way to guard against
mistakes made because of this change.
There is probably an argument for supporting the old syntax via some
syntactic sugar, as it is slightly prettier that way, but for now I
have chosen to keep the implementation as simple as possible.
The RISCV spec, ARM spec, and tests have been updated to account for
this change. Furthermore the option type can now be included from
$SAIL_DIR/lib/ using
$include <option.sail>
|
|
|
|
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.
|
|
|
|
For an enumeration type T, we can create a function T_of_num and num_of_T which convert from the enum to and from a numeric type. The numeric type is range(0, n) where n is the number of constructors in the enum minus one. This makes sure the conversion is type safe, but maybe this is too much of a hassle.
It would be possible to automatically overload all these functions into generic to_enum and from_enum as in Haskell's Enum typeclass, but we don't do this yet.
Currently these functions affect a few lem test cases, but I think that is only because they are tested without any prelude functions and pattern rewrites require a few functions to be defined
What is really broken is if one tries to generate these functions like
enum x = A | B | C
function f A = 0
function f B = 1
function f C = 2
the rewriter really doesn't like function clauses like this, and it seems really hard to fix properly (I tried and gave up), this is a shame as the generation code is much more succinct with definitions like above
|
|
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.
|
|
|
|
New testcase for bitfield syntax
Updated to work with latest lem and linksem
|
|
|
|
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.
|
|
|
|
* Changed comment syntax to C-style /* */ and //
* References to registers and mutable variables are never created
implicitly - a reference to a register or variable R is now created
via the expression "ref R". References are assigned like "(*Y) = X",
with "(*ref R) = X" being equivalent to "R = X". Everything is always
explicit now, which simplifies the logic in the typechecker. There's
also now an invariant that every id directly in a LEXP is mutable,
which is actually required for our rewriter steps to be sound.
* More flexible syntax for L-expressions to better support wierd
power-idioms, some syntax sugar means that:
X.GET(a, b, c) ==> _mod_GET(X, a, b, c)
X->GET(a, b, c) ==> _mod_GET(ref X, a, b, c)
for setters, this can be combined with the (still somewhat poorly
named) LEXP_memory construct, such that:
X->SET(a, b, c) = Y ==> _mod_SET(ref X, a, b, c, Y)
Currently I use the _mod_ prefix for these 'modifier' functions, but
we could omit that a la rust.
* The register bits typedef construct no longer exists in the
typechecker. This construct never worked consistently between backends
and inc/dec vectors, and it can be easily replaced by structs with
fancy setters/getters if need be. One can also use custom type operators to mimic the syntax, i.e.
type operator ... ('n : Int) ('m : Int) = slice('n, 'm)
struct cr = {
CR0 : 32 ... 35,
/* 32 : LT; 33 : GT; 34 : EQ; 35 : SO; */
CR1 : 36 ... 39,
/* 36 : FX; 37 : FEX; 38 : VX; 39 : OX; */
CR2 : 40 ... 43,
CR3 : 44 ... 47,
CR4 : 48 ... 51,
CR5 : 52 ... 55,
CR6 : 56 ... 59,
CR7 : 60 ... 63,
}
This greatly simplifies a lot of the logic in the typechecker, as it
means that E_field is no longer ambiguously overloaded between records
and register bit typedefs. This also makes writing semantics for these
constructs much simpler.
|
|
Experimenting with porting riscv model to new typechecker
|
|
|
|
Works with the vector branch of asl_parser
|
|
Add the ast.sed script we need to build sail. Currently we just need
this to fix up the locations in the AST but it will be removed once we
can share locations between ocaml and lem.
|
|
|
|
Requires linenoise library (opam install linenoise) for readline
support. Use 'make isail' to build sail with interactive
support. Plain 'make sail' should work as before with no additional
dependencies.
Use 'sail -i <commands>' to run sail interactively, e.g.
sail -new_parser -i test/ocaml/prelude.sail test/ocaml/trycatch/tc.sail
then try some commands for typechecking and evaluation
sail> :t main
sail> main ()
Doesn't use the lem interpreter right now, instead has a small
operational semantics in src/interpreter.ml, but this is not very
complete and will be changed/removed.
|
|
Breaks parsing ambiguities by removing = as an identifier in the old parser
and requiring parentheses for some expressions in the new parser
|
|
Also fix bug in mono analysis with generated variables
Breaks lots of typechecking tests because it generates unnecessary
equality tests on units (and the tests don't have generic equality),
which I'll fix next.
|
|
|
|
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).
|
|
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.
|
|
There are several key changes here:
1) This commit allows for user defined operations in n-expressions
using the Nexp_app constructor. These operations are linked to
operators in the SMT solver, by using the smt extern when defining
operations. Notably, this allows integer division and modular
arithmetic to be used in types. This is best demonstrated with an
example:
infixl 7 /
infixl 7 %
val operator / = {
smt: "div",
ocaml: "quotient"
} : forall 'n 'm, 'm != 0. (atom('n), atom('m)) -> {'o, 'o = 'n / 'm. atom('o)}
val mod_atom = {
smt: "mod",
ocaml: "modulus"
} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = mod_atom('n, 'm). atom('o)}
val "print_int" : (string, int) -> unit
overload operator % = mod_atom
val main : unit -> unit
function main () = {
let 'm : {'x, 'x % 3 = 1. atom('x)} = 4;
let 'n = m / 3;
_prove(constraint(('m - 1) % 3 = 0));
_prove(constraint('n * 3 + 1 = 'm));
(* let x = 3 / 0; (* Will fail *) *)
print_int("n = ", n);
()
}
As can be seen, these nexp ops can be arbitrary user defined operators
and even operator overloading works (although there are some caveats).
This feature is very experimental, and some things won't work very
well once you use custom operators - notably unification. However,
this not necissarily a downside, because if restrict yourself to the
subset of sail types that correspond to liquid types, then there is
never a need to unify n-expressions. Looking further ahead, if we
switch to a liquid type system a la minisail, then we no longer need
to treat + - and * specially in n-expressions. So possible future
refactorings could involve collapsing the Nexp datatype.
2) The typechecker is stricter about valspecs (and other types) being
well-formed. This is a breaking change because previously we allowed
things like:
val f : atom('n) -> atom('n)
and now this must be
val f : forall 'n. atom('n) -> atom('n)
if we want to allow the first syntax, then initial-check should
desugar it this way - but it must be well-formed by the time it hits
the type-checker, otherwise it's not clear that we do the right
thing. Note we can actually have top-level type variables by using
top-level let bindings with P_var. There's a future line of
refactoring that would make it so that type variables can shadow each
other properly (we should do this) - currently they all have to have
unique names.
3) atom('n) is no longer syntactic sugar for range('n, 'n). The reason
why we want to do this is that if we wanted to be smart about what
sail operations can be translated into SMT operations at the type
level we care very much that they talk about atoms and not
ranges. Why? Because atom is the term level representation of a
specific type variable so it's clear how to map between term level
functions and type level functions, i.e. (atom('n) -> atom('n)) can be
reflected at the type level by a type level function with kind Int ->
Int, but the same is not true for range. Furthermore, both are
interdefinable as
atom('n) -> range('n, 'n)
range('n, 'm) -> {'o, 'n <= 'o <= 'm. atom('n)}
and I think the second is actually slightly more elegant. This change
*should* be backwards compatible, as the type-checker knows how to
convert from atom to ranges and unify them with each other, but there
may be bugs introduced here...
|
|
For example,
val test = { ocaml: "test_ocaml" } : unit -> unit
will only be external for OCaml. For other backends, it will have to be
defined.
|
