| 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.
|
|
|
|
Fixed an issue with pattern matching on enums
Fixed an issue whereby fix_early_returns would cause memory leaks
Added optimizations for some of the builtins used in the decode
function. Optimizations are turned on with the -O flag.
|
|
Add support for short-ciruiting and/or. I forgot about this in the
original ANF specification and not having it causes problems for the
ARM spec.
|
|
Now compiles to C and builds a working executable. Just need to
correctly implement all the library builtins (some are still stubs),
and it should work.
|
|
|
|
Turns out the __TakeColdReset function is actually in the v8.3 XML. I
went and looked for it, and it's there, it just wasn't being picked up
by ASL parser because it's not called from any instructions. I added a
new field to the json config files for ASL parser that can tell it
about any such special functions that it should guarantee to include.
Also fixed a bug in C loop compilation
|
|
|
|
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.
|
|
|
|
|
|
|
|
to help Lem go from a general type `bits('n)` to a specific type `bits(16)`
at a case split, and the other way around for a returned value.
Doesn't handle function clause patterns yet
|
|
|
|
|
|
Can now compile things like early returns. The same approach should
work for exception handling as well. Once that's in place, just need
to work a bit more on getting union types to work + the library of
builtins, then we should be able to compile and run some of our specs
via C. Also added some documentation in comments for the general
approach taken when compiling (need many more though).
|
|
|
|
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.
|
|
|
|
|
|
|
|
Also refactored the hand written ARM prelude and pulled out some common functionality into files in sail/lib
|
|
|
|
- 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.
|
|
|
|
(no vector type start position, comment syntax)
|
|
|
|
Fixed test cases for ocaml backend and interpreter
|
|
|
|
|
|
|
|
|
|
Works with the vector branch of asl_parser
|
|
|
|
Add the ast.sed script we need to build sail. Currently we just need
this to fix up the locations in the AST but it will be removed once we
can share locations between ocaml and lem.
|
|
|
|
Also, to support this,
constant propagation for integer multiply,
fix substitution of concrete values for nvars,
size parameters in single argument functions,
fix kind for itself,
add eq_atom to prelude
|
|
|
|
- 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
|
|
aarch64 vector instructions.
There's maybe a better more general way to do this but I'm not sure
what that would be.
|
|
and_bool and or_bool now are treated specially in the ocaml backend,
so that they have the correct short-circuiting behaviour. This is
required so that assertions don't fail for the ARM spec for predicates
that shouldn't be tested in certain circumstances, for example things like:
IsAArch32() && AArch32_specific_predicate
Also fixed an issue in the sail library for ocaml where greater than
or equal to was being mapped to greater than.
|
|
|
|
|
|
|
|
Added a test case for this behavior
|
|
experiments
|
|
|
