|
| 1 | +--- |
| 2 | +title: Semantic patching |
| 3 | +tags: [semantic-patching] |
| 4 | +keywords: patch, patching, semantic, smpl, spoon |
| 5 | +--- |
| 6 | + |
| 7 | +The [spoon-smpl](https://github.com/mkforsb/spoon/tree/smpl/spoon-smpl) submodule provides a |
| 8 | +prototype implementation of a subset of [SmPL](http://coccinelle.lip6.fr/) (Semantic Patch Language) |
| 9 | +for a subset of Java. SmPL patches can be thought of as traditional plain text patches with enhanced |
| 10 | +expressiveness thanks to support for the syntax and semantics of specific programming languages. For |
| 11 | +example, a Java SmPL patch can be written to specify a generic transformation that reorders of a series |
| 12 | +of method call arguments without having to worry about matching any specific literal variable names |
| 13 | +or other literal argument expressions. |
| 14 | + |
| 15 | + |
| 16 | +### Installation |
| 17 | + |
| 18 | +On a Unix-like system, the following set of commands should be sufficient for getting spoon-smpl up |
| 19 | +and running from scratch. |
| 20 | + |
| 21 | +``` |
| 22 | +$ git clone -b smpl https://github.com/mkforsb/spoon.git |
| 23 | +$ cd spoon/spoon-smpl |
| 24 | +$ mvn package |
| 25 | +$ ./tools/smplcli.sh |
| 26 | +usage: |
| 27 | +smplcli ACTION [ARG [ARG ..]] |
| 28 | +
|
| 29 | + ACTIONs: |
| 30 | + patch apply SmPL patch |
| 31 | + requires --smpl-file and --java-file |
| 32 | +
|
| 33 | + check run model checker |
| 34 | + requires --smpl-file and --java-file |
| 35 | +
|
| 36 | + checksub run model checker on every subformula |
| 37 | + requires --smpl-file and --java-file |
| 38 | +
|
| 39 | + rewrite rewrite SmPL input |
| 40 | + requires --smpl-file |
| 41 | +
|
| 42 | + compile compile SmPL input |
| 43 | + requires --smpl-file |
| 44 | +
|
| 45 | + ctl compile and print CTL formula |
| 46 | + requires --smpl-file |
| 47 | +
|
| 48 | + ARGs: |
| 49 | + --smpl-file FILENAME |
| 50 | + --java-file FILENAME |
| 51 | +``` |
| 52 | + |
| 53 | +Alternatively, the command line application can be invoked directly as: |
| 54 | + |
| 55 | +``` |
| 56 | +$ java -cp <classpath> spoon.smpl.CommandlineApplication |
| 57 | +``` |
| 58 | + |
| 59 | + |
| 60 | +### Scope of implementation |
| 61 | + |
| 62 | +Due in large to the prototypical nature of the current implementation there is a lack of clear |
| 63 | +specification and documentation. The most helpful resources currently available are: |
| 64 | + |
| 65 | +1. [smpl_grammar.txt](https://github.com/mkforsb/spoon/blob/smpl/spoon-smpl/smpl_grammar.txt): covers parts of the currently supported grammar. |
| 66 | +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. |
| 67 | +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. |
| 68 | +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. |
| 69 | + |
| 70 | +### Basic usage |
| 71 | + |
| 72 | +The basic use case of spoon-smpl involves at minimum two files: one .java source file and one |
| 73 | +semantic patch. For this tutorial, we will use the following two files: |
| 74 | + |
| 75 | +#### File 1: example semantic patch (patch.smpl) |
| 76 | +```patch |
| 77 | +@@ |
| 78 | +type T; |
| 79 | +identifier ret; |
| 80 | +constant C; |
| 81 | +@@ |
| 82 | +- T ret = C; |
| 83 | +... when != ret |
| 84 | +- return ret; |
| 85 | ++ return C; |
| 86 | +``` |
| 87 | + |
| 88 | +This example patch removes local variables only used to return a constant. |
| 89 | + |
| 90 | + |
| 91 | +#### File 2: example Java source (Program.java) |
| 92 | +```java |
| 93 | +public class Program { |
| 94 | + public int fn1() { |
| 95 | + int x = 1; |
| 96 | + return x; |
| 97 | + } |
| 98 | + |
| 99 | + public int fn2(boolean print) { |
| 100 | + int x = 2; |
| 101 | + |
| 102 | + if (print) { |
| 103 | + System.out.println("hello from fn2"); |
| 104 | + } |
| 105 | + |
| 106 | + return x; |
| 107 | + } |
| 108 | + |
| 109 | + public int fn3(boolean print) { |
| 110 | + int x = 3; |
| 111 | + |
| 112 | + if (print) { |
| 113 | + System.out.println(x); |
| 114 | + } |
| 115 | + |
| 116 | + return x; |
| 117 | + } |
| 118 | +} |
| 119 | +``` |
| 120 | + |
| 121 | +We then apply the semantic patch to the Java source code as follows (output also shown): |
| 122 | + |
| 123 | +``` |
| 124 | +$ ./tools/smplcli.sh patch --smpl-file patch.smpl --java-file Program.java |
| 125 | +
|
| 126 | +public class Program { |
| 127 | + public int fn1() { |
| 128 | + return 1; |
| 129 | + } |
| 130 | +
|
| 131 | + public int fn2(boolean print) { |
| 132 | + if (print) { |
| 133 | + java.lang.System.out.println("hello from fn2"); |
| 134 | + } |
| 135 | + return 2; |
| 136 | + } |
| 137 | +
|
| 138 | + public int fn3(boolean print) { |
| 139 | + int x = 3; |
| 140 | + if (print) { |
| 141 | + java.lang.System.out.println(x); |
| 142 | + } |
| 143 | + return x; |
| 144 | + } |
| 145 | +} |
| 146 | +
|
| 147 | +``` |
| 148 | + |
| 149 | +### Graphical interface |
| 150 | + |
| 151 | +There is a very simple graphical interface available in `tools/smplgui.py`. This tool requires |
| 152 | +Python 3 and a suitable `python3-pyqt5` package providing Qt5 bindings, in particular the module |
| 153 | +`PyQt5.QtGui`. Furthermore, the tool currently assumes it is executing on a Unix-like system from |
| 154 | +a working directory in which the file `./tools/smplcli.sh` is available to run spoon-smpl. As such, |
| 155 | +it is recommended to start the tool from the spoon-smpl root folder using the command `$ ./tools/smplgui.py`. |
| 156 | + |
| 157 | +![Spoon-smpl graphical interface]({{ "/images/smplgui.png" | prepend: site.baseurl }}) |
| 158 | + |
| 159 | +The tool provides two panes for editing the semantic patch and some Java source code, respectively. |
| 160 | +The upper left pane contains the semantic patch, while the upper right pane contains the Java source |
| 161 | +code. Finally, the tool provides a number of modes for invoking spoon-smpl using the inputs shown in |
| 162 | +the two panes. To change mode one presses the F6 key followed by the key corresponding to the |
| 163 | +desired mode, as shown in the image below. To execute the currently selected mode, one presses the |
| 164 | +F5 key. |
| 165 | + |
| 166 | +![Spoon-smpl graphical interface modes]({{ "/images/smplgui-modes.png" | prepend: site.baseurl }}) |
| 167 | + |
| 168 | +These modes correspond to the `ACTION` alternatives present in `spoon.smpl.CommandLineApplication`, |
| 169 | +with the addition of the `gentest` mode which generates a test case in a special format for the |
| 170 | +inputs present in the two upper panes. |
| 171 | + |
| 172 | + |
| 173 | +### Batch processing |
| 174 | + |
| 175 | +Spoon-smpl provides a batch processing mode in which a single semantic patch is applied to a full |
| 176 | +source tree recursively. This mode is implemented in the form of a Spoon `Processor` that also |
| 177 | +features a `main` method. The following example command is intended to be executed in the spoon-smpl |
| 178 | +root directory, where a call to `mvn package` has placed a full suite of `.jar` files in the |
| 179 | +`./target` sub-directory. |
| 180 | + |
| 181 | +``` |
| 182 | +$ java -cp $(for f in target/*.jar; do echo -n $f:; done) spoon.smpl.SmPLProcessor \ |
| 183 | + --with-diff-command "bash -c \"diff -U5 -u {a} {b}\"" \ |
| 184 | + --with-smpl-file "path/to/patch.smpl" \ |
| 185 | + |
| 186 | + ## The following options are passed to spoon.Launcher, more may be added |
| 187 | + -i "path/to/target/source" \ |
| 188 | + -o "path/to/write/output" \ |
| 189 | + -p spoon.smpl.SmPLProcessor |
| 190 | +``` |
| 191 | + |
| 192 | +The expression `-cp $(for f in target/*.jar; do echo -n $f:; done)` collects and places on the |
| 193 | +classpatch all `.jar` files found in the `target` sub-directory. |
| 194 | + |
| 195 | +The `--with-diff-command` option expects a shell-executable command string containing the |
| 196 | +placeholder expressions `{a}` and `{b}`. The placeholders are substituted for the full paths to the |
| 197 | +pretty-printed input and the pretty-printed output respectively, for each modified file in the |
| 198 | +source tree. For example, in the event that spoon-smpl during batch processing has modified a file |
| 199 | +`Program.java`, the option used in the example command would result in a command akin to the |
| 200 | +following being executed: |
| 201 | + |
| 202 | +``` |
| 203 | +bash -c "diff -U5 -u /tmp/9qKMH/Program.java /tmp/CYd40/Program.java" |
| 204 | +``` |
| 205 | + |
| 206 | + |
| 207 | +### Developing |
| 208 | + |
| 209 | +The following code shows the core workflow of spoon-smpl, and is intended to guide developers |
| 210 | +towards finding the code for the component(s) of interest: |
| 211 | + |
| 212 | +```java |
| 213 | +boolean tryApplyPatch(String plainTextSmPLCode, CtExecutable patchTargetExe) { |
| 214 | + // Parse a plain text SmPL patch |
| 215 | + SmPLRule rule = SmPLParser.parse(plainTextSmPLCode); |
| 216 | + |
| 217 | + // Create the CFG from the executable block |
| 218 | + SmPLMethodCFG cfg = new SmPLMethodCFG(patchTargetExe); |
| 219 | + |
| 220 | + // Create the CTL model from the CFG |
| 221 | + CFGModel model = new CFGModel(cfg); |
| 222 | + |
| 223 | + // Create the model checker |
| 224 | + ModelChecker checker = new ModelChecker(model); |
| 225 | + |
| 226 | + // Run the model checker on the formula that encodes the SmPL patch |
| 227 | + // This uses the visitor pattern |
| 228 | + // We ask the formula tree to accept the model checker visitor |
| 229 | + rule.getFormula().accept(checker); |
| 230 | + |
| 231 | + // Fetch the results |
| 232 | + ModelChecker.ResultSet results = checker.getResult(); |
| 233 | + |
| 234 | + // If we get an empty result, there were no matches |
| 235 | + // If we get no witnesses, there were no transformations to apply |
| 236 | + if (results.isEmpty() || results.getAllWitnesses().isEmpty()) { |
| 237 | + // Restore metamodel changes applied by SmPLMethodCFG |
| 238 | + model.getCfg().restoreUnsupportedElements(); |
| 239 | + return false; |
| 240 | + } |
| 241 | + |
| 242 | + // Apply transformations |
| 243 | + Transformer.transform(model, results.getAllWitnesses()); |
| 244 | + |
| 245 | + // Copy any new methods added by the patch |
| 246 | + if (rule.getMethodsAdded().size() > 0) { |
| 247 | + Transformer.copyAddedMethods(model, rule); |
| 248 | + } |
| 249 | + |
| 250 | + // Restore metamodel changes applied by SmPLMethodCFG |
| 251 | + model.getCfg().restoreUnsupportedElements(); |
| 252 | + return true; |
| 253 | +} |
| 254 | + |
| 255 | +``` |
0 commit comments