| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-11-13 | add linenoise to .merlin | Jon French | |
| 2018-11-01 | Merge branch 'sail2' into rmem_interpreter | Jon French | |
| 2018-11-01 | Interpreter: last couple of builtins to get RISC-V working | Jon French | |
| 2018-10-29 | Merge pull request #21 from rems-project/riscv_c_platform | Alasdair Armstrong | |
| Merge C platform bits for RISC-V | |||
| 2018-10-24 | Add constraint synonyms | Alasdair Armstrong | |
| Currently not enabled by default, the flag -Xconstraint_synonyms enables them For generating constraints in ASL parser, we want to be able to give names to the constraints that we attach to certain variables. It's slightly awkward right now when constraints get long complicated because the entire constraint always has to be typed out in full whenever it appears, and there's no way to abstract away from that. This adds constraint synonyms, which work much like type synonyms except for constraints, e.g. constraint Size('n) = 'n in {1, 2, 4, 8} | 128 <= 'n <= 256 these constraints can then be used instead of the full constraint, e.g. val f : forall 'n, where Size('n). int('n) -> unit Unfortunatly we need to have a keyword to 'call' the constraint synonym otherwise the grammer stops being LR(1). This could be resolved by parsing all constraints into Parse_ast.atyp and then de-sugaring them into constraints, which is what happens for n-expressions already, but that would require quite a bit of work on the parser. To avoid this forcing changes to any other parts of Sail, the intended invariant is that all constraints appearing anywhere in a type-checked AST have no constraint synonyms, so they don't have to worry about matching on NC_app, or calling Env.expand_typquant_synonyms (which isn't even exported for this reason). | |||
| 2018-10-24 | Interpreter, RISC-V: move memory actions to parts of the interpreter ↵ | Jon French | |
| response and refactor RISC-V model accordingly | |||
| 2018-10-24 | RISC-V: add Sail implementations of just enough platform for interpreter to work | Jon French | |
| 2018-10-24 | add a couple things to gitignore | Jon French | |
| 2018-10-24 | Interpreter: add handling of undefs and sizeofs, and initialize registers to ↵ | Jon French | |
| undefined on startup | |||
| 2018-10-24 | Interpreter: improve error handling/messages | Jon French | |
| 2018-10-24 | src/Makefile: add isail.byte target for debugging interpreter | Jon French | |
| 2018-10-24 | Interpreter: don't silently use OCaml externs, only interpreter externs | Jon French | |
| (Adds 'interpreter' externs as appropriate.) | |||
| 2018-10-23 | RISC-V: switch c tests to use the C platform simulator; update .gitignore. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: use stderr for terminal output in OCaml backend. | Prashanth Mundkur | |
| Also add a brief README for booting Linux on the C and OCaml backends. | |||
| 2018-10-23 | RISC-V: separate jalr execute clause for seq model and rmem. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: Initial splitting of instructions across multiple files. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: Allow the C platform to get the DTB from a file, so that OS boot is ↵ | Prashanth Mundkur | |
| possible without linking to Spike. When linked with Spike, ensure that the DTBs being used are identical. | |||
| 2018-10-23 | RISC-V: add cli option to dump the platform device-tree. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: Add a platform knob to control mtval contents on illegal instruction ↵ | Prashanth Mundkur | |
| faults. | |||
| 2018-10-23 | RISC-V: various fixes | Prashanth Mundkur | |
| - add mstatus to cross-check - fix typo in assembly mapping for lr/sc | |||
| 2018-10-23 | RISC-V: fix: sstatus.SD depends on .XS and .FS. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: adjust main loop for the non-spike case. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: implement terminal output for C platform. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: tick the clock in the C platform. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: Add device tree blob into rom, currently only when linked against spike. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: add default reset vector. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: fix up platform bits for lr/sc. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: set htif tohost port address using ELF symbol. | Prashanth Mundkur | |
| 2018-10-23 | RTS: Add elf symbol lookup support. | Prashanth Mundkur | |
| 2018-10-23 | Fix typo in plat_ram_size | Alasdair Armstrong | |
| 2018-10-23 | RISC-V: Add some debug logs for within_phys_mem. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: Allow Spike linkage to be conditionally enabled. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: flush logs at each step. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: Flesh out more of the tandem checks in the C platform simulator. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: An initial C Sail model linked against Spike for testing. | Prashanth Mundkur | |
| 2018-10-23 | RTS: allow elf-loader to provide entry info. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: Refactor c platform bits. | Prashanth Mundkur | |
| 2018-10-22 | Coq: use function type more carefully in untupling | Brian Campbell | |
| And update the RISC-V patch accordingly. | |||
| 2018-10-22 | Update Coq patch for RISC-V, add string_take to Coq library | Brian Campbell | |
| 2018-10-22 | Coq: work around constructors with tupled arguments | Brian Campbell | |
| 2018-10-22 | Fix lem arguments for functions with tuple arguments | Alasdair Armstrong | |
| Make lem output understand difference between functions taking a tuple and functions taking multiple arguments. Previously it assumed that no functions ever took a tuple as an argument, which is incorrect for mappings. | |||
| 2018-10-22 | Merge branch 'sail2' into rmem_interpreter | Jon French | |
| 2018-10-22 | Pretty_print_lem.untuple_args_pat: temporary hack to allow functions that ↵ | Jon French | |
| actually take a tuple argument | |||
| 2018-10-16 | Merge branch 'sail2' into rmem_interpreter | Jon French | |
| 2018-10-16 | add a couple more RISC-V things to gitignore | Jon French | |
| 2018-10-16 | Re-implement space-related mapping functions in Sail rather than backends | Jon French | |
| Uses new primop 'string_take' which is much easier to implement in e.g. C | |||
| 2018-10-16 | rewrites: remove now-unnecessary temporary string hack from ↵ | Jon French | |
| rewrite_defs_pat_lits | |||
| 2018-10-15 | Update manual snapshot | Alasdair Armstrong | |
| 2018-10-15 | Ocaml backend: omit function definitions for externs | Jon French | |
| 2018-10-15 | Add interpreted RISC-V model to test suite | Jon French | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |