From 3526ae57c24be55f274d4fdec8ccaef692438750 Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Sat, 22 Aug 2026 16:47:44 -0400 Subject: [PATCH] fix(reachability): announce a target that is never called (finding B) TargetPass instruments call sites whose callee matches the requested name. When the program never calls that function, nothing is instrumented and the reachability property holds trivially -- and nothing in the output says so. Zero call sites is not an error. A program that genuinely never calls reach_error IS safe with respect to reach_error, and TRUE is correct there. The defect is that such a TRUE is indistinguishable from a TRUE earned by exploring the program. So the fix is visibility, not a change of verdict: the pass scans the module once and, when the target has no call sites, says what the verdict is worth. Measured on the CASTLE v6 baseline, which is what moves this from a suspicion to a defect with a number. 98 of 217 runs used `--target-function-name main` -- a program does not call its own entry point: TRUE 57, TIMEOUT 22, UNKNOWN 10, ERROR 9, FALSE-* 0 Not one FALSE, while the other modes produce 49 across the same corpus. 59 of those 98 programs were known to be vulnerable and none was detected. Seventeen were scored: 5 FN, and 12 TN -- credit for answers an oracle that can only say "correct" could not have failed to give. Excluding the mode, recall goes from 74.0% to 79.4%; precision is unchanged at 98.2%, since the mode yields neither TP nor FP. Correcting my own earlier reading: the 61 N/A rows are N/A because the harness declares those CWEs out of scope, not because of finding B. B's real cost is the 17 scored cases. Still open, deliberately: the harness maps 13 CWEs onto this mode as an escape default. Fixing that changes baseline scoring, so it waits for the v6 run to finish rather than moving the criterion mid-run. Verified end to end against a full build, not just the pass in isolation: test_target_coverage.sh 4/4. Co-Authored-By: Claude Opus 5 (1M context) --- .github/workflows/ci.yml | 1 + docs/TESTCOMP-CHECKLIST.md | 37 ++++--- .../2026-08-12-castle-juliet-findings.md | 61 +++++++++- modules/backend/pass/TargetPass.cpp | 57 ++++++++++ tests/integration/test_target_coverage.sh | 104 ++++++++++++++++++ 5 files changed, 245 insertions(+), 15 deletions(-) create mode 100755 tests/integration/test_target_coverage.sh diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 151802d29..5d50d53a1 100644 --- a/.github/workflows/ci.yml +++ 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 ' # =========================================================== diff --git a/docs/TESTCOMP-CHECKLIST.md b/docs/TESTCOMP-CHECKLIST.md index a8cadb5b4..84f9f9e71 100644 --- a/docs/TESTCOMP-CHECKLIST.md +++ b/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,14 +47,20 @@ 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. --- @@ -62,10 +68,10 @@ slicing. É uma pergunta respondível com os dados que já temos. | 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 `` no emissor; e o de diff --git a/docs/reports/2026-08-12-castle-juliet-findings.md b/docs/reports/2026-08-12-castle-juliet-findings.md index abf046bb2..a8803aef5 100644 --- a/docs/reports/2026-08-12-castle-juliet-findings.md +++ b/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 diff --git a/modules/backend/pass/TargetPass.cpp b/modules/backend/pass/TargetPass.cpp index 5ba7d30fe..7d7ee0068 100644 --- a/modules/backend/pass/TargetPass.cpp +++ b/modules/backend/pass/TargetPass.cpp @@ -13,10 +13,67 @@ #include #include +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(&I); + if (callInst == nullptr) continue; + const Function* callee = callInst->getCalledFunction(); + if (callee == nullptr) { + callee = dyn_cast( + 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()), diff --git a/tests/integration/test_target_coverage.sh b/tests/integration/test_target_coverage.sh new file mode 100755 index 000000000..5aab5c024 --- /dev/null +++ b/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