Tagging of test suites

.github/workflows/check-test-tagging.sh

@@ -0,0 +1,31 @@
+#!/bin/bash -eu
+
+set -o pipefail
+
+test_dir=src/test
+
+echo '::group::All test suites:'
+tests="$(./mill test.testOnly -- -t '' -oW | tr -d ':' | sort)"
+echo "$tests"
+echo '::endgroup::'
+echo
+echo '::group::Disabled test suites:'
+grep '@test_util.tags.DisabledTest' --context=1 -R $test_dir
+echo '::endgroup::'
+echo
+
+ok=true
+echo '::group::Test suites with no tag annotations:'
+for t in $tests; do
+  defn="$(grep 'class\s\+'"$t"'[ (]' --before-context=2 -R $test_dir)"
+  if ! grep -q '@test_util.tags.' <<< "$defn"; then
+    echo 'test suite has no `@test_util.tags.*` annotation:' >&2
+    grep 'class\s\+'"$t"'[ (]' -R $test_dir
+    echo
+    ok=false
+  fi
+done
+echo '::endgroup::'
+
+$ok
+

.github/workflows/run-examples.yml

@@ -8,6 +8,18 @@ on:
       - main
   workflow_dispatch:
 jobs:
+  CheckTestTagging:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-java@v4
+        with:
+          distribution: 'temurin'
+          java-version: '21'
+      - run: './mill test.compile'
+      - name: Check all test suites have at least one tag
+        run: .github/workflows/check-test-tagging.sh
+
   Scalafmt:
     runs-on: ubuntu-latest
     steps:
@@ -52,8 +64,9 @@ jobs:
       - run: sudo apt-get install -y z3='4.8.12-*'
       - run: dotnet tool install --global boogie --version '3.4.3'
 
-      - name: System Tests
-        run: ./mill test.testOnly 'SystemTests*'
+      - run: ./mill compile
+      - run: ./scripts/scalatest.sh -oID -n test_util.tags.StandardSystemTest
+
       - uses: actions/upload-artifact@v4
         with:
           name: testresult-${{ github.run_number }}
@@ -103,44 +116,11 @@ jobs:
       - run: dotnet tool install --global boogie --version '3.4.3'
 
       - run: ./mill test.compile
+      - run: ./scripts/scalatest.sh -oID -n test_util.tags.UnitTest
 
         # every test with package prefix:
         # sbt "show test:definedTests"
 
-        # note: tests prefixed with '!' are expected to fail.
-        #       if they are fixed, the '!' should be removed.
-
-      - run: ./mill test.testOnly IrreducibleLoop
-        if: ${{ ! cancelled() }}
-      - run: ./mill test.testOnly BitVectorAnalysisTests
-        if: ${{ ! cancelled() }}
-      - run: ./mill test.testOnly '*IntrusiveListPublicInterfaceTest'
-        if: ${{ ! cancelled() }}
-      - run: ./mill test.testOnly util.intrusive_list.IntrusiveListTest
-        if: ${{ ! cancelled() }}
-      - run: ./mill test.testOnly DataStructureAnalysisTest
-        if: ${{ ! cancelled() }}
-      - run: ./mill test.testOnly ParamAnalysisTests
-        if: ${{ ! cancelled() }}
-      - run: ./mill test.testOnly LiveVarsAnalysisTests
-        if: ${{ ! cancelled() }}
-      - run: ./mill test.testOnly ir.ToScalaTest
-        if: ${{ ! cancelled() }}
-      - run: ./mill test.testOnly ir.IRTest
-        if: ${{ ! cancelled() }}
-      - run: ./mill test.testOnly ir.IRToDSLTest
-        if: ${{ ! cancelled() }}
-      - run: ./mill test.testOnly ir.CILVisitorTest
-        if: ${{ ! cancelled() }}
-      - run: ./mill test.testOnly ir.InterpreterTests
-        if: ${{ ! cancelled() }}
-      - run: ./mill test.testOnly ir.InvariantTest
-        if: ${{ ! cancelled() }}
-      - run: ./mill test.testOnly ProcedureSummaryTests || true
-        if: ${{ ! cancelled() }}
-      - run: ./mill test.testOnly TaintAnalysisTests
-        if: ${{ ! cancelled() }}
-
   AnalysisSystemTests:
     runs-on: ubuntu-latest
 
@@ -161,15 +141,7 @@ jobs:
       - run: sudo apt-get install -y z3='4.8.12-*'
       - run: dotnet tool install --global boogie --version '3.4.3'
 
-      - run: echo "All systemtest suites:" & ./mill test.testOnly '*SystemTests*' -- -z 'xxxx'
-
-      - run: ./mill test.testOnly DSAMemoryRegionSystemTestsBAP
-        if: ${{ ! cancelled() }}
-      - run: ./mill test.testOnly DSAMemoryRegionSystemTestsGTIRB
-        if: ${{ ! cancelled() }}
-      - run: ./mill test.testOnly AnalysisSystemTestsBAP
-        if: ${{ ! cancelled() }}
-      - run: ./mill test.testOnly AnalysisSystemTestsGTIRB
-        if: ${{ ! cancelled() }}
-      - run: ./mill test.testOnly SimplifySystemTests
-        if: ${{ ! cancelled() }}
+      - run: echo "All systemtest suites:" && ./mill test.testOnly '*SystemTests*' -- -z 'xxxx'
+
+      - run: ./mill compile
+      - run: ./scripts/scalatest.sh -oID -n test_util.tags.AnalysisSystemTest

scripts/scalatest.sh

@@ -0,0 +1,19 @@
+#!/bin/bash
+
+# Executes the full Scalatest runner (https://www.scalatest.org/user_guide/using_the_runner).
+#
+# This is needed to use some more advanced arguments of the runner, since `./mill test.run`
+# silently ignores some arguments (for example, -n and -l).
+
+# NOTE: executing the runner through this script may try to start a GUI.
+#       to avoid this and use the console, pass -o.
+
+classes="$(./mill show test.compile | grep '"classes"' | cut -d'"' -f4 | cut -d: -f4)"
+
+if ! [[ -d "$classes" ]]; then
+  echo "unable to determine mill class output directory: $classes" >&2
+  exit 1
+fi
+
+exec ./mill test.runMain org.scalatest.tools.Runner -R "$classes" "$@"
+

src/main/scala/translating/IRExpToSMT2.scala

@@ -205,7 +205,7 @@ object BasilIRToSMT2 extends BasilIRExpWithVis[Sexp] {
     }
 
     val terms = list(sym("push")) :: BasilIRToSMT2.extractDecls(e)
-      ++ List(assert, list(sym("set-option"), sym(":smt.timeout"), sym("1")), list(sym("check-sat")))
+      ++ List(assert, list(sym("check-sat")))
       ++ (if (getModel) then
             List(list(sym("echo"), sym("\"" + name.getOrElse("") + "  ::  " + e + "\"")), list(sym("get-model")))
           else List())

src/test/scala/BitVectorAnalysisTests.scala

@@ -5,6 +5,7 @@ import util.Logger
 
 import scala.runtime.stdLibPatches.Predef.assert
 
+@test_util.tags.UnitTest
 class BitVectorAnalysisTests extends AnyFunSuite {
 
   test("BitVector to Natural - should convert BitVector to natural number") {

src/test/scala/DataStructureAnalysisTest.scala

@@ -27,6 +27,7 @@ import translating.PrettyPrinter.*
   * BASILRESULT.analysis.get.bu is the set of graphs from the end of the bottom-up phase BASILRESULT.analysis.get.td is
   * the set of graphs from the end of the top-down phase
   */
+@test_util.tags.UnitTest
 class DataStructureAnalysisTest extends AnyFunSuite {
 
   def runAnalysis(program: Program): StaticAnalysisContext = {

src/test/scala/DifferentialAnalysisTest.scala

@@ -30,7 +30,28 @@ import util.RunUtils.loadAndTranslate
 
 import scala.collection.mutable
 
-class DifferentialTest extends AnyFunSuite {
+abstract class DifferentialTest extends AnyFunSuite, TestCustomisation {
+
+  override def customiseTestsByName(name: String) = name match {
+    case "analysis_differential:floatingpoint/clang:GTIRB" | "analysis_differential:floatingpoint/gcc:GTIRB" =>
+      Mode.NotImplemented("needs FP_Mul")
+
+    case "analysis_differential:function1/gcc_O2:BAP" | "analysis_differential:function1/gcc_O2:GTIRB" |
+        "analysis_differential:malloc_with_local/gcc_O2:BAP" | "analysis_differential:malloc_with_local/gcc_O2:GTIRB" |
+        "analysis_differential:malloc_with_local3/gcc_O2:BAP" |
+        "analysis_differential:malloc_with_local3/gcc_O2:GTIRB" =>
+      Mode.NotImplemented("needs printf_chk")
+
+    case "analysis_differential:syscall/clang:BAP" | "analysis_differential:syscall/clang:GTIRB" |
+        "analysis_differential:syscall/clang_O2:GTIRB" | "analysis_differential:syscall/gcc:BAP" |
+        "analysis_differential:syscall/gcc:GTIRB" =>
+      Mode.NotImplemented("needs fork")
+
+    case "analysis_differential:syscall/gcc_O2:BAP" => Mode.TempFailure("traceInit empty")
+    case "analysis_differential:syscall/gcc_O2:GTIRB" => Mode.NotImplemented("needs fork")
+
+    case _ => Mode.Normal
+  }
 
   Logger.setLevel(LogLevel.WARN)
 
@@ -109,6 +130,7 @@ class DifferentialTest extends AnyFunSuite {
   }
 }
 
+@test_util.tags.AnalysisSystemTest
 class DifferentialAnalysisTest extends DifferentialTest {
 
   def runSystemTests(): Unit = {
@@ -142,6 +164,7 @@ class DifferentialAnalysisTest extends DifferentialTest {
   runSystemTests()
 }
 
+@test_util.tags.AnalysisSystemTest
 class DifferentialAnalysisTestSimplification extends DifferentialTest {
 
   def runSystemTests(): Unit = {

src/test/scala/IndirectCallTests.scala

@@ -17,10 +17,26 @@ import scala.collection.mutable.ArrayBuffer
 import scala.collection.mutable
 import test_util.BASILTest
 import test_util.TestConfig
+import test_util.TestCustomisation
 
 import java.io.{BufferedWriter, File, FileWriter}
 
-class IndirectCallTests extends AnyFunSuite, BASILTest {
+@test_util.tags.StandardSystemTest
+class IndirectCallTests extends AnyFunSuite, BASILTest, TestCustomisation {
+
+  override def customiseTestsByName(name: String) = name match {
+    case "indirect_call_outparam/clang:BAP" | "indirect_call_outparam/clang:GTIRB" | "indirect_call_outparam/gcc:BAP" |
+        "indirect_call_outparam/gcc:GTIRB" | "jumptable/clang:BAP" | "jumptable/clang:GTIRB" =>
+      Mode.TempFailure("indirect call not resolved to correct target")
+
+    case "jumptable3/clang:GTIRB" | "jumptable3/clang_O2:GTIRB" | "switch2/clang:GTIRB" =>
+      Mode.TempFailure("indirect call not resolved to goto")
+
+    case "jumptable/gcc:BAP" | "jumptable/gcc:GTIRB" =>
+      Mode.TempFailure("Expected verification success, but got failure")
+
+    case _ => Mode.Normal
+  }
 
   /** @param label - the label of the IndirectCall to be resolved
     * @param labelProcedure - the name of the procedure containing the IndirectCall to be resolved

src/test/scala/InterpretTestConstProp.scala

@@ -31,6 +31,7 @@ import util.RunUtils.loadAndTranslate
 
 import scala.collection.mutable
 
+@test_util.tags.StandardSystemTest
 class ConstPropInterpreterValidate extends AnyFunSuite with TestValueDomainWithInterpreter[FlatElement[BitVecLiteral]] {
 
   Logger.setLevel(LogLevel.ERROR)

src/test/scala/IrreducibleLoop.scala

@@ -15,6 +15,7 @@ import test_util.BASILTest.writeToFile
 /** Add more tests by simply adding them to the programs directory. Refer to the existing tests for the expected
   * directory structure and file-name patterns.
   */
+@test_util.tags.UnitTest
 class IrreducibleLoop extends AnyFunSuite {
   val testPath = "./src/test/irreducible_loops"
   Logger.setLevel(LogLevel.ERROR)

src/test/scala/LiveVarsAnalysisTests.scala

@@ -21,6 +21,7 @@ import test_util.BASILTest
 import util.{BASILResult, StaticAnalysisConfig}
 import translating.PrettyPrinter.*
 
+@test_util.tags.UnitTest
 class LiveVarsAnalysisTests extends AnyFunSuite, BASILTest {
   Logger.setLevel(LogLevel.ERROR)
   private val correctPath = "./src/test/correct/"

src/test/scala/ParamAnalysisTests.scala

@@ -4,6 +4,7 @@ import org.scalatest.funsuite.AnyFunSuite
 import test_util.BASILTest
 import util.{BASILResult, StaticAnalysisConfig, Logger, LogLevel}
 
+@test_util.tags.UnitTest
 class ParamAnalysisTests extends AnyFunSuite, BASILTest {
   private val correctPath = "./src/test/correct/"
 

src/test/scala/PointsToTest.scala

@@ -12,6 +12,7 @@ import java.nio.file.attribute.BasicFileAttributes
 
 import ir.dsl.*
 
+@test_util.tags.DisabledTest
 class PointsToTest extends AnyFunSuite with OneInstancePerTest {
 
   def runAnalyses(

src/test/scala/SATTest.scala

@@ -6,6 +6,7 @@ import test_util.BASILTest
 import util.*
 import translating.BasilIRToSMT2
 
+@test_util.tags.UnitTest
 class SATTest extends AnyFunSuite {
   test(" basic taut ") {
     // Logger.setLevel(LogLevel.DEBUG)

src/test/scala/SVATest.scala

@@ -9,6 +9,7 @@ import util.*
 
 import scala.collection.immutable.{AbstractSeq, LinearSeq}
 
+@test_util.tags.UnitTest
 class SVATest extends AnyFunSuite {
 
   def runAnalysis(program: Program): StaticAnalysisContext = {