| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
Assigning to an uninitialized variable as the last statement in a
block is almost certainly a type, and if that occurs then the
lift_assign re-write will introduce empty blocks causing this error to
occur. Now when we see such an empty block when converting to A-normal
form we turn it into unit, and emit a warning stating that an empty
block has been found as well as the probable cause (uninitialized
variable).
|
|
Now that Jenkins is updated to a newer version of OCaml we can finally
fix some warning with more recent versions of OCaml than 4.02.3. Also
fix a Lem test case that was failing.
|
|
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.
|
|
|
|
Current pass rate is 170 out of 181. Looks like there are some issues
with rv64ua-p-lrsc.elf, rv64ua-v-lrsc.elf, and rv64uc-p-rvc.elf which
I think are caused by me not implementing parts of the RISC-V platform
correctly in C. Some of the div and mod tests also fail, which is
probably an issue with using the correct rounding.
|
|
|
|
typing
Added a regression test as c/test/downcast_fn.sail
|
|
constructors
Add a new printing function for debugging that recursively prints
constructor types.
Fix an interpreter bug when pattern matching on constructors with
tuple types.
|
|
Now all we need to do is make sure the RISC-V builtins are mapped to
the correct C functions, and RISC-V in C should work
(hopefully). We're still missing some of the functions in sail.c for
the mappings so those have to be implemented.
|
|
Allow pat_lits rewrite to map L_unit to wildcard patterns, rather than
introducing eq_unit tests as guards.
Add a fold_function and fold_funcl functions in rewriter.ml that apply
the pattern and expression algebras to top-level functions, which
means that they correctly get applied to top-level function patterns
when they are used. Currently modifying the re-writing passes to do
this introduces some bugs which needs investigated further. The
current situation is that top-level patterns and patterns elsewhere
are often treated differently because rewrite_exp doesn't (and indeed
cannot, due to how the re-writer is structured) rewrite top level
patterns.
Fix pattern completeness check for unit literals
Fix a bug in Sail->ANF transform where blocks were always annotated
with type unit incorrectly. This caused issues in pattern literal
re-writes where the guard was a block returning a boolean. A test case
for this is added as test/c/and_block.sail.
Fix a bug caused by nested polymorphic function calls and matching in
top-level patterns. Test case is test/c/tl_poly_match.sail.
Pass location info through codegen_conversion for better error
reporting
|
|
Interpreter used a re-write (vector concat removal) that is dependent
on the vector_string_to_bit_list rewriting pass. This fixes the
interpreter to work without either vector concat removal, or turning
bitstrings into vector literals like [bitzero, bitzero, bitone]. This
has the upside of reducing the number of steps the interpreter needs
for working with bitvectors so should improve interpreter performance.
We also now test all the C compilation tests behave the same using the
interpreter. Currently the real number tests fail due to limitations
of Lem's rational library (this must be fixed in Lem). This required
supporting configuration registers in the interpreter. As such the
interpreter was refactored to more cleanly process registers when
building an initial global state. The functions are also collected
into the global state, which removes the need to search for them in
the AST every time a function call happens. This should not only
improve performance, but also removes the need to pass an AST into the
interpretation functions.
|
|
|
|
This change allows the RISC-V spec to compile to C, but more testing
is needed to ensure it works correctly.
|
|
Make the C l-expression type in Sail more generic and expressive, and
refactor the generation of conversions into a seperate
codegen_conversion function, which can handle more complex cases than
the previous more ad-hoc method.
|
|
Test that basic bi-directional mappings compile correctly
Test that a minimal file importing the prelude compiles correctly
|
|
Ensure that this works even when the union types are dependent in the wrong order, before topologically sorting definitions. We do this by calling fix_variant_ctyps on all cdefs by passing a list of
prior cdefs to specialize_variants.
|
|
|
|
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.
|
|
Add new python test runner script, which allows tests to be run in
parallel before collecting the results. This makes the tests run a lot
faster, especially for the builtins and C compilation tests. Also
handles reporting errors mushc more nicely than the previous way of
doing it in shell script.
|
|
|
|
|
|
We now generate anonymous types in the correct order, but post specialisation more dependencies can occur between named types, so an additional
sorting step is needed to ensure that these happen in the correct order. In theory we could end up with circular dependencies here that don't exist
at the Sail source level, but this shouldn't occur often (or ever) in practice. I think this is fixable but it would require some code generator
changes.
|
|
lifted types
Add a test case for nested variant constructors
|
|
|
|
Especially for return expressions, which fixes a test case
|
|
|
|
|
|
- Fix ambiguities in parser.mly
- Ensure that no new identifiers are bound in or-patterns and
not-patterns, by adding a no_bindings switch to the
environment. These patterns shouldn't generate any bogus flow typing
constraints because we just pass through the original environment
without adding any possible constraints (although this does mean we
don't get any flow typing from negated numeric literals right now,
which is a TODO).
- Reformat some code to match surrounding code.
- Add a typechecking test case for not patterns
- Add a typechecking test case for or patterns
At least at the front end everything should work now, but we need to
do a little bit more to rewrite these patterns away for lem etc.
|
|
|
|
|
|
Fixes monomorphisation on files using mappings.
Also extended constant propagation to handle pattern matches on
bitvector expressions (because an earlier rewrite replaces the literals).
Also moved L_undef rewriting because monomorphisation can handle them
but not the replacement functions.
|
|
|
|
Uses previous stage to deal with (e.g.) guards.
New option -dcoq_warn_nonex tells you where all of the extra default
cases were added.
|
|
|
|
|
|
|
|
Also use zero-initialised memory. Apparently some tests access unitialised
memory, and the default behaviour of the Lem shallow embedding is to fail in
this case.
|
|
|
|
Use nondeterministic choice by default instead of a deterministic bitstream
generator in the state, which is slightly awkward to reason about, because
every use of undefined_boolS changes the state. The previous behaviour can be
implemented as Sail code, if desired.
Also add a default implementation of internal_pick that nondeterministically
chooses an element from a list.
|
|
|
|
|
|
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'.
|
