| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-06-27 | Fix reading reals from strings in C lib | Alasdair Armstrong | |
| 2018-06-27 | libsail: optimise real_power | Alastair Reid | |
| The Arm spec uses the value 2.0^1000000 to represent infinity so it is worth making real_power take logarithmic time. | |||
| 2018-06-27 | Add a mips_c_gcov target that builds mips_c model with coverage reporting. | Robert Norton | |
| 2018-06-27 | Add a new function cycle_limit_reached that returns bool, allowing for ↵ | Robert Norton | |
| graceful exit on reaching cycle limit. This aids coverage and valgrind instrumentation. | |||
| 2018-06-27 | Fix real implementation in C to use GMP rationals | Alasdair Armstrong | |
| Implement square root function for rationals up to an arbitrary precision, currently 30 decimal places. May need to increase this for ARM tests. | |||
| 2018-06-27 | Main: refactor fetch_and_execute | Alastair Reid | |
| No functional change | |||
| 2018-06-27 | RTS: __SetConfig support is off by default | Alastair Reid | |
| Use -DHAVE_SETCONFIG to enable __SetConfig support | |||
| 2018-06-27 | RTS: Add support for __ListConfig | Alastair Reid | |
| 2018-06-27 | RTS: Delete __SetConfig stub function | Alastair Reid | |
| This is now directly supported from SAIL so we can call the SAIL __SetConfig function instead. | |||
| 2018-06-27 | Make sure __SetConfig gets included in generated code | Alasdair Armstrong | |
| 2018-06-27 | Main: fix PC advance after HINT and other EndOfInstruction | Alastair Reid | |
| 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 | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |