| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2018-06-20 | Coq: reverse_endianness | Brian Campbell | |
| 2018-06-20 | Coq: add missing existential projection on simple let expressions | Brian Campbell | |
| 2018-06-20 | Coq: Tidy up libraries, export String | Brian Campbell | |
| 2018-06-20 | Coq: print div/mod/abs in nexps; avoid mod as an identifier | Brian Campbell | |
| 2018-06-20 | Coq: port handling of effectful and/or from Lem backend | Brian Campbell | |
| 2018-06-20 | Coq: a few more ops | Brian Campbell | |
| 2018-06-19 | Minor optimization in ocaml_backend to use ints instead of strings for ↵ | Prashanth Mundkur | |
| Big_int literals. Improves tests/riscv duration by around 2% and size of riscv.o by 15%. | |||
| 2018-06-19 | Add more detail to riscv execution trace log. | Prashanth Mundkur | |
| 2018-06-19 | Coq: use undefined_bitvector | Brian Campbell | |
| 2018-06-19 | Coq: library name update (as we did for Lem) | Brian Campbell | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |