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

摘要

Reasoning about program control-flow paths is an important func-tionality of a number of recent program matching languages andassociated searching and transformation tools. Temporal logic pro-vides a well-defined means of expressing properties of control-flowpaths in programs, and indeed an extension of the temporal logicCTL has been applied to the problem of specifying and verifyingthe transformations commonly performed by optimizing compilers.Nevertheless, in developing the Coccinelle program transformationtool for performing Linux collateral evolutions in systems code, wehave found that existing variants of CTL do not adequately supportrules that transform subterms other than the ones matching an entireformula. Being able to transform any of the subterms of a matchedterm seems essential in the domain targeted by Coccinelle. In this paper, we propose an extension to CTL named CTL-VW (CTL with variables and witnesses) that is a suitable basisfor the semantics and implementation of the Coccinelle's programmatching language. Our extension to CTL includes existentialquantification over program fragments, which allows metavariablesin the program matching language to range over different valueswithin different control-flow paths, and a notion of witnesses thatrecord such existential bindings for use in the subsequent programtransformation process. We formalize CTL-VW and describe its usein the context of Coccinelle. We then assess the performance of theapproach in practice, using a transformation rule that fixes severalreference count bugs in Linux code.