Set statement: Check assignee for validity

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/QuerySideProofRule.java

@@ -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.
@@ -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 {

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/AbstractConditionalBreakpoint.java

@@ -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);

key.core.symbolic_execution/src/test/resources/testcase/set/useOperationContractStatementsInImpliciteConstructor/oracle/UseOperationContractStatementsInImpliciteConstructor.xml

@@ -360,62 +360,13 @@ new IllegalArgumentException("Array can't be null.");" 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>

key.core/src/main/antlr4/JmlParser.g4

@@ -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))?

key.core/src/main/java/de/uka/ilkd/key/informationflow/proof/init/StateVars.java

@@ -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);
     }

key.core/src/main/java/de/uka/ilkd/key/java/JavaTools.java

@@ -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;
@@ -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 {
 
@@ -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;
 
@@ -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);

key.core/src/main/java/de/uka/ilkd/key/java/KeYJavaASTFactory.java

@@ -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;
@@ -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>
      */

key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java

@@ -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;
 
@@ -1119,8 +1120,12 @@ public VariableSpecification convert(
 
             final ProgramElementName name =
                 VariableNamer.parseName(makeAdmissibleName(recoderVarSpec.getName()));
+            var isGhost = containsModifier(recoderVarSpec.getParent(),
+                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());
 
@@ -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).
      */
@@ -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(),
@@ -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());
     }

key.core/src/main/java/de/uka/ilkd/key/java/recoderext/JMLTransformer.java

@@ -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);

key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SetStatement.java

@@ -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;
+    }
+}