sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2017-12-06	Add top-level pattern match guards internally	Brian Campbell
	Also fix bug in mono analysis with generated variables Breaks lots of typechecking tests because it generates unnecessary equality tests on units (and the tests don't have generic equality), which I'll fix next.
2017-12-05	Update license headers for Sail source	Alasdair Armstrong

2017-11-30	Merge branch 'master' into experiments	Alasdair Armstrong

2017-11-17	Fix interpreter to work with new typechecker	Alasdair Armstrong
	Need to map sail type annotations to interpreter type annotations in lem_ast ouput. This doesn't seem too hard.
2017-09-29	fix deep_shallow_convert, stop using interp_interface.instruction for most ↵	Christopher Pulte
	things, SF and CP bugfixing
2017-07-24	interpreter: optionally print debugging traces	Jon French

2017-07-24	vector parts of interpreter now evaluate all arguments of expression before ↵	Jon French
	exiting due to one of them being unknown; fixes incorrect exhaustive analysis for footprints
2017-07-24	move value type definitions to ott, and introduce new E_internal_value ast ↵	Jon French
	node for passing around encapsulated evaluated values; change Interp.to_exp to now just wrap values in this node
2017-05-28	fixed exmem	Shaked Flur

2017-05-24	Merge branch 'master' of bitbucket.org:Peter_Sewell/sail	Shaked Flur
	# Conflicts: # src/lem_interp/interp.lem # src/lem_interp/interp_inter_imp.lem # src/lem_interp/interp_interface.lem # src/parser.mly # src/pretty_print_lem.ml
2017-05-24	added the exmem effect for AArch64 store-exclusive	Shaked Flur

2017-05-24	Change types of MEMr_tag, MEMval_tag and co. so that tag is separate from ↵	Robert Norton
	data and invent rmemt and wmvt effects for them. Extend the interpreter context to include lists of tagged memory read and write functions. The memory model must round down the address to the nearest capability aligned address when reading/writing tags. Remove TAGw which is no longer needed as a result.
2017-03-24	Print tracking information for V_track, hopefully fix extern_vector_value, ↵	Christopher Pulte
	fix sail_values bug.
2017-02-03	fix headers	Peter Sewell

2017-01-25	Make interpreter a little more flexible on the format of a register type to ↵	Kathy Gray
	match ASL; add missing functions/cases to library
2017-01-23	remove taint printing	Kathy Gray

2017-01-23	Extend lib with min and max	Kathy Gray

2016-11-23	Add new type checking file. Small changes to type inference, temporary ↵	Kathy Gray
	change to printing
2016-11-09	move decode_error type back to Sail_impl_base for now	Christopher Pulte

2016-11-08	fixes	Christopher Pulte

2016-10-25	Improve pattern match failure error messages	Kathy Gray

2016-10-22	fixes, Interp.value printing for debugging	Christopher Pulte

2016-10-21	shallow embedding progress	Christopher Pulte

2016-10-06	move type definitions that both interpreter and shallow embedding use to ↵	Christopher Pulte
	sail_impl_base, add sail_impl_base.outcome, add interp_inter_imp auxiliary functions, make prompt use sail_impl_base.outcome
2016-09-13	Add optional address to memv events	Kathy Gray

2016-09-09	minor fixes	Kathy Gray

2016-08-17	tuple assignment now implemented so (a,b) := foo() will now work	Kathy Gray

2016-08-17	Fix pattern match bug in interp where vector accesses were using the wrong ↵	Kathy Gray
	start index
2016-08-14	Add missing case to replicate	Kathy Gray

2016-07-26	And fix abbrev oversite in interpreter	Kathy Gray

2016-07-25	Actually fix stack for return	Kathy Gray

2016-07-25	Fix stack for return	Kathy Gray

2016-07-23	Add a return exp form to Sail, supported in type checker and in interpreter.	Kathy Gray
	TODO: add an event for a return so that rewriters can find and remove them as needed for OCaml and Lem
2016-06-03	Fix bug exposed/introduced by properly handling vector starts in the type ↵	Kathy Gray
	checker
2016-06-03	turn off debug print statements	Kathy Gray

2016-06-03	Mips file: removed some unnecessary parenthesis	Kathy Gray
	Interp: trying to add some debugging to isolate bug
2016-05-09	Reverse the list of events to respect their order	Kathy Gray

2016-05-09	Add more debugging information for vector concatenation	Kathy Gray

2016-04-19	Make value treatment on memory write calls uniform for function call vs ↵	Kathy Gray
	assignment expression
2016-04-18	More fixes to interp with regards to warnings and debugging info	Kathy Gray

2016-04-13	Remove some warnings, in progress.	Kathy Gray

2016-03-30	Small missing cases in patterns	Kathy Gray

2016-01-28	Support exit and assert better in sequential interpreter and general ↵	Kathy Gray
	interpreter interface
2016-01-27	Make mips build again	Kathy Gray
	Make quiet mode for sequential interpreter not print
2016-01-26	Stop turning all decreasing vectors into indexed ones : i.e. let's print ↵	Kathy Gray
	them sensibly at last
2016-01-26	Fix some bugs in writing registers with slices in the sequential interpreter	Kathy Gray

2016-01-20	Assorted bug fixes that gets one mips instruction running (then fails for ↵	Kathy Gray
	expected reasons) :)
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-19	Put None and Some into interpreter environments	Kathy Gray
	Also making progress towards separating int sized things from integer sized things
2016-01-11	Interpreter that understands assert	Kathy Gray