| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-05-11 | Add missing document list example to repository | Alasdair Armstrong | |
| 2018-05-11 | Update and alphabetise author list in manual | Alasdair Armstrong | |
| 2018-05-11 | More builtin names in constant propagation | Brian Campbell | |
| 2018-05-11 | Temporary hacks for monomorphisation | Brian Campbell | |
| Mostly introducing type variables for regsize in valspecs | |||
| 2018-05-11 | Make nexp simplification a little smarter | Brian Campbell | |
| (should really make the Lem pretty printer use the solver properly, but this is a useful stopgap) | |||
| 2018-05-11 | Actually use the correct type for singleton rewriting this time | Brian Campbell | |
| 2018-05-11 | Be much more careful to introduce the right bitvector casts to the right sizes | Brian Campbell | |
| 2018-05-11 | Handle automatic existential unpacking in function application in mono analysis | Brian Campbell | |
| 2018-05-11 | Use type from funcl in singleton rewriting | Brian Campbell | |
| The pattern types may be subtypes, using those caused it to try rewriting int parameters and failing | |||
| 2018-05-11 | Add link to Thomas's Sail/Isabelle documentation in manual | Alasdair Armstrong | |
| Replace the old manual with new version in repository root | |||
| 2018-05-11 | More work on documentation | Alasdair Armstrong | |
| Should have all the main language features covered in at least some detail now. | |||
| 2018-05-11 | Work around Lem generation problem in RISC-V | Thomas Bauereiss | |
| "sum" is an existing constant in Isabelle, and the Lem constant avoiding mechanism does not seem to pick it up when used as the name of a function parameter. | |||
| 2018-05-11 | Add snapshot of generated Isabelle theories | Thomas Bauereiss | |
| Currently contains Lem and Sail libraries, and RISC-V and CHERI-MIPS specs. | |||
| 2018-05-11 | add .git to dev-repo in opam file to satisfy opam-publish. | Robert Norton | |
| 2018-05-11 | prepare sail 0.2 release | Robert Norton | |
| 2018-05-11 | Add uart stub with registers based on ARM uart spec | Alasdair Armstrong | |
| 2018-05-11 | Remove buggy bit list comparison functions from Lem library | Thomas 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-11 | Remove unneeded _sail suffix from latex files. | Robert Norton | |
| 2018-05-11 | Avoid generating latex files that differ only by case because this causes ↵ | Robert Norton | |
| confusion on case insensitive file systems (e.g. mac). | |||
| 2018-05-10 | latex: 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-10 | Document the register_inaccessible function. | Robert Norton | |
| 2018-05-09 | Remove unused definitions. | Prashanth Mundkur | |
| 2018-05-09 | remove redundant cloc targets. | Robert Norton | |
| 2018-05-09 | add loc for arm full. | Robert Norton | |
| 2018-05-09 | Add full translated aarch64 spec including vector instructions | Alasdair Armstrong | |
| 2018-05-09 | Use latex support for generating cheri documentation and remove sed based ↵ | Robert Norton | |
| hack. Also some minor code cleanups and comments. | |||
| 2018-05-09 | Add 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-09 | Remove start and end markers that are no longer needed now that sail has ↵ | Robert Norton | |
| latex output. | |||
| 2018-05-09 | Add language=sail option in listings command for latex output. This helps ↵ | Robert Norton | |
| with documents containing listings in multiple languages. | |||
| 2018-05-09 | Fix an issue with C compilation | Alasdair Armstrong | |
| 2018-05-09 | Fix printing of hex strings in Lem | Thomas Bauereiss | |
| 2018-05-09 | Adapt Isabelle code generation to Byte_sequence changes | Thomas Bauereiss | |
| 2018-05-09 | Add tests for Isabelle->OCaml generation for CHERI and AArch64 | Thomas Bauereiss | |
| 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 | Run ARM built-in tests for Lem backend (via OCaml) | Thomas Bauereiss | |
| 2018-05-09 | Support short-circuiting of Boolean expressions in Lem | Thomas Bauereiss | |
| 2018-05-09 | Generate initial register state record | Thomas 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-09 | Add type system documentation | Alasdair Armstrong | |
| 2018-05-09 | Merge pull request #12 from emersion/fix-byte-sequence | Robert Norton | |
| Fix Byte_sequence errors due to linksem update | |||
| 2018-05-09 | Fix Byte_sequence errors due to linksem update | emersion | |
| 2018-05-08 | More work on Sail documentation | Alasdair Armstrong | |
| 2018-05-07 | Add a register indicating no trigger/breakpoint support, which allows the ↵ | Prashanth Mundkur | |
| breakpoint test to pass. | |||
| 2018-05-07 | Fix another mask computation bug. | Prashanth Mundkur | |
| 2018-05-07 | Adjust default pte update setting to match spike's default. | Prashanth Mundkur | |
| 2018-05-07 | Log trap value on traps. | Prashanth Mundkur | |
| 2018-05-07 | Fix a missed csr read. | Prashanth Mundkur | |
| 2018-05-04 | Tweak the execution log. | Prashanth Mundkur | |
| 2018-05-04 | Fix two bugs in the page-table walker, and add some comments. | Prashanth Mundkur | |
| 2018-05-04 | Fix printing of ld. | Prashanth Mundkur | |
| 2018-05-04 | Checked that variable names in split_fun rewrites are really variables | Brian Campbell | |
| Otherwise some clauses disappear | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |