summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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)
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-04Add back purely sequential Lem generationThomas Bauereiss
The datatype package of HOL4 does not support the prompt monad, so this patch restores the option to generate a model that only uses the state monad. Also add a Makefile target cheri_sequential.lem in the cheri/ directory.
2018-05-04Bit of hackery to MIPS prelude and Makefiles to get monomorphised CHERIBrian Campbell
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 06:43:29 +0000