sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
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

2014-05-08	more interface changes	Kathy Gray

2014-05-06	Begin tie to ppcmem style actions/outcomes	Kathy Gray
	Change type of + on vectors to (bit vector,bit vector) -> bit vector
2014-05-01	Make an overloading type decision (all + operations return ranges, never ↵	Kathy Gray
	vectors) and make the test suite pass again
2014-04-30	More support for overloading functions; primarily focusing on +	Kathy Gray
	WARNING: vector test breaks due to not having implemented the full range of different + functions In general, we need to decide whether vector + vector, vector + range and range + vector should all return ranges, vectors or a mixture
2014-04-25	rename interpreter's local memory type to reflect that it's all local memory	Kathy Gray

2014-04-21	Remove unsoundness of pattern match in interpreter	Kathy Gray

2014-04-15	Use type information in vector concatenation pattern matching in interpreter.	Kathy Gray
	Does not properly bind variables (i.e. in the pattern 0b01:(bit[3]) a: 0b0001 subsequent uses of a will not be bound in the interpreter, though they are in the type checker), so until bug is fixed, treat all such identifiers as _
2014-04-08	Reduce redundant information in AST	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-03	Implement some arithmetic operations	Gabriel Kerneis

2014-04-03	Re-index vector slices	Gabriel Kerneis
	- increasing vector slices are re-indexed from 0 - decreasing vector slices are re-indexed towards 0 I don't know how the type system handles this currently, but it is essential for the correctness of execution.
2014-04-03	Implement bitwise library operations	Gabriel Kerneis

2014-04-03	Typeclass Eq for values	Gabriel Kerneis
	Again, this is necessary to compare big_int
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-04-02	eq and neq return bit, not bool	Gabriel Kerneis

2014-04-02	Fix EXTS and signedness of to_num	Gabriel Kerneis

2014-04-01	Allow negative "nat" internally	Gabriel Kerneis
	to_num and to_vec probably still need to be fixed
2014-03-31	Extend constraint checking, and add casts for base of a vector shifts (i.e. ↵	Kathy Gray
	from 0 to 32 etc, doesn't change order yet.).
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-19	Fix bug when reading register through a cast	Kathy Gray

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-12	Correctly type checking and interpreting accesses of register "fields". ↵	Kathy Gray
	Register-reading action isn't reading the subreg correctly still (seems to be making up a value though). Corrects but to vectors.sail and power.sail use of plus. (A new bug in power.sail is exposed using a binary operator with one value)