| Age | Commit message (Collapse) | Author |
|---|
|
the generated pattern so re-typechecking works
|
|
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...
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
In particular, the complicated "what nexps are in scope" test can be
replaced by a simple "are the nvars in scope" check.
|
|
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.
|
|
|
|
Also allow options to be set via a pragma in Sail files
|
|
|
|
|
|
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.
|
|
|
|
Particularly useful when execute has been split up (e.g., on RISC-V).
Only enabled on Coq for now.
|
|
|
|
Also required some solver fixes:
- make sure that ArithFacts are always cleared to avoid loops
- extract_properties should do the goal first because it might add extra
work to do in the hypotheses
- unfolding should come before extract_properties
|
|
constructed when a function call, cast, or binder demands them, removing
some ambiguous corner cases.
Also
- Don't simplify nexps before printing (note that we usually end up
needing a (8 * x) / 8 lemma as a result)
- More extraction of properties in the goal
- Splitting of conditionals/matches in goals (which can occur more often
because of the new positions of build_ex in definitions)
- Try simple solving first to improve speed / reduce proof sizes / help
fill in metavariables (because manipulating the goal can interfere with
instantiating them)
- Update RISC-V patch
|
|
and use the original ids rather than fresh ones; both to allow referring to matched ids in guards
|
|
|
|
|
|
|
|
|
|
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
|
|
unnecessary problems with mappings/pat_to_exp
|
|
|
|
|
|
guards
|
|
exp_of_mpat
|
|
cleaner generated code and reduced compiler warnings
|
|
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.
|
|
an explicit rewrite step in Rewrites, just before pat_lits
|
|
|
|
generated id pattern"
This reverts commit 9fdd1ecbed32ebb408256628b6661ccbf5f16c18.
|
|
pattern
|
|
This change allows the RISC-V spec to compile to C, but more testing
is needed to ensure it works correctly.
|
