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.

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

Set statement: Check assignee for validity #3195

Closed
wants to merge 14 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
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
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,8 @@

import org.key_project.util.collection.ImmutableList;

import org.jspecify.annotations.NonNull;

/**
* <p>
* A {@link BuiltInRule} which evaluates a query in a side proof.
Expand Down Expand Up @@ -194,6 +196,7 @@ public IBuiltInRuleApp createApp(PosInOccurrence pos, TermServices services) {
/**
* {@inheritDoc}
*/
@NonNull
@Override
public ImmutableList<Goal> apply(Goal goal, Services services, RuleApp ruleApp)
throws RuleAbortException {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -333,7 +333,7 @@ private Term computeTermForCondition(String condition) {
PositionedString ps = new PositionedString(condition);

var context = Context.inMethodWithSelfVar(pm, selfVar);
JmlIO io = new JmlIO().services(getProof().getServices()).context(context)
JmlIO io = new JmlIO(getProof().getServices()).context(context)
.parameters(varsForCondition);

return io.parseExpression(ps);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -360,62 +360,13 @@ new IllegalArgumentException(&quot;Array can&apos;t be null.&quot;);" pathCondit
</value>
</variable>
<callStackEntry path="/0"/>
<exceptionalMethodReturn name="&lt;throw java.lang.IllegalArgumentException&gt;" signature="&lt;exceptional return of &lt;call self.average(array)&gt;&gt;" pathCondition="equals(array,null)" pathConditionChanged="false" methodReturnCondition="equals(array,null)">
<variable name="self" isArrayIndex="false">
<value name="self {true}" typeString="UseOperationContractStatementsInImpliciteConstructor" valueString="self" isValueAnObject="true" isValueUnknown="false" conditionString="true">
</value>
</variable>
<variable name="array" isArrayIndex="false">
<value name="array {true}" typeString="Null" valueString="null" isValueAnObject="false" isValueUnknown="false" conditionString="true">
</value>
</variable>
<variable name="exc" isArrayIndex="false">
<value name="exc {true}" typeString="Null" valueString="null" isValueAnObject="false" isValueUnknown="false" conditionString="true">
</value>
</variable>
<variable name="i" isArrayIndex="false">
<value name="i {true}" typeString="java.lang.IllegalArgumentException" valueString="i_3" isValueAnObject="false" isValueUnknown="false" conditionString="true">
</value>
</variable>
<callStackEntry path="/0"/>
<termination name="&lt;uncaught java.lang.IllegalArgumentException&gt;" pathCondition="equals(array,null)" pathConditionChanged="false" terminationKind="EXCEPTIONAL" branchVerified="true">
<variable name="exc" isArrayIndex="false">
<value name="exc {true}" typeString="java.lang.IllegalArgumentException" valueString="i_3" isValueAnObject="false" isValueUnknown="false" conditionString="true">
</value>
</variable>
</termination>
<completedBlockEntry path="/0/0" conditionString="equals(array,null)"/>
<callStateVariable name="self" isArrayIndex="false">
<value name="self {true}" typeString="UseOperationContractStatementsInImpliciteConstructor" valueString="self" isValueAnObject="true" isValueUnknown="false" conditionString="true">
</value>
</callStateVariable>
<callStateVariable name="array" isArrayIndex="false">
<value name="array {true}" typeString="Null" valueString="null" isValueAnObject="false" isValueUnknown="false" conditionString="true">
</value>
</callStateVariable>
<callStateVariable name="exc" isArrayIndex="false">
<value name="exc {true}" typeString="Null" valueString="null" isValueAnObject="false" isValueUnknown="false" conditionString="true">
</value>
</callStateVariable>
<callStateVariable name="heapBefore_average" isArrayIndex="false">
<value name="heapBefore_average {true}" typeString="Heap" valueString="heap" isValueAnObject="false" isValueUnknown="false" conditionString="true">
</value>
</callStateVariable>
<callStateVariable name="savedHeapBefore_average" isArrayIndex="false">
<value name="savedHeapBefore_average {true}" typeString="Heap" valueString="savedHeap" isValueAnObject="false" isValueUnknown="false" conditionString="true">
</value>
</callStateVariable>
</exceptionalMethodReturn>
</statement>
</branchCondition>
<blockCompletionEntry path="/0/0/0/0"/>
<blockCompletionEntry path="/0/0/1/0/0"/>
</branchStatement>
<methodReturnEntry path="/0/0/0/0/0/0/0/0"/>
<methodReturnEntry path="/0/0/0/0/0/0/1/0"/>
<methodReturnEntry path="/0/0/1/0/0"/>
</methodCall>
<terminationEntry path="/0/0/0/0/0/0/0/0/0"/>
<terminationEntry path="/0/0/0/0/0/0/1/0/0"/>
<terminationEntry path="/0/0/1/0/0/0"/>
</start>
2 changes: 1 addition & 1 deletion key.core/src/main/antlr4/JmlParser.g4
Original file line number Diff line number Diff line change
Expand Up @@ -161,7 +161,7 @@ in_group_clause: IN expression;
maps_into_clause: MAPS expression;
nowarn_pragma: NOWARN expression;
debug_statement: DEBUG expression;
set_statement: SET expression EQUAL_SINGLE expression SEMI_TOPLEVEL;
set_statement: SET (assignee=expression) EQUAL_SINGLE (value=expression) SEMI_TOPLEVEL;
merge_point_statement:
MERGE_POINT
(MERGE_PROC (proc=STRING_LITERAL))?
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -179,8 +179,7 @@ private static Term newVariable(Term t, String name, Services services) {
String newName = tb.newName(name);
ProgramElementName pen = new ProgramElementName(newName);
ProgramVariable progVar = (ProgramVariable) t.op();
LocationVariable newVar = new LocationVariable(pen, progVar.getKeYJavaType(),
progVar.getContainerType(), progVar.isStatic(), progVar.isModel());
LocationVariable newVar = LocationVariable.fromProgramVariable(progVar, pen);
register(newVar, services);
return tb.var(newVar);
}
Expand Down
23 changes: 21 additions & 2 deletions key.core/src/main/java/de/uka/ilkd/key/java/JavaTools.java
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;


import de.uka.ilkd.key.java.reference.ExecutionContext;
import de.uka.ilkd.key.java.statement.CatchAllStatement;
import de.uka.ilkd.key.java.statement.LabeledStatement;
Expand All @@ -14,12 +15,13 @@

import org.key_project.util.ExtList;

import org.jspecify.annotations.Nullable;

/**
* Miscellaneous static methods related to Java blocks or statements in KeY. Mostly moved from
* key.util.MiscTools here.
*
* @author bruns
*
*/
public final class JavaTools {

Expand Down Expand Up @@ -49,6 +51,20 @@ public static SourceElement getActiveStatement(JavaBlock jb) {
public static JavaBlock removeActiveStatement(JavaBlock jb, Services services) {
assert jb.program() != null;
final SourceElement activeStatement = JavaTools.getActiveStatement(jb);
return replaceStatement(jb, services, activeStatement, null);
}

/**
* Returns the passed java block with `statement` replaced with `with`.
*
* @param jb the block
* @param statement the statement to replace
* @param with what to replace with. If this is null, the statement will be removed
* @return the modified block
*/
public static JavaBlock replaceStatement(JavaBlock jb, Services services,
SourceElement statement, @Nullable SourceElement with) {
assert jb.program() != null;
Statement newProg = (Statement) (new CreatingASTVisitor(jb.program(), false, services) {
private boolean done = false;

Expand All @@ -61,9 +77,12 @@ public ProgramElement go() {

@Override
public void doAction(ProgramElement node) {
if (!done && node == activeStatement) {
if (!done && node == statement) {
done = true;
stack.pop();
if (with != null) {
addToTopOfStack(with);
}
changed();
} else {
super.doAction(node);
Expand Down
41 changes: 11 additions & 30 deletions key.core/src/main/java/de/uka/ilkd/key/java/KeYJavaASTFactory.java
Original file line number Diff line number Diff line change
Expand Up @@ -31,36 +31,7 @@
import de.uka.ilkd.key.java.reference.ThisReference;
import de.uka.ilkd.key.java.reference.TypeRef;
import de.uka.ilkd.key.java.reference.TypeReference;
import de.uka.ilkd.key.java.statement.Branch;
import de.uka.ilkd.key.java.statement.Break;
import de.uka.ilkd.key.java.statement.Case;
import de.uka.ilkd.key.java.statement.Catch;
import de.uka.ilkd.key.java.statement.Continue;
import de.uka.ilkd.key.java.statement.Default;
import de.uka.ilkd.key.java.statement.Do;
import de.uka.ilkd.key.java.statement.Else;
import de.uka.ilkd.key.java.statement.EmptyStatement;
import de.uka.ilkd.key.java.statement.EnhancedFor;
import de.uka.ilkd.key.java.statement.Finally;
import de.uka.ilkd.key.java.statement.For;
import de.uka.ilkd.key.java.statement.ForUpdates;
import de.uka.ilkd.key.java.statement.Guard;
import de.uka.ilkd.key.java.statement.IForUpdates;
import de.uka.ilkd.key.java.statement.IGuard;
import de.uka.ilkd.key.java.statement.ILoopInit;
import de.uka.ilkd.key.java.statement.If;
import de.uka.ilkd.key.java.statement.LabeledStatement;
import de.uka.ilkd.key.java.statement.LoopInit;
import de.uka.ilkd.key.java.statement.MethodBodyStatement;
import de.uka.ilkd.key.java.statement.MethodFrame;
import de.uka.ilkd.key.java.statement.Return;
import de.uka.ilkd.key.java.statement.Switch;
import de.uka.ilkd.key.java.statement.SynchronizedBlock;
import de.uka.ilkd.key.java.statement.Then;
import de.uka.ilkd.key.java.statement.Throw;
import de.uka.ilkd.key.java.statement.TransactionStatement;
import de.uka.ilkd.key.java.statement.Try;
import de.uka.ilkd.key.java.statement.While;
import de.uka.ilkd.key.java.statement.*;
import de.uka.ilkd.key.logic.ProgramElementName;
import de.uka.ilkd.key.logic.VariableNamer;
import de.uka.ilkd.key.logic.op.IProgramMethod;
Expand Down Expand Up @@ -102,6 +73,16 @@ public static CopyAssignment assign(final ExtList parameters) {
return assignment;
}

/**
* Create an assignment.
*
* @param parameters the assignment parameters (variable, expression) as {@link ExtList}
* @return a new {@link CopyAssignment} as defined by <code>parameters</code>
*/
public static SetStatement setStatement(final ExtList parameters) {
return new SetStatement(parameters);
}

/**
* creates an attribute access <code>prefix.field </code>
*/
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,7 @@
import recoder.abstraction.Type;
import recoder.io.DataLocation;
import recoder.java.NonTerminalProgramElement;
import recoder.java.declaration.DeclarationSpecifier;
import recoder.java.declaration.TypeDeclaration;
import recoder.list.generic.ASTList;

Expand Down Expand Up @@ -1119,8 +1120,12 @@ public VariableSpecification convert(

final ProgramElementName name =
VariableNamer.parseName(makeAdmissibleName(recoderVarSpec.getName()));
var isGhost = containsModifier(recoderVarSpec.getParent(),
wadoon marked this conversation as resolved.
Show resolved Hide resolved
de.uka.ilkd.key.java.recoderext.Ghost.class);
var isFinal = recoderVarSpec.isFinal();

final ProgramVariable pv =
new LocationVariable(name, getKeYJavaType(recoderType), recoderVarSpec.isFinal());
new LocationVariable(name, getKeYJavaType(recoderType), isGhost, isFinal);
varSpec = new VariableSpecification(collectChildren(recoderVarSpec), pv,
recoderVarSpec.getDimensions(), pv.getKeYJavaType());

Expand Down Expand Up @@ -1222,6 +1227,18 @@ public FieldSpecification convert(recoder.java.declaration.FieldSpecification re
return varSpec;
}

private static boolean containsModifier(recoder.java.declaration.JavaDeclaration fs,
Class<? extends DeclarationSpecifier> cls) {
ASTList<DeclarationSpecifier> specifiers = fs.getDeclarationSpecifiers();
int s = (specifiers == null) ? 0 : specifiers.size();
for (int i = 0; i < s; i += 1) {
if (cls.isInstance(specifiers.get(i))) {
return true;
}
}
return false;
}

/**
* this is needed by #convert(FieldSpecification).
*/
Expand All @@ -1248,20 +1265,16 @@ private ProgramVariable getProgramVariableForFieldSpecification(
final Literal compileTimeConstant =
getCompileTimeConstantInitializer(recoderVarSpec);

boolean isModel = false;
boolean isModel = containsModifier(recoderVarSpec.getParent(),
de.uka.ilkd.key.java.recoderext.Model.class);
boolean isFinal = recoderVarSpec.isFinal();
for (recoder.java.declaration.Modifier mod : recoderVarSpec.getParent()
.getModifiers()) {
if (mod instanceof de.uka.ilkd.key.java.recoderext.Model) {
isModel = true;
break;
}
}
boolean isGhost = containsModifier(recoderVarSpec.getParent(),
de.uka.ilkd.key.java.recoderext.Ghost.class);

if (compileTimeConstant == null) {
pv = new LocationVariable(pen, getKeYJavaType(recoderType),
getKeYJavaType(recContainingClassType), recoderVarSpec.isStatic(), isModel,
false, isFinal);
isGhost, isFinal);
} else {
pv = new ProgramConstant(pen, getKeYJavaType(recoderType),
getKeYJavaType(recContainingClassType), recoderVarSpec.isStatic(),
Expand Down Expand Up @@ -1765,6 +1778,11 @@ public CopyAssignment convert(recoder.java.expression.operator.CopyAssignment ar
return new CopyAssignment(collectChildrenAndComments(arg));
}

public SetStatement convert(
de.uka.ilkd.key.java.recoderext.SetStatement arg) {
return new SetStatement(collectChildrenAndComments(arg), arg.getParserContext());
}

public TransactionStatement convert(de.uka.ilkd.key.java.recoderext.TransactionStatement tr) {
return new TransactionStatement(tr.getType());
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -430,16 +430,19 @@ private void transformSetStatement(TextualJMLSetStatement stat, Comment[] origin
StatementBlock astParent = (StatementBlock) originalComments[0].getParent().getASTParent();
int childIndex = astParent.getIndexOfChild(originalComments[0].getParent());

var statement = stat.getAssignment();

// parse statement, attach to AST
de.uka.ilkd.key.java.Position pos =
de.uka.ilkd.key.java.Position.fromToken(stat.getAssignment().start);
try {
String assignment = getFullText(stat.getAssignment()).substring(3);
String assignment = getFullText(statement).substring(3);
List<Statement> stmtList = services.getProgramFactory().parseStatements(assignment);
assert stmtList.size() == 1;
CopyAssignment assignStmt = (CopyAssignment) stmtList.get(0);
updatePositionInformation(assignStmt, pos);
doAttach(assignStmt, astParent, childIndex);
var setStatement = (CopyAssignment) stmtList.get(0);
var set = new SetStatement(setStatement, statement);
updatePositionInformation(set, pos);
doAttach(set, astParent, childIndex);
} catch (Throwable e) {
throw new SLTranslationException(e.getMessage() + " (" + e.getClass().getName() + ")",
Location.fromToken(stat.getAssignment().start), e);
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,48 @@
/* 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.java.recoderext;

import de.uka.ilkd.key.speclang.njml.JmlParser;

import recoder.java.expression.operator.CopyAssignment;

/**
* Wrapper for JML set statements which lifts the contained parse tree to the Translator.
*
* @author Julian Wiesler
*/
public class SetStatement extends CopyAssignment {
/**
* Parser context of the assignment
*/
private final JmlParser.Set_statementContext context;

/**
* Primary constructor
*
* @param proto the copy assignment
* @param context the context of the assignment
*/
public SetStatement(CopyAssignment proto, JmlParser.Set_statementContext context) {
super(proto);
this.context = context;
}

/**
* {@inheritDoc}
*/
@Override
public SetStatement deepClone() {
return new SetStatement(this, this.context);
}

/**
* Gets the contained parser context
*
* @return the parser context
*/
public JmlParser.Set_statementContext getParserContext() {
return context;
}
}
Loading
Loading