Develop

.github/workflows/ci.yml

@@ -3,18 +3,29 @@
 #
 # Runs on every push and pull request.
 # Installs LLVM 16 directly on ubuntu-22.04 runner.
-# Unit tests use -DSKIP_KLEE=ON -DSKIP_LIB_FUZZER=ON,
+# Unit tests use -DSKIP_KLEE=ON -DSKIP_AFL_PLUS_PLUS=ON,
 # so the full Dockerfile.dev dependencies are not needed.
 #
 # Phase 1.5 — OpenSSF Best Practices Badge (Analysis section)
 ############################################################
 name: CI
 
 on:
+  # Push cobre só as branches de integração. O filtro antigo listava 'feat-*'
+  # com hífen, que nunca casou com a convenção real (feat/castle-juliet-baseline,
+  # feat/testcomp-conformance) -- então nenhum push de branch era verificado, e
+  # todo run verde até aqui veio do gatilho pull_request.
+  #
+  # Branches de feature ficam cobertas pelo pull_request abaixo, e não por push,
+  # para não disparar dois runs idênticos a cada push numa branch com PR aberta.
   push:
-    branches: [develop, main, master, 'feat-*']
-  pull_request:
     branches: [develop, main, master]
+  # Inclui feat/** como ALVO para que PRs empilhadas sejam verificadas. Sem isso
+  # uma PR cuja base é outra branch de feature não dispara nada -- a #56 abriu
+  # com um único check -- e os gates de regressão que ela própria adiciona nunca
+  # rodariam nela.
+  pull_request:
+    branches: [develop, main, master, 'feat/**']
 
 jobs:
   # ===========================================================
@@ -48,7 +59,7 @@ jobs:
           mkdir -p build && cd build
           cmake .. -G Ninja \
             -DLLVM_DIR=/usr/lib/llvm-16/lib/cmake/llvm \
-            -DSKIP_LIB_FUZZER=ON \
+            -DSKIP_AFL_PLUS_PLUS=ON \
             -DSKIP_KLEE=ON \
             -DENABLE_TEST=ON
         env:
@@ -93,7 +104,7 @@ jobs:
           mkdir -p build && cd build
           cmake .. -G Ninja \
             -DLLVM_DIR=/usr/lib/llvm-16/lib/cmake/llvm \
-            -DSKIP_LIB_FUZZER=ON \
+            -DSKIP_AFL_PLUS_PLUS=ON \
             -DSKIP_KLEE=ON \
             -DENABLE_TEST=ON \
             -DCMAKE_EXPORT_COMPILE_COMMANDS=ON
@@ -180,7 +191,7 @@ jobs:
           mkdir -p build && cd build
           cmake .. -G Ninja \
             -DLLVM_DIR=/usr/lib/llvm-16/lib/cmake/llvm \
-            -DSKIP_LIB_FUZZER=ON \
+            -DSKIP_AFL_PLUS_PLUS=ON \
             -DSKIP_KLEE=ON \
             -DENABLE_TEST=ON \
             -DMAP2CHECK_ENABLE_SANITIZERS=ON
@@ -291,7 +302,222 @@ jobs:
             '
 
   # ===========================================================
-  # Job 5: Dynamic Analysis — Valgrind memcheck (OpenSSF)
+  # Job 5: CASTLE Benchmark Regression Tests
+  # ===========================================================
+  # Verifies Map2Check against 5 CASTLE micro-benchmarks
+  # (CWE-415, 416, 476, 787) — memory safety regression suite.
+  castle-regression:
+    name: CASTLE Regression
+    runs-on: ubuntu-22.04
+    timeout-minutes: 20
+    needs: [build-and-test]
+
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
+      - name: Free disk space
+        run: |
+          sudo rm -rf /usr/share/dotnet /usr/local/lib/android /opt/ghc
+          sudo docker image prune -a -f || true
+
+      - name: Pull map2check-dev image
+        run: docker pull ghcr.io/hbgit/map2check-dev:latest
+
+      - name: Build + install Map2Check in container
+        run: |
+          docker run --rm \
+            -u root \
+            -v "${{ github.workspace }}:/workspace" \
+            -w /workspace \
+            -e CC=/usr/bin/clang-16 \
+            -e CXX=/usr/bin/clang++-16 \
+            ghcr.io/hbgit/map2check-dev:latest bash -c '
+              rm -rf build_castle_ci install_castle_ci
+              mkdir -p build_castle_ci && cd build_castle_ci
+              cmake .. -G Ninja \
+                -DLLVM_DIR=/usr/lib/llvm-16/lib/cmake/llvm \
+                -DENABLE_TEST=ON \
+                -DMAP2CHECK_DYNAMIC_LINK=ON \
+                -DCMAKE_INSTALL_PREFIX=/workspace/install_castle_ci
+              ninja
+              ninja install
+              mkdir -p /workspace/install_castle_ci/lib/klee
+              ln -sf /opt/klee/lib/klee/runtime /workspace/install_castle_ci/lib/klee/runtime
+              ln -sf /usr/lib/llvm-16/lib/clang /workspace/install_castle_ci/lib/clang
+            '
+
+      - name: Run regression tests
+        run: |
+          docker run --rm \
+            -u root \
+            -v "${{ github.workspace }}:/workspace" \
+            -w /workspace \
+            -e MAP2CHECK_PATH=/workspace/install_castle_ci \
+            ghcr.io/hbgit/map2check-dev:latest bash -c '
+              bash tests/integration/test_verdict_classifier.sh
+              bash tests/integration/test_juliet_sampling.sh
+              bash tests/integration/test_castle_regression.sh
+              bash tests/integration/test_main_argv.sh
+              bash tests/integration/test_modes.sh
+              bash tests/integration/test_add_invariants.sh
+              bash tests/integration/test_test_suite_emission.sh
+              bash tests/integration/test_target_coverage.sh
+              bash tests/integration/test_ktest_object_names.sh
+              bash tests/integration/test_testcomp_regressions.sh
+              bash tests/integration/test_exit_codes.sh
+              bash tests/integration/test_cwe_mode_mapping.sh
+            '
+
+  # ===========================================================
+  # Job: Invariants — o contrato do --add-invariants
+  # ===========================================================
+  # Roda o MESMO teste em qualquer estado em que a imagem esteja. Enquanto a
+  # imagem publicada não trouxer o Clam, ele afirma que a flag falha alto
+  # (issue #54). Quando a imagem passar a trazê-lo, o mesmo teste afirma que a
+  # flag tem sucesso E injeta verifier.assume. A linha CAPABILITY no log diz
+  # qual contrato foi verificado, então a volta da capacidade fica visível em
+  # vez de inferida.
+  #
+  # Nenhum check vermelho é estacionado de propósito: um check que se espera
+  # vermelho passa a ser ignorado, e aí ninguém percebe o dia em que fica verde.
+  invariants-clam:
+    name: Invariants (Clam)
+    runs-on: ubuntu-22.04
+    timeout-minutes: 25
+    needs: [build-and-test]
+
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
+      - name: Free disk space
+        run: |
+          sudo rm -rf /usr/share/dotnet /usr/local/lib/android /opt/ghc
+          sudo docker image prune -a -f || true
+
+      - name: Pull map2check-dev image
+        run: docker pull ghcr.io/hbgit/map2check-dev:latest
+
+      - name: Build with -DENABLE_CLAM=ON
+        run: |
+          docker run --rm \
+            -u root \
+            -v "${{ github.workspace }}:/workspace" \
+            -w /workspace \
+            -e CC=/usr/bin/clang-16 \
+            -e CXX=/usr/bin/clang++-16 \
+            ghcr.io/hbgit/map2check-dev:latest bash -c '
+              rm -rf build_clam_ci install_clam_ci
+              mkdir -p build_clam_ci && cd build_clam_ci
+              cmake .. -G Ninja \
+                -DLLVM_DIR=/usr/lib/llvm-16/lib/cmake/llvm \
+                -DENABLE_CLAM=ON \
+                -DMAP2CHECK_DYNAMIC_LINK=ON \
+                -DCMAKE_INSTALL_PREFIX=/workspace/install_clam_ci
+              ninja
+              ninja install
+              mkdir -p /workspace/install_clam_ci/lib/klee
+              ln -sf /opt/klee/lib/klee/runtime /workspace/install_clam_ci/lib/klee/runtime
+              ln -sf /usr/lib/llvm-16/lib/clang /workspace/install_clam_ci/lib/clang
+            '
+
+      - name: Assert the --add-invariants contract
+        run: |
+          docker run --rm \
+            -u root \
+            -v "${{ github.workspace }}:/workspace" \
+            -w /workspace \
+            -e MAP2CHECK_PATH=/workspace/install_clam_ci \
+            ghcr.io/hbgit/map2check-dev:latest bash -c '
+              bash tests/integration/test_add_invariants.sh
+            '
+
+  # ===========================================================
+  # Job: Test-Comp conformance — o validador oficial
+  # ===========================================================
+  # Afirma que uma suíte emitida REPRODUZ o bug, que é o que a competição
+  # pontua. A validade estrutural do XML é afirmada à parte, pelo
+  # test_test_suite_emission.sh no job do CASTLE — uma suíte pode ser
+  # perfeitamente bem formada e valer zero ponto.
+  #
+  # Note que o TestCov sai com código 0 tanto quando cobre quanto quando não
+  # cobre; o veredito está na linha "Result:". Ver
+  # tests/testcomp/NOTES-testcov-output.md.
+  testcov-gate:
+    name: Test-Comp Validation (TestCov)
+    runs-on: ubuntu-22.04
+    timeout-minutes: 25
+    needs: [build-and-test]
+
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
+      - name: Free disk space
+        run: |
+          sudo rm -rf /usr/share/dotnet /usr/local/lib/android /opt/ghc
+          sudo docker image prune -a -f || true
+
+      - name: Pull map2check-dev image
+        run: docker pull ghcr.io/hbgit/map2check-dev:latest
+
+      - name: Build + install Map2Check in container
+        run: |
+          docker run --rm \
+            -u root \
+            -v "${{ github.workspace }}:/workspace" \
+            -w /workspace \
+            -e CC=/usr/bin/clang-16 \
+            -e CXX=/usr/bin/clang++-16 \
+            ghcr.io/hbgit/map2check-dev:latest bash -c '
+              rm -rf build_testcov_ci install_testcov_ci
+              mkdir -p build_testcov_ci && cd build_testcov_ci
+              cmake .. -G Ninja \
+                -DLLVM_DIR=/usr/lib/llvm-16/lib/cmake/llvm \
+                -DMAP2CHECK_DYNAMIC_LINK=ON \
+                -DCMAKE_INSTALL_PREFIX=/workspace/install_testcov_ci
+              ninja
+              ninja install
+              mkdir -p /workspace/install_testcov_ci/lib/klee
+              ln -sf /opt/klee/lib/klee/runtime /workspace/install_testcov_ci/lib/klee/runtime
+              ln -sf /usr/lib/llvm-16/lib/clang /workspace/install_testcov_ci/lib/clang
+            '
+
+      - name: Run TestCov over the conformance corpus
+        run: |
+          docker run --rm \
+            -u root \
+            -v "${{ github.workspace }}:/workspace" \
+            -w /workspace \
+            -e MAP2CHECK_PATH=/workspace/install_testcov_ci \
+            -e KEEP_WORK=1 \
+            ghcr.io/hbgit/map2check-dev:latest bash -c '
+              # zip for the suite archive, gcc/lcov for coverage measurement.
+              apt-get update -qq
+              apt-get install -y -qq python3-pip zip gcc lcov
+              pip3 install --quiet testcov
+              # The tool-info module is what BenchExec loads on competition
+              # infrastructure. Nothing else here exercises it, and a wrong one
+              # only shows up days after submission as every task erroring out.
+              python3 tests/integration/test_benchexec_toolinfo.py
+              # Cover-Branches: the other competition category, and the one
+              # whose suite has more than one test case. Validated by TestCov,
+              # not by inspecting the XML -- only the validator can say whether
+              # the branches are actually exercised.
+              MAP2CHECK_PATH=/workspace/install_testcov_ci \
+                bash tests/integration/test_cover_branches.sh
+              bash tests/testcomp/run_testcov_suite.sh
+            '
+
+  # ===========================================================
+  # Job 6: Dynamic Analysis — Valgrind memcheck (OpenSSF)
   # ===========================================================
   # Build ISOLADO e SEM sanitizers: a shadow memory do ASan/UBSan
   # conflita com a VM do Valgrind. Debug + DWARF-4 para stacks
@@ -326,7 +552,7 @@ jobs:
           mkdir -p build && cd build
           cmake .. -G Ninja \
             -DLLVM_DIR=/usr/lib/llvm-16/lib/cmake/llvm \
-            -DSKIP_LIB_FUZZER=ON \
+            -DSKIP_AFL_PLUS_PLUS=ON \
             -DSKIP_KLEE=ON \
             -DENABLE_TEST=ON \
             -DCMAKE_BUILD_TYPE=Debug \

.github/workflows/docker-publish.yml

@@ -2,8 +2,17 @@
 # Publish map2check-dev Docker image to GitHub Container Registry
 #
 # Triggers:
-#   - Push to develop (Dockerfile.dev changes)
-#   - Manual dispatch (workflow_dispatch)
+#   - Push to develop (Dockerfile.dev changes)  -> build AND push
+#   - Pull request touching Dockerfile.dev      -> build only, no push
+#   - Manual dispatch (workflow_dispatch)       -> build AND push
+#
+# The pull_request trigger is not decoration. Until it existed, Dockerfile.dev
+# was only ever built after a merge, so a recipe that cannot build reached
+# develop and broke the image: the Clam section built with the default cc
+# (GCC 11) instead of clang-16, and GCC rejects a construct in sea-dsa that
+# clang only warns about. Nothing pre-merge could have caught that, because
+# nothing pre-merge compiled the file. It is paths-filtered, so PRs that do not
+# touch the Dockerfile pay nothing.
 #
 # Phase 1.5 — OpenSSF Best Practices Badge
 ############################################################
@@ -14,6 +23,10 @@ on:
     branches: [develop]
     paths:
       - 'Dockerfile.dev'
+  pull_request:
+    branches: [develop, main, master]
+    paths:
+      - 'Dockerfile.dev'
   workflow_dispatch:
 
 env:
@@ -32,7 +45,10 @@ jobs:
       - name: Checkout
         uses: actions/checkout@v4
 
+      # Skipped on pull_request: the run does not push, and a PR from a fork
+      # has no packages:write token to log in with anyway.
       - name: Log in to GHCR
+        if: github.event_name != 'pull_request'
         uses: docker/login-action@v3
         with:
           registry: ${{ env.REGISTRY }}
@@ -48,11 +64,13 @@ jobs:
             type=raw,value=latest
             type=sha,prefix=
 
+      # push is false on pull_request: the point there is to prove the recipe
+      # builds, not to publish an image from an unmerged branch over :latest.
       - name: Build and push
         uses: docker/build-push-action@v5
         with:
           context: .
           file: ./Dockerfile.dev
-          push: true
+          push: ${{ github.event_name != 'pull_request' }}
           tags: ${{ steps.meta.outputs.tags }}
           labels: ${{ steps.meta.outputs.labels }}

.github/workflows/greetings.yml

@@ -5,6 +5,9 @@ on: [pull_request, issues]
 jobs:
   greeting:
     runs-on: ubuntu-latest
+    permissions:
+      issues: write
+      pull-requests: write
     steps:
     - uses: actions/first-interaction@v1
       with:

.github/workflows/release.yml

@@ -1,7 +1,7 @@
 ############################################################
 # Map2Check Release — Draft Release automático no master
 #
-# Build completo (KLEE 3.1 + LibFuzzer) dentro da imagem
+# Build completo (KLEE 3.1 + AFL++) dentro da imagem
 # ghcr.io/hbgit/map2check-dev, empacota release/ em .zip e
 # publica Draft Release via semantic-release.
 ############################################################