sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2017-12-05	Update license headers for Sail source	Alasdair Armstrong

2017-08-16	lem_interp: remove broken val_to_string_internal functions, replace with ↵	Jon French
	string_of_value as used everywhere else
2017-02-03	fix headers	Peter Sewell

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-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-17	Use red printing for the value in the hole from Printing_functions instead ↵	Kathy Gray
	of mangling the ascii manually
2014-11-06	Refactor printing to display the contents the [_] and to better format bit ↵	Kathy Gray
	vectors
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-04	clarify Step constructor	Kathy Gray

2014-08-19	make test_power_interactive working again; now using interp_interface ↵	Kathy Gray
	instead of internal actions
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-05	start tainting values with register dependencies	Kathy Gray

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-16	Reading from an alias to two concatenated registers; not writing yet.	Kathy Gray

2014-07-15	Finishing up some of the support for Exit	Kathy Gray

2014-06-30	Support for nondeterministic blocks	Kathy Gray

2014-06-10	Minor color and build tweaks	Gabriel Kerneis

2014-06-10	More colors	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-09	Support deinfix pretty-printing	Gabriel Kerneis

2014-06-09	Add "continuation" command in interpreter	Gabriel Kerneis
	This displays the full continuation of the current breakpoint, which is basically the closest that we have from the "context" requested by Peter. Especially using it after the "execute" breakpoint shows the code of the instruction to be executed.
2014-06-09	Add switch to show/hide casts in interpreter	Gabriel Kerneis
	Use "show_casts" and "hide_casts" in interactive interpreter to display or show casts in expressions. Hidden by default (makes things much less readable otherwise).
2014-06-07	Improve help message	Gabriel Kerneis

2014-06-07	Print mem and env	Gabriel Kerneis

2014-06-07	Stack printing	Gabriel Kerneis

2014-06-06	Compact debug output and first draft of interactive loop	Gabriel Kerneis

2014-06-05	Enable single-stepping for test/power.sail	Gabriel Kerneis

2014-05-29	Check constraints in power.sail; this required using big_int instead of int ↵	Kathy Gray
	to support 264. Note: now nat (short hand for range<0,infinity>) should only be used if you really mean a nat instead of a bounded number (i.e. range<0,232>)
2014-05-28	correct mismatched parens didn't mean to commit...	Kathy Gray

2014-05-28	Support stepped interpreting, and use normalisation instead of eval_nexp in ↵	Kathy Gray
	constraints
2014-05-21	More interface support; interp_inter_imp now compiling	Kathy Gray

2014-05-12	More interface support	Kathy Gray

2014-05-08	more interface changes	Kathy Gray

2014-04-04	Cosmetic improvements (statistics, --quiet)	Gabriel Kerneis

2014-04-04	Improve Power execution	Gabriel Kerneis
	- Move FDE loop to the OCaml side of the Power model (avoid leaking memory due to lack of TCO in interpreter) - Display cycle count - Check the value of CIA at the end of each cycle and stop if it is equal to the initial value of LR, returning the value in GPR3.
2014-04-02	Solve more constraints; fix up test suite bugs uncovered by solving more ↵	Kathy Gray
	constraints. Clean up Lem output a little for readability while debugging.
2014-03-20	Remove work-around from interpreter, move it to power.sail	Gabriel Kerneis
	Two bugs are worked-around here: - missing cast to nat when a vector is wrapped in exts (exts is a no-op currently anyway, so we are discarding it) - missing cast (due to limited type-inference) in one if branch: type given explicitly.
2014-03-20	Workaround missing casts for external calls	Gabriel Kerneis
	This patch should be reverted when the interpreter is fixed. The first instruction of main.bin is now executed. The second one fails, seemingly because of a similar missing cast issue (external function add receives register GPR1 as value).
2014-03-19	Fix endianness	Gabriel Kerneis
	This will never end…
2014-03-17	Revert broken vector handling	Gabriel Kerneis

2014-03-14	Support regbits read and write	Gabriel Kerneis
	No support for non-contiguous writes.
2014-03-14	Pretty-print subreg correctly	Gabriel Kerneis

2014-03-12	Remove automagic register initialization	Gabriel Kerneis

2014-03-11	More work on interpreter and Power model	Gabriel Kerneis

2014-03-07	Treat registers as values when not being actively read or written to, so ↵	Kathy Gray
	that we can have a vector of registers for example. Also, register types can be explicitly referenced.
2014-02-28	Fix endianness	Gabriel Kerneis
	In fact, increasing order is big-endian, not little-endian. This is good news for us, because it means we do not need any switch for the POWER spec.
2014-02-28	Load ELF sections to virtual memory addresses	Gabriel Kerneis
	Roughly 110KB/s (~5 seconds to load "hello" test).
2014-02-27	More flexible test execution	Gabriel Kerneis