Summary:
Add a path condition to each symbolic state, represented in sledge's arithmetic domain. This gives a precise account of arithmetic constraints. In particular, it is relation and thus is more robust in the face of inter-procedural analysis.
This is gated behind a flag for now as there are performance issues with the new arithmetic.
Reviewed By: jberdine
Differential Revision: D20393947
fbshipit-source-id: b780de22a
Summary:
Show that the SSA restrictions imply that the blocks can be
topologically sorted so that any use of a variable follows its
definition in the list of blocks. This showed a slight flaw in my
definition of SSA form. It used to treat program counters up to
equality. However, PCs that point to a block header contain the location
that control came from (so that the Phi instructions can be executed),
but the SSA restrictions shouldn't pay attention to that, so now the
definition of SSA introduces a equivalence on PCs that ignores that
additional information.
Reviewed By: jberdine
Differential Revision: D21066873
fbshipit-source-id: 735575a1f
Summary:
Introduce an explicit assumption that all of the instructions are ones
that are implemented in the translation so far, rather than just
cheating proof cases.
Reviewed By: jberdine
Differential Revision: D20891352
fbshipit-source-id: 37598bd8f
Summary:
Separate into separate files the theorems that are just about the
translation (mostly about the structure of the variable->expression
mapping that the translation builds) from theorems about the translation
and the semantics.
Also move the stuff about dominator_ordered into the SSA Theory, since
it only makes sense for SSA programs, but doesn't have anything to do
with the translation.
Reviewed By: jberdine
Differential Revision: D20673124
fbshipit-source-id: 9d8b08164
Summary:
The LLVM->LLAIR translation keeps a mapping of variables to expressions.
Previously, the invariants related to that mapping were kept in the
state relation, and so the proof needed show that they were preserved
along execution traces. This wasn't obvious as the state changes in
non-SSA ways during evaluation, but the correctness of the mappings is
heavily based on the program being in SSA form. This change separates
out the invariants, and the proof uses the final mapping that the
compiler builds, which contains all of the relevant bindings that might
be needed during execution.
Reviewed By: jberdine
Differential Revision: D20625109
fbshipit-source-id: d4c2dfe19
Summary:
Treat the remainder of dividing a rational by an integer as if the
rational was an integer division.
Reviewed By: jvillard
Differential Revision: D21042515
fbshipit-source-id: b5d42ddec
Summary:
The partial treatment of Mul and Div terms can simplify some cases,
but since it is only a partial treatment that is not producing a
normal form, in other cases the "simplification" results in large and
non-canonical terms. It is safer to leave them uninterpreted.
Reviewed By: jvillard
Differential Revision: D21042521
fbshipit-source-id: 04fc37f1a
Summary:
The heights of And and Or terms can grow high. This interacts poorly
with some unoptimized Equality operations such as normalization that
do some processing at every subterm.
Reviewed By: jvillard
Differential Revision: D21042518
fbshipit-source-id: 55e6acbb1
Summary:
These are map and folding map that perform a cycle-preserving
pre-order transformation.
Reviewed By: jvillard
Differential Revision: D20877974
fbshipit-source-id: 251288228
Summary:
The current notion of "simplified" function symbols, which are treated
as a hybrid between interpreted and uninterpreted, has no logical
basis. Normalization is now strong enough, due to stronger handling of
the changing carrier set, that the "simplified" classification can be
removed.
Reviewed By: jvillard
Differential Revision: D20726961
fbshipit-source-id: 9962ea323
Summary:
It is possible for the canonical form of a term in (the carrier set
of) a relation to be a term that is not in the relation. It is also
possible for this term to be equal to a term in the relation. It is
the job of the lookup subroutine of normalization to find these
equations.
The current implementation of entails_eq is incomplete in this case,
in particular, when an uninterpreted term has an interpreted subterm,
which itself has a subterm that is not a representative.
This diff strengthens normalization (and hence it's callers such as
entails_eq) to handle such cases. This makes lookup work slightly
harder. An alternative would be to extend the carrier with new terms
from normalization to the carrier and closing the relation, and then
re-normalizing. That would lead to much inflated representation sizes,
and is inefficient.
Reviewed By: jvillard
Differential Revision: D20612565
fbshipit-source-id: 3b7534a62
Summary:
This diff adds enough interpretation of Mul and Div terms to be able
to exclude them from the domain of solution substitutions. While
non-linear arithmetic is still treated very incompletely, this change
increases the propagation power of the equality constraints that are
deduced. Mainly, this appears to be enough to avoid operations that
are semantically equivalence-preserving such as solve_for_vars from
producing equalities that are unprovable from their inputs.
Reviewed By: jvillard
Differential Revision: D20863528
fbshipit-source-id: fca74cba3
Summary:
For non-linear polynomial equations, the solver can currently choose
to solve for a variable that occurs in a non-linear subterm, leading
to a non-idepotent solution substitution. For example, `x - y + (x ×
z) = 0` could be solved for `x`, leading to `x ↦ y - (x × z)` where
`x` is solved in terms of itself. This diff refines Term.solve_zero_eq
to avoid such cyclic solutions.
Reviewed By: jvillard
Differential Revision: D20637482
fbshipit-source-id: 6d7df85c3
Summary:
Strengthen the canonizer for division and rational constant terms. It
is important to avoid constructing `Q.t` values with 0 denominators,
as they do not represent real numbers, and the algebraic manipulation
done by the rest of the solver is incorrect in that case.
Additionally strengthen the Term representation invariants to check
that all coefficients and exponents are valid real rational numbers.
Also normalize division by an integer or rational to multiplication by
a rational.
Reviewed By: jvillard
Differential Revision: D20663964
fbshipit-source-id: 210962fe0
Summary:
Equations of the form `a = b` where `a` is a proper subterm of `b` are
possible when uninterpreted functions are involved. Internally,
Equality does not eagerly substitute `b` for `a`, but external clients
can repeatedly `Equality.normalize` terms and thereby incrementally
blow up the sizes of terms.
This diff uses the heights of uninterpreted terms to choose equality
class representatives to avoid such blow-ups, by orienting equations
so that tall terms are represented by short terms, so that repeated
normalization cannot increase term height indefinitely.
Reviewed By: jvillard
Differential Revision: D20785632
fbshipit-source-id: ff4c5bacd
Summary:
The types are constants and need not be re-checked for equality during
normalization, etc.
Reviewed By: jvillard
Differential Revision: D20863526
fbshipit-source-id: 1adde5ee0
Summary:
Ensure all entry points check the representation invariant before
returning, and strengthen it to check the constraints on preference
between representative terms, and to check that the relation is
closed.
Reviewed By: jvillard
Differential Revision: D20612566
fbshipit-source-id: b345397c4
Summary:
Change the implementation of `Equality.Subst.compose` to preserve
physical equality if the result is `Subst.equal` to the first
argument.
Reviewed By: jvillard
Differential Revision: D20752671
fbshipit-source-id: 4641a298a
Summary:
Currently there is an implicit assumption in Sh.simplify that
variables do not occur free in an equality relation which makes no
constraint on their values. This diff adds a step to formula
simplification that explicitly removes eliminated existentials from
equality relations.
Reviewed By: jvillard
Differential Revision: D20726960
fbshipit-source-id: 7109aa479
Summary:
Fix the crash in
```
(And_eq () (Var (id 10) (name v))
(Mul (((Var (id 8) (name v)) 1) ((Var (id 9) (name v)) 1)))
((xs ()) (sat true) (rep ())))
```
The solver for interpreted functions relies on the solution
substitutions containing mappings from variables to interpreted
applications, and never in the reverse. When solving equations
involving polynomials, this constraint is specifically
established. But for equalities involving only monomials, it could
happen that e.g. `x` was chosen as the representative of `a × b`,
which violates this constraint.
Reviewed By: jvillard
Differential Revision: D20596422
fbshipit-source-id: 69b026f03
Summary: Term.compare already ignores Var names, make Term.equal do so as well.
Reviewed By: jvillard
Differential Revision: D20663961
fbshipit-source-id: 59e7aa880
Summary:
Generate output on stderr containing lines such as:
```
solve_for_vars time: 0.105 ms 0.871 ms 79 calls
```
which indicates that the current maximal time of a single
`solve_for_vars` query is `0.105 ms` and so far the total time spent in
`solve_for_vars` over `79` queries is `0.871 ms`.
At program exit, there is also a line for each timer indicating the
max query time and final accumulated duration and number of queries:
```
solve_for_vars time: 0.173 ms 17.242 ms 1108 calls
```
Additionally, replay sexp are dumped interactively. A query exceeding
1 sec is dumped, then one exceeding 2 sec, then 4 sec, etc.
Reviewed By: jvillard
Differential Revision: D20852160
fbshipit-source-id: 0a316891e
Summary:
Rename and clarify documentation to indicate that the stronger
specification wrt physical equality is due to requiring the mapped
function to be an endofunction.
Reviewed By: jvillard
Differential Revision: D20863524
fbshipit-source-id: 74dabeb5c
Summary:
Otherwise there is an alias `'a t` for `'a option` polluting the
global namespace, which causes e.g. merlin to produce confusing types.
Reviewed By: jvillard
Differential Revision: D20831349
fbshipit-source-id: dff7b4f15
Josh Berdine
Scott Owens
Jules Villard