| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-09-19 | Coq: more fixes for AArch64 | Brian Campbell | |
| - implement set_slice and set_slice_int - lemmas for more constraints - make real sqrt visible - unfolding list membership needs andb and orb to be handled first | |||
| 2018-09-19 | rewrite_defs_pat_string_append: fix bug with guarded Some | Jon French | |
| 2018-09-19 | separate decimal_string_of_bits from string_of_bits | Jon French | |
| 2018-09-19 | src/gen_lib/sail2_string.lem: more Lem monomorphisations for ↵ | Jon French | |
| hex_bits_N_matches_prefix | |||
| 2018-09-18 | Fix issues with tuple Constructors taking multiple arguments | Alasdair Armstrong | |
| This really demonstrates why we should switch to Typ_fn being a typ list * typ constructor because the implementation here feels *really* hacky with dummy Typ_tup constructors being used to enforce single arguments for constructors. | |||
| 2018-09-18 | Add string mapping functions to interpreter | Alasdair Armstrong | |
| 2018-09-17 | Add diffs to sail files for Aarch64 Coq generation | Brian Campbell | |
| 2018-09-17 | Coq: fix types in aarch64_extras undefined_vector and casts for arguments | Brian Campbell | |
| 2018-09-17 | Coq: solve some constraint/type errors with AArch64 | Brian Campbell | |
| - hints for dotp - handle exists separately when trying eauto to keep search depth low - more uniform existential handling (i.e., we now handle all existentials in the way we used to only handle existentials around atoms) | |||
| 2018-09-17 | Coq: remove an obsolete specialisation | Brian Campbell | |
| Broke E_internal_plet on some simple existential types | |||
| 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 | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |