| Age | Commit message (Collapse) | Author |
|---|
|
default (off by default).
|
|
|
|
|
|
version instead and make sure to install util and copy it to ocaml build directory.
|
|
ocaml main so that we can have simboot + kernel. Support UART output only.
|
|
|
|
|
|
resolving the difference in type parameters between the prompt and state
monads, and allowing a single output file to be used with either.
Normally, the type alias is to the prompt monad, but for HOL4 we use the
state monad.
|
|
|
|
Also add test cases and Isabelle lemmas
|
|
|
|
(should really make the Lem pretty printer use the solver properly,
but this is a useful stopgap)
|
|
|
|
|
|
|
|
The pattern types may be subtypes, using those caused it to try rewriting
int parameters and failing
|
|
|
|
In order to use up-to-date sequential CHERI model for test suite
|
|
Found bugs by running CHERI test suite on Isabelle-exported model: signed
less-than for bit lists was missing negations for the two's complement, and
unsigned less-than compared the reverse lists.
Since all other backends implement this in Sail, it seems best to just remove
this code.
Also add support for infix operators to Lem backend, by z-encoding their
identifiers like the other backends do.
|
|
|
|
confusion on case insensitive file systems (e.g. mac).
|
|
of omitting valspec in documentation if it is deemed too verbose and still have hyperlinks work. The caveat is that it could result in multiply defined labels.
|
|
with documents containing listings in multiple languages.
|
|
|
|
|
|
|
|
Typechecking for-loops failed after the Lem rewriting passes in some cases: if
the lower bound for the loop may be greater than the upper bound, the loop
variable's type might be empty, and it cannot be initialised. This patch adds
a guard "lower <= upper" around the loop body, and removes it again during
pretty-printing.
|
|
|
|
|
|
Filled with default values (e.g., 0) and used to initialise the state monad.
There is already code to generate a Sail function "initialize_registers", but
this is monadic itself, so it cannot be used to initialise the monad.
|
|
|
|
The datatype package of HOL4 does not support the prompt monad, so this patch
restores the option to generate a model that only uses the state monad. Also
add a Makefile target cheri_sequential.lem in the cheri/ directory.
|
|
Otherwise some clauses disappear
|
|
|
|
(from Thomas)
|
|
|
|
Adds return type to pattern so that the original function body is still
type checked, rather than switching to type inference which may fail.
|
|
+ add additional lexp
+ update aarch64 mono demo source
- still needs support for tyvars from assignments in dependency analysis
|
|
Add value-only version of compute_{pat,exp}_alg to help
Experiment with adding equality constraints between type vars and args in
Coq output
|
|
|
|
1. Experiment with allowing some flow typing on mutable variables for
translating ASL in a more idiomatic way. I realise after updating some
of the test cases that this could have some problematic side effects
for lem translation, where mutable variables are translated into
monadic code. We'd need to ensure that whatever flow typing happens
for mutable variables also works for monadic code, including within
transformed loops. If this doesn't work out some of these changes may
need to be reverted.
2. Make the type inference for l-expressions a bit smarter. Splits the
type checking rules for l-expressions into a inference part and a
checking part like the other bi-directional rules. Should not be able
to type check slightly more l-expresions, such as nested vector slices
that may not have checked previously.
The l-expression rules for vector patterns should be simpler now, but
they are also more strict about bounds checking. Previously the bounds
checks were derived from the corresponding operations that would
appear on the RHS (i.e. LEXP_vector would get it's check from
vector_access). This meant that the l-expression bounds checks could
be weakend by weakening the checks on those operations. Now this is no
longer possible, there is a -no_lexp_bounds_check option which turns
of bounds checking in l-expressions. Currently this is on for the
generated ARM spec, but this should only be temporary.
3. Add a LEXP_vector_concat which mirrors P_vector_concat except in
l-expressions. Previously there was a hack that overloaded LEXP_tup
for this to translate some ASL patterns, but that was fairly
ugly. Adapt the rewriter and other parts of the code to handle
this. The rewriter for lexp tuple vector assignments is now a rewriter
for vector concat assignments.
4. Include a newly generated version of aarch64_no_vector
5. Update the Ocaml test suite to use builtins in lib/
|
|
Removes some patches in ASL parser
Allow immutable variables to shadow mutable ones. This is useful for
translating ASL.
|
|
|
|
- originally based on the Lem backend
- added externs to some of the library files and tests
- added wildcard to extern valspecs in parser
- added Type_check.get_val_spec_orig to return the valspec with the
function's original names for bound type variables
Note that most of the tests will fail currently
|
|
|
|
Take into account existential types when determining bounds for the loop
variable
|
|
|
|
Use non-recursive fix_eff_exp instead of recursive propagate_exp_effect,
assuming that the effects of subexpressions have already been fixed by the
recursive calls of the rewriter.
|
|
This is meant to increase performance; for example, generating debug messages
that include pretty-printed expressions can be very costly, if those
expressions are complex (e.g. deeply nested E_internal_plet nodes representing
a long sequence of monadic binds).
|
|
builds this defaults to git root.
|
