| Age | Commit message (Collapse) | Author |
|---|
|
This is for a bug I encountered while moving some docs over from the ISA
spec into sail documentation comments.
|
|
|
|
|
|
|
|
and tests.
|
|
Some of the output from the tests scripts is odd on Jenkins, try to
fix this by flushing stdout more regularly in the test scripts
|
|
|
|
Test the builtin functions by compiling them to C, OCaml, and OCaml
via Lem. Split up some of the longer builtin test programs to avoid
stack overflows when compiling to OCaml, as 3000+ line long blocks can
cause issues with some re-writing steps.
Also test constant-folding with builtins (this should reduce the
asserts in these files to assert true), and also test constant folding
with the C compilation.
Fix a bug whereby vectors with heap-allocated elements were not
initialized correctly.
Fix a bug caused by compiling and optimising empty vector literals.
Fix an OCaml test case that broke due to the ref type being used. Now
uses references to registers.
Fix a bug where Sail would output big integers that lem can't
parse. Checks if integer is between Int32.min_int and Int32.max_int
and if not, use integerOfString to represent the integer. Really this
should be fixed in Lem.
Make the python test runner script the default for testing builtins
and running the C compilation tests in test/run_tests.sh
Add a ocaml_build_dir option that sets a custom build directory for
OCaml. This is needed for running OCaml tests in parallel so the
builds don't clobber one another.
|
|
- 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.
|
|
Added library for simple integer arithmetic functions in lib/arith.sail
WIP TeX file for formatting latex output included in lib/sail.tex
Fixes for bugs in sail_lib
|
|
|
|
|
|
Uses the typechecker tests for now. Also fix two minor bugs in pretty-printer
and rewriter uncovered by the tests.
|
|
|
|
We add the generated ARM no_vector spec from the public v8.3 XML
release, mostly so that we can add end-to-end test cases for sail
using it. This kind of large example is very useful for thoroughly
testing the sail compiler and interpreter.
|
|
|
|
Now constraints on type constructors are checked correctly when
checking that types are well formed using Env.wf_typ. The arity and
kind of type constructor arguments are also checked in the same way.
Also some general cleanups to the type checker code, with some
auxillary functions being moved to more appropriate files.
|
|
|
