| Age | Commit message (Collapse) | Author |
|---|
|
|
|
* Improve type inference for numeric if statements (if_infer test)
* Correctly handle constraints for existentially quantified constructors (constraint_ctor test)
* Canonicalise all numeric types in function arguments, which
triggers some weird edge cases between parametric polymorphism and
subtyping of numeric arguments
* Because of this eq_int, eq_range, and eq_atom etc become identical
* Avoid duplicating destruct_exist in Env
* Handle some odd subtyping cases better
|
|
Change Typ_arg_ to A_. We use it a lot more now typ_arg is used instead of
uvar as the result of unify. Plus A_ could either stand for argument, or
Any/A type which is quite appropriate in most use cases.
Restore instantiation info in infer_funapp'. Ideally we would save this
instead of recomputing it ever time we need it. However I checked and
there are over 300 places in the code that would need to be changed to add
an extra argument to E_app. Still some issues causing specialisation to
fail however.
Improve the error message when we swap how we infer/check an l-expression,
as this could previously cause the actual cause of a type-checking failure
to be effectively hidden.
|
|
On a new branch because it's completely broken everything for now
|
|
Previously the valid constraints had to be carefully restricted to
avoid parser ambiguities between n_constraint and atyp. With the
initial check refactored, we can now parse constraints into atyp using
ATyp_app for the operators, and changing ATyp_constant into a more
general ATyp_lit for true and false. Logically this new structure is
more uniform, as atyp is now the parse representation for all
Bool-kinded things (constraints), Type-kinded things (regular types),
and Int-kinded things (n-expressions), and initial_check.ml now splits
all three into n_constraint, typ, and nexp respectively, rather than
how it was before with initial_check splitting types and nexps, but
constraints already being separate in the parser.
|
|
Mostly this is to change how we desugar types in order to make us more
flexible with what we can parse as a valid constraint as
type. Previously the structure of the initial check forced some
awkward limitations on what was parseable due to how the parse AST is
set up.
As part of this, I've taken the de-scattering of scattered functions
out of the initial check, and moved it to a re-writing step after
type-checking, where I think it logically belongs. This doesn't change
much right now, but opens up some more possibilities in the future:
Since scattered functions are now typechecked normally, any future
module system for Sail would be able to handle them specially, and the
Latex documentation backend can now document scattered functions
explicitly, rather than relying on hackish 'de-scattering' logic to
present documentation as the functions originally appeared.
This has one slight breaking change which is that union clauses must
appear before their uses in scattered functions, so
union ast = Foo : unit
function clause execute(Foo())
is ok, but
function clause execute(Foo())
union ast = Foo : unit
is not. Previously this worked because the de-scattering moved union
clauses upwards before type-checking, but as this now happens after
type-checking they must appear in the correct order. This doesn't
occur in ARM, RISC-V, MIPS, but did appear in Cheri and I submitted a
pull request to re-order the places where it happens.
|
|
This makes dealing with records and field expressions in Sail much
nicer because the constructors are no longer stacked together like
matryoshka dolls with unnecessary layers. Previously to get the fields
of a record it would be either
E_aux (E_record (FES_aux (FES_Fexps (fexps, _), _)), _)
but now it is simply:
E_aux (E_record fexps, _)
|
|
Rather than having K_aux (K_kind [BK_aux (BK_int, _)], _) represent
the Int kind, we now just have K_aux (K_int, _). Since the language is
first order we have no need for fancy kinds in the AST.
|
|
They weren't needed for ASL parser like I thought they would be, and
they increase the complexity of dealing with constraints throughout
Sail, so just remove them.
Also fix some compiler warnings
|
|
- 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
|
|
Essentially all we have to do to make this work is introduce a member of
the Value type, V_attempted_read <reg>, which is returned whenever we
try to read a register value with allow_registers disabled. This defers
the failure from reading the register to the point where the register
value is used (simply because nothing knows how to deal with
V_attempted_read). However, if V_attempted_read is returned directly as
the result of evaluating an expression, then we can replace the
expression with a single direct register read. This optimises some
indirection in the ARM specification.
|
|
Should hopefully fix memory leak in RISC-V.
Also adds an optimization pass that removes copying structs and allows
some structs to simply alias each other and avoid copying their
contents. This requires knowing certain things about the lifetimes of
the structs involved, as can't free the struct if another variable is
referencing it - therefore we conservatively only apply this
optimization for variables that are lifted outside function
definitions, and should therefore never get freed until the model
exits - however this may cause issues outside ARMv8, as there may be
cases where a struct can exist within a variant type (which are not
yet subject to this lifting optimisation), that would break these
assumptions - therefore this optimisation is only enabled with the
-Oexperimental flag.
|
|
This optimisation re-uses variables if possible, rather than
allocating new ones.
|
|
|
|
|
|
Bitvectors that aren't fixed size, but can still be shown to fit
within 64-bits, now have a specialised representation. Still need to
introduce more optimized functions, as right now we mostly have to
convert them into large bitvectors to pass them into most
functions. Nevertheless, this doubles the performance of the TLBLookup
function in ARMv8.
|
|
- Propagate types more accurately to improve optimization on ANF
representation.
- Add a generic optimization pass to remove redundant variables that
simply alias other variables.
- Modify Sail interactive mode, so it can compile a specification with
the :compile command, view generated intermediate representation via
the :ir <function> command, and step-through the IR with :exec <exp>
(although this is very incomplete)
- Introduce a third bitvector representation, between fast
fixed-precision bitvectors, and variable length large
bitvectors. The bitvector types are now from most efficient to least
* CT_fbits for fixed precision, 64-bit or less bitvectors
* CT_sbits for 64-bit or less, variable length bitvectors
* CT_lbits for arbitrary variable length bitvectors
- Support for generating C code using CT_sbits is currently
incomplete, it just exists in the intermediate representation right
now.
- Include ctyp in AV_C_fragment, so we don't have to recompute it
|
|
because >100 field records slow everything down
|
|
|
|
71020c2f460e6031776df17cf8f2f71df5bb9730 introduced assert error messages containing " revealing unescaped string literals in generated lem and prompting review of other backends.
|
|
|
|
Also fix some C optimisations
|
|
Fixes CHERI Lem build
|
|
This was _really_ slow - about 50secs for ARM. If this changes causes
breakages we should fix them in some other way.
Also using Reporting.err_unreachable in ANF translation, and fix slice
optimization when creating slices larger than 64-bits in C translation
|
|
|
|
|
|
This brings Sail closer to MiniSail, and means that
type my_range 'n 'm = {'o, 'n <= 'o <= 'm. int('o)}
will work on the left hand side of a function type in the same way as
a regular built-in range type. This means that in principle neither
range nor int need be built-in types, as both can be implemented in
terms of int('n) (atom internally). It also means we can easily
identify type variables that need to be made into implict arguments,
with the criterion for that being simply any type variable that
doesn't appear in a base type on the LHS of the function, or only
appears on the RHS.
|
|
|
|
|
|
details (TODO make this optional).
|
|
|
|
|
|
usere more flexibility about formatting generated latex.
|
|
Also add a special case for shift-left when we are shifting 8 by a two
bit opcode, or 32 by a one bit opcode.
|
|
This fixes another case we often have to patch manually in translated ASL
code where a function returns a (result, Constraint)-pair.
Also (slightly) improve the error message for when we fail to infer a
l-expression, as we are going to hit this case more often now.
|
|
Previously the following would fail:
```
default Order dec
$include <prelude.sail>
register V : vector(1, dec, vector(32, dec, bit))
val zeros : forall 'n, 'n >= 0. unit -> vector('n, dec, bit)
function main() : unit -> unit = {
V[0] = zeros()
}
```
Since the type-checker wouldn't see that zeros() must have type
`vector(32, dec, bit)` from the type of `V[0]`. It now tries both to
infer the expression, and use that to check the assignment, and if
that fails we infer the lexp to check the assignment. This pattern
occurs a lot in ASL, and we often had to patch zeros() to zeros(32) or
similar there.
|
|
|
|
Also ensure no collisions for function clause constructor categories
|
|
|
|
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.
|
|
* 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.
|
|
This should fix the issue in cheri128
Also introduce a feature to more easily debug the C backend:
sail -dfunction Name
will pretty-print the ANF and IR representation of just the Name
function. I want to make this work for the type-checker as well, but
it's a bit hard to get that to not fire during re-writing passes right
now.
|
|
This goes partway to resolving issue #23, as it now generates C code,
but it seems like there is still an issue with the generated C.
|
|
We need to ensure that we expand type-synonyms when calculating which
types a register depends on during topological sorting in order to
place the undefined_type function in the correct place, even when type
is indirected through a function.
|
|
When topologically sorting the top-level definitions, we add the
undefined_X functions for any type X to a registers dependencies if it
uses the type X, this ensures that any such functions are generated
before the register declaration. In theory this is only needed for
OCaml, but adding these edges in the definition graph shouldn't cause
any issues.
|
|
For ASL parser, we have code that can add additional constraints to a
function if they are required by functions it calls, but for more
general range analysis we need to restrict the return types of various
ASL functions that return int. To do this we can write some code that
walks over the type-checked AST for a function body and tries to infer
a more restrictive return type at each function exit point. Then we
try to union those types together if possible to infer a more
restricted return type.
For example, for the highest_set_bit function
val highest_set_bit : forall ('n : Int), 'n >= 0. bits('n) -> int
function highest_set_bit x = {
foreach (i from ('n - 1) to 0 by 1 in dec) {
print_int("idx = ", i);
if [x[i]] == 0b1 then return(i) else ()
};
return(negate(1))
}
Which is annotated as returning any int, we can synthesise a return
type of
{'m, ('m = -1 | (0 <= 'm & 'm <= ('n - 1))). int('m)}
Currently I have this code in Sail as it's likely also useful as a
optimisation/lint but it could also live in the asl_parser repository.
|
|
(only affects Reduce on Aarch64)
|
|
Also some pretty printer improvements
Make all the tests use the same colours for green/red/yellow
|
