Parallelize CI

.github/license-check/config.json

@@ -6,7 +6,8 @@
       "**/*.go",
       "build.sbt",
       "src/main/resources/stubs/github.com/**/*.gobra",
-      "**/Gobra*.g4"
+      "**/Gobra*.g4",
+      "src/test/java/**/*.java"
     ],
     "exclude": [
       "carbon/**",

.github/test-and-measure-ram.sh

@@ -5,10 +5,11 @@
 # start pidstats and write output to synced folder /build/gobra/sync
 pidstat 1 -r -H -p ALL > /build/gobra/sync/pidstat.txt & PIDSTAT_PID=$!
 
-# execute sbt test and stop pidstat independent of outcome
+# execute sbt with the provided $SBTCOMMAND or 'test' and stop pidstat independent of outcome
 # set `-Dsbt.color=always` such that sbt displays warnings in yellow, passed test cases in green and failed ones in red.
 # it seems that sbt on it's own thinks that colors cannot be displayed when run in docker and thus turns them off by default.
-sbt -Dsbt.color=always test
+COMMAND="${SBTCOMMAND:-test}"
+sbt -Dsbt.color=always "$COMMAND"
 TEST_RES=$?
 kill -INT $PIDSTAT_PID
 

.github/workflows/test.yml

@@ -10,10 +10,18 @@ on:
   push: # run this workflow on every push
   pull_request: # run this workflow on every pull_request
 
+env:
+  BUILD_IMAGE_WORKFLOW_ARTIFACT_NAME: gobra-build-image
+  BUILD_IMAGE_FILENAME: build-image.tar
+  FINAL_IMAGE_WORKFLOW_ARTIFACT_NAME: gobra-final-image
+  FINAL_IMAGE_FILENAME: final-image.tar
+
+
 jobs:
-  # there is a single job to avoid copying the built docker image from one job to the other
-  build-test-deploy-container:
+  build-container:
     runs-on: ubuntu-latest
+    outputs:
+      IMAGE_TAG: ${{ steps.output_step.outputs.IMAGE_TAG }}
     env:
       IMAGE_ID: ghcr.io/${{ github.repository_owner }}/gobra
       # image labels are new-line separated key value pairs (according to https://specs.opencontainers.org/image-spec/annotations/):
@@ -24,13 +32,6 @@ jobs:
         org.opencontainers.image.revision=${{ github.sha }}
         org.opencontainers.image.licenses=MPL-2.0
         org.opencontainers.image.description=Gobra image for revision ${{ github.sha }} built by workflow run ${{ github.run_id }}
-      CONCLUSION_SUCCESS: "success"
-      CONCLUSION_FAILURE: "failure"
-      # Output levels according to severity.
-      # They identify the kinds of annotations to be printed by Github.
-      NOTICE_LEVEL: "info"
-      WARNING_LEVEL: "warning"
-      FAILURE_LEVEL: "error"
     steps:
       - name: Checkout Gobra
         uses: actions/checkout@v6
@@ -70,9 +71,6 @@ jobs:
             # use latest tag for default branch and with highest priority (1000 is the highest default priority for the other types):
             type=raw,value=latest,priority=1100,enable={{is_default_branch}}
 
-      - name: Get first tag
-        run: echo "IMAGE_TAG=$(echo "${{ steps.image-metadata.outputs.tags }}" | head -1)" >> $GITHUB_ENV
-
       - name: Build image up to including stage 'build'
         id: image-build
         # note that the action's name is misleading: this step does NOT push
@@ -89,14 +87,110 @@ jobs:
           # use GitHub cache:
           cache-from: type=gha, scope=${{ github.workflow }}
           cache-to: type=gha, scope=${{ github.workflow }}
+          outputs: type=docker,dest=/tmp/${{ env.BUILD_IMAGE_FILENAME }}
+
+      - name: Upload build image
+        uses: actions/upload-artifact@v4
+        with:
+          name: ${{ env.BUILD_IMAGE_WORKFLOW_ARTIFACT_NAME }}
+          path: /tmp/${{ env.BUILD_IMAGE_FILENAME }}
+          retention-days: 1
+
+      - name: Build entire image
+        uses: docker/build-push-action@v6
+        with:
+          context: .
+          load: true # make the built image available in docker (locally)
+          file: workflow-container/Dockerfile
+          tags: ${{ steps.image-metadata.outputs.tags }}
+          labels: ${{ steps.image-metadata.outputs.labels }}
+          push: false
+          provenance: false # without this, GH displays 2 architecture (unknown/unknown) and omits labels
+          # use GitHub cache:
+          cache-from: type=gha, scope=${{ github.workflow }}
+          cache-to: type=gha, scope=${{ github.workflow }}
+          outputs: type=docker,dest=/tmp/${{ env.FINAL_IMAGE_FILENAME }}
+
+      - name: Upload final image
+        uses: actions/upload-artifact@v4
+        with:
+          name: ${{ env.FINAL_IMAGE_WORKFLOW_ARTIFACT_NAME }}
+          path: /tmp/${{ env.FINAL_IMAGE_FILENAME }}
+          retention-days: 1
 
-      - name: Execute all tests
+      - name: Get first tag
+        run: echo "IMAGE_TAG=$(echo "${{ steps.image-metadata.outputs.tags }}" | head -1)" >> $GITHUB_ENV
+
+      - name: Set job output
+        id: output_step
+        run: echo "IMAGE_TAG=${{ env.IMAGE_TAG }}" >> $GITHUB_OUTPUT
+
+
+  prepare-matrix:
+    runs-on: ubuntu-latest
+    outputs:
+      matrix: ${{ steps.set-matrix.outputs.matrix }}
+    steps:
+      - name: Checkout Gobra
+        uses: actions/checkout@v4
+        # we do not need any submodules here as we need the folders containing our test cases
+
+      - id: set-matrix
+        run: |
+          # find subfolders of `regressions` and use those as a natural split of the GobraTests
+          # store these subfolders as a JSON array:
+          REGRESSION_SUBFOLDERS=$(ls src/test/resources/regressions)
+          MATRIX_ENTRIES=''
+          for SUBFOLDER in $REGRESSION_SUBFOLDERS; do
+            MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"GobraTests - regressions/$SUBFOLDER\", \"sbt-command\": \"set javaOptions += \\\"-DGOBRATESTS_REGRESSIONS_DIR=regressions/$SUBFOLDER\\\";  testOnly * -- -n viper.gobra.tags.GobraTestsTag\", \"pidstat-filename\": \"pidstat-GobraTests-$SUBFOLDER.txt\"},"
+          done
+          # add an entry for all other non-GobraTests tests:
+          MATRIX_ENTRIES="$MATRIX_ENTRIES {\"name\": \"All other tests\", \"sbt-command\": \"testOnly * -- -l viper.gobra.tags.GobraTestsTag\", \"pidstat-filename\": \"pidstat-OtherTests.txt\"},"
+          # print matrix for debugging purposes:
+          echo "matrix={\"include\": [$MATRIX_ENTRIES]}"
+          echo "matrix={\"include\": [$MATRIX_ENTRIES]}" >> $GITHUB_OUTPUT
+
+
+  run-all-tests:
+    name: ${{ matrix.name }}
+    runs-on: ubuntu-latest
+    needs: [build-container, prepare-matrix]
+    env:
+      CONCLUSION_SUCCESS: "success"
+      CONCLUSION_FAILURE: "failure"
+      # Output levels according to severity.
+      # They identify the kinds of annotations to be printed by Github.
+      NOTICE_LEVEL: "info"
+      WARNING_LEVEL: "warning"
+      FAILURE_LEVEL: "error"
+      # we do the context expansion here to avoid escaping problems below as explained in https://stackoverflow.com/a/77924154/1990080
+      SBT_COMMAND: ${{ matrix.sbt-command }}
+    strategy:
+      # tests should not be stopped when they fail on one of the OSes:
+      fail-fast: false
+      matrix: ${{ fromJson(needs.prepare-matrix.outputs.matrix) }}
+    steps:
+      # we only need .github/test-and-measure-ram.sh. Thus, we do not checkout the submodules
+      - name: Checkout Gobra
+        uses: actions/checkout@v4
+
+      - name: Download build image
+        uses: actions/download-artifact@v4
+        with:
+          name: ${{ env.BUILD_IMAGE_WORKFLOW_ARTIFACT_NAME }}
+          path: /tmp
+
+      - name: Load image
+        run: docker load --input /tmp/${{ env.BUILD_IMAGE_FILENAME }}
+
+      - name: Execute tests
         run: |
           # create a directory to sync with the docker container and to store the created pidstats
           mkdir -p $PWD/sync
           docker run \
+            -e SBTCOMMAND="$SBT_COMMAND" \
             --mount type=volume,dst=/build/gobra/sync,volume-driver=local,volume-opt=type=none,volume-opt=o=bind,volume-opt=device=$PWD/sync \
-            ${{ env.IMAGE_TAG }} \
+            ${{ needs.build-container.outputs.IMAGE_TAG }} \
             /bin/sh -c "$(cat .github/test-and-measure-ram.sh)"
 
       - name: Get max RAM usage by Java and Z3
@@ -187,27 +281,27 @@ jobs:
         if: ${{ always() }}
         uses: actions/upload-artifact@v6
         with:
-          name: pidstat.txt
+          name: ${{ matrix.pidstat-filename }}
           path: sync/pidstat.txt
 
-      - name: Build entire image
-        uses: docker/build-push-action@v6
+
+  test-final-container-and-deploy:
+    runs-on: ubuntu-latest
+    needs: [build-container, run-all-tests]
+    steps:
+      - name: Download final image
+        uses: actions/download-artifact@v4
         with:
-          context: .
-          load: true # make the built image available in docker (locally)
-          file: workflow-container/Dockerfile
-          tags: ${{ steps.image-metadata.outputs.tags }}
-          labels: ${{ steps.image-metadata.outputs.labels }}
-          push: false
-          provenance: false # without this, GH displays 2 architecture (unknown/unknown) and omits labels
-          # use GitHub cache:
-          cache-from: type=gha, scope=${{ github.workflow }}
-          cache-to: type=gha, scope=${{ github.workflow }}
+          name: ${{ env.FINAL_IMAGE_WORKFLOW_ARTIFACT_NAME }}
+          path: /tmp
+
+      - name: Load image
+        run: docker load --input /tmp/${{ env.FINAL_IMAGE_FILENAME }}
 
       - name: Test final container by verifying a file
         run: |
           docker run \
-            ${{ env.IMAGE_TAG }} \
+            ${{ needs.build-container.outputs.IMAGE_TAG }} \
             -i tutorial-examples/basic-annotations.gobra
 
       - name: Decide whether image should be deployed or not
@@ -234,16 +328,6 @@ jobs:
           username: ${{ github.actor }}
           password: ${{ secrets.GITHUB_TOKEN }}
 
-      - name: Push entire image
+      - name: Push image
         if: env.SHOULD_DEPLOY == 'true'
-        uses: docker/build-push-action@v6
-        with:
-          context: .
-          file: workflow-container/Dockerfile
-          tags: ${{ steps.image-metadata.outputs.tags }}
-          labels: ${{ steps.image-metadata.outputs.labels }}
-          push: true
-          provenance: false # without this, GH displays 2 architecture (unknown/unknown) and omits labels
-          # use GitHub cache:
-          cache-from: type=gha, scope=${{ github.workflow }}
-          cache-to: type=gha, scope=${{ github.workflow }}
+        run: docker push ${{ needs.build-container.outputs.IMAGE_TAG }}

src/test/java/viper/gobra/tags/GobraTestsTag.java

@@ -0,0 +1,21 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2025 ETH Zurich.
+
+package viper.gobra.tags;
+
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+// We define a custom tag to selectively enable / disable GobraTests from SBT.
+// According to the documentation of org.scalatest.Tag, this annotation must be defined in Java
+// as Scala annotations are not available at runtime, which is confirmed by our own experiments.
+
+@org.scalatest.TagAnnotation
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.METHOD, ElementType.TYPE})
+public @interface GobraTestsTag {}

src/test/scala/viper/gobra/GobraTests.scala

@@ -14,17 +14,23 @@ import scalaz.EitherT
 import scalaz.Scalaz.futureInstance
 import viper.gobra.frontend.PackageResolver.RegularPackage
 import viper.gobra.frontend.Source.FromFileSource
-import viper.gobra.frontend.info.Info
+import viper.gobra.frontend.info.{Info, TypeInfo}
 import viper.gobra.frontend.{Config, PackageResolver, Parser, Source}
 import viper.gobra.reporting.VerifierResult.{Failure, Success}
 import viper.gobra.reporting.{GobraMessage, GobraReporter, VerifierError}
+import viper.gobra.tags.GobraTestsTag
 import viper.silver.testing.{AbstractOutput, AnnotatedTestInput, ProjectInfo, SystemUnderTest}
 import viper.silver.utility.TimingUtils
 import viper.gobra.util.{DefaultGobraExecutionContext, GobraExecutionContext}
 
-import scala.concurrent.{Await, Future}
+import java.util.concurrent.atomic.AtomicReference
+import scala.concurrent.{Await, Future, Promise}
 import scala.concurrent.duration.Duration
 
+
+// tag this class with `GobraTestsTag` such that we can run all except this test class
+// (if necessary) by executing `sbt "testOnly * -- -l viper.gobra.GobraTestsTag"`
+@GobraTestsTag
 class GobraTests extends AbstractGobraTests with BeforeAndAfterAll {
 
   val regressionsPropertyName = "GOBRATESTS_REGRESSIONS_DIR"
@@ -36,7 +42,8 @@ class GobraTests extends AbstractGobraTests with BeforeAndAfterAll {
   var gobraInstance: Gobra = _
   var executor: GobraExecutionContext = _
   var inputs: Vector[Source] = Vector.empty
-  val cacheParserAndTypeChecker = true
+  val shouldPreParseAndTypeCheck = true
+  val preParseAndTypeCheckResult: AtomicReference[Option[Future[Vector[Either[Vector[VerifierError], TypeInfo]]]]] = new AtomicReference(None)
 
   override def beforeAll(): Unit = {
     executor = new DefaultGobraExecutionContext()
@@ -55,31 +62,51 @@ class GobraTests extends AbstractGobraTests with BeforeAndAfterAll {
       reporter = StringifyReporter,
       packageInfoInputMap = Map(Source.getPackageInfoOrCrash(source, Path.of("")) -> Vector(source)),
       checkConsistency = true,
-      cacheParserAndTypeChecker = cacheParserAndTypeChecker,
+      cacheParserAndTypeChecker = shouldPreParseAndTypeCheck,
       z3Exe = z3Exe,
       // termination checks in functions are currently disabled in the tests. This can be enabled in the future,
       // but requires some work to add termination measures all over the test suite.
       disableCheckTerminationPureFns = true,
     )
 
-  override def runTests(testName: Option[String], args: Args): Status = {
-    if (cacheParserAndTypeChecker) {
-      implicit val execContext: GobraExecutionContext = executor
-      val futs = inputs.map(source => {
-        val config = getConfig(source)
-        val pkgInfo = config.packageInfoInputMap.keys.head
-        val fut = for {
-          finalConfig <- EitherT.fromEither(Future.successful(gobraInstance.getAndMergeInFileConfig(config, pkgInfo)))
-          parseResult <- Parser.parse(finalConfig, pkgInfo)
-          pkg = RegularPackage(pkgInfo.id)
-          typeCheckResult <- Info.check(finalConfig, pkg, parseResult)
-        } yield typeCheckResult
-        fut.toEither
-      })
-      Await.result(Future.sequence(futs), Duration.Inf)
-      println("pre-parsing and pre-typeChecking completed")
+  // The testing framework calls first `runTests` once, followed by multiple calls to `runTest`.
+  // Even if we skip `GobraTests` by instructing ScalaTest to ignore a certain tag, `runTests` is still called.
+  // Thus, we start the pre-parsing and pre-typeChecking at the first invocation of `runTest`.
+  override def runTest(testName: String, args: Args): Status = {
+    if (shouldPreParseAndTypeCheck) {
+      val result: Promise[Vector[Either[Vector[VerifierError], TypeInfo]]] = Promise()
+      val prevValue = preParseAndTypeCheckResult.getAndUpdate {
+        case None => Some(result.future)
+        case v => v // leave unchanged
+      }
+      // We start the pre-parsing and pre-typechecking only if we just updated the atomic reference, i.e., the
+      // previous value was `None`.
+      val fut = prevValue match {
+        case Some(f) => f // atomic reference was already set by another thread
+        case None =>
+          implicit val execContext: GobraExecutionContext = executor
+          val futs = inputs.map(source => {
+            val config = getConfig(source)
+            val pkgInfo = config.packageInfoInputMap.keys.head
+            val fut = for {
+              finalConfig <- EitherT.fromEither(Future.successful(gobraInstance.getAndMergeInFileConfig(config, pkgInfo)))
+              parseResult <- Parser.parse(finalConfig, pkgInfo)
+              pkg = RegularPackage(pkgInfo.id)
+              typeCheckResult <- Info.check(finalConfig, pkg, parseResult)
+            } yield typeCheckResult
+            fut.toEither
+          })
+          Future.sequence(futs)
+            .andThen(res => {
+              result.complete(res) // set the result to the promise
+            })
+          result.future // return the promise's future
+      }
+      // block until the pre-parsing and pre-typechecking is completed:
+      Await.result(fut, Duration.Inf)
     }
-    super.runTests(testName, args)
+
+    super.runTest(testName, args)
   }
 
   override def afterAll(): Unit = {

src/test/scala/viper/gobra/parsing/GobraParserTests.scala

@@ -23,10 +23,7 @@ import scala.concurrent.duration.Duration
 
 class GobraParserTests extends AbstractGobraTests with BeforeAndAfterAll {
 
-  val regressionsPropertyName = "GOBRATESTS_REGRESSIONS_DIR"
-
-  val regressionsDir: String = System.getProperty(regressionsPropertyName, "better_errors")
-  val testDirectories: Seq[String] = Vector(regressionsDir)
+  val testDirectories: Seq[String] = Vector("better_errors")
   override val defaultTestPattern: String = PackageResolver.inputFilePattern
 
   var gobraInstance: Gobra = _