sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2016-01-20	Assorted bug fixes that gets one mips instruction running (then fails for ↵	Kathy Gray
	expected reasons) :)
2016-01-20	trim some obsolete/bitrotted make stuff.	Robert Norton

2016-01-20	build all mips stuff in _build. Still hacky and might be preferable to use ↵	Robert Norton
	ocamlbuild but works OK and shouldn't have to call sanitize.
2016-01-20	Decoding a mips instruction :)	Kathy Gray
	Not executing yet as some previous commit has broken the interpreter's local assignment
2016-01-20	Show opcode in sequential interpreter when decode fails	Kathy Gray

2016-01-19	Put None and Some into interpreter environments	Kathy Gray
	Also making progress towards separating int sized things from integer sized things
2016-01-19	hacky initial makery for mips interpreter. Builds stuff in wrong places and ↵	Robert Norton
	needs fixing but nearly works.
2016-01-14	small edit to previous commit	Kathy Gray

2016-01-14	Fix cumulative effects for circumstance when lifting variable introductions ↵	Kathy Gray
	out of an if Note: this fixes the local cumulative effects for the e_assign and e_if, it may not properly propagate them to the context of the surrounding block
2016-01-13	Closes issue #28 and issue #27	Kathy Gray
	Note: also adds a most_significant function to the standard library, that returns the lowest indexed bit in a inc bit vector and the biggest indexed bit in a dec bit vector.
2016-01-12	Fix undefined nvar occurrences that were impacting ARM	Kathy Gray

2016-01-11	Interpreter interface now supports option<ast> result from decode and etc ↵	Kathy Gray
	instead of looking for exit calls
2016-01-11	Interpreter that understands assert	Kathy Gray

2016-01-07	Add E_assert to basic rewriters	Kathy Gray

2016-01-06	Add new assert expression to Sail	Kathy Gray
	This splits the former functionality of exit into errors, which should now use assert(bool,option<string>), and a means of signalling actions such as instruction-level exceptions, interrupts, or other features that impact the ISA. The latter will now be tracked with an effect escape, and so any function containing exit and declared pure will generate a type error. WARNING: ARM spec will not build with this commit until I modify it. MIPS spec will not build with this commit until modified.
2015-12-22	More make file goo, and fixing a typo in run_with_elf	Kathy Gray

2015-12-22	More gluing mips to interpreter	Kathy Gray

2015-12-22	Add mips64 to get_elf in Makefile	Robert Norton

2015-12-21	Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2	Christopher

2015-12-21	fixes, pp progress	Christopher

2015-12-17	Remove external functions that the library provides, having added them to ↵	Kathy Gray
	the type environment finally. (Also small cleaning of the new makefile)
2015-12-16	Fix a bug in checking vector accesses and ranges that was hiding some bugs, ↵	Kathy Gray
	and causing some incorrect lem_ast generation in mips code
2015-12-16	rewriter and pp changes for generating ARM output	Christopher

2015-12-15	better location information	Christopher

2015-12-14	Adding new location constructor for location of generated terms	Kathy Gray

2015-12-10	fix	Christopher

2015-12-09	adapted for Kathy's lexp effect typing changes: register writes should be ↵	Christopher
	correct now, fixes, pp
2015-12-09	Fix overlooked case of effect tagging for sub register writes. Close issue ↵	Kathy Gray
	#23 again
2015-12-08	wreg effects and tags now proper for LEXP_field, LEXP_vector ↵	Kathy Gray
	LEXP_vector_range for sub register writes. Closes issue #23
2015-12-08	Some easy fixes to vector and list type inference. Closes issue #25 and ↵	Kathy Gray
	issue #26
2015-12-07	Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2	Christopher

2015-12-07	adapted pp for Kathy's effect type changes	Christopher

2015-12-07	Interpreter working again with updated tag, effects, and types behaviour	Kathy Gray

2015-12-07	Reading of register slices and bits should now be tagged and effect ↵	Kathy Gray
	annotated properly, as well as field accesses. Writing of register slices and bits still look like writes of full registers from tags and effects (probably, if it works, it's an accident) WARNING: interpreter still not up to date with this change
2015-12-04	First bit of making tags and effects on sub vector accesses work for static ↵	Kathy Gray
	compilation. So, it should be right for E_field, but isn't right for E_vector_access, and hasn't begun for E_vector_subrange Isn't right for any writes WARNING lem ast files generated from this may not have the proper behaviour on field accesses.
2015-12-03	added prompt.lem for connecting to concurrency model and ↵	Christopher Pulte
	{power,armv8}_extras.lem; fixes
2015-11-25	non-working sail/mips interpreter integration for kathy to look at and ↵	Robert Norton
	example mips elf file.
2015-11-25	fixes, pp	Christopher Pulte

2015-11-24	Fixup effect equality bug introduced by adding e_escape	Kathy Gray

2015-11-24	Add BE_escape effect when an E_exit is seen	Kathy Gray
	Close #20
2015-11-22	do effect annotation updates more systematically, fix dedup	Christopher Pulte

2015-11-20	Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2	Christopher Pulte

2015-11-20	no more unecessary variables from removing vector-concatenation pattern ↵	Christopher Pulte
	matches, reset variable name counter for each function clause, fixes
2015-11-20	make the abis directory as well	Kathy Gray

2015-11-20	fixes to get-elf to work on linux. Hope it works on Mac too.	Robert Norton

2015-11-19	Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2	Christopher Pulte

2015-11-19	fixes for cumulative effect anotations	Christopher Pulte

2015-11-19	Keep up with linksem	Kathy Gray

2015-11-19	More makefile type	Kathy Gray

2015-11-19	typo in make file	Kathy Gray