sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2017-03-27	Fix broken to_vec of negative values. Old code was a bit confused. Probably ↵	Robert Norton
	possible to rewrite using arithmetic on big_int which might be faster.
2017-03-25	endianness fix	Shaked Flur

2017-03-24	fixed endianness	Shaked Flur

2017-03-24	Checkpoint work-in-progress mips sequential interpreter using ocaml shallow ↵	Robert Norton
	embedding.
2017-03-24	changes to ocaml pp to allow mips->ocaml to compile	Robert Norton

2017-03-24	Christopher, Peter: make "run_interp_model.ml" build again (endianness)	Peter Sewell

2017-03-24	Print tracking information for V_track, hopefully fix extern_vector_value, ↵	Christopher Pulte
	fix sail_values bug.
2017-03-23	the interpreter/shallow expects little-endian memory-values	Shaked Flur

2017-03-02	tweak comments	Peter Sewell

2017-02-14	remove the -i option	Peter Sewell

2017-02-14	tidy command-line options	Peter Sewell

2017-02-09	wib	Peter Sewell

2017-02-09	group initial type environment into meaningful sections; pretty-print in ↵	Peter Sewell
	user-readable way
2017-02-09	tweak pp of initial type environment and l2.ott comments	Peter Sewell

2017-02-08	put back the header into Sail_impl_base	Christopher Pulte

2017-02-08	pull in Shaked's type class instance changes, fix Ord and Eq instances	Christopher Pulte

2017-02-05	command-line option to dump initial type environment	Peter Sewell

2017-02-03	replace bit vector return types in getCapX functions with equivalent integer ↵	Robert Norton
	range types. This removes quite a few uses of unsigned() in cheri intsruction pseudocode. Could potentially take things furter.
2017-02-03	fix headers	Peter Sewell

2017-02-03	licensing	Peter Sewell

2017-02-01	document coercions	Peter Sewell

2017-02-01	fix up uint type bounds	Kathy Gray

2017-01-31	Kathy, Peter: pp of initial type environment	Peter Sewell

2017-01-27	fix right shift	Kathy Gray

2017-01-27	failing test with c128	Robert Norton

2017-01-26	c128: xor E with 48 when storing in memory so that null cap is all zeros but ↵	Robert Norton
	has non-zero E (latest spec.)
2017-01-26	christopher, kathy, peter: hacky experiment on nias_of_instruction	Peter Sewell

2017-01-25	Merge branch 'master' of https://bitbucket.org/Peter_Sewell/sail	Kathy Gray

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-25	merge cheri 256 and 128 together factoring out differing parts into separate ↵	Robert Norton
	cheri_prelude files.
2017-01-25	Merge branch 'master' of https://bitbucket.org/Peter_Sewell/sail	Kathy Gray

2017-01-25	Make vector equality remember about the possibility of unknown values	Kathy Gray

2017-01-24	Merge branch 'master' of https://bitbucket.org/Peter_Sewell/sail	Christopher Pulte

2017-01-24	functionality for comparing handwritten analysis function with exhaustive ↵	Christopher Pulte
	interpreter
2017-01-24	first pass at cheri128 sail.	Robert Norton

2017-01-24	Remember to pass through collapse argument in else case in bit_lifteds_to_string	Robert Norton

2017-01-23	remove taint printing	Kathy Gray

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

2017-01-14	update pretty printing to actually reflect lem ast changes	Kathy Gray

2017-01-14	changes to enable interpreter exhaustive analysis in ppcmem again	Christopher Pulte

2017-01-12	Adding sample generated power file	Kathy Gray

2017-01-07	Turn back on resolving branch nexp unification more than once. This is the ↵	Kathy Gray
	right thing to do because otherwise the order of the resolution of branch constraints matters, and that's not easily controllable. This will require figuring out why it's infinite looping for ASL's checking rather than just turning it off.
2016-12-12	pp fix	Christopher Pulte

2016-12-12	cheri sail export progress	Christopher Pulte

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

2016-12-08	add target for building cheri_notlb.lem	Robert Norton

2016-12-02	fix interpreter build following refactoring	Robert Norton

2016-12-01	move interpreter-specific types from Sail_impl_base to Interp_interface	Christopher Pulte

2016-11-30	shallow embedding fix, rename 'copy' to 'reset_vector_start', don't print ↵	Christopher Pulte
	shallow/deep ast conversion type class instances anymore, add herdtools ast / shallow ast conversion functions, add mips ImplementationDefinedStopFetching instruction
2016-11-30	add new barrier kind for MIPS (only one for now).	Robert Norton