| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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-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 | Fix bug in elf_loader: zero memory when segment memsz exceeds size. | Prashanth Mundkur | |
| 2018-06-22 | Coq: use simple forms for simple pattern matches in E_internal_let | Brian Campbell | |
| 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 | 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: 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-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 | Coq: use undefined_bitvector | 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 | Coq: better handling of identifiers, esp infix ones | Brian Campbell | |
| 2018-06-15 | Fixes for C RTS for aarch64 no it's split into multiple files | Alasdair Armstrong | |
| Fix a bug involving indentifers on the left hand side of assignment statements not being shadowed correctly within foreach loops. Make the different between different types of integer division explicit in at least the C compilation for now. fdiv_int is division rounding towards -infinity (floor). while tdiv_int is truncating towards zero. Same for fmod_int and tmod_int. | |||
| 2018-06-14 | rename all lem support files to sail2_foo to avoid conflict with sail1 in rmem | Jon French | |
| 2018-06-14 | provide impl of int_of_string_opt in Sail_lib to support older Ocaml versions | Jon French | |
| 2018-06-14 | Refactor C backend, and split RTS into multiple files | Alasdair | |
| 2018-06-13 | Tracing instrumentation for C backend | Alasdair Armstrong | |
| 2018-06-13 | Coq: library updates, informative type errors, fix type aliases | Brian Campbell | |
| (The last bit is to declare type aliases as Type so that Coq uses the type scope for notation, so * is prod, not multiplication). | |||
| 2018-06-12 | Coq: Handle simple top-level type variable definitions | Brian Campbell | |
| (also another error reporting improvement) | |||
| 2018-06-12 | Coq: upgrade some errors to report locations | Brian Campbell | |
| 2018-06-12 | Coq: support for range type, along with related existential improvements | Brian Campbell | |
| Plus - Complete solver support for inequalities - Reduce exponentials in solver | |||
| 2018-06-11 | add 'pat as id' mapping-patterns | Jon French | |
| 2018-06-11 | More efficient bitfield implementation | Alasdair Armstrong | |
| 2018-06-11 | Merge branch 'sail2' into mappings | Jon French | |
| (involved some manual tinkering with gitignore, type_check, riscv) | |||
| 2018-06-11 | change double-caret for string-append-pattern to single caret, since that ↵ | Jon French | |
| wouldn't be legal in a pattern anyway | |||
| 2018-06-11 | better type inference of union-constructors and mappings | Jon French | |
| 2018-06-09 | Fix issue in C_backend, and run C tests with undefined behavior sanitizer | Alasdair | |
| 2018-06-09 | Fix issue with catch block return values not being compiled correctly | Alasdair | |
| This should fix the issue raised in commit 45554f Adds a test loop_exception that tests throwing exceptions in loops, various looping constructs, and returning values from try/catch blocks. Also modified the test-suite to test C compiled output both with and without optimisations | |||
| 2018-06-08 | Fix use of non-tail-recursive calls in elf_loader. | Prashanth Mundkur | |
| 2018-06-08 | type checking mappings: allow inferring based on the other side's id inferences | Jon French | |
| 2018-06-08 | Coq: some handling of existential types as function return types | Brian Campbell | |
| 2018-06-08 | Coq: add destructuring of atom existentials in patterns | Brian Campbell | |
| Plus test case, broken builtin name | |||
| 2018-06-08 | Coq: track add_typquant change | Brian Campbell | |
| 2018-06-08 | Correct dependencies of bytecode sail | Brian Campbell | |
| 2018-06-08 | Coq: existential and constraint solving work | Brian Campbell | |
| - add existential unpacking for function arguments - add mechanism for using properties for existentially typed top-level values (useful for the typechecking tests) - support for length_list and In in Coq constraint solving | |||
| 2018-06-08 | Coq: some very basic existential support | Brian Campbell | |
| Only single variable in places, only packed at literals and variables, no unpacking | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |