| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-01-24 | Make recheck_defs_without_effects restore old flag properly | Brian Campbell | |
| 2019-01-23 | Make rewriting of E_assign a bit more robust | Thomas Bauereiss | |
| 2019-01-23 | Add another flow-typing case for E_internal_plet | Thomas Bauereiss | |
| Copied from a corresponding case for E_block, so that this flow typing still gets picked up after E_block has been rewritten away. | |||
| 2019-01-22 | Add a pragma for unrolling recursive functions | Alasdair Armstrong | |
| For example in RISC-V for the translation table walk: $optimize unroll 2 val walk32 ... function walk32 ... would create two extra copies of the walk_32 function, walk_32_unroll_1 and walk_32_unroll_2, with only walk_32_unroll_2 being recursive. Currently we only support the case where we have $optimize unroll, directly followed by a valspec, then a function, but this should be generalised in future. This optimization nearly doubles the performance of RISC-V It is implemented using a new Optimize.recheck rewrite that replaces the ordinary recheck_defs pass. It uses a new typechecker check_with_envs function that allows re-writes to utilise intermediate typechecking environments to minimize the amount of AST checking that occurs, for performance reasons. Note that older Sail versions including the current OPAM release will complain about the optimize pragma, so this cannot be used until they become up to date with this change. | |||
| 2019-01-22 | Make sure there is an ocaml representation for optimized memory read for | Alasdair | |
| RISC-V | |||
| 2019-01-22 | Make sure we optimize constrained union constructors | Alasdair | |
| 2019-01-21 | Update manual snapshot and add basic sail -latex documentation | Alasdair Armstrong | |
| 2019-01-21 | Add output directory option for generated Isabelle auxiliary theories | Thomas Bauereiss | |
| 2019-01-21 | Fix some issues with latex generation so manual builds again | Alasdair Armstrong | |
| since riscv is no longer in this repository, and we use the RISC-V duopod as an example, you need to build as: make RISCV=directory manual.pdf if directory is not equal to ../../sail-riscv (which is where it would be if sail and sail-riscv are checked out in the same respository together) | |||
| 2019-01-21 | Fix a bug with type-checking and latex generation | Alasdair Armstrong | |
| We should maybe just make the -latex option behavior the default to avoid this kind of thing | |||
| 2019-01-17 | Work around an issue with type abbreviations in HOL | Thomas Bauereiss | |
| If we use the bitlist representation of bitvectors, the type argument in type abbreviations such as "bits('n)" becomes dead, which confuses HOL; as a workaround, expand type synonyms in this case. | |||
| 2019-01-17 | Output configuration registers for Lem | Thomas Bauereiss | |
| Treat them as constants for now (with their initial value); in order to support updates, we would have to embed them properly into the monads. | |||
| 2019-01-17 | Fix bug in letbind_effects rewrite | Thomas Bauereiss | |
| Don't wrap effectful expressions in E_internal_return | |||
| 2019-01-16 | Latex: handle underscores when generating latex names. | Prashanth Mundkur | |
| 2019-01-14 | Add options for output directories for the lem and coq backends. | Prashanth Mundkur | |
| 2019-01-14 | Add a function to perform re-writes in parallel | Alasdair | |
| rewrite_defs_base_parallel j is the same as rewrite_defs_base except it performs the re-writes in j parallel processes. Currently only the trivial_sizeof re-write is parallelised this way with a default of 4. This works on my machine (TM) but may fail elsewhere. Because 2019 OCaml concurrency support is lacking, we use Unix.fork and Marshal.to_channel to send the info from the child processes performing the re-write back to the parent. Also fix a missing case in pretty_print_lem | |||
| 2019-01-14 | Support some more unification cases | Thomas Bauereiss | |
| 2019-01-14 | Make rewriting of foreach loops for Lem more robust | Thomas Bauereiss | |
| Bind loop bounds to type variables, and don't pull existential variables out of context | |||
| 2019-01-14 | Merge remote-tracking branch 'origin/sail2' into asl_flow2 | Alasdair | |
| 2019-01-11 | Updates for sail-arm release | Alasdair Armstrong | |
| We want to ensure that no_devices.sail and devices.sail have the same effect footprint, because with a snapshot-type release in sail-arm, we can't rebuild the spec with asl_to_sail every time we switch from running elf binaries to booting OS's. This commit allows registers to have arbitrary effects, so registers that are really representing memory-mapped devices don't have to have the wmem/rmem effect. | |||
| 2019-01-10 | Fixes so 8.5 with vector instructions compiles to C | Alasdair Armstrong | |
| 2019-01-09 | Coq: the division used in smt.sail should be Euclidean | Brian Campbell | |
| 2019-01-09 | Merge sail2 into monads | Thomas Bauereiss | |
| 2019-01-09 | Coq: add parens around negative integer literals | Brian Campbell | |
| 2019-01-08 | Improvements for v85 | Alasdair Armstrong | |
| 2019-01-04 | Add a few helper lemmas | Thomas Bauereiss | |
| 2019-01-03 | Make sure to close file handles when printing error messages | Alasdair Armstrong | |
| 2019-01-03 | Comment out bisect coverage in ocamlbuild files | Alasdair Armstrong | |
| 2019-01-02 | Coq: tweak recently introduced type check to ignore effects | Brian Campbell | |
| 2019-01-02 | ...without debug printing | Jon French | |
| 2019-01-02 | restore V_attempted_read behaviour after merge | Jon French | |
| 2018-12-31 | Last rewrite reordering needs more typechecking | Brian Campbell | |
| 2018-12-31 | Coq: move function clause merging to keep measure argument intact | Brian Campbell | |
| 2018-12-30 | Sort dependencies of termination measures properly | Brian Campbell | |
| 2018-12-29 | Coq: ensure that recursive functions compute | Brian Campbell | |
| 2018-12-29 | Add separate termination_measure declarations | Brian Campbell | |
| 2018-12-28 | Remove opt_spc_matches_prefix from sail.h (fixes C tests) | Jon French | |
| 2018-12-28 | Merge branch 'sail2' into rmem_interpreter | Jon French | |
| 2018-12-27 | Coq: avoid putting ambiguous numeric literals in Coq output | Brian Campbell | |
| There are situations when we really want a more refined expression, such as 8 * n instead of 64 (when we know n = 8 from a case split), but we might not be able to generate it. For now we generate an underscore and let Coq figure it out from the context. | |||
| 2018-12-27 | fix missed case in refactored val-spec extern parser | Jon French | |
| 2018-12-27 | Coq: fix name clashes and instantiation calculation | Brian Campbell | |
| 2018-12-27 | new command line option -marshal <file> to marshal out rewritten AST to a file | Jon French | |
| Adds new dependency: base64 | |||
| 2018-12-27 | remove unused previous-version-of-flow-typing functions from typechecker | Jon French | |
| (they store flow-typing info as functions; preparing for marshalling) | |||
| 2018-12-27 | basic Sail-side support for rmem use of interpreter | Jon French | |
| 2018-12-27 | refactor val-spec AST to store externs as an assoc-list rather than a ↵ | Jon French | |
| function (preparing for marshalling) | |||
| 2018-12-27 | pass typechecking environment around interpreter and rewriters | Jon French | |
| 2018-12-26 | More cleanup | Alasdair Armstrong | |
| Remove unused name schemes and DEF_kind | |||
| 2018-12-26 | Some cleanup | Alasdair Armstrong | |
| 2018-12-26 | Add makefile target for building with Bisect coverage | Alasdair Armstrong | |
| 2018-12-26 | More error messages improvments | Alasdair Armstrong | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |