| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |||
| 2018-05-04 | Fix missing nexp id rewriting | Brian Campbell | |
| 2018-05-04 | Rewrite constant nexps in specs | Brian Campbell | |
| (from Thomas) | |||
| 2018-05-04 | Add support for top-level values to monomorphisation singleton rewrite | Brian Campbell | |
| 2018-05-04 | Fix mono cast introduction to avoid a checking to inference change | Brian 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-04 | Start updating monomorphisation | Brian Campbell | |
| + add additional lexp + update aarch64 mono demo source - still needs support for tyvars from assignments in dependency analysis | |||
| 2018-05-04 | Rename type vars in Coq backend when they clash with identifiers | Brian 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 | |||
| 2018-05-04 | Basic Coq constraints | Brian Campbell | |
| 2018-05-03 | Fix a typo in sret decode and privilege checks in xret. | Prashanth Mundkur | |
| 2018-05-03 | Add implementation of sfence with a fixme note. | Prashanth Mundkur | |
| 2018-05-03 | Fix a bug in privilege transition, add better transition logging. | Prashanth Mundkur | |
| 2018-05-03 | Implement wfi, and cleanup handling illegal operations. | Prashanth Mundkur | |
| 2018-05-03 | Fix interrupt dispatch, improve execution logs, cleanup unused bits. | Prashanth Mundkur | |
| 2018-05-03 | Simplify the top-level execute loop using the step function. | Prashanth Mundkur | |
| 2018-05-03 | Fix up interrupt and exception dispatch. | Prashanth Mundkur | |
| 2018-05-03 | Implement fetch to properly handle RVC and address translation, and add a ↵ | Prashanth Mundkur | |
| step function for execution. | |||
| 2018-05-03 | Flow typing and l-expression changes for ASL parser | Alasdair Armstrong | |
| 1. Experiment with allowing some flow typing on mutable variables for translating ASL in a more idiomatic way. I realise after updating some of the test cases that this could have some problematic side effects for lem translation, where mutable variables are translated into monadic code. We'd need to ensure that whatever flow typing happens for mutable variables also works for monadic code, including within transformed loops. If this doesn't work out some of these changes may need to be reverted. 2. Make the type inference for l-expressions a bit smarter. Splits the type checking rules for l-expressions into a inference part and a checking part like the other bi-directional rules. Should not be able to type check slightly more l-expresions, such as nested vector slices that may not have checked previously. The l-expression rules for vector patterns should be simpler now, but they are also more strict about bounds checking. Previously the bounds checks were derived from the corresponding operations that would appear on the RHS (i.e. LEXP_vector would get it's check from vector_access). This meant that the l-expression bounds checks could be weakend by weakening the checks on those operations. Now this is no longer possible, there is a -no_lexp_bounds_check option which turns of bounds checking in l-expressions. Currently this is on for the generated ARM spec, but this should only be temporary. 3. Add a LEXP_vector_concat which mirrors P_vector_concat except in l-expressions. Previously there was a hack that overloaded LEXP_tup for this to translate some ASL patterns, but that was fairly ugly. Adapt the rewriter and other parts of the code to handle this. The rewriter for lexp tuple vector assignments is now a rewriter for vector concat assignments. 4. Include a newly generated version of aarch64_no_vector 5. Update the Ocaml test suite to use builtins in lib/ | |||
| 2018-05-03 | Fix duopod with latest riscv prelude | Alasdair Armstrong | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |