sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2017-06-21	Pretty-print bitvector expressions	Thomas Bauereiss
	- Add case distinctions between bitvector types and vectors of other element types (e.g. registers) and use the corresponding operations (i.e. "bvslice", "bvaccess", etc for the former, and "slice", "access", etc for the latter) when pretty-printing expressions - Add type annotations to expressions when the type includes bitvectors with concretely known length - Update state.lem to use bitvectors (in the interface, at least; internally, bitvectors are still stored as bit lists for now, since that makes it easier to support storing different registers with different lengths) This has been tested with the CHERI-MIPS model with some success, but some things are still missing: - Bitvector patterns are not handled yet - Some bitvector length monomorphisation is needed in a few places of the model - Some type annotations are missing, because the (old) Sail type checker does not infer bitvector lengths in some instances where one would hope it to do that; this should be checked with the new type checker
2017-05-24	added the exmem effect for AArch64 store-exclusive	Shaked Flur

2017-03-23	the interpreter/shallow expects little-endian memory-values	Shaked Flur

2016-12-09	sail changes for making lem embedding Isabelle-friendlier	Christopher Pulte

2016-11-27	make outcome_s contain the instruction state pretty print rather than the ↵	Christopher Pulte
	instruction state, factor out interpreter/shallow embedding value conversion
2016-11-14	add option -lem_sequential for producing shallow embedding that refers to ↵	Christopher Pulte
	state monad, library fixes
2016-11-08	fixes	Christopher Pulte

2016-11-07	factor out regfp analysis types into etc/regfp.sail	Christopher Pulte

2016-10-28	shallow embedding progress	Christopher Pulte

2016-10-27	more shallow embedding fixes	Christopher Pulte

2016-10-21	shallow embedding progress	Christopher Pulte

2016-10-10	changed the way registers/register fields work, fixes, nicer names for new ↵	Christopher Pulte
	letbound variables
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-30	fixes, update isntruction_analysis for NIAs and DIA	Christopher Pulte

2016-09-25	nicer lem output: no more unecessary 'unit' returns if if-expressions, ↵	Christopher Pulte
	for-loops or case-expressions also return updated variables
2016-09-23	sail-to-lem progress	Christopher Pulte

2016-09-21	fixes	Christopher Pulte

2016-09-19	sail-to-lem progress	Christopher Pulte

2016-09-07	push some lem pp changes	Christopher Pulte

2015-12-21	fixes, pp progress	Christopher

2015-12-15	better location information	Christopher

2015-12-03	added prompt.lem for connecting to concurrency model and ↵	Christopher Pulte
	{power,armv8}_extras.lem; fixes