sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2017-09-29	fix those build errors	Christopher Pulte

2017-09-29	fix deep_shallow_convert, stop using interp_interface.instruction for most ↵	Christopher Pulte
	things, SF and CP bugfixing
2017-09-26	fixes	Christopher Pulte

2017-09-21	wib	Shaked Flur

2017-09-21	added a comment to the x86 lock'd read and write	Shaked Flur

2017-09-20	add support for x86 lock prefix (also remove unused Read/Write_tag kind in ↵	Robert Norton
	etc/regfp.sail.
2017-09-19	fix	Christopher Pulte

2017-09-15	x86: implement regfp analysis function (no control flow yet)	Robert Norton

2017-09-15	reinstate deep/shallow conversion	Christopher Pulte

2017-09-03	added RISC-V strong-acquire/release	Shaked Flur

2017-08-31	add EnumerationType type class: if a type is a member you get Ord membership ↵	Christopher Pulte
	and Set membership for free
2017-08-31	added RISC-V AMOs	Shaked Flur

2017-08-30	typeclass instance Ord(opcode)	Christopher Pulte

2017-08-24	typo	Shaked Flur

2017-08-24	typo	Shaked Flur

2017-08-24	added barrier-kind for x86 MFENCE;	Shaked Flur
	fixed some compare functions;
2017-08-22	Merge branch 'master' of https://bitbucket.org/Peter_Sewell/sail	Christopher Pulte

2017-08-22	and fix that other places	Christopher Pulte

2017-08-22	added RISC-V "fence w,w" and "fence.i";	Shaked Flur
	fixed the interpreter nias analysis;
2017-08-22	adapt state.lem to RISCV additions	Christopher Pulte

2017-08-19	RISC-V store-release	Shaked Flur

2017-08-17	added RISC-V load-acquire	Shaked Flur

2017-08-17	fixed the RISC-V fences (3 types: "rw,rw"/"r,rw"/"rw,w")	Shaked Flur

2017-08-16	lem_interp: remove broken val_to_string_internal functions, replace with ↵	Jon French
	string_of_value as used everywhere else
2017-08-12	Resolve ambiguity between negation of integers and bools	Thomas Bauereiss

2017-08-12	Fix compilation issue for 32-bit systems	Thomas Bauereiss

2017-08-02	fix sail library test interpreter glue for API change. Also fix ↵	Robert Norton
	build_context val spec which was out of dated although lem did not complain for some reason...
2017-08-02	fix run_with_elf*.ml with changed lem_interp api	Jon French

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-07-19	split library tests into separate files to avoid risk of sail compiler stack ↵	Robert Norton
	overflow.
2017-07-19	borrow some of aa's bash code to convert library test suite output to junit ↵	Robert Norton
	xml for jenkins.
2017-07-06	Tests for (almost) all sail builtins. Many interesting things discovered. ↵	Robert Norton
	Library in need of rationalisation.
2017-07-06	fix off by one in type of add_vec builtin function. There are many more ↵	Robert Norton
	dubious types but will wait for library rationalisation to fix.
2017-07-06	fix interpreter version of get_min/max_representable which similarly broken ↵	Robert Norton
	to ocaml version. TODO: also fix copies in sail_values.lem and sail_values_word.lem.
2017-07-06	fix interpreter lteq/gteq for range/vec.	Robert Norton

2017-07-06	fix interpreter version of != which was broken for vector/range comparisons.	Robert Norton

2017-07-06	substitute all uses of mod_big_int and div_big_int for Z.rem and Z.div which ↵	Robert Norton
	have correct rounding behaviour. Missed these when changing quot and mod functions.
2017-07-06	implement abs function correctly for ocaml shallow embedding.	Robert Norton

2017-07-06	fix dodgy get_min/max_representable functions. Looks like an attempt at ↵	Robert Norton
	optimisation went wrong.
2017-07-04	further testing of sail library.	Robert Norton

2017-06-30	add more tests for sail library. Can't compile entire file due to sail ↵	Robert Norton
	performance bug or infinite loop. Add some missing shallow embedding funcitons.
2017-06-29	beginnings of a sail library test suite.	Robert Norton

2017-06-22	fix three different copies of the hardware_quot function to do proper ↵	Robert Norton
	trucation towards zero. Previous version was incorrect if result was exact and a<0 and b>0.
2017-06-22	add a 'print' built-in function handy for writing sail tests.	Robert Norton

2017-06-14	Add a work-in-progress version of sail_values.lem	Brian Campbell
	that uses the new Lem machine words library.
2017-06-05	Attempt to make Lem-prettyprinting of function clauses more robust	Thomas Bauereiss
	Instead of abusing patterns as expressions, bind patterns to names (if they are more complex than an identifier or literal and don't have a name already) and generate expressions referring to those names (which we then pass as arguments to the auxiliary functions).
2017-06-05	Fix pretty-printing of function clauses with wildcards for Lem	Thomas Bauereiss
	Before, wildcards sometimes ended up in the arguments to the function call on the RHS, in particular when using vector patterns (which implicitly introduce wildcards for the order and index parameters).
2017-06-02	Add tag memory to Lem shallow embedding	Thomas Bauereiss