| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-06-26 | Fix duplicate riscv mem-ea, spotted by Jon French. | Prashanth Mundkur | |
| 2018-06-26 | Add configuration registers so __SetConfig ASL can be translated | Alasdair Armstrong | |
| Registers can now be marked as configuration registers, for example: register configuration CFG_RVBAR = 0x1300000 They work like ordinary registers except they can only be set by functions with the 'configuration' effect and have no effect when read. They also have an initialiser, like a let-binding. Internally there is a new reg_dec constructor DEC_config. They are intended to represent configuration parameters for the model, which can change between runs, but don't change during execution. Currently they'll only work when compiled to C. Internally registers can now have custom effects for reads and writes rather than just rreg and wreg, so the type signatures of Env.add_register and Env.get_register have changed, as well as the Register lvar, so in the type checker we now write: Env.add_register id read_effect write_effect typ rather than Env.add_register id typ For the corresponding change to ASL parser there's a function is_config in asl_to_sail.ml which controls what becomes a configuration register for ARM. Some things we have to keep as let-bindings because Sail can't handle them changing at runtime - e.g. the length of vectors in other top-level definitions. Luckily __SetConfig doesn't (yet) try to change those options. Together these changes allow us to translate the ASL __SetConfig function, which means we should get command-line option compatibility with ArchEx for running the ARM conformance tests. | |||
| 2018-06-26 | Main: further refinement of execution cycle | Alastair Reid | |
| Mostly improving error messages | |||
| 2018-06-26 | Prelude: as received from Alasdair | Alastair Reid | |
| 2018-06-26 | Main: attempt to capture AArch64 execution cycle | Alastair Reid | |
| 2018-06-26 | mips: fix duplication of cycle_count call that arose due to git merge. | Robert Norton | |
| 2018-06-26 | mips: comment out printing of EXCEPTION on every ISA exception. | Robert Norton | |
| 2018-06-26 | turn on warnings when compiling mips c then dial back ones that are ↵ | Robert Norton | |
| triggered by generated code (probably false positives). Fix some warnings in rts.c | |||
| 2018-06-26 | RTS: implement sleep primitives | Alastair Reid | |
| Note that an alternative implementation choice is just to implement them as SAIL functions manipulating a global variable. Not sure which is better. | |||
| 2018-06-26 | RTS: stub support for -C command line option | Alastair Reid | |
| 2018-06-26 | ELF: Restore error messages in ELF reader | Alastair Reid | |
| 2018-06-26 | In guarded pattern rewriting, irrefutable patterns subsume wildcards | Brian Campbell | |
| Necessary to prevent redundant clauses that Coq will reject (There's still a problem if you use a variable rather than a wildcard, see the test) | |||
| 2018-06-26 | In elf_loader don't attempt to convert paddr to int64 because on MIPS it is ↵ | Robert Norton | |
| quite likely to exceed representable range of signed 64-bit integer (e.g. address starting 0x9...). Also make clear which values are displayed in hex vs. decimal. | |||
| 2018-06-25 | Add a riscv platform parameter to control trapping to M-mode on misaligned ↵ | Prashanth Mundkur | |
| access, and a cli option to control it. | |||
| 2018-06-25 | Increment the riscv trace step counter only when instructions are executed. | Prashanth Mundkur | |
| 2018-06-25 | Hook in the missed misa legalizer. | Prashanth Mundkur | |
| 2018-06-25 | Fix riscv interrupt pending check to handle implicit enabling at lower ↵ | Prashanth Mundkur | |
| privileges. Also fix timer threshold comparison to be <= instead of <. | |||
| 2018-06-25 | Make sstatus.UXL legalization match spike for now. Leave a fixme to make ↵ | Prashanth Mundkur | |
| this a platform setting. | |||
| 2018-06-25 | Fix a missed fixme for the sstatus view of mstatus. | Prashanth Mundkur | |
| 2018-06-25 | Fix tracecmp for spike's recursive calls for sie/sip/sstatus csr writes. | Prashanth Mundkur | |
| 2018-06-25 | Check for variables in disjointness check | Thomas Bauereiss | |
| 2018-06-25 | Support bitlist representation in Sail2_string | Thomas Bauereiss | |
| 2018-06-25 | Fix a bug in pattern guard rewriting | Thomas Bauereiss | |
| Remember and use fallthrough clauses instead of dropping them when the last clause in a group has a guard | |||
| 2018-06-25 | Coq: add typeclass based comparison, and instantiate for enums | Brian Campbell | |
| 2018-06-25 | Coq: automatic cast introduction | Brian Campbell | |
| 2018-06-25 | Use getopt rather than argp for Mac compatibility in C runtime | Alasdair Armstrong | |
| Also further tweaks to Sail library for C and include sail lib files for tracing | |||
| 2018-06-25 | add device tree file for mips. | Robert Norton | |
| 2018-06-25 | mips: add optional tracing of register writes (commented out). | Robert Norton | |
| 2018-06-25 | flush stdout after putchar for terminal emulation purposes. | Robert Norton | |
| 2018-06-25 | Fix bugs in mips ldl/ldr that were probably introduced in porting to sail2. | Robert Norton | |
| 2018-06-23 | Add clock tick checks to the riscv tracecmp tool. | Prashanth Mundkur | |
| 2018-06-23 | Fix a missing check for interrupt dispatch when riscv clint registers are ↵ | Prashanth Mundkur | |
| written. | |||
| 2018-06-23 | Split Sail->ANF translation into its own file | Alasdair | |
| Refactor the C compilation process by moving out the conversion to A-normal form into its own file. Also make the A-normal form AST parameterised by the type of the types annotating it. The idea being we can have a typ aexp -> ctyp aexp translation, converting to low-level types at a slightly higher level before mapping into our low-level IR. This would fix some issues we have where the type of variables change due to flow typing, because we could map the sail types to low-level types in the ANF ast where we still have some knowledge about the structure of the original Sail. | |||
| 2018-06-22 | Make riscv pte dirty-bit update handling configurable via a platform cli option. | Prashanth Mundkur | |
| Fix a redundant clock tick. | |||
| 2018-06-22 | Some more riscv trace log tweaking for spike compatibility. | Prashanth Mundkur | |
| 2018-06-22 | Add cli options to riscv simulator to dump platform device-tree info. | Prashanth Mundkur | |
| 2018-06-22 | Fix Lem build of MIPS/CHERI | Thomas Bauereiss | |
| 2018-06-22 | Add a simple trace log comparison tool for riscv vs. a patched spike. | Prashanth Mundkur | |
| 2018-06-22 | Fix up constraints in OCaml reg_ref test | Brian Campbell | |
| 2018-06-22 | Add current state of mips_extras.v | Brian Campbell | |
| 2018-06-22 | Precise bitvector subrange functions for Coq. | Brian Campbell | |
| Also fix the constraints in the standard prelude files, add a couple of useful cast rewriting lemmas. | |||
| 2018-06-22 | Fix bug in elf_loader: zero memory when segment memsz exceeds size. | Prashanth Mundkur | |
| 2018-06-22 | More trace log tweaks. | Prashanth Mundkur | |
| 2018-06-22 | Add bitvector size constraints in MIPS | Brian Campbell | |
| 2018-06-22 | Add coq builtins for MIPS | Brian Campbell | |
| 2018-06-22 | Add coq generation rule for mips | Brian Campbell | |
| 2018-06-22 | Coq: use simple forms for simple pattern matches in E_internal_let | Brian Campbell | |
| 2018-06-22 | Coq: library updates, esp extending bitvector multiplies, Undefined | Brian Campbell | |
| 2018-06-22 | Coq: project away range types in comparisons | Brian Campbell | |
| 2018-06-22 | build mips and mips_c when running tests. | Robert Norton | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |