| Age | Commit message (Collapse) | Author |
|---|
|
One day we will be free from the 4.02.3 menace, but today is not that day. :(
This should fix Sail on Jenkins
This reverts commit 86e29bcbb1597c4ef1f6cae8edbeed42f9a31414.
|
|
Especially for return expressions, which fixes a test case
|
|
|
|
Handles mutable variables and conditionals (there are still some corner
cases that don't appear in Aarch64 to do).
The pretty printer is now back to preferring to use concrete types, but
has a special case for casts to print more general types.
|
|
One due to using raw types from the type checker in casts without trying
to turn them into sane types, the other due to forgetting to use the
constraint when trying to simplify sizes in existential types. Both
triggered because the type checker now records more specific types.
|
|
1. for monadic values (not in a terribly useful way, though)
2. for more types
|
|
|
|
|
|
The new option -dcoq_debug_on takes a list of functions to output tracing
on.
|
|
|
|
Rather than exporting the implementation of type annotations as
type tannot = (Env.t * typ * effect) option
we leave it abstract as
type tannot
Some additional functions have been added to type_check.mli to work
with these abstract type annotations. Most use cases where the type
was constructed explicitly can be handled by using either mk_tannot or
empty_tannot. For pattern matching on a tannot there is a function
val destruct_tannot : tannot -> (Env.t * typ * effect) option
Note that it is specifically not guaranteed that using mk_tannot on
the elements returned by destruct_tannot re-constructs the same
tannot, as destruct_tannot is only used to give the old view of a type
annotation, and we may add additional information that will not be
returned by destruct_tannot.
|
|
|
|
|
|
- Fix ambiguities in parser.mly
- Ensure that no new identifiers are bound in or-patterns and
not-patterns, by adding a no_bindings switch to the
environment. These patterns shouldn't generate any bogus flow typing
constraints because we just pass through the original environment
without adding any possible constraints (although this does mean we
don't get any flow typing from negated numeric literals right now,
which is a TODO).
- Reformat some code to match surrounding code.
- Add a typechecking test case for not patterns
- Add a typechecking test case for or patterns
At least at the front end everything should work now, but we need to
do a little bit more to rewrite these patterns away for lem etc.
|
|
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.
|
|
Changes are:
- String.capitalize -> String.capitalize_ascii
- String.uppercase -> String.uppercase_ascii
- String.lowercase -> String.lowercase_ascii
Basically just making the change that the warning message suggested.
|
|
E_internal_cast, E_sizeof_internal, E_internal_exp,
E_internal_exp_user, E_comment, and E_comment_struc were all
unused. For a lem based interpreter, we want to be able to compile it
to iUsabelle, and due to slowness inherent in Isabelle's datatype
package we want to remove unused constructors in our AST type.
Also remove the lem_ast backend - it's heavily bitrotted, and for
loading the ARM ast into the interpreter it's just not viable to use
this approach as it just doesn't scale. We really need a way to be
able to serialise and deserialise the AST efficiently in Lem.
|
|
|
|
|
|
Fixes monomorphisation on files using mappings.
Also extended constant propagation to handle pattern matches on
bitvector expressions (because an earlier rewrite replaces the literals).
Also moved L_undef rewriting because monomorphisation can handle them
but not the replacement functions.
|
|
Some more testing needed to make sure it runs FreeBSD properly and CHERI before merging
|
|
Uses previous stage to deal with (e.g.) guards.
New option -dcoq_warn_nonex tells you where all of the extra default
cases were added.
|
|
|
|
(e.g., coerce_int_nat in aarch64)
|
|
Adds missing constraints for aarch64
|
|
|
|
|
|
|
|
As a result, add proof to pow2.
|
|
|
|
|
|
Changes to the interpreter to better support constant folding during
compilation mean it can now throw exceptions to the caller, allow the
caller to handle the error, rather than simply printing an error. This
broke the ARM interpreter test because exit() is handled by throwing
an Exit exception in the interpreter.
|
|
interpreter implementations of same.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
On second thought, this change should not really make a difference; the CHERI
test suite still passes without it. Moreover, using unsigned conversion of the
vector argument leads to more convenient lemmas for the provers.
|
|
add_vec_int and similar functions in the Lem library used unsigned instead of
signed conversion.
|
|
|
|
|
|
|
|
|
|
This makes it consistent with the C backend, and also makes it easier to compare traces across execution re-runs.
|
|
If we have an nexp that we can't print, look for an equivalent type
variable before looking for a constant - the constant may only be valid
locally (e.g., under an if) while the type variable will be valid
throughout the function.
Fixes a problem with aget_Mem on aarch64.
|
