Cover-Branches, engine measurement, and eleven defects the corpus found

.github/workflows/ci.yml

@@ -366,6 +366,9 @@ jobs:
               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
             '
 
   # ===========================================================
@@ -504,6 +507,12 @@ jobs:
               # 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
             '
 

.gitignore

@@ -109,3 +109,9 @@ install_testcov_ci/
 .claude/
 .opencode/
 CLAUDE.md.bak-*
+
+# Test-Comp benchmark corpus (sv-benchmarks, ~13 GB). Cloned on demand for the
+# stratified runs; never committed. The pre-existing "sv-benchmarks/*" rule
+# above ignores the CONTENTS of such a directory but not the directory entry
+# itself, which is why this line names the path we actually clone into.
+tests/testcomp/bench/

Dockerfile.dev

@@ -229,6 +229,97 @@ RUN printf 'int main(){int i=0,s=0;while(i<10){s+=i;i++;}return s;}\n' > /tmp/cl
     test "$(llvm-dis-16 -o - /tmp/clamcheck.bc | grep -c 'verifier\.assume')" -gt 0 && \
     echo "Clam injects invariants: OK" && rm -f /tmp/clamcheck.c /tmp/clamcheck.bc
 
+# ============================================================
+# 7c. DG + sbt-slicer — program slicing with respect to an error site
+# ============================================================
+# Phase 2 of docs/map2check_migration_plan.md, and the same pipeline Symbiotic
+# uses: build a System Dependence Graph, keep only what the error site depends
+# on, hand the smaller program to KLEE.
+#
+# What it is for, in numbers from this repository: finding K2 measured the cost
+# of a nondeterministic read at 1 -> 21 -> 114 -> 861 partial paths for 2 -> 4
+# reads. Most of that forking happens in code that cannot influence the target,
+# and slicing removes it before KLEE ever sees it.
+#
+# Two limits worth knowing before relying on it. Slicing needs a criterion, so
+# it serves Cover-Error and does nothing for Cover-Branches, where every branch
+# matters and there is no error site to slice towards. And a slice taken with
+# respect to one error can remove another -- fine for a tool answering one
+# property, a hazard for a baseline that scores precision per CWE.
+#
+# Built with clang-16 for the reason section 7b spells out: the ENV CC below is
+# declared later in this file and would not apply here, and these are LLVM
+# projects that expect the LLVM toolchain.
+#
+# DG is taken from llvm-latest, NOT master, and the difference is the same one
+# crab-llvm taught: the maintained version was somewhere else. master calls
+# llvm::Function::getBasicBlockList(), which LLVM 16 made private, so it simply
+# does not compile here. llvm-latest's newest commit is literally "Fix build
+# for LLVM < 18".
+#
+# Pinned to SHAs. Neither project has had a versioned release since 2020, so
+# without a pin the image changes when upstream does -- what crab@dev
+# demonstrated by moving the day before it was needed.
+ARG DG_SHA=b34da890694f5210e475f34018239fc9d126d1ee         # llvm-latest @ 2023-11-29
+ARG SBT_SLICER_SHA=e350116b39be215277803fe2f5e5ac4a161c16b8 # master @ 2025-03-27
+
+RUN set -eux; \
+    pin() { \
+      git init -q "$2" && \
+      git -C "$2" remote add origin "$1" && \
+      git -C "$2" fetch -q --depth 1 origin "$3" && \
+      git -C "$2" checkout -q FETCH_HEAD; \
+    }; \
+    # Both projects pin C++14 with a plain set(), which overrides anything
+    # passed on the command line, and LLVM 16's headers use std::is_unsigned_v
+    # -- C++17. Patching the two lines is the smallest change that builds; the
+    # alternative is carrying a fork.
+    bump() { \
+      sed -i 's/set(CMAKE_CXX_STANDARD 14)/set(CMAKE_CXX_STANDARD 17)/; \
+              s/-std=c++14/-std=c++17/' "$1/CMakeLists.txt"; \
+    }; \
+    pin https://github.com/mchalupa/dg.git /tmp/dg "$DG_SHA"; \
+    bump /tmp/dg; \
+    # IN-SOURCE, deliberately. sbt-slicer's CMakeLists documents DG_PATH as
+    # "a path to an in-source build of dg" and derives both the include path
+    # and the library path from it; an out-of-tree build satisfies neither
+    # (the headers stay in the source tree, the libraries land in the build
+    # tree) and sbt-slicer fails to find dg/tools/llvm-slicer-opts.h.
+    cd /tmp/dg && \
+    cmake . -DCMAKE_BUILD_TYPE=Release \
+             -DCMAKE_C_COMPILER=/usr/bin/clang-16 \
+             -DCMAKE_CXX_COMPILER=/usr/bin/clang++-16 \
+             -DLLVM_DIR=/usr/lib/llvm-16/lib/cmake/llvm \
+             -DCMAKE_INSTALL_PREFIX=/opt/dg && \
+    make -j"$(nproc)" && make install && \
+    pin https://github.com/staticafi/sbt-slicer.git /tmp/sbt-slicer \
+        "$SBT_SLICER_SHA"; \
+    bump /tmp/sbt-slicer; \
+    mkdir /tmp/sbt-slicer/build && cd /tmp/sbt-slicer/build && \
+    cmake .. -DCMAKE_BUILD_TYPE=Release \
+             -DCMAKE_C_COMPILER=/usr/bin/clang-16 \
+             -DCMAKE_CXX_COMPILER=/usr/bin/clang++-16 \
+             -DLLVM_DIR=/usr/lib/llvm-16/lib/cmake/llvm \
+             -DDG_PATH=/tmp/dg \
+             -DCMAKE_INSTALL_PREFIX=/opt/sbt-slicer && \
+    make -j"$(nproc)" && make install && \
+    rm -rf /tmp/dg /tmp/sbt-slicer
+
+ENV SBT_SLICER=/opt/sbt-slicer/bin/sbt-slicer
+# dg installs shared libraries, and sbt-slicer links against them without an
+# rpath: without this the binary exists, builds, and dies on every invocation
+# with "libdganalysis.so: cannot open shared object file".
+ENV LD_LIBRARY_PATH="/opt/dg/lib:${LD_LIBRARY_PATH}"
+
+# Fail the image build if the slicer cannot actually slice. A binary that
+# exists and refuses every input is the failure mode section 7b was written
+# about: --add-invariants stayed dead for years behind exactly that.
+RUN printf 'extern int __VERIFIER_nondet_int(void);\nvoid reach_error(void);\nint main(){int a=__VERIFIER_nondet_int();int junk=__VERIFIER_nondet_int();int s=0;for(int i=0;i<50;i++){s+=junk*i;}if(a==7){reach_error();}return s;}\n' > /tmp/slicecheck.c && \
+    clang-16 -c -emit-llvm -g -O0 -o /tmp/slicecheck.bc /tmp/slicecheck.c && \
+    /opt/sbt-slicer/bin/sbt-slicer -c reach_error -o /tmp/sliced.bc /tmp/slicecheck.bc && \
+    test -s /tmp/sliced.bc && \
+    echo "sbt-slicer slices: OK" && rm -f /tmp/slicecheck.c /tmp/slicecheck.bc /tmp/sliced.bc
+
 # ============================================================
 # 8. WABT (WebAssembly Binary Toolkit) — wasm2c, wasm2wat, wasm-ld
 # ============================================================

docs/TESTCOMP-CHECKLIST.md

@@ -4,7 +4,7 @@ Estado das frentes do [plano de desenvolvimento](../.opencode/Plano%20de%20desen
 (local, fora do repositório). Este arquivo é o índice vivo: cada item aponta para a
 evidência que sustenta o estado declarado.
 
-**Última atualização:** 2026-08-22
+**Última atualização:** 2026-08-23 (v8)
 
 ## Legenda
 
@@ -23,7 +23,7 @@ evidência que sustenta o estado declarado.
 |---|---|---|
 | **H1.1** Emissor de test suite XML | ✅ | `modules/frontend/test_suite/`. `--generate-test-suite` emite `metadata.xml` + `testcase-N.xml` no formato de intercâmbio. 13 testes unitários + 12 asserções de integração. **Custo real muito abaixo das 2 pw estimadas**: o runtime já registrava os valores em ordem de consumo, faltava só serializar |
 | **H1.2** Conversor ktest→XML | ✅ | **Colapsou dentro do H1.1.** O log é escrito pelo binário instrumentado em tempo de execução, então já carrega os valores concretos do KLEE. Não precisou de conversor separado |
-| **H1.3** Conversor corpus-LibFuzzer→XML | 🟡 | O emissor é agnóstico de engine por construção (`NonDetGeneratorLibFuzzy.c:47` descarrega o mesmo log). **Falta:** log por input, para suítes com múltiplos test cases. **É o gargalo declarado**: bloqueia H2.5 e é o motivo pelo qual o tool-info recusa `cover-branches` |
+| **H1.3** Vetores de entrada por caminho | ✅ | **Resolvido por outro caminho que o planejado.** O KLEE já grava um `.ktest` por caminho explorado, com os objetos simbólicos em ordem de consumo; `ktest_reader.cpp` os lê. A alternativa (o runtime gravar um log por estado) foi **medida e descartada**: levou um run de 1s/`FALSE` para 100s/`SUCCEEDED` errado, porque cada escrita é chamada externa que o KLEE executa concretamente. 16 testes unitários fixam o parse contra bytes montados à mão |
 | **H1.4** Empacotamento BenchExec / fm-tools | ✅ | `utils/moduleBenchExec/map2check_testcomp.py` (`BaseTool2`) + `utils/map2check-testcomp-wrapper.py`, ambos no zip de release. 15 asserções contra o benchexec real em `tests/integration/test_benchexec_toolinfo.py`. **Falta:** registrar em `fm-tools` (fora deste repositório). O `map2check.py` SV-COMP segue em `BaseTool` 1.x — obsoleto mas ainda presente no benchexec 3.35, então não está morto |
 | **H1.5** E2E no CI com TestCov | ✅ | Job `Test-Comp Validation (TestCov)`, 6/6 contra manifesto medido. Ver `tests/testcomp/` |
 
@@ -35,7 +35,7 @@ evidência que sustenta o estado declarado.
 | **H2.2** Orquestração com time-slicing | ⬜ | Default híbrido atual (LibFuzzer 0.2× → KLEE 0.8×) preservado |
 | **H2.3** Seed exchange fuzzer↔KLEE | ⬜ | — |
 | **H2.4** Slicing pré-simbólico | ⬜ | Ver nota de prioridade abaixo |
-| **H2.5** Modo Cover-Branches | ⬜ | Bloqueado por H1.3 (log por input). O módulo tool-info **recusa** a propriedade em vez de aceitá-la e pontuar zero |
+| **H2.5** Modo Cover-Branches | ✅ | `--cover-branches` emite um test case por caminho do KLEE, `coversError` falso (são caminhos, não violações), teto de 500. Wrapper e tool-info **aceitam** a propriedade. Validado ponta a ponta: 7 test cases num programa de 6 ramos, **TestCov 100,0%**. Gate no CI (`test_cover_branches.sh`) mede cobertura pelo validador, não inspecionando XML |
 
 ### Nota de prioridade sobre H2
 
@@ -72,6 +72,7 @@ medir o efeito de K nesse corpus.
 | Invariantes: gate diferencial p/ promover a default | ⬜ | Task 7 do [plano de revival](superpowers/plans/2026-08-16-add-invariants-revival.md). Depende de rodar sobre corpus real |
 | **Baseline CASTLE + Juliet (v5)** | ✅ | PR #55. CASTLE 98,2% precisão, Juliet 90,8% (99,2% descontando artefatos de mapeamento) |
 | Corrida v6 (depois/antes) | 🟡 | **CASTLE fechado** (217/250): precisão 98,2%, recall 74,0%; excluindo o modo degenerado do achado B, recall 79,4%. Juliet: 3 de 4 fatias fechadas, `c` em andamento. **Regra de atribuição: invariantes DESLIGADOS na corrida principal**, senão overflow + timeout + amostragem + invariantes ficam conjuntamente não creditáveis |
+| **Corpus Test-Comp estratificado** | 🟡 | `fetch-benchmarks.sh` + `build_corpus.py` + `run_testcomp_evaluation.sh`. 372 tarefas cover-error e 480 cover-branches, cota por subcategoria e passo determinístico. Corrida de 2026-08-22 em andamento; ver [as notas de leitura](../tests/testcomp/RUN-2026-08-22-NOTES.md) — **o orçamento é 60s contra os 900s da competição, não são scores** |
 | **Alcançabilidade (CWE-843/628/770/835)** | ⬜ | Adiado por decisão. Sob a lente SV-COMP as quatro colapsam em uma: só 835 mapeia para categoria pontuável (Termination), e os wrappers declaram não suportar |
 
 ---
@@ -92,6 +93,12 @@ Todos com evidência em [findings](reports/2026-08-12-castle-juliet-findings.md)
 | — | Imagem: Clam compilava com GCC 11 em vez de clang-16 (o `ENV CC` está 88 linhas abaixo do `RUN`), e GCC rejeita o que o clang só avisa. **A receita nunca compilou** | ✅ compiladores nomeados no `CLAM_CFG` (#58) |
 | — | `Dockerfile.dev` só era compilado **depois** do merge, então um Dockerfile inválido chegava à `develop` sem nada poder barrá-lo | ✅ o workflow de publish roda em PRs que tocam o arquivo, com `push: false` (#58) |
 | — | Clam e suas três dependências vinham de branches móveis; `crab@dev` mudou em 21/08 | ✅ pinados por SHA como `ARG` (#59) |
+| **L** | **Suíte de Cover-Error saía sem nenhum `<input>`.** O estado que alcança o alvo aborta, e estado abortado não roda handler de saída, então o `klee_log.csv` nunca era escrito. **290 de 376 execuções que reportaram FAILED** emitiram um test case vazio: a ferramenta achava o bug e não conseguia prová-lo | ✅ fallback para o `.ktest` do caminho que o KLEE marcou com `.err` |
+| **M** | **`--property-file` relativo nunca era lido.** `resolveSpecification` roda depois do `chdir` para o scratch. Invisível porque o palpite do fallback coincide com a propriedade real das duas categorias — nenhuma saída diferia | ✅ resolvido contra `getOriginalPath()` |
+| **N** | **`--cover-branches` caía no default `MEMTRACK_MODE`** e instrumentava rastreamento de memória para uma tarefa sem propriedade | ✅ `COVER_BRANCHES_MODE`, pipeline só com `nondet-pass` |
+| **O** | **`MemoryTrackPass` emitia chamada com tipo incompatível.** Declara `map2check_malloc(ptr, i64)` e repassava o operando sem converter; programa que aloca com `i32` gerava módulo quebrado. **110 de 110 tarefas ProductLines** morriam em 2s de um orçamento de 60s. Sobreviveu porque Juliet e CASTLE alocam com `i64` | ✅ coerção nos 3 sítios |
+| **P** | **Teto de 500 test cases inviabilizava a validação.** Dos 116 casos cuja validação falhou, 115 tinham ≥100 casos e a mediana era exatamente 500 | ✅ teto em 50 |
+| **Q** | **O KLEE perdia toda a exploração ao esgotar o orçamento.** Só um `timeout` externo o limitava; um programa com 12 leituras nondet explorou 3982 caminhos e gerou **zero** `.ktest` — `unable to write output test case, losing it`, 3982 vezes. Atingir o orçamento é o caso NORMAL numa corrida de competição | ✅ `--max-time` próprio + busca `dfs` no cover-branches, para os estados terminarem em sequência e gravarem à medida que terminam |
 
 ## Defeitos abertos
 
@@ -110,7 +117,7 @@ Todos com evidência em [findings](reports/2026-08-12-castle-juliet-findings.md)
 | O quê | Contagem |
 |---|---|
 | `ctest` (unitários) | 8 |
-| Integração | 97 asserções em 9 scripts |
+| Integração | ~117 asserções em 12 scripts |
 | Conformidade Test-Comp | 6 programas |
 | Jobs de CI | 10, todos verdes na PR #59 (o 10º builda a imagem no próprio PR) |
 

modules/backend/library/lib/NonDetGeneratorLibFuzzy.c

@@ -76,8 +76,34 @@ int LLVMFuzzerTestOneInput(const uint8_t *Data, size_t Size) {
   return 0;
 }
 
+/* Fills `out` with `size` bytes from the fuzzer's buffer, in target order.
+ *
+ * The generators below used to take ONE byte and cast it, whatever the type.
+ * A `long` could therefore only ever be 0..255; so could a `short`, a
+ * `size_t`, a pointer -- and a `double` could only be an integral value
+ * between 0.0 and 255.0. Nothing negative was reachable at all, because an
+ * unsigned byte cast to a signed type stays non-negative.
+ *
+ * Beyond the obvious loss of reach, this is what made seeding impossible: the
+ * byte layout IS the exchange format between the two engines, and a KLEE
+ * vector holding short x = 4242 cannot be written into a slot one byte wide.
+ * Consuming sizeof(type) puts the fuzzer on the same layout KLEE already uses
+ * -- NonDetGeneratorKlee.c passes sizeof(non_det) to klee_make_symbolic -- so
+ * a vector means the same thing to both. */
+static void get_bytes_from_fuzzer(void *out, size_t size) {
+  unsigned char *destination = (unsigned char *)out;
+  size_t i = 0;
+  for (; i < size; i++) {
+    destination[i] = get_next_input_from_fuzzer();
+  }
+}
+
 #define MAP2CHECK_NON_DET_GENERATOR(type)                                      \
-  type map2check_non_det_##type() { return (type)get_next_input_from_fuzzer(); }
+  type map2check_non_det_##type() {                                            \
+    type value;                                                                \
+    get_bytes_from_fuzzer(&value, sizeof(value));                              \
+    return value;                                                              \
+  }
 
 MAP2CHECK_NON_DET_GENERATOR(char)
 MAP2CHECK_NON_DET_GENERATOR(pointer)
@@ -96,28 +122,27 @@ MAP2CHECK_NON_DET_GENERATOR(sector_t)
 MAP2CHECK_NON_DET_GENERATOR(double)
 // MAP2CHECK_NON_DET_GENERATOR(uint)
 
-// Considering an int on a x64, then a 64 bit integer is 8 times a 8 bit integer
-int map2check_non_det_int() {
-  uint64_t result = 0;
-  int i = 0;
-  for (; i < 8; i++)
-    /* cast before the shift: uint8_t promotes to int, and shifting an int
-     * by up to 56 bits is undefined behavior */
-    result |= (uint64_t)get_next_input_from_fuzzer() << (8 * i);
-
-  return (int)result;
-}
+/* Was reading EIGHT bytes and truncating to int, so half of every integer's
+ * worth of fuzzer entropy was consumed and thrown away -- and, worse for
+ * seeding, the layout did not match what KLEE writes for the same read. */
+MAP2CHECK_NON_DET_GENERATOR(int)
 
-uint map2check_non_det_uint() { return (uint)map2check_non_det_int(); }
+MAP2CHECK_NON_DET_GENERATOR(uint)
+MAP2CHECK_NON_DET_GENERATOR(unsigned)
 
-unsigned map2check_non_det_unsigned() {
-  return (unsigned)map2check_non_det_int();
-}
+/* Upper bound on a fuzzer-chosen string length.
+ *
+ * The length comes from a full-width unsigned, so before this the malloc below
+ * could be asked for four billion bytes on a whim. Any string long enough to
+ * matter for a benchmark fits well inside this. */
+#define MAP2CHECK_MAX_FUZZED_STRING 4096
 
 char *map2check_non_det_pchar() {
   unsigned length = map2check_non_det_unsigned();
   if (length == 0)
     return NULL;
+  if (length > MAP2CHECK_MAX_FUZZED_STRING)
+    length = MAP2CHECK_MAX_FUZZED_STRING;
   /* heap allocation: returning a local VLA would leave the caller with a
    * dangling pointer (cppcheck returnDanglingLifetime) */
   char *string = malloc(length);