sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2016-03-08	missing file from last commit	Kathy Gray

2016-03-08	Return undefined value on reads of uninitialised memory	Kathy Gray

2016-03-08	Fix error in handling type abbreviations in LEXP type checker	Kathy Gray

2016-03-08	Start task of setting up tagged memory in sequential interpreter	Kathy Gray

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-03-03	Fix typo in manual which had true instead of false on assert documentation	Kathy Gray
	Fix bug in local register access
2016-03-02	Add new language feature to permit definitions of items of kind Nat, etc as ↵	Kathy Gray
	well as items of kind Type. Syntax for the feature is: def Nat id = nexp Note: some useful nexps may not parse properly. All typedef forms can also be used as def Type ... if desired, but this is not required.
2016-02-24	Small mixups to get the initial check infrastructure working for full ast ↵	Kathy Gray
	processing
2016-02-23	Several fixes	Kathy Gray
	Improve printing for asl to sail readability; Add -o option for selecting the name of file generation; Add additional initial check module for turning generated ast nodes into ready-to-type-check ast nodes
2016-02-11	point to lem and linksem embedded versions of libraries instead of relying ↵	Robert Norton
	on opam provided ones.
2016-02-11	Begin adding some new library functions like absolute value	Kathy Gray

2016-02-11	use paths relative to current makefile for lem and linksem.	Robert Norton

2016-02-09	fix scattered type union source printing	Kathy Gray

2016-02-08	slightly clean up vector type printing and empty effect printing for functions	Kathy Gray

2016-02-05	fix typo in kathy's last commit.	Robert Norton

2016-02-05	change signed mod behaviour for numbers to match that of vectors	Kathy Gray

2016-02-04	fix pretty printing of new mod_s	Robert Norton

2016-02-04	add mod_s to lexer and parser	Kathy Gray

2016-02-04	Add mod_s	Kathy Gray

2016-02-04	add forgotten lib binding	Kathy Gray

2016-02-04	and for quot_s	Kathy Gray

2016-02-04	Relax constraints on quot temporarily since it was prohibiting negative ↵	Kathy Gray
	numbers accidentally
2016-02-03	mips: finish implementing address translation on instruction fetch and ↵	Robert Norton
	remove temporary hack in TranslateAddr.
2016-02-03	mips: add support for LLAddr, a debug register used for ll/sc. Also add ↵	Robert Norton
	missing psuedo-registers in run_with_elf.
2016-02-03	add example of elf file which fails to load due to linksem error: ↵	Robert Norton
	get_elf64_global_symbol_init: invariant failed, global variable appears in multiple segments
2016-02-02	mips.sail: add an 'inBranchDelay' register so that SignalException can set ↵	Robert Norton
	correct state on exception. branchPending does not work because it is cleared before executing the branch delay.
2016-02-02	Print out the address of the instruction running in sequential interpreter	Kathy Gray

2016-02-02	Get mips stuff hooked up with translate address.	Kathy Gray
	Note: this support is rather mips centric at the moment
2016-02-02	add translate_address functionality	Kathy Gray

2016-01-29	fix typo in kathy's last commit.	Robert Norton

2016-01-29	Put correct tags on to_vec calls	Kathy Gray

2016-01-29	mips.sail: it turns out that all sail comparisons are signed contrary to ↵	Robert Norton
	manual so emulate unsigned comparisons by prepending a zero bit, as in mips spec.
2016-01-28	Add test for sltu. Fixed decode function which was returning wrong ast node ↵	Robert Norton
	but test still does not pass, apparently because sail is doing signed comparison for <
2016-01-28	add test exposing problem with ddiv.	Robert Norton

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