Discovering affine equalities using random interpretation

ABSTRACT

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.

REFERENCES

• 1: A. Aiken, M. Fähndrich, and Z. Su. Detecting races in relay ladder logic programs. International Journal on Software Tools for Technology Transfer, 3(1):93--105, 2000.
• 2: B. Alpern , M. N. Wegman , F. K. Zadeck, Detecting equality of variables in programs, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-11, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73561]
• 3: M. Blum, A. Chandra, and M. Wegman. Equivalence of free boolean graphs can be decided probabilistically in polynomial time. Information Processing Letters, 10:80--82, 1980.
• 4: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 5: Patrick Cousot , Nicolas Halbwachs, Automatic discovery of linear restraints among variables of a program, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.84-96, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512770]
• 6: Michael D. Ernst , Jake Cockrell , William G. Griswold , David Notkin, Dynamically Discovering Likely Program Invariants to Support Program Evolution, IEEE Transactions on Software Engineering, v.27 n.2, p.99-123, February 2001 [doi>10.1109/32.908957]
• 7: Manuel Fähndrich , Jeffrey S. Foster , Zhendong Su , Alexander Aiken, Partial online cycle elimination in inclusion constraint graphs, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.85-96, June 17-19, 1998, Montreal, Quebec, Canada
• 8: D. Hamlet. Random testing. In J. Marciniak, editor, Encyclopedia of Software Engineering, pages 970--978. Wiley, New York, 1994.
• 9: M. Karr. Affine relationships among variables of a program. In Acta Informatica, pages 133--151. Springer, 1976.
• 10: George C. Necula, Translation validation for an optimizing compiler, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.83-94, June 18-21, 2000, Vancouver, British Columbia, Canada
• 11: Amir Pnueli , Michael Siegel , Eli Singerman, Translation Validation, Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.151-166, March 28-April 04, 1998
• 12: B. K. Rosen , M. N. Wegman , F. K. Zadeck, Global value numbers and redundant computations, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.12-27, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73562]
• 13: J. T. Schwartz, Fast Probabilistic Algorithms for Verification of Polynomial Identities, Journal of the ACM (JACM), v.27 n.4, p.701-717, Oct. 1980 [doi>10.1145/322217.322225]
• 14: M. Wegman, V. C. Sreedhar, and R. Bodik. Probabilistic value numbering. Unpublished manuscript, 2001.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis

General Terms:
Algorithms, Theory, Verification

Keywords:
affine relationships, linear equalities, random interpretation, randomized algorithm