sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2014-04-15	Put conditional path information into constraint gathering so that checking ↵	Kathy Gray
	uses appropriate information gleaned from pattern matching
2014-04-10	more constraint resolution; and turning off some assert falses until I find ↵	Kathy Gray
	out why unification isn't being forced everywhere it needs to
2014-04-08	Reduce redundant information in AST	Kathy Gray

2014-04-08	Try to reduce size of Lem output a little bit	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	Power example now EXECUTES (almost) CORRECTLY! \o/	Gabriel Kerneis
	Warning: we set the link register to the address of the first instruction, which means the program is effectively an infinite loop returning 42 forever. (Except it slows down and leaks memory, probably because the interpreter doesn't optimise the tail call in fde_loop.) 42, 42, 42, 42, 42, 42, 42, 42, ...
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	Remove workarounds and update Power model	Gabriel Kerneis

2014-04-03	Typeclass Eq for values	Gabriel Kerneis
	Again, this is necessary to compare big_int
2014-04-03	make sail backwards compatible to older ocaml again	Kathy Gray

2014-04-03	Do implicit coercions on expliciit casts	Kathy Gray

2014-04-03	Fix arity error in bitwise helper function	Kathy Gray

2014-04-03	start solving more constraints	Kathy Gray

2014-04-03	Exhibit two bugs about bitwise operators and vector casts	Gabriel Kerneis

2014-04-03	Correct types of bitwise operators	Gabriel Kerneis

2014-04-03	More constraint solving through evaluation, fix size knowledge on coercion.	Kathy Gray

2014-04-02	Fix bug that was throwing away the cast telling the interpreter to read a ↵	Kathy Gray
	register
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	Checking missing cast for register as value in testsuite	Gabriel Kerneis

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-02	Update Power model	Gabriel Kerneis

2014-04-02	Skip constraint resolution to build Power model	Gabriel Kerneis

2014-04-02	Add more information for resolving constraints involving variables; clean up ↵	Kathy Gray
	various constraint generation (removing repetitive and adding missing constraints)
2014-04-02	Add -skip_constraints to type-check without constraints	Gabriel Kerneis

2014-04-01	Allow negative "nat" internally	Gabriel Kerneis
	to_num and to_vec probably still need to be fixed
2014-04-01	Fix parsing of nexp constraints	Gabriel Kerneis

2014-04-01	More type corrections for constraints	Kathy Gray

2014-04-01	constraint corrections for to_num and to_vec	Kathy Gray

2014-03-31	Fix constraint bug with +	Kathy Gray

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-31	test/vectors.sail: failing constraint checking	Gabriel Kerneis
	Type error: Type constraint mismatch: constraint arising from here requires 0 to be greater than or equal to 32
2014-03-27	Check simple constraints (i.e. ones using only constants).	Kathy Gray
	Changes syntax of tuple type from * to , so that nexps of the form 8 * 'n can be supported in the parser, which was apparently not true before.
2014-03-26	More steps towards solving and using constraint information	Kathy Gray

2014-03-26	Steps towards solving constraints	Kathy Gray

2014-03-23	adding if test	Kathy Gray

2014-03-23	Correctly unify types with default declarations and across if blocks for ↵	Kathy Gray
	introduced variables.
2014-03-23	Fix more unification bugs	Kathy Gray

2014-03-20	reset earlier commits to test3, that were supposed to be chosen instead of ↵	Kathy Gray
	my changes in the conflict resolution but oops.
2014-03-20	small test changes	Kathy Gray

2014-03-20	Fix type checking bug that was incorrectly unifying type variables, leading ↵	Kathy Gray
	function 'a id x = x to have type 'a 'b . 'a -> 'b
2014-03-20	Type bit[n] means bit[0..n-1]	Gabriel Kerneis

2014-03-20	Add missing GPR registers for Power example	Gabriel Kerneis
	Second instruction now executes (but probably not correctly, check arithmetic since we ignore exts). Next step is to implement bitwise_or.
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	Fix default type env	Gabriel Kerneis

2014-03-20	More tests for implicit casts	Gabriel Kerneis
	The last test added in vectors.sail fails.
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).