| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
The suffix _lemmas is more descriptive than _extras.
|
|
Architecture-specific lemmas about concrete registers and types are generated
and written to a file <prefix>_lemmas.thy, generic lemmas are in the
theories *_extras.thy in lib/isabelle. In particular, State_extras contains
simplification lemmas about the lifting from prompt to state monad.
|
|
|
|
|
|
Generate only one Lem model based on the prompt monad (instead of two models
with different monads), and add a lifting from prompt to state monad. Add some
Isabelle lemmas about the monad lifting.
Also drop the "_embed" and "_sequential" suffixes from names of generated
files.
|
|
- 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.
|
|
removed IK_cond_branch, and added IK_branch
|
|
|
|
passing tests.
|
|
|
|
(accidentally committed the wrong file)
|
|
Makes bitvector typeclass instance dictionaries disappear from generated
Isabelle output.
|
|
combinators)
Add Isabelle-specific theories imported directly after monad definitions, but
before other combinators. These theories contain lemmas that tell the function
package how to deal with monadic binds in function definitions.
|
|
The internal function _reg_deref is declared as pure, so that bitfield setters
can be implemented as read-modify-write, while only having a wreg effect.
However, for the Lem shallow embedding, the read step of those setters needs to
be embedded into the monad. This could be special-cased in the Lem pretty
printer, but then the pretty printer would have to replicate some logic of the
letbind_effects rewriting step. It seems simplest to add the effect annotation
early in the Lem rewriting pipeline, in the fix_val_specs step. This means
that this rewriting step can only be used for other backends if these
additional effects are acceptable.
|
|
- Remove vector start indices
- Library refactoring: Definitions in sail_operators.lem now use Bitvector
type class and work for both bit list and machine word representations
- Add Lem bindings to AArch64 and RISC-V preludes
TODO: Merge specialised machine word operations from sail_operators_mwords into
sail_operators.
|
|
|
|
The type-checker already supports a user-defined "exception" type that can be
used in throw and try-catch expressions. This patch adds support for that to
the Lem shallow embedding by adapting the existing exception mechanisms of the
state and prompt monads. User-defined exceptions are distinguished from
builtin exception cases. For example, the state monad uses
type ex 'e =
| Exit
| Assert of string
| Throw of 'e
to distinguish between calls to "exit", failed assertions, and user-defined
exceptions, respectively. Early return is also handled using the exception
mechanism, by lifting to a monad with "either 'r exception" as the exception
type, where 'r is the expected return type and "exception" is the user-defined
exception type.
|
|
|
|
|
|
|
|
|
|
- Add support for some internal nodes to type checker
- Add more explicit type annotations during rewriting
- Remove hardcoded rewrites for E_vector_update etc from Lem pretty-printer;
these will be resolved by the type checker during rewriting now
|
|
|
|
|
|
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
|
|
Map to calls to monadic function assert_exp that throws an exception if the
assertion is false
|
|
(complains due to added val spec)
|
|
registers is no longer xored with 48 so need to initialise it. Also use E and T values used by CHERI hw and adjust decoding functions appropriately. Fix shift functions for ocaml shallow embedding which failed to handle shifts greater than vector length.
|
|
|
|
|
|
(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
|
|
|
|
|
|
|
|
things, SF and CP bugfixing
|
|
|
|
- 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.
|
|
|
|
|
|
|
|
|
