sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2017-08-29	Make Lem export of CHERI(-256) typecheck	Thomas Bauereiss
	Note: The effect annotations of the execute function differ between CHERI and MIPS, so I split out a new file mips_ast_decl.sail for MIPS with just the initial declarations of ast, decode, and execute (with the right effects for MIPS).
2017-08-24	Use relative path in Makefile	Thomas Bauereiss

2017-08-24	Fix some bugs related to the CHERI spec	Thomas Bauereiss
	- Correctly pass exponentials to Z3 - Infer types of functional record updates - Support "def Nat"
2017-07-21	Everything moved to new typechecker	Alasdair Armstrong
	Modified initial_check.ml so it no longer requires type_internal. It's still needs cleaned up in a few ways. Most of the things it's trying to do could be done nicer if we took some time to re-factor it, and some of the things should just be handled by the main typechecker, leaving it as a think layer between the parse_ast and the ast. Now that's done everything can be switched to the new typechecker and the _new suffixes were deleted from everything except the monomorphisation pass because I don't know the status of that.
2017-06-29	Ocamlbuild targets should always be remade	Brian Campbell

2017-05-10	Build Cheri_embed_types.thy together with Cheri_embed_sequential.thy	Thomas Bauereiss

2017-05-08	add make rules to (attempt to) build arm and power ml.	Robert Norton

2017-04-25	Add support for uart terminal. Also add read_bit_reg function for faster and ↵	Robert Norton
	neater access to registers of single bit.
2017-04-21	it turns out zarith has a function for printing big_ints in hex. Remove the ↵	Robert Norton
	dependency on ocaml uint library by using it.
2017-04-21	add make variable for setting ocaml compilation options (e.g. set to -p to ↵	Robert Norton
	enable gprof profiling)
2017-04-20	remove unnecessary lemlib include in compile.	Robert Norton

2017-04-20	add support for cheri128 ocaml shallow embedding	Robert Norton

2017-04-20	build a single run_embed.native with mips and cheri models linked and choose ↵	Robert Norton
	between them using a command line switch.
2017-04-06	add support for address translation and exit handling in mips ocaml shallow ↵	Robert Norton
	embedding test setup.
2017-03-24	Checkpoint work-in-progress mips sequential interpreter using ocaml shallow ↵	Robert Norton
	embedding.
2017-02-03	replace bit vector return types in getCapX functions with equivalent integer ↵	Robert Norton
	range types. This removes quite a few uses of unsigned() in cheri intsruction pseudocode. Could potentially take things furter.
2017-02-03	fix headers	Peter Sewell

2017-01-25	merge cheri 256 and 128 together factoring out differing parts into separate ↵	Robert Norton
	cheri_prelude files.
2017-01-24	first pass at cheri128 sail.	Robert Norton

2016-12-12	cheri sail export progress	Christopher Pulte

2016-12-08	add target for building cheri_notlb.lem	Robert Norton

2016-11-28	make sail produce prompt and state version of shallow embedding files at the ↵	Christopher Pulte
	same time with the types both have in common factored out into separate file, rename one mips shallow embedding _extras file as required by this
2016-11-23	Make type checker not run to fix point on resolving case-split type ↵	Kathy Gray
	variables; modern implementation of nexp unification seems not to need it
2016-11-22	fix mips Makefile	Christopher Pulte

2016-11-14	add option -lem_sequential for producing shallow embedding that refers to ↵	Christopher Pulte
	state monad, library fixes
2016-11-08	fixes	Christopher Pulte

2016-11-07	factor out regfp analysis types into etc/regfp.sail	Christopher Pulte

2016-11-03	split out RI node so that ppcmem model does not implement reserved ↵	Robert Norton
	instruction exception behaviour but sequential model does (for test suite).
2016-10-20	changes to support get_model for ppcmem.	Robert Norton

2016-09-23	Add register footprint function needed by ppcmem (mips only for now)	Robert Norton

2016-06-03	Change path inside sail Makefile to look for sail directory instead of l2	Kathy Gray

2016-05-26	add makery for mips/cheir LOC count.	Robert Norton

2016-04-21	Introduce wrapper function around MEMw* so that we can clear tags on ↵	Robert Norton
	non-capability writes on cheri.
2016-04-14	add cheri make target analagous to mips	Robert Norton

2016-04-13	Copy run_with_elf to make run_with_elf_cheri and revert run_with_elf to mips ↵	Robert Norton
	version. Temporary 'solution' to building mips and cheri builds until proper factorising can take place.
2016-03-08	add beginnings of cheri sail for kathy to do some debugging.	Robert Norton

2016-03-07	Split mips.sail into three file and make use of the new -o option in ↵	Robert Norton
	preparation for adding cheri support in separate files.
2016-02-11	point to lem and linksem embedded versions of libraries instead of relying ↵	Robert Norton
	on opam provided ones.
2016-02-11	use paths relative to current makefile for lem and linksem.	Robert Norton

2016-01-26	tweak to dependencies to hopefully reduce need to rebuild mips.sail.	Robert Norton

2016-01-21	build mips interpreter with -g	Robert Norton

2016-01-20	trim some obsolete/bitrotted make stuff.	Robert Norton

2016-01-20	build all mips stuff in _build. Still hacky and might be preferable to use ↵	Robert Norton
	ocamlbuild but works OK and shouldn't have to call sanitize.
2016-01-19	hacky initial makery for mips interpreter. Builds stuff in wrong places and ↵	Robert Norton
	needs fixing but nearly works.
2015-12-22	Add mips64 to get_elf in Makefile	Robert Norton

2015-11-25	non-working sail/mips interpreter integration for kathy to look at and ↵	Robert Norton
	example mips elf file.
2015-11-20	make the abis directory as well	Kathy Gray

2015-11-20	fixes to get-elf to work on linux. Hope it works on Mac too.	Robert Norton

2015-11-19	Keep up with linksem	Kathy Gray

2015-11-19	More makefile type	Kathy Gray