Make the CI more robust w.r.t. the test_comp_bisim job

.github/workflows/ci.yml

@@ -519,6 +519,11 @@ jobs:
         with:
           submodules: true
 
+      - uses: haskell/actions/setup@v2
+        id: setup-haskell
+        with:
+          ghc-version: "9.4.8"
+
       - name: Install system dependencies
         shell: bash
         run: .github/ci.sh install_system_deps
@@ -572,6 +577,8 @@ jobs:
         run: |
           export PATH="$PWD/bin:$PWD/dist/bin:$PATH"
           dist-tests/integration_tests
+        env:
+          ENABLE_HPC: true
 
       - name: Compute coverage
         shell: bash
@@ -804,6 +811,7 @@ jobs:
       - heapster-tests
       - saw-remote-api-tests
       - cabal-test
+      - coverage
       - s2n-tests
       - exercises
     steps:

intTests/IntegrationTest.hs

@@ -22,8 +22,15 @@ import Test.Tasty.HUnit ( testCase, (@=?), assertBool )
 import Test.Tasty.ExpectedFailure ( ignoreTest )
 
 
--- | Reads from DISABLED_TESTS env var or disabled_tests.txt file
--- (preference is given to the former) and returns the list of tests.
+-- | Compute the list of tests to disable in this run of the test suite. This
+-- reads from the following locations:
+--
+-- * The @DISABLED_TESTS@ environment variable, or if that is not defined, the
+--   @disabled_tests.txt@ file (preference given to the former).
+--
+-- * If the @ENABLE_HPC@ environment variable is defined, the
+--   @disabled_tests_hpc.txt@ file.
+--
 -- Shell-style comments are removed, and test names are assumed to be
 -- a single word without whitespace.  The input can separate testnames
 -- with any type of whitespace (space, tab, newline).
@@ -32,13 +39,19 @@ import Test.Tasty.ExpectedFailure ( ignoreTest )
 getDisabledTestList :: FilePath -> IO [String]
 getDisabledTestList testdir = do
   let dtfile = testdir </> "disabled_tests.txt"
+  let dtHpcFile = testdir </> "disabled_tests_hpc.txt"
   dset <- lookupEnv "DISABLED_TESTS" >>= \case
     Just d -> return d
     Nothing -> readFile dtfile
+  dsetHpc <- lookupEnv "ENABLE_HPC" >>= \case
+    Just _ -> readFile dtHpcFile
+    Nothing -> return ""
   let removeComment = takeWhile ((/=) '#')
       stripWhitespace = words
       processInput = join . map (stripWhitespace . removeComment) . lines
-  return $ processInput dset
+  let tests1 = processInput dsetHpc
+  let tests2 = processInput dset
+  return $ tests1 ++ tests2
 
 
 -- | Gets the list of tests (subdirectories) to run given the base

intTests/disabled_tests_hpc.txt

@@ -0,0 +1,7 @@
+# Tests that are not run when running the `coverage` CI job, which builds SAW
+# with HPC code coverage enabled. Unfortunately, Haskell executables compiled
+# with coverage enabled have a tendency to use greater amounts of memory, and
+# when running these test cases, the difference in memory is enough to exceed
+# the maximum memory requirements imposed by GitHub Actions CI runners.
+
+test_comp_bisim

intTests/test_comp_bisim/cryptol/spec.cry

@@ -6,19 +6,19 @@ type input  = feedback_input 16
 type output = feedback_output 16
 
 // add10 spec
-type add10_state  = feedback_state 16 8
+type add10_state  = feedback_state 16 4
 add10_spec : (add10_state, input) -> (add10_state, output)
 add10_spec = feedback_spec`{n=10} f
   where f x = x + 10
 
 // pow4 spec
-type pow4_state  = feedback_state 16 8
+type pow4_state  = feedback_state 16 3
 pow4_spec : (pow4_state, input) -> (pow4_state, output)
 pow4_spec = feedback_spec`{n=2} f
   where f x = x ^^ 4
 
 // comp spec
-type comp_spec_state = feedback_state 16 8
+type comp_spec_state = feedback_state 16 4
 comp_spec : (comp_spec_state, input) -> (comp_spec_state, output)
 comp_spec = feedback_spec `{n=13} f
   where f x = (x ^^ 4) + 10