Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix #3524 #3525

Merged
merged 10 commits into from
Nov 25, 2024
Merged

Fix #3524 #3525

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
8f7b21f
Fix 3524
Drodt Oct 30, 2024
8fc8c29
Update taclet equality tests
Drodt Oct 31, 2024
4d0835b
Fix slicing test (changed loop rules add two more rules, resulting in…
unp1 Oct 31, 2024
34f5827
Fix saved proof (adapted saved proof for fixed loop invariant rule)
unp1 Oct 31, 2024
68eb108
update qodana linter
unp1 Oct 31, 2024
87f4b5f
clean up taclet builder
unp1 Oct 31, 2024
2014116
clean up taclet builder
unp1 Oct 31, 2024
e3fdf2f
Separate SVs for decls and updates
Drodt Nov 4, 2024
7a14261
Update TacletEq tests
Drodt Nov 4, 2024
fa17636
Merge branch 'main' into fix-2524
Drodt Nov 4, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions key.core/src/main/antlr4/KeYLexer.g4
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -145,6 +145,7 @@ EQUAL_UNIQUE : '\\equalUnique';
NEW : '\\new';
NEW_TYPE_OF: '\\newTypeOf';
NEW_DEPENDING_ON: '\\newDependingOn';
NEW_LOCAL_VARS: '\\newLocalVars';
HAS_ELEMENTARY_SORT:'\\hasElementarySort';
NEWLABEL : '\\newLabel';
CONTAINS_ASSIGNMENT : '\\containsAssignment';
Expand Down
1 change: 1 addition & 0 deletions key.core/src/main/antlr4/KeYParser.g4
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -688,6 +688,7 @@ varexpId: // weigl, 2021-03-12: This will be later just an arbitrary identifier.
| NEW
| NEW_TYPE_OF
| NEW_DEPENDING_ON
| NEW_LOCAL_VARS
| HAS_ELEMENTARY_SORT
| SAME
| ISSUBTYPE
Expand Down
2 changes: 2 additions & 0 deletions key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramReplaceVisitor.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
* SPDX-License-Identifier: GPL-2.0-only */
package de.uka.ilkd.key.java.visitor;


import de.uka.ilkd.key.java.ProgramElement;
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.java.SourceElement;
Expand All @@ -16,6 +17,7 @@
import org.key_project.util.ExtList;
import org.key_project.util.collection.ImmutableArray;


/**
* Walks through a java AST in depth-left-fist-order. This walker is used to transform a program
* according to the given SVInstantiations.
Expand Down
5 changes: 4 additions & 1 deletion key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -161,6 +161,8 @@ public void apply(TacletBuilder<?> tacletBuilder, Object[] arguments,
}
};

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

static class NotFreeInTacletBuilderCommand extends AbstractTacletBuilderCommand {
public NotFreeInTacletBuilderCommand(@NonNull ArgumentType... argumentsTypes) {
Expand Down Expand Up @@ -367,7 +369,8 @@ public IsLabeledCondition build(Object[] arguments, List<String> parameters,
// region Registry
static {
register(SAME_OBSERVER, SIMPLIFY_ITE_UPDATE, ABSTRACT_OR_INTERFACE, SAME, IS_SUBTYPE,
STRICT, DISJOINT_MODULO_NULL, NEW_JAVATYPE, NEW_VAR, FREE_1, FREE_2, FREE_3, FREE_4,
STRICT, DISJOINT_MODULO_NULL, NEW_JAVATYPE, NEW_VAR, NEW_LOCAL_VARS, FREE_1, FREE_2,
FREE_3, FREE_4,
FREE_5, NEW_TYPE_OF, NEW_DEPENDING_ON, FREE_LABEL_IN_VARIABLE, DIFFERENT, FINAL,
ENUM_CONST, LOCAL_VARIABLE, ARRAY_LENGTH, ARRAY, REFERENCE_ARRAY, MAY_EXPAND_METHOD_2,
MAY_EXPAND_METHOD_3, STATIC_METHOD, THIS_REFERENCE, REFERENCE, ENUM_TYPE,
Expand Down
111 changes: 111 additions & 0 deletions key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewLocalVarsCondition.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,111 @@
/* This file is part of KeY - https://key-project.org
* KeY is licensed under the GNU General Public License Version 2
* SPDX-License-Identifier: GPL-2.0-only */
package de.uka.ilkd.key.rule.conditions;

import java.util.ArrayList;
import java.util.List;

import de.uka.ilkd.key.java.ProgramElement;
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.java.Statement;
import de.uka.ilkd.key.java.abstraction.ArrayType;
import de.uka.ilkd.key.java.abstraction.KeYJavaType;
import de.uka.ilkd.key.java.declaration.LocalVariableDeclaration;
import de.uka.ilkd.key.java.declaration.VariableDeclaration;
import de.uka.ilkd.key.java.declaration.VariableSpecification;
import de.uka.ilkd.key.java.reference.TypeRef;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.logic.op.LocationVariable;
import de.uka.ilkd.key.logic.op.SchemaVariable;
import de.uka.ilkd.key.rule.MatchConditions;
import de.uka.ilkd.key.rule.VariableCondition;
import de.uka.ilkd.key.rule.inst.ProgramList;
import de.uka.ilkd.key.rule.inst.SVInstantiations;
import de.uka.ilkd.key.util.MiscTools;

import org.key_project.logic.SyntaxElement;
import org.key_project.util.collection.*;

/**
* For the loop scope rule, if a local program variable that may be altered by the loop body appears
* in the frame condition,
* it is necessary to use the value <i>before</i> the loop first executes in the frame condition.
* <br>
* To achieve this, this condition generates (1) the "before" version of each variable that may be
* written to by the loop
* {@link MiscTools#getLocalOuts(ProgramElement, Services)}; (2) an update storing the value of each
* such PV in its "before" version,
* i.e., {@code {...||i_before := i||...}}; (3) the reverse of the update, to be applied to the
* frame condition, i.e.,
* {@code {...||i := i_before||...}}.
*/
public class NewLocalVarsCondition implements VariableCondition {
/**
* A SV that will store variable declarations for the "before" version of variables.
*/
private final SchemaVariable varDeclsSV;
/**
* Will store the update {@code {...||i_before := i||...}}.
*/
private final SchemaVariable updateBeforeSV;
/**
* Will store the update {@code {...||i := i_before||...}}.
*/
private final SchemaVariable updateFrameSV;
/**
* The loop body.
*/
private final SchemaVariable bodySV;

public NewLocalVarsCondition(SchemaVariable varDeclsSV, SchemaVariable updateBeforeSV,
SchemaVariable updateFrameSV, SchemaVariable bodySV) {
this.varDeclsSV = varDeclsSV;
this.updateBeforeSV = updateBeforeSV;
this.updateFrameSV = updateFrameSV;
this.bodySV = bodySV;
}

@Override
public MatchConditions check(SchemaVariable var, SyntaxElement instCandidate,
MatchConditions matchCond, Services services) {
SVInstantiations svInst = matchCond.getInstantiations();
if (svInst.getInstantiation(varDeclsSV) != null) {
return matchCond;
}
var body = (Statement) svInst.getInstantiation(bodySV);
if (body == null) {
return matchCond;
}

var vars = MiscTools.getLocalOuts(body, services);
List<VariableDeclaration> decls = new ArrayList<>(vars.size());
ImmutableList<Term> updatesBefore = ImmutableSLList.nil();
ImmutableList<Term> updatesFrame = ImmutableSLList.nil();
var tb = services.getTermBuilder();
for (var v : vars) {
final var newName =
services.getVariableNamer().getTemporaryNameProposal(v.name() + "_before");
KeYJavaType type = v.getKeYJavaType();
var locVar = new LocationVariable(newName, type);
var spec = new VariableSpecification(locVar);
int dim = 0;
if (type.getJavaType() instanceof ArrayType at) {
dim = at.getDimension();
}
decls.add(new LocalVariableDeclaration(new TypeRef(type, dim), spec));
updatesBefore = updatesBefore.append(tb.elementary(tb.var(locVar), tb.var(v)));
updatesFrame = updatesFrame.append(tb.elementary(tb.var(v), tb.var(locVar)));
}
return matchCond.setInstantiations(
svInst.add(varDeclsSV, new ProgramList(new ImmutableArray<>(decls)), services)
.add(updateBeforeSV, tb.parallel(updatesBefore), services)
.add(updateFrameSV, tb.parallel(updatesFrame), services));
}

@Override
public String toString() {
return "\\newLocalVars(" + varDeclsSV + ", " + updateBeforeSV + ", " + updateFrameSV + ", "
+ bodySV + ")";
}
}
8 changes: 4 additions & 4 deletions key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateBeforeLoopUpdate.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,14 +7,13 @@
import de.uka.ilkd.key.ldt.HeapLDT;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.logic.TermBuilder;
import de.uka.ilkd.key.logic.op.AbstractTermTransformer;
import de.uka.ilkd.key.logic.op.Modality;
import de.uka.ilkd.key.logic.op.UpdateableOperator;
import de.uka.ilkd.key.logic.op.*;
import de.uka.ilkd.key.rule.inst.SVInstantiations;
import de.uka.ilkd.key.util.MiscTools;

import org.key_project.logic.Name;


/**
* Initializes the "before loop" update needed for the modifiable clause.
*
Expand Down Expand Up @@ -64,7 +63,8 @@ public Term transform(Term term, SVInstantiations svInst, Services services) {
* @return The anonymizing update.
*/
private static Term createBeforeLoopUpdate(boolean isTransaction, boolean isPermissions,
Term anonHeapTerm, Term anonSavedHeapTerm, Term anonPermissionsHeapTerm,
Term anonHeapTerm, Term anonSavedHeapTerm,
Term anonPermissionsHeapTerm,
Services services) {
final TermBuilder tb = services.getTermBuilder();
final HeapLDT heapLDT = services.getTypeConverter().getHeapLDT();
Expand Down
6 changes: 1 addition & 5 deletions key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateFrameCond.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,10 +11,7 @@
import de.uka.ilkd.key.ldt.HeapLDT;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.logic.TermBuilder;
import de.uka.ilkd.key.logic.op.AbstractTermTransformer;
import de.uka.ilkd.key.logic.op.LocationVariable;
import de.uka.ilkd.key.logic.op.Modality;
import de.uka.ilkd.key.logic.op.ProgramVariable;
import de.uka.ilkd.key.logic.op.*;
import de.uka.ilkd.key.rule.inst.SVInstantiations;
import de.uka.ilkd.key.speclang.HeapContext;
import de.uka.ilkd.key.speclang.LoopSpecification;
Expand Down Expand Up @@ -102,7 +99,6 @@ private static Term createFrameCondition(final LoopSpecification loopSpec,

frameCondition = frameCondition == null ? fc : tb.and(frameCondition, fc);
}

return frameCondition;
}

Expand Down
2 changes: 1 addition & 1 deletion key.core/src/main/javacc/de/uka/ilkd/key/parser/schemajava/SchemaJavaParser.jj
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4365,7 +4365,7 @@ RKeYMetaConstruct KeYMetaConstructStatement() :
return result;
}
)
|
|
(
"#resolve-multiple-var-decl" "(" stat = Statement() ")" ";"
{
Expand Down
54 changes: 49 additions & 5 deletions key.core/src/main/resources/de/uka/ilkd/key/proof/rules/loopScopeRules.key
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,9 @@
\schemaVar \program Variable #heapBefore_LOOP;
\schemaVar \program Variable #savedHeapBefore_LOOP;
\schemaVar \program Variable #permissionsBefore_LOOP;
\schemaVar \program [list] Statement #localVarDeclsBefore_LOOP;
\schemaVar \update #updateBefore_LOOP;
\schemaVar \update #updateFrame_LOOP;

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

Expand All @@ -46,6 +49,7 @@
\varcond(\new(#heapBefore_LOOP, Heap))
\varcond(\new(#savedHeapBefore_LOOP, Heap))
\varcond(\new(#permissionsBefore_LOOP, Heap))
\varcond(\newLocalVars(#localVarDeclsBefore_LOOP, #updateBefore_LOOP, #updateFrame_LOOP, #body))

\varcond(\storeTermIn(loopFormula, \modality{#dia}{ while (#nse) #body }\endmodality (post)))
// Implementation Note (DS, 2019-04-11): We have to separately store the active statement
Expand All @@ -71,8 +75,14 @@
#typeof(#savedHeapBefore_LOOP) #savedHeapBefore_LOOP;
#typeof(#permissionsBefore_LOOP) #permissionsBefore_LOOP;
#typeof(#variant) #variant;
#localVarDeclsBefore_LOOP
}\endmodality (
{#createBeforeLoopUpdate(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP)
{#createBeforeLoopUpdate(
loopFormula,
#heapBefore_LOOP,
#savedHeapBefore_LOOP,
#permissionsBefore_LOOP)
|| #updateBefore_LOOP
|| #createLocalAnonUpdate(loopFormula)
|| #createHeapAnonUpdate(loopFormula, anon_heap_LOOP, anon_savedHeap_LOOP, anon_permissions_LOOP)}
{#variant := variantTerm}
Expand All @@ -93,7 +103,11 @@
(#x<<loopScopeIndex>> = TRUE -> post) &
(#x<<loopScopeIndex>> = FALSE ->
inv
& #createFrameCond(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP)
& {#updateFrame_LOOP} #createFrameCond(
loopFormula,
#heapBefore_LOOP,
#savedHeapBefore_LOOP,
#permissionsBefore_LOOP)
& prec(variantTerm, #variant))
)))
)
Expand All @@ -117,13 +131,17 @@
\schemaVar \program Variable #heapBefore_LOOP;
\schemaVar \program Variable #savedHeapBefore_LOOP;
\schemaVar \program Variable #permissionsBefore_LOOP;
\schemaVar \program [list] Statement #localVarDeclsBefore_LOOP;
\schemaVar \update #updateBefore_LOOP;
\schemaVar \update #updateFrame_LOOP;

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

\varcond(\new(#x, boolean))
\varcond(\new(#heapBefore_LOOP, Heap))
\varcond(\new(#savedHeapBefore_LOOP, Heap))
\varcond(\new(#permissionsBefore_LOOP, Heap))
\varcond(\newLocalVars(#localVarDeclsBefore_LOOP, #updateBefore_LOOP, #updateFrame_LOOP, #body))

\varcond(\storeTermIn(loopFormula, \modality{#box}{ while (#nse) #body }\endmodality (post)))
\varcond(\storeStmtIn(#loopStmt, \modality{#box}{ while (#nse) #body }\endmodality (post)))
Expand All @@ -140,10 +158,12 @@
#typeof(#heapBefore_LOOP) #heapBefore_LOOP;
#typeof(#savedHeapBefore_LOOP) #savedHeapBefore_LOOP;
#typeof(#permissionsBefore_LOOP) #permissionsBefore_LOOP;
#localVarDeclsBefore_LOOP
}
\endmodality (
{#createBeforeLoopUpdate(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP)
|| #createLocalAnonUpdate(loopFormula)
|| #updateBefore_LOOP
|| #createHeapAnonUpdate(loopFormula, anon_heap_LOOP, anon_savedHeap_LOOP, anon_permissions_LOOP)}
(inv & freeInv ->
(\modality{#box}{
Expand All @@ -162,7 +182,11 @@
(#x<<loopScopeIndex>> = TRUE -> post) &
(#x<<loopScopeIndex>> = FALSE ->
inv
& #createFrameCond(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP))
& {#updateFrame_LOOP} #createFrameCond(
loopFormula,
#heapBefore_LOOP,
#savedHeapBefore_LOOP,
#permissionsBefore_LOOP))
)))
)
)
Expand Down Expand Up @@ -221,6 +245,9 @@
\schemaVar \program Variable #heapBefore_LOOP;
\schemaVar \program Variable #savedHeapBefore_LOOP;
\schemaVar \program Variable #permissionsBefore_LOOP;
\schemaVar \program [list] Statement #localVarDeclsBefore_LOOP;
\schemaVar \update #updateBefore_LOOP;
\schemaVar \update #updateFrame_LOOP;

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

Expand All @@ -229,6 +256,7 @@
\varcond(\new(#heapBefore_LOOP, Heap))
\varcond(\new(#savedHeapBefore_LOOP, Heap))
\varcond(\new(#permissionsBefore_LOOP, Heap))
\varcond(\newLocalVars(#localVarDeclsBefore_LOOP, #updateBefore_LOOP, #updateFrame_LOOP, #body))

\varcond(\storeTermIn(loopFormula, \modality{#dia}{ while (#nse) #body }\endmodality (post)))
\varcond(\storeStmtIn(#loopStmt, \modality{#dia}{ while (#nse) #body }\endmodality (post)))
Expand All @@ -247,10 +275,12 @@
#typeof(#savedHeapBefore_LOOP) #savedHeapBefore_LOOP;
#typeof(#permissionsBefore_LOOP) #permissionsBefore_LOOP;
#typeof(#variant) #variant;
#localVarDeclsBefore_LOOP
}
\endmodality (
{#createBeforeLoopUpdate(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP)
|| #createLocalAnonUpdate(loopFormula)
|| #updateBefore_LOOP
|| #createHeapAnonUpdate(loopFormula, anon_heap_LOOP, anon_savedHeap_LOOP, anon_permissions_LOOP)}
{#variant := variantTerm}
(inv & freeInv ->
Expand All @@ -269,7 +299,11 @@
}\endmodality (
#x<<loopScopeIndex>> = FALSE ->
inv
& #createFrameCond(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP)
& {#updateFrame_LOOP} #createFrameCond(
loopFormula,
#heapBefore_LOOP,
#savedHeapBefore_LOOP,
#permissionsBefore_LOOP)
& prec(variantTerm, #variant)
)))
)
Expand Down Expand Up @@ -327,13 +361,17 @@
\schemaVar \program Variable #heapBefore_LOOP;
\schemaVar \program Variable #savedHeapBefore_LOOP;
\schemaVar \program Variable #permissionsBefore_LOOP;
\schemaVar \program [list] Statement #localVarDeclsBefore_LOOP;
\schemaVar \update #updateBefore_LOOP;
\schemaVar \update #updateFrame_LOOP;

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

\varcond(\new(#x, boolean))
\varcond(\new(#heapBefore_LOOP, Heap))
\varcond(\new(#savedHeapBefore_LOOP, Heap))
\varcond(\new(#permissionsBefore_LOOP, Heap))
\varcond(\newLocalVars(#localVarDeclsBefore_LOOP, #updateBefore_LOOP, #updateFrame_LOOP, #body))

\varcond(\storeTermIn(loopFormula, \modality{#box}{ while (#nse) #body }\endmodality (post)))
\varcond(\storeStmtIn(#loopStmt, \modality{#box}{ while (#nse) #body }\endmodality (post)))
Expand All @@ -349,10 +387,12 @@
\modality{#box}{ #typeof(#heapBefore_LOOP) #heapBefore_LOOP;
#typeof(#savedHeapBefore_LOOP) #savedHeapBefore_LOOP;
#typeof(#permissionsBefore_LOOP) #permissionsBefore_LOOP;
#localVarDeclsBefore_LOOP
}
\endmodality (
{#createBeforeLoopUpdate(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP)
|| #createLocalAnonUpdate(loopFormula)
|| #updateBefore_LOOP
|| #createHeapAnonUpdate(loopFormula, anon_heap_LOOP, anon_savedHeap_LOOP, anon_permissions_LOOP)}
(inv & freeInv ->
(\modality{#box}{
Expand All @@ -370,7 +410,11 @@
}\endmodality (
#x<<loopScopeIndex>> = FALSE ->
inv
& #createFrameCond(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP)
& {#updateFrame_LOOP} #createFrameCond(
loopFormula,
#heapBefore_LOOP,
#savedHeapBefore_LOOP,
#permissionsBefore_LOOP)
)))
)
)
Expand Down
Loading
Loading