sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2018-01-24	Have some simple sail programs compiling to C	Alasdair Armstrong

2018-01-18	Clean up command line options slightly	Alasdair Armstrong
	Changed -mono-split to -mono_split to be consistent with other options that use underscores, -mono-split still works but gives a warning message, just so nothing breaks immediately because of this. Removed this sil commands since they really don't do anything right now.
2018-01-05	Fix duplicate definitions created by merge	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.
2017-12-15	Experimenting with interactive mode	Alasdair Armstrong

2017-12-05	Update license headers for Sail source	Alasdair Armstrong

2017-11-30	Improvements to enable parsing and checking intermediate rewriting	Alasdair Armstrong
	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).
2017-11-27	Split rewriter into separate rewriting library and rewrite passes	Alasdair Armstrong
	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.