sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2018-07-12	Fix bug for large integers in OCaml compilation	Alasdair Armstrong

2018-07-09	Fix bug in rewriting of try-catch-blocks with variable updates	Thomas Bauereiss

2018-07-09	Tweak rewriting of literal patterns for Lem	Thomas Bauereiss

2018-07-09	Add explanatory comment to guard rewriting	Thomas Bauereiss

2018-07-03	Fix letbind_effects on LEXP_deref with an effectful subexpression	Brian Campbell

2018-06-26	In guarded pattern rewriting, irrefutable patterns subsume wildcards	Brian Campbell
	Necessary to prevent redundant clauses that Coq will reject (There's still a problem if you use a variable rather than a wildcard, see the test)
2018-06-25	Check for variables in disjointness check	Thomas Bauereiss

2018-06-25	Fix a bug in pattern guard rewriting	Thomas Bauereiss
	Remember and use fallthrough clauses instead of dropping them when the last clause in a group has a guard
2018-06-11	add 'pat as id' mapping-patterns	Jon French

2018-06-11	Merge branch 'sail2' into mappings	Jon French
	(involved some manual tinkering with gitignore, type_check, riscv)
2018-06-06	Some work on improving error messages	Alasdair Armstrong
	We now store the location where type variables were bound, so we can use this information when printing error messages. Factor type errors out into type_error.ml. This means that Type_check.check is now Type_error.check, as it previously it handled wrapping the type_errors into reporting_basic errors. Type_check.check' has therefore been renamed to Type_check.check.
2018-05-21	fix bug in rewrite_defs_mapping_patterns where pattern-uses of mappings with ↵	Jon French
	multiple arguments weren't type-checking correctly
2018-05-18	Fix bug in rewriting variable updates	Thomas Bauereiss

2018-05-18	temporary HACK for aarch64: make rewrite_defs_pat_lits ignore strings	Jon French

2018-05-18	more riscv mappings; riscv now builds successfully to lem which builds to ↵	Jon French
	isabelle (but isabelle almost certainly broken)
2018-05-17	fix bug in rewrite_defs_pat_string_append -- make it pass types through ↵	Jon French
	correctly
2018-05-16	Add support for inline val-spec declaration for mappings	Jon French
	This means that a mapping which formerly had to be pre-declared like val name : a <-> b ... mapping name { x <-> y, ... } can now be shortened to mapping name : a <-> b { x <-> y, ... }
2018-05-15	reorder lem rewrite passes and explicitly remove mapping valspecs; string ↵	Jon French
	stuff now compiles to Lem
2018-05-15	rewrite_defs_guarded_pats: guards deserve rewriting too	Jon French

2018-05-14	make debug printing of realised mappings both optional and lazy	Jon French

2018-05-11	support for mapping-patterns inside (should be) all other pattern types	Jon French

2018-05-10	Merge branch 'sail2' into mappings	Jon French

2018-05-10	generalise string pattern matching to arbitrary arguments rather than just ↵	Jon French
	an id; also remove builtin special-casing as it's not needed!
2018-05-09	Add more annotations for loop bounds in Lem rewriting	Thomas Bauereiss
	Typechecking for-loops failed after the Lem rewriting passes in some cases: if the lower bound for the loop may be greater than the upper bound, the loop variable's type might be empty, and it cannot be initialised. This patch adds a guard "lower <= upper" around the loop body, and removes it again during pretty-printing.
2018-05-09	Support short-circuiting of Boolean expressions in Lem	Thomas Bauereiss

2018-05-08	fixed sub-mappings	Jon French

2018-05-04	Checked that variable names in split_fun rewrites are really variables	Brian Campbell
	Otherwise some clauses disappear
2018-05-04	Fix missing nexp id rewriting	Brian Campbell

2018-05-04	Rewrite constant nexps in specs	Brian Campbell
	(from Thomas)
2018-05-03	Flow typing and l-expression changes for ASL parser	Alasdair Armstrong
	1. Experiment with allowing some flow typing on mutable variables for translating ASL in a more idiomatic way. I realise after updating some of the test cases that this could have some problematic side effects for lem translation, where mutable variables are translated into monadic code. We'd need to ensure that whatever flow typing happens for mutable variables also works for monadic code, including within transformed loops. If this doesn't work out some of these changes may need to be reverted. 2. Make the type inference for l-expressions a bit smarter. Splits the type checking rules for l-expressions into a inference part and a checking part like the other bi-directional rules. Should not be able to type check slightly more l-expresions, such as nested vector slices that may not have checked previously. The l-expression rules for vector patterns should be simpler now, but they are also more strict about bounds checking. Previously the bounds checks were derived from the corresponding operations that would appear on the RHS (i.e. LEXP_vector would get it's check from vector_access). This meant that the l-expression bounds checks could be weakend by weakening the checks on those operations. Now this is no longer possible, there is a -no_lexp_bounds_check option which turns of bounds checking in l-expressions. Currently this is on for the generated ARM spec, but this should only be temporary. 3. Add a LEXP_vector_concat which mirrors P_vector_concat except in l-expressions. Previously there was a hack that overloaded LEXP_tup for this to translate some ASL patterns, but that was fairly ugly. Adapt the rewriter and other parts of the code to handle this. The rewriter for lexp tuple vector assignments is now a rewriter for vector concat assignments. 4. Include a newly generated version of aarch64_no_vector 5. Update the Ocaml test suite to use builtins in lib/
2018-05-03	support sub-mappings in string-append-patterns	Jon French

2018-05-03	synthesise string-prefix-check functions for mappings where either side is ↵	Jon French
	string (kind of hacky but there you go)
2018-05-02	scattered mappings	Jon French

2018-05-02	refactor string append pattern ast to be based on lists rather than pairs	Jon French

2018-05-01	add type annotation patterns to mpats	Jon French

2018-05-01	rewriting of builtin mappings e.g. int	Jon French

2018-05-01	further progress but confounds the type checker?	Jon French

2018-05-01	progress on debugging string pattern matching	Jon French

2018-05-01	oops, not every pattern is in fact string_typ, remember to pass through the ↵	Jon French
	original type in rewrite_defs_pat_string_append when not doing anything
2018-05-01	create a single funcl with a match, rather than converting mapcls to funcls, ↵	Jon French
	because OCaml among others doesn't allow top-level guards
2018-05-01	further progress	Jon French

2018-05-01	starting to also do integer support	Jon French

2018-05-01	starting to also do integer support	Jon French

2018-05-01	start of string pattern matching: currently only literals	Jon French

2018-05-01	fix refactored rewrite_pexp_with_guards (where type information is and is ↵	Jon French
	not...)
2018-05-01	more refactoring of pexp rewriters	Jon French

2018-05-01	Type_check: factor rewrite_pexps_with_guards out of rewrite_defs_pat_lits	Jon French

2018-04-26	Fix bug in rewriting of loops	Thomas Bauereiss
	Take into account existential types when determining bounds for the loop variable
2018-04-26	Avoid adding explicit type annotations with generated type variables	Thomas Bauereiss

2018-04-26	Make effect propagation in rewriter more efficient	Thomas Bauereiss
	Use non-recursive fix_eff_exp instead of recursive propagate_exp_effect, assuming that the effects of subexpressions have already been fixed by the recursive calls of the rewriter.