Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Generalize ParsableVariable and Schemavariables #3436

Merged
merged 28 commits into from
May 22, 2024
Merged
Show file tree
Hide file tree
Changes from 27 commits
Commits
Show all changes
28 commits
Select commit Hold shift + click to select a range
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -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() + "'.";
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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());
Expand All @@ -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();
}
Expand All @@ -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();
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}
Expand All @@ -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);
}
Expand All @@ -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);
Expand All @@ -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);
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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 =
Expand All @@ -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());
}
}
}
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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;
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -148,8 +149,12 @@
// 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);

Check warning on line 154 in key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/util/TestSymbolicExecutionUtil.java

View workflow job for this annotation

GitHub Actions / qodana

Redundant 'Collection.addAll()' call

'putAll()' call can be replaced with parametrized constructor call
expectedSettings.put(SymbolicExecutionUtil.CHOICE_SETTING_RUNTIME_EXCEPTIONS, newValue);

Assertions.assertEquals(expectedSettings, changedSettings);
} finally {
if (originalValue != null) {
SymbolicExecutionUtil.setChoiceSetting(
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand Down Expand Up @@ -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));
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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.");
Expand All @@ -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.");
Expand All @@ -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.");
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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.");
Expand All @@ -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.");
Expand All @@ -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.");
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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");
Expand Down
Loading
Loading