Generalize ParsableVariable and Schemavariables (#3436)

KeYProject · May 22, 2024 · 55ab074 · 55ab074
2 parents 120b06f + a16defe
commit 55ab074
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");