| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
- fixed mapping of cregs to regs
- fixed interpretation of NOP
- fixed sign-extension for C.LW
- added C.LD
- fixed cut-paste errors in C.XOR, C.AND
- fixed interpretations of C.ADDW, C.SUBW
- fixed decode of C.LDSP
|
|
support for RVC in the misa.
|
|
|
|
|
|
test_cp2_rep_underflow).
|
|
|
|
overloaded accessor functions for X registers.
|
|
|
|
|
|
|
|
|
|
|
|
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)
|
|
... all 4500 lines of it.
Need to figure out how to cut out some details to make more minimal.
|
|
|
|
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)
|
|
|
|
|
|
|
|
Conversations with Alexandre/Jon indicate that a BSV generator
should be able to deal with this recursion, and Thomas has
fixed the Lem generator.
|
|
for illegal-instruction exceptions. changed to excinfo.
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
- introduce the misa register
- check the appropriate instruction bits to decide whether it is compressed
- check misa.C to decide whether we can execute compressed instructions
- add a decodeCompressed function
- add two of the most basic RVC instructions: NOP and ILLEGAL
|
|
Look deep into sub-patterns for identifiers and literals instead of relying on
assumptions about possible nestings
|
|
Make rewriter look into P_typ patterns instead of throwing them away.
|
