| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-09-12 | Coq: remove extra "True"s from constraints | Brian Campbell | |
| The omega tactic doesn't like them | |||
| 2018-09-11 | Coq: some basic handling for more existentials | Brian Campbell | |
| 2018-09-11 | Coq: remove a bunch of Lem-isms | Brian Campbell | |
| In particular, the complicated "what nexps are in scope" test can be replaced by a simple "are the nvars in scope" check. | |||
| 2018-09-11 | Update coq-riscv snapshot patch and README | Brian Campbell | |
| 2018-09-10 | RISC-V: move the PC and minstret updates into the step function, to better ↵ | Prashanth Mundkur | |
| localize them, making loop() purely a platform function. | |||
| 2018-09-10 | C: Add documentation for C compilation in manual.tex | Alasdair Armstrong | |
| 2018-09-10 | Various fixes | Alasdair Armstrong | |
| C: Don't print usage message and quit when called with no arguments, as this is used for testing C output OCaml: Fix generation of datatypes with multiple type arguments OCaml: Generate P_cons pattern correctly C: Fix constant propagation to not propagate letbindings with type annotations. This behaviour could cause type errors due to how type variables are introduced. Now we only propagate letbindings when the type of the propagated variable is guaranteed to be the same as the inferred type of the binding. Tests: Add OCaml tests to the C end-to-end tests (which really shouldn't be in test/c/ any more, something like test/compile might be better). Currently some issues with reals there like interpreter. Tests: Rename list.sail -> list_test.sail because ocaml doesn't want to compile files called list.ml. | |||
| 2018-09-07 | C: Support RISC-V in elf loader. | Prashanth Mundkur | |
| 2018-09-07 | C: add a usage message to the rts. | Prashanth Mundkur | |
| 2018-09-07 | Jenkins: Fix Jenkins issue with RISC-V test suite | Alasdair Armstrong | |
| 2018-09-07 | RISCV: Run RISC-V tests using version compiled to C | Alasdair Armstrong | |
| Current pass rate is 170 out of 181. Looks like there are some issues with rv64ua-p-lrsc.elf, rv64ua-v-lrsc.elf, and rv64uc-p-rvc.elf which I think are caused by me not implementing parts of the RISC-V platform correctly in C. Some of the div and mod tests also fail, which is probably an issue with using the correct rounding. | |||
| 2018-09-06 | C: Fix a bug with shadowing in nested let-bindings | Alasdair | |
| 2018-09-06 | Coq: update RISC-V snapshot | Brian Campbell | |
| 2018-09-06 | Coq: fill in a few more RISC-V axioms | Brian Campbell | |
| 2018-09-06 | Coq: more string handling | Brian Campbell | |
| 2018-09-06 | Coq: fix up some barrier/memory definitions for RISC-V | Brian Campbell | |
| 2018-09-06 | RISCV: Get enough of the RISCV platform into C to run some tests | Alasdair Armstrong | |
| 2018-09-06 | Allow options to be set in the interactive mode | Alasdair Armstrong | |
| Also allow options to be set via a pragma in Sail files | |||
| 2018-09-05 | Coq: fill in trivial ranges in constraint solver | Brian Campbell | |
| 2018-09-04 | C: add an option to control generation of main(). | Prashanth Mundkur | |
| 2018-09-04 | C: split out setup/init and teardown functions from main(). | Prashanth Mundkur | |
| 2018-09-04 | C: Tweaks to RISC-V to get compiling to C | Alasdair Armstrong | |
| Revert a change to string_of_bits because it broke all the RISC-V tests in OCaml. string_of_int (int_of_string x) is not valid because x may not fit within an integer. | |||
| 2018-09-04 | Improve error messages for include and ifdef statements | Alasdair Armstrong | |
| 2018-09-04 | Add a rewrite to minimise the number of functions marked as recursive | Brian Campbell | |
| Particularly useful when execute has been split up (e.g., on RISC-V). Only enabled on Coq for now. | |||
| 2018-09-04 | Coq: fix early returns with rich types | Brian Campbell | |
| 2018-09-03 | Coq: solver should split earlier | Brian Campbell | |
| otherwise some other parts don't work properly. Also update RISC-V patch. | |||
| 2018-09-03 | Coq: get top-level value definitions to work nicely again | Brian Campbell | |
| Also required some solver fixes: - make sure that ArithFacts are always cleared to avoid loops - extract_properties should do the goal first because it might add extra work to do in the hypotheses - unfolding should come before extract_properties | |||
| 2018-09-03 | Coq: update RISC-V patch again | Brian Campbell | |
| 2018-09-03 | Coq: rework generation of dependent pairs so that they are only | Brian Campbell | |
| constructed when a function call, cast, or binder demands them, removing some ambiguous corner cases. Also - Don't simplify nexps before printing (note that we usually end up needing a (8 * x) / 8 lemma as a result) - More extraction of properties in the goal - Splitting of conditionals/matches in goals (which can occur more often because of the new positions of build_ex in definitions) - Try simple solving first to improve speed / reduce proof sizes / help fill in metavariables (because manipulating the goal can interfere with instantiating them) - Update RISC-V patch | |||
| 2018-08-31 | Some C stubs for platform bits for RISC-V. | Prashanth Mundkur | |
| 2018-08-31 | rewrite_defs_pat_string_append: only guard the innermost recursive pattern, ↵ | Jon French | |
| and use the original ids rather than fresh ones; both to allow referring to matched ids in guards | |||
| 2018-08-31 | mappings: Support for unidirectional mapping clauses | Jon French | |
| 2018-08-31 | riscv prelude: yet more manual monomorphisations for hex_bits | Jon French | |
| 2018-08-31 | fix some compiler warnings | Jon French | |
| 2018-08-31 | sync and centralise the two .merlin files | Jon French | |
| 2018-08-30 | Annotate the RISC-V prelude for C builtins. | Prashanth Mundkur | |
| Add some builtins to the C sail lib. Enable some gcc warnings. | |||
| 2018-08-30 | C: Fix a bug where function argument type becomes more specific due to flow ↵ | Alasdair Armstrong | |
| typing Added a regression test as c/test/downcast_fn.sail | |||
| 2018-08-30 | Add a C header containing declarations needed by RISC-V. | Prashanth Mundkur | |
| 2018-08-30 | Allow additional includes to be specified for C backend. | Prashanth Mundkur | |
| 2018-08-30 | Coq: correct endianness reversal bug | Brian Campbell | |
| 2018-08-30 | C: Fix an issue with struct field being generalised inside polymorphic ↵ | Alasdair Armstrong | |
| constructors Add a new printing function for debugging that recursively prints constructor types. Fix an interpreter bug when pattern matching on constructors with tuple types. | |||
| 2018-08-29 | C: Fix some issues with tuples as arguments to polymorphic constructors | Alasdair Armstrong | |
| Now all we need to do is make sure the RISC-V builtins are mapped to the correct C functions, and RISC-V in C should work (hopefully). We're still missing some of the functions in sail.c for the mappings so those have to be implemented. | |||
| 2018-08-29 | Updated snapshots for Isabelle 2018 | Thomas Bauereiss | |
| 2018-08-28 | Coq: make some library definitions compute | Brian Campbell | |
| 2018-08-28 | Coq snapshot: make some library definitions compute | Brian Campbell | |
| 2018-08-28 | Basic Makefile support for Coq generation from CHERI | Brian Campbell | |
| 2018-08-28 | fix some compiler not-matched warnings about Typ_bidir and Typ_internal_unknown | Jon French | |
| 2018-08-28 | add __POS__ argument to Err_unreachable for better error reporting | Jon French | |
| 2018-08-28 | Adapt theory imports for Isabelle 2018 | Thomas Bauereiss | |
| Requires a recent Lem version that supports generating session-qualified imports, e.g. revision rems-project/lem@d92b077f1781765a65082c815ff363ef79499860 | |||
| 2018-08-28 | fix bug in RISCV assembly mapping, incorrect order of FENCE pred/succ bits | Jon French | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |