sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2016-09-09	update instruction_analysis to support nias and instruction kind	Christopher Pulte

2016-09-07	push some lem pp changes	Christopher Pulte

2016-09-02	Extend type checking so that patterns with vector concatenation don't permit ↵	Kathy Gray
	under specified vector lengths (at least for function patterns) Extend interpreter interface to have a function for Christopher's instruction analysis
2016-08-24	pull files from idlarm	Shaked Flur

2016-08-18	move register_base_name and slice_of_reg_name from ppcmem thread semantics ↵	Christopher
	to interp_interface, fix reg_name comparison and equality
2016-08-17	tuple assignment now implemented so (a,b) := foo() will now work	Kathy Gray

2016-08-17	Fix pattern match bug in interp where vector accesses were using the wrong ↵	Kathy Gray
	start index
2016-08-14	Add missing case to replicate	Kathy Gray

2016-08-14	Start adding form for (a,b,c) := foo()	Kathy Gray
	Not working yet
2016-08-10	Missing case in lib	Kathy Gray

2016-08-10	Fix sizeof code generation to look at parameter bounds	Kathy Gray

2016-08-09	More fixes to resolving nat variables across cases	Kathy Gray

2016-08-08	Fix bug in type checker that ignored some pattern's constraints; fix second ↵	Kathy Gray
	bug that didn't cope properly with flow sensitive analysis across more than two case branches.
2016-08-06	Add duplicate_bits to lib	Kathy Gray
	Pull Peter's changes to interp_interface back into the primary repo
2016-08-05	Fix list parsing and empty vector parsing	Kathy Gray
	Add div to library functions
2016-08-01	Remove raise_c2_exception_v function which is not needed after permissions ↵	Robert Norton
	merge and no longer appears in spec.
2016-08-01	Complete transition to merged perms. We need to take care to keep around the ↵	Robert Norton
	unused reserved permissions for when copying data, and stragely for candperms too.
2016-07-28	Banish exit from the mips/cheri sail except at end of SignalException ↵	Robert Norton
	function. There is a plan to replace this syntax with something more understandable. Should make no functional difference using sequential interpretor but will need to do some work on exception functions when integrating with ppcmem so that it know register writes are exceptional etc.
2016-07-28	Complete another if statement with an empty else.	Robert Norton

2016-07-28	Use recently introduced 'not' function instead of ~ for boolean negation. ↵	Robert Norton
	More readable when extracted to manual.
2016-07-27	Fix misspelt marker comment.	Robert Norton

2016-07-27	Add final 'else' to CCheckPerms because Peter pointed out that it is better ↵	Robert Norton
	this way.
2016-07-27	CCall comment out of extracted psuedocode region.	Robert Norton

2016-07-27	Normalise whitespace in cheri_insts.sail for cleaner extraction of ↵	Robert Norton
	instructions into manual. Whitespace only.
2016-07-27	Add a function 'not' to the library with type bit -> bit	Kathy Gray

2016-07-26	Fix incomplete match warning in run_with*	Robert Norton

2016-07-26	Increase size of TLB to 64 entries. In theory this should improve FreeBSD ↵	Robert Norton
	boot time by reducing TLB misses but an apparent reduction in IPS counteracts this. Makes use of foreach and return to implement tlbSearch.
2016-07-26	Add support for BERI specific behaviour which permits some unaligned ↵	Robert Norton
	accesses, for compatibility with clang.
2016-07-26	And fix abbrev oversite in interpreter	Kathy Gray

2016-07-26	Fix type abbreviation support oversight	Kathy Gray

2016-07-26	Add minimal support for emulated Altera JTAG UART.	Robert Norton

2016-07-26	Add support for loading a raw binary file at given location in memory prior ↵	Robert Norton
	to sequential simulation. This is needed for booting FreeBSD where a minimal bootloader (simboot.elf) runs before jumping into the kernel loaded in memory.
2016-07-26	Add Makefile and marker comments in cheri sail file for extracting ↵	Robert Norton
	individual instructions to go in CHERI documentation.
2016-07-25	Fix incorrect register number for CP0Cause in mtc0. The only test which ↵	Robert Norton
	writes this register also needs software irq, which isn't implemented, so effectively this was untested although it happens quite early in kernel boot.
2016-07-25	win	Kathy Gray

2016-07-25	one more go	Kathy Gray

2016-07-25	Actually fix stack for return	Kathy Gray

2016-07-25	Fix stack for return	Kathy Gray

2016-07-25	Support return in interpreter pretty printer (also fix typo for default case)	Kathy Gray

2016-07-25	auto coerce to bit vector from bit	Kathy Gray
	pretty print lret effects into lem
2016-07-24	Make sure that all type constructors with unit type have a type union with ↵	Kathy Gray
	just an id (hopefully fixes Christopher issue).
2016-07-23	Add effect annotation for return, and actually keep a return after type check.	Kathy Gray

2016-07-23	update to remove use of return as variable	Kathy Gray

2016-07-23	Add a return exp form to Sail, supported in type checker and in interpreter.	Kathy Gray
	TODO: add an event for a return so that rewriters can find and remove them as needed for OCaml and Lem
2016-07-20	Make rewriter understand type abbreviations for removing internal_exp instances	Kathy Gray

2016-07-13	fix	Christopher

2016-07-13	fixes	Christopher

2016-07-12	sail-to-lem and lem library fixes	Christopher

2016-07-01	Add missing case to arith_op_no0	Kathy Gray
	Add type refinement to arm spec
2016-06-28	Munge exception destination PC so we hit the correct address even when ↵	Robert Norton
	kcc.base is non-zero.