| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Breaks parsing ambiguities by removing = as an identifier in the old parser
and requiring parentheses for some expressions in the new parser
|
|
|
|
|
|
steps
Parser now has syntax for mutual recusion blocks
mutual {
... fundefs ...
}
which is used for parsing and pretty printing
DEF_internal_mutrec. It's stripped away by the initial_check, so the
typechecker never sees DEF_internal_mutrec. Maybe this could change,
as forcing mutual recursion to be explicit would probably be a good
thing.
Added record syntax to the new parser
New option -dmagic_hash is similar to GHC's -XMagicHash in that it
allows for identifiers to contain the special hash character, which is
used to introduce new autogenerated variables in a way that doesn't
clash with existing names.
Option -sil compiles sail down to the intermediate language defined in
sil.ott (not complete yet).
|
|
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.
|
|
For example,
val test = { ocaml: "test_ocaml" } : unit -> unit
will only be external for OCaml. For other backends, it will have to be
defined.
|
|
For example:
val test = { ocaml: "test_ocaml", lem: "test_lem" } : unit -> unit
val main : unit -> unit
function main () = {
test ();
}
for a backend not explicitly provided, the extern name would be simply
"test" in this case, i.e. the string version of the id.
Also fixed some bugs in the ocaml backend.
|
|
|
|
the same name between sail and the target
|
|
|
|
|
|
|
|
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.
|
|
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
|
|
|
|
|
|
|
|
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.
|
|
- 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
|
|
backed.
Ocaml doesn't support undefined values, so we need a way to remove
them from the specification in order to generate good ocaml
code. There are more subtle issues to - like if we initialize a
mutable variable with an undefined list, then the ocaml runtime has no
way of telling what it's length should be (as this information is
removed by the simple_types pass).
We therefore rewrite undefined literals with calls to functions that
create undefined types, e.g.
(bool) undefined becomes undefined_bool ()
(vector<'n,'m,dec,bit>) undefined becomes undefined_vector(sizeof 'n, sizeof 'm, undefined_bit ())
We therefore have to generate undefined_X functions for any user
defined datatype X. initial_check seems to be the logical place for
this. This is straightforward provided the user defined types are
not-recursive (and it shouldn't be too bad even if they are).
|
|
The reason you want this is to do something like (note new parser only):
*********
default Order dec
type bits 'n:Int = vector('n - 1, 'n, dec, bit)
val zeros : forall 'n. atom('n) -> bits('n)
val decode : bool -> unit
function decode b = {
let 'datasize: {|32, 64|} = if b then 32 else 64;
let imm: bits('datasize) = zeros(datasize);
()
}
*********
for the ASL decode functions, where the typechecker now knows that the
datasize variable and the length of imm are the same.
|
|
|
|
operators.
|
|
|
|
|
|
Added a copy of the current parser/lexer in parser2.mly and
lexer2.mll. They can be used with the -new_parser flag. Currently they
are just copies of the existing files.
|
