| Age | Commit message (Collapse) | Author |
|---|
|
Essentially all we have to do to make this work is introduce a member of
the Value type, V_attempted_read <reg>, which is returned whenever we
try to read a register value with allow_registers disabled. This defers
the failure from reading the register to the point where the register
value is used (simply because nothing knows how to deal with
V_attempted_read). However, if V_attempted_read is returned directly as
the result of evaluating an expression, then we can replace the
expression with a single direct register read. This optimises some
indirection in the ARM specification.
|
|
Should hopefully fix memory leak in RISC-V.
Also adds an optimization pass that removes copying structs and allows
some structs to simply alias each other and avoid copying their
contents. This requires knowing certain things about the lifetimes of
the structs involved, as can't free the struct if another variable is
referencing it - therefore we conservatively only apply this
optimization for variables that are lifted outside function
definitions, and should therefore never get freed until the model
exits - however this may cause issues outside ARMv8, as there may be
cases where a struct can exist within a variant type (which are not
yet subject to this lifting optimisation), that would break these
assumptions - therefore this optimisation is only enabled with the
-Oexperimental flag.
|
|
This optimisation re-uses variables if possible, rather than
allocating new ones.
|
|
Bitvectors that aren't fixed size, but can still be shown to fit
within 64-bits, now have a specialised representation. Still need to
introduce more optimized functions, as right now we mostly have to
convert them into large bitvectors to pass them into most
functions. Nevertheless, this doubles the performance of the TLBLookup
function in ARMv8.
|
|
|
|
Also fix a test with an insufficient constraint
|
|
|
|
|
|
|
|
Previously the following would fail:
```
default Order dec
$include <prelude.sail>
register V : vector(1, dec, vector(32, dec, bit))
val zeros : forall 'n, 'n >= 0. unit -> vector('n, dec, bit)
function main() : unit -> unit = {
V[0] = zeros()
}
```
Since the type-checker wouldn't see that zeros() must have type
`vector(32, dec, bit)` from the type of `V[0]`. It now tries both to
infer the expression, and use that to check the assignment, and if
that fails we infer the lexp to check the assignment. This pattern
occurs a lot in ASL, and we often had to patch zeros() to zeros(32) or
similar there.
|
|
|
|
* Previously we allowed the following bizarre syntax for a forall
quantifier on a function:
val foo(arg1: int('n), arg2: typ2) -> forall 'n, 'n >= 0. unit
this commit changes this to the more sane:
val foo forall 'n, 'n >= 2. (arg1: int('n), arg2: typ2) -> unit
Having talked about it today, we could consider adding the syntax
val foo where 'n >= 2. (arg1: int('n), arg2: typ2) -> unit
which would avoid the forall (by implicitly quantifying variables in
the constraint), and be slightly more friendly especially for
documentation purposes. Only RISC-V used this syntax, so all uses of
it there have been switched to the new style.
* Second, there is a new (somewhat experimental) syntax for
existentials, that is hopefully more readable and closer to
minisail:
val foo(x: int, y: int) -> int('m) with 'm >= 2
"type('n) with constraint" is equivalent to minisail: {'n: type | constraint}
the type variables in typ are implicitly quantified, so this is equivalent to
{'n, constraint. typ('n)}
In order to make this syntax non-ambiguous we have to use == in
constraints rather than =, but this is a good thing anyway because
the previous situation where = was type level equality and == term
level equality was confusing. Now all the type type-level and
term-level operators can be consistent. However, to avoid breaking
anything = is still allowed in non-with constraints, and produces a
deprecated warning when parsed.
|
|
This should fix the issue in cheri128
Also introduce a feature to more easily debug the C backend:
sail -dfunction Name
will pretty-print the ANF and IR representation of just the Name
function. I want to make this work for the type-checker as well, but
it's a bit hard to get that to not fire during re-writing passes right
now.
|
|
|
|
Also some pretty printer improvements
Make all the tests use the same colours for green/red/yellow
|
|
Merge C platform bits for RISC-V
|
|
Currently not enabled by default, the flag -Xconstraint_synonyms
enables them
For generating constraints in ASL parser, we want to be able to give
names to the constraints that we attach to certain variables. It's
slightly awkward right now when constraints get long complicated
because the entire constraint always has to be typed out in full
whenever it appears, and there's no way to abstract away from that.
This adds constraint synonyms, which work much like type synonyms
except for constraints, e.g.
constraint Size('n) = 'n in {1, 2, 4, 8} | 128 <= 'n <= 256
these constraints can then be used instead of the full constraint, e.g.
val f : forall 'n, where Size('n). int('n) -> unit
Unfortunatly we need to have a keyword to 'call' the constraint
synonym otherwise the grammer stops being LR(1). This could be
resolved by parsing all constraints into Parse_ast.atyp and then
de-sugaring them into constraints, which is what happens for
n-expressions already, but that would require quite a bit of work on
the parser.
To avoid this forcing changes to any other parts of Sail, the intended
invariant is that all constraints appearing anywhere in a type-checked
AST have no constraint synonyms, so they don't have to worry about
matching on NC_app, or calling Env.expand_typquant_synonyms (which
isn't even exported for this reason).
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
