sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2017-08-10	Add support for early return to Lem backend	Thomas Bauereiss
	Implemented using the exception monad, by throwing and catching the return value
2017-08-09	Pretty-print some more type annotations	Thomas Bauereiss

2017-08-08	Fix Lem bindings in test cases	Thomas Bauereiss
	Add a test case with the MIPS spec using the TLB stub. Use the sequential monad for Lem testing for now; the free monad (in "prompt.lem") has not been updated for machine words yet.
2017-08-08	Glue together Sail prelude and Lem library	Thomas Bauereiss

2017-08-08	Various fixes and improvements for the Lem pretty-printing	Thomas Bauereiss
	- Add some missing "wreg" effect annotations in the type checker - Improve pretty-printing of register type definitions: In addition to a "build" function, output an actual type definition, and some getter/setter functions for register fields - Fix a bug in sizeof rewriting that caused it to fail when rewriting nested calls of functions that contained sizeof expressions - Fix pretty-printing of user-defined union types with type variables (cf. test case option_either.sail) - Simplify nexps, e.g. "(8 * 8) - 1" becomes "63", in order to be able to output more type annotations with bitvector lengths - Add (back) some support for specifying Lem bindings in val specs using "val extern ... foo = bar" - Misc bug fixes
2017-08-08	Add x86 decoder.	Anthony Fox

2017-08-08	Add add_typ_var to mli file	Alastair Reid
	This function is used by asl_to_sail2.ml
2017-08-07	Fixed pretty printing of E_cons	Alasdair Armstrong

2017-08-07	Merge branch 'sail_new_tc' of https://bitbucket.org/Peter_Sewell/sail into ↵	Alasdair Armstrong
	sail_new_tc
2017-08-07	Fixed various issues regarding typechecking lists.	Alasdair Armstrong

2017-08-07	Merged in acjf3/sail/sail_new_tc (pull request #2)	Anthony Fox
	Initial commit of x86 model (ported from L3).
2017-08-07	Initial commit of x86 model (ported from L3).	Anthony Fox

2017-08-02	Fix run_tests.sh so it cleans up generated ml files when testing ocaml backend	Alasdair Armstrong

2017-08-02	Improve pretty-printing of register declaration and assignment	Thomas Bauereiss

2017-08-02	Tune vector_subrange	Thomas Bauereiss

2017-08-02	Add debugging option to dump AST after rewriting steps	Thomas Bauereiss

2017-08-01	Add missing lexp case to Ocaml pretty-printer	Thomas Bauereiss

2017-08-01	Added ocaml generation to run_tests.sh	Alasdair Armstrong

2017-08-01	Fixed a bug where type_synonyms were not being expanded properly when ↵	Alasdair Armstrong
	considering possible casts
2017-08-01	Fixed a bug where as patterns weren't binding their variable correctly	Alasdair Armstrong

2017-08-01	Added more patterns to ast_util and improved type checking of patterns	Alasdair Armstrong

2017-08-01	Remove some hardcoded calls to obsolete Lem library functions	Thomas Bauereiss

2017-08-01	Fix some effect propagation bugs in rewriter	Thomas Bauereiss

2017-07-28	Add true and false to n_constraint language. Also small tweaks for ASL ↵	Alasdair Armstrong
	generation.
2017-07-27	Rewrite guarded patterns for Lem backend	Thomas Bauereiss

2017-07-27	Add cons patterns to pretty-printers	Thomas Bauereiss

2017-07-27	Merge branch 'sail_new_tc' of https://bitbucket.org/Peter_Sewell/sail into ↵	Alasdair Armstrong
	sail_new_tc
2017-07-27	Merge branch 'master' into sail_new_tc	Alasdair Armstrong

2017-07-27	Some more test cases	Alasdair Armstrong

2017-07-27	Parameterise convert_ast by the bitvector order	Alasdair Armstrong

2017-07-27	Fixed a bug where sail would run out of file descriptors when passed a large ↵	Alasdair Armstrong
	number of files
2017-07-27	P_cons in monomorphisation	Brian Campbell

2017-07-27	Fix up constructor handling in monomorphisation	Brian Campbell

2017-07-27	Mirror AST change	Brian Campbell

2017-07-27	Add test cases for overlapping record field names	Alasdair Armstrong

2017-07-27	Allow local mutable records, and fix bugs with overlapping record field names.	Alasdair Armstrong

2017-07-27	Fixed bug with pattern synonyms in Cons and List patterns	Alasdair Armstrong

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

2017-07-26	Add right shift to lib/prelude.sail, and add case for E_exit in ↵	Alasdair Armstrong
	Ast_util.string_of_exp
2017-07-26	Allow arbitrary identifiers in nexp expressions	Alasdair Armstrong
	Fixed some bugs in the initial check that caused valid code to fail to parse Add a nid utility function that creates an id n-expression, similar to nvar, nconstant etc
2017-07-26	mips_extras.lem: fix references to Interp.V_foo	Jon French

2017-07-26	Interpreter doesn't build with new typechecker + changes from master	Alasdair Armstrong
	Makes it so that the jenkins buildserver will only try to build sail and not the interpreter for sail_new_tc
2017-07-26	Merge remote-tracking branch 'origin/master' into sail_new_tc	Alasdair Armstrong

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-26	Improve rewriting of sizeof expressions	Thomas Bauereiss
	If some type-level variables in a sizeof expression in a function body cannot be directly extracted from the parameters of the function, add a new parameter for each unresolved parameter, and rewrite calls to the function accordingly
2017-07-26	Merge	Thomas Bauereiss

2017-07-25	Fixed bug where strings were not escaped correctly within string	Alasdair Armstrong
	literals when pretty printing sail.
2017-07-25	Add instantiation_of helper function to type_check.mli that returns	Alasdair Armstrong
	the instantiated type variables in a function application
2017-07-25	Improved l-expressions	Alasdair Armstrong
	- Fixed a bug where some l-expressions which wrote registers wern't picking up register writes. - Can now write to registers with record types. e.g. ARM's ProcState record from ASL.
2017-07-25	Add partial support for rewriting of sizeof expressions	Thomas Bauereiss
	Tries to extract values of nexps from the (type annotations of) parameters passed to the function. This seems to correspond to the behaviour of the previous typechecker.