| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
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
|
|
Add a new short_loc_to_string function that produces just the file and line number as
a single line. loc_to_string adds a bunch of terminal color codes and other formatting
designed for producing pretty error-messages in the terminal, which isn't ideal when
the string appears in prover output as part of an assert statement. This is should be
purely an aesthetic change.
|
|
Prevents some type variables that came from unpacking existentials
leaking into generated Coq types.
|
|
It helps the Coq backend if the shape of constraints embedded in types
doesn't change too much.
|
|
|
|
|
|
|
|
Check in a slightly nicer stylesheet for OCamldoc generated
documentation in etc. Most just add a maximum width and increase the
font size because the default looks absolutely terrible on high-DPI
monitors.
Move val_spec_ids out of initial_check and into ast_util where it
probably belongs. Rename some functions in util.ml to better match the
OCaml stdlib.
|
|
This shouldn't change any functionality.
|
|
|
|
Perhaps suprisingly to some, this did not mean that Sail was
unable to typecheck the identify function.
While doing this rename Effect_opt_pure to Effect_opt_none - as
Effect_opt_pure was the effect equivalent of Typ_annot_opt_none,
and actually means that the function definition lacks an effect
annnotation, not that the function is actually pure, so this was
*extremely* misleading. The effect_opt that actually indicated a
function is pure was (and still is) the succinct:
Effect_opt_aux (Effect_opt_effect (Effect_aux (Effect_set [], _)), _)
In fact because in the grammar we only specify effects on
valspecs (they can always be inferred for fundefs in the absence
of a valspec) effect_opts are basically vestigial and are always
Effect_opt_none.
What might actually be super nice would be to remove rec_opt,
effect_opt and typ_annot_opt from fundefs in ast.ml altogether
and if we want them in the syntax just have them in parse_ast.ml
and pull them into a valspec during the initial check.
|
|
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
|
|
When adding a constraint such as `x <= 2^n-1` to an environment
containing e.g. `n in {32, 64}` or similar, we can enumerate all
values of n and add `n == 32 & x <= 2^32-1 | n == 64 & x <= 2^64-1`
instead. The exponentials then get simplified away, which means that
we stay on the SMT solver's happy path.
This is enabled by the (experimental, name subject to change) flag
-smt_linearize, as this both allows some things to typecheck that
didn't before (see pow_32_64.sail in test/typecheck/pass), but also
may potentially cause some things that typecheck to no longer
typecheck for SMT solvers like z3 that have some support for reasoning
with power functions, or where we could simply treat the exponential
as a uninterpreted function.
Also make the -dsmt_verbose option print the smtlib2 files for the
solve functions in constraint.ml. We currently ignore the -smt_solver
option for these, because smtlib does not guarantee a standard format
for the output of get-model, so we always use z3 in this case.
Following the last commit where solve got renamed solve_unique, there
are now 3 functions for solving constraints:
* Constraint.solve_smt, which finds a solution if one exists
* Constraint.solve_all_smt, which returns all possible
solutions. Currently there's no bound, so this could loop forever if
there are infinite solutions.
* Constraint.solve_unique, which returns a unique solution if one exists
Fix a bug where $option pragmas were dropped unnecessarily.
|
|
Make type-at-cursor work for scattered function clauses in emacs
|
|
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
|
|
|
|
|
|
This supports the following syntax:
type xlen : Int = 64
type ylen : Int = 1
type xlenbits = bits(xlen)
bitfield Mstatus : xlenbits = {
SD : xlen - ylen,
SXL : xlen - ylen - 1 .. xlen - ylen - 3
}
|
|
Tweak colours of monomorphistion test output
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
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
|
|
Simply constraints further before calling Z3 to improve performance of
sizeof re-writing.
|
|
Fixes some re-writer issues that was preventing RISC-V from building
with new flow-typing constraints. Unfortunately because the flow
typing now understands slightly more about boolean variables, the very
large nested case statements with matches predicates produced by the
string-matching end up causing a huge blowup in the overall
compilation time.
|
|
|
|
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
|
|
|
|
* 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
|
|
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.
|
