| Age | Commit message (Collapse) | Author |
|---|
|
Isabelle does not like nested annotations like "((exp :: typ) :: typ)".
|
|
|
|
Turns out the __TakeColdReset function is actually in the v8.3 XML. I
went and looked for it, and it's there, it just wasn't being picked up
by ASL parser because it's not called from any instructions. I added a
new field to the json config files for ASL parser that can tell it
about any such special functions that it should guarantee to include.
Also fixed a bug in C loop compilation
|
|
Goes through the C compiler without any errors, but as we still don't
have all the requisite builtins it won't actually produce an
executable. There are still a few things that don't work properly,
such as vectors of non-bit types - but once those are fixed and the
Sail library is implemented fully it should work.
|
|
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.
|
|
|
|
Also update the main aarch64 (no_vector) spec with latest asl_parser
|
|
|
|
|
|
|
|
|
|
Useful for feature functions, e.g. HaveFP16Ext
|
|
|
|
Solves a problem where generated kids crept into type annotations during
rewriting and caused later typechecking passes to fail.
|
|
(still some work to do in AtomToItself rewrite, but should work despite
error messages)
|
|
|
|
|
|
Describes precisely the intermediate representation used in the C
backend in an ott grammar, and also removes several C-isms where raw C
code was inserted into the IR, so in theory this IR could be
interpreted by a small VM/interpreter or compiled to LLVM bytecode
etc. Currently the I_raw constructor for inserting C code is just used
for inserting GCC attributes, so it can safely be ignored.
Also augment and refactor the instruction type with an aux constructor
so location information can be propagated down to this level.
|
|
Option -ddump_flow_graphs when used with -c will create graphviz files
for each function in the specification with control and data
dependencies shown.
|
|
|
|
to help Lem go from a general type `bits('n)` to a specific type `bits(16)`
at a case split, and the other way around for a returned value.
Doesn't handle function clause patterns yet
|
|
Turn of warnings so we don't get warnings for generated code, this fixes the false-positive warnings in the riscv test suite. Also use basename in test/riscv/run_tests.sh to not print long paths
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Make destructuring existentials less arcane by allowing them to be destructured via type patterns (typ_pat in ast.ml). This allows the following code for example:
val mk_square : unit -> {'n 'm, 'n = 'm. vector('n, dec, vector('m, dec, bit))}
function test (() : unit) -> unit = {
let matrix as vector('width, _, 'height) = mk_square ();
_prove(constraint('width = 'height));
()
}
where 'width we become 'n from mk_square, and 'height becomes 'm. The old syntax
let vector as 'length = ...
or even
let 'vector = ...
still works under this new scheme in a uniform way, so this is backwards compatible
The way this works is when a kind identifier in a type pattern is bound against a type, e.g. 'height being bound against vector('m, dec, bit) in the example, then we get a constraint that 'height is equal to the first and only n-expression in the type, in this case 'm. If the type has two or more n-expressions (or zero) then this is a type error.
|
|
|
|
|
|
This was technically allowed previously but the rules for type
variable names in function types were too strict so it didn't work.
Also fixed a bug where Nexp_app constructors were never considered identical
and fixed a bug where top-level let bindings got annotated with the
wrong environment
|
|
passing tests.
|
|
|
|
|
|
if necessary
|
|
(otherwise wildcard cases won't be cut short at the assertion)
|
|
Wanted to know yesterday if possible to parameterise specification by 32/64 bits in context of RISCV - i.e. can we do something like
let size = 32
type xlen = bits(size)
This patch tweaks the typechecker slightly to allow type variables to be introduced by global let bindings in the same way they can be introduced by local let bindings (techically this was always allowed, but some bugs prevented it from really working), so
let 'size : atom(32) = 32
means we have a global type variable 'size, with a global constraint 'size = 32
We can go further though...
let 'size : {|32, 64|} = 32
means we have a global type variable 'size with a constraint 'size = 32 | 'size = 64, in this case the specification will only typecheck if the specification is correct for BOTH 'size = 32 and 'size = 64. This also creates a global binding size (note no tick) with value 32 and type atom('size), one can also do
let _ as 'size : {|32, 64|} = 32
which won't create the binding, only the type variable.
These global type variables are bound to not be very well understood by certain parts of sail, so typical here be dragons warning etc.
|
|
Can now compile things like early returns. The same approach should
work for exception handling as well. Once that's in place, just need
to work a bit more on getting union types to work + the library of
builtins, then we should be able to compile and run some of our specs
via C. Also added some documentation in comments for the general
approach taken when compiling (need many more though).
|
|
|
|
(preventing non-monomorphised sizes appearing in wildcard cases)
|
|
|
|
|
|
|
|
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.
|
|
Currently the fix is to disallow this shadowing entirely, because it
seems to cause trouble for ocaml.
|
|
|
|
|
