Program analysis for compiler validation

ABSTRACT

Translation Validation is an approach of ensuring compilation correctness in which each compiler run is followed by a validation pass that proves that the target code produced by the compiler is a correct translation (implementation) of the source code. It has been previously shown that the problem of translation validation can be reduced to checking if a single system - the corss-product of the source and target, satisfies a specific property. In this paper, we show how to adapt the existing program analysis techniques in the setting of translation validation. In addition, we present a novel invariant generation algorithm which strengthens our analysis when the input programs contain dynamically allocated data structures. Finally, we report on the prototype tool that applies the developed methodology to verification of the LLVM compiler. The tool handles many of the classical intraprocedural compiler optimizations such as constant folding, reassociation, common subexpression elimination, code motion, dead code elimination, and others.

REFERENCES

• 1: CVC3: An Automatic Theorem Prover for Satisfiability Modulo Theories (SMT).
• 2: The LLVM Compiler Infrastructure Project. http://llvm.org.
• 3: Mike Barnett , K. Rustan M. Leino, Weakest-precondition of unstructured programs, Proceedings of the 6th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, September 05-06, 2005, Lisbon, Portugal
• 4: Ron Cytron , Jeanne Ferrante , Barry K. Rosen , Mark N. Wegman , F. Kenneth Zadeck, Efficiently computing static single assignment form and the control dependence graph, ACM Transactions on Programming Languages and Systems (TOPLAS), v.13 n.4, p.451-490, Oct. 1991 [doi>10.1145/115372.115320]
• 5: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 6: Sumit Gulwani and Ashish Tiwari. Assertion checking over combined abstraction of linear arithmetic and uninterpreted functions. In The 15th European Symposium on Programming, pages 279--293. Springer, March 2006.
• 7: Chris Lattner , Vikram Adve, LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation, Proceedings of the international symposium on Code generation and optimization: feedback-directed and runtime optimization, p.75, March 20-24, 2004, Palo Alto, California
• 8: Steven S. Muchnick, Advanced compiler design and implementation, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1998
• 9: 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
• 10: 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
• 11: Amir Pnueli. Verification of procedural programs. In We Will Show Them! Essays in Honour of Dov Gabbay, Volume Two, pages 543--590. College Publications, 2005.
• 12: Xavier Rival, Symbolic transfer function-based approaches to certified compilation, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-13, January 14-16, 2004, Venice, Italy
• 13: Saddek Bensalem , Yassine Lakhnech , Hassen Saïdi, Powerful Techniques for the Automatic Generation of Invariants, Proceedings of the 8th International Conference on Computer Aided Verification, p.323-335, August 03, 1996
• 14: Loren Taylor Simpson. Value-Driven Redundancy Elimination. PhD thesis, Rice University, 1996.
• 15: Anna Zaks , Amir Pnueli, CoVaC: Compiler Validation by Program Analysis of the Cross-Product, Proceedings of the 15th international symposium on Formal Methods, May 26-30, 2008, Turku, Finland [doi>10.1007/978-3-540-68237-0_5]
• 16: Lenore Zuck, Amir Pnueli, Yi Fang, and Benjamin Goldberg. VOC: A methodology for the translation validation of optimizing compilers. Journal of Universal Computer Science, 9(3):223--247, 2003.
• 17: Lenore Zuck , Amir Pnueli , Benjamin Goldberg , Clark Barrett , Yi Fang , Ying Hu, Translation and Run-Time Validation of Loop Transformations, Formal Methods in System Design, v.27 n.3, p.335-360, November 2005 [doi>10.1007/s10703-005-3402-z]