summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2019-08-02Fix up some edge cases with the bitvector/polyvector splitBrian 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-01Merge branch 'sail2' into separate_bvAlasdair Armstrong
2019-08-01Merge remote-tracking branch 'origin/rv_duopod_fix' into sail2Alasdair Armstrong
Fixes #53
2019-07-31Coq: reasoning for until loopsBrian 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-31Revert "Need to separate out the 0.10 lem library from upcoming 0.11"Alasdair Armstrong
This reverts commit 3fb4cf236c0d4b15831576faa45c763853632568.
2019-07-31Merge branch 'sail2' into union_barrierAlasdair Armstrong
2019-07-31Updates to function unfolding to support scattered definitionsAlasdair Armstrong
2019-07-29Add type check after descattering to keep type environments up to dateBrian Campbell
2019-07-18Need to separate out the 0.10 lem library from upcoming 0.11Alasdair 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-18Add a option to check for a feature symbolAlasdair Armstrong
2019-07-18Add a feature flag for barrier type changeAlasdair Armstrong
Fix SMT mem_builtin test case
2019-07-18Support DMB/DSB domainsShaked Flur
2019-07-16Fix all remaining tests for this branchAlasdair
2019-07-16Get monomorphisation tests working with separate bitvectorsAlasdair Armstrong
2019-07-16Merge remote-tracking branch 'origin/sail2' into separate_bvAlasdair Armstrong
2019-07-11Make sure we do constant-fold primitives howeverAlasdair 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-11Make 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-03Consider references in topological sortingThomas Bauereiss
2019-06-30Fix bug with toplevel pattern in RISC-V duopodAlasdair
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-28Monomorphisation: add some alternative names for ones and zero_extend as ↵Robert Norton
used in risc-v spec.
2019-06-28ToFromInterp backend: always wrap typ arg values in a function, fixes option ↵Jon French
types in riscv
2019-06-28Add a warning for potentially unsafe castsAlasdair
2019-06-27SMT: Add a reverse endianness function and fix some bugsAlasdair Armstrong
2019-06-26Fix: Make sure to consider NC_app when checking constraints are identicalAlasdair Armstrong
2019-06-26Make sure we take constraint synonyms into account when checking if types ↵Alasdair Armstrong
are identical
2019-06-25SMT: Add another case to appendAlasdair Armstrong
2019-06-21Coq: add missing property derivation casts for effectful expressionsBrian Campbell
These don't appear much, but are now showing up in the sail-arm model due to an innocent change elsewhere.
2019-06-21Coq: be more careful when dealing with wildcard argument patternsBrian 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-20Coq: avoid more unnecessary uses of pattern bindersBrian Campbell
2019-06-20Coq: handle wildcard binders of bools properlyBrian Campbell
2019-06-20Add additional case to append for Sail -> SMTAlasdair Armstrong
2019-06-20Add more cases to signed for Sail SMTAlasdair Armstrong
2019-06-20Handle more uses of mutable variables during monomorphisation cast insertionBrian Campbell
In particular, bitvector subrange updates work with this version.
2019-06-19Make 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-19Make 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-19Fix buggy ocaml implementation of count_leading_zeros and also make tail ↵Robert Norton
recursive.
2019-06-19Rewriting improvements for monomorphic aarch64_smallBrian 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-19Monomorphisation improvements for aarch64_smallBrian 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-18Fix handling of E_internal_plet in rewriteThomas Bauereiss
2019-06-18Implement count_leading_zeros in LemThomas Bauereiss
2019-06-17Implement 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-13Fix some bugs in Lem rewriterThomas 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-13Add new option to splice in alternative function definitionsBrian Campbell
In particular, this is useful for replacing basic bitvector functions with monomorphisation-friendly ones.
2019-06-13Add AST for greater-than and less-than constraintsBrian 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-12Handle partial matches in guarded pattern rewriteThomas 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-12SMT: Fix missing case for append builtinAlasdair Armstrong
2019-06-11Coq: improve readability of types filesBrian Campbell
Also get rid of the notation warnings for single element records.
2019-06-10Add 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-08Workaround for OCaml bytecode memory bugBrian Campbell
See <https://github.com/ocaml/ocaml/issues/8699#issuecomment-499108873>, tested on 4.07.1 and 4.08+rc2.
2019-06-06SMT: Rename some functions to make usage clearerAlasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 13:54:41 +0000