| Age | Commit message (Collapse) | Author |
|---|
|
(involved some manual tinkering with gitignore, type_check, riscv)
|
|
|
|
We now store the location where type variables were bound, so we can
use this information when printing error messages.
Factor type errors out into type_error.ml. This means that
Type_check.check is now Type_error.check, as it previously it handled
wrapping the type_errors into reporting_basic
errors. Type_check.check' has therefore been renamed to
Type_check.check.
|
|
isabelle (but isabelle almost certainly broken)
|
|
|
|
|
|
The datatype package of HOL4 does not support the prompt monad, so this patch
restores the option to generate a model that only uses the state monad. Also
add a Makefile target cheri_sequential.lem in the cheri/ directory.
|
|
- originally based on the Lem backend
- added externs to some of the library files and tests
- added wildcard to extern valspecs in parser
- added Type_check.get_val_spec_orig to return the valspec with the
function's original names for bound type variables
Note that most of the tests will fail currently
|
|
|
|
|
|
(Preprocessed into a real record type with a fresh id and a reference
to that generated record type.)
|
|
builds this defaults to git root.
|
|
files in installed location.
|
|
definitions from sail/lib.
|
|
Turn on complex nexp rewriting for mono by default
(NB: solving is currently quite slow, will optimise)
|
|
(for monomorphisation, off for now because the analysis needs extended).
Also tighten up orig_nexp, make Lem backend replace # in type variables.
|
|
|
|
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.
|
|
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.
|
|
Makes bitvector typeclass instance dictionaries disappear from generated
Isabelle output.
|
|
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.
|
|
(and stop afterwards unless asked)
|
|
|
|
|
|
Can now use C-style include declarations to include files within other sail files. This is done in such a way that all the location information is preserved in error messages. As an example:
$include "aarch64/prelude.sail"
$define SYM
$ifndef SYM
$include <../util.sail>
$endif
would include the file aarch64/prelude.sail relative to the file where the include is contained. It then defines a symbol SYM and includes another file if it is not defined. The <../util.sail> include will be accessed relative to $SAIL_DIR/lib, so $SAIL_DIR/lib/../util.sail in this case.
This can be used with the standard C trick of
$ifndef ONCE
$define ONCE
val f : unit -> unit
$endif
so no matter how many sail files include the above file, the valspec for f will only appear once.
Currently we just have $include, $define, $ifdef and $ifndef (with $else and $endif). We're using $ rather than # because # is already used in internal identifiers, although this could be switched.
|
|
|
|
- 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.
|
|
Changed -mono-split to -mono_split to be consistent with other options
that use underscores, -mono-split still works but gives a warning
message, just so nothing breaks immediately because of this.
Removed this sil commands since they really don't do anything right
now.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
* Changed comment syntax to C-style /* */ and //
* References to registers and mutable variables are never created
implicitly - a reference to a register or variable R is now created
via the expression "ref R". References are assigned like "(*Y) = X",
with "(*ref R) = X" being equivalent to "R = X". Everything is always
explicit now, which simplifies the logic in the typechecker. There's
also now an invariant that every id directly in a LEXP is mutable,
which is actually required for our rewriter steps to be sound.
* More flexible syntax for L-expressions to better support wierd
power-idioms, some syntax sugar means that:
X.GET(a, b, c) ==> _mod_GET(X, a, b, c)
X->GET(a, b, c) ==> _mod_GET(ref X, a, b, c)
for setters, this can be combined with the (still somewhat poorly
named) LEXP_memory construct, such that:
X->SET(a, b, c) = Y ==> _mod_SET(ref X, a, b, c, Y)
Currently I use the _mod_ prefix for these 'modifier' functions, but
we could omit that a la rust.
* The register bits typedef construct no longer exists in the
typechecker. This construct never worked consistently between backends
and inc/dec vectors, and it can be easily replaced by structs with
fancy setters/getters if need be. One can also use custom type operators to mimic the syntax, i.e.
type operator ... ('n : Int) ('m : Int) = slice('n, 'm)
struct cr = {
CR0 : 32 ... 35,
/* 32 : LT; 33 : GT; 34 : EQ; 35 : SO; */
CR1 : 36 ... 39,
/* 36 : FX; 37 : FEX; 38 : VX; 39 : OX; */
CR2 : 40 ... 43,
CR3 : 44 ... 47,
CR4 : 48 ... 51,
CR5 : 52 ... 55,
CR6 : 56 ... 59,
CR7 : 60 ... 63,
}
This greatly simplifies a lot of the logic in the typechecker, as it
means that E_field is no longer ambiguously overloaded between records
and register bit typedefs. This also makes writing semantics for these
constructs much simpler.
|
|
Experimenting with porting riscv model to new typechecker
|
|
|
|
|
|
|
|
|
|
Recent patches have made the rewriter more strict about performing
type correct rewrites. This is mostly a good thing but did cause some
problems with the ocaml backend.
Currently the sizeof rewriter doesn't seem to preserve type
correctness - I suspect this is because when it resolves the sizeofs,
it generates constraints that are true, but not in a form where the
typechecker can see that they are true. I disabled the re-check after
the sizeof rewriting pass to fix this. Maybe we don't want to do this
anyway because it's slow.
Changes to function clauses with guards + monomorphisation changed how
the typechecker handles literal patterns. I added a rewriting pass to
rewrite literals to guarded equality checks, which is run before
generating ocaml.
The rewriter currently uses Env.empty in a view places. This can cause
bugs because Env.empty is a totally unitialised environment that
doesn't satisfy invariants we expect of an environment. This should be
changed to initial_env and it shouldn't be exported, I fixed a few
cases where this caused things to go wrong, but it should probably not
be exported from Type_check.ml.
|
|
|
|
steps
Parser now has syntax for mutual recusion blocks
mutual {
... fundefs ...
}
which is used for parsing and pretty printing
DEF_internal_mutrec. It's stripped away by the initial_check, so the
typechecker never sees DEF_internal_mutrec. Maybe this could change,
as forcing mutual recursion to be explicit would probably be a good
thing.
Added record syntax to the new parser
New option -dmagic_hash is similar to GHC's -XMagicHash in that it
allows for identifiers to contain the special hash character, which is
used to introduce new autogenerated variables in a way that doesn't
clash with existing names.
Option -sil compiles sail down to the intermediate language defined in
sil.ott (not complete yet).
|
|
|
|
As discussed previously, we wanted to start refactoring the re-writer
to make it a bit less monolithic, and in the future potentially break
it into separate files for backend-specific rewrites and stuff.
- rewriter.ml now contains the generic re-writing code
- rewrites.ml contains the rewriting passes themselves
It would be nice if the generic rewriting code didn't depend on the
typechecker, because then it could be used in ASL parser on untyped
code.
|
