matching of operators for assignments

Author: wadoon

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

@@ -22,7 +22,7 @@
 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;
+import static de.uka.ilkd.key.java.ast.expression.Assignment.AssignmentKind.COPY;
 
 public class BasicLoopExecutionSnippet extends ReplaceAndRegisterMethod implements FactoryMethod {
 
@@ -104,7 +104,7 @@ private Pair<JavaBlock, JavaBlock> buildJavaBlock(BasicSnippetData d) {
         StatementBlock sb = (StatementBlock) inv.getLoop().getBody();
 
         final Assignment guardVarDecl =
-            new Assignment(Copy, (LocationVariable) d.origVars.guard.op(),
+            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.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/ProgramVariableReferencesAnalyst.java

@@ -20,7 +20,7 @@
 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;
+import static de.uka.ilkd.key.java.ast.expression.Assignment.AssignmentKind.COPY;
 
 /**
  * Extracts read and write access to fields ({@link IProgramVariable}) via assignments.
@@ -35,7 +35,7 @@ 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 Assignment a && a.getKind() == Copy) {
+            if (statement instanceof Assignment a && a.getKind() == COPY) {
                 LinkedHashSet<IProofReference<?>> result = new LinkedHashSet<>();
                 listReferences(node, a,
                     services.getJavaInfo().getArrayLength(), result, true);

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

@@ -34,7 +34,7 @@
 
 import org.jspecify.annotations.Nullable;
 
-import static de.uka.ilkd.key.java.ast.expression.Assignment.AssignmentKind.Copy;
+import static de.uka.ilkd.key.java.ast.expression.Assignment.AssignmentKind.COPY;
 
 /**
  * The KeYASTFactory helps building KeY Java AST structures.
@@ -45,7 +45,7 @@ public abstract class KeYJavaASTFactory {
      * creates an assignment <code> lhs:=rhs </code>
      */
     public static Assignment assign(Expression lhs, Expression rhs) {
-        return new Assignment(Copy, lhs, rhs);
+        return new Assignment(COPY, lhs, rhs);
     }
 
     /**

key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/Assignment.java

@@ -9,17 +9,22 @@
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.java.ast.Comment;
 import de.uka.ilkd.key.java.ast.PositionInfo;
+import de.uka.ilkd.key.java.ast.ProgramElement;
+import de.uka.ilkd.key.java.ast.SourceData;
 import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType;
 import de.uka.ilkd.key.java.ast.expression.literal.BooleanLiteral;
+import de.uka.ilkd.key.java.ast.expression.operator.LogicFunctionalOperator;
 import de.uka.ilkd.key.java.ast.reference.ExecutionContext;
 import de.uka.ilkd.key.java.visitor.Visitor;
 
+import de.uka.ilkd.key.rule.MatchConditions;
+import org.jspecify.annotations.Nullable;
 import org.key_project.util.ExtList;
 import org.key_project.util.collection.ImmutableArray;
 
 import org.jspecify.annotations.NullMarked;
 
-import static de.uka.ilkd.key.java.ast.expression.Assignment.AssignmentKind.Copy;
+import static de.uka.ilkd.key.java.ast.expression.Assignment.AssignmentKind.COPY;
 
 
 /**
@@ -37,18 +42,18 @@ public AssignmentKind getKind() {
     }
 
     public enum AssignmentKind {
-        Copy(""),
-        BinaryOr("|"),
-        Divide("/"),
-        ShiftLeft("<<"),
-        UnsignedShiftRight(">>>"),
-        Plus("+"),
-        ShiftRight(">>"),
-        Minus("-"),
-        Modulo("%"),
-        Times("*"),
-        BinaryAnd("&"),
-        BinaryXOr("^");
+        COPY(""),
+        BINARY_OR("|"),
+        DIVIDE("/"),
+        SHIFT_LEFT("<<"),
+        UNSIGNED_SHIFT_RIGHT(">>>"),
+        PLUS("+"),
+        SHIFT_RIGHT(">>"),
+        MINUS("-"),
+        MODULO("%"),
+        TIMES("*"),
+        BINARY_AND("&"),
+        BINARY_XOR("^");
 
         public final String symbol;
 
@@ -85,7 +90,7 @@ public Assignment(AssignmentKind kind, Expression lhs, Expression rhs) {
     }
 
     public Assignment(Expression lhs, Expression rhs) {
-        this(Copy, lhs, rhs);
+        this(COPY, lhs, rhs);
     }
 
 
@@ -101,6 +106,17 @@ public boolean isLeftAssociative() {
     }
 
 
+    @Override
+    public @Nullable MatchConditions match(SourceData source, MatchConditions matchCond) {
+        final ProgramElement src = source.getSource();
+        if(src instanceof Assignment other) {
+            if (getKind().equals(other.getKind())) {
+                return super.match(source, matchCond);
+            }
+        }
+        return null;
+    }
+
     /**
      * retrieves the type of the assignment expression
      *

key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/LogicFunctionalOperator.java

@@ -20,6 +20,7 @@
 import de.uka.ilkd.key.pp.PrettyPrinter;
 
 import de.uka.ilkd.key.rule.MatchConditions;
+import org.jspecify.annotations.Nullable;
 import org.key_project.util.collection.ImmutableArray;
 
 import static de.uka.ilkd.key.pp.PrettyPrinter.*;
@@ -106,7 +107,7 @@ public KeYJavaType getKeYJavaType(Services javaServ, ExecutionContext ec) {
     }
 
     @Override
-    public MatchConditions match(SourceData source, MatchConditions matchCond) {
+    public @Nullable MatchConditions match(SourceData source, MatchConditions matchCond) {
         final ProgramElement src = source.getSource();
         if(src instanceof LogicFunctionalOperator other) {
             if (getFunction().equals(other.getFunction())) {

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

@@ -231,18 +231,18 @@ public Object visit(AssignExpr n, Void arg) {
         var pi = createPositionInfo(n);
         var c = createComments(n);
         var op = switch (n.getOperator()) {
-            case ASSIGN -> AssignmentKind.Copy;
-            case PLUS -> AssignmentKind.Plus;
-            case MINUS -> AssignmentKind.Minus;
-            case MULTIPLY -> AssignmentKind.Times;
-            case DIVIDE -> AssignmentKind.Divide;
-            case BINARY_AND -> AssignmentKind.BinaryAnd;
-            case BINARY_OR -> AssignmentKind.BinaryOr;
-            case XOR -> AssignmentKind.BinaryXOr;
-            case REMAINDER -> AssignmentKind.Modulo;
-            case LEFT_SHIFT -> AssignmentKind.ShiftLeft;
-            case SIGNED_RIGHT_SHIFT -> AssignmentKind.ShiftRight;
-            case UNSIGNED_RIGHT_SHIFT -> AssignmentKind.UnsignedShiftRight;
+            case ASSIGN -> AssignmentKind.COPY;
+            case PLUS -> AssignmentKind.PLUS;
+            case MINUS -> AssignmentKind.MINUS;
+            case MULTIPLY -> AssignmentKind.TIMES;
+            case DIVIDE -> AssignmentKind.DIVIDE;
+            case BINARY_AND -> AssignmentKind.BINARY_AND;
+            case BINARY_OR -> AssignmentKind.BINARY_OR;
+            case XOR -> AssignmentKind.BINARY_XOR;
+            case REMAINDER -> AssignmentKind.MODULO;
+            case LEFT_SHIFT -> AssignmentKind.SHIFT_LEFT;
+            case SIGNED_RIGHT_SHIFT -> AssignmentKind.SHIFT_RIGHT;
+            case UNSIGNED_RIGHT_SHIFT -> AssignmentKind.UNSIGNED_SHIFT_RIGHT;
         };
         return new Assignment(pi, c, op, target, expr);
     }

key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractOperationPO.java

@@ -42,7 +42,7 @@
 import com.github.javaparser.ast.key.KeyTransactionStatement;
 import org.jspecify.annotations.Nullable;
 
-import static de.uka.ilkd.key.java.ast.expression.Assignment.AssignmentKind.Copy;
+import static de.uka.ilkd.key.java.ast.expression.Assignment.AssignmentKind.COPY;
 
 /**
  * <p>
@@ -908,11 +908,11 @@ protected JavaBlock buildJavaBlock(ImmutableList<LocationVariable> formalParVars
             sb2 = tryBlock;
         } else {
             // create try statement
-            final Assignment nullStat = new Assignment(Copy, exceptionVar, NullLiteral.NULL);
+            final Assignment nullStat = new Assignment(COPY, exceptionVar, NullLiteral.NULL);
             final VariableSpecification eSpec = new VariableSpecification(eVar);
             final ParameterDeclaration excDecl =
                 new ParameterDeclaration(new Modifier[0], excTypeRef, eSpec, false);
-            final Assignment assignStat = new Assignment(Copy, exceptionVar, eVar);
+            final Assignment assignStat = new Assignment(COPY, exceptionVar, eVar);
             final Catch catchStat =
                 new Catch(excDecl, catchBlock == null ? new StatementBlock(assignStat)
                         : new StatementBlock(assignStat, catchBlock));

key.core/src/main/java/de/uka/ilkd/key/rule/ObserverToUpdateRule.java

@@ -11,14 +11,12 @@
 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.reference.*;
-import de.uka.ilkd.key.logic.*;
 import de.uka.ilkd.key.logic.JTerm;
 import de.uka.ilkd.key.logic.JavaBlock;
 import de.uka.ilkd.key.logic.TermBuilder;
 import de.uka.ilkd.key.logic.TermServices;
 import de.uka.ilkd.key.logic.label.TermLabelManager;
 import de.uka.ilkd.key.logic.label.TermLabelState;
-import de.uka.ilkd.key.logic.op.*;
 import de.uka.ilkd.key.logic.op.IObserverFunction;
 import de.uka.ilkd.key.logic.op.JModality;
 import de.uka.ilkd.key.logic.op.LocationVariable;
@@ -351,7 +349,7 @@ private static ModelFieldInstantiation matchModelField(JTerm focusTerm, Services
         // active statement must be reading model field
         final SourceElement activeStatement = JavaTools.getActiveStatement(mainFml.javaBlock());
         if (!(activeStatement instanceof Assignment ca
-                && ca.getKind() == Assignment.AssignmentKind.Copy)) {
+                && ca.getKind() == Assignment.AssignmentKind.COPY)) {
             return null;
         }
 

key.core/src/main/java/de/uka/ilkd/key/rule/QueryExpand.java

@@ -45,7 +45,7 @@
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 
-import static de.uka.ilkd.key.java.ast.expression.Assignment.AssignmentKind.Copy;
+import static de.uka.ilkd.key.java.ast.expression.Assignment.AssignmentKind.COPY;
 
 
 /**
@@ -201,7 +201,7 @@ public Pair<JTerm, JTerm> queryEvalTerm(Services services, JTerm query,
 
         stmnt.add(KeYJavaASTFactory.declare(result, progResultType));
 
-        final Assignment assignment = new Assignment(Copy, result, mr);
+        final Assignment assignment = new Assignment(COPY, result, mr);
 
         stmnt.add(assignment);
 

key.core/src/main/java/de/uka/ilkd/key/rule/UseOperationContractRule.java

@@ -927,7 +927,7 @@ protected void createPostGoal(Goal postGoal) {
                 resultAssign = new StatementBlock();
             } else {
                 final Assignment ca =
-                    new Assignment(Assignment.AssignmentKind.Copy, inst.actualResult, resultVar);
+                    new Assignment(Assignment.AssignmentKind.COPY, inst.actualResult, resultVar);
                 resultAssign = new StatementBlock(ca);
             }
             final StatementBlock postSB = replaceStatement(jb, resultAssign);