Sciweavers

Share
APLAS
2007
ACM

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

9 years 5 months ago
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.
Neil D. Jones, René Rydhof Hansen
Added 12 Aug 2010
Updated 12 Aug 2010
Type Conference
Year 2007
Where APLAS
Authors Neil D. Jones, René Rydhof Hansen
Comments (0)
books