Universe Type Rules

.gitignore

@@ -51,6 +51,7 @@ bin/
 .settings
 .project
 .classpath
+.factorypath
 
 # Files generated by IntelliJ ANTLR plugin
 key.core/src/main/gen

key.core/src/main/antlr4/KeYLexer.g4

@@ -160,6 +160,7 @@ MAXEXPANDMETHOD : '\\mayExpandMethod';
 STRICT    : '\\strict';
 TYPEOF : '\\typeof';
 INSTANTIATE_GENERIC : '\\instantiateGeneric';
+HAS_ANNOTATION: '\\hasAnnotation';
 
 // Quantifiers, binding, substitution
 FORALL : '\\forall' | '\u2200';

key.core/src/main/antlr4/KeYParser.g4

@@ -736,6 +736,7 @@ varexpId: // weigl, 2021-03-12: This will be later just an arbitrary identifier.
   | GET_VARIANT
   | IS_LABELED
   | ISINSTRICTFP
+  | HAS_ANNOTATION
 ;
 
 varexp_argument

key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/modifier/AnnotationUseSpecification.java

@@ -3,6 +3,8 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.java.ast.declaration.modifier;
 
+import org.key_project.logic.SyntaxElement;
+
 import de.uka.ilkd.key.java.ast.ProgramElement;
 import de.uka.ilkd.key.java.ast.declaration.Modifier;
 import de.uka.ilkd.key.java.ast.reference.TypeReference;
@@ -18,7 +20,7 @@ public AnnotationUseSpecification(TypeReference tr) {
     }
 
     protected String getSymbol() {
-        return "@" + tr.toString();
+        return "@" + tr.getName();
     }
 
     public TypeReference getTypeReferenceAt(int index) {
@@ -39,8 +41,12 @@ public ProgramElement getChildAt(int index) {
         throw new ArrayIndexOutOfBoundsException();
     }
 
+    @Override
+    public SyntaxElement getChild(int index) {
+        return getChildAt(index);
+    }
+
     public int getChildCount() {
         return 1;
     }
-
 }

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

@@ -80,7 +80,6 @@ public New(ExtList children, ReferencePrefix rp, PositionInfo pi) {
         accessPath = rp;
     }
 
-
     /**
      * Constructor for the transformation of COMPOST ASTs to KeY.
      *
@@ -180,6 +179,9 @@ public int getChildCount() {
         if (anonymousClass != null) {
             result++;
         }
+        if (annotations != null) {
+            result += annotations.size();
+        }
         return result;
     }
 
@@ -210,6 +212,13 @@ public ProgramElement getChildAt(int index) {
             if (index == 0) {
                 return anonymousClass;
             }
+            index--;
+        }
+        if (annotations != null) {
+            len = annotations.size();
+            if (len > index) {
+                return annotations.get(index);
+            }
         }
         throw new ArrayIndexOutOfBoundsException();
     }

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

@@ -178,6 +178,9 @@ public int getChildCount() {
         if (arrayInitializer != null) {
             result++;
         }
+        if (annotations != null) {
+            result += annotations.size();
+        }
         return result;
     }
 
@@ -210,6 +213,13 @@ public ProgramElement getChildAt(int index) {
             if (index == 0) {
                 return arrayInitializer;
             }
+            index--;
+        }
+        if (annotations != null) {
+            len = annotations.size();
+            if (len > index) {
+                return annotations.get(index);
+            }
         }
         throw new ArrayIndexOutOfBoundsException();
     }

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

@@ -5,6 +5,7 @@
 
 import java.util.List;
 
+import de.uka.ilkd.key.java.ast.declaration.modifier.AnnotationUseSpecification;
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.java.ast.Comment;
 import de.uka.ilkd.key.java.ast.PositionInfo;
@@ -31,6 +32,11 @@ public abstract class TypeOperator extends Operator implements TypeReferenceCont
      */
     protected final TypeReference typeReference;
 
+    /**
+     * Annotations.
+     */
+    protected final ImmutableArray<AnnotationUseSpecification> annotations;
+
 
     /**
      * Constructor for the transformation of COMPOST ASTs to KeY.
@@ -43,6 +49,8 @@ public abstract class TypeOperator extends Operator implements TypeReferenceCont
     protected TypeOperator(ExtList children) {
         super(children);
         typeReference = children.get(TypeReference.class);
+        annotations = new ImmutableArray<>(
+            children.collect(AnnotationUseSpecification.class));
     }
 
     /**
@@ -56,26 +64,39 @@ protected TypeOperator(ExtList children) {
     protected TypeOperator(ExtList children, PositionInfo pi) {
         super(children);
         typeReference = children.get(TypeReference.class);
+        annotations = new ImmutableArray<>(
+            children.collect(AnnotationUseSpecification.class));
     }
 
     protected TypeOperator(Expression unaryChild, TypeReference typeref) {
         super(unaryChild);
         typeReference = typeref;
+        annotations = null;
     }
 
     protected TypeOperator(Expression[] arguments, TypeReference typeref) {
         super(arguments);
         typeReference = typeref;
+        annotations = null;
+    }
+
+    protected TypeOperator(Expression[] arguments, TypeReference typeref,
+            ImmutableArray<AnnotationUseSpecification> annotations) {
+        super(arguments);
+        typeReference = typeref;
+        this.annotations = annotations;
     }
 
     protected TypeOperator() {
         typeReference = null;
+        annotations = null;
     }
 
     public TypeOperator(PositionInfo pi, List<Comment> c, ImmutableArray<Expression> arguments,
             TypeReference type) {
         super(pi, c, arguments);
         typeReference = type;
+        annotations = null;
     }
 
     /**
@@ -122,5 +143,12 @@ public KeYJavaType getKeYJavaType(Services javaServ) {
         return getTypeReference().getKeYJavaType();
     }
 
-
+    /**
+     * A getter for the annotations.
+     *
+     * @return the annotations.
+     */
+    public ImmutableArray<AnnotationUseSpecification> getAnnotations() {
+        return annotations;
+    }
 }

key.core/src/main/java/de/uka/ilkd/key/ldt/JavaDLTheory.java

@@ -20,7 +20,7 @@
 import org.key_project.util.ExtList;
 
 /**
- * The JavaDL theory class provides access to function symvols, sorts that are part of the core
+ * The JavaDL theory class provides access to function symbols, sorts that are part of the core
  * logic
  * like cast or instanceof functions.
  */

key.core/src/main/java/de/uka/ilkd/key/macros/HeapSimplificationMacro.java

@@ -63,6 +63,35 @@ public String getDescription() {
         "wellFormedAnonEQ", "wellFormedMemsetArrayObjectEQ", "wellFormedMemsetArrayPrimitiveEQ",
         "wellFormedMemsetObjectEQ", "wellFormedMemsetLocSetEQ", "wellFormedMemsetPrimitiveEQ",
 
+        // universe rules
+        "createdRepfpElement",
+
+        "dismissSelectOfDominatedObject", "dismissSelectOfDominatingObject",
+        "dismissSelectOfDominatedAnon", "dismissSelectOfDominatedCreatedAnon",
+
+        "dismissSelectOfSelfRepfpComplementAnon", "dismissSelectOfSelfCreatedRepfpComplementAnon",
+        "dismissSelectOfDominatingRepfpComplementAnon",
+        "dismissSelectOfDominatingCreatedRepfpComplementAnon",
+
+        "dismissSelectOfDominatedObjectEQ", "dismissSelectOfDominatingObjectEQ",
+        "dismissSelectOfDominatedAnonEQ", "dismissSelectOfDominatedCreatedAnonEQ",
+
+        "dismissSelectOfSelfRepfpComplementAnonEQ",
+        "dismissSelectOfSelfCreatedRepfpComplementAnonEQ",
+        "dismissSelectOfDominatingRepfpComplementAnonEQ",
+        "dismissSelectOfDominatingCreatedRepfpComplementAnonEQ",
+
+        "simplifySelectOfDominatedAnon", "simplifySelectOfDominatedCreatedAnon",
+        "simplifySelectOfSelfRepfpComplementAnon", "simplifySelectOfSelfCreatedRepfpComplementAnon",
+        "simplifySelectOfDominatingRepfpComplementAnon",
+        "simplifySelectOfDominatingCreatedRepfpComplementAnon",
+
+        "simplifySelectOfDominatedAnonEQ", "simplifySelectOfDominatedCreatedAnonEQ",
+        "simplifySelectOfSelfRepfpComplementAnonEQ",
+        "simplifySelectOfSelfCreatedRepfpComplementAnonEQ",
+        "simplifySelectOfDominatingRepfpComplementAnonEQ",
+        "simplifySelectOfDominatingCreatedRepfpComplementAnonEQ",
+
         // locset rules
         "elementOfEmpty", "elementOfAllLocs", "elementOfSingleton", "elementOfUnion",
         "elementOfIntersect", "elementOfSetMinus", "elementOfAllFields", "elementOfAllObjects",

key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java

@@ -270,6 +270,8 @@ public VariableCondition build(Object[] arguments, List<String> parameters,
         new ConstructorBasedBuilder("static", StaticReferenceCondition.class, SV);
     public static final TacletBuilderCommand DIFFERENT_FIELDS =
         new ConstructorBasedBuilder("differentFields", DifferentFields.class, SV, SV);
+    public static final AbstractConditionBuilder HAS_ANNOTATION =
+        new ConstructorBasedBuilder("hasAnnotation", HasAnnotationCondition.class, SV, S);
     public static final AbstractConditionBuilder SAME_OBSERVER =
         new ConstructorBasedBuilder("sameObserver", SameObserverCondition.class, PV, PV);
     public static final AbstractConditionBuilder applyUpdateOnRigid = new ConstructorBasedBuilder(
@@ -382,7 +384,8 @@ public IsLabeledCondition build(Object[] arguments, List<String> parameters,
             applyUpdateOnRigid, DROP_EFFECTLESS_ELEMENTARIES, SIMPLIFY_ITE_UPDATE, SUBFORMULAS,
             STATIC_FIELD, MODEL_FIELD, SUBFORMULA, DROP_EFFECTLESS_STORES, EQUAL_UNIQUE,
             META_DISJOINT,
-            IS_OBSERVER, CONSTANT, HAS_SORT, LABEL, NEW_LABEL, HAS_ELEM_SORT, IS_IN_STRICTFP);
+            IS_OBSERVER, CONSTANT, HAS_SORT, LABEL, NEW_LABEL, HAS_ELEM_SORT, IS_IN_STRICTFP,
+            HAS_ANNOTATION);
         register(STORE_TERM_IN, STORE_STMT_IN, HAS_INVARIANT, GET_INVARIANT, GET_FREE_INVARIANT,
             GET_VARIANT, IS_LABELED);
         loadWithServiceLoader();

key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java

@@ -7,6 +7,7 @@
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.java.ast.*;
+import de.uka.ilkd.key.java.ast.declaration.modifier.AnnotationUseSpecification;
 import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType;
 import de.uka.ilkd.key.java.ast.abstraction.Type;
 import de.uka.ilkd.key.java.ast.ccatch.*;
@@ -174,7 +175,7 @@ protected static String encodeUnicodeChars(String str) {
      *
      * @param list a program element list.
      */
-    protected void writeKeywordList(ImmutableArray<Modifier> list) {
+    protected <T extends Modifier> void writeKeywordList(ImmutableArray<T> list) {
         for (int i = 0; i < list.size(); i++) {
             if (i != 0) {
                 layouter.brk();
@@ -1453,6 +1454,14 @@ public void performActionOnNewArray(NewArray x) {
         if (addParentheses) {
             layouter.print("(");
         }
+
+        ImmutableArray<AnnotationUseSpecification> annots = x.getAnnotations();
+        boolean hasAnnots = annots != null && !annots.isEmpty();
+        if (hasAnnots) {
+            writeKeywordList(annots);
+            layouter.print(" ");
+        }
+
         layouter.print("new ");
 
         x.getTypeReference().visit(this);
@@ -1514,6 +1523,13 @@ public void performActionOnNew(New x) {
         printReferencePrefix(x.getReferencePrefix());
         layouter.keyWord("new").print(" ");
 
+        ImmutableArray<AnnotationUseSpecification> annots = x.getAnnotations();
+        boolean hasAnnots = annots != null && !annots.isEmpty();
+        if (hasAnnots) {
+            writeKeywordList(annots);
+            layouter.print(" ");
+        }
+
         x.getTypeReference().visit(this);
         printArguments(x.getArguments());
         if (x.getClassDeclaration() != null) {

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

@@ -41,6 +41,8 @@
 
 import com.github.javaparser.ast.key.KeyTransactionStatement;
 import org.jspecify.annotations.Nullable;
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
 
 /**
  * <p>
@@ -79,6 +81,7 @@
  * @author Martin Hentschel
  */
 public abstract class AbstractOperationPO extends AbstractPO {
+    private static final Logger LOGGER = LoggerFactory.getLogger(AbstractOperationPO.class);
     private static final String JAVA_LANG_THROWABLE = "java.lang.Throwable";
 
     protected InitConfig proofConfig;

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

@@ -32,11 +32,14 @@
 import org.key_project.util.collection.ImmutableSet;
 import org.key_project.util.collection.Pair;
 
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
 
 /**
  * An abstract proof obligation implementing common functionality.
  */
 public abstract class AbstractPO implements IPersistablePO {
+    private static final Logger LOGGER = LoggerFactory.getLogger(AbstractPO.class);
 
     protected TermBuilder tb;
     protected final InitConfig environmentConfig;

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

@@ -36,6 +36,8 @@
 
 import org.jspecify.annotations.NonNull;
 import org.jspecify.annotations.Nullable;
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
 
 import static de.uka.ilkd.key.java.KeYJavaASTFactory.declare;
 
@@ -62,6 +64,8 @@
  * </p>
  */
 public class FunctionalOperationContractPO extends AbstractOperationPO implements ContractPO {
+    private static final Logger LOGGER =
+        LoggerFactory.getLogger(FunctionalOperationContractPO.class);
     public static final Map<Boolean, @NonNull String> TRANSACTION_TAGS =
         new LinkedHashMap<>();