Discovering Affine Equalities Using Random Interpretation
We present a new polynomial-time randomized algorithm for discovering
affine equalities involving variables in a program. The key idea of
the algorithm is to execute a code fragment on a few random inputs,
but in such a way that all paths are covered on each run. This makes
it possible to rule out invalid relationships even with very few runs.
The algorithm is based on two main techniques. First, both branches of a
conditional are executed on each run and at joint points we perform an
affine combination of the joining states. Secondly, in the branches of
an equality conditional we adjust the data values on the fly to
reflect the truth value of the guarding boolean expression. This
increases the number of affine equalities that the analysis discovers.
The algorithm is simpler to implement than alternative deterministic
versions, has better computational complexity, and has an extremely
small probability of error for even a small number of runs. This
algorithm is an example of how randomization can provide a trade-off
between the cost and complexity of program analysis, and a small
probability of unsoundness.