sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2018-02-16	Can now compile aarch64/duopod to C	Alasdair Armstrong
	Goes through the C compiler without any errors, but as we still don't have all the requisite builtins it won't actually produce an executable. There are still a few things that don't work properly, such as vectors of non-bit types - but once those are fixed and the Sail library is implemented fully it should work.
2018-02-15	Update duopod spec so it has no address translation	Alasdair Armstrong
	Also update the main aarch64 (no_vector) spec with latest asl_parser
2018-02-12	Add support for top-level letbindings to C backend	Alasdair Armstrong

2018-02-02	Add aarch64 duopod...	Alasdair Armstrong
	... all 4500 lines of it. Need to figure out how to cut out some details to make more minimal.
2018-02-01	More work on C compilation	Alasdair Armstrong
	Can now compile things like early returns. The same approach should work for exception handling as well. Once that's in place, just need to work a bit more on getting union types to work + the library of builtins, then we should be able to compile and run some of our specs via C. Also added some documentation in comments for the general approach taken when compiling (need many more though).
2018-01-31	Add wrappers around Lem operators using bitvector type class	Thomas Bauereiss
	Makes bitvector typeclass instance dictionaries disappear from generated Isabelle output.
2018-01-30	Fix failing Lem tests	Alasdair Armstrong

2018-01-26	Fixed loading ARM elf files	Alasdair Armstrong
	Also refactored the hand written ARM prelude and pulled out some common functionality into files in sail/lib
2018-01-23	Added additional tests, and fixed ocaml build of ARM tests	Alasdair Armstrong

2018-01-22	Update Lem shallow embedding to Sail2	Thomas Bauereiss
	- Remove vector start indices - Library refactoring: Definitions in sail_operators.lem now use Bitvector type class and work for both bit list and machine word representations - Add Lem bindings to AArch64 and RISC-V preludes TODO: Merge specialised machine word operations from sail_operators_mwords into sail_operators.
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-18	Modified ocaml backend to use ocamlfind for linksem and lem	Alasdair Armstrong
	Fixed test cases for ocaml backend and interpreter
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-17	Add generated ARM spec and test cases for it	Alasdair Armstrong
	We add the generated ARM no_vector spec from the public v8.3 XML release, mostly so that we can add end-to-end test cases for sail using it. This kind of large example is very useful for thoroughly testing the sail compiler and interpreter.