summaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Collapse)Author
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
2019-05-13Parse dereferences in orderinary expressionsAlasdair
2019-05-13fix typo in excl_res externJon French
2019-05-10SMT: Experiment with symbolic memory reads and writesAlasdair Armstrong
2019-05-09SMT: Make path conditionals more preciseAlasdair Armstrong
Previously path conditionals for a node were defined as the path conditional of the immediate dominator (+ a guard for explicit guard nodes after conditional branches), whereas now they are the path conditional of the immediate dominator plus an expression encapsulating all the guards between the immediate dominator and the node. This is needed as the previous method was incorrect for certain control flow graphs. This slows down the generated SMT massively, because it causes the path conditionals to become huge when the immediate dominator is far away from the node in question. It also changes computing path conditionals from O(n) to O(n^2) which is not ideal as our inlined graphs can become massive. Need to figure out a better way to generate minimal path conditionals between the immediate dominator and the node. I upped the timeout for the SMT tests from 20s to 300s each but this may still cause a failure in Jenkins because that machine is slow.
2019-05-08Remove generated TeX fileThomas Bauereiss
2019-05-07Merge branch 'sail2' into smt_experimentsAlasdair Armstrong
2019-05-07Patch up a couple of Isabelle proofs due to memory interface changesBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 19:08:22 +0000