| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
(so that we get enough type annotations for bitvectors)
|
|
Isabelle does not like nested annotations like "((exp :: typ) :: typ)".
|
|
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.
|
|
|
|
|
|
It assumes that execute is non-recursive, which is not the case for RISC-V with
compressed instructions. Splitting execute into different auxiliary functions
for each clause is probably still useful, as Isabelle is likely to parse many
small functions faster than one big (potentially recursive) function, but this
splitting should be done in the rewriter instead of the pretty-printer, in
order to properly deal with recursion.
|
|
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.
|
|
Allow pretty-printing of existential types, if the existentially quantified
variables do not actually appear in the Lem output. This is useful for the bit
list representation of bitvectors, as it will print the type annotation "list
bitU" for bitvectors whose length depends on an existentially quantified
variable.
|
|
Uses the typechecker tests for now. Also fix two minor bugs in pretty-printer
and rewriter uncovered by the tests.
|
|
- 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.
|
|
|
|
|
|
Keep track of which type variables have been bound in the function declaration,
and allow those to be pretty-printed
|
|
|
|
For example:
bitfield cr : vector(8, dec, bit) = {
CR0 : 7 .. 4,
LT : 7,
CR1 : 3 .. 2,
CR2 : 1,
CR3 : 0,
}
The difference this creates a newtype wrapper around the vector type,
then generates getters and setters for all the fields once, rather
than having to handle this construct separately in every backend.
|
|
Experimenting with porting riscv model to new typechecker
|
|
|
|
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.
|
|
Was missing the case where the tuple of arguments is bound against a single
variable using P_id (not P_as). Now replaces that with the expected number of
argument variables, and rebinds the single variable in the body, as for the
other cases.
|
|
Works with the vector branch of asl_parser
|
|
This makes Lem prefer plain "definition" when generating Isabelle output for
functions, which is processed by Isabelle much faster than "fun"/"function"
definitions.
This change is not complete yet, because the Sail library functions still need
to be changed to not use tupled arguments (possibly as part of a bigger
refactoring of the library). For now, external functions are special-cased in
the pretty-printer and get tupled arguments.
|
|
|
|
|
|
Also fix bug in mono analysis with generated variables
Breaks lots of typechecking tests because it generates unnecessary
equality tests on units (and the tests don't have generic equality),
which I'll fix next.
|
|
|
|
- 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
|
|
|
|
|
|
|
|
Alastair's test cases revealed that using regular ints causes issues
throughout sail, where all kinds of things can internally overflow in
edge cases. This either causes crashes (e.g. int_of_string fails for
big ints) or bizarre inexplicable behaviour. This patch switches the
sail AST to use big_int rather than int, and updates everything
accordingly.
This touches everything and there may be bugs where I mistranslated
things, and also n = m will still typecheck with big_ints but fail at
runtime (ocaml seems to have decided that static typing is unnecessary
for equality...), as it needs to be changed to eq_big_int.
I also got rid of the old unused ocaml backend while I was updating
things, so as to not have to fix it.
|
|
|
|
For example,
val test = { ocaml: "test_ocaml" } : unit -> unit
will only be external for OCaml. For other backends, it will have to be
defined.
|
|
For example:
val test = { ocaml: "test_ocaml", lem: "test_lem" } : unit -> unit
val main : unit -> unit
function main () = {
test ();
}
for a backend not explicitly provided, the extern name would be simply
"test" in this case, i.e. the string version of the id.
Also fixed some bugs in the ocaml backend.
|
|
|
|
|
|
embedding
Checks for command-line flag -undefined_gen and uses the undefined value
generator functions of the form undefined_typ to initialise registers
|
|
|
|
Translates atom('n) types into itself('n) types that won't be erased
Also exports more rewriting functions
|
|
|
|
Map to calls to monadic function assert_exp that throws an exception if the
assertion is false
|
|
|
|
|
|
|
|
(includes variables for bitvector sizes)
|
|
appear in the output
|
|
checking that the type variables visible in the output aren't
existential
|
|
|
