sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2014-07-03	Adjust behavior on Unknown values in pattern match to stop matching as soon ↵	Kathy Gray
	as a pattern is matched without using an unknown; also causes full expansion on function calls with unknowns matched in patterns, however the local state is not reset.
2014-07-02	Fix ordering issue in vector-concat pattern matching	Gabriel Kerneis

2014-07-01	Update case of EXTS	Gabriel Kerneis

2014-06-30	Support for nondeterministic blocks	Kathy Gray

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

2014-06-25	Add support for actions that read just a slice or single bit of a register	Kathy Gray

2014-06-24	Get enumerations working in interpreter	Kathy Gray
	(plus a few other small related corrections)
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-19	Add mod:vec->range->vec	Gabriel Kerneis

2014-06-18	Fix mod_vec in library	Gabriel Kerneis

2014-06-18	Add definition of mod to lib	Kathy Gray

2014-06-18	Make hex constants work; improve utility of casts for selecting overloaded ↵	Kathy Gray
	functions
2014-06-12	Interpret when an unknown is inserted into the program by interp_exhaustive	Kathy Gray
	Short version of below; ready to hook interp_exhaustive up to something to test, but haven't yet. If an unknown value influences a pattern match within an expression, each passing pattern is found and the bodies strung together into a block with let expressions to bind the variables. In a function call, the cases are all collected but the support is not in place at the moment to evaluate them. If an unknown is the result of the cond expression in an if, the then and else case become a block. Unknowns within the interpreter propagate to more Unknowns; also for some but not all library functions yet.
2014-06-11	Equality between range and bit vector	Gabriel Kerneis
	The type-constraints are inspired from those for (+). They seem to work but I am not sure they make sense. The vector is interpreted as unsigned.
2014-06-11	Improve error message for missing library functions	Gabriel Kerneis

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

2014-06-10	More colors	Gabriel Kerneis

2014-06-09	Better, colored hole	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 more stops in interpreter (stopping just at the point of each internal ↵	Kathy Gray
	function call) Also turning off an annoying printf I left in.
2014-06-09	Working towards evaluating with interp_exhaustive	Kathy Gray

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-09	Merge branch 'for-dagstuhl' into master	Gabriel Kerneis
	Conflicts: src/lem_interp/interp_lib.lem src/lem_interp/run_interp.ml Remove "to_vec_safe" work-around
2014-06-07	Add optional overloading on expected return type to fix bug in constraint ↵	Kathy Gray
	solving; get test_power running again by supporting the correct operations and bit operations
2014-06-07	exts returns bit[64] instead of nat	Gabriel Kerneis
	Update power.sail to new, pretty-printer-based version
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-07	Print holes as [x]	Gabriel Kerneis

2014-06-07	Fix E_vector_append in interp pretty-printer	Gabriel Kerneis

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

2014-06-06	Improve work-around	Gabriel Kerneis
	Default to 64 bit for vec + range
2014-06-06	Add a pretty-printer for Interp_ast	Gabriel Kerneis
	Copy-pasted with a few tweaks from Pretty_printer. Should really make a functor instead, but not sure how to deal with E_internal_cast yet. Note that Interp_ast and Ast are not generated from the same ott file (resp. l2.ott and l2_type.ott), but they are close enough that the code almost "just works".
2014-06-05	Enable single-stepping for test/power.sail	Gabriel Kerneis

2014-06-05	Refactor to_vec and add work-around to avoid truncation	Gabriel Kerneis

2014-06-04	Fixup type coercions and overloading	Kathy Gray
	Reduce the number of implicit coercions we're doing, expanding overloading and fixing up types of functions. Warning: test_power does not run as not all overloaded funcitons are implemented Warning: vector concatenation does not pretty print to sail source yet
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-22	A (hopefully) sufficient interface and implementation between memory and the ↵	Kathy Gray
	interpreter
2014-05-21	correct accidental capitalization of Interp in file name	Kathy Gray

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

2014-05-20	More interface	Kathy Gray

2014-05-14	More interface update for connecting externally (interp_interface provides ↵	Kathy Gray
	functions for connecting the interpreter to a memory model) Also adding default values to index vectors for supporting sparse vectors/maps
2014-05-12	More interface support	Kathy Gray