| Age | Commit message (Collapse) | Author |
|---|
|
- Bitvector pattern rewriting had stopped working due to a line of code being
lost in some merge.
- Fix a bug in early return rewriting that caused returns getting pulled out of
if-statements to disappear.
- There were some variable name clashes with keywords because doc_lem_id was
not always called.
- Ast_util.is_number failed to check for "int" and "nat" built-in types,
causing pattern matching on natural number literals to fail.
|
|
Assignments of the form "(v1, v2, v3) = vector" are common in ASL. They split
the vector on the right-hand side into subvectors and assign those to the
vectors in the tuple. The new rewriting step performs this splitting and
replaces the right-hand side with the tuple of subvectors. The assignment is
then handled by an existing rewriting step for tuple assignments.
|
|
Necessary for the Lem backend if effect checking is turned off in the type
checker: the monad translation needs proper effect annotations.
|
|
Moreover, add support for pretty-printing (to Lem) vector access/update
operations for vectors with non-constant, but normalized start index.
|
|
Requires version of Lem with real number support, currently at
https://bitbucket.org/bauereiss/lem/branch/reals
|
|
With -ddump_rewrite_ast, pretty-print Sail code after each rewriting step in
addition to dumping the AST.
|
|
|
|
Also improves flow typing in assert statements for ASL parser
This patch does currently introduce a few test failures, probably due
to the new way literals are handled in case statements, which needs to
be investigated and fixed if possible.
|
|
|
|
|
|
Menhir pretty printer can now print enough sail to be useful with ASL parser
Fixity declarations are now preserved in the AST
Menhir parser now runs without the Pre-lexer
Ocaml backend now supports variant typedefs, as the machinery to
generate arbitrary instances of variant types has been added to the
-undefined_gen flag
|
|
|
|
New option -memo_z3 memoizes calls to the Z3 solver, and saves these
results between calls to sail. This greatly increases the performance
of sail when re-checking large specifications by about an order of
magnitude. For example:
time sail -no_effects prelude.sail aarch64_no_vector.sail
real 0m4.391s
user 0m0.856s
sys 0m0.464s
After running with -memo_z3 once, running again gives:
time sail -memo_z3 -no_effects prelude.sail aarch64_no_vector.sail
real 0m0.457s
user 0m0.448s
sys 0m0.008s
Both the old and the new parser should now have better error messages
where the location of the parse error is displayed visually in the
error message and highlighted.
|
|
experiments
|
|
The code for these is now rather ugly though... it needs to be cleaned up at some point
Also various improvements to new menhir parser
|
|
|
|
|
|
|
|
|
|
experiments
|
|
|
|
|
|
|
|
|
|
- Remove start indices and indexing order from bitvector types. Instead add
them as arguments to functions accessing/updating bitvectors. These arguments
are effectively implicit, thanks to wrappers in prelude_wrappers.sail and a
"sizeof" rewriting pass.
- Add a typeclass for bitvectors with a few basic functions (converting to/from
bitlists, converting to an integer, getting and setting bits). Make both
monads use this interface, so that they work with both the bitlist and the
machine word representation of bitvectors.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
also rename NC_nat_set_bounded to NC_set (it was an int set not a nat set anyway)
|
|
just LB_val in AST
also rename functions in rewriter.ml appropriately.
|
|
|
|
|
|
Also fixed basic ocaml test suite
|
|
experiments
|
|
|
|
|
|
as GPR
This was wrongly translated as an update of the vector of references.
|
|
|
|
- Modified how sail type error messages are displayed. The
typechecker, rather than immediately outputing a string has a
datatype for error types, which are the pretty-printed using a
PPrint pretty-printer. Needs more work for all the error messages.
- Error messages now attempt to highlight the part of the file where
the error occurred, by printing the line the error is on and
highlighting where the error message is in red. Again, this needs to
be made more robust, especially when the error messages span
multiple lines.
Other things
- Improved new parser and lexer. Made the lexer & parser handling of
colons simpler and more intuitive.
- Added some more typechecking test cases
|
|
|
|
experiments
|
|
|
|
|
|
- Support tuples in lexps
- Rewrite trivial sizeofs
- Rewrite early returns more aggressively
- Support let bindings with ticked variables (binding both a type-level and
term-level variable at the same time)
|
|
|
|
|
