| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
Update INSTALL.md
|
|
The new option -dcoq_debug_on takes a list of functions to output tracing
on.
|
|
|
|
adding sail's installation steps for macOS
|
|
isa spec.
|
|
|
|
|
|
|
|
|
|
This reverts commit 4c84c70eafbbf9bea475e3264f21eedc3555021f.
|
|
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.
|
|
Fix a tiny typo in INSTALL.md
|
|
|
|
|
|
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
|
|
This allows debug messages to include the current cycle count
which can be useful for debugging.
|
|
Several v8.4 tests were failing because they attempted to enter EL2 secure
mode (which is supported on v8.4 but not on v8.3).
This test detects an attempt to enter EL2 secure and reports an easily diagnosed
error message.
|
|
|
|
|
|
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.
|
|
|
|
Use eauto so that user-added hints are more flexible,
example with Replicate in aarch64, dropped zbool to prevent slow
proof searches (and preprocessing deals with boolean comparisons now).
Report failed constraints after preprocessing;
Separate preprocessing tactic out.
|
|
|
|
(e.g., coerce_int_nat in aarch64)
|
|
|
|
|
|
Adds missing constraints for aarch64
|
|
|
|
|
|
|
|
As a result, add proof to pow2.
|
|
|
|
|
|
|
|
to code gen issue.
|
|
|
