sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
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)
2014-03-11	More work on interpreter and Power model	Gabriel Kerneis

2014-03-11	Confusion between first index and vector length	Gabriel Kerneis

2014-03-11	Increase support for register "field" accesses; there is now a bug in how ↵	Kathy Gray
	run_interp handles SubReg register forms.
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-03-04	More polymorphism for addition	Gabriel Kerneis

2014-03-03	Fixing assorted bugs. Adding ability to put a type on the identifier being ↵	Kathy Gray
	assigned to in assignments.
2014-03-01	Fix printing bug on vector slicing that caused only one element to ever be ↵	Kathy Gray
	sliced
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	Fetch-decode POWER interpreter	Gabriel Kerneis
	Many limitations and bugs currently, but loads binary and decodes opcodes correctly (using endianness hacks). Disabled in the default test suite (but still compiled), run "make test_power" to try it.
2014-02-28	Load ELF sections to virtual memory addresses	Gabriel Kerneis
	Roughly 110KB/s (~5 seconds to load "hello" test).
2014-02-27	Fix error to constructor pattern matching	Kathy Gray

2014-02-27	Partial fix for to_vec_inc/to_vec_dec	Gabriel Kerneis
	Lem's word library does some dark magic because of its assumption that words represent signed integers. Therefore, it is unreliable to truncate words, as well as to use the internal representation. boolListFrombitSeq seems safe for our purposes, though (provided the bitseq has been created with an infinite length from a positive integer).
2014-02-27	More flexible test execution	Gabriel Kerneis

2014-02-27	Merge branch 'interp_typed'	Kathy Gray
	Conflicts: src/lem_interp/interp.lem src/lem_interp/run_interp.ml
2014-02-26	Get interpreter working using types, no added functionality yet	Kathy Gray

2014-02-26	Debug and fix memory multi-bytes memory writes	Gabriel Kerneis

2014-02-26	Fix vector slicing	Gabriel Kerneis

2014-02-25	Manage annot	Kathy Gray

2014-02-25	First step of using type information in interpreter. Reading and writing ↵	Kathy Gray
	plain registers supported; memory reading and writing is broken.
2014-02-21	Add type annotations to lem grammar, including printing out the annotated ↵	Kathy Gray
	ast, and extending the interpreter to expect annotations. Annotations and locations are still not used by the interpreter.
2014-02-18	Put a plaster on bug for finding memory reading/writing operations	Kathy Gray

2014-02-18	Remove spurious add infix	Gabriel Kerneis

2014-02-18	Report failing tests and return 1 in case of error	Gabriel Kerneis

2014-02-18	Improve interpreter pretty-printing	Gabriel Kerneis

2014-02-18	Adding explicit order to for loops	Kathy Gray

2014-02-14	Attempt multi-byte memory read and write	Gabriel Kerneis
	Test seems to fail for some reason, probably endianess and off-by-one bugs all over the place. Needs debugging code to monitor memory updates and display bitvectors in a compact way.
2014-02-14	Write slice to memory	Gabriel Kerneis
	I'm not sure whether this is useful at all. It is currently a bit broken when subrange is not in the "correct" order. Presumably the typechecker should catch this? I'm not quite sure what the intended semantics should be. Probably the same bug occurs with register slices too.
2014-02-14	Fix infinite loop bug, and test1.sail type checking bug	Kathy Gray

2014-02-14	Register slice write	Gabriel Kerneis

2014-02-13	Index memory with big_ints in interpreter	Gabriel Kerneis
	Also add support for sliced reads. Still need to implement sliced writes, as well as multi-word memory writes.
2014-02-13	Missing default case for literal equality test	Gabriel Kerneis

2014-02-13	Display backtrace when interpreter fails	Gabriel Kerneis

2014-02-13	Implement equality for big_int literals	Gabriel Kerneis
	Lem does not infer instances for typeclasses, falling back to unsafe comparison which does not work for big_int in OCaml.
2014-02-12	More library functions for interpreter	Gabriel Kerneis
	There is now enough stuff to decode and execute a very basic Branch instruction (encoding everything as little-endian rather than big- endian among many other work-arounds).
2014-02-12	Fix endianess issues	Gabriel Kerneis

2014-02-12	Replace nat by natural in interpreter	Gabriel Kerneis

2014-02-07	Fix a few stupid bugs	Gabriel Kerneis

2014-02-07	Implement is_one	Gabriel Kerneis

2014-02-07	Report unimplemented function name	Gabriel Kerneis

2014-02-05	Replace symbolic link by actual file	Gabriel Kerneis

2014-02-05	First bit of Power spec	Gabriel Kerneis
	Only chapter about branches (except system calls because of sail typechecking issue). Decoding seems to work. Execution typechecks currently, but is pretty surely broken otherwise.