Skip to content

Commit 71edf0e

Browse files
wadoonwadoon
authored
Backport of KEY-2.12.1 into main (#3296)
Backporting the bug fixes in KEY-2.12.1 to main. This PR supersedes #3251 to avoid merge conflicts due to file header changes. Necessary changes were cherry-picked.
2 parents d48057e + a302071 commit 71edf0e

24 files changed

Lines changed: 200 additions & 32 deletions

File tree

‎build.gradle‎

Lines changed: 0 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -32,16 +32,6 @@ idea {
3232
}
3333
}
3434

35-
// Helper function that calls "git rev-parse" to
36-
// find names/SHAs for commits
37-
static def gitRevParse(String args) {
38-
try {
39-
return "git rev-parse $args".execute().text.trim()
40-
} catch (Exception e) {
41-
return ""
42-
}
43-
}
44-
4535
static def getDate() {
4636
return new Date().format('yyyyMMdd')
4737
}

‎key.core/build.gradle‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -178,6 +178,7 @@ task generateVersionFiles() {
178178
def branch = new File(outputFolder, "branch")
179179
def versionf = new File(outputFolder, "version")
180180

181+
inputs.files "$project.rootDir/.git/HEAD"
181182
outputs.files sha1, branch, versionf
182183

183184
def gitRevision = gitRevParse('HEAD')
@@ -190,6 +191,16 @@ task generateVersionFiles() {
190191
}
191192
}
192193

194+
// Helper function that calls "git rev-parse" to
195+
// find names/SHAs for commits
196+
static def gitRevParse(String args) {
197+
try {
198+
return "git rev-parse $args".execute().text.trim()
199+
} catch (Exception e) {
200+
return ""
201+
}
202+
}
203+
193204
// @AW: Say something here. From POV this explain by itself.
194205
processResources.dependsOn generateVersionFiles, generateSolverPropsList, generateSMTListings
195206

‎key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -318,5 +318,4 @@ public boolean isDisposed() {
318318
public Pair<String, Location> getProofScript() {
319319
return proofScript;
320320
}
321-
322321
}

‎key.core/src/main/java/de/uka/ilkd/key/java/Services.java‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@
1414
import de.uka.ilkd.key.proof.init.InitConfig;
1515
import de.uka.ilkd.key.proof.init.Profile;
1616
import de.uka.ilkd.key.proof.mgt.SpecificationRepository;
17+
import de.uka.ilkd.key.settings.ProofIndependentSettings;
1718
import de.uka.ilkd.key.util.Debug;
1819
import de.uka.ilkd.key.util.KeYRecoderExcHandler;
1920

@@ -298,6 +299,10 @@ public void setProof(Proof p_proof) {
298299
"Services are already owned by another proof:" + proof.name());
299300
}
300301
proof = p_proof;
302+
if (!ProofIndependentSettings.DEFAULT_INSTANCE.getTermLabelSettings().getUseOriginLabels()
303+
|| !proof.getSettings().getTermLabelSettings().getUseOriginLabels()) {
304+
profile.getTermLabelManager().disableOriginLabelRefactorings();
305+
}
301306
}
302307

303308

‎key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabelManager.java‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,8 @@
55

66
import java.util.*;
77
import java.util.Map.Entry;
8+
import java.util.Set;
9+
import java.util.stream.Collectors;
810

911
import de.uka.ilkd.key.java.Services;
1012
import de.uka.ilkd.key.logic.*;
@@ -16,6 +18,11 @@
1618
import de.uka.ilkd.key.rule.Rule;
1719
import de.uka.ilkd.key.rule.RuleApp;
1820
import de.uka.ilkd.key.rule.label.*;
21+
import de.uka.ilkd.key.rule.label.ChildTermLabelPolicy;
22+
import de.uka.ilkd.key.rule.label.OriginTermLabelRefactoring;
23+
import de.uka.ilkd.key.rule.label.TermLabelMerger;
24+
import de.uka.ilkd.key.rule.label.TermLabelPolicy;
25+
import de.uka.ilkd.key.rule.label.TermLabelRefactoring;
1926
import de.uka.ilkd.key.rule.label.TermLabelRefactoring.RefactoringScope;
2027
import de.uka.ilkd.key.util.LinkedHashMap;
2128
import de.uka.ilkd.key.util.Pair;
@@ -2194,4 +2201,14 @@ protected void mergeLabels(SequentChangeInfo currentSequent, Services services,
21942201
}
21952202
}
21962203
}
2204+
2205+
/**
2206+
* Fully disable origin tracking. This will remove the {@link OriginTermLabelRefactoring} from
2207+
* the manager.
2208+
*/
2209+
public void disableOriginLabelRefactorings() {
2210+
allRulesRefactorings = ImmutableList.fromList(
2211+
allRulesRefactorings.stream().filter(x -> !(x instanceof OriginTermLabelRefactoring))
2212+
.collect(Collectors.toList()));
2213+
}
21972214
}

‎key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacroFinishedInfo.java‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,9 +4,11 @@
44
package de.uka.ilkd.key.macros;
55

66
import java.util.HashMap;
7+
import java.util.List;
78
import java.util.Map;
89

910
import de.uka.ilkd.key.proof.Goal;
11+
import de.uka.ilkd.key.proof.Node;
1012
import de.uka.ilkd.key.proof.Proof;
1113
import de.uka.ilkd.key.proof.Statistics;
1214
import de.uka.ilkd.key.prover.impl.ApplyStrategyInfo;
@@ -70,6 +72,12 @@ public ProofMacroFinishedInfo(ProofMacro macro, ImmutableList<Goal> goals) {
7072
this(macro, goals, goals.isEmpty() ? null : goals.head().proof(), false);
7173
}
7274

75+
public ProofMacroFinishedInfo(ProofMacro macro, ImmutableList<Goal> goals,
76+
List<Node> statisticNodes) {
77+
this(macro, goals, goals.isEmpty() ? null : goals.head().proof(),
78+
statisticNodes.isEmpty() ? null : new Statistics(statisticNodes));
79+
}
80+
7381
public ProofMacroFinishedInfo(ProofMacro macro, Proof proof) {
7482
this(macro, proof.openEnabledGoals(), proof, false);
7583
}

‎key.core/src/main/java/de/uka/ilkd/key/macros/StrategyProofMacro.java‎

Lines changed: 11 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,13 @@
33
* SPDX-License-Identifier: GPL-2.0-only */
44
package de.uka.ilkd.key.macros;
55

6+
import java.util.List;
7+
import java.util.stream.Collectors;
8+
69
import de.uka.ilkd.key.control.UserInterfaceControl;
710
import de.uka.ilkd.key.logic.PosInOccurrence;
811
import de.uka.ilkd.key.proof.Goal;
12+
import de.uka.ilkd.key.proof.Node;
913
import de.uka.ilkd.key.proof.Proof;
1014
import de.uka.ilkd.key.prover.GoalChooser;
1115
import de.uka.ilkd.key.prover.ProverCore;
@@ -72,6 +76,7 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof,
7276
// false
7377
return null;
7478
}
79+
List<Node> nodes = goals.stream().map(Goal::node).collect(Collectors.toList());
7580

7681
final GoalChooser goalChooser =
7782
proof.getInitConfig().getProfile().getSelectedGoalChooserBuilder().create();
@@ -84,9 +89,9 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof,
8489
new ProgressBarListener(goals.size(), getMaxSteps(proof), listener);
8590
applyStrategy.addProverTaskObserver(pml);
8691
// add a focus manager if there is a focus
87-
if (posInOcc != null && goals != null) {
88-
AutomatedRuleApplicationManager realManager = null;
89-
FocussedRuleApplicationManager manager = null;
92+
if (posInOcc != null) {
93+
AutomatedRuleApplicationManager realManager;
94+
FocussedRuleApplicationManager manager;
9095
for (Goal goal : goals) {
9196
realManager = goal.getRuleAppManager();
9297
realManager.clearCache();
@@ -99,7 +104,7 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof,
99104
Strategy oldStrategy = proof.getActiveStrategy();
100105
proof.setActiveStrategy(createStrategy(proof, posInOcc));
101106

102-
ProofMacroFinishedInfo info = new ProofMacroFinishedInfo(this, goals, proof, false);
107+
ProofMacroFinishedInfo info;
103108
try {
104109
// find the relevant goals
105110
// and start
@@ -125,7 +130,8 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof,
125130
}
126131
final ImmutableList<Goal> resultingGoals =
127132
setDifference(proof.openGoals(), ignoredOpenGoals);
128-
info = new ProofMacroFinishedInfo(this, resultingGoals);
133+
info = new ProofMacroFinishedInfo(this, resultingGoals,
134+
nodes);
129135
proof.setActiveStrategy(oldStrategy);
130136
doPostProcessing(proof);
131137
applyStrategy.removeProverTaskObserver(pml);

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

Lines changed: 72 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -73,6 +73,78 @@ protected Statistics(int nodes, int branches, int cachedBranches, int interactiv
7373
this.timePerStepInMillis = timePerStepInMillis;
7474
}
7575

76+
public Statistics(List<Node> startNodes) {
77+
if (startNodes.isEmpty()) {
78+
throw new IllegalArgumentException("can't generate statistics on zero nodes");
79+
}
80+
81+
int nodes = 0;
82+
int branches = 0;
83+
int cachedBranches = 0;
84+
int interactiveSteps = 0;
85+
int symbExApps = 0;
86+
int quantifierInstantiations = 0;
87+
int ossApps = 0;
88+
int mergeRuleApps = 0;
89+
int totalRuleApps = 0;
90+
int smtSolverApps = 0;
91+
int dependencyContractApps = 0;
92+
int operationContractApps = 0;
93+
int blockLoopContractApps = 0;
94+
int loopInvApps = 0;
95+
long autoModeTimeInMillis = 0;
96+
long timeInMillis = 0;
97+
98+
for (Node startNode : startNodes) {
99+
final Iterator<Node> it = startNode.subtreeIterator();
100+
101+
TemporaryStatistics tmp = new TemporaryStatistics();
102+
103+
Node node;
104+
while (it.hasNext()) {
105+
node = it.next();
106+
tmp.changeOnNode(node, interactiveAppsDetails);
107+
}
108+
109+
nodes += tmp.nodes;
110+
branches = tmp.branches;
111+
cachedBranches = tmp.cachedBranches;
112+
interactiveSteps = tmp.interactive;
113+
symbExApps = tmp.symbExApps;
114+
quantifierInstantiations = tmp.quant;
115+
ossApps = tmp.oss;
116+
mergeRuleApps = tmp.mergeApps;
117+
totalRuleApps = tmp.nodes + tmp.ossCaptured - 1;
118+
smtSolverApps = tmp.smt;
119+
dependencyContractApps = tmp.dep;
120+
operationContractApps = tmp.contr;
121+
blockLoopContractApps = tmp.block;
122+
loopInvApps = tmp.inv;
123+
autoModeTimeInMillis = startNode.proof().getAutoModeTime();
124+
timeInMillis = (System.currentTimeMillis() - startNode.proof().creationTime);
125+
}
126+
127+
this.nodes = nodes;
128+
this.branches = branches;
129+
this.cachedBranches = cachedBranches;
130+
this.interactiveSteps = interactiveSteps;
131+
this.symbExApps = symbExApps;
132+
this.quantifierInstantiations = quantifierInstantiations;
133+
this.ossApps = ossApps;
134+
this.mergeRuleApps = mergeRuleApps;
135+
this.totalRuleApps = totalRuleApps;
136+
this.smtSolverApps = smtSolverApps;
137+
this.dependencyContractApps = dependencyContractApps;
138+
this.operationContractApps = operationContractApps;
139+
this.blockLoopContractApps = blockLoopContractApps;
140+
this.loopInvApps = loopInvApps;
141+
this.autoModeTimeInMillis = autoModeTimeInMillis;
142+
this.timeInMillis = timeInMillis;
143+
this.timePerStepInMillis = nodes <= 1 ? .0f : (autoModeTimeInMillis / (float) (nodes - 1));
144+
145+
generateSummary(startNodes.get(0).proof());
146+
}
147+
76148
Statistics(Node startNode) {
77149
final Iterator<Node> it = startNode.subtreeIterator();
78150

‎key.core/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -92,7 +92,7 @@ public static ClosedBy findPreviousProof(DefaultListModel<Proof> previousProofs,
9292
// for each node, check that the sequent in the reference is
9393
// a subset of the new sequent
9494
Node n = nodesToCheck.remove();
95-
if (checkedNodes.contains(n)) {
95+
if (checkedNodes.contains(n) || !n.isClosed()) {
9696
continue;
9797
}
9898
checkedNodes.add(n);

‎key.core/src/main/java/de/uka/ilkd/key/smt/communication/ExternalProcessLauncher.java‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -76,7 +76,9 @@ public void launch(final String[] command) throws IOException {
7676
*/
7777
public void stop() {
7878
if (process != null) {
79-
process.destroy();
79+
// make sure the solver process is properly killed,
80+
// otherwise it may consume excessive CPU and RAM
81+
process.destroyForcibly();
8082
}
8183
// TODO: where to close the pipe?
8284
// pipe.close();

0 commit comments

Comments
 (0)