sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2014-10-27	add objdump disassembly of hello4 executable	Peter Sewell

2014-10-27	source and assembly of test hello4	Kathy Gray

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	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-15	Get the actual start address instead of the address of the start address	Kathy Gray

2014-10-15	Fixup printing on dumping memory to a lem file	Kathy Gray

2014-10-15	Add ability to print out binary as lem file of memory dump instead of ↵	Kathy Gray
	running binary; to generate files for Peter to load, in the first instance.
2014-10-14	Iron out bugs in running new executable with branching; add new executable ↵	Kathy Gray
	as well.
2014-10-10	make run_power.ml compile again	Kathy Gray

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-04	Refine overloading resolution with respect to vectors and ranges	Kathy Gray
	Fix a few other bugs as well
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-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	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-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-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-15	Add failing test for type of aliases	Gabriel Kerneis
	File "test/regbits.sail", line 23, character 3 to line 23, character 4 Type error: Can only assign to identifiers with type register or reg, found identifier CA with type bit
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-04	Correct error of forgetting type information that was allowing more programs ↵	Kathy Gray
	than it should have
2014-07-04	Update power.sail	Gabriel Kerneis

2014-07-02	Update Power example	Gabriel Kerneis

2014-06-27	Update type conformance for overloading resolution on order arguments.	Kathy Gray
	Also, correctly type check nondet blocks
2014-06-26	Adding better support for unspecified values in indexed vectors	Kathy Gray
	Also begining to add support for nondeterministic blocks and cleaning up some of the Many warnings on pattern matches
2014-06-25	Add support for actions that read just a slice or single bit of a register	Kathy Gray

2014-06-24	Get vector length for to_inc_vec and to_dec_vec from the type system after ↵	Kathy Gray
	constraint solving (instead of hardcoding 64 as the default).
2014-06-23	Get indexed vectors, particularly with default values, working	Kathy Gray

2014-06-18	Correct effect matching bug; and print out effect lists	Kathy Gray

2014-06-18	Make hex constants work; improve utility of casts for selecting overloaded ↵	Kathy Gray
	functions
2014-06-11	power.sail: store mode64bit in a bool register	Gabriel Kerneis
	This is now possible because we handle coercions better.
2014-06-11	Update power.sail: remove some hacks	Gabriel Kerneis

2014-06-09	Improve interaction after chat with Peter	Gabriel Kerneis
	- remember mode (run, step or next) between instructions - display continuation by default in step mode - start in step mode by default - incompatible change: the shorthand for stack is now bt (=backtrace), since s becomes the shorthand for step - incompatible change: pressing enter now repeats the current mode, instead of "step"
2014-06-07	Don't use cycle for fetch-decode-execute	Gabriel Kerneis

2014-06-07	exts returns bit[64] instead of nat	Gabriel Kerneis
	Update power.sail to new, pretty-printer-based version
2014-06-07	Copy main.bin in Sail repository for Power test	Gabriel Kerneis

2014-06-07	Pattern-matching exhaustiveness	Gabriel Kerneis

2014-06-06	Add wrapper script and --interactive for demo	Gabriel Kerneis

2014-06-05	Shorten debug output for power	Gabriel Kerneis