sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
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-30	Executing an actual elf file	Kathy Gray

2014-09-29	Connect up to elf model; which doesn't seem to be representing the elf file ↵	Kathy Gray
	properly yet but run_power.native is connected to it
2014-09-29	add run_power to last commit	Kathy Gray

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-10	reduce lem macro overhead for sail _ very slightly _	Kathy Gray

2014-09-09	Small fix to printing	Kathy Gray

2014-09-09	Full power.sail now type checking and generating Lem.	Kathy Gray

2014-09-09	Get more constraints resolving in power.sail	Kathy Gray

2014-09-05	refinements to constraint checking	Kathy Gray

2014-09-04	Refine overloading resolution with respect to vectors and ranges	Kathy Gray
	Fix a few other bugs as well
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-30	fix various bugs exposed by armv8	Kathy Gray

2014-08-28	more bug fixes and adding more library functions	Kathy Gray

2014-08-28	fixes to bugs exposed by arm model	Kathy Gray

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-24	Use LEM_DIR environment variable if defined	Gabriel Kerneis
	LEM_DIR must contain the absolute path the Lem directory. If not defined, the previous behaviour is retained: a relative path is used, assuming Lem is in bitbucket/lem.
2014-08-24	Silence some OCaml warnings	Gabriel Kerneis

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	Silence some lem warnings in compilation.	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-13	Kathy, Peter tweak Makefile for interactive demo and src/myocamlbuild.ml to ↵	Peter Sewell
	temporarily use other version of Lem
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-05	missed file from last commit	Kathy Gray

2014-08-05	Support extracting length information into more functions	Kathy Gray