sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2015-11-25	non-working sail/mips interpreter integration for kathy to look at and ↵	Robert Norton
	example mips elf file.
2015-11-05	some progress on lem backend: rewrite away mutable variable assignments, ↵	Christopher Pulte
	rewrite for-loops, if/case-expressions to return updated variables
2015-10-20	Fixing bugs in pretty printer to ocaml	Kathy Gray

2015-10-17	clean up, more readability	Christopher Pulte

2015-10-05	added funcl pattern rewriting to remove vector concat patterns	Christopher Pulte

2014-11-27	updated test for power.sail	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-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-12	Stop overzealously looking for constructors, only when the type suggests to	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	setup printing for memory on tests	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	Pull in updated elf model, make build work again (at least for me)	Kathy Gray

2014-10-27	Correct externally visible endianness bugs	Kathy Gray

2014-10-27	debugging temp	Kathy Gray

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