| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-08-22 | rewrite_defs_pat_lits: add an explicit type annotation around generated id ↵ | Jon French | |
| pattern | |||
| 2018-08-21 | C: Correctly handle the kinds of patterns generated by mappings | Alasdair Armstrong | |
| This change allows the RISC-V spec to compile to C, but more testing is needed to ensure it works correctly. | |||
| 2018-08-20 | Refactor tuple conversions in Sail to C compilation | Alasdair Armstrong | |
| Make the C l-expression type in Sail more generic and expressive, and refactor the generation of conversions into a seperate codegen_conversion function, which can handle more complex cases than the previous more ad-hoc method. | |||
| 2018-08-18 | Correctly handle specialising polymorphic types in nested unions | Alasdair | |
| Ensure that this works even when the union types are dependent in the wrong order, before topologically sorting definitions. We do this by calling fix_variant_ctyps on all cdefs by passing a list of prior cdefs to specialize_variants. | |||
| 2018-08-18 | Correctly specialise type annotation in polymorphic functions | Alasdair | |
| 2018-08-17 | Improve builtins tests | Alasdair Armstrong | |
| Test the builtin functions by compiling them to C, OCaml, and OCaml via Lem. Split up some of the longer builtin test programs to avoid stack overflows when compiling to OCaml, as 3000+ line long blocks can cause issues with some re-writing steps. Also test constant-folding with builtins (this should reduce the asserts in these files to assert true), and also test constant folding with the C compilation. Fix a bug whereby vectors with heap-allocated elements were not initialized correctly. Fix a bug caused by compiling and optimising empty vector literals. Fix an OCaml test case that broke due to the ref type being used. Now uses references to registers. Fix a bug where Sail would output big integers that lem can't parse. Checks if integer is between Int32.min_int and Int32.max_int and if not, use integerOfString to represent the integer. Really this should be fixed in Lem. Make the python test runner script the default for testing builtins and running the C compilation tests in test/run_tests.sh Add a ocaml_build_dir option that sets a custom build directory for OCaml. This is needed for running OCaml tests in parallel so the builds don't clobber one another. | |||
| 2018-08-17 | Coq: also introduce autocast at type annotations | Brian Campbell | |
| 2018-08-17 | Extend guarded patterns rewriting to exception catching | Brian Campbell | |
| Also fix nested matches and generic rewriting under E_throw. | |||
| 2018-08-16 | Add the type an expression was checked against to tannots, and use for Coq | Brian Campbell | |
| Tweak extra Coq files to match. Tweak early return rewrite to use declared return type, which can always be put into an E_cast. | |||
| 2018-08-16 | Use Set rather than Hashtbl in graph.ml | Alasdair Armstrong | |
| Removes the need for the node type to have a valid Hash function | |||
| 2018-08-16 | Remove unused ref type | Alasdair Armstrong | |
| 2018-08-16 | Various cleanups to ott grammar | Alasdair Armstrong | |
| Add additional well-formedness check when calling typing rules | |||
| 2018-08-15 | Temporary fix for RISC-V Lem generation | Brian Campbell | |
| 2018-08-15 | Get RISC-V on Coq into reasonable state to show | Brian Campbell | |
| - Fill in Coq builtins for more of the RISC-V prelude - Update Barriers - More general autocast - Temporary sub_nat definition (until the backend handles nat better) - Patch to bring results into a reasonable state - Use Let rather than Definition for non-dependent top-level values | |||
| 2018-08-14 | Improve error messages from C backend, and fix issues with assigning to pointers | Alasdair Armstrong | |
| 2018-08-14 | Remove some comments from C output | Alasdair Armstrong | |
| Cleanup some debugging output | |||
| 2018-08-14 | Merge remote-tracking branch 'origin/sail2' into polymorphic_variants | Alasdair Armstrong | |
| 2018-08-13 | Add graph library graph.ml, and use to correctly sort type definitions | Alasdair | |
| 2018-08-13 | Remove old specialisation code in specialize.ml | Alasdair | |
| 2018-08-13 | Sort ctype_defs in dependency order after specialisation | Alasdair | |
| We now generate anonymous types in the correct order, but post specialisation more dependencies can occur between named types, so an additional sorting step is needed to ensure that these happen in the correct order. In theory we could end up with circular dependencies here that don't exist at the Sail source level, but this shouldn't occur often (or ever) in practice. I think this is fixable but it would require some code generator changes. | |||
| 2018-08-13 | Coq: drop redundant final wildcard clauses | Brian Campbell | |
| Deals with pattern matches generated from mappings, plus the occasional error. | |||
| 2018-08-13 | Guarded clauses rewrite: variable patterns subsume enums | Brian Campbell | |
| Prevents redundant clauses. | |||
| 2018-08-12 | Coq: handle enums in binders, make top-level patterns exhaustive | Brian Campbell | |
| 2018-08-10 | Coq: add some of string library | Brian Campbell | |
| 2018-08-09 | Fix a bug by ensuring that monomorphic variant constructors do not get ↵ | Alasdair Armstrong | |
| lifted types Add a test case for nested variant constructors | |||
| 2018-08-09 | Add type information to AP_app constructors | Alasdair Armstrong | |
| 2018-08-09 | Fix bugs involving multi-argument variant type constructors | Alasdair Armstrong | |
| 2018-08-09 | Coq: debugging on top-level lets | Brian Campbell | |
| 2018-08-09 | Coq: tidy up debugging messages | Brian Campbell | |
| 2018-08-09 | Coq: decompose dependent pairs at internal_plet as well as let | Brian Campbell | |
| 2018-08-09 | Coq: handle nats like ranges, not atoms | Brian Campbell | |
| 2018-08-08 | Fix ordering of generated anonymous types for each cdef | Alasdair Armstrong | |
| 2018-08-07 | Revert "Warnings: deal with all the deprecation warnings" | Alasdair Armstrong | |
| One day we will be free from the 4.02.3 menace, but today is not that day. :( This should fix Sail on Jenkins This reverts commit 86e29bcbb1597c4ef1f6cae8edbeed42f9a31414. | |||
| 2018-08-07 | More updates for fixing variant types | Alasdair Armstrong | |
| 2018-08-07 | Lem: print more bitvector types | Brian Campbell | |
| Especially for return expressions, which fixes a test case | |||
| 2018-08-07 | Fix propagation of overly-specific types in early_return rewrite | Brian Campbell | |
| 2018-08-07 | Improve cast introduction for Lem | Brian Campbell | |
| Handles mutable variables and conditionals (there are still some corner cases that don't appear in Aarch64 to do). The pretty printer is now back to preferring to use concrete types, but has a special case for casts to print more general types. | |||
| 2018-08-06 | Cast each argument to a polymorphic constructor into it's most general type | Alasdair Armstrong | |
| 2018-08-06 | Make sure monomorphic constructors are preserved | Alasdair Armstrong | |
| 2018-08-06 | Add a simple test case for polymorphic variant type | Alasdair Armstrong | |
| 2018-08-06 | More fixes for polymorphic data types | Alasdair Armstrong | |
| 2018-08-03 | More work on fixing polymorphic constructor monomorphisation | Alasdair Armstrong | |
| 2018-08-03 | Fix existential variable problems in monomorphisation | Brian Campbell | |
| One due to using raw types from the type checker in casts without trying to turn them into sane types, the other due to forgetting to use the constraint when trying to simplify sizes in existential types. Both triggered because the type checker now records more specific types. | |||
| 2018-08-03 | Coq: generalise dependent pair handling a little | Brian Campbell | |
| 1. for monadic values (not in a terribly useful way, though) 2. for more types | |||
| 2018-08-02 | Coq: remove type removal holdover from Lem backend, add MIPS lemma | Brian Campbell | |
| 2018-08-02 | Coq: proper precedence for constraints (both prop and bool) | Brian Campbell | |
| 2018-08-02 | Start working on a solution for correctly monomorphising polymorphic variant ↵ | Alasdair Armstrong | |
| types | |||
| 2018-08-01 | Remove old test directory in src/test | Alasdair Armstrong | |
| 2018-08-01 | Coq: implicit range conversions for function arguments, debug tracing | Brian Campbell | |
| The new option -dcoq_debug_on takes a list of functions to output tracing on. | |||
| 2018-07-27 | Remove unused U_effect constructor | Alasdair Armstrong | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |