sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2014-10-30	Merge branch 'master' of bitbucket.org:Peter_Sewell/l2	Peter Sewell

2014-10-30	more compact pp of binary values (following verilog literal syntax)	Peter Sewell
	(though we still get some long lists of bitzero,bitzero,... in the instruction state printing...)
2014-10-30	Fix type error that Lem didn't catch with the interpreter alone	Kathy Gray

2014-10-30	harmonise argument order	Peter Sewell

2014-10-30	Add parameter to interp_exhaust with type maybe (list (reg_name,value)) for ↵	Kathy Gray
	registers we might read that we want values for (particularly the PC)
2014-10-30	Add case to neg for interp_lib	Kathy Gray

2014-10-29	tweak value pp (remove byte count)	Peter Sewell

2014-10-28	taint tracking unknown in interpreter	Kathy Gray

2014-10-28	Allow tracking of unknowns in interp library, removing the P hacks.	Kathy Gray
	Add a function from instruction to istate
2014-10-28	function in progress take 2	Kathy Gray

2014-10-28	hacks on taint tracking	Peter Sewell

2014-10-28	Add proper tag to constructors when storing continuation	Kathy Gray

2014-10-28	Function definition in progress	Kathy Gray

2014-10-28	K,P fix constructor-as-variable error	Peter Sewell

2014-10-27	Correct externally visible endianness bugs	Kathy Gray

2014-10-27	Add printing for instruction form	Kathy Gray

2014-10-22	Update printing for testing, fix some bugs found along the way	Kathy Gray

2014-10-20	Update the printing interface for ppcmem as opposed to run_model functionality	Kathy Gray

2014-10-20	Catch more types in constructor parameters	Kathy Gray

2014-10-20	Separate out printing facility from model driver into printing_functions ↵	Kathy Gray
	interface
2014-10-16	bug fixes to run test from Christopher's tests	Kathy Gray

2014-10-14	Iron out bugs in running new executable with branching; add new executable ↵	Kathy Gray
	as well.
2014-10-10	Functions for operating on bit and byte vectors from the interpreter interface	Kathy Gray

2014-10-08	Support exporting single bit and bool values to external bitvectors	Kathy Gray

2014-10-07	Connect interpreter to representation of instructions.	Kathy Gray
	Warning: this changes a few of the constructor names in the instruction_extractor.lem interface
2014-10-07	Track dependencies on size of memory access	Kathy Gray

2014-10-07	kathy,peter: making decode integration with ppcmem2 typecheck	Peter Sewell

2014-10-07	Actually add the new file	Kathy Gray

2014-10-07	Merge and make real Peter's comment type	Kathy Gray

2014-10-07	Put in type for instruction form for models; remove extra information from ↵	Kathy Gray
	Bytevectors; add place holder for memory size dependency tracking
2014-10-07	comment with suggested i_state_or_error type	Peter Sewell

2014-10-04	clarify Step constructor	Kathy Gray

2014-10-03	Add a decoding function to interp_interface and interp_inter_imp. (Note, ↵	Kathy Gray
	this is quite specific to Power's spec)
2014-10-02	correct renaming typo	Kathy Gray

2014-10-01	Fix bug omitting wmem effects	Kathy Gray

2014-09-30	Corrected writing to register bug. Now interpreter produces same result as ↵	Kathy Gray
	gdb on actual binary for hello6
2014-09-30	Add type annotations to funcls to track effects and constraints from one ↵	Kathy Gray
	function-clause
2014-09-29	Add in elf model from Dominic/Stephen. Make run_power build again. Does not ↵	Kathy Gray
	effectively use elf model yet
2014-09-19	Functions to extract instruction information	Kathy Gray

2014-09-11	Adding support for extracting the information Christopher needs about an ↵	Kathy Gray
	instruction
2014-09-04	Make exhaust run from the first breakpoint in the interactive interpreter	Kathy Gray
	(I still think this is a silly place to run exhaust from, but it no longer finds errors or crashes)
2014-08-27	Changes to get another (slightly larger) executable running;	Kathy Gray
	adding executable as a test as well
2014-08-26	small changes for arm	Kathy Gray

2014-08-21	Improve printing of function calls in stepper mode	Kathy Gray

2014-08-21	Allow command line interface to exhaustively evaluate the next step, ↵	Kathy Gray
	printing the events. Note: this commit switches back to a standard lem build located in ~/bitbucket/lem/lem
2014-08-20	Add ability to track register dependencies in interactive stepper; thus ↵	Kathy Gray
	testing register tracking/tainting
2014-08-19	make test_power_interactive working again; now using interp_interface ↵	Kathy Gray
	instead of internal actions
2014-08-19	Add file that actually drives command line interpreter	Kathy Gray

2014-08-18	Handling many register reads, writes, and memory reads.	Kathy Gray
	There are problems that warrant discussion about handling special registers that hold records or data structures previously.
2014-08-18	fix compile error	Kathy Gray