sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2014-02-16	A bit of cleanup, including checking for loops and overloading 0 and 1 to be ↵	Kathy Gray
	bits in patterns where detectable.
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	update syntax of vector slicing.	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-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	Checking assignment to a variable	Kathy Gray

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

2014-02-12	Remove spurious declaration	Gabriel Kerneis

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

2014-02-12	Change nat to natural in ott	Kathy Gray
	Type checking now recurses through assign, but doesn’t do the proper checks yet
2014-02-11	struct/record type checking	Kathy Gray

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

2014-02-07	Most of the vector expression type checking	Kathy Gray

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-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-06	coerce bit to bool when not a literal bit. Note: this will only add a ↵	Kathy Gray
	conversion function for expressions of bit type, an explicit cast to bit would be needed to come from an enum or nat.
2014-02-06	coercians for bits to bools for literals	Kathy Gray

2014-02-06	type check more vectors	Kathy Gray

2014-02-06	push effect information around while checking expressions	Kathy Gray

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	Fix pattern constructor bug in type checking (darn tuples/not tuples)	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-02-05	Revert "Accept single bits as boolean values for if in interpreter"	Gabriel Kerneis
	This reverts commit 828f19828e41ced146f06e9a7eb4183cd9ef3ab4. It was a temporary workaround now fixed when we generate Sail code.
2014-02-05	Deinfixable colon	Gabriel Kerneis

2014-02-03	More type checking, including coercing 0 and 1 into bits when appropriate ↵	Kathy Gray
	(in limited circumstances at the moment due to which expressions are actually checked, so test files should not yet be changed)
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-30	Expression type checking, not complete	Kathy Gray

2014-01-29	Type check function headers and parameters	Kathy Gray

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	Accept single bits as boolean values for if in interpreter	Gabriel Kerneis

2014-01-15	Improve error messages	Gabriel Kerneis