Merge branch 'refs/heads/main' into weigl/key-javaparser3

* refs/heads/main: (63 commits)
  unified naming of operator to "seq_upd".
  Bump org.ow2.asm:asm from 9.6 to 9.7
  reformat after merge
  fix hashing of set statements and assert statements
  Typo in message in dlsmt.sh
  More logging in run all proofs
  Infrastructure for selection of proof groups
  Update pull_request_template.md
  fix check for cvc5
  exit in error in dlsmt.sh
  fix cvc5
  fix smt solver downloader script for z3
  added references to hard-coded rulesets
  applying spotless
  replacing "\seq_length(x)" by "x.length" in set statements in examples
  fix rap for SetStatmentRule
  fix rap for JmlAssertRule
  repair unit tests
  Update broken link in README.md
  different highlighting for JML statements
  ...

# Conflicts:
#	key.core/src/main/java/de/uka/ilkd/key/java/JavaTools.java
#	key.core/src/main/java/de/uka/ilkd/key/java/KeYJavaASTFactory.java
#	key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java
#	key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/adt/SeqPut.java
#	key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/JmlAssert.java
#	key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/SetStatement.java
#	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/JMLTransformer.java
#	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/JmlAssert.java
#	key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java
#	key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgVarReplaceVisitor.java
#	key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramVariableCollector.java
#	key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java
#	key.core/src/main/java/de/uka/ilkd/key/ldt/SeqLDT.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/JavaBlock.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java
#	key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/mgt/SpecificationRepository.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/AuxiliaryContractBuilders.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/JmlAssertRule.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FieldTypeToSortCondition.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StaticFieldCondition.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/IntroAtPreDefsOp.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/SLEnvInput.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java
#	key.core/src/test/java/de/uka/ilkd/key/java/ProofJavaProgramFactoryTest.java
#	key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/ProofCollection.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.java

.github/dlsmt.sh

@@ -1,6 +1,6 @@
 # No shebang!
 
-## Weigl's little helper to download SMT-solvers. 
+## Weigl's little helper to download SMT-solvers.
 # SPDX-License-Identifier: GPL-2.0-or-later
 
 # This script is meant to be executed inside an Github Action to download the SMT-solver. 
@@ -27,6 +27,7 @@
 mkdir smt-solvers
 cd smt-solvers
 
+set -x # exit on error
 
 #################################################
 echo "::group::{install z3}"
@@ -36,7 +37,10 @@ if readlink -f */bin/z3; then
   echo "::notice::{Z3 found. Caching works! Skip installation}"
 else 
   echo "Download Z3"
-  gh release download --skip-existing -p 'z3-*-x64-glibc-*.zip' -R Z3Prover/z3
+  rm z3-*.zip
+  # gh release download --skip-existing -p 'z3-*-x64-glibc-2.35.zip' -R Z3Prover/z3
+  ## pin to a release
+  wget -q https://github.com/Z3Prover/z3/releases/download/z3-4.13.0/z3-4.13.0-x64-glibc-2.35.zip
   unzip -n z3*.zip
   rm z3-*-x64-glibc-*.zip  
 fi
@@ -51,14 +55,19 @@ echo "::endgroup::"
 
 #################################################
 echo "::group::{install cvc5}"
-if -f cvc5-Linux; then 
-  echo "::notice::{Z3 found. Caching works! Skip installation}"
+if -f cvc5-Linux-static/bin/cvc5; then
+  echo "::notice::{CVC5 found. Caching works! Skip installation}"
 else 
   echo "Install CVC5"
-  gh release download --skip-existing -p 'cvc5-Linux' -R cvc5/cvc5  
+  # does not work anymore
+  # gh release download --skip-existing -p 'cvc5-Linux' -R cvc5/cvc5
+
+  wget -q https://github.com/cvc5/cvc5/releases/download/cvc5-1.1.2/cvc5-Linux-static.zip
+  unzip cvc5-Linux-static.zip
+  rm cvc5-Linux-static.zip
 fi 
 
-CVC5=$(readlink -f cvc5-Linux)
+CVC5=$(readlink -f cvc5-Linux-static/bin/cvc5)
 echo "CVC5 installed and added to path: CVC5"
 chmod u+x $CVC5
 echo $(dirname $CVC5) >> $GITHUB_PATH

.github/pull_request_template.md

@@ -2,8 +2,8 @@
 Thanks for submitting this pull request for KeY.
 Since the project has a strict review policy, please make the
 reviewer's job easier by providing the necessary information
-in the text below. The comments may remain since they will be
-invisible when showing the PR.
+in the text below. The comments can be deleted, but may also 
+remain since they will be invisible when showing the PR.
 -->
 
 ## Related Issue
@@ -17,26 +17,48 @@ This pull request addresses #.
 <!-- Please give a brief description of what behaviour changes and 
      why it should be changed. -->
 
+## Plan
+
+<!-- If this pull request is not yet finished, but has open jobs,
+     please list them here. It helps others to estimate the state of this
+     PR. This list can and should be adapted as the PR develops.
+     Items should be crossed out when finished, not deleted.
+     
+     Remove the section if the PR was finished at submission time.
+     The following items are examples:
+-->
+* [ ] Implement feature 1
+* [ ] Implement feature 2
+* [ ] Code cleanup
+* [ ] Document the changes
+
 ## Type of pull request
 
-<!--- What types of changes does your code introduce? Put an `x` in the box(es) that apply: -->
+<!--- What types of changes does your code introduce? 
+      Delete those lines that do not apply.      
+-->
 
-- [ ] Bug fix (non-breaking change which fixes an issue)
-- [ ] Refactoring (behaviour should not change or only minimally change)
-- [ ] New feature (non-breaking change which adds functionality)
-- [ ] Breaking change (fix or feature that would cause existing functionality to change)
-- [ ] There are changes to the (Java) code
-- [ ] There are changes to the taclet rule base
-- [ ] There are changes to the deployment/CI infrastructure (gradle, github, ...)
-- [ ] Other: 
+- Bug fix (non-breaking change which fixes an issue)
+- Refactoring (behaviour should not change or only minimally change)
+- New feature (non-breaking change which adds functionality)
+- Breaking change (fix or feature that would cause existing functionality to change)
+- There are changes to the (Java) code
+- There are changes to the taclet rule base
+- There are changes to the deployment/CI infrastructure (gradle, github, ...)
+- Other: 
 
 ## Ensuring quality
+
+<!--- How did you make sure that the proposed change improves the code base? 
+      Delete those lines that do not apply.
+      Please make an effort to delete as few lines as possible. :-)
+-->
 
-- [ ] I made sure that introduced/changed code is well documented (javadoc and inline comments).
-- [ ] I made sure that new/changed end-user features are well documented (https://github.com/KeYProject/key-docs).
-- [ ] I added new test case(s) for new functionality.
-- [ ] I have tested the feature as follows: ...
-- [ ] I have checked that runtime performance has not deteriorated.
+- I made sure that introduced/changed code is well documented (javadoc and inline comments).
+- I made sure that new/changed end-user features are well documented (https://github.com/KeYProject/key-docs).
+- I added new test case(s) for new functionality.
+- I have tested the feature as follows: ...
+- I have checked that runtime performance has not deteriorated.
 
 ## Additional information and contact(s)
 

README.md

@@ -20,7 +20,7 @@ The current version of KeY is 2.12.2, licensed under GPL v2.
 Feel free to use the project templates to get started using KeY:
 * [For Verification Projects](https://github.com/KeYProject/verification-project-template)
 * [Using as a Library](https://github.com/KeYProject/key-java-example)
-* [Using as a Symbolic Execution Backend](https://github.com/KeYProject/key-symbex-example)
+* [Using as a Symbolic Execution Backend](https://github.com/KeYProject/symbex-java-example)
 
 ## Requirements
 

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

@@ -31,6 +31,8 @@
 import org.key_project.logic.sort.Sort;
 import org.key_project.util.collection.ImmutableList;
 
+import org.jspecify.annotations.NonNull;
+
 /**
  * <p>
  * A {@link BuiltInRule} which evaluates a query in a side proof.
@@ -187,6 +189,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

@@ -335,7 +335,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/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java

@@ -77,6 +77,9 @@
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 
+import static de.uka.ilkd.key.logic.equality.IrrelevantTermLabelsProperty.IRRELEVANT_TERM_LABELS_PROPERTY;
+import static de.uka.ilkd.key.logic.equality.RenamingProperty.RENAMING_PROPERTY;
+
 /**
  * Provides utility methods for symbolic execution with KeY.
  *
@@ -393,7 +396,7 @@ else if (term.op() == Junctor.NOT) {
      * @return true if the term represents the one
      */
     private static boolean isOne(Term subOne, IntegerLDT integerLDT) {
-        return subOne.equalsModIrrelevantTermLabels(integerLDT.one());
+        return subOne.equalsModProperty(integerLDT.one(), IRRELEVANT_TERM_LABELS_PROPERTY);
     }
 
     /**
@@ -1984,13 +1987,16 @@ private static void collectSpecifcationCasesPreconditions(Term normalExcDefiniti
             List<Term> exceptinalConditions) throws ProofInputException {
         if (term.op() == Junctor.AND) {
             Term lastChild = term.sub(term.arity() - 1);
-            if (lastChild.equalsModIrrelevantTermLabels(normalExcDefinition)
-                    || lastChild.equalsModIrrelevantTermLabels(exceptionalExcDefinition)) {
+            if (lastChild.equalsModProperty(normalExcDefinition, IRRELEVANT_TERM_LABELS_PROPERTY)
+                    || lastChild.equalsModProperty(exceptionalExcDefinition,
+                        IRRELEVANT_TERM_LABELS_PROPERTY)) {
                 // Nothing to do, condition is just true
             } else {
                 Term firstChild = term.sub(0);
-                if (firstChild.equalsModIrrelevantTermLabels(normalExcDefinition)
-                        || firstChild.equalsModIrrelevantTermLabels(exceptionalExcDefinition)) {
+                if (firstChild
+                        .equalsModProperty(normalExcDefinition, IRRELEVANT_TERM_LABELS_PROPERTY)
+                        || firstChild.equalsModProperty(exceptionalExcDefinition,
+                            IRRELEVANT_TERM_LABELS_PROPERTY)) {
                     // Nothing to do, condition is just true
                 } else {
                     for (int i = 0; i < term.arity(); i++) {
@@ -2002,47 +2008,56 @@ private static void collectSpecifcationCasesPreconditions(Term normalExcDefiniti
             }
         } else if (term.op() == Junctor.IMP) {
             Term leftTerm = term.sub(0);
-            if (leftTerm.equalsModIrrelevantTermLabels(normalExcDefinition)
-                    || leftTerm.equalsModIrrelevantTermLabels(exceptionalExcDefinition)) {
+            if (leftTerm.equalsModProperty(normalExcDefinition, IRRELEVANT_TERM_LABELS_PROPERTY)
+                    || leftTerm.equalsModProperty(exceptionalExcDefinition,
+                        IRRELEVANT_TERM_LABELS_PROPERTY)) {
                 // Nothing to do, condition is just true
             } else {
                 Term rightTerm = term.sub(1);
                 // Deal with heavy weight specification cases
                 if (rightTerm.op() == Junctor.AND && rightTerm.sub(0).op() == Junctor.IMP
                         && rightTerm.sub(0).sub(0)
-                                .equalsModIrrelevantTermLabels(normalExcDefinition)) {
+                                .equalsModProperty(normalExcDefinition,
+                                    IRRELEVANT_TERM_LABELS_PROPERTY)) {
                     normalConditions.add(leftTerm);
                 } else if (rightTerm.op() == Junctor.AND && rightTerm.sub(1).op() == Junctor.IMP
                         && rightTerm.sub(1).sub(0)
-                                .equalsModIrrelevantTermLabels(exceptionalExcDefinition)) {
+                                .equalsModProperty(exceptionalExcDefinition,
+                                    IRRELEVANT_TERM_LABELS_PROPERTY)) {
                     exceptinalConditions.add(leftTerm);
                 }
                 // Deal with light weight specification cases
                 else if (rightTerm.op() == Junctor.IMP
-                        && rightTerm.sub(0).equalsModIrrelevantTermLabels(normalExcDefinition)) {
+                        && rightTerm.sub(0).equalsModProperty(normalExcDefinition,
+                            IRRELEVANT_TERM_LABELS_PROPERTY)) {
                     normalConditions.add(leftTerm);
                 } else if (rightTerm.op() == Junctor.IMP && rightTerm.sub(0)
-                        .equalsModIrrelevantTermLabels(exceptionalExcDefinition)) {
+                        .equalsModProperty(exceptionalExcDefinition,
+                            IRRELEVANT_TERM_LABELS_PROPERTY)) {
                     exceptinalConditions.add(leftTerm);
                 } else {
                     Term excCondition = rightTerm;
                     // Check if right child is exception definition
                     if (excCondition.op() == Junctor.AND) {
                         excCondition = excCondition.sub(excCondition.arity() - 1);
                     }
-                    if (excCondition.equalsModIrrelevantTermLabels(normalExcDefinition)) {
+                    if (excCondition.equalsModProperty(normalExcDefinition,
+                        IRRELEVANT_TERM_LABELS_PROPERTY)) {
                         normalConditions.add(leftTerm);
                     } else if (excCondition
-                            .equalsModIrrelevantTermLabels(exceptionalExcDefinition)) {
+                            .equalsModProperty(exceptionalExcDefinition,
+                                IRRELEVANT_TERM_LABELS_PROPERTY)) {
                         exceptinalConditions.add(leftTerm);
                     } else {
                         // Check if left child is exception definition
                         if (rightTerm.op() == Junctor.AND) {
                             excCondition = rightTerm.sub(0);
-                            if (excCondition.equalsModIrrelevantTermLabels(normalExcDefinition)) {
+                            if (excCondition.equalsModProperty(normalExcDefinition,
+                                IRRELEVANT_TERM_LABELS_PROPERTY)) {
                                 normalConditions.add(leftTerm);
                             } else if (excCondition
-                                    .equalsModIrrelevantTermLabels(exceptionalExcDefinition)) {
+                                    .equalsModProperty(exceptionalExcDefinition,
+                                        IRRELEVANT_TERM_LABELS_PROPERTY)) {
                                 exceptinalConditions.add(leftTerm);
                             } else {
                                 throw new ProofInputException("Exeptional condition expected, "
@@ -2673,7 +2688,7 @@ private static boolean checkReplaceTerm(Term toCheck, PosInOccurrence posInOccur
             Term replaceTerm) {
         Term termAtPio = followPosInOccurrence(posInOccurrence, toCheck);
         if (termAtPio != null) {
-            return termAtPio.equalsModRenaming(replaceTerm);
+            return termAtPio.equalsModProperty(replaceTerm, RENAMING_PROPERTY);
         } else {
             return false;
         }
@@ -3419,11 +3434,13 @@ private static List<Term> findSkolemReplacements(Sequent sequent, Term skolemCon
             if (term != skolemEquality) {
                 int skolemCheck = checkSkolemEquality(term);
                 if (skolemCheck == -1) {
-                    if (term.sub(0).equalsModIrrelevantTermLabels(skolemConstant)) {
+                    if (term.sub(0).equalsModProperty(skolemConstant,
+                        IRRELEVANT_TERM_LABELS_PROPERTY)) {
                         result.add(term.sub(1));
                     }
                 } else if (skolemCheck == 1) {
-                    if (term.sub(1).equalsModIrrelevantTermLabels(skolemConstant)) {
+                    if (term.sub(1).equalsModProperty(skolemConstant,
+                        IRRELEVANT_TERM_LABELS_PROPERTY)) {
                         result.add(term.sub(0));
                     }
                 }
@@ -3513,7 +3530,8 @@ public static Term computePathCondition(Node parentNode, Node childNode, boolean
                 }
                 childNode = parent;
             }
-            if (services.getTermBuilder().ff().equalsModIrrelevantTermLabels(pathCondition)) {
+            if (services.getTermBuilder().ff().equalsModProperty(pathCondition,
+                IRRELEVANT_TERM_LABELS_PROPERTY)) {
                 throw new ProofInputException(
                     "Path condition computation failed because the result is false.");
             }

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/JmlLexer.g4

@@ -280,7 +280,7 @@ SEQCONCAT: '\\seq_concat';  //KeY extension, not official JML
 SEQDEF: '\\seq_def';  //KeY extension, not official JML
 SEQEMPTY: '\\seq_empty';  //KeY extension, not official JML
 SEQGET: '\\seq_get';  //KeY extension, not official JML
-SEQREPLACE: '\\seq_put';  //KeY extension, not official JML
+SEQREPLACE: '\\seq_upd';  //KeY extension, not official JML
 SEQREVERSE: '\\seq_reverse';  //KeY extension, not official JML
 SEQSINGLETON: '\\seq_singleton';  //KeY extension, not official JML
 SEQSUB: '\\seq_sub';  //KeY extension, not official JML