Skip to content

Commit f8f38d0

Browse files
wadoonwadoon
committed
spotless
1 parent aebcce2 commit f8f38d0

57 files changed

Lines changed: 716 additions & 635 deletions

Some content is hidden

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

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

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,6 @@
2323
import de.uka.ilkd.key.speclang.HeapContext;
2424
import de.uka.ilkd.key.speclang.SpecificationElement;
2525

26-
import org.jspecify.annotations.Nullable;
2726
import org.key_project.logic.Name;
2827
import org.key_project.logic.sort.Sort;
2928
import org.key_project.util.LRUCache;

‎key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/JmlAssert.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,9 +11,9 @@
1111
import de.uka.ilkd.key.logic.op.LocationVariable;
1212
import de.uka.ilkd.key.nparser.KeyAst;
1313
import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLAssertStatement;
14-
1514
import de.uka.ilkd.key.speclang.njml.JmlIO;
1615
import de.uka.ilkd.key.speclang.njml.JmlParser;
16+
1717
import org.key_project.util.ExtList;
1818
import org.key_project.util.collection.ImmutableList;
1919

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

Lines changed: 48 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -33,8 +33,8 @@
3333
import de.uka.ilkd.key.speclang.njml.JmlParser.ProofArgContext;
3434
import de.uka.ilkd.key.speclang.njml.JmlParser.ProofCmdCaseContext;
3535
import de.uka.ilkd.key.speclang.njml.JmlParser.ProofCmdContext;
36-
3736
import de.uka.ilkd.key.util.MiscTools;
37+
3838
import org.key_project.logic.Term;
3939
import org.key_project.logic.op.Modality;
4040
import org.key_project.prover.engine.ProverTaskListener;
@@ -90,12 +90,14 @@ JTerm resolve(Map<LocationVariable, JFunction> obtainMap, Services services) {
9090
return result;
9191
}
9292

93-
private void assertNoObtainVarsLeft(JTerm term, Map<LocationVariable, JFunction> obtainMap) {
93+
private void assertNoObtainVarsLeft(JTerm term,
94+
Map<LocationVariable, JFunction> obtainMap) {
9495
var v = new DefaultVisitor() {
9596
@Override
9697
public void visit(Term visited) {
97-
if(obtainMap.containsKey(term.op())) {
98-
throw new RuntimeException("Use of obtain variable before it being obtained: " + term.op());
98+
if (obtainMap.containsKey(term.op())) {
99+
throw new RuntimeException(
100+
"Use of obtain variable before it being obtained: " + term.op());
99101
}
100102
}
101103
};
@@ -133,17 +135,19 @@ private static JmlAssert getJmlAssert(Node node) {
133135
}
134136

135137
private static void collectUpdates(JTerm update, Map<JTerm, JTerm> updates, Services services) {
136-
switch(update.op()) {
138+
switch (update.op()) {
137139
case ElementaryUpdate eu ->
138-
updates.put(services.getTermBuilder().var((ProgramVariable) eu.lhs()), update.sub(0));
140+
updates.put(services.getTermBuilder().var((ProgramVariable) eu.lhs()),
141+
update.sub(0));
139142

140-
case UpdateJunctor uj-> {
143+
case UpdateJunctor uj -> {
141144
collectUpdates(update.sub(0), updates, services);
142145
collectUpdates(update.sub(1), updates, services);
143146
}
144147

145148
default ->
146-
throw new IllegalStateException("Unexpected update operation: " + update.op().getClass());
149+
throw new IllegalStateException(
150+
"Unexpected update operation: " + update.op().getClass());
147151
}
148152
}
149153

@@ -177,22 +181,27 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof,
177181
"Running attached script from goal " + goal.node().serialNr(), 0));
178182

179183
KeyAst.JMLProofScript proofScript = jmlAssert.getAssertionProof();
180-
Map<ParserRuleContext, JTerm> termMap = getTermMap(jmlAssert, getJavaBlock(goal), proof.getServices());
181-
// We heavily rely on that variables have been computed before, otherwise this will raise an NPE.
182-
Map<LocationVariable, JFunction> obtainMap = makeObtainVarMap(jmlAssert.collectVariablesInProof(null));
183-
@Nullable OpReplacer updateReplacer = getUpdateReplacer(goal);
184+
Map<ParserRuleContext, JTerm> termMap =
185+
getTermMap(jmlAssert, getJavaBlock(goal), proof.getServices());
186+
// We heavily rely on that variables have been computed before, otherwise this will
187+
// raise an NPE.
188+
Map<LocationVariable, JFunction> obtainMap =
189+
makeObtainVarMap(jmlAssert.collectVariablesInProof(null));
190+
@Nullable
191+
OpReplacer updateReplacer = getUpdateReplacer(goal);
184192
List<ScriptCommandAst> renderedProof =
185193
renderProof(proofScript, termMap, updateReplacer, proof.getServices());
186194
ProofScriptEngine pse = new ProofScriptEngine(proof);
187195
pse.setInitiallySelectedGoal(goal);
188196
pse.getStateMap().putUserData("jml.obtainVarMap", obtainMap);
189197
pse.getStateMap().getValueInjector().addConverter(JTerm.class, ObtainAwareTerm.class,
190-
oat -> oat.resolve(obtainMap, goal.proof().getServices()));
198+
oat -> oat.resolve(obtainMap, goal.proof().getServices()));
191199
// TODO: Perhaps have holes also in JML?
192-
pse.getStateMap().getValueInjector().addConverter(TermWithHoles.class, ObtainAwareTerm.class,
193-
oat -> new TermWithHoles(oat.resolve(obtainMap, goal.proof().getServices())));
200+
pse.getStateMap().getValueInjector().addConverter(TermWithHoles.class,
201+
ObtainAwareTerm.class,
202+
oat -> new TermWithHoles(oat.resolve(obtainMap, goal.proof().getServices())));
194203
pse.getStateMap().getValueInjector().addConverter(boolean.class, ObtainAwareTerm.class,
195-
oat -> Boolean.parseBoolean(oat.term.toString()));
204+
oat -> Boolean.parseBoolean(oat.term.toString()));
196205
LOGGER.debug("---- Script");
197206
LOGGER.debug(renderedProof.stream().map(ScriptCommandAst::asCommandLine)
198207
.collect(Collectors.joining("\n")));
@@ -216,7 +225,8 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof,
216225
}
217226

218227

219-
private Map<ParserRuleContext, JTerm> getTermMap(JmlAssert jmlAssert, JavaBlock javaBlock, Services services) {
228+
private Map<ParserRuleContext, JTerm> getTermMap(JmlAssert jmlAssert, JavaBlock javaBlock,
229+
Services services) {
220230
SpecificationRepository.@Nullable JmlStatementSpec jmlspec =
221231
services.getSpecificationRepository().getStatementSpec(jmlAssert);
222232
if (jmlspec == null) {
@@ -237,17 +247,20 @@ private Map<ParserRuleContext, JTerm> getTermMap(JmlAssert jmlAssert, JavaBlock
237247
}
238248

239249
/**
240-
* For some reason, the self variable in the spec is not the same as the self variable and needs to
250+
* For some reason, the self variable in the spec is not the same as the self variable and needs
251+
* to
241252
* be corrected.
242253
*/
243-
private JTerm correctSelfVar(int index, JavaBlock javaBlock, SpecificationRepository.JmlStatementSpec spec, Services services) {
254+
private JTerm correctSelfVar(int index, JavaBlock javaBlock,
255+
SpecificationRepository.JmlStatementSpec spec, Services services) {
244256
final MethodFrame frame = JavaTools.getInnermostMethodFrame(javaBlock, services);
245257
final JTerm self = MiscTools.getSelfTerm(frame, services);
246258
return spec.getTerm(services, self, index);
247259

248260
}
249261

250-
private Map<LocationVariable, JFunction> makeObtainVarMap(ImmutableList<LocationVariable> locationVariables) {
262+
private Map<LocationVariable, JFunction> makeObtainVarMap(
263+
ImmutableList<LocationVariable> locationVariables) {
251264
HashMap<LocationVariable, JFunction> result = new HashMap<>();
252265
for (LocationVariable lv : locationVariables) {
253266
result.put(lv, null);
@@ -256,7 +269,8 @@ private Map<LocationVariable, JFunction> makeObtainVarMap(ImmutableList<Location
256269
}
257270

258271
private static List<ScriptCommandAst> renderProof(KeyAst.JMLProofScript script,
259-
Map<ParserRuleContext, JTerm> termMap, @Nullable OpReplacer update, Services services) throws ScriptException {
272+
Map<ParserRuleContext, JTerm> termMap, @Nullable OpReplacer update, Services services)
273+
throws ScriptException {
260274
List<ScriptCommandAst> result = new ArrayList<>();
261275
// Push current settings onto the settings stack
262276
result.add(new ScriptCommandAst("set", Map.of("stack", "push"), List.of()));
@@ -271,15 +285,15 @@ private static List<ScriptCommandAst> renderProof(KeyAst.JMLProofScript script,
271285
}
272286

273287
private static List<ScriptCommandAst> renderProofCmd(ProofCmdContext ctx,
274-
Map<ParserRuleContext, JTerm> termMap,
275-
@Nullable OpReplacer update, Services services) throws ScriptException {
288+
Map<ParserRuleContext, JTerm> termMap,
289+
@Nullable OpReplacer update, Services services) throws ScriptException {
276290
List<ScriptCommandAst> result = new ArrayList<>();
277291

278292
// Push the current branch context
279293
result.add(new ScriptCommandAst("branches", Map.of(), List.of("push")));
280294

281295
// Compose the command itself
282-
if(ctx.obtain != null) {
296+
if (ctx.obtain != null) {
283297
ScriptCommandAst command = renderObtainCommand(ctx, termMap, update, services);
284298
result.add(command);
285299
} else {
@@ -289,7 +303,7 @@ private static List<ScriptCommandAst> renderProofCmd(ProofCmdContext ctx,
289303

290304
// handle followup proofCmd if present
291305
JmlParser.ProofCmdSuffixContext suffix = ctx.proofCmdSuffix();
292-
if(suffix != null) {
306+
if (suffix != null) {
293307
if (!suffix.proofCmd().isEmpty()) {
294308
result.add(new ScriptCommandAst("branches", Map.of(), List.of("single")));
295309
for (ProofCmdContext proofCmdContext : suffix.proofCmd()) {
@@ -301,7 +315,7 @@ private static List<ScriptCommandAst> renderProofCmd(ProofCmdContext ctx,
301315
for (ProofCmdCaseContext pcase : suffix.proofCmdCase()) {
302316
String label = StringUtil.stripQuotes(pcase.label.getText());
303317
result.add(new ScriptCommandAst("branches", Map.of("branch", label),
304-
List.of("select")));
318+
List.of("select")));
305319
for (ProofCmdContext proofCmdContext : pcase.proofCmd()) {
306320
result.addAll(renderProofCmd(proofCmdContext, termMap, update, services));
307321
}
@@ -314,11 +328,12 @@ private static List<ScriptCommandAst> renderProofCmd(ProofCmdContext ctx,
314328
return result;
315329
}
316330

317-
private static ScriptCommandAst renderObtainCommand(ProofCmdContext ctx, Map<ParserRuleContext, JTerm> termMap,
318-
@Nullable OpReplacer update, Services services) throws ScriptException {
331+
private static ScriptCommandAst renderObtainCommand(ProofCmdContext ctx,
332+
Map<ParserRuleContext, JTerm> termMap,
333+
@Nullable OpReplacer update, Services services) throws ScriptException {
319334
Map<String, Object> named = new HashMap<>();
320335

321-
String argName = switch(ctx.obtKind.getType()) {
336+
String argName = switch (ctx.obtKind.getType()) {
322337
case JmlLexer.SUCH_THAT -> "such_that";
323338
case JmlLexer.EQUAL_SINGLE -> "equals";
324339
case JmlLexer.FROM_GOAL -> "from_goal";
@@ -327,7 +342,7 @@ private static ScriptCommandAst renderObtainCommand(ProofCmdContext ctx, Map<Par
327342

328343
named.put("var", ctx.var.getText());
329344

330-
if(ctx.expression() == null) {
345+
if (ctx.expression() == null) {
331346
named.put(argName, true);
332347
} else {
333348
JmlParser.ExpressionContext exp = ctx.expression();
@@ -347,7 +362,8 @@ private static ScriptCommandAst renderObtainCommand(ProofCmdContext ctx, Map<Par
347362
return new ScriptCommandAst("__obtain", named, List.of(), Location.fromToken(ctx.start));
348363
}
349364

350-
private static @NonNull ScriptCommandAst renderRegularCommand(ProofCmdContext ctx, Map<ParserRuleContext, JTerm> termMap, @Nullable OpReplacer update, Services services) {
365+
private static @NonNull ScriptCommandAst renderRegularCommand(ProofCmdContext ctx,
366+
Map<ParserRuleContext, JTerm> termMap, @Nullable OpReplacer update, Services services) {
351367
Map<String, Object> named = new HashMap<>();
352368
List<Object> positional = new ArrayList<>();
353369
for (ProofArgContext argContext : ctx.proofArg()) {
@@ -372,7 +388,7 @@ private static ScriptCommandAst renderObtainCommand(ProofCmdContext ctx, Map<Par
372388
}
373389
}
374390
return new ScriptCommandAst(ctx.cmd.getText(), named, positional,
375-
Location.fromToken(ctx.start));
391+
Location.fromToken(ctx.start));
376392
}
377393

378394

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

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,8 @@
3434
*/
3535
public class ScriptAwarePrepMacro extends SequentialProofMacro {
3636

37-
private final ProofMacro autoMacro = new SymbolicExecutionOnlyMacro(); // new FinishSymbolicExecutionMacro();
37+
private final ProofMacro autoMacro = new SymbolicExecutionOnlyMacro(); // new
38+
// FinishSymbolicExecutionMacro();
3839
private final ApplyScriptsMacro applyMacro = new ApplyScriptsMacro(null);
3940

4041
@Override

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

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

6-
import de.uka.ilkd.key.control.TermLabelVisibilityManager;
6+
import java.io.IOException;
7+
import java.util.Arrays;
8+
import java.util.List;
9+
import java.util.Map;
10+
import java.util.WeakHashMap;
11+
712
import de.uka.ilkd.key.logic.op.Junctor;
8-
import de.uka.ilkd.key.logic.op.ObserverFunction;
913
import de.uka.ilkd.key.logic.op.UpdateApplication;
1014
import de.uka.ilkd.key.proof.Goal;
1115
import de.uka.ilkd.key.proof.Proof;
1216
import de.uka.ilkd.key.rule.*;
1317
import de.uka.ilkd.key.strategy.Strategy;
14-
import org.jspecify.annotations.NonNull;
18+
1519
import org.key_project.logic.Name;
1620
import org.key_project.logic.Term;
1721
import org.key_project.logic.op.Modality;
@@ -21,15 +25,9 @@
2125
import org.key_project.prover.sequent.PosInOccurrence;
2226
import org.key_project.prover.sequent.Sequent;
2327
import org.key_project.prover.sequent.SequentFormula;
24-
import org.key_project.prover.strategy.costbased.NumberRuleAppCost;
2528
import org.key_project.util.Streams;
26-
import org.key_project.util.java.StringUtil;
2729

28-
import java.io.IOException;
29-
import java.util.Arrays;
30-
import java.util.List;
31-
import java.util.Map;
32-
import java.util.WeakHashMap;
30+
import org.jspecify.annotations.NonNull;
3331

3432
/**
3533
* This macro is very restritive in which rules are allowed to be applied for symbolic
@@ -44,11 +42,16 @@ public class SymbolicExecutionOnlyMacro extends StrategyProofMacro {
4442
static {
4543
try {
4644
ADMITTED_RULES = Arrays.asList(
47-
Streams.toString(SymbolicExecutionOnlyMacro.class.getResourceAsStream("SymbolicExecutionOnlyMacro.admittedRules.txt")).split("\n"));
45+
Streams.toString(SymbolicExecutionOnlyMacro.class
46+
.getResourceAsStream("SymbolicExecutionOnlyMacro.admittedRules.txt"))
47+
.split("\n"));
4848
ADMITTED_RULE_SETS = Arrays.asList(
49-
Streams.toString(SymbolicExecutionOnlyMacro.class.getResourceAsStream("SymbolicExecutionOnlyMacro.admittedRuleSets.txt")).split("\n"));
49+
Streams.toString(SymbolicExecutionOnlyMacro.class
50+
.getResourceAsStream("SymbolicExecutionOnlyMacro.admittedRuleSets.txt"))
51+
.split("\n"));
5052
} catch (IOException e) {
51-
throw new RuntimeException("Failed to load admitted rules for symbolic execution macro.", e);
53+
throw new RuntimeException(
54+
"Failed to load admitted rules for symbolic execution macro.", e);
5255
}
5356
}
5457

@@ -93,11 +96,11 @@ public static boolean isAdmittedRule(RuleApp ruleApp) {
9396
}
9497
}
9598

96-
if("ifthenelse_split_for".equals(name)) {
99+
if ("ifthenelse_split_for".equals(name)) {
97100
Term iteTerm = ruleApp.posInOccurrence().subTerm();
98101
Term then = iteTerm.sub(1);
99102
Term elze = iteTerm.sub(2);
100-
if(isUpdatedModality(then) && isUpdatedModality(elze)) {
103+
if (isUpdatedModality(then) && isUpdatedModality(elze)) {
101104
return true;
102105
}
103106
}
@@ -111,10 +114,10 @@ public static boolean isAdmittedRule(RuleApp ruleApp) {
111114
}
112115
}
113116

114-
if(rule instanceof UseOperationContractRule ||
117+
if (rule instanceof UseOperationContractRule ||
115118
rule instanceof JmlAssertRule ||
116119
rule instanceof WhileInvariantRule ||
117-
rule instanceof LoopScopeInvariantRule )
120+
rule instanceof LoopScopeInvariantRule)
118121
return true;
119122

120123
return false;
@@ -124,13 +127,14 @@ public static boolean isAdmittedRule(RuleApp ruleApp) {
124127
* return true if there is a boolean combination of updated modalities
125128
*/
126129
private static boolean isUpdatedModality(Term term) {
127-
while(term.op() instanceof UpdateApplication) {
130+
while (term.op() instanceof UpdateApplication) {
128131
term = term.sub(1);
129132
}
130-
if(term.op() instanceof Modality) {;
133+
if (term.op() instanceof Modality) {
134+
;
131135
return true;
132136
}
133-
if(term.op() == Junctor.IMP || term.op() == Junctor.AND) {
137+
if (term.op() == Junctor.IMP || term.op() == Junctor.AND) {
134138
return term.subs().stream().allMatch(SymbolicExecutionOnlyMacro::isUpdatedModality);
135139
}
136140
return false;
@@ -152,7 +156,7 @@ public Name name() {
152156

153157
@Override
154158
public boolean isApprovedApp(RuleApp app, PosInOccurrence pio, Goal goal) {
155-
if(!hasModality(goal) || isThrowNullBranch(goal)) {
159+
if (!hasModality(goal) || isThrowNullBranch(goal)) {
156160
return false;
157161
}
158162
return isAdmittedRule(app) && super.isApprovedApp(app, pio, goal);
@@ -178,7 +182,7 @@ private boolean hasModality(Sequent seq) {
178182
}
179183

180184
private boolean hasModality(Term term) {
181-
if(term.op() instanceof Modality) {
185+
if (term.op() instanceof Modality) {
182186
return true;
183187
}
184188
return term.subs().stream().anyMatch(this::hasModality);

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

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,14 @@
11
/* This file is part of KeY - https://key-project.org
22
* KeY is licensed under the GNU General Public License Version 2
33
* SPDX-License-Identifier: GPL-2.0-only */
4-
54
package de.uka.ilkd.key.macros;
65

76

87
import de.uka.ilkd.key.control.UserInterfaceControl;
98
import de.uka.ilkd.key.proof.Goal;
109
import de.uka.ilkd.key.proof.Node;
1110
import de.uka.ilkd.key.proof.Proof;
11+
1212
import org.key_project.prover.engine.ProverTaskListener;
1313
import org.key_project.prover.sequent.PosInOccurrence;
1414
import org.key_project.util.collection.ImmutableList;
@@ -63,11 +63,11 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic,
6363

6464
private static boolean isSideGoal(Goal g) {
6565
Node node = g.node();
66-
while (node != null && node.getNodeInfo() != null
67-
&& node.getNodeInfo().getBranchLabel() != null) {
68-
String label = node.getNodeInfo().getBranchLabel();
66+
while (node != null && node.getNodeInfo() != null
67+
&& node.getNodeInfo().getBranchLabel() != null) {
68+
String label = node.getNodeInfo().getBranchLabel();
6969
if (label.contains("Null Reference")
70-
|| label.contains("Index Out of Bounds")) {
70+
|| label.contains("Index Out of Bounds")) {
7171
return true;
7272
}
7373
node = node.parent();

0 commit comments

Comments
 (0)