summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-05-10Type_check: special case appending an empty vectorJon French
2018-05-10load-type riscv assemblyJon French
2018-05-10rtype mapping clausesJon French
2018-05-10move common mappings to riscv_types.sailJon French
2018-05-10hacky monomorphic bits-string-parser for nowJon French
2018-05-10Merge branch 'sail2' into mappingsJon French
2018-05-10riscv/Makefile: add SAIL variable for easier debuggingJon French
2018-05-10refining spaces 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-09Remove unused definitions.Prashanth Mundkur
2018-05-09remove redundant cloc targets.Robert Norton
2018-05-09add loc for arm full.Robert Norton
2018-05-09Add full translated aarch64 spec including vector instructionsAlasdair Armstrong
2018-05-09Use latex support for generating cheri documentation and remove sed based ↵Robert Norton
hack. Also some minor code cleanups and comments.
2018-05-09Add targets for counting lines in mips, cheri and riscv. Can use either ↵Robert Norton
sloccount or cloc. sloccount seems to be reliable but lacks a way to tell it that sail files can be treated like ocaml without renaming the files. cloc has a nicer interface is lower quality in other regards like broken ocaml support in versions shipped with Ubuntu (e.g. treats {...} as comment, no nested comments support). For sail2 syntax this is OK because we use the C parser instead which gives the same results as sloccount.
2018-05-09Remove start and end markers that are no longer needed now that sail has ↵Robert Norton
latex output.
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-09Adapt Isabelle code generation to Byte_sequence changesThomas 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-09start of riscv assembly mappingsJon French
2018-05-09allow empty brackets to pass unit to sub-mpatsJon French
2018-05-09add SAIL_FLAGS env var to riscv makefileJon French
2018-05-09Add type system documentationAlasdair Armstrong
2018-05-09Merge pull request #12 from emersion/fix-byte-sequenceRobert Norton
Fix Byte_sequence errors due to linksem update
2018-05-09Fix Byte_sequence errors due to linksem updateemersion
2018-05-08More work on Sail documentationAlasdair Armstrong
2018-05-08Merge branch 'sail2' into mappingsJon French
2018-05-08fixed sub-mappingsJon French
2018-05-07Add a register indicating no trigger/breakpoint support, which allows the ↵Prashanth Mundkur
breakpoint test to pass.
2018-05-07Fix another mask computation bug.Prashanth Mundkur
2018-05-07Adjust default pte update setting to match spike's default.Prashanth Mundkur
2018-05-07Log trap value on traps.Prashanth Mundkur
2018-05-07Fix a missed csr read.Prashanth Mundkur
2018-05-04Tweak the execution log.Prashanth Mundkur
2018-05-04Fix two bugs in the page-table walker, and add some comments.Prashanth Mundkur
2018-05-04Fix printing of ld.Prashanth Mundkur
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-03 10:40:43 +0000