Clean up the Java AST: Avoid sub-classes in favor of Enum

key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/impl/InformationFlowContractImpl.java

@@ -11,7 +11,7 @@
 import de.uka.ilkd.key.informationflow.po.InfFlowContractPO;
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType;
-import de.uka.ilkd.key.java.ast.declaration.modifier.VisibilityModifier;
+import de.uka.ilkd.key.java.ast.declaration.Modifier;
 import de.uka.ilkd.key.logic.JTerm;
 import de.uka.ilkd.key.logic.op.IObserverFunction;
 import de.uka.ilkd.key.logic.op.IProgramMethod;
@@ -431,7 +431,7 @@ public String getPODisplayName() {
 
 
     @Override
-    public VisibilityModifier getVisibility() {
+    public Modifier.ModifierKind getVisibility() {
         assert false; // this is currently not applicable for contracts
         return null;
     }

key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicLoopExecutionSnippet.java

@@ -9,7 +9,6 @@
 import de.uka.ilkd.key.java.ast.Statement;
 import de.uka.ilkd.key.java.ast.StatementBlock;
 import de.uka.ilkd.key.java.ast.expression.Assignment;
-import de.uka.ilkd.key.java.ast.expression.operator.CopyAssignment;
 import de.uka.ilkd.key.java.ast.reference.ExecutionContext;
 import de.uka.ilkd.key.java.ast.statement.MethodFrame;
 import de.uka.ilkd.key.logic.JTerm;
@@ -23,6 +22,8 @@
 import org.key_project.util.collection.ImmutableSLList;
 import org.key_project.util.collection.Pair;
 
+import static de.uka.ilkd.key.java.ast.expression.Assignment.AssignmentKind.Copy;
+
 public class BasicLoopExecutionSnippet extends ReplaceAndRegisterMethod implements FactoryMethod {
 
     @Override
@@ -102,8 +103,9 @@ private Pair<JavaBlock, JavaBlock> buildJavaBlock(BasicSnippetData d) {
         LoopSpecification inv = (LoopSpecification) d.get(BasicSnippetData.Key.LOOP_INVARIANT);
         StatementBlock sb = (StatementBlock) inv.getLoop().getBody();
 
-        final Assignment guardVarDecl = new CopyAssignment((LocationVariable) d.origVars.guard.op(),
-            inv.getLoop().getGuardExpression());
+        final Assignment guardVarDecl =
+            new Assignment(Copy, (LocationVariable) d.origVars.guard.op(),
+                inv.getLoop().getGuardExpression());
         final Statement guardVarMethodFrame = context == null ? guardVarDecl
                 : new MethodFrame(null, context, new StatementBlock(guardVarDecl));
 

key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicSymbolicExecutionSnippet.java

@@ -12,9 +12,9 @@
 import de.uka.ilkd.key.java.ast.declaration.Modifier;
 import de.uka.ilkd.key.java.ast.declaration.ParameterDeclaration;
 import de.uka.ilkd.key.java.ast.declaration.VariableSpecification;
+import de.uka.ilkd.key.java.ast.expression.Assignment;
 import de.uka.ilkd.key.java.ast.expression.Expression;
 import de.uka.ilkd.key.java.ast.expression.literal.NullLiteral;
-import de.uka.ilkd.key.java.ast.expression.operator.CopyAssignment;
 import de.uka.ilkd.key.java.ast.expression.operator.New;
 import de.uka.ilkd.key.java.ast.reference.TypeRef;
 import de.uka.ilkd.key.java.ast.reference.TypeReference;
@@ -124,7 +124,7 @@ private JavaBlock buildJavaBlock(BasicSnippetData d, ImmutableList<JTerm> formal
                 formalArray.toArray(new Expression[formalArray.size()]);
             KeYJavaType forClass = (KeYJavaType) d.get(BasicSnippetData.Key.FOR_CLASS);
             final New n = new New(formalArray2, new TypeRef(forClass), null);
-            final CopyAssignment ca = new CopyAssignment(selfVar, n);
+            final Assignment ca = new Assignment(selfVar, n);
             sb = new StatementBlock(ca);
         } else {
             final MethodBodyStatement call =
@@ -137,19 +137,17 @@ private JavaBlock buildJavaBlock(BasicSnippetData d, ImmutableList<JTerm> formal
         final TypeReference excTypeRef = javaInfo.createTypeReference(eType);
 
         // create try statement
-        final CopyAssignment nullStat = new CopyAssignment(exceptionVar, NullLiteral.NULL);
+        final Assignment nullStat = new Assignment(exceptionVar, NullLiteral.NULL);
         final VariableSpecification eSpec = new VariableSpecification(eVar);
         final ParameterDeclaration excDecl =
             new ParameterDeclaration(new Modifier[0], excTypeRef, eSpec, false);
-        final CopyAssignment assignStat = new CopyAssignment(exceptionVar, eVar);
+        final Assignment assignStat = new Assignment(exceptionVar, eVar);
         final Catch catchStat = new Catch(excDecl, new StatementBlock(assignStat));
         final Try tryStat = new Try(sb, new Branch[] { catchStat });
         final StatementBlock sb2 = new StatementBlock(nullStat, tryStat);
 
         // create java block
-        JavaBlock result = JavaBlock.createJavaBlock(sb2);
-
-        return result;
+        return JavaBlock.createJavaBlock(sb2);
     }
 
 

key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/ProgramVariableReferencesAnalyst.java

@@ -9,7 +9,7 @@
 import de.uka.ilkd.key.java.ast.ExpressionContainer;
 import de.uka.ilkd.key.java.ast.ProgramElement;
 import de.uka.ilkd.key.java.ast.SourceElement;
-import de.uka.ilkd.key.java.ast.expression.operator.CopyAssignment;
+import de.uka.ilkd.key.java.ast.expression.Assignment;
 import de.uka.ilkd.key.java.ast.reference.FieldReference;
 import de.uka.ilkd.key.java.ast.reference.ReferencePrefix;
 import de.uka.ilkd.key.java.ast.statement.If;
@@ -20,6 +20,8 @@
 import de.uka.ilkd.key.proof_references.reference.DefaultProofReference;
 import de.uka.ilkd.key.proof_references.reference.IProofReference;
 
+import static de.uka.ilkd.key.java.ast.expression.Assignment.AssignmentKind.Copy;
+
 /**
  * Extracts read and write access to fields ({@link IProgramVariable}) via assignments.
  *
@@ -33,9 +35,9 @@ public class ProgramVariableReferencesAnalyst implements IProofReferencesAnalyst
     public LinkedHashSet<IProofReference<?>> computeReferences(Node node, Services services) {
         if (node.getAppliedRuleApp() != null && node.getNodeInfo() != null) {
             SourceElement statement = node.getNodeInfo().getActiveStatement();
-            if (statement instanceof CopyAssignment) {
+            if (statement instanceof Assignment a && a.getKind() == Copy) {
                 LinkedHashSet<IProofReference<?>> result = new LinkedHashSet<>();
-                listReferences(node, (CopyAssignment) statement,
+                listReferences(node, a,
                     services.getJavaInfo().getArrayLength(), result, true);
                 return result;
             } else if (statement instanceof If) {
@@ -66,7 +68,7 @@ protected void listReferences(Node node, ProgramElement pe, ProgramVariable arra
             if (pv.isMember()) {
                 DefaultProofReference<ProgramVariable> reference =
                     new DefaultProofReference<>(IProofReference.ACCESS, node,
-                        (ProgramVariable) pe);
+                        pv);
                 ProofReferenceUtil.merge(toFill, reference);
             }
         } else if (pe instanceof FieldReference fr) {

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionOperationContract.java

@@ -11,7 +11,7 @@
 import de.uka.ilkd.key.java.ast.ProgramElement;
 import de.uka.ilkd.key.java.ast.SourceElement;
 import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType;
-import de.uka.ilkd.key.java.ast.expression.operator.CopyAssignment;
+import de.uka.ilkd.key.java.ast.expression.Assignment;
 import de.uka.ilkd.key.java.ast.statement.MethodFrame;
 import de.uka.ilkd.key.logic.JTerm;
 import de.uka.ilkd.key.logic.TermBuilder;
@@ -305,7 +305,7 @@ protected static LocationVariable extractResultVariableFromPostBranch(Node node,
         postModality = TermBuilder.goBelowUpdates(postModality);
         MethodFrame mf = JavaTools.getInnermostMethodFrame(postModality.javaBlock(), services);
         SourceElement firstElement = NodeInfo.computeActiveStatement(mf.getFirstElement());
-        if (!(firstElement instanceof CopyAssignment assignment)) {
+        if (!(firstElement instanceof Assignment assignment)) {
             return null;
         }
         ProgramElement rightChild = assignment.getChildAt(1);

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/AbstractBackwardSlicer.java

@@ -14,8 +14,8 @@
 import de.uka.ilkd.key.java.ast.NonTerminalProgramElement;
 import de.uka.ilkd.key.java.ast.ProgramElement;
 import de.uka.ilkd.key.java.ast.SourceElement;
+import de.uka.ilkd.key.java.ast.expression.Assignment;
 import de.uka.ilkd.key.java.ast.expression.Expression;
-import de.uka.ilkd.key.java.ast.expression.operator.CopyAssignment;
 import de.uka.ilkd.key.java.ast.reference.ReferencePrefix;
 import de.uka.ilkd.key.java.ast.reference.ThisReference;
 import de.uka.ilkd.key.proof.Node;
@@ -64,9 +64,8 @@ public ImmutableArray<Node> doSlicing(Node seedNode, Location seedLocation,
                     if (oldAliases != null) {
                         try {
                             // Update relevant locations if required
-                            if (activeStatement instanceof CopyAssignment) {
-                                SourceElement originalTarget =
-                                    ((CopyAssignment) activeStatement).getArguments().get(0);
+                            if (activeStatement instanceof Assignment a) {
+                                SourceElement originalTarget = a.getArguments().get(0);
                                 ReferencePrefix relevantTarget = toReferencePrefix(originalTarget);
                                 Location normalizedPrefix =
                                     normalizeAlias(services, relevantTarget, info);

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/ThinBackwardSlicer.java

@@ -9,8 +9,8 @@
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.java.ast.SourceElement;
+import de.uka.ilkd.key.java.ast.expression.Assignment;
 import de.uka.ilkd.key.java.ast.expression.Expression;
-import de.uka.ilkd.key.java.ast.expression.operator.CopyAssignment;
 import de.uka.ilkd.key.java.ast.reference.ReferencePrefix;
 import de.uka.ilkd.key.java.ast.statement.MethodBodyStatement;
 import de.uka.ilkd.key.logic.JTerm;
@@ -38,7 +38,7 @@ protected boolean accept(Node node, Node previousChild, Services services,
             throws ProofInputException {
         try {
             boolean accept = false;
-            if (activeStatement instanceof CopyAssignment copyAssignment) {
+            if (activeStatement instanceof Assignment copyAssignment) {
                 ImmutableArray<Expression> arguments = copyAssignment.getArguments();
                 if (arguments.size() >= 1) {
                     SourceElement originalTarget = arguments.get(0);

key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/slicing/TestThinBackwardSlicer.java

@@ -10,7 +10,7 @@
 import de.uka.ilkd.key.java.ast.SourceElement;
 import de.uka.ilkd.key.java.ast.declaration.VariableDeclaration;
 import de.uka.ilkd.key.java.ast.declaration.VariableSpecification;
-import de.uka.ilkd.key.java.ast.expression.operator.CopyAssignment;
+import de.uka.ilkd.key.java.ast.expression.Assignment;
 import de.uka.ilkd.key.java.ast.reference.ReferencePrefix;
 import de.uka.ilkd.key.java.ast.statement.Return;
 import de.uka.ilkd.key.proof.Node;
@@ -781,8 +781,8 @@ public Pair<Node, ReferencePrefix> findSeed(Proof proof) {
             Assertions.assertNotNull(seedNode);
             // Get seed location
             SourceElement activeStatemt = seedNode.getNodeInfo().getActiveStatement();
-            Assertions.assertInstanceOf(CopyAssignment.class, activeStatemt);
-            CopyAssignment assignment = (CopyAssignment) activeStatemt;
+            Assertions.assertInstanceOf(Assignment.class, activeStatemt);
+            Assignment assignment = (Assignment) activeStatemt;
             SourceElement seedLocation = assignment.getChildAt(1);
             return new Pair<>(seedNode, (ReferencePrefix) seedLocation);
         }
@@ -818,8 +818,8 @@ public Pair<Node, ReferencePrefix> findSeed(Proof proof) {
             Assertions.assertNotNull(seedNode);
             // Get seed location
             SourceElement activeStatemt = seedNode.getNodeInfo().getActiveStatement();
-            Assertions.assertInstanceOf(CopyAssignment.class, activeStatemt);
-            CopyAssignment assignment = (CopyAssignment) activeStatemt;
+            Assertions.assertInstanceOf(Assignment.class, activeStatemt);
+            Assignment assignment = (Assignment) activeStatemt;
             SourceElement seedLocation = assignment.getChildAt(0);
             return new Pair<>(seedNode, (ReferencePrefix) seedLocation);
         }

key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestgenFacade.java

@@ -6,6 +6,7 @@
 import java.io.IOException;
 import java.util.Collection;
 import java.util.List;
+import java.util.NoSuchElementException;
 import java.util.concurrent.Callable;
 
 import de.uka.ilkd.key.control.KeYEnvironment;
@@ -66,7 +67,7 @@ public void launcherStopped(SolverLauncher launcher,
 
                     tg.generateJUnitTestSuite(finishedSolvers);
                     reporter.writeln("Compile the generated files using a Java compiler.");
-                } catch (IOException e) {
+                } catch (NoSuchElementException | IOException e) {
                     reporter.reportException(e);
                 }
             }

key.core.wd/src/main/java/de/uka/ilkd/key/wd/BlockWellDefinedness.java

@@ -7,7 +7,7 @@
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType;
-import de.uka.ilkd.key.java.ast.declaration.modifier.VisibilityModifier;
+import de.uka.ilkd.key.java.ast.declaration.Modifier;
 import de.uka.ilkd.key.logic.JTerm;
 import de.uka.ilkd.key.logic.TermBuilder;
 import de.uka.ilkd.key.logic.TermServices;
@@ -109,7 +109,7 @@ public String getTypeName() {
     }
 
     @Override
-    public VisibilityModifier getVisibility() {
+    public Modifier.ModifierKind getVisibility() {
         return block.getVisibility();
     }
 

key.core.wd/src/main/java/de/uka/ilkd/key/wd/ClassWellDefinedness.java

@@ -7,7 +7,7 @@
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType;
-import de.uka.ilkd.key.java.ast.declaration.modifier.VisibilityModifier;
+import de.uka.ilkd.key.java.ast.declaration.Modifier;
 import de.uka.ilkd.key.logic.JTerm;
 import de.uka.ilkd.key.logic.TermBuilder;
 import de.uka.ilkd.key.logic.TermServices;
@@ -155,7 +155,7 @@ public String getTypeName() {
     }
 
     @Override
-    public VisibilityModifier getVisibility() {
+    public Modifier.ModifierKind getVisibility() {
         return inv.getVisibility();
     }
 

key.core.wd/src/main/java/de/uka/ilkd/key/wd/LoopWellDefinedness.java

@@ -7,7 +7,7 @@
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType;
-import de.uka.ilkd.key.java.ast.declaration.modifier.VisibilityModifier;
+import de.uka.ilkd.key.java.ast.declaration.Modifier;
 import de.uka.ilkd.key.logic.JTerm;
 import de.uka.ilkd.key.logic.TermBuilder;
 import de.uka.ilkd.key.logic.TermServices;
@@ -99,7 +99,7 @@ public String getTypeName() {
     }
 
     @Override
-    public VisibilityModifier getVisibility() {
+    public Modifier.ModifierKind getVisibility() {
         return inv.getVisibility();
     }
 

key.core.wd/src/main/java/de/uka/ilkd/key/wd/MethodWellDefinedness.java

@@ -9,7 +9,7 @@
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType;
-import de.uka.ilkd.key.java.ast.declaration.modifier.VisibilityModifier;
+import de.uka.ilkd.key.java.ast.declaration.Modifier;
 import de.uka.ilkd.key.logic.JTerm;
 import de.uka.ilkd.key.logic.TermBuilder;
 import de.uka.ilkd.key.logic.TermServices;
@@ -468,7 +468,7 @@ public String getTypeName() {
     }
 
     @Override
-    public VisibilityModifier getVisibility() {
+    public Modifier.ModifierKind getVisibility() {
         return contract.getVisibility();
     }
 

key.core.wd/src/main/java/de/uka/ilkd/key/wd/SpecificationRepositoryWD.java

@@ -10,7 +10,6 @@
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType;
-import de.uka.ilkd.key.java.ast.declaration.modifier.VisibilityModifier;
 import de.uka.ilkd.key.logic.JTerm;
 import de.uka.ilkd.key.logic.op.IObserverFunction;
 import de.uka.ilkd.key.logic.op.ProgramVariable;
@@ -363,7 +362,7 @@ public void addClassInvariant(ClassInvariant inv) {
         }
 
         // inherit non-private, non-static invariants
-        if (!inv.isStatic() && VisibilityModifier.allowsInheritance(inv.getVisibility())) {
+        if (!inv.isStatic() && inv.getVisibility().allowsInheritance()) {
             final ImmutableList<KeYJavaType> subs = services.getJavaInfo().getAllSubtypes(kjt);
             for (KeYJavaType sub : subs) {
                 ClassInvariant subInv = inv.setKJT(sub);

key.core/src/main/java/de/uka/ilkd/key/java/JavaInfo.java

@@ -8,7 +8,6 @@
 import de.uka.ilkd.key.java.ast.ProgramElement;
 import de.uka.ilkd.key.java.ast.abstraction.*;
 import de.uka.ilkd.key.java.ast.declaration.*;
-import de.uka.ilkd.key.java.ast.declaration.modifier.VisibilityModifier;
 import de.uka.ilkd.key.java.ast.expression.Expression;
 import de.uka.ilkd.key.java.ast.reference.ExecutionContext;
 import de.uka.ilkd.key.java.ast.reference.TypeRef;
@@ -35,6 +34,8 @@
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 
+import static de.uka.ilkd.key.java.ast.declaration.Modifier.ModifierKind.*;
+
 /**
  * an instance serves as representation of a Java model underlying a DL formula. This class provides
  * calls to access the elements of the Java model using the KeY data structures only. Implementation
@@ -377,14 +378,18 @@ public static boolean isVisibleTo(SpecificationElement ax, KeYJavaType visibleTo
         // TODO: package information not yet available
         // BUGFIX: package-private is understood as private (see bug #1268)
         final boolean visibleToPackage = false;
-        final VisibilityModifier visibility = ax.getVisibility();
-        if (VisibilityModifier.isPublic(visibility)) {
+        final Modifier.ModifierKind visibility = ax.getVisibility();
+        assert visibility != null && visibility.isVisibility();
+
+        if (PUBLIC == visibility) {
             return true;
         }
-        if (VisibilityModifier.allowsInheritance(visibility)) {
+
+        if (visibility.allowsInheritance()) {
             return visibleTo.getSort().extendsTrans(kjt.getSort()) || visibleToPackage;
         }
-        if (VisibilityModifier.isPackageVisible(visibility)) {
+
+        if (visibility == PROTECTED || visibility == JML_PACKAGE) {
             return visibleToPackage;
         } else {
             return kjt.equals(visibleTo);

key.core/src/main/java/de/uka/ilkd/key/java/JavaService.java

@@ -794,7 +794,7 @@ public JavaBlock readBlock(String block, JPContext context,
         }
         var f = JavaBlock
                 .createJavaBlock((StatementBlock) getConverter(allowSchemaJava).process(sb));
-        JavaLogger.print(block, f);
+        // JavaLogger.print(block, f);
         return f;
     }