| Age | Commit message (Collapse) | Author |
|---|
|
and tests.
|
|
|
|
This is now split into instructions, regs, memory and platform, each
controlled individually. Currently all are enabled and not connected to
any command-line options, so a recompile is needed for trace tuning.
|
|
Uses new primop 'string_take' which is much easier to implement in e.g. C
|
|
|
|
I got bored of this so I wrote a Python script to generate all of them
between 1 and 33, plus 48 and 64. It's in a comment.
We should really get around to making the typechecker work with
polymorphic mappings...
|
|
|
|
|
|
|
|
Revert a change to string_of_bits because it broke all the RISC-V
tests in OCaml. string_of_int (int_of_string x) is not valid because x may not
fit within an integer.
|
|
|
|
|
|
Add some builtins to the C sail lib.
Enable some gcc warnings.
|
|
|
|
- Fill in Coq builtins for more of the RISC-V prelude
- Update Barriers
- More general autocast
- Temporary sub_nat definition (until the backend handles nat better)
- Patch to bring results into a reasonable state
- Use Let rather than Definition for non-dependent top-level values
|
|
|
|
|
|
Note that constraints have been added to ensure that all bitvector types
are inhabited.
|
|
|
|
|
|
|
|
|
|
(involved some manual tinkering with gitignore, type_check, riscv)
|
|
Also fixes to C backend for compiling MIPS spec to C
- Fix an issue with const correctness in internal_vector_update
functions generated by C backend
- Add builtins for MIPS to sail.h
- Fix an issue where reg_deref didn't work when called on pointers to
large bitvectors, i.e. vectors containing references to large
bitfields as in the MIPS TLB code
- Various bug fixes and changes for running U-boot on ARM model,
including for interpreter and OCaml compilation.
- Fix memory leak issues and incorrect shadowing for foreach loops
- Update C header file. Fixes memory leak in memory read/write
builtins.
- Add aux constructor to ANF representation to hold environment
information.
- Fix undefined behavior caused by optimisation left shifting uint64_t
vectors 64 or more times. Unfortunately there's more issues because
the same happens for X >> 64 right shifts. It would make sense for
this to be zero, because that would guarantee the property that ((X
>> n) >> m) == (X >> (n + m)) but we probably need to do (X >> (n -
1) >> 1) in the optimisation to ensure that we don't cause
UB. Shifting by 63 and then by 1 is well-defined, but shifting by 64
in one go isn't according to the C standard. This issue with
right-shifts only occurs for zero-length vectors, so it's not a huge
deal, but it's still annoying.
- Add versions of print_bits and print_int that print to
stderr. Follows OCaml convention of print/prerr. Should make things
more explicit. Different backends had different ideas about where
print should output to, not every backend needs to have this
(e.g. theorem prover backends don't need to print) but having both
stderr and stdout seperate and clear is useful for executable models
(UART needs to be stdout, debug messages should be stderr).
|
|
|
|
build until we add suitable platform definitions/stubs.
The platform bits are not yet hooked into the model, but only into the build, so are untested.
|
|
|
|
isabelle (but isabelle almost certainly broken)
|
|
|
|
|
|
Found bugs by running CHERI test suite on Isabelle-exported model: signed
less-than for bit lists was missing negations for the two's complement, and
unsigned less-than compared the reverse lists.
Since all other backends implement this in Sail, it seems best to just remove
this code.
Also add support for infix operators to Lem backend, by z-encoding their
identifiers like the other backends do.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
and riscv_types.
Also remove an unused break().
|
|
Can now compile RISCV. Requires some library tweaks before it'll pass any tests,
Also adds hyperlinks to wip latex output
|
|
Some functions are partial, e.g. converting a bitvector to an integer, which
might fail for the bit list representation due to undefined bits. Undefined
cases can be handled in different ways:
- call Lem's failwith, which maps to undefined/ARB in Isabelle and HOL (the
default so far),
- return an option type,
- raise a failure in the monad, or
- use a bitstream oracle to resolve undefined bits.
This patch adds different versions of partial functions corresponding to those
options. The desired behaviour can be selected by choosing a binding in the
Sail prelude. The naming scheme is that the failwith version is the default,
while the other versions have the suffixes _maybe, _fail, and _oracle,
respectively.
|
|
Also work on making C backend compile RISC-V
|
|
Previously union types could have no-argument constructors, for
example the option type was previously:
union option ('a : Type) = {
Some : 'a,
None
}
Now every union constructor must have a type, so option becomes:
union option ('a : Type) = {
Some : 'a,
None : unit
}
The reason for this is because previously these two different types of
constructors where very different in the AST, constructors with
arguments were used the E_app AST node, and no-argument constructors
used the E_id node. This was particularly awkward, because it meant
that E_id nodes could have polymorphic types, i.e. every E_id node
that was also a union constructor had to be annotated with a type
quantifier, in constrast with all other identifiers that have
unquantified types. This became an issue when monomorphising types,
because the machinery for figuring out function instantiations can't
be applied to identifier nodes. The same story occurs in patterns,
where previously unions were split across P_id and P_app nodes - now
the P_app node alone is used solely for unions.
This is a breaking change because it changes the syntax for union
constructors - where as previously option was matched as:
function is_none opt = match opt {
Some(_) => false,
None => true
}
it is now matched as
function is_none opt = match opt {
Some(_) => false,
None() => true
}
note that constructor() is syntactic sugar for constructor(()), i.e. a
one argument constructor with unit as it's value. This is exactly the
same as for functions where a unit-function can be called as f() and
not as f(()). (This commit also makes exit() work consistently in the
same way) An attempt to pattern match a variable with the same name as
a union-constructor now gives an error as a way to guard against
mistakes made because of this change.
There is probably an argument for supporting the old syntax via some
syntactic sugar, as it is slightly prettier that way, but for now I
have chosen to keep the implementation as simple as possible.
The RISCV spec, ARM spec, and tests have been updated to account for
this change. Furthermore the option type can now be included from
$SAIL_DIR/lib/ using
$include <option.sail>
|
|
|
|
|
|
passing tests.
|
|
Makes bitvector typeclass instance dictionaries disappear from generated
Isabelle output.
|
|
|
