| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2018-06-22 | add support for new cycle_limit feature in mips. | Robert Norton | |
| 2018-06-21 | Add command line option support for Sail->C compiled models | Alasdair Armstrong | |
| For example, the MIPS model can boot FreeBSD as ./mips_c --binary=0x100000,/path/to/kernel --image=/path/to/simboot.sailbin Or with short options as ./mips_c -b 0x100000,/path/to/kernel -i /path/to/simboot.sailbin The current options are: -e, --elf, which loads an elf file directly -n, --entry, which sets the entry point -i, --image, which loads an image file compiled by "sail -elf" using Linksem -b, --binary, which loads a plain binary image into memory at a specific address -l, --cyclelimit, which means the (new) cycle_count() builtin exits the model after a certain number of calls Also there are the default -? --help and --usage options. | |||
| 2018-06-21 | Follow Sail2 renaming in Isabelle library | Thomas Bauereiss | |
| 2018-06-21 | Remove loading kernel from mips main | Alasdair Armstrong | |
| 2018-06-21 | Merge branch 'sail2' of github.com:rems-project/sail into sail2 | Alasdair Armstrong | |
| 2018-06-21 | add PMP registers to CSR, fix build | Jon French | |
| 2018-06-21 | Merge branch 'tracing' into sail2 | Alasdair Armstrong | |
| 2018-06-21 | Fix MIPS wrt changes to C runtime | Alasdair Armstrong | |
| This plus changes to bitfield internals is enough to run some MIPS tests at 1Mhz. | |||
| 2018-06-21 | Simplify the ANF->IR translation | Alasdair Armstrong | |
| Previously the ANF->IR translation cared too much about how things were allocated in C, so it had to constantly check whether things needed to be allocated on the stack or heap, and generate different cequences of IR instructions depending on either. This change removes the ialloc IR instruction, and changes iinit and idecl so that the code generator now generates different C for the same IR instructions based on the variable types involved. The next change in this vein would be to merge icopy and iconvert at the IR level so that conversions between uint64_t and large-bitvectors are inserted by the code generator. This would be good because it would make the ANF->IR translation more robust to changes in the types of variables caused by flow-typing, and optimization passes could convert large bitvectors to uint64_t as local changes. | |||
| 2018-06-21 | changes to riscv model to support rmem | Jon French | |
| 2018-06-20 | Coq: Generate MR when appropriate; syntax fixes | Brian Campbell | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |