Shard the long-running CORE runs of contracts-dfcc and jbmc-strings

.gitignore

@@ -70,7 +70,7 @@ regression/solver-hardness/solver-hardness-simple/solver_hardness.json
 regression/goto-instrument-wmm-core/*/*.txt
 regression/goto-instrument-wmm-core/*/*.dot
 jbmc/regression/**/tests.log
-jbmc/regression/**/tests-symex-driven-loading*.log
+jbmc/regression/**/tests-*.log
 unit/memory-analyzer/input.inc
 unit/memory-analyzer/test.inc
 unit/gdb.txt

jbmc/regression/jbmc-strings/CMakeLists.txt

@@ -1,6 +1,13 @@
-add_test_pl_tests(
-    "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation"
-)
+set(jbmc_strings_cmdline
+    "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation")
+set(jbmc_strings_shards 4)
+
+# The plain (non-symex-driven) CORE run of this suite is one of the slowest
+# non-sharded CORE ctests; shard it (keeping its 30-minute per-shard timeout)
+# so it runs as several parallel ctest entries on the macOS runners. See
+# add_sharded_test_pl_tests.
+add_sharded_test_pl_tests(
+  "${jbmc_strings_cmdline}" "core" ${jbmc_strings_shards} 1800)
 
 # The symex-driven-lazy-loading run of this suite is the single largest CORE
 # ctest on the macOS runners (~1-1.5h), and a single ctest test runs serially
@@ -9,11 +16,10 @@ add_test_pl_tests(
 # dominating the job's wall-clock.
 add_sharded_test_pl_profile(
   "jbmc-strings-symex-driven-lazy-loading"
-  "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading"
+  "${jbmc_strings_cmdline} --symex-driven-lazy-loading"
   "-C;-X;symex-driven-lazy-loading-expected-failure"
   "CORE"
   "symex-driven-loading"
-  4
+  ${jbmc_strings_shards}
   10800
 )
-set_tests_properties("jbmc-strings-CORE" PROPERTIES TIMEOUT 1800)

regression/CMakeLists.txt

@@ -53,6 +53,28 @@ macro(add_test_pl_tests cmdline)
     add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -K KNOWNBUG ${ARGN})
 endmacro(add_test_pl_tests)
 
+# Like add_test_pl_tests, but split the CORE profile into <shard_count>
+# parallel shards (see add_sharded_test_pl_profile) so a long-running CORE
+# suite runs as several parallel ctest entries instead of one indivisible test
+# -- e.g. to keep the slowest suites from dominating the macOS runners'
+# wall-clock or approaching the per-test timeout. THOROUGH/FUTURE/KNOWNBUG
+# remain single tests. <log_suffix> names the per-shard CORE logs and each CORE
+# shard is given <timeout>. Any extra arguments (e.g. -X exclusions) are
+# forwarded to every profile.
+macro(add_sharded_test_pl_tests cmdline log_suffix shard_count timeout)
+    get_filename_component(TEST_DIR_NAME ${CMAKE_CURRENT_SOURCE_DIR} NAME)
+    message(STATUS "Adding sharded tests in directory: ${TEST_DIR_NAME}")
+    # Build the CORE flags as a list so an empty ARGN collapses to just -C (no
+    # spurious empty argument reaching test.pl).
+    set(_core_flags "-C" ${ARGN})
+    add_sharded_test_pl_profile(
+        "${TEST_DIR_NAME}" "${cmdline}" "${_core_flags}" "CORE"
+        "${log_suffix}" ${shard_count} ${timeout})
+    add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -T THOROUGH ${ARGN})
+    add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -F FUTURE ${ARGN})
+    add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -K KNOWNBUG ${ARGN})
+endmacro(add_sharded_test_pl_tests)
+
 # For the best possible utilisation of multiple cores when
 # running tests in parallel, it is important that these directories are
 # listed with decreasing runtimes (i.e. longest running at the top)

regression/contracts-dfcc/CMakeLists.txt

@@ -13,9 +13,15 @@ else()
 endif()
 
 
-add_test_pl_tests(
-    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> $<TARGET_FILE:cbmc> ${is_windows} true" ${gcc_only}
-)
+set(dfcc_cmd
+    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> $<TARGET_FILE:cbmc> ${is_windows} true")
+set(dfcc_core_shards 4)
+
+# The CORE run of this suite is one of the slowest non-sharded CORE ctests;
+# shard it (and keep its 30-minute per-shard timeout) so it runs as several
+# parallel ctest entries on the macOS runners. See add_sharded_test_pl_tests.
+add_sharded_test_pl_tests(
+    "${dfcc_cmd}" "dfcc-core" ${dfcc_core_shards} 1800 ${gcc_only})
 
 add_test_pl_profile(
     "contracts-non-dfcc"
@@ -42,15 +48,16 @@ add_test_pl_profile(
 
 # solver appears on the PATH in Windows already
 if(NOT "${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
-  set_property(
-    TEST "contracts-dfcc-CORE"
-    PROPERTY ENVIRONMENT
-      "PATH=$ENV{PATH}:$<TARGET_FILE_DIR:smt2_solver>"
-  )
+  foreach(shard RANGE 1 ${dfcc_core_shards})
+    set_property(
+      TEST "contracts-dfcc-${shard}-CORE"
+      PROPERTY ENVIRONMENT
+        "PATH=$ENV{PATH}:$<TARGET_FILE_DIR:smt2_solver>"
+    )
+  endforeach()
   set_property(
     TEST "contracts-non-dfcc-CORE"
     PROPERTY ENVIRONMENT
       "PATH=$ENV{PATH}:$<TARGET_FILE_DIR:smt2_solver>"
   )
 endif()
-set_tests_properties("contracts-dfcc-CORE" PROPERTIES TIMEOUT 1800)