| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
Add a test case in test/c/eq_struct.sail. Ensure that the macro EQUAL(type) will always give a valid equality function for any
builtin type in sail.h.
|
|
Non bitvector literals for decreasing vectors were not being reversed
correctly, so the list of capability registers was effectively in
reverse order.
Added a test case to test/c/ based on this aspect of CHERI
|
|
We should test before the first iteration in case 'to' starts out as
less than 'from'.
|
|
vector_update_subrange wasn't setting its return length correctly
|
|
|
|
|
|
Necessary to prevent redundant clauses that Coq will reject
(There's still a problem if you use a variable rather than a wildcard,
see the test)
|
|
|
|
|
|
|
|
Previously the ANF->IR translation cared too much about how things
were allocated in C, so it had to constantly check whether things
needed to be allocated on the stack or heap, and generate different
cequences of IR instructions depending on either. This change removes
the ialloc IR instruction, and changes iinit and idecl so that the
code generator now generates different C for the same IR instructions
based on the variable types involved.
The next change in this vein would be to merge icopy and iconvert at
the IR level so that conversions between uint64_t and large-bitvectors
are inserted by the code generator. This would be good because it
would make the ANF->IR translation more robust to changes in the types
of variables caused by flow-typing, and optimization passes could
convert large bitvectors to uint64_t as local changes.
|
|
(still need to sort out some string stuff, though)
|
|
Fix a bug involving indentifers on the left hand side of assignment
statements not being shadowed correctly within foreach loops.
Make the different between different types of integer division
explicit in at least the C compilation for now. fdiv_int is division
rounding towards -infinity (floor). while tdiv_int is truncating
towards zero. Same for fmod_int and tmod_int.
|
|
|
|
|
|
Plus
- Complete solver support for inequalities
- Reduce exponentials in solver
|
|
It can be proved almost entirely by symbolic execution (in <15s) _if_
the right definitions are in the compset. It took a lot of interactive
stumbling about to discover that LUPDATE was missing from the standard
list compset.
|
|
The proof now gets through simulation of the first instruction of the test.
|
|
|
|
|
|
|
|
|
|
|
|
(involved some manual tinkering with gitignore, type_check, riscv)
|
|
|
|
|
|
This should fix the issue raised in commit 45554f
Adds a test loop_exception that tests throwing exceptions in loops, various looping constructs, and returning values from try/catch blocks. Also modified the test-suite to test C compiled output both with and without optimisations
|
|
Plus test case, broken builtin name
|
|
|
|
|
|
functions in mips spec in prepartion for using this file in mips prelude. Also modify tests that use this header. We should consider prefixing library builtins to avoid name clashes. overload can then be used to provide aliases if desired.
|
|
Also add an additional -Oz3 flag that uses z3 to optimize some
additional types. This is currently very experimental and doesn't
fully work yet.
|
|
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.
|
|
- Refactor the flow typing implementation in the type-checker. This
should fix an issue involving riscv_platform. Specifically it should
now work better when an if statement contains multiple conditions
combined with and/or, only some of which imply constraints at the
type level. This change also simplifies the implementation of flow
typing, and removes some obscure features that were hardly used -
specifically, flow typing could modify types, but this was fairly
obscure and doesn't seem to affect any of our specifications. More
testing is needed to ensure that this change hasn't inadvertantly
broken anything, but it does pass all our tests and continue to
typecheck arm, riscv and cheri.
- Also adds a option for generating faster undefined functions for
enum and variant types. Previously I tried to optimise away such
functions in the C backend, because they could be slow and cause
considerable uneccessary allocation, however this was error prone
and it turns out a much simpler solution is to simply make the
functions themselves much faster, at the cost of hard-coding certain
decisions about what undefined means for these types at compile tile
(which is fine for fast emulation). This almost doubles the
performance of the generated C code.
- Add a wrapper for right shift to avoid UB when shifting by 64 or
more places.
|
|
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).
|
|
|
|
Useful for partial test cases (e.g., some of the typechecking tests)
Also a bonus warning for such functions in normal use
|
|
declaration"
This reverts commit 895f868cd537277ba61dfc427fee0e288af7e226.
These are actually treated as Ints (although you could pretend they
weren't and it mostly worked).
|
|
|
|
|
|
|
|
platform build.
|
|
|
|
|
|
|
|
|
|
pass.
|
|
Also add test cases and Isabelle lemmas
|
