summaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Collapse)Author
2019-07-31Merge branch 'sail2' into union_barrierAlasdair Armstrong
2019-07-31Remove redundant ifdef and run SMT tests by defaultAlasdair Armstrong
2019-07-31Change platform_barrier so it doesn't care about it's argument typeAlasdair Armstrong
2019-07-29Coq: add state monad version of while/until loops and lifting resultsBrian Campbell
2019-07-25Update Coq barrier definitionBrian Campbell
2019-07-25Basic port of proof machinery to CoqBrian 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 feature flag for barrier type changeAlasdair Armstrong
Fix SMT mem_builtin test case
2019-07-18Update aarch64_small to build with new barriersAlasdair Armstrong
Make sure barrier changes don't affect other models for now
2019-07-18Support DMB/DSB domainsShaked Flur
2019-07-15Add a fast path to speed up platform_read_ram: use fast_read_ram if read is ↵Robert Norton
8 bytes or less to avoid cost of using GMP integers (including free/malloc).
2019-07-04Add coq builtin for concat_str (copied from mips prelude).Robert Norton
2019-06-27SMT: Add a reverse endianness function and fix some bugsAlasdair Armstrong
2019-06-27Coq: less constrained version of slice for ARM modelBrian Campbell
2019-06-21Coq: even more robust handling of unknown goalsBrian Campbell
2019-06-21Coq: better handling of unknown constraintsBrian Campbell
Move the tactic forward so that preprocessing can't try silly things, simpl to get rid of embedded proofs.
2019-06-20Coq: avoid some unnecessary reduction in the constraint solverBrian Campbell
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-17Add sail implementation of count_leading_zeros. We could use this for ↵Robert Norton
backends where the builtin isn't supported but sail support for this is currently a bit broken (will use sail version when it shouldn't e.g. for smt).
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-13Coq: add eq_bit built-inBrian Campbell
2019-06-12Fix Lem binding for abs_intThomas Bauereiss
2019-06-11Coq: add concatenation operator for polymorphic vectorsBrian Campbell
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-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-05Coq: exploit arithmetic solver for some mixed integer/bool problems.Brian Campbell
2019-06-05Coq: generalize proof terms before main solverBrian Campbell
Ensures that dependencies in proofs don't affect rewriting.
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-03Coq: experiment with another boolean iff solving methodBrian Campbell
2019-05-30Set interpreter builtin for truncateLSB.Robert Norton
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-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-24Coq: switch to computable versions of BBV shiftsBrian 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-21Coq: remove premature unfolding of local definitionsBrian Campbell
2019-05-20Coq: fix property extraction bug, solve some constraints involving setsBrian Campbell
2019-05-19Coq: add signed bitvector to integer function that doesn't need >0 constraintBrian Campbell
2019-05-19Coq: proper definitions for some undefined value functionsBrian Campbell
That is, undefined_bitvector, undefined_unit, internal_pick.
2019-05-17SMT: Finish adding all memory builtins from lib/regfp.sailAlasdair Armstrong
2019-05-15Coq: constraint solving for aarch64Brian Campbell
Also split out main solver tactic to make debugging a little easier.
2019-05-14Various bugfixesAlasdair Armstrong
Since we have __deref to desugar *x in this file (as it's the one file everything includes) we might as well add a __bitfield_deref here too, for the bitfield setters. Make sure undefined_nat can be used in C Both -memo_z3 and -no_memo_z3 were listed as default options, now only -no_memo_z3 is listed as the default.
2019-05-14Merge branch 'smt_experiments' into sail2Alasdair Armstrong
2019-05-14Add feature that allows functions to require type variables are constantAlasdair Armstrong
can now write e.g. forall (constant 'n : Int) rather than forall ('n: Int) which requires 'n to be a constant integer value whenever the function is called. I added this to the 'addrsize variable on memory reads/writes to absolutely guarantee in the SMT generation that we don't have to worry about the address being a variable length bitvector.
2019-05-13Merge branch 'sail2' into smt_experimentsAlasdair
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-13 21:35:23 +0000