sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2017-04-06	Implement exit by raising Sail_exit exception	Robert Norton

2017-04-03	Rename TranslateAddress to TranslatePC and remove the accessType argument -- ↵	Robert Norton
	it is only ever used for translating the PC.
2017-03-30	Make length function return big_int	Robert Norton

2017-03-29	change reqiured to work with little endian interpreter.	Robert Norton

2017-03-29	Factor out pretty printers into separate files. Hopefully this will make ↵	Robert Norton
	searching easier.
2017-03-28	temporary fix for problem duplicate (lack of direction) -- assume decreasing ↵	Robert Norton
	for mips compatibility.
2017-03-28	Fix erroneous bitwise xor.	Robert Norton

2017-03-27	fix bitshift operators. I think these should be independent of vector order...	Robert Norton

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.