sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
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

2014-08-18	Switch run_power to use interp_interface. Compilers and begins running, and ↵	Kathy Gray
	then hits an error. So still in progress Note: moved barrier kind changes to interp_interface, along with other memory kinds
2014-08-18	wib?	Peter Sewell

2014-08-18	make interp_exhaustive not take an interp_mode argument	Peter Sewell

2014-08-18	tweak barrier kinds in interface (likely needs changes elsewhere)	Peter Sewell

2014-08-14	Small tweaks to interp_interface interface	Kathy Gray
	Also adding more comments and getting the ml files built in the build process
2014-08-13	Update library functions	Kathy Gray

2014-08-13	FInd/fix a redundant case now that warnings are manageable	Kathy Gray

2014-08-13	Complete tainting phase 1	Kathy Gray
	Now when mode.track_values is true, on every register read, the returned value is tainted with the register it came from. This tracking is followed through every operation the interperter touches (except library functions, to be completed next). One a memory operation involving a tracked value, there is optionally list of registers that value arose from in the memory request (i.e. maybe (list reg_name)).
2014-08-12	taint tracking through most of interpreter	Kathy Gray
	Need to add cases for tracking a taint past a conditional check where possible; and then to actually generate them from reading registers.
2014-08-12	more taint tracking, yet again	Kathy Gray

2014-08-11	More taint tracking.	Kathy Gray
	Catch interp_inter_imp up with interp. WARNING: This commit triggers an exponential performance bug in Lem. To alleviate this bug, I am running with a locally modified Lem that has line 1321 of lem/src/typed_ast.ml commented out (On my laptop, I gave up trying to compile after about 900 seconds; beefier computers May be able to run unmodified, I don't know)
2014-08-09	More tracking register dependency; another check point that compiles in ↵	Kathy Gray
	under two minutes
2014-08-08	Tracking register dependence.	Kathy Gray
	Check point where Lem will compile interpreter in under 2 minutes
2014-08-07	Fix bug introduced by last commit	Kathy Gray

2014-08-07	Track taints across machine calls.	Kathy Gray
	This introduced a bug in vector.sail, commented out and needs to be fixed.