| Age | Commit message (Collapse) | Author |
|---|
|
|
|
This refactoring is intended to allow this type to have more than just a
list of definitions in future.
|
|
|
|
Reformats input source code using the pretty printer preserving the file
structure. Probably not useable as an ocamlformat or rustfmt like tool,
but good enough to take generated code without formatting and make it
readable.
|
|
Insert $file_start and $file_end pragmas in the AST, as well as
$include_start and $include_end pragmas so we can reconstruct the
original file structure later if needed, provided nothing like
topological sorting has been done.
Have the Lexer produce a list of comments whenever it parses a file,
which can the be attached to the nearest nodes in the abstract syntax
tree.
|
|
|
|
|
|
The following now works to run sail on every HVC call with hafnium
function gdb_init() -> unit = {
// Connect to QEMU via GDB
sail_gdb_qemu("");
sail_gdb_symbol_file("hafnium.elf.sym");
sail_gdb_send("break-insert sync_lower_exception")
}
function gdb() -> unit = {
gdb_init();
while true do {
sail_gdb_send("exec-continue");
sail_gdb_sync()
}
}
|
|
Remove P_record as it's never been implemented in
parser/typechecker/rewriter, and is not likely to be. This also means
we can get rid of some ugliness with the fpat and mfpat types. Stubs
for P_or and P_not are left as they still may get added to ASL and we
might want to support them, although there are good reasons to keep
our patterns simple.
The lem warning for while -> while0 for ocaml doesn't matter because
it's only used in lem, and the 32-bit number warning is just noise.
|
|
Mostly to make constraints sent to the SMT solver and Coq nicer, but
also makes it easy to remove uninformative constraints in the Coq
back-end.
|
|
See <https://github.com/ocaml/ocaml/issues/8699#issuecomment-499108873>,
tested on 4.07.1 and 4.08+rc2.
|
|
Clean up ott grammar a bit
|
|
can now write e.g.
forall (constant 'n : Int) rather than forall ('n: Int)
which requires 'n to be a constant integer value whenever the function
is called. I added this to the 'addrsize variable on memory
reads/writes to absolutely guarantee in the SMT generation that we
don't have to worry about the address being a variable length
bitvector.
|
|
|
|
|
|
Currently only supports pure termination measures for loops with effects.
The user syntax uses separate termination measure declarations, as in the
previous recursive termination measures, which are rewritten into the
loop AST nodes before type checking (because it would be rather difficult
to calculate the correct environment to type check the separate declaration
in).
|
|
- Rename DeIid to Operator. It corresponds to operator <string> in the
syntax. The previous name is from when it was called deinfix in
sail1.
- Removed things that weren't actually common from
pretty_print_common.ml, e.g. printing identifiers is backend
specific. The doc_id function here was only used for a very specific
use case in pretty_print_lem, so I simplified it and renamed it to
doc_sia_id, as it is always used for a SIA.Id whatever that is.
- There is some support for anonymous records in constructors, e.g.
union Foo ('a : Type) = {
MkFoo : { field1 : 'a, field2 : int }
}
somewhat similar to the enum syntax in Rust. I'm not sure when this
was added, but there were a few odd things about it. It was
desugared in the preprocessor, rather than initial_check, and the
desugaring generated incorrect code for polymorphic anonymous
records as above.
I moved the code to initial_check, so the pre-processor now just
deals with pre-processor things and not generating types, and I
fixed the code to work with polymorphic types. This revealed some
issues in the C backend w.r.t. polymorphic structs, which is the
bulk of this commit. I also added some tests for this feature.
- OCaml backend can now generate a valid string_of function for
polymorphic structs, previously this would cause the ocaml to fail
to compile.
- Some cleanup in the Sail ott definition
- Add support for E_var in interpreter previously this would just
cause the interpreter to fail
|
|
Issue with pretty-printing mapping clauses types fixed by both
cf7eb8b83 and 0e2f1710a, so remove the redundant clauses. In the
parser we allow both
```
| Mapping id
{ mk_sd (SD_mapping ($2, mk_tannotn)) $startpos $endpos }
| Mapping id Colon funcl_typ
{ mk_sd (SD_mapping ($2, $4)) $startpos $endpos }
```
so we should probably use doc_binding to correctly print any
quantifier on the funcl_typ. Although since polymorphism and mappings
don't play nicely together right now this likely doesn't occur very
often in practice.
|
|
|
|
|
|
|
|
specialize functions now take a 'specialization' parameter that
specifies how they will specialize the AST. typ_ord_specialization
gives the previous behaviour, whereas int_specialization allows
specializing on Int-kinded arguments. Note that this can loop forever
unless the appropriate case splits are inserted beforehand, presumably
by monomorphisation.
rename is_nat_kopt -> is_int_kopt for consistency
|
|
This makes sure we don't do any kind of re-writing or de-scatter any
definitions when loading files into emacs. The difference here is that
normally all files are processed together, but the emacs mode loads
each file one by one. This is probably what we want to be doing
anyway, so location information stays accurate for scattered
functions for things like type-at-cursor commands and similar.
Also fix some warnings.
Fixes #32
|
|
|
|
Tweak colours of monomorphistion test output
|
|
|
|
Fix pretty printer bug
|
|
|
|
We want to ensure that no_devices.sail and devices.sail have the same
effect footprint, because with a snapshot-type release in sail-arm, we
can't rebuild the spec with asl_to_sail every time we switch from
running elf binaries to booting OS's. This commit allows registers to
have arbitrary effects, so registers that are really representing
memory-mapped devices don't have to have the wmem/rmem effect.
|
|
|
|
|
|
|
|
function (preparing for marshalling)
|
|
Remove unused name schemes and DEF_kind
|
|
Also output termination measures in Sail printer
|
|
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
|
|
|
|
We should infer type variable kinds better in initial_check.ml, but we really don't want to have to deal
with that everywhere, especially when we can no longer easily cheat and assume KOpt_none implies K_int.
|
|
Remove some dead code in Pretty_print_common
Start thinking a bit about Minisail-esque syntactic sugar in initial_check
|
|
|
|
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, _)
|
|
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
|
|
|
|
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.
|
