| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |||
| 2018-06-08 | Coq: fix axiom generation | Brian Campbell | |
| 2018-06-08 | Coq: update foreach handling, correct field accesses | Brian Campbell | |
| 2018-06-08 | Coq: correct failure on unsupported undefined values | Brian Campbell | |
| 2018-06-08 | Coq: use record update syntax (only single fields work for now) | Brian Campbell | |
| 2018-06-08 | Coq: correct implicitness of type arguments in unions | Brian Campbell | |
| 2018-06-07 | Fix bug in add_bits optimization | Alasdair Armstrong | |
| 2018-06-07 | Fix a small bug in monomorphisation | Thomas Bauereiss | |
| 2018-06-06 | Fix a typo. | Yao Li | |
| 2018-06-07 | Add a constant folding optimization pass | Alasdair | |
| 2018-06-06 | Factor utility functions for IR into separate file and struct update ↵ | Alasdair Armstrong | |
| optimizations. Move the utility functions for graph generation and pretty printing of intermediate representation instructions into a separate file, bytecode_util.ml, by analogy with ast_util.ml. Add an optimization pass that searches for specific patterns of struct updates and removes uncessary copying of the structs involved. With this optimisation pass the time taken for u-boot to run approx 57,000,000 instructions goes down from about 11-12 minutes to 8 minutes (about 120,000 IPS). | |||
| 2018-06-06 | Some additional fixes to C backend. Re-enable primitive optimizations. | Alasdair Armstrong | |
| Also add an additional -Oz3 flag that uses z3 to optimize some additional types. This is currently very experimental and doesn't fully work yet. | |||
| 2018-06-06 | Some work on improving error messages | Alasdair Armstrong | |
| We now store the location where type variables were bound, so we can use this information when printing error messages. Factor type errors out into type_error.ml. This means that Type_check.check is now Type_error.check, as it previously it handled wrapping the type_errors into reporting_basic errors. Type_check.check' has therefore been renamed to Type_check.check. | |||
| 2018-06-04 | Fix an issue with riscv_platform involving flow typing | Alasdair Armstrong | |
| - Refactor the flow typing implementation in the type-checker. This should fix an issue involving riscv_platform. Specifically it should now work better when an if statement contains multiple conditions combined with and/or, only some of which imply constraints at the type level. This change also simplifies the implementation of flow typing, and removes some obscure features that were hardly used - specifically, flow typing could modify types, but this was fairly obscure and doesn't seem to affect any of our specifications. More testing is needed to ensure that this change hasn't inadvertantly broken anything, but it does pass all our tests and continue to typecheck arm, riscv and cheri. - Also adds a option for generating faster undefined functions for enum and variant types. Previously I tried to optimise away such functions in the C backend, because they could be slow and cause considerable uneccessary allocation, however this was error prone and it turns out a much simpler solution is to simply make the functions themselves much faster, at the cost of hard-coding certain decisions about what undefined means for these types at compile tile (which is fine for fast emulation). This almost doubles the performance of the generated C code. - Add a wrapper for right shift to avoid UB when shifting by 64 or more places. | |||
| 2018-06-04 | Fix bug with function return types in C backend | Alasdair Armstrong | |
| 2018-06-04 | switch to using a Map data structure for cheri tags in ocaml backend. This ↵ | Robert Norton | |
| solves a problem where the Hashtbl module was encountering a stack overflow booting CheriBSD. There seems to be little or no performance impact. | |||
| 2018-06-04 | Use Util.split_on_char in sail_lib.ml | Alasdair Armstrong | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |