A Foundation for Flow-Based Program Matching Using Temporal Logic and Model Checking

Julien Brunel, Damien Doligez, Rene Rydhof Hansen, Julia Lawall, Gilles Mulle

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

33 Citationer (Scopus)

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.

 


OriginalsprogEngelsk
TitelProceedings of the ACM Symposium on Principles of Programming Languages (POPL'09)
Antal sider13
ForlagAssociation for Computing Machinery
Publikationsdato2009
Sider114-126
ISBN (Trykt)978-1-60558-379-2
DOI
StatusUdgivet - 2009
BegivenhedAnnual Symposium on Principles of Programming Languages  (POPL 09) - Savannah, GA, USA
Varighed: 21 jan. 200923 jan. 2009
Konferencens nummer: 36

Konference

KonferenceAnnual Symposium on Principles of Programming Languages  (POPL 09)
Nummer36
Land/OmrådeUSA
BySavannah, GA
Periode21/01/200923/01/2009

Fingeraftryk

Dyk ned i forskningsemnerne om 'A Foundation for Flow-Based Program Matching Using Temporal Logic and Model Checking'. Sammen danner de et unikt fingeraftryk.

Citationsformater