| Age | Commit message (Collapse) | Author |
|---|
|
|
|
should be kept in normal form i.e. a positive mpz_t with no bits higher than len set.
|
|
|
|
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).
|
|
First, the specialisation of option types has been fixed by allowing
the specialisation of constructor return types - this essentially
means that a constructor, such as Some : 'a -> option('a) can get
specialised to int -> option(int), rather than int -> option('a). This
means that these constructors are treated like GADTs internally. Since
this only happens just before the C translation, I haven't put much
effort into making this very robust so far.
Second, there was a bug in C compilation for the typing of return
expressions in non-unit contexts, which has been fixed.
Finally support for vector literals that are non-bitvectors has been
added.
|
|
Fixed an issue whereby an option constructor that was never
constructed, but only matched on, would cause compilation to
fail. Temporarily fixed an issue where union types that can be
entirely stack-allocated were not being treated as such, by simply
heap-allocating all unions. Need to adapt the code generator to handle
this case properly. Fixed a further small issue whereby multiple union
types would confuse the type specialisation pass.
Added a test case for compiling option types.
RISCV now generates C code, but there are still some bugs that need to
be squashed before it compile and work.
|
|
Add a flag to Sail that allows for an image of an elf file to be
dumped in a simple format using linksem, used as
sail -elf test.elf -o test.bin
This image file can then be used by a compiled C version of a sail
spec as with ocaml simply by
./a.out test.bin
|
