sail - Formal specification language for ISAs

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

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

2014-10-27	Correct externally visible endianness bugs	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	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-03	Add a decoding function to interp_interface and interp_inter_imp. (Note, ↵	Kathy Gray
	this is quite specific to Power's spec)
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-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-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-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	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-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-06-30	Support for nondeterministic blocks	Kathy Gray

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

2014-06-09	Working towards evaluating with interp_exhaustive	Kathy Gray

2014-05-28	Support stepped interpreting, and use normalisation instead of eval_nexp in ↵	Kathy Gray
	constraints
2014-05-22	A (hopefully) sufficient interface and implementation between memory and the ↵	Kathy Gray
	interpreter
2014-05-21	More interface support; interp_inter_imp now compiling	Kathy Gray

2014-05-20	Fix interp compiling bug	Kathy Gray

2014-05-20	yet more interface	Kathy Gray