| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
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
|
|
Make sure barrier changes don't affect other models for now
|
|
|
|
8 bytes or less to avoid cost of using GMP integers (including free/malloc).
|
|
|
|
|
|
|
|
|
|
Move the tactic forward so that preprocessing can't try silly things,
simpl to get rid of embedded proofs.
|
|
|
|
- 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 (!)
|
|
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).
|
|
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.
|
|
|
|
|
|
|
|
Solves some ARM model constraints much more quickly
|
|
|
|
Also rename them for uniformity with other backends.
|
|
|
|
|
|
Ensures that dependencies in proofs don't affect rewriting.
|
|
- make the exists, iff solver handle more cases
- avoid exposing omega to goals with local definitions involving proofs
|
|
|
|
|
|
- don't clear boolean local definitions - we need those now
- some boolean disjunction fixes
|
|
|
|
- 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)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
That is, undefined_bitvector, undefined_unit, internal_pick.
|
|
|
|
Also split out main solver tactic to make debugging a little easier.
|
|
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.
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
