summaryrefslogtreecommitdiff
path: root/aarch64/Makefile
AgeCommit message (Collapse)Author
2018-12-20Fix monomorpisation tests with typechecker changesAlasdair Armstrong
Add an extra argument for Type_check.prove for the location of the prove call (as prove __POS__) to help debug SMT related issues
2018-11-30Parser tweaks and fixesAlasdair Armstrong
- Completely remove the nexp = nexp syntax in favour of nexp == nexp. All our existing specs have already switched over. As part of this fix every test that used the old syntax, and update the generated aarch64 specs - Remove the `type when constraint` syntax. It just makes changing the parser in any way really awkward. - Change the syntax for declaring new types with multiple type parameters from: type foo('a : Type) ('n : Int), constraint = ... to type foo('a: Type, 'n: Int), constraint = ... This makes type declarations mimic function declarations, and makes the syntax for declaring types match the syntax for using types, as foo is used as foo(type, nexp). None of our specifications use types with multiple type parameters so this change doesn't actually break anything, other than some tests. The brackets around the type parameters are now mandatory. - Experiment with splitting Type/Order type parameters from Int type parameters in the parser. Currently in a type bar(x, y, z) all of x, y, and z could be either numeric expressions, orders, or types. This means that in the parser we are severely restricted in what we can parse in numeric expressions because everything has to be parseable as a type (atyp) - it also means we can't introduce boolean type variables/expressions or other minisail features (like removing ticks from type variables!) because we are heavily constrained by what we can parse unambigiously due to how these different type parameters can be mixed and interleaved. There is now experimental syntax: vector::<'o, 'a>('n) <--> vector('n, 'o, 'a) which splits the type argument list into two between Type/Order-polymorphic arguments and Int-polymorphic arguments. The exact choice of delimiters isn't set in stone - ::< and > match generics in Rust. The obvious choices of < and > / [ and ] are ambigious in various ways. Using this syntax right now triggers a warning. - Fix undefined behaviour in C compilation when concatenating a 0-length vector with a 64-length vector.
2018-08-28Adapt theory imports for Isabelle 2018Thomas Bauereiss
Requires a recent Lem version that supports generating session-qualified imports, e.g. revision rems-project/lem@d92b077f1781765a65082c815ff363ef79499860
2018-06-11More efficient bitfield implementationAlasdair Armstrong
2018-06-07Add a constant folding optimization passAlasdair
2018-06-06Factor utility functions for IR into separate file and struct update ↵Alasdair Armstrong
optimizations. Move the utility functions for graph generation and pretty printing of intermediate representation instructions into a separate file, bytecode_util.ml, by analogy with ast_util.ml. Add an optimization pass that searches for specific patterns of struct updates and removes uncessary copying of the structs involved. With this optimisation pass the time taken for u-boot to run approx 57,000,000 instructions goes down from about 11-12 minutes to 8 minutes (about 120,000 IPS).
2018-06-06Some additional fixes to C backend. Re-enable primitive optimizations.Alasdair Armstrong
Also add an additional -Oz3 flag that uses z3 to optimize some additional types. This is currently very experimental and doesn't fully work yet.
2018-06-04Fix bug with function return types in C backendAlasdair Armstrong
2018-05-09add loc for arm full.Robert Norton
2018-05-09Add tests for Isabelle->OCaml generation for CHERI and AArch64Thomas Bauereiss