Julien Brunel
Gilles Muller
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.
- Ki Yung Ahn and Tim Sheard. Shared subtypes: subtyping recursive parametrized algebraic data types. In Haskell '08: Proceedings of the 1st ACM SIGPLAN Haskell symposium, pages 75--86, New York, NY, USA, 2008. ACM. Google Scholar
Digital Library
- James Cheney and Ralf Hinze. First-class phantom types. Technical Report CUCIS TR2003-1901, Cornell University, 2003.Google Scholar
- Dominic Duggan and John Ophel. Type-checking multi-parameter type classes. J. Funct. Program., 12 (2): 133--158, 2002. Google ScholarDigital Library
- Louis-Julien Guillemette and Stefan Monnier. A type-preserving compiler in Haskell. In ICFP '08: Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, pages 75--86, New York, NY, USA, 2008. ACM. Google ScholarDigital Library
- Mark P. Jones. Type classes with functional dependencies. In Proc. of ESOP 2000, number 1782 in Lecture Notes in Computer Science. Springer-Verlag, 2000. Google ScholarDigital Library
- Christine Paulin-Mohring. Inductive definitions in the system Coq-rules and properties. In M. Bezem and J. Groote, editors, International conference on Typed Lambda Calculi and Applications. LNCS 664, Springer-Verlag, 1993. Google ScholarDigital Library
- Simon Peyton Jones, Mark P. Jones, and Erik Meijer. Type classes: exploring the design space. In Haskell Workshop, Amsterdam, June 1997.Google Scholar
- Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn. Simple unification-based type inference for gadts. In International Conference on Functional Programming, Portland, Oregon, September 2006. Google ScholarDigital Library
- Frank Pfenning and Carsten Schürmann. System description: Twelf -- a meta-logical framework for deductive systems. In International Conference on Automated Deduction, volume 1632 of Lecture Notes in Artificial Intelligence, pages 202--206, July 1999. Google ScholarDigital Library
- 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).Google Scholar
- Tom Schrijvers, Simon Peyton Jones, Manuel Chakravarty, and Martin Sulzmann. Type checking with open type functions. In ICFP '08: Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, pages 51--62, New York, NY, USA, 2008. ACM. Google ScholarDigital Library
- Tim Sheard. Languages of the future. In OOPSLA '04: Companion to the 19th annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, pages 116--119, New York, NY, USA, 2004. ACM Press. ISBN 1-58113-833-4. Google ScholarDigital Library
- Matthieu Sozeau and Nicolas Oury. First-class type classes. In 21th International Conference on Theorem Proving in Higher Order Logics, pages 278--293. LNCS 5170, Springer-Verlag, 2008. Google ScholarDigital Library
- Peter J. Stuckey and Martin Sulzmann. A theory of overloading. ACM Transactions on Programming Languages and Systems (TOPLAS), 27 (6): 1--54, 2005. Google ScholarDigital Library
- Martin Sulzmann, Manuel Chakravarty, Simon Peyton Jones, and Kevin Donnelly. System F with type equality coercions. In ACM SIGPLAN International Workshop on Types in Language Design and Implementation (TLDI'07). ACM, 2007. Google ScholarDigital Library
- Martin Sulzmann, Gregory J. Duck, Simon Peyton-Jones, and Peter J. Stuckey. Understanding functional dependencies via Constraint Handling Rules. J. Funct. Program., 17 (1): 83--129, 2007. Google ScholarDigital Library
- Philip Wadler and Stephen Blott. How to make ad-hoc polymorphism less ad hoc. In Symposium on Principles of Programming Languages, Austin, TX, January 1989. Google ScholarDigital Library
- Hongwei Xi, Chiyan Chen, and Gang Chen. Guarded recursive datatype constructors. In Symposium on Principles of Programming Languages, pages 224--235, New Orleans, LA, January 2003. Google ScholarDigital Library
Index Terms
- A foundation for flow-based program matching: using temporal logic and model checking
Recommendations
A foundation for flow-based program matching: using temporal logic and model checking
POPL '09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesReasoning 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-...
Model checking discounted temporal properties
Tools and algorithms for the construction and analysis of systems (TACAS 2004)Temporal logic is two-valued: formulas are interpreted as either true or false. When applied to the analysis of stochastic systems, or systems with imprecise formal models, temporal logic is therefore fragile: even small changes in the model can lead to ...
Temporal Logic Query Checking: A Tool for Model Exploration
Temporal logic query checking was first introduced by W. Chan in order to speed up design understanding by discovering properties not known a priori. A query is a temporal logic formula containing a special symbol ?_1, known as a placeholder. Given a ...
Comments