summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2019-05-28Make sure single clause functions with top-level guards work correctlyAlasdair Armstrong
2019-05-24Add a :thin_slice command to isail to isolate a given set of functionsBrian Campbell
2019-05-24Coq: support if-then-throw typechecking special caseBrian Campbell
2019-05-24Coq: switch to computable versions of BBV shiftsBrian Campbell
2019-05-23Coq: support loops which update richly typed variablesBrian Campbell
2019-05-23Coq: solve some division constraintsBrian Campbell
2019-05-23Coq: define the names from the Sail real libraryBrian Campbell
2019-05-23Fix bug in slice_maskThomas Bauereiss
2019-05-22Coq: tweak disjunctions tactic with subst to support more constraintsBrian Campbell
2019-05-22Coq: replace inferrable integer arguments with _ at more typesBrian Campbell
Previously we only checked at atom, now use destruct_atom_nexp to pick up implicit too.
2019-05-22Use opam instructions in INSTALL.mdAlasdair Armstrong
Move the instructions to build everything from source to the wiki
2019-05-22Fix: Update INSTALL.md with opam switch instructionsAlasdair Armstrong
2019-05-22Move Util.warn to Reporting, and make it take the location as a parameterAlasdair Armstrong
Also add a $suppress_warnings directive that ensures that no warnings are generated for a specific file.
2019-05-21SMT: Use a separate constructor for memory read variablesAlasdair Armstrong
We want to ensure simplication can treat these separately so we don't accidentally simplify away dependencies between reads and write addresses.
2019-05-21Fix: undefined_nat test for interpreterAlasdair Armstrong
2019-05-21SMT: Add control flow node numbers to memory events to track program orderAlasdair Armstrong
Add path conditions to memory events Allow simplication of generated SMT based on constructor kinds
2019-05-21Lem: Fix bug in generation of val-specsThomas Bauereiss
Used to output duplicate type variables in some cases.
2019-05-21Coq: remove premature unfolding of local definitionsBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 14:50:16 +0000