| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
|
|
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.
|
|
Also: Merge remote-tracking branch 'origin/sail_new_tc' into experiments
|
|
Make state monad parametric in register state, and generate a record with
registers from the Sail spec
|
|
|
|
|
|
|
|
Implemented using the exception monad, by throwing and catching the return
value
|
|
|
|
|
|
|
|
have correct rounding behaviour. Missed these when changing quot and mod functions.
|
|
|
|
optimisation went wrong.
|
|
performance bug or infinite loop. Add some missing shallow embedding funcitons.
|
|
trucation towards zero. Previous version was incorrect if result was exact and a<0 and b>0.
|
|
|
|
|
|
- Add case distinctions between bitvector types and vectors of other element
types (e.g. registers) and use the corresponding operations (i.e. "bvslice",
"bvaccess", etc for the former, and "slice", "access", etc for the latter) when
pretty-printing expressions
- Add type annotations to expressions when the type includes bitvectors with
concretely known length
- Update state.lem to use bitvectors (in the interface, at least; internally,
bitvectors are still stored as bit lists for now, since that makes it easier
to support storing different registers with different lengths)
This has been tested with the CHERI-MIPS model with some success, but some
things are still missing:
- Bitvector patterns are not handled yet
- Some bitvector length monomorphisation is needed in a few places of the model
- Some type annotations are missing, because the (old) Sail type checker does
not infer bitvector lengths in some instances where one would hope it to do
that; this should be checked with the new type checker
|
|
|
|
|
|
|
|
that uses the new Lem machine words library.
|
|
|
|
|
|
# Conflicts:
# src/lem_interp/interp.lem
# src/lem_interp/interp_inter_imp.lem
# src/lem_interp/interp_interface.lem
# src/parser.mly
# src/pretty_print_lem.ml
|
|
|
|
zero but it is not exposed via Bit_int_Z. Use it instead of rolling our own. Also ocaml / and mod already do the right thing.
|
|
for set_vector_subrange_bit.
|
|
Some tests intentionally produce undefined values (e.g. divide by zero) and this might be required for them to work.
|
|
|
|
bytes. This makes loading binaries much quicker but doesn't seem to make a big difference to execution speed.
|
|
|
|
bit_int_of_int. Likely very little performance benefit but slightly more readable.
|
|
|
|
|
|
need to use power.
|
|
|
|
|
|
neq_range.
|
|
|
