sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2015-03-18	Use boolean on write where applicable	Kathy Gray

2015-03-17	Correct directionality in interpreter. Now the interpreter shouldn't use inc ↵	Kathy Gray
	unless that's the current default or there's no default set in the spec
2015-03-15	Many changes:	Kathy Gray
	Split out specification specific memory and external functions Reduce the presence of big_int Reduce the use of inc direction, instead using a default from the spec. Still a few places need to be parameterised over direction Also some bug fixes exposed by above and running ARM second instruction
2015-02-27	Fix a series of errors leading to the first ARM instruction not running.	Kathy Gray
	Including: Correct loss of constraints between declared constraints, pattern constraints and expression body constraints Handle insertion of dependent parameters in the case of unit parameters Add a case to how ifields are translated to permit numbers as well as bits and bitvectors Expand interpreter to actually handle user-defined functions on the left had side of the assignment expression.
2014-12-11	Many fixes, primarily dealing with undefined	Kathy Gray
	Including: turn an undefined literal into a vector of undefined values of the correct length handle sparse vector unspecified default values as undefined literals allow global lets to call library functions
2014-12-10	Fix mismatch errors in interpreter, mostly relating to taint/detaint behaviour	Kathy Gray
	Also fixed for loop evaluation
2014-11-23	make interpreter work better with unknowns, make interp_inter_imp do better ↵	Kathy Gray
	on coercions
2014-11-23	Merge branch 'master' of bitbucket.org:Peter_Sewell/l2	Peter Sewell

2014-11-23	the properly named "git"	Peter Sewell

2014-11-23	extern single bit and single bool to instruction_fields	Kathy Gray

2014-11-23	Fill in some of the basic coercions	Kathy Gray

2014-11-23	clean up interp inter	Kathy Gray

2014-11-23	more coercions	Peter Sewell

2014-11-23	OCaml stubs for coercions and _to_istate OCaml	Peter Sewell

2014-11-23	wib (comment out to typecheck the rest...)	Peter Sewell

2014-11-23	fight with interface/impl mismatch. lose.	Peter Sewell

2014-11-23	update instruction/istate decoding.	Kathy Gray
	Use register size. Printing again doesn't compile
2014-11-22	interp_interface happy again. printing functions now doesn't compile	Kathy Gray

2014-11-22	Add size of register to register for making appropriate unknown register_values	Kathy Gray

2014-11-22	Changing interface in step with Peter and ppcmem changes	Kathy Gray

2014-11-21	Support signed and unsigned arithmetic	Kathy Gray

2014-11-21	Fix bugs now documented in ppcmem notes	Kathy Gray

2014-11-20	look for sub matches of registers on exhaustive mode	Kathy Gray

2014-11-19	add byte_list_of_integer	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	Actually expect barriers to happen	Kathy Gray

2014-11-18	Fix countLeadingZeroes typo (diff in number of es present)	Kathy Gray

2014-11-16	Add some missing functions	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	Catch more cases of registers for extern_reg	Kathy Gray

2014-11-13	Set start index on bits in extern_value	Kathy Gray

2014-11-07	Add integer_of_byte_list : list word8 -> integer	Kathy Gray

2014-11-07	typo	Kathy Gray

2014-11-07	more num_to_bits	Kathy Gray

2014-11-07	Put back old num_to_bits temporarily; add in a num_to_bits_correct that ↵	Kathy Gray
	treats the last argument as a big num
2014-11-07	Fix types in num_to_bits	Kathy Gray

2014-11-05	Correct bug treating unsigned values as signed in arith operations	Kathy Gray

2014-11-05	fix(?) a Big_int/int type error wrt trans_sail	Peter Sewell

2014-11-04	Merge branch 'master' of bitbucket.org:Peter_Sewell/l2	Peter Sewell

2014-11-04	proposed split of decode into decode-to-instruction and ↵	Peter Sewell
	instruction-to-instructionstate
2014-11-04	Read parts of a register, not always just the whole thing	Kathy Gray

2014-11-04	K,P debugging	Peter Sewell

2014-11-04	Fix setting of initial position in a vector after a slice	Kathy Gray

2014-10-31	Add a num to bits function; start hooking up the power.ml file to the ↵	Kathy Gray
	symbol/memory address list.
2014-10-30	Fix type error that Lem didn't catch with the interpreter alone	Kathy Gray

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-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	Function definition in progress	Kathy Gray