|
- 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
|
