sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2019-07-31	Merge branch 'sail2' into union_barrier	Alasdair Armstrong

2019-07-31	Updates to function unfolding to support scattered definitions	Alasdair Armstrong

2019-07-31	Remove redundant ifdef and run SMT tests by default	Alasdair Armstrong

2019-07-31	Change platform_barrier so it doesn't care about it's argument type	Alasdair Armstrong

2019-07-29	Coq: add state monad version of while/until loops and lifting results	Brian Campbell

2019-07-29	Add type check after descattering to keep type environments up to date	Brian Campbell

2019-07-25	Some documentation of mappings and string matching	Jon French

2019-07-25	Update Coq barrier definition	Brian Campbell

2019-07-25	Basic port of proof machinery to Coq	Brian Campbell

2019-07-18	Need to separate out the 0.10 lem library from upcoming 0.11	Alasdair Armstrong
	Unlike the prompt-monad change I don't see a way to do this easily purely on the model side Make sure a64_barrier_type and domain aren't visible for RISC-V isabelle build
2019-07-18	Add a option to check for a feature symbol	Alasdair Armstrong

2019-07-18	Add a feature flag for barrier type change	Alasdair Armstrong
	Fix SMT mem_builtin test case
2019-07-18	Update aarch64_small to build with new barriers	Alasdair Armstrong
	Make sure barrier changes don't affect other models for now
2019-07-18	Support DMB/DSB domains	Shaked Flur

2019-07-15	Add a fast path to speed up platform_read_ram: use fast_read_ram if read is ↵	Robert Norton
	8 bytes or less to avoid cost of using GMP integers (including free/malloc).
2019-07-11	Make sure we do constant-fold primitives however	Alasdair Armstrong
	Previous change would stop all things defined externally from being folded, which was overly strict. We do want to allow folding for shared primitives, and can use the set of safe_primops in the interpreter for this.
2019-07-11	Make sure constant folding won't fold external definitions that also have ↵	Alasdair Armstrong
	sail definitions Definitions can be made external on a per-backend basis, so we need to make sure constant folding doesn't inline external functions that have sail definitions for backends other than the ones we are currently targetting
2019-07-04	Add coq builtin for concat_str (copied from mips prelude).	Robert Norton

2019-07-04	Bump opam version.	Robert Norton

2019-07-03	Consider references in topological sorting	Thomas Bauereiss

2019-06-28	Monomorphisation: add some alternative names for ones and zero_extend as ↵	Robert Norton
	used in risc-v spec.
2019-06-28	ToFromInterp backend: always wrap typ arg values in a function, fixes option ↵	Jon French
	types in riscv
2019-06-28	Add a warning for potentially unsafe casts	Alasdair

2019-06-27	SMT: Add a reverse endianness function and fix some bugs	Alasdair Armstrong

2019-06-27	Coq: less constrained version of slice for ARM model	Brian Campbell

2019-06-26	Fix: Make sure to consider NC_app when checking constraints are identical	Alasdair Armstrong

2019-06-26	Make sure we take constraint synonyms into account when checking if types ↵	Alasdair Armstrong
	are identical
2019-06-25	SMT: Add another case to append	Alasdair Armstrong

2019-06-24	Rules and supporting files for building aarch64_small monomorphised Isabelle	Brian Campbell

2019-06-21	Coq: even more robust handling of unknown goals	Brian Campbell

2019-06-21	Coq: better handling of unknown constraints	Brian Campbell
	Move the tactic forward so that preprocessing can't try silly things, simpl to get rid of embedded proofs.
2019-06-21	Coq: add missing property derivation casts for effectful expressions	Brian Campbell
	These don't appear much, but are now showing up in the sail-arm model due to an innocent change elsewhere.
2019-06-21	Coq: be more careful when dealing with wildcard argument patterns	Brian Campbell
	If they're merged with a type variable then we still need to name the argument so that it can be used in other types.
2019-06-20	Coq: avoid more unnecessary uses of pattern binders	Brian Campbell

2019-06-20	Coq: handle wildcard binders of bools properly	Brian Campbell

2019-06-20	Coq: avoid some unnecessary reduction in the constraint solver	Brian Campbell

2019-06-20	Add additional case to append for Sail -> SMT	Alasdair Armstrong

2019-06-20	Add more cases to signed for Sail SMT	Alasdair Armstrong

2019-06-20	Tweak two aarch64_small definitions to help monomorphisation	Brian Campbell

2019-06-20	Handle more uses of mutable variables during monomorphisation cast insertion	Brian Campbell
	In particular, bitvector subrange updates work with this version.
2019-06-19	Make C emulator exit with failure for uncaught exception. Make special case ↵	Robert Norton
	for 'exception.sail' test that deliberately exits with uncaught exception.
2019-06-19	Make default ocaml main exit with non-zero exit code in case of uncaught ↵	Robert Norton
	exception. This is ensures test failures are detected.
2019-06-19	Fix buggy ocaml implementation of count_leading_zeros and also make tail ↵	Robert Norton
	recursive.
2019-06-19	Rewriting improvements for monomorphic aarch64_small	Brian Campbell
	- allow disjoint_pat to be used on patterns that have just been introduced by the rewrite without rechecking - don't rebuild the matched expression in the generated fallthrough case (or any wildcard fall-through) - it may be dead code and generate badly typed Lem - update the type environment passed to rewrites whenever type checking is performed; stale information broke some rewrites
2019-06-19	Monomorphisation improvements for aarch64_small	Brian Campbell
	- additional rewrites (signed extend of subrange@zeros, subrange assignment, variants with casts) - drop # from new top-level type variables (e.g., n_times_8) so that the rewriter knows that they're safe to include in casts - add casts in else-branches when only one possible value for a size is left - add casts when assertions force a size to be a particular value - don't use types to detect set constraints in analysis because we won't know which part of the assertion should be replaced - also use non-top-level type variables when simplifying sizes in analysis (useful when it can from pattern matching on an ast) - cope with repeated int('n) in a pattern match (!)
2019-06-18	Fix two SMT test cases	Thomas Bauereiss

2019-06-18	Update test cases	Thomas Bauereiss

2019-06-18	Fix handling of E_internal_plet in rewrite	Thomas Bauereiss

2019-06-18	Implement count_leading_zeros in Lem	Thomas Bauereiss

2019-06-17	Add sail implementation of count_leading_zeros. We could use this for ↵	Robert Norton
	backends where the builtin isn't supported but sail support for this is currently a bit broken (will use sail version when it shouldn't e.g. for smt).