| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Add value-only version of compute_{pat,exp}_alg to help
Experiment with adding equality constraints between type vars and args in
Coq output
|
|
1. Experiment with allowing some flow typing on mutable variables for
translating ASL in a more idiomatic way. I realise after updating some
of the test cases that this could have some problematic side effects
for lem translation, where mutable variables are translated into
monadic code. We'd need to ensure that whatever flow typing happens
for mutable variables also works for monadic code, including within
transformed loops. If this doesn't work out some of these changes may
need to be reverted.
2. Make the type inference for l-expressions a bit smarter. Splits the
type checking rules for l-expressions into a inference part and a
checking part like the other bi-directional rules. Should not be able
to type check slightly more l-expresions, such as nested vector slices
that may not have checked previously.
The l-expression rules for vector patterns should be simpler now, but
they are also more strict about bounds checking. Previously the bounds
checks were derived from the corresponding operations that would
appear on the RHS (i.e. LEXP_vector would get it's check from
vector_access). This meant that the l-expression bounds checks could
be weakend by weakening the checks on those operations. Now this is no
longer possible, there is a -no_lexp_bounds_check option which turns
of bounds checking in l-expressions. Currently this is on for the
generated ARM spec, but this should only be temporary.
3. Add a LEXP_vector_concat which mirrors P_vector_concat except in
l-expressions. Previously there was a hack that overloaded LEXP_tup
for this to translate some ASL patterns, but that was fairly
ugly. Adapt the rewriter and other parts of the code to handle
this. The rewriter for lexp tuple vector assignments is now a rewriter
for vector concat assignments.
4. Include a newly generated version of aarch64_no_vector
5. Update the Ocaml test suite to use builtins in lib/
|
|
|
|
Use non-recursive fix_eff_exp instead of recursive propagate_exp_effect,
assuming that the effects of subexpressions have already been fixed by the
recursive calls of the rewriter.
|
|
Isabelle does not like nested annotations like "((exp :: typ) :: typ)".
|
|
|
|
* Changed comment syntax to C-style /* */ and //
* References to registers and mutable variables are never created
implicitly - a reference to a register or variable R is now created
via the expression "ref R". References are assigned like "(*Y) = X",
with "(*ref R) = X" being equivalent to "R = X". Everything is always
explicit now, which simplifies the logic in the typechecker. There's
also now an invariant that every id directly in a LEXP is mutable,
which is actually required for our rewriter steps to be sound.
* More flexible syntax for L-expressions to better support wierd
power-idioms, some syntax sugar means that:
X.GET(a, b, c) ==> _mod_GET(X, a, b, c)
X->GET(a, b, c) ==> _mod_GET(ref X, a, b, c)
for setters, this can be combined with the (still somewhat poorly
named) LEXP_memory construct, such that:
X->SET(a, b, c) = Y ==> _mod_SET(ref X, a, b, c, Y)
Currently I use the _mod_ prefix for these 'modifier' functions, but
we could omit that a la rust.
* The register bits typedef construct no longer exists in the
typechecker. This construct never worked consistently between backends
and inc/dec vectors, and it can be easily replaced by structs with
fancy setters/getters if need be. One can also use custom type operators to mimic the syntax, i.e.
type operator ... ('n : Int) ('m : Int) = slice('n, 'm)
struct cr = {
CR0 : 32 ... 35,
/* 32 : LT; 33 : GT; 34 : EQ; 35 : SO; */
CR1 : 36 ... 39,
/* 36 : FX; 37 : FEX; 38 : VX; 39 : OX; */
CR2 : 40 ... 43,
CR3 : 44 ... 47,
CR4 : 48 ... 51,
CR5 : 52 ... 55,
CR6 : 56 ... 59,
CR7 : 60 ... 63,
}
This greatly simplifies a lot of the logic in the typechecker, as it
means that E_field is no longer ambiguously overloaded between records
and register bit typedefs. This also makes writing semantics for these
constructs much simpler.
|
|
|
|
|
|
Improved handling of try/catch
Better handling of unprovable constraints when the environment contains
false
|
|
Also fix bug in mono analysis with generated variables
Breaks lots of typechecking tests because it generates unnecessary
equality tests on units (and the tests don't have generic equality),
which I'll fix next.
|
|
|
|
|
|
As discussed previously, we wanted to start refactoring the re-writer
to make it a bit less monolithic, and in the future potentially break
it into separate files for backend-specific rewrites and stuff.
- rewriter.ml now contains the generic re-writing code
- rewrites.ml contains the rewriting passes themselves
It would be nice if the generic rewriting code didn't depend on the
typechecker, because then it could be used in ASL parser on untyped
code.
|
|
Alastair's test cases revealed that using regular ints causes issues
throughout sail, where all kinds of things can internally overflow in
edge cases. This either causes crashes (e.g. int_of_string fails for
big ints) or bizarre inexplicable behaviour. This patch switches the
sail AST to use big_int rather than int, and updates everything
accordingly.
This touches everything and there may be bugs where I mistranslated
things, and also n = m will still typecheck with big_ints but fail at
runtime (ocaml seems to have decided that static typing is unnecessary
for equality...), as it needs to be changed to eq_big_int.
I also got rid of the old unused ocaml backend while I was updating
things, so as to not have to fix it.
|
|
|
|
Translates atom('n) types into itself('n) types that won't be erased
Also exports more rewriting functions
|
|
|
|
|
|
|
|
|
|
With -ddump_rewrite_ast, pretty-print Sail code after each rewriting step in
addition to dumping the AST.
|
|
|
|
|
|
|
|
just LB_val in AST
also rename functions in rewriter.ml appropriately.
|
|
|
|
|
|
|
|
Implemented using the exception monad, by throwing and catching the return
value
|
|
|
|
|
|
Modified initial_check.ml so it no longer requires type_internal. It's
still needs cleaned up in a few ways. Most of the things it's trying
to do could be done nicer if we took some time to re-factor it, and
some of the things should just be handled by the main typechecker,
leaving it as a think layer between the parse_ast and the ast.
Now that's done everything can be switched to the new typechecker and
the _new suffixes were deleted from everything except the
monomorphisation pass because I don't know the status of that.
|
|
Initial typecheck still uses previous typechecker
|
|
|
|
|
|
|
|
Not working yet
|
|
TODO: add an event for a return so that rewriters can find and remove them as needed for OCaml and Lem
|
|
|
|
rewrite for-loops, if/case-expressions to return updated variables
|
|
|
|
|
|
|
|
|
|
normalise_exp exp that should transform expressions into a form where they can be embedded into monadic lem or prover definitions. Both untested
|
|
|
|
Add a new internal node for moving assignments into scope-preserving expressions that more explicitly define the scope
|
|
transformations restored :)
|
