| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Allow a file sail.json in the same directory as the sail source file
which contains the ordering and options needed for sail files involved
in a specific ISA definition. I have an example for v8.5 in sail-arm.
The interactive Sail process running within emacs then knows about the
relationship between Sail files, so C-c C-l works for files in the ARM
spec. Also added a C-c C-x command to jump to a type error. Requires
yojson library to build interactive Sail.
|
|
Can now use C-c C-s to start an interactive Sail process, C-c C-l to
load a file, and C-c C-q to kill the sail process. Type errors are
highlighted in the emacs buffer (like with merlin for OCaml) with a
tooltip for the type-error, as well as being displayed in the
minibuffer. Need to add a C-c C-x command like merlin to jump to the
error, and figure out how to handle multiple files nicely, as well as
hooking the save function like tuareg/merlin, but this is already
enough to make working with small examples quite a bit more pleasant.
|
|
Rather than using sizeof-rewriting which is slow and error-prone, just
make implicit function arguments explicit, so:
val ZeroExtend : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)
let x : bits(32) = ZeroExtend(0xFFFF)
would be re-written (by the typechecker itself) into
val ZeroExtend : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)
let x : bits(32) = ZeroExtend(32, 0xFFFF)
then all we need to do is map implicit -> int in a rewrite, and use
trivial sizeof-rewriting only. We pretty much never want to use the
form of sizeof-rewriting that propagates function arguments through
multiple functions because it's extremely error-prone. Anything that
isn't re-writable via trivial sizeof rewriting should be a type error,
so it would be good to re-write sizeof expressions within the
type-checker.
|
|
|
|
This adds ELPA metadata, which should allow authorship
of MELPA packages for Sail mode.
Signed-off-by: Austin Seipp <aseipp@pobox.com>
|
|
For example in RISC-V for the translation table walk:
$optimize unroll 2
val walk32 ...
function walk32 ...
would create two extra copies of the walk_32 function,
walk_32_unroll_1 and walk_32_unroll_2, with only walk_32_unroll_2
being recursive. Currently we only support the case where we have
$optimize unroll, directly followed by a valspec, then a function, but
this should be generalised in future.
This optimization nearly doubles the performance of RISC-V
It is implemented using a new Optimize.recheck rewrite that replaces
the ordinary recheck_defs pass. It uses a new typechecker
check_with_envs function that allows re-writes to utilise intermediate
typechecking environments to minimize the amount of AST checking that
occurs, for performance reasons.
Note that older Sail versions including the current OPAM release will
complain about the optimize pragma, so this cannot be used until they
become up to date with this change.
|
|
|
|
test/typecheck/pass/tautology.sail constaints tests of various boolean
properties, e.g.
// de Morgan
_prove(constraint(not('p | 'q) <--> not('p) & not('q)));
_prove(constraint(not('p & 'q) <--> not('p) | not('q)));
introduce a new _not_prove case which allows us to assert in tests
that a constraint is not provable. This test essentially tests that
constraints map to sensible problems in the SMT solver, without
testing flow typing or any other features.
Add a script test/typecheck/update_errors.sh, which regenerates the
expected error messages. Testing that type-checking failures is
important, but can be brittle when the error messages change for
inconsequential reasons. This script automates fixing this.
Also ensure that this test case works correctly in Lem
|
|
On a new branch because it's completely broken everything for now
|
|
- Completely remove the nexp = nexp syntax in favour of nexp ==
nexp. All our existing specs have already switched over. As part of
this fix every test that used the old syntax, and update the
generated aarch64 specs
- Remove the `type when constraint` syntax. It just makes changing the
parser in any way really awkward.
- Change the syntax for declaring new types with multiple type
parameters from:
type foo('a : Type) ('n : Int), constraint = ...
to
type foo('a: Type, 'n: Int), constraint = ...
This makes type declarations mimic function declarations, and makes
the syntax for declaring types match the syntax for using types, as
foo is used as foo(type, nexp). None of our specifications use types
with multiple type parameters so this change doesn't actually break
anything, other than some tests. The brackets around the type
parameters are now mandatory.
- Experiment with splitting Type/Order type parameters from Int type
parameters in the parser.
Currently in a type bar(x, y, z) all of x, y, and z could be either
numeric expressions, orders, or types. This means that in the parser
we are severely restricted in what we can parse in numeric
expressions because everything has to be parseable as a type (atyp)
- it also means we can't introduce boolean type
variables/expressions or other minisail features (like removing
ticks from type variables!) because we are heavily constrained by
what we can parse unambigiously due to how these different type
parameters can be mixed and interleaved.
There is now experimental syntax: vector::<'o, 'a>('n) <-->
vector('n, 'o, 'a) which splits the type argument list into two
between Type/Order-polymorphic arguments and Int-polymorphic
arguments. The exact choice of delimiters isn't set in stone - ::<
and > match generics in Rust. The obvious choices of < and > / [ and
] are ambigious in various ways.
Using this syntax right now triggers a warning.
- Fix undefined behaviour in C compilation when concatenating a
0-length vector with a 64-length vector.
|
|
- Fix pretty printing nested constraints
- Add flow typing for if condition then { throw exn }; ... blocks
- Add optimisations for bitvector concatenation in C
|
|
The main changes so far are:
* Allow markdown formatting in doc comments. We parse the markdown
using Omd, which is a OCaml library for parsing markdown. The nice
thing about this library is it's pure OCaml and has no dependencies
other the the stdlib. Incidentally it was also developed at OCaml
labs. Using markdown keeps our doc-comments from becoming latex
specfic, and having an actual parser is _much_ nicer than trying to
hackily process latex in doc-comments using OCamls somewhat sub-par
regex support.
* More sane conversion latex identifiers the main approach is to
convert Sail identifiers to lowerCamelCase, replacing numbers with
words, and then add a 'category' code based on the type of
identifier, so for a function we'd have fnlowerCamelCase and for
type synonym typelowerCamelCase etc. Because this transformation is
non-injective we keep track of identifiers we've generated so we end
up with identifierA, identifierB, identifierC when there are
collisions.
* Because we parse markdown in doc comments doc comments can use Sail
identifiers directly in hyperlinks, without having to care about how
they are name-mangled down into TeX compatible things.
* Allow directives to be passed through the compiler to
backends. There are various $latex directives that modify the latex
output. Most usefully there's a
$latex newcommand name markdown
directive that uses the markdown parser to generate latex
commands. An example of why this is useful is bellow. We can also use
$latex noref id
To suppress automatically inserting links to an identifier
* Refactor the latex generator to make the overall generation process
cleaner
* Work around the fact that some operating systems consider
case-sensitive file names to be a good thing
* Fix a bug where latex generation wouldn't occur unless the directory
specified by -o didn't exist
This isn't quite all the requested features for good CHERI
documentation, but new features should be much easier to add now.
|
|
* Previously we allowed the following bizarre syntax for a forall
quantifier on a function:
val foo(arg1: int('n), arg2: typ2) -> forall 'n, 'n >= 0. unit
this commit changes this to the more sane:
val foo forall 'n, 'n >= 2. (arg1: int('n), arg2: typ2) -> unit
Having talked about it today, we could consider adding the syntax
val foo where 'n >= 2. (arg1: int('n), arg2: typ2) -> unit
which would avoid the forall (by implicitly quantifying variables in
the constraint), and be slightly more friendly especially for
documentation purposes. Only RISC-V used this syntax, so all uses of
it there have been switched to the new style.
* Second, there is a new (somewhat experimental) syntax for
existentials, that is hopefully more readable and closer to
minisail:
val foo(x: int, y: int) -> int('m) with 'm >= 2
"type('n) with constraint" is equivalent to minisail: {'n: type | constraint}
the type variables in typ are implicitly quantified, so this is equivalent to
{'n, constraint. typ('n)}
In order to make this syntax non-ambiguous we have to use == in
constraints rather than =, but this is a good thing anyway because
the previous situation where = was type level equality and == term
level equality was confusing. Now all the type type-level and
term-level operators can be consistent. However, to avoid breaking
anything = is still allowed in non-with constraints, and produces a
deprecated warning when parsed.
|
|
Currently not enabled by default, the flag -Xconstraint_synonyms
enables them
For generating constraints in ASL parser, we want to be able to give
names to the constraints that we attach to certain variables. It's
slightly awkward right now when constraints get long complicated
because the entire constraint always has to be typed out in full
whenever it appears, and there's no way to abstract away from that.
This adds constraint synonyms, which work much like type synonyms
except for constraints, e.g.
constraint Size('n) = 'n in {1, 2, 4, 8} | 128 <= 'n <= 256
these constraints can then be used instead of the full constraint, e.g.
val f : forall 'n, where Size('n). int('n) -> unit
Unfortunatly we need to have a keyword to 'call' the constraint
synonym otherwise the grammer stops being LR(1). This could be
resolved by parsing all constraints into Parse_ast.atyp and then
de-sugaring them into constraints, which is what happens for
n-expressions already, but that would require quite a bit of work on
the parser.
To avoid this forcing changes to any other parts of Sail, the intended
invariant is that all constraints appearing anywhere in a type-checked
AST have no constraint synonyms, so they don't have to worry about
matching on NC_app, or calling Env.expand_typquant_synonyms (which
isn't even exported for this reason).
|
|
Also allow options to be set via a pragma in Sail files
|
|
|
|
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.
|
|
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/
|
|
|
|
|
|
|
|
|
|
Fix a bug in initial check which caused X() = y to expect an additional parameter.
Some tweaks to sail2 emacs mode
|
|
More work on Latex output
|
|
|
|
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.
|
|
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
|
|
|
|
aarch64 vector instructions.
There's maybe a better more general way to do this but I'm not sure
what that would be.
|
|
|
|
|
|
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
|
|
The code for these is now rather ugly though... it needs to be cleaned up at some point
Also various improvements to new menhir parser
|
|
|
|
|
|
to translate exceptions in ASL. See test/typecheck/pass/trycatch.sail.
|
|
|
|
For example:
default Order dec
val bit[64] -> unit effect pure test64
val cast forall 'n, 'n = 32 | 'n = 64. bit['n] -> unit effect pure test
function forall 'n. unit test addr =
{
_prove(constraint('n != 16));
assert(constraint('n = 64), "64-bit mode");
_prove(constraint('n = 64));
test64(addr);
}
This doesn't affect the AST at all as _prove is just a ordinary function
that the typechecker treats specially.
|
|
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.
|
|
|
|
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
|
|
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).
|
|
|
|
|
