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 Coccinelle’s 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.
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 Coccinelle’s 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.
| Original language | English |
|---|---|
| Title of host publication | POPL '09 : Proceedings of the 36th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages |
| Number of pages | 12 |
| Publisher | Association for Computing Machinery |
| Publication date | 2009 |
| Pages | 114-126 |
| ISBN (Print) | 978-1-60558-379-2 |
| DOIs | |
| Publication status | Published - 2009 |
| Event | Annual Symposium on Principles of Programming Languages - Savannah, Georgia, United States Duration: 21 Jan 2009 → 23 Jan 2009 Conference number: 36 |
Conference
| Conference | Annual Symposium on Principles of Programming Languages |
|---|---|
| Number | 36 |
| Country/Territory | United States |
| City | Savannah, Georgia |
| Period | 21/01/2009 → 23/01/2009 |
| Series | SIGPLAN Notices |
|---|---|
| Number | 44(1) |
| ISSN | 0362-1340 |