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