Skip to content

Commit 41abead

Browse files
wadoonwadoon
committed
adaption for JmlParser (renaming of stuff)
1 parent 2adca9e commit 41abead

11 files changed

Lines changed: 60 additions & 79 deletions

File tree

‎key.core/build.gradle‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -21,10 +21,10 @@ dependencies {
2121

2222
api project(':key.util')
2323

24-
def JP_VERSION = "3.28.0-K13.5"
25-
api "org.key-project.proofjava:javaparser-core:$JP_VERSION"
26-
api "org.key-project.proofjava:javaparser-core-serialization:$JP_VERSION"
27-
api "org.key-project.proofjava:javaparser-symbol-solver-core:$JP_VERSION"
24+
def JP_VERSION = "3.28.0-J8.0-K13.5-SNAPSHOT"
25+
api "io.github.jmltoolkit:jmlparser-core:$JP_VERSION"
26+
api "io.github.jmltoolkit:jmlparser-core-serialization:$JP_VERSION"
27+
api "io.github.jmltoolkit:jmlparser-symbol-solver-core:$JP_VERSION"
2828

2929
testImplementation("com.google.truth:truth:1.4.4")
3030
testImplementation(project(":key.core"))

‎key.core/src/main/java/de/uka/ilkd/key/java/KeYProgModelInfo.java‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -421,7 +421,9 @@ public ClassOrInterfaceType getType(String... names) {
421421
return null;
422422
}
423423
final SymbolReference<ResolvedMethodDeclaration> method = MethodResolutionLogic
424-
.solveMethodInType(rct, name, jpSignature, contextTypeDeclaration.get());
424+
.solveMethodInType(rct, name, jpSignature
425+
//TODO super important , contextTypeDeclaration.get()
426+
);
425427
return method.getDeclaration()
426428
.map(d -> (IProgramMethod) Objects
427429
.requireNonNull(mapping.resolvedDeclarationToKeY(d)))
@@ -688,26 +690,24 @@ private ImmutableList<KeYJavaType> recFindImplementations(
688690
return result;
689691
}
690692

691-
692-
// TODO(weigl): Implemented by @Drodt, no idea if it's correct
693693
private boolean declaresApplicableMethods(ResolvedTypeDeclaration rt, String name,
694694
List<ResolvedType> signature, ResolvedReferenceTypeDeclaration context) {
695695
if (rt instanceof MethodResolutionCapability mrc) {
696-
var method = mrc.solveMethod(name, signature, false, context);
696+
var method = mrc.solveMethod(name, signature, false
697+
//TODO super important: , context
698+
);
697699
return method.isSolved();
698700
}
699701
return false;
700702
}
701703

702-
// TODO(weigl): Implemented by @Drodt, no idea if it's correct
703704
private boolean isDeclaringInterface(
704705
ResolvedTypeDeclaration ct, String name,
705706
List<ResolvedType> signature) {
706707
Debug.assertTrue(ct.isInterface());
707708
var id = ct.asInterface();
708709
var set = id.getDeclaredMethods();
709710
for (var m : set) {
710-
// TODO: check if m is visible for ct
711711
if (name.equals(m.getName())
712712
&& isCompatibleSignature(signature, m.formalParameterTypes()))
713713
return true;

‎key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/TransactionStatement.java‎

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -5,24 +5,23 @@
55

66
import java.util.List;
77

8+
import com.github.javaparser.ast.key.KeyTransactionStmt;
89
import de.uka.ilkd.key.java.*;
910
import de.uka.ilkd.key.java.ast.*;
1011
import de.uka.ilkd.key.java.visitor.Visitor;
1112
import de.uka.ilkd.key.rule.MatchConditions;
1213

13-
import com.github.javaparser.ast.key.KeyTransactionStatement;
14-
1514
public class TransactionStatement extends JavaStatement {
16-
private final KeyTransactionStatement.TransactionType type;
15+
private final KeyTransactionStmt.TransactionType type;
1716

18-
public TransactionStatement(KeyTransactionStatement.TransactionType type) {
17+
public TransactionStatement(KeyTransactionStmt.TransactionType type) {
1918
super();
2019
this.type = type;
2120
}
2221

2322
public TransactionStatement(
2423
PositionInfo pi, List<Comment> c,
25-
KeyTransactionStatement.TransactionType type) {
24+
KeyTransactionStmt.TransactionType type) {
2625
super(pi, c);
2726
this.type = type;
2827
}

‎key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java‎

Lines changed: 7 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -61,6 +61,7 @@
6161
import com.github.javaparser.ast.comments.TraditionalJavadocComment;
6262
import com.github.javaparser.ast.expr.*;
6363
import com.github.javaparser.ast.key.*;
64+
import com.github.javaparser.ast.jml.*;
6465
import com.github.javaparser.ast.key.sv.*;
6566
import com.github.javaparser.ast.modules.*;
6667
import com.github.javaparser.ast.nodeTypes.NodeWithModifiers;
@@ -271,6 +272,7 @@ public Object visit(BinaryExpr n, Void arg) {
271272
case MULTIPLY -> new Times(pi, c, lhs, rhs);
272273
case DIVIDE -> new Divide(pi, c, lhs, rhs);
273274
case REMAINDER -> new Modulo(pi, c, lhs, rhs);
275+
default -> throw new IllegalStateException("Unexpected value: " + n.getOperator());
274276
};
275277
}
276278

@@ -1708,12 +1710,6 @@ public Object visit(KeyCcatchReturn n, Void arg) {
17081710
StatementBlock block = accepto(n.getBlock());
17091711
return new Ccatch(pi, c, null, param, block);
17101712
}
1711-
1712-
@Override
1713-
public Object visit(KeyCatchAllStatement n, Void arg) {
1714-
// TODO
1715-
return reportUnsupportedElement(n);
1716-
}
17171713
// endregion
17181714

17191715
@Override
@@ -1809,7 +1805,7 @@ private ImmutableArray<Expression> map(
18091805
}
18101806

18111807
@Override
1812-
public Object visit(KeyExecStatement n, Void arg) {
1808+
public Object visit(KeyExecStmt n, Void arg) {
18131809
var pi = createPositionInfo(n);
18141810
var c = createComments(n);
18151811
StatementBlock body = accept(n.getExecBlock());
@@ -1833,7 +1829,7 @@ public Object visit(KeyExecutionContext n, Void arg) {
18331829
}
18341830

18351831
@Override
1836-
public Object visit(KeyLoopScopeBlock n, Void arg) {
1832+
public Object visit(KeyLoopScopeBlockStmt n, Void arg) {
18371833
var pi = createPositionInfo(n);
18381834
var c = createComments(n);
18391835
StatementBlock body = accept(n.getBlock());
@@ -1842,7 +1838,7 @@ public Object visit(KeyLoopScopeBlock n, Void arg) {
18421838
}
18431839

18441840
@Override
1845-
public Object visit(KeyMergePointStatement n, Void arg) {
1841+
public Object visit(KeyMergePointStmt n, Void arg) {
18461842
var pi = createPositionInfo(n);
18471843
var c = createComments(n);
18481844
IProgramVariable expr = accept(n.getExpr());
@@ -1869,7 +1865,7 @@ public Object visit(KeyMethodBodyStatement n, Void arg) {
18691865
}
18701866

18711867
@Override
1872-
public Object visit(KeyMethodCallStatement n, Void arg) {
1868+
public Object visit(KeyMethodCallStmt n, Void arg) {
18731869
var pi = createPositionInfo(n);
18741870
var c = createComments(n);
18751871
IProgramVariable resultVar = accepto(n.getName());
@@ -1893,7 +1889,7 @@ private IProgramMethod resolveMethodSignature(KeYJavaType type, KeyMethodSignatu
18931889
}
18941890

18951891
@Override
1896-
public Object visit(KeyTransactionStatement n, Void arg) {
1892+
public Object visit(KeyTransactionStmt n, Void arg) {
18971893
var pi = createPositionInfo(n);
18981894
var c = createComments(n);
18991895
return new TransactionStatement(pi, c, n.getType());
@@ -2197,11 +2193,6 @@ public Object visit(RecordDeclaration n, Void arg) {
21972193
public Object visit(CompactConstructorDeclaration n, Void arg) {
21982194
return reportUnsupportedElement(n);
21992195
}
2200-
2201-
@Override
2202-
public Object visit(KeyRangeExpression n, Void arg) {
2203-
return reportUnsupportedElement(n);
2204-
}
22052196
// endregion
22062197

22072198
@Override

‎key.core/src/main/java/de/uka/ilkd/key/java/transformations/ConstantExpressionEvaluator.java‎

Lines changed: 1 addition & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,6 @@
1111
import com.github.javaparser.ast.expr.*;
1212
import com.github.javaparser.ast.key.KeyEscapeExpression;
1313
import com.github.javaparser.ast.key.KeyPassiveExpression;
14-
import com.github.javaparser.ast.key.KeyRangeExpression;
1514
import com.github.javaparser.ast.key.sv.KeyExpressionSV;
1615
import com.github.javaparser.ast.key.sv.KeyMetaConstructExpression;
1716
import com.github.javaparser.ast.stmt.ExplicitConstructorInvocationStmt;
@@ -193,6 +192,7 @@ public Object visit(BinaryExpr n, Void arg) {
193192
yield ((Integer) left) % (Integer) right;
194193
throw new RuntimeException();
195194
}
195+
default -> throw new IllegalStateException("Unexpected value: " + n.getOperator());
196196
};
197197
}
198198

@@ -428,12 +428,6 @@ public Object visit(KeyEscapeExpression n, Void arg) {
428428

429429
}
430430

431-
@Override
432-
public Object visit(KeyRangeExpression n, Void arg) {
433-
throw new RuntimeException("unsupported expression");
434-
435-
}
436-
437431
@Override
438432
public Object visit(KeyExpressionSV n, Void arg) {
439433
throw new RuntimeException("unsupported expression");

‎key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ConstantStringExpressionEvaluator.java‎

Lines changed: 13 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,10 @@
1818

1919
import java.util.Objects;
2020

21+
import com.github.javaparser.ast.jml.doc.JmlDoc;
22+
import com.github.javaparser.ast.jml.doc.JmlDocDeclaration;
23+
import com.github.javaparser.ast.jml.doc.JmlDocStmt;
24+
import com.github.javaparser.ast.jml.doc.JmlDocType;
2125
import de.uka.ilkd.key.java.transformations.ConstantExpressionEvaluator;
2226
import de.uka.ilkd.key.java.transformations.EvaluationException;
2327

@@ -689,7 +693,7 @@ public void visit(KeyCcatchReturn n, Object arg) {
689693
}
690694

691695
@Override
692-
public void visit(KeyCatchAllStatement n, Object arg) {
696+
public void visit(KeyCatchAllStmt n, Object arg) {
693697
super.visit(n, arg);
694698
defaultAction(n, arg);
695699
}
@@ -701,7 +705,7 @@ public void visit(KeyEscapeExpression n, Object arg) {
701705
}
702706

703707
@Override
704-
public void visit(KeyExecStatement n, Object arg) {
708+
public void visit(KeyExecStmt n, Object arg) {
705709
super.visit(n, arg);
706710
defaultAction(n, arg);
707711
}
@@ -713,13 +717,13 @@ public void visit(KeyExecutionContext n, Object arg) {
713717
}
714718

715719
@Override
716-
public void visit(KeyLoopScopeBlock n, Object arg) {
720+
public void visit(KeyLoopScopeBlockStmt n, Object arg) {
717721
super.visit(n, arg);
718722
defaultAction(n, arg);
719723
}
720724

721725
@Override
722-
public void visit(KeyMergePointStatement n, Object arg) {
726+
public void visit(KeyMergePointStmt n, Object arg) {
723727
super.visit(n, arg);
724728
defaultAction(n, arg);
725729
}
@@ -731,7 +735,7 @@ public void visit(KeyMethodBodyStatement n, Object arg) {
731735
}
732736

733737
@Override
734-
public void visit(KeyMethodCallStatement n, Object arg) {
738+
public void visit(KeyMethodCallStmt n, Object arg) {
735739
super.visit(n, arg);
736740
defaultAction(n, arg);
737741
}
@@ -743,13 +747,7 @@ public void visit(KeyMethodSignature n, Object arg) {
743747
}
744748

745749
@Override
746-
public void visit(KeyRangeExpression n, Object arg) {
747-
super.visit(n, arg);
748-
defaultAction(n, arg);
749-
}
750-
751-
@Override
752-
public void visit(KeyTransactionStatement n, Object arg) {
750+
public void visit(KeyTransactionStmt n, Object arg) {
753751
super.visit(n, arg);
754752
defaultAction(n, arg);
755753
}
@@ -863,19 +861,19 @@ public void visit(JmlDoc n, Object arg) {
863861
}
864862

865863
@Override
866-
public void visit(JmlDocsBodyDeclaration n, Object arg) {
864+
public void visit(JmlDocDeclaration n, Object arg) {
867865
super.visit(n, arg);
868866
defaultAction(n, arg);
869867
}
870868

871869
@Override
872-
public void visit(JmlDocsTypeDeclaration n, Object arg) {
870+
public void visit(JmlDocType n, Object arg) {
873871
super.visit(n, arg);
874872
defaultAction(n, arg);
875873
}
876874

877875
@Override
878-
public void visit(JmlDocsStatements n, Object arg) {
876+
public void visit(JmlDocStmt n, Object arg) {
879877
super.visit(n, arg);
880878
defaultAction(n, arg);
881879
}

‎key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JMLTransformer.java‎

Lines changed: 12 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@
77
import java.util.*;
88
import java.util.regex.Pattern;
99

10+
import com.github.javaparser.ast.jml.doc.*;
1011
import de.uka.ilkd.key.java.ConvertException;
1112
import de.uka.ilkd.key.nparser.KeyAst;
1213
import de.uka.ilkd.key.parser.Location;
@@ -275,8 +276,8 @@ private void transformClassLevelComments(TypeDeclaration<?> td) throws SLTransla
275276

276277
for (BodyDeclaration<?> member : members) {
277278
// JMLDocsBodyDeclaration: JML comments inside a class/interface/... body
278-
if (member instanceof JmlDocsBodyDeclaration bd) {
279-
String concatenatedComment = sanitizer.asString(bd.jmlDocs());
279+
if (member instanceof JmlDocDeclaration bd) {
280+
String concatenatedComment = sanitizer.asString(bd.jmlComments());
280281

281282
// The preparser split along the grammar rules in KeYParser.g4, and gives you a list
282283
// of JML entities.
@@ -431,7 +432,7 @@ private void transformMethodLevelCommentsAt(BlockStmt blockStmt, URI fileName)
431432
while (stmt instanceof LabeledStmt labeledStmt) {
432433
var inner = labeledStmt.getStatement();
433434

434-
if (inner instanceof JmlDocsStatements) {
435+
if (inner instanceof JmlDocStmt) {
435436
throw new SLTranslationException(
436437
("Here is something wrong. Your label '%s' is glued to a " +
437438
"JML annotation instead of a Java statement. Please consider the use of braces")
@@ -458,8 +459,8 @@ private void transformMethodLevelCommentsAt(BlockStmt blockStmt, URI fileName)
458459
}
459460
} else if (stmt instanceof NodeWithBody<?> b && b.getBody().isBlockStmt()) {
460461
transformMethodLevelCommentsAt(b.getBody().asBlockStmt(), fileName);
461-
} else if (stmt instanceof JmlDocsStatements doc) {
462-
String concat = sanitizer.asString(doc.getJmlDocs());
462+
} else if (stmt instanceof JmlDocStmt doc) {
463+
String concat = sanitizer.asString(doc.jmlComments());
463464
ImmutableList<TextualJMLConstruct> constructs =
464465
io.parseMethodLevel(concat, fileName, pos);
465466
services.addWarnings(io.getWarnings());
@@ -542,10 +543,10 @@ public void apply(@NonNull CompilationUnit cu) {
542543
final var types = new ArrayList<>(cu.getTypes());
543544
ImmutableList<JMLModifier> modifiers = null;
544545
for (TypeDeclaration<?> td : types) {
545-
if (td instanceof JmlDocsTypeDeclaration jdtd) {
546+
if (td instanceof JmlDocType jdtd) {
546547
// Currently, we only support modifier at type declaration level.
547548
// Other things would be ghost classes or model imports.
548-
var input = sanitizer.asString(jdtd.jmlDocs());
549+
var input = sanitizer.asString(jdtd.jmlComments());
549550
PreParser pp = getPreParser();
550551
modifiers = pp.parseModifiers(input);
551552
} else {
@@ -584,7 +585,7 @@ private void transformModifiers(NodeWithModifiers<?> hasMods) {
584585
for (Modifier mod : hasMods.getModifiers()) {
585586
var kw = mod.getKeyword();
586587
if (kw instanceof JmlDocModifier jdm) {
587-
var modifiers = sanitizer.asString(jdm.getJmlDocs());
588+
var modifiers = sanitizer.asString(jdm.getJmlComments());
588589
var jmlMods = pp.parseModifiers(modifiers);
589590
for (var jmlMod : jmlMods) {
590591
hasMods.addModifier(jmlMod.getParserKeyword());
@@ -636,7 +637,9 @@ public String asString(Collection<Token> jmlDocs, boolean emulateGlobalPosition)
636637
}
637638

638639
public String asString(NodeList<JmlDoc> jmlDocs, boolean emulateGlobalPosition) {
639-
return asStringJT(jmlDocs.stream().map(JmlDoc::getContent).toList(), emulateGlobalPosition);
640+
return asStringJT(jmlDocs.stream()
641+
.map(it -> it.getTokenRange()
642+
.map(TokenRange::getBegin).orElse(null)).toList(), emulateGlobalPosition);
640643
}
641644

642645
public String toSanitizedString(StringBuilder s) {

‎key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JmlDocRemoval.java‎

Lines changed: 4 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -5,10 +5,7 @@
55

66
import com.github.javaparser.ast.CompilationUnit;
77
import com.github.javaparser.ast.Modifier;
8-
import com.github.javaparser.ast.key.JmlDocModifier;
9-
import com.github.javaparser.ast.key.JmlDocsBodyDeclaration;
10-
import com.github.javaparser.ast.key.JmlDocsStatements;
11-
import com.github.javaparser.ast.key.JmlDocsTypeDeclaration;
8+
import com.github.javaparser.ast.jml.doc.*;
129
import org.jspecify.annotations.NonNull;
1310

1411
/**
@@ -30,9 +27,9 @@ public void apply(CompilationUnit cu) {
3027
}
3128
}
3229

33-
if (it instanceof JmlDocsStatements ||
34-
it instanceof JmlDocsTypeDeclaration ||
35-
it instanceof JmlDocsBodyDeclaration) {
30+
if (it instanceof JmlDocStmt ||
31+
it instanceof JmlDocType ||
32+
it instanceof JmlDocDeclaration) {
3633
it.remove();
3734
}
3835
});

0 commit comments

Comments
 (0)