A foundation for flow-based program matching: using temporal logic and model checking

ABSTRACT

Reasoning about program control-flow paths is an important functionality of a number of recent program matching languages and associated searching and transformation tools. Temporal logic provides a well-defined means of expressing properties of control-flow paths in programs, and indeed an extension of the temporal logic CTL has been applied to the problem of specifying and verifying the transformations commonly performed by optimizing compilers. Nevertheless, in developing the Coccinelle program transformation tool for performing Linux collateral evolutions in systems code, we have found that existing variants of CTL do not adequately support rules that transform subterms other than the ones matching an entire formula. Being able to transform any of the subterms of a matched term seems essential in the domain targeted by Coccinelle.

In this paper, we propose an extension to CTL named CTLVW (CTL with variables and witnesses) that is a suitable basis for the semantics and implementation of the Coccinelles program matching language. Our extension to CTL includes existential quantification over program fragments, which allows metavariables in the program matching language to range over different values within different control-flow paths, and a notion of witnesses that record such existential bindings for use in the subsequent program transformation process. We formalize CTL-VW and describe its use in the context of Coccinelle. We then assess the performance of the approach in practice, using a transformation rule that fixes several reference count bugs in Linux code.

REFERENCES

• 1: Ki Yung Ahn , Tim Sheard, Shared subtypes: subtyping recursive parametrized algebraic data types, Proceedings of the first ACM SIGPLAN symposium on Haskell, September 25-25, 2008, Victoria, BC, Canada
• 2: James Cheney and Ralf Hinze. First-class phantom types. Technical Report CUCIS TR2003-1901, Cornell University, 2003.
• 3: Dominic Duggan , John Ophel, Type-checking multi-parameter type classes, Journal of Functional Programming, v.12 n.2, p.133-158, March 2002 [doi>10.1017/S0956796801004233]
• 4: Louis-Julien Guillemette , Stefan Monnier, A type-preserving compiler in Haskell, Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, September 20-28, 2008, Victoria, BC, Canada
• 5: Mark P. Jones, Type Classes with Functional Dependencies, Proceedings of the 9th European Symposium on Programming Languages and Systems, p.230-244, April 02, 2000
• 6: Christine Paulin-Mohring, Inductive Definitions in the system Coq - Rules and Properties, Proceedings of the International Conference on Typed Lambda Calculi and Applications, p.328-345, March 16-18, 1993
• 7: Simon Peyton Jones, Mark P. Jones, and Erik Meijer. Type classes: exploring the design space. In Haskell Workshop, Amsterdam, June 1997.
• 8: Simon Peyton Jones , Dimitrios Vytiniotis , Stephanie Weirich , Geoffrey Washburn, Simple unification-based type inference for GADTs, Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming, September 16-21, 2006, Portland, Oregon, USA
• 9: Frank Pfenning , Carsten Schürmann, System Description: Twelf - A Meta-Logical Framework for Deductive Systems, Proceedings of the 16th International Conference on Automated Deduction: Automated Deduction, p.202-206, July 07-10, 1999
• 10: Tom Schrijvers and Martin Sulzmann. Unified Type Checking for Type Classes and Type Functions, 2008. Poster at the International Conference on Functional Programming (ICFP'08).
• 11: Tom Schrijvers , Simon Peyton Jones , Manuel Chakravarty , Martin Sulzmann, Type checking with open type functions, Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, September 20-28, 2008, Victoria, BC, Canada
• 12: Tim Sheard, Languages of the future, Companion to the 19th annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, October 24-28, 2004, Vancouver, BC, CANADA [doi>10.1145/1028664.1028711]
• 13: Matthieu Sozeau , Nicolas Oury, First-Class Type Classes, Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics, August 18-21, 2008, Montreal, P.Q., Canada [doi>10.1007/978-3-540-71067-7_23]
• 14: Peter J. Stuckey , Martin Sulzmann, A theory of overloading, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.6, p.1216-1269, November 2005 [doi>10.1145/1108970.1108974]
• 15: Martin Sulzmann , Manuel M. T. Chakravarty , Simon Peyton Jones , Kevin Donnelly, System F with type equality coercions, Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation, January 16-16, 2007, Nice, Nice, France [doi>10.1145/1190315.1190324]
• 16: Martin Sulzmann , Gregory J. Duck , Simon Peyton-Jones , Peter J. Stuckey, Understanding functional dependencies via constraint handling rules, Journal of Functional Programming, v.17 n.1, p.83-129, January 2007 [doi>10.1017/S0956796806006137]
• 17: P. Wadler , S. Blott, How to make ad-hoc polymorphism less ad hoc, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.60-76, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75283]
• 18: Hongwei Xi , Chiyan Chen , Gang Chen, Guarded recursive datatype constructors, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.224-235, January 15-17, 2003, New Orleans, Louisiana, USA

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Temporal logic

General Terms:
Algorithms, Languages, Theory

Keywords:
bug finding, ctl, model checking, program matching, program transformation