| Age | Commit message (Collapse) | Author |
|---|
|
|
|
requires syntax change for unit constructors of union types.
|
|
definitions.
|
|
|
|
|
|
version for mips.
|
|
intialising and dumping CHERI state. Somewhat working cheri sail2 model.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
- 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.
|
|
Make state monad parametric in register state, and generate a record with
registers from the Sail spec
|
|
Add a test case with the MIPS spec using the TLB stub.
Use the sequential monad for Lem testing for now; the free monad (in
"prompt.lem") has not been updated for machine words yet.
|
|
|
|
length, and removed redundant calls to extension functions.
|
|
|
|
val specs are the same
|
|
|
|
annotated patterns and lexps
Added get_enum to type checker interface
|
|
* Experimented with using list<bit> to clean up manually monomorphised code in MIPS tlb
* Added option -dtc_verbose to control verbosity of new typechecker
* Allowed functions with val specs to omit their type declarations
|
|
This introduces some shift/reduce and reduce/reduce conflicts, but I don't think these matter.
|
|
* Fixed a bug where non-polymorphic function return types could be incorrect
* Added support for LEXP_memory AST node
* Flow typing constraint generation for all inequality operators
* Better support for increasing vector indices in field access expressions
|
|
|
|
Also:
- Added support for foreach loops
- Started work on type unions
- Flow typing can now generate constraints, in addition to restricting range-typed variables
- Various bugfixes
- Better unification for nexps with multiplication
|
