Nullness Type System for key.core

.github/workflows/code_quality.yml

@@ -24,21 +24,6 @@ jobs:
       - name: Build with Gradle
         run: ./gradlew -DENABLE_NULLNESS=true compileTest
 
-
-  qodana:
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v4
-        with:
-          fetch-depth: 0
-      - name: 'Qodana Scan'
-        uses: JetBrains/qodana-action@v2024.1.8
-
-      - uses: github/codeql-action/upload-sarif@v3
-        if: success() || failure()
-        with:
-          sarif_file: ${{ runner.temp }}/qodana/results/qodana.sarif.json
-
   formatting:
     runs-on: ubuntu-latest
     steps:
@@ -52,74 +37,3 @@ jobs:
         uses: gradle/actions/setup-gradle@v3.5.0
       - name: SpotlessCheck
         run: ./gradlew --continue spotlessCheck
-
-  # checkstyle:
-  #   runs-on: ubuntu-latest
-  #   steps:
-  #     - uses: actions/checkout@v4
-  #       with:
-  #         fetch-depth: 0
-  #     - run: scripts/tools/checkstyle/runIncrementalCheckstyle.sh --xml | tee report.xml
-  #     - run: |
-  #         npx violations-command-line -sarif sarif-report.json \
-  #         -v "CHECKSTYLE" "." ".*/report.xml$" "Checkstyle"     \
-  #         -diff-to $(git merge-base HEAD origin/main) -pv false
-
-  #     - uses: github/codeql-action/upload-sarif@v3
-  #       if: success() || failure()
-  #       with:
-  #         sarif_file: sarif-report.json
-
-
-  checkstyle_new:
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v4
-      - uses: actions/setup-java@v4
-        with:
-          distribution: 'corretto'
-          java-version: '21'
-          cache: 'gradle'
-      - name: Setup Gradle
-        uses: gradle/actions/setup-gradle@v3.5.0
-      - name: Checkstyle
-        run: ./gradlew --continue checkstyleMainChanged
-      - run: |
-          npx violations-command-line -sarif sarif-report.json \
-          -v "CHECKSTYLE" "." ".*/build/reports/checkstyle/main_diff.xml$" "Checkstyle"
-
-      #-diff-from $(git merge-base HEAD origin/main)
-      # - run: python3 ./.github/printcs.py */build/reports/checkstyle/main_diff.xml
-
-      # $(git merge-base HEAD origin/main)
-
-      - uses: github/codeql-action/upload-sarif@v3
-        if: success() || failure()
-        with:
-          sarif_file: sarif-report.json          
-
-  pmd:
-    runs-on: ubuntu-latest      
-    steps:
-      - uses: actions/checkout@v4
-      - uses: actions/setup-java@v4
-        with:
-          distribution: 'corretto'
-          java-version: '21'
-          cache: 'gradle'
-      - name: Setup Gradle
-        uses: gradle/actions/setup-gradle@v3.5.0
-      - name: PMD checks
-        run: ./gradlew --continue pmdMainChanged
-
-      # - run: python3 ./.github/printAnnotations.py */build/reports/pmd/main.xml
-
-      - run: |
-          npx violations-command-line -sarif pmd-report.json \
-          -v "PMD" "." ".*/build/reports/pmd/main_diff.xml$" "PMD"
-
-      # -diff-from $(git merge-base HEAD origin/main)
-      - name: Upload SARIF file
-        uses: github/codeql-action/upload-sarif@v3
-        with:
-          sarif_file: pmd-report.json

.github/workflows/sonarqube.yml

@@ -0,0 +1,49 @@
+## Copied from SonarCloud
+
+name: SonarCloud
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+    types: [opened, synchronize, reopened]
+
+jobs:
+  build:
+    name: Build and analyze
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          fetch-depth: 0  # Shallow clones should be disabled for a better relevancy of analysis
+      - name: Set up JDK 21
+        uses: actions/setup-java@v3
+        with:
+          java-version: 21
+          distribution: 'zulu' 
+      - name: Cache SonarCloud packages
+        uses: actions/cache@v3
+        with:
+          path: ~/.sonar/cache
+          key: ${{ runner.os }}-sonar
+          restore-keys: ${{ runner.os }}-sonar
+      - name: Cache Gradle packages
+        uses: actions/cache@v3
+        with:
+          path: ~/.gradle/caches
+          key: ${{ runner.os }}-gradle-${{ hashFiles('**/*.gradle') }}
+          restore-keys: ${{ runner.os }}-gradle
+
+      - name: Generate and submit dependency graph
+        uses: gradle/actions/dependency-submission@v3
+        with:
+            build-scan-publish: true
+            build-scan-terms-of-use-url: "https://gradle.com/terms-of-service"
+            build-scan-terms-of-use-agree: "yes"
+
+      - name: Build and analyze
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}  # Needed to get PR information, if any
+          SONAR_TOKEN: ${{ secrets.SONAR_TOKEN }}
+          GRADLE_OPTS: "-Xmx6g -XX:MaxMetaspaceSize=512m  -Dfile.encoding=UTF-8"
+        run: ./gradlew --parallel --continue  -DjacocoEnabled=true -x :key.core.symbolic_execution:test -x :key.core.proof_references:test classes testClasses :key.util:test jacocoTestReport sonar

build.gradle

@@ -25,8 +25,19 @@ plugins {
 
     // EISOP Checker Framework
     id "org.checkerframework" version "0.6.41"
+
+    id("org.sonarqube") version "5.0.0.4638"
+}
+
+sonar {
+  properties {
+    property "sonar.projectKey", "KeYProject_key"
+    property "sonar.organization", "keyproject"
+    property "sonar.host.url", "https://sonarcloud.io"
+  }
 }
 
+
 // Configure this project for use inside IntelliJ:
 idea {
     module {

gradle.properties

@@ -0,0 +1 @@
+org.gradle.jvmargs=-Xmx2g -XX:MaxMetaspaceSize=512m -Dfile.encoding=UTF-8

key.core/build.gradle

@@ -266,3 +266,20 @@ task generateRAPUnitTests(type: JavaExec) {
 sourceSets.test.java.srcDirs("$buildDir/generated-src/rap/")
 
 sourcesJar.dependsOn(runAntlr4Jml, runAntlr4Key, compileJavacc, generateGrammarSource)
+
+
+checkerFramework {
+    if(System.getProperty("ENABLE_NULLNESS")) {
+        checkers = [
+                "org.checkerframework.checker.nullness.NullnessChecker",
+        ]
+        extraJavacArgs = [
+                "-AonlyDefs=^de\\.uka\\.ilkd\\.key\\.(ldt|macros|settings)",
+                "-Xmaxerrs", "10000",
+                "-Astubs=$rootDir/key.util/src/main/checkerframework:permit-nullness-assertion-exception.astub",
+                "-AstubNoWarnIfNotFound",
+                "-Werror",
+                "-Aversion",
+        ]
+    }
+}

key.core/src/main/java/de/uka/ilkd/key/java/declaration/ArrayDeclaration.java

@@ -207,8 +207,7 @@ public static ProgramElementName createName(TypeReference basetype) {
         } else if (javaBasetype instanceof PrimitiveType) {
             return ((PrimitiveType) javaBasetype).getArrayElementName();
         }
-        assert false;
-        return null;
+        throw new RuntimeException("Not Implemented");
     }
 
 

key.core/src/main/java/de/uka/ilkd/key/java/reference/FieldReference.java

@@ -10,6 +10,8 @@
 
 import org.key_project.util.ExtList;
 
+import org.jspecify.annotations.Nullable;
+
 
 public class FieldReference extends VariableReference
         implements MemberReference, ReferenceSuffix, TypeReferenceContainer, ExpressionContainer {
@@ -28,7 +30,7 @@ protected FieldReference(ReferencePrefix prefix) {
         this.prefix = prefix;
     }
 
-    public FieldReference(ProgramVariable pv, ReferencePrefix prefix) {
+    public FieldReference(ProgramVariable pv, @Nullable ReferencePrefix prefix) {
         this(pv, prefix, PositionInfo.UNDEFINED);
     }