The Semantics of "Semantic Patches" in Coccinelle: Program Transformation for the Working Programmer

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 compilation is formally proven correct and a model check algorithm is outlined.

• Type: Conference
• Year: 2007
• Where: APLAS
• Authors: Neil D. Jones, René Rydhof Hansen
• Keywords: APLAS 2007, Linux Device Drivers, Programming Languages, Semantic Patch Language, Semantics