sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2019-02-03	Merge branch 'sail2' into rmem_interpreter	Jon French

2019-01-31	Fix an unnecessary cast insertion on assignments	Brian Campbell

2019-01-31	Turn on cast insertion for -lem_mwords and revert b826df25	Brian Campbell
	now that cast insertion can handle RISC-V Also inserts specs for casts in they're not present
2019-01-31	Drop type annotations in top-level nexp rewriting in favour of valspecs	Brian Campbell
	otherwise the valspec rewriting will be inconsistent with the type annotation. Note that the type checker will have introduced valspecs where necessary.
2019-01-31	Make cast insertion handle more complex nexps and pushing casts into blocks	Brian Campbell
	# Conflicts: # src/monomorphise.ml
2019-01-31	Monomorphisation: improve cast insertion and nexp rewriting on variants	Brian Campbell
	It now pushes casts into lets and constructor applications, and so supports the case needed for RISC-V.
2019-01-31	Add missing cases to constraint comparison	Brian Campbell

2019-01-31	Support case splitting on variables as well as sizeof in cast introduction	Brian Campbell

2019-01-29	Improve generation of initial register state	Thomas Bauereiss
	Define initial values for record types once instead of repeating them in the initial register state.
2019-01-28	Lem: Be more careful about nexps occurring in the function signature	Thomas Bauereiss
	Don't ask Z3 to simplify them, as flow typing might lead to different results in different if-branches, for example, leading to type errors in Lem.
2019-01-25	Monomorphisation: update a built-in name	Brian Campbell

2019-01-25	Fix solution finding using SMT by looking for the right variable	Brian Campbell

2019-01-22	Add a pragma for unrolling recursive functions	Alasdair Armstrong
	For example in RISC-V for the translation table walk: $optimize unroll 2 val walk32 ... function walk32 ... would create two extra copies of the walk_32 function, walk_32_unroll_1 and walk_32_unroll_2, with only walk_32_unroll_2 being recursive. Currently we only support the case where we have $optimize unroll, directly followed by a valspec, then a function, but this should be generalised in future. This optimization nearly doubles the performance of RISC-V It is implemented using a new Optimize.recheck rewrite that replaces the ordinary recheck_defs pass. It uses a new typechecker check_with_envs function that allows re-writes to utilise intermediate typechecking environments to minimize the amount of AST checking that occurs, for performance reasons. Note that older Sail versions including the current OPAM release will complain about the optimize pragma, so this cannot be used until they become up to date with this change.
2019-01-22	Make sure there is an ocaml representation for optimized memory read for	Alasdair
	RISC-V
2019-01-22	Make sure we optimize constrained union constructors	Alasdair

2019-01-21	Update manual snapshot and add basic sail -latex documentation	Alasdair Armstrong

2019-01-21	Add output directory option for generated Isabelle auxiliary theories	Thomas Bauereiss

2019-01-21	Fix some issues with latex generation so manual builds again	Alasdair Armstrong
	since riscv is no longer in this repository, and we use the RISC-V duopod as an example, you need to build as: make RISCV=directory manual.pdf if directory is not equal to ../../sail-riscv (which is where it would be if sail and sail-riscv are checked out in the same respository together)
2019-01-21	Fix a bug with type-checking and latex generation	Alasdair Armstrong
	We should maybe just make the -latex option behavior the default to avoid this kind of thing
2019-01-16	Latex: handle underscores when generating latex names.	Prashanth Mundkur

2019-01-14	Add options for output directories for the lem and coq backends.	Prashanth Mundkur

2019-01-09	Coq: the division used in smt.sail should be Euclidean	Brian Campbell

2019-01-09	Coq: add parens around negative integer literals	Brian Campbell

2019-01-02	Coq: tweak recently introduced type check to ignore effects	Brian Campbell

2019-01-02	...without debug printing	Jon French

2019-01-02	restore V_attempted_read behaviour after merge	Jon French

2018-12-31	Last rewrite reordering needs more typechecking	Brian Campbell

2018-12-31	Coq: move function clause merging to keep measure argument intact	Brian Campbell

2018-12-30	Sort dependencies of termination measures properly	Brian Campbell

2018-12-29	Coq: ensure that recursive functions compute	Brian Campbell

2018-12-29	Add separate termination_measure declarations	Brian Campbell

2018-12-28	Remove opt_spc_matches_prefix from sail.h (fixes C tests)	Jon French

2018-12-28	Merge branch 'sail2' into rmem_interpreter	Jon French

2018-12-27	Coq: avoid putting ambiguous numeric literals in Coq output	Brian Campbell
	There are situations when we really want a more refined expression, such as 8 * n instead of 64 (when we know n = 8 from a case split), but we might not be able to generate it. For now we generate an underscore and let Coq figure it out from the context.
2018-12-27	fix missed case in refactored val-spec extern parser	Jon French

2018-12-27	Coq: fix name clashes and instantiation calculation	Brian Campbell

2018-12-27	new command line option -marshal <file> to marshal out rewritten AST to a file	Jon French
	Adds new dependency: base64
2018-12-27	remove unused previous-version-of-flow-typing functions from typechecker	Jon French
	(they store flow-typing info as functions; preparing for marshalling)
2018-12-27	basic Sail-side support for rmem use of interpreter	Jon French

2018-12-27	refactor val-spec AST to store externs as an assoc-list rather than a ↵	Jon French
	function (preparing for marshalling)
2018-12-27	pass typechecking environment around interpreter and rewriters	Jon French

2018-12-23	Remove a comment that breaks Isabelle build	Thomas Bauereiss
	With the new comment syntax, Isabelle seems to barf on that comment, apparently due to the backslashes.
2018-12-22	Added RISC-V fence.tso	Shaked Flur

2018-12-19	Coq: handle pairs of ranges (and other existential types) properly	Brian Campbell
	(Needed for current CHERI.)
2018-12-19	Coq: handle existentials in hypotheses during solving, add max_nat, better casts	Brian Campbell

2018-12-18	Check more carefully for recursive functions when generating Lem	Thomas Bauereiss
	Annotating non-recursive functions as recursive in Lem output is allowed, but will make Lem use "fun"/"function" commands when generating Isabelle output, which is much slower to process than "definiton".
2018-12-17	Adapt Coq and termination measure support to typechecker changes	Brian Campbell
	Also output termination measures in Sail printer
2018-12-14	Add some experimental support for non-lexical flow-typing rules	Alasdair Armstrong
	Add a file nl_flow.ml which can analyse a block of Sail expressions and insert constraints for flow-typing rules which do not follow the lexical structure of the code (and therefore the syntax-directed typing rules can't do any flow-typing for). A common case found in ASL translated Sail would be something like function decode(Rt: bits(4)) = { if Rt == 0xF then { throw(Error_see("instruction")); }; let t = unsigned(Rt); execute(t) } which would currently fail is execute has a 0 <= t <= 14 constraint for a register it writes to. However if we spot this pattern and add an assertion automatically: let t = unsigned(Rt); assert(t != 15); execute(t) Then everything works, because the assertion is in the correct place for regular flow typing. Currently it only works for this specific use-case, and is turned on using the -non_lexical_flow flag
2018-12-14	Add a few more tests for Jenkins	Alasdair Armstrong
	Some of the output from the tests scripts is odd on Jenkins, try to fix this by flushing stdout more regularly in the test scripts
2018-12-14	Add truncateLSB builtin useful for implementing Cheri Concentrate. Also add ↵	Robert Norton
	bool_of_bit and bit_of_bool in sail_lib