Skip to content

Migrate to JMLtk #3966

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wadoon wants to merge 1 commit into
base: main
Choose a base branch
from
Draft

Migrate to JMLtk #3966

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion build.gradle
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -76,7 +76,7 @@ subprojects {
repositories {
mavenCentral()
//maven { url = "https://git.key-project.org/api/v4/projects/35/packages/maven/" }
//maven { url = "https://central.sonatype.com/repository/maven-snapshots/" }
maven { url = "https://central.sonatype.com/repository/maven-snapshots/" }
}

dependencies {
Expand Down
8 changes: 4 additions & 4 deletions gradle/libs.versions.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ stringtemplate = "4.3.4"

# Java parsing and analysis
javapoet = "1.13.0"
javaparser = "3.28.0-K13.6"
javaparser = "3.28.2-J8.0-K13.5-SNAPSHOT"
truth = "1.4.5"

# UI and CLI
Expand Down Expand Up @@ -67,9 +67,9 @@ stringtemplate = { module = "org.antlr:ST4", version.ref = "stringtemplate" }

# Java source code processing
javapoet = { module = "com.squareup:javapoet", version.ref = "javapoet" }
javaparser-core = { module = "org.key-project.proofjava:javaparser-core", version.ref = "javaparser" }
javaparser-core-serialization = { module = "org.key-project.proofjava:javaparser-core-serialization", version.ref = "javaparser" }
javaparser-symbol-solver-core = { module = "org.key-project.proofjava:javaparser-symbol-solver-core", version.ref = "javaparser" }
javaparser-core = { module = "io.github.jmltoolkit:jmlparser-core", version.ref = "javaparser" }
javaparser-core-serialization = { module = "io.github.jmltoolkit:jmlparser-core-serialization", version.ref = "javaparser" }
javaparser-symbol-solver-core = { module = "io.github.jmltoolkit:jmlparser-symbol-solver-core", version.ref = "javaparser" }

# Testing utilities
truth = { module = "com.google.truth:truth", version.ref = "truth" }
Expand Down
14 changes: 8 additions & 6 deletions key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/TransactionStatement.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,24 +5,26 @@

import java.util.List;

import de.uka.ilkd.key.java.*;
import de.uka.ilkd.key.java.ast.*;
import de.uka.ilkd.key.java.ast.Comment;
import de.uka.ilkd.key.java.ast.PositionInfo;
import de.uka.ilkd.key.java.ast.ProgramElement;
import de.uka.ilkd.key.java.ast.SourceData;
import de.uka.ilkd.key.java.visitor.Visitor;
import de.uka.ilkd.key.rule.MatchConditions;

import com.github.javaparser.ast.key.KeyTransactionStatement;
import com.github.javaparser.ast.key.KeyTransactionStmt;

public class TransactionStatement extends JavaStatement {
private final KeyTransactionStatement.TransactionType type;
private final KeyTransactionStmt.TransactionType type;

public TransactionStatement(KeyTransactionStatement.TransactionType type) {
public TransactionStatement(KeyTransactionStmt.TransactionType type) {
super();
this.type = type;
}

public TransactionStatement(
PositionInfo pi, List<Comment> c,
KeyTransactionStatement.TransactionType type) {
KeyTransactionStmt.TransactionType type) {
super(pi, c);
this.type = type;
}
Expand Down
48 changes: 20 additions & 28 deletions key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,6 +60,8 @@
import com.github.javaparser.ast.body.MethodDeclaration;
import com.github.javaparser.ast.comments.TraditionalJavadocComment;
import com.github.javaparser.ast.expr.*;
import com.github.javaparser.ast.jml.stmt.JmlExpressionStmt;
import com.github.javaparser.ast.jml.stmt.JmlExpressionStmt.JmlStmtKind;
import com.github.javaparser.ast.key.*;
import com.github.javaparser.ast.key.sv.*;
import com.github.javaparser.ast.modules.*;
Expand Down Expand Up @@ -278,6 +280,8 @@ public Object visit(BinaryExpr n, Void arg) {
case MULTIPLY -> BinaryOperatorKind.TIMES;
case DIVIDE -> BinaryOperatorKind.DIVIDE;
case REMAINDER -> BinaryOperatorKind.MODULO;
default ->
throw new IllegalStateException("JML operators not allowed: " + n.getOperator());
};
return new BinaryOperator(pi, c, op, lhs, rhs);
}
Expand Down Expand Up @@ -760,32 +764,21 @@ private ClassOrInterfaceDeclaration getContainingClass(Node node) {
}

@Override
public Object visit(KeYMarkerStatement n, Void arg) {
public Object visit(JmlExpressionStmt n, Void arg) {
PositionInfo pi = createPositionInfo(n);
return switch (n.getKind()) {
case MarkerStatementHelper.KIND_ASSERT -> {
case JmlStmtKind.ASSERT -> {
TextualJMLAssertStatement construct = n.getData(MarkerStatementHelper.KEY_ASSERT);
yield new JmlAssert(TextualJMLAssertStatement.Kind.ASSERT, construct, pi);
}
case MarkerStatementHelper.KIND_ASSUME -> {
case JmlStmtKind.ASSUME -> {
TextualJMLAssertStatement construct = n.getData(MarkerStatementHelper.KEY_ASSERT);
yield new JmlAssert(TextualJMLAssertStatement.Kind.ASSUME, construct, pi);
}
case MarkerStatementHelper.KIND_SET -> {
case JmlStmtKind.SET -> {
KeyAst.SetStatementContext context = n.getData(MarkerStatementHelper.KEY_ASSIGN);
yield new SetStatement(context, pi);
}


case MarkerStatementHelper.KIND_MERGE_POINT -> {
var loc = new LocationVariable(
services.getVariableNamer().getTemporaryNameProposal("x"),
services.getNamespaces().sorts().lookup("boolean"));
List<Comment> c = createComments(n);

TextualJMLMergePointDecl a = n.getData(MarkerStatementHelper.KEY_MERGE_POINT);
yield new MergePointStatement(pi, c, a, loc);
}
default -> throw new IllegalStateException("Unexpected value: " + n.getKind());
};
}
Expand Down Expand Up @@ -1696,7 +1689,7 @@ public Object visit(KeyCcatchReturn n, Void arg) {
}

@Override
public Object visit(KeyCatchAllStatement n, Void arg) {
public Object visit(KeyCatchAllStmt n, Void arg) {
// TODO
return reportUnsupportedElement(n);
}
Expand Down Expand Up @@ -1801,7 +1794,7 @@ private ImmutableArray<Expression> map(
}

@Override
public Object visit(KeyExecStatement n, Void arg) {
public Object visit(KeyExecStmt n, Void arg) {
PositionInfo pi = createPositionInfo(n);
var c = createComments(n);
StatementBlock body = accept(n.getExecBlock());
Expand All @@ -1825,7 +1818,7 @@ public Object visit(KeyExecutionContext n, Void arg) {
}

@Override
public Object visit(KeyLoopScopeBlock n, Void arg) {
public Object visit(KeyLoopScopeBlockStmt n, Void arg) {
PositionInfo pi = createPositionInfo(n);
List<Comment> c = createComments(n);
StatementBlock body = accept(n.getBlock());
Expand All @@ -1834,11 +1827,15 @@ public Object visit(KeyLoopScopeBlock n, Void arg) {
}

@Override
public Object visit(KeyMergePointStatement n, Void arg) {
public Object visit(KeyMergePointStmt n, Void arg) {
var pi = createPositionInfo(n);
List<Comment> c = createComments(n);
IProgramVariable expr = accept(n.getExpr());
return new MergePointStatement(pi, c, null, expr);
// IProgramVariable expr = accept(n.getExpr());
var loc = new LocationVariable(
services.getVariableNamer().getTemporaryNameProposal("x"),
services.getNamespaces().sorts().lookup("boolean"));
TextualJMLMergePointDecl a = n.getData(MarkerStatementHelper.KEY_MERGE_POINT);
return new MergePointStatement(pi, c, a, loc);
}

@Override
Expand All @@ -1861,7 +1858,7 @@ public Object visit(KeyMethodBodyStatement n, Void arg) {
}

@Override
public Object visit(KeyMethodCallStatement n, Void arg) {
public Object visit(KeyMethodCallStmt n, Void arg) {
PositionInfo pi = createPositionInfo(n);
List<Comment> c = createComments(n);
IProgramVariable resultVar = accepto(n.getName());
Expand All @@ -1885,7 +1882,7 @@ private IProgramMethod resolveMethodSignature(KeYJavaType type, KeyMethodSignatu
}

@Override
public Object visit(KeyTransactionStatement n, Void arg) {
public Object visit(KeyTransactionStmt n, Void arg) {
PositionInfo pi = createPositionInfo(n);
List<Comment> c = createComments(n);
return new TransactionStatement(pi, c, n.getType());
Expand Down Expand Up @@ -2190,11 +2187,6 @@ public Object visit(RecordDeclaration n, Void arg) {
public Object visit(CompactConstructorDeclaration n, Void arg) {
return reportUnsupportedElement(n);
}

@Override
public Object visit(KeyRangeExpression n, Void arg) {
return reportUnsupportedElement(n);
}
// endregion

@Override
Expand Down
12 changes: 4 additions & 8 deletions key.core/src/main/java/de/uka/ilkd/key/java/transformations/ConstantExpressionEvaluator.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,6 @@
import com.github.javaparser.ast.expr.*;
import com.github.javaparser.ast.key.KeyEscapeExpression;
import com.github.javaparser.ast.key.KeyPassiveExpression;
import com.github.javaparser.ast.key.KeyRangeExpression;
import com.github.javaparser.ast.key.sv.KeyExpressionSV;
import com.github.javaparser.ast.key.sv.KeyMetaConstructExpression;
import com.github.javaparser.ast.stmt.ExplicitConstructorInvocationStmt;
Expand Down Expand Up @@ -79,7 +78,7 @@ public Expression evaluate(String string) throws EvaluationException {
private static class ConstantExpressionEvaluatorVisitor
extends GenericVisitorAdapter<Object, Void> {

private Queue<FieldDeclaration> path = new LinkedList<FieldDeclaration>();
private final Queue<FieldDeclaration> path = new LinkedList<>();

@Override
public Object visit(ArrayAccessExpr n, Void arg) {
Expand All @@ -106,6 +105,9 @@ public Object visit(BinaryExpr n, Void arg) {
Object left = n.getLeft().accept(this, arg);
Object right = n.getRight().accept(this, arg);
return switch (n.getOperator()) {
case IMPLICATION, ANTIVALENCE, EQUIVALENCE, RIMPLICATION, SUB_LOCKE, SUB_LOCK,
RANGE, SUBTYPE ->
throw new RuntimeException();
case OR -> {
if (left instanceof Boolean && right instanceof Boolean)
yield ((Boolean) left) || (Boolean) right;
Expand Down Expand Up @@ -428,12 +430,6 @@ public Object visit(KeyEscapeExpression n, Void arg) {

}

@Override
public Object visit(KeyRangeExpression n, Void arg) {
throw new RuntimeException("unsupported expression");

}

@Override
public Object visit(KeyExpressionSV n, Void arg) {
throw new RuntimeException("unsupported expression");
Expand Down
34 changes: 13 additions & 21 deletions ...java/de/uka/ilkd/key/java/transformations/pipeline/ConstantStringExpressionEvaluator.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,10 @@
import com.github.javaparser.ast.comments.MarkdownComment;
import com.github.javaparser.ast.comments.TraditionalJavadocComment;
import com.github.javaparser.ast.expr.*;
import com.github.javaparser.ast.jml.doc.JmlDoc;
import com.github.javaparser.ast.jml.doc.JmlDocDeclaration;
import com.github.javaparser.ast.jml.doc.JmlDocStmt;
import com.github.javaparser.ast.jml.doc.JmlDocType;
import com.github.javaparser.ast.key.*;
import com.github.javaparser.ast.key.sv.*;
import com.github.javaparser.ast.modules.ModuleDeclaration;
Expand Down Expand Up @@ -689,7 +693,7 @@ public void visit(KeyCcatchReturn n, Object arg) {
}

@Override
public void visit(KeyCatchAllStatement n, Object arg) {
public void visit(KeyCatchAllStmt n, Object arg) {
super.visit(n, arg);
defaultAction(n, arg);
}
Expand All @@ -701,7 +705,7 @@ public void visit(KeyEscapeExpression n, Object arg) {
}

@Override
public void visit(KeyExecStatement n, Object arg) {
public void visit(KeyExecStmt n, Object arg) {
super.visit(n, arg);
defaultAction(n, arg);
}
Expand All @@ -713,13 +717,13 @@ public void visit(KeyExecutionContext n, Object arg) {
}

@Override
public void visit(KeyLoopScopeBlock n, Object arg) {
public void visit(KeyLoopScopeBlockStmt n, Object arg) {
super.visit(n, arg);
defaultAction(n, arg);
}

@Override
public void visit(KeyMergePointStatement n, Object arg) {
public void visit(KeyMergePointStmt n, Object arg) {
super.visit(n, arg);
defaultAction(n, arg);
}
Expand All @@ -731,7 +735,7 @@ public void visit(KeyMethodBodyStatement n, Object arg) {
}

@Override
public void visit(KeyMethodCallStatement n, Object arg) {
public void visit(KeyMethodCallStmt n, Object arg) {
super.visit(n, arg);
defaultAction(n, arg);
}
Expand All @@ -743,13 +747,7 @@ public void visit(KeyMethodSignature n, Object arg) {
}

@Override
public void visit(KeyRangeExpression n, Object arg) {
super.visit(n, arg);
defaultAction(n, arg);
}

@Override
public void visit(KeyTransactionStatement n, Object arg) {
public void visit(KeyTransactionStmt n, Object arg) {
super.visit(n, arg);
defaultAction(n, arg);
}
Expand Down Expand Up @@ -863,25 +861,19 @@ public void visit(JmlDoc n, Object arg) {
}

@Override
public void visit(JmlDocsBodyDeclaration n, Object arg) {
super.visit(n, arg);
defaultAction(n, arg);
}

@Override
public void visit(JmlDocsTypeDeclaration n, Object arg) {
public void visit(JmlDocDeclaration n, Object arg) {
super.visit(n, arg);
defaultAction(n, arg);
}

@Override
public void visit(JmlDocsStatements n, Object arg) {
public void visit(JmlDocType n, Object arg) {
super.visit(n, arg);
defaultAction(n, arg);
}

@Override
public void visit(KeYMarkerStatement n, Object arg) {
public void visit(JmlDocStmt n, Object arg) {
super.visit(n, arg);
defaultAction(n, arg);
}
Expand Down
Loading
Loading