sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2018-01-24	More work on experimental C backend	Alasdair Armstrong

2018-01-23	Started working on C backend for sail	Alasdair Armstrong
	Also updated some of the documentation in the sail source code
2018-01-22	Added rewriter that specializes all function calls in a specification.	Alasdair Armstrong
	This removes all type polymorphism, so we can generate optimized bitvector code and compile to languages without parametric polymorphism.
2018-01-18	Modified unification so Type_check.instantiation_of works after sizeof rewriting	Alasdair Armstrong
	This change allows the AST to be type-checked after sizeof re-writing. It modifies the unification algorithm to better support checking multiplication in constraints, by using division and modulus SMT operators if they are defined. Also made sure the typechecker doesn't re-introduce E_constraint nodes, otherwise re-checking after sizeof-rewriting will re-introduce constraint nodes.
2018-01-16	Test the ocaml interpreter with the same tests as the ocaml compilation	Alasdair Armstrong

2018-01-16	Created version of typecheck test suite for sail2 branch	Alasdair Armstrong
	Currently doesn't try to compile to lem or use the MIPS spec All the failing tests have been removed because I intend to handle them differently - they were very fragile before because there was no indication of why they failed, so as sail evolved they tended to start failing for the wrong reasons and not testing what they were supposed to.
2018-01-15	Add help to interactive mode, and load files incrementally	Alasdair Armstrong

2018-01-15	Refactored and improved ocaml interpreter	Alasdair Armstrong

2018-01-12	OCaml interactive mode can now run full aarch64 examples, and ocaml test cases.	Alasdair Armstrong

2018-01-11	Ocaml semantics can now run aarch64 hello world example using octapod	Alasdair Armstrong
	New testcase for bitfield syntax Updated to work with latest lem and linksem
2018-01-05	Moved parser, lexer and pretty printer to correct locations.	Alasdair Armstrong

2018-01-05	Merge remote-tracking branch 'origin/interactive' into vector	Alasdair Armstrong

2018-01-03	Lots of experimental changes on this branch	Alasdair Armstrong
	* 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.
2018-01-03	Updates to interpreter	Alasdair Armstrong
	Experimenting with porting riscv model to new typechecker
2017-12-15	Experimenting with interactive mode	Alasdair Armstrong

2017-12-14	An experimental version of sail without bitvector start indexes.	Alasdair Armstrong
	Works with the vector branch of asl_parser
2017-12-11	Allow stepping through code when evaluating	Alasdair Armstrong

2017-12-11	Prototype interactive mode for sail.	Alasdair Armstrong
	Requires linenoise library (opam install linenoise) for readline support. Use 'make isail' to build sail with interactive support. Plain 'make sail' should work as before with no additional dependencies. Use 'sail -i <commands>' to run sail interactively, e.g. sail -new_parser -i test/ocaml/prelude.sail test/ocaml/trycatch/tc.sail then try some commands for typechecking and evaluation sail> :t main sail> main () Doesn't use the lem interpreter right now, instead has a small operational semantics in src/interpreter.ml, but this is not very complete and will be changed/removed.