| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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-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-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 | |
| 2019-06-26 | Fix: Make sure to consider NC_app when checking constraints are identical | Alasdair Armstrong | |
| 2019-06-26 | Make sure we take constraint synonyms into account when checking if types ↵ | Alasdair Armstrong | |
| are identical | |||
| 2019-06-25 | SMT: Add another case to append | Alasdair Armstrong | |
| 2019-06-21 | Coq: add missing property derivation casts for effectful expressions | Brian Campbell | |
| These don't appear much, but are now showing up in the sail-arm model due to an innocent change elsewhere. | |||
| 2019-06-21 | Coq: be more careful when dealing with wildcard argument patterns | Brian Campbell | |
| If they're merged with a type variable then we still need to name the argument so that it can be used in other types. | |||
| 2019-06-20 | Coq: avoid more unnecessary uses of pattern binders | Brian Campbell | |
| 2019-06-20 | Coq: handle wildcard binders of bools properly | Brian Campbell | |
| 2019-06-20 | Add additional case to append for Sail -> SMT | Alasdair Armstrong | |
| 2019-06-20 | Add more cases to signed for Sail SMT | Alasdair Armstrong | |
| 2019-06-20 | Handle more uses of mutable variables during monomorphisation cast insertion | Brian Campbell | |
| In particular, bitvector subrange updates work with this version. | |||
| 2019-06-19 | Make C emulator exit with failure for uncaught exception. Make special case ↵ | Robert Norton | |
| for 'exception.sail' test that deliberately exits with uncaught exception. | |||
| 2019-06-19 | Make default ocaml main exit with non-zero exit code in case of uncaught ↵ | Robert Norton | |
| exception. This is ensures test failures are detected. | |||
| 2019-06-19 | Fix buggy ocaml implementation of count_leading_zeros and also make tail ↵ | Robert Norton | |
| recursive. | |||
| 2019-06-19 | Rewriting improvements for monomorphic aarch64_small | Brian Campbell | |
| - allow disjoint_pat to be used on patterns that have just been introduced by the rewrite without rechecking - don't rebuild the matched expression in the generated fallthrough case (or any wildcard fall-through) - it may be dead code and generate badly typed Lem - update the type environment passed to rewrites whenever type checking is performed; stale information broke some rewrites | |||
| 2019-06-19 | Monomorphisation improvements for aarch64_small | Brian Campbell | |
| - additional rewrites (signed extend of subrange@zeros, subrange assignment, variants with casts) - drop # from new top-level type variables (e.g., n_times_8) so that the rewriter knows that they're safe to include in casts - add casts in else-branches when only one possible value for a size is left - add casts when assertions force a size to be a particular value - don't use types to detect set constraints in analysis because we won't know which part of the assertion should be replaced - also use non-top-level type variables when simplifying sizes in analysis (useful when it can from pattern matching on an ast) - cope with repeated int('n) in a pattern match (!) | |||
| 2019-06-18 | Fix handling of E_internal_plet in rewrite | Thomas Bauereiss | |
| 2019-06-18 | Implement count_leading_zeros in Lem | Thomas Bauereiss | |
| 2019-06-17 | Implement a count_leading_zeros builtin for ocaml and c. This may be a ↵ | Robert Norton | |
| slight performance improvement and keeps compatibility with smt backend that already had a builtin for this because it can't handle the loop in the sail version. Will need implementations for prover backends. | |||
| 2019-06-13 | Fix some bugs in Lem rewriter | Thomas Bauereiss | |
| A missing type annotation in rewrite_guarded_clauses caused a crash in some cases. Also fix an effect propagation bug in rewrite_letbind_effects. | |||
| 2019-06-13 | Add new option to splice in alternative function definitions | Brian Campbell | |
| In particular, this is useful for replacing basic bitvector functions with monomorphisation-friendly ones. | |||
| 2019-06-13 | Add AST for greater-than and less-than constraints | Brian Campbell | |
| Mostly to make constraints sent to the SMT solver and Coq nicer, but also makes it easy to remove uninformative constraints in the Coq back-end. | |||
| 2019-06-12 | Handle partial matches in guarded pattern rewrite | Thomas Bauereiss | |
| Add a fallthrough case that fails to potentially partial pattern matches. This also helps to preserve any guard in the final match case, which might be needed for flow typing (see the discussion on issue #51). TODO: Merge with the MakeExhaustive rewrite, which currently does not support guarded patterns. | |||
| 2019-06-12 | SMT: Fix missing case for append builtin | Alasdair Armstrong | |
| 2019-06-11 | Coq: improve readability of types files | Brian Campbell | |
| Also get rid of the notation warnings for single element records. | |||
| 2019-06-10 | Add well-formedness check for type schemes in valspecs. | Brian Campbell | |
| Fixes #47. Also adjust the nexp substitution so that the error message points to a useful location, and replace the empty environment with the initial environment in a few functions that do type checking to ensure that the prover is set up (which may be needed for the wf check). | |||
| 2019-06-08 | Workaround for OCaml bytecode memory bug | Brian Campbell | |
| See <https://github.com/ocaml/ocaml/issues/8699#issuecomment-499108873>, tested on 4.07.1 and 4.08+rc2. | |||
| 2019-06-06 | SMT: Rename some functions to make usage clearer | Alasdair Armstrong | |
| 2019-06-06 | Fix tdiv_int and tmod_int bindings for Lem | Thomas Bauereiss | |
| Also rename them for uniformity with other backends. | |||
| 2019-06-06 | Add arith_shiftr to C and OCaml libraries | Thomas Bauereiss | |
| 2019-06-06 | SMT: Add function to de-serialise serialised model | Alasdair Armstrong | |
| 2019-06-06 | Add an option to pre-compile the axiomatic model for SMT | Alasdair Armstrong | |
| 2019-06-06 | Update aarch64_small hgen files | Alasdair Armstrong | |
| 2019-06-05 | Add some regression tests | Alasdair | |
| 2019-06-05 | Fix: Make sure we check Jib types match for operators before optimizing | Alasdair Armstrong | |
| Insert coercions for AV_cval if neccessary Simplify any n in 2 ^ n, to make sure we can always evaluate 2 ^ n when n is a constant before passing it to the SMT solver. | |||
| 2019-06-05 | Coq: fix type alias expansion in constraints | Brian Campbell | |
| 2019-06-04 | Make sure aarch64_small can generate Jib for SMT | Alasdair Armstrong | |
| Add a test case for this | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |