diff --git a/key.core/build.gradle b/key.core/build.gradle index 69a6d954e8e..9464a810246 100644 --- a/key.core/build.gradle +++ b/key.core/build.gradle @@ -21,10 +21,10 @@ dependencies { api project(':key.util') - def JP_VERSION = "3.28.0-K13.5" - api "org.key-project.proofjava:javaparser-core:$JP_VERSION" - api "org.key-project.proofjava:javaparser-core-serialization:$JP_VERSION" - api "org.key-project.proofjava:javaparser-symbol-solver-core:$JP_VERSION" + def JP_VERSION = "3.28.0-J8.0-K13.5-SNAPSHOT" + api "io.github.jmltoolkit:jmlparser-core:$JP_VERSION" + api "io.github.jmltoolkit:jmlparser-core-serialization:$JP_VERSION" + api "io.github.jmltoolkit:jmlparser-symbol-solver-core:$JP_VERSION" testImplementation("com.google.truth:truth:1.4.4") testImplementation(project(":key.core")) diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/KeYProgModelInfo.java b/key.core/src/main/java/de/uka/ilkd/key/java/KeYProgModelInfo.java index a0342b15026..ca2d623ad9c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/KeYProgModelInfo.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/KeYProgModelInfo.java @@ -421,7 +421,9 @@ public ClassOrInterfaceType getType(String... names) { return null; } final SymbolReference method = MethodResolutionLogic - .solveMethodInType(rct, name, jpSignature, contextTypeDeclaration.get()); + .solveMethodInType(rct, name, jpSignature + //TODO super important , contextTypeDeclaration.get() + ); return method.getDeclaration() .map(d -> (IProgramMethod) Objects .requireNonNull(mapping.resolvedDeclarationToKeY(d))) @@ -688,18 +690,17 @@ private ImmutableList recFindImplementations( return result; } - - // TODO(weigl): Implemented by @Drodt, no idea if it's correct private boolean declaresApplicableMethods(ResolvedTypeDeclaration rt, String name, List signature, ResolvedReferenceTypeDeclaration context) { if (rt instanceof MethodResolutionCapability mrc) { - var method = mrc.solveMethod(name, signature, false, context); + var method = mrc.solveMethod(name, signature, false + //TODO super important: , context + ); return method.isSolved(); } return false; } - // TODO(weigl): Implemented by @Drodt, no idea if it's correct private boolean isDeclaringInterface( ResolvedTypeDeclaration ct, String name, List signature) { @@ -707,7 +708,6 @@ private boolean isDeclaringInterface( var id = ct.asInterface(); var set = id.getDeclaredMethods(); for (var m : set) { - // TODO: check if m is visible for ct if (name.equals(m.getName()) && isCompatibleSignature(signature, m.formalParameterTypes())) return true; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/ProgramElement.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/ProgramElement.java index fa6d0ef6242..bd7f88bc208 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/ProgramElement.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/ProgramElement.java @@ -4,8 +4,8 @@ package de.uka.ilkd.key.java.ast; +import com.github.javaparser.ast.jml.clauses.JmlContract; import de.uka.ilkd.key.rule.MatchConditions; -import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; @@ -26,12 +26,6 @@ public interface ProgramElement extends SourceElement, ModelElement { */ Comment[] getComments(); - /// - default ImmutableList getAttachedJml() { - return ImmutableSLList.nil(); - } - - /** * matches the source "text" (@link SourceData#getSource()) against the pattern represented by * this object. In case of a successful match the resulting {@link MatchConditions} with the diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/StatementBlock.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/StatementBlock.java index bf47856cf72..b084f141640 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/StatementBlock.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/StatementBlock.java @@ -16,7 +16,6 @@ import de.uka.ilkd.key.java.visitor.Visitor; import de.uka.ilkd.key.logic.PosInProgram; import de.uka.ilkd.key.logic.ProgramPrefix; -import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct; import de.uka.ilkd.key.util.Debug; import org.key_project.util.ExtList; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/ClassDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/ClassDeclaration.java index 90124b65d2e..113e74245f5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/ClassDeclaration.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/ClassDeclaration.java @@ -12,7 +12,6 @@ import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; import de.uka.ilkd.key.java.visitor.Visitor; import de.uka.ilkd.key.logic.ProgramElementName; -import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct; import org.key_project.util.ExtList; import org.key_project.util.collection.ImmutableArray; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/ConstructorDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/ConstructorDeclaration.java index 2c06b4cec0f..8d2a8187034 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/ConstructorDeclaration.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/ConstructorDeclaration.java @@ -5,6 +5,7 @@ import java.util.List; +import com.github.javaparser.ast.jml.clauses.JmlContract; import de.uka.ilkd.key.java.ast.Comment; import de.uka.ilkd.key.java.ast.PositionInfo; import de.uka.ilkd.key.java.ast.StatementBlock; @@ -12,7 +13,6 @@ import de.uka.ilkd.key.java.ast.reference.TypeReference; import de.uka.ilkd.key.java.visitor.Visitor; import de.uka.ilkd.key.logic.ProgramElementName; -import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct; import org.key_project.util.ExtList; import org.key_project.util.collection.ImmutableArray; @@ -63,7 +63,7 @@ public ConstructorDeclaration(PositionInfo pi, List c, ImmutableArray map1, Throws exceptions, StatementBlock body, boolean parentIsInterfaceDeclaration, - List specs) { + List specs) { super(pi, c, map, o, comments, name, map1, exceptions, body, parentIsInterfaceDeclaration, ImmutableList.fromList(specs)); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/InterfaceDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/InterfaceDeclaration.java index 55e5c8e44b0..29aaea8c7ca 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/InterfaceDeclaration.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/InterfaceDeclaration.java @@ -24,7 +24,6 @@ import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; import de.uka.ilkd.key.java.visitor.Visitor; import de.uka.ilkd.key.logic.ProgramElementName; -import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct; import org.key_project.util.ExtList; import org.key_project.util.collection.ImmutableArray; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/JavaDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/JavaDeclaration.java index e779e9c26e6..8c6e793266d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/JavaDeclaration.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/JavaDeclaration.java @@ -18,12 +18,12 @@ import java.util.List; +import com.github.javaparser.ast.jml.clauses.JmlContract; import de.uka.ilkd.key.java.ast.Comment; import de.uka.ilkd.key.java.ast.Declaration; import de.uka.ilkd.key.java.ast.JavaNonTerminalProgramElement; import de.uka.ilkd.key.java.ast.PositionInfo; import de.uka.ilkd.key.java.ast.declaration.modifier.*; -import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct; import org.key_project.util.ExtList; import org.key_project.util.collection.ImmutableArray; @@ -39,7 +39,7 @@ public abstract class JavaDeclaration extends JavaNonTerminalProgramElement implements Declaration { - protected final ImmutableList attachedJml; + protected final ImmutableList attachedJml; /** @@ -53,7 +53,7 @@ public abstract class JavaDeclaration extends JavaNonTerminalProgramElement impl public JavaDeclaration(PositionInfo pi, List comments, @NonNull ImmutableArray modArray, - ImmutableList attachedJml) { + ImmutableList attachedJml) { super(pi, comments); this.modArray = modArray; this.attachedJml = attachedJml; @@ -89,7 +89,7 @@ public JavaDeclaration(ExtList children) { super(children); modArray = new ImmutableArray<>(children.collect(Modifier.class)); this.attachedJml = - ImmutableList.fromList(List.of(children.collect(TextualJMLConstruct.class))); + ImmutableList.fromList(List.of(children.collect(JmlContract.class))); } @@ -115,7 +115,7 @@ public VisibilityModifier getVisibilityModifier() { @Override - public ImmutableList getAttachedJml() { + public ImmutableList getAttachedJml() { return attachedJml; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/MethodDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/MethodDeclaration.java index a4337f93c26..a608793dab4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/MethodDeclaration.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/MethodDeclaration.java @@ -5,6 +5,7 @@ import java.util.List; +import com.github.javaparser.ast.jml.clauses.JmlContract; import de.uka.ilkd.key.java.ast.*; import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; import de.uka.ilkd.key.java.ast.abstraction.Method; @@ -13,7 +14,6 @@ import de.uka.ilkd.key.java.visitor.Visitor; import de.uka.ilkd.key.logic.ProgramElementName; import de.uka.ilkd.key.speclang.jml.JMLInfoExtractor; -import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct; import de.uka.ilkd.key.speclang.njml.SpecMathMode; import org.key_project.util.ExtList; @@ -94,7 +94,7 @@ public MethodDeclaration( Comment[] voidComments, ProgramElementName name, ImmutableArray parameters, Throws exceptions, StatementBlock body, boolean parentIsInterfaceDeclaration, - ImmutableList attachedJml) { + ImmutableList attachedJml) { super(pi, comments, modArray, attachedJml); this.returnType = returnType; this.voidComments = voidComments; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/TypeDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/TypeDeclaration.java index 56b7eb8c87b..0cd3f337310 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/TypeDeclaration.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/TypeDeclaration.java @@ -12,7 +12,6 @@ import de.uka.ilkd.key.java.ast.expression.literal.NullLiteral; import de.uka.ilkd.key.logic.ProgramElementName; import de.uka.ilkd.key.speclang.jml.JMLInfoExtractor; -import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct; import de.uka.ilkd.key.speclang.njml.SpecMathMode; import org.key_project.util.ExtList; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Do.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Do.java index dccf026f5a7..bf73faf59bb 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Do.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Do.java @@ -8,7 +8,6 @@ import de.uka.ilkd.key.java.ast.*; import de.uka.ilkd.key.java.ast.expression.Expression; import de.uka.ilkd.key.java.visitor.Visitor; -import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct; import org.key_project.util.ExtList; import org.key_project.util.collection.ImmutableList; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/EnhancedFor.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/EnhancedFor.java index f5235a72f21..85285f3443c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/EnhancedFor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/EnhancedFor.java @@ -9,7 +9,6 @@ import de.uka.ilkd.key.java.ast.declaration.LocalVariableDeclaration; import de.uka.ilkd.key.java.visitor.CreatingASTVisitor; import de.uka.ilkd.key.java.visitor.Visitor; -import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct; import org.key_project.util.ExtList; import org.key_project.util.collection.ImmutableList; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/For.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/For.java index bda9f070b2c..c13daf20b6d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/For.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/For.java @@ -10,7 +10,6 @@ import de.uka.ilkd.key.java.ast.declaration.VariableSpecification; import de.uka.ilkd.key.java.ast.expression.Expression; import de.uka.ilkd.key.java.visitor.Visitor; -import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct; import org.key_project.util.ExtList; import org.key_project.util.collection.ImmutableArray; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/JmlAssert.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/JmlAssert.java index dd5c3a67f0a..504ef0c3c33 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/JmlAssert.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/JmlAssert.java @@ -9,7 +9,6 @@ import de.uka.ilkd.key.java.ast.ProgramElement; import de.uka.ilkd.key.java.visitor.Visitor; import de.uka.ilkd.key.nparser.KeyAst; -import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLAssertStatement; import org.key_project.util.ExtList; @@ -27,7 +26,7 @@ public class JmlAssert extends JavaStatement { /** * the kind of the statement, assert or assume */ - private final TextualJMLAssertStatement.Kind kind; + private final Kind kind; /** * the condition in parse tree form @@ -42,7 +41,7 @@ public class JmlAssert extends JavaStatement { * @param positionInfo * the position information for this statement */ - public JmlAssert(TextualJMLAssertStatement.Kind kind, KeyAst.Expression condition, + public JmlAssert(Kind kind, KeyAst.Expression condition, PositionInfo positionInfo) { super(positionInfo); this.kind = kind; @@ -55,7 +54,7 @@ public JmlAssert(TextualJMLAssertStatement.Kind kind, KeyAst.Expression conditio */ public JmlAssert(ExtList children) { super(children); - this.kind = Objects.requireNonNull(children.get(TextualJMLAssertStatement.Kind.class)); + this.kind = Objects.requireNonNull(children.get(Kind.class)); this.condition = Objects.requireNonNull(children.get(KeyAst.Expression.class)); } @@ -63,7 +62,7 @@ public JmlAssert(JmlAssert other) { this(other.kind, other.condition, other.getPositionInfo()); } - public TextualJMLAssertStatement.Kind getKind() { + public Kind getKind() { return kind; } @@ -166,4 +165,19 @@ public ProgramElement getChildAt(int index) { public void visit(Visitor v) { v.performActionOnJmlAssert(this); } + + public enum Kind { + ASSERT("assert"), ASSUME("assume"); + + private final String name; + + Kind(String name) { + this.name = name; + } + + @Override + public String toString() { + return name; + } + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/LoopStatement.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/LoopStatement.java index be33875ad4d..1c1a7b12566 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/LoopStatement.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/LoopStatement.java @@ -8,7 +8,6 @@ import de.uka.ilkd.key.java.*; import de.uka.ilkd.key.java.ast.*; import de.uka.ilkd.key.java.ast.expression.Expression; -import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct; import org.key_project.util.ExtList; import org.key_project.util.collection.ImmutableArray; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/MergePointStatement.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/MergePointStatement.java index f0b3a8ce6a0..f030b54dbcd 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/MergePointStatement.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/MergePointStatement.java @@ -23,8 +23,6 @@ import de.uka.ilkd.key.java.ast.expression.Expression; import de.uka.ilkd.key.java.visitor.Visitor; import de.uka.ilkd.key.logic.op.IProgramVariable; -import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct; -import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLMergePointDecl; import org.key_project.util.ExtList; import org.key_project.util.collection.ImmutableList; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/TransactionStatement.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/TransactionStatement.java index beb6fa277e1..16acd245286 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/TransactionStatement.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/TransactionStatement.java @@ -5,24 +5,23 @@ import java.util.List; +import com.github.javaparser.ast.key.KeyTransactionStmt; import de.uka.ilkd.key.java.*; import de.uka.ilkd.key.java.ast.*; import de.uka.ilkd.key.java.visitor.Visitor; import de.uka.ilkd.key.rule.MatchConditions; -import com.github.javaparser.ast.key.KeyTransactionStatement; - 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 c, - KeyTransactionStatement.TransactionType type) { + KeyTransactionStmt.TransactionType type) { super(pi, c); this.type = type; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/While.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/While.java index 0262e9d3943..e238a1b9e6d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/While.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/While.java @@ -8,7 +8,6 @@ import de.uka.ilkd.key.java.ast.*; import de.uka.ilkd.key.java.ast.expression.Expression; import de.uka.ilkd.key.java.visitor.Visitor; -import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct; import org.key_project.util.ExtList; import org.key_project.util.collection.ImmutableList; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java b/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java index b2985ea025e..7374582afbc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java @@ -8,6 +8,7 @@ import java.util.function.Predicate; import java.util.stream.Collectors; +import com.github.javaparser.ast.jml.stmt.JmlExpressionStmt; import de.uka.ilkd.key.java.*; import de.uka.ilkd.key.java.ast.*; import de.uka.ilkd.key.java.ast.CompilationUnit; @@ -29,7 +30,6 @@ import de.uka.ilkd.key.java.transformations.ConstantExpressionEvaluator; import de.uka.ilkd.key.java.transformations.EvaluationException; import de.uka.ilkd.key.java.transformations.MarkerStatementHelper; -import de.uka.ilkd.key.java.transformations.pipeline.JMLTransformer; import de.uka.ilkd.key.ldt.HeapLDT; import de.uka.ilkd.key.ldt.JavaDLTheory; import de.uka.ilkd.key.logic.ProgramElementName; @@ -39,10 +39,6 @@ import de.uka.ilkd.key.parser.Location; import de.uka.ilkd.key.parser.ParserException; import de.uka.ilkd.key.rule.metaconstruct.*; -import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLAssertStatement; -import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct; -import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLLoopSpec; -import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLMergePointDecl; import org.key_project.logic.Namespace; import org.key_project.logic.op.Function; @@ -269,6 +265,7 @@ public Object visit(BinaryExpr n, Void arg) { case MULTIPLY -> new Times(pi, c, lhs, rhs); case DIVIDE -> new Divide(pi, c, lhs, rhs); case REMAINDER -> new Modulo(pi, c, lhs, rhs); + default -> throw new IllegalStateException("Unexpected value: " + n.getOperator()); }; } @@ -746,24 +743,41 @@ private ClassOrInterfaceDeclaration getContainingClass(Node node) { return null; } + @Override + public Object visit(JmlExpressionStmt n, Void arg) { + var pi = createPositionInfo(n); + switch (n.getKind()) { + case ASSUME, ASSUME_REDUNDANTLY-> { + var construct = n.getData(MarkerStatementHelper.KEY_EXPR); + yield new JmlAssert(JmlAssert.Kind.ASSERT, construct, pi); + } + case ASSERT, ASSERT_REDUNDANTLY -> { + var construct = n.getData(MarkerStatementHelper.KEY_EXPR); + yield new JmlAssert(JmlAssert.Kind.ASSUME, construct, pi); + } + case SET -> { + var context = n.getData(MarkerStatementHelper.KEY_ASSIGN); + yield new SetStatement(context, pi); + } + } + } + @Override public Object visit(KeYMarkerStatement n, Void arg) { var pi = createPositionInfo(n); return switch (n.getKind()) { case MarkerStatementHelper.KIND_ASSERT -> { var construct = n.getData(MarkerStatementHelper.KEY_EXPR); - yield new JmlAssert(TextualJMLAssertStatement.Kind.ASSERT, construct, pi); + yield new JmlAssert(JmlAssert.Kind.ASSERT, construct, pi); } case MarkerStatementHelper.KIND_ASSUME -> { var construct = n.getData(MarkerStatementHelper.KEY_EXPR); - yield new JmlAssert(TextualJMLAssertStatement.Kind.ASSUME, construct, pi); + yield new JmlAssert(JmlAssert.Kind.ASSUME, construct, pi); } case MarkerStatementHelper.KIND_SET -> { var context = n.getData(MarkerStatementHelper.KEY_ASSIGN); yield new SetStatement(context, pi); } - - case MarkerStatementHelper.KIND_MERGE_POINT -> { var loc = new LocationVariable( services.getVariableNamer().getTemporaryNameProposal("x"), @@ -1706,12 +1720,6 @@ public Object visit(KeyCcatchReturn n, Void arg) { StatementBlock block = accepto(n.getBlock()); return new Ccatch(pi, c, null, param, block); } - - @Override - public Object visit(KeyCatchAllStatement n, Void arg) { - // TODO - return reportUnsupportedElement(n); - } // endregion @Override @@ -1807,7 +1815,7 @@ private ImmutableArray map( } @Override - public Object visit(KeyExecStatement n, Void arg) { + public Object visit(KeyExecStmt n, Void arg) { var pi = createPositionInfo(n); var c = createComments(n); StatementBlock body = accept(n.getExecBlock()); @@ -1831,7 +1839,7 @@ public Object visit(KeyExecutionContext n, Void arg) { } @Override - public Object visit(KeyLoopScopeBlock n, Void arg) { + public Object visit(KeyLoopScopeBlockStmt n, Void arg) { var pi = createPositionInfo(n); var c = createComments(n); StatementBlock body = accept(n.getBlock()); @@ -1840,7 +1848,7 @@ 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); var c = createComments(n); IProgramVariable expr = accept(n.getExpr()); @@ -1867,7 +1875,7 @@ public Object visit(KeyMethodBodyStatement n, Void arg) { } @Override - public Object visit(KeyMethodCallStatement n, Void arg) { + public Object visit(KeyMethodCallStmt n, Void arg) { var pi = createPositionInfo(n); var c = createComments(n); IProgramVariable resultVar = accepto(n.getName()); @@ -1891,7 +1899,7 @@ private IProgramMethod resolveMethodSignature(KeYJavaType type, KeyMethodSignatu } @Override - public Object visit(KeyTransactionStatement n, Void arg) { + public Object visit(KeyTransactionStmt n, Void arg) { var pi = createPositionInfo(n); var c = createComments(n); return new TransactionStatement(pi, c, n.getType()); @@ -2195,11 +2203,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 diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/loader/JavaParserFactory.java b/key.core/src/main/java/de/uka/ilkd/key/java/loader/JavaParserFactory.java index 9b8389596eb..f39aada0a0b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/loader/JavaParserFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/loader/JavaParserFactory.java @@ -4,10 +4,7 @@ package de.uka.ilkd.key.java.loader; import java.io.Reader; -import java.util.ArrayList; -import java.util.Collection; -import java.util.List; -import java.util.Optional; +import java.util.*; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.ast.ResolvedLogicalType; @@ -95,7 +92,11 @@ private ParserConfiguration getConfiguration() { if (config == null) { config = new ParserConfiguration(); config.setStoreTokens(true); + config.setKeepJmlDocs(false); + config.setProcessJml(true); } + // TODO update the activated JML keys with the current settings. + config.setJmlKeys(Collections.singletonList(Collections.singletonList("key"))); config.setLanguageLevel(ParserConfiguration.LanguageLevel.RAW); config.setSymbolResolver(getSymbolSolver()); return config; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/ConstantExpressionEvaluator.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/ConstantExpressionEvaluator.java index f30cedc7188..dd24fd1dc56 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/ConstantExpressionEvaluator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/ConstantExpressionEvaluator.java @@ -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; @@ -193,6 +192,7 @@ public Object visit(BinaryExpr n, Void arg) { yield ((Integer) left) % (Integer) right; throw new RuntimeException(); } + default -> throw new IllegalStateException("Unexpected value: " + n.getOperator()); }; } @@ -428,12 +428,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"); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/KeYJavaPipeline.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/KeYJavaPipeline.java index da9dff5027c..382858dadf5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/KeYJavaPipeline.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/KeYJavaPipeline.java @@ -39,8 +39,8 @@ public List getSteps() { public static KeYJavaPipeline createDefault(TransformationPipelineServices pipelineServices) { KeYJavaPipeline p = new KeYJavaPipeline(pipelineServices); p.add(new EnumClassBuilder(pipelineServices)); - p.add(new JMLTransformer(pipelineServices)); - p.add(new JmlDocRemoval(pipelineServices)); + //p.add(new JMLTransformer(pipelineServices)); + //p.add(new JmlDocRemoval(pipelineServices)); p.add(new ImplicitFieldAdder(pipelineServices)); p.add(new InstanceAllocationMethodBuilder(pipelineServices)); p.add(new ConstructorNormalformBuilder(pipelineServices)); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/MarkerStatementHelper.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/MarkerStatementHelper.java index 187cc4c4b29..26579acd5a7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/MarkerStatementHelper.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/MarkerStatementHelper.java @@ -4,7 +4,6 @@ package de.uka.ilkd.key.java.transformations; import de.uka.ilkd.key.nparser.KeyAst; -import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLMergePointDecl; import com.github.javaparser.ast.DataKey; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ConstantStringExpressionEvaluator.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ConstantStringExpressionEvaluator.java index e81be4b6201..6c94db8b1ec 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ConstantStringExpressionEvaluator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ConstantStringExpressionEvaluator.java @@ -18,6 +18,10 @@ import java.util.Objects; +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 de.uka.ilkd.key.java.transformations.ConstantExpressionEvaluator; import de.uka.ilkd.key.java.transformations.EvaluationException; @@ -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); } @@ -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); } @@ -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); } @@ -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); } @@ -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); } @@ -863,19 +861,19 @@ public void visit(JmlDoc n, Object arg) { } @Override - public void visit(JmlDocsBodyDeclaration n, Object arg) { + public void visit(JmlDocDeclaration n, Object arg) { super.visit(n, arg); defaultAction(n, arg); } @Override - public void visit(JmlDocsTypeDeclaration n, Object arg) { + public void visit(JmlDocType n, Object arg) { super.visit(n, arg); defaultAction(n, arg); } @Override - public void visit(JmlDocsStatements n, Object arg) { + public void visit(JmlDocStmt n, Object arg) { super.visit(n, arg); defaultAction(n, arg); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JMLTransformer.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JMLTransformer.java deleted file mode 100644 index c24de23403f..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JMLTransformer.java +++ /dev/null @@ -1,834 +0,0 @@ -/* This file is part of KeY - https://key-project.org - * KeY is licensed under the GNU General Public License Version 2 - * SPDX-License-Identifier: GPL-2.0-only */ -package de.uka.ilkd.key.java.transformations.pipeline; - -import java.net.URI; -import java.util.*; -import java.util.regex.Pattern; - -import de.uka.ilkd.key.java.ConvertException; -import de.uka.ilkd.key.nparser.KeyAst; -import de.uka.ilkd.key.parser.Location; -import de.uka.ilkd.key.settings.ProofIndependentSettings; -import de.uka.ilkd.key.speclang.PositionedString; -import de.uka.ilkd.key.speclang.jml.pretranslation.*; -import de.uka.ilkd.key.speclang.njml.PreParser; -import de.uka.ilkd.key.speclang.translation.SLTranslationException; -import de.uka.ilkd.key.util.parsing.BuildingException; - -import org.key_project.util.collection.ImmutableList; - -import com.github.javaparser.*; -import com.github.javaparser.ast.*; -import com.github.javaparser.ast.body.*; -import com.github.javaparser.ast.expr.VariableDeclarationExpr; -import com.github.javaparser.ast.key.*; -import com.github.javaparser.ast.nodeTypes.NodeWithBody; -import com.github.javaparser.ast.nodeTypes.NodeWithModifiers; -import com.github.javaparser.ast.nodeTypes.NodeWithOptionalBlockStmt; -import com.github.javaparser.ast.nodeTypes.NodeWithParameters; -import com.github.javaparser.ast.stmt.*; -import com.github.javaparser.ast.type.Type; -import com.google.common.base.Strings; -import org.jspecify.annotations.NonNull; -import org.jspecify.annotations.Nullable; -import org.slf4j.Logger; -import org.slf4j.LoggerFactory; - -import static de.uka.ilkd.key.java.transformations.MarkerStatementHelper.*; - -/// JMLTransformer translates the JML annotation comments into parse trees that are attached -/// to the Java AST nodes. -/// This class handles JML annotations at three different levels: -/// -/// * Type level / Compilation Unit -/// -/// Currently, the support is limited for JML modifiers on classes -/// -/// * Class level / Body Declarations -/// -/// On this level, type-internal declaration can appear like class invariants, -/// model methods and ghost fields. But also modifiers are captured -/// -/// * Method level / Statements -/// -/// Support for ghost statements. -/// -/// After execution this {@link JavaTransformer}, contracts are attached to -/// {@link MethodDeclaration}, or {@link BlockStmt}, {@link FieldDeclaration} and -/// {@link MethodDeclaration} were introduced for ghost and model declarations, -/// JML statements (assume, assert, ...) are inserted into the bodies using -/// {@link KeYMarkerStatement}. -/// -/// You can access attached JML information using the {@link DataKey} in -/// [JMLTransformer#KEY_SPEC_CASE], -/// [JMLTransformer#KEY_SPEC_CASE], and [JMLTransformer#KEY_SPEC_CASE]. -/// -/// JMLModifier are reduced to *normal* modifier of -/// {@link com.github.javaparser.ast.Modifier.DefaultKeyword}. -/// -/// @author weigl -/// @author drodt -/// @author lanzinger -/// @author bubel -/// @author pfeifer -/// @author ulbrich -@SuppressWarnings("OptionalGetWithoutIsPresent") -public final class JMLTransformer extends JavaTransformer { - public static final EnumSet JAVA_MODS = - EnumSet.of(JMLModifier.ABSTRACT, JMLModifier.FINAL, JMLModifier.PRIVATE, - JMLModifier.PROTECTED, JMLModifier.PUBLIC, JMLModifier.STATIC); - - private static final Logger LOGGER = LoggerFactory.getLogger(JMLTransformer.class); - - private final JmlDocSanitizer sanitizer = new JmlDocSanitizer( - ProofIndependentSettings.DEFAULT_INSTANCE.getGeneralSettings().getJmlEnabledKeys()); - - /// KEY for contracts - public static final DataKey> KEY_SPEC_CASE = new DataKey<>() { - }; - /// KEY for class level specification - public static final DataKey> KEY_CLASS_SPEC = new DataKey<>() { - }; - - /// KEY for loop specifications - public static final DataKey> KEY_LOOP_SPEC = new DataKey<>() { - }; - - - /** - * Creates a transformation that adds JML specific elements, for example - * ghost fields and model method declarations. - * - * @param services the CrossReferenceServiceConfiguration to access model - * information - */ - public JMLTransformer(TransformationPipelineServices services) { - super(services); - } - - /** - * Transform the given ghost or model field declaration into a "real" field declaration, and - * attach modifiers. - * - * @param decl the given textual model/ghost field declaration - * @return the newly created FieldDeclaration - * @throws SLTranslationException - */ - private @NonNull FieldDeclaration transformClassFieldDecl(TextualJMLFieldDecl decl) - throws SLTranslationException { - NodeList modifiers = new NodeList<>(); - for (JMLModifier m : decl.getModifiers()) { - Modifier mod = new Modifier(m.getParserKeyword()); - modifiers.add(mod); - } - - final var dims = decl.getDecl().typespec().dims(); - - // for cases like `int[] a[]`, which are allowed in Java (a is 2d here) - int arrayDims = - (dims != null ? dims.LBRACKET().size() : 0) + decl.getDecl().LBRACKET().size(); - Type type = StaticJavaParser.parseType( - decl.getDecl().typespec().type().getText() + Strings.repeat("[]", arrayDims)); - String name = decl.getDecl().IDENT().getText(); - - // TODO Copy position from textual jml field decl - FieldDeclaration fieldDecl = new FieldDeclaration( - modifiers, new VariableDeclarator(type, name)); - - if (decl.getModifiers().contains(JMLModifier.INSTANCE) - && decl.getModifiers().contains(JMLModifier.STATIC)) { - throw new SLTranslationException( - "JML field can't be static and instance at once " + decl.getDecl().getText()); - } - return fieldDecl; - } - - /** - * Transform the given local ghost/model variable declaration into a "real" statement. - * - * @param decl the given ghost/model declaration (TextualJMLFieldDecl is also used to represent - * local variable declarations!) - * @return the newly created statement - */ - private @NonNull Statement transformVariableDecl(TextualJMLFieldDecl decl) { - NodeList modifiers = new NodeList<>(); - for (JMLModifier m : decl.getModifiers()) { - if (m.equals(JMLModifier.MODEL)) { - throw new BuildingException(decl.getDecl(), - "Model modifier on variable declaration detected, only model fields are allowed"); - } - - Modifier mod = new Modifier(m.getParserKeyword()); - modifiers.add(mod); - } - - final var dims = decl.getDecl().typespec().dims(); - - // for cases like `int[] a[]`, which are allowed in Java (a is 2d here) - int arrayDims = - (dims != null ? dims.LBRACKET().size() : 0) + decl.getDecl().LBRACKET().size(); - Type type = StaticJavaParser.parseType( - decl.getDecl().typespec().type().getText() + Strings.repeat("[]", arrayDims)); - String name = decl.getDecl().IDENT().getText(); - - // TODO Copy position from textual jml field decl - var expr = new VariableDeclarationExpr(type, name); - expr.setModifiers(modifiers); - if (decl.getDecl().initialiser() != null) { - var init = decl.getDecl().initialiser().expression().getText(); - expr.getVariables().getFirst().setInitializer(StaticJavaParser.parseExpression(init)); - } - return new ExpressionStmt(expr); - } - - /** - * Transform the given model method declaration into a "real" method declaration. - * - * @param decl the give textual model method declaration - * @param jmlModifiers - * @return the new method declaration - * @throws SLTranslationException - */ - private @NonNull MethodDeclaration transformMethodDecl(TextualJMLMethodDecl decl, - @Nullable TextualJMLModifierList jmlModifiers) - throws SLTranslationException { - // prepend Java modifiers - PositionedString declWithMods = - new PositionedString(decl.getParsableDeclaration()); - - ImmutableList mods = - jmlModifiers != null ? jmlModifiers.getModifiers() : ImmutableList.of(); - ImmutableList modifiers = mods.prepend(decl.getModifiers()); - - // only handle model methods - if (!modifiers.contains(JMLModifier.MODEL)) { - throw new SLTranslationException("JML method declaration has to be model!", - declWithMods.location); - } - - // parse declaration, attach to AST - MethodDeclaration methodDecl; - ParseResult md = - services.getParser().parseMethodDeclaration(declWithMods.text); - if (md.getResult().isEmpty()) { - throw new SLTranslationException( - "could not parse", declWithMods.location); - } - methodDecl = md.getResult().get(); - - // add model modifier - for (var modifier : modifiers) { - methodDecl.addModifier(modifier.getParserKeyword()); - } - addSpec(methodDecl, decl); - return methodDecl; - } - - - private Statement transformAssertStatement(TextualJMLAssertStatement stat) { - KeyAst.Expression ctx = stat.getContext(); - de.uka.ilkd.key.java.Position pos = ctx.getStartLocation().getPosition(); - int kind = switch (stat.getKind()) { - case ASSERT -> KIND_ASSERT; - case ASSUME -> KIND_ASSUME; - }; - KeYMarkerStatement stmt = new KeYMarkerStatement(kind); - // TODO simulate/ copy token range. - stmt.setData(KEY_EXPR, ctx); - return stmt; - } - - private Statement transformSetStatement(TextualJMLSetStatement stat) { - KeyAst.SetStatementContext ctx = new KeyAst.SetStatementContext(stat.getAssignment()); - // de.uka.ilkd.key.java.Position pos = ctx.getStartLocation().getPosition(); - KeYMarkerStatement stmt = new KeYMarkerStatement(KIND_SET); - // TODO simulate/ copy token range. - stmt.setData(KEY_ASSIGN, ctx); - return stmt; - } - - private KeYMarkerStatement transformMergePointDecl(TextualJMLMergePointDecl stat) { - KeYMarkerStatement mps = new KeYMarkerStatement(KIND_MERGE_POINT); - mps.setData(KEY_MERGE_POINT, stat); - return mps; - } - - /** - * Transform all class level JML comments (such as class invariants, represents clauses, - * method contract, model method declarations, ...) with the {@link PreParser} and attach them - * to either the type declaration itself (model methods, class invariants, ...) or their - * (directly) subsequent callable declaration (method contracts). - * - * @param td the given type declaration (typically a class declaration) - * @throws SLTranslationException - */ - private void transformClassLevelComments(TypeDeclaration td) throws SLTranslationException { - URI fileName = td.findCompilationUnit().flatMap(CompilationUnit::getStorage) - .map(it -> it.getPath().toUri()) - .orElse(null); - - ArrayList> members = new ArrayList<>(td.getMembers()); - ArrayList specCases = new ArrayList<>(); - TextualJMLModifierList jmlModifiers = null; - - for (BodyDeclaration member : members) { - // JMLDocsBodyDeclaration: JML comments inside a class/interface/... body - if (member instanceof JmlDocsBodyDeclaration bd) { - String concatenatedComment = sanitizer.asString(bd.jmlDocs()); - - // The preparser split along the grammar rules in KeYParser.g4, and gives you a list - // of JML entities. - PreParser pp = getPreParser(); - // We might have multiple textual constructs now, because the single comment could - // contain multiple JML entities (e.g. method contract and ghost field declaration) - - de.uka.ilkd.key.java.Position pos = - de.uka.ilkd.key.java.Position.fromOneZeroBased(1, 0); - ImmutableList constructs = - pp.parseClassLevel(concatenatedComment, fileName, pos); - services.addWarnings(pp.getWarnings()); - - // handle model and ghost declarations in textual constructs - for (TextualJMLConstruct c : constructs) { - if (c instanceof TextualJMLFieldDecl fd) { - // ghost/model field decl.: transform into "real" field decl. - td.addMember(transformClassFieldDecl(fd)); - } else if (c instanceof TextualJMLMethodDecl md) { - // model method decl.: - final MethodDeclaration decl = transformMethodDecl(md, jmlModifiers); - jmlModifiers = null; // these are used now - // attach all specification cases accumulated so far - for (TextualJMLSpecCase specCase : specCases) { - addSpec(decl, specCase); - } - td.addMember(decl); - specCases.clear(); - } else if (c instanceof TextualJMLClassAxiom - || c instanceof TextualJMLRepresents - || c instanceof TextualJMLClassInv - || c instanceof TextualJMLInitially - || c instanceof TextualJMLDepends) { - addClassSpec(td, c); - } else if (c instanceof TextualJMLSpecCase specCase) { - // accumulate spec cases (these are model method contracts) to attach them - // in a later loop iteration to the model method declaration - specCases.add(specCase); - } else if (c instanceof TextualJMLModifierList newModifiers) { - if (jmlModifiers != null) { - throw new SLTranslationException( - "There seems to be more than one set of dangling modifiers", - c.getLocation()); - } - jmlModifiers = newModifiers; - } else { - String errorMessage = switch (c) { - case TextualJMLSetStatement a -> - "A set assignment only allowed inside of a method body"; - case TextualJMLMergePointDecl a -> - "Merge points are only allowed inside of a method body"; - case TextualJMLLoopSpec a -> - "Loop specifications are only allowed inside of a method body or initializers"; - case TextualJMLAssertStatement a -> - "Assert statements are only allowed inside of a method body or initializers"; - default -> "Unknown subclass of TextualJMLSpecCase: " + c.getClass(); - }; - throw new ConvertException(errorMessage, c.getLocation()); - } - } - } else if (jmlModifiers != null) { - // Attach any dangling modifiers from the preceding JML comment to the current node. - if (member instanceof NodeWithModifiers hasMods) { - for (var jmlMod : jmlModifiers.getModifiers()) { - hasMods.addModifier(jmlMod.getParserKeyword()); - } - } else { - throw new SLTranslationException( - "Modifiers before node that cannot have modifiers: " + member.getClass(), - jmlModifiers.getLocation()); - } - jmlModifiers = null; - } - - // add specifications to (Java) method and constructor declarations - if (member instanceof CallableDeclaration c) { - for (var specCase : specCases) { - addSpec(c, specCase); - } - specCases.clear(); - } - - // on methods, constructor, ... also process the parameters. - if (member instanceof NodeWithParameters nwp) { - NodeList params = nwp.getParameters(); - for (var param : params) { - transformModifiers(param); - } - } - } - - - for (BodyDeclaration member : td.members()) { - // attach anything that should be inside a method - if (member instanceof NodeWithOptionalBlockStmt call - && call.getBody().isPresent()) { - transformMethodLevelCommentsAt(call.getBody().get(), fileName); - } - - // modifiers (such as pure, spec_public, model, ghost, ...) - if (member instanceof NodeWithModifiers hasMods) { - transformModifiers(hasMods); - } - - if (member instanceof TypeDeclaration inner) { - transformClassLevelComments(inner); - } - } - } - - private static @NonNull PreParser getPreParser() { - return new PreParser(); - } - - private void addClassSpec(TypeDeclaration td, TextualJMLConstruct c) { - if (!td.containsData(KEY_CLASS_SPEC)) { - td.setData(KEY_CLASS_SPEC, new ArrayList<>(4)); - } - List specList = td.getData(KEY_CLASS_SPEC); - specList.add(c); - } - - private void addSpec(Node nextMember, TextualJMLConstruct specCase) { - if (!nextMember.containsData(KEY_SPEC_CASE)) { - nextMember.setData(KEY_SPEC_CASE, new ArrayList<>(4)); - } - List specList = nextMember.getData(KEY_SPEC_CASE); - specList.add(specCase); - } - - private void addLoopSpec(Node nextMember, TextualJMLLoopSpec spec) { - if (!nextMember.containsData(KEY_LOOP_SPEC)) { - nextMember.setData(KEY_LOOP_SPEC, new ArrayList<>(4)); - } - List specList = nextMember.getData(KEY_LOOP_SPEC); - specList.add(spec); - } - - private void transformMethodLevelCommentsAt(BlockStmt blockStmt, URI fileName) - throws SLTranslationException { - PreParser io = getPreParser(); - var stmts = new ArrayList<>(blockStmt.getStatements()); - var newStmts = new ArrayList(blockStmt.getStatements().size() * 2); - - final de.uka.ilkd.key.java.Position pos = - de.uka.ilkd.key.java.Position.fromOneZeroBased(1, 0); - - for (int i = 0; i < stmts.size(); i++) { - var stmt = stmts.get(i); - newStmts.add(stmt); - - while (stmt instanceof LabeledStmt labeledStmt) { - var inner = labeledStmt.getStatement(); - - if (inner instanceof JmlDocsStatements) { - throw new SLTranslationException( - ("Here is something wrong. Your label '%s' is glued to a " + - "JML annotation instead of a Java statement. Please consider the use of braces") - .formatted(labeledStmt.getLabel()), - Location.fromNode(inner)); - } - // go into the labled statement - stmt = inner; - // and treat it like a regular statement. Especially, that means - // the processing go into labled blocks `l:{}`, labled ifs `l:if(){}` or labled - // loops. - // It can not be a JML annotation statement by the exception above; - } - - - if (stmt instanceof BlockStmt bs) { - transformMethodLevelCommentsAt(bs, fileName); - } else if (stmt instanceof IfStmt is) { - if (is.thenStmt().isBlockStmt()) { - transformMethodLevelCommentsAt(is.thenStmt().asBlockStmt(), fileName); - } - if (is.elseStmt() != null && is.elseStmt().isBlockStmt()) { - transformMethodLevelCommentsAt(is.elseStmt().asBlockStmt(), fileName); - } - } else if (stmt instanceof NodeWithBody b && b.getBody().isBlockStmt()) { - transformMethodLevelCommentsAt(b.getBody().asBlockStmt(), fileName); - } else if (stmt instanceof JmlDocsStatements doc) { - String concat = sanitizer.asString(doc.getJmlDocs()); - ImmutableList constructs = - io.parseMethodLevel(concat, fileName, pos); - services.addWarnings(io.getWarnings()); - - // handle ghost declarations and set assignments in textual constructs - for (TextualJMLConstruct c : constructs) { - Statement statement; - switch (c) { - // local ghost variable declaration! - case TextualJMLFieldDecl field -> statement = transformVariableDecl(field); - case TextualJMLSetStatement set -> statement = transformSetStatement(set); - case TextualJMLMergePointDecl mergePointDecl -> - statement = transformMergePointDecl(mergePointDecl); - case TextualJMLAssertStatement assertStatement -> - statement = transformAssertStatement(assertStatement); - case TextualJMLSpecCase spec -> { - var specifiedStmt = stmts.get(i + 1); - if (specifiedStmt instanceof BlockStmt - || specifiedStmt instanceof NodeWithBody /* aka loops */ - || specifiedStmt instanceof LabeledStmt) { - addSpec(specifiedStmt, spec); - continue; - } else { - throw new IllegalStateException( - "Could not find a suitable statement for the specification in body of " - + blockStmt.getRange().get().begin + " for contracts " - + spec); - } - } - case TextualJMLLoopSpec spec -> { - var specifiedStmt = stmts.get(i + 1); - // go into labled statements - while (specifiedStmt instanceof LabeledStmt labeledStmt) { - specifiedStmt = labeledStmt.getStatement(); - } - if (specifiedStmt instanceof BlockStmt - || specifiedStmt instanceof NodeWithBody /* aka loops */ - || specifiedStmt instanceof LabeledStmt) { - addLoopSpec(specifiedStmt, spec); - continue; - } else { - throw new IllegalStateException( - "Could not find a suitable statement for the specification in body of " - + blockStmt.getRange().get().begin + " for contracts " - + spec); - } - } - default -> { - LOGGER.error("{}: Jml element unhandled: {}", c.getLocation(), - c.getClass()); - continue; - } - } - - if (statement != null) { - newStmts.add(statement); - } - } - } - - } - - blockStmt.getStatements().clear(); - blockStmt.getStatements().addAll(newStmts); - } - - @Override - public void apply(@NonNull CompilationUnit cu) { - // abort if JML is disabled - if (!ProofIndependentSettings.DEFAULT_INSTANCE.getGeneralSettings().isUseJML()) { - return; - } - - try { - URI resource = cu.getStorage() - .map(it -> it.getPath().toUri()) - .orElse(null); - - // iterate through all classes/interfaces/... in this compilation unit - final var types = new ArrayList<>(cu.getTypes()); - ImmutableList modifiers = null; - for (TypeDeclaration td : types) { - if (td instanceof JmlDocsTypeDeclaration jdtd) { - // Currently, we only support modifier at type declaration level. - // Other things would be ghost classes or model imports. - var input = sanitizer.asString(jdtd.jmlDocs()); - PreParser pp = getPreParser(); - modifiers = pp.parseModifiers(input); - } else { - if (modifiers != null && !modifiers.isEmpty()) { - for (var jmlMod : modifiers) { - td.addModifier(jmlMod.getParserKeyword()); - } - modifiers = null; - } - transformModifiers(td); - /* - * attach anything that should be directly inside classes (e.g. method - * contracts, - * model methods, class invariants, ghost field declarations, ...). - */ - transformClassLevelComments(td); - } - } - } catch (SLTranslationException e) { - // Wrap the exception into a runtime exception because recoder does - // not allow otherwise. It will be unwrapped later ... - throw new RuntimeException(e); - } - } - - /** - * Parse modifiers inside JML comments and attach them to the node as proper modifiers - * (modifiers are registered in JavaParser fork already). - * - * @param hasMods the node the modifiers should be attached to - */ - private void transformModifiers(NodeWithModifiers hasMods) { - PreParser pp = getPreParser(); - services.addWarnings(pp.getWarnings()); - - for (Modifier mod : hasMods.getModifiers()) { - var kw = mod.getKeyword(); - if (kw instanceof JmlDocModifier jdm) { - var modifiers = sanitizer.asString(jdm.getJmlDocs()); - var jmlMods = pp.parseModifiers(modifiers); - for (var jmlMod : jmlMods) { - hasMods.addModifier(jmlMod.getParserKeyword()); - } - } - } - } -} - - -record JmlDocSanitizer(Set enabledKeys) { - - public String asString(NodeList jmlDocs) { - return asString(jmlDocs, true); - } - - public String asStringJT(Collection jmlDocs, boolean emulateGlobalPosition) { - if (jmlDocs.isEmpty()) - return ""; - StringConstructor s = new StringConstructor(); - for (JavaToken tok : jmlDocs) { - if (emulateGlobalPosition) { - final Optional range = tok.getRange(); - if (range.isPresent()) { - Position cur = range.get().begin; - s.expandTo(cur.line, cur.column); - } - } else { - s.append("\n"); - } - s.append(tok.getText()); - } - return toSanitizedString(s.getBuffer()); - } - - public String asString(Collection jmlDocs, boolean emulateGlobalPosition) { - if (jmlDocs.isEmpty()) - return ""; - StringConstructor s = new StringConstructor(); - for (Token tok : jmlDocs) { - if (emulateGlobalPosition) { - s.expandTo(tok.beginLine, tok.beginColumn); - } else { - s.append("\n"); - } - s.append(tok.image); - } - return toSanitizedString(s.getBuffer()); - } - - public String asString(NodeList jmlDocs, boolean emulateGlobalPosition) { - return asStringJT(jmlDocs.stream().map(JmlDoc::getContent).toList(), emulateGlobalPosition); - } - - public String toSanitizedString(StringBuilder s) { - cleanComments(s); - cleanAtSigns(s); - return s.toString(); - } - - private static void cleanAtSigns(StringBuilder s) { - for (int pos = 0; pos < s.length(); pos++) { - char cur = s.charAt(pos); - if (cur == '\n') { - ++pos; - for (; pos < s.length(); pos++) { - if (!Character.isWhitespace(s.charAt(pos))) - break; - } - for (; pos < s.length(); pos++) { - if ('@' == s.charAt(pos)) { - s.setCharAt(pos, ' '); - } - } - } - } - } - - private void cleanComments(StringBuilder s) { - int cur = 0; - for (; cur < s.length() - 1; ++cur) { - if (isJavaCommentStart(s, cur)) { - if (isJmlComment(s, cur)) { - cur = activateJmlComment(s, cur); - } else { - cur = cleanComment(s, cur); - } - } - } - } - - private int cleanComment(StringBuilder s, int pos) { - char second = s.charAt(pos + 1); - int end; - if (second == '*') { - end = s.indexOf("*/", pos + 2) + 2; - } else { - end = s.indexOf("\n", pos + 2); - } - if (end == -1) { - // Comment is aborted by EOF rather than */ or \n - end = s.length(); - } - for (int i = pos; i < end; i++) { - s.setCharAt(i, ' '); - } - return end; - } - - private int activateJmlComment(StringBuilder s, int pos) { - boolean blockComment = s.charAt(pos) == '/' && s.charAt(pos + 1) == '*'; - if (blockComment) { - int endPos = s.indexOf("*/", pos); - if (endPos >= 0) { - s.setCharAt(endPos, ' '); - s.setCharAt(endPos + 1, ' '); - } - } - for (int i = pos; i < s.length(); i++) { - char point = s.charAt(i); - s.setCharAt(i, ' '); - if (point == '@') { - return i; - } - } - return s.length(); - } - - private boolean isJmlComment(StringBuilder s, int pos) { - int posAt = s.indexOf("@", pos + 2); - if (posAt < 0) - return false; - for (int i = pos + 2; i < posAt; i++) { - int point = s.charAt(i); - if (!(Character.isJavaIdentifierPart(point) || point == '-' || point == '+')) { - return false; - } - } - // unconditional JML comment - if (pos + 2 == posAt) - return true; - String[] keys = splitTags(s.substring(pos + 2, posAt)); - return isActiveJmlSpec(keys); - } - - private static final Pattern tag = Pattern.compile("(?=[+-])"); - - private static String[] splitTags(String substring) { - return tag.split(substring); - } - - private boolean isJavaCommentStart(StringBuilder s, int pos) { - return s.charAt(pos) == '/' && (s.charAt(pos + 1) == '*' || s.charAt(pos + 1) == '/'); - } - - public static boolean isActiveJmlSpec(Collection activeKeys, String[] keys) { - if (keys.length == 0) { - // a JML annotation with no keys is always included, - return true; - } - // a JML annotation with at least one positive-key is only included - boolean plusKeyFound = false; - // if at least one of these positive keys is enabled - boolean enabledPlusKeyFound = false; - // a JML annotation with an enabled negative-key is ignored (even if there are enabled - // positive-keys). - boolean enabledNegativeKeyFound = false; - for (String marker : keys) { - if (marker.isEmpty()) - continue; - plusKeyFound = plusKeyFound || isPositive(marker); - enabledPlusKeyFound = - enabledPlusKeyFound || isPositive(marker) && isEnabled(activeKeys, marker); - enabledNegativeKeyFound = - enabledNegativeKeyFound || isNegative(marker) && isEnabled(activeKeys, marker); - if ("-".equals(marker) || "+".equals(marker)) { - return false; - } - } - return (!plusKeyFound || enabledPlusKeyFound) && !enabledNegativeKeyFound; - } - - public boolean isActiveJmlSpec(String[] keys) { - return isActiveJmlSpec(enabledKeys, keys); - } - - private static boolean isNegative(String marker) { - return marker.charAt(0) == '-'; - } - - private static boolean isEnabled(Collection enabledKeys, String marker) { - // remove [+-] prefix - return enabledKeys.contains(marker.substring(1).toLowerCase()); - } - - private static boolean isPositive(String marker) { - return marker.charAt(0) == '+'; - } -} - - -class StringConstructor { - - private final StringBuilder sb = new StringBuilder(1024); - - // JavaCC starts with 1/1 - private int curLine = 1; - - private int curColumn = 1; - - public StringConstructor append(String value) { - sb.ensureCapacity(sb.length() + value.length() + 1); - for (char c : value.toCharArray()) { - sb.append(c); - if (c == '\n') { - curColumn = 1; - curLine++; - } else { - curColumn++; - } - } - return this; - } - - public StringConstructor expandTo(int line, int column) { - if (curLine > line || (curLine == line && curColumn > column)) { - throw new IllegalArgumentException(); - } - for (; curLine < line; curLine++) { - sb.append("\n"); - curColumn = 1; - } - for (; curColumn < column; curColumn++) { - sb.append(" "); - } - return this; - } - - @Override - public String toString() { - return sb.toString(); - } - - public StringBuilder getBuffer() { - return sb; - } -} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JmlDocRemoval.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JmlDocRemoval.java index cd1d0721a2b..d1f5af6335e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JmlDocRemoval.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JmlDocRemoval.java @@ -5,10 +5,7 @@ import com.github.javaparser.ast.CompilationUnit; import com.github.javaparser.ast.Modifier; -import com.github.javaparser.ast.key.JmlDocModifier; -import com.github.javaparser.ast.key.JmlDocsBodyDeclaration; -import com.github.javaparser.ast.key.JmlDocsStatements; -import com.github.javaparser.ast.key.JmlDocsTypeDeclaration; +import com.github.javaparser.ast.jml.doc.*; import org.jspecify.annotations.NonNull; /** @@ -30,9 +27,9 @@ public void apply(CompilationUnit cu) { } } - if (it instanceof JmlDocsStatements || - it instanceof JmlDocsTypeDeclaration || - it instanceof JmlDocsBodyDeclaration) { + if (it instanceof JmlDocStmt || + it instanceof JmlDocType || + it instanceof JmlDocDeclaration) { it.remove(); } }); diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractOperationPO.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractOperationPO.java index 1ea6eb95518..9f82f98c42b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractOperationPO.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractOperationPO.java @@ -39,7 +39,7 @@ import org.key_project.util.collection.ImmutableSLList; import org.key_project.util.collection.ImmutableSet; -import com.github.javaparser.ast.key.KeyTransactionStatement; +import com.github.javaparser.ast.key.KeyTransactionStmt; import org.jspecify.annotations.Nullable; /** @@ -921,19 +921,19 @@ protected JavaBlock buildJavaBlock(ImmutableList formalParVars sb2 = new StatementBlock(transaction ? new Statement[] { new TransactionStatement( - KeyTransactionStatement.TransactionType.BEGIN), + KeyTransactionStmt.TransactionType.BEGIN), nullStat, tryStat, new TransactionStatement( - KeyTransactionStatement.TransactionType.FINISH) } + KeyTransactionStmt.TransactionType.FINISH) } : new Statement[] { nullStat, tryStat }); } else { sb2 = new StatementBlock(transaction ? new Statement[] { new TransactionStatement( - KeyTransactionStatement.TransactionType.BEGIN), + KeyTransactionStmt.TransactionType.BEGIN), nullStat, beforeTry, tryStat, new TransactionStatement( - KeyTransactionStatement.TransactionType.FINISH) } + KeyTransactionStmt.TransactionType.FINISH) } : new Statement[] { nullStat, beforeTry, tryStat }); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AuxiliaryContractBuilders.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AuxiliaryContractBuilders.java index d78676170aa..470084a9c76 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/AuxiliaryContractBuilders.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/AuxiliaryContractBuilders.java @@ -7,6 +7,7 @@ import java.util.Map.Entry; import java.util.stream.Collectors; +import com.github.javaparser.ast.key.KeyTransactionStmt; import de.uka.ilkd.key.java.*; import de.uka.ilkd.key.java.ast.*; import de.uka.ilkd.key.java.ast.Label; @@ -56,7 +57,6 @@ import org.key_project.util.collection.ImmutableSLList; import org.key_project.util.collection.ImmutableSet; -import com.github.javaparser.ast.key.KeyTransactionStatement; import org.jspecify.annotations.NonNull; import static de.uka.ilkd.key.logic.equality.IrrelevantTermLabelsProperty.IRRELEVANT_TERM_LABELS_PROPERTY; @@ -1589,7 +1589,7 @@ private StatementBlock finishTransactionIfModalityIsTransactional( final Statement statement) { if (instantiation.isTransactional()) { return new StatementBlock(statement, - new TransactionStatement(KeyTransactionStatement.TransactionType.FINISH)); + new TransactionStatement(KeyTransactionStmt.TransactionType.FINISH)); } else { if (statement instanceof StatementBlock) { return (StatementBlock) statement; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/JmlAssertRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/JmlAssertRule.java index 236ba196b9d..4a9765247c2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/JmlAssertRule.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/JmlAssertRule.java @@ -15,7 +15,6 @@ import de.uka.ilkd.key.logic.op.Transformer; import de.uka.ilkd.key.logic.op.UpdateApplication; import de.uka.ilkd.key.proof.Goal; -import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLAssertStatement.Kind; import de.uka.ilkd.key.util.MiscTools; import org.key_project.logic.Name; @@ -28,6 +27,8 @@ import org.jspecify.annotations.NonNull; +import static de.uka.ilkd.key.java.ast.statement.JmlAssert.*; + /** * A rule for JML assert/assume statements. * This implements the rules as: @@ -140,7 +141,7 @@ public IBuiltInRuleApp createApp(PosInOccurrence occurrence, TermServices servic } JTerm condition = - tb.convertToFormula(spec.getTerm(services, self, JmlAssert.INDEX_CONDITION)); + tb.convertToFormula(spec.getTerm(services, self, INDEX_CONDITION)); condition = tb.addLabel(condition, new OriginTermLabel.Origin( kind == Kind.ASSERT ? OriginTermLabel.SpecType.ASSERT diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/WhileInvariantTransformer.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/WhileInvariantTransformer.java index 3f0907a142d..b7cc7c631cb 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/WhileInvariantTransformer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/WhileInvariantTransformer.java @@ -7,6 +7,7 @@ import java.util.LinkedList; import java.util.ListIterator; +import com.github.javaparser.ast.key.KeyTransactionStmt; import de.uka.ilkd.key.java.*; import de.uka.ilkd.key.java.ast.JavaNonTerminalProgramElement; import de.uka.ilkd.key.java.ast.ProgramElement; @@ -38,8 +39,6 @@ import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; -import com.github.javaparser.ast.key.KeyTransactionStatement; - public final class WhileInvariantTransformer { /** the outer label that is used to leave the while loop ('l1') */ private final SchemaVariable outerLabel = SchemaVariableFactory @@ -224,7 +223,7 @@ public JTerm transform(TermLabelState termLabelState, Rule rule, JavaBlock mainJavaBlock = JavaBlock.createJavaBlock(transaction ? new StatementBlock(resSta, new TransactionStatement( - KeyTransactionStatement.TransactionType.FINISH)) + KeyTransactionStmt.TransactionType.FINISH)) : new StatementBlock(resSta)); return services.getTermBuilder().prog(loopBodyModalityKind, mainJavaBlock, result, computeLoopBodyModalityLabels(termLabelState, services, applicationPos, rule, ruleApp, diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/AbstractAuxiliaryContractImpl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/AbstractAuxiliaryContractImpl.java index 055e5d28789..e779e50ed11 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/AbstractAuxiliaryContractImpl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/AbstractAuxiliaryContractImpl.java @@ -21,7 +21,6 @@ import de.uka.ilkd.key.pp.LogicPrinter; import de.uka.ilkd.key.proof.OpReplacer; import de.uka.ilkd.key.speclang.Contract.OriginalVariables; -import de.uka.ilkd.key.speclang.jml.pretranslation.Behavior; import de.uka.ilkd.key.util.InfFlowSpec; import org.key_project.util.collection.DefaultImmutableSet; diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/BlockContractImpl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/BlockContractImpl.java index 8bc763b7563..ab012f0cfce 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/BlockContractImpl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/BlockContractImpl.java @@ -19,7 +19,6 @@ import de.uka.ilkd.key.logic.op.JModality; import de.uka.ilkd.key.logic.op.LocationVariable; import de.uka.ilkd.key.proof.mgt.SpecificationRepository; -import de.uka.ilkd.key.speclang.jml.pretranslation.Behavior; import de.uka.ilkd.key.util.InfFlowSpec; import org.key_project.util.collection.DefaultImmutableSet; diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java index 89b0053817e..6de2db92eba 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java @@ -43,7 +43,6 @@ import de.uka.ilkd.key.proof.mgt.SpecificationRepository; import de.uka.ilkd.key.rule.inst.SVInstantiations; import de.uka.ilkd.key.rule.metaconstruct.EnhancedForElimination; -import de.uka.ilkd.key.speclang.jml.pretranslation.Behavior; import de.uka.ilkd.key.util.InfFlowSpec; import org.key_project.logic.SyntaxElement; diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLInfoExtractor.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLInfoExtractor.java index d63ac422977..c8c8573a1ae 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLInfoExtractor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLInfoExtractor.java @@ -9,7 +9,6 @@ import de.uka.ilkd.key.java.ast.declaration.*; import de.uka.ilkd.key.java.ast.declaration.modifier.Modifiers; import de.uka.ilkd.key.logic.op.IProgramMethod; -import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct; import de.uka.ilkd.key.speclang.njml.SpecMathMode; import de.uka.ilkd.key.util.MiscTools; diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java index a7f3c262dc4..52b522ddbd1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java @@ -3,12 +3,16 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.speclang.jml; -import java.net.URI; -import java.util.*; - +import com.github.javaparser.ast.jml.body.JmlClassAccessibleDeclaration; +import com.github.javaparser.ast.jml.body.JmlClassExprDeclaration; +import com.github.javaparser.ast.jml.body.JmlRepresentsDeclaration; +import com.github.javaparser.ast.jml.clauses.JmlContract; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.TypeConverter; -import de.uka.ilkd.key.java.ast.*; +import de.uka.ilkd.key.java.ast.Label; +import de.uka.ilkd.key.java.ast.PositionInfo; +import de.uka.ilkd.key.java.ast.Statement; +import de.uka.ilkd.key.java.ast.StatementBlock; import de.uka.ilkd.key.java.ast.abstraction.ArrayType; import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; import de.uka.ilkd.key.java.ast.abstraction.Type; @@ -27,19 +31,18 @@ import de.uka.ilkd.key.parser.Location; import de.uka.ilkd.key.proof.init.InitConfig; import de.uka.ilkd.key.speclang.*; -import de.uka.ilkd.key.speclang.jml.pretranslation.*; import de.uka.ilkd.key.speclang.jml.translation.JMLSpecFactory; import de.uka.ilkd.key.speclang.njml.JmlFacade; import de.uka.ilkd.key.speclang.njml.LabeledParserRuleContext; import de.uka.ilkd.key.speclang.translation.SLTranslationException; import de.uka.ilkd.key.speclang.translation.SLWarningException; - +import org.antlr.v4.runtime.ParserRuleContext; import org.key_project.util.collection.*; -import org.key_project.util.collection.DefaultImmutableSet; -import org.key_project.util.collection.ImmutableArray; -import org.key_project.util.collection.ImmutableList; -import org.antlr.v4.runtime.ParserRuleContext; +import java.net.URI; +import java.util.ArrayList; +import java.util.LinkedList; +import java.util.List; import static de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLSpecCase.Clause.SIGNALS_ONLY; import static de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLSpecCase.ClauseHd.*; @@ -55,16 +58,18 @@ public final class JMLSpecExtractor implements SpecExtractor { private static final String THROWABLE = "java.lang.Throwable"; private static final String ERROR = "java.lang.Error"; private static final String RUNTIME_EXCEPTION = "java.lang.RuntimeException"; - /** The default signals only clause for errors and runtime exceptions. **/ + /** + * The default signals only clause for errors and runtime exceptions. + **/ private static final String DEFAULT_SIGNALS_ONLY = - format("signals_only %s, %s;", ERROR, RUNTIME_EXCEPTION); + format("signals_only %s, %s;", ERROR, RUNTIME_EXCEPTION); /** * This is the term label for implicit specification clauses. This is important for * well-definedness checks. Hence, do not change its usages unless you understand and have * thought about the semantics of the corresponding well-definedness checks. **/ private static final TermLabel IMPL_TERM_LABEL = - ParameterlessTermLabel.IMPLICIT_SPECIFICATION_LABEL; + ParameterlessTermLabel.IMPLICIT_SPECIFICATION_LABEL; private final Services services; private final JMLSpecFactory jsf; private ImmutableList warnings = ImmutableSLList.nil(); @@ -97,7 +102,7 @@ private ParserRuleContext getDefaultSignalsOnly(IProgramMethod pm) { for (int i = 0; i < exceptions.size(); i++) { if (services.getJavaInfo().isSubtype(exceptions.get(i).getKeYJavaType(), - services.getJavaInfo().getKeYJavaType(THROWABLE))) { + services.getJavaInfo().getKeYJavaType(THROWABLE))) { b.append(", ").append(exceptions.get(i).getKeYJavaType().getFullName()); } } @@ -113,11 +118,11 @@ private ParserRuleContext getDefaultSignalsOnly(IProgramMethod pm) { * of a reference array type that also its elements are non-null In case of implicit fields or * primitive typed fields/variables the empty set is returned * - * @param varName the String specifying the variable/field name - * @param kjt the KeYJavaType representing the variables/field declared type + * @param varName the String specifying the variable/field name + * @param kjt the KeYJavaType representing the variables/field declared type * @param isImplicitVar a boolean indicating if the field is an implicit one (in which case - * no - * @param services the services object + * no + * @param services the services object * @return set of formulas specifying non-nullity for field/variables */ public static ImmutableSet createNonNullPositionedString( @@ -133,10 +138,10 @@ public static ImmutableSet createNonNullPositionedStri // use special "deep" non null predicate (see bug #1392) // ... looks a bit like a hack with those DL escapes ... final String nonNullString = - arrayDepth > 0 ? format("\\dl_nonNull(\\dl_heap(),%s,%d)", varName, arrayDepth) - : format("%s != null", varName); + arrayDepth > 0 ? format("\\dl_nonNull(\\dl_heap(),%s,%d)", varName, arrayDepth) + : format("%s != null", varName); final ParserRuleContext ps = - JmlFacade.parseExpr(new PositionedString(nonNullString, location)); + JmlFacade.parseExpr(new PositionedString(nonNullString, location)); result = result.add(new LabeledParserRuleContext(ps, IMPL_TERM_LABEL)); } return result; @@ -190,10 +195,10 @@ public ImmutableSet extractClassSpecs(KeYJavaType kjt) } // check for spec_* modifiers (bug #1280) if (JMLInfoExtractor.hasJMLModifier((FieldDeclaration) member, - Modifiers.JML_SPEC_PUBLIC.class)) { + Modifiers.JML_SPEC_PUBLIC.class)) { visibility = new Public(); } else if (JMLInfoExtractor.hasJMLModifier((FieldDeclaration) member, - Modifiers.JML_SPEC_PROTECTED.class)) { + Modifiers.JML_SPEC_PROTECTED.class)) { visibility = new Protected(); } @@ -206,13 +211,13 @@ public ImmutableSet extractClassSpecs(KeYJavaType kjt) // and not for implicit fields. if (!JMLInfoExtractor.isNullable((FieldDeclaration) member, td)) { ImmutableSet nonNullInvs = - createNonNullPositionedString(field.getProgramName(), - field.getProgramVariable().getKeYJavaType(), - field.isImplicit(), - new Location(fileName, member.getEndPosition()), services); + createNonNullPositionedString(field.getProgramName(), + field.getProgramVariable().getKeYJavaType(), + field.isImplicit(), + new Location(fileName, member.getEndPosition()), services); for (LabeledParserRuleContext classInv : nonNullInvs) { final ClassInvariant jmlClassInvariant = - jsf.createJMLClassInvariant(kjt, visibility, isStatic, classInv); + jsf.createJMLClassInvariant(kjt, visibility, isStatic, classInv); result = result.add(jmlClassInvariant); } } @@ -220,34 +225,40 @@ public ImmutableSet extractClassSpecs(KeYJavaType kjt) } } + com.github.javaparser.ast.body.TypeDeclaration original = + services.getTypeConverter(); - var constructs = td.getAttachedJml(); // create class invs out of textual constructs, add them to result - for (TextualJMLConstruct c : constructs) { + for (var c : original.getMembers()) { try { switch (c) { - case TextualJMLClassInv textualInv -> { - ClassInvariant inv = jsf.createJMLClassInvariant(kjt, textualInv); - result = result.add(inv); - } - case TextualJMLInitially textualRep -> { - InitiallyClause inc = jsf.createJMLInitiallyClause(kjt, textualRep); - result = result.add(inc); + case JmlClassExprDeclaration jmlDecl -> { + switch (jmlDecl.kind().identifier()) { + case "\\invariant" -> { + ClassInvariant inv = jsf.createJMLClassInvariant(kjt, jmlDecl); + result = result.add(inv); + } + case "\\axiom" -> { + ClassAxiom ax = jsf.createJMLClassAxiom(kjt, jmlDecl); + result = result.add(ax); + } + case "\\initially" -> { + InitiallyClause inc = jsf.createJMLInitiallyClause(kjt, jmlDecl); + result = result.add(inc); + } + } } - case TextualJMLRepresents textualRep -> { + + case JmlRepresentsDeclaration textualRep -> { ClassAxiom rep = jsf.createJMLRepresents(kjt, textualRep); result = result.add(rep); } - case TextualJMLDepends textualDep -> { + + case JmlClassAccessibleDeclaration textualDep -> { Contract depContract = jsf.createJMLDependencyContract(kjt, textualDep); result = result.add(depContract); } - case TextualJMLClassAxiom textualJMLClassAxiom -> { - ClassAxiom ax = jsf.createJMLClassAxiom(kjt, textualJMLClassAxiom); - result = result.add(ax); - } - case null, default -> { - } + // DO NOTHING // There may be other kinds of JML constructs which are // not specifications. @@ -268,7 +279,7 @@ public List extractMethodSpecs(IProgramMethod pm) /** * Extracts method specifications (i.e., contracts) from Java+JML input. * - * @param pm method to extract for + * @param pm method to extract for * @param addInvariant whether to add static invariants to pre- and post-conditions */ @Override @@ -286,26 +297,16 @@ public List extractMethodSpecs(IProgramMethod pm, boolean final boolean isHelper = JMLInfoExtractor.isHelper(pm); // get textual JML constructs - ImmutableList constructs = pm.getMethodDeclaration().getAttachedJml(); + var constructs = pm.getMethodDeclaration().getAttachedJml(); ParserRuleContext modelMethodDefinition = null; - for (var c : constructs) { - if (c instanceof TextualJMLMethodDecl m) { - if (pm.getMethodDeclaration().containsModifier(Model.class)) { - modelMethodDefinition = m.getMethodDefinition(); - break; - } + for (JmlContract m : constructs) { + if (pm.getMethodDeclaration().containsModifier(Model.class)) { + modelMethodDefinition = m.getMethodDefinition(); + break; } } - // Model method without specification. We need to create a specCase - // to attach the AXIOMS clase for its definition. - if (modelMethodDefinition != null && constructs.size() == 1) { - TextualJMLSpecCase specCase = - new TextualJMLSpecCase(ImmutableList.of(), Behavior.MODEL_BEHAVIOR); - constructs = constructs.append(specCase); - } - for (var c : constructs) { if (c instanceof TextualJMLSpecCase specCase) { specCase = specCase.copy(); @@ -318,12 +319,12 @@ public List extractMethodSpecs(IProgramMethod pm, boolean if (isStrictlyPure || pm.isModel()) { for (LocationVariable heap : HeapContext.getModifiableHeaps(services, false)) { specCase.addClause(ASSIGNABLE, heap.name(), - JmlFacade.parseExpr("\\strictly_nothing")); + JmlFacade.parseExpr("\\strictly_nothing")); } } else if (isPure) { for (LocationVariable heap : HeapContext.getModifiableHeaps(services, false)) { specCase.addClause(ASSIGNABLE, heap.name(), - JmlFacade.parseExpr("\\nothing")); + JmlFacade.parseExpr("\\nothing")); } } @@ -343,37 +344,37 @@ public List extractMethodSpecs(IProgramMethod pm, boolean if (!pm.isConstructor()) { specCase.addClause(REQUIRES, new LabeledParserRuleContext( - JmlFacade.parseExpr(invString), IMPL_TERM_LABEL)); + JmlFacade.parseExpr(invString), IMPL_TERM_LABEL)); if (hasFreeInvariant) { specCase.addClause(REQUIRES_FREE, new LabeledParserRuleContext( - JmlFacade.parseExpr(invFreeString), IMPL_TERM_LABEL)); + JmlFacade.parseExpr(invFreeString), IMPL_TERM_LABEL)); } } else if (addInvariant) { // add static invariant to constructor's precondition specCase.addClause(REQUIRES, new LabeledParserRuleContext( - JmlFacade.parseExpr(format("%s.\\inv", pm.getName())), - IMPL_TERM_LABEL)); + JmlFacade.parseExpr(format("%s.\\inv", pm.getName())), + IMPL_TERM_LABEL)); if (hasFreeInvariant) { specCase.addClause(REQUIRES_FREE, new LabeledParserRuleContext( - JmlFacade.parseExpr(format("%s.\\inv_free", pm.getName())), - IMPL_TERM_LABEL)); + JmlFacade.parseExpr(format("%s.\\inv_free", pm.getName())), + IMPL_TERM_LABEL)); } } if (specCase.getBehavior() != Behavior.EXCEPTIONAL_BEHAVIOR) { specCase.addClause(ENSURES, new LabeledParserRuleContext( - JmlFacade.parseExpr(invString), IMPL_TERM_LABEL)); + JmlFacade.parseExpr(invString), IMPL_TERM_LABEL)); if (hasFreeInvariant) { specCase.addClause(ENSURES_FREE, new LabeledParserRuleContext( - JmlFacade.parseExpr(invFreeString), IMPL_TERM_LABEL)); + JmlFacade.parseExpr(invFreeString), IMPL_TERM_LABEL)); } } if (specCase.getBehavior() != Behavior.NORMAL_BEHAVIOR && !pm.isModel()) { specCase.addClause(TextualJMLSpecCase.Clause.SIGNALS, - new LabeledParserRuleContext( - JmlFacade.parseClause( - format("signals (Throwable e) %s;", invString)), - IMPL_TERM_LABEL)); + new LabeledParserRuleContext( + JmlFacade.parseClause( + format("signals (Throwable e) %s;", invString)), + IMPL_TERM_LABEL)); } } @@ -381,16 +382,16 @@ public List extractMethodSpecs(IProgramMethod pm, boolean // add non-null preconditions for (int j = 0, n = pm.getParameterDeclarationCount(); j < n; j++) { final VariableSpecification paramDecl = - pm.getParameterDeclarationAt(j).getVariableSpecification(); + pm.getParameterDeclarationAt(j).getVariableSpecification(); if (!JMLInfoExtractor.parameterIsNullable(pm, j)) { // no additional precondition for primitive types! // createNonNullPos... takes care of that final ImmutableSet nonNullParams = - createNonNullPositionedString(paramDecl.getName(), - paramDecl.getProgramVariable().getKeYJavaType(), false, - new Location(fileName, - pm.getStartPosition()), - services); + createNonNullPositionedString(paramDecl.getName(), + paramDecl.getProgramVariable().getKeYJavaType(), false, + new Location(fileName, + pm.getStartPosition()), + services); for (LabeledParserRuleContext nonNull : nonNullParams) { specCase.addClause(REQUIRES, nonNull); } @@ -403,10 +404,10 @@ public List extractMethodSpecs(IProgramMethod pm, boolean if (!pm.isVoid() && !pm.isConstructor() && !JMLInfoExtractor.resultIsNullable(pm) && specCase.getBehavior() != Behavior.EXCEPTIONAL_BEHAVIOR) { final ImmutableSet resultNonNull = - createNonNullPositionedString("\\result", resultType, false, - new Location(fileName, - pm.getStartPosition()), - services); + createNonNullPositionedString("\\result", resultType, false, + new Location(fileName, + pm.getStartPosition()), + services); for (LabeledParserRuleContext nonNull : resultNonNull) { specCase.addClause(ENSURES, nonNull); } @@ -421,7 +422,7 @@ public List extractMethodSpecs(IProgramMethod pm, boolean // translate contract try { ImmutableSet contracts = - jsf.createJMLOperationContracts(pm, specCase); + jsf.createJMLOperationContracts(pm, specCase); for (Contract contract : contracts) { result.add(contract); } @@ -435,13 +436,13 @@ public List extractMethodSpecs(IProgramMethod pm, boolean @Override public ImmutableSet extractBlockContracts(final IProgramMethod method, - final StatementBlock block) throws SLTranslationException { + final StatementBlock block) throws SLTranslationException { return createBlockContracts(method, new LinkedList<>(), block); } @Override public ImmutableSet extractBlockContracts(final IProgramMethod method, - final LabeledStatement labeled) throws SLTranslationException { + final LabeledStatement labeled) throws SLTranslationException { final List