diff --git a/.github/license-check/config.json b/.github/license-check/config.json index 9582adef6..0b939ac2c 100644 --- a/.github/license-check/config.json +++ b/.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/**", diff --git a/.github/test-and-measure-ram.sh b/.github/test-and-measure-ram.sh index 0b7a6afc6..524417f39 100755 --- a/.github/test-and-measure-ram.sh +++ b/.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 diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 5a01f5fd9..21ab3f160 100644 --- a/.github/workflows/test.yml +++ b/.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 }} diff --git a/src/test/java/viper/gobra/tags/GobraTestsTag.java b/src/test/java/viper/gobra/tags/GobraTestsTag.java new file mode 100644 index 000000000..c8ec04a8d --- /dev/null +++ b/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 {} diff --git a/src/test/scala/viper/gobra/GobraTests.scala b/src/test/scala/viper/gobra/GobraTests.scala index d528cced7..ee269dd21 100644 --- a/src/test/scala/viper/gobra/GobraTests.scala +++ b/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 = { diff --git a/src/test/scala/viper/gobra/parsing/GobraParserTests.scala b/src/test/scala/viper/gobra/parsing/GobraParserTests.scala index 66e338af3..63ddd266e 100644 --- a/src/test/scala/viper/gobra/parsing/GobraParserTests.scala +++ b/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 = _ diff --git a/workflow-container/Dockerfile b/workflow-container/Dockerfile index 988437ecb..d82852d7b 100644 --- a/workflow-container/Dockerfile +++ b/workflow-container/Dockerfile @@ -65,6 +65,9 @@ COPY viperserver /build/gobra/viperserver RUN sbt assembly +# force compilation of test classes: +RUN sbt "test:compile" + # a second build stage starts here that is based of a fresh image. # note that only stuff explicitly copied from "build" will be present. @@ -98,4 +101,7 @@ COPY --from=build /build/gobra/target/scala-2.13/gobra.jar . COPY src/test/resources/regressions/examples/evaluation ./evaluation COPY src/test/resources/regressions/examples/tutorial-examples ./tutorial-examples +# create the directory that Gobra uses to write its stats to: +RUN mkdir -p .gobra + ENTRYPOINT ["java", "-Xss128m", "-jar", "gobra.jar"]