sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2017-10-06	Remove BK_effect constructor	Alasdair Armstrong

2017-10-06	Various improvements to menhir parser, and performance improvments for Z3 calls	Alasdair Armstrong
	New option -memo_z3 memoizes calls to the Z3 solver, and saves these results between calls to sail. This greatly increases the performance of sail when re-checking large specifications by about an order of magnitude. For example: time sail -no_effects prelude.sail aarch64_no_vector.sail real 0m4.391s user 0m0.856s sys 0m0.464s After running with -memo_z3 once, running again gives: time sail -memo_z3 -no_effects prelude.sail aarch64_no_vector.sail real 0m0.457s user 0m0.448s sys 0m0.008s Both the old and the new parser should now have better error messages where the location of the parse error is displayed visually in the error message and highlighted.
2017-10-04	Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ↵	Alasdair Armstrong
	experiments
2017-10-04	Fixed a bug in vector concatenation l-expressions	Alasdair Armstrong
	The code for these is now rather ugly though... it needs to be cleaned up at some point Also various improvements to new menhir parser
2017-10-04	Alasdair, Peter: towards new Sail ott	Peter Sewell

2017-10-04	Add pretty printer for menhir parser	Alasdair Armstrong

2017-10-04	Merge branch 'cleanup' into experiments	Alasdair Armstrong

2017-10-04	Add pretty printing for while loops	Alasdair Armstrong

2017-10-04	Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ↵	Alasdair Armstrong
	experiments
2017-10-03	Fixes to new parser	Alasdair Armstrong

2017-10-03	Fixed some loop bugs for ASL parser	Alasdair Armstrong

2017-09-29	Support vector registers (other than bitvectors)	Thomas Bauereiss

2017-09-29	Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into experiments	Thomas Bauereiss

2017-09-29	Some more refactoring of Sail library	Thomas Bauereiss
	- Remove start indices and indexing order from bitvector types. Instead add them as arguments to functions accessing/updating bitvectors. These arguments are effectively implicit, thanks to wrappers in prelude_wrappers.sail and a "sizeof" rewriting pass. - Add a typeclass for bitvectors with a few basic functions (converting to/from bitlists, converting to an integer, getting and setting bits). Make both monads use this interface, so that they work with both the bitlist and the machine word representation of bitvectors.
2017-09-29	Move Isabelle library	Thomas Bauereiss

2017-09-29	Add MIPS->Isabelle target to Makefile	Thomas Bauereiss

2017-09-27	Add while-loops to Lem backend	Thomas Bauereiss

2017-09-27	Fixed command line flag naming	Alasdair Armstrong

2017-09-26	Added while-do and repeat-until loops to sail for translating ASL	Alasdair Armstrong

2017-09-21	Refactored AST valspecs into single constructor	Alasdair Armstrong

2017-09-21	Remove unused kind_def (KD_) nodes from AST	Alasdair Armstrong

2017-09-21	Change NC_fixed to NC_equal to match NC_not_equal	Alasdair Armstrong
	also rename NC_nat_set_bounded to NC_set (it was an int set not a nat set anyway)
2017-09-21	Simplify AST by removing LB_val_explicit and replace LB_val_implicit with ↵	Alasdair Armstrong
	just LB_val in AST also rename functions in rewriter.ml appropriately.
2017-09-21	Cleaning up the AST and removing redundant and/or unused nodes	Alasdair Armstrong

2017-09-19	Added additional case for tuple l-expressions to increase compatability for ASL.	Alasdair Armstrong

2017-09-18	Added additional utility functions in ast_util	Alasdair Armstrong
	Also fixed basic ocaml test suite
2017-09-14	Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ↵	Alasdair Armstrong
	experiments
2017-09-14	Fix bug in topological sorting	Thomas Bauereiss

2017-09-14	Fix some more test cases	Thomas Bauereiss

2017-09-14	Fix a regression when writing to a register via a reference in a vector such ↵	Thomas Bauereiss
	as GPR This was wrongly translated as an update of the vector of references.
2017-09-13	Fixed code display in error messages that span multiple lines	Alasdair Armstrong

2017-09-13	Work on improving Sail error messages	Alasdair Armstrong
	- Modified how sail type error messages are displayed. The typechecker, rather than immediately outputing a string has a datatype for error types, which are the pretty-printed using a PPrint pretty-printer. Needs more work for all the error messages. - Error messages now attempt to highlight the part of the file where the error occurred, by printing the line the error is on and highlighting where the error message is in red. Again, this needs to be made more robust, especially when the error messages span multiple lines. Other things - Improved new parser and lexer. Made the lexer & parser handling of colons simpler and more intuitive. - Added some more typechecking test cases
2017-09-08	Fixed bug when printing Typ_args in Lem AST output	Alasdair Armstrong

2017-09-07	Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ↵	Alasdair Armstrong
	experiments
2017-09-07	Add ocaml run-time and updates to sail for ocaml backend	Alasdair Armstrong

2017-09-05	Fix printing of negative numbers	Alastair Reid

2017-09-02	Various fixes for Hexapod	Thomas Bauereiss
	- Support tuples in lexps - Rewrite trivial sizeofs - Rewrite early returns more aggressively - Support let bindings with ticked variables (binding both a type-level and term-level variable at the same time)
2017-09-02	Remove dependency of state.lem on bitvector operations	Thomas Bauereiss

2017-09-02	Add command line flags to toggle sequential monad and native machine words	Thomas Bauereiss

2017-09-01	Testing typedef generation for ocaml	Alasdair Armstrong

2017-09-01	More test cases for ocaml backend	Alasdair Armstrong

2017-09-01	Started work on test suite for ocaml backend	Alasdair Armstrong

2017-08-30	Remove debug print statement from rewriter	Alasdair Armstrong

2017-08-30	Improved ocaml backend to the point where the hexapod spec produces ↵	Alasdair Armstrong
	syntactically correct ocaml
2017-08-30	Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ↵	Alasdair Armstrong
	experiments
2017-08-30	Ocaml backend can now run ocamlbuild automatically to build ocaml	Alasdair Armstrong
	files into runable executable.
2017-08-30	Fix another bug in local variable update rewriting	Thomas Bauereiss
	E_internal_let is only used for introducing local variables, not updating existing ones.
2017-08-29	Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ↵	Alasdair Armstrong
	experiments
2017-08-29	More work on ocaml backend.	Alasdair Armstrong
	Works for basic examples with arbitrary register types, so for example we can compile: val extern string -> unit effect pure print = "print_endline" val unit -> string effect pure hello_world function hello_world () = { return "Hello, World!"; "Unreachable" } val unit -> unit effect {wreg, rreg} main register string REG function main () = { REG := "Hello, Sail!"; print(REG); REG := hello_world (); print(REG); return () } into open Sail_lib;; let zhello_world () = with_return (fun r -> begin r.return "Hello, World!"; "Unreachable" end);; let zREG : (string) ref = ref (undefined_string ());; let zmain () = with_return (fun r -> begin zREG := "Hello, Sail!"; print_endline !zREG; zREG := zhello_world (); print_endline !zREG; r.return () end);; let initialize_registers () = with_return (fun r -> zREG := undefined_string ());; with the arbitrary register types and early returns being handled appropriately, given a suitable implementation for Sail_lib
2017-08-29	Make Lem export of CHERI(-256) typecheck	Thomas Bauereiss
	Note: The effect annotations of the execute function differ between CHERI and MIPS, so I split out a new file mips_ast_decl.sail for MIPS with just the initial declarations of ast, decode, and execute (with the right effects for MIPS).