sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2014-11-20	Handle constructors with zero parameters better.	Kathy Gray

2014-11-20	Set vector start for more register writes	Kathy Gray

2014-11-20	set more vector starts before sending them off to register writes	Kathy Gray

2014-11-19	Correct off-by-one bug in type checking vector slices	Kathy Gray
	Convert sparse vectors into full-fledged vectors more frequently and on export to memory system
2014-11-18	Fix various pattern match bugs; add a few functions	Kathy Gray

2014-11-17	Make env_union intelligently join two environments instead of just list append.	Kathy Gray

2014-11-16	Add overflow checking arithmetic operations. Fix various bugs that this exposed	Kathy Gray
	Of note: Interp_lib.to_num now takes an Unsigned or a Signed constructor, rather than a boolean
2014-11-13	numbers got to big for show, write my own version	Kathy Gray

2014-11-06	Refactor printing to display the contents the [_] and to better format bit ↵	Kathy Gray
	vectors
2014-11-05	Fix bug on decoding Sc	Kathy Gray

2014-11-04	Read parts of a register, not always just the whole thing	Kathy Gray

2014-11-04	Fixes bugs:	Kathy Gray
	not setting starting bit of vector properly not treating properly if when given a non boolean --- bool largely removed in place of bit, removing many/most is_one casts but true and false are still possible values coerces between bit vectors of length one and bits again, because reading from a register can otherwise be wrong with respect to the interface
2014-11-04	Fix setting of initial position in a vector after a slice	Kathy Gray

2014-10-28	taint tracking unknown in interpreter	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-16	bug fixes to run test from Christopher's tests	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	Put in type for instruction form for models; remove extra information from ↵	Kathy Gray
	Bytevectors; add place holder for memory size dependency tracking
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-26	small changes for arm	Kathy Gray

2014-08-21	Improve printing of function calls in stepper mode	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	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	tweak barrier kinds in interface (likely needs changes elsewhere)	Peter Sewell

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

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.
2014-08-05	start tainting values with register dependencies	Kathy Gray

2014-08-01	Support separated memory read/write functions.	Kathy Gray
	Also allows register writing functions to be on the left hand side of an assignment in the same way. The last parameter to a writing function is the value to be written, and should appear on the right hand side of an assignment expression.
2014-07-30	working dec vectors	Kathy Gray

2014-07-18	Writing to concatenated aliases	Kathy Gray

2014-07-16	Reading from an alias to two concatenated registers; not writing yet.	Kathy Gray

2014-07-16	Get writing working for aliases in the interpreter, other than concatenation.	Kathy Gray

2014-07-14	Add register to alias concatenation type	Kathy Gray

2014-07-14	Initial support for aliases and exit through the type system and the ↵	Kathy Gray
	interpreter. An alias can be read within the interpreter, but not written to. Exits aren't yet taken in the interpreter.
2014-07-03	Adjust behavior on Unknown values in pattern match to stop matching as soon ↵	Kathy Gray
	as a pattern is matched without using an unknown; also causes full expansion on function calls with unknowns matched in patterns, however the local state is not reset.
2014-07-02	Fix ordering issue in vector-concat pattern matching	Gabriel Kerneis

2014-06-30	Support for nondeterministic blocks	Kathy Gray

2014-06-25	Add support for memory barrier	Kathy Gray

2014-06-25	Add support for actions that read just a slice or single bit of a register	Kathy Gray

2014-06-24	Get enumerations working in interpreter	Kathy Gray
	(plus a few other small related corrections)
2014-06-23	Get indexed vectors, particularly with default values, working	Kathy Gray

2014-06-18	Make hex constants work; improve utility of casts for selecting overloaded ↵	Kathy Gray
	functions
2014-06-12	Interpret when an unknown is inserted into the program by interp_exhaustive	Kathy Gray
	Short version of below; ready to hook interp_exhaustive up to something to test, but haven't yet. If an unknown value influences a pattern match within an expression, each passing pattern is found and the bodies strung together into a block with let expressions to bind the variables. In a function call, the cases are all collected but the support is not in place at the moment to evaluate them. If an unknown is the result of the cond expression in an if, the then and else case become a block. Unknowns within the interpreter propagate to more Unknowns; also for some but not all library functions yet.