| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
just LB_val in AST
also rename functions in rewriter.ml appropriately.
|
|
|
|
|
|
|
|
|
|
|
|
Modified initial_check.ml so it no longer requires type_internal. It's
still needs cleaned up in a few ways. Most of the things it's trying
to do could be done nicer if we took some time to re-factor it, and
some of the things should just be handled by the main typechecker,
leaving it as a think layer between the parse_ast and the ast.
Now that's done everything can be switched to the new typechecker and
the _new suffixes were deleted from everything except the
monomorphisation pass because I don't know the status of that.
|
|
Initial typecheck still uses previous typechecker
|
|
- 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
|
|
for set_vector_subrange_bit.
|
|
|
|
|
|
bit_int_of_int. Likely very little performance benefit but slightly more readable.
|
|
doesn't mistake the - for minus operator
|
|
|
|
|
|
|
|
|
|
|
|
exceptions are not permitted so a local mutable variable, ret, is used in ocaml to store the return value. This avoids having to define a new exception type for each function. Ocaml infers the type of the option when it is assigned at the return site.
|
|
bit (specifically it caused generated ocaml to fail to type check for an undef number.
|
|
taking account of register direction.
|
|
accidentally replacing Vregister with Vvalue or Vregister... Seems to work for MIPS but not sure if might encounter vector of something other than bit or register. A more specific value type would have made this a compile-time error rather than run-time.
|
|
searching easier.
|
