sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2017-08-15	fix incorrect mnemonic for lui	Robert Norton

2017-08-15	riscv: fix word/half backwards in load.	Robert Norton

2017-08-15	riscv: limit stores to only relevant bytes.	Robert Norton

2017-08-14	add risc-v fence instruction as re-using MIPS sync for now. Also place ↵	Robert Norton
	holders for FENCE.I and ECALL.
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-11	further riscv rmem integration.	Robert Norton

2017-08-08	work on integrating risc-v model with rmem (incomplete).	Robert Norton

2017-08-08	work around missing >=_u in sail.	Robert Norton

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	add .merlin file	Jon French

2017-08-02	fix run_with_elf*.ml with changed lem_interp api	Jon French

2017-07-27	implement RV64I based on version 2.0 user spec.	Robert Norton

2017-07-26	mips_extras.lem: fix references to Interp.V_foo	Jon French

2017-07-26	Merged in ojno/sail (pull request #1)	Jonathan French
	Footprint exhaustive evaluation fixes Approved-by: Jonathan French <me@jonathanfrench.net>
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-21	remove -merge true from ott makefile -- lem at least doesn't build with it	Jon French

2017-07-21	l2.ott: port across additions to base_effect from rmem	Jon French

2017-07-21	l2.ott: factor ocaml 'l' type reference into ott definition of 'l'	Jon French

2017-07-21	l2.ott, l2_parse.ott: remove unnecessary 'type text = string'	Jon French

2017-07-20	add new CNEXEQ instruction.	Robert Norton

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-07-04	change to cgettype -- returns -1 if not sealed instead of 0.	Robert Norton

2017-07-03	Update to copytype and ccseal -- now use belt and braces approach when ↵	Robert Norton
	handling unsealed capabilities by clearing tag and setting cursor to -1. Also CCSeal got an encoding.
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-22	fix a typo spotted in CPtrCmp instruction -- CLEU was using signed ↵	Robert Norton
	comparison instead of unsigned.
2017-06-22	revised ccopytype with check for offset being in bounds and clearing tag ↵	Robert Norton
	instead of using magic value if unsealed. Also corresponding CCSeal instruction which degrades to a cmove if ct.tag is unset.
2017-06-16	prefer arithmetic on integers followed by cast to bit[64] in CCopyType.	Robert Norton

2017-06-16	remove unnecessary local variable definitions copy and pasted from cbuildcap.	Robert Norton

2017-06-16	fix previous commit so that it builds.	Robert Norton

2017-06-16	implement new CBuildCap and CCopyType instrucitons for ISAv6.	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-13	Add Makefile and ROOT for Isabelle library	Thomas Bauereiss

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).