Skip to content

Commit 9ef68b3

Browse files
unp1unp1
authored
Fix #3524 (#3525)
2 parents 9b32d97 + fa17636 commit 9ef68b3

File tree

14 files changed

+192
-29
lines changed

14 files changed

+192
-29
lines changed

‎key.core/src/main/antlr4/KeYLexer.g4‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -145,6 +145,7 @@ EQUAL_UNIQUE : '\\equalUnique';
145145
NEW : '\\new';
146146
NEW_TYPE_OF: '\\newTypeOf';
147147
NEW_DEPENDING_ON: '\\newDependingOn';
148+
NEW_LOCAL_VARS: '\\newLocalVars';
148149
HAS_ELEMENTARY_SORT:'\\hasElementarySort';
149150
NEWLABEL : '\\newLabel';
150151
CONTAINS_ASSIGNMENT : '\\containsAssignment';

‎key.core/src/main/antlr4/KeYParser.g4‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -688,6 +688,7 @@ varexpId: // weigl, 2021-03-12: This will be later just an arbitrary identifier.
688688
| NEW
689689
| NEW_TYPE_OF
690690
| NEW_DEPENDING_ON
691+
| NEW_LOCAL_VARS
691692
| HAS_ELEMENTARY_SORT
692693
| SAME
693694
| ISSUBTYPE

‎key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramReplaceVisitor.java‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@
33
* SPDX-License-Identifier: GPL-2.0-only */
44
package de.uka.ilkd.key.java.visitor;
55

6+
67
import de.uka.ilkd.key.java.ProgramElement;
78
import de.uka.ilkd.key.java.Services;
89
import de.uka.ilkd.key.java.SourceElement;
@@ -16,6 +17,7 @@
1617
import org.key_project.util.ExtList;
1718
import org.key_project.util.collection.ImmutableArray;
1819

20+
1921
/**
2022
* Walks through a java AST in depth-left-fist-order. This walker is used to transform a program
2123
* according to the given SVInstantiations.

‎key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -161,6 +161,8 @@ public void apply(TacletBuilder<?> tacletBuilder, Object[] arguments,
161161
}
162162
};
163163

164+
public static final TacletBuilderCommand NEW_LOCAL_VARS = new ConstructorBasedBuilder(
165+
"newLocalVars", NewLocalVarsCondition.class, SV, SV, SV, SV);
164166

165167
static class NotFreeInTacletBuilderCommand extends AbstractTacletBuilderCommand {
166168
public NotFreeInTacletBuilderCommand(@NonNull ArgumentType... argumentsTypes) {
@@ -367,7 +369,8 @@ public IsLabeledCondition build(Object[] arguments, List<String> parameters,
367369
// region Registry
368370
static {
369371
register(SAME_OBSERVER, SIMPLIFY_ITE_UPDATE, ABSTRACT_OR_INTERFACE, SAME, IS_SUBTYPE,
370-
STRICT, DISJOINT_MODULO_NULL, NEW_JAVATYPE, NEW_VAR, FREE_1, FREE_2, FREE_3, FREE_4,
372+
STRICT, DISJOINT_MODULO_NULL, NEW_JAVATYPE, NEW_VAR, NEW_LOCAL_VARS, FREE_1, FREE_2,
373+
FREE_3, FREE_4,
371374
FREE_5, NEW_TYPE_OF, NEW_DEPENDING_ON, FREE_LABEL_IN_VARIABLE, DIFFERENT, FINAL,
372375
ENUM_CONST, LOCAL_VARIABLE, ARRAY_LENGTH, ARRAY, REFERENCE_ARRAY, MAY_EXPAND_METHOD_2,
373376
MAY_EXPAND_METHOD_3, STATIC_METHOD, THIS_REFERENCE, REFERENCE, ENUM_TYPE,

‎key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewLocalVarsCondition.java‎

Lines changed: 111 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,111 @@
1+
/* This file is part of KeY - https://key-project.org
2+
* KeY is licensed under the GNU General Public License Version 2
3+
* SPDX-License-Identifier: GPL-2.0-only */
4+
package de.uka.ilkd.key.rule.conditions;
5+
6+
import java.util.ArrayList;
7+
import java.util.List;
8+
9+
import de.uka.ilkd.key.java.ProgramElement;
10+
import de.uka.ilkd.key.java.Services;
11+
import de.uka.ilkd.key.java.Statement;
12+
import de.uka.ilkd.key.java.abstraction.ArrayType;
13+
import de.uka.ilkd.key.java.abstraction.KeYJavaType;
14+
import de.uka.ilkd.key.java.declaration.LocalVariableDeclaration;
15+
import de.uka.ilkd.key.java.declaration.VariableDeclaration;
16+
import de.uka.ilkd.key.java.declaration.VariableSpecification;
17+
import de.uka.ilkd.key.java.reference.TypeRef;
18+
import de.uka.ilkd.key.logic.Term;
19+
import de.uka.ilkd.key.logic.op.LocationVariable;
20+
import de.uka.ilkd.key.logic.op.SchemaVariable;
21+
import de.uka.ilkd.key.rule.MatchConditions;
22+
import de.uka.ilkd.key.rule.VariableCondition;
23+
import de.uka.ilkd.key.rule.inst.ProgramList;
24+
import de.uka.ilkd.key.rule.inst.SVInstantiations;
25+
import de.uka.ilkd.key.util.MiscTools;
26+
27+
import org.key_project.logic.SyntaxElement;
28+
import org.key_project.util.collection.*;
29+
30+
/**
31+
* For the loop scope rule, if a local program variable that may be altered by the loop body appears
32+
* in the frame condition,
33+
* it is necessary to use the value <i>before</i> the loop first executes in the frame condition.
34+
* <br>
35+
* To achieve this, this condition generates (1) the "before" version of each variable that may be
36+
* written to by the loop
37+
* {@link MiscTools#getLocalOuts(ProgramElement, Services)}; (2) an update storing the value of each
38+
* such PV in its "before" version,
39+
* i.e., {@code {...||i_before := i||...}}; (3) the reverse of the update, to be applied to the
40+
* frame condition, i.e.,
41+
* {@code {...||i := i_before||...}}.
42+
*/
43+
public class NewLocalVarsCondition implements VariableCondition {
44+
/**
45+
* A SV that will store variable declarations for the "before" version of variables.
46+
*/
47+
private final SchemaVariable varDeclsSV;
48+
/**
49+
* Will store the update {@code {...||i_before := i||...}}.
50+
*/
51+
private final SchemaVariable updateBeforeSV;
52+
/**
53+
* Will store the update {@code {...||i := i_before||...}}.
54+
*/
55+
private final SchemaVariable updateFrameSV;
56+
/**
57+
* The loop body.
58+
*/
59+
private final SchemaVariable bodySV;
60+
61+
public NewLocalVarsCondition(SchemaVariable varDeclsSV, SchemaVariable updateBeforeSV,
62+
SchemaVariable updateFrameSV, SchemaVariable bodySV) {
63+
this.varDeclsSV = varDeclsSV;
64+
this.updateBeforeSV = updateBeforeSV;
65+
this.updateFrameSV = updateFrameSV;
66+
this.bodySV = bodySV;
67+
}
68+
69+
@Override
70+
public MatchConditions check(SchemaVariable var, SyntaxElement instCandidate,
71+
MatchConditions matchCond, Services services) {
72+
SVInstantiations svInst = matchCond.getInstantiations();
73+
if (svInst.getInstantiation(varDeclsSV) != null) {
74+
return matchCond;
75+
}
76+
var body = (Statement) svInst.getInstantiation(bodySV);
77+
if (body == null) {
78+
return matchCond;
79+
}
80+
81+
var vars = MiscTools.getLocalOuts(body, services);
82+
List<VariableDeclaration> decls = new ArrayList<>(vars.size());
83+
ImmutableList<Term> updatesBefore = ImmutableSLList.nil();
84+
ImmutableList<Term> updatesFrame = ImmutableSLList.nil();
85+
var tb = services.getTermBuilder();
86+
for (var v : vars) {
87+
final var newName =
88+
services.getVariableNamer().getTemporaryNameProposal(v.name() + "_before");
89+
KeYJavaType type = v.getKeYJavaType();
90+
var locVar = new LocationVariable(newName, type);
91+
var spec = new VariableSpecification(locVar);
92+
int dim = 0;
93+
if (type.getJavaType() instanceof ArrayType at) {
94+
dim = at.getDimension();
95+
}
96+
decls.add(new LocalVariableDeclaration(new TypeRef(type, dim), spec));
97+
updatesBefore = updatesBefore.append(tb.elementary(tb.var(locVar), tb.var(v)));
98+
updatesFrame = updatesFrame.append(tb.elementary(tb.var(v), tb.var(locVar)));
99+
}
100+
return matchCond.setInstantiations(
101+
svInst.add(varDeclsSV, new ProgramList(new ImmutableArray<>(decls)), services)
102+
.add(updateBeforeSV, tb.parallel(updatesBefore), services)
103+
.add(updateFrameSV, tb.parallel(updatesFrame), services));
104+
}
105+
106+
@Override
107+
public String toString() {
108+
return "\\newLocalVars(" + varDeclsSV + ", " + updateBeforeSV + ", " + updateFrameSV + ", "
109+
+ bodySV + ")";
110+
}
111+
}

‎key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateBeforeLoopUpdate.java‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -7,14 +7,13 @@
77
import de.uka.ilkd.key.ldt.HeapLDT;
88
import de.uka.ilkd.key.logic.Term;
99
import de.uka.ilkd.key.logic.TermBuilder;
10-
import de.uka.ilkd.key.logic.op.AbstractTermTransformer;
11-
import de.uka.ilkd.key.logic.op.Modality;
12-
import de.uka.ilkd.key.logic.op.UpdateableOperator;
10+
import de.uka.ilkd.key.logic.op.*;
1311
import de.uka.ilkd.key.rule.inst.SVInstantiations;
1412
import de.uka.ilkd.key.util.MiscTools;
1513

1614
import org.key_project.logic.Name;
1715

16+
1817
/**
1918
* Initializes the "before loop" update needed for the modifiable clause.
2019
*
@@ -64,7 +63,8 @@ public Term transform(Term term, SVInstantiations svInst, Services services) {
6463
* @return The anonymizing update.
6564
*/
6665
private static Term createBeforeLoopUpdate(boolean isTransaction, boolean isPermissions,
67-
Term anonHeapTerm, Term anonSavedHeapTerm, Term anonPermissionsHeapTerm,
66+
Term anonHeapTerm, Term anonSavedHeapTerm,
67+
Term anonPermissionsHeapTerm,
6868
Services services) {
6969
final TermBuilder tb = services.getTermBuilder();
7070
final HeapLDT heapLDT = services.getTypeConverter().getHeapLDT();

‎key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateFrameCond.java‎

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -11,10 +11,7 @@
1111
import de.uka.ilkd.key.ldt.HeapLDT;
1212
import de.uka.ilkd.key.logic.Term;
1313
import de.uka.ilkd.key.logic.TermBuilder;
14-
import de.uka.ilkd.key.logic.op.AbstractTermTransformer;
15-
import de.uka.ilkd.key.logic.op.LocationVariable;
16-
import de.uka.ilkd.key.logic.op.Modality;
17-
import de.uka.ilkd.key.logic.op.ProgramVariable;
14+
import de.uka.ilkd.key.logic.op.*;
1815
import de.uka.ilkd.key.rule.inst.SVInstantiations;
1916
import de.uka.ilkd.key.speclang.HeapContext;
2017
import de.uka.ilkd.key.speclang.LoopSpecification;
@@ -102,7 +99,6 @@ private static Term createFrameCondition(final LoopSpecification loopSpec,
10299

103100
frameCondition = frameCondition == null ? fc : tb.and(frameCondition, fc);
104101
}
105-
106102
return frameCondition;
107103
}
108104

‎key.core/src/main/javacc/de/uka/ilkd/key/parser/schemajava/SchemaJavaParser.jj‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4365,7 +4365,7 @@ RKeYMetaConstruct KeYMetaConstructStatement() :
43654365
return result;
43664366
}
43674367
)
4368-
|
4368+
|
43694369
(
43704370
"#resolve-multiple-var-decl" "(" stat = Statement() ")" ";"
43714371
{

‎key.core/src/main/resources/de/uka/ilkd/key/proof/rules/loopScopeRules.key‎

Lines changed: 49 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,9 @@
3838
\schemaVar \program Variable #heapBefore_LOOP;
3939
\schemaVar \program Variable #savedHeapBefore_LOOP;
4040
\schemaVar \program Variable #permissionsBefore_LOOP;
41+
\schemaVar \program [list] Statement #localVarDeclsBefore_LOOP;
42+
\schemaVar \update #updateBefore_LOOP;
43+
\schemaVar \update #updateFrame_LOOP;
4144

4245
\find((\modality{#dia} {.. while (#nse) #body ... }\endmodality (post)))
4346

@@ -46,6 +49,7 @@
4649
\varcond(\new(#heapBefore_LOOP, Heap))
4750
\varcond(\new(#savedHeapBefore_LOOP, Heap))
4851
\varcond(\new(#permissionsBefore_LOOP, Heap))
52+
\varcond(\newLocalVars(#localVarDeclsBefore_LOOP, #updateBefore_LOOP, #updateFrame_LOOP, #body))
4953

5054
\varcond(\storeTermIn(loopFormula, \modality{#dia}{ while (#nse) #body }\endmodality (post)))
5155
// Implementation Note (DS, 2019-04-11): We have to separately store the active statement
@@ -71,8 +75,14 @@
7175
#typeof(#savedHeapBefore_LOOP) #savedHeapBefore_LOOP;
7276
#typeof(#permissionsBefore_LOOP) #permissionsBefore_LOOP;
7377
#typeof(#variant) #variant;
78+
#localVarDeclsBefore_LOOP
7479
}\endmodality (
75-
{#createBeforeLoopUpdate(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP)
80+
{#createBeforeLoopUpdate(
81+
loopFormula,
82+
#heapBefore_LOOP,
83+
#savedHeapBefore_LOOP,
84+
#permissionsBefore_LOOP)
85+
|| #updateBefore_LOOP
7686
|| #createLocalAnonUpdate(loopFormula)
7787
|| #createHeapAnonUpdate(loopFormula, anon_heap_LOOP, anon_savedHeap_LOOP, anon_permissions_LOOP)}
7888
{#variant := variantTerm}
@@ -93,7 +103,11 @@
93103
(#x<<loopScopeIndex>> = TRUE -> post) &
94104
(#x<<loopScopeIndex>> = FALSE ->
95105
inv
96-
& #createFrameCond(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP)
106+
& {#updateFrame_LOOP} #createFrameCond(
107+
loopFormula,
108+
#heapBefore_LOOP,
109+
#savedHeapBefore_LOOP,
110+
#permissionsBefore_LOOP)
97111
& prec(variantTerm, #variant))
98112
)))
99113
)
@@ -117,13 +131,17 @@
117131
\schemaVar \program Variable #heapBefore_LOOP;
118132
\schemaVar \program Variable #savedHeapBefore_LOOP;
119133
\schemaVar \program Variable #permissionsBefore_LOOP;
134+
\schemaVar \program [list] Statement #localVarDeclsBefore_LOOP;
135+
\schemaVar \update #updateBefore_LOOP;
136+
\schemaVar \update #updateFrame_LOOP;
120137

121138
\find((\modality{#box} {.. while (#nse) #body ... }\endmodality (post)))
122139

123140
\varcond(\new(#x, boolean))
124141
\varcond(\new(#heapBefore_LOOP, Heap))
125142
\varcond(\new(#savedHeapBefore_LOOP, Heap))
126143
\varcond(\new(#permissionsBefore_LOOP, Heap))
144+
\varcond(\newLocalVars(#localVarDeclsBefore_LOOP, #updateBefore_LOOP, #updateFrame_LOOP, #body))
127145

128146
\varcond(\storeTermIn(loopFormula, \modality{#box}{ while (#nse) #body }\endmodality (post)))
129147
\varcond(\storeStmtIn(#loopStmt, \modality{#box}{ while (#nse) #body }\endmodality (post)))
@@ -140,10 +158,12 @@
140158
#typeof(#heapBefore_LOOP) #heapBefore_LOOP;
141159
#typeof(#savedHeapBefore_LOOP) #savedHeapBefore_LOOP;
142160
#typeof(#permissionsBefore_LOOP) #permissionsBefore_LOOP;
161+
#localVarDeclsBefore_LOOP
143162
}
144163
\endmodality (
145164
{#createBeforeLoopUpdate(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP)
146165
|| #createLocalAnonUpdate(loopFormula)
166+
|| #updateBefore_LOOP
147167
|| #createHeapAnonUpdate(loopFormula, anon_heap_LOOP, anon_savedHeap_LOOP, anon_permissions_LOOP)}
148168
(inv & freeInv ->
149169
(\modality{#box}{
@@ -162,7 +182,11 @@
162182
(#x<<loopScopeIndex>> = TRUE -> post) &
163183
(#x<<loopScopeIndex>> = FALSE ->
164184
inv
165-
& #createFrameCond(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP))
185+
& {#updateFrame_LOOP} #createFrameCond(
186+
loopFormula,
187+
#heapBefore_LOOP,
188+
#savedHeapBefore_LOOP,
189+
#permissionsBefore_LOOP))
166190
)))
167191
)
168192
)
@@ -221,6 +245,9 @@
221245
\schemaVar \program Variable #heapBefore_LOOP;
222246
\schemaVar \program Variable #savedHeapBefore_LOOP;
223247
\schemaVar \program Variable #permissionsBefore_LOOP;
248+
\schemaVar \program [list] Statement #localVarDeclsBefore_LOOP;
249+
\schemaVar \update #updateBefore_LOOP;
250+
\schemaVar \update #updateFrame_LOOP;
224251

225252
\find((\modality{#dia} {.. while (#nse) #body ... }\endmodality (post)))
226253

@@ -229,6 +256,7 @@
229256
\varcond(\new(#heapBefore_LOOP, Heap))
230257
\varcond(\new(#savedHeapBefore_LOOP, Heap))
231258
\varcond(\new(#permissionsBefore_LOOP, Heap))
259+
\varcond(\newLocalVars(#localVarDeclsBefore_LOOP, #updateBefore_LOOP, #updateFrame_LOOP, #body))
232260

233261
\varcond(\storeTermIn(loopFormula, \modality{#dia}{ while (#nse) #body }\endmodality (post)))
234262
\varcond(\storeStmtIn(#loopStmt, \modality{#dia}{ while (#nse) #body }\endmodality (post)))
@@ -247,10 +275,12 @@
247275
#typeof(#savedHeapBefore_LOOP) #savedHeapBefore_LOOP;
248276
#typeof(#permissionsBefore_LOOP) #permissionsBefore_LOOP;
249277
#typeof(#variant) #variant;
278+
#localVarDeclsBefore_LOOP
250279
}
251280
\endmodality (
252281
{#createBeforeLoopUpdate(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP)
253282
|| #createLocalAnonUpdate(loopFormula)
283+
|| #updateBefore_LOOP
254284
|| #createHeapAnonUpdate(loopFormula, anon_heap_LOOP, anon_savedHeap_LOOP, anon_permissions_LOOP)}
255285
{#variant := variantTerm}
256286
(inv & freeInv ->
@@ -269,7 +299,11 @@
269299
}\endmodality (
270300
#x<<loopScopeIndex>> = FALSE ->
271301
inv
272-
& #createFrameCond(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP)
302+
& {#updateFrame_LOOP} #createFrameCond(
303+
loopFormula,
304+
#heapBefore_LOOP,
305+
#savedHeapBefore_LOOP,
306+
#permissionsBefore_LOOP)
273307
& prec(variantTerm, #variant)
274308
)))
275309
)
@@ -327,13 +361,17 @@
327361
\schemaVar \program Variable #heapBefore_LOOP;
328362
\schemaVar \program Variable #savedHeapBefore_LOOP;
329363
\schemaVar \program Variable #permissionsBefore_LOOP;
364+
\schemaVar \program [list] Statement #localVarDeclsBefore_LOOP;
365+
\schemaVar \update #updateBefore_LOOP;
366+
\schemaVar \update #updateFrame_LOOP;
330367

331368
\find((\modality{#box} {.. while (#nse) #body ... }\endmodality (post)))
332369

333370
\varcond(\new(#x, boolean))
334371
\varcond(\new(#heapBefore_LOOP, Heap))
335372
\varcond(\new(#savedHeapBefore_LOOP, Heap))
336373
\varcond(\new(#permissionsBefore_LOOP, Heap))
374+
\varcond(\newLocalVars(#localVarDeclsBefore_LOOP, #updateBefore_LOOP, #updateFrame_LOOP, #body))
337375

338376
\varcond(\storeTermIn(loopFormula, \modality{#box}{ while (#nse) #body }\endmodality (post)))
339377
\varcond(\storeStmtIn(#loopStmt, \modality{#box}{ while (#nse) #body }\endmodality (post)))
@@ -349,10 +387,12 @@
349387
\modality{#box}{ #typeof(#heapBefore_LOOP) #heapBefore_LOOP;
350388
#typeof(#savedHeapBefore_LOOP) #savedHeapBefore_LOOP;
351389
#typeof(#permissionsBefore_LOOP) #permissionsBefore_LOOP;
390+
#localVarDeclsBefore_LOOP
352391
}
353392
\endmodality (
354393
{#createBeforeLoopUpdate(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP)
355394
|| #createLocalAnonUpdate(loopFormula)
395+
|| #updateBefore_LOOP
356396
|| #createHeapAnonUpdate(loopFormula, anon_heap_LOOP, anon_savedHeap_LOOP, anon_permissions_LOOP)}
357397
(inv & freeInv ->
358398
(\modality{#box}{
@@ -370,7 +410,11 @@
370410
}\endmodality (
371411
#x<<loopScopeIndex>> = FALSE ->
372412
inv
373-
& #createFrameCond(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP)
413+
& {#updateFrame_LOOP} #createFrameCond(
414+
loopFormula,
415+
#heapBefore_LOOP,
416+
#savedHeapBefore_LOOP,
417+
#permissionsBefore_LOOP)
374418
)))
375419
)
376420
)

0 commit comments

Comments
 (0)