summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-12Fix Lem binding for abs_intThomas Bauereiss
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: add concatenation operator for polymorphic vectorsBrian Campbell
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-06Fix aarch64_small testAlasdair Armstrong
2019-06-06Coq: more aggressive rewriting before solvingBrian Campbell
Solves some ARM model constraints much more quickly
2019-06-06Coq: tweak bool to Z to use less memoryBrian Campbell
2019-06-06SMT: Rename some functions to make usage clearerAlasdair Armstrong
2019-06-06Fix tdiv_int and tmod_int bindings for LemThomas Bauereiss
Also rename them for uniformity with other backends.
2019-06-06Add arith_shiftr to C and OCaml librariesThomas Bauereiss
2019-06-06SMT: Add function to de-serialise serialised modelAlasdair Armstrong
2019-06-06Fix aarch64_small makefileAlasdair Armstrong
2019-06-06Add an option to pre-compile the axiomatic model for SMTAlasdair Armstrong
2019-06-06Update aarch64_small hgen filesAlasdair Armstrong
2019-06-06update funding acksPeter Sewell
2019-06-05Add some regression testsAlasdair
2019-06-05Coq: exploit arithmetic solver for some mixed integer/bool problems.Brian Campbell
2019-06-05Fix: Make sure we check Jib types match for operators before optimizingAlasdair 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-05Coq: generalize proof terms before main solverBrian Campbell
Ensures that dependencies in proofs don't affect rewriting.
2019-06-05Coq: fix type alias expansion in constraintsBrian Campbell
2019-06-04Make sure aarch64_small can generate Jib for SMTAlasdair Armstrong
Add a test case for this
2019-06-04Remove unused AST constructorAlasdair Armstrong
Clean up ott grammar a bit
2019-06-04Coq: more constraint solvingBrian Campbell
- make the exists, iff solver handle more cases - avoid exposing omega to goals with local definitions involving proofs
2019-06-04Merge pull request #52 from scottj97/update-gitignoreAlasdair Armstrong
Add new files to .gitignore
2019-06-04SMT: Add a fuzzing tool for the SMT builtinsAlasdair Armstrong
2019-06-03Add new files to .gitignoreScott Johnson
2019-06-03Test case for previous commitBrian Campbell
2019-06-03Coq: support non-exhaustive pattern rewrite for exception handlingBrian Campbell
2019-06-03Coq: experiment with another boolean iff solving methodBrian Campbell
2019-05-31Add SMT related things to libsail fileAlasdair Armstrong
2019-05-31Change specialization interface slightlyAlasdair Armstrong
2019-05-30Implement ones builtin in sail_lib and add to interpreter. However currently ↵Robert Norton
this is implemented in lib/vector_dec.sail as sail function that calls not_vec on sail_zeros.
2019-05-30Set interpreter builtin for truncateLSB.Robert Norton
2019-05-29Some minor grammar fixes in internals.mdAlasdair Armstrong
2019-05-29Fix some typosAlasdair Armstrong
2019-05-29Add some Sail internals documentationAlasdair Armstrong
2019-05-29Coq: more solver improvementsBrian Campbell
- don't clear boolean local definitions - we need those now - some boolean disjunction fixes
2019-05-29Coq: need a proof for _shr32Brian Campbell
2019-05-29SMT: Make bitvector equality work between vectors of different lengthsAlasdair Armstrong
2019-05-29SMT: Fix sail_truncate and sail_mask for unusual argument typesAlasdair Armstrong
2019-05-29Fix sail_truncate error message in SMTAlasdair Armstrong
2019-05-28Fix typechecking test expected errorAlasdair Armstrong
2019-05-28Coq: more constraint solvingBrian Campbell
- add division lemma - deal with some awkward \/ constraints from asl_parser - try simple integer comparison proofs before omega (which can blow up on trivial properties in large contexts)
2019-05-28Coq: don't output complex bool types at let expressionsBrian Campbell
2019-05-28Just build lem in aarch64_small testAlasdair Armstrong
2019-05-28SMT: Add min and max functionsAlasdair Armstrong
Allow conversion between int(n) and int in smt_conversion
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 23:00:35 +0000