summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2018-05-23riscv decode now uses mapping-decode and passes testsJon French
2018-05-23fix typo in error message in type_check.mlJon French
2018-05-21further RISCV mapping: all extant non-compressed instructions doneJon French
2018-05-21fix bug in rewrite_defs_mapping_patterns where pattern-uses of mappings with ↵Jon French
multiple arguments weren't type-checking correctly
2018-05-18temporary HACK for aarch64: make rewrite_defs_pat_lits ignore stringsJon French
2018-05-18more riscv mappings; riscv now builds successfully to lem which builds to ↵Jon French
isabelle (but isabelle almost certainly broken)
2018-05-17fix bug in rewrite_defs_pat_string_append -- make it pass types through ↵Jon French
correctly
2018-05-16fix a couple warnings in type_check.mlJon French
2018-05-16Add support for inline val-spec declaration for mappingsJon 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-15Merge branch 'sail2' into mappingsJon French
2018-05-15reorder lem rewrite passes and explicitly remove mapping valspecs; string ↵Jon French
stuff now compiles to Lem
2018-05-15rewrite_defs_guarded_pats: guards deserve rewriting tooJon French
2018-05-14make debug printing of realised mappings both optional and lazyJon French
2018-05-12Fix bug in handling of registers with option typeThomas Bauereiss
Also add test cases and Isabelle lemmas
2018-05-11More builtin names in constant propagationBrian Campbell
2018-05-11Make nexp simplification a little smarterBrian Campbell
(should really make the Lem pretty printer use the solver properly, but this is a useful stopgap)
2018-05-11Actually use the correct type for singleton rewriting this timeBrian Campbell
2018-05-11Be much more careful to introduce the right bitvector casts to the right sizesBrian Campbell
2018-05-11Handle automatic existential unpacking in function application in mono analysisBrian Campbell
2018-05-11Use type from funcl in singleton rewritingBrian Campbell
The pattern types may be subtypes, using those caused it to try rewriting int parameters and failing
2018-05-11further riscv mappingJon French
2018-05-11support for mapping-patterns inside (should be) all other pattern typesJon French
2018-05-11Remove buggy bit list comparison functions from Lem libraryThomas Bauereiss
Found bugs by running CHERI test suite on Isabelle-exported model: signed less-than for bit lists was missing negations for the two's complement, and unsigned less-than compared the reverse lists. Since all other backends implement this in Sail, it seems best to just remove this code. Also add support for infix operators to Lem backend, by z-encoding their identifiers like the other backends do.
2018-05-11Remove unneeded _sail suffix from latex files.Robert Norton
2018-05-11Avoid generating latex files that differ only by case because this causes ↵Robert Norton
confusion on case insensitive file systems (e.g. mac).
2018-05-10latex: don't include the prefix in the label. This means we have the option ↵Robert Norton
of omitting valspec in documentation if it is deemed too verbose and still have hyperlinks work. The caveat is that it could result in multiply defined labels.
2018-05-10more mappingJon French
2018-05-10Type_check: special case appending an empty vectorJon French
2018-05-10hacky monomorphic bits-string-parser for nowJon French
2018-05-10Merge branch 'sail2' into mappingsJon French
2018-05-10add space handling mappings to riscv prelude and sail_lib.mlJon French
2018-05-10generalise 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-09Add language=sail option in listings command for latex output. This helps ↵Robert Norton
with documents containing listings in multiple languages.
2018-05-09Fix an issue with C compilationAlasdair Armstrong
2018-05-09Fix printing of hex strings in LemThomas Bauereiss
2018-05-09Add tests for Isabelle->OCaml generation for CHERI and AArch64Thomas Bauereiss
2018-05-09Add more annotations for loop bounds in Lem rewritingThomas 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-09Run ARM built-in tests for Lem backend (via OCaml)Thomas Bauereiss
2018-05-09Support short-circuiting of Boolean expressions in LemThomas Bauereiss
2018-05-09Generate initial register state recordThomas Bauereiss
Filled with default values (e.g., 0) and used to initialise the state monad. There is already code to generate a Sail function "initialize_registers", but this is monadic itself, so it cannot be used to initialise the monad.
2018-05-09allow empty brackets to pass unit to sub-mpatsJon French
2018-05-09Fix Byte_sequence errors due to linksem updateemersion
2018-05-08fixed sub-mappingsJon French
2018-05-04Checked that variable names in split_fun rewrites are really variablesBrian Campbell
Otherwise some clauses disappear
2018-05-04Fix missing nexp id rewritingBrian Campbell
2018-05-04Rewrite constant nexps in specsBrian Campbell
(from Thomas)
2018-05-04Add support for top-level values to monomorphisation singleton rewriteBrian Campbell
2018-05-04Fix mono cast introduction to avoid a checking to inference changeBrian Campbell
Adds return type to pattern so that the original function body is still type checked, rather than switching to type inference which may fail.
2018-05-04Start updating monomorphisationBrian Campbell
+ add additional lexp + update aarch64 mono demo source - still needs support for tyvars from assignments in dependency analysis
2018-05-04Rename type vars in Coq backend when they clash with identifiersBrian Campbell
Add value-only version of compute_{pat,exp}_alg to help Experiment with adding equality constraints between type vars and args in Coq output
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 03:02:13 +0000