| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
With the new comment syntax, Isabelle seems to barf on that comment,
apparently due to the backslashes.
|
|
|
|
The inter-instruction semantics is responsible for correctly handling memory
writes without tags; the lifting to the state monad handles it as writing a
value with a zero tag bit.
|
|
Use E_read_memt for reading tagged memory, as in sail2_impl_base.lem,
and rename E_write_mem to E_write_memt, since it always writes a tag.
|
|
It is used for nondeterministic choice, so Undefined might be
misleading.
|
|
Lets one distinguish in a trace whether an instruction tried to read
tagged memory or just read data without caring about the tag; this is
useful for formulating predicates on traces.
|
|
|
|
Removes some friction by back-and-forth conversion when handling events
|
|
Running traces, directly accessing memory state
|
|
- Merge tag reading/writing outcomes into memory value reading/writing outcomes
- Add effective address to Write_mem; this duplicates information in the
Write_ea outcome that should come before, but it makes the effective address
more conveniently available in events and traces, and it allows the following
simplification in the state monad:
- Remove write_ea field from state record; the effective address is now
expected as a parameter to the write_memS function
- Remove last_exclusive_operation_was_load field from state record; this was
used to keep track of exclusive loads, but this was a a relatively coarse
approximation anyway, so it might make more sense to track this in
(architecture-specific) Sail code. Overall, the state record now simply
contains the fields regstate, memstate, tagstate.
|
|
Uses new primop 'string_take' which is much easier to implement in e.g. C
|
|
|
|
hex_bits_N_matches_prefix
|
|
|
|
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.
|
|
|
|
|
|
Use nondeterministic choice by default instead of a deterministic bitstream
generator in the state, which is slightly awkward to reason about, because
every use of undefined_boolS changes the state. The previous behaviour can be
implemented as Sail code, if desired.
Also add a default implementation of internal_pick that nondeterministically
chooses an element from a list.
|
|
|
|
|
|
|
|
|
|
(involved some manual tinkering with gitignore, type_check, riscv)
|
|
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).
|
|
|
|
|
|
isabelle (but isabelle almost certainly broken)
|
|
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.
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
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.
|
|
mono rewrites
|
|
Also clean up some library functions a bit, and add some missing failure
handling variants of division operations on bitvectors.
|
|
They are used in various specs and test cases.
|
|
(note that they're already declared in lib/arith.sail)
|
|
|
|
Rename l2.ott to sail.ott
|
|
definitions from sail/lib.
|
|
In particular, improve indentation of if-expressions, and provide infix syntax
for monadic binds in Isabelle, allowing Lem to preserve source whitespace.
|
