fix: six defects in the engine, and the v15 campaign that measures them - #65
Open
GuilhermeBn198 wants to merge 14 commits into
Open
fix: six defects in the engine, and the v15 campaign that measures them#65GuilhermeBn198 wants to merge 14 commits into
GuilhermeBn198 wants to merge 14 commits into
Conversation
… bug
59 of 59 XCSP tasks answered VERIFICATION SUCCEEDED -- "this program is
correct" -- in about two seconds. Every one of those programs has a reachable
bug. It was the single largest block of wrong answers in the corpus: 41% of all
145 false claims of correctness.
The cause is one word. Those programs write
void assume(int cond) { if (!cond) abort(); }
and the rewrite list matched assume_abort_if_not and __VERIFIER_assume but not
the plain name. So the first failing assumption aborted, KLEE halted on it, no
property was ever recorded, and the run reported success. reach_error sits
after twenty-odd assumptions in these files, so it was never reachable.
Same defect already fixed once, missed for being spelled shorter.
Measured after: AllInterval-005 and aim-100-3-4-sat-4 both go SUCCEEDED ->
FAILED, with the rewrite firing.
"assume" is a generic name, so the signature check does more work now: void
taking one integer is the idiom's shape, and anything called assume with
another shape is left alone.
The regression test puts reach_error AFTER the assumptions, the way the XCSP
files do, so a run that still aborts on the first one cannot reach it.
Found by cross-tabulating verdicts against TestCov's validation instead of
reporting the covered rate alone -- 145 SUCCEEDED on programs known to contain
bugs is a number an aggregate hides.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
sbt-slicer drops the DEFINITION of the function it slices towards.
reach_error is where the slice ends -- nothing it does can influence
whether it is reached -- so the call site survives and the body does not.
KLEE tolerates the declaration. The native LibFuzzer link does not:
undefined reference to `reach_error'
No *-fuzzed.out is produced, the fuzzer stage then does nothing at all,
and the run comes back UNKNOWN. Nothing in the log said so.
Measured on reducercommutativity/rangesum05.i:
--nondet-generator fuzzer FAILED, 8 crash inputs
--nondet-generator fuzzer --slice UNKNOWN, 0 crash inputs, no binary
and end to end, hybrid + --slice went from a 0-input suite that TestCov
scored UNKNOWN to a 5-input suite it scores TRUE -- identical to control.
This is what cost the sliced arm the bulk of its 133 lost detections in
the v11 factorial (24.4% covered against a 44.6% control, over 817
paired tasks).
The stub is WEAK, so where the slice did keep the body the strong
definition still wins at link time. Failing to build it warns rather
than aborting: without the stub the fuzzer stage is lost, but KLEE still
runs on the slice.
Also carries the three slicing fixes that were still uncommitted:
LD_LIBRARY_PATH was being set to a literal $VAR, --entry had to become
plain main once slicing moved ahead of instrumentation, and the slice
now runs BEFORE callPass so the instrumentation is applied to what
survives rather than removed by it.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
KLEE can burn its whole budget, halt on the timer, and still leave TARGET-REACHED in map2check_property: a state wrote the file through an external call and was then terminated by --dump-states-on-halt without ever reaching the abort. The verdict logic trusts that file, so the run answers FAILED while emitting a suite with zero <input> elements. Measured on reducercommutativity/rangesum05.i, --nondet-generator symex: 1446 paths explored, HaltTimer, zero .err files, klee_log.csv empty, verdict FAILED, suite empty, TestCov UNKNOWN. This is where FAILED-but-NOT_COVERED comes from -- 21% of the control arm's FAILED verdicts across 817 paired tasks in the v11 factorial. Downgrading costs nothing that was ever scored: Test-Comp scores the SUITE, not the verdict, and a suite with no inputs covers nothing under either label. What it buys is a precision number that means something. The check consults exactly the two sources emitTestSuite consults, so it can never disagree with what actually gets written. Verified: a program KLEE does solve still answers FAILED with its two inputs intact. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Five runs queued behind each other rather than beside each other. The machine has sixteen cores and map2check's LibFuzzer phase runs -jobs=8, so container count -- not container CPU quota -- is what oversubscribes it. Measured: nine containers sit at ~700% CPU with 20% idle, which is the shape to hold. Order: v12 Test-Comp (slice vs its own control, weak-stub fix) and Juliet a+b and CASTLE run now; Juliet c+d chain behind a+b; v13 (FALSE-FAILED guard) chains behind v12 so a contention difference cannot be mistaken for the effect; a one-file-per-family Juliet/CASTLE smoke chains last to show the guard cannot reach modes it is gated out of. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Three defects, one symptom. Every ERROR verdict on the v12 Test-Comp corpus -- 20 of them, concentrated in ECA and Recursive -- landed at 87 to 89 seconds against a 60 second budget and a 90 second outer timeout. The harness reads a missing VERIFICATION line as a crashed tool. 1. The log never reached disk. stdout is block-buffered whenever it is not a terminal, and every harness here redirects it to a file, so a run killed by the outer timeout lost its ENTIRE log -- including a verdict it may already have printed. The logs of those 20 tasks were zero bytes. Log now flushes every message; there are a few dozen per run, so this costs nothing worth measuring. This one also made the other two invisible. With the log surviving, the last line says exactly which step was still running. 2. The LibFuzzer compile was unbounded. Two clang invocations at -O2 over the whole instrumented module, no timeout on either. On the large programs that outlasts the entire budget, and the run was still linking its fuzzer binary when it was killed. Now bounded, and a binary that does not build is announced rather than left as a silent no-op -- the failure mode the sliced arm spent a whole campaign in. 3. The engines sized themselves from the NOMINAL budget: LibFuzzer 0.2x and KLEE 0.8x, which adds to the whole of it and leaves nothing for the two compile-instrument-link passes the hybrid pays between them. They now size against what is LEFT, so the sum stays inside the budget however many phases there turn out to be. Also drops TargetPass's per-function write to errs(): unbuffered, one syscall per function, run once per engine, and on the ECA programs the log of a failing run was tens of thousands of copies of that one line. Kept behind MAP2CHECK_DEBUG_PASSES. eca-rers2012/Problem08_label51.c went from ERROR with an empty log to VERIFICATION UNKNOWN with a test suite. Verified unchanged: rangesum05 under fuzzer, fuzzer --slice, and the hybrid end to end with TestCov, plus a program KLEE solves outright. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
v13 measured the FALSE-FAILED guard alone. Two more fixes landed before it could start -- the log flush and the bounded fuzzer compile -- so the arm that runs next carries all three, and calling it v13 would name a binary that no longer exists. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Same class as the fuzzer compile, same symptom. sbt-slicer builds a system dependence graph over the whole module and had no timeout on it. Measured on the v12 corpus: the sliced arm recorded 26 ERROR verdicts against the control's 9, every one at 87 to 89 seconds, and 17 of them were tasks the control ANSWERED -- three with FAILED. Slicing did not fail on those programs; it took the run past its deadline. A slice that does not finish costs nothing: the existing fallback analyses the whole program, which is what the control does anyway. Overrunning the budget costs the verdict. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…e it BUDGET 60 -> 300. Everything so far ran at 60s, which is a throughput choice rather than a competition one -- and three of the four fixes this arm carries are about what happens when a run reaches its deadline, so the deadline is the one variable that has to be right. Stated plainly because it will be read wrong otherwise: a COVERED rate at 300s is NOT comparable to v12's at 60s. More budget finds more bugs on its own. slice therefore still runs beside its own control here -- that comparison stays valid because both arms move together, while the absolute number becomes the competition-conditions one. CASTLE and Juliet run on the same binary, at THEIR budgets, not at 300s. This run answers "did the four fixes break anything"; changing two variables at once would stop it answering that. Juliet c+d chain behind a+b -- container count is what oversubscribes this machine, not CPU quota. Drops the separate v14 smoke: a full Juliet and CASTLE sweep on the same binary subsumes a one-file-per-family sample of it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Corpus raised to quota 400 per category. The nesting property holds, so
these are supersets of the 40 and 150 used before, in the same order:
partial results stay stratified and comparable.
cover-error 1087 tasks -- the ENTIRE applicable pool, not a sample.
Quota 400 caps only ECA, at 421 applicable. The 819-task
corpus every earlier baseline used covered 74% of it.
cover-branches 2765 tasks of 4330 applicable.
Arms:
cover-error control + slice. Slicing is measured here because here
it has a criterion.
cover-branches control only. Slicing needs something to slice TOWARDS
and Cover-Branches has nothing -- every branch is the
goal -- so a slice arm here would measure the absence
of a feature.
BUDGET=300, the competition figure. Three of the four fixes this binary
carries are about what happens when a run reaches its deadline, so the
deadline is the one variable that has to be real. Cost is not 5x the 60s
runs: measured on v12, the median task takes 18s and only 10% reach the
ceiling.
Juliet moves to PER_FAMILY=10 -- much wider CWE coverage at the price of
the line-by-line comparison with v9, which is recovered by comparing on
the intersection instead. CASTLE runs whole. Both at THEIR budgets, not
at 300s: this half answers "did the four fixes break anything", and
moving two variables at once would stop it answering that.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The corpus runs whole, uninterrupted, so the deadline stops being a truncation mechanism and becomes a backstop. Phase 2 gets six shards rather than three because Cover-Branches is structurally the expensive half, not merely the larger one: Cover-Error exits at the first violating path -- measured median 18s of a 300s budget -- while branch harvesting runs KLEE to the deadline every time and then hands TestCov a suite of up to 50 vectors to validate. Budget the pair at up to 600s per task. 2765 tasks over six shards is ~77h worst case and far less in the mean; phase 1 has released its cores by then, so the six do not contend. Verified before arming, on the same three programs under the previous binary and this one: rangesum05.i 2 testcases / 2 testcases sum01-1.c 14 testcases / 14 testcases standard_copy1_ground-1.c 1 testcase / 1 testcase Cover-Branches is untouched by the budget changes. The two-testcase result that prompted the check is the program, not the binary. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… run
KLEE: ERROR: Illegal number format: 36.75s
Exited klee with 256
KLEE's duration parser rejects a fractional value and exits without
executing a single instruction. The old expression, 0.7*timeout, was
whole for every budget in use and so never exposed this. Its replacement
0.875*kleeBudget is whole only when kleeBudget is a multiple of 8 -- and
kleeBudget now derives from the time REMAINING, which is whatever the
clock says when the previous phase ends.
The failure is total and silent: no symbolic phase at all, so nothing
can be proved safe. Measured against v9 on the Juliet intersection, it
collapsed 464 TN verdicts to 1, and took FN, TIMEOUT and TP down with
them. CASTLE showed the same shape.
Test-Comp at 300s escaped INTERMITTENTLY -- kleeBudget lands on 240 when
the run is fast, and 0.875*240 is 210 -- which is exactly why five
smoke programs at 300s all passed and the defect still shipped. The
cover-error phase it did reach recorded 619 UNKNOWN of 1059, a number I
wrongly attributed to the harder q400 corpus.
Every duration this file emits is now an integer, not only this one.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The v14 run is discarded: the fractional --max-time killed every KLEE
phase, so no number it produced means anything.
The gate is the change that matters. The launchers now wait on the
validation sweep container rather than firing on a timer, so the run
cannot start before the binary has been compared against the
pre-change one. Skipping that ordering is what cost the v14 run.
Validation, install_ld vs install_v15, 16 cases: 14 identical.
juliet --memtrack 6/6 identical -- the mode where the KLEE defect
showed on every single run, since at a 60s budget
--max-time almost never lands on an integer
cover-branches 4/4 identical, including the 50-testcase cap
cover-error 4/6 identical
The two that differed turned out to be the OLD binary being
non-deterministic, not the new one regressing. Three runs each:
dll_of_dll-1.i ld: UNKNOWN SUCCEEDED UNKNOWN v15: UNKNOWN x3
test_locks_5.c ld: SUCCEEDED UNKNOWN SUCCEEDED v15: SUCCEEDED x3
v15 is stable where ld flips. And dll_of_dll's sibling carries
expected_unreach=false, so ld's intermittent SUCCEEDED there was a
wrong answer that v15 no longer gives.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
️✅ There are no secrets present in this pull request anymore.If these secrets were true positive and are still valid, we highly recommend you to revoke them. 🦉 GitGuardian detects secrets in your source code to help developers and security teams secure the modern development process. You are seeing this because you or someone else with access to this repository has authorized GitGuardian to scan your pull request. |
Adds docs/Map2Check-Relatorio-v15.docx -- the report for the v15 campaign: 13 220 tasks across four blocks, all executed to completion on this branch's binary at the competition budget of 300s per task. Test-Comp cover-error 1087 x 2 arms control 470 covered (43.2%) Test-Comp cover-branches 2765 mean coverage 53.0% Juliet 8060 cases TP 1154, TN 3290, FP 120 CASTLE 221 cases TP 54, TN 44, FN 14, FP 1 The cover-error corpus is the ENTIRE applicable pool, not a sample: the quota of 400 per category caps only ECA. Both arms ran the same 1087 tasks, so every comparison is paired. What it establishes: the six fixes on this branch did not move accuracy anywhere -- CASTLE is identical on all 217 comparable cases, Juliet holds TP, FP and FN exactly and gains one TN over 1054 cases. Slicing costs 58 tasks (McNemar chi2 = 36.10), but 57 of them are ECA, and the report declines to conclude "slicing does not work" from that, because none of sbt-slicer's parameters are configured explicitly here while Symbiotic passes criteria we do not. The raw CSVs are NOT versioned. tests/juliet/results*/ and tests/castle/results_v*/ were already excluded; tests/testcomp/ results_v15_*/ now joins them, so all three corpora are treated alike. The numbers that matter live in the report. The v14 results are DELETED rather than left in place. That campaign ran a binary whose KLEE phase aborted without executing an instruction, on a fractional --max-time; no number it produced means anything, and leaving the files in the tree invites citing them. Appendix A records why. .gitignore also now covers build_*/, install_*/ and release/. Each install_* holds ~42 MB of binaries and exists to allow bisection between builds without recompiling -- which is how the --max-time defect was found -- but they are local artefacts. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The three corpora are now treated alike. tests/juliet/results*/ and tests/castle/results_v*/ were already excluded; tests/testcomp/results_*/ joins them, and the 77 CSVs this branch had accumulated come out of the tree. They were never on develop -- every one of them was added by this branch over the v8 to v15 campaigns -- so removing them restores the repository to the shape it had, minus nothing that predates the work. What stays is what a reader needs: the code, the harnesses that produce the data, and docs/Map2Check-Relatorio-v15.docx, which carries the numbers with the definitions required to read them. Raw CSVs in a repository are neither reviewable in a diff nor citable in a paper; they are 15 000 lines that make every future diff harder. The data itself remains on the machine that produced it, and remains recoverable from this branch's history for anyone who needs a row. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
GuilhermeBn198
force-pushed
the
fix/slice-target-stub
branch
from
August 27, 2026 23:56
366fbe1 to
475454b
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Seis correções no motor, medidas por uma campanha completa de 13 220 tarefas, mais o relatório que a lê.
O que quebrou e foi corrigido
Todas as seis têm causa localizada e verificável. Nenhuma é explosão de caminhos.
--max-timefracionário matava o KLEE por inteiro. O parser de duração do KLEE rejeita valor fracionário e sai com 256 sem executar uma instrução. A expressão antiga era inteira por acidente em todos os orçamentos em uso; a nova derivava do tempo restante, que é o que o relógio disser. Falha total e silenciosa: nenhuma fase simbólica, logo nada podia ser provado seguro. Colapsou 464 verdadeiros negativos do Juliet para 1.O slicer apagava o corpo da própria função-critério.
reach_erroré onde a fatia termina, então o sbt-slicer preserva o call-site e descarta a definição. O KLEE tolera; o link nativo do LibFuzzer falha comundefined reference. Nenhum binário de fuzzing era produzido, o estágio do fuzzer não fazia nada, e o run voltava UNKNOWN sem uma linha de log. Corrigido ligando de volta uma definição fraca.O log nunca chegava ao disco.
stdouté bufferizado em bloco quando não é terminal, e todo harness redireciona para arquivo. Um run morto pelo timeout externo perdia o log inteiro, inclusive um veredito já impresso. Esse defeito escondia os dois seguintes.A compilação do LibFuzzer não tinha limite. Dois
clang -O2sobre o módulo instrumentado inteiro, sem timeout. Nos programas grandes isso dura mais que o orçamento todo.Os motores se dimensionavam pelo orçamento nominal, 0,2× + 0,8× = 100%, sem sobrar nada para os dois ciclos de compilar-instrumentar-linkar que o híbrido paga entre eles. Agora medem contra o que resta.
O Map2Check reportava FAILED sem conseguir provar. Um veredito de violação agora exige que o vetor seja recuperável, checando exatamente as duas fontes que o
emitTestSuiteconsulta.O que a campanha mede
Quatro blocos, todos executados integralmente em
install_v15, orçamento de competição de 300 s por tarefa.O corpus de cover-error é o pool inteiro aplicável, não amostra — a cota de 400 por categoria só limita ECA. Os dois braços rodaram as mesmas 1087 tarefas, então toda comparação é pareada.
Não-regressão
CASTLE: 217 de 217 idênticos ao baseline anterior, zero divergências. Juliet: TP, FP e FN exatamente iguais na interseção de 1054 casos, com um TN a mais. As seis correções não moveram acurácia em lugar nenhum.
Sobre o slicing
Controle 470 contra slice 412, McNemar χ² = 36,10. Mas 57 das 58 tarefas perdidas estão em ECA, onde a taxa despenca de 14,5% para 0,2%; fora de ECA o braço empata ou ganha ligeiramente.
O relatório se recusa a concluir "slicing não funciona" a partir disso, e essa recusa é deliberada: nenhum parâmetro do sbt-slicer é configurado explicitamente por nós, e o Symbiotic — de onde a ferramenta vem — passa critérios que não passamos. O resultado pode dizer mais sobre a ausência de configuração do que sobre a técnica.
Slicing e seed exchange permanecem marcados como experimentais.
Relatório
docs/Map2Check-Relatorio-v15.docx— 6448 palavras. Abre com definição de métricas, porque três números distintos deste trabalho poderiam ser chamados de "precisão" e significam coisas diferentes: no cover-error, 1086 das 1087 tarefas têm bug alcançável, logo não existe verdadeiro negativo nem falso positivo possível, e o percentual é recall.Traz onze perguntas em aberto, entre elas:
O que fica de fora
Apenas os CSVs do Test-Comp são commitados;
tests/juliet/results*/etests/castle/results_v*/são excluídos pelo.gitignore, escolha existente do projeto que preservei.Os resultados do v14 são deletados, não mantidos. Aquela campanha rodou o binário do
--max-timefracionário; nenhum número dela significa nada, e deixar os arquivos na árvore convida a citá-los. O apêndice A do relatório registra o porquê.Ressalva
O seed exchange não foi medido com o binário corrigido — o único dado que existe vem de uma campanha invalidada. Fechar isso custa dois braços de cover-error, cerca de dez horas.
🤖 Generated with Claude Code
https://claude.ai/code/session_01Esv32VnfaiPL6gcUyTz5Sp