sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2016-01-28	Support exit and assert better in sequential interpreter and general ↵	Kathy Gray
	interpreter interface
2016-01-27	Add --max_instruction to sequential interpreter to permit an upper bound on ↵	Kathy Gray
	instructions run
2016-01-27	Add ability to run to a particular instruction execution number	Kathy Gray
	Could later add the ability to run to a particular instruction form (like we had in ppcmem2) or address
2016-01-27	Make mips build again	Kathy Gray
	Make quiet mode for sequential interpreter not print
2016-01-27	Fix issue where constraint solver wasn't rewriting enough equality ↵	Kathy Gray
	constraints and thus causing inequality checks to be missed
2016-01-27	start adding breakpoint	Kathy Gray

2016-01-26	Stop turning all decreasing vectors into indexed ones : i.e. let's print ↵	Kathy Gray
	them sensibly at last
2016-01-26	fix starting indices for mips initial register values.	Robert Norton

2016-01-26	Fix some bugs in writing registers with slices in the sequential interpreter	Kathy Gray

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

2016-01-26	Add example of test which dies whilst trying to throw exception.	Robert Norton

2016-01-26	print reg dump in correct format for cheri test suite. Reinstate timing of ↵	Robert Norton
	execution.
2016-01-26	Fix problem in run_with_model where we forgot that ppcmem2 treats everything ↵	Kathy Gray
	as increasing, and updated ranges accordingly, and mistakenly were using the wrong range values for register slicing.
2016-01-26	move closer to power.sail -> power.ml output	Kathy Gray

2016-01-26	add example of mips test which fails with first instruction (jal)	Robert Norton

2016-01-26	dump registers in format expected by cheri test suite when halting. Remove ↵	Robert Norton
	distinction between prog_mem and data_mem at least for now as data_mem was not being populated correctly (wrong elf flags?).
2016-01-22	mips: fix PC update logic so branches might work.	Robert Norton

2016-01-22	add some test elf files for mips (pinched from cheri test suite).	Robert Norton

2016-01-21	Start splitting values/etc into int/big_int for ocaml generation	Kathy Gray

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

2016-01-21	mips interpreter successfully executes more than one instruction after some ↵	Robert Norton
	wrangling of integer types
2016-01-21	mips: rename GPRs so that they sort lexicographically for display.	Robert Norton

2016-01-20	see writes to registers in the register file for sequential interpreter	Kathy Gray

2016-01-20	keep specified order of vectors...	Kathy Gray

2016-01-20	Assorted bug fixes that gets one mips instruction running (then fails for ↵	Kathy Gray
	expected reasons) :)
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-20	Decoding a mips instruction :)	Kathy Gray
	Not executing yet as some previous commit has broken the interpreter's local assignment
2016-01-20	Show opcode in sequential interpreter when decode fails	Kathy Gray

2016-01-19	Put None and Some into interpreter environments	Kathy Gray
	Also making progress towards separating int sized things from integer sized things
2016-01-19	hacky initial makery for mips interpreter. Builds stuff in wrong places and ↵	Robert Norton
	needs fixing but nearly works.
2016-01-14	small edit to previous commit	Kathy Gray

2016-01-14	Fix cumulative effects for circumstance when lifting variable introductions ↵	Kathy Gray
	out of an if Note: this fixes the local cumulative effects for the e_assign and e_if, it may not properly propagate them to the context of the surrounding block
2016-01-13	Closes issue #28 and issue #27	Kathy Gray
	Note: also adds a most_significant function to the standard library, that returns the lowest indexed bit in a inc bit vector and the biggest indexed bit in a dec bit vector.
2016-01-12	Fix undefined nvar occurrences that were impacting ARM	Kathy Gray

2016-01-11	Interpreter interface now supports option<ast> result from decode and etc ↵	Kathy Gray
	instead of looking for exit calls
2016-01-11	Interpreter that understands assert	Kathy Gray

2016-01-07	Add E_assert to basic rewriters	Kathy Gray

2016-01-06	Add new assert expression to Sail	Kathy Gray
	This splits the former functionality of exit into errors, which should now use assert(bool,option<string>), and a means of signalling actions such as instruction-level exceptions, interrupts, or other features that impact the ISA. The latter will now be tracked with an effect escape, and so any function containing exit and declared pure will generate a type error. WARNING: ARM spec will not build with this commit until I modify it. MIPS spec will not build with this commit until modified.
2015-12-22	More make file goo, and fixing a typo in run_with_elf	Kathy Gray

2015-12-22	More gluing mips to interpreter	Kathy Gray

2015-12-22	Add mips64 to get_elf in Makefile	Robert Norton

2015-12-21	Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2	Christopher

2015-12-21	fixes, pp progress	Christopher

2015-12-17	Remove external functions that the library provides, having added them to ↵	Kathy Gray
	the type environment finally. (Also small cleaning of the new makefile)
2015-12-16	Fix a bug in checking vector accesses and ranges that was hiding some bugs, ↵	Kathy Gray
	and causing some incorrect lem_ast generation in mips code
2015-12-16	rewriter and pp changes for generating ARM output	Christopher

2015-12-15	better location information	Christopher

2015-12-14	Adding new location constructor for location of generated terms	Kathy Gray

2015-12-10	fix	Christopher