The semantics of "semantic patches" in coccinelle: Program transformation for the working programmer

Abstract

We rationally reconstruct the core of the Coccinelle system, used for automating and documenting collateral evolutions in Linux device drivers. A denotational semantics of the system's underlying semantic patch language (SmPL) is developed, and extended to include variables. The semantics is in essence a higher-order functional program and so executable; but is inefficient and limited to straight-line source programs. A richer and more efficient SmPL version is defined, implemented by compiling to the temporal logic CTL-V (CTL with existentially quantified variables ranging over source code parameters and program points; defined using the staging concept from partial evaluation). The compilar tion is formally proven correct and a model check algorithm is outlined. © Springer-Verlag Berlin Heidelberg 2007.