Spoon-smpl: Semantic Patches for Java

This Spoon module implements the Semantic Patch Language called SmPL. The Semantic Patch Language, invented for C by the seminal tool Coccinelle enables to apply transformations in an automated way, where the transformation itself is a patch written in a special syntax.

Here is an example of a semantic patch that replaces all calls to a specific method by another one.

@@
Context ctx;
expression E;
@@
- ctx.getResources().getColor(E)
+ ContextCompat.getColor(ctx , E)

Spoon-SmPL's initial version has been implemented by Mikael Forsberg as part of his master's thesis "Design and Implementation of Semantic Patch Support for the Spoon Java Transformation Engine' at KTH Royal Institute of Technology".

References:

• SmPL: A Domain-Specific Language for Specifying Collateral Evolutions in Linux Device Drivers
• A Foundation for Flow-Based Program Matching Using Temporal Logic and Model Checking
• Semantic Patches for Java Program Transformation
• Design and Implementation of Semantic Patch Support for the Spoon Java Transformation Engine' at KTH Royal Institute of Technology

Supported SmPL Features

The following table shows some of the currently supported SmPL syntax/features:

Syntax	Description
@@ identifier x; @@	Identifier metavariable.
@@ type x; @@	Arbitrary type name metavariable.
@@ SomeType x; @@	Specific type name metavariable.
@@ constant x; @@	Constant metavariable.
@@ expression x; @@	Expression metavariable.
statement	Context match.
- statement	Match and deletion.
+ statement	Addition.
...	Computation path wildcard operator.
... when != expr	"    with match constraint.
... when exists	"    with constraint relaxation.
... when any	"    with constraint relaxation.
<... P ...>	Computation path wildcard with optional match of P.
f(...)	Argument or parameter list wildcard match.

Additional helpful resources currently available are:

1. smpl_grammar.txt: covers parts of the currently supported grammar.
2. Test cases: contains easy-to-read test cases that reveal both supported patch language features and supported Java elements.
3. PatternBuilder.java: shows the set of matchable Java elements, but can be cumbersome to read.
4. Substitutor.java: shows the set of transformable Java elements, but can be cumbersome to read.

Architecture Notes

• Parsing SMPL: see SmPLLexer
  • SmPLLexer is used by SmPLParser, whose main method is method parse. Next, method rewrite transforms the SmPL code into the Java DSL.
• class SmPLRule encapsulates a single rule, it is created by method SmPLParser#compile
• class FormulaCompiler generates the CTL formula, method compileFormula() returns a Formula
• ModelChecker takes a CFGModel as input (there is one CFGModel instance per method in the project to be analyzed) (there are many CFGModel and only one Formula, and then evaluates the formula on the model. The evaluation is done through interpretation with a visitor over the formula code. It returns a Result containing a set of Witness that encode the metavariable bindings and transformation operations, and this set is taken as input by Transformer.
• Transformer takes the CFG model and a set of Witness
• package spoon.smpl.operation contains reified operations and a way to execute them
• Substitutor substitutes meta-variables by their bound values
• The full loop can be seen in method spoon.smpl.SmPLProcessor#tryApplyPatch

Ideas

• CFGModel could be merged SmPLMethodCFG
• The Operation hierarchy could be merged with that of Gumtree-Spoon
• Substitutor could be unified with the existing Pattern architecture.