The semantics of semantic patches in Coccinelle: Program transformation for the working programmer (full paper). Project home page: www.emn.fr/x-info/coccinelle

Abstract. We rationally reconstruct the core of the Coccinelle system, used for automating and documenting collateral evolutions in Linux de-vice drivers. A denotational semantics of the system’s underlying seman-tic patch language (SmPL) is developed, and extended to include vari-ables. The semantics is in essence a higher-order functional program and so executable; but is inefficient and limited to straight-line source pro-grams. A richer and more efficient SmPL version is defined, implemented by compiling to the temporal logic CTL-V (CTL with existentially quan-tified variables ranging over source code parameters and program points; defined using the staging concept from partial evaluation). The compila-tion is formally proven correct and a model check algorithm is outlined.