| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-07-02 | Coq: add some string functions | Brian Campbell | |
| 2018-07-02 | Coq: replace simpl in a tactic with a more precise "change" | Brian Campbell | |
| Prevents partial unfolding of Z.pow. | |||
| 2018-06-30 | RTS: fix replicate_bits | Alastair Reid | |
| Fixes handling of Replicate(x, 0). | |||
| 2018-06-30 | RTS: Add length asserts to bits ops | Alastair Reid | |
| Added assertions to check that length of bit operations is sensible (i.e., consistent with type system). | |||
| 2018-06-30 | Fix an issue with vector_update_subrange | Alasdair | |
| vector_update_subrange wasn't setting its return length correctly | |||
| 2018-06-29 | RTS: tweak TIMEOUT message | Alastair Reid | |
| Making the message more like archex messages simplifies tooling. Plus, it is a better message. | |||
| 2018-06-28 | RTS: Fix utterly broken command line parsing | Alastair Reid | |
| 2018-06-28 | RTS: Add --verbosity flag to C model | Alastair Reid | |
| This is interpreted as a set of bits that control various bits of output. Bit 0 is print the PC on every cycle. (It would probably be useful to standardise a few of these flags across all models. Other candidates are accesses to physical memory, throwing SAIL exceptions, current privilege level, ...) | |||
| 2018-06-28 | Add tagged memory to C rts to cheri can be compiled to C | Alasdair Armstrong | |
| 2018-06-28 | Fix warning in rts.c | Robert Norton | |
| 2018-06-28 | Add option to build ocaml with bisect_ppx coverage support. Add cheri ↵ | Robert Norton | |
| targets using this. | |||
| 2018-06-28 | RTS: Add missing #include | Alastair Reid | |
| Every Unix is subtly different. | |||
| 2018-06-27 | RTS/Main: tweaking cycle counter handling | Alastair Reid | |
| 2018-06-27 | Actually fix real literals, and add a test for various properties | Alasdair Armstrong | |
| 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 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 | 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-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-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 | flush stdout after putchar for terminal emulation purposes. | Robert Norton | |
| 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 | Add coq builtins for MIPS | 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-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 | 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-20 | Coq: reverse_endianness | Brian Campbell | |
| 2018-06-20 | Coq: Tidy up libraries, export String | 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 | Coq: library name update (as we did for Lem) | Brian Campbell | |
| 2018-06-19 | Add elf parsing from Alastair | Alasdair Armstrong | |
| 2018-06-19 | Improvements to Sail C for booting Linux | Alasdair Armstrong | |
| 2018-06-18 | Separate bitvector access/update from generic vector access in std prelude | Brian Campbell | |
| (necessary for backends where they're different) Coq uint/sint and related fixes | |||
| 2018-06-18 | Coq: fix up some comparison operations in prelude | Brian Campbell | |
| 2018-06-18 | Coq: update prompt monad wrt Lem | Brian Campbell | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |