fix(reachability): announce a target that is never called (finding B)

.github/workflows/ci.yml

@@ -364,6 +364,7 @@ jobs:
               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
             '
 
   # ===========================================================

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-16
+**Última atualização:** 2026-08-22
 
 ## Legenda
 
@@ -47,25 +47,31 @@ disso mudam o quadro, e **nenhuma das duas é explosão de caminhos**:
    não resolvidas**, e 575 se perdem. Quatro fontes de entrada ficam em exatamente
    **50,0%** de acerto entre os decididos — assinatura de provar a variante segura e
    errar a vulnerável.
-2. O **achado K, já investigado**: o timeout descarta violações que a ferramenta
-   já encontrou e gravou em disco. `isTimeout()` tem precedência sobre a
-   propriedade violada, então um FALSE legítimo vira UNKNOWN só porque o
+2. O **achado K, corrigido**: o timeout descartava violações que a ferramenta
+   já tinha encontrado e gravado em disco. `isTimeout()` tinha precedência sobre
+   a propriedade violada, então um FALSE legítimo virava UNKNOWN só porque o
    orçamento acabou *depois* do trabalho estar feito.
 
-**Recomendação de sequência:** medir quantos UNKNOWN do v5 são violações
-descartadas pelo achado K antes de comprometer qualquer pessoa-semana em
-slicing. É uma pergunta respondível com os dados que já temos.
+**O que a medição do v6 respondeu.** No CASTLE, a correção do K mudou **zero**
+vereditos — e o motivo não é que K fosse pequeno, é que o **achado B o mascara**:
+dos 22 casos indecididos no v5 que rerodaram, 20 usam o modo degenerado, onde
+nenhuma violação chega a ser registrada e portanto K não tem o que resgatar.
+Medir K exige um corpus onde os modos sejam reais — o Juliet, ainda em execução.
+
+**Recomendação de sequência:** corrigir o achado B antes de comprometer qualquer
+pessoa-semana em slicing. Ele bloqueia 45% das execuções do CASTLE *e* impede
+medir o efeito de K nesse corpus.
 
 ---
 
 ## Frentes fora do plano original
 
 | Frente | Estado | Evidência |
 |---|---|---|
-| **Invariantes (`--add-invariants`)** | ✅ Fase A + B | Clam `dev16`, `-DENABLE_CLAM=ON`, **desligado por default**. Ver [a revisão da dependência](reports/2026-08-16-crabllvm-review.md) |
+| **Invariantes (`--add-invariants`)** | ✅ **vivo e provado em CI** | Clam `dev16` pinado, `-DENABLE_CLAM=ON`, **desligado por default**. O job `Invariants (Clam)` passou de `ABSENT` para `PRESENT (exit 0)` quando a imagem republicou; a sonda do Dockerfile confirma `Clam injects invariants: OK`. Issue #54 fechada. Ver [a revisão da dependência](reports/2026-08-16-crabllvm-review.md) |
 | 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) | ⬜ | **Regra de atribuição: invariantes DESLIGADOS na corrida principal**, senão overflow + timeout + amostragem + invariantes ficam conjuntamente não creditáveis |
+| 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 |
 | **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 |
 
 ---
@@ -82,16 +88,19 @@ Todos com evidência em [findings](reports/2026-08-12-castle-juliet-findings.md)
 | — | `--add-invariants` aceito e ignorado sem rastro na entrada `.bc` (issue #54) | ✅ sai com código 3 |
 | — | Invocação legada do Crab: `--llvm-pp-loops` e `--crab-promote-assume` anulavam a injeção | ✅ removidas, medido |
 | — | Pass 2 do CASTLE era re-execução byte-idêntica do pass 1 em todo o v5 | ✅ reconhece código 3 |
+| **K** | `isTimeout()` descartava violações já encontradas e gravadas: `TARGET-REACHED found` → `Forcing timeout` → `VERIFICATION UNKNOWN`. Disparava em 80% das execuções do Juliet v5 | ✅ resgate restrito a evidência confiável (`c4ef3a355`) |
+| — | 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) |
 
 ## Defeitos abertos
 
 | # | Defeito | Prioridade |
 |---|---|---|
-| **K** | **Investigado.** `isTimeout()` descarta violações já encontradas e gravadas: `TARGET-REACHED found` → `Forcing timeout` → `VERIFICATION UNKNOWN`. Correção proposta, não aplicada (muda a contagem UNKNOWN→FALSE de todo o baseline) | **Alta** — mecanismo barato de inflar UNKNOWN, sem relação com explosão de caminhos |
 | **K2** | Custo por leitura nondet cresce muito: 1 → 21 → 114 → 861 caminhos parciais para 2 → 4 leituras. Nenhum `.err`, então não são erros | Média — segundo fio a puxar |
 | **G** | `main()` descarta o retorno de `map2check_execution()`; código de saída nunca reflete a análise | Média |
-| **B** | Modo reachability degenerado com `target-function-name main` | Média |
-| — | Garantia de ordenação do corpus depende de um único programa (`two_guards.c`) | Baixa — some quando K for corrigido |
+| **B** | **Medido no v6.** Modo reachability degenerado com `target-function-name main`: 98 de 217 execuções, **zero vereditos FALSE**, 59 programas vulneráveis, 0 detectados. 12 TN e 5 FN pontuados sobre um oráculo que só sabe responder "correto" | **Alta** — 🟡 o caso trivial agora se anuncia (`TargetPass`); falta corrigir o mapeamento CWE→modo do harness, o que **muda a pontuação do baseline** e por isso espera o v6 fechar |
+| — | Garantia de ordenação do corpus depende de um único programa (`two_guards.c`) | Baixa — K já foi corrigido; falta reconferir se ainda vale |
 | — | `CLAUDE.md` linka um `.clang-format` que não existe | Baixa |
 
 ---
@@ -101,9 +110,9 @@ Todos com evidência em [findings](reports/2026-08-12-castle-juliet-findings.md)
 | O quê | Contagem |
 |---|---|
 | `ctest` (unitários) | 8 |
-| Integração | 78 asserções em 7 scripts |
+| Integração | 82 asserções em 8 scripts |
 | Conformidade Test-Comp | 6 programas |
-| Jobs de CI | 9, todos verdes na PR #56 |
+| Jobs de CI | 10, todos verdes na PR #59 (o 10º builda a imagem no próprio PR) |
 
 Gates que provei que **conseguem falhar** (um gate nunca visto vermelho não protege
 ninguém): o do TestCov, invertendo a ordem dos `<input>` no emissor; e o de

docs/reports/2026-08-12-castle-juliet-findings.md

@@ -105,7 +105,7 @@
 |---|---|---|---|
 | A | Truncamento 32-bit no allocation log | `AllocationLog.c` | ✅ corrigido (§1.3) |
 | A2 | Assinatura i64/i32 + ponto de inserção dos binops (overflow runtime quebrado) | `OperationsFunctions.hpp`, `OverflowPass.cpp` | ✅ corrigido (§1.9) |
-| B | `--target-function --target-function-name main` é **degenerado**: TargetPass instrumenta chamadas *para* `main` (que ninguém faz) e `AnalysisModeNone` sempre retorna "correct" | `TargetPass.cpp`, `AnalysisModeNone.c` | aberto (afeta 253/362/369/628/674/770/835) |
+| B | `--target-function --target-function-name main` é **degenerado**: TargetPass instrumenta chamadas *para* `main` (que ninguém faz) e `AnalysisModeNone` sempre retorna "correct" | `TargetPass.cpp`, `AnalysisModeNone.c` | **medido no v6** (§2.1) — 🟡 o caso trivial agora se anuncia; o mapeamento do harness continua aberto |
 | C | `divisionByZeroError()` era TODO no-op | `AnalysisModeOverflow.c:86` | ✅ corrigido (§1.8) |
 | D | Overhead "fuzzer-first": default roda LibFuzzer (60s) antes do KLEE | `map2check.cpp:498-508` | aberto (G5 — lean reachability via `--nondet-generator symex`) |
 | E | 33/250 CASTLE não compilam por headers externos (`mysql.h`, `openssl/*.h`) | imagem Docker | aberto (maioria CWE-89/798, fora de escopo) |
@@ -117,6 +117,65 @@
 | K | **Investigado e corrigido.** O timeout descartava violações já encontradas e gravadas: `isTimeout()` tinha precedência sobre a propriedade violada. Disparava em 80% das execuções do Juliet v5 | `map2check.cpp` | ✅ corrigido — resgate restrito a evidência confiável |
 | K2 | Custo por leitura nondet cresce muito: 1 → 21 → 114 → 861 caminhos parciais para 2 → 4 leituras, sem nenhum `.err` | KLEE + instrumentação | aberto |
 
+### Achado B, medido: um oráculo que só sabe dizer "correto"
+
+O achado B foi registrado em agosto como uma suspeita estrutural: `TargetPass`
+instrumenta *call sites* cujo callee tem o nome pedido, e um programa não chama
+o próprio `main`, logo nada é instrumentado. O baseline v6 do CASTLE permite
+sair da suspeita e medir.
+
+**98 das 217 execuções (45%) rodaram nesse modo.** O que elas produziram:
+
+| veredito | n |
+|---|---|
+| TRUE | 57 |
+| TIMEOUT | 22 |
+| UNKNOWN | 10 |
+| ERROR | 9 |
+| **FALSE-\*** | **0** |
+
+Nenhum FALSE. Não é escassez: nos outros modos, as mesmas 217 execuções
+produzem 49 vereditos FALSE-\* (`FALSE-DEREF` 21, `FALSE-FREE` 12, `FALSE` 10,
+`FALSE-DIVBYZERO` 6, `FALSE-MEMCLEANUP` 6). O modo degenerado é o único que
+nunca acusa nada.
+
+**59 dos 98 programas eram sabidamente vulneráveis. Zero foram detectados.**
+
+O efeito na pontuação tem dois lados, e o segundo é o mais incômodo:
+
+| | efeito |
+|---|---|
+| 5 FN | perdas garantidas — o oráculo não podia acertar |
+| **12 TN** | **crédito por acertos que um oráculo que só diz "correto" não tinha como errar** |
+
+Descontando o modo inteiro, o CASTLE v6 sai de **recall 74,0% para 79,4%**
+(precisão fica em 98,2%: nenhum TP ou FP vem desse modo — ele não produz
+nenhum dos dois). Ou seja, B **não** infla precisão; ele **deprime recall** e
+**infla TN**.
+
+Os outros 61 casos do modo são CWEs que o harness já declara fora de escopo e
+pontua N/A, então não distorcem métrica alguma. Vale corrigir o registro: uma
+leitura anterior atribuiu os 61 N/A ao achado B — eles são N/A por decisão de
+escopo, não por causa dele. O custo real de B são os 17 casos pontuados.
+
+#### O que foi feito e o que falta
+
+Zero call sites **não é um erro**. Se um programa realmente nunca chama
+`reach_error`, então "o erro é inalcançável" é a resposta certa e TRUE é
+legítimo. O defeito é que esse TRUE é **indistinguível**, na saída, de um TRUE
+conquistado explorando o programa.
+
+Então a correção do lado da ferramenta é de visibilidade, não de veredito:
+`TargetPass` agora varre o módulo uma vez e, se o alvo não é chamado em lugar
+nenhum, avisa dizendo o que o veredito vale ali. Coberto por
+`tests/integration/test_target_coverage.sh` (4 asserções), que exige as duas
+direções — o alvo real fica em silêncio, o alvo ausente se anuncia.
+
+O que **falta** é o lado do harness: o mapeamento CWE→modo usa
+`--target-function-name main` como default de escape para 13 CWEs. Corrigi-lo
+muda a pontuação do baseline, então espera o v6 fechar — trocar o critério no
+meio da corrida é exatamente o que torna duas medições incomparáveis.
+
 ### Achado K, investigado: o timeout descarta violações já encontradas
 
 **Sintoma.** Ao montar o corpus de conformidade do Test-Comp, o programa mais

modules/backend/pass/TargetPass.cpp

@@ -13,10 +13,67 @@
 #include <llvm/Passes/PassBuilder.h>
 #include <llvm/Passes/PassPlugin.h>
 
+namespace {
+
+/// Counts the call sites TargetPass will match, across the whole module.
+unsigned countTargetCallSites(const llvm::Module& M, llvm::StringRef Name) {
+  unsigned sites = 0;
+  for (const Function& Fn : M) {
+    for (const BasicBlock& BB : Fn) {
+      for (const llvm::Instruction& I : BB) {
+        const CallInst* callInst = dyn_cast<CallInst>(&I);
+        if (callInst == nullptr) continue;
+        const Function* callee = callInst->getCalledFunction();
+        if (callee == nullptr) {
+          callee = dyn_cast<Function>(
+              callInst->getCalledOperand()->stripPointerCasts());
+        }
+        if (callee != nullptr && callee->getName() == Name) ++sites;
+      }
+    }
+  }
+  return sites;
+}
+
+}  // namespace
+
 PreservedAnalyses TargetPass::run(Function& F,
                                   llvm::FunctionAnalysisManager& AM) {
   llvm::errs() << "Running TargetPass with: " << this->targetFunctionName;
 
+  // Reported once per module, not once per function. This is a function pass,
+  // so there is no module-entry hook to hang it on; opt runs once per
+  // invocation, which makes a local static the honest way to say "first
+  // function we see".
+  //
+  // A target that is never called is NOT an error. If a program genuinely
+  // never calls reach_error, then "the error is unreachable" is the correct
+  // answer and TRUE is right. What is wrong is that such a TRUE looks exactly
+  // like a TRUE earned by exploring the program, and nothing in the output
+  // tells them apart.
+  //
+  // That indistinguishability is the whole of finding B. The CASTLE harness
+  // mapped seven CWEs onto `--target-function-name main`; TargetPass looks for
+  // calls TO main, a program does not call its own entry point, so zero sites
+  // were instrumented. Measured on the v6 baseline: 98 of 217 runs went through
+  // that mode and produced TRUE, TIMEOUT or ERROR -- not one FALSE among them,
+  // on 59 programs known to be vulnerable. Twelve of those runs were scored as
+  // true negatives, credit for answers an oracle that can only say "correct"
+  // could not have failed to give.
+  static bool announcedTargetCoverage = false;
+  if (!announcedTargetCoverage) {
+    announcedTargetCoverage = true;
+    if (countTargetCallSites(*F.getParent(), this->targetFunctionName) == 0) {
+      llvm::errs() << "\n[map2check] WARNING: target function '"
+                   << this->targetFunctionName
+                   << "' is never called in this module. TargetPass"
+                      " instruments call sites, so nothing was instrumented"
+                      " and the reachability property holds trivially: a TRUE"
+                      " verdict here means the target is absent, not that the"
+                      " program is safe.\n";
+    }
+  }
+
   this->targetFunctionMap2Check = F.getParent()->getOrInsertFunction(
       "map2check_target_function", Type::getVoidTy(F.getContext()),
       PointerType::get(F.getContext(), 0), Type::getInt32Ty(F.getContext()),

tests/integration/test_target_coverage.sh

@@ -0,0 +1,104 @@
+#!/bin/bash
+# test_target_coverage.sh -- reachability targets that are never called.
+#
+# TargetPass instruments CALL SITES whose callee matches --target-function-name.
+# If the program never calls that function, nothing is instrumented, and the
+# reachability property holds for a reason that has nothing to do with the
+# program: the target simply is not there.
+#
+# That is not an error, and this test does not treat it as one. A program that
+# genuinely never calls reach_error IS safe with respect to reach_error, and
+# TRUE is the right answer. The defect is that such a TRUE is indistinguishable
+# in the output from a TRUE earned by exploring the program.
+#
+# That indistinguishability is finding B, and it is not hypothetical. The
+# CASTLE harness mapped seven CWEs onto `--target-function-name main`; a
+# program does not call its own entry point, so zero sites were instrumented.
+# On the v6 baseline, 98 of 217 runs went through that mode: 57 TRUE, 22
+# TIMEOUT, 9 ERROR, 10 UNKNOWN -- and not one FALSE, across 59 programs known
+# to be vulnerable. Twelve of them were scored as true negatives.
+#
+# So the contract asserted here is about VISIBILITY: the trivial case must
+# announce itself, and the real case must not cry wolf.
+
+set -u
+
+MAP2CHECK_DIR="${MAP2CHECK_PATH:-/workspace/install_e2e}"
+MAP2CHECK="$MAP2CHECK_DIR/map2check"
+
+PASSED=0
+FAILED=0
+ok()   { echo "  PASS $1"; PASSED=$((PASSED+1)); }
+fail() { echo "  FAIL $1: $2"; FAILED=$((FAILED+1)); }
+
+WORK=$(mktemp -d)
+trap 'rm -rf "$WORK"' EXIT
+
+# One program, used for both cases. It really does call reach_error, so the
+# difference between the two runs below is only which name is asked for --
+# which is the point: the same program is trivially safe with respect to a
+# target it does not contain, and genuinely analysable with respect to one it
+# does.
+cat > "$WORK/prog.c" <<'EOF'
+extern int __VERIFIER_nondet_int(void);
+extern void reach_error(void);
+int main(void) {
+  int x = __VERIFIER_nondet_int();
+  if (x == 7) {
+    reach_error();
+  }
+  return 0;
+}
+EOF
+
+MARKER="is never called in this module"
+
+echo "=== Target coverage warning ==="
+
+# --- Case 1: a target the program really calls -------------------------------
+# The budget is small on purpose. The warning is emitted during instrumentation,
+# long before any solving, so this test never needs the analysis to finish.
+out_real=$( cd "$WORK" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 5 90 \
+  "$MAP2CHECK" --target-function --target-function-name reach_error \
+  --timeout 10 prog.c 2>&1 )
+
+if echo "$out_real" | grep -q "$MARKER"; then
+  fail "a called target stays quiet" \
+       "warned about reach_error, which this program does call"
+else
+  ok "a called target stays quiet"
+fi
+
+# --- Case 2: the degenerate target (finding B) -------------------------------
+out_main=$( cd "$WORK" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 5 90 \
+  "$MAP2CHECK" --target-function --target-function-name main \
+  --timeout 10 prog.c 2>&1 )
+
+if echo "$out_main" | grep -q "$MARKER"; then
+  ok "an uncalled target announces itself"
+else
+  fail "an uncalled target announces itself" \
+       "no warning for --target-function-name main, which nothing calls"
+fi
+
+# The warning has to name the target. A generic "target not found" would send
+# whoever reads the log looking for the wrong thing.
+if echo "$out_main" | grep -q "'main'"; then
+  ok "the warning names the target it is about"
+else
+  fail "the warning names the target it is about" "target name absent"
+fi
+
+# And it has to say what the verdict is worth, not just that something is
+# missing. "TRUE means the target is absent, not that the program is safe" is
+# the part a reader acts on.
+if echo "$out_main" | grep -qi "not that the program is safe"; then
+  ok "the warning says what a TRUE verdict is worth here"
+else
+  fail "the warning says what a TRUE verdict is worth here" \
+       "no statement about the meaning of the verdict"
+fi
+
+echo "  ---"
+echo "  Results: $PASSED passed, $FAILED failed"
+[ "$FAILED" -eq 0 ] || exit 1