Merge branch 'main' into weigl/junit4rm

* main: (25 commits) Fix comment Fix checkstyle workflow Fix merge conflicts & spotless Remove todo Spotless Fix? resolving error Move ParsableVariable to ncore Spotless Spotless Rename AbstractSV to OperatorSV Beautified code Fix settings test for SE Spotless fixes Fix taclet prefix check when parsing Fix taclet equality test Fix parsing of variable conditions Fix errors resulting from changing ParseableVar Delete Legacy Matcher and adapt VM matcher for new Modality operator Fix errors after changing ParsableVars Fix type error ...
KeYProject · May 23, 2024 · 9be815d · 9be815d
2 parents 6145fe7 + 55ab074
commit 9be815d
Show file tree

Hide file tree

Showing 174 changed files with 3,740 additions and 5,037 deletions.
diff --git a/...c/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionAuxiliaryContract.java b/...c/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionAuxiliaryContract.java
@@ -175,10 +175,10 @@ protected void collectRemembranceVariables(Term term,
             if (SymbolicExecutionUtil.isHeap(eu.lhs(),
                 getServices().getTypeConverter().getHeapLDT())) {
                 remembranceHeaps.put((LocationVariable) term.sub(0).op(),
-                    getServices().getTermBuilder().var(eu.lhs()));
+                    getServices().getTermBuilder().varOfUpdateableOp(eu.lhs()));
             } else {
                 remembranceLocalVariables.put((LocationVariable) term.sub(0).op(),
-                    getServices().getTermBuilder().var(eu.lhs()));
+                    getServices().getTermBuilder().varOfUpdateableOp(eu.lhs()));
             }
         } else {
             assert false : "Unsupported update term with operator '" + term.op() + "'.";

diff --git a/...mbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodPO.java b/...mbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodPO.java
@@ -157,17 +157,17 @@ protected ImmutableList<StatementBlock> buildOperationBlocks(
      * {@inheritDoc}
      */
     @Override
-    protected Term generateMbyAtPreDef(ProgramVariable selfVar,
-            ImmutableList<ProgramVariable> paramVars, Services services) {
+    protected Term generateMbyAtPreDef(LocationVariable selfVar,
+            ImmutableList<LocationVariable> paramVars, Services services) {
         return tb.tt();
     }
 
     /**
      * {@inheritDoc}
      */
     @Override
-    protected Term getPre(List<LocationVariable> modHeaps, ProgramVariable selfVar,
-            ImmutableList<ProgramVariable> paramVars,
+    protected Term getPre(List<LocationVariable> modHeaps, LocationVariable selfVar,
+            ImmutableList<LocationVariable> paramVars,
             Map<LocationVariable, LocationVariable> atPreVars, Services services) {
         if (precondition != null && !precondition.isEmpty()) {
             var context = Context.inMethod(getProgramMethod(), services.getTermBuilder());
@@ -184,9 +184,9 @@ protected Term getPre(List<LocationVariable> modHeaps, ProgramVariable selfVar,
      * {@inheritDoc}
      */
     @Override
-    protected Term getPost(List<LocationVariable> modHeaps, ProgramVariable selfVar,
-            ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar,
-            ProgramVariable exceptionVar, Map<LocationVariable, LocationVariable> atPreVars,
+    protected Term getPost(List<LocationVariable> modHeaps, LocationVariable selfVar,
+            ImmutableList<LocationVariable> paramVars, LocationVariable resultVar,
+            LocationVariable exceptionVar, Map<LocationVariable, LocationVariable> atPreVars,
             Services services) {
         return tb.tt();
     }
@@ -196,7 +196,8 @@ protected Term getPost(List<LocationVariable> modHeaps, ProgramVariable selfVar,
      */
     @Override
     protected Term buildFrameClause(List<LocationVariable> modHeaps, Map<Term, Term> heapToAtPre,
-            ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, Services services) {
+            LocationVariable selfVar, ImmutableList<LocationVariable> paramVars,
+            Services services) {
         return tb.tt();
     }
 

diff --git a/..._execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodSubsetPO.java b/..._execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodSubsetPO.java
@@ -224,10 +224,10 @@ protected boolean endsWithReturn(Statement[] statements) {
      * {@inheritDoc}
      */
     @Override
-    protected Term getPre(List<LocationVariable> modHeaps, ProgramVariable selfVar,
-            ImmutableList<ProgramVariable> paramVars,
+    protected Term getPre(List<LocationVariable> modHeaps, LocationVariable selfVar,
+            ImmutableList<LocationVariable> paramVars,
             Map<LocationVariable, LocationVariable> atPreVars, Services services) {
-        ImmutableList<ProgramVariable> paramVarsList =
+        ImmutableList<LocationVariable> paramVarsList =
             convert(undeclaredVariableCollector.result());
         return super.getPre(modHeaps, selfVar, paramVarsList, atPreVars, services);
     }
@@ -236,10 +236,10 @@ protected Term getPre(List<LocationVariable> modHeaps, ProgramVariable selfVar,
      * {@inheritDoc}
      */
     @Override
-    protected Term buildFreePre(ProgramVariable selfVar, KeYJavaType selfKJT,
-            ImmutableList<ProgramVariable> paramVars, List<LocationVariable> heaps,
+    protected Term buildFreePre(LocationVariable selfVar, KeYJavaType selfKJT,
+            ImmutableList<LocationVariable> paramVars, List<LocationVariable> heaps,
             Services proofServices) {
-        ImmutableList<ProgramVariable> paramVarsList =
+        ImmutableList<LocationVariable> paramVarsList =
             convert(undeclaredVariableCollector.result());
         return super.buildFreePre(selfVar, selfKJT, paramVarsList, heaps, proofServices);
     }
@@ -248,10 +248,10 @@ protected Term buildFreePre(ProgramVariable selfVar, KeYJavaType selfKJT,
      * {@inheritDoc}
      */
     @Override
-    protected Term ensureUninterpretedPredicateExists(ImmutableList<ProgramVariable> paramVars,
-            ImmutableList<LocationVariable> formalParamVars, ProgramVariable exceptionVar,
+    protected Term ensureUninterpretedPredicateExists(ImmutableList<LocationVariable> paramVars,
+            ImmutableList<LocationVariable> formalParamVars, LocationVariable exceptionVar,
             String name, Services proofServices) {
-        ImmutableList<ProgramVariable> paramVarsList =
+        ImmutableList<LocationVariable> paramVarsList =
             convert(undeclaredVariableCollector.result());
         return super.ensureUninterpretedPredicateExists(paramVarsList, formalParamVars,
             exceptionVar, name, proofServices);
@@ -263,8 +263,8 @@ protected Term ensureUninterpretedPredicateExists(ImmutableList<ProgramVariable>
      * @param c The {@link Collection} to convert.
      * @return The created {@link ImmutableList}.
      */
-    protected static ImmutableList<ProgramVariable> convert(Collection<LocationVariable> c) {
-        ImmutableList<ProgramVariable> result = ImmutableSLList.nil();
+    protected static ImmutableList<LocationVariable> convert(Collection<LocationVariable> c) {
+        ImmutableList<LocationVariable> result = ImmutableSLList.nil();
         for (LocationVariable var : c) {
             result = result.append(var);
         }

diff --git a/...de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/AbstractConditionalBreakpoint.java b/...de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/AbstractConditionalBreakpoint.java
@@ -57,10 +57,10 @@ public abstract class AbstractConditionalBreakpoint extends AbstractHitCountBrea
     private String conditionString;
 
     /**
-     * A list of {@link ProgramVariable}s containing all variables that were parsed and have to be
+     * A list of {@link LocationVariable}s containing all variables that were parsed and have to be
      * possibly replaced during runtime.
      */
-    private ImmutableList<ProgramVariable> varsForCondition;
+    private ImmutableList<LocationVariable> varsForCondition;
 
     /**
      * The KeYJavaType of the container of the element associated with the breakpoint.
@@ -84,9 +84,9 @@ public abstract class AbstractConditionalBreakpoint extends AbstractHitCountBrea
     private final Set<LocationVariable> paramVars;
 
     /**
-     * A {@link ProgramVariable} representing the instance the class KeY is working on
+     * A {@link LocationVariable} representing the instance the class KeY is working on
      */
-    private ProgramVariable selfVar;
+    private LocationVariable selfVar;
 
     /**
      * The {@link IProgramMethod} this Breakpoint lies within
@@ -291,14 +291,14 @@ private Term computeTermForCondition(String condition) {
         setSelfVar(new LocationVariable(
             new ProgramElementName(getProof().getServices().getTermBuilder().newName("self")),
             containerType, null, false, false));
-        ImmutableList<ProgramVariable> varsForCondition = ImmutableSLList.nil();
+        ImmutableList<LocationVariable> varsForCondition = ImmutableSLList.nil();
         if (getPm() != null) {
             // collect parameter variables
             for (ParameterDeclaration pd : getPm().getParameters()) {
                 for (VariableSpecification vs : pd.getVariables()) {
                     this.paramVars.add((LocationVariable) vs.getProgramVariable());
                     varsForCondition =
-                        varsForCondition.append((ProgramVariable) vs.getProgramVariable());
+                        varsForCondition.append((LocationVariable) vs.getProgramVariable());
                 }
             }
             // Collect local variables
@@ -313,7 +313,7 @@ private Term computeTermForCondition(String condition) {
         }
         JavaInfo info = getProof().getServices().getJavaInfo();
         ImmutableList<KeYJavaType> kjts = info.getAllSupertypes(containerType);
-        ImmutableList<ProgramVariable> globalVars = ImmutableSLList.nil();
+        ImmutableList<LocationVariable> globalVars = ImmutableSLList.nil();
         for (KeYJavaType kjtloc : kjts) {
             if (kjtloc.getJavaType() instanceof TypeDeclaration) {
                 ImmutableList<Field> fields =
@@ -322,7 +322,7 @@ private Term computeTermForCondition(String condition) {
                     if ((kjtloc.equals(containerType) || !field.isPrivate())
                             && !((LocationVariable) field.getProgramVariable()).isImplicit()) {
                         globalVars =
-                            globalVars.append((ProgramVariable) field.getProgramVariable());
+                            globalVars.append((LocationVariable) field.getProgramVariable());
                     }
                 }
             }
@@ -423,10 +423,10 @@ public boolean isBreakpointHit(SourceElement activeStatement, RuleApp ruleApp, P
      */
     protected abstract boolean isInScopeForCondition(Node node);
 
-    private ImmutableList<ProgramVariable> saveAddVariable(LocationVariable x,
-            ImmutableList<ProgramVariable> varsForCondition) {
+    private ImmutableList<LocationVariable> saveAddVariable(LocationVariable x,
+            ImmutableList<LocationVariable> varsForCondition) {
         boolean contains = false;
-        for (ProgramVariable paramVar : varsForCondition) {
+        for (var paramVar : varsForCondition) {
             if (paramVar.toString().equals(x.toString())) {
                 contains = true;
                 break;
@@ -512,28 +512,28 @@ public void setVariableNamingMap(Map<SVSubstitute, SVSubstitute> variableNamingM
     /**
      * @return the selfVar
      */
-    public ProgramVariable getSelfVar() {
+    public LocationVariable getSelfVar() {
         return selfVar;
     }
 
     /**
      * @param selfVar the selfVar to set
      */
-    public void setSelfVar(ProgramVariable selfVar) {
+    public void setSelfVar(LocationVariable selfVar) {
         this.selfVar = selfVar;
     }
 
     /**
      * @return the varsForCondition
      */
-    public ImmutableList<ProgramVariable> getVarsForCondition() {
+    public ImmutableList<LocationVariable> getVarsForCondition() {
         return varsForCondition;
     }
 
     /**
      * @param varsForCondition the varsForCondition to set
      */
-    public void setVarsForCondition(ImmutableList<ProgramVariable> varsForCondition) {
+    public void setVarsForCondition(ImmutableList<LocationVariable> varsForCondition) {
         this.varsForCondition = varsForCondition;
     }
 

diff --git a/...test/java/de/uka/ilkd/key/symbolic_execution/testcase/util/TestSymbolicExecutionUtil.java b/...test/java/de/uka/ilkd/key/symbolic_execution/testcase/util/TestSymbolicExecutionUtil.java
@@ -4,6 +4,7 @@
 package de.uka.ilkd.key.symbolic_execution.testcase.util;
 
 import java.io.File;
+import java.util.HashMap;
 import java.util.Map;
 
 import de.uka.ilkd.key.control.KeYEnvironment;
@@ -148,8 +149,12 @@ public void test2GetAndSetChoiceSetting() {
             // Make sure that all other settings are unchanged.
             Map<String, String> changedSettings =
                 ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().getDefaultChoices();
-            defaultSettings.put(SymbolicExecutionUtil.CHOICE_SETTING_RUNTIME_EXCEPTIONS, newValue);
-            Assertions.assertEquals(defaultSettings, changedSettings);
+
+            Map<String, String> expectedSettings = new HashMap<>();
+            expectedSettings.putAll(defaultSettings);
+            expectedSettings.put(SymbolicExecutionUtil.CHOICE_SETTING_RUNTIME_EXCEPTIONS, newValue);
+
+            Assertions.assertEquals(expectedSettings, changedSettings);
         } finally {
             if (originalValue != null) {
                 SymbolicExecutionUtil.setChoiceSetting(

diff --git a/key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletFindModel.java b/key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletFindModel.java
@@ -302,7 +302,7 @@ private Term addOrigin(Term term) {
     private ProgramElement parseRow(int irow) throws SVInstantiationParserException {
 
         String instantiation = (String) getValueAt(irow, 1);
-        SchemaVariable sv = (SchemaVariable) getValueAt(irow, 0);
+        ProgramSV sv = (ProgramSV) getValueAt(irow, 0);
 
         ContextInstantiationEntry contextInstantiation =
             originalApp.instantiations().getContextInstantiation();
@@ -353,7 +353,7 @@ public TacletApp createTacletAppFromVarInsts() throws SVInstantiationException {
                     sort = idd.sort();
                     if (sort == null) {
                         try {
-                            sort = result.getRealSort(sv, services);
+                            sort = result.getRealSort((OperatorSV) sv, services);
                         } catch (SortException e) {
                             throw new MissingSortException(String.valueOf(sv),
                                 createPosition(irow));

diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/BlockExecutionPO.java b/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/BlockExecutionPO.java
@@ -252,8 +252,8 @@ protected ImmutableList<StatementBlock> buildOperationBlocks(
 
     @Override
     @Deprecated
-    protected Term getPre(List<LocationVariable> modHeaps, ProgramVariable selfVar,
-            ImmutableList<ProgramVariable> paramVars,
+    protected Term getPre(List<LocationVariable> modHeaps, LocationVariable selfVar,
+            ImmutableList<LocationVariable> paramVars,
             Map<LocationVariable, LocationVariable> atPreVars, Services services) {
         throw new UnsupportedOperationException(
             "Not supported any more. " + "Please use the POSnippetFactory instead.");
@@ -262,9 +262,9 @@ protected Term getPre(List<LocationVariable> modHeaps, ProgramVariable selfVar,
 
     @Override
     @Deprecated
-    protected Term getPost(List<LocationVariable> modHeaps, ProgramVariable selfVar,
-            ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar,
-            ProgramVariable exceptionVar, Map<LocationVariable, LocationVariable> atPreVars,
+    protected Term getPost(List<LocationVariable> modHeaps, LocationVariable selfVar,
+            ImmutableList<LocationVariable> paramVars, LocationVariable resultVar,
+            LocationVariable exceptionVar, Map<LocationVariable, LocationVariable> atPreVars,
             Services services) {
         throw new UnsupportedOperationException(
             "Not supported any more. " + "Please use the POSnippetFactory instead.");
@@ -274,16 +274,17 @@ protected Term getPost(List<LocationVariable> modHeaps, ProgramVariable selfVar,
     @Override
     @Deprecated
     protected Term buildFrameClause(List<LocationVariable> modHeaps, Map<Term, Term> heapToAtPre,
-            ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, Services services) {
+            LocationVariable selfVar, ImmutableList<LocationVariable> paramVars,
+            Services services) {
         throw new UnsupportedOperationException(
             "Not supported any more. " + "Please use the POSnippetFactory instead.");
     }
 
 
     @Override
     @Deprecated
-    protected Term generateMbyAtPreDef(ProgramVariable selfVar,
-            ImmutableList<ProgramVariable> paramVars, Services services) {
+    protected Term generateMbyAtPreDef(LocationVariable selfVar,
+            ImmutableList<LocationVariable> paramVars, Services services) {
         throw new UnsupportedOperationException(
             "Not supported any more. " + "Please use the POSnippetFactory instead.");
     }

diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/InfFlowContractPO.java b/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/InfFlowContractPO.java
@@ -244,8 +244,8 @@ protected ImmutableList<StatementBlock> buildOperationBlocks(
 
     @Override
     @Deprecated
-    protected Term getPre(List<LocationVariable> modHeaps, ProgramVariable selfVar,
-            ImmutableList<ProgramVariable> paramVars,
+    protected Term getPre(List<LocationVariable> modHeaps, LocationVariable selfVar,
+            ImmutableList<LocationVariable> paramVars,
             Map<LocationVariable, LocationVariable> atPreVars, Services services) {
         throw new UnsupportedOperationException(
             "Not supported any more. " + "Please use the POSnippetFactory instead.");
@@ -254,9 +254,9 @@ protected Term getPre(List<LocationVariable> modHeaps, ProgramVariable selfVar,
 
     @Override
     @Deprecated
-    protected Term getPost(List<LocationVariable> modHeaps, ProgramVariable selfVar,
-            ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar,
-            ProgramVariable exceptionVar, Map<LocationVariable, LocationVariable> atPreVars,
+    protected Term getPost(List<LocationVariable> modHeaps, LocationVariable selfVar,
+            ImmutableList<LocationVariable> paramVars, LocationVariable resultVar,
+            LocationVariable exceptionVar, Map<LocationVariable, LocationVariable> atPreVars,
             Services services) {
         throw new UnsupportedOperationException(
             "Not supported any more. " + "Please use the POSnippetFactory instead.");
@@ -266,16 +266,17 @@ protected Term getPost(List<LocationVariable> modHeaps, ProgramVariable selfVar,
     @Override
     @Deprecated
     protected Term buildFrameClause(List<LocationVariable> modHeaps, Map<Term, Term> heapToAtPre,
-            ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, Services services) {
+            LocationVariable selfVar, ImmutableList<LocationVariable> paramVars,
+            Services services) {
         throw new UnsupportedOperationException(
             "Not supported any more. " + "Please use the POSnippetFactory instead.");
     }
 
 
     @Override
     @Deprecated
-    protected Term generateMbyAtPreDef(ProgramVariable selfVar,
-            ImmutableList<ProgramVariable> paramVars, Services services) {
+    protected Term generateMbyAtPreDef(LocationVariable selfVar,
+            ImmutableList<LocationVariable> paramVars, Services services) {
         throw new UnsupportedOperationException(
             "Not supported any more. " + "Please use the POSnippetFactory instead.");
     }

diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/InfFlowProofSymbols.java b/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/InfFlowProofSymbols.java
@@ -613,11 +613,13 @@ private void printSchemaVariables(StringBuilder result) {
 
         result.append("\\schemaVariables{\n");
         for (final SchemaVariable sv : getSchemaVariables()) {
-            final String prefix = sv instanceof FormulaSV ? "\\formula "
-                    : sv instanceof TermSV ? "\\term " : "\\variables ";
+            if (!(sv instanceof OperatorSV asv))
+                continue;
+            final String prefix = asv instanceof FormulaSV ? "\\formula "
+                    : asv instanceof TermSV ? "\\term " : "\\variables ";
             result.append(prefix);
-            result.append(sv.sort().name()).append(" ");
-            result.append(sv.name());
+            result.append(asv.sort().name()).append(" ");
+            result.append(asv.name());
             result.append(";\n");
         }
         result.append("}\n\n");