sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2019-03-15	Make mono_rewrites less dependant on ASL prelude	Thomas Bauereiss
	... so that it can be more easily used for other specs. Also add some functions to vector_dec.sail to support this.
2019-03-07	Fix bug in a mono rewrite helper function	Thomas Bauereiss

2019-02-07	Monomorphisation tweaks for v8.5	Thomas Bauereiss
	Various tweaks to the monomorphisation rewrites. Disable old sizeof rewriting for Lem backend and rely on the type checker rewriting implicit arguments. Also avoid unifying nexps with sums, as this can easily fail due to commutativity and associativity.
2019-01-29	Add a few more type annotations after mono rewrites	Thomas Bauereiss

2018-12-13	Remove redundant zero extensions more aggressively in mono rewrites	Thomas Bauereiss
	subrange_subrange_concat does a zero extension internally, so another zero extension of its result is redundant and can lead to a type error in Lem (because Lem's type system cannot calculate the length of the intermediate result of subrange_subrange_concat).
2018-12-13	Fix issue with sizeof-rewriting and monomorphisation	Alasdair Armstrong
	Sizeof-rewriting could introduce extra arguments to functions that instantiate_simple_equations could fill in with overly complicated types, causing unification to fail when building lem.
2018-08-07	Improve cast introduction for Lem	Brian Campbell
	Handles mutable variables and conditionals (there are still some corner cases that don't appear in Aarch64 to do). The pretty printer is now back to preferring to use concrete types, but has a special case for casts to print more general types.
2018-07-11	Fix off-by-one bugs in monomorphisation rewrites involving bitvector subranges	Thomas Bauereiss
	CHERI test suite now passes using Isabelle-generated emulator
2018-05-17	Clean up MIPS for HOL4 a little	Brian Campbell
	Move mono_rewrites into lib
2018-02-16	Add alternative definitions of aarch64 functions for monomorphisation	Brian Campbell

2018-02-14	Another mono rewrite for aarch64	Brian Campbell

2018-02-08	Add (most of) the bitvector cast insertion transformation	Brian Campbell
	to help Lem go from a general type `bits('n)` to a specific type `bits(16)` at a case split, and the other way around for a returned value. Doesn't handle function clause patterns yet
2018-02-02	Add arithmetic shift right for aarch64 mono	Brian Campbell

2018-01-29	Sync mono rewrites definitions with library	Brian Campbell

2018-01-26	One more mono rewrite	Brian Campbell

2018-01-19	Update monomorphisation for sail2	Brian Campbell
	(no vector type start position, comment syntax)
2018-01-16	Another useful monomorphisation rewrite	Brian Campbell

2018-01-09	More monomorphisation rewrites for aarch64	Brian Campbell

2018-01-09	Add some optional experimental rewrites to help with monomorphisation	Brian Campbell