summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-05-17Refactor main.sailThomas Bauereiss
2018-05-17Remove sequential code againBrian Campbell
2018-05-17Clean up CHERI HOL generation a little tooBrian Campbell
2018-05-17Clean up MIPS for HOL4 a littleBrian Campbell
Move mono_rewrites into lib
2018-05-17Tidy up HOL4 riscv a littleBrian Campbell
2018-05-17Use an intermediate base_monad type alias in Lem,Brian Campbell
resolving the difference in type parameters between the prompt and state monads, and allowing a single output file to be used with either. Normally, the type alias is to the prompt monad, but for HOL4 we use the state monad.
2018-05-16Add handwritten script to HolmakefileBrian Campbell
2018-05-16More targeted gitignore for HOL4Brian Campbell
(will do individual models later)
2018-05-16Termination proofs and lemmata for sail_values holRamana Kumar
2018-05-16Ignore .hollogsRamana Kumar
2018-05-16Declare hol automatic termination in sail_valuesRamana Kumar
2018-05-16Add global gitignore entries for HOL4Brian Campbell
2018-05-15Make all of Sail HOL libraries, not just the base heapBrian Campbell
2018-05-11Add Isabelle code generation for sequential CHERI modelThomas Bauereiss
2018-05-11Add Boolean short-circuiting to state monadThomas Bauereiss
2018-05-11Merge branch 'sail2' into cheri-monoThomas Bauereiss
In order to use up-to-date sequential CHERI model for test suite
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-10Document the register_inaccessible function.Robert Norton
2018-05-10RISC-V in HOL4Brian Campbell
2018-05-10Clean up HOL library properlyBrian Campbell
2018-05-09Remove unused definitions.Prashanth Mundkur
2018-05-09Tweaks for sequential CHERI in HOLBrian Campbell
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-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-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-07HOL script generation for library and CHERIBrian Campbell
(still needs some Lem work on types before it will be useful)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 05:53:18 +0000