| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-10-25 | Coq: clean up some formatting | Brian Campbell | |
| 2019-10-25 | Allow interactive commands to be setup outside isail.ml | Alasdair Armstrong | |
| can use Interactive.register_command to set up a new interactive command, which allows commands to be set up near where the functionality they interact with is defined, e.g. the ast slicing commands are registered in Slice.ml. Also allows help messages to be generated in a consistent way. | |||
| 2019-10-24 | Coq: use `abstract` to separate out proofs from definitions | Brian Campbell | |
| - requires fixpoint definitions containing proofs to be processed in proof mode (due to a bug in Coq), so change libraries and pretty printing to do that - adjust some lemmas to avoid extra evars | |||
| 2019-10-17 | Allow generating C that doesn't hard code any libraries | Alasdair Armstrong | |
| 2019-10-16 | Make nostd Sail arena allocator thread safe (maybe) | Alasdair | |
| 2019-10-15 | More work on bare-metal Sail | Alasdair Armstrong | |
| 2019-10-14 | Add -Ofixed_int and -Ofixed_bits to assume fixed-precision ints and ↵ | Alasdair Armstrong | |
| bitvectors in C Assumes a Sail C library that has functions with the right types to support this. Currently lib/int128 supports the -Ofixed_int option, which was previously -Oint128. Add a version of Sail C library that can be built with -nostdlib and -ffreestanding, assuming the above options. Currently just a header file without any implementation, but with the right types | |||
| 2019-10-02 | Coq: generate decidable equality instances for variant types | Brian Campbell | |
| It only produces them when necessary (because some types do not have decidable equality due to embedded proofs). Also add trivial instance for the unit type. | |||
| 2019-10-02 | Coq: limited support for existentially-typed tuples | Brian Campbell | |
| - in particular at monadic interfaces (i.e., sufficient for instruction ast types) - see commented out part of test/coq/pass/ast_with_dep_tuple.sail for an example that's not currently supported - generate definitions for type-level Bool definitions (i.e., predicates) | |||
| 2019-09-12 | Remove unnecessary copies of non-existant files in ocaml backend. | Robert Norton | |
| 2019-08-22 | additional option to tweak Coq output to support user-defined monad: | pes20 | |
| -coq_alt_modules2 <filename> provide additional alternative modules to open only in main (non-_types) Coq output, and suppress default definitions of MR and M monads | |||
| 2019-08-20 | add -coq_alt_modules option to override the default imported modules | pes20 | |
| 2019-08-20 | add -coq_alt_modules option to override the default imported modules | pes20 | |
| 2019-08-20 | add -coq_alt_modules option to override the default imported modules | pes20 | |
| 2019-08-14 | Add a mono rewrite for (ones(n) @ zeros(m)) | Thomas Bauereiss | |
| 2019-08-14 | Inline reg_deref in Lem output | Thomas Bauereiss | |
| 2019-08-14 | Use bitvector type in mono rewrites | Thomas Bauereiss | |
| Also don't require a previously declared default vector indexing order in vector_dec.sail. | |||
| 2019-08-13 | Coq: fix non-exhaustive pattern match failure in riscv duopod | Brian Campbell | |
| 2019-08-08 | Fix machine words again | Alasdair Armstrong | |
| 2019-08-08 | Update machine words | Alasdair Armstrong | |
| 2019-08-08 | Fix bitvectorToFromInterp | Alasdair Armstrong | |
| 2019-08-08 | Use bitToFromInterp in bitvectorToFromInterp | Alasdair Armstrong | |
| 2019-08-08 | Add same to bitlist representation | Alasdair Armstrong | |
| 2019-08-08 | Add bitvectorToFromInterp | Alasdair Armstrong | |
| 2019-08-05 | Print effect sets in alphabetical order | Alasdair Armstrong | |
| 2019-08-05 | Remove escape/pure effect restriction for mapping | Alasdair Armstrong | |
| 2019-08-02 | Fix all warnings (except for two lem warnings) | Alasdair Armstrong | |
| Remove P_record as it's never been implemented in parser/typechecker/rewriter, and is not likely to be. This also means we can get rid of some ugliness with the fpat and mfpat types. Stubs for P_or and P_not are left as they still may get added to ASL and we might want to support them, although there are good reasons to keep our patterns simple. The lem warning for while -> while0 for ocaml doesn't matter because it's only used in lem, and the 32-bit number warning is just noise. | |||
| 2019-08-02 | Fix up some edge cases with the bitvector/polyvector split | Brian Campbell | |
| Mostly in the Coq backend, plus a few testcases that use bitvector builtins on poly-vectors (which works on some backends, but not Coq). Also handle some additional list inclusion proofs in Coq. | |||
| 2019-08-01 | Merge branch 'sail2' into separate_bv | Alasdair Armstrong | |
| 2019-08-01 | Merge remote-tracking branch 'origin/rv_duopod_fix' into sail2 | Alasdair Armstrong | |
| Fixes #53 | |||
| 2019-07-31 | Coq: reasoning for until loops | Brian Campbell | |
| Loops measures are now abstracted over the variables so that they can be used in proofs. Add total Hoare logic rules for until. | |||
| 2019-07-31 | Revert "Need to separate out the 0.10 lem library from upcoming 0.11" | Alasdair Armstrong | |
| This reverts commit 3fb4cf236c0d4b15831576faa45c763853632568. | |||
| 2019-07-31 | Merge branch 'sail2' into union_barrier | Alasdair Armstrong | |
| 2019-07-31 | Updates to function unfolding to support scattered definitions | Alasdair Armstrong | |
| 2019-07-29 | Add type check after descattering to keep type environments up to date | Brian Campbell | |
| 2019-07-18 | Need to separate out the 0.10 lem library from upcoming 0.11 | Alasdair Armstrong | |
| Unlike the prompt-monad change I don't see a way to do this easily purely on the model side Make sure a64_barrier_type and domain aren't visible for RISC-V isabelle build | |||
| 2019-07-18 | Add a option to check for a feature symbol | Alasdair Armstrong | |
| 2019-07-18 | Add a feature flag for barrier type change | Alasdair Armstrong | |
| Fix SMT mem_builtin test case | |||
| 2019-07-18 | Support DMB/DSB domains | Shaked Flur | |
| 2019-07-16 | Fix all remaining tests for this branch | Alasdair | |
| 2019-07-16 | Get monomorphisation tests working with separate bitvectors | Alasdair Armstrong | |
| 2019-07-16 | Merge remote-tracking branch 'origin/sail2' into separate_bv | Alasdair Armstrong | |
| 2019-07-11 | Make sure we do constant-fold primitives however | Alasdair Armstrong | |
| Previous change would stop all things defined externally from being folded, which was overly strict. We do want to allow folding for shared primitives, and can use the set of safe_primops in the interpreter for this. | |||
| 2019-07-11 | Make sure constant folding won't fold external definitions that also have ↵ | Alasdair Armstrong | |
| sail definitions Definitions can be made external on a per-backend basis, so we need to make sure constant folding doesn't inline external functions that have sail definitions for backends other than the ones we are currently targetting | |||
| 2019-07-03 | Consider references in topological sorting | Thomas Bauereiss | |
| 2019-06-30 | Fix bug with toplevel pattern in RISC-V duopod | Alasdair | |
| Do this by making sure that generic pattern literal re-writing gets applied to top-level function clauses. This requires re-ordering the rewrites for most backends otherwise they break, which hopefully wo anything. After doing this re-ordering I had to turn off casting when rewriting bitvector patterns, otherwise insane things can happen. | |||
| 2019-06-28 | Monomorphisation: add some alternative names for ones and zero_extend as ↵ | Robert Norton | |
| used in risc-v spec. | |||
| 2019-06-28 | ToFromInterp backend: always wrap typ arg values in a function, fixes option ↵ | Jon French | |
| types in riscv | |||
| 2019-06-28 | Add a warning for potentially unsafe casts | Alasdair | |
| 2019-06-27 | SMT: Add a reverse endianness function and fix some bugs | Alasdair Armstrong | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |