Merge branch 'main' into more-general-equalsModProperty

.github/workflows/code_quality.yml

@@ -19,10 +19,10 @@ jobs:
           java-version: 21
           distribution: 'corretto'
           cache: 'gradle'
+      - name: Setup Gradle
+        uses: gradle/actions/setup-gradle@v3.3.2
       - name: Build with Gradle
-        uses: gradle/gradle-build-action@v3.3.2
-        with:
-          arguments: -DENABLE_NULLNESS=true compileTest
+        run: ./gradlew -DENABLE_NULLNESS=true compileTest
 
 
   qodana:
@@ -48,10 +48,10 @@ jobs:
           distribution: 'corretto'
           java-version: '21'
           cache: 'gradle'
-      - name: Build with Gradle
-        uses: gradle/gradle-build-action@v3.3.2
-        with:
-          arguments: --continue spotlessCheck
+      - name: Setup Gradle
+        uses: gradle/actions/setup-gradle@v3.3.2
+      - name: SpotlessCheck
+        run: ./gradlew --continue spotlessCheck
 
   # checkstyle:
   #   runs-on: ubuntu-latest
@@ -80,11 +80,10 @@ jobs:
           distribution: 'corretto'
           java-version: '21'
           cache: 'gradle'
-
-      - name: Build with Gradle
-        uses: gradle/gradle-build-action@v3.3.2
-        with:
-          arguments: --continue checkstyleMainChanged
+      - name: Setup Gradle
+        uses: gradle/actions/setup-gradle@v3.3.2
+      - name: Checkstyle
+        run: ./gradlew --continue checkstyleMainChanged
       - run: |
           npx violations-command-line -sarif sarif-report.json \
           -v "CHECKSTYLE" "." ".*/build/reports/checkstyle/main_diff.xml$" "Checkstyle"
@@ -108,10 +107,10 @@ jobs:
           distribution: 'corretto'
           java-version: '21'
           cache: 'gradle'
-      - name: Build with Gradle
-        uses: gradle/gradle-build-action@v3.3.2
-        with:
-          arguments: --continue pmdMainChanged
+      - name: Setup Gradle
+        uses: gradle/actions/setup-gradle@v3.3.2
+      - name: PMD checks
+        run: ./gradlew --continue pmdMainChanged
 
       # - run: python3 ./.github/printAnnotations.py */build/reports/pmd/main.xml
 

.github/workflows/gradle-publish.yml

@@ -21,17 +21,15 @@ jobs:
         cache: 'gradle'
         server-id: github # Value of the distributionManagement/repository/id field of the pom.xml
 
+    - name: Setup Gradle
+      uses: gradle/actions/setup-gradle@v3.3.2
     - name: Assemble with Gradle
-      uses: gradle/gradle-build-action@v3.3.2
-      with:
-        arguments: assemble
+      run: ./gradlew assemble
 
     # The USERNAME and TOKEN need to correspond to the credentials environment variables used in
     # the publishing section of your build.gradle
     - name: Publish to GitHub Packages
-      uses: gradle/gradle-build-action@v3.3.2
-      with:
-        arguments: publish
+      run: ./gradlew publish
       env:
         USERNAME: ${{ github.actor }}
         TOKEN: ${{ secrets.GITHUB_TOKEN }}

.github/workflows/javadoc.yml

@@ -18,11 +18,10 @@ jobs:
           java-version: '21'
           distribution: 'corretto'
           cache: 'gradle'
-
-      - name: Build with Gradle
-        uses: gradle/gradle-build-action@v3.3.2
-        with:
-          arguments: alldoc
+      - name: Setup Gradle
+        uses: gradle/actions/setup-gradle@v3.3.2
+      - name: Build Documentation with Gradle
+        run: ./gradlew alldoc
 
       - name: Package
         run: tar cvfj javadoc.tar.bz2 build/docs/javadoc

.github/workflows/nightlydeploy.yml

@@ -30,10 +30,10 @@ jobs:
           java-version: 17
           distribution: 'temurin'
 
+      - name: Setup Gradle
+        uses: gradle/actions/setup-gradle@v3.3.2
       - name: Build with Gradle
-        uses: gradle/gradle-build-action@v3.3.2
-        with:
-          arguments: --parallel assemble
+        run: ./gradlew --parallel assemble
 
       - name: Delete previous nightly release
         continue-on-error: true

.github/workflows/opttest.yml

@@ -24,10 +24,10 @@ jobs:
           distribution: 'corretto'
           cache: 'gradle'
 
-      - name: Build with Gradle
-        uses: gradle/gradle-build-action@v3.3.2
-        with:
-          arguments: --continue ${{ matrix.tests }}
+      - name: Setup Gradle
+        uses: gradle/actions/setup-gradle@v3.3.2
+      - name: Test with Gradle
+        run: ./gradlew --continue ${{ matrix.tests }}
 
       - name: Upload test results
         uses: actions/upload-artifact@v4

.github/workflows/tests.yml

@@ -37,10 +37,10 @@ jobs:
           distribution: 'corretto'
           cache: 'gradle'
 
-      - name: Build with Gradle
-        uses: gradle/gradle-build-action@v3.3.2
-        with:
-          arguments: --continue -DjacocoEnabled=true -x :key.core.symbolic_execution:test -x :key.core.proof_references:test test
+      - name: Setup Gradle
+        uses: gradle/actions/setup-gradle@v3.3.2
+      - name: Test with Gradle
+        run: ./gradlew --continue -DjacocoEnabled=true -x :key.core.symbolic_execution:test -x :key.core.proof_references:test test
 
       - name: Upload test results
         uses: actions/upload-artifact@v4
@@ -86,11 +86,10 @@ jobs:
         run: .github/dlsmt.sh
         shell: bash
 
-
+      - name: Setup Gradle
+        uses: gradle/actions/setup-gradle@v3.3.2
       - name: "Running tests: ${{ matrix.test }}"
-        uses: gradle/gradle-build-action@v3.3.2
-        with:
-          arguments: --continue ${{ matrix.test }}
+        run: ./gradlew --continue ${{ matrix.test }}
 
       - name: Upload test results
         uses: actions/upload-artifact@v4

.github/workflows/tests_winmac.yml

@@ -28,10 +28,11 @@ jobs:
           distribution: 'corretto'
           cache: 'gradle'
 
-      - name: Build with Gradle
-        uses: gradle/gradle-build-action@v3.3.2
-        with:
-          arguments: --continue -x :key.core.symbolic_execution:test -x :key.core.proof_references:test test
+      - name: Setup Gradle
+        uses:
+          gradle/actions/setup-gradle@v3.3.2
+      - name: Test with Gradle
+        run: ./gradlew --continue -x :key.core.symbolic_execution:test -x :key.core.proof_references:test test
 
       - name: Upload test results
         uses: actions/upload-artifact@v4
@@ -74,10 +75,10 @@ jobs:
       - name: Install SMT-Solvers
         run: .github/dlsmt.sh
 
+      - name: Setup Gradle
+        uses: gradle/actions/setup-gradle@v3.3.2
       - name: "Running tests: ${{ matrix.test }}"
-        uses: gradle/gradle-build-action@v3.3.2
-        with:
-          arguments: --continue ${{ matrix.test }}
+        run: ./gradlew --continue ${{ matrix.test }}
 
       - name: Upload test results
         uses: actions/upload-artifact@v4

key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java

@@ -681,6 +681,18 @@ public ChoiceExpr visitOption_expr_paren(KeYParser.Option_expr_parenContext ctx)
 
     @Override
     public ChoiceExpr visitOption_expr_prop(KeYParser.Option_expr_propContext ctx) {
+        String category = ctx.option().cat.getText();
+        String value = ctx.option().value.getText();
+        String choiceStr = category + ":" + value;
+        /*
+         * Make sure that the choice (category and value!) is known to KeY, i.e. that it is declared
+         * in the file `optionsDeclarations.key`. This prevents from accidentally deactivating
+         * (parts of) taclets due to non-existing choices (see
+         * https://github.com/KeYProject/key/issues/3352).
+         */
+        if (choices().lookup(choiceStr) == null) {
+            semanticError(ctx, "Could not find choice: %s", category + ":" + choiceStr);
+        }
         return ChoiceExpr.variable(ctx.option().cat.getText(), ctx.option().value.getText());
     }
 

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

@@ -396,7 +396,6 @@ private void setUpProofHelper(ProofOblInput problem, ProofAggregate pl)
             throw new ProofInputException("No proof");
         }
 
-        // register non-built-in rules
         // register non-built-in rules
         Proof[] proofs = pl.getProofs();
         reportStatus("Registering rules", proofs.length * 10);

key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java

@@ -166,6 +166,8 @@ public Taclet generateRelationalRepresentsTaclet(Name tacletName, Term originalA
             new RewriteTacletGoalTemplate(addedSeq, ImmutableSLList.nil(), findTerm);
 
         // choices, rule set
+        // Be careful that the choices used here is actually declared (see optionsDeclarations.key),
+        // otherwise the taclet will be unusable!
         var choice = ChoiceExpr.variable("modelFields",
             satisfiabilityGuard ? "showSatisfiability" : "treatAsAxiom");
         final RuleSet ruleSet = new RuleSet(

key.core/src/main/java/de/uka/ilkd/key/settings/ChoiceSettings.java

@@ -34,14 +34,14 @@ public class ChoiceSettings extends AbstractSettings {
 
     private static final String PROP_CHOICE_DEFAULT = "category2Default";
     private static final String PROP_CHOICE_CATEGORIES = "category2Choices";
-    private HashMap<String, String> category2Default;
 
 
     /**
      * maps categories to a set of Strings(representing the choices which are options for this
      * category).
      */
     private Map<String, Set<String>> category2Choices = new LinkedHashMap<>();
+    private Map<String, String> category2Default;
 
 
     public ChoiceSettings() {

key.core/src/main/java/de/uka/ilkd/key/speclang/SLEnvInput.java

@@ -5,9 +5,7 @@
 
 import java.io.File;
 import java.net.URL;
-import java.util.Arrays;
-import java.util.List;
-import java.util.Set;
+import java.util.*;
 
 import de.uka.ilkd.key.java.JavaInfo;
 import de.uka.ilkd.key.java.JavaReduxFileCollection;
@@ -16,6 +14,7 @@
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.java.StatementBlock;
 import de.uka.ilkd.key.java.abstraction.KeYJavaType;
+import de.uka.ilkd.key.java.abstraction.Type;
 import de.uka.ilkd.key.java.declaration.ClassDeclaration;
 import de.uka.ilkd.key.java.declaration.InterfaceDeclaration;
 import de.uka.ilkd.key.java.declaration.TypeDeclaration;
@@ -332,6 +331,21 @@ private ImmutableSet<PositionedString> createSpecs(SpecExtractor specExtractor)
                     specExtractor.extractMethodSpecs(pm, staticInvPresent);
                 specRepos.addSpecs(methodSpecs);
 
+                Type declaringType = pm.getContainerType().getJavaType();
+
+                // Create default contracts for all methods except KeY default methods (like <init>)
+                // and Object methods.
+                if (methodSpecs.isEmpty()
+                        && (declaringType instanceof TypeDeclaration decl && decl.isLibraryClass())
+                        && !declaringType.getFullName().equals("java.lang.Object")
+                        && !pm.isImplicit()) {
+                    specRepos.addContract(specExtractor.createDefaultContract(pm,
+                        initConfig.getActivatedChoices().exists(
+                            choice -> choice.category().equals("soundDefaultContracts")
+                                    && choice.name().toString()
+                                            .equals("soundDefaultContracts:on"))));
+                }
+
                 addLoopInvariants(specExtractor, specRepos, kjt, pm);
                 addLoopContracts(specExtractor, specRepos, kjt, pm);
                 addBlockAndLoopContracts(specExtractor, specRepos, pm);

key.core/src/main/java/de/uka/ilkd/key/speclang/SpecExtractor.java

@@ -109,4 +109,6 @@ ImmutableSet<LoopContract> extractLoopContracts(IProgramMethod method,
      * unsupported features which have been ignored by the translation)
      */
     ImmutableList<PositionedString> getWarnings();
+
+    Contract createDefaultContract(IProgramMethod pm, boolean useSoundDefault);
 }

key.core/src/main/java/de/uka/ilkd/key/speclang/WellDefinednessCheck.java

@@ -669,11 +669,10 @@ static RewriteTaclet createTaclet(String name, Term find1, Term find2, Term goal
         assert find1.sub(0).op().name().equals(find2.sub(0).op().name());
         assert find1.sub(0).arity() == find2.sub(0).arity();
 
-        Map<ProgramVariable, ProgramVariable> map =
-            new LinkedHashMap<>();
+        Map<Operator, Operator> map = new LinkedHashMap<>();
         int i = 0;
         for (Term sub : find1.sub(0).subs()) {
-            map.put((ProgramVariable) find2.sub(0).sub(i).op(), (ProgramVariable) sub.op());
+            map.put(find2.sub(0).sub(i).op(), sub.op());
             i++;
         }
         final OpReplacer or = new OpReplacer(map, services.getTermFactory());

key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java

@@ -740,4 +740,9 @@ public LoopSpecification extractLoopInvariant(IProgramMethod pm, LoopStatement l
     public ImmutableList<PositionedString> getWarnings() {
         return warnings.append(JMLTransformer.getWarningsOfLastInstance());
     }
+
+    @Override
+    public Contract createDefaultContract(IProgramMethod method, boolean useSoundDefault) {
+        return jsf.createDefaultContract(method, useSoundDefault);
+    }
 }

key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java

@@ -205,6 +205,48 @@ private ImmutableSet<Contract> createInformationFlowContracts(ContractClauses cl
         return symbDatas;
     }
 
+    public Contract createDefaultContract(IProgramMethod method, boolean useSoundDefault) {
+        ProgramVariableCollection progVarCollection = createProgramVariables(method);
+        LocationVariable heap = services.getTypeConverter().getHeapLDT().getHeap();
+        Term excNull = tb.equals(tb.var(progVarCollection.excVar), tb.NULL());
+
+        if (useSoundDefault) {
+            return cf.func(
+                generateName(method, Behavior.BEHAVIOR, null), // base name
+                method, // program method
+                false, // terminates
+                Map.of(heap, tb.tt()), // pre
+                Map.of(heap, tb.tt()), // freePre
+                null, // measuredBy
+                Map.of(heap, tb.tt()), // post
+                Map.of(heap, tb.tt()), // freePost
+                Map.of(), // axioms
+                Map.of(heap, tb.allLocs()), // mod
+                Map.of(heap, tb.allLocs()), // freeMod
+                Map.of(heap, tb.allLocs()), // accessible
+                Map.of(heap, true), // has mod
+                Map.of(heap, true), // has free mod
+                progVarCollection);
+        } else {
+            return cf.func(
+                generateName(method, Behavior.NORMAL_BEHAVIOR, null), // base name
+                method, // program method
+                true, // terminates
+                Map.of(heap, tb.tt()), // pre
+                Map.of(heap, tb.tt()), // freePre
+                null, // measuredBy
+                Map.of(heap, excNull), // post
+                Map.of(heap, tb.tt()), // freePost
+                Map.of(), // axioms
+                Map.of(heap, tb.empty()), // mod
+                Map.of(heap, tb.empty()), // freeMod
+                Map.of(heap, tb.empty()), // accessible
+                Map.of(heap, false), // has mod
+                Map.of(heap, false), // has free mod
+                progVarCollection);
+        }
+    }
+
     // -------------------------------------------------------------------------
     // internal classes
     // -------------------------------------------------------------------------

key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/io/PrintStream.java

@@ -14,6 +14,7 @@ public class PrintStream extends java.io.FilterOutputStream {
     public void print(char[] s);
     public void print(java.lang.String s);
     public void print(java.lang.Object obj);
+    public void printf(java.lang.String s, Object... args);
     public void println();
     public void println(boolean x);
     public void println(char x);

key.core/src/main/resources/de/uka/ilkd/key/proof/rules/intRulesJavaSemantics.key

@@ -119,7 +119,7 @@
 // --------------------------------------------------------------------------
 // Axioms defining the integer translation functions
 // --------------------------------------------------------------------------
-\rules(programRules:Java, intRules:javaSemantics) {
+\rules(programRules:Java & (intRules:javaSemantics | intRules:arithmeticSemanticsCheckingOF)) {
     expandInByte {
         \find(inByte(i))
         \replacewith(inRangeByte(i))
@@ -149,7 +149,9 @@
         \replacewith(inRangeLong(i))
         \heuristics(concrete)
     };
+}
 
+\rules(programRules:Java, intRules:javaSemantics) {
     translateJavaUnaryMinusInt {
         \find(javaUnaryMinusInt(left))
         \replacewith(unaryMinusJint(left))