| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
vector_access is a bit hacky at the moment - it expects a constraint to
be shown between the index and the list size, but we don't track list
sizes in general
|
|
dtb to be mapped.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
Move mono_rewrites into lib
|
|
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.
|
|
|
|
(will do individual models later)
|
|
|
|
|
|
Currently contains Lem and Sail libraries, and RISC-V and CHERI-MIPS specs.
|
|
In order to use up-to-date sequential CHERI model for test suite
|
|
|
|
|
|
|
|
|
|
|
|
(still needs some Lem work on types before it will be useful)
|
|
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.
|
|
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/
|
|
- 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
|
|
|
|
|
|
|
|
|
|
Placed in lib/isabelle/manual/document.pdf
Also fixed a few typos.
|
|
|
|
|
|
Also clean up some library functions a bit, and add some missing failure
handling variants of division operations on bitvectors.
|
|
|
|
|
|
This commit primarily changes how existential types are bound in
letbindings. Essentially, the constraints on both numeric and
existentially quantified types are lifted into the surrounding type
context automatically, so in
```
val f : nat -> nat
let x = f(3)
```
whereas x would have had type nat by default before, it'll now have
type atom('n) with a constraint that 'n >= 0 (where 'n is some fresh
type variable). This has several advantages: x can be passed to
functions expecting an atom argument, such as a vector indexing
operation without any clunky cast functions - ex_int, ex_nat, and
ex_range are no longer required. The let 'x = something() syntax is
also less needed, and is now only really required when we specifically
want a name to refer to x's type. This changes slightly the nature of
the type pattern syntax---whereas previously it was used to cause an
existential to be destructured, it now just provides names for an
automatically destructured binding. Usually however, this just works
the same.
Also:
- Fixed an issue where the rewrite_split_fun_constr_pats rewriting
pass didn't add type paramemters for newly added type variables in
generated function parameters.
- Updated string_of_ functions in ast_util to reflect syntax changes
- Fixed a C compilation issue where elements of union type
constructors were not being coerced between big integers and 64-bit
integers where appropriate
- Type annotations in patterns now generalise, rather than restrict
the type of the pattern. This should be safer and easier to handle
in the various backends. I don't think any code we had was relying
on this behaviour anyway.
- Add inequality operator to lib/flow.sail
- Fix an issue whereby top-level let bindings with annotations were
checked incorrectly
|
|
|
|
Fix a bug in initial check which caused X() = y to expect an additional parameter.
Some tweaks to sail2 emacs mode
|
|
More work on Latex output
|
|
definitions from sail/lib.
|
|
Added library for simple integer arithmetic functions in lib/arith.sail
WIP TeX file for formatting latex output included in lib/sail.tex
Fixes for bugs in sail_lib
|
|
First, the specialisation of option types has been fixed by allowing
the specialisation of constructor return types - this essentially
means that a constructor, such as Some : 'a -> option('a) can get
specialised to int -> option(int), rather than int -> option('a). This
means that these constructors are treated like GADTs internally. Since
this only happens just before the C translation, I haven't put much
effort into making this very robust so far.
Second, there was a bug in C compilation for the typing of return
expressions in non-unit contexts, which has been fixed.
Finally support for vector literals that are non-bitvectors has been
added.
|
