From ebab6507aa1f9c91191e4d390f2bf41c1c272c55 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sun, 12 Apr 2026 03:53:59 +0200 Subject: [PATCH 1/7] AST generation --- .../de/uka/ilkd/key/logic/VariableNamer.java | 4 +- key.ncore.java/build.gradle | 22 + key.ncore.java/src/adt/java-ast.java | 1082 +++++++++++++++++ .../org/key_project/ncore/java/Generator.java | 530 ++++++++ .../ncore/java/ReadAllHierarchy.java | 795 ++++++++++++ .../java/ast/DefaultProperties.java | 34 + .../org/key_project/java/ast/Properties.java | 13 + .../org/key_project/java/ast/Property.java | 25 + settings.gradle | 1 + 9 files changed, 2504 insertions(+), 2 deletions(-) create mode 100644 key.ncore.java/build.gradle create mode 100644 key.ncore.java/src/adt/java-ast.java create mode 100644 key.ncore.java/src/generator/java/org/key_project/ncore/java/Generator.java create mode 100644 key.ncore.java/src/generator/java/org/key_project/ncore/java/ReadAllHierarchy.java create mode 100644 key.ncore.java/src/main/java/org/key_project/java/ast/DefaultProperties.java create mode 100644 key.ncore.java/src/main/java/org/key_project/java/ast/Properties.java create mode 100644 key.ncore.java/src/main/java/org/key_project/java/ast/Property.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/VariableNamer.java b/key.core/src/main/java/de/uka/ilkd/key/logic/VariableNamer.java index bee675efa44..67b4483d3c3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/VariableNamer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/VariableNamer.java @@ -679,7 +679,7 @@ public int getIndex() { /** * temporary indexed ProgramElementName */ - private static class TempIndProgramElementName extends IndProgramElementName { + public static class TempIndProgramElementName extends IndProgramElementName { TempIndProgramElementName(String basename, int index, NameCreationInfo creationInfo) { super(basename + TEMP_INDEX_SEPARATOR + index, basename, index, creationInfo); } @@ -695,7 +695,7 @@ private static class TempIndProgramElementName extends IndProgramElementName { /** * regular indexed ProgramElementName */ - private static class PermIndProgramElementName extends IndProgramElementName { + public static class PermIndProgramElementName extends IndProgramElementName { static final char SEPARATOR = '_'; PermIndProgramElementName(String basename, int index, NameCreationInfo creationInfo) { diff --git a/key.ncore.java/build.gradle b/key.ncore.java/build.gradle new file mode 100644 index 00000000000..497a6f2ea81 --- /dev/null +++ b/key.ncore.java/build.gradle @@ -0,0 +1,22 @@ +sourceSets { + generator { + java { + srcDir("src/generator/java") + } + } + main { + java { srcDir("src/generated/java") } + } +} + +dependencies { + generatorImplementation(project(":key.core")) + + + implementation("info.picocli:picocli:4.7.7") + + def JP_VERSION = "3.28.0-K13.5" + implementation("org.key-project.proofjava:javaparser-core:$JP_VERSION") + implementation("org.key-project.proofjava:javaparser-symbol-solver-core:$JP_VERSION") + testImplementation("com.google.truth:truth:1.4.5") +} \ No newline at end of file diff --git a/key.ncore.java/src/adt/java-ast.java b/key.ncore.java/src/adt/java-ast.java new file mode 100644 index 00000000000..e4bc355948d --- /dev/null +++ b/key.ncore.java/src/adt/java-ast.java @@ -0,0 +1,1082 @@ +import org.jspecify.annotations.Nullable; + +class CompilationUnit extends JavaNonTerminalProgramElement { + @Nullable PackageSpecification packageSpec; + List imports; + List typeDeclarations; +} + +class ContextStatementBlock extends StatementBlock { } + +abstract class Declaration { } + +abstract class ExpressionContainer { } + +class Import extends JavaNonTerminalProgramElement { + boolean isMultiImport; + TypeReferenceInfix reference; +} + +abstract class JavaNonTerminalProgramElement extends JavaProgramElement { +} + +abstract class JavaProgramElement extends JavaSourceElement { +} + +abstract class Label { +} + +abstract class LoopInitializer { +} + +abstract class NamedProgramElement { +} + +class PackageSpecification extends JavaNonTerminalProgramElement { + + PackageReference reference; +} + +abstract class ParameterContainer { +} + +abstract class ProgramElement { +} + +abstract class ProgramVariableName { +} + +abstract class Reference { +} + +abstract class ScopeDefiningElement { +} + +abstract class Statement { +} + +class StatementBlock extends JavaStatement { +} + +abstract class StatementContainer { +} + +abstract class TerminalProgramElement { +} + +abstract class TypeScope { +} + +abstract class VariableScope { +} + +class CcatchBreakLabelParameterDeclaration extends CcatchNonstandardParameterDeclaration { +} + +class CcatchBreakWildcardParameterDeclaration extends CcatchNonstandardParameterDeclaration { +} + +class CcatchContinueLabelParameterDeclaration extends CcatchNonstandardParameterDeclaration { +} + +class CcatchContinueParameterDeclaration extends CcatchNonstandardParameterDeclaration { +} + +class CcatchContinueWildcardParameterDeclaration extends CcatchNonstandardParameterDeclaration { +} + +abstract class CcatchNonstandardParameterDeclaration extends JavaNonTerminalProgramElement { +} + +class CcatchReturnParameterDeclaration extends CcatchNonstandardParameterDeclaration { +} + +class CcatchReturnValParameterDeclaration extends CcatchNonstandardParameterDeclaration { +} + +class ArrayDeclaration extends TypeDeclaration { +} + +class ClassDeclaration extends TypeDeclaration { + + Extends extending; + + Implements implementing; + + boolean isInnerClass; + + boolean isLocalClass; + + boolean isAnonymousClass; +} + +class ClassInitializer extends JavaDeclaration { + + StatementBlock body; +} + +class ConstructorDeclaration extends MethodDeclaration { +} + +class EnumClassDeclaration extends ClassDeclaration { +} + +class Extends extends InheritanceSpecification { +} + +class FieldDeclaration extends VariableDeclaration { + + List fieldSpecs; +} + +class FieldSpecification extends VariableSpecification { +} + +class Implements extends InheritanceSpecification { +} + +abstract class InheritanceSpecification extends JavaNonTerminalProgramElement { + + List supertypes; +} + +class InterfaceDeclaration extends TypeDeclaration { + + Extends extending; +} + +abstract class JavaDeclaration extends JavaNonTerminalProgramElement { + + ImmutableList attachedJml; + + List modArray; +} + +class LocalVariableDeclaration extends VariableDeclaration { + + List varSpecs; +} + +abstract class MemberDeclaration { +} + +class MethodDeclaration extends JavaDeclaration { + + TypeReference returnType; + + Comment[] voidComments; + + ProgramElementName name; + + List parameters; + + Throws exceptions; + + StatementBlock body; + + JMLModifiers jmlModifiers; + + boolean parentIsInterfaceDeclaration; +} + +abstract class Modifier extends JavaProgramElement { +} + +class ParameterDeclaration extends VariableDeclaration { + List varSpec; +} + +class SuperArrayDeclaration extends TypeDeclaration { +} + +class Throws extends JavaNonTerminalProgramElement { + + List exceptions; +} + +abstract class TypeDeclaration extends JavaDeclaration { + + ProgramElementName name; + + ProgramElementName fullName; + + List members; + + boolean parentIsInterfaceDeclaration; + + boolean isLibrary; + + JMLModifiers jmlModifiers; +} + +abstract class TypeDeclarationContainer { +} + +abstract class VariableDeclaration extends JavaDeclaration { + + TypeReference typeReference; + + boolean parentIsInterfaceDeclaration; +} + +class VariableSpecification extends JavaNonTerminalProgramElement { + + Expression initializer; + + int dimensions; + + Type type; + + IProgramVariable programVariable; +} + +class Abstract extends Modifier { +} + +class AnnotationUseSpecification extends Modifier { + + TypeReference tr; +} + +class Final extends Modifier { +} + +class Ghost extends Modifier { +} + +class Model extends Modifier { +} + +class ABSTRACT extends Modifier { +} + +class DEFAULT extends Modifier { +} + +class FINAL extends Modifier { +} + +class JML_CODE extends Modifier { +} + +class JML_CODE_BIGINT_MATH extends Modifier { +} + +class JML_CODE_JAVA_MATH extends Modifier { +} + +class JML_CODE_SAFE_MATH extends Modifier { +} + +class JML_HELPER extends Modifier { +} + +class JML_INSTANCE extends Modifier { +} + +class JML_NON_NULL extends Modifier { +} + +class JML_NON_NULL_BY_DEFAULT extends Modifier { +} + +class JML_NON_NULL_ELEMENTS extends Modifier { +} + +class JML_NO_STATE extends Modifier { +} + +class JML_NULLABLE extends Modifier { +} + +class JML_NULLABLE_BY_DEFAULT extends Modifier { +} + +class JML_OT_READ_ONLY extends Modifier { +} + +class JML_OT_REP extends Modifier { +} + +class JML_PACKAGE extends Modifier { +} + +class JML_PURE extends Modifier { +} + +class JML_SPEC_BIGINT_MATH extends Modifier { +} + +class JML_SPEC_JAVA_MATH extends Modifier { +} + +class JML_SPEC_PACKAGE extends Modifier { +} + +class JML_SPEC_PRIVATE extends Modifier { +} + +class JML_SPEC_PROTECTED extends Modifier { +} + +class JML_SPEC_PUBLIC extends Modifier { +} + +class JML_SPEC_SAFE_MATH extends Modifier { +} + +class JML_STRICTLY_PURE extends Modifier { +} + +class JML_TWO_STATE extends Modifier { +} + +class JML_UNPARSABLE_MODIFIERS extends Modifier { +} + +class NATIVE extends Modifier { +} + +class NON_SEALED extends Modifier { +} + +class PRIVATE extends Modifier { +} + +class PROTECTED extends Modifier { +} + +class PUBLIC extends Modifier { +} + +class SEALED extends Modifier { +} + +class STATIC extends Modifier { +} + +class STRICTFP extends Modifier { +} + +class SYNCHRONIZED extends Modifier { +} + +class TRANSIENT extends Modifier { +} + +class TRANSITIVE extends Modifier { +} + +class VOLATILE extends Modifier { +} + +class Native extends Modifier { +} + +class NoState extends Modifier { +} + +class Private extends VisibilityModifier { +} + +class Protected extends VisibilityModifier { +} + +class Public extends VisibilityModifier { +} + +class Static extends Modifier { +} + +class StrictFp extends Modifier { +} + +class Synchronized extends Modifier { +} + +class Transient extends Modifier { +} + +class TwoState extends Modifier { +} + +abstract class VisibilityModifier extends Modifier { +} + +class Volatile extends Modifier {} + +class ArrayInitializer extends JavaNonTerminalProgramElement { + KeYJavaType kjt; +} + +abstract class Assignment extends Operator { +} + +abstract class Expression { +} + +abstract class ExpressionStatement { +} + +abstract class Operator extends JavaNonTerminalProgramElement { +} + +class ParenthesizedExpression extends Operator {} + +class PassiveExpression extends ParenthesizedExpression {} + +abstract class AbstractIntegerLiteral extends Literal {} + +class BooleanLiteral extends Literal {} + +class CharLiteral extends AbstractIntegerLiteral {} + +class DoubleLiteral extends Literal { + + String value; +} + +class EmptyMapLiteral extends Literal { +} + +class EmptySeqLiteral extends Literal { +} + +class EmptySetLiteral extends Literal { +} + +class FloatLiteral extends Literal { + + String value; +} + +class FreeLiteral extends Literal { +} + +class IntLiteral extends AbstractIntegerLiteral { +} + +abstract class Literal extends JavaProgramElement {} + +class LongLiteral extends AbstractIntegerLiteral {} + +class RealLiteral extends Literal { + String value; +} + +class StringLiteral extends Literal { + String value; +} + +class BinaryAnd extends BinaryOperator { +} + +class BinaryAndAssignment extends Assignment { +} + +class BinaryNot extends Operator { +} + +abstract class BinaryOperator extends Operator { +} + +class BinaryOr extends BinaryOperator { +} + +class BinaryOrAssignment extends Assignment { +} + +class BinaryXOr extends BinaryOperator { +} + +class BinaryXOrAssignment extends Assignment { +} + +abstract class ComparativeOperator extends Operator { +} + +class Conditional extends Operator { +} + +class CopyAssignment extends Assignment { +} + +class DLEmbeddedExpression extends Operator { +} + +class Divide extends BinaryOperator { +} + +class DivideAssignment extends Assignment { +} + +class Equals extends ComparativeOperator { +} + +class ExactInstanceof extends TypeOperator { +} + +class GreaterOrEquals extends ComparativeOperator { +} + +class GreaterThan extends ComparativeOperator { +} + +class Instanceof extends TypeOperator { +} + +class Intersect extends BinaryOperator { +} + +class LessOrEquals extends ComparativeOperator { +} + +class LessThan extends ComparativeOperator { +} + +class LogicalAnd extends Operator { +} + +class LogicalNot extends Operator { +} + +class LogicalOr extends Operator { +} + +class Minus extends BinaryOperator { +} + +class MinusAssignment extends Assignment { +} + +class Modulo extends BinaryOperator { +} + +class ModuloAssignment extends Assignment { +} + +class Negative extends Operator { +} + +class New extends TypeOperator { + + ClassDeclaration anonymousClass; + + ReferencePrefix accessPath; +} + +class NewArray extends TypeOperator { + + int dimensions; + + ArrayInitializer arrayInitializer; +} + +class NotEquals extends ComparativeOperator { +} + +class Plus extends BinaryOperator { +} + +class PlusAssignment extends Assignment { +} + +class Positive extends Operator { +} + +class PostDecrement extends Assignment { +} + +class PostIncrement extends Assignment { +} + +class PreDecrement extends Assignment { +} + +class PreIncrement extends Assignment { +} + +class ShiftLeft extends Operator { +} + +class ShiftLeftAssignment extends Assignment { +} + +class ShiftRight extends Operator { +} + +class ShiftRightAssignment extends Assignment { +} + +class Subtype extends BinaryOperator { +} + +class Times extends BinaryOperator { +} + +class TimesAssignment extends Assignment { +} + +class TypeCast extends TypeOperator { +} + +abstract class TypeOperator extends Operator { + + TypeReference typeReference; +} + +class UnsignedShiftRight extends Operator { +} + +class UnsignedShiftRightAssignment extends Assignment { +} + +class AllFields extends Operator { +} + +class AllObjects extends Operator { +} + +class SeqConcat extends BinaryOperator { +} + +class SeqGet extends Operator { +} + +class SeqIndexOf extends Operator { +} + +class SeqLength extends Operator { +} + +class SeqPut extends Operator { +} + +class SeqReverse extends Operator { +} + +class SeqSingleton extends Operator { +} + +class SeqSub extends Operator { +} + +class SetMinus extends BinaryOperator { +} + +class SetUnion extends BinaryOperator { +} + +class Singleton extends Operator { +} + +class ArrayLengthReference extends JavaNonTerminalProgramElement { + + ReferencePrefix prefix; +} + +class ArrayReference extends JavaNonTerminalProgramElement { + + ReferencePrefix prefix; + + List inits; +} + +abstract class ConstructorReference { +} + +class ExecutionContext extends JavaNonTerminalProgramElement { + + TypeReference classContext; + + ReferencePrefix runtimeInstance; +} + +class FieldReference extends VariableReference { + + ReferencePrefix prefix; +} + +abstract class IExecutionContext { +} + +abstract class MemberReference { +} + +class MetaClassReference extends JavaNonTerminalProgramElement { + + TypeReference typeReference; +} + +abstract class MethodName { +} + +abstract class MethodOrConstructorReference { +} + +class MethodReference extends JavaNonTerminalProgramElement { + + ReferencePrefix prefix; + + MethodName name; + + List arguments; +} + +abstract class NameReference { +} + +class PackageReference extends JavaNonTerminalProgramElement { + + ReferencePrefix prefix; + + ProgramElementName name; +} + +abstract class PackageReferenceContainer { +} + +abstract class ReferencePrefix { +} + +abstract class ReferenceSuffix { +} + +class SchemaTypeReference extends TypeReferenceImp { +} + +class SchematicFieldReference extends FieldReference { + + SchemaVariable schemaVariable; +} + +abstract class SpecialConstructorReference extends JavaNonTerminalProgramElement { + + List arguments; +} + +class SuperConstructorReference extends SpecialConstructorReference { + + ReferencePrefix prefix; +} + +class SuperReference extends JavaNonTerminalProgramElement { +} + +class ThisConstructorReference extends SpecialConstructorReference { +} + +class ThisReference extends JavaNonTerminalProgramElement { +} + +class TypeRef extends TypeReferenceImp { +} + +abstract class TypeReference { +} + +abstract class TypeReferenceContainer { +} + +abstract class TypeReferenceImp extends JavaNonTerminalProgramElement { + + ReferencePrefix prefix; + + int dimensions; + + ProgramElementName name; +} + +abstract class TypeReferenceInfix { +} + +class VariableReference extends JavaNonTerminalProgramElement { + + ProgramVariable variable; +} + +class Assert extends JavaStatement { +} + +abstract class Branch {} + +abstract class BranchImp extends JavaNonTerminalProgramElement { +} + +abstract class BranchStatement extends JavaStatement {} + +class Break extends LabelJumpStatement {} + +class Case extends BranchImp { + Expression expression; + List body; +} + +class Catch extends BranchImp { + ParameterDeclaration parameter; + StatementBlock body; +} + +class CatchAllStatement extends JavaNonTerminalProgramElement {} + +class Ccatch extends BranchImp {} + +class Continue extends LabelJumpStatement {} + +class Default extends BranchImp { + List body; +} + +class Do extends LoopStatement { +} + +class Else extends BranchImp { + + Statement body; +} + +class EmptyStatement extends JavaProgramElement { +} + +class EnhancedFor extends LoopStatement { +} + +class Exec extends BranchStatement { +} + +abstract class ExpressionJumpStatement extends JumpStatement { + + Expression expression; +} + +class Finally extends BranchImp { + + StatementBlock body; +} + +class For extends LoopStatement { +} + +class ForUpdates extends JavaNonTerminalProgramElement { + + List updates; +} + +class Guard extends JavaNonTerminalProgramElement { + + Expression expr; +} + +abstract class IForUpdates {} +abstract class IGuard {} +abstract class ILoopInit {} + +class If extends BranchStatement { + Expression condition; + Statement thenBranch; + Statement elseBranch; +} + +abstract class JavaStatement extends JavaNonTerminalProgramElement { +} + +class JmlAssert extends JavaStatement { +} + +abstract class JumpStatement extends JavaStatement { +} + +abstract class LabelJumpStatement extends JumpStatement { + + Label name; +} + +class LabeledStatement extends JavaStatement { + Label name; + Statement body; +} + +class LoopInit extends JavaNonTerminalProgramElement { + + List inits; +} + +class LoopScopeBlock extends JavaStatement { +} + +abstract class LoopStatement extends JavaStatement { + + ILoopInit inits; + + IForUpdates updates; + + IGuard guard; + + Statement body; + + ImmutableList attachedJml; +} + +class MergePointStatement extends JavaStatement { + + IProgramVariable identifier; +} + +class MethodBodyStatement extends JavaNonTerminalProgramElement { +} + +class MethodFrame extends JavaStatement { +} + +class Return extends ExpressionJumpStatement { +} + +class SetStatement extends JavaStatement { +} + +class Switch extends BranchStatement { + + List branches; + + Expression expression; +} + +class SynchronizedBlock extends JavaStatement { + + Expression expression; + + StatementBlock body; +} + +class Then extends BranchImp { +} + +class Throw extends ExpressionJumpStatement { +} + +class TransactionStatement extends JavaStatement { +} + +class Try extends BranchStatement { +} + +class While extends LoopStatement { +} + +abstract class ProgramConstruct { +} + +class ProgramElementName extends Name { +} + +abstract class ProgramPrefix { +} + +abstract class IndProgramElementName extends ProgramElementName { +} + +class PermIndProgramElementName extends IndProgramElementName { +} + +class TempIndProgramElementName extends IndProgramElementName { +} + +abstract class IProgramMethod { +} + +abstract class IProgramVariable { +} + +class LocationVariable extends ProgramVariable { +} + +class ProgramConstant extends ProgramVariable { +} + +class ProgramMethod extends ObserverFunction { +} + +class ProgramSV extends JOperatorSV { +} + +abstract class ProgramVariable extends JAbstractSortedOperator { +} + +abstract class AbstractProgramElement { +} + +class ArrayLength extends ProgramTransformer { +} + +class ArrayPostDecl extends ProgramTransformer { +} + +class ConstructorCall extends ProgramTransformer { +} + +class CreateObject extends ProgramTransformer { +} + +class DoBreak extends ProgramTransformer { +} + +class EnhancedForElimination extends ProgramTransformer { +} + +class EvaluateArgs extends ProgramTransformer { +} + +class ExpandMethodBody extends ProgramTransformer { +} + +class ForInitUnfoldTransformer extends ProgramTransformer { +} + +class ForToWhile extends ProgramTransformer { +} + +abstract class InitArray extends ProgramTransformer { +} + +class InitArrayCreation extends InitArray { +} + +class IsStatic extends ProgramTransformer {} + +class MethodCall extends ProgramTransformer { + MethodReference methRef; + ReferencePrefix newContext; + ProgramVariable pvar; + List arguments; + KeYJavaType staticPrefixType; +} + +class MultipleVarDecl extends ProgramTransformer { +} + +class PostWork extends ProgramTransformer { +} + +abstract class ProgramTransformer extends JavaNonTerminalProgramElement { +} + +class ReattachLoopInvariant extends ProgramTransformer { +} + +class SpecialConstructorCall extends ProgramTransformer { +} + +class StaticInitialisation extends ProgramTransformer { +} + +class SwitchToIf extends ProgramTransformer { +} + +class TypeOf extends ProgramTransformer { +} + +class Unpack extends ProgramTransformer { +} + +class UnwindLoop extends ProgramTransformer { +} diff --git a/key.ncore.java/src/generator/java/org/key_project/ncore/java/Generator.java b/key.ncore.java/src/generator/java/org/key_project/ncore/java/Generator.java new file mode 100644 index 00000000000..197d66ed381 --- /dev/null +++ b/key.ncore.java/src/generator/java/org/key_project/ncore/java/Generator.java @@ -0,0 +1,530 @@ +package org.key_project.ncore.java; + +import com.github.javaparser.ParserConfiguration; +import com.github.javaparser.StaticJavaParser; +import com.github.javaparser.ast.CompilationUnit; +import com.github.javaparser.ast.NodeList; +import com.github.javaparser.ast.body.*; +import com.github.javaparser.ast.expr.*; +import com.github.javaparser.ast.nodeTypes.NodeWithName; +import com.github.javaparser.ast.nodeTypes.NodeWithSimpleName; +import com.github.javaparser.ast.stmt.BlockStmt; +import com.github.javaparser.ast.stmt.ExpressionStmt; +import com.github.javaparser.ast.stmt.ReturnStmt; +import com.github.javaparser.ast.type.ClassOrInterfaceType; +import com.github.javaparser.ast.type.PrimitiveType; +import com.github.javaparser.ast.type.Type; +import com.github.javaparser.utils.SourceRoot; +import com.google.common.collect.Multimap; +import com.google.common.collect.MultimapBuilder; +import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.NullMarked; +import org.jspecify.annotations.Nullable; + +import java.io.File; +import java.nio.file.Path; +import java.nio.file.Paths; +import java.util.ArrayList; +import java.util.List; +import java.util.TreeMap; +import java.util.concurrent.Callable; +import java.util.stream.Collectors; + +import static com.github.javaparser.StaticJavaParser.*; +import static com.github.javaparser.ast.Modifier.DefaultKeyword.*; + +/** + * + * @author Alexander Weigl + * @version 1 (4/11/26) + */ +@SuppressWarnings("OptionalGetWithoutIsPresent") +public class Generator implements Callable { + public static final Path ROOT = Paths.get("key.ncore.java/src/generated/java"); + CompilationUnit metaModel; + + List nodeSteps = new ArrayList<>(64); + List preSteps = new ArrayList<>(64); + + public static void main(String[] args) throws Exception { + new Generator().call(); + } + + public Generator() { + preSteps.add(pushFieldsDown); + addStep(Generator::setPackage); + addStep(Generator::processFields); + addStep(Generator::addAllFieldsConstructor); + addStep(Generator::addCopyConstructor); + addStep(Generator::addEquals); + addStep(Generator::ToString); + addStep(Generator::addHashCode); + + addStep(Generator::addWiths); + + addStep(Generator::addBuilder); + addStep(Generator::addOverrideConstructor); + addStep(Generator::addOverrideConstructor2); + addStep(Generator::addGetProperties); + addStep(Generator::processFieldsAccessor); + } + + private static void addBuilder(ClassOrInterfaceDeclaration target) { + if(target.isInterface()) return; + + var builder = new ClassOrInterfaceDeclaration(); + builder.setName("Builder"); + builder.addModifier(PUBLIC, FINAL, STATIC); + + for (var field : target.getFields()) { + for (var variable : field.variables()) { + var f = builder.addField(variable.getType().clone(), + variable.getNameAsString(), PUBLIC); + f.addAnnotation(Nullable.class); + } + } + + var build = builder.addMethod("build", PUBLIC); + build.setType(new ClassOrInterfaceType(null, target.getNameAsString())); + + var args = builder.getFields().stream().flatMap(it -> it.variables().stream()) + .map(it -> (Expression) it.getNameAsExpression()) + .collect(Collectors.toList()); + build.getBody().get().addStatement(new ReturnStmt( + new ObjectCreationExpr(null, + new ClassOrInterfaceType(null, target.getNameAsString()), + new NodeList<>(args)))); + + builder.getFields().stream().flatMap(it -> it.variables().stream()).forEach(it -> { + var m = builder.addMethod(it.getNameAsString(), PUBLIC); + m.addParameter(new Parameter(it.getType().clone(), it.getNameAsString())); + m.setType(new ClassOrInterfaceType(null, "Builder")); + m.getBody().get().addStatement("this.%s=%s;".formatted(it.getNameAsString(), it.getNameAsString())); + m.getBody().get().addStatement("return this;"); + }); + + + builder.getFields().stream().flatMap(it -> it.variables().stream()) + .filter(Generator::isList) + .forEach(it -> { + var m = builder.addMethod(it.getNameAsString(), PUBLIC); + var t = it.getType().asClassOrInterfaceType().getTypeArguments().get().getFirst(); + m.addParameter(new Parameter(t.clone(), it.getNameAsString())); + m.setType(new ClassOrInterfaceType(null, "Builder")); + m.getBody().get().addStatement("if(this.%s==null) this.%s = new ArrayList<>();".formatted(it.getNameAsString(), it.getNameAsString())); + m.getBody().get().addStatement("this.%s.add(%s);".formatted(it.getNameAsString(), it.getNameAsString())); + m.getBody().get().addStatement("return this;"); + }); + + target.addMember(builder); + + var tb = target.addMethod("builder", PUBLIC); + tb.setType(new ClassOrInterfaceType(null, "Builder")); + final var b = tb.getBody().get(); + b.addStatement("Builder b = new Builder();"); + builder.getFields().stream().flatMap(it -> it.variables().stream()).forEach(it -> + b.addStatement("b.%s = %s;".formatted(it.getNameAsString(), it.getNameAsString()))); + b.addStatement("return b;"); + } + + private static boolean isList(VariableDeclarator type) { + return type.getTypeAsString().startsWith("List<"); + } + + private static void addWiths(ClassOrInterfaceDeclaration target) { + target.getFields().stream() + .flatMap(it -> it.getVariables().stream()).forEach(it -> { + var args = + target.getFields().stream() + .flatMap(f -> f.getVariables().stream()) + .map(v -> { + if (v == it) { + return (Expression) v.getNameAsExpression(); + } else { + return new MethodCallExpr(null, v.getNameAsString()); + } + }).toList(); + + var m = target.addMethod("with" + it.getNameAsString(), PUBLIC); + m.addParameter(new Parameter(it.getType().clone(), it.getNameAsString())); + m.setType(new ClassOrInterfaceType(null, target.getNameAsString())); + m.getBody().get().addStatement(new ReturnStmt( + new ObjectCreationExpr(null, + new ClassOrInterfaceType(null, target.getNameAsString()), + new NodeList<>(args)))); + }); + } + + private static void addEquals(ClassOrInterfaceDeclaration target) { + if (target.isAbstract()) { + return; + } + MethodDeclaration equals = target.addMethod("equals", PUBLIC); + equals.addModifier(FINAL); + equals.addAnnotation(Override.class); + equals.setType(Boolean.TYPE); + final var o = getNullableObject(); + equals.getParameters().add(o); + BlockStmt body = equals.getBody().get(); + body.addStatement(parseStatement("if(this == o) return true;")); + body.addStatement(parseStatement("if(!(o instanceof %s that)) return false;".formatted(target.getNameAsString()))); + Expression equalFields = target.getFields().stream() + .flatMap(it -> it.getVariables().stream()) + .map(it -> callObjects("equals", it.getNameAsExpression(), + new FieldAccessExpr(new NameExpr("that"), it.getNameAsString()))) + .reduce((a, b) -> new BinaryExpr(a, b, BinaryExpr.Operator.AND)) + .orElse(new BooleanLiteralExpr(true)); + body.addStatement(new ReturnStmt(equalFields)); + } + + private static void addHashCode(ClassOrInterfaceDeclaration target) { + if (target.isAbstract()) { + return; + } + + MethodDeclaration hashCode = target.addMethod("hashCode", PUBLIC); + hashCode.addModifier(FINAL); + hashCode.addAnnotation(Override.class); + hashCode.setType(Integer.TYPE); + Expression[] args = target.getFields() + .stream() + .flatMap(it -> it.getVariables().stream()) + .map(NodeWithSimpleName::getNameAsExpression) + .map(it -> (Expression) it) + .toArray(Expression[]::new); + + if (args.length == 0) + assert false : "No defined fields"; + else + hashCode.getBody().get().addStatement(new ReturnStmt( + callObjects("hash", args) + )); + } + + private static void ToString(ClassOrInterfaceDeclaration clazz) { + if (clazz.isAbstract()) { + return; + } + + MethodDeclaration toString = clazz.addMethod("toString", PUBLIC, FINAL); + toString.addAnnotation(Override.class); + toString.setType(String.class); + var parameters = clazz.getFields().stream().flatMap(it -> it.getVariables().stream()).toList(); + var sb = (clazz.getNameAsString() + "[") + + parameters.stream().map(NodeWithSimpleName::getNameAsString).map(it -> it + "=%s") + .collect(Collectors.joining(", ")) + "]"; + + var args = parameters.stream().map(NodeWithSimpleName::getNameAsExpression) + .map(it -> (Expression) it).toList(); + toString.getBody().get().addStatement(new ReturnStmt( + new MethodCallExpr(new StringLiteralExpr(sb), "formatted", new NodeList<>(args)))); + } + + private static Expression callObjects(String method, Expression... args) { + return new MethodCallExpr(new NameExpr("Objects"), method, new NodeList<>(args)); + } + + private static @NonNull Parameter getNullableObject() { + Type tObject = StaticJavaParser.parseType("java.lang.Object"); + return new Parameter(new NodeList<>(), tObject, new SimpleName("o")); + } + + private static void addAllFieldsConstructor(ClassOrInterfaceDeclaration target) { + if (target.isInterface()) { + return; + } + ConstructorDeclaration constr = new ConstructorDeclaration(); + var body = constr.getBody().get(); + var params = constr.getParameters(); + constr.setName(target.getNameAsString()); + constr.setModifiers(PUBLIC); + + for (var field : target.getFields()) { + for (var variable : field.getVariables()) { + params.add(new Parameter(variable.getType().clone(), variable.getNameAsString())); + body.addStatement( + new ExpressionStmt(new AssignExpr( + new FieldAccessExpr(new ThisExpr(), variable.getNameAsString()), + variable.getNameAsExpression(), AssignExpr.Operator.ASSIGN + ))); + } + } + + + target.addMember(constr); + } + + private static void addOverrideConstructor(ClassOrInterfaceDeclaration target) { + if (target.isInterface()) { + return; + } + + ConstructorDeclaration constr = target.addConstructor(PUBLIC); + var body = constr.getBody().get(); + var params = constr.getParameters(); + constr.setName(target.getNameAsString()); + params.add(new Parameter(new ClassOrInterfaceType(null, target.getNameAsString()), "other")); + + params.add(new Parameter(parseType("Properties"), "map")); + + var args = target.getFields().stream().flatMap(it -> it.getVariables().stream()) + .map(NodeWithSimpleName::getNameAsString) + .map(it -> + (Expression) parseExpression("map.get(PROPERTY_%s, other.%s)".formatted(it.toUpperCase(), it))) + .toList(); + body.addStatement(new MethodCallExpr(null, "this", new NodeList<>(args))); + } + + private static void addOverrideConstructor2(ClassOrInterfaceDeclaration target) { + if (target.isInterface()) { + return; + } + + ConstructorDeclaration constr = target.addConstructor(PUBLIC); + var body = constr.getBody().get(); + var params = constr.getParameters(); + constr.setName(target.getNameAsString()); + params.add(new Parameter(parseType("Properties"), "map")); + + var args = target.getFields().stream().flatMap(it -> it.getVariables().stream()) + .map(NodeWithSimpleName::getNameAsString) + .map(it -> + (Expression) parseExpression("map.get(PROPERTY_%s)".formatted(it.toUpperCase()))) + .toList(); + body.addStatement(new MethodCallExpr(null, "this", new NodeList<>(args))); + } + + + private static void addGetProperties(ClassOrInterfaceDeclaration target) { + if (target.isInterface()) { + return; + } + + var method = target.addMethod("properties", PUBLIC); + method.setType("Properties"); + var body = method.getBody().get(); + + + body.addStatement("Properties p = new DefaultProperties();"); + target.getFields().stream() + .flatMap(it -> it.getVariables().stream()) + .forEach(variable -> body.addStatement("p.set(PROPERTY_%s, %s());".formatted(variable.getNameAsString().toUpperCase(), variable.getNameAsString()))); + body.addStatement("return p;"); + } + + + private static void addCopyConstructor(ClassOrInterfaceDeclaration target) { + if (target.isInterface()) { + return; + } + + ConstructorDeclaration constr = target.addConstructor(PUBLIC); + var body = constr.getBody().get(); + var params = constr.getParameters(); + constr.setName(target.getNameAsString()); + params.add(new Parameter(new ClassOrInterfaceType(null, target.getNameAsString()), "other")); + + /* + for (var field : target.getFields()) { + for (var variable : field.getVariables()) { + //params.add(new Parameter(variable.getType().clone(), variable.getNameAsString())); + body.addStatement( + new ExpressionStmt(new AssignExpr( + new FieldAccessExpr(new ThisExpr(), variable.getNameAsString()), + new FieldAccessExpr(new NameExpr("other"), variable.getNameAsString()), + AssignExpr.Operator.ASSIGN + )) + ); + } + } + */ + + var args = target.getFields().stream().flatMap(it -> it.getVariables().stream()) + .map(NodeWithSimpleName::getNameAsString) + .map(it -> (Expression) new FieldAccessExpr(new NameExpr("other"), it)) + .toList(); + body.addStatement(new MethodCallExpr(null, "this", new NodeList<>(args))); + + } + + static Multimap inheritanceMap = MultimapBuilder.treeKeys().treeSetValues().build(); + static Multimap permittedTypes = MultimapBuilder.treeKeys().treeSetValues().build(); + + private static final PreStep pushFieldsDown = types -> { + TreeMap fields = new TreeMap<>(); + + for (TypeDeclaration decl : types) { + fields.put(decl.getNameAsString(), (ClassOrInterfaceDeclaration) decl); + + var zuper = ((ClassOrInterfaceDeclaration) decl).getExtendedTypes().getOFirst() + .map(NodeWithSimpleName::getNameAsString); + zuper.ifPresent(s -> inheritanceMap.put(decl.getNameAsString(), s)); + } + + // compute transitive closure + boolean changed = true; + while (changed) { + changed = false; + for (var clazz : inheritanceMap.keySet()) { + final var strings = new ArrayList<>(inheritanceMap.get(clazz)); + for (var zuper : strings) { + changed = changed || inheritanceMap.putAll(clazz, inheritanceMap.get(zuper)); + } + } + } + + for (var decl : fields.sequencedValues()) { + if (decl.hasModifier(ABSTRACT)) { + continue; + } + + var newFields = new TreeMap(); + for (var c : inheritanceMap.get(decl.getNameAsString())) { + final var classOrInterfaceDeclaration = fields.get(c); + if (classOrInterfaceDeclaration != null) { + for (FieldDeclaration it : classOrInterfaceDeclaration.getFields()) { + var name = it.getVariable(0).getNameAsString(); + newFields.computeIfAbsent(name, (k) -> { + final var clone = it.clone(); + clone.addAnnotation(Override.class.getName()); + clone.setRange(null); + return clone; + }); + } + } + } + assert newFields.size() <= 10; + decl.getMembers().addAll(newFields.values()); + } + }; + + private void addStep(NodeStep nodeStep) { + nodeSteps.add(nodeStep); + } + + @Override + public Integer call() throws Exception { + var config = new ParserConfiguration(); + config.setStoreTokens(false); + config.setLexicalPreservationEnabled(false); + config.setLanguageLevel(ParserConfiguration.LanguageLevel.JAVA_25); + + StaticJavaParser.setConfiguration(config); + metaModel = StaticJavaParser.parse(new File("key.ncore.java/src/adt/java-ast.java").getAbsoluteFile()); + SourceRoot sourceRoot = new SourceRoot(ROOT); + + final var types = metaModel.getTypes(); + for (var nodeStep : preSteps) { + nodeStep.applyOn(types); + } + + for (var type : types) { + var cu = new CompilationUnit(); + cu.addType(type); + metaModel.getImports().forEach(it -> cu.addImport(it.clone())); + metaModel.addImport("java.lang.Objects"); + metaModel.addImport("java.util.*"); + + for (var nodeStep : nodeSteps) { + nodeStep.applyOn((ClassOrInterfaceDeclaration) type); + } + + sourceRoot.add(cu); + } + + sourceRoot.saveAll(); + return 0; + } + + interface NodeStep { + void applyOn(ClassOrInterfaceDeclaration target); + } + + static void setPackage(ClassOrInterfaceDeclaration target) { + var annotation = target.getAnnotationByName("Package") + .map(NodeWithName::getNameAsString) + .orElse("org.key_project.java.ast"); + + CompilationUnit cu = target.findCompilationUnit().get(); + cu.setPackageDeclaration(annotation); + + cu.setStorage(ROOT.resolve(annotation.replace(".", "/")) + .resolve(target.getNameAsString() + ".java")); + + target.addAnnotation(NullMarked.class); + target.addModifier(PUBLIC); + + boolean isAbstract = target.isAbstract(); + if (isAbstract) { + target.setInterface(true); + for (var s : permittedTypes.get(target.getNameAsString())) { + target.getPermittedTypes().add(new ClassOrInterfaceType(null, s)); + } + } else { + target.addModifier(FINAL); + } + } + + + private static void processFieldsAccessor(ClassOrInterfaceDeclaration target) { + if (target.isInterface()) return; + + target.findCompilationUnit().get().addImport("org.key_project.java.ast.Property"); + + for (var field : target.getFields()) { + for (var variable : field.getVariables()) { + final var dataKey = new ClassOrInterfaceType(null, new SimpleName("Property"), + new NodeList<>(toBoxType(variable.getType().clone()))); + var f = target.addField( + dataKey, "PROPERTY_" + variable.getNameAsString().toUpperCase(), PUBLIC, STATIC, FINAL); + f.getVariables().getFirst().setInitializer("new Property<>(\"%s\")".formatted(variable.getNameAsString())); + } + } + } + + private static Type toBoxType(Type clone) { + if (clone instanceof PrimitiveType pt) { + return pt.toBoxedType(); + } + return clone; + } + + static void processFields(ClassOrInterfaceDeclaration target) { + boolean isAbstract = target.isAbstract(); + + for (var field : target.getFields()) { + if (isAbstract) { + field.remove(); + } else { + field.setModifiers(PRIVATE, FINAL); + } + + for (var variable : field.getVariables()) { + var getter = target.addMethod(variable.getNameAsString()); + getter.setType(variable.getType().clone()); + + var nullable = field.getAnnotationByName("Nullable"); + if (nullable.isPresent()) { + getter.addAndGetAnnotation(Nullable.class); + } + + if (isAbstract) { + //getter.addModifier(Modifier.DefaultKeyword.ABSTRACT); + getter.setBody(null); + } else { + getter.getBody().get().addStatement(new ReturnStmt(variable.getNameAsExpression())); + getter.addModifier(PUBLIC, FINAL); + } + field.getAnnotationByName("Override") + .ifPresent(it -> { + it.remove(); + getter.addAnnotation(it); + }); + } + } + } + + private interface PreStep { + void applyOn(NodeList> types); + } +} \ No newline at end of file diff --git a/key.ncore.java/src/generator/java/org/key_project/ncore/java/ReadAllHierarchy.java b/key.ncore.java/src/generator/java/org/key_project/ncore/java/ReadAllHierarchy.java new file mode 100644 index 00000000000..815478ac7fb --- /dev/null +++ b/key.ncore.java/src/generator/java/org/key_project/ncore/java/ReadAllHierarchy.java @@ -0,0 +1,795 @@ +package org.key_project.ncore.java; + +import com.github.javaparser.ast.body.ClassOrInterfaceDeclaration; +import com.github.javaparser.ast.type.ClassOrInterfaceType; +import de.uka.ilkd.key.java.ast.*; +import de.uka.ilkd.key.java.ast.ccatch.*; +import de.uka.ilkd.key.java.ast.declaration.*; +import de.uka.ilkd.key.java.ast.declaration.modifier.*; +import de.uka.ilkd.key.java.ast.expression.*; +import de.uka.ilkd.key.java.ast.expression.literal.*; +import de.uka.ilkd.key.java.ast.expression.operator.*; +import de.uka.ilkd.key.java.ast.expression.operator.adt.*; +import de.uka.ilkd.key.java.ast.reference.*; +import de.uka.ilkd.key.java.ast.statement.*; +import de.uka.ilkd.key.logic.ProgramConstruct; +import de.uka.ilkd.key.logic.ProgramElementName; +import de.uka.ilkd.key.logic.ProgramPrefix; +import de.uka.ilkd.key.logic.VariableNamer; +import de.uka.ilkd.key.logic.op.*; +import de.uka.ilkd.key.rule.AbstractProgramElement; +import de.uka.ilkd.key.rule.metaconstruct.*; + +import java.io.File; +import java.io.FileNotFoundException; +import java.io.PrintWriter; +import java.lang.reflect.AccessFlag; +import java.util.*; +import java.util.stream.Collectors; + +import static de.uka.ilkd.key.java.ast.declaration.modifier.Modifiers.*; + + +/** + * + * @author Alexander Weigl + * @version 1 (4/11/26) + */ +public class ReadAllHierarchy { + static Set> allClasses = new HashSet<>(List.of( + GreaterThan.class, + ExecutionContext.class, + ArrayLength.class, + SuperReference.class, + ProgramTransformer.class, + Instanceof.class, + ArrayInitializer.class, + ProgramSV.class, + Exec.class, + ThisReference.class, + MethodCall.class, + FieldDeclaration.class, + ForInitUnfoldTransformer.class, + SchemaTypeReference.class, + EnhancedForElimination.class, + IProgramVariable.class, + ClassDeclaration.class, + ContextStatementBlock.class, + MethodReference.class, + SpecialConstructorCall.class, + FloatLiteral.class, + TypeDeclaration.class, + PackageReference.class, + SuperConstructorReference.class, + SeqSub.class, + Positive.class, + SchematicFieldReference.class, + TypeCast.class, + ForToWhile.class, + LogicalOr.class, + LabelJumpStatement.class, + ReattachLoopInvariant.class, + Switch.class, + InterfaceDeclaration.class, + JML_NULLABLE_BY_DEFAULT.class, + PostDecrement.class, + Break.class, + TypeDeclaration.class, + CcatchContinueWildcardParameterDeclaration.class, + InitArrayCreation.class, + TypeRef.class, + UnsignedShiftRightAssignment.class, + EnumClassDeclaration.class, + CatchAllStatement.class, + LoopInit.class, + TypeReferenceImp.class, + MethodOrConstructorReference.class, + ForToWhile.class, + FieldReference.class, + PostIncrement.class, + ForToWhile.class, + MultipleVarDecl.class, + EnumClassDeclaration.class, + TypeDeclaration.class, + Break.class, + Conditional.class, + JavaDeclaration.class, + CompilationUnit.class, + PostWork.class, + JML_HELPER.class, + ReattachLoopInvariant.class, + ClassDeclaration.class, + ConstructorDeclaration.class, + LessOrEquals.class, + Modulo.class, + ThisReference.class, + UnwindLoop.class, + ArrayReference.class, + InterfaceDeclaration.class, + UnwindLoop.class, + EnhancedForElimination.class, + MethodCall.class, + PostWork.class, + LocalVariableDeclaration.class, + ReferencePrefix.class, + ExactInstanceof.class, + EvaluateArgs.class, + FieldReference.class, + EnumClassDeclaration.class, + ExpandMethodBody.class, + Switch.class, + Unpack.class, + ContextStatementBlock.class, + SpecialConstructorReference.class, + Exec.class, + ConstructorCall.class, + VariableNamer.IndProgramElementName.class, + IsStatic.class, + ProgramSV.class, + ArrayLength.class, + BranchStatement.class, + PostIncrement.class, + ProgramSV.class, + ForInitUnfoldTransformer.class, + PackageReference.class, + Operator.class, + Label.class, + TypeDeclaration.class, + JML_SPEC_PACKAGE.class, + SwitchToIf.class, + ExpandMethodBody.class, + ExpandMethodBody.class, + Instanceof.class, + Switch.class, + TypeReference.class, + CcatchContinueLabelParameterDeclaration.class, + ForInitUnfoldTransformer.class, + Throws.class, + SuperArrayDeclaration.class, + BinaryOrAssignment.class, + ExpandMethodBody.class, + UnsignedShiftRightAssignment.class, + Equals.class, + ProgramConstruct.class, + ExactInstanceof.class, + NotEquals.class, + PostIncrement.class, + ShiftRight.class, + SuperArrayDeclaration.class, + SchemaTypeReference.class, + TypeReferenceImp.class, + ForToWhile.class, + ConstructorCall.class, + FieldDeclaration.class, + LogicalAnd.class, + EvaluateArgs.class, + ParenthesizedExpression.class, + ConstructorCall.class, + SeqLength.class, + SeqConcat.class, + EnumClassDeclaration.class, + SuperConstructorReference.class, + PackageSpecification.class, + ClassInitializer.class, + ProgramSV.class, + PRIVATE.class, + InitArray.class, + UnwindLoop.class, + ExecutionContext.class, + ProgramConstruct.class, + New.class, + ArrayPostDecl.class, + For.class, + MethodFrame.class, + ForUpdates.class, + SuperArrayDeclaration.class, + Unpack.class, + ArrayLengthReference.class, + LoopInitializer.class, + ClassDeclaration.class, + DoBreak.class, + BranchStatement.class, + InterfaceDeclaration.class, + JavaDeclaration.class, + SetStatement.class, + Finally.class, + Ccatch.class, + EnhancedForElimination.class, + PassiveExpression.class, + SeqGet.class, + ArrayReference.class, + AllFields.class, + MethodDeclaration.class, + SwitchToIf.class, + For.class, + ConstructorCall.class, + ExpressionJumpStatement.class, + Case.class, + LoopScopeBlock.class, + SetMinus.class, + IntLiteral.class, + ThisReference.class, + ProgramTransformer.class, + ShiftRightAssignment.class, + Import.class, + SpecialConstructorCall.class, + PreDecrement.class, + Ghost.class, + LabelJumpStatement.class, + PostDecrement.class, + TypeCast.class, + EvaluateArgs.class, + StaticInitialisation.class, + MethodCall.class, + Unpack.class, + ConstructorReference.class, + ForUpdates.class, + ProgramTransformer.class, + ProgramElement.class, + Then.class, + SynchronizedBlock.class, + ArrayDeclaration.class, + NON_SEALED.class, + ShiftRight.class, + TypeOperator.class, + Extends.class, + GreaterOrEquals.class, + ArrayReference.class, + DoBreak.class, + SuperReference.class, + Abstract.class, + Catch.class, + UnsignedShiftRightAssignment.class, + TypeReferenceImp.class, + TypeOf.class, + LocationVariable.class, + Expression.class, + Transient.class, + AnnotationUseSpecification.class, + ExpandMethodBody.class, + SpecialConstructorReference.class, + BinaryXOr.class, + BinaryAndAssignment.class, + ForToWhile.class, + Equals.class, + PostWork.class, + SwitchToIf.class, + JavaStatement.class, + ArrayDeclaration.class, + MethodReference.class, + ThisConstructorReference.class, + JML_NO_STATE.class, + ProgramSV.class, + MethodDeclaration.class, + DoubleLiteral.class, + EnhancedFor.class, + ProgramConstruct.class, + Default.class, + FreeLiteral.class, + Literal.class, + InheritanceSpecification.class, + JML_PACKAGE.class, + ThisConstructorReference.class, + FieldReference.class, + PUBLIC.class, + SpecialConstructorCall.class, + BinaryXOrAssignment.class, + CcatchReturnValParameterDeclaration.class, + ClassInitializer.class, + Assert.class, + PostWork.class, + Break.class, + InitArrayCreation.class, + TypeDeclaration.class, + Singleton.class, + ExpandMethodBody.class, + Private.class, + CcatchBreakWildcardParameterDeclaration.class, + VariableDeclaration.class, + CreateObject.class, + InitArray.class, + IExecutionContext.class, + SchematicFieldReference.class, + JmlAssert.class, + VariableNamer.IndProgramElementName.class, + SeqPut.class, + Assignment.class, + MethodCall.class, + Try.class, + SeqIndexOf.class, + BinaryOr.class, + ConstructorCall.class, + JML_NON_NULL.class, + JML_SPEC_BIGINT_MATH.class, + ProgramConstruct.class, + Do.class, + CcatchReturnValParameterDeclaration.class, + IsStatic.class, + MethodReference.class, + ExpandMethodBody.class, + PostWork.class, + ConstructorDeclaration.class, + BinaryAnd.class, + If.class, + FieldReference.class, + SuperConstructorReference.class, + VariableNamer.IndProgramElementName.class, + Exec.class, + FieldDeclaration.class, + CreateObject.class, + LessThan.class, + LoopStatement.class, + Import.class, + ProgramConstruct.class, + Case.class, + UnwindLoop.class, + Catch.class, + EmptyMapLiteral.class, + VariableReference.class, + MethodReference.class, + TypeOperator.class, + JML_SPEC_PUBLIC.class, + TypeCast.class, + CreateObject.class, + JavaNonTerminalProgramElement.class, + Intersect.class, + TypeReferenceImp.class, + ArrayPostDecl.class, + PlusAssignment.class, + Times.class, + DoBreak.class, + ABSTRACT.class, + ForInitUnfoldTransformer.class, + ShiftLeftAssignment.class, + Protected.class, + TypeScope.class, + ForInitUnfoldTransformer.class, + IsStatic.class, + ClassDeclaration.class, + LogicalNot.class, + EmptySetLiteral.class, + ProgramSV.class, + Switch.class, + VariableDeclaration.class, + ForToWhile.class, + MultipleVarDecl.class, + SuperArrayDeclaration.class, + StaticInitialisation.class, + ConstructorDeclaration.class, + TypeOf.class, + InitArray.class, + MethodBodyStatement.class, + BinaryXOrAssignment.class, + SpecialConstructorCall.class, + CcatchBreakLabelParameterDeclaration.class, + ClassInitializer.class, + Guard.class, + Statement.class, + InterfaceDeclaration.class, + ConstructorCall.class, + Unpack.class, + MethodDeclaration.class, + ArrayPostDecl.class, + TypeOf.class, + EvaluateArgs.class, + SwitchToIf.class, + MultipleVarDecl.class, + Plus.class, + JumpStatement.class, + Times.class, + BinaryNot.class, + ConstructorDeclaration.class, + ClassDeclaration.class, + SeqIndexOf.class, + FieldSpecification.class, + MethodBodyStatement.class, + ProgramSV.class, + SeqConcat.class, + ModuloAssignment.class, + RealLiteral.class, + BinaryOperator.class, + BinaryXOr.class, + Then.class, + SpecialConstructorCall.class, + For.class, + TimesAssignment.class, + Unpack.class, + StringLiteral.class, + MethodDeclaration.class, + TypeDeclarationContainer.class, + Literal.class, + BooleanLiteral.class, + PreDecrement.class, + STRICTFP.class, + StatementBlock.class, + CcatchContinueLabelParameterDeclaration.class, + MultipleVarDecl.class, + LocalVariableDeclaration.class, + Reference.class, + TypeRef.class, + MultipleVarDecl.class, + ReattachLoopInvariant.class, + MethodDeclaration.class, + MultipleVarDecl.class, + EnhancedFor.class, + JML_INSTANCE.class, + Conditional.class, + UnwindLoop.class, + SpecialConstructorReference.class, + EnhancedForElimination.class, + While.class, + DoBreak.class, + UnsignedShiftRight.class, + MethodFrame.class, + ArrayLengthReference.class, + SpecialConstructorReference.class, + IsStatic.class, + Else.class, + JML_OT_REP.class, + ProgramTransformer.class, + MethodCall.class, + NameReference.class, + ForUpdates.class, + ConstructorCall.class, + ConstructorDeclaration.class, + MethodReference.class, + Assert.class, + SwitchToIf.class, + ArrayPostDecl.class, + CopyAssignment.class, + FieldSpecification.class, + InitArrayCreation.class, + UnwindLoop.class, + Exec.class, + TypeOf.class, + SeqIndexOf.class, + TypeRef.class, + VOLATILE.class, + EvaluateArgs.class, + SEALED.class, + LogicalNot.class, + DoBreak.class, + CcatchContinueParameterDeclaration.class, + ProgramSV.class, + Modulo.class, + EnhancedForElimination.class, + ProgramConstruct.class, + ProgramMethod.class, + MethodName.class, + Default.class, + ProgramTransformer.class, + JML_CODE.class, + ModuloAssignment.class, + ShiftLeft.class, + Negative.class, + Case.class, + NewArray.class, + Ccatch.class, + Switch.class, + MethodCall.class, + ProgramConstant.class, + PackageReferenceContainer.class, + BinaryOrAssignment.class, + TypeReferenceInfix.class, + ComparativeOperator.class, + DoBreak.class, + PreDecrement.class, + UnsignedShiftRightAssignment.class, + InitArrayCreation.class, + JML_SPEC_PRIVATE.class, + StatementBlock.class, + ProgramConstruct.class, + FieldDeclaration.class, + FieldReference.class, + ExpandMethodBody.class, + PROTECTED.class, + Finally.class, + SuperArrayDeclaration.class, + Do.class, + AbstractIntegerLiteral.class, + MethodCall.class, + ExpandMethodBody.class, + Extends.class, + SchematicFieldReference.class, + StaticInitialisation.class, + TypeOf.class, + JML_CODE_JAVA_MATH.class, + LoopStatement.class, + SeqPut.class, + SpecialConstructorReference.class, + TypeCast.class, + JML_STRICTLY_PURE.class, + DLEmbeddedExpression.class, + ReattachLoopInvariant.class, + TypeRef.class, + IProgramMethod.class, + CcatchContinueParameterDeclaration.class, + PreIncrement.class, + TypeOf.class, + MergePointStatement.class, + CharLiteral.class, + ModuloAssignment.class, + ConstructorReference.class, + JML_UNPARSABLE_MODIFIERS.class, + MultipleVarDecl.class, + PostWork.class, + SchemaTypeReference.class, + ArrayPostDecl.class, + ScopeDefiningElement.class, + JavaStatement.class, + CharLiteral.class, + Divide.class, + TypeRef.class, + InheritanceSpecification.class, + ComparativeOperator.class, + SetMinus.class, + EmptyStatement.class, + SwitchToIf.class, + SchematicFieldReference.class, + DoBreak.class, + JML_NULLABLE.class, + SeqReverse.class, + Try.class, + LoopInit.class, + ExpressionContainer.class, + IsStatic.class, + ProgramConstruct.class, + New.class, + EmptySetLiteral.class, + ForInitUnfoldTransformer.class, + BinaryOperator.class, + LabeledStatement.class, + MinusAssignment.class, + Operator.class, + MethodDeclaration.class, + MethodReference.class, + Extends.class, + ForToWhile.class, + IsStatic.class, + GreaterOrEquals.class, + Native.class, + ShiftLeftAssignment.class, + LabeledStatement.class, + ArrayReference.class, + PackageReference.class, + Unpack.class, + Minus.class, + MemberDeclaration.class, + SpecialConstructorCall.class, + Divide.class, + MemberReference.class, + TypeReference.class, + InitArray.class, + SchematicFieldReference.class, + ExpandMethodBody.class, + Throws.class, + IForUpdates.class, + Volatile.class, + SuperReference.class, + StaticInitialisation.class, + ExpressionStatement.class, + TypeRef.class, + SchematicFieldReference.class, + InheritanceSpecification.class, + Catch.class, + LogicalOr.class, + ModuloAssignment.class, + Import.class, + Catch.class, + ProgramElementName.class, + InterfaceDeclaration.class, + Instanceof.class, + New.class, + Continue.class, + ProgramSV.class, + SchematicFieldReference.class, + Implements.class, + BinaryAnd.class, + ShiftLeftAssignment.class, + PreDecrement.class, + Ccatch.class, + Static.class, + Return.class, + TRANSIENT.class, + PackageSpecification.class, + TypeOperator.class, + TypeReferenceImp.class, + Branch.class, + Operator.class, + Exec.class, + ReattachLoopInvariant.class, + Divide.class, + AllFields.class, + SeqLength.class, + ForToWhile.class, + NamedProgramElement.class, + JML_NON_NULL_ELEMENTS.class, + MethodFrame.class, + VariableSpecification.class, + BranchImp.class, + CreateObject.class, + Try.class, + BinaryOperator.class, + ProgramConstant.class, + ProgramVariable.class, + Switch.class, + MinusAssignment.class, + PostIncrement.class, + SeqReverse.class, + SetUnion.class, + MethodFrame.class, + Guard.class, + JML_PURE.class, + CcatchReturnValParameterDeclaration.class, + PlusAssignment.class, + LessOrEquals.class, + InitArray.class, + Assert.class, + EnhancedForElimination.class, + EnhancedForElimination.class, + SchematicFieldReference.class, + LogicalAnd.class, + JML_SPEC_PROTECTED.class, + Equals.class, + ConstructorReference.class, + ConstructorDeclaration.class, + ShiftLeft.class, + SwitchToIf.class, + SuperConstructorReference.class, + Guard.class, + ArrayDeclaration.class, + ProgramVariable.class, + ProgramMethod.class, + IsStatic.class, + IsStatic.class, + MergePointStatement.class, + PostDecrement.class, + For.class, + StaticInitialisation.class, + ProgramTransformer.class, + MultipleVarDecl.class, + SchemaTypeReference.class, + EnumClassDeclaration.class, + TypeRef.class, + FieldDeclaration.class, + FINAL.class, + MetaClassReference.class, + SeqSingleton.class, + LocalVariableDeclaration.class, + IGuard.class, + ProgramVariableName.class, + ProgramConstruct.class, + SchemaTypeReference.class, + Else.class, + ProgramConstruct.class, + Continue.class, + TypeRef.class, + TypeRef.class, + ReattachLoopInvariant.class, + ConstructorCall.class, + EnumClassDeclaration.class, + Do.class, + MethodCall.class, + BinaryOrAssignment.class, + ArrayLengthReference.class, + Positive.class, + SchematicFieldReference.class, + PostWork.class, + EmptyStatement.class, + SpecialConstructorCall.class, + Break.class, + ForUpdates.class, + ArrayPostDecl.class, + EvaluateArgs.class, + InitArray.class, + MethodDeclaration.class, + TypeReferenceImp.class, + Unpack.class, + InitArray.class, + TimesAssignment.class, + MethodReference.class, + ReattachLoopInvariant.class, + ProgramConstruct.class, + IsStatic.class, + JavaDeclaration.class, + Catch.class, + DivideAssignment.class, + ProgramPrefix.class, + SuperReference.class, + LabelJumpStatement.class, + Throw.class, + TypeReference.class, + CatchAllStatement.class, + InitArray.class, + ClassInitializer.class, + TypeRef.class, + BranchImp.class, + TransactionStatement.class, + ParameterContainer.class, + VariableScope.class, + Final.class, + DEFAULT.class, + TRANSITIVE.class, + StatementContainer.class, + NATIVE.class, + TypeReferenceContainer.class, + TerminalProgramElement.class, + SYNCHRONIZED.class, + JML_OT_READ_ONLY.class, + NoState.class, + Modifier.class, + VisibilityModifier.class, + CcatchReturnParameterDeclaration.class, + VariableNamer.PermIndProgramElementName.class, + Subtype.class, + AllObjects.class, + Declaration.class, + JML_CODE_BIGINT_MATH.class, + JavaProgramElement.class, + LongLiteral.class, + ParameterDeclaration.class, + JML_SPEC_JAVA_MATH.class, + TwoState.class, + ILoopInit.class, + Model.class, + ReferenceSuffix.class, + JML_TWO_STATE.class, + CcatchNonstandardParameterDeclaration.class, + StrictFp.class, + EmptySeqLiteral.class, + AbstractProgramElement.class, + Synchronized.class, + JML_NON_NULL_BY_DEFAULT.class, + JML_CODE_SAFE_MATH.class, + Public.class, + JML_SPEC_SAFE_MATH.class, + VariableNamer.TempIndProgramElementName.class, + Modifiers.STATIC.class + )); + + public static void main(String[] args) throws FileNotFoundException { + var all = new TreeSet>(Comparator.comparing(Class::getName)); + all.addAll(allClasses); + + System.out.println(all.size()); + var cu = new com.github.javaparser.ast.CompilationUnit(); + + for (var clazz : all) { + var r = new ClassOrInterfaceDeclaration(); + r.setName(clazz.getSimpleName()); + if (clazz.getSuperclass() != null) { + r.getExtendedTypes().add(new ClassOrInterfaceType(null, clazz.getSuperclass().getSimpleName())); + } + + if(clazz.accessFlags().contains(AccessFlag.ABSTRACT)) { + r.addModifier(com.github.javaparser.ast.Modifier.DefaultKeyword.ABSTRACT); + } + + for (var declaredField : clazz.getDeclaredFields()) { + if (declaredField.isSynthetic() + || declaredField.accessFlags().contains(AccessFlag.STATIC) + || declaredField.accessFlags().contains(AccessFlag.PRIVATE)) + continue; + + String type; + if(declaredField.getType().getTypeParameters().length==0) + type = declaredField.getType().getSimpleName(); + else { + type = declaredField.getGenericType().toString(); + int j = type.lastIndexOf('<'); + int i = type.lastIndexOf('.', j); + type = type.substring(i+1); + } + System.out.println(type); + r.addField(type, declaredField.getName()); + } + + + cu.addType(r); + } + + try (var out = new PrintWriter(new File("key.ncore.java/src/adt/java-ast.java").getAbsoluteFile())) { + out.write(cu.toString()); + } + } +} diff --git a/key.ncore.java/src/main/java/org/key_project/java/ast/DefaultProperties.java b/key.ncore.java/src/main/java/org/key_project/java/ast/DefaultProperties.java new file mode 100644 index 00000000000..9fad13f846e --- /dev/null +++ b/key.ncore.java/src/main/java/org/key_project/java/ast/DefaultProperties.java @@ -0,0 +1,34 @@ +package org.key_project.java.ast; + +import java.util.HashMap; +import java.util.Map; + +/** + * + * @author Alexander Weigl + * @version 1 (4/12/26) + */ +@SuppressWarnings("unchecked") +public class DefaultProperties implements Properties { + private final Map, Object> properties = new HashMap<>(); + + @Override + public T get(Property property, T defaultValue) { + return (T) properties.getOrDefault(property, defaultValue); + } + + @Override + public T get(Property property) { + return (T) properties.get(property); + } + + @Override + public boolean contains(Property property) { + return properties.containsKey(property); + } + + @Override + public void set(Property property, T value) { + properties.put(property, value); + } +} diff --git a/key.ncore.java/src/main/java/org/key_project/java/ast/Properties.java b/key.ncore.java/src/main/java/org/key_project/java/ast/Properties.java new file mode 100644 index 00000000000..baffde6241d --- /dev/null +++ b/key.ncore.java/src/main/java/org/key_project/java/ast/Properties.java @@ -0,0 +1,13 @@ +package org.key_project.java.ast; + +/** + * + * @author Alexander Weigl + * @version 1 (4/12/26) + */ +public interface Properties { + T get(Property property, T defaultValue); + T get(Property property); + boolean contains(Property property); + void set(Property property, T value); +} diff --git a/key.ncore.java/src/main/java/org/key_project/java/ast/Property.java b/key.ncore.java/src/main/java/org/key_project/java/ast/Property.java new file mode 100644 index 00000000000..2222d55acde --- /dev/null +++ b/key.ncore.java/src/main/java/org/key_project/java/ast/Property.java @@ -0,0 +1,25 @@ +package org.key_project.java.ast; + +import com.github.javaparser.ast.Node; + +/** + * A key to a piece of data associated with a {@link Node} at runtime. + * The key contains type information that can be used to check the + * type of any user data value for the key when the value is set. DataKey is abstract in order to + * force the creation of a subtype. That subtype is used to test for identity when looking for the + * user data because actual object identity would suffer from problems under serialization. + * So, the correct way to declare a DataKey is like this: + *

+ * 

+ * {@code
+ * public static final DataKey ROLE = new DataKey() { };
+ * }
+ *
+ *

+ * This code was taken from the Wicket project. + * + * @param The type of the object which is stored + * @see Node#getData(com.github.javaparser.ast.DataKey) + */ +public record Property(String name) { +} diff --git a/settings.gradle b/settings.gradle index 00226f6fa82..282af3d9866 100644 --- a/settings.gradle +++ b/settings.gradle @@ -7,6 +7,7 @@ plugins { include "key.util" include "key.ncore" include 'key.ncore.calculus' +include 'key.ncore.java' include "key.core" //include "key.core.rifl" From 8be2ffa35d631b626562c46733a20854c93eea61 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sat, 18 Apr 2026 13:30:43 +0200 Subject: [PATCH 2/7] wip --- key.ncore.java/src/adt/java-ast.java | 743 +++------ .../org/key_project/ncore/java/Generator.java | 189 ++- .../org/key_project/ncore/java/PostSteps.java | 157 ++ .../org/key_project/ncore/java/PreSteps.java | 10 + .../ncore/java/ReadAllHierarchy.java | 1448 +++++++++-------- .../key_project/java/ast/AssignmentKind.java | 22 + .../java/ast/BinaryOperatorKind.java | 37 + .../java/ast/DefaultProperties.java | 3 + .../java/org/key_project/java/ast/EqEx.java | 12 + .../key_project/java/ast/LogicFunction.java | 31 + .../org/key_project/java/ast/Properties.java | 6 + .../org/key_project/java/ast/Property.java | 3 + .../java/ast/UnaryOperatorKind.java | 28 + 13 files changed, 1357 insertions(+), 1332 deletions(-) create mode 100644 key.ncore.java/src/generator/java/org/key_project/ncore/java/PostSteps.java create mode 100644 key.ncore.java/src/generator/java/org/key_project/ncore/java/PreSteps.java create mode 100644 key.ncore.java/src/main/java/org/key_project/java/ast/AssignmentKind.java create mode 100644 key.ncore.java/src/main/java/org/key_project/java/ast/BinaryOperatorKind.java create mode 100644 key.ncore.java/src/main/java/org/key_project/java/ast/EqEx.java create mode 100644 key.ncore.java/src/main/java/org/key_project/java/ast/LogicFunction.java create mode 100644 key.ncore.java/src/main/java/org/key_project/java/ast/UnaryOperatorKind.java diff --git a/key.ncore.java/src/adt/java-ast.java b/key.ncore.java/src/adt/java-ast.java index e4bc355948d..b5c06279b9c 100644 --- a/key.ncore.java/src/adt/java-ast.java +++ b/key.ncore.java/src/adt/java-ast.java @@ -1,4 +1,10 @@ import org.jspecify.annotations.Nullable; +import de.uka.ilkd.key.speclang.jml.pretranslation.*; + +// ROOT +abstract class JavaSourceElement { + @EqEx PositionInfo positionInfo; +} class CompilationUnit extends JavaNonTerminalProgramElement { @Nullable PackageSpecification packageSpec; @@ -17,85 +23,60 @@ class Import extends JavaNonTerminalProgramElement { TypeReferenceInfix reference; } -abstract class JavaNonTerminalProgramElement extends JavaProgramElement { -} +abstract class JavaNonTerminalProgramElement extends JavaProgramElement {} -abstract class JavaProgramElement extends JavaSourceElement { -} +abstract class JavaProgramElement extends JavaSourceElement {} -abstract class Label { -} +abstract class Label {} -abstract class LoopInitializer { -} +abstract class LoopInitializer {} -abstract class NamedProgramElement { -} +abstract class NamedProgramElement {} class PackageSpecification extends JavaNonTerminalProgramElement { PackageReference reference; } -abstract class ParameterContainer { -} +abstract class ParameterContainer {} -abstract class ProgramElement { -} +abstract class ProgramElement {} -abstract class ProgramVariableName { -} +abstract class ProgramVariableName {} -abstract class Reference { -} +abstract class Reference {} -abstract class ScopeDefiningElement { -} +abstract class ScopeDefiningElement {} -abstract class Statement { -} +abstract class Statement {} -class StatementBlock extends JavaStatement { -} +class StatementBlock extends JavaStatement {} -abstract class StatementContainer { -} +abstract class StatementContainer {} -abstract class TerminalProgramElement { -} +abstract class TerminalProgramElement {} -abstract class TypeScope { -} +abstract class TypeScope {} -abstract class VariableScope { -} +abstract class VariableScope {} -class CcatchBreakLabelParameterDeclaration extends CcatchNonstandardParameterDeclaration { -} +class CcatchBreakLabelParameterDeclaration extends CcatchNonstandardParameterDeclaration {} -class CcatchBreakWildcardParameterDeclaration extends CcatchNonstandardParameterDeclaration { -} +class CcatchBreakWildcardParameterDeclaration extends CcatchNonstandardParameterDeclaration {} -class CcatchContinueLabelParameterDeclaration extends CcatchNonstandardParameterDeclaration { -} +class CcatchContinueLabelParameterDeclaration extends CcatchNonstandardParameterDeclaration {} -class CcatchContinueParameterDeclaration extends CcatchNonstandardParameterDeclaration { -} +class CcatchContinueParameterDeclaration extends CcatchNonstandardParameterDeclaration {} -class CcatchContinueWildcardParameterDeclaration extends CcatchNonstandardParameterDeclaration { -} +class CcatchContinueWildcardParameterDeclaration extends CcatchNonstandardParameterDeclaration {} -abstract class CcatchNonstandardParameterDeclaration extends JavaNonTerminalProgramElement { -} +abstract class CcatchNonstandardParameterDeclaration extends JavaNonTerminalProgramElement {} -class CcatchReturnParameterDeclaration extends CcatchNonstandardParameterDeclaration { -} +class CcatchReturnParameterDeclaration extends CcatchNonstandardParameterDeclaration {} -class CcatchReturnValParameterDeclaration extends CcatchNonstandardParameterDeclaration { -} +class CcatchReturnValParameterDeclaration extends CcatchNonstandardParameterDeclaration {} -class ArrayDeclaration extends TypeDeclaration { -} +class ArrayDeclaration extends TypeDeclaration {} class ClassDeclaration extends TypeDeclaration { @@ -115,25 +96,20 @@ class ClassInitializer extends JavaDeclaration { StatementBlock body; } -class ConstructorDeclaration extends MethodDeclaration { -} +class ConstructorDeclaration extends MethodDeclaration {} -class EnumClassDeclaration extends ClassDeclaration { -} +class EnumClassDeclaration extends ClassDeclaration {} -class Extends extends InheritanceSpecification { -} +class Extends extends InheritanceSpecification {} class FieldDeclaration extends VariableDeclaration { List fieldSpecs; } -class FieldSpecification extends VariableSpecification { -} +class FieldSpecification extends VariableSpecification {} -class Implements extends InheritanceSpecification { -} +class Implements extends InheritanceSpecification {} abstract class InheritanceSpecification extends JavaNonTerminalProgramElement { @@ -157,8 +133,7 @@ class LocalVariableDeclaration extends VariableDeclaration { List varSpecs; } -abstract class MemberDeclaration { -} +abstract class MemberDeclaration {} class MethodDeclaration extends JavaDeclaration { @@ -179,15 +154,13 @@ class MethodDeclaration extends JavaDeclaration { boolean parentIsInterfaceDeclaration; } -abstract class Modifier extends JavaProgramElement { -} +abstract class Modifier extends JavaProgramElement {} class ParameterDeclaration extends VariableDeclaration { List varSpec; } -class SuperArrayDeclaration extends TypeDeclaration { -} +class SuperArrayDeclaration extends TypeDeclaration {} class Throws extends JavaNonTerminalProgramElement { @@ -209,8 +182,7 @@ abstract class TypeDeclaration extends JavaDeclaration { JMLModifiers jmlModifiers; } -abstract class TypeDeclarationContainer { -} +abstract class TypeDeclarationContainer {} abstract class VariableDeclaration extends JavaDeclaration { @@ -230,333 +202,208 @@ class VariableSpecification extends JavaNonTerminalProgramElement { IProgramVariable programVariable; } -class Abstract extends Modifier { -} +class Abstract extends Modifier {} class AnnotationUseSpecification extends Modifier { TypeReference tr; } -class Final extends Modifier { -} +class Final extends Modifier {} -class Ghost extends Modifier { -} +class Ghost extends Modifier {} -class Model extends Modifier { -} +class Model extends Modifier {} -class ABSTRACT extends Modifier { -} +class ABSTRACT extends Modifier {} -class DEFAULT extends Modifier { -} +class DEFAULT extends Modifier {} -class FINAL extends Modifier { -} +class FINAL extends Modifier {} -class JML_CODE extends Modifier { -} +class JML_CODE extends Modifier {} -class JML_CODE_BIGINT_MATH extends Modifier { -} +class JML_CODE_BIGINT_MATH extends Modifier {} -class JML_CODE_JAVA_MATH extends Modifier { -} +class JML_CODE_JAVA_MATH extends Modifier {} -class JML_CODE_SAFE_MATH extends Modifier { -} +class JML_CODE_SAFE_MATH extends Modifier {} -class JML_HELPER extends Modifier { -} +class JML_HELPER extends Modifier {} -class JML_INSTANCE extends Modifier { -} +class JML_INSTANCE extends Modifier {} -class JML_NON_NULL extends Modifier { -} +class JML_NON_NULL extends Modifier {} -class JML_NON_NULL_BY_DEFAULT extends Modifier { -} +class JML_NON_NULL_BY_DEFAULT extends Modifier {} -class JML_NON_NULL_ELEMENTS extends Modifier { -} +class JML_NON_NULL_ELEMENTS extends Modifier {} -class JML_NO_STATE extends Modifier { -} +class JML_NO_STATE extends Modifier {} -class JML_NULLABLE extends Modifier { -} +class JML_NULLABLE extends Modifier {} -class JML_NULLABLE_BY_DEFAULT extends Modifier { -} +class JML_NULLABLE_BY_DEFAULT extends Modifier {} -class JML_OT_READ_ONLY extends Modifier { -} +class JML_OT_READ_ONLY extends Modifier {} -class JML_OT_REP extends Modifier { -} +class JML_OT_REP extends Modifier {} -class JML_PACKAGE extends Modifier { -} +class JML_PACKAGE extends Modifier {} -class JML_PURE extends Modifier { -} +class JML_PURE extends Modifier {} -class JML_SPEC_BIGINT_MATH extends Modifier { -} +class JML_SPEC_BIGINT_MATH extends Modifier {} -class JML_SPEC_JAVA_MATH extends Modifier { -} +class JML_SPEC_JAVA_MATH extends Modifier {} -class JML_SPEC_PACKAGE extends Modifier { -} +class JML_SPEC_PACKAGE extends Modifier {} -class JML_SPEC_PRIVATE extends Modifier { -} +class JML_SPEC_PRIVATE extends Modifier {} -class JML_SPEC_PROTECTED extends Modifier { -} +class JML_SPEC_PROTECTED extends Modifier {} -class JML_SPEC_PUBLIC extends Modifier { -} +class JML_SPEC_PUBLIC extends Modifier {} -class JML_SPEC_SAFE_MATH extends Modifier { -} +class JML_SPEC_SAFE_MATH extends Modifier {} -class JML_STRICTLY_PURE extends Modifier { -} +class JML_STRICTLY_PURE extends Modifier {} -class JML_TWO_STATE extends Modifier { -} +class JML_TWO_STATE extends Modifier {} -class JML_UNPARSABLE_MODIFIERS extends Modifier { -} +class JML_UNPARSABLE_MODIFIERS extends Modifier {} -class NATIVE extends Modifier { -} +class NATIVE extends Modifier {} -class NON_SEALED extends Modifier { -} +class NON_SEALED extends Modifier {} -class PRIVATE extends Modifier { -} +class PRIVATE extends Modifier {} -class PROTECTED extends Modifier { -} +class PROTECTED extends Modifier {} -class PUBLIC extends Modifier { -} +class PUBLIC extends Modifier {} -class SEALED extends Modifier { -} +class SEALED extends Modifier {} -class STATIC extends Modifier { -} +class STATIC extends Modifier {} -class STRICTFP extends Modifier { -} +class STRICTFP extends Modifier {} -class SYNCHRONIZED extends Modifier { -} +class SYNCHRONIZED extends Modifier {} -class TRANSIENT extends Modifier { -} +class TRANSIENT extends Modifier {} -class TRANSITIVE extends Modifier { -} +class TRANSITIVE extends Modifier {} -class VOLATILE extends Modifier { -} +class VOLATILE extends Modifier {} -class Native extends Modifier { -} +class Native extends Modifier {} -class NoState extends Modifier { -} +class NoState extends Modifier {} -class Private extends VisibilityModifier { -} +class Private extends VisibilityModifier {} -class Protected extends VisibilityModifier { -} +class Protected extends VisibilityModifier {} -class Public extends VisibilityModifier { -} +class Public extends VisibilityModifier {} -class Static extends Modifier { -} +class Static extends Modifier {} -class StrictFp extends Modifier { -} +class StrictFp extends Modifier {} -class Synchronized extends Modifier { -} +class Synchronized extends Modifier {} -class Transient extends Modifier { -} +class Transient extends Modifier {} -class TwoState extends Modifier { -} +class TwoState extends Modifier {} -abstract class VisibilityModifier extends Modifier { -} +abstract class VisibilityModifier extends Modifier {} class Volatile extends Modifier {} class ArrayInitializer extends JavaNonTerminalProgramElement { KeYJavaType kjt; } +abstract class Expression {} -abstract class Assignment extends Operator { -} - -abstract class Expression { -} +abstract class ExpressionStatement {} -abstract class ExpressionStatement { -} +abstract class Operator extends JavaNonTerminalProgramElement {} -abstract class Operator extends JavaNonTerminalProgramElement { +class ParenthesizedExpression extends Operator { + Expression child; } -class ParenthesizedExpression extends Operator {} - class PassiveExpression extends ParenthesizedExpression {} -abstract class AbstractIntegerLiteral extends Literal {} +abstract class Literal extends JavaProgramElement { + String value; +} + +abstract class AbstractIntegerLiteral extends Literal { +} class BooleanLiteral extends Literal {} class CharLiteral extends AbstractIntegerLiteral {} -class DoubleLiteral extends Literal { +class DoubleLiteral extends Literal {} - String value; -} +class EmptyMapLiteral extends Literal {} -class EmptyMapLiteral extends Literal { -} +class EmptySeqLiteral extends Literal {} -class EmptySeqLiteral extends Literal { -} - -class EmptySetLiteral extends Literal { -} +class EmptySetLiteral extends Literal {} class FloatLiteral extends Literal { - String value; } -class FreeLiteral extends Literal { -} +class FreeLiteral extends Literal {} -class IntLiteral extends AbstractIntegerLiteral { -} - -abstract class Literal extends JavaProgramElement {} +class IntLiteral extends AbstractIntegerLiteral {} class LongLiteral extends AbstractIntegerLiteral {} -class RealLiteral extends Literal { - String value; -} - -class StringLiteral extends Literal { - String value; -} - -class BinaryAnd extends BinaryOperator { -} - -class BinaryAndAssignment extends Assignment { -} +class RealLiteral extends Literal {} -class BinaryNot extends Operator { -} +class StringLiteral extends Literal {} -abstract class BinaryOperator extends Operator { +class Assignment extends Operator { + AssignmentKind kind; + Expression left; + Expression right; } -class BinaryOr extends BinaryOperator { -} -class BinaryOrAssignment extends Assignment { +class BinaryOperator extends Operator { + BinaryOperatorKind kind; + Expression left; + Expression right; } -class BinaryXOr extends BinaryOperator { -} +class UnaryOperator implements Operator { + UnaryOperatorKind kind; + Expression child; -class BinaryXOrAssignment extends Assignment { } -abstract class ComparativeOperator extends Operator { +class LogicalFunctionOperator extends Operator { + LogicFunction function; + List arguments; } class Conditional extends Operator { + Expression condition; + Expression thenExpr; + Expression elseExpr; } -class CopyAssignment extends Assignment { -} - -class DLEmbeddedExpression extends Operator { -} - -class Divide extends BinaryOperator { -} - -class DivideAssignment extends Assignment { -} - -class Equals extends ComparativeOperator { -} - -class ExactInstanceof extends TypeOperator { -} - -class GreaterOrEquals extends ComparativeOperator { -} - -class GreaterThan extends ComparativeOperator { -} - -class Instanceof extends TypeOperator { -} - -class Intersect extends BinaryOperator { -} - -class LessOrEquals extends ComparativeOperator { -} - -class LessThan extends ComparativeOperator { -} - -class LogicalAnd extends Operator { -} - -class LogicalNot extends Operator { -} - -class LogicalOr extends Operator { -} - -class Minus extends BinaryOperator { -} - -class MinusAssignment extends Assignment { -} - -class Modulo extends BinaryOperator { -} +class DLEmbeddedExpression extends Operator {} -class ModuloAssignment extends Assignment { -} +class ExactInstanceof extends TypeOperator {} -class Negative extends Operator { -} +class Instanceof extends TypeOperator {} class New extends TypeOperator { @@ -572,103 +419,13 @@ class NewArray extends TypeOperator { ArrayInitializer arrayInitializer; } -class NotEquals extends ComparativeOperator { -} - -class Plus extends BinaryOperator { -} - -class PlusAssignment extends Assignment { -} - -class Positive extends Operator { -} - -class PostDecrement extends Assignment { -} - -class PostIncrement extends Assignment { -} - -class PreDecrement extends Assignment { -} - -class PreIncrement extends Assignment { -} - -class ShiftLeft extends Operator { -} - -class ShiftLeftAssignment extends Assignment { -} - -class ShiftRight extends Operator { -} - -class ShiftRightAssignment extends Assignment { -} - -class Subtype extends BinaryOperator { -} - -class Times extends BinaryOperator { -} - -class TimesAssignment extends Assignment { -} - -class TypeCast extends TypeOperator { -} +class TypeCast extends TypeOperator {} abstract class TypeOperator extends Operator { TypeReference typeReference; } -class UnsignedShiftRight extends Operator { -} - -class UnsignedShiftRightAssignment extends Assignment { -} - -class AllFields extends Operator { -} - -class AllObjects extends Operator { -} - -class SeqConcat extends BinaryOperator { -} - -class SeqGet extends Operator { -} - -class SeqIndexOf extends Operator { -} - -class SeqLength extends Operator { -} - -class SeqPut extends Operator { -} - -class SeqReverse extends Operator { -} - -class SeqSingleton extends Operator { -} - -class SeqSub extends Operator { -} - -class SetMinus extends BinaryOperator { -} - -class SetUnion extends BinaryOperator { -} - -class Singleton extends Operator { -} class ArrayLengthReference extends JavaNonTerminalProgramElement { @@ -682,8 +439,7 @@ class ArrayReference extends JavaNonTerminalProgramElement { List inits; } -abstract class ConstructorReference { -} +abstract class ConstructorReference {} class ExecutionContext extends JavaNonTerminalProgramElement { @@ -697,22 +453,18 @@ class FieldReference extends VariableReference { ReferencePrefix prefix; } -abstract class IExecutionContext { -} +abstract class IExecutionContext {} -abstract class MemberReference { -} +abstract class MemberReference {} class MetaClassReference extends JavaNonTerminalProgramElement { TypeReference typeReference; } -abstract class MethodName { -} +abstract class MethodName {} -abstract class MethodOrConstructorReference { -} +abstract class MethodOrConstructorReference {} class MethodReference extends JavaNonTerminalProgramElement { @@ -723,8 +475,7 @@ class MethodReference extends JavaNonTerminalProgramElement { List arguments; } -abstract class NameReference { -} +abstract class NameReference {} class PackageReference extends JavaNonTerminalProgramElement { @@ -733,17 +484,13 @@ class PackageReference extends JavaNonTerminalProgramElement { ProgramElementName name; } -abstract class PackageReferenceContainer { -} +abstract class PackageReferenceContainer {} -abstract class ReferencePrefix { -} +abstract class ReferencePrefix {} -abstract class ReferenceSuffix { -} +abstract class ReferenceSuffix {} -class SchemaTypeReference extends TypeReferenceImp { -} +class SchemaTypeReference extends TypeReferenceImp {} class SchematicFieldReference extends FieldReference { @@ -760,23 +507,17 @@ class SuperConstructorReference extends SpecialConstructorReference { ReferencePrefix prefix; } -class SuperReference extends JavaNonTerminalProgramElement { -} +class SuperReference extends JavaNonTerminalProgramElement {} -class ThisConstructorReference extends SpecialConstructorReference { -} +class ThisConstructorReference extends SpecialConstructorReference {} -class ThisReference extends JavaNonTerminalProgramElement { -} +class ThisReference extends JavaNonTerminalProgramElement {} -class TypeRef extends TypeReferenceImp { -} +class TypeRef extends TypeReferenceImp {} -abstract class TypeReference { -} +abstract class TypeReference {} -abstract class TypeReferenceContainer { -} +abstract class TypeReferenceContainer {} abstract class TypeReferenceImp extends JavaNonTerminalProgramElement { @@ -787,21 +528,18 @@ abstract class TypeReferenceImp extends JavaNonTerminalProgramElement { ProgramElementName name; } -abstract class TypeReferenceInfix { -} +abstract class TypeReferenceInfix {} class VariableReference extends JavaNonTerminalProgramElement { ProgramVariable variable; } -class Assert extends JavaStatement { -} +class Assert extends JavaStatement {} abstract class Branch {} -abstract class BranchImp extends JavaNonTerminalProgramElement { -} +abstract class BranchImp extends JavaNonTerminalProgramElement {} abstract class BranchStatement extends JavaStatement {} @@ -827,25 +565,20 @@ class Default extends BranchImp { List body; } -class Do extends LoopStatement { -} +class Do extends LoopStatement {} class Else extends BranchImp { Statement body; } -class EmptyStatement extends JavaProgramElement { -} +class EmptyStatement extends JavaProgramElement {} -class EnhancedFor extends LoopStatement { -} +class EnhancedFor extends LoopStatement {} -class Exec extends BranchStatement { -} +class Exec extends BranchStatement {} abstract class ExpressionJumpStatement extends JumpStatement { - Expression expression; } @@ -854,8 +587,7 @@ class Finally extends BranchImp { StatementBlock body; } -class For extends LoopStatement { -} +class For extends LoopStatement {} class ForUpdates extends JavaNonTerminalProgramElement { @@ -877,17 +609,13 @@ class If extends BranchStatement { Statement elseBranch; } -abstract class JavaStatement extends JavaNonTerminalProgramElement { -} +abstract class JavaStatement extends JavaNonTerminalProgramElement {} -class JmlAssert extends JavaStatement { -} +class JmlAssert extends JavaStatement {} -abstract class JumpStatement extends JavaStatement { -} +abstract class JumpStatement extends JavaStatement {} abstract class LabelJumpStatement extends JumpStatement { - Label name; } @@ -897,24 +625,20 @@ class LabeledStatement extends JavaStatement { } class LoopInit extends JavaNonTerminalProgramElement { - List inits; } class LoopScopeBlock extends JavaStatement { + Expression variant; + Statement body; } abstract class LoopStatement extends JavaStatement { - ILoopInit inits; - IForUpdates updates; - IGuard guard; - Statement body; - - ImmutableList attachedJml; + ImmutableList attachedJml; } class MergePointStatement extends JavaStatement { @@ -922,17 +646,13 @@ class MergePointStatement extends JavaStatement { IProgramVariable identifier; } -class MethodBodyStatement extends JavaNonTerminalProgramElement { -} +class MethodBodyStatement extends JavaNonTerminalProgramElement {} -class MethodFrame extends JavaStatement { -} +class MethodFrame extends JavaStatement {} -class Return extends ExpressionJumpStatement { -} +class Return extends ExpressionJumpStatement {} -class SetStatement extends JavaStatement { -} +class SetStatement extends JavaStatement {} class Switch extends BranchStatement { @@ -948,98 +668,67 @@ class SynchronizedBlock extends JavaStatement { StatementBlock body; } -class Then extends BranchImp { -} +class Then extends BranchImp {} -class Throw extends ExpressionJumpStatement { -} +class Throw extends ExpressionJumpStatement {} -class TransactionStatement extends JavaStatement { -} +class TransactionStatement extends JavaStatement {} -class Try extends BranchStatement { -} +class Try extends BranchStatement {} -class While extends LoopStatement { -} +class While extends LoopStatement {} -abstract class ProgramConstruct { -} +abstract class ProgramConstruct {} -class ProgramElementName extends Name { -} +class ProgramElementName extends Name {} -abstract class ProgramPrefix { -} +abstract class ProgramPrefix {} -abstract class IndProgramElementName extends ProgramElementName { -} +abstract class IndProgramElementName extends ProgramElementName {} -class PermIndProgramElementName extends IndProgramElementName { -} +class PermIndProgramElementName extends IndProgramElementName {} -class TempIndProgramElementName extends IndProgramElementName { -} +class TempIndProgramElementName extends IndProgramElementName {} -abstract class IProgramMethod { -} +abstract class IProgramMethod {} -abstract class IProgramVariable { -} +abstract class IProgramVariable {} -class LocationVariable extends ProgramVariable { -} +class LocationVariable extends ProgramVariable {} -class ProgramConstant extends ProgramVariable { -} +class ProgramConstant extends ProgramVariable {} -class ProgramMethod extends ObserverFunction { -} +class ProgramMethod extends ObserverFunction {} -class ProgramSV extends JOperatorSV { -} +class ProgramSV extends JOperatorSV {} -abstract class ProgramVariable extends JAbstractSortedOperator { -} +abstract class ProgramVariable extends JAbstractSortedOperator {} -abstract class AbstractProgramElement { -} +abstract class AbstractProgramElement {} -class ArrayLength extends ProgramTransformer { -} +class ArrayLength extends ProgramTransformer {} -class ArrayPostDecl extends ProgramTransformer { -} +class ArrayPostDecl extends ProgramTransformer {} -class ConstructorCall extends ProgramTransformer { -} +class ConstructorCall extends ProgramTransformer {} -class CreateObject extends ProgramTransformer { -} +class CreateObject extends ProgramTransformer {} -class DoBreak extends ProgramTransformer { -} +class DoBreak extends ProgramTransformer {} -class EnhancedForElimination extends ProgramTransformer { -} +class EnhancedForElimination extends ProgramTransformer {} -class EvaluateArgs extends ProgramTransformer { -} +class EvaluateArgs extends ProgramTransformer {} -class ExpandMethodBody extends ProgramTransformer { -} +class ExpandMethodBody extends ProgramTransformer {} -class ForInitUnfoldTransformer extends ProgramTransformer { -} +class ForInitUnfoldTransformer extends ProgramTransformer {} -class ForToWhile extends ProgramTransformer { -} +class ForToWhile extends ProgramTransformer {} -abstract class InitArray extends ProgramTransformer { -} +abstract class InitArray extends ProgramTransformer {} -class InitArrayCreation extends InitArray { -} +class InitArrayCreation extends InitArray {} class IsStatic extends ProgramTransformer {} @@ -1051,32 +740,22 @@ class MethodCall extends ProgramTransformer { KeYJavaType staticPrefixType; } -class MultipleVarDecl extends ProgramTransformer { -} +class MultipleVarDecl extends ProgramTransformer {} -class PostWork extends ProgramTransformer { -} +class PostWork extends ProgramTransformer {} -abstract class ProgramTransformer extends JavaNonTerminalProgramElement { -} +abstract class ProgramTransformer extends JavaNonTerminalProgramElement {} -class ReattachLoopInvariant extends ProgramTransformer { -} +class ReattachLoopInvariant extends ProgramTransformer {} -class SpecialConstructorCall extends ProgramTransformer { -} +class SpecialConstructorCall extends ProgramTransformer {} -class StaticInitialisation extends ProgramTransformer { -} +class StaticInitialisation extends ProgramTransformer {} -class SwitchToIf extends ProgramTransformer { -} +class SwitchToIf extends ProgramTransformer {} -class TypeOf extends ProgramTransformer { -} +class TypeOf extends ProgramTransformer {} -class Unpack extends ProgramTransformer { -} +class Unpack extends ProgramTransformer {} -class UnwindLoop extends ProgramTransformer { -} +class UnwindLoop extends ProgramTransformer {} diff --git a/key.ncore.java/src/generator/java/org/key_project/ncore/java/Generator.java b/key.ncore.java/src/generator/java/org/key_project/ncore/java/Generator.java index 197d66ed381..44c52440ecc 100644 --- a/key.ncore.java/src/generator/java/org/key_project/ncore/java/Generator.java +++ b/key.ncore.java/src/generator/java/org/key_project/ncore/java/Generator.java @@ -1,5 +1,21 @@ +/* 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 org.key_project.ncore.java; +import java.io.File; +import java.nio.file.Files; +import java.nio.file.Path; +import java.nio.file.Paths; +import java.util.ArrayList; +import java.util.List; +import java.util.TreeMap; +import java.util.concurrent.Callable; +import java.util.stream.Collectors; + +import org.key_project.ncore.java.PostSteps.PostStep; +import org.key_project.ncore.java.PreSteps.PreStep; + import com.github.javaparser.ParserConfiguration; import com.github.javaparser.StaticJavaParser; import com.github.javaparser.ast.CompilationUnit; @@ -21,15 +37,6 @@ import org.jspecify.annotations.NullMarked; import org.jspecify.annotations.Nullable; -import java.io.File; -import java.nio.file.Path; -import java.nio.file.Paths; -import java.util.ArrayList; -import java.util.List; -import java.util.TreeMap; -import java.util.concurrent.Callable; -import java.util.stream.Collectors; - import static com.github.javaparser.StaticJavaParser.*; import static com.github.javaparser.ast.Modifier.DefaultKeyword.*; @@ -45,6 +52,7 @@ public class Generator implements Callable { List nodeSteps = new ArrayList<>(64); List preSteps = new ArrayList<>(64); + List postSteps = new ArrayList<>(64); public static void main(String[] args) throws Exception { new Generator().call(); @@ -67,10 +75,16 @@ public Generator() { addStep(Generator::addOverrideConstructor2); addStep(Generator::addGetProperties); addStep(Generator::processFieldsAccessor); + + postSteps.add(PostSteps::createVisitor); + postSteps.add(PostSteps::createVoidVisitor); + postSteps.add(PostSteps::createTraversalVisitor); + postSteps.add(PostSteps::createDeepCopyVisitor); } private static void addBuilder(ClassOrInterfaceDeclaration target) { - if(target.isInterface()) return; + if (target.isInterface()) + return; var builder = new ClassOrInterfaceDeclaration(); builder.setName("Builder"); @@ -79,7 +93,7 @@ private static void addBuilder(ClassOrInterfaceDeclaration target) { for (var field : target.getFields()) { for (var variable : field.variables()) { var f = builder.addField(variable.getType().clone(), - variable.getNameAsString(), PUBLIC); + variable.getNameAsString(), PUBLIC); f.addAnnotation(Nullable.class); } } @@ -89,17 +103,18 @@ private static void addBuilder(ClassOrInterfaceDeclaration target) { var args = builder.getFields().stream().flatMap(it -> it.variables().stream()) .map(it -> (Expression) it.getNameAsExpression()) - .collect(Collectors.toList()); + .toList(); build.getBody().get().addStatement(new ReturnStmt( - new ObjectCreationExpr(null, - new ClassOrInterfaceType(null, target.getNameAsString()), - new NodeList<>(args)))); + new ObjectCreationExpr(null, + new ClassOrInterfaceType(null, target.getNameAsString()), + new NodeList<>(args)))); builder.getFields().stream().flatMap(it -> it.variables().stream()).forEach(it -> { var m = builder.addMethod(it.getNameAsString(), PUBLIC); m.addParameter(new Parameter(it.getType().clone(), it.getNameAsString())); m.setType(new ClassOrInterfaceType(null, "Builder")); - m.getBody().get().addStatement("this.%s=%s;".formatted(it.getNameAsString(), it.getNameAsString())); + m.getBody().get().addStatement( + "this.%s=%s;".formatted(it.getNameAsString(), it.getNameAsString())); m.getBody().get().addStatement("return this;"); }); @@ -108,11 +123,14 @@ private static void addBuilder(ClassOrInterfaceDeclaration target) { .filter(Generator::isList) .forEach(it -> { var m = builder.addMethod(it.getNameAsString(), PUBLIC); - var t = it.getType().asClassOrInterfaceType().getTypeArguments().get().getFirst(); + var t = + it.getType().asClassOrInterfaceType().getTypeArguments().get().getFirst(); m.addParameter(new Parameter(t.clone(), it.getNameAsString())); m.setType(new ClassOrInterfaceType(null, "Builder")); - m.getBody().get().addStatement("if(this.%s==null) this.%s = new ArrayList<>();".formatted(it.getNameAsString(), it.getNameAsString())); - m.getBody().get().addStatement("this.%s.add(%s);".formatted(it.getNameAsString(), it.getNameAsString())); + m.getBody().get().addStatement("if(this.%s==null) this.%s = new ArrayList<>();" + .formatted(it.getNameAsString(), it.getNameAsString())); + m.getBody().get().addStatement( + "this.%s.add(%s);".formatted(it.getNameAsString(), it.getNameAsString())); m.getBody().get().addStatement("return this;"); }); @@ -122,8 +140,8 @@ private static void addBuilder(ClassOrInterfaceDeclaration target) { tb.setType(new ClassOrInterfaceType(null, "Builder")); final var b = tb.getBody().get(); b.addStatement("Builder b = new Builder();"); - builder.getFields().stream().flatMap(it -> it.variables().stream()).forEach(it -> - b.addStatement("b.%s = %s;".formatted(it.getNameAsString(), it.getNameAsString()))); + builder.getFields().stream().flatMap(it -> it.variables().stream()).forEach(it -> b + .addStatement("b.%s = %s;".formatted(it.getNameAsString(), it.getNameAsString()))); b.addStatement("return b;"); } @@ -135,23 +153,23 @@ private static void addWiths(ClassOrInterfaceDeclaration target) { target.getFields().stream() .flatMap(it -> it.getVariables().stream()).forEach(it -> { var args = - target.getFields().stream() - .flatMap(f -> f.getVariables().stream()) - .map(v -> { - if (v == it) { - return (Expression) v.getNameAsExpression(); - } else { - return new MethodCallExpr(null, v.getNameAsString()); - } - }).toList(); + target.getFields().stream() + .flatMap(f -> f.getVariables().stream()) + .map(v -> { + if (v == it) { + return (Expression) v.getNameAsExpression(); + } else { + return new MethodCallExpr(null, v.getNameAsString()); + } + }).toList(); var m = target.addMethod("with" + it.getNameAsString(), PUBLIC); m.addParameter(new Parameter(it.getType().clone(), it.getNameAsString())); m.setType(new ClassOrInterfaceType(null, target.getNameAsString())); m.getBody().get().addStatement(new ReturnStmt( - new ObjectCreationExpr(null, - new ClassOrInterfaceType(null, target.getNameAsString()), - new NodeList<>(args)))); + new ObjectCreationExpr(null, + new ClassOrInterfaceType(null, target.getNameAsString()), + new NodeList<>(args)))); }); } @@ -167,11 +185,12 @@ private static void addEquals(ClassOrInterfaceDeclaration target) { equals.getParameters().add(o); BlockStmt body = equals.getBody().get(); body.addStatement(parseStatement("if(this == o) return true;")); - body.addStatement(parseStatement("if(!(o instanceof %s that)) return false;".formatted(target.getNameAsString()))); + body.addStatement(parseStatement( + "if(!(o instanceof %s that)) return false;".formatted(target.getNameAsString()))); Expression equalFields = target.getFields().stream() .flatMap(it -> it.getVariables().stream()) .map(it -> callObjects("equals", it.getNameAsExpression(), - new FieldAccessExpr(new NameExpr("that"), it.getNameAsString()))) + new FieldAccessExpr(new NameExpr("that"), it.getNameAsString()))) .reduce((a, b) -> new BinaryExpr(a, b, BinaryExpr.Operator.AND)) .orElse(new BooleanLiteralExpr(true)); body.addStatement(new ReturnStmt(equalFields)); @@ -197,8 +216,7 @@ private static void addHashCode(ClassOrInterfaceDeclaration target) { assert false : "No defined fields"; else hashCode.getBody().get().addStatement(new ReturnStmt( - callObjects("hash", args) - )); + callObjects("hash", args))); } private static void ToString(ClassOrInterfaceDeclaration clazz) { @@ -209,15 +227,17 @@ private static void ToString(ClassOrInterfaceDeclaration clazz) { MethodDeclaration toString = clazz.addMethod("toString", PUBLIC, FINAL); toString.addAnnotation(Override.class); toString.setType(String.class); - var parameters = clazz.getFields().stream().flatMap(it -> it.getVariables().stream()).toList(); + var parameters = + clazz.getFields().stream().flatMap(it -> it.getVariables().stream()).toList(); var sb = (clazz.getNameAsString() + "[") - + parameters.stream().map(NodeWithSimpleName::getNameAsString).map(it -> it + "=%s") - .collect(Collectors.joining(", ")) + "]"; + + parameters.stream().map(NodeWithSimpleName::getNameAsString).map(it -> it + "=%s") + .collect(Collectors.joining(", ")) + + "]"; var args = parameters.stream().map(NodeWithSimpleName::getNameAsExpression) .map(it -> (Expression) it).toList(); toString.getBody().get().addStatement(new ReturnStmt( - new MethodCallExpr(new StringLiteralExpr(sb), "formatted", new NodeList<>(args)))); + new MethodCallExpr(new StringLiteralExpr(sb), "formatted", new NodeList<>(args)))); } private static Expression callObjects(String method, Expression... args) { @@ -243,10 +263,9 @@ private static void addAllFieldsConstructor(ClassOrInterfaceDeclaration target) for (var variable : field.getVariables()) { params.add(new Parameter(variable.getType().clone(), variable.getNameAsString())); body.addStatement( - new ExpressionStmt(new AssignExpr( - new FieldAccessExpr(new ThisExpr(), variable.getNameAsString()), - variable.getNameAsExpression(), AssignExpr.Operator.ASSIGN - ))); + new ExpressionStmt(new AssignExpr( + new FieldAccessExpr(new ThisExpr(), variable.getNameAsString()), + variable.getNameAsExpression(), AssignExpr.Operator.ASSIGN))); } } @@ -263,14 +282,15 @@ private static void addOverrideConstructor(ClassOrInterfaceDeclaration target) { var body = constr.getBody().get(); var params = constr.getParameters(); constr.setName(target.getNameAsString()); - params.add(new Parameter(new ClassOrInterfaceType(null, target.getNameAsString()), "other")); + params.add( + new Parameter(new ClassOrInterfaceType(null, target.getNameAsString()), "other")); params.add(new Parameter(parseType("Properties"), "map")); var args = target.getFields().stream().flatMap(it -> it.getVariables().stream()) .map(NodeWithSimpleName::getNameAsString) - .map(it -> - (Expression) parseExpression("map.get(PROPERTY_%s, other.%s)".formatted(it.toUpperCase(), it))) + .map(it -> (Expression) parseExpression( + "map.get(PROPERTY_%s, other.%s)".formatted(it.toUpperCase(), it))) .toList(); body.addStatement(new MethodCallExpr(null, "this", new NodeList<>(args))); } @@ -288,8 +308,8 @@ private static void addOverrideConstructor2(ClassOrInterfaceDeclaration target) var args = target.getFields().stream().flatMap(it -> it.getVariables().stream()) .map(NodeWithSimpleName::getNameAsString) - .map(it -> - (Expression) parseExpression("map.get(PROPERTY_%s)".formatted(it.toUpperCase()))) + .map(it -> (Expression) parseExpression( + "map.get(PROPERTY_%s)".formatted(it.toUpperCase()))) .toList(); body.addStatement(new MethodCallExpr(null, "this", new NodeList<>(args))); } @@ -308,7 +328,8 @@ private static void addGetProperties(ClassOrInterfaceDeclaration target) { body.addStatement("Properties p = new DefaultProperties();"); target.getFields().stream() .flatMap(it -> it.getVariables().stream()) - .forEach(variable -> body.addStatement("p.set(PROPERTY_%s, %s());".formatted(variable.getNameAsString().toUpperCase(), variable.getNameAsString()))); + .forEach(variable -> body.addStatement("p.set(PROPERTY_%s, %s());".formatted( + variable.getNameAsString().toUpperCase(), variable.getNameAsString()))); body.addStatement("return p;"); } @@ -322,22 +343,23 @@ private static void addCopyConstructor(ClassOrInterfaceDeclaration target) { var body = constr.getBody().get(); var params = constr.getParameters(); constr.setName(target.getNameAsString()); - params.add(new Parameter(new ClassOrInterfaceType(null, target.getNameAsString()), "other")); + params.add( + new Parameter(new ClassOrInterfaceType(null, target.getNameAsString()), "other")); /* - for (var field : target.getFields()) { - for (var variable : field.getVariables()) { - //params.add(new Parameter(variable.getType().clone(), variable.getNameAsString())); - body.addStatement( - new ExpressionStmt(new AssignExpr( - new FieldAccessExpr(new ThisExpr(), variable.getNameAsString()), - new FieldAccessExpr(new NameExpr("other"), variable.getNameAsString()), - AssignExpr.Operator.ASSIGN - )) - ); - } - } - */ + * for (var field : target.getFields()) { + * for (var variable : field.getVariables()) { + * //params.add(new Parameter(variable.getType().clone(), variable.getNameAsString())); + * body.addStatement( + * new ExpressionStmt(new AssignExpr( + * new FieldAccessExpr(new ThisExpr(), variable.getNameAsString()), + * new FieldAccessExpr(new NameExpr("other"), variable.getNameAsString()), + * AssignExpr.Operator.ASSIGN + * )) + * ); + * } + * } + */ var args = target.getFields().stream().flatMap(it -> it.getVariables().stream()) .map(NodeWithSimpleName::getNameAsString) @@ -347,8 +369,10 @@ private static void addCopyConstructor(ClassOrInterfaceDeclaration target) { } - static Multimap inheritanceMap = MultimapBuilder.treeKeys().treeSetValues().build(); - static Multimap permittedTypes = MultimapBuilder.treeKeys().treeSetValues().build(); + static Multimap inheritanceMap = + MultimapBuilder.treeKeys().treeSetValues().build(); + static Multimap permittedTypes = + MultimapBuilder.treeKeys().treeSetValues().build(); private static final PreStep pushFieldsDown = types -> { TreeMap fields = new TreeMap<>(); @@ -410,7 +434,9 @@ public Integer call() throws Exception { config.setLanguageLevel(ParserConfiguration.LanguageLevel.JAVA_25); StaticJavaParser.setConfiguration(config); - metaModel = StaticJavaParser.parse(new File("key.ncore.java/src/adt/java-ast.java").getAbsoluteFile()); + metaModel = StaticJavaParser + .parse(new File("key.ncore.java/src/adt/java-ast.java").getAbsoluteFile()); + Files.createDirectories(ROOT); SourceRoot sourceRoot = new SourceRoot(ROOT); final var types = metaModel.getTypes(); @@ -418,6 +444,7 @@ public Integer call() throws Exception { nodeStep.applyOn(types); } + List nodeUnits = new ArrayList<>(types.size()); for (var type : types) { var cu = new CompilationUnit(); cu.addType(type); @@ -429,9 +456,14 @@ public Integer call() throws Exception { nodeStep.applyOn((ClassOrInterfaceDeclaration) type); } + nodeUnits.add(cu); sourceRoot.add(cu); } + for (var nodeStep : postSteps) { + nodeStep.applyOn(nodeUnits, sourceRoot); + } + sourceRoot.saveAll(); return 0; } @@ -467,17 +499,20 @@ static void setPackage(ClassOrInterfaceDeclaration target) { private static void processFieldsAccessor(ClassOrInterfaceDeclaration target) { - if (target.isInterface()) return; + if (target.isInterface()) + return; target.findCompilationUnit().get().addImport("org.key_project.java.ast.Property"); for (var field : target.getFields()) { for (var variable : field.getVariables()) { final var dataKey = new ClassOrInterfaceType(null, new SimpleName("Property"), - new NodeList<>(toBoxType(variable.getType().clone()))); + new NodeList<>(toBoxType(variable.getType().clone()))); var f = target.addField( - dataKey, "PROPERTY_" + variable.getNameAsString().toUpperCase(), PUBLIC, STATIC, FINAL); - f.getVariables().getFirst().setInitializer("new Property<>(\"%s\")".formatted(variable.getNameAsString())); + dataKey, "PROPERTY_" + variable.getNameAsString().toUpperCase(), PUBLIC, STATIC, + FINAL); + f.getVariables().getFirst().setInitializer( + "new Property<>(\"%s\")".formatted(variable.getNameAsString())); } } } @@ -509,10 +544,11 @@ static void processFields(ClassOrInterfaceDeclaration target) { } if (isAbstract) { - //getter.addModifier(Modifier.DefaultKeyword.ABSTRACT); + // getter.addModifier(Modifier.DefaultKeyword.ABSTRACT); getter.setBody(null); } else { - getter.getBody().get().addStatement(new ReturnStmt(variable.getNameAsExpression())); + getter.getBody().get() + .addStatement(new ReturnStmt(variable.getNameAsExpression())); getter.addModifier(PUBLIC, FINAL); } field.getAnnotationByName("Override") @@ -524,7 +560,4 @@ static void processFields(ClassOrInterfaceDeclaration target) { } } - private interface PreStep { - void applyOn(NodeList> types); - } -} \ No newline at end of file +} diff --git a/key.ncore.java/src/generator/java/org/key_project/ncore/java/PostSteps.java b/key.ncore.java/src/generator/java/org/key_project/ncore/java/PostSteps.java new file mode 100644 index 00000000000..442c58d2810 --- /dev/null +++ b/key.ncore.java/src/generator/java/org/key_project/ncore/java/PostSteps.java @@ -0,0 +1,157 @@ +/* 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 org.key_project.ncore.java; + +import java.nio.file.Paths; +import java.util.List; + +import com.github.javaparser.StaticJavaParser; +import com.github.javaparser.ast.CompilationUnit; +import com.github.javaparser.ast.Modifier; +import com.github.javaparser.ast.NodeList; +import com.github.javaparser.ast.body.ClassOrInterfaceDeclaration; +import com.github.javaparser.ast.expr.AssignExpr; +import com.github.javaparser.ast.expr.SimpleName; +import com.github.javaparser.ast.nodeTypes.modifiers.NodeWithPrivateModifier; +import com.github.javaparser.ast.stmt.BlockStmt; +import com.github.javaparser.ast.type.ClassOrInterfaceType; +import com.github.javaparser.ast.type.TypeParameter; +import com.github.javaparser.utils.SourceRoot; +import de.uka.ilkd.key.java.ast.expression.Assignment; +import de.uka.ilkd.key.java.ast.expression.ExpressionStatement; + +import static com.github.javaparser.ast.Modifier.DefaultKeyword.PUBLIC; +import static org.key_project.ncore.java.Generator.ROOT; + +public class PostSteps { + public static void createVisitor(List nodeUnits, SourceRoot sourceRoot) { + var cu = new CompilationUnit(); + String name = "org.key_project.key.java.ast.visitor"; + cu.setPackageDeclaration(name); + cu.setStorage(ROOT.resolve("org/key_project/java/ast/visitor/Visitor.java")); + System.out.println(cu.getStorage().get().getPath()); + + var generic = new TypeParameter("R"); + + var type = cu.addClass("Visitor"); + type.setInterface(true); + type.addTypeParameter(generic.clone()); + + for (CompilationUnit clazz : nodeUnits) { + try { + var t = clazz.getPrimaryType().get(); + if (!(t instanceof ClassOrInterfaceDeclaration c)) continue; + if (c.isInterface()) continue; + + cu.addImport(t.getFullyQualifiedName().get()); + + var m = type.addMethod("visit"); + m.addParameter(new ClassOrInterfaceType(null, t.getNameAsString()), "n"); + m.setType(generic.clone()); + m.setBody(null); + + var accept = t.addMethod("accept", PUBLIC); + accept.setType(generic.clone()); + accept.getTypeParameters().add(generic.clone()); + accept.addParameter(new ClassOrInterfaceType(null, new SimpleName(type.getFullyQualifiedName().get()), + new NodeList<>(generic.clone())), + "visitor"); + accept.getBody().get() + .addStatement("return visitor.visit(this);"); + } catch (Exception e) { + System.err.println(e.getMessage() + " :: " + clazz.getStorage().get().getPath()); + } + } + sourceRoot.add(cu); + } + + public static void createVoidVisitor(List nodeUnits, SourceRoot sourceRoot) { + var cu = new CompilationUnit(); + String name = "org.key_project.key.java.ast.visitor"; + cu.setPackageDeclaration(name); + cu.setStorage(ROOT.resolve("org/key_project/java/ast/visitor/VoidVisitor.java")); + System.out.println(cu.getStorage().get().getPath()); + + var type = cu.addClass("VoidVisitor"); + type.setInterface(true); + + for (CompilationUnit clazz : nodeUnits) { + try { + var t = clazz.getPrimaryType().get(); + if (!(t instanceof ClassOrInterfaceDeclaration c)) continue; + if (c.isInterface()) continue; + + cu.addImport(t.getFullyQualifiedName().get()); + + var m = type.addMethod("visit"); + m.addParameter(new ClassOrInterfaceType(null, t.getNameAsString()), "n"); + m.setBody(null); + + + var accept = t.addMethod("accept", PUBLIC); + accept.addParameter(new ClassOrInterfaceType(null, type.getFullyQualifiedName().get()), + "visitor"); + accept.getBody().get().addStatement("visitor.visit(this);"); + + + } catch (Exception e) { + System.err.println(e.getMessage() + " :: " + clazz.getStorage().get().getPath()); + } + } + sourceRoot.add(cu); + } + + public static void createTraversalVisitor(List nodeUnits, SourceRoot sourceRoot) { + var cu = new CompilationUnit(); + String name = "org.key_project.key.java.ast.visitor"; + cu.setPackageDeclaration(name); + cu.setStorage(ROOT.resolve("org/key_project/java/ast/visitor/TraversalVisitor.java")); + System.out.println(cu.getStorage().get().getPath()); + + var type = cu.addClass("TraversalVisitor", PUBLIC, + Modifier.DefaultKeyword.ABSTRACT); + type.getImplementedTypes().add( + (ClassOrInterfaceType) StaticJavaParser.parseType("Visitor")); + + for (CompilationUnit clazz : nodeUnits) { + try { + var t = clazz.getPrimaryType().get(); + cu.addImport(t.getFullyQualifiedName().get()); + + if (!(t instanceof ClassOrInterfaceDeclaration c)) continue; + if (c.isInterface()) continue; + + var m = type.addMethod("visit", PUBLIC); + m.addParameter(new ClassOrInterfaceType(null, t.getNameAsString()), "n"); + m.addAnnotation(Override.class); + BlockStmt body = m.getBody().get(); + body.addStatement("var b = n.builder();"); + t.getFields() + .stream().filter(NodeWithPrivateModifier::isPrivate) + .forEach(f -> + body.addStatement( + "b.%s = (%s) accept(n.%s());" + .formatted(f.getVariable(0).getNameAsExpression(), + f.getVariable(0).getTypeAsString(), + f.getVariable(0).getNameAsExpression()))); + body.addStatement("return b.build();"); + m.setType(new ClassOrInterfaceType(null, t.getFullyQualifiedName().get())); + } catch (Exception e) { + System.err.println(e.getMessage() + " :: " + clazz.getStorage().get().getPath()); + } + } + sourceRoot.add(cu); + } + + + public static void createDeepCopyVisitor(List nodeUnits, SourceRoot sourceRoot) { + + } + + public interface PostStep { + void applyOn(List nodeUnits, SourceRoot sourceRoot); + } + + +} diff --git a/key.ncore.java/src/generator/java/org/key_project/ncore/java/PreSteps.java b/key.ncore.java/src/generator/java/org/key_project/ncore/java/PreSteps.java new file mode 100644 index 00000000000..f015e41a485 --- /dev/null +++ b/key.ncore.java/src/generator/java/org/key_project/ncore/java/PreSteps.java @@ -0,0 +1,10 @@ +package org.key_project.ncore.java; + +import com.github.javaparser.ast.NodeList; +import com.github.javaparser.ast.body.TypeDeclaration; + +public class PreSteps { + interface PreStep { + void applyOn(NodeList> types); + } +} diff --git a/key.ncore.java/src/generator/java/org/key_project/ncore/java/ReadAllHierarchy.java b/key.ncore.java/src/generator/java/org/key_project/ncore/java/ReadAllHierarchy.java index 815478ac7fb..2a467876f97 100644 --- a/key.ncore.java/src/generator/java/org/key_project/ncore/java/ReadAllHierarchy.java +++ b/key.ncore.java/src/generator/java/org/key_project/ncore/java/ReadAllHierarchy.java @@ -1,7 +1,14 @@ +/* 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 org.key_project.ncore.java; -import com.github.javaparser.ast.body.ClassOrInterfaceDeclaration; -import com.github.javaparser.ast.type.ClassOrInterfaceType; +import java.io.File; +import java.io.FileNotFoundException; +import java.io.PrintWriter; +import java.lang.reflect.AccessFlag; +import java.util.*; + import de.uka.ilkd.key.java.ast.*; import de.uka.ilkd.key.java.ast.ccatch.*; import de.uka.ilkd.key.java.ast.declaration.*; @@ -20,12 +27,8 @@ import de.uka.ilkd.key.rule.AbstractProgramElement; import de.uka.ilkd.key.rule.metaconstruct.*; -import java.io.File; -import java.io.FileNotFoundException; -import java.io.PrintWriter; -import java.lang.reflect.AccessFlag; -import java.util.*; -import java.util.stream.Collectors; +import com.github.javaparser.ast.body.ClassOrInterfaceDeclaration; +import com.github.javaparser.ast.type.ClassOrInterfaceType; import static de.uka.ilkd.key.java.ast.declaration.modifier.Modifiers.*; @@ -37,715 +40,714 @@ */ public class ReadAllHierarchy { static Set> allClasses = new HashSet<>(List.of( - GreaterThan.class, - ExecutionContext.class, - ArrayLength.class, - SuperReference.class, - ProgramTransformer.class, - Instanceof.class, - ArrayInitializer.class, - ProgramSV.class, - Exec.class, - ThisReference.class, - MethodCall.class, - FieldDeclaration.class, - ForInitUnfoldTransformer.class, - SchemaTypeReference.class, - EnhancedForElimination.class, - IProgramVariable.class, - ClassDeclaration.class, - ContextStatementBlock.class, - MethodReference.class, - SpecialConstructorCall.class, - FloatLiteral.class, - TypeDeclaration.class, - PackageReference.class, - SuperConstructorReference.class, - SeqSub.class, - Positive.class, - SchematicFieldReference.class, - TypeCast.class, - ForToWhile.class, - LogicalOr.class, - LabelJumpStatement.class, - ReattachLoopInvariant.class, - Switch.class, - InterfaceDeclaration.class, - JML_NULLABLE_BY_DEFAULT.class, - PostDecrement.class, - Break.class, - TypeDeclaration.class, - CcatchContinueWildcardParameterDeclaration.class, - InitArrayCreation.class, - TypeRef.class, - UnsignedShiftRightAssignment.class, - EnumClassDeclaration.class, - CatchAllStatement.class, - LoopInit.class, - TypeReferenceImp.class, - MethodOrConstructorReference.class, - ForToWhile.class, - FieldReference.class, - PostIncrement.class, - ForToWhile.class, - MultipleVarDecl.class, - EnumClassDeclaration.class, - TypeDeclaration.class, - Break.class, - Conditional.class, - JavaDeclaration.class, - CompilationUnit.class, - PostWork.class, - JML_HELPER.class, - ReattachLoopInvariant.class, - ClassDeclaration.class, - ConstructorDeclaration.class, - LessOrEquals.class, - Modulo.class, - ThisReference.class, - UnwindLoop.class, - ArrayReference.class, - InterfaceDeclaration.class, - UnwindLoop.class, - EnhancedForElimination.class, - MethodCall.class, - PostWork.class, - LocalVariableDeclaration.class, - ReferencePrefix.class, - ExactInstanceof.class, - EvaluateArgs.class, - FieldReference.class, - EnumClassDeclaration.class, - ExpandMethodBody.class, - Switch.class, - Unpack.class, - ContextStatementBlock.class, - SpecialConstructorReference.class, - Exec.class, - ConstructorCall.class, - VariableNamer.IndProgramElementName.class, - IsStatic.class, - ProgramSV.class, - ArrayLength.class, - BranchStatement.class, - PostIncrement.class, - ProgramSV.class, - ForInitUnfoldTransformer.class, - PackageReference.class, - Operator.class, - Label.class, - TypeDeclaration.class, - JML_SPEC_PACKAGE.class, - SwitchToIf.class, - ExpandMethodBody.class, - ExpandMethodBody.class, - Instanceof.class, - Switch.class, - TypeReference.class, - CcatchContinueLabelParameterDeclaration.class, - ForInitUnfoldTransformer.class, - Throws.class, - SuperArrayDeclaration.class, - BinaryOrAssignment.class, - ExpandMethodBody.class, - UnsignedShiftRightAssignment.class, - Equals.class, - ProgramConstruct.class, - ExactInstanceof.class, - NotEquals.class, - PostIncrement.class, - ShiftRight.class, - SuperArrayDeclaration.class, - SchemaTypeReference.class, - TypeReferenceImp.class, - ForToWhile.class, - ConstructorCall.class, - FieldDeclaration.class, - LogicalAnd.class, - EvaluateArgs.class, - ParenthesizedExpression.class, - ConstructorCall.class, - SeqLength.class, - SeqConcat.class, - EnumClassDeclaration.class, - SuperConstructorReference.class, - PackageSpecification.class, - ClassInitializer.class, - ProgramSV.class, - PRIVATE.class, - InitArray.class, - UnwindLoop.class, - ExecutionContext.class, - ProgramConstruct.class, - New.class, - ArrayPostDecl.class, - For.class, - MethodFrame.class, - ForUpdates.class, - SuperArrayDeclaration.class, - Unpack.class, - ArrayLengthReference.class, - LoopInitializer.class, - ClassDeclaration.class, - DoBreak.class, - BranchStatement.class, - InterfaceDeclaration.class, - JavaDeclaration.class, - SetStatement.class, - Finally.class, - Ccatch.class, - EnhancedForElimination.class, - PassiveExpression.class, - SeqGet.class, - ArrayReference.class, - AllFields.class, - MethodDeclaration.class, - SwitchToIf.class, - For.class, - ConstructorCall.class, - ExpressionJumpStatement.class, - Case.class, - LoopScopeBlock.class, - SetMinus.class, - IntLiteral.class, - ThisReference.class, - ProgramTransformer.class, - ShiftRightAssignment.class, - Import.class, - SpecialConstructorCall.class, - PreDecrement.class, - Ghost.class, - LabelJumpStatement.class, - PostDecrement.class, - TypeCast.class, - EvaluateArgs.class, - StaticInitialisation.class, - MethodCall.class, - Unpack.class, - ConstructorReference.class, - ForUpdates.class, - ProgramTransformer.class, - ProgramElement.class, - Then.class, - SynchronizedBlock.class, - ArrayDeclaration.class, - NON_SEALED.class, - ShiftRight.class, - TypeOperator.class, - Extends.class, - GreaterOrEquals.class, - ArrayReference.class, - DoBreak.class, - SuperReference.class, - Abstract.class, - Catch.class, - UnsignedShiftRightAssignment.class, - TypeReferenceImp.class, - TypeOf.class, - LocationVariable.class, - Expression.class, - Transient.class, - AnnotationUseSpecification.class, - ExpandMethodBody.class, - SpecialConstructorReference.class, - BinaryXOr.class, - BinaryAndAssignment.class, - ForToWhile.class, - Equals.class, - PostWork.class, - SwitchToIf.class, - JavaStatement.class, - ArrayDeclaration.class, - MethodReference.class, - ThisConstructorReference.class, - JML_NO_STATE.class, - ProgramSV.class, - MethodDeclaration.class, - DoubleLiteral.class, - EnhancedFor.class, - ProgramConstruct.class, - Default.class, - FreeLiteral.class, - Literal.class, - InheritanceSpecification.class, - JML_PACKAGE.class, - ThisConstructorReference.class, - FieldReference.class, - PUBLIC.class, - SpecialConstructorCall.class, - BinaryXOrAssignment.class, - CcatchReturnValParameterDeclaration.class, - ClassInitializer.class, - Assert.class, - PostWork.class, - Break.class, - InitArrayCreation.class, - TypeDeclaration.class, - Singleton.class, - ExpandMethodBody.class, - Private.class, - CcatchBreakWildcardParameterDeclaration.class, - VariableDeclaration.class, - CreateObject.class, - InitArray.class, - IExecutionContext.class, - SchematicFieldReference.class, - JmlAssert.class, - VariableNamer.IndProgramElementName.class, - SeqPut.class, - Assignment.class, - MethodCall.class, - Try.class, - SeqIndexOf.class, - BinaryOr.class, - ConstructorCall.class, - JML_NON_NULL.class, - JML_SPEC_BIGINT_MATH.class, - ProgramConstruct.class, - Do.class, - CcatchReturnValParameterDeclaration.class, - IsStatic.class, - MethodReference.class, - ExpandMethodBody.class, - PostWork.class, - ConstructorDeclaration.class, - BinaryAnd.class, - If.class, - FieldReference.class, - SuperConstructorReference.class, - VariableNamer.IndProgramElementName.class, - Exec.class, - FieldDeclaration.class, - CreateObject.class, - LessThan.class, - LoopStatement.class, - Import.class, - ProgramConstruct.class, - Case.class, - UnwindLoop.class, - Catch.class, - EmptyMapLiteral.class, - VariableReference.class, - MethodReference.class, - TypeOperator.class, - JML_SPEC_PUBLIC.class, - TypeCast.class, - CreateObject.class, - JavaNonTerminalProgramElement.class, - Intersect.class, - TypeReferenceImp.class, - ArrayPostDecl.class, - PlusAssignment.class, - Times.class, - DoBreak.class, - ABSTRACT.class, - ForInitUnfoldTransformer.class, - ShiftLeftAssignment.class, - Protected.class, - TypeScope.class, - ForInitUnfoldTransformer.class, - IsStatic.class, - ClassDeclaration.class, - LogicalNot.class, - EmptySetLiteral.class, - ProgramSV.class, - Switch.class, - VariableDeclaration.class, - ForToWhile.class, - MultipleVarDecl.class, - SuperArrayDeclaration.class, - StaticInitialisation.class, - ConstructorDeclaration.class, - TypeOf.class, - InitArray.class, - MethodBodyStatement.class, - BinaryXOrAssignment.class, - SpecialConstructorCall.class, - CcatchBreakLabelParameterDeclaration.class, - ClassInitializer.class, - Guard.class, - Statement.class, - InterfaceDeclaration.class, - ConstructorCall.class, - Unpack.class, - MethodDeclaration.class, - ArrayPostDecl.class, - TypeOf.class, - EvaluateArgs.class, - SwitchToIf.class, - MultipleVarDecl.class, - Plus.class, - JumpStatement.class, - Times.class, - BinaryNot.class, - ConstructorDeclaration.class, - ClassDeclaration.class, - SeqIndexOf.class, - FieldSpecification.class, - MethodBodyStatement.class, - ProgramSV.class, - SeqConcat.class, - ModuloAssignment.class, - RealLiteral.class, - BinaryOperator.class, - BinaryXOr.class, - Then.class, - SpecialConstructorCall.class, - For.class, - TimesAssignment.class, - Unpack.class, - StringLiteral.class, - MethodDeclaration.class, - TypeDeclarationContainer.class, - Literal.class, - BooleanLiteral.class, - PreDecrement.class, - STRICTFP.class, - StatementBlock.class, - CcatchContinueLabelParameterDeclaration.class, - MultipleVarDecl.class, - LocalVariableDeclaration.class, - Reference.class, - TypeRef.class, - MultipleVarDecl.class, - ReattachLoopInvariant.class, - MethodDeclaration.class, - MultipleVarDecl.class, - EnhancedFor.class, - JML_INSTANCE.class, - Conditional.class, - UnwindLoop.class, - SpecialConstructorReference.class, - EnhancedForElimination.class, - While.class, - DoBreak.class, - UnsignedShiftRight.class, - MethodFrame.class, - ArrayLengthReference.class, - SpecialConstructorReference.class, - IsStatic.class, - Else.class, - JML_OT_REP.class, - ProgramTransformer.class, - MethodCall.class, - NameReference.class, - ForUpdates.class, - ConstructorCall.class, - ConstructorDeclaration.class, - MethodReference.class, - Assert.class, - SwitchToIf.class, - ArrayPostDecl.class, - CopyAssignment.class, - FieldSpecification.class, - InitArrayCreation.class, - UnwindLoop.class, - Exec.class, - TypeOf.class, - SeqIndexOf.class, - TypeRef.class, - VOLATILE.class, - EvaluateArgs.class, - SEALED.class, - LogicalNot.class, - DoBreak.class, - CcatchContinueParameterDeclaration.class, - ProgramSV.class, - Modulo.class, - EnhancedForElimination.class, - ProgramConstruct.class, - ProgramMethod.class, - MethodName.class, - Default.class, - ProgramTransformer.class, - JML_CODE.class, - ModuloAssignment.class, - ShiftLeft.class, - Negative.class, - Case.class, - NewArray.class, - Ccatch.class, - Switch.class, - MethodCall.class, - ProgramConstant.class, - PackageReferenceContainer.class, - BinaryOrAssignment.class, - TypeReferenceInfix.class, - ComparativeOperator.class, - DoBreak.class, - PreDecrement.class, - UnsignedShiftRightAssignment.class, - InitArrayCreation.class, - JML_SPEC_PRIVATE.class, - StatementBlock.class, - ProgramConstruct.class, - FieldDeclaration.class, - FieldReference.class, - ExpandMethodBody.class, - PROTECTED.class, - Finally.class, - SuperArrayDeclaration.class, - Do.class, - AbstractIntegerLiteral.class, - MethodCall.class, - ExpandMethodBody.class, - Extends.class, - SchematicFieldReference.class, - StaticInitialisation.class, - TypeOf.class, - JML_CODE_JAVA_MATH.class, - LoopStatement.class, - SeqPut.class, - SpecialConstructorReference.class, - TypeCast.class, - JML_STRICTLY_PURE.class, - DLEmbeddedExpression.class, - ReattachLoopInvariant.class, - TypeRef.class, - IProgramMethod.class, - CcatchContinueParameterDeclaration.class, - PreIncrement.class, - TypeOf.class, - MergePointStatement.class, - CharLiteral.class, - ModuloAssignment.class, - ConstructorReference.class, - JML_UNPARSABLE_MODIFIERS.class, - MultipleVarDecl.class, - PostWork.class, - SchemaTypeReference.class, - ArrayPostDecl.class, - ScopeDefiningElement.class, - JavaStatement.class, - CharLiteral.class, - Divide.class, - TypeRef.class, - InheritanceSpecification.class, - ComparativeOperator.class, - SetMinus.class, - EmptyStatement.class, - SwitchToIf.class, - SchematicFieldReference.class, - DoBreak.class, - JML_NULLABLE.class, - SeqReverse.class, - Try.class, - LoopInit.class, - ExpressionContainer.class, - IsStatic.class, - ProgramConstruct.class, - New.class, - EmptySetLiteral.class, - ForInitUnfoldTransformer.class, - BinaryOperator.class, - LabeledStatement.class, - MinusAssignment.class, - Operator.class, - MethodDeclaration.class, - MethodReference.class, - Extends.class, - ForToWhile.class, - IsStatic.class, - GreaterOrEquals.class, - Native.class, - ShiftLeftAssignment.class, - LabeledStatement.class, - ArrayReference.class, - PackageReference.class, - Unpack.class, - Minus.class, - MemberDeclaration.class, - SpecialConstructorCall.class, - Divide.class, - MemberReference.class, - TypeReference.class, - InitArray.class, - SchematicFieldReference.class, - ExpandMethodBody.class, - Throws.class, - IForUpdates.class, - Volatile.class, - SuperReference.class, - StaticInitialisation.class, - ExpressionStatement.class, - TypeRef.class, - SchematicFieldReference.class, - InheritanceSpecification.class, - Catch.class, - LogicalOr.class, - ModuloAssignment.class, - Import.class, - Catch.class, - ProgramElementName.class, - InterfaceDeclaration.class, - Instanceof.class, - New.class, - Continue.class, - ProgramSV.class, - SchematicFieldReference.class, - Implements.class, - BinaryAnd.class, - ShiftLeftAssignment.class, - PreDecrement.class, - Ccatch.class, - Static.class, - Return.class, - TRANSIENT.class, - PackageSpecification.class, - TypeOperator.class, - TypeReferenceImp.class, - Branch.class, - Operator.class, - Exec.class, - ReattachLoopInvariant.class, - Divide.class, - AllFields.class, - SeqLength.class, - ForToWhile.class, - NamedProgramElement.class, - JML_NON_NULL_ELEMENTS.class, - MethodFrame.class, - VariableSpecification.class, - BranchImp.class, - CreateObject.class, - Try.class, - BinaryOperator.class, - ProgramConstant.class, - ProgramVariable.class, - Switch.class, - MinusAssignment.class, - PostIncrement.class, - SeqReverse.class, - SetUnion.class, - MethodFrame.class, - Guard.class, - JML_PURE.class, - CcatchReturnValParameterDeclaration.class, - PlusAssignment.class, - LessOrEquals.class, - InitArray.class, - Assert.class, - EnhancedForElimination.class, - EnhancedForElimination.class, - SchematicFieldReference.class, - LogicalAnd.class, - JML_SPEC_PROTECTED.class, - Equals.class, - ConstructorReference.class, - ConstructorDeclaration.class, - ShiftLeft.class, - SwitchToIf.class, - SuperConstructorReference.class, - Guard.class, - ArrayDeclaration.class, - ProgramVariable.class, - ProgramMethod.class, - IsStatic.class, - IsStatic.class, - MergePointStatement.class, - PostDecrement.class, - For.class, - StaticInitialisation.class, - ProgramTransformer.class, - MultipleVarDecl.class, - SchemaTypeReference.class, - EnumClassDeclaration.class, - TypeRef.class, - FieldDeclaration.class, - FINAL.class, - MetaClassReference.class, - SeqSingleton.class, - LocalVariableDeclaration.class, - IGuard.class, - ProgramVariableName.class, - ProgramConstruct.class, - SchemaTypeReference.class, - Else.class, - ProgramConstruct.class, - Continue.class, - TypeRef.class, - TypeRef.class, - ReattachLoopInvariant.class, - ConstructorCall.class, - EnumClassDeclaration.class, - Do.class, - MethodCall.class, - BinaryOrAssignment.class, - ArrayLengthReference.class, - Positive.class, - SchematicFieldReference.class, - PostWork.class, - EmptyStatement.class, - SpecialConstructorCall.class, - Break.class, - ForUpdates.class, - ArrayPostDecl.class, - EvaluateArgs.class, - InitArray.class, - MethodDeclaration.class, - TypeReferenceImp.class, - Unpack.class, - InitArray.class, - TimesAssignment.class, - MethodReference.class, - ReattachLoopInvariant.class, - ProgramConstruct.class, - IsStatic.class, - JavaDeclaration.class, - Catch.class, - DivideAssignment.class, - ProgramPrefix.class, - SuperReference.class, - LabelJumpStatement.class, - Throw.class, - TypeReference.class, - CatchAllStatement.class, - InitArray.class, - ClassInitializer.class, - TypeRef.class, - BranchImp.class, - TransactionStatement.class, - ParameterContainer.class, - VariableScope.class, - Final.class, - DEFAULT.class, - TRANSITIVE.class, - StatementContainer.class, - NATIVE.class, - TypeReferenceContainer.class, - TerminalProgramElement.class, - SYNCHRONIZED.class, - JML_OT_READ_ONLY.class, - NoState.class, - Modifier.class, - VisibilityModifier.class, - CcatchReturnParameterDeclaration.class, - VariableNamer.PermIndProgramElementName.class, - Subtype.class, - AllObjects.class, - Declaration.class, - JML_CODE_BIGINT_MATH.class, - JavaProgramElement.class, - LongLiteral.class, - ParameterDeclaration.class, - JML_SPEC_JAVA_MATH.class, - TwoState.class, - ILoopInit.class, - Model.class, - ReferenceSuffix.class, - JML_TWO_STATE.class, - CcatchNonstandardParameterDeclaration.class, - StrictFp.class, - EmptySeqLiteral.class, - AbstractProgramElement.class, - Synchronized.class, - JML_NON_NULL_BY_DEFAULT.class, - JML_CODE_SAFE_MATH.class, - Public.class, - JML_SPEC_SAFE_MATH.class, - VariableNamer.TempIndProgramElementName.class, - Modifiers.STATIC.class - )); + GreaterThan.class, + ExecutionContext.class, + ArrayLength.class, + SuperReference.class, + ProgramTransformer.class, + Instanceof.class, + ArrayInitializer.class, + ProgramSV.class, + Exec.class, + ThisReference.class, + MethodCall.class, + FieldDeclaration.class, + ForInitUnfoldTransformer.class, + SchemaTypeReference.class, + EnhancedForElimination.class, + IProgramVariable.class, + ClassDeclaration.class, + ContextStatementBlock.class, + MethodReference.class, + SpecialConstructorCall.class, + FloatLiteral.class, + TypeDeclaration.class, + PackageReference.class, + SuperConstructorReference.class, + SeqSub.class, + Positive.class, + SchematicFieldReference.class, + TypeCast.class, + ForToWhile.class, + LogicalOr.class, + LabelJumpStatement.class, + ReattachLoopInvariant.class, + Switch.class, + InterfaceDeclaration.class, + JML_NULLABLE_BY_DEFAULT.class, + PostDecrement.class, + Break.class, + TypeDeclaration.class, + CcatchContinueWildcardParameterDeclaration.class, + InitArrayCreation.class, + TypeRef.class, + UnsignedShiftRightAssignment.class, + EnumClassDeclaration.class, + CatchAllStatement.class, + LoopInit.class, + TypeReferenceImp.class, + MethodOrConstructorReference.class, + ForToWhile.class, + FieldReference.class, + PostIncrement.class, + ForToWhile.class, + MultipleVarDecl.class, + EnumClassDeclaration.class, + TypeDeclaration.class, + Break.class, + Conditional.class, + JavaDeclaration.class, + CompilationUnit.class, + PostWork.class, + JML_HELPER.class, + ReattachLoopInvariant.class, + ClassDeclaration.class, + ConstructorDeclaration.class, + LessOrEquals.class, + Modulo.class, + ThisReference.class, + UnwindLoop.class, + ArrayReference.class, + InterfaceDeclaration.class, + UnwindLoop.class, + EnhancedForElimination.class, + MethodCall.class, + PostWork.class, + LocalVariableDeclaration.class, + ReferencePrefix.class, + ExactInstanceof.class, + EvaluateArgs.class, + FieldReference.class, + EnumClassDeclaration.class, + ExpandMethodBody.class, + Switch.class, + Unpack.class, + ContextStatementBlock.class, + SpecialConstructorReference.class, + Exec.class, + ConstructorCall.class, + VariableNamer.IndProgramElementName.class, + IsStatic.class, + ProgramSV.class, + ArrayLength.class, + BranchStatement.class, + PostIncrement.class, + ProgramSV.class, + ForInitUnfoldTransformer.class, + PackageReference.class, + Operator.class, + Label.class, + TypeDeclaration.class, + JML_SPEC_PACKAGE.class, + SwitchToIf.class, + ExpandMethodBody.class, + ExpandMethodBody.class, + Instanceof.class, + Switch.class, + TypeReference.class, + CcatchContinueLabelParameterDeclaration.class, + ForInitUnfoldTransformer.class, + Throws.class, + SuperArrayDeclaration.class, + BinaryOrAssignment.class, + ExpandMethodBody.class, + UnsignedShiftRightAssignment.class, + Equals.class, + ProgramConstruct.class, + ExactInstanceof.class, + NotEquals.class, + PostIncrement.class, + ShiftRight.class, + SuperArrayDeclaration.class, + SchemaTypeReference.class, + TypeReferenceImp.class, + ForToWhile.class, + ConstructorCall.class, + FieldDeclaration.class, + LogicalAnd.class, + EvaluateArgs.class, + ParenthesizedExpression.class, + ConstructorCall.class, + SeqLength.class, + SeqConcat.class, + EnumClassDeclaration.class, + SuperConstructorReference.class, + PackageSpecification.class, + ClassInitializer.class, + ProgramSV.class, + PRIVATE.class, + InitArray.class, + UnwindLoop.class, + ExecutionContext.class, + ProgramConstruct.class, + New.class, + ArrayPostDecl.class, + For.class, + MethodFrame.class, + ForUpdates.class, + SuperArrayDeclaration.class, + Unpack.class, + ArrayLengthReference.class, + LoopInitializer.class, + ClassDeclaration.class, + DoBreak.class, + BranchStatement.class, + InterfaceDeclaration.class, + JavaDeclaration.class, + SetStatement.class, + Finally.class, + Ccatch.class, + EnhancedForElimination.class, + PassiveExpression.class, + SeqGet.class, + ArrayReference.class, + AllFields.class, + MethodDeclaration.class, + SwitchToIf.class, + For.class, + ConstructorCall.class, + ExpressionJumpStatement.class, + Case.class, + LoopScopeBlock.class, + SetMinus.class, + IntLiteral.class, + ThisReference.class, + ProgramTransformer.class, + ShiftRightAssignment.class, + Import.class, + SpecialConstructorCall.class, + PreDecrement.class, + Ghost.class, + LabelJumpStatement.class, + PostDecrement.class, + TypeCast.class, + EvaluateArgs.class, + StaticInitialisation.class, + MethodCall.class, + Unpack.class, + ConstructorReference.class, + ForUpdates.class, + ProgramTransformer.class, + ProgramElement.class, + Then.class, + SynchronizedBlock.class, + ArrayDeclaration.class, + NON_SEALED.class, + ShiftRight.class, + TypeOperator.class, + Extends.class, + GreaterOrEquals.class, + ArrayReference.class, + DoBreak.class, + SuperReference.class, + Abstract.class, + Catch.class, + UnsignedShiftRightAssignment.class, + TypeReferenceImp.class, + TypeOf.class, + LocationVariable.class, + Expression.class, + Transient.class, + AnnotationUseSpecification.class, + ExpandMethodBody.class, + SpecialConstructorReference.class, + BinaryXOr.class, + BinaryAndAssignment.class, + ForToWhile.class, + Equals.class, + PostWork.class, + SwitchToIf.class, + JavaStatement.class, + ArrayDeclaration.class, + MethodReference.class, + ThisConstructorReference.class, + JML_NO_STATE.class, + ProgramSV.class, + MethodDeclaration.class, + DoubleLiteral.class, + EnhancedFor.class, + ProgramConstruct.class, + Default.class, + FreeLiteral.class, + Literal.class, + InheritanceSpecification.class, + JML_PACKAGE.class, + ThisConstructorReference.class, + FieldReference.class, + PUBLIC.class, + SpecialConstructorCall.class, + BinaryXOrAssignment.class, + CcatchReturnValParameterDeclaration.class, + ClassInitializer.class, + Assert.class, + PostWork.class, + Break.class, + InitArrayCreation.class, + TypeDeclaration.class, + Singleton.class, + ExpandMethodBody.class, + Private.class, + CcatchBreakWildcardParameterDeclaration.class, + VariableDeclaration.class, + CreateObject.class, + InitArray.class, + IExecutionContext.class, + SchematicFieldReference.class, + JmlAssert.class, + VariableNamer.IndProgramElementName.class, + SeqPut.class, + Assignment.class, + MethodCall.class, + Try.class, + SeqIndexOf.class, + BinaryOr.class, + ConstructorCall.class, + JML_NON_NULL.class, + JML_SPEC_BIGINT_MATH.class, + ProgramConstruct.class, + Do.class, + CcatchReturnValParameterDeclaration.class, + IsStatic.class, + MethodReference.class, + ExpandMethodBody.class, + PostWork.class, + ConstructorDeclaration.class, + BinaryAnd.class, + If.class, + FieldReference.class, + SuperConstructorReference.class, + VariableNamer.IndProgramElementName.class, + Exec.class, + FieldDeclaration.class, + CreateObject.class, + LessThan.class, + LoopStatement.class, + Import.class, + ProgramConstruct.class, + Case.class, + UnwindLoop.class, + Catch.class, + EmptyMapLiteral.class, + VariableReference.class, + MethodReference.class, + TypeOperator.class, + JML_SPEC_PUBLIC.class, + TypeCast.class, + CreateObject.class, + JavaNonTerminalProgramElement.class, + Intersect.class, + TypeReferenceImp.class, + ArrayPostDecl.class, + PlusAssignment.class, + Times.class, + DoBreak.class, + ABSTRACT.class, + ForInitUnfoldTransformer.class, + ShiftLeftAssignment.class, + Protected.class, + TypeScope.class, + ForInitUnfoldTransformer.class, + IsStatic.class, + ClassDeclaration.class, + LogicalNot.class, + EmptySetLiteral.class, + ProgramSV.class, + Switch.class, + VariableDeclaration.class, + ForToWhile.class, + MultipleVarDecl.class, + SuperArrayDeclaration.class, + StaticInitialisation.class, + ConstructorDeclaration.class, + TypeOf.class, + InitArray.class, + MethodBodyStatement.class, + BinaryXOrAssignment.class, + SpecialConstructorCall.class, + CcatchBreakLabelParameterDeclaration.class, + ClassInitializer.class, + Guard.class, + Statement.class, + InterfaceDeclaration.class, + ConstructorCall.class, + Unpack.class, + MethodDeclaration.class, + ArrayPostDecl.class, + TypeOf.class, + EvaluateArgs.class, + SwitchToIf.class, + MultipleVarDecl.class, + Plus.class, + JumpStatement.class, + Times.class, + BinaryNot.class, + ConstructorDeclaration.class, + ClassDeclaration.class, + SeqIndexOf.class, + FieldSpecification.class, + MethodBodyStatement.class, + ProgramSV.class, + SeqConcat.class, + ModuloAssignment.class, + RealLiteral.class, + BinaryOperator.class, + BinaryXOr.class, + Then.class, + SpecialConstructorCall.class, + For.class, + TimesAssignment.class, + Unpack.class, + StringLiteral.class, + MethodDeclaration.class, + TypeDeclarationContainer.class, + Literal.class, + BooleanLiteral.class, + PreDecrement.class, + STRICTFP.class, + StatementBlock.class, + CcatchContinueLabelParameterDeclaration.class, + MultipleVarDecl.class, + LocalVariableDeclaration.class, + Reference.class, + TypeRef.class, + MultipleVarDecl.class, + ReattachLoopInvariant.class, + MethodDeclaration.class, + MultipleVarDecl.class, + EnhancedFor.class, + JML_INSTANCE.class, + Conditional.class, + UnwindLoop.class, + SpecialConstructorReference.class, + EnhancedForElimination.class, + While.class, + DoBreak.class, + UnsignedShiftRight.class, + MethodFrame.class, + ArrayLengthReference.class, + SpecialConstructorReference.class, + IsStatic.class, + Else.class, + JML_OT_REP.class, + ProgramTransformer.class, + MethodCall.class, + NameReference.class, + ForUpdates.class, + ConstructorCall.class, + ConstructorDeclaration.class, + MethodReference.class, + Assert.class, + SwitchToIf.class, + ArrayPostDecl.class, + CopyAssignment.class, + FieldSpecification.class, + InitArrayCreation.class, + UnwindLoop.class, + Exec.class, + TypeOf.class, + SeqIndexOf.class, + TypeRef.class, + VOLATILE.class, + EvaluateArgs.class, + SEALED.class, + LogicalNot.class, + DoBreak.class, + CcatchContinueParameterDeclaration.class, + ProgramSV.class, + Modulo.class, + EnhancedForElimination.class, + ProgramConstruct.class, + ProgramMethod.class, + MethodName.class, + Default.class, + ProgramTransformer.class, + JML_CODE.class, + ModuloAssignment.class, + ShiftLeft.class, + Negative.class, + Case.class, + NewArray.class, + Ccatch.class, + Switch.class, + MethodCall.class, + ProgramConstant.class, + PackageReferenceContainer.class, + BinaryOrAssignment.class, + TypeReferenceInfix.class, + ComparativeOperator.class, + DoBreak.class, + PreDecrement.class, + UnsignedShiftRightAssignment.class, + InitArrayCreation.class, + JML_SPEC_PRIVATE.class, + StatementBlock.class, + ProgramConstruct.class, + FieldDeclaration.class, + FieldReference.class, + ExpandMethodBody.class, + PROTECTED.class, + Finally.class, + SuperArrayDeclaration.class, + Do.class, + AbstractIntegerLiteral.class, + MethodCall.class, + ExpandMethodBody.class, + Extends.class, + SchematicFieldReference.class, + StaticInitialisation.class, + TypeOf.class, + JML_CODE_JAVA_MATH.class, + LoopStatement.class, + SeqPut.class, + SpecialConstructorReference.class, + TypeCast.class, + JML_STRICTLY_PURE.class, + DLEmbeddedExpression.class, + ReattachLoopInvariant.class, + TypeRef.class, + IProgramMethod.class, + CcatchContinueParameterDeclaration.class, + PreIncrement.class, + TypeOf.class, + MergePointStatement.class, + CharLiteral.class, + ModuloAssignment.class, + ConstructorReference.class, + JML_UNPARSABLE_MODIFIERS.class, + MultipleVarDecl.class, + PostWork.class, + SchemaTypeReference.class, + ArrayPostDecl.class, + ScopeDefiningElement.class, + JavaStatement.class, + CharLiteral.class, + Divide.class, + TypeRef.class, + InheritanceSpecification.class, + ComparativeOperator.class, + SetMinus.class, + EmptyStatement.class, + SwitchToIf.class, + SchematicFieldReference.class, + DoBreak.class, + JML_NULLABLE.class, + SeqReverse.class, + Try.class, + LoopInit.class, + ExpressionContainer.class, + IsStatic.class, + ProgramConstruct.class, + New.class, + EmptySetLiteral.class, + ForInitUnfoldTransformer.class, + BinaryOperator.class, + LabeledStatement.class, + MinusAssignment.class, + Operator.class, + MethodDeclaration.class, + MethodReference.class, + Extends.class, + ForToWhile.class, + IsStatic.class, + GreaterOrEquals.class, + Native.class, + ShiftLeftAssignment.class, + LabeledStatement.class, + ArrayReference.class, + PackageReference.class, + Unpack.class, + Minus.class, + MemberDeclaration.class, + SpecialConstructorCall.class, + Divide.class, + MemberReference.class, + TypeReference.class, + InitArray.class, + SchematicFieldReference.class, + ExpandMethodBody.class, + Throws.class, + IForUpdates.class, + Volatile.class, + SuperReference.class, + StaticInitialisation.class, + ExpressionStatement.class, + TypeRef.class, + SchematicFieldReference.class, + InheritanceSpecification.class, + Catch.class, + LogicalOr.class, + ModuloAssignment.class, + Import.class, + Catch.class, + ProgramElementName.class, + InterfaceDeclaration.class, + Instanceof.class, + New.class, + Continue.class, + ProgramSV.class, + SchematicFieldReference.class, + Implements.class, + BinaryAnd.class, + ShiftLeftAssignment.class, + PreDecrement.class, + Ccatch.class, + Static.class, + Return.class, + TRANSIENT.class, + PackageSpecification.class, + TypeOperator.class, + TypeReferenceImp.class, + Branch.class, + Operator.class, + Exec.class, + ReattachLoopInvariant.class, + Divide.class, + AllFields.class, + SeqLength.class, + ForToWhile.class, + NamedProgramElement.class, + JML_NON_NULL_ELEMENTS.class, + MethodFrame.class, + VariableSpecification.class, + BranchImp.class, + CreateObject.class, + Try.class, + BinaryOperator.class, + ProgramConstant.class, + ProgramVariable.class, + Switch.class, + MinusAssignment.class, + PostIncrement.class, + SeqReverse.class, + SetUnion.class, + MethodFrame.class, + Guard.class, + JML_PURE.class, + CcatchReturnValParameterDeclaration.class, + PlusAssignment.class, + LessOrEquals.class, + InitArray.class, + Assert.class, + EnhancedForElimination.class, + EnhancedForElimination.class, + SchematicFieldReference.class, + LogicalAnd.class, + JML_SPEC_PROTECTED.class, + Equals.class, + ConstructorReference.class, + ConstructorDeclaration.class, + ShiftLeft.class, + SwitchToIf.class, + SuperConstructorReference.class, + Guard.class, + ArrayDeclaration.class, + ProgramVariable.class, + ProgramMethod.class, + IsStatic.class, + IsStatic.class, + MergePointStatement.class, + PostDecrement.class, + For.class, + StaticInitialisation.class, + ProgramTransformer.class, + MultipleVarDecl.class, + SchemaTypeReference.class, + EnumClassDeclaration.class, + TypeRef.class, + FieldDeclaration.class, + FINAL.class, + MetaClassReference.class, + SeqSingleton.class, + LocalVariableDeclaration.class, + IGuard.class, + ProgramVariableName.class, + ProgramConstruct.class, + SchemaTypeReference.class, + Else.class, + ProgramConstruct.class, + Continue.class, + TypeRef.class, + TypeRef.class, + ReattachLoopInvariant.class, + ConstructorCall.class, + EnumClassDeclaration.class, + Do.class, + MethodCall.class, + BinaryOrAssignment.class, + ArrayLengthReference.class, + Positive.class, + SchematicFieldReference.class, + PostWork.class, + EmptyStatement.class, + SpecialConstructorCall.class, + Break.class, + ForUpdates.class, + ArrayPostDecl.class, + EvaluateArgs.class, + InitArray.class, + MethodDeclaration.class, + TypeReferenceImp.class, + Unpack.class, + InitArray.class, + TimesAssignment.class, + MethodReference.class, + ReattachLoopInvariant.class, + ProgramConstruct.class, + IsStatic.class, + JavaDeclaration.class, + Catch.class, + DivideAssignment.class, + ProgramPrefix.class, + SuperReference.class, + LabelJumpStatement.class, + Throw.class, + TypeReference.class, + CatchAllStatement.class, + InitArray.class, + ClassInitializer.class, + TypeRef.class, + BranchImp.class, + TransactionStatement.class, + ParameterContainer.class, + VariableScope.class, + Final.class, + DEFAULT.class, + TRANSITIVE.class, + StatementContainer.class, + NATIVE.class, + TypeReferenceContainer.class, + TerminalProgramElement.class, + SYNCHRONIZED.class, + JML_OT_READ_ONLY.class, + NoState.class, + Modifier.class, + VisibilityModifier.class, + CcatchReturnParameterDeclaration.class, + VariableNamer.PermIndProgramElementName.class, + Subtype.class, + AllObjects.class, + Declaration.class, + JML_CODE_BIGINT_MATH.class, + JavaProgramElement.class, + LongLiteral.class, + ParameterDeclaration.class, + JML_SPEC_JAVA_MATH.class, + TwoState.class, + ILoopInit.class, + Model.class, + ReferenceSuffix.class, + JML_TWO_STATE.class, + CcatchNonstandardParameterDeclaration.class, + StrictFp.class, + EmptySeqLiteral.class, + AbstractProgramElement.class, + Synchronized.class, + JML_NON_NULL_BY_DEFAULT.class, + JML_CODE_SAFE_MATH.class, + Public.class, + JML_SPEC_SAFE_MATH.class, + VariableNamer.TempIndProgramElementName.class, + Modifiers.STATIC.class)); public static void main(String[] args) throws FileNotFoundException { var all = new TreeSet>(Comparator.comparing(Class::getName)); @@ -758,10 +760,11 @@ public static void main(String[] args) throws FileNotFoundException { var r = new ClassOrInterfaceDeclaration(); r.setName(clazz.getSimpleName()); if (clazz.getSuperclass() != null) { - r.getExtendedTypes().add(new ClassOrInterfaceType(null, clazz.getSuperclass().getSimpleName())); + r.getExtendedTypes() + .add(new ClassOrInterfaceType(null, clazz.getSuperclass().getSimpleName())); } - if(clazz.accessFlags().contains(AccessFlag.ABSTRACT)) { + if (clazz.accessFlags().contains(AccessFlag.ABSTRACT)) { r.addModifier(com.github.javaparser.ast.Modifier.DefaultKeyword.ABSTRACT); } @@ -772,13 +775,13 @@ public static void main(String[] args) throws FileNotFoundException { continue; String type; - if(declaredField.getType().getTypeParameters().length==0) + if (declaredField.getType().getTypeParameters().length == 0) type = declaredField.getType().getSimpleName(); else { type = declaredField.getGenericType().toString(); int j = type.lastIndexOf('<'); int i = type.lastIndexOf('.', j); - type = type.substring(i+1); + type = type.substring(i + 1); } System.out.println(type); r.addField(type, declaredField.getName()); @@ -788,7 +791,8 @@ public static void main(String[] args) throws FileNotFoundException { cu.addType(r); } - try (var out = new PrintWriter(new File("key.ncore.java/src/adt/java-ast.java").getAbsoluteFile())) { + try (var out = + new PrintWriter(new File("key.ncore.java/src/adt/java-ast.java").getAbsoluteFile())) { out.write(cu.toString()); } } diff --git a/key.ncore.java/src/main/java/org/key_project/java/ast/AssignmentKind.java b/key.ncore.java/src/main/java/org/key_project/java/ast/AssignmentKind.java new file mode 100644 index 00000000000..bcac500f06e --- /dev/null +++ b/key.ncore.java/src/main/java/org/key_project/java/ast/AssignmentKind.java @@ -0,0 +1,22 @@ +package org.key_project.java.ast; + +public enum AssignmentKind { + Copy(""), + BinaryOr("|"), + Divide("/"), + ShiftLeft("<<"), + UnsignedShiftRight(">>>"), + Plus("+"), + ShiftRight(">>"), + Minus("-"), + Modulo("%"), + Times("*"), + BinaryAnd("&"), + BinaryXOr("^"); + + public final String symbol; + + AssignmentKind(String symbol) { + this.symbol = symbol; + } + } diff --git a/key.ncore.java/src/main/java/org/key_project/java/ast/BinaryOperatorKind.java b/key.ncore.java/src/main/java/org/key_project/java/ast/BinaryOperatorKind.java new file mode 100644 index 00000000000..1127a948521 --- /dev/null +++ b/key.ncore.java/src/main/java/org/key_project/java/ast/BinaryOperatorKind.java @@ -0,0 +1,37 @@ +package org.key_project.java.ast; + +public enum BinaryOperatorKind { + DIVIDE(2, "/"), + MODULO(2, "%"), + TIMES(2, "*"), + MINUS(3, "-"), + PLUS(3, "+"), + SUBTYPE(3, "<:"), + + SHIFT_LEFT(4, "<<"), + SHIFT_RIGHT(4, ">>"), + UNSIGNED_SHIFT_RIGHT(4, ">>>"), + + GREATER_OR_EQUALS(5, ">="), + LESS_OR_EQUALS(5, "<="), + GREATER_THAN(5, ">"), + LESS_THAN(5, "<"), + EQUALS(6, "=="), + NOT_EQUALS(6, "!="), + + + BINARY_AND(7, "&"), + BINARY_XOR(8, "^"), + BINARY_OR(9, "|"), + LOGICAL_AND(10, "&&"), + LOGICAL_OR(11, "||"); + + + public final int precedence; + public final String symbol; + + BinaryOperatorKind(int precedence, String symbol) { + this.precedence = precedence; + this.symbol = symbol; + } +} diff --git a/key.ncore.java/src/main/java/org/key_project/java/ast/DefaultProperties.java b/key.ncore.java/src/main/java/org/key_project/java/ast/DefaultProperties.java index 9fad13f846e..12e5d82909d 100644 --- a/key.ncore.java/src/main/java/org/key_project/java/ast/DefaultProperties.java +++ b/key.ncore.java/src/main/java/org/key_project/java/ast/DefaultProperties.java @@ -1,3 +1,6 @@ +/* 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 org.key_project.java.ast; import java.util.HashMap; diff --git a/key.ncore.java/src/main/java/org/key_project/java/ast/EqEx.java b/key.ncore.java/src/main/java/org/key_project/java/ast/EqEx.java new file mode 100644 index 00000000000..f918f7c6897 --- /dev/null +++ b/key.ncore.java/src/main/java/org/key_project/java/ast/EqEx.java @@ -0,0 +1,12 @@ +package org.key_project.java.ast; + + +import java.lang.annotation.ElementType; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; + +@Retention(RetentionPolicy.SOURCE) +@Target(ElementType.FIELD) +public @interface EqEx { +} diff --git a/key.ncore.java/src/main/java/org/key_project/java/ast/LogicFunction.java b/key.ncore.java/src/main/java/org/key_project/java/ast/LogicFunction.java new file mode 100644 index 00000000000..8f6ae183565 --- /dev/null +++ b/key.ncore.java/src/main/java/org/key_project/java/ast/LogicFunction.java @@ -0,0 +1,31 @@ +package org.key_project.java.ast; + +public enum LogicFunction { + Intersect(2, 1, PrimitiveType.JAVA_LOCSET, AsFunction("\\intersect")), + SetUnion(2, 1, PrimitiveType.JAVA_LOCSET, AsFunction("\\set_union")), + SetMinus(2, 1, PrimitiveType.JAVA_LOCSET, AsFunction("\\set_minus")), + AllObjects(1, 1, PrimitiveType.JAVA_LOCSET, AsFunction("\\all_objects")), + SeqPut(3, 1, PrimitiveType.JAVA_SEQ, AsFunction("\\seq_upd")), + SeqGet(1, 1, PrimitiveType.JAVA_INT, AsArrayAccess()), + SeqReverse(1, 1, PrimitiveType.JAVA_SEQ, AsFunction("\\seq_reverse")), + AllFields(1, 1, PrimitiveType.JAVA_LOCSET, AsFunction("\\all_fields")), + SeqIndexOf(2, 1, PrimitiveType.JAVA_INT, AsFunction("\\indexOf")), + SeqSingleton(1, 1, PrimitiveType.JAVA_SEQ, AsFunction("\\seq_singleton")), + SeqSub(3, 1, PrimitiveType.JAVA_SEQ, AsFunction("\\seq_sub")), + SeqConcat(2, 1, PrimitiveType.JAVA_SEQ, AsFunction("\\seq_concat")), + Singleton(1, 1, PrimitiveType.JAVA_LOCSET, AsFunction("\\singleton")), + SeqLength(1, 1, PrimitiveType.JAVA_INT, AsSuffix("length")); + + public final int arity; + public final int precedence; + public final PrimitiveType returnType; + public final PrettyPrinter.PrintOp format; + + LogicFunction(int arity, int precedence, PrimitiveType returnType, + PrettyPrinter.PrintOp format) { + this.arity = arity; + this.precedence = precedence; + this.returnType = returnType; + this.format = format; + } + } diff --git a/key.ncore.java/src/main/java/org/key_project/java/ast/Properties.java b/key.ncore.java/src/main/java/org/key_project/java/ast/Properties.java index baffde6241d..b72d394f04c 100644 --- a/key.ncore.java/src/main/java/org/key_project/java/ast/Properties.java +++ b/key.ncore.java/src/main/java/org/key_project/java/ast/Properties.java @@ -1,3 +1,6 @@ +/* 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 org.key_project.java.ast; /** @@ -7,7 +10,10 @@ */ public interface Properties { T get(Property property, T defaultValue); + T get(Property property); + boolean contains(Property property); + void set(Property property, T value); } diff --git a/key.ncore.java/src/main/java/org/key_project/java/ast/Property.java b/key.ncore.java/src/main/java/org/key_project/java/ast/Property.java index 2222d55acde..a74364cd518 100644 --- a/key.ncore.java/src/main/java/org/key_project/java/ast/Property.java +++ b/key.ncore.java/src/main/java/org/key_project/java/ast/Property.java @@ -1,3 +1,6 @@ +/* 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 org.key_project.java.ast; import com.github.javaparser.ast.Node; diff --git a/key.ncore.java/src/main/java/org/key_project/java/ast/UnaryOperatorKind.java b/key.ncore.java/src/main/java/org/key_project/java/ast/UnaryOperatorKind.java new file mode 100644 index 00000000000..981cc4334ca --- /dev/null +++ b/key.ncore.java/src/main/java/org/key_project/java/ast/UnaryOperatorKind.java @@ -0,0 +1,28 @@ +package org.key_project.java.ast; + +public enum UnaryOperatorKind { + LOGICAL_NOT("!", 1), + NEGATIVE("-", 1), + POSITIVE("+", 1), + BINARY_NOT("~", 1), + + PRE_INCREMENT("++", 0), + PRE_DECREMENT("--", 0), + POST_INCREMENT("++", 0, POSTFIX), + POST_DECREMENT("--", 0, POSTFIX); + + + public final String symbol; + public final int precedence; + public final int notation; + + UnaryOperatorKind(String symbol, int precedence) { + this(symbol, precedence, PREFIX); + } + + UnaryOperatorKind(String symbol, int precedence, int notation) { + this.symbol = symbol; + this.notation = notation; + this.precedence = precedence; + } + } From 405a476893d59a53a1677713a385c3fb82103dcb Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sun, 19 Apr 2026 15:56:10 +0200 Subject: [PATCH 3/7] wip --- key.ncore.java/build.gradle | 1 + key.ncore.java/src/adt/java-ast.java | 221 ++------ .../org/key_project/ncore/java/Generator.java | 514 ++---------------- .../org/key_project/ncore/java/NodeSteps.java | 420 ++++++++++++++ .../org/key_project/ncore/java/PreSteps.java | 71 +++ .../java/org/key_project/java/ast/EqEx.java | 1 + 6 files changed, 575 insertions(+), 653 deletions(-) create mode 100644 key.ncore.java/src/generator/java/org/key_project/ncore/java/NodeSteps.java diff --git a/key.ncore.java/build.gradle b/key.ncore.java/build.gradle index 497a6f2ea81..299489a7fc9 100644 --- a/key.ncore.java/build.gradle +++ b/key.ncore.java/build.gradle @@ -10,6 +10,7 @@ sourceSets { } dependencies { + implementation project(':key.core') generatorImplementation(project(":key.core")) diff --git a/key.ncore.java/src/adt/java-ast.java b/key.ncore.java/src/adt/java-ast.java index b5c06279b9c..4f1b51a4325 100644 --- a/key.ncore.java/src/adt/java-ast.java +++ b/key.ncore.java/src/adt/java-ast.java @@ -1,5 +1,7 @@ +// Imports are copied to every file import org.jspecify.annotations.Nullable; import de.uka.ilkd.key.speclang.jml.pretranslation.*; +import de.uka.ilkd.key.java.ast.PositionInfo; // ROOT abstract class JavaSourceElement { @@ -202,124 +204,11 @@ class VariableSpecification extends JavaNonTerminalProgramElement { IProgramVariable programVariable; } -class Abstract extends Modifier {} - class AnnotationUseSpecification extends Modifier { TypeReference tr; } -class Final extends Modifier {} - -class Ghost extends Modifier {} - -class Model extends Modifier {} - -class ABSTRACT extends Modifier {} - -class DEFAULT extends Modifier {} - -class FINAL extends Modifier {} - -class JML_CODE extends Modifier {} - -class JML_CODE_BIGINT_MATH extends Modifier {} - -class JML_CODE_JAVA_MATH extends Modifier {} - -class JML_CODE_SAFE_MATH extends Modifier {} - -class JML_HELPER extends Modifier {} - -class JML_INSTANCE extends Modifier {} - -class JML_NON_NULL extends Modifier {} - -class JML_NON_NULL_BY_DEFAULT extends Modifier {} - -class JML_NON_NULL_ELEMENTS extends Modifier {} - -class JML_NO_STATE extends Modifier {} - -class JML_NULLABLE extends Modifier {} - -class JML_NULLABLE_BY_DEFAULT extends Modifier {} - -class JML_OT_READ_ONLY extends Modifier {} - -class JML_OT_REP extends Modifier {} - -class JML_PACKAGE extends Modifier {} - -class JML_PURE extends Modifier {} - -class JML_SPEC_BIGINT_MATH extends Modifier {} - -class JML_SPEC_JAVA_MATH extends Modifier {} - -class JML_SPEC_PACKAGE extends Modifier {} - -class JML_SPEC_PRIVATE extends Modifier {} - -class JML_SPEC_PROTECTED extends Modifier {} - -class JML_SPEC_PUBLIC extends Modifier {} - -class JML_SPEC_SAFE_MATH extends Modifier {} - -class JML_STRICTLY_PURE extends Modifier {} - -class JML_TWO_STATE extends Modifier {} - -class JML_UNPARSABLE_MODIFIERS extends Modifier {} - -class NATIVE extends Modifier {} - -class NON_SEALED extends Modifier {} - -class PRIVATE extends Modifier {} - -class PROTECTED extends Modifier {} - -class PUBLIC extends Modifier {} - -class SEALED extends Modifier {} - -class STATIC extends Modifier {} - -class STRICTFP extends Modifier {} - -class SYNCHRONIZED extends Modifier {} - -class TRANSIENT extends Modifier {} - -class TRANSITIVE extends Modifier {} - -class VOLATILE extends Modifier {} - -class Native extends Modifier {} - -class NoState extends Modifier {} - -class Private extends VisibilityModifier {} - -class Protected extends VisibilityModifier {} - -class Public extends VisibilityModifier {} - -class Static extends Modifier {} - -class StrictFp extends Modifier {} - -class Synchronized extends Modifier {} - -class Transient extends Modifier {} - -class TwoState extends Modifier {} - -abstract class VisibilityModifier extends Modifier {} - -class Volatile extends Modifier {} class ArrayInitializer extends JavaNonTerminalProgramElement { KeYJavaType kjt; @@ -334,7 +223,9 @@ class ParenthesizedExpression extends Operator { Expression child; } -class PassiveExpression extends ParenthesizedExpression {} +class PassiveExpression extends Operator{ + Expression child; +} abstract class Literal extends JavaProgramElement { String value; @@ -535,36 +426,39 @@ class VariableReference extends JavaNonTerminalProgramElement { ProgramVariable variable; } -class Assert extends JavaStatement {} +class Assert extends JavaStatement { + Expression expression; + @Nullable String message; +} abstract class Branch {} -abstract class BranchImp extends JavaNonTerminalProgramElement {} - abstract class BranchStatement extends JavaStatement {} class Break extends LabelJumpStatement {} -class Case extends BranchImp { +class Case extends Branch { Expression expression; List body; } -class Catch extends BranchImp { +class Default extends Branch { + List body; +} + + +abstract class CatchClause + +class SingleCatch { ParameterDeclaration parameter; StatementBlock body; } -class CatchAllStatement extends JavaNonTerminalProgramElement {} - -class Ccatch extends BranchImp {} +class CatchAllStatement extends CatchClause {} +class Ccatch extends CatchClause {} class Continue extends LabelJumpStatement {} -class Default extends BranchImp { - List body; -} - class Do extends LoopStatement {} class Else extends BranchImp { @@ -655,10 +549,8 @@ class Return extends ExpressionJumpStatement {} class SetStatement extends JavaStatement {} class Switch extends BranchStatement { - - List branches; - Expression expression; + List branches; } class SynchronizedBlock extends JavaStatement { @@ -674,7 +566,11 @@ class Throw extends ExpressionJumpStatement {} class TransactionStatement extends JavaStatement {} -class Try extends BranchStatement {} +class Try extends BranchStatement { + StatementBlock tryBlock; + List catches; + @Nullable StatementBlock finallyBlock; +} class While extends LoopStatement {} @@ -691,13 +587,10 @@ class PermIndProgramElementName extends IndProgramElementName {} class TempIndProgramElementName extends IndProgramElementName {} abstract class IProgramMethod {} - abstract class IProgramVariable {} class LocationVariable extends ProgramVariable {} - class ProgramConstant extends ProgramVariable {} - class ProgramMethod extends ObserverFunction {} class ProgramSV extends JOperatorSV {} @@ -706,56 +599,34 @@ abstract class ProgramVariable extends JAbstractSortedOperator {} abstract class AbstractProgramElement {} -class ArrayLength extends ProgramTransformer {} +class InitArrayCreation extends InitArray {} +abstract class ProgramTransformer extends JavaNonTerminalProgramElement {} +class ReattachLoopInvariant extends ProgramTransformer {} +class SpecialConstructorCall extends ProgramTransformer {} +class StaticInitialisation extends ProgramTransformer {} +class SwitchToIf extends ProgramTransformer {} +class TypeOf extends ProgramTransformer {} +class Unpack extends ProgramTransformer {} +class UnwindLoop extends ProgramTransformer {} +class MultipleVarDecl extends ProgramTransformer {} +class PostWork extends ProgramTransformer {} +class IsStatic extends ProgramTransformer {} +class MethodCall extends ProgramTransformer { + MethodReference methRef; + ReferencePrefix newContext; + ProgramVariable pvar; + List arguments; + KeYJavaType staticPrefixType; +} +class ArrayLength extends ProgramTransformer {} class ArrayPostDecl extends ProgramTransformer {} - class ConstructorCall extends ProgramTransformer {} - class CreateObject extends ProgramTransformer {} - class DoBreak extends ProgramTransformer {} - class EnhancedForElimination extends ProgramTransformer {} - class EvaluateArgs extends ProgramTransformer {} - class ExpandMethodBody extends ProgramTransformer {} - class ForInitUnfoldTransformer extends ProgramTransformer {} - class ForToWhile extends ProgramTransformer {} - abstract class InitArray extends ProgramTransformer {} - -class InitArrayCreation extends InitArray {} - -class IsStatic extends ProgramTransformer {} - -class MethodCall extends ProgramTransformer { - MethodReference methRef; - ReferencePrefix newContext; - ProgramVariable pvar; - List arguments; - KeYJavaType staticPrefixType; -} - -class MultipleVarDecl extends ProgramTransformer {} - -class PostWork extends ProgramTransformer {} - -abstract class ProgramTransformer extends JavaNonTerminalProgramElement {} - -class ReattachLoopInvariant extends ProgramTransformer {} - -class SpecialConstructorCall extends ProgramTransformer {} - -class StaticInitialisation extends ProgramTransformer {} - -class SwitchToIf extends ProgramTransformer {} - -class TypeOf extends ProgramTransformer {} - -class Unpack extends ProgramTransformer {} - -class UnwindLoop extends ProgramTransformer {} diff --git a/key.ncore.java/src/generator/java/org/key_project/ncore/java/Generator.java b/key.ncore.java/src/generator/java/org/key_project/ncore/java/Generator.java index 44c52440ecc..22c0bab5a3d 100644 --- a/key.ncore.java/src/generator/java/org/key_project/ncore/java/Generator.java +++ b/key.ncore.java/src/generator/java/org/key_project/ncore/java/Generator.java @@ -3,51 +3,33 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.ncore.java; +import com.github.javaparser.ParserConfiguration; +import com.github.javaparser.StaticJavaParser; +import com.github.javaparser.ast.CompilationUnit; +import com.github.javaparser.ast.body.ClassOrInterfaceDeclaration; +import com.github.javaparser.utils.SourceRoot; +import org.key_project.ncore.java.NodeSteps.NodeStep; +import org.key_project.ncore.java.PostSteps.PostStep; +import org.key_project.ncore.java.PreSteps.PreStep; + import java.io.File; import java.nio.file.Files; import java.nio.file.Path; import java.nio.file.Paths; import java.util.ArrayList; import java.util.List; -import java.util.TreeMap; import java.util.concurrent.Callable; -import java.util.stream.Collectors; - -import org.key_project.ncore.java.PostSteps.PostStep; -import org.key_project.ncore.java.PreSteps.PreStep; - -import com.github.javaparser.ParserConfiguration; -import com.github.javaparser.StaticJavaParser; -import com.github.javaparser.ast.CompilationUnit; -import com.github.javaparser.ast.NodeList; -import com.github.javaparser.ast.body.*; -import com.github.javaparser.ast.expr.*; -import com.github.javaparser.ast.nodeTypes.NodeWithName; -import com.github.javaparser.ast.nodeTypes.NodeWithSimpleName; -import com.github.javaparser.ast.stmt.BlockStmt; -import com.github.javaparser.ast.stmt.ExpressionStmt; -import com.github.javaparser.ast.stmt.ReturnStmt; -import com.github.javaparser.ast.type.ClassOrInterfaceType; -import com.github.javaparser.ast.type.PrimitiveType; -import com.github.javaparser.ast.type.Type; -import com.github.javaparser.utils.SourceRoot; -import com.google.common.collect.Multimap; -import com.google.common.collect.MultimapBuilder; -import org.jspecify.annotations.NonNull; -import org.jspecify.annotations.NullMarked; -import org.jspecify.annotations.Nullable; - -import static com.github.javaparser.StaticJavaParser.*; -import static com.github.javaparser.ast.Modifier.DefaultKeyword.*; +import java.util.stream.Stream; /** * * @author Alexander Weigl * @version 1 (4/11/26) */ -@SuppressWarnings("OptionalGetWithoutIsPresent") public class Generator implements Callable { public static final Path ROOT = Paths.get("key.ncore.java/src/generated/java"); + public static final Generator INSTANCE = new Generator(); + CompilationUnit metaModel; List nodeSteps = new ArrayList<>(64); @@ -55,26 +37,25 @@ public class Generator implements Callable { List postSteps = new ArrayList<>(64); public static void main(String[] args) throws Exception { - new Generator().call(); + INSTANCE.call(); } public Generator() { - preSteps.add(pushFieldsDown); - addStep(Generator::setPackage); - addStep(Generator::processFields); - addStep(Generator::addAllFieldsConstructor); - addStep(Generator::addCopyConstructor); - addStep(Generator::addEquals); - addStep(Generator::ToString); - addStep(Generator::addHashCode); - - addStep(Generator::addWiths); - - addStep(Generator::addBuilder); - addStep(Generator::addOverrideConstructor); - addStep(Generator::addOverrideConstructor2); - addStep(Generator::addGetProperties); - addStep(Generator::processFieldsAccessor); + preSteps.add(new PreSteps.PreComputation()); + + addStep(NodeSteps::setPackage); + addStep(NodeSteps::processFields); + addStep(NodeSteps::addAllFieldsConstructor); + addStep(NodeSteps::addCopyConstructor); + addStep(NodeSteps::addEquals); + addStep(NodeSteps::ToString); + addStep(NodeSteps::addHashCode); + addStep(NodeSteps::addWiths); + addStep(NodeSteps::addBuilder); + addStep(NodeSteps::addOverrideConstructor); + addStep(NodeSteps::addOverrideConstructor2); + addStep(NodeSteps::addGetProperties); + addStep(NodeSteps::processFieldsAccessor); postSteps.add(PostSteps::createVisitor); postSteps.add(PostSteps::createVoidVisitor); @@ -82,350 +63,18 @@ public Generator() { postSteps.add(PostSteps::createDeepCopyVisitor); } - private static void addBuilder(ClassOrInterfaceDeclaration target) { - if (target.isInterface()) - return; - - var builder = new ClassOrInterfaceDeclaration(); - builder.setName("Builder"); - builder.addModifier(PUBLIC, FINAL, STATIC); - - for (var field : target.getFields()) { - for (var variable : field.variables()) { - var f = builder.addField(variable.getType().clone(), - variable.getNameAsString(), PUBLIC); - f.addAnnotation(Nullable.class); - } - } - - var build = builder.addMethod("build", PUBLIC); - build.setType(new ClassOrInterfaceType(null, target.getNameAsString())); - - var args = builder.getFields().stream().flatMap(it -> it.variables().stream()) - .map(it -> (Expression) it.getNameAsExpression()) - .toList(); - build.getBody().get().addStatement(new ReturnStmt( - new ObjectCreationExpr(null, - new ClassOrInterfaceType(null, target.getNameAsString()), - new NodeList<>(args)))); - - builder.getFields().stream().flatMap(it -> it.variables().stream()).forEach(it -> { - var m = builder.addMethod(it.getNameAsString(), PUBLIC); - m.addParameter(new Parameter(it.getType().clone(), it.getNameAsString())); - m.setType(new ClassOrInterfaceType(null, "Builder")); - m.getBody().get().addStatement( - "this.%s=%s;".formatted(it.getNameAsString(), it.getNameAsString())); - m.getBody().get().addStatement("return this;"); - }); - - - builder.getFields().stream().flatMap(it -> it.variables().stream()) - .filter(Generator::isList) - .forEach(it -> { - var m = builder.addMethod(it.getNameAsString(), PUBLIC); - var t = - it.getType().asClassOrInterfaceType().getTypeArguments().get().getFirst(); - m.addParameter(new Parameter(t.clone(), it.getNameAsString())); - m.setType(new ClassOrInterfaceType(null, "Builder")); - m.getBody().get().addStatement("if(this.%s==null) this.%s = new ArrayList<>();" - .formatted(it.getNameAsString(), it.getNameAsString())); - m.getBody().get().addStatement( - "this.%s.add(%s);".formatted(it.getNameAsString(), it.getNameAsString())); - m.getBody().get().addStatement("return this;"); - }); - - target.addMember(builder); - - var tb = target.addMethod("builder", PUBLIC); - tb.setType(new ClassOrInterfaceType(null, "Builder")); - final var b = tb.getBody().get(); - b.addStatement("Builder b = new Builder();"); - builder.getFields().stream().flatMap(it -> it.variables().stream()).forEach(it -> b - .addStatement("b.%s = %s;".formatted(it.getNameAsString(), it.getNameAsString()))); - b.addStatement("return b;"); - } - - private static boolean isList(VariableDeclarator type) { - return type.getTypeAsString().startsWith("List<"); - } - - private static void addWiths(ClassOrInterfaceDeclaration target) { - target.getFields().stream() - .flatMap(it -> it.getVariables().stream()).forEach(it -> { - var args = - target.getFields().stream() - .flatMap(f -> f.getVariables().stream()) - .map(v -> { - if (v == it) { - return (Expression) v.getNameAsExpression(); - } else { - return new MethodCallExpr(null, v.getNameAsString()); - } - }).toList(); - - var m = target.addMethod("with" + it.getNameAsString(), PUBLIC); - m.addParameter(new Parameter(it.getType().clone(), it.getNameAsString())); - m.setType(new ClassOrInterfaceType(null, target.getNameAsString())); - m.getBody().get().addStatement(new ReturnStmt( - new ObjectCreationExpr(null, - new ClassOrInterfaceType(null, target.getNameAsString()), - new NodeList<>(args)))); - }); - } - - private static void addEquals(ClassOrInterfaceDeclaration target) { - if (target.isAbstract()) { - return; - } - MethodDeclaration equals = target.addMethod("equals", PUBLIC); - equals.addModifier(FINAL); - equals.addAnnotation(Override.class); - equals.setType(Boolean.TYPE); - final var o = getNullableObject(); - equals.getParameters().add(o); - BlockStmt body = equals.getBody().get(); - body.addStatement(parseStatement("if(this == o) return true;")); - body.addStatement(parseStatement( - "if(!(o instanceof %s that)) return false;".formatted(target.getNameAsString()))); - Expression equalFields = target.getFields().stream() - .flatMap(it -> it.getVariables().stream()) - .map(it -> callObjects("equals", it.getNameAsExpression(), - new FieldAccessExpr(new NameExpr("that"), it.getNameAsString()))) - .reduce((a, b) -> new BinaryExpr(a, b, BinaryExpr.Operator.AND)) - .orElse(new BooleanLiteralExpr(true)); - body.addStatement(new ReturnStmt(equalFields)); - } - - private static void addHashCode(ClassOrInterfaceDeclaration target) { - if (target.isAbstract()) { - return; - } - - MethodDeclaration hashCode = target.addMethod("hashCode", PUBLIC); - hashCode.addModifier(FINAL); - hashCode.addAnnotation(Override.class); - hashCode.setType(Integer.TYPE); - Expression[] args = target.getFields() - .stream() - .flatMap(it -> it.getVariables().stream()) - .map(NodeWithSimpleName::getNameAsExpression) - .map(it -> (Expression) it) - .toArray(Expression[]::new); - - if (args.length == 0) - assert false : "No defined fields"; - else - hashCode.getBody().get().addStatement(new ReturnStmt( - callObjects("hash", args))); - } - - private static void ToString(ClassOrInterfaceDeclaration clazz) { - if (clazz.isAbstract()) { - return; - } - - MethodDeclaration toString = clazz.addMethod("toString", PUBLIC, FINAL); - toString.addAnnotation(Override.class); - toString.setType(String.class); - var parameters = - clazz.getFields().stream().flatMap(it -> it.getVariables().stream()).toList(); - var sb = (clazz.getNameAsString() + "[") - + parameters.stream().map(NodeWithSimpleName::getNameAsString).map(it -> it + "=%s") - .collect(Collectors.joining(", ")) - + "]"; - - var args = parameters.stream().map(NodeWithSimpleName::getNameAsExpression) - .map(it -> (Expression) it).toList(); - toString.getBody().get().addStatement(new ReturnStmt( - new MethodCallExpr(new StringLiteralExpr(sb), "formatted", new NodeList<>(args)))); - } - - private static Expression callObjects(String method, Expression... args) { - return new MethodCallExpr(new NameExpr("Objects"), method, new NodeList<>(args)); - } - - private static @NonNull Parameter getNullableObject() { - Type tObject = StaticJavaParser.parseType("java.lang.Object"); - return new Parameter(new NodeList<>(), tObject, new SimpleName("o")); - } - - private static void addAllFieldsConstructor(ClassOrInterfaceDeclaration target) { - if (target.isInterface()) { - return; - } - ConstructorDeclaration constr = new ConstructorDeclaration(); - var body = constr.getBody().get(); - var params = constr.getParameters(); - constr.setName(target.getNameAsString()); - constr.setModifiers(PUBLIC); - - for (var field : target.getFields()) { - for (var variable : field.getVariables()) { - params.add(new Parameter(variable.getType().clone(), variable.getNameAsString())); - body.addStatement( - new ExpressionStmt(new AssignExpr( - new FieldAccessExpr(new ThisExpr(), variable.getNameAsString()), - variable.getNameAsExpression(), AssignExpr.Operator.ASSIGN))); - } - } - - - target.addMember(constr); - } - - private static void addOverrideConstructor(ClassOrInterfaceDeclaration target) { - if (target.isInterface()) { - return; - } - - ConstructorDeclaration constr = target.addConstructor(PUBLIC); - var body = constr.getBody().get(); - var params = constr.getParameters(); - constr.setName(target.getNameAsString()); - params.add( - new Parameter(new ClassOrInterfaceType(null, target.getNameAsString()), "other")); - - params.add(new Parameter(parseType("Properties"), "map")); - - var args = target.getFields().stream().flatMap(it -> it.getVariables().stream()) - .map(NodeWithSimpleName::getNameAsString) - .map(it -> (Expression) parseExpression( - "map.get(PROPERTY_%s, other.%s)".formatted(it.toUpperCase(), it))) - .toList(); - body.addStatement(new MethodCallExpr(null, "this", new NodeList<>(args))); - } - - private static void addOverrideConstructor2(ClassOrInterfaceDeclaration target) { - if (target.isInterface()) { - return; - } - - ConstructorDeclaration constr = target.addConstructor(PUBLIC); - var body = constr.getBody().get(); - var params = constr.getParameters(); - constr.setName(target.getNameAsString()); - params.add(new Parameter(parseType("Properties"), "map")); - - var args = target.getFields().stream().flatMap(it -> it.getVariables().stream()) - .map(NodeWithSimpleName::getNameAsString) - .map(it -> (Expression) parseExpression( - "map.get(PROPERTY_%s)".formatted(it.toUpperCase()))) - .toList(); - body.addStatement(new MethodCallExpr(null, "this", new NodeList<>(args))); - } - - - private static void addGetProperties(ClassOrInterfaceDeclaration target) { - if (target.isInterface()) { - return; - } - - var method = target.addMethod("properties", PUBLIC); - method.setType("Properties"); - var body = method.getBody().get(); - - - body.addStatement("Properties p = new DefaultProperties();"); - target.getFields().stream() - .flatMap(it -> it.getVariables().stream()) - .forEach(variable -> body.addStatement("p.set(PROPERTY_%s, %s());".formatted( - variable.getNameAsString().toUpperCase(), variable.getNameAsString()))); - body.addStatement("return p;"); - } - - - private static void addCopyConstructor(ClassOrInterfaceDeclaration target) { - if (target.isInterface()) { - return; - } - - ConstructorDeclaration constr = target.addConstructor(PUBLIC); - var body = constr.getBody().get(); - var params = constr.getParameters(); - constr.setName(target.getNameAsString()); - params.add( - new Parameter(new ClassOrInterfaceType(null, target.getNameAsString()), "other")); - - /* - * for (var field : target.getFields()) { - * for (var variable : field.getVariables()) { - * //params.add(new Parameter(variable.getType().clone(), variable.getNameAsString())); - * body.addStatement( - * new ExpressionStmt(new AssignExpr( - * new FieldAccessExpr(new ThisExpr(), variable.getNameAsString()), - * new FieldAccessExpr(new NameExpr("other"), variable.getNameAsString()), - * AssignExpr.Operator.ASSIGN - * )) - * ); - * } - * } - */ - - var args = target.getFields().stream().flatMap(it -> it.getVariables().stream()) - .map(NodeWithSimpleName::getNameAsString) - .map(it -> (Expression) new FieldAccessExpr(new NameExpr("other"), it)) - .toList(); - body.addStatement(new MethodCallExpr(null, "this", new NodeList<>(args))); - - } - - static Multimap inheritanceMap = - MultimapBuilder.treeKeys().treeSetValues().build(); - static Multimap permittedTypes = - MultimapBuilder.treeKeys().treeSetValues().build(); - - private static final PreStep pushFieldsDown = types -> { - TreeMap fields = new TreeMap<>(); - - for (TypeDeclaration decl : types) { - fields.put(decl.getNameAsString(), (ClassOrInterfaceDeclaration) decl); - - var zuper = ((ClassOrInterfaceDeclaration) decl).getExtendedTypes().getOFirst() - .map(NodeWithSimpleName::getNameAsString); - zuper.ifPresent(s -> inheritanceMap.put(decl.getNameAsString(), s)); - } - - // compute transitive closure - boolean changed = true; - while (changed) { - changed = false; - for (var clazz : inheritanceMap.keySet()) { - final var strings = new ArrayList<>(inheritanceMap.get(clazz)); - for (var zuper : strings) { - changed = changed || inheritanceMap.putAll(clazz, inheritanceMap.get(zuper)); - } - } - } - - for (var decl : fields.sequencedValues()) { - if (decl.hasModifier(ABSTRACT)) { - continue; - } - - var newFields = new TreeMap(); - for (var c : inheritanceMap.get(decl.getNameAsString())) { - final var classOrInterfaceDeclaration = fields.get(c); - if (classOrInterfaceDeclaration != null) { - for (FieldDeclaration it : classOrInterfaceDeclaration.getFields()) { - var name = it.getVariable(0).getNameAsString(); - newFields.computeIfAbsent(name, (k) -> { - final var clone = it.clone(); - clone.addAnnotation(Override.class.getName()); - clone.setRange(null); - return clone; - }); - } - } - } - assert newFields.size() <= 10; - decl.getMembers().addAll(newFields.values()); - } - }; - private void addStep(NodeStep nodeStep) { nodeSteps.add(nodeStep); } + @SuppressWarnings("unchecked") + T getStep(Class step) { + return (T) Stream.concat(preSteps.stream(), postSteps.stream()) + .filter(step::isInstance) + .findFirst() + .orElse(null); + } + @Override public Integer call() throws Exception { var config = new ParserConfiguration(); @@ -468,96 +117,5 @@ public Integer call() throws Exception { return 0; } - interface NodeStep { - void applyOn(ClassOrInterfaceDeclaration target); - } - - static void setPackage(ClassOrInterfaceDeclaration target) { - var annotation = target.getAnnotationByName("Package") - .map(NodeWithName::getNameAsString) - .orElse("org.key_project.java.ast"); - - CompilationUnit cu = target.findCompilationUnit().get(); - cu.setPackageDeclaration(annotation); - - cu.setStorage(ROOT.resolve(annotation.replace(".", "/")) - .resolve(target.getNameAsString() + ".java")); - - target.addAnnotation(NullMarked.class); - target.addModifier(PUBLIC); - - boolean isAbstract = target.isAbstract(); - if (isAbstract) { - target.setInterface(true); - for (var s : permittedTypes.get(target.getNameAsString())) { - target.getPermittedTypes().add(new ClassOrInterfaceType(null, s)); - } - } else { - target.addModifier(FINAL); - } - } - - - private static void processFieldsAccessor(ClassOrInterfaceDeclaration target) { - if (target.isInterface()) - return; - - target.findCompilationUnit().get().addImport("org.key_project.java.ast.Property"); - - for (var field : target.getFields()) { - for (var variable : field.getVariables()) { - final var dataKey = new ClassOrInterfaceType(null, new SimpleName("Property"), - new NodeList<>(toBoxType(variable.getType().clone()))); - var f = target.addField( - dataKey, "PROPERTY_" + variable.getNameAsString().toUpperCase(), PUBLIC, STATIC, - FINAL); - f.getVariables().getFirst().setInitializer( - "new Property<>(\"%s\")".formatted(variable.getNameAsString())); - } - } - } - - private static Type toBoxType(Type clone) { - if (clone instanceof PrimitiveType pt) { - return pt.toBoxedType(); - } - return clone; - } - - static void processFields(ClassOrInterfaceDeclaration target) { - boolean isAbstract = target.isAbstract(); - - for (var field : target.getFields()) { - if (isAbstract) { - field.remove(); - } else { - field.setModifiers(PRIVATE, FINAL); - } - - for (var variable : field.getVariables()) { - var getter = target.addMethod(variable.getNameAsString()); - getter.setType(variable.getType().clone()); - - var nullable = field.getAnnotationByName("Nullable"); - if (nullable.isPresent()) { - getter.addAndGetAnnotation(Nullable.class); - } - - if (isAbstract) { - // getter.addModifier(Modifier.DefaultKeyword.ABSTRACT); - getter.setBody(null); - } else { - getter.getBody().get() - .addStatement(new ReturnStmt(variable.getNameAsExpression())); - getter.addModifier(PUBLIC, FINAL); - } - field.getAnnotationByName("Override") - .ifPresent(it -> { - it.remove(); - getter.addAnnotation(it); - }); - } - } - } } diff --git a/key.ncore.java/src/generator/java/org/key_project/ncore/java/NodeSteps.java b/key.ncore.java/src/generator/java/org/key_project/ncore/java/NodeSteps.java new file mode 100644 index 00000000000..91add20d721 --- /dev/null +++ b/key.ncore.java/src/generator/java/org/key_project/ncore/java/NodeSteps.java @@ -0,0 +1,420 @@ +package org.key_project.ncore.java; + +import com.github.javaparser.StaticJavaParser; +import com.github.javaparser.ast.CompilationUnit; +import com.github.javaparser.ast.NodeList; +import com.github.javaparser.ast.body.*; +import com.github.javaparser.ast.expr.*; +import com.github.javaparser.ast.nodeTypes.NodeWithName; +import com.github.javaparser.ast.nodeTypes.NodeWithSimpleName; +import com.github.javaparser.ast.stmt.BlockStmt; +import com.github.javaparser.ast.stmt.ExpressionStmt; +import com.github.javaparser.ast.stmt.ReturnStmt; +import com.github.javaparser.ast.type.ClassOrInterfaceType; +import com.github.javaparser.ast.type.PrimitiveType; +import com.github.javaparser.ast.type.Type; +import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.NullMarked; +import org.jspecify.annotations.Nullable; + +import java.util.stream.Collectors; + +import static com.github.javaparser.StaticJavaParser.*; +import static com.github.javaparser.ast.Modifier.DefaultKeyword.*; + +/** + * + * @author Alexander Weigl + * @version 1 (4/19/26) + */ +@SuppressWarnings("OptionalGetWithoutIsPresent") +public class NodeSteps { + static void addWiths(ClassOrInterfaceDeclaration target) { + target.getFields().stream() + .flatMap(it -> it.getVariables().stream()).forEach(it -> { + var args = + target.getFields().stream() + .flatMap(f -> f.getVariables().stream()) + .map(v -> { + if (v == it) { + return (Expression) v.getNameAsExpression(); + } else { + return new MethodCallExpr(null, v.getNameAsString()); + } + }).toList(); + + var m = target.addMethod("with" + upperStart(it.getNameAsString()), PUBLIC); + m.addParameter(new Parameter(it.getType().clone(), it.getNameAsString())); + m.setType(new ClassOrInterfaceType(null, target.getNameAsString())); + m.getBody().get().addStatement(new ReturnStmt( + new ObjectCreationExpr(null, + new ClassOrInterfaceType(null, target.getNameAsString()), + new NodeList<>(args)))); + }); + } + + private static String upperStart(String nameAsString) { + var c = nameAsString.substring(0,1).toUpperCase(); + return c + nameAsString.substring(1); + } + + static void addEquals(ClassOrInterfaceDeclaration target) { + if (target.isAbstract() || target.isInterface()) { + return; + } + MethodDeclaration equals = target.addMethod("equals", PUBLIC); + equals.addModifier(FINAL); + equals.addAnnotation(Override.class); + equals.setType(Boolean.TYPE); + final var o = getNullableObject(); + equals.getParameters().add(o); + BlockStmt body = equals.getBody().get(); + body.addStatement(parseStatement("if(this == o) return true;")); + body.addStatement(parseStatement( + "if(!(o instanceof %s that)) return false;".formatted(target.getNameAsString()))); + Expression equalFields = target.getFields().stream() + .filter(it -> it.getAnnotationByName("EqEx").isEmpty()) + .flatMap(it -> it.getVariables().stream()) + .map(it -> callObjects("equals", it.getNameAsExpression(), + new FieldAccessExpr(new NameExpr("that"), it.getNameAsString()))) + .reduce((a, b) -> new BinaryExpr(a, b, BinaryExpr.Operator.AND)) + .orElse(new BooleanLiteralExpr(true)); + body.addStatement(new ReturnStmt(equalFields)); + } + + static void addHashCode(ClassOrInterfaceDeclaration target) { + if (target.isAbstract() || target.isInterface()) { + return; + } + + MethodDeclaration hashCode = target.addMethod("hashCode", PUBLIC); + hashCode.addModifier(FINAL); + hashCode.addAnnotation(Override.class); + hashCode.setType(Integer.TYPE); + Expression[] args = target.getFields() + .stream() + .filter(it -> it.getAnnotationByName("EqEx").isEmpty()) + .flatMap(it -> it.getVariables().stream()) + .map(NodeWithSimpleName::getNameAsExpression) + .map(it -> (Expression) it) + .toArray(Expression[]::new); + + if (args.length == 0) + assert false : "No defined fields"; + else + hashCode.getBody().get().addStatement(new ReturnStmt( + callObjects("hash", args))); + } + + static void ToString(ClassOrInterfaceDeclaration clazz) { + if (clazz.isAbstract()||clazz.isInterface()) { + return; + } + + MethodDeclaration toString = clazz.addMethod("toString", PUBLIC, FINAL); + toString.addAnnotation(Override.class); + toString.setType(String.class); + var parameters = + clazz.getFields().stream().flatMap(it -> it.getVariables().stream()).toList(); + var sb = (clazz.getNameAsString() + "[") + + parameters.stream().map(NodeWithSimpleName::getNameAsString).map(it -> it + "=%s") + .collect(Collectors.joining(", ")) + + "]"; + + var args = parameters.stream().map(NodeWithSimpleName::getNameAsExpression) + .map(it -> (Expression) it).toList(); + toString.getBody().get().addStatement(new ReturnStmt( + new MethodCallExpr(new StringLiteralExpr(sb), "formatted", new NodeList<>(args)))); + } + + private static Expression callObjects(String method, Expression... args) { + return new MethodCallExpr(new NameExpr("Objects"), method, new NodeList<>(args)); + } + + private static @NonNull Parameter getNullableObject() { + Type tObject = StaticJavaParser.parseType("java.lang.Object"); + return new Parameter(new NodeList<>(), tObject, new SimpleName("o")); + } + + static void addAllFieldsConstructor(ClassOrInterfaceDeclaration target) { + if (target.isInterface()) { + return; + } + ConstructorDeclaration constr = new ConstructorDeclaration(); + var body = constr.getBody().get(); + var params = constr.getParameters(); + constr.setName(target.getNameAsString()); + constr.setModifiers(PUBLIC); + + for (var field : target.getFields()) { + for (var variable : field.getVariables()) { + params.add(new Parameter(variable.getType().clone(), variable.getNameAsString())); + body.addStatement( + new ExpressionStmt(new AssignExpr( + new FieldAccessExpr(new ThisExpr(), variable.getNameAsString()), + variable.getNameAsExpression(), AssignExpr.Operator.ASSIGN))); + } + } + + + target.addMember(constr); + } + + static void addOverrideConstructor(ClassOrInterfaceDeclaration target) { + if (target.isInterface()) { + return; + } + + ConstructorDeclaration constr = target.addConstructor(PUBLIC); + var body = constr.getBody().get(); + var params = constr.getParameters(); + constr.setName(target.getNameAsString()); + params.add( + new Parameter(new ClassOrInterfaceType(null, target.getNameAsString()), "other")); + + params.add(new Parameter(parseType("Properties"), "map")); + + var args = target.getFields().stream().flatMap(it -> it.getVariables().stream()) + .map(NodeWithSimpleName::getNameAsString) + .map(it -> (Expression) parseExpression( + "map.get(PROPERTY_%s, other.%s)".formatted(it.toUpperCase(), it))) + .toList(); + body.addStatement(new MethodCallExpr(null, "this", new NodeList<>(args))); + } + + static void addOverrideConstructor2(ClassOrInterfaceDeclaration target) { + if (target.isInterface()) { + return; + } + + ConstructorDeclaration constr = target.addConstructor(PUBLIC); + var body = constr.getBody().get(); + var params = constr.getParameters(); + constr.setName(target.getNameAsString()); + params.add(new Parameter(parseType("Properties"), "map")); + + var args = target.getFields().stream().flatMap(it -> it.getVariables().stream()) + .map(NodeWithSimpleName::getNameAsString) + .map(it -> (Expression) parseExpression( + "map.get(PROPERTY_%s)".formatted(it.toUpperCase()))) + .toList(); + body.addStatement(new MethodCallExpr(null, "this", new NodeList<>(args))); + } + + static void addGetProperties(ClassOrInterfaceDeclaration target) { + if (target.isInterface()) { + return; + } + + var method = target.addMethod("properties", PUBLIC); + method.setType("Properties"); + var body = method.getBody().get(); + + + body.addStatement("Properties p = new DefaultProperties();"); + target.getFields().stream() + .flatMap(it -> it.getVariables().stream()) + .forEach(variable -> body.addStatement("p.set(PROPERTY_%s, %s());".formatted( + variable.getNameAsString().toUpperCase(), variable.getNameAsString()))); + body.addStatement("return p;"); + } + + static void addCopyConstructor(ClassOrInterfaceDeclaration target) { + if (target.isInterface()) { + return; + } + + ConstructorDeclaration constr = target.addConstructor(PUBLIC); + var body = constr.getBody().get(); + var params = constr.getParameters(); + constr.setName(target.getNameAsString()); + params.add( + new Parameter(new ClassOrInterfaceType(null, target.getNameAsString()), "other")); + + /* + * for (var field : target.getFields()) { + * for (var variable : field.getVariables()) { + * //params.add(new Parameter(variable.getType().clone(), variable.getNameAsString())); + * body.addStatement( + * new ExpressionStmt(new AssignExpr( + * new FieldAccessExpr(new ThisExpr(), variable.getNameAsString()), + * new FieldAccessExpr(new NameExpr("other"), variable.getNameAsString()), + * AssignExpr.Operator.ASSIGN + * )) + * ); + * } + * } + */ + + var args = target.getFields().stream().flatMap(it -> it.getVariables().stream()) + .map(NodeWithSimpleName::getNameAsString) + .map(it -> (Expression) new FieldAccessExpr(new NameExpr("other"), it)) + .toList(); + body.addStatement(new MethodCallExpr(null, "this", new NodeList<>(args))); + + } + + static void setPackage(ClassOrInterfaceDeclaration target) { + var annotation = target.getAnnotationByName("Package") + .map(NodeWithName::getNameAsString) + .orElse("org.key_project.java.ast"); + + CompilationUnit cu = target.findCompilationUnit().get(); + cu.setPackageDeclaration(annotation); + + cu.setStorage(Generator.ROOT.resolve(annotation.replace(".", "/")) + .resolve(target.getNameAsString() + ".java")); + + target.addAnnotation(NullMarked.class); + target.addModifier(PUBLIC); + + boolean isAbstract = target.isAbstract() || target.isInterface(); + if (isAbstract) { + target.setInterface(true); + target.addModifier(SEALED); + target.removeModifier(ABSTRACT); + var permittedTypes + = Generator.INSTANCE.getStep(PreSteps.PreComputation.class).permittedTypes; + for (var s : permittedTypes.get(target.getNameAsString())) { + target.getPermittedTypes().add(new ClassOrInterfaceType(null, s)); + } + } else { + target.addModifier(FINAL); + target.setImplementedTypes(target.getExtendedTypes()); + target.setExtendedTypes(new NodeList<>()); + } + } + + static void processFieldsAccessor(ClassOrInterfaceDeclaration target) { + if (target.isInterface()) + return; + + target.findCompilationUnit().get().addImport("org.key_project.java.ast.Property"); + + for (var field : target.getFields()) { + for (var variable : field.getVariables()) { + final var dataKey = new ClassOrInterfaceType(null, new SimpleName("Property"), + new NodeList<>(toBoxType(variable.getType().clone()))); + var f = target.addField( + dataKey, "PROPERTY_" + variable.getNameAsString().toUpperCase(), PUBLIC, STATIC, + FINAL); + f.getVariables().getFirst().setInitializer( + "new Property<>(\"%s\")".formatted(variable.getNameAsString())); + } + } + } + + private static Type toBoxType(Type clone) { + if (clone instanceof PrimitiveType pt) { + return pt.toBoxedType(); + } + return clone; + } + + static void processFields(ClassOrInterfaceDeclaration target) { + boolean isAbstract = target.isAbstract() || target.isInterface(); + + for (var field : target.getFields()) { + if (isAbstract) { + field.remove(); + } else { + field.setModifiers(PRIVATE, FINAL); + } + + for (var variable : field.getVariables()) { + var getter = target.addMethod(variable.getNameAsString()); + getter.setType(variable.getType().clone()); + + var nullable = field.getAnnotationByName("Nullable"); + if (nullable.isPresent()) { + getter.addAndGetAnnotation(Nullable.class); + } + + if (isAbstract) { + // getter.addModifier(Modifier.DefaultKeyword.ABSTRACT); + getter.setBody(null); + } else { + getter.getBody().get() + .addStatement(new ReturnStmt(variable.getNameAsExpression())); + getter.addModifier(PUBLIC, FINAL); + } + field.getAnnotationByName("Override") + .ifPresent(it -> { + it.remove(); + getter.addAnnotation(it); + }); + } + } + } + + static void addBuilder(ClassOrInterfaceDeclaration target) { + if (target.isInterface()) + return; + + var builder = new ClassOrInterfaceDeclaration(); + builder.setName("Builder"); + builder.addModifier(PUBLIC, FINAL, STATIC); + + for (var field : target.getFields()) { + for (var variable : field.variables()) { + var f = builder.addField(variable.getType().clone(), + variable.getNameAsString(), PUBLIC); + f.addAnnotation(Nullable.class); + } + } + + var build = builder.addMethod("build", PUBLIC); + build.setType(new ClassOrInterfaceType(null, target.getNameAsString())); + + var args = builder.getFields().stream().flatMap(it -> it.variables().stream()) + .map(it -> (Expression) it.getNameAsExpression()) + .toList(); + build.getBody().get().addStatement(new ReturnStmt( + new ObjectCreationExpr(null, + new ClassOrInterfaceType(null, target.getNameAsString()), + new NodeList<>(args)))); + + builder.getFields().stream().flatMap(it -> it.variables().stream()).forEach(it -> { + var m = builder.addMethod(it.getNameAsString(), PUBLIC); + m.addParameter(new Parameter(it.getType().clone(), it.getNameAsString())); + m.setType(new ClassOrInterfaceType(null, "Builder")); + m.getBody().get().addStatement( + "this.%s=%s;".formatted(it.getNameAsString(), it.getNameAsString())); + m.getBody().get().addStatement("return this;"); + }); + + + builder.getFields().stream().flatMap(it -> it.variables().stream()) + .filter(NodeSteps::isList) + .forEach(it -> { + var m = builder.addMethod(it.getNameAsString(), PUBLIC); + var t = + it.getType().asClassOrInterfaceType().getTypeArguments().get().getFirst(); + m.addParameter(new Parameter(t.clone(), it.getNameAsString())); + m.setType(new ClassOrInterfaceType(null, "Builder")); + m.getBody().get().addStatement("if(this.%s==null) this.%s = new ArrayList<>();" + .formatted(it.getNameAsString(), it.getNameAsString())); + m.getBody().get().addStatement( + "this.%s.add(%s);".formatted(it.getNameAsString(), it.getNameAsString())); + m.getBody().get().addStatement("return this;"); + }); + + target.addMember(builder); + + var tb = target.addMethod("builder", PUBLIC); + tb.setType(new ClassOrInterfaceType(null, "Builder")); + final var b = tb.getBody().get(); + b.addStatement("Builder b = new Builder();"); + builder.getFields().stream().flatMap(it -> it.variables().stream()).forEach(it -> b + .addStatement("b.%s = %s;".formatted(it.getNameAsString(), it.getNameAsString()))); + b.addStatement("return b;"); + } + + private static boolean isList(VariableDeclarator type) { + return type.getTypeAsString().startsWith("List<"); + } + + interface NodeStep { + void applyOn(ClassOrInterfaceDeclaration target); + } +} diff --git a/key.ncore.java/src/generator/java/org/key_project/ncore/java/PreSteps.java b/key.ncore.java/src/generator/java/org/key_project/ncore/java/PreSteps.java index f015e41a485..9099d1f3042 100644 --- a/key.ncore.java/src/generator/java/org/key_project/ncore/java/PreSteps.java +++ b/key.ncore.java/src/generator/java/org/key_project/ncore/java/PreSteps.java @@ -1,9 +1,80 @@ package org.key_project.ncore.java; import com.github.javaparser.ast.NodeList; +import com.github.javaparser.ast.body.ClassOrInterfaceDeclaration; +import com.github.javaparser.ast.body.FieldDeclaration; import com.github.javaparser.ast.body.TypeDeclaration; +import com.github.javaparser.ast.nodeTypes.NodeWithSimpleName; +import com.google.common.collect.Multimap; +import com.google.common.collect.MultimapBuilder; + +import java.util.ArrayList; +import java.util.TreeMap; + +import static com.github.javaparser.ast.Modifier.DefaultKeyword.ABSTRACT; public class PreSteps { + final static class PreComputation implements PreStep { + Multimap inheritanceMap = MultimapBuilder.treeKeys().treeSetValues().build(); + Multimap permittedTypes = MultimapBuilder.treeKeys().treeSetValues().build(); + + @Override + public void applyOn(NodeList> types) { + TreeMap fields = new TreeMap<>(); + + for (TypeDeclaration decl : types) { + fields.put(decl.getNameAsString(), (ClassOrInterfaceDeclaration) decl); + + var zuper = ((ClassOrInterfaceDeclaration) decl).getExtendedTypes().getOFirst() + .map(NodeWithSimpleName::getNameAsString); + zuper.ifPresent(s -> inheritanceMap.put(decl.getNameAsString(), s)); + } + + // compute transitive closure + boolean changed = true; + while (changed) { + changed = false; + for (var clazz : inheritanceMap.keySet()) { + final var strings = new ArrayList<>(inheritanceMap.get(clazz)); + for (var zuper : strings) { + changed = changed || inheritanceMap.putAll(clazz, inheritanceMap.get(zuper)); + } + } + } + + for (var decl : fields.sequencedValues()) { + if (decl.hasModifier(ABSTRACT)) { + continue; + } + + var newFields = new TreeMap(); + for (var c : inheritanceMap.get(decl.getNameAsString())) { + final var classOrInterfaceDeclaration = fields.get(c); + if (classOrInterfaceDeclaration != null) { + for (FieldDeclaration it : classOrInterfaceDeclaration.getFields()) { + var name = it.getVariable(0).getNameAsString(); + newFields.computeIfAbsent(name, (k) -> { + final var clone = it.clone(); + clone.addAnnotation(Override.class.getName()); + clone.setRange(null); + return clone; + }); + } + } + } + decl.getMembers().addAll(newFields.values()); + } + + fillPermittedTypes(); + } + + private void fillPermittedTypes() { + for (var entry : inheritanceMap.entries()) { + permittedTypes.put(entry.getValue(), entry.getKey()); + } + } + } + interface PreStep { void applyOn(NodeList> types); } diff --git a/key.ncore.java/src/main/java/org/key_project/java/ast/EqEx.java b/key.ncore.java/src/main/java/org/key_project/java/ast/EqEx.java index f918f7c6897..f129629fb70 100644 --- a/key.ncore.java/src/main/java/org/key_project/java/ast/EqEx.java +++ b/key.ncore.java/src/main/java/org/key_project/java/ast/EqEx.java @@ -6,6 +6,7 @@ import java.lang.annotation.RetentionPolicy; import java.lang.annotation.Target; +/// Exclude a field from equality and hashCode. @Retention(RetentionPolicy.SOURCE) @Target(ElementType.FIELD) public @interface EqEx { From e5559a79466eeef62346528df3b125c0e7160727 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sun, 19 Apr 2026 16:59:21 +0200 Subject: [PATCH 4/7] wip --- key.ncore.java/src/adt/java-ast.java | 4 +- .../org/key_project/ncore/java/Generator.java | 3 + .../org/key_project/ncore/java/NodeSteps.java | 65 ++++++++++++++-- .../org/key_project/ncore/java/PostSteps.java | 74 ++++++++++++++++--- .../java/org/key_project/java/ast/EqEx.java | 2 +- .../org/key_project/java/ast/Package.java | 13 ++++ .../util/collection/ImmutableArray.java | 14 +++- .../key_project/util/collection/RoList.java | 33 +++++++++ 8 files changed, 188 insertions(+), 20 deletions(-) create mode 100644 key.ncore.java/src/main/java/org/key_project/java/ast/Package.java create mode 100644 key.util/src/main/java/org/key_project/util/collection/RoList.java diff --git a/key.ncore.java/src/adt/java-ast.java b/key.ncore.java/src/adt/java-ast.java index 4f1b51a4325..ace984c2615 100644 --- a/key.ncore.java/src/adt/java-ast.java +++ b/key.ncore.java/src/adt/java-ast.java @@ -5,7 +5,7 @@ // ROOT abstract class JavaSourceElement { - @EqEx PositionInfo positionInfo; + @EqEx @Nullable PositionInfo positionInfo; } class CompilationUnit extends JavaNonTerminalProgramElement { @@ -447,7 +447,7 @@ class Default extends Branch { } -abstract class CatchClause +abstract class CatchClause {} class SingleCatch { ParameterDeclaration parameter; diff --git a/key.ncore.java/src/generator/java/org/key_project/ncore/java/Generator.java b/key.ncore.java/src/generator/java/org/key_project/ncore/java/Generator.java index 22c0bab5a3d..aa799fd9f89 100644 --- a/key.ncore.java/src/generator/java/org/key_project/ncore/java/Generator.java +++ b/key.ncore.java/src/generator/java/org/key_project/ncore/java/Generator.java @@ -3,6 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.ncore.java; +import com.github.javaparser.ParseProblemException; import com.github.javaparser.ParserConfiguration; import com.github.javaparser.StaticJavaParser; import com.github.javaparser.ast.CompilationUnit; @@ -46,6 +47,7 @@ public Generator() { addStep(NodeSteps::setPackage); addStep(NodeSteps::processFields); addStep(NodeSteps::addAllFieldsConstructor); + addStep(NodeSteps::addAllWoOptFieldsConstructor); addStep(NodeSteps::addCopyConstructor); addStep(NodeSteps::addEquals); addStep(NodeSteps::ToString); @@ -58,6 +60,7 @@ public Generator() { addStep(NodeSteps::processFieldsAccessor); postSteps.add(PostSteps::createVisitor); + postSteps.add(PostSteps::createArgVisitor); postSteps.add(PostSteps::createVoidVisitor); postSteps.add(PostSteps::createTraversalVisitor); postSteps.add(PostSteps::createDeepCopyVisitor); diff --git a/key.ncore.java/src/generator/java/org/key_project/ncore/java/NodeSteps.java b/key.ncore.java/src/generator/java/org/key_project/ncore/java/NodeSteps.java index 91add20d721..a9fc3ac8a20 100644 --- a/key.ncore.java/src/generator/java/org/key_project/ncore/java/NodeSteps.java +++ b/key.ncore.java/src/generator/java/org/key_project/ncore/java/NodeSteps.java @@ -147,12 +147,21 @@ static void addAllFieldsConstructor(ClassOrInterfaceDeclaration target) { constr.setModifiers(PUBLIC); for (var field : target.getFields()) { + var isOptional = field.getAnnotations().stream().anyMatch(it -> it.getNameAsString().equals("Nullable")); for (var variable : field.getVariables()) { - params.add(new Parameter(variable.getType().clone(), variable.getNameAsString())); - body.addStatement( - new ExpressionStmt(new AssignExpr( - new FieldAccessExpr(new ThisExpr(), variable.getNameAsString()), - variable.getNameAsExpression(), AssignExpr.Operator.ASSIGN))); + final var p = new Parameter(variable.getType().clone(), variable.getNameAsString()); + field.getAnnotations().stream().map(AnnotationExpr::clone) + .forEach(p::addAnnotation); + params.add(p); + if(isOptional){ + body.addStatement( + "this.%s = %s;".formatted( + variable.getNameAsString(), variable.getNameAsString())); + }else { + body.addStatement( + "this.%s = Objects.requireNonNull(%s);".formatted( + variable.getNameAsString(), variable.getNameAsString())); + } } } @@ -160,6 +169,41 @@ static void addAllFieldsConstructor(ClassOrInterfaceDeclaration target) { target.addMember(constr); } + static void addAllWoOptFieldsConstructor(ClassOrInterfaceDeclaration target) { + if (target.isInterface()) { + return; + } + ConstructorDeclaration constr = new ConstructorDeclaration(); + var body = constr.getBody().get(); + var params = constr.getParameters(); + constr.setName(target.getNameAsString()); + constr.setModifiers(PUBLIC); + + for (var field : target.getFields()) { + var isOptional = field.getAnnotations().stream().anyMatch(it -> it.getNameAsString().equals("Nullable")); + + + for (var variable : field.getVariables()) { + if(isOptional){ + body.addStatement( + "this.%s = null;".formatted(variable.getNameAsString())); + }else { + final var p = new Parameter(variable.getType().clone(), variable.getNameAsString()); + field.getAnnotations().stream().map(AnnotationExpr::clone) + .forEach(p::addAnnotation); + params.add(p); + body.addStatement( + "this.%s = Objects.requireNonNull(%s);".formatted( + variable.getNameAsString(), variable.getNameAsString())); + } + } + } + + + target.addMember(constr); + } + + static void addOverrideConstructor(ClassOrInterfaceDeclaration target) { if (target.isInterface()) { return; @@ -322,6 +366,12 @@ static void processFields(ClassOrInterfaceDeclaration target) { } for (var variable : field.getVariables()) { + if(isList(variable)) { + var old = variable.getType().asClassOrInterfaceType(); + old.setName("RoList"); + } + + var getter = target.addMethod(variable.getNameAsString()); getter.setType(variable.getType().clone()); @@ -411,7 +461,10 @@ static void addBuilder(ClassOrInterfaceDeclaration target) { } private static boolean isList(VariableDeclarator type) { - return type.getTypeAsString().startsWith("List<"); + if(type.getType().isClassOrInterfaceType()) { + return type.getType().asClassOrInterfaceType().getNameAsString().equals("List"); + } + return false; } interface NodeStep { diff --git a/key.ncore.java/src/generator/java/org/key_project/ncore/java/PostSteps.java b/key.ncore.java/src/generator/java/org/key_project/ncore/java/PostSteps.java index 442c58d2810..72e134883d5 100644 --- a/key.ncore.java/src/generator/java/org/key_project/ncore/java/PostSteps.java +++ b/key.ncore.java/src/generator/java/org/key_project/ncore/java/PostSteps.java @@ -3,24 +3,21 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.ncore.java; -import java.nio.file.Paths; -import java.util.List; - import com.github.javaparser.StaticJavaParser; import com.github.javaparser.ast.CompilationUnit; import com.github.javaparser.ast.Modifier; import com.github.javaparser.ast.NodeList; import com.github.javaparser.ast.body.ClassOrInterfaceDeclaration; -import com.github.javaparser.ast.expr.AssignExpr; import com.github.javaparser.ast.expr.SimpleName; import com.github.javaparser.ast.nodeTypes.modifiers.NodeWithPrivateModifier; import com.github.javaparser.ast.stmt.BlockStmt; import com.github.javaparser.ast.type.ClassOrInterfaceType; import com.github.javaparser.ast.type.TypeParameter; import com.github.javaparser.utils.SourceRoot; -import de.uka.ilkd.key.java.ast.expression.Assignment; -import de.uka.ilkd.key.java.ast.expression.ExpressionStatement; +import java.util.List; + +import static com.github.javaparser.ast.Modifier.DefaultKeyword.DEFAULT; import static com.github.javaparser.ast.Modifier.DefaultKeyword.PUBLIC; import static org.key_project.ncore.java.Generator.ROOT; @@ -30,7 +27,6 @@ public static void createVisitor(List nodeUnits, SourceRoot sou String name = "org.key_project.key.java.ast.visitor"; cu.setPackageDeclaration(name); cu.setStorage(ROOT.resolve("org/key_project/java/ast/visitor/Visitor.java")); - System.out.println(cu.getStorage().get().getPath()); var generic = new TypeParameter("R"); @@ -64,6 +60,22 @@ public static void createVisitor(List nodeUnits, SourceRoot sou } } sourceRoot.add(cu); + + var s = StaticJavaParser.parseBlock("{return defaultVisit(n);}"); + var visitorWithDefaults = cu.clone(); + visitorWithDefaults.setStorage(ROOT.resolve("org/key_project/java/ast/visitor/VisitorWithDefaults.java")); + final var vwdef = visitorWithDefaults.getType(0); + vwdef.setName("VisitorWithDefaults"); + for (var method : vwdef.getMethods()) { + method.addModifier(DEFAULT); + method.setBody(s.clone()); + } + visitorWithDefaults.addImport("org.key_project.java.ast.*"); + var m = vwdef.addMethod("defaultVisit"); + m.addParameter("JavaSourceElement", "n"); + m.setType(generic.clone()); + m.setBody(null); + sourceRoot.add(visitorWithDefaults); } public static void createVoidVisitor(List nodeUnits, SourceRoot sourceRoot) { @@ -144,6 +156,52 @@ public static void createTraversalVisitor(List nodeUnits, Sourc sourceRoot.add(cu); } + public static void createArgVisitor(List nodeUnits, SourceRoot sourceRoot) { + var cu = new CompilationUnit(); + String name = "org.key_project.key.java.ast.visitor"; + cu.setPackageDeclaration(name); + cu.setStorage(ROOT.resolve("org/key_project/java/ast/visitor/ArgVisitor.java")); + System.out.println(cu.getStorage().get().getPath()); + + var generic = new TypeParameter("R"); + var argType = new TypeParameter("A"); + + var type = cu.addClass("ArgVisitor"); + type.setInterface(true); + type.addTypeParameter(generic.clone()); + type.addTypeParameter(argType.clone()); + + for (CompilationUnit clazz : nodeUnits) { + try { + var t = clazz.getPrimaryType().get(); + if (!(t instanceof ClassOrInterfaceDeclaration c)) continue; + if (c.isInterface()) continue; + + cu.addImport(t.getFullyQualifiedName().get()); + + var m = type.addMethod("visit"); + m.addParameter(new ClassOrInterfaceType(null, t.getNameAsString()), "n"); + m.addParameter(argType.clone(), "arg"); + m.setType(generic.clone()); + m.setBody(null); + + var accept = t.addMethod("accept", PUBLIC); + accept.setType(generic.clone()); + accept.getTypeParameters().add(generic.clone()); + accept.getTypeParameters().add(argType.clone()); + accept.addParameter(new ClassOrInterfaceType(null, new SimpleName(type.getFullyQualifiedName().get()), + new NodeList<>(generic.clone(),argType.clone())), + "visitor"); + accept.addParameter(argType.clone(), "arg"); + accept.getBody().get() + .addStatement("return visitor.visit(this,arg);"); + } catch (Exception e) { + System.err.println(e.getMessage() + " :: " + clazz.getStorage().get().getPath()); + } + } + sourceRoot.add(cu); + } + public static void createDeepCopyVisitor(List nodeUnits, SourceRoot sourceRoot) { @@ -152,6 +210,4 @@ public static void createDeepCopyVisitor(List nodeUnits, Source public interface PostStep { void applyOn(List nodeUnits, SourceRoot sourceRoot); } - - } diff --git a/key.ncore.java/src/main/java/org/key_project/java/ast/EqEx.java b/key.ncore.java/src/main/java/org/key_project/java/ast/EqEx.java index f129629fb70..ce5fd804282 100644 --- a/key.ncore.java/src/main/java/org/key_project/java/ast/EqEx.java +++ b/key.ncore.java/src/main/java/org/key_project/java/ast/EqEx.java @@ -8,6 +8,6 @@ /// Exclude a field from equality and hashCode. @Retention(RetentionPolicy.SOURCE) -@Target(ElementType.FIELD) +@Target({ElementType.PARAMETER, ElementType.FIELD}) public @interface EqEx { } diff --git a/key.ncore.java/src/main/java/org/key_project/java/ast/Package.java b/key.ncore.java/src/main/java/org/key_project/java/ast/Package.java new file mode 100644 index 00000000000..be1b2fad55d --- /dev/null +++ b/key.ncore.java/src/main/java/org/key_project/java/ast/Package.java @@ -0,0 +1,13 @@ +package org.key_project.java.ast; + +import java.lang.annotation.ElementType; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; + +/// Sets the suffix of the package with respect to `org.key_project.java.ast` +@Retention(RetentionPolicy.SOURCE) +@Target({ElementType.TYPE}) +public @interface Package { + String value() default ""; +} diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java index 70936b13073..110271c6a2b 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java +++ b/key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java @@ -14,7 +14,7 @@ import org.jspecify.annotations.Nullable; public class ImmutableArray - implements java.lang.Iterable, java.io.Serializable { + implements RoList, java.io.Serializable { private static final long serialVersionUID = -9041545065066866250L; @@ -106,7 +106,7 @@ public final boolean isEmpty() { return content.length == 0; } - public boolean contains(S op) { + public boolean contains(Object op) { for (S el : content) { if (Objects.equals(el, op)) { return true; @@ -174,6 +174,16 @@ public Iterator iterator() { return new ArrayIterator(this); } + @Override + public S getFirst() { + return this.content[0]; + } + + @Override + public S getLast() { + return this.content[this.content.length - 1]; + } + private static class ArrayIterator implements Iterator { private int i = 0; diff --git a/key.util/src/main/java/org/key_project/util/collection/RoList.java b/key.util/src/main/java/org/key_project/util/collection/RoList.java new file mode 100644 index 00000000000..71c374c0fa1 --- /dev/null +++ b/key.util/src/main/java/org/key_project/util/collection/RoList.java @@ -0,0 +1,33 @@ +package org.key_project.util.collection; + +import org.jspecify.annotations.Nullable; + +import java.util.Iterator; +import java.util.List; +import java.util.stream.Stream; + +/** + * + * @author Alexander Weigl + * @version 1 (4/19/26) + */ +public interface RoList extends Iterable { + int size(); + E get(int index); + + boolean isEmpty(); + default boolean isNonEmpty() { + return !isEmpty(); + } + + boolean contains(Object e); + Iterator iterator(); + E getFirst(); + E getLast(); + + Stream stream(); + + default List toList() { + return stream().toList(); + } +} From d64ab7f38152005c71b0647e35ba8e5bc39945be Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sun, 19 Apr 2026 18:19:38 +0200 Subject: [PATCH 5/7] wip --- key.ncore.java/src/adt/java-ast.java | 5 +- .../org/key_project/ncore/java/Generator.java | 2 + .../org/key_project/ncore/java/NodeSteps.java | 6 + .../org/key_project/ncore/java/PostSteps.java | 181 ++++++++++++++---- .../java/org/key_project/java/ast/Root.java | 13 ++ .../org/key_project/java/ast/Visitable.java | 16 ++ .../key_project/util/collection/RoList.java | 110 ++++++++++- 7 files changed, 293 insertions(+), 40 deletions(-) create mode 100644 key.ncore.java/src/main/java/org/key_project/java/ast/Root.java create mode 100644 key.ncore.java/src/main/java/org/key_project/java/ast/Visitable.java diff --git a/key.ncore.java/src/adt/java-ast.java b/key.ncore.java/src/adt/java-ast.java index ace984c2615..19932f42a20 100644 --- a/key.ncore.java/src/adt/java-ast.java +++ b/key.ncore.java/src/adt/java-ast.java @@ -2,9 +2,10 @@ import org.jspecify.annotations.Nullable; import de.uka.ilkd.key.speclang.jml.pretranslation.*; import de.uka.ilkd.key.java.ast.PositionInfo; +import org.key_project.util.collection.*; -// ROOT -abstract class JavaSourceElement { +@Root +abstract class JavaSourceElement implements Visitable { @EqEx @Nullable PositionInfo positionInfo; } diff --git a/key.ncore.java/src/generator/java/org/key_project/ncore/java/Generator.java b/key.ncore.java/src/generator/java/org/key_project/ncore/java/Generator.java index aa799fd9f89..310ed3aba2e 100644 --- a/key.ncore.java/src/generator/java/org/key_project/ncore/java/Generator.java +++ b/key.ncore.java/src/generator/java/org/key_project/ncore/java/Generator.java @@ -45,6 +45,7 @@ public Generator() { preSteps.add(new PreSteps.PreComputation()); addStep(NodeSteps::setPackage); + addStep(NodeSteps::enforceHierarchy); addStep(NodeSteps::processFields); addStep(NodeSteps::addAllFieldsConstructor); addStep(NodeSteps::addAllWoOptFieldsConstructor); @@ -63,6 +64,7 @@ public Generator() { postSteps.add(PostSteps::createArgVisitor); postSteps.add(PostSteps::createVoidVisitor); postSteps.add(PostSteps::createTraversalVisitor); + postSteps.add(PostSteps::createTraversalCopyOnDemandVisitor); postSteps.add(PostSteps::createDeepCopyVisitor); } diff --git a/key.ncore.java/src/generator/java/org/key_project/ncore/java/NodeSteps.java b/key.ncore.java/src/generator/java/org/key_project/ncore/java/NodeSteps.java index a9fc3ac8a20..f9c078e97d1 100644 --- a/key.ncore.java/src/generator/java/org/key_project/ncore/java/NodeSteps.java +++ b/key.ncore.java/src/generator/java/org/key_project/ncore/java/NodeSteps.java @@ -467,6 +467,12 @@ private static boolean isList(VariableDeclarator type) { return false; } + public static void enforceHierarchy(ClassOrInterfaceDeclaration decl) { + if(decl.getExtendedTypes().isEmpty()) { + decl.addExtendedType("JavaSourceElement"); + } + } + interface NodeStep { void applyOn(ClassOrInterfaceDeclaration target); } diff --git a/key.ncore.java/src/generator/java/org/key_project/ncore/java/PostSteps.java b/key.ncore.java/src/generator/java/org/key_project/ncore/java/PostSteps.java index 72e134883d5..6bae1750d58 100644 --- a/key.ncore.java/src/generator/java/org/key_project/ncore/java/PostSteps.java +++ b/key.ncore.java/src/generator/java/org/key_project/ncore/java/PostSteps.java @@ -8,29 +8,28 @@ import com.github.javaparser.ast.Modifier; import com.github.javaparser.ast.NodeList; import com.github.javaparser.ast.body.ClassOrInterfaceDeclaration; +import com.github.javaparser.ast.body.FieldDeclaration; +import com.github.javaparser.ast.body.VariableDeclarator; import com.github.javaparser.ast.expr.SimpleName; import com.github.javaparser.ast.nodeTypes.modifiers.NodeWithPrivateModifier; import com.github.javaparser.ast.stmt.BlockStmt; import com.github.javaparser.ast.type.ClassOrInterfaceType; +import com.github.javaparser.ast.type.Type; import com.github.javaparser.ast.type.TypeParameter; import com.github.javaparser.utils.SourceRoot; import java.util.List; +import java.util.stream.Collectors; -import static com.github.javaparser.ast.Modifier.DefaultKeyword.DEFAULT; -import static com.github.javaparser.ast.Modifier.DefaultKeyword.PUBLIC; +import static com.github.javaparser.ast.Modifier.DefaultKeyword.*; import static org.key_project.ncore.java.Generator.ROOT; public class PostSteps { public static void createVisitor(List nodeUnits, SourceRoot sourceRoot) { - var cu = new CompilationUnit(); - String name = "org.key_project.key.java.ast.visitor"; - cu.setPackageDeclaration(name); - cu.setStorage(ROOT.resolve("org/key_project/java/ast/visitor/Visitor.java")); - var generic = new TypeParameter("R"); - var type = cu.addClass("Visitor"); + var cu = new CompilationUnit(); + var type = createTypeAndSetDefaults(cu, "Visitor", PUBLIC); type.setInterface(true); type.addTypeParameter(generic.clone()); @@ -40,8 +39,6 @@ public static void createVisitor(List nodeUnits, SourceRoot sou if (!(t instanceof ClassOrInterfaceDeclaration c)) continue; if (c.isInterface()) continue; - cu.addImport(t.getFullyQualifiedName().get()); - var m = type.addMethod("visit"); m.addParameter(new ClassOrInterfaceType(null, t.getNameAsString()), "n"); m.setType(generic.clone()); @@ -80,12 +77,7 @@ public static void createVisitor(List nodeUnits, SourceRoot sou public static void createVoidVisitor(List nodeUnits, SourceRoot sourceRoot) { var cu = new CompilationUnit(); - String name = "org.key_project.key.java.ast.visitor"; - cu.setPackageDeclaration(name); - cu.setStorage(ROOT.resolve("org/key_project/java/ast/visitor/VoidVisitor.java")); - System.out.println(cu.getStorage().get().getPath()); - - var type = cu.addClass("VoidVisitor"); + var type = createTypeAndSetDefaults(cu, "VoidVisitor", PUBLIC); type.setInterface(true); for (CompilationUnit clazz : nodeUnits) { @@ -94,8 +86,6 @@ public static void createVoidVisitor(List nodeUnits, SourceRoot if (!(t instanceof ClassOrInterfaceDeclaration c)) continue; if (c.isInterface()) continue; - cu.addImport(t.getFullyQualifiedName().get()); - var m = type.addMethod("visit"); m.addParameter(new ClassOrInterfaceType(null, t.getNameAsString()), "n"); m.setBody(null); @@ -116,20 +106,14 @@ public static void createVoidVisitor(List nodeUnits, SourceRoot public static void createTraversalVisitor(List nodeUnits, SourceRoot sourceRoot) { var cu = new CompilationUnit(); - String name = "org.key_project.key.java.ast.visitor"; - cu.setPackageDeclaration(name); - cu.setStorage(ROOT.resolve("org/key_project/java/ast/visitor/TraversalVisitor.java")); - System.out.println(cu.getStorage().get().getPath()); - - var type = cu.addClass("TraversalVisitor", PUBLIC, - Modifier.DefaultKeyword.ABSTRACT); + var type = createTypeAndSetDefaults(cu, "CopyVisitor", PUBLIC); type.getImplementedTypes().add( - (ClassOrInterfaceType) StaticJavaParser.parseType("Visitor")); + (ClassOrInterfaceType) StaticJavaParser.parseType("Visitor")); + addAcceptMethods(type); for (CompilationUnit clazz : nodeUnits) { try { var t = clazz.getPrimaryType().get(); - cu.addImport(t.getFullyQualifiedName().get()); if (!(t instanceof ClassOrInterfaceDeclaration c)) continue; if (c.isInterface()) continue; @@ -144,9 +128,9 @@ public static void createTraversalVisitor(List nodeUnits, Sourc .forEach(f -> body.addStatement( "b.%s = (%s) accept(n.%s());" - .formatted(f.getVariable(0).getNameAsExpression(), - f.getVariable(0).getTypeAsString(), - f.getVariable(0).getNameAsExpression()))); + .formatted(f.getVariable(0).getNameAsExpression(), + f.getVariable(0).getTypeAsString(), + f.getVariable(0).getNameAsExpression()))); body.addStatement("return b.build();"); m.setType(new ClassOrInterfaceType(null, t.getFullyQualifiedName().get())); } catch (Exception e) { @@ -156,17 +140,142 @@ public static void createTraversalVisitor(List nodeUnits, Sourc sourceRoot.add(cu); } - public static void createArgVisitor(List nodeUnits, SourceRoot sourceRoot) { + public static void createTraversalCopyOnDemandVisitor(List nodeUnits, SourceRoot sourceRoot) { var cu = new CompilationUnit(); - String name = "org.key_project.key.java.ast.visitor"; + var type = createTypeAndSetDefaults(cu, "CopyOnWriteVisitor", PUBLIC); + + type.getImplementedTypes().add( + (ClassOrInterfaceType) StaticJavaParser.parseType("Visitor")); + addAcceptMethods(type); + + + for (CompilationUnit clazz : nodeUnits) { + try { + var t = clazz.getPrimaryType().get(); + + if (!(t instanceof ClassOrInterfaceDeclaration c)) continue; + if (c.isInterface()) continue; + + var m = type.addMethod("visit", PUBLIC); + m.addParameter(new ClassOrInterfaceType(null, t.getNameAsString()), "n"); + m.addAnnotation(Override.class); + BlockStmt body = m.getBody().get(); + body.addStatement("var b = n.builder();"); + t.getFields() + .stream() + .filter(NodeWithPrivateModifier::isPrivate) + .filter(PostSteps::isAstNode) + .forEach(f -> + body.addStatement( + "b.%s = (%s) accept(n.%s());" + .formatted(f.getVariable(0).getNameAsExpression(), + f.getVariable(0).getTypeAsString(), + f.getVariable(0).getNameAsExpression()))); + final var formatted = "boolean clean = %s;".formatted( + t.getFields().isEmpty() ? "false" : + t.getFields() + .stream().filter(NodeWithPrivateModifier::isPrivate) + .map(it -> { + final var n = it.getVariable(0).getNameAsString(); + return "(n.%s() == b.%s)".formatted(n, n); + }) + .collect(Collectors.joining("&&")) + ); + body.addStatement(formatted); + body.addStatement("return clean?n:b.build();"); + m.setType(new ClassOrInterfaceType(null, t.getFullyQualifiedName().get())); + } catch (Exception e) { + System.err.println(e.getMessage() + " :: " + clazz.getStorage().get().getPath()); + } + } + sourceRoot.add(cu); + } + + private static boolean isAstNode(FieldDeclaration field) { + return isAstNode(field.getVariables().getFirst()); + } + + private static boolean isAstNode(VariableDeclarator v) { + return isAstNode(v.getType()); + } + + private static boolean isAstNode(Type type) { + if (type.isClassOrInterfaceType()) { + var c = type.asClassOrInterfaceType(); + if (c.getNameAsString().equals("RoList")) { + return isAstNode(c.getTypeArguments().get().getFirst()); + } + + final var name = c.getNameAsString(); + if (name.equals("String")) { + return false; + } + try { + c.toUnboxedType(); + return false; + } catch (UnsupportedOperationException e) { + return !(name.contains("Kind") || name.equals("PositionInfo") || name.equals("JMLModifiers")); + } + } + return false; + } + + /// + /// ```java + /// T accept(T n) { + /// return n != null ? n.accept(this) : null; + /// } + /// RoList accept(RoList n) { + /// return n != null ? n.stream().map(it -> (T) it.accept(this)).toList() : null; + /// } + /// ``` + private static void addAcceptMethods(ClassOrInterfaceDeclaration type) { + var t = StaticJavaParser.parseTypeParameter("T extends Visitable"); + var typeT = StaticJavaParser.parseType("T"); + + { + var accept = type.addMethod("accept", PROTECTED); + accept.addTypeParameter(t); + accept.addParameter(typeT, "n"); + accept.setType(typeT.clone()); + accept.getBody().get().addStatement("return n!=null?n.accept(this):null;"); + } + + { + var acceptList = type.addMethod("accept", PROTECTED); + acceptList.addTypeParameter(t.clone()); + acceptList.addParameter(StaticJavaParser.parseType("RoList"), "n"); + acceptList.setType("RoList"); + acceptList.getBody().get().addStatement("return n != null ? n.stream().map(it -> (T) it.accept(this)).collect(RoList.collector()) : null;"); + } + + { + var acceptList = type.addMethod("accept", PROTECTED); + acceptList.addTypeParameter("T"); + acceptList.addParameter("T", "n"); + acceptList.setType("T"); + acceptList.getBody().get().addStatement("return n;"); + } + } + + private static ClassOrInterfaceDeclaration createTypeAndSetDefaults(CompilationUnit cu, String typeName, Modifier.DefaultKeyword... mods) { + String name = "org.key_project.java.ast.visitor"; cu.setPackageDeclaration(name); - cu.setStorage(ROOT.resolve("org/key_project/java/ast/visitor/ArgVisitor.java")); - System.out.println(cu.getStorage().get().getPath()); + cu.addImport("org.key_project.java.ast.visitor.*"); + cu.addImport("org.key_project.java.ast.*"); + cu.addImport("de.uka.ilkd.key.java.ast.PositionInfo"); + cu.addImport("org.key_project.util.collection.*"); + cu.setStorage(ROOT.resolve("org/key_project/java/ast/visitor/%s.java".formatted(typeName))); + return cu.addClass(typeName, mods); + } + + public static void createArgVisitor(List nodeUnits, SourceRoot sourceRoot) { + var cu = new CompilationUnit(); + var type = createTypeAndSetDefaults(cu, "ArgVisitor", PUBLIC); var generic = new TypeParameter("R"); var argType = new TypeParameter("A"); - var type = cu.addClass("ArgVisitor"); type.setInterface(true); type.addTypeParameter(generic.clone()); type.addTypeParameter(argType.clone()); @@ -190,7 +299,7 @@ public static void createArgVisitor(List nodeUnits, SourceRoot accept.getTypeParameters().add(generic.clone()); accept.getTypeParameters().add(argType.clone()); accept.addParameter(new ClassOrInterfaceType(null, new SimpleName(type.getFullyQualifiedName().get()), - new NodeList<>(generic.clone(),argType.clone())), + new NodeList<>(generic.clone(), argType.clone())), "visitor"); accept.addParameter(argType.clone(), "arg"); accept.getBody().get() diff --git a/key.ncore.java/src/main/java/org/key_project/java/ast/Root.java b/key.ncore.java/src/main/java/org/key_project/java/ast/Root.java new file mode 100644 index 00000000000..85d775b6a10 --- /dev/null +++ b/key.ncore.java/src/main/java/org/key_project/java/ast/Root.java @@ -0,0 +1,13 @@ +package org.key_project.java.ast; + + +import java.lang.annotation.ElementType; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; + +/// Marks the ROOT class of the hierarchy +@Retention(RetentionPolicy.SOURCE) +@Target({ElementType.TYPE}) +public @interface Root { +} diff --git a/key.ncore.java/src/main/java/org/key_project/java/ast/Visitable.java b/key.ncore.java/src/main/java/org/key_project/java/ast/Visitable.java new file mode 100644 index 00000000000..a79c35fd532 --- /dev/null +++ b/key.ncore.java/src/main/java/org/key_project/java/ast/Visitable.java @@ -0,0 +1,16 @@ +package org.key_project.java.ast; + +import org.key_project.java.ast.visitor.*; + +/** + * + * @author Alexander Weigl + * @version 1 (4/19/26) + */ +public interface Visitable { + R accept(Visitor visitor); + + R accept(ArgVisitor visitor, A arg); + + void accept(VoidVisitor visitor); +} diff --git a/key.util/src/main/java/org/key_project/util/collection/RoList.java b/key.util/src/main/java/org/key_project/util/collection/RoList.java index 71c374c0fa1..14ed7069be9 100644 --- a/key.util/src/main/java/org/key_project/util/collection/RoList.java +++ b/key.util/src/main/java/org/key_project/util/collection/RoList.java @@ -2,8 +2,12 @@ import org.jspecify.annotations.Nullable; -import java.util.Iterator; -import java.util.List; +import java.util.*; +import java.util.function.BiConsumer; +import java.util.function.BinaryOperator; +import java.util.function.Function; +import java.util.function.Supplier; +import java.util.stream.Collector; import java.util.stream.Stream; /** @@ -12,6 +16,108 @@ * @version 1 (4/19/26) */ public interface RoList extends Iterable { + RoList EMPTY = new RoList<>() { + @Override + public int size() { + return 0; + } + + @Override + public Object get(int index) { + throw new IndexOutOfBoundsException(); + } + + @Override + public boolean isEmpty() { + return true; + } + + @Override + public boolean contains(Object e) { + return false; + } + + @Override + public Iterator iterator() { + return new Iterator<>() { + @Override + public boolean hasNext() { + return false; + } + + @Override + public Object next() { + throw new NoSuchElementException(); + } + }; + } + + @Override + public Object getFirst() { + throw new NoSuchElementException(); + } + + @Override + public Object getLast() { + throw new NoSuchElementException(); + } + + @Override + public Stream stream() { + return Stream.empty(); + } + }; + + static Collector, RoList> collector() { + return new Collector<>() { + @Override + public Supplier> supplier() { + return ArrayList::new; + } + + @Override + public BiConsumer, T> accumulator() { + return List::add; + } + + @Override + public BinaryOperator> combiner() { + return (a, b) -> { + a.addAll(b); + return a; + }; + } + + @Override + public Function, RoList> finisher() { + return (a) -> RoList.fromList(a); + } + + @Override + public Set characteristics() { + return Set.of(); + } + }; + } + + static RoList fromList(List a) { + if(a.isEmpty()) { + return RoList.empty(); + }else if(a.size()==1){ + return RoList.singleton(a.getFirst()); + }else{ + return new ImmutableArray<>(a); + } + } + + static RoList singleton(T item) { + return new SingletonRoList<>(item); + } + + static RoList empty() { + return (RoList) EMPTY; + } + int size(); E get(int index); From c50bbc13ce39be6fa6eb3a3f6cf524a4f1b8ddbc Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sun, 19 Apr 2026 18:40:39 +0200 Subject: [PATCH 6/7] spotless --- .../org/key_project/ncore/java/Generator.java | 20 +-- .../org/key_project/ncore/java/NodeSteps.java | 125 +++++++++--------- .../org/key_project/ncore/java/PostSteps.java | 125 ++++++++++-------- .../org/key_project/ncore/java/PreSteps.java | 18 ++- .../key_project/java/ast/AssignmentKind.java | 35 ++--- .../java/ast/BinaryOperatorKind.java | 3 + .../java/org/key_project/java/ast/EqEx.java | 5 +- .../key_project/java/ast/LogicFunction.java | 53 ++++---- .../org/key_project/java/ast/Package.java | 5 +- .../java/org/key_project/java/ast/Root.java | 5 +- .../java/ast/UnaryOperatorKind.java | 41 +++--- .../org/key_project/java/ast/Visitable.java | 3 + .../key_project/util/collection/RoList.java | 18 ++- 13 files changed, 259 insertions(+), 197 deletions(-) diff --git a/key.ncore.java/src/generator/java/org/key_project/ncore/java/Generator.java b/key.ncore.java/src/generator/java/org/key_project/ncore/java/Generator.java index 310ed3aba2e..218205132de 100644 --- a/key.ncore.java/src/generator/java/org/key_project/ncore/java/Generator.java +++ b/key.ncore.java/src/generator/java/org/key_project/ncore/java/Generator.java @@ -3,16 +3,6 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.ncore.java; -import com.github.javaparser.ParseProblemException; -import com.github.javaparser.ParserConfiguration; -import com.github.javaparser.StaticJavaParser; -import com.github.javaparser.ast.CompilationUnit; -import com.github.javaparser.ast.body.ClassOrInterfaceDeclaration; -import com.github.javaparser.utils.SourceRoot; -import org.key_project.ncore.java.NodeSteps.NodeStep; -import org.key_project.ncore.java.PostSteps.PostStep; -import org.key_project.ncore.java.PreSteps.PreStep; - import java.io.File; import java.nio.file.Files; import java.nio.file.Path; @@ -22,6 +12,16 @@ import java.util.concurrent.Callable; import java.util.stream.Stream; +import org.key_project.ncore.java.NodeSteps.NodeStep; +import org.key_project.ncore.java.PostSteps.PostStep; +import org.key_project.ncore.java.PreSteps.PreStep; + +import com.github.javaparser.ParserConfiguration; +import com.github.javaparser.StaticJavaParser; +import com.github.javaparser.ast.CompilationUnit; +import com.github.javaparser.ast.body.ClassOrInterfaceDeclaration; +import com.github.javaparser.utils.SourceRoot; + /** * * @author Alexander Weigl diff --git a/key.ncore.java/src/generator/java/org/key_project/ncore/java/NodeSteps.java b/key.ncore.java/src/generator/java/org/key_project/ncore/java/NodeSteps.java index f9c078e97d1..a65a83a6fa2 100644 --- a/key.ncore.java/src/generator/java/org/key_project/ncore/java/NodeSteps.java +++ b/key.ncore.java/src/generator/java/org/key_project/ncore/java/NodeSteps.java @@ -1,5 +1,10 @@ +/* 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 org.key_project.ncore.java; +import java.util.stream.Collectors; + import com.github.javaparser.StaticJavaParser; import com.github.javaparser.ast.CompilationUnit; import com.github.javaparser.ast.NodeList; @@ -8,7 +13,6 @@ import com.github.javaparser.ast.nodeTypes.NodeWithName; import com.github.javaparser.ast.nodeTypes.NodeWithSimpleName; import com.github.javaparser.ast.stmt.BlockStmt; -import com.github.javaparser.ast.stmt.ExpressionStmt; import com.github.javaparser.ast.stmt.ReturnStmt; import com.github.javaparser.ast.type.ClassOrInterfaceType; import com.github.javaparser.ast.type.PrimitiveType; @@ -17,8 +21,6 @@ import org.jspecify.annotations.NullMarked; import org.jspecify.annotations.Nullable; -import java.util.stream.Collectors; - import static com.github.javaparser.StaticJavaParser.*; import static com.github.javaparser.ast.Modifier.DefaultKeyword.*; @@ -33,28 +35,28 @@ static void addWiths(ClassOrInterfaceDeclaration target) { target.getFields().stream() .flatMap(it -> it.getVariables().stream()).forEach(it -> { var args = - target.getFields().stream() - .flatMap(f -> f.getVariables().stream()) - .map(v -> { - if (v == it) { - return (Expression) v.getNameAsExpression(); - } else { - return new MethodCallExpr(null, v.getNameAsString()); - } - }).toList(); + target.getFields().stream() + .flatMap(f -> f.getVariables().stream()) + .map(v -> { + if (v == it) { + return (Expression) v.getNameAsExpression(); + } else { + return new MethodCallExpr(null, v.getNameAsString()); + } + }).toList(); var m = target.addMethod("with" + upperStart(it.getNameAsString()), PUBLIC); m.addParameter(new Parameter(it.getType().clone(), it.getNameAsString())); m.setType(new ClassOrInterfaceType(null, target.getNameAsString())); m.getBody().get().addStatement(new ReturnStmt( - new ObjectCreationExpr(null, - new ClassOrInterfaceType(null, target.getNameAsString()), - new NodeList<>(args)))); + new ObjectCreationExpr(null, + new ClassOrInterfaceType(null, target.getNameAsString()), + new NodeList<>(args)))); }); } private static String upperStart(String nameAsString) { - var c = nameAsString.substring(0,1).toUpperCase(); + var c = nameAsString.substring(0, 1).toUpperCase(); return c + nameAsString.substring(1); } @@ -71,12 +73,12 @@ static void addEquals(ClassOrInterfaceDeclaration target) { BlockStmt body = equals.getBody().get(); body.addStatement(parseStatement("if(this == o) return true;")); body.addStatement(parseStatement( - "if(!(o instanceof %s that)) return false;".formatted(target.getNameAsString()))); + "if(!(o instanceof %s that)) return false;".formatted(target.getNameAsString()))); Expression equalFields = target.getFields().stream() .filter(it -> it.getAnnotationByName("EqEx").isEmpty()) .flatMap(it -> it.getVariables().stream()) .map(it -> callObjects("equals", it.getNameAsExpression(), - new FieldAccessExpr(new NameExpr("that"), it.getNameAsString()))) + new FieldAccessExpr(new NameExpr("that"), it.getNameAsString()))) .reduce((a, b) -> new BinaryExpr(a, b, BinaryExpr.Operator.AND)) .orElse(new BooleanLiteralExpr(true)); body.addStatement(new ReturnStmt(equalFields)); @@ -103,11 +105,11 @@ static void addHashCode(ClassOrInterfaceDeclaration target) { assert false : "No defined fields"; else hashCode.getBody().get().addStatement(new ReturnStmt( - callObjects("hash", args))); + callObjects("hash", args))); } static void ToString(ClassOrInterfaceDeclaration clazz) { - if (clazz.isAbstract()||clazz.isInterface()) { + if (clazz.isAbstract() || clazz.isInterface()) { return; } @@ -115,16 +117,16 @@ static void ToString(ClassOrInterfaceDeclaration clazz) { toString.addAnnotation(Override.class); toString.setType(String.class); var parameters = - clazz.getFields().stream().flatMap(it -> it.getVariables().stream()).toList(); + clazz.getFields().stream().flatMap(it -> it.getVariables().stream()).toList(); var sb = (clazz.getNameAsString() + "[") - + parameters.stream().map(NodeWithSimpleName::getNameAsString).map(it -> it + "=%s") - .collect(Collectors.joining(", ")) - + "]"; + + parameters.stream().map(NodeWithSimpleName::getNameAsString).map(it -> it + "=%s") + .collect(Collectors.joining(", ")) + + "]"; var args = parameters.stream().map(NodeWithSimpleName::getNameAsExpression) .map(it -> (Expression) it).toList(); toString.getBody().get().addStatement(new ReturnStmt( - new MethodCallExpr(new StringLiteralExpr(sb), "formatted", new NodeList<>(args)))); + new MethodCallExpr(new StringLiteralExpr(sb), "formatted", new NodeList<>(args)))); } private static Expression callObjects(String method, Expression... args) { @@ -147,20 +149,21 @@ static void addAllFieldsConstructor(ClassOrInterfaceDeclaration target) { constr.setModifiers(PUBLIC); for (var field : target.getFields()) { - var isOptional = field.getAnnotations().stream().anyMatch(it -> it.getNameAsString().equals("Nullable")); + var isOptional = field.getAnnotations().stream() + .anyMatch(it -> it.getNameAsString().equals("Nullable")); for (var variable : field.getVariables()) { final var p = new Parameter(variable.getType().clone(), variable.getNameAsString()); field.getAnnotations().stream().map(AnnotationExpr::clone) .forEach(p::addAnnotation); params.add(p); - if(isOptional){ + if (isOptional) { body.addStatement( - "this.%s = %s;".formatted( - variable.getNameAsString(), variable.getNameAsString())); - }else { + "this.%s = %s;".formatted( + variable.getNameAsString(), variable.getNameAsString())); + } else { body.addStatement( - "this.%s = Objects.requireNonNull(%s);".formatted( - variable.getNameAsString(), variable.getNameAsString())); + "this.%s = Objects.requireNonNull(%s);".formatted( + variable.getNameAsString(), variable.getNameAsString())); } } } @@ -180,21 +183,23 @@ static void addAllWoOptFieldsConstructor(ClassOrInterfaceDeclaration target) { constr.setModifiers(PUBLIC); for (var field : target.getFields()) { - var isOptional = field.getAnnotations().stream().anyMatch(it -> it.getNameAsString().equals("Nullable")); + var isOptional = field.getAnnotations().stream() + .anyMatch(it -> it.getNameAsString().equals("Nullable")); for (var variable : field.getVariables()) { - if(isOptional){ + if (isOptional) { body.addStatement( - "this.%s = null;".formatted(variable.getNameAsString())); - }else { - final var p = new Parameter(variable.getType().clone(), variable.getNameAsString()); + "this.%s = null;".formatted(variable.getNameAsString())); + } else { + final var p = + new Parameter(variable.getType().clone(), variable.getNameAsString()); field.getAnnotations().stream().map(AnnotationExpr::clone) .forEach(p::addAnnotation); params.add(p); body.addStatement( - "this.%s = Objects.requireNonNull(%s);".formatted( - variable.getNameAsString(), variable.getNameAsString())); + "this.%s = Objects.requireNonNull(%s);".formatted( + variable.getNameAsString(), variable.getNameAsString())); } } } @@ -214,14 +219,14 @@ static void addOverrideConstructor(ClassOrInterfaceDeclaration target) { var params = constr.getParameters(); constr.setName(target.getNameAsString()); params.add( - new Parameter(new ClassOrInterfaceType(null, target.getNameAsString()), "other")); + new Parameter(new ClassOrInterfaceType(null, target.getNameAsString()), "other")); params.add(new Parameter(parseType("Properties"), "map")); var args = target.getFields().stream().flatMap(it -> it.getVariables().stream()) .map(NodeWithSimpleName::getNameAsString) .map(it -> (Expression) parseExpression( - "map.get(PROPERTY_%s, other.%s)".formatted(it.toUpperCase(), it))) + "map.get(PROPERTY_%s, other.%s)".formatted(it.toUpperCase(), it))) .toList(); body.addStatement(new MethodCallExpr(null, "this", new NodeList<>(args))); } @@ -240,7 +245,7 @@ static void addOverrideConstructor2(ClassOrInterfaceDeclaration target) { var args = target.getFields().stream().flatMap(it -> it.getVariables().stream()) .map(NodeWithSimpleName::getNameAsString) .map(it -> (Expression) parseExpression( - "map.get(PROPERTY_%s)".formatted(it.toUpperCase()))) + "map.get(PROPERTY_%s)".formatted(it.toUpperCase()))) .toList(); body.addStatement(new MethodCallExpr(null, "this", new NodeList<>(args))); } @@ -259,7 +264,7 @@ static void addGetProperties(ClassOrInterfaceDeclaration target) { target.getFields().stream() .flatMap(it -> it.getVariables().stream()) .forEach(variable -> body.addStatement("p.set(PROPERTY_%s, %s());".formatted( - variable.getNameAsString().toUpperCase(), variable.getNameAsString()))); + variable.getNameAsString().toUpperCase(), variable.getNameAsString()))); body.addStatement("return p;"); } @@ -273,7 +278,7 @@ static void addCopyConstructor(ClassOrInterfaceDeclaration target) { var params = constr.getParameters(); constr.setName(target.getNameAsString()); params.add( - new Parameter(new ClassOrInterfaceType(null, target.getNameAsString()), "other")); + new Parameter(new ClassOrInterfaceType(null, target.getNameAsString()), "other")); /* * for (var field : target.getFields()) { @@ -317,8 +322,8 @@ static void setPackage(ClassOrInterfaceDeclaration target) { target.setInterface(true); target.addModifier(SEALED); target.removeModifier(ABSTRACT); - var permittedTypes - = Generator.INSTANCE.getStep(PreSteps.PreComputation.class).permittedTypes; + var permittedTypes = + Generator.INSTANCE.getStep(PreSteps.PreComputation.class).permittedTypes; for (var s : permittedTypes.get(target.getNameAsString())) { target.getPermittedTypes().add(new ClassOrInterfaceType(null, s)); } @@ -338,12 +343,12 @@ static void processFieldsAccessor(ClassOrInterfaceDeclaration target) { for (var field : target.getFields()) { for (var variable : field.getVariables()) { final var dataKey = new ClassOrInterfaceType(null, new SimpleName("Property"), - new NodeList<>(toBoxType(variable.getType().clone()))); + new NodeList<>(toBoxType(variable.getType().clone()))); var f = target.addField( - dataKey, "PROPERTY_" + variable.getNameAsString().toUpperCase(), PUBLIC, STATIC, - FINAL); + dataKey, "PROPERTY_" + variable.getNameAsString().toUpperCase(), PUBLIC, STATIC, + FINAL); f.getVariables().getFirst().setInitializer( - "new Property<>(\"%s\")".formatted(variable.getNameAsString())); + "new Property<>(\"%s\")".formatted(variable.getNameAsString())); } } } @@ -366,7 +371,7 @@ static void processFields(ClassOrInterfaceDeclaration target) { } for (var variable : field.getVariables()) { - if(isList(variable)) { + if (isList(variable)) { var old = variable.getType().asClassOrInterfaceType(); old.setName("RoList"); } @@ -408,7 +413,7 @@ static void addBuilder(ClassOrInterfaceDeclaration target) { for (var field : target.getFields()) { for (var variable : field.variables()) { var f = builder.addField(variable.getType().clone(), - variable.getNameAsString(), PUBLIC); + variable.getNameAsString(), PUBLIC); f.addAnnotation(Nullable.class); } } @@ -420,16 +425,16 @@ static void addBuilder(ClassOrInterfaceDeclaration target) { .map(it -> (Expression) it.getNameAsExpression()) .toList(); build.getBody().get().addStatement(new ReturnStmt( - new ObjectCreationExpr(null, - new ClassOrInterfaceType(null, target.getNameAsString()), - new NodeList<>(args)))); + new ObjectCreationExpr(null, + new ClassOrInterfaceType(null, target.getNameAsString()), + new NodeList<>(args)))); builder.getFields().stream().flatMap(it -> it.variables().stream()).forEach(it -> { var m = builder.addMethod(it.getNameAsString(), PUBLIC); m.addParameter(new Parameter(it.getType().clone(), it.getNameAsString())); m.setType(new ClassOrInterfaceType(null, "Builder")); m.getBody().get().addStatement( - "this.%s=%s;".formatted(it.getNameAsString(), it.getNameAsString())); + "this.%s=%s;".formatted(it.getNameAsString(), it.getNameAsString())); m.getBody().get().addStatement("return this;"); }); @@ -439,13 +444,13 @@ static void addBuilder(ClassOrInterfaceDeclaration target) { .forEach(it -> { var m = builder.addMethod(it.getNameAsString(), PUBLIC); var t = - it.getType().asClassOrInterfaceType().getTypeArguments().get().getFirst(); + it.getType().asClassOrInterfaceType().getTypeArguments().get().getFirst(); m.addParameter(new Parameter(t.clone(), it.getNameAsString())); m.setType(new ClassOrInterfaceType(null, "Builder")); m.getBody().get().addStatement("if(this.%s==null) this.%s = new ArrayList<>();" .formatted(it.getNameAsString(), it.getNameAsString())); m.getBody().get().addStatement( - "this.%s.add(%s);".formatted(it.getNameAsString(), it.getNameAsString())); + "this.%s.add(%s);".formatted(it.getNameAsString(), it.getNameAsString())); m.getBody().get().addStatement("return this;"); }); @@ -461,14 +466,14 @@ static void addBuilder(ClassOrInterfaceDeclaration target) { } private static boolean isList(VariableDeclarator type) { - if(type.getType().isClassOrInterfaceType()) { + if (type.getType().isClassOrInterfaceType()) { return type.getType().asClassOrInterfaceType().getNameAsString().equals("List"); } return false; } public static void enforceHierarchy(ClassOrInterfaceDeclaration decl) { - if(decl.getExtendedTypes().isEmpty()) { + if (decl.getExtendedTypes().isEmpty()) { decl.addExtendedType("JavaSourceElement"); } } diff --git a/key.ncore.java/src/generator/java/org/key_project/ncore/java/PostSteps.java b/key.ncore.java/src/generator/java/org/key_project/ncore/java/PostSteps.java index 6bae1750d58..2bcd7de6f98 100644 --- a/key.ncore.java/src/generator/java/org/key_project/ncore/java/PostSteps.java +++ b/key.ncore.java/src/generator/java/org/key_project/ncore/java/PostSteps.java @@ -3,6 +3,9 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.ncore.java; +import java.util.List; +import java.util.stream.Collectors; + import com.github.javaparser.StaticJavaParser; import com.github.javaparser.ast.CompilationUnit; import com.github.javaparser.ast.Modifier; @@ -18,9 +21,6 @@ import com.github.javaparser.ast.type.TypeParameter; import com.github.javaparser.utils.SourceRoot; -import java.util.List; -import java.util.stream.Collectors; - import static com.github.javaparser.ast.Modifier.DefaultKeyword.*; import static org.key_project.ncore.java.Generator.ROOT; @@ -36,8 +36,10 @@ public static void createVisitor(List nodeUnits, SourceRoot sou for (CompilationUnit clazz : nodeUnits) { try { var t = clazz.getPrimaryType().get(); - if (!(t instanceof ClassOrInterfaceDeclaration c)) continue; - if (c.isInterface()) continue; + if (!(t instanceof ClassOrInterfaceDeclaration c)) + continue; + if (c.isInterface()) + continue; var m = type.addMethod("visit"); m.addParameter(new ClassOrInterfaceType(null, t.getNameAsString()), "n"); @@ -47,9 +49,11 @@ public static void createVisitor(List nodeUnits, SourceRoot sou var accept = t.addMethod("accept", PUBLIC); accept.setType(generic.clone()); accept.getTypeParameters().add(generic.clone()); - accept.addParameter(new ClassOrInterfaceType(null, new SimpleName(type.getFullyQualifiedName().get()), - new NodeList<>(generic.clone())), - "visitor"); + accept.addParameter( + new ClassOrInterfaceType(null, + new SimpleName(type.getFullyQualifiedName().get()), + new NodeList<>(generic.clone())), + "visitor"); accept.getBody().get() .addStatement("return visitor.visit(this);"); } catch (Exception e) { @@ -60,7 +64,8 @@ public static void createVisitor(List nodeUnits, SourceRoot sou var s = StaticJavaParser.parseBlock("{return defaultVisit(n);}"); var visitorWithDefaults = cu.clone(); - visitorWithDefaults.setStorage(ROOT.resolve("org/key_project/java/ast/visitor/VisitorWithDefaults.java")); + visitorWithDefaults.setStorage( + ROOT.resolve("org/key_project/java/ast/visitor/VisitorWithDefaults.java")); final var vwdef = visitorWithDefaults.getType(0); vwdef.setName("VisitorWithDefaults"); for (var method : vwdef.getMethods()) { @@ -83,8 +88,10 @@ public static void createVoidVisitor(List nodeUnits, SourceRoot for (CompilationUnit clazz : nodeUnits) { try { var t = clazz.getPrimaryType().get(); - if (!(t instanceof ClassOrInterfaceDeclaration c)) continue; - if (c.isInterface()) continue; + if (!(t instanceof ClassOrInterfaceDeclaration c)) + continue; + if (c.isInterface()) + continue; var m = type.addMethod("visit"); m.addParameter(new ClassOrInterfaceType(null, t.getNameAsString()), "n"); @@ -92,8 +99,9 @@ public static void createVoidVisitor(List nodeUnits, SourceRoot var accept = t.addMethod("accept", PUBLIC); - accept.addParameter(new ClassOrInterfaceType(null, type.getFullyQualifiedName().get()), - "visitor"); + accept.addParameter( + new ClassOrInterfaceType(null, type.getFullyQualifiedName().get()), + "visitor"); accept.getBody().get().addStatement("visitor.visit(this);"); @@ -104,19 +112,22 @@ public static void createVoidVisitor(List nodeUnits, SourceRoot sourceRoot.add(cu); } - public static void createTraversalVisitor(List nodeUnits, SourceRoot sourceRoot) { + public static void createTraversalVisitor(List nodeUnits, + SourceRoot sourceRoot) { var cu = new CompilationUnit(); var type = createTypeAndSetDefaults(cu, "CopyVisitor", PUBLIC); type.getImplementedTypes().add( - (ClassOrInterfaceType) StaticJavaParser.parseType("Visitor")); + (ClassOrInterfaceType) StaticJavaParser.parseType("Visitor")); addAcceptMethods(type); for (CompilationUnit clazz : nodeUnits) { try { var t = clazz.getPrimaryType().get(); - if (!(t instanceof ClassOrInterfaceDeclaration c)) continue; - if (c.isInterface()) continue; + if (!(t instanceof ClassOrInterfaceDeclaration c)) + continue; + if (c.isInterface()) + continue; var m = type.addMethod("visit", PUBLIC); m.addParameter(new ClassOrInterfaceType(null, t.getNameAsString()), "n"); @@ -125,12 +136,11 @@ public static void createTraversalVisitor(List nodeUnits, Sourc body.addStatement("var b = n.builder();"); t.getFields() .stream().filter(NodeWithPrivateModifier::isPrivate) - .forEach(f -> - body.addStatement( - "b.%s = (%s) accept(n.%s());" - .formatted(f.getVariable(0).getNameAsExpression(), - f.getVariable(0).getTypeAsString(), - f.getVariable(0).getNameAsExpression()))); + .forEach(f -> body.addStatement( + "b.%s = (%s) accept(n.%s());" + .formatted(f.getVariable(0).getNameAsExpression(), + f.getVariable(0).getTypeAsString(), + f.getVariable(0).getNameAsExpression()))); body.addStatement("return b.build();"); m.setType(new ClassOrInterfaceType(null, t.getFullyQualifiedName().get())); } catch (Exception e) { @@ -140,12 +150,13 @@ public static void createTraversalVisitor(List nodeUnits, Sourc sourceRoot.add(cu); } - public static void createTraversalCopyOnDemandVisitor(List nodeUnits, SourceRoot sourceRoot) { + public static void createTraversalCopyOnDemandVisitor(List nodeUnits, + SourceRoot sourceRoot) { var cu = new CompilationUnit(); var type = createTypeAndSetDefaults(cu, "CopyOnWriteVisitor", PUBLIC); type.getImplementedTypes().add( - (ClassOrInterfaceType) StaticJavaParser.parseType("Visitor")); + (ClassOrInterfaceType) StaticJavaParser.parseType("Visitor")); addAcceptMethods(type); @@ -153,8 +164,10 @@ public static void createTraversalCopyOnDemandVisitor(List node try { var t = clazz.getPrimaryType().get(); - if (!(t instanceof ClassOrInterfaceDeclaration c)) continue; - if (c.isInterface()) continue; + if (!(t instanceof ClassOrInterfaceDeclaration c)) + continue; + if (c.isInterface()) + continue; var m = type.addMethod("visit", PUBLIC); m.addParameter(new ClassOrInterfaceType(null, t.getNameAsString()), "n"); @@ -165,22 +178,20 @@ public static void createTraversalCopyOnDemandVisitor(List node .stream() .filter(NodeWithPrivateModifier::isPrivate) .filter(PostSteps::isAstNode) - .forEach(f -> - body.addStatement( - "b.%s = (%s) accept(n.%s());" - .formatted(f.getVariable(0).getNameAsExpression(), - f.getVariable(0).getTypeAsString(), - f.getVariable(0).getNameAsExpression()))); + .forEach(f -> body.addStatement( + "b.%s = (%s) accept(n.%s());" + .formatted(f.getVariable(0).getNameAsExpression(), + f.getVariable(0).getTypeAsString(), + f.getVariable(0).getNameAsExpression()))); final var formatted = "boolean clean = %s;".formatted( - t.getFields().isEmpty() ? "false" : - t.getFields() - .stream().filter(NodeWithPrivateModifier::isPrivate) - .map(it -> { - final var n = it.getVariable(0).getNameAsString(); - return "(n.%s() == b.%s)".formatted(n, n); - }) - .collect(Collectors.joining("&&")) - ); + t.getFields().isEmpty() ? "false" + : t.getFields() + .stream().filter(NodeWithPrivateModifier::isPrivate) + .map(it -> { + final var n = it.getVariable(0).getNameAsString(); + return "(n.%s() == b.%s)".formatted(n, n); + }) + .collect(Collectors.joining("&&"))); body.addStatement(formatted); body.addStatement("return clean?n:b.build();"); m.setType(new ClassOrInterfaceType(null, t.getFullyQualifiedName().get())); @@ -214,7 +225,8 @@ private static boolean isAstNode(Type type) { c.toUnboxedType(); return false; } catch (UnsupportedOperationException e) { - return !(name.contains("Kind") || name.equals("PositionInfo") || name.equals("JMLModifiers")); + return !(name.contains("Kind") || name.equals("PositionInfo") + || name.equals("JMLModifiers")); } } return false; @@ -223,10 +235,10 @@ private static boolean isAstNode(Type type) { /// /// ```java /// T accept(T n) { - /// return n != null ? n.accept(this) : null; + /// return n != null ? n.accept(this) : null; /// } /// RoList accept(RoList n) { - /// return n != null ? n.stream().map(it -> (T) it.accept(this)).toList() : null; + /// return n != null ? n.stream().map(it -> (T) it.accept(this)).toList() : null; /// } /// ``` private static void addAcceptMethods(ClassOrInterfaceDeclaration type) { @@ -246,7 +258,8 @@ private static void addAcceptMethods(ClassOrInterfaceDeclaration type) { acceptList.addTypeParameter(t.clone()); acceptList.addParameter(StaticJavaParser.parseType("RoList"), "n"); acceptList.setType("RoList"); - acceptList.getBody().get().addStatement("return n != null ? n.stream().map(it -> (T) it.accept(this)).collect(RoList.collector()) : null;"); + acceptList.getBody().get().addStatement( + "return n != null ? n.stream().map(it -> (T) it.accept(this)).collect(RoList.collector()) : null;"); } { @@ -258,7 +271,8 @@ private static void addAcceptMethods(ClassOrInterfaceDeclaration type) { } } - private static ClassOrInterfaceDeclaration createTypeAndSetDefaults(CompilationUnit cu, String typeName, Modifier.DefaultKeyword... mods) { + private static ClassOrInterfaceDeclaration createTypeAndSetDefaults(CompilationUnit cu, + String typeName, Modifier.DefaultKeyword... mods) { String name = "org.key_project.java.ast.visitor"; cu.setPackageDeclaration(name); cu.addImport("org.key_project.java.ast.visitor.*"); @@ -283,8 +297,10 @@ public static void createArgVisitor(List nodeUnits, SourceRoot for (CompilationUnit clazz : nodeUnits) { try { var t = clazz.getPrimaryType().get(); - if (!(t instanceof ClassOrInterfaceDeclaration c)) continue; - if (c.isInterface()) continue; + if (!(t instanceof ClassOrInterfaceDeclaration c)) + continue; + if (c.isInterface()) + continue; cu.addImport(t.getFullyQualifiedName().get()); @@ -298,9 +314,11 @@ public static void createArgVisitor(List nodeUnits, SourceRoot accept.setType(generic.clone()); accept.getTypeParameters().add(generic.clone()); accept.getTypeParameters().add(argType.clone()); - accept.addParameter(new ClassOrInterfaceType(null, new SimpleName(type.getFullyQualifiedName().get()), - new NodeList<>(generic.clone(), argType.clone())), - "visitor"); + accept.addParameter( + new ClassOrInterfaceType(null, + new SimpleName(type.getFullyQualifiedName().get()), + new NodeList<>(generic.clone(), argType.clone())), + "visitor"); accept.addParameter(argType.clone(), "arg"); accept.getBody().get() .addStatement("return visitor.visit(this,arg);"); @@ -312,7 +330,8 @@ public static void createArgVisitor(List nodeUnits, SourceRoot } - public static void createDeepCopyVisitor(List nodeUnits, SourceRoot sourceRoot) { + public static void createDeepCopyVisitor(List nodeUnits, + SourceRoot sourceRoot) { } diff --git a/key.ncore.java/src/generator/java/org/key_project/ncore/java/PreSteps.java b/key.ncore.java/src/generator/java/org/key_project/ncore/java/PreSteps.java index 9099d1f3042..97daf7898ed 100644 --- a/key.ncore.java/src/generator/java/org/key_project/ncore/java/PreSteps.java +++ b/key.ncore.java/src/generator/java/org/key_project/ncore/java/PreSteps.java @@ -1,5 +1,11 @@ +/* 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 org.key_project.ncore.java; +import java.util.ArrayList; +import java.util.TreeMap; + import com.github.javaparser.ast.NodeList; import com.github.javaparser.ast.body.ClassOrInterfaceDeclaration; import com.github.javaparser.ast.body.FieldDeclaration; @@ -8,15 +14,14 @@ import com.google.common.collect.Multimap; import com.google.common.collect.MultimapBuilder; -import java.util.ArrayList; -import java.util.TreeMap; - import static com.github.javaparser.ast.Modifier.DefaultKeyword.ABSTRACT; public class PreSteps { final static class PreComputation implements PreStep { - Multimap inheritanceMap = MultimapBuilder.treeKeys().treeSetValues().build(); - Multimap permittedTypes = MultimapBuilder.treeKeys().treeSetValues().build(); + Multimap inheritanceMap = + MultimapBuilder.treeKeys().treeSetValues().build(); + Multimap permittedTypes = + MultimapBuilder.treeKeys().treeSetValues().build(); @Override public void applyOn(NodeList> types) { @@ -37,7 +42,8 @@ public void applyOn(NodeList> types) { for (var clazz : inheritanceMap.keySet()) { final var strings = new ArrayList<>(inheritanceMap.get(clazz)); for (var zuper : strings) { - changed = changed || inheritanceMap.putAll(clazz, inheritanceMap.get(zuper)); + changed = + changed || inheritanceMap.putAll(clazz, inheritanceMap.get(zuper)); } } } diff --git a/key.ncore.java/src/main/java/org/key_project/java/ast/AssignmentKind.java b/key.ncore.java/src/main/java/org/key_project/java/ast/AssignmentKind.java index bcac500f06e..333ea814449 100644 --- a/key.ncore.java/src/main/java/org/key_project/java/ast/AssignmentKind.java +++ b/key.ncore.java/src/main/java/org/key_project/java/ast/AssignmentKind.java @@ -1,22 +1,25 @@ +/* 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 org.key_project.java.ast; public enum AssignmentKind { - Copy(""), - BinaryOr("|"), - Divide("/"), - ShiftLeft("<<"), - UnsignedShiftRight(">>>"), - Plus("+"), - ShiftRight(">>"), - Minus("-"), - Modulo("%"), - Times("*"), - BinaryAnd("&"), - BinaryXOr("^"); + Copy(""), + BinaryOr("|"), + Divide("/"), + ShiftLeft("<<"), + UnsignedShiftRight(">>>"), + Plus("+"), + ShiftRight(">>"), + Minus("-"), + Modulo("%"), + Times("*"), + BinaryAnd("&"), + BinaryXOr("^"); - public final String symbol; + public final String symbol; - AssignmentKind(String symbol) { - this.symbol = symbol; - } + AssignmentKind(String symbol) { + this.symbol = symbol; } +} diff --git a/key.ncore.java/src/main/java/org/key_project/java/ast/BinaryOperatorKind.java b/key.ncore.java/src/main/java/org/key_project/java/ast/BinaryOperatorKind.java index 1127a948521..c35471eafb8 100644 --- a/key.ncore.java/src/main/java/org/key_project/java/ast/BinaryOperatorKind.java +++ b/key.ncore.java/src/main/java/org/key_project/java/ast/BinaryOperatorKind.java @@ -1,3 +1,6 @@ +/* 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 org.key_project.java.ast; public enum BinaryOperatorKind { diff --git a/key.ncore.java/src/main/java/org/key_project/java/ast/EqEx.java b/key.ncore.java/src/main/java/org/key_project/java/ast/EqEx.java index ce5fd804282..b2994df22b7 100644 --- a/key.ncore.java/src/main/java/org/key_project/java/ast/EqEx.java +++ b/key.ncore.java/src/main/java/org/key_project/java/ast/EqEx.java @@ -1,3 +1,6 @@ +/* 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 org.key_project.java.ast; @@ -8,6 +11,6 @@ /// Exclude a field from equality and hashCode. @Retention(RetentionPolicy.SOURCE) -@Target({ElementType.PARAMETER, ElementType.FIELD}) +@Target({ ElementType.PARAMETER, ElementType.FIELD }) public @interface EqEx { } diff --git a/key.ncore.java/src/main/java/org/key_project/java/ast/LogicFunction.java b/key.ncore.java/src/main/java/org/key_project/java/ast/LogicFunction.java index 8f6ae183565..f2310f32b8e 100644 --- a/key.ncore.java/src/main/java/org/key_project/java/ast/LogicFunction.java +++ b/key.ncore.java/src/main/java/org/key_project/java/ast/LogicFunction.java @@ -1,31 +1,34 @@ +/* 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 org.key_project.java.ast; public enum LogicFunction { - Intersect(2, 1, PrimitiveType.JAVA_LOCSET, AsFunction("\\intersect")), - SetUnion(2, 1, PrimitiveType.JAVA_LOCSET, AsFunction("\\set_union")), - SetMinus(2, 1, PrimitiveType.JAVA_LOCSET, AsFunction("\\set_minus")), - AllObjects(1, 1, PrimitiveType.JAVA_LOCSET, AsFunction("\\all_objects")), - SeqPut(3, 1, PrimitiveType.JAVA_SEQ, AsFunction("\\seq_upd")), - SeqGet(1, 1, PrimitiveType.JAVA_INT, AsArrayAccess()), - SeqReverse(1, 1, PrimitiveType.JAVA_SEQ, AsFunction("\\seq_reverse")), - AllFields(1, 1, PrimitiveType.JAVA_LOCSET, AsFunction("\\all_fields")), - SeqIndexOf(2, 1, PrimitiveType.JAVA_INT, AsFunction("\\indexOf")), - SeqSingleton(1, 1, PrimitiveType.JAVA_SEQ, AsFunction("\\seq_singleton")), - SeqSub(3, 1, PrimitiveType.JAVA_SEQ, AsFunction("\\seq_sub")), - SeqConcat(2, 1, PrimitiveType.JAVA_SEQ, AsFunction("\\seq_concat")), - Singleton(1, 1, PrimitiveType.JAVA_LOCSET, AsFunction("\\singleton")), - SeqLength(1, 1, PrimitiveType.JAVA_INT, AsSuffix("length")); + Intersect(2, 1, PrimitiveType.JAVA_LOCSET, AsFunction("\\intersect")), + SetUnion(2, 1, PrimitiveType.JAVA_LOCSET, AsFunction("\\set_union")), + SetMinus(2, 1, PrimitiveType.JAVA_LOCSET, AsFunction("\\set_minus")), + AllObjects(1, 1, PrimitiveType.JAVA_LOCSET, AsFunction("\\all_objects")), + SeqPut(3, 1, PrimitiveType.JAVA_SEQ, AsFunction("\\seq_upd")), + SeqGet(1, 1, PrimitiveType.JAVA_INT, AsArrayAccess()), + SeqReverse(1, 1, PrimitiveType.JAVA_SEQ, AsFunction("\\seq_reverse")), + AllFields(1, 1, PrimitiveType.JAVA_LOCSET, AsFunction("\\all_fields")), + SeqIndexOf(2, 1, PrimitiveType.JAVA_INT, AsFunction("\\indexOf")), + SeqSingleton(1, 1, PrimitiveType.JAVA_SEQ, AsFunction("\\seq_singleton")), + SeqSub(3, 1, PrimitiveType.JAVA_SEQ, AsFunction("\\seq_sub")), + SeqConcat(2, 1, PrimitiveType.JAVA_SEQ, AsFunction("\\seq_concat")), + Singleton(1, 1, PrimitiveType.JAVA_LOCSET, AsFunction("\\singleton")), + SeqLength(1, 1, PrimitiveType.JAVA_INT, AsSuffix("length")); - public final int arity; - public final int precedence; - public final PrimitiveType returnType; - public final PrettyPrinter.PrintOp format; + public final int arity; + public final int precedence; + public final PrimitiveType returnType; + public final PrettyPrinter.PrintOp format; - LogicFunction(int arity, int precedence, PrimitiveType returnType, - PrettyPrinter.PrintOp format) { - this.arity = arity; - this.precedence = precedence; - this.returnType = returnType; - this.format = format; - } + LogicFunction(int arity, int precedence, PrimitiveType returnType, + PrettyPrinter.PrintOp format) { + this.arity = arity; + this.precedence = precedence; + this.returnType = returnType; + this.format = format; } +} diff --git a/key.ncore.java/src/main/java/org/key_project/java/ast/Package.java b/key.ncore.java/src/main/java/org/key_project/java/ast/Package.java index be1b2fad55d..3749f947489 100644 --- a/key.ncore.java/src/main/java/org/key_project/java/ast/Package.java +++ b/key.ncore.java/src/main/java/org/key_project/java/ast/Package.java @@ -1,3 +1,6 @@ +/* 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 org.key_project.java.ast; import java.lang.annotation.ElementType; @@ -7,7 +10,7 @@ /// Sets the suffix of the package with respect to `org.key_project.java.ast` @Retention(RetentionPolicy.SOURCE) -@Target({ElementType.TYPE}) +@Target({ ElementType.TYPE }) public @interface Package { String value() default ""; } diff --git a/key.ncore.java/src/main/java/org/key_project/java/ast/Root.java b/key.ncore.java/src/main/java/org/key_project/java/ast/Root.java index 85d775b6a10..cfec916d195 100644 --- a/key.ncore.java/src/main/java/org/key_project/java/ast/Root.java +++ b/key.ncore.java/src/main/java/org/key_project/java/ast/Root.java @@ -1,3 +1,6 @@ +/* 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 org.key_project.java.ast; @@ -8,6 +11,6 @@ /// Marks the ROOT class of the hierarchy @Retention(RetentionPolicy.SOURCE) -@Target({ElementType.TYPE}) +@Target({ ElementType.TYPE }) public @interface Root { } diff --git a/key.ncore.java/src/main/java/org/key_project/java/ast/UnaryOperatorKind.java b/key.ncore.java/src/main/java/org/key_project/java/ast/UnaryOperatorKind.java index 981cc4334ca..71f9f869cec 100644 --- a/key.ncore.java/src/main/java/org/key_project/java/ast/UnaryOperatorKind.java +++ b/key.ncore.java/src/main/java/org/key_project/java/ast/UnaryOperatorKind.java @@ -1,28 +1,31 @@ +/* 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 org.key_project.java.ast; public enum UnaryOperatorKind { - LOGICAL_NOT("!", 1), - NEGATIVE("-", 1), - POSITIVE("+", 1), - BINARY_NOT("~", 1), + LOGICAL_NOT("!", 1), + NEGATIVE("-", 1), + POSITIVE("+", 1), + BINARY_NOT("~", 1), - PRE_INCREMENT("++", 0), - PRE_DECREMENT("--", 0), - POST_INCREMENT("++", 0, POSTFIX), - POST_DECREMENT("--", 0, POSTFIX); + PRE_INCREMENT("++", 0), + PRE_DECREMENT("--", 0), + POST_INCREMENT("++", 0, POSTFIX), + POST_DECREMENT("--", 0, POSTFIX); - public final String symbol; - public final int precedence; - public final int notation; + public final String symbol; + public final int precedence; + public final int notation; - UnaryOperatorKind(String symbol, int precedence) { - this(symbol, precedence, PREFIX); - } + UnaryOperatorKind(String symbol, int precedence) { + this(symbol, precedence, PREFIX); + } - UnaryOperatorKind(String symbol, int precedence, int notation) { - this.symbol = symbol; - this.notation = notation; - this.precedence = precedence; - } + UnaryOperatorKind(String symbol, int precedence, int notation) { + this.symbol = symbol; + this.notation = notation; + this.precedence = precedence; } +} diff --git a/key.ncore.java/src/main/java/org/key_project/java/ast/Visitable.java b/key.ncore.java/src/main/java/org/key_project/java/ast/Visitable.java index a79c35fd532..6b4ee339d3a 100644 --- a/key.ncore.java/src/main/java/org/key_project/java/ast/Visitable.java +++ b/key.ncore.java/src/main/java/org/key_project/java/ast/Visitable.java @@ -1,3 +1,6 @@ +/* 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 org.key_project.java.ast; import org.key_project.java.ast.visitor.*; diff --git a/key.util/src/main/java/org/key_project/util/collection/RoList.java b/key.util/src/main/java/org/key_project/util/collection/RoList.java index 14ed7069be9..adc6f129057 100644 --- a/key.util/src/main/java/org/key_project/util/collection/RoList.java +++ b/key.util/src/main/java/org/key_project/util/collection/RoList.java @@ -1,7 +1,8 @@ +/* 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 org.key_project.util.collection; -import org.jspecify.annotations.Nullable; - import java.util.*; import java.util.function.BiConsumer; import java.util.function.BinaryOperator; @@ -10,6 +11,8 @@ import java.util.stream.Collector; import java.util.stream.Stream; +import org.jspecify.annotations.Nullable; + /** * * @author Alexander Weigl @@ -101,11 +104,11 @@ public Set characteristics() { } static RoList fromList(List a) { - if(a.isEmpty()) { + if (a.isEmpty()) { return RoList.empty(); - }else if(a.size()==1){ + } else if (a.size() == 1) { return RoList.singleton(a.getFirst()); - }else{ + } else { return new ImmutableArray<>(a); } } @@ -119,16 +122,21 @@ static RoList empty() { } int size(); + E get(int index); boolean isEmpty(); + default boolean isNonEmpty() { return !isEmpty(); } boolean contains(Object e); + Iterator iterator(); + E getFirst(); + E getLast(); Stream stream(); From 58f4a43f278c03dbbefeb23c66df3e05b3ed452d Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sun, 19 Apr 2026 21:06:47 +0200 Subject: [PATCH 7/7] missing --- .../util/collection/SingletonRoList.java | 75 +++++++++++++++++++ 1 file changed, 75 insertions(+) create mode 100644 key.util/src/main/java/org/key_project/util/collection/SingletonRoList.java diff --git a/key.util/src/main/java/org/key_project/util/collection/SingletonRoList.java b/key.util/src/main/java/org/key_project/util/collection/SingletonRoList.java new file mode 100644 index 00000000000..b42b35f0c3d --- /dev/null +++ b/key.util/src/main/java/org/key_project/util/collection/SingletonRoList.java @@ -0,0 +1,75 @@ +/* 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 org.key_project.util.collection; + +import java.util.Iterator; +import java.util.NoSuchElementException; +import java.util.Objects; +import java.util.stream.Stream; + +/** + * + * @author Alexander Weigl + * @version 1 (4/19/26) + */ +public record SingletonRoList(T item) implements RoList { + @Override + public int size() { + return 1; + } + + @Override + public T get(int index) { + if (index == 0) { + return item(); + } + throw new IndexOutOfBoundsException(); + } + + @Override + public boolean isEmpty() { + return false; + } + + @Override + public boolean contains(Object e) { + return Objects.equals(e, item); + } + + @Override + public Iterator iterator() { + return new Iterator<>() { + private boolean called; + + @Override + public boolean hasNext() { + return !called; + } + + @Override + public T next() { + if (called) { + throw new NoSuchElementException(); + } + called = true; + return item; + } + }; + } + + @Override + public T getFirst() { + return item; + } + + @Override + public T getLast() { + return item; + } + + @Override + public Stream stream() { + return Stream.of(item); + } +}