feat(spoon-smpl): initial support for the semantic patch language (Cr…

…edits: Mikael Forsberg) (#3282)

chore/travis/travis-extra.sh

@@ -75,6 +75,18 @@ git diff
 
 mvn -q -Djava.src.version=11 test
 
+##################################################################
+# Spoon-smpl
+##################################################################
+cd ../spoon-smpl
+
+# always depends on the latest snapshot, just installed with "mvn install" above
+mvn -q versions:use-latest-versions -DallowSnapshots=true -Dincludes=fr.inria.gforge.spoon
+git diff
+
+mvn -q -Djava.src.version=11 test
+mvn -q checkstyle:checkstyle license:check
+
 ##################################################################
 ## Trigerring extra tasks that we don't want to commit to master
 ## (For experimental CI features, short lived tasks, etc)

doc/_data/sidebar_doc.yml

@@ -130,6 +130,13 @@ entries:
           product: all
           version: all
 
+        - title: Semantic patching
+          url: /spoon_smpl.html
+          audience: writers, designers
+          platform: all
+          product: all
+          version: all
+
         - title: Code Generation
           url: '/pattern.html#generator'
           audience: writers, designers

doc/spoon_smpl.md

@@ -0,0 +1,255 @@
+---
+title: Semantic patching
+tags: [semantic-patching]
+keywords: patch, patching, semantic, smpl, spoon
+---
+
+The [spoon-smpl](https://github.com/mkforsb/spoon/tree/smpl/spoon-smpl) submodule provides a
+prototype implementation of a subset of [SmPL](http://coccinelle.lip6.fr/) (Semantic Patch Language)
+for a subset of Java. SmPL patches can be thought of as traditional plain text patches with enhanced
+expressiveness thanks to support for the syntax and semantics of specific programming languages. For
+example, a Java SmPL patch can be written to specify a generic transformation that reorders of a series
+of method call arguments without having to worry about matching any specific literal variable names
+or other literal argument expressions.
+
+
+### Installation
+
+On a Unix-like system, the following set of commands should be sufficient for getting spoon-smpl up
+and running from scratch.
+
+```
+$ git clone -b smpl https://github.com/mkforsb/spoon.git
+$ cd spoon/spoon-smpl
+$ mvn package
+$ ./tools/smplcli.sh
+usage:
+smplcli ACTION [ARG [ARG ..]]
+
+    ACTIONs:
+        patch        apply SmPL patch
+                     requires --smpl-file and --java-file
+
+        check        run model checker
+                     requires --smpl-file and --java-file
+
+        checksub     run model checker on every subformula
+                     requires --smpl-file and --java-file
+
+        rewrite      rewrite SmPL input
+                     requires --smpl-file
+
+        compile      compile SmPL input
+                     requires --smpl-file
+
+        ctl          compile and print CTL formula
+                     requires --smpl-file
+
+    ARGs:
+        --smpl-file FILENAME
+        --java-file FILENAME
+```
+
+Alternatively, the command line application can be invoked directly as:
+
+```
+$ java -cp <classpath> spoon.smpl.CommandlineApplication
+```
+
+
+### Scope of implementation
+
+Due in large to the prototypical nature of the current implementation there is a lack of clear
+specification and documentation. The most helpful resources currently available are:
+
+1. [smpl_grammar.txt](https://github.com/mkforsb/spoon/blob/smpl/spoon-smpl/smpl_grammar.txt): covers parts of the currently supported grammar.
+2. [Test cases](https://github.com/mkforsb/spoon/tree/smpl/spoon-smpl/src/test/resources/endtoend): contains easy-to-read test cases that reveal both supported patch language features and supported Java elements.
+3. [PatternBuilder.java](https://github.com/mkforsb/spoon/blob/smpl/spoon-smpl/src/main/java/spoon/smpl/pattern/PatternBuilder.java): shows the set of matchable Java elements, but can be cumbersome to read.
+4. [Substitutor.java](https://github.com/mkforsb/spoon/blob/smpl/spoon-smpl/src/main/java/spoon/smpl/Substitutor.java): shows the set of transformable Java elements, but can be cumbersome to read.
+
+### Basic usage
+
+The basic use case of spoon-smpl involves at minimum two files: one .java source file and one 
+semantic patch. For this tutorial, we will use the following two files:
+
+#### File 1: example semantic patch (patch.smpl)
+```patch
+@@
+type T;
+identifier ret;
+constant C;
+@@
+- T ret = C;
+... when != ret
+- return ret;
++ return C;
+```
+
+This example patch removes local variables only used to return a constant.
+
+
+#### File 2: example Java source (Program.java)
+```java
+public class Program {
+    public int fn1() {
+        int x = 1;
+        return x;
+    }
+
+    public int fn2(boolean print) {
+        int x = 2;
+
+        if (print) {
+            System.out.println("hello from fn2");
+        }
+
+        return x;
+    }
+
+    public int fn3(boolean print) {
+        int x = 3;
+
+        if (print) {
+            System.out.println(x);
+        }
+
+        return x;
+    }
+}
+```
+
+We then apply the semantic patch to the Java source code as follows (output also shown):
+
+```
+$ ./tools/smplcli.sh patch --smpl-file patch.smpl --java-file Program.java
+
+public class Program {
+    public int fn1() {
+        return 1;
+    }
+
+    public int fn2(boolean print) {
+        if (print) {
+            java.lang.System.out.println("hello from fn2");
+        }
+        return 2;
+    }
+
+    public int fn3(boolean print) {
+        int x = 3;
+        if (print) {
+            java.lang.System.out.println(x);
+        }
+        return x;
+    }
+}
+
+```
+
+### Graphical interface
+
+There is a very simple graphical interface available in `tools/smplgui.py`. This tool requires 
+Python 3 and a suitable `python3-pyqt5` package providing Qt5 bindings, in particular the module
+`PyQt5.QtGui`. Furthermore, the tool currently assumes it is executing on a Unix-like system from
+a working directory in which the file `./tools/smplcli.sh` is available to run spoon-smpl. As such,
+it is recommended to start the tool from the spoon-smpl root folder using the command `$ ./tools/smplgui.py`.
+
+![Spoon-smpl graphical interface]({{ "/images/smplgui.png" | prepend: site.baseurl }})
+
+The tool provides two panes for editing the semantic patch and some Java source code, respectively.
+The upper left pane contains the semantic patch, while the upper right pane contains the Java source
+code. Finally, the tool provides a number of modes for invoking spoon-smpl using the inputs shown in
+the two panes. To change mode one presses the F6 key followed by the key corresponding to the
+desired mode, as shown in the image below. To execute the currently selected mode, one presses the
+F5 key.
+
+![Spoon-smpl graphical interface modes]({{ "/images/smplgui-modes.png" | prepend: site.baseurl }})
+
+These modes correspond to the `ACTION` alternatives present in `spoon.smpl.CommandLineApplication`,
+with the addition of the `gentest` mode which generates a test case in a special format for the
+inputs present in the two upper panes.
+
+
+### Batch processing
+
+Spoon-smpl provides a batch processing mode in which a single semantic patch is applied to a full
+source tree recursively. This mode is implemented in the form of a Spoon `Processor` that also
+features a `main` method. The following example command is intended to be executed in the spoon-smpl
+root directory, where a call to `mvn package` has placed a full suite of `.jar` files in the
+`./target` sub-directory.
+
+```
+$ java -cp $(for f in target/*.jar; do echo -n $f:; done) spoon.smpl.SmPLProcessor \
+       --with-diff-command "bash -c \"diff -U5 -u {a} {b}\""                       \
+       --with-smpl-file "path/to/patch.smpl"                                       \
+       
+       ## The following options are passed to spoon.Launcher, more may be added
+       -i "path/to/target/source"                                                  \
+       -o "path/to/write/output"                                                   \
+       -p spoon.smpl.SmPLProcessor
+```
+
+The expression `-cp $(for f in target/*.jar; do echo -n $f:; done)` collects and places on the
+classpatch all `.jar` files found in the `target` sub-directory.
+
+The `--with-diff-command` option expects a shell-executable command string containing the
+placeholder expressions `{a}` and `{b}`. The placeholders are substituted for the full paths to the
+pretty-printed input and the pretty-printed output respectively, for each modified file in the
+source tree. For example, in the event that spoon-smpl during batch processing has modified a file
+`Program.java`, the option used in the example command would result in a command akin to the
+following being executed:
+
+```
+bash -c "diff -U5 -u /tmp/9qKMH/Program.java /tmp/CYd40/Program.java"
+```
+
+
+### Developing
+
+The following code shows the core workflow of spoon-smpl, and is intended to guide developers
+towards finding the code for the component(s) of interest:
+
+```java
+boolean tryApplyPatch(String plainTextSmPLCode, CtExecutable patchTargetExe) {
+    // Parse a plain text SmPL patch
+    SmPLRule rule = SmPLParser.parse(plainTextSmPLCode);
+
+    // Create the CFG from the executable block
+    SmPLMethodCFG cfg = new SmPLMethodCFG(patchTargetExe);
+
+    // Create the CTL model from the CFG
+    CFGModel model = new CFGModel(cfg);
+
+    // Create the model checker
+    ModelChecker checker = new ModelChecker(model);
+
+    // Run the model checker on the formula that encodes the SmPL patch
+    // This uses the visitor pattern
+    //   We ask the formula tree to accept the model checker visitor
+    rule.getFormula().accept(checker);
+
+    // Fetch the results
+    ModelChecker.ResultSet results = checker.getResult();
+
+    // If we get an empty result, there were no matches
+    // If we get no witnesses, there were no transformations to apply
+    if (results.isEmpty() || results.getAllWitnesses().isEmpty()) {
+        // Restore metamodel changes applied by SmPLMethodCFG
+        model.getCfg().restoreUnsupportedElements();
+        return false;
+    }
+
+    // Apply transformations
+    Transformer.transform(model, results.getAllWitnesses());
+
+    // Copy any new methods added by the patch
+    if (rule.getMethodsAdded().size() > 0) {
+        Transformer.copyAddedMethods(model, rule);
+    }
+
+    // Restore metamodel changes applied by SmPLMethodCFG
+    model.getCfg().restoreUnsupportedElements();
+    return true;
+}
+
+```

spoon-smpl/LICENSE.txt

@@ -0,0 +1,19 @@
+The MIT License
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in
+all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+THE SOFTWARE.

spoon-smpl/README.md

@@ -0,0 +1,39 @@
+# Spoon-smpl: Semantic Patches for Java
+
+This Spoon module implements the Semantic Patch Language called [SmPL](https://en.wikipedia.org/wiki/Coccinelle_(software)#Semantic_Patch_Language "Wikipedia entry"). The Semantic Patch Language, invented for C by the seminal tool [Coccinelle](https://github.com/coccinelle/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.
+
+```java
+@@
+Context ctx;
+expression E;
+@@
+- ctx.getResources().getColor(E)
++ ContextCompat.getColor(ctx , E)
+``` 
+
+Spoon-SmPL has been implemented by Mikael Forsberg in 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](http://coccinelle.lip6.fr/papers/ercim.pdf)
+* [A Foundation for Flow-Based Program Matching Using Temporal Logic and Model Checking](http://coccinelle.lip6.fr/papers/popl09.pdf)
+* [Semantic Patches for Java Program Transformation](https://drops.dagstuhl.de/opus/volltexte/2019/10814/pdf/LIPIcs-ECOOP-2019-22.pdf)
+
+## 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.