| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Also uncovered a few other issues w.r.t lists
|
|
|
|
This allows read_mem and read_reg effects to be handled by GDB
|
|
|
|
recursive.
|
|
slight performance improvement and keeps compatibility with smt backend that already had a builtin for this because it can't handle the loop in the sail version. Will need implementations for prover backends.
|
|
|
|
|
|
this is implemented in lib/vector_dec.sail as sail function that calls not_vec on sail_zeros.
|
|
Only change that should be needed for 99.9% of uses is to change
vector('n, 'ord, bit) to bitvector('n, 'ord), and adding
$ifndef FEATURE_BITVECTOR_TYPE
type bitvector('n, dec) = vector('n, dec, bit)
$endif
for to support any Sail before this
Currently I have all C, Typechecking, and SMT tests passing, as well
as the RISC-V spec building OCaml and C completely unmodified.
|
|
|
|
* Includes adding support for bitlist-Lem
* Adds new command-line option -Ofast_undefined
|
|
|
|
inconsistent with ocaml etc.). Rename div and mod builtins to ediv_int/emod_int and tdiv_int/tmod_int and add corresponding implementations. Add a test with negative operands. This will break existing models but will mean users have to think about which versions they want and won't accidentally use the wrong one.
|
|
|
|
RISC-V
|
|
bool_of_bit and bit_of_bool in sail_lib
|
|
|
|
|
|
|
|
Uses new primop 'string_take' which is much easier to implement in e.g. C
|
|
|
|
|
|
(aimed at RISC-V)
|
|
|
|
than binary
|
|
|
|
int_of_string
This fixes e.g. problems with 64-bit bitmask immediates in ARM assembly.
|
|
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...
|
|
|
|
C: Don't print usage message and quit when called with no arguments,
as this is used for testing C output
OCaml: Fix generation of datatypes with multiple type arguments
OCaml: Generate P_cons pattern correctly
C: Fix constant propagation to not propagate letbindings with type
annotations. This behaviour could cause type errors due to how type
variables are introduced. Now we only propagate letbindings when the
type of the propagated variable is guaranteed to be the same as the
inferred type of the binding.
Tests: Add OCaml tests to the C end-to-end tests (which really
shouldn't be in test/c/ any more, something like test/compile might be
better). Currently some issues with reals there like interpreter.
Tests: Rename list.sail -> list_test.sail because ocaml doesn't want
to compile files called list.ml.
|
|
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 additional well-formedness check when calling typing rules
|
|
|
|
This makes it consistent with the C backend, and also makes it easier to compare traces across execution re-runs.
|
|
|
|
|
|
|
|
|
|
|
|
(involved some manual tinkering with gitignore, type_check, riscv)
|
|
solves a problem where the Hashtbl module was encountering a stack overflow booting CheriBSD. There seems to be little or no performance impact.
|
|
|
|
Looks like Jenkins is still on OCaml 4.02.3. We should probably upgrade to 4.05 at some point.
|
|
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).
|
|
|
|
(<5% on a simple test) but dramatically reduces memory usage compared to having a hash table entry per byte!
|
|
|
