Skip to content

Commit

Permalink
Merge 60efbd1 into e7d4213
Browse files Browse the repository at this point in the history
  • Loading branch information
mkforsb committed Apr 2, 2020
2 parents e7d4213 + 60efbd1 commit 9b19e38
Show file tree
Hide file tree
Showing 52 changed files with 4,645 additions and 0 deletions.
8 changes: 8 additions & 0 deletions spoon-smpl/README.md
@@ -0,0 +1,8 @@
# spoon-smpl

This module aims to implement support for (a variant/subset of) [SmPL](https://en.wikipedia.org/wiki/Coccinelle_(software)#Semantic_Patch_Language "Wikipedia entry").

Papers:
* [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)
93 changes: 93 additions & 0 deletions spoon-smpl/pom.xml
@@ -0,0 +1,93 @@
<?xml version="1.0" encoding="UTF-8"?>
<project xmlns="http://maven.apache.org/POM/4.0.0"
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
<modelVersion>4.0.0</modelVersion>
<groupId>fr.inria.gforge.spoon</groupId>
<artifactId>spoon-smpl</artifactId>
<version>0.0.1</version>
<licenses>
<license>
<name>The MIT license</name>
<url>http://www.opensource.org/licenses/mit-license.php</url>
<distribution>repo</distribution>
</license>
</licenses>
<parent>
<groupId>fr.inria.gforge.spoon</groupId>
<artifactId>spoon-pom</artifactId>
<version>1.0</version>
<relativePath>../spoon-pom</relativePath>
</parent>
<build>
<plugins>
<plugin>
<groupId>org.apache.maven.plugins</groupId>
<artifactId>maven-compiler-plugin</artifactId>
<version>3.3</version>
<configuration>
<source>1.8</source>
<target>1.8</target>
</configuration>
</plugin>
<plugin>
<groupId>org.apache.maven.plugins</groupId>
<artifactId>maven-checkstyle-plugin</artifactId>
<version>3.1.0</version>
<configuration>
<failsOnError>true</failsOnError>
<configLocation>../checkstyle.xml</configLocation>
<consoleOutput>true</consoleOutput>
</configuration>
<executions>
<execution>
<phase>verify</phase>
<goals>
<goal>checkstyle</goal>
</goals>
</execution>
</executions>
</plugin>
</plugins>
<pluginManagement>
<plugins>
<plugin>
<groupId>com.mycila</groupId>
<artifactId>license-maven-plugin</artifactId>
<configuration>
<header>LICENSE.txt</header>
<basedir>src</basedir>
<includes>
<include>main/java/**</include>
</includes>
</configuration>
<executions>
<execution>
<goals>
<goal>check</goal>
</goals>
</execution>
</executions>
</plugin>
</plugins>
</pluginManagement>
</build>
<dependencies>
<dependency>
<groupId>fr.inria.gforge.spoon</groupId>
<artifactId>spoon-core</artifactId>
<version>8.1.0-SNAPSHOT</version>
</dependency>
<dependency>
<groupId>fr.inria.gforge.spoon</groupId>
<artifactId>control-flow</artifactId>
<version>0.0.1</version>
</dependency>
<dependency>
<groupId>junit</groupId>
<artifactId>junit</artifactId>
<version>4.11</version>
<scope>test</scope>
</dependency>
</dependencies>
</project>
68 changes: 68 additions & 0 deletions spoon-smpl/smpl_grammar.txt
@@ -0,0 +1,68 @@
TODO: markdownify this file

First milestone SmPL grammar:

Adapted from http://coccinelle.lip6.fr/docs/main_grammar.pdf



Note: This grammar is incomplete as it does not cover dot modifiers <...> and <+...+>,
pattern disjunction (p | ... | p) and conjunction (p && ... && p)

These constructs are to be part of the first milestone but could not be
trivially lifted from the official grammar PDF as they are buried in the
C-specific parts of that grammar.



program ::= include_cocci* changeset+

include_cocci ::= #include string
| using string patch-local isomorphism definitions?
| using pathToIsoFile
// | virtual id (,id)*

changeset ::= metavariables transformation
// | script_metavariables script_code

metavariables ::= @@ metadecl* @@ | @ rulename @ metadecl* @@

// rulename ::= id [extends id] [depends on] [scope] dep [iso] [disable-iso] [exists] [rulekind]
rulename ::= id

metadecl ::= identifier ids ;
| type ids ;
| expression [list] ids ;
| statement [list] ids ;
| constant ids ;
| JavaType ids ;
// too much removed to include here

ids ::= pmid (, pmid)*
pmid ::= id | mid
mid ::= rulename_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 any lifting shortest path restriction
// | when strict applicable to error states (how are these determined?)
| when exists not all paths need to match
| when forall all paths must match the complete rule
// | when true != expr
// | when false != expr


OPTDOTSEQ(grammar, when) = [... (when)*] grammar (... (when)* grammar)* [... (when)*]




Notable omissions in first milestone:

dots in method calls: foo(...)
"when any" lifting of shortest-path restriction for dots
"fresh identifier" metavariables for code generation
constraints/regexes on metavariable ids
3 changes: 3 additions & 0 deletions spoon-smpl/smplcli.sh
@@ -0,0 +1,3 @@
#!/bin/bash
DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
java -cp $(for f in $DIR/target/*.jar; do echo -n $f:; done) spoon.smpl.CommandlineApplication $@
105 changes: 105 additions & 0 deletions spoon-smpl/src/main/java/spoon/smpl/BranchLabel.java
@@ -0,0 +1,105 @@
package spoon.smpl;

import spoon.reflect.code.CtIf;
import spoon.reflect.declaration.CtElement;
import spoon.smpl.formula.BranchPattern;
import spoon.smpl.formula.Predicate;
import spoon.smpl.pattern.PatternBuilder;
import spoon.smpl.pattern.PatternMatcher;
import spoon.smpl.pattern.PatternNode;

import java.util.Map;

/**
* A BranchLabel is a Label used to associate states with CtElement code
* elements that can be matched using BranchPattern Formula elements.
*/
public class BranchLabel implements Label {
/**
* Create a new BranchLabel.
* @param cond Condition element of a branch statement element such as CtIf
*/
public BranchLabel(CtElement cond) {
CtElement parent = cond.getParent(); // throws ParentNotInitializedException

boolean ok = false;

// check for supported type of branch element, more supported types to come
if (parent instanceof CtIf) {
ok = true;
}

if (!ok) {
throw new IllegalArgumentException("Invalid condition parent");
}

this.cond = cond;

PatternBuilder builder = new PatternBuilder();
cond.accept(builder);
this.condPattern = builder.getResult();

this.metavarBindings = null;
}

/**
* Test whether the label matches the given predicate.
* @param obj Predicate to test
* @return True if the predicate is a StatementPattern element whose Pattern matches the code exactly once, false otherwise.
*/
public boolean matches(Predicate obj) {
if (obj instanceof BranchPattern) {
BranchPattern bp = (BranchPattern) obj;

if (!bp.getBranchType().isInstance(cond.getParent())) {
return false;
}

PatternMatcher matcher = new PatternMatcher(bp.getConditionPattern());
condPattern.accept(matcher);
metavarBindings = matcher.getParameters();
return matcher.getResult() && bp.processMetavariableBindings(metavarBindings);
} else {
return false;
}
}

/**
* Retrieve any metavariable bindings involved in matching the most recently
* given predicate.
* @return most recent metavariable bindings, or null if there were no bindings
*/
@Override
public Map<String, Object> getMetavariableBindings() {
return metavarBindings;
}

/**
* Reset/clear metavariable bindings
*/
@Override
public void reset() {
metavarBindings = null;
}

/**
* Get the code element.
* @return The code element
*/
public CtElement getCondition() {
return cond;
}

/**
* The branch condition element.
*/
private CtElement cond;

/**
* The pattern corresponding to the branch condition element.
* Part of temporary substitute for spoon.pattern.
*/
private PatternNode condPattern;

private Map<String, Object> metavarBindings;
}

0 comments on commit 9b19e38

Please sign in to comment.