sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2017-12-05	Update license headers for Sail source	Alasdair Armstrong

2017-11-29	Better lem_ast tagging and interpreter tweaks	Alasdair Armstrong

2017-07-24	interpreter: optionally print debugging traces	Jon French

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-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	Christopher, Peter: make "run_interp_model.ml" build again (endianness)	Peter Sewell

2017-02-03	fix headers	Peter Sewell

2016-10-17	updates for ppcmem printing	Kathy Gray

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-14	Add memory kind for concurrent tag reads and writes	Kathy Gray

2016-09-14	Change reading and writing of tag memory to report the tag/look for the tag ↵	Kathy Gray
	as the first byte of the byte list on tagged memory operations
2016-09-13	Support memea and memv in sequential interpreter	Kathy Gray

2016-07-28	Banish exit from the mips/cheri sail except at end of SignalException ↵	Robert Norton
	function. There is a plan to replace this syntax with something more understandable. Should make no functional difference using sequential interpretor but will need to do some work on exception functions when integrating with ppcmem so that it know register writes are exceptional etc.
2016-06-07	Fix issue in accessing fields and slices of registers during translate address	Kathy Gray

2016-06-03	Fix bug exposed/introduced by properly handling vector starts in the type ↵	Kathy Gray
	checker
2016-04-25	Make interpreter able to read registers during translate address and decode.	Kathy Gray
	This is not yet connected to any model and not yet tested. Also, reduce the number of parentheses needed by the parser. Namely, register declarations should no longer need parens around the types and let expressions should need fewer instances of parens around the expression (i.e. let a = exp ).
2016-03-08	missing file from last commit	Kathy Gray

2016-03-08	Start task of setting up tagged memory in sequential interpreter	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	Fix some bugs in writing registers with slices in the sequential interpreter	Kathy Gray

2016-01-26	Fix problem in run_with_model where we forgot that ppcmem2 treats everything ↵	Kathy Gray
	as increasing, and updated ranges accordingly, and mistakenly were using the wrong range values for register slicing.
2016-01-20	see writes to registers in the register file for sequential interpreter	Kathy Gray

2016-01-20	Assorted bug fixes that gets one mips instruction running (then fails for ↵	Kathy Gray
	expected reasons) :)
2015-11-17	Very nearly there sequential interpreter, just need to hook in the spec ↵	Kathy Gray
	files for the different isas to support
2015-11-12	Incorporating elf into sequential interpreter	Kathy Gray
	Fix an effect bug on aliased id
2015-11-10	Make first half of sequential interpreter driver compile again	Kathy Gray

2015-04-22	Fix some interpreter bugs preventing ARM instructions from making progress	Kathy Gray

2014-11-17	Use red printing for the value in the hole from Printing_functions instead ↵	Kathy Gray
	of mangling the ascii manually
2014-11-06	Refactor printing to display the contents the [_] and to better format bit ↵	Kathy Gray
	vectors
2014-11-04	Fix setting of initial position in a vector after a slice	Kathy Gray

2014-10-30	Add parameter to interp_exhaust with type maybe (list (reg_name,value)) for ↵	Kathy Gray
	registers we might read that we want values for (particularly the PC)
2014-10-27	Correct externally visible endianness bugs	Kathy Gray

2014-10-20	Separate out printing facility from model driver into printing_functions ↵	Kathy Gray
	interface
2014-10-14	Iron out bugs in running new executable with branching; add new executable ↵	Kathy Gray
	as well.
2014-10-07	kathy,peter: making decode integration with ppcmem2 typecheck	Peter Sewell

2014-10-07	Put in type for instruction form for models; remove extra information from ↵	Kathy Gray
	Bytevectors; add place holder for memory size dependency tracking
2014-09-30	Corrected writing to register bug. Now interpreter produces same result as ↵	Kathy Gray
	gdb on actual binary for hello6
2014-08-27	Changes to get another (slightly larger) executable running;	Kathy Gray
	adding executable as a test as well
2014-08-21	Improve printing of function calls in stepper mode	Kathy Gray

2014-08-21	Allow command line interface to exhaustively evaluate the next step, ↵	Kathy Gray
	printing the events. Note: this commit switches back to a standard lem build located in ~/bitbucket/lem/lem
2014-08-20	Add ability to track register dependencies in interactive stepper; thus ↵	Kathy Gray
	testing register tracking/tainting
2014-08-19	make test_power_interactive working again; now using interp_interface ↵	Kathy Gray
	instead of internal actions
2014-08-19	Add file that actually drives command line interpreter	Kathy Gray