sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
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-28	Correct bug in parsing and handling a['a:'b] types	Kathy Gray

2014-02-27	Load POWER binary into interpreter's memory	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-25	Sensible types for POWER registers	Gabriel Kerneis

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-15	Full type checker. No constraint checking in place.	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	Infinite loop in interpreter for register slice write	Gabriel Kerneis
	I believe the issue is on the Lem side, but I might be doing something wrong on the OCaml side too.
2014-02-14	Register slice write	Gabriel Kerneis

2014-02-13	Disable line which does not typecheck in test1	Gabriel Kerneis
	We need to fix that one, but I don't know if the bug is in test1 or in the type checker.
2014-02-13	Add definition of ignore to make tests executable	Gabriel Kerneis

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	Checking assignment to a variable	Kathy Gray

2014-02-12	Remove spurious declaration	Gabriel Kerneis

2014-02-12	Fix type errors in power.sail	Gabriel Kerneis

2014-02-07	type checking switch/case expressions	Kathy Gray

2014-02-07	Implement is_one	Gabriel Kerneis

2014-02-07	Correct variable-name bug that was throwing away type checking coercions and ↵	Kathy Gray
	type annotations
2014-02-07	more checking	Kathy Gray

2014-02-07	Use bit->bool coercion for power.sail	Gabriel Kerneis

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

2014-02-05	Test scattered typedef cross-reference	Gabriel Kerneis

2014-02-05	Fix type id parsing error ans associated type checking bugs in scattereds	Kathy Gray

2014-02-05	Typechecking lets, concrete vectors, and function calls (minus effects)	Kathy Gray

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.
2014-02-05	Adding failing typechecking test	Gabriel Kerneis
	File "test/test1.sail", line 27, character 22 to line 27, character 26 Type error: Type mismatch :(6() * ) , bit
2014-01-31	More type checking and conversions	Kathy Gray
	(Temporarily turning off unbound identifier checks, until all variable-introducing forms are checked)
2014-01-17	Type check through type definitions and val specifications, building ↵	Kathy Gray
	definition environment. Skipping function definition, let bind, and expression checking for this commit (to come).
2014-01-15	Test indexed match	Gabriel Kerneis

2014-01-14	Fix vector concat pattern matching	Gabriel Kerneis
	The concatenation list was reversed.
2014-01-09	Fixed a single-argument tuple bug on function calls	Kathy Gray

2014-01-09	Fixed bug in resuming after an action (which was manifesting as an apparent ↵	Kathy Gray
	pattern match bug, which was actually working fine).
2014-01-08	More tests for various vector patterns bugs	Gabriel Kerneis

2014-01-08	Between Scylla and Charybdis	Gabriel Kerneis

2014-01-08	Fix pretty-printing of switch-cases	Gabriel Kerneis
	Weird bug, cf. test/pattern.sail.
2014-01-07	Add first operationnal tests for vectors	Gabriel Kerneis

2014-01-07	bug: unbound let-defined (and local?) variables	Gabriel Kerneis
	In test/test1.sail, trying to resolve variable v1 in main yields: test1: error: unbound identifier
2014-01-07	Add bit and bitvector literal test	Gabriel Kerneis

2013-12-16	minor wip on tiny model	Gabriel Kerneis

2013-12-13	Fix effect annotation pretty-printing	Gabriel Kerneis
	There is also a bug for parsing effect annotations (in fundecl). But for some reason, my fix for the parser does not work: test/test2.sail still refuses to parse (chokes on "effect pure"), even with "Effect" added to parser.mly.