sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2016-10-06	move type definitions that both interpreter and shallow embedding use to ↵	Christopher Pulte
	sail_impl_base, add sail_impl_base.outcome, add interp_inter_imp auxiliary functions, make prompt use sail_impl_base.outcome
2016-09-30	add Robert's DIA typeclass instances	Christopher Pulte

2016-09-30	fixes, update isntruction_analysis for NIAs and DIA	Christopher Pulte

2016-09-28	Possible fix for equality and inequality	Kathy Gray

2016-09-28	Fix type checking bug that was missing unifications for nats	Kathy Gray

2016-09-26	minor changes	Christopher Pulte

2016-09-26	nicer lem output: fewer unnecessary letbinds, monad binds and returns	Christopher Pulte

2016-09-25	nicer lem output: no more unecessary 'unit' returns if if-expressions, ↵	Christopher Pulte
	for-loops or case-expressions also return updated variables
2016-09-24	nicer lem output: fewer unecessary 'return's	Christopher Pulte

2016-09-23	Merge branch 'master' of https://bitbucket.org/Peter_Sewell/sail	Christopher Pulte

2016-09-23	sail-to-lem progress	Christopher Pulte

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

2016-09-21	fixes	Christopher Pulte

2016-09-19	Merge branch 'master' of https://bitbucket.org/Peter_Sewell/sail	Christopher Pulte

2016-09-19	sail-to-lem progress	Christopher Pulte

2016-09-19	Fix type check bug	Kathy Gray

2016-09-19	remove conflict message	Christopher Pulte

2016-09-16	fix	Christopher Pulte

2016-09-16	make vector concatenation pattern removal deal with vector patterns of ↵	Christopher Pulte
	unknown length (in the last item)
2016-09-14	Switch mips/cheri over to using memory ea/val for writes. Tag is now first ↵	Robert Norton
	byte of value for capability writes. Still need TAGw for now but should kill eventually.
2016-09-14	Add memory kind for concurrent tag reads and writes	Kathy Gray

2016-09-14	Change reading and writing of tag memory to report the tag/look for the tag ↵	Kathy Gray
	as the first byte of the byte list on tagged memory operations
2016-09-13	Support memea and memv in sequential interpreter	Kathy Gray

2016-09-13	Add optional address to memv events	Kathy Gray

2016-09-13	add show functions, fix	Christopher Pulte

2016-09-13	extern slice for instruction analysis	Kathy Gray

2016-09-12	add list append function	Kathy Gray

2016-09-09	Fix bug in type checking cons that put the list first instead of the new element	Kathy Gray

2016-09-09	minor fixes	Kathy Gray

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-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-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-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	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