| Age | Commit message (Collapse) | Author |
|---|
|
Looks like Jenkins is still on OCaml 4.02.3. We should probably upgrade to 4.05 at some point.
|
|
Also fixes to C backend for compiling MIPS spec to C
- Fix an issue with const correctness in internal_vector_update
functions generated by C backend
- Add builtins for MIPS to sail.h
- Fix an issue where reg_deref didn't work when called on pointers to
large bitvectors, i.e. vectors containing references to large
bitfields as in the MIPS TLB code
- Various bug fixes and changes for running U-boot on ARM model,
including for interpreter and OCaml compilation.
- Fix memory leak issues and incorrect shadowing for foreach loops
- Update C header file. Fixes memory leak in memory read/write
builtins.
- Add aux constructor to ANF representation to hold environment
information.
- Fix undefined behavior caused by optimisation left shifting uint64_t
vectors 64 or more times. Unfortunately there's more issues because
the same happens for X >> 64 right shifts. It would make sense for
this to be zero, because that would guarantee the property that ((X
>> n) >> m) == (X >> (n + m)) but we probably need to do (X >> (n -
1) >> 1) in the optimisation to ensure that we don't cause
UB. Shifting by 63 and then by 1 is well-defined, but shifting by 64
in one go isn't according to the C standard. This issue with
right-shifts only occurs for zero-length vectors, so it's not a huge
deal, but it's still annoying.
- Add versions of print_bits and print_int that print to
stderr. Follows OCaml convention of print/prerr. Should make things
more explicit. Different backends had different ideas about where
print should output to, not every backend needs to have this
(e.g. theorem prover backends don't need to print) but having both
stderr and stdout seperate and clear is useful for executable models
(UART needs to be stdout, debug messages should be stderr).
|
|
|
|
(Similar to the proper translation for function definitions)
|
|
Otherwise it has occasional problems working out the return type
|
|
Useful for partial test cases (e.g., some of the typechecking tests)
Also a bonus warning for such functions in normal use
|
|
|
|
(<5% on a simple test) but dramatically reduces memory usage compared to having a hash table entry per byte!
|
|
declaration"
This reverts commit 895f868cd537277ba61dfc427fee0e288af7e226.
These are actually treated as Ints (although you could pretend they
weren't and it mostly worked).
|
|
Stops (e.g.) an Int being used as a Type, including when no kind was
declared. The following commit will remove the test for the latter
case.
|
|
|
|
|
|
|
|
|
|
|
|
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)
|
