diff --git a/chore/travis/travis-extra.sh b/chore/travis/travis-extra.sh index df2881e3de3..bda63159deb 100755 --- a/chore/travis/travis-extra.sh +++ b/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) diff --git a/doc/_data/sidebar_doc.yml b/doc/_data/sidebar_doc.yml index 7d7fed4a369..9e453a1756f 100644 --- a/doc/_data/sidebar_doc.yml +++ b/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 diff --git a/doc/images/smplgui-modes.png b/doc/images/smplgui-modes.png new file mode 100644 index 00000000000..d4a6ad0d2cb Binary files /dev/null and b/doc/images/smplgui-modes.png differ diff --git a/doc/images/smplgui.png b/doc/images/smplgui.png new file mode 100644 index 00000000000..3e2eceee5de Binary files /dev/null and b/doc/images/smplgui.png differ diff --git a/doc/spoon_smpl.md b/doc/spoon_smpl.md new file mode 100644 index 00000000000..74d026c9aab --- /dev/null +++ b/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 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; +} + +``` diff --git a/spoon-smpl/LICENSE.txt b/spoon-smpl/LICENSE.txt new file mode 100644 index 00000000000..8e49eed08f5 --- /dev/null +++ b/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. \ No newline at end of file diff --git a/spoon-smpl/README.md b/spoon-smpl/README.md new file mode 100644 index 00000000000..6a57ba56f47 --- /dev/null +++ b/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. diff --git a/spoon-smpl/pom.xml b/spoon-smpl/pom.xml new file mode 100644 index 00000000000..1f2177e1840 --- /dev/null +++ b/spoon-smpl/pom.xml @@ -0,0 +1,98 @@ + + + 4.0.0 + fr.inria.gforge.spoon + spoon-smpl + 0.0.1 + + + The MIT license + http://www.opensource.org/licenses/mit-license.php + repo + + + + fr.inria.gforge.spoon + spoon-pom + 1.0 + ../spoon-pom + + + + + org.apache.maven.plugins + maven-compiler-plugin + 3.3 + + 11 + 11 + + + + org.apache.maven.plugins + maven-checkstyle-plugin + 3.1.0 + + true + ../checkstyle.xml + true + + + + verify + + checkstyle + + + + + + + + + com.mycila + license-maven-plugin + +
LICENSE.txt
+ src + + main/java/** + + + + + + check + + + + + + + + + + fr.inria.gforge.spoon + spoon-core + 8.4.0-SNAPSHOT + + + fr.inria.gforge.spoon + spoon-control-flow + 0.0.2-SNAPSHOT + + + junit + junit + 4.12 + test + + + + diff --git a/spoon-smpl/smpl_grammar.txt b/spoon-smpl/smpl_grammar.txt new file mode 100644 index 00000000000..c902481c83d --- /dev/null +++ b/spoon-smpl/smpl_grammar.txt @@ -0,0 +1,41 @@ +TODO: further update this file to reflect the "final" implementation used in the thesis +TODO: markdownify this file + + + Adapted from http://coccinelle.lip6.fr/docs/main_grammar.pdf + + + Note: This grammar is incomplete as it does not cover dots variant < ... > + and pattern disjunction ( a | b ) + + + + program ::= changeset+ + + changeset ::= metavariables transformation + + metavariables ::= @@ metadecl* @@ | @ rulename @ metadecl* @@ + + rulename ::= id + + metadecl ::= metatype ids (when matches "regex")? ; + + metatype ::= identifier + | type + | expression + | statement + | constant + | JavaType + + ids ::= id (, id)* + + transformation ::= OPTDOTSEQ(top, when) + + top ::= java_expr | java_decl_stmt+ | java_fundecl //this is where the java lives + + when ::= when != when_code + | when exists + | when any + + OPTDOTSEQ(grammar, when) = [... (when)*] grammar (... (when)* grammar)* [... (when)*] + \ No newline at end of file diff --git a/spoon-smpl/src/main/java/spoon/smpl/AnchoredOperationsMap.java b/spoon-smpl/src/main/java/spoon/smpl/AnchoredOperationsMap.java new file mode 100644 index 00000000000..a4bfc7bd08d --- /dev/null +++ b/spoon-smpl/src/main/java/spoon/smpl/AnchoredOperationsMap.java @@ -0,0 +1,72 @@ +/** + * 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. + */ + +package spoon.smpl; + +import spoon.smpl.operation.Operation; + +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; + +/** + * An AnchoredOperationsMap is a Map from line numbers (integers) to Lists of Operations. + */ +public class AnchoredOperationsMap extends HashMap> { + /** + * Special key used for anchoring operations to the method body block. + */ + public static final Integer methodBodyAnchor = -1; + + /** + * Get operations anchored to the method body block, if any. + * + * @return List of operations, or null. + */ + public List getOperationsAnchoredToMethodBody() { + return getOrDefault(methodBodyAnchor, null); + } + + /** + * Ensure a key exists, adding it if it does not. + * + * @param k Key which must exist + */ + public void addKeyIfNotExists(Integer k) { + if (!containsKey(k)) { + put(k, new ArrayList<>()); + } + } + + /** + * Merge all contents from a second AnchoredOperationsMap map into + * this one. + * + * @param other AnchoredOperationsMap from which to merge all contents + */ + public void join(AnchoredOperationsMap other) { + for (int k : other.keySet()) { + addKeyIfNotExists(k); + get(k).addAll(other.get(k)); + } + } +} diff --git a/spoon-smpl/src/main/java/spoon/smpl/CFGModel.java b/spoon-smpl/src/main/java/spoon/smpl/CFGModel.java new file mode 100644 index 00000000000..f78796aa1c2 --- /dev/null +++ b/spoon-smpl/src/main/java/spoon/smpl/CFGModel.java @@ -0,0 +1,223 @@ +/** + * 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. + */ + +package spoon.smpl; + +import fr.inria.controlflow.BranchKind; +import fr.inria.controlflow.ControlFlowNode; +import spoon.reflect.declaration.CtElement; +import spoon.reflect.declaration.CtExecutable; +import spoon.smpl.label.BranchLabel; +import spoon.smpl.label.MetadataLabel; +import spoon.smpl.label.MethodHeaderLabel; +import spoon.smpl.label.PropositionLabel; +import spoon.smpl.label.StatementLabel; + +import java.util.ArrayList; +import java.util.Collections; +import java.util.HashMap; +import java.util.List; +import java.util.Map; + +/** + * A CFGModel builds a CTL model from a given SmPL-adapted CFG. + */ +public class CFGModel implements Model { + /** + * Create a new CTL model from a given SmPL-adapted CFG. + * + * @param cfg SmPL-adapted CFG to use as model + */ + public CFGModel(SmPLMethodCFG cfg) { + this.cfg = cfg; + + states = new ArrayList<>(); + successors = new HashMap<>(); + labels = new HashMap<>(); + + for (ControlFlowNode node : cfg.vertexSet()) { + if (node.getKind() == BranchKind.BEGIN) { + // Dont add a state for the BEGIN node + continue; + } + + int state = node.getId(); + + // Add a state ID for each vertex ID and prepare lists of successors and labels + states.add(state); + successors.put(state, new ArrayList()); + labels.put(state, new ArrayList