Skip to content

Commit 6b2bec3

Browse files
wadoonwadoon
authored
Merge branch 'main' into weigl/pckgreworked
2 parents c057a0e + 9ef68b3 commit 6b2bec3

File tree

17 files changed

+200
-35
lines changed

17 files changed

+200
-35
lines changed

‎.github/workflows/code_quality.yml‎

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -22,9 +22,7 @@ jobs:
2222
- name: Setup Gradle
2323
uses: gradle/actions/[email protected]
2424
- name: Build with Gradle
25-
uses: gradle/[email protected]
26-
with:
27-
arguments: -DENABLE_NULLNESS=true compileTest
25+
run: ./gradlew -DENABLE_NULLNESS=true compileTest
2826

2927
formatting:
3028
runs-on: ubuntu-latest
@@ -36,6 +34,5 @@ jobs:
3634
java-version: '21'
3735
cache: 'gradle'
3836
- name: Build with Gradle
39-
uses: gradle/[email protected]
40-
with:
41-
arguments: --continue spotlessCheck
37+
run: ./gradlew --parallel --continue spotlessCheck
38+

‎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
{

0 commit comments

Comments
 (0)