| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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.
|
|
|
|
mono rewrites
|
|
Also clean up some library functions a bit, and add some missing failure
handling variants of division operations on bitvectors.
|
|
|
|
In particular, improve indentation of if-expressions, and provide infix syntax
for monadic binds in Isabelle, allowing Lem to preserve source whitespace.
|
|
|
|
- Update Lem bindings and extras files
- Rewrite Nexp_var's if they are bound to a constant, similar to Nexp_id's
(used for cap_size in the CHERI spec)
- Add Lem and Isabelle Makefile targets for CHERI
|
|
Some functions are partial, e.g. converting a bitvector to an integer, which
might fail for the bit list representation due to undefined bits. Undefined
cases can be handled in different ways:
- call Lem's failwith, which maps to undefined/ARB in Isabelle and HOL (the
default so far),
- return an option type,
- raise a failure in the monad, or
- use a bitstream oracle to resolve undefined bits.
This patch adds different versions of partial functions corresponding to those
options. The desired behaviour can be selected by choosing a binding in the
Sail prelude. The naming scheme is that the failwith version is the default,
while the other versions have the suffixes _maybe, _fail, and _oracle,
respectively.
|
|
|
|
- Use simplified monad type (e.g., without the with_aux constructors that are
not needed by the shallow embedding).
- Add support for registers with arbitrary types (e.g., records, enumerations,
vectors of vectors). Instead of using bit lists as the common representation
of register values at the monad interface, use a register_value type that is
generated per spec as a union of all register types that occur in the spec.
Conversion functions between register_value and concrete types are generated.
- Use the same representation of register references as the state monad, in
preparation of rebasing the state monad onto the prompt monad.
- Split out those types from sail_impl_base.lem that are used by the shallow
embedding into a new module sail_instr_kinds.lem, and import that. Removing
the dependency on Sail_impl_base from the shallow embedding avoids name clashes
between the different monad types.
Not yet done:
- Support for reading/writing register slices. Currently, a rewriting pass
pushes register slices in l-expressions to the right-hand side, turning a
write to a register slice into a read-modify-write. For interfacing with the
concurreny model, we will want to be more precise than that (in particular
since some specs represent register files as big single registers containing a
vector of bitvectors).
- Lemmas about the conversion functions to/from register_value should be
generated automatically.
|
|
|
|
|
|
Makes bitvector typeclass instance dictionaries disappear from generated
Isabelle output.
|
|
|
|
Also, rename a few functions for uniformity, e.g. bool_and -> and_bool
|
|
Translates atom('n) types into itself('n) types that won't be erased
Also exports more rewriting functions
|
|
(complains due to added val spec)
|
|
(and fix up monomorphisation)
|
|
Moreover, add support for pretty-printing (to Lem) vector access/update
operations for vectors with non-constant, but normalized start index.
|
|
Requires version of Lem with real number support, currently at
https://bitbucket.org/bauereiss/lem/branch/reals
|
|
|
|
|
|
- Remove start indices and indexing order from bitvector types. Instead add
them as arguments to functions accessing/updating bitvectors. These arguments
are effectively implicit, thanks to wrappers in prelude_wrappers.sail and a
"sizeof" rewriting pass.
- Add a typeclass for bitvectors with a few basic functions (converting to/from
bitlists, converting to an integer, getting and setting bits). Make both
monads use this interface, so that they work with both the bitlist and the
machine word representation of bitvectors.
|
|
mono-experiments
|
|
|
|
Note: The effect annotations of the execute function differ between CHERI and
MIPS, so I split out a new file mips_ast_decl.sail for MIPS with just the
initial declarations of ast, decode, and execute (with the right effects for
MIPS).
|
|
|
|
|
|
- Add back support for bit list representation of bit vectors, for backwards
compatibility in order to ease integration with the interpreter. For this
purpose, split out a file sail_operators.lem from sail_values.lem, and add a
variant sail_operators_mwords.lem for the machine word representation of
bitvectors. Currently, Sail is hardcoded to use machine words for the
sequential state monad, and bit lists for the free monad, but this could be
turned into a command line flag.
- Add a prelude_wrappers.sail file for glueing the Sail prelude to the Lem
library. The wrappers make use of sizeof expressions to extract type
information from bitvectors (length, start index) in order to pass it to the
Lem functions.
- Add early return support to the free monad, using a new constructor "Return
of 'r". As with the sequential monad, functions with early return are
wrapped into "catch_early_return", which extracts the return value at the end
of the function execution.
|
