| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-09-17 | Coq: make generic_neq work on real | Brian Campbell | |
| 2018-09-17 | Rewrites.rewrite_defs_mapping_patterns: emit an explicit type annotation on ↵ | Jon French | |
| the generated pattern so re-typechecking works | |||
| 2018-09-14 | Sail_lib.string_of_bits: print in decimal (properly, with bigints) rather ↵ | Jon French | |
| than binary | |||
| 2018-09-14 | (oops, should have been with "more hex_bits_N monomorphs") | Jon French | |
| 2018-09-14 | Sail_lib.int_of_string_opt: use Big_int.of_string rather than OCaml ↵ | Jon French | |
| int_of_string This fixes e.g. problems with 64-bit bitmask immediates in ARM assembly. | |||
| 2018-09-14 | More monomorphisations for hex_bits_N... | Jon French | |
| I got bored of this so I wrote a Python script to generate all of them between 1 and 33, plus 48 and 64. It's in a comment. We should really get around to making the typechecker work with polymorphic mappings... | |||
| 2018-09-14 | RISCV prelude: fix typo in ocaml extern for negate_* | Jon French | |
| 2018-09-14 | Sail_lib and RISCV prelude: functions for bitwise operations on ints | Jon French | |
| 2018-09-14 | Type_check: allow mappings to contain escape effects | Jon French | |
| 2018-09-13 | C: Fix an issue with assigning to unitialized variables at end of blocks | Alasdair Armstrong | |
| Assigning to an uninitialized variable as the last statement in a block is almost certainly a type, and if that occurs then the lift_assign re-write will introduce empty blocks causing this error to occur. Now when we see such an empty block when converting to A-normal form we turn it into unit, and emit a warning stating that an empty block has been found as well as the probable cause (uninitialized variable). | |||
| 2018-09-13 | Coq: real built-ins for AArch64 | Brian Campbell | |
| 2018-09-12 | Jenkins: Fix deprecation warnings | Alasdair Armstrong | |
| Now that Jenkins is updated to a newer version of OCaml we can finally fix some warning with more recent versions of OCaml than 4.02.3. Also fix a Lem test case that was failing. | |||
| 2018-09-12 | Coq: update RISC-V patch | Brian Campbell | |
| 2018-09-12 | Coq: fix type annotations for early return | Brian Campbell | |
| 2018-09-12 | Coq: make generic_eq work on more types | Brian Campbell | |
| 2018-09-12 | Coq: avoid some use of pattern binders to help Coq's type checker | Brian Campbell | |
| 2018-09-12 | Coq: print more type information for existentially typed vectors | Brian Campbell | |
| 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 | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |