| Age | Commit message (Collapse) | Author |
|---|
|
Also, to support this,
constant propagation for integer multiply,
fix substitution of concrete values for nvars,
size parameters in single argument functions,
fix kind for itself,
add eq_atom to prelude
|
|
|
|
|
|
Breaks parsing ambiguities by removing = as an identifier in the old parser
and requiring parentheses for some expressions in the new parser
|
|
Broke analysis a little
|
|
|
|
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.
|
|
|
|
- Add support for some internal nodes to type checker
- Add more explicit type annotations during rewriting
- Remove hardcoded rewrites for E_vector_update etc from Lem pretty-printer;
these will be resolved by the type checker during rewriting now
|
|
|
|
|
|
Also some simple rules to try to format if statements better based on
contents while pretty printing.
|
|
|
|
|
|
|
|
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).
|
|
|
|
|
|
|
|
|
|
|
|
aarch64 vector instructions.
There's maybe a better more general way to do this but I'm not sure
what that would be.
|
|
|
|
|
|
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.
|
|
|
|
experiments
|
|
and_bool and or_bool now are treated specially in the ocaml backend,
so that they have the correct short-circuiting behaviour. This is
required so that assertions don't fail for the ARM spec for predicates
that shouldn't be tested in certain circumstances, for example things like:
IsAArch32() && AArch32_specific_predicate
Also fixed an issue in the sail library for ocaml where greater than
or equal to was being mapped to greater than.
|
|
|
|
|
|
(mostly to make test cases easier)
|
|
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.
|
|
|
|
Use overloading to find eq/neq
Track range/atom split
Missing type expansion
|
|
experiments
|
|
This bug manifested as the ARM example elf executable printing the
wrong characters... but otherwise doing not failing and exiting
cleanly. It didn't trigger the test suite at all. I tracked it down to
this line using git-bisect, and while returning nc_true is a bit
suspect I'm still not 100% sure how this caused such a subtle and
annoying bug in the generated ocaml code - it took several hours to
track down the breakage to this line.
|
|
|
|
|
|
|
|
|
|
|
|
Instruction extractor code that I commented out in this commit seems
buggy anyway - it will claim that the length of all bitvectors is 64?!
|
|
Need to map sail type annotations to interpreter type annotations in lem_ast ouput. This doesn't seem too hard.
|
|
numbers below 129
|
|
This is the first step towards getting the interpreter working on this branch
|
|
|
|
Now constraints on type constructors are checked correctly when
checking that types are well formed using Env.wf_typ. The arity and
kind of type constructor arguments are also checked in the same way.
Also some general cleanups to the type checker code, with some
auxillary functions being moved to more appropriate files.
|
|
|
|
|
|
|
