Skip to content

Commit 76cfef2

Browse files
unp1unp1
authored
Generalize Taclet Implementation (#3605)
2 parents 71bc6c7 + b25e49f commit 76cfef2

File tree

224 files changed

+3255
-4318
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

224 files changed

+3255
-4318
lines changed

‎key.core.proof_references/src/test/java/de/uka/ilkd/key/proof_references/testcase/AbstractProofReferenceTestCase.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,6 @@
1212

1313
import de.uka.ilkd.key.control.KeYEnvironment;
1414
import de.uka.ilkd.key.java.abstraction.KeYJavaType;
15-
import de.uka.ilkd.key.logic.Choice;
1615
import de.uka.ilkd.key.logic.op.IObserverFunction;
1716
import de.uka.ilkd.key.logic.op.IProgramMethod;
1817
import de.uka.ilkd.key.proof.Node;
@@ -29,6 +28,7 @@
2928
import de.uka.ilkd.key.strategy.StrategyProperties;
3029
import de.uka.ilkd.key.util.HelperClassForTests;
3130

31+
import org.key_project.logic.Choice;
3232
import org.key_project.util.collection.DefaultImmutableSet;
3333
import org.key_project.util.collection.ImmutableList;
3434
import org.key_project.util.collection.ImmutableSLList;

‎key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/proof/TermProgramVariableCollectorKeepUpdatesForBreakpointconditions.java‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,13 +4,14 @@
44
package de.uka.ilkd.key.proof;
55

66
import de.uka.ilkd.key.java.Services;
7-
import de.uka.ilkd.key.logic.Term;
87
import de.uka.ilkd.key.logic.op.LocationVariable;
98
import de.uka.ilkd.key.logic.op.Modality;
109
import de.uka.ilkd.key.strategy.IBreakpointStopCondition;
1110
import de.uka.ilkd.key.symbolic_execution.strategy.breakpoint.AbstractConditionalBreakpoint;
1211
import de.uka.ilkd.key.symbolic_execution.strategy.breakpoint.IBreakpoint;
1312

13+
import org.key_project.logic.Term;
14+
1415
public class TermProgramVariableCollectorKeepUpdatesForBreakpointconditions
1516
extends TermProgramVariableCollector {
1617
private final IBreakpointStopCondition breakpointStopCondition;

‎key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/SymbolicExecutionTreeBuilder.java‎

Lines changed: 9 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -254,16 +254,12 @@ public SymbolicExecutionTreeBuilder(Proof proof, boolean mergeBranchConditions,
254254
*/
255255
protected void initMethodCallStack(final Node root, Services services) {
256256
// Find all modalities in the succedent
257-
final List<Term> modalityTerms = new LinkedList<>();
258-
for (SequentFormula sequentFormula : root.sequent()
259-
.succedent()) {
260-
sequentFormula.formula().execPreOrder(new DefaultVisitor() {
261-
@Override
262-
public void visit(Term visited) {
263-
if (visited.op() instanceof Modality
264-
&& SymbolicExecutionUtil.hasSymbolicExecutionLabel(visited)) {
265-
modalityTerms.add(visited);
266-
}
257+
final List<org.key_project.logic.Term> modalityTerms = new LinkedList<>();
258+
for (SequentFormula sequentFormula : root.sequent().succedent()) {
259+
sequentFormula.formula().execPreOrder((DefaultVisitor) visited -> {
260+
if (visited.op() instanceof Modality
261+
&& SymbolicExecutionUtil.hasSymbolicExecutionLabel(visited)) {
262+
modalityTerms.add(visited);
267263
}
268264
});
269265
}
@@ -278,7 +274,7 @@ public void visit(Term visited) {
278274
"Sequent contains multiple modalities with symbolic execution label.");
279275
}
280276
// Make sure that modality has symbolic execution label
281-
Term modalityTerm = modalityTerms.get(0);
277+
var modalityTerm = modalityTerms.get(0);
282278
SymbolicExecutionTermLabel label =
283279
SymbolicExecutionUtil.getSymbolicExecutionLabel(modalityTerm);
284280
if (label == null) {
@@ -287,7 +283,8 @@ public void visit(Term visited) {
287283
}
288284
// Check if modality contains method frames
289285
if (!modalityTerms.isEmpty()) {
290-
JavaBlock javaBlock = modalityTerm.javaBlock();
286+
final Modality mod = (Modality) modalityTerm.op();
287+
JavaBlock javaBlock = mod.programBlock();
291288
final ProgramElement program = javaBlock.program();
292289
final List<Node> initialStack = new LinkedList<>();
293290
new JavaASTVisitor(program, services) {

‎key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/SymbolicLayoutExtractor.java‎

Lines changed: 7 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -702,15 +702,13 @@ protected Set<Term> collectObjectsFromSequent(Sequent sequent, Set<Term> objects
702702
protected Set<Term> collectSymbolicObjectsFromTerm(Term term, final Set<Term> objectsToIgnore)
703703
throws ProofInputException {
704704
final Set<Term> result = new LinkedHashSet<>();
705-
term.execPreOrder(new DefaultVisitor() {
706-
@Override
707-
public void visit(Term visited) {
708-
visited = OriginTermLabel.removeOriginLabels(visited, getServices());
709-
if (SymbolicExecutionUtil.hasReferenceSort(getServices(), visited)
710-
&& visited.freeVars().isEmpty() && !objectsToIgnore.contains(visited)
711-
&& !SymbolicExecutionUtil.isSkolemConstant(visited)) {
712-
result.add(visited);
713-
}
705+
term.execPreOrder((DefaultVisitor) p_visited -> {
706+
Term visited = (Term) p_visited;
707+
visited = OriginTermLabel.removeOriginLabels(visited, getServices());
708+
if (SymbolicExecutionUtil.hasReferenceSort(getServices(), visited)
709+
&& visited.freeVars().isEmpty() && !objectsToIgnore.contains(visited)
710+
&& !SymbolicExecutionUtil.isSkolemConstant(visited)) {
711+
result.add(visited);
714712
}
715713
});
716714
return result;

‎key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/TruthValueTracingUtil.java‎

Lines changed: 15 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -452,14 +452,11 @@ private static void updatePredicateResultBasedOnNewMinorIdsOSS(
452452
final Map<String, MultiEvaluationResult> results) {
453453
if (parentPio != null) {
454454
// Check application term and all of its children and grand children
455-
parentPio.subTerm().execPreOrder(new DefaultVisitor() {
456-
@Override
457-
public void visit(Term visited) {
458-
checkForNewMinorIdsOSS(childPio.sequentFormula(), visited,
455+
parentPio.subTerm()
456+
.execPreOrder((DefaultVisitor) visited -> checkForNewMinorIdsOSS(
457+
childPio.sequentFormula(), (Term) visited,
459458
termLabelName,
460-
parentPio, tb, results);
461-
}
462-
});
459+
parentPio, tb, results));
463460
// Check application term parents
464461
PosInOccurrence currentPio = parentPio;
465462
while (!currentPio.isTopLevel()) {
@@ -487,11 +484,11 @@ private static void checkForNewMinorIdsOSS(
487484
TermBuilder tb,
488485
Map<String, MultiEvaluationResult> results) {
489486
TermLabel label = term.getLabel(termLabelName);
490-
if (label instanceof FormulaTermLabel) {
491-
Term replacement = checkForNewMinorIdsOSS(onlyChangedChildSF, (FormulaTermLabel) label,
487+
if (label instanceof final FormulaTermLabel formulaLabel) {
488+
Term replacement = checkForNewMinorIdsOSS(onlyChangedChildSF, formulaLabel,
492489
parentPio.isInAntec(), tb);
493490
if (replacement != null) {
494-
updatePredicateResult((FormulaTermLabel) label, replacement, results);
491+
updatePredicateResult(formulaLabel, replacement, results);
495492
}
496493
}
497494
}
@@ -543,13 +540,10 @@ private static void updatePredicateResultBasedOnNewMinorIds(
543540
parentRuleApp.posInOccurrence();
544541
if (parentPio != null) {
545542
// Check application term and all of its children and grand children
546-
parentPio.subTerm().execPreOrder(new DefaultVisitor() {
547-
@Override
548-
public void visit(Term visited) {
549-
checkForNewMinorIds(childNode, visited, termLabelName, parentPio, tb,
550-
results);
551-
}
552-
});
543+
parentPio.subTerm()
544+
.execPreOrder((DefaultVisitor) visited -> checkForNewMinorIds(childNode,
545+
(Term) visited, termLabelName, parentPio, tb,
546+
results));
553547
// Check application term parents
554548
PosInOccurrence currentPio = parentPio;
555549
while (!currentPio.isTopLevel()) {
@@ -638,12 +632,13 @@ private static void listLabelReplacements(
638632
final String labelId, final List<Term> resultToFill) {
639633
sf.formula().execPreOrder(new DefaultVisitor() {
640634
@Override
641-
public boolean visitSubtree(Term visited) {
642-
return !hasLabelOfInterest(visited);
635+
public boolean visitSubtree(org.key_project.logic.Term visited) {
636+
return !hasLabelOfInterest((Term) visited);
643637
}
644638

645639
@Override
646-
public void visit(Term visited) {
640+
public void visit(org.key_project.logic.Term p_visited) {
641+
final Term visited = (Term) p_visited;
647642
if (hasLabelOfInterest(visited)) {
648643
resultToFill.add(visited);
649644
}

‎key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionSideProofUtil.java‎

Lines changed: 21 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -36,9 +36,11 @@
3636
import de.uka.ilkd.key.util.ProofStarter;
3737
import de.uka.ilkd.key.util.SideProofUtil;
3838

39+
import org.key_project.logic.Choice;
3940
import org.key_project.logic.Name;
4041
import org.key_project.logic.Namespace;
4142
import org.key_project.logic.op.Function;
43+
import org.key_project.logic.op.Operator;
4244
import org.key_project.prover.engine.impl.ApplyStrategyInfo;
4345
import org.key_project.prover.sequent.Sequent;
4446
import org.key_project.prover.sequent.SequentFormula;
@@ -202,7 +204,7 @@ public static List<ResultsAndCondition> computeResultsAndConditions(
202204
for (SequentFormula sf : sequent.antecedent()) {
203205
final Term formula = (Term) sf.formula();
204206
if (newPredicateIsSequentFormula) {
205-
if (Operator.opEquals(formula.op(), operator)) {
207+
if (de.uka.ilkd.key.logic.op.Operator.opEquals(formula.op(), operator)) {
206208
throw new IllegalStateException(
207209
"Result predicate found in antecedent.");
208210
} else {
@@ -224,7 +226,7 @@ public static List<ResultsAndCondition> computeResultsAndConditions(
224226
for (SequentFormula sf : sequent.succedent()) {
225227
final Term formula = (Term) sf.formula();
226228
if (newPredicateIsSequentFormula) {
227-
if (Operator.opEquals(formula.op(), operator)) {
229+
if (de.uka.ilkd.key.logic.op.Operator.opEquals(formula.op(), operator)) {
228230
if (result != null) {
229231
throw new IllegalStateException(
230232
"Result predicate found multiple times in succedent.");
@@ -271,7 +273,7 @@ private static Term constructResultIfContained(Services services,
271273

272274
private static Term constructResultIfContained(Services services, Term term,
273275
Operator operator) {
274-
if (Operator.opEquals(term.op(), operator)) {
276+
if (de.uka.ilkd.key.logic.op.Operator.opEquals(term.op(), operator)) {
275277
return term.sub(0);
276278
} else {
277279
Term result = null;
@@ -299,7 +301,8 @@ private static Term constructResultIfContained(Services services, Term term,
299301

300302
private static boolean isOperatorASequentFormula(Sequent sequent, final Operator operator) {
301303
return CollectionUtil.search(sequent,
302-
element -> Operator.opEquals(element.formula().op(), operator)) != null;
304+
element -> de.uka.ilkd.key.logic.op.Operator.opEquals(element.formula().op(),
305+
operator)) != null;
303306
}
304307

305308
/**
@@ -314,10 +317,10 @@ public static void addNewNamesToNamespace(Services services, Term term) {
314317
final Namespace<IProgramVariable> progVars = services.getNamespaces().programVariables();
315318
// LogicVariables are always local bound
316319
term.execPreOrder((DefaultVisitor) visited -> {
317-
if (visited.op() instanceof Function) {
318-
functions.add((Function) visited.op());
319-
} else if (visited.op() instanceof IProgramVariable) {
320-
progVars.add((IProgramVariable) visited.op());
320+
if (visited.op() instanceof Function function) {
321+
functions.add(function);
322+
} else if (visited.op() instanceof IProgramVariable progVar) {
323+
progVars.add(progVar);
321324
}
322325
});
323326
}
@@ -362,7 +365,7 @@ protected static class ContainsModalityOrQueryVisitor implements DefaultVisitor
362365
* {@inheritDoc}
363366
*/
364367
@Override
365-
public void visit(Term visited) {
368+
public void visit(org.key_project.logic.Term visited) {
366369
if (visited.op() instanceof Modality) {
367370
containsModalityOrQuery = true;
368371
} else if (visited.op() instanceof IProgramMethod) {
@@ -389,16 +392,14 @@ public boolean isContainsModalityOrQuery() {
389392
* @param sequentToProve The {@link Sequent} to extract relevant things from.
390393
* @return The found relevant things.
391394
*/
392-
public static Set<Operator> extractRelevantThings(final Services services,
395+
public static Set<Operator> extractRelevantThings(
396+
final Services services,
393397
Sequent sequentToProve) {
394398
final Set<Operator> result = new HashSet<>();
395399
for (SequentFormula sf : sequentToProve) {
396-
sf.formula().execPreOrder(new DefaultVisitor() {
397-
@Override
398-
public void visit(Term visited) {
399-
if (isRelevantThing(services, visited)) {
400-
result.add(visited.op());
401-
}
400+
sf.formula().execPreOrder((DefaultVisitor) visited -> {
401+
if (isRelevantThing(services, visited)) {
402+
result.add(visited.op());
402403
}
403404
});
404405
}
@@ -417,7 +418,7 @@ public void visit(Term visited) {
417418
* @param term The {@link Term} to check.
418419
* @return {@code true} is relevant thing, {@code false} is not relevant.
419420
*/
420-
private static boolean isRelevantThing(Services services, Term term) {
421+
private static boolean isRelevantThing(Services services, org.key_project.logic.Term term) {
421422
if (term.op() instanceof IProgramVariable) {
422423
return true;
423424
} else if (term.op() instanceof Function) {
@@ -526,7 +527,8 @@ protected static class ContainsIrrelevantThingsVisitor implements DefaultVisitor
526527
* @param services The {@link Services} to use.
527528
* @param relevantThings The relevant things.
528529
*/
529-
public ContainsIrrelevantThingsVisitor(Services services, Set<Operator> relevantThings) {
530+
public ContainsIrrelevantThingsVisitor(Services services,
531+
Set<Operator> relevantThings) {
530532
this.services = services;
531533
this.relevantThings = relevantThings;
532534
}
@@ -535,7 +537,7 @@ public ContainsIrrelevantThingsVisitor(Services services, Set<Operator> relevant
535537
* {@inheritDoc}
536538
*/
537539
@Override
538-
public void visit(Term visited) {
540+
public void visit(org.key_project.logic.Term visited) {
539541
if (isRelevantThing(services, visited)) {
540542
if (!SymbolicExecutionUtil.isSelect(services, visited)
541543
&& !SymbolicExecutionUtil.isBoolean(services, visited.op())

‎key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java‎

Lines changed: 17 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -1301,7 +1301,7 @@ public static SymbolicExecutionTermLabel getSymbolicExecutionLabel(
13011301
* contain a {@link SymbolicExecutionTermLabel} or the given {@link Term} is
13021302
* {@code null}.
13031303
*/
1304-
public static boolean hasSymbolicExecutionLabel(Term term) {
1304+
public static boolean hasSymbolicExecutionLabel(org.key_project.logic.Term term) {
13051305
return getSymbolicExecutionLabel(term) != null;
13061306
}
13071307

@@ -1312,10 +1312,11 @@ public static boolean hasSymbolicExecutionLabel(Term term) {
13121312
* @return The first found {@link SymbolicExecutionTermLabel} or {@code null} if no
13131313
* {@link SymbolicExecutionTermLabel} is provided.
13141314
*/
1315-
public static SymbolicExecutionTermLabel getSymbolicExecutionLabel(Term term) {
1316-
if (term != null) {
1317-
term = TermBuilder.goBelowUpdates(term);
1318-
return (SymbolicExecutionTermLabel) CollectionUtil.search(term.getLabels(),
1315+
public static SymbolicExecutionTermLabel getSymbolicExecutionLabel(
1316+
org.key_project.logic.Term term) {
1317+
if (term instanceof Term jTerm) {
1318+
jTerm = TermBuilder.goBelowUpdates(jTerm);
1319+
return (SymbolicExecutionTermLabel) CollectionUtil.search(jTerm.getLabels(),
13191320
element -> element instanceof SymbolicExecutionTermLabel);
13201321
} else {
13211322
return null;
@@ -1541,7 +1542,7 @@ public FindModalityWithSymbolicExecutionLabelId(boolean maximum) {
15411542
* {@inheritDoc}
15421543
*/
15431544
@Override
1544-
public void visit(Term visited) {
1545+
public void visit(org.key_project.logic.Term visited) {
15451546
SymbolicExecutionTermLabel label = getSymbolicExecutionLabel(visited);
15461547
if (label != null) {
15471548
if (posInTerm == null
@@ -1556,7 +1557,7 @@ public void visit(Term visited) {
15561557
* {@inheritDoc}
15571558
*/
15581559
@Override
1559-
public void subtreeEntered(Term subtreeRoot) {
1560+
public void subtreeEntered(org.key_project.logic.Term subtreeRoot) {
15601561
if (currentPosInTerm == null) {
15611562
currentPosInTerm = PosInTerm.getTopLevel();
15621563
} else {
@@ -1570,7 +1571,7 @@ public void subtreeEntered(Term subtreeRoot) {
15701571
* {@inheritDoc}
15711572
*/
15721573
@Override
1573-
public void subtreeLeft(Term subtreeRoot) {
1574+
public void subtreeLeft(org.key_project.logic.Term subtreeRoot) {
15741575
currentPosInTerm = currentPosInTerm.up();
15751576
indexStack.removeFirst();
15761577
if (!indexStack.isEmpty()) {
@@ -3257,12 +3258,10 @@ private static Set<Term> collectSkolemConstants(Sequent sequent, Term term) {
32573258
*/
32583259
private static Set<Term> collectSkolemConstantsNonRecursive(Term term) {
32593260
final Set<Term> result = new HashSet<>();
3260-
term.execPreOrder(new DefaultVisitor() {
3261-
@Override
3262-
public void visit(Term visited) {
3263-
if (isSkolemConstant(visited)) {
3264-
result.add(visited);
3265-
}
3261+
term.execPreOrder((DefaultVisitor) visited -> {
3262+
final Term visitedTerm = (Term) visited;
3263+
if (isSkolemConstant(visitedTerm)) {
3264+
result.add(visitedTerm);
32663265
}
32673266
});
32683267
return result;
@@ -3803,7 +3802,7 @@ public static boolean isChoiceSettingInitialised() {
38033802
* Checks if the given node should be represented as loop body termination.
38043803
*
38053804
* @param node The current {@link Node} in the proof tree of KeY.
3806-
* @param ruleApp The {@link RuleApp} may used or not used in the rule.
3805+
* @param ruleApp The {@link RuleApp} may or may not be used in the rule.
38073806
* @return {@code true} represent node as loop body termination, {@code false} represent node as
38083807
* something else.
38093808
*/
@@ -3839,7 +3838,7 @@ public static boolean isLoopBodyTermination(final Node node,
38393838
* @return {@code true} {@link Operator} is heap, {@code false} {@link Operator} is something
38403839
* else.
38413840
*/
3842-
public static boolean isHeap(Operator op, HeapLDT heapLDT) {
3841+
public static boolean isHeap(org.key_project.logic.op.Operator op, HeapLDT heapLDT) {
38433842
if (op instanceof final SortedOperator sortedOperator) {
38443843
final Sort opSort = sortedOperator.sort();
38453844
return CollectionUtil.search(heapLDT.getAllHeaps(),
@@ -3884,7 +3883,7 @@ public static boolean isSelect(Services services, org.key_project.logic.Term ter
38843883
* @param op The {@link Operator} to check.
38853884
* @return {@code true} is number, {@code false} is something else.
38863885
*/
3887-
public static boolean isNumber(Operator op) {
3886+
public static boolean isNumber(org.key_project.logic.op.Operator op) {
38883887
if (op instanceof Function) {
38893888
String[] numbers =
38903889
{ "#", "0", "1", "2", "3", "4", "5", "6", "7", "8", "9", "Z", "neglit" };
@@ -3902,7 +3901,7 @@ public static boolean isNumber(Operator op) {
39023901
* @param op The {@link Operator} to check.
39033902
* @return {@code true} is boolean, {@code false} is something else.
39043903
*/
3905-
public static boolean isBoolean(Services services, Operator op) {
3904+
public static boolean isBoolean(Services services, org.key_project.logic.op.Operator op) {
39063905
BooleanLDT booleanLDT = services.getTypeConverter().getBooleanLDT();
39073906
return booleanLDT.getFalseConst() == op || booleanLDT.getTrueConst() == op;
39083907
}

0 commit comments

Comments
 (0)