diff --git a/CHANGELOG.md b/CHANGELOG.md index ff411b8a9..828d25d84 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -5,6 +5,74 @@ The format loosely follows [Keep a Changelog](https://keepachangelog.com/en/1.0. ## [Unreleased] +## [9.0.0] - Unreleased + +A major version: the fuzzing engine changed (LibFuzzer → AFL++ 4.40c), the +`--nondet-generator` values changed (`fuzzer` → `afl`), and several verdicts +change meaning -- a KLEE run that did not explore every path is no longer +TRUE, and the program's own `abort()` prunes a path instead of ending the +search. Measured against the v15 baseline in `docs/reports/tacas-experiment-log.md`. + +### Changed (breaking) + +- **The default hybrid is the alternation** (`--alternate-engines`, with seed + exchange) whenever `--timeout` is given. `--fixed-hybrid` keeps the 8.x + schedule. Measured on the 213-task Cover-Error sample: 157 covered, against + 128 for the 8.x hybrid. On Cover-Branches: 53.5% against 46.5% (R26). +- The fuzzer's corpus is part of Cover-Branches suites by default + (`MAP2CHECK_FUZZER_SUITE=0` turns it off). + +- Fuzzing engine: LibFuzzer replaced by AFL++ 4.40c (persistent mode, PCGUARD, + CmpLog). `--nondet-generator fuzzer` is now `--nondet-generator afl`. +- Verdicts: TRUE only from an exhaustive KLEE exploration. KLEE exiting 0 after + its timer, after concretizing a symbolic input (floats), after killing + states (`*.err`, `*.early`), near its memory cap, or after crashing is now + UNKNOWN, never TRUE. +- The program's own `abort()` (inline or through `assume_abort_if_not`) prunes + the path (`map2check_assume(0)`, `klee_silent_exit` under KLEE) instead of + stopping KLEE's search. + +### Added + +- `--slice` for every property (reachability, assert, memtrack, memcleanup, + overflow) through sbt-slicer, preserving the nondet read order; the slice is + computed once per run (`.slice/`), a slicer failure is remembered, and + the criteria are collected without regex. Experiment knobs: + `MAP2CHECK_SLICE_CLEANUP=light|o2`, `MAP2CHECK_SLICER_FLAGS`. +- `--seed-exchange`: the engines hand each other input vectors through a + persistent store (`.seeds/`) -- the fuzzer queue, replayed through the + witness binary into typed `.ktest` seeds for KLEE (ranked: new-edge entries + first), and KLEE's vectors back to the fuzzer. +- `--alternate-engines`: AFL++ and KLEE take turns, each ending when its engine + stagnates (`AFL_EXIT_ON_TIME`; KLEE's covered instructions from `run.stats`, + SQLite optional), with windows and patience doubling every round. +- KLEE's vectors, completed with zeros past their end, are run natively + through the witness after every KLEE phase that found nothing. +- AFL++ binaries built once per run (`.build/`), within one build budget. +- The fuzzer's corpus contributes Cover-Branches test cases (up to half the + suite, deduplicated). +- `--add-invariants` profiles (`MAP2CHECK_CLAM_PROFILE=default|memory|none`), + the number of invariants inserted in the log, and a fallback when Clam + fails. `MAP2CHECK_PREOPT=ssa` (reachability and assert): the module in SSA + form before instrumentation. +- `MAP2CHECK_CHECK_CSTRINGS=1`: the strings a `%s` or `puts` reads are checked. + +### Fixed + +- The AFL++ generator replayed its input from the start past its end: a + `while (__VERIFIER_nondet_int())` loop never ended and afl-fuzz aborted in + its dry run. Reads past the end are now zero. +- MemoryTrackPass matched memory intrinsics by their LLVM 6 names: + `memset/memcpy/memmove` were never checked under LLVM 16. +- A fuzzer binary that fails to link is reported with its cause instead of as + a build timeout; an unreadable input program is reported as such. +- The Cover-Branches suite: the 50-case cap and duplicates count across + phases, and a run starts from an empty suite. +- Evaluation harnesses: children no longer inherit the manifest's descriptor + (the program under test could move the loop's offset); a crash replayed from + the fuzzer is not a tool failure. + + ### Changed - Replaced LibFuzzer with AFL++ 4.40c (persistent, PCGUARD) as the fuzzing engine. diff --git a/CLAUDE.md b/CLAUDE.md index 6e3827fb7..f48d9f3f3 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -61,6 +61,14 @@ the driver is present at `$CLAM_DIR/bin/clam.py`. It is opt-in because an unsoun invariant produces a wrong TRUE rather than an error — see [the dependency review](docs/reports/2026-08-16-crabllvm-review.md). +Status of `--add-invariants` (2026-09-30): **optional and under study**. +- The crab-llvm invariants of the SV-COMP 2019/2020 builds were emitted as `llvm.assume`, + which neither `NonDetPass` nor KLEE consumes. +- On the current hybrid, Clam's profiles (`MAP2CHECK_CLAM_PROFILE=default|memory|none`) + have shown no gain so far. +- A dedicated study round is pending; see `docs/reports/tacas-experiment-log.md` (INV-1, + R25) and `docs/backlog.md`. + Enabling sanitizers switches from static to shared linking and enables `-fsanitize=address,undefined -fno-omit-frame-pointer -g`. ### Run unit tests @@ -107,6 +115,18 @@ Entry point: `map2check.cpp` → `main()`. Parses CLI options (via Boost.Program 5. `executeAnalysis()` — run the instrumented binary; collect results 6. Witness/counterexample generation in [counter_example/](modules/frontend/counter_example/) and [witness/](modules/frontend/witness/) +With no `--nondet-generator`, `main()` runs the hybrid, and each phase builds a new `Caller`: +- **Alternating (the default since 9.0, needs `--timeout`):** AFL++ and KLEE take turns + (`alternateEngines()`), each stopped on stagnation. +- **Fixed (`--fixed-hybrid`):** the 8.x schedule. + +State that must survive the phases lives beside the scratch directory, not inside it: +`.seeds/` (seed store), `.slice/` (slice cache) and `.build/` (AFL++ +binaries). + +A TRUE verdict requires an exhaustive KLEE run: see `kleeDroppedPaths()` in +`modules/frontend/test_suite/ktest_reader.cpp`. + **Verification modes** (enum `Map2CheckMode`): `MEMTRACK_MODE`, `REACHABILITY_MODE`, `OVERFLOW_MODE`, `ASSERT_MODE`, `MEMCLEANUP_MODE`. To add a new analysis: extend `callPass()` in [caller.cpp](modules/frontend/caller.cpp) and add a CLI option in [map2check.cpp](modules/frontend/map2check.cpp). diff --git a/CMakeLists.txt b/CMakeLists.txt index a10f305e4..b3f272042 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -1,5 +1,5 @@ cmake_minimum_required(VERSION 3.20) -project(Map2Check VERSION 8.0.0 LANGUAGES C CXX) +project(Map2Check VERSION 9.0.0 LANGUAGES C CXX) option(BUILD_DOC "Build documentation" OFF) option(SKIP_AFL_PLUS_PLUS "Don't use AFL++" OFF) diff --git a/Dockerfile.dev b/Dockerfile.dev index 9a8080ba2..9499e6c09 100644 --- a/Dockerfile.dev +++ b/Dockerfile.dev @@ -177,8 +177,12 @@ RUN printf 'int main(void){return 0;}\n' > /tmp/aflcheck.c && \ # libzstd-dev is required, not optional: LLVM 16 from apt.llvm.org exports # zstd::libzstd_shared, so Clam's find_package(LLVM) fails outright without it. # libflint-dev is NOT needed -- that belongs to the PPLite domain, and no -# optional domain is enabled here: --crab-track=num uses the default interval -# domain, so LDD, Apron, Elina and PPLite would all be dead weight. +# optional domain is enabled here. Clam's default domain is zones (a DBM, +# built into Crab), the same default the crab-llvm of the SV-COMP builds had; +# what LDD, Apron, Elina and PPLite would add is boxes, oct and pk, which the +# old engine shipped (Apron) and --add-invariants never selected. Whether they +# are worth building is part of the pending --add-invariants study +# (docs/backlog.md). RUN apt-get update && apt-get install -y \ libmpfr-dev \ libzstd-dev \ diff --git a/README.md b/README.md index 9fcf74bfe..8286728b2 100644 --- a/README.md +++ b/README.md @@ -71,6 +71,77 @@ $ ./map2check --help When you use a LLVM bytecode as input for the tool, be sure to add `-g` flag when generating the file, it is not required, but map2check will provide better info (like line numbers). +#### Engines, test suites and analysis options (9.0) + +

+Map2Check generates inputs with two engines: the AFL++ 4.40c fuzzer (persistent mode, PCGUARD, +CmpLog) and the KLEE 3.1 symbolic executor. By default, and whenever --timeout is +given, the two run as an alternating hybrid. They take turns, each turn ends once its engine stops +finding new coverage, and every round doubles the turn's window. The engines also hand each other +input vectors. +

+ +| Option | Effect | +|---|---| +| *(default, with `--timeout`)* | Alternating hybrid with seed exchange. Same as `--alternate-engines`. | +| `--fixed-hybrid` | The 8.x schedule: the fuzzer for 0.2 of the budget, then KLEE. | +| `--fixed-hybrid --seed-exchange` | The 8.x schedule with seed exchange (0.2 / 0.6 / 0.2, with a last fuzzer phase). | +| `--nondet-generator afl` / `symex` | One engine only: AFL++ or KLEE. In 8.x the fuzzer value was `fuzzer`. | +| `--slice` | Slice the program before the analysis (sbt-slicer), for reachability, `--check-asserts`, `--memtrack`, `--memcleanup-property` and `--check-overflow`. | +| `--generate-test-suite` | Emit a Test-Comp test suite (`test-suite/`). | +| `--generate-test-suite --cover-branches` | Emit a Cover-Branches suite, up to 50 cases, from KLEE's paths and the fuzzer's corpus. | +| `--add-invariants` | Optional, and off in the default build. See below. | + +

+Verdicts. A TRUE verdict needs KLEE to have explored every path. Map2Check reports +UNKNOWN instead when KLEE stopped early for any reason: +

+ +- its timer ran out; +- it concretized a symbolic input (for example a floating-point value); +- it killed states; +- it hit its memory cap; +- it crashed. + +

+A call to abort() in the program under analysis is treated the way SV-COMP treats it: as +an assumption. It prunes that path and does not end the search. +

+ +

+Environment knobs. These exist for experiments; the defaults are the measured choices. +

+ +| Variable | Default | Meaning | +|---|---|---| +| `MAP2CHECK_FUZZER_SUITE` | on | `0` leaves the fuzzer's corpus out of Cover-Branches suites. | +| `MAP2CHECK_SLICE_CLEANUP` | none | `light` or `o2`: an opt pipeline over the fresh slice. Measured neutral. | +| `MAP2CHECK_SLICER_FLAGS` | — | Extra sbt-slicer flags, e.g. `--cda=ntscd`. Measured neutral. | +| `MAP2CHECK_PREOPT` | off | `ssa`: mem2reg + simplifycfg before instrumentation, for reachability and assert only. Measured neutral in the hybrid. | +| `MAP2CHECK_CHECK_CSTRINGS` | off | `1`: check the strings a `%s` or `puts` reads. It fixes one wrong TRUE on Juliet, but produces false positives on memory the runtime does not track (CASTLE: FP from 1 to 4). | +| `MAP2CHECK_CLAM_PROFILE` | default | `memory` or `none`: see `--add-invariants`. | + +

+--add-invariants inserts abstract-interpretation invariants computed by +Clam (formerly crab-llvm). The build must be configured +with -DENABLE_CLAM=ON and Clam installed at $CLAM_DIR; otherwise the option is +refused with exit code 3. +

+ +

+The option stays optional while it is under study. So far: +

+ +- In the SV-COMP 2019/2020 builds, the invariants reached neither the instrumentation nor KLEE: they were emitted as `llvm.assume`. +- On the current hybrid, the first measurement found no gain. +- Clam is bounded to 0.2 of the budget and falls back to the plain compile when it fails. +- A dedicated study round is planned. See `docs/reports/tacas-experiment-log.md` (INV-1, R25). + +

+Measurements of every option above are recorded in +docs/reports/tacas-experiment-log.md. +

+ ___ #### Verifying WebAssembly (WASM) binaries diff --git a/docs/backlog.md b/docs/backlog.md new file mode 100644 index 000000000..d67822c40 --- /dev/null +++ b/docs/backlog.md @@ -0,0 +1,66 @@ +# Backlog + +Itens decididos como "não agora", cada um com o motivo e onde está a evidência. + +## `--add-invariants`: rodada dedicada de estudo + +- **Estado:** a opção é opcional e fica desligada no build padrão (`-DENABLE_CLAM=OFF`). + O usuário ainda desconfia da conclusão "não ajuda". +- **O que já se sabe** (log de experimentos, INV-1 e R25): + - Na v7.3 os invariantes saíam como `llvm.assume` e ficavam inertes. Até out/2018 eles + chegavam ao KLEE (`--crab-track=arr --crab-add-invariants=after-load`). + - Numa sonda só com o KLEE, o ganho veio do pré-processamento em SSA, não dos + invariantes. + - No híbrido (71 tarefas de Cover-Error e 50 de MemSafety), os perfis do Clam não + ganharam e o MemSafety teve mais FALSE errados (4 contra 2). Parte dos ERROR vinha do + Clam sem limite de tempo, já corrigido. +- **O que a rodada precisa responder:** + - efeito só com o KLEE (`--nondet-generator symex`), onde os invariantes têm mais + chance de pesar, separado do efeito no híbrido; + - por que os FALSE errados de MemSafety aumentam: um invariante incorreto ou o + caminho de compilação do Clam (`-m 64`, pré-processamento próprio); + - os domínios que o motor antigo tinha e o nosso Clam não compila: Apron (`oct`, + `pk`) e LDD (`boxes`); + - o gate: nenhuma detecção perdida no CASTLE e numa amostra do Juliet. + +## Limite de memória do KLEE nas rodadas paralelas + +- **Sintoma:** com 8 contêineres, e às vezes com 4, a memória da máquina (23 GB) chega a + ficar crítica. O KLEE usa até `--max-memory` = 2000 MB por processo. Um KLEE morto + pelo OOM killer sai como "did not finish its run", ou seja UNKNOWN, e contamina a + medição. Os vigias do Claude Code também foram encerrados por isso. +- **Opções:** + - passar `--max-memory` por execução, proporcional às vagas; + - limitar a memória por contêiner (`docker run --memory`); + - registrar no resultado quando o KLEE morreu por falta de memória, para descartar e + repetir essas tarefas. +- **Por que não agora:** não afeta o produto (uma execução de competição tem uma tarefa + por máquina), só a infraestrutura de medição. + +## Harness de campanha fora do repositório + +- Os escalonadores das rodadas R19 a R26 vivem em `../tacas-results/` e não são + versionados, por decisão: campanhas não pertencem ao repositório do produto. +- Dois defeitos deles contaminaram rodadas, e quem escrever o próximo precisa evitá-los: + - `IFS=$'\t' read` junta tabs consecutivos, e uma coluna vazia desloca as seguintes; + usar `-` nos campos vazios; + - os filhos herdavam o manifest pelo descritor 3. Corrigido no harness do repositório + (`3<&-`). + +## Validação de witness (fase D, item 4.2): estudo, a discutir com o orientador + +- **Estado atual:** + - O Map2Check gera só witness **GraphML** (`--generate-witness`, formato 1.0), gravado + em `../witness.graphml` a partir do scratch. + - Não gera o formato **2.0 (YAML)**, adotado pelo SV-COMP. É preciso confirmar no + call do ano quais formatos ainda são aceitos. + - Nenhum teste valida os witnesses gerados. + - A Test-Comp não usa witness; a suíte é validada pelo TestCov. O item só pesa para o + SV-COMP. +- **Caminho barato já esboçado (validação por execução):** compilar o programa original + (com ASan, para as propriedades de memória), alimentá-lo com o vetor que viola a + propriedade (que o Map2Check já emite na suíte de Cover-Error) e confirmar o + `reach_error` ou o crash. É parecido com o que o TestCov faz e com os validadores por + execução do SV-COMP. +- **Não começar a implementação** antes da conversa com o orientador: definir se o + objetivo é o formato 2.0, a validação por execução, os dois ou nenhum. diff --git a/docs/migration-schedule.md b/docs/migration-schedule.md index 17b23e94e..d2a4c039d 100644 --- a/docs/migration-schedule.md +++ b/docs/migration-schedule.md @@ -4,6 +4,15 @@ **Fim previsto:** 30/Mai/2027 **Regime:** ~5h/dia útil de desenvolvimento efetivo +> **Situação em 29/Set/2026 — linha TACAS.** As fases 2 e 3 foram antecipadas e entregues +> por um caminho diferente do planejado abaixo: o slicing usa o `sbt-slicer` (dg) como +> processo externo, e não uma biblioteca integrada; a coordenação AFL++ ↔ KLEE roda dentro +> do frontend C++, e não num coordenador Python com IPC. As tabelas das fases 2 e 3 trazem +> o status real e onde cada item foi feito. Medições em `docs/reports/tacas-experiment-log.md` +> (rodadas R1–R19). Resultado de referência (R15, Cover-Error, 213 tarefas, 300 s): controle +> tacasv2 **129 cobertas** × v15 111, TRUE errado 27 → 5, tempo mediano 43 → 5 s; com a troca +> de sementes (R16) **148 cobertas**. + --- ## Métricas do Codebase Atual @@ -176,19 +185,19 @@ | Done | ID | Tarefa | Início | Fim | Dias | Teste | Relatório | |:-----|:---|:-------|:-------|:----|:-----|:------|:----------| -| ☐ | 2.1.1 | Criar `FindDG.cmake` (FetchContent de `mchalupa/dg`) | 28/Set | 30/Set | 3 | DG compila com LLVM 16 | — | -| ☐ | 2.1.2 | Validar `llvm-slicer` standalone no container | 01/Out | 02/Out | 2 | Slice de programa simples funciona | — | -| ☐ | 2.1.3 | Criar módulo `SlicingPreprocessor` (API C++) | 05/Out | 16/Out | 10 | Testes unitários do módulo | — | -| ☐ | 2.1.4 | Definir critério de slicing automático (`__VERIFIER_error` + MemSafety) | 19/Out | 23/Out | 5 | Slice preserva instruções de interesse | `docs/migration/2.1-dg-library.md` | +| ✅ | 2.1.1 | ~~`FindDG.cmake`~~ → `sbt-slicer` (dg) instalado no `Dockerfile.dev` em `/opt/sbt-slicer` | 28/Set | 26/Set | — | Slicer roda com LLVM 16 | tacasv2a | +| ✅ | 2.1.2 | Validar o slicer standalone no container | 01/Out | 26/Set | — | Slice de programa simples funciona | tacasv2a | +| ✅ | 2.1.3 | ~~`SlicingPreprocessor`~~ → `Caller::runSlicer` + `utils/slicer.hpp` (critérios, estatísticas, stub do alvo) | 05/Out | 27/Set | — | `SlicerTest` (21 testes) | specs `2026-09-2{6,7}-tacasv2{a,b,c}-*` | +| ✅ | 2.1.4 | Critérios por propriedade: alvo/assert antes da instrumentação; `map2check_*` + nondets + externas + intrínsecos de memória depois dela (memsafety, memcleanup, overflow) | 19/Out | 27/Set | — | Integração §13–§25 | `docs/reports/tacas-experiment-log.md` (R1–R14b) | ### 2.2 Integração no Pipeline (Semanas 18-20) | Done | ID | Tarefa | Início | Fim | Dias | Teste | Relatório | |:-----|:---|:-------|:-------|:----|:-----|:------|:----------| -| ☐ | 2.2.1 | Adicionar opção `--slice` ao CLI | 26/Out | 27/Out | 2 | `map2check --help` mostra opção | — | -| ☐ | 2.2.2 | Integrar pipeline: `C → IR → Slice → Instrumentação → Análise` | 28/Out | 06/Nov | 8 | Suite completa com `--slice` ativo | — | -| ☐ | 2.2.3 | Testes comparativos: com e sem slicing nos 9 benchmarks | 09/Nov | 13/Nov | 5 | Tabela de redução de tamanho bitcode | — | -| ☐ | 2.2.4 | Testes em benchmarks SV-COMP ReachSafety (amostra) | 16/Nov | 20/Nov | 5 | ≥ baseline em cobertura | `docs/migration/2.2-slicing-pipeline.md` | +| ✅ | 2.2.1 | Opção `--slice` no CLI | 26/Out | 26/Set | — | `map2check --help` mostra opção | tacasv2a | +| ✅ | 2.2.2 | Pipeline `C → IR → Slice → Instrumentação → Análise` (e slice pós-instrumentação para memória/overflow) | 28/Out | 27/Set | — | Integração com `--slice` | tacasv2a/b/c | +| ✅ | 2.2.3 | Comparativos controle × slice (Test-Comp, MemSafety, NoOverflows, CASTLE, Juliet) | 09/Nov | 28/Set | — | R8–R15 | `docs/reports/tacas-experiment-log.md` | +| ⏳ | 2.2.4 | Test-Comp Cover-Error: slice **empata** com o controle (126 × 129, R15) — otimizações na 2.4 | 16/Nov | — | — | ≥ controle em cobertas, TRUE errado = 0 | R15, R19 | ### 2.3 Validação e Buffer (Semanas 21-22) @@ -197,6 +206,15 @@ | ☐ | 2.3.1 | Medir impacto: memória, tempo, taxa de unknown | 23/Nov | 27/Nov | 5 | Relatório quantitativo | `docs/migration/2.3-fase2-final.md` | | ☐ | 2.3.2 | **Buffer/contingência** | 30/Nov | 04/Dez | 5 | — | — | +### 2.4 Otimizações do slicing — tacas 2d (Set/2026) + +| Done | ID | Tarefa | Teste | Relatório | +|:-----|:---|:-------|:------|:----------| +| ✅ | 2.4.1 | Fatiar uma vez por execução (cache `.slice/`, inclusive da falha do slicer) — elimina os 4 ERROR de ECA da R15 | Integração §31 | spec `2026-09-29-tacas-2d-slicing-optimizations-design.md` | +| ⏳ | 2.4.2 | Limpeza pós-slice (`MAP2CHECK_SLICE_CLEANUP` = `light` ou `o2`) — em medição | R19 | — | +| ⏳ | 2.4.3 | Parâmetros do dg (`--cda=ntscd`, `--pta=fs`) — em medição | R19 | — | +| ☐ | 2.4.4 | Cutoff-diverging com `!dbg` (só se 2.4.1–2.4.3 não bastarem) | — | — | + > **Marco Fase 2:** Slicing funcional, redução mensurável em timeouts > **Data-alvo:** 04/Dez/2026 @@ -208,29 +226,40 @@ | Done | ID | Tarefa | Início | Fim | Dias | Teste | Relatório | |:-----|:---|:-------|:-------|:----|:-----|:------|:----------| -| ☐ | 3.1.1 | `FindAFLPlusPlus.cmake` — compilar/instalar AFL++ 4.40c | 07/Dez | 11/Dez | 5 | `afl-fuzz --version` OK | — | -| ☐ | 3.1.2 | Instrumentação AFL++ com LLVM 16 (modo PCGUARD) | 14/Dez | 18/Dez | 5 | Programa de teste instrumentado e fuzzado | — | -| ☐ | 3.1.3 | Wrapper de compilação para programas com instrumentação AFL++ | 21/Dez | 24/Dez | 4 | Programa fuzzeado encontra crash | — | -| ☐ | 3.1.4 | Validação: fuzzing standalone em benchmarks simples | 05/Jan | 09/Jan | 5 | ≥3 crashes encontrados em programas unsafe | `docs/migration/3.1-aflpp.md` | +| ✅ | 3.1.1 | AFL++ 4.40c no `Dockerfile.dev` (toolchain em `/usr/local/bin`), substituindo o LibFuzzer | 07/Dez | 25/Set | — | `afl-fuzz --version` OK | tacasv1 | +| ✅ | 3.1.2 | Instrumentação PCGUARD + modo persistente + binário CmpLog | 14/Dez | 26/Set | — | Programa instrumentado e fuzzado | tacasv1 | +| ✅ | 3.1.3 | Pipeline de compilação AFL++ no `Caller` + replay de crash pelo binário witness | 21/Dez | 26/Set | — | Crash confirmado por replay | tacasv1 | +| ✅ | 3.1.4 | Validação em Test-Comp; correções: leitura após o fim da entrada devolve zero (laços `while(nondet)` travavam o dry run) | 05/Jan | 29/Set | — | Integração §32 | spec `2026-09-25-tacasv1-aflpp-migration-design.md` | ### 3.2 Coordenador Central (Semanas 27-30) | Done | ID | Tarefa | Início | Fim | Dias | Teste | Relatório | |:-----|:---|:-------|:-------|:----|:-----|:------|:----------| -| ☐ | 3.2.1 | Criar módulo `coordinator/` (Python + subprocess) | 12/Jan | 16/Jan | 5 | Testes unitários do módulo | — | -| ☐ | 3.2.2 | IPC POSIX: shared memory + semáforos | 19/Jan | 23/Jan | 5 | Comunicação bidirecional testada | — | -| ☐ | 3.2.3 | Ciclo de vida: AFL++ → monitoramento → KLEE → reinjeção | 26/Jan | 06/Fev | 10 | Programa simples verificado end-to-end | — | -| ☐ | 3.2.4 | Heurística de Desbloqueio de Fronteira (Δt, proximidade) | 09/Fev | 13/Fev | 5 | Detecção de estagnação + branch flipping | `docs/migration/3.2-coordinator.md` | +| ✅ | 3.2.1 | ~~`coordinator/` em Python~~ → laço `alternateEngines()` no frontend C++ (`--alternate-engines`) | 12/Jan | 29/Set | — | `AlternationTest` | spec `2026-09-29-tacas-3b-engine-alternation-design.md` | +| ✅ | 3.2.2 | ~~IPC POSIX~~ → troca por arquivos no store `.seeds/` (fases sequenciais, 1 núcleo) | 19/Jan | 28/Set | — | Integração §11, §26–§28 | tacas 3a | +| ✅ | 3.2.3 | Ciclo AFL++ → KLEE → reinjeção, em rodadas com janelas que dobram | 26/Jan | 29/Set | — | Integração §33 | tacas 3b | +| ⏳ | 3.2.4 | Detecção de estagnação (`AFL_EXIT_ON_TIME`; `CoveredInstructions` do `run.stats` do KLEE) — em medição; *branch flipping* por proximidade ainda não | 09/Fev | — | — | R19 | tacas 3b | ### 3.3 Smart Seeds e Validação (Semanas 31-34) | Done | ID | Tarefa | Início | Fim | Dias | Teste | Relatório | |:-----|:---|:-------|:-------|:----|:-----|:------|:----------| -| ☐ | 3.3.1 | Gerenciador de Smart Seeds (serialização, conversão, filtro) | 16/Fev | 20/Fev | 5 | Seeds transferidas AFL++ ↔ KLEE | — | -| ☐ | 3.3.2 | Ranking por densidade SDG | 23/Fev | 27/Fev | 5 | Seeds priorizadas corretamente | — | -| ☐ | 3.3.3 | Teste integrado: pipeline completo com coordenação | 02/Mar | 06/Mar | 5 | Benchmark com melhoria de cobertura | `docs/migration/3.3-fase3-final.md` | +| ✅ | 3.3.1 | Smart seeds: fila do AFL++ → replay tipado → `.ktest`; `.ktest` → bytes do AFL++ (`--seed-exchange`) | 16/Fev | 28/Set | — | `SeedStoreTest`, `KtestReaderTest` | spec `2026-09-28-tacasv3a-smart-seeds-plumbing-design.md` | +| ☐ | 3.3.2 | Ranking de sementes (novidade de cobertura; densidade SDG) — tacas 3c | 23/Fev | — | 5 | Seeds priorizadas corretamente | — | +| ⏳ | 3.3.3 | Teste integrado com coordenação: R16 (seeds 148 × 129 cobertas); R19 (alternância) em curso | 02/Mar | — | — | Benchmark com melhoria de cobertura | `docs/reports/tacas-experiment-log.md` | | ☐ | 3.3.4 | **Buffer/contingência** | 09/Mar | 13/Mar | 5 | — | — | +### 3.4 Correções de veredito achadas nas rodadas TACAS + +| Done | ID | Correção | Teste | +|:-----|:---|:---------|:------| +| ✅ | 3.4.1 | KLEE parado pelo HaltTimer não é prova (TRUE errado 27 → 5 na R15) | Integração | +| ✅ | 3.4.2 | Vetor vazio conta como testemunha (programas sem entrada) | `KtestReaderTest` | +| ✅ | 3.4.3 | `abort()` do programa poda o caminho (`map2check_assume(0)`), não encerra a busca do KLEE | Integração §29 | +| ✅ | 3.4.4 | KLEE que concretizou uma entrada ou matou estados cedo não é prova | Integração §30 | +| ☐ | 3.4.5 | MemoryTrackPass não instrumenta os intrínsecos `llvm.memcpy/memset/memmove` do LLVM 16 | — | +| ☐ | 3.4.6 | Falso positivo do memtrack no busybox `sleep-3` | — | + > **Marco Fase 3:** Coordenador funcional, AFL++ ↔ KLEE com Smart Seeds > **Data-alvo:** 13/Mar/2027 diff --git a/docs/reports/2026-08-16-crabllvm-review.md b/docs/reports/2026-08-16-crabllvm-review.md index 9bbd10a42..0d71e71a6 100644 --- a/docs/reports/2026-08-16-crabllvm-review.md +++ b/docs/reports/2026-08-16-crabllvm-review.md @@ -283,3 +283,28 @@ Tudo verificável e datado de 2026-08-16: - Leitura direta dos cinco pontos de acoplamento no Map2Check, citados por arquivo e linha - Baseline v5 para os números de externas não resolvidas e de precisão + +--- + +## Adendo (2026-09-30): o que o motor antigo fazia de fato + +Medido com o release v7.3.1 (SV-COMP 2020), que roda em `python:2.7-slim` com o clang do +LLVM 6 que vem nele. Detalhes em `docs/reports/tacas-experiment-log.md`, INV-1 e R25. + +- **Houve duas configurações.** Até 18/10/2018 (commit `4bb409c20`) o Map2Check usava + `--crab-track=arr --crab-add-invariants=after-load`, e os invariantes saíam como + `verifier.assume`, que o NonDetPass mapeava para `klee_assume`. Da v7.3 em diante + entrou o `--crab-promote-assume`, que emite `llvm.assume`. O NonDetPass antigo não o + mapeava, e o KLEE 2.1 do release o ignora (o mesmo vale para o KLEE 3.1). **Nas versões + de competição de 2019 e 2020 os invariantes não tinham efeito.** +- A seção 2 desta revisão já suspeitava disso ("a invocação legada não teria injetado + nada"); agora está medido. +- **O que parecia funcionar** provavelmente era o caminho de compilação: passar pelo + crab-llvm, e hoje pelo Clam, deixa o módulo em SSA, e o KLEE explora isso melhor. Numa + sonda só com o KLEE, o Clam sem nenhum invariante decidiu o que o pipeline normal + deixava UNKNOWN. +- **No híbrido atual** (R25) os perfis do Clam não ganharam, e o MemSafety teve mais + FALSE errados. +- A opção continua **opcional**. Os perfis (`MAP2CHECK_CLAM_PROFILE=default|memory|none`), + a contagem de invariantes no log, o limite de 0,2T e o recuo para a compilação normal + entraram na 9.0. A rodada dedicada de estudo está em `docs/backlog.md`. diff --git a/docs/reports/2026-09-29-handoff-tacas.md b/docs/reports/2026-09-29-handoff-tacas.md new file mode 100644 index 000000000..21b0d5e20 --- /dev/null +++ b/docs/reports/2026-09-29-handoff-tacas.md @@ -0,0 +1,215 @@ +# Handoff TACAS — 2026-09-29 (atualizado à tarde) + +Ponto de partida para a próxima sessão. Regras do usuário que continuam valendo: + +- **Nunca mergear**: sempre abrir PR, com base `develop`. +- Branches se chamam `feat/…`. **Não mexer no gatilho do `ci.yml`**. +- **Registrar cada mini-rodada** em `docs/reports/tacas-experiment-log.md` e comparar uma + a uma. +- LibFuzzer está abandonado. +- Commits e PRs em inglês; docs e relatórios em pt-BR. +- **Nunca rodar `cmake .` num `build_*` sem `-DCMAKE_INSTALL_PREFIX`.** O prefixo volta + para `release/` e o `ninja install` sobrescreve a instalação de referência. + +Em 2026-09-29 o usuário delegou as decisões ("você tem permissão para fazer as decisões que +quiser") e pediu, nesta ordem: +1. investigar os TRUE errados restantes; +2. implementar o 2d e o 3b com as abordagens recomendadas; +3. lançar os testes ao final. + +## 1. Pilha de branches (locais, **nenhuma enviada ainda**) + +Cada branch parte da anterior. As PRs devem ser abertas em cadeia (cada uma com base na +anterior, ou todas contra `develop` em ordem). + +| branch | commits próprios (resumo) | +|---|---| +| `feat/tacas-smart-seeds` | 3a (sementes), revisão, `provedSafe`, **fix abort → assume**, **fix caminhos descartados** (+ duas correções dele), logs R15/R16/R18 | +| `feat/tacas-2d-slicing` | 2d: slice uma vez por execução (cache `.slice/`), knobs `MAP2CHECK_SLICE_CLEANUP` e `MAP2CHECK_SLICER_FLAGS`, `opt` limitado | +| `feat/tacas-3b-alternation` | fix AFL (zeros após o fim da entrada); 3b `--alternate-engines`; correções da revisão; `migration-schedule.md` atualizado | +| `feat/tacas-memtrack-intrinsics` | fix: `memset/memcpy/memmove` checados no LLVM 16 (despacho por `MemSetInst`/`MemTransferInst`); fix: mensagem de erro de link do AFL++ | +| `feat/tacas-3c-seed-ranking` | 3c v1: entradas `+cov` da fila vão primeiro para o KLEE (spec `2026-09-29-tacas-3c-seed-ranking-design.md`); logs R16-CB/R17/R19 parcial; fix do classificador (segfault do replay do AFL não é ERROR) | +| `feat/tacas-memtrack-strings` | fix: `%s`/`puts` checam a string antes da chamada (o `printf` roda como externa no KLEE → TRUE errado do Juliet CWE193) | +| (3b, depois da R19) | `fix(hybrid): the fuzzer gets all of KLEE's vectors, built once, with growing patience` — as 5 perdas eca-* da alternância | +| `feat/tacas-klee-vector-replay` (acima de fuzzer-suite) | vetores do KLEE executados nativamente com zeros após o fim, depois de cada fase KLEE sem violação (o ganho eca-* do braço seeds, agora explícito e também no híbrido simples) | +| `feat/tacas-fuzzer-suite` | knob `MAP2CHECK_FUZZER_SUITE=1`: o corpus do AFL++ entra na suíte de Cover-Branches (até metade, sem duplicatas) | + +- **Ponta da pilha:** `feat/tacas-3c-seed-ranking` (a R19 e a R17 usam o build de + `8c70e5a73`; a R20 usa `install_r20`, da ponta com o 3c). +- **Testes:** unitários 12/12; integração 46 seções. +- **Specs:** + - `docs/superpowers/specs/2026-09-29-tacas-2d-slicing-optimizations-design.md`; + - `docs/superpowers/specs/2026-09-29-tacas-3b-engine-alternation-design.md`, que inclui + a seção "Revisão". +- **Revisão final (subagente opus):** achados 1–9 tratados. + - 1: o contador "partially completed paths" também conta podas por assunção e impedia + qualquer prova. Corrigido. + - 2–3: KLEE que morreu e "skipping fork". Corrigidos. + - 4–9: suíte de Cover-Branches entre fases, orçamento das fases, SIGINT duplo, paciência + do KLEE e flags. Corrigidos. + +## 2. Correções de veredito desta sessão (todas testadas) + +- **`abort()` do programa vira poda** (`map2check_assume(0)`). Resolveu 6 de 8 TRUE errados + da R15 e também o falso positivo do memtrack no `busybox sleep-3`: o `bb_show_usage()` + chamava `abort()` com `argv` ainda alocado. +- **KLEE que descartou caminhos não é prova.** Os casos são: + - "silently concretizing" (double simbólico: `sin_interpolated_index-1`); + - qualquer `*.err` ou `*.early` (VLA: `insertion_sort-1-2`); + - HaltTimer; + - "skipping fork" ou "over memory cap"; + - `info` sem "done: completed paths" (crash). +- **`nondet_assume` do KLEE usa `klee_silent_exit`.** O `klee_assume(0)` gerava `user.err`. +- **AFL++:** leitura após o fim da entrada devolve 0. Antes ela recomeçava o buffer, o + `while(nondet())` nunca terminava e o `afl-fuzz` abortava no dry run. +- **Memtrack:** intrínsecos de memória do LLVM 16 passaram a ser checados. + +## 3. Resultados já registrados no log + +- **R16 (Cover-Error, sementes 3a × controle R15):** **148 × 129 cobertas** (+15%), pares + 21 × 2. Os 7 TRUE errados vêm dos dois defeitos já corrigidos. +- **R18:** a correção do abort eliminou 6 de 8 TRUE errados. Os 2 restantes eram + caminhos descartados, também corrigidos. + +## 4. Rodadas em execução (dados em `/home/guilherme/github/prism/tacas-results/`) + +- **Build:** `install_r19`, cópia congelada do `build_abort/install` no commit `8c70e5a73` + (registrado em `r19-commit.txt`). +- **R19:** + - Escalonador: `r19-sched.sh`, rodando com `setsid`, log em `r19-sched.log`. Os jobs estão + em `r19-jobs.tsv`, com no máximo 11 contêineres ao mesmo tempo. + - Cover-Error (`r15-ce.tsv`): control, seeds, alternate, slice, slice-light, slice-o2, + slice-ntscd, slice-ptafs, 3 shards cada. + - Cover-Branches (`r15-cb.tsv`): control, seeds, alternate, 2 shards cada. + - Resultados em `R19--_s/results.csv`. + - A primeira tentativa foi descartada (`discarded-r19a/`): o build tinha o contador de + parciais errado e os defeitos da revisão. +- **R17:** + - Escalonador: `r17-sched.sh`, log em `r17-sched.log`. Divide as vagas com a R19. + - SV-COMP MemSafety (50), MemCleanup (10) e NoOverflows (20), 120 s, braços control, + seeds e alternate. + - Manifests `r17-*.tsv`, regenerados com `build_corpus.py` e os mesmos parâmetros da + R9/R13. Os originais se perderam em diretórios temporários. + - Resultados em `R17--/`. +- **R20:** `r20-sched.sh`, que espera a R19 lançar seus 30 jobs. Mede Cover-Error seeds e + alternate com o ranking do 3c (`install_r20`), para comparar com os mesmos braços da R19. +- **R21:** `r21-sched.sh`. MemSafety e MemCleanup (control) e o CASTLE com `install_r21` + (checagem de `%s`), para comparar com a R17 e a R14. Gate: nenhum falso positivo novo. +- **R22:** `r22-sched.sh`, que espera a R19. Cover-Branches control, seeds e alternate + com `MAP2CHECK_FUZZER_SUITE=1` (`install_r23`: o `r22-run.sh` foi reapontado), para + comparar com a R19. +- **R23:** `r23-sched.sh`, que espera a R19. Cover-Error seeds e alternate com o build + final (`install_r23`: ponta `feat/tacas-fuzzer-suite`, com a alternância corrigida — sem + limite na troca KLEE → AFL++, cache dos binários do AFL++, paciência crescente). + Comparar com a R19. A R20 ficou só com o braço seeds, que isola o 3c. +- **R24:** `r24-sched.sh`, que espera a R19. Cover-Error control e seeds com `install_r24` + (ponta `feat/tacas-klee-vector-replay`). Comparar o control com o da R19 (efeito do + replay de vetores) e o seeds com o da R23. +- **Incidente da R19:** o shard 0 do braço seeds tinha 38 linhas do shard 1 e faltavam 42 + tarefas dele. Foi relançado como `r19-ce-seeds-0-resume` (e `control-0-resume` para 2 + faltantes). Na análise, filtrar as linhas pelo índice no manifest (`i % 3 == shard`). +- **R16 Cover-Branches** (`r16-cb-seeds-*`, build antigo) terminando; comparar com a R15. + +**Análise pendente:** +- **Cover-Error:** cobertas, TRUE errado e pares discordantes de cada braço contra o + control. Gate: TRUE errado = 0. +- **Cover-Branches:** cobertura média. +- **R17:** correct-true, correct-false, wrong-true, wrong-false. + - Um wrong-true bloqueia o braço. + - Contar TRUE corretos, porque a parada por estagnação pode custar provas. +- **2d:** promover o vencedor entre light, o2, ntscd e ptafs a padrão, com commit próprio. +- **3b:** promover `--alternate-engines` a padrão do híbrido se ele ganhar de seeds. + +## 4b. Estado em 2026-09-29, noite + +- **Resultados já no log:** R19 (Cover-Error e Cover-Branches) e R21. + - Cover-Error: seeds +23 −0 contra o control; alternate +20 −0. + - Cover-Branches: alternate 50,3% contra 44,7%. + - TRUE errado 0 em todos os braços. +- **Correções da noite:** + - fd 3 do harness fechado para os filhos; + - varredura do IR sem regex (2d); + - orçamento único para as 3 compilações do AFL++ (3b); + - checagem de `%s` atrás de `MAP2CHECK_CHECK_CSTRINGS=1`, por falso positivo em Juliet + good. + - A ponta passou na integração 50/50. +- **Knobs de slicing:** nenhum promovido (as variantes ficaram em ±3). +- **Na fila** (8 vagas, reduzidas por falta de memória): R20, R21-castle, R22, R23, R24 + (e o shard `r24-ce-control-0-resume`). As rodadas usam installs anteriores às correções + da noite. Isso só afeta slice em programas enormes e o harness, que foi corrigido no repo + e vale para contêineres novos. + +- **R22 control relançado** (`r22-cb-control-*-rerun`): a primeira tentativa deu ERROR nas + 120 tarefas ("cannot create std::vector larger than max_size()", input ilegível no hash) + durante o pico de falta de memória; os dados foram para `discarded-r22a/`. O hash agora + falha com mensagem clara (`fix(frontend): an unreadable input program...`). + +## 4c. Próxima frente, por decisão do usuário: a lacuna Crab-LLVM → Clam + +Depois de fechar a campanha atual e **antes das outras lacunas** (floats, memória não +inicializada, busca dirigida). O ponto de partida: +- O motor antigo era a cadeia de forks `hbgit/crab-llvm` (branch `dev-llvm-6.0`), com + `hbgit/crab`, `hbgit/sea-dsa` e `hbgit/llvm-dsa`. Os commits públicos do hbgit nesses + forks são só de porte e build para o LLVM 6. As especializações de que o usuário lembra + não aparecem ali; **perguntar onde estão**. +- O release do SV-COMP 2020 (`v7.3.1`, `map2check-rc-v7.3-svcomp20.zip`) traz o motor + compilado em `bin/crabllvm`, com Apron (domínios `oct` e `pk`). O domínio padrão era + `zones`. +- No Clam `dev16` do `Dockerfile.dev`, o padrão também é `zones`, mas nem Apron, nem Elina, + nem LDD, nem PPLite são compilados: `oct`, `pk` e `boxes` ficam indisponíveis. O + comentário do Dockerfile que fala em "intervalos" está errado. +- O `--add-invariants` sobre o Clam **nunca foi medido** (o gate previsto é CASTLE e Juliet + sem perder detecção). +- **Sonda de 2026-09-29, num programa com laço.** O motor do v7.3.1 roda em + `python:2.7-slim` com o clang do LLVM 6 que vem no próprio release. + - As flags do v7.3.1, tiradas das strings do binário, incluem `--crab-promote-assume`: + **17 invariantes emitidos como `llvm.assume`**. + - O Clam, com as flags atuais, emite **18 como `verifier.assume`**, que o NonDetPass + converte em `klee_assume`. + - O NonDetPass antigo só reconhecia `verifier.assume`, e o **KLEE ignora `llvm.assume`** + (testado no 3.1). Então, no v7.3.1, os invariantes **não chegavam ao KLEE como + restrição**. Se ajudavam, era pelo otimizador do LLVM, que dobra ramos com base em + `llvm.assume`. O mecanismo é outro, e é provavelmente isso que "não é a mesma coisa" + quer dizer. + - Os dois motores produzem fatos no estilo de zones (`x − y ≤ c`). +- **INV-1 feito** (log de experimentos). Os invariantes estavam inertes desde a v7.3 + (out/2018). O ganho observado vinha do pré-processamento em SSA, não dos invariantes. + Branch `feat/tacas-invariants`: + - `MAP2CHECK_CLAM_PROFILE=default|memory|none`; + - `MAP2CHECK_PREOPT=ssa`, só para alcançabilidade e assert; + - build `build_inv` com `-DENABLE_CLAM=ON` e os links `lib/klee/runtime` e `lib/clang` + criados à mão. +- **R25 na fila** (`r25-sched.sh`, `install_r25`): + - Cover-Error, shard 0 (71 tarefas): off, ssa, clam-none, clam-default, clam-memory; + - MemSafety (50): off, clam-none, clam-default, clam-memory. + - Gate: nenhuma detecção perdida. +- Primeiro passo (feito, ver INV-1): um **inventário diferencial**. Rodar o motor do v7.3.1 e o Clam `dev16` + nos mesmos programas e comparar os invariantes, antes de portar qualquer coisa. + +## 5. Depois das rodadas + +1. Registrar R17 e R19 no log. +2. Promover os knobs vencedores. +3. Push das 4 branches e PRs em cadeia, sem merge, com os números na descrição. +4. **3c:** ranking de sementes (novidade de cobertura, densidade SDG). +5. **Ideia anotada:** usar o corpus do AFL++ como casos de Cover-Branches, via replay + tipado. Hoje a suíte de CB sai só do KLEE. +6. **Perda de 2026-09-29:** o `release/results/map2check_castle.2026-07-17_04-53-54.results.sv-comp19_map2check.txt` + foi apagado por engano e não tem cópia. Regera-se com `tests/castle/run_castle_benchexec.sh`. + `release/` foi restaurado a partir de `install_v15/`. +7. O worktree velho `../Map2Check-2c` precisa de `--force` para ser removido. **Pedir + permissão** antes. + +## 6. Campanha completa da 9.0 (lançada em 2026-09-30, 14h16) + +- **Lançador:** `../tacas-results/v9-campaign.sh`, rodando com `setsid`, log em + `../tacas-results/v9-campaign.log`. Ele espera o R26 terminar e roda sozinho, na ordem + do plano: CASTLE, Cover-Error (1087, 3 shards), Juliet (grupos a–d, como a v15) e + Cover-Branches (2765, 6 shards). +- **Build:** `install_v9`, cópia congelada da ponta de `feat/map2check-9.0` + (`v9-commit.txt`). Um commit de código novo antes do merge exige rodar de novo a parte + afetada. +- **Imagem:** `map2check-v9-eval:latest`, que é a `map2check-dev:aflpp` com o TestCov. +- **Condições da v15:** `--memory=4g`, `--cpus=2` (Test-Comp) e `--cpus=1` (Juliet e + CASTLE), 300 s, `PER_FAMILY=10`; no máximo 5 contêineres. +- **Resultados:** `../tacas-results/V9-*`, pareados com `tests/*/results_v15*`. diff --git a/docs/reports/2026-09-30-plano-campanha-completa.md b/docs/reports/2026-09-30-plano-campanha-completa.md new file mode 100644 index 000000000..487633a04 --- /dev/null +++ b/docs/reports/2026-09-30-plano-campanha-completa.md @@ -0,0 +1,66 @@ +# Plano da campanha completa pós-merge (Map2Check 9.0) + +**Objetivo:** medir a 9.0 no **mesmo recorte da campanha v15** (relatório +`docs/Map2Check-Relatorio-v15.docx`), com a configuração padrão da 9.0, para uma +comparação pareada tarefa a tarefa. É a base do artigo e da decisão de release. + +## O que roda + +**Um braço só:** a configuração padrão da 9.0, que é o híbrido alternado com troca de +sementes e o corpus do fuzzer nas suítes de Cover-Branches. Os braços alternativos +(`--fixed-hybrid`, `--slice`, knobs) já foram medidos nas amostras (R15 a R26) e não +entram. A v15 **não roda de novo**: os resultados dela estão em `tests/*/results_v15*` +e o pareamento é feito pelo programa. + +| corpus | tarefas | manifest | custo médio por tarefa* | horas-vaga | +|---|---|---|---|---| +| Test-Comp Cover-Error | 1 087 | `tests/testcomp/corpus/cover-error-q400.tsv` (o recorte da v15) | ~85 s + TestCov ≈ 110 s | ~33 | +| Test-Comp Cover-Branches | 2 765 (o mesmo recorte da v15, confirmado) | `tests/testcomp/corpus/cover-branches-q400.tsv` | ~240 s + TestCov ≈ 300 s | ~230 | +| Juliet (escopo C) | ~8 000 | `tests/juliet` (os 4 shards da v15) | ~36 s | ~80 | +| CASTLE | 250 (119 em escopo) | `tests/castle` | ~60 s | ~2 | +| SV-COMP MemSafety, MemCleanup e NoOverflows | por categoria, a decidir | `build_corpus.py` | ~36 s | depende | + +\* medido nas rodadas R17, R19 e R26 com 300 s (Test-Comp) e 120 s (SV-COMP). + +## Capacidade e duração + +- Máquina: 16 núcleos, 23 GB. Com **no máximo 5 contêineres** a memória não fica crítica + (com 8 ela ficou; ver `docs/backlog.md`, limite de memória do KLEE). +- Duração, com 5 vagas: + - Cover-Error: ~7 h; + - Juliet: ~16 h; + - Cover-Branches: ~2 dias (2 765 tarefas); + - CASTLE e SV-COMP por categoria: algumas horas. + - Total: **~3,5 dias**. +- Ordem sugerida, das decisões mais baratas para as mais caras: + 1. CASTLE; + 2. Cover-Error; + 3. SV-COMP; + 4. Juliet; + 5. Cover-Branches. + +## Regras da execução + +- **Build:** a tag da 9.0 depois do merge, com o install congelado (copiado) antes do + início, como nas rodadas R19 a R26. +- **Escalonador fora do repositório** (decisão do projeto). Ele precisa: + - usar `-` em vez de campo vazio na lista de jobs (o bash junta tabs consecutivos); + - retomar pelo CSV; + - separar os shards por índice do manifest. +- **Validação de cada lote antes de seguir:** + - nenhuma tarefa com ERROR em massa, que é sinal de problema de infraestrutura; + - contar as tarefas com "did not finish its run" (KLEE morto por falta de memória) e + repeti-las. +- **Registro:** cada corpus concluído entra em `docs/reports/tacas-experiment-log.md`, + comparado à v15 com: + - cobertas e TRUE errado (Cover-Error); + - cobertura média (Cover-Branches); + - TP, FN, TN e FP (Juliet e CASTLE); + - correct e wrong (SV-COMP). + +## Critérios de aceite para a release + +- TRUE errado = 0 em Cover-Error e nenhum wrong-true novo no SV-COMP. +- Cover-Error e Cover-Branches: não piores que a v15 no pareado (a amostra aponta + +46 cobertas em 213). +- CASTLE e Juliet: FP não maiores que os da v15, e FN iguais ou menores. diff --git a/docs/reports/tacas-experiment-log.md b/docs/reports/tacas-experiment-log.md index adbed7c00..a015deb86 100644 --- a/docs/reports/tacas-experiment-log.md +++ b/docs/reports/tacas-experiment-log.md @@ -286,3 +286,451 @@ classificador contava todo FALSE nelas como errado (corrigido: "any"). - **Leitura:** com o build final, o slicing de memória fica **34 × 33 corretos** e **1 × 2 TRUE errados** contra o controle nesta amostra — ligeiramente melhor, e sem nenhum erro novo atribuível à fatia. + +## R15 — amostra Test-Comp: tacasv2 (develop) × v15, Cover-Error (2026-09-28) + +- **Config:** build da `develop` depois do merge de #69/#68/#70/#71; `build_corpus.py + --property cover-error --per-category 20` (213 tarefas, **todas pareadas** com a + campanha v15 — amostragem aninhada), 300 s, TestCov 300 s, 3 shards por braço. + Controle = híbrido sem slice (tacasv1 + correções); slice = `--slice`. + +| braço | cobertas | TRUE errado | FALSE errado | tempo mediano | +|---|---|---|---|---| +| v15 controle | 111 | **27** | 0 | 43 s | +| v15 slice | 108 | 15 | 0 | — | +| **R15 controle** | **129** | **5** | 0 | **5 s** | +| R15 slice | 126 | 4 | 0 | 7 s | + +- **Controle × v15:** +18 cobertas (+16%); pares discordantes 20 × 2 (só R15 × só v15). + Por categoria (v15 → R15): ProductLines 14 → 20, Loops 13 → 16, Arrays 15 → 18, + ECA 2 → 5, Sequentialized 0 → 2; Heap 19 → 18 (única perda). +- **TRUE errado 27 → 5:** a correção "KLEE parado pelo timer não é prova" confirmada em + escala — a v15 respondia TRUE em 27 de 212 tarefas com bug. +- **Slice × controle:** 126 × 129 (pares discordantes 3 × 6) — empate técnico, leve + desvantagem. TRUE errado 4 × 5: o slice elimina 2 (`pals_lcr…`) e introduz 2 + (`float-benchs/cast_union_tight.c`, `loops/insertion_sort-1-2.c`); 4 ERROR (ECA, + ~330 s, sem suíte) só no slice. +- **Em aberto:** os 4–5 TRUE errados restantes (`seq-mthreaded/pals_*`, + `float-benchs/sin_interpolated_index-1.c`, e os 2 do slice) e os 4 ERROR do slice. + +### R15 — Cover-Branches, controle × v15 (mesma rodada) + +- 120 tarefas (10 por categoria), todas pareadas com a v15; só o braço controle (o + slicing não atua em Cover-Branches). +- **Cobertura média: v15 48,0% × R15 47,7%** — neutra. Melhor em 6 tarefas, pior em 3, + igual em 111. Recursive 51,9 → 45,0% (a única queda relevante); XCSP 74,2 → 77,7%. +- Validação do TestCov mais limpa: VALIDATED 116 (v15: 107), VALIDATED_ABORTS 3 (v15: 10), + TESTCOV_ERROR 1 (v15: 3). Tempo mediano 183 × 195 s. +- **Leitura:** o AFL++ não muda a cobertura de ramos nesta amostra; o ganho da tacasv2 + está no Cover-Error. + +## R18 — validação da correção do abort() nos TRUE errados da R15 (2026-09-29) + +- **Config:** `build_abort` (commit 1eb8a30b9), 300 s, as tarefas com TRUE errado da R15: + 6 no braço controle (sem slice), 2 no braço slice (`--slice`). Manifests + `tacas-results/r18-{ctrl,slice}.tsv`. + +| tarefa | braço | R15 | R18 | +|---|---|---|---| +| pals_lcr.4.1 | controle | TRUE errado | FAILED/COVERED (83 s) | +| pals_lcr-var-start-time.4.2 | controle | TRUE errado | FAILED/COVERED (175 s) | +| pals_STARTPALS_Triplicated.1 | controle | TRUE errado | FAILED/COVERED (9 s) | +| pals_floodmax.3.1 | controle | TRUE errado (R16) | FAILED/COVERED (24 s) | +| pals_floodmax.3.4 | controle | TRUE errado | UNKNOWN (256 s) | +| sin_interpolated_index-1 | controle | TRUE errado | **TRUE errado** (59 s) | +| cast_union_tight | slice | TRUE errado | FAILED/COVERED (1 s) | +| insertion_sort-1-2 | slice | TRUE errado | **TRUE errado** (3 s) | + +- **Leitura:** 6 de 8 TRUE errados eliminados (5 viraram FAILED coberto, 1 UNKNOWN). + `cast_union_tight` também era abort inline, não defeito do slice. Restam 2 com causa + diferente: `sin_interpolated_index-1` (controle) e `insertion_sort-1-2` (slice) — investigar. + +### R18 — causa dos 2 TRUE errados restantes (2026-09-29) + +Reproduzidos à mão (`build_abort`, 300 s). **Causa comum:** o KLEE sai com 0 quando a fila +esvazia, e o frontend lia isso como exploração completa — mas nos dois casos ele tinha +**descartado caminhos**: + +- `sin_interpolated_index-1` (controle): `silently concretizing (reason: floating point) + expression (ReadLSB w64 0 non_det_double) to value 0` — o KLEE 3.1 não tem double + simbólico; 1 caminho, "completo", TRUE. +- `insertion_sort-1-2` (slice): o VLA `int v[SIZE]` gerou `concretized symbolic size` e + `null page access` — 2 estados mortos por erros do próprio KLEE (`partially completed + paths = 2` no `info`), TRUE. + +**Correção:** `kleeDroppedPaths()` generaliza o `kleeHaltedOnTimer`: HaltTimer, qualquer +"silently concretizing" em `warnings.txt`, ou `partially completed paths > 0` → a execução +é tratada como timeout (violação registrada vale; senão UNKNOWN). Revalidação: `sin` → **FAILED** numa execução e UNKNOWN noutra (o AFL++ da fase 1 acha ou +não o 180.0; sem `--seed-exchange` não há fase 3 — a frase anterior dizia o contrário e +estava errada), `insertion_sort` --slice → **UNKNOWN**. Nunca TRUE. Integração 40/40 (§30 nova: double concretizado; vermelha no +`build_seeds`, verde no novo). Uma §31 (abort dentro do `assert` da libc) foi descartada: +passava também no binário antigo — esse caminho não gera TRUE errado. + +**Custo esperado:** programas com float/VLA que o KLEE "provava" passam a UNKNOWN. Medir +TRUE corretos no SV-COMP (R17) — é o preço da solidez. + +## R16 — `--seed-exchange` (3a) × controle R15, Cover-Error (2026-09-29) + +- **Config:** `build_seeds` (3a + revisão, **sem** as correções do abort e dos caminhos + descartados — mesma base de veredito que o controle R15), `--seed-exchange`, amostra + `r15-ce.tsv` (213, todas pareadas), 300 s, 3 shards. + +| braço | cobertas | TRUE errado | ERROR | tempo mediano | +|---|---|---|---|---| +| R15 controle | 129 | 5 | 0 | 5 s | +| **R16 seeds** | **148** | 7 | 0 | 6 s | + +- **+19 cobertas (+15%)**, pares discordantes **21 × 2**. Por categoria (controle → seeds): + Sequentialized 2 → 8, XCSP 7 → 13, ECA 5 → 8, Recursive 7 → 9, ControlFlow 3 → 4, + BitVectors 7 → 8; as demais iguais. Perdas: 2 ECA (`Problem13_label54`, + `Problem10_label12`). +- **TRUE errado 7:** todos da família `pals_*` (abort inline) e `sin_interpolated_index-1` + (double concretizado) — os dois defeitos que esta branch já corrige (1eb8a30b9, + 4c16013bc). O braço seeds expõe mais deles porque a fase 3 do AFL++ não roda depois de + uma "prova" do KLEE. +- **Leitura:** a troca de sementes é o maior ganho medido na linha TACAS até aqui. A + rodada limpa (R19, build final nos dois braços) confirma sem os TRUE errados. +- Cover-Branches do R16 ainda rodando. + +### Correção da correção — poda por assunção não é caminho descartado (2026-09-29) + +A primeira versão do `kleeDroppedPaths` lia `partially completed paths > 0` no `info`. Esse +contador inclui os caminhos **podados por assunção**: `klee_assume(0)` num caminho já falso +é um erro do KLEE (`user.err`, "invalid klee_assume call (provably false)"), e até +`klee_silent_exit` conta como parcial (medido num programa mínimo: os dois dão +`partially completed paths = 1`). Resultado: **nenhum programa com `assume_abort_if_not` +ou abort inline podia mais ser provado** — o §29 `safe.c` ia de TRUE para UNKNOWN. + +Correção: `nondet_assume` (KLEE) poda com `klee_silent_exit(0)`, que não deixa arquivo; e +os caminhos descartados passam a ser lidos pelo que cada estado morto deixa no disco — +qualquer `*.err` ou `*.early` —, além do HaltTimer e do "silently concretizing". O §29 +agora exige TRUE. `sin` e `insertion_sort` seguem sem TRUE errado (UNKNOWN; o segundo por +`ptr.err`). + +**Efeito na R19:** o `install_r19` tem a versão com o contador. Em Test-Comp isso não muda +a cobertura (o veredito não pontua), só impede o `provedSafe` de encerrar a execução mais +cedo em programas com assunções. A R17 (SV-COMP, onde TRUE pontua) precisa do build +corrigido. + +### R16 — Cover-Branches, `--seed-exchange` × controle R15 (2026-09-29) + +- Mesma config da R16 Cover-Error (`build_seeds`), amostra `r15-cb.tsv` (120, pareadas). +- **Cobertura média: controle 47,7% × seeds 49,7%** (+2,0 p.p.); melhor em 26 tarefas, pior + em 9. Tempo mediano 195 → 160 s. +- Por categoria (controle → seeds): ControlFlow 41,3 → 57,9, BitVectors 65,7 → 73,7, + Recursive 45,0 → 53,0; **Loops 67,1 → 60,8** (uma tarefa: `geo2-ll_unwindbound50` + −62,5 p.p.), XCSP 77,7 → 75,0 (`AllInterval-011` −27 p.p.). +- TestCov: VALIDATED 118 (R15: 116), VALIDATED_ABORTS 1 (3). +- **Leitura:** diferente da tacasv2 (neutra em CB), a troca de sementes melhora a cobertura + de ramos, apesar de a suíte de CB sair só do KLEE — o KLEE semeado explora ramos que o + controle não alcançava. As duas quedas grandes ficam para a R19 confirmar (ruído do + fuzzer × efeito real). + +## R17 — SV-COMP MemSafety/MemCleanup/NoOverflows, control × seeds × alternate (2026-09-29) + +- **Config:** `install_r19` (commit 8c70e5a73), manifests regenerados com `build_corpus.py` + (memsafety 10/categoria = 50, memcleanup 10, overflow 10/categoria = 20), 120 s. + +| memsafety (50) | correct-true | correct-false | wrong-true | wrong-false | unknown | error | +|---|---|---|---|---|---|---| +| control | 10 | 19 | 2 | 3 | 10 | 6 | +| seeds | 10 | 20 | 1 | 3 | 10 | 6 | +| alternate | 9 | 20 | 1 | 3 | 10 | 7 | + +- MemCleanup (10): control 6 corretos, seeds 6, alternate 6. NoOverflows (20): control e + seeds 2 correct-true + 17 unknown; alternate idem (2 + 17 + 1 error) — os três iguais. +- **wrong-true comum aos três:** `CWE121…CWE193_char_declare_cpy_07_bad`. Causa: o modelo + `ldv_strcpy` copia `strlen` bytes (sem o terminador) e o estouro real é a **leitura** em + `printf("%s")` — que o KLEE executa como **chamada externa** (a uClibc do KLEE declara + `printf` sem defini-lo: `calling external: printf(...)`), fora de qualquer checagem, e o + memtrack não confere argumentos `%s`. Lacuna de solidez pré-existente; correção em + aberto: checar a string de cada `%s` (e `puts`/`str*`) antes da chamada. +- **wrong-true só no control:** `CWE122…CWE129_rand_18_bad` — os braços com sementes o + acham (FALSE correto). +- **Os 6 `error` são do classificador, não da ferramenta:** as tarefas + `array-memsafety/*-alloca` têm `alloca` de tamanho não determinístico; o AFL++ acha um + crash (pilha estourada), o replay imprime "Segmentation fault", e + `verdict_classifier.sh` conta isso como falha — embora o Map2Check termine com UNKNOWN + (o KLEE concretiza o tamanho → `model.err` → caminho descartado). +- **Leitura:** as sementes não pioram nada em SV-COMP e ganham 1 FALSE e eliminam 1 TRUE + errado; a alternância perde 1 TRUE correto frente ao control (a estagnação corta o KLEE + — o preço previsto na revisão). + +## R19 — Test-Comp, parcial (2026-09-29) + +- **Cover-Error, 171 tarefas pareadas nos 4 braços principais** (o shard 0 do braço seeds + perdeu 42 tarefas por um incidente de escrita e está sendo completado): + +| braço | cobertas | TRUE errado | ERROR | tempo mediano | +|---|---|---|---|---| +| R15 control (referência) | 101 | 5 | 0 | 6 s | +| control | 101 | **0** | 0 | 3 s | +| **seeds** | **120** | 0 | 0 | 5 s | +| alternate | 118 | 0 | 0 | 14 s | +| slice | 102 | 0 | 2 | 4 s | + +- seeds × control: **+20 −1**; alternate × control: +17 −0; alternate × seeds: +4 −6; + slice × control: +3 −2. +- **TRUE errado zerado em todos os braços** (eram 5 no control R15): as correções do abort e + dos caminhos descartados confirmadas em escala. +- Braços slice-light/o2/ntscd/ptafs e Cover-Branches ainda rodando. + +### R19 — diagnóstico das perdas de `--alternate-engines` (2026-09-29) + +Contra o braço seeds, a alternância perde 6 e ganha 2; 5 das perdas são eca-*. Reproduzido +em `eca-rers2012/Problem06_label05.c` (300 s): + +- **A troca KLEE → AFL++ estava limitada** aos 64 vetores mais recentes do KLEE. No braço + seeds, a fase 3 do AFL++ recebe todos (4676), e o dry run dela encontra vetores que, + completados com zeros depois do fim, chegam ao `reach_error` (`sig:06`, crashes com + `op:dry_run`). É isso que cobre essas tarefas eca-* que o KLEE sozinho deixa UNKNOWN. + O limite descartava justamente esses vetores. Ele tinha vindo de um laço cuja calibração + nunca terminava, problema já resolvido com a leitura de zeros. +- **Cada fase do AFL++ recompilava os 3 binários:** ~24 s por fase em eca-*. +- **A estagnação fixa de 15 s cortava o AFL++ em ~17 s**, onde o híbrido fixo dava 60 s. + +**Correção** (`fix(hybrid): the fuzzer gets all of KLEE's vectors, built once, with growing +patience`): sem limite na troca, cache dos binários por execução (`.build/`, também +beneficia a fase 3 do braço seeds) e paciência do AFL++ dobrando por rodada. +`Problem06_label05`: UNKNOWN → **FAILED em 157 s** (seeds: 281 s). Remedição na R23. + +## R19 — resultado (2026-09-29) + +**Cover-Error, 213 tarefas** (linhas filtradas pelo shard; os shards afetados pelo incidente +do descritor 3 foram completados com `-resume`): + +| braço | cobertas | % | TRUE errado | ERROR | vs control | tempo mediano | +|---|---|---|---|---|---|---| +| control | 128 | 60,1 | 0 | 0 | — | 3 s | +| **seeds** | **151** | **70,9** | 0 | 0 | **+23 −0** | 5 s | +| alternate | 148 | 69,5 | 0 | 0 | +20 −0 | 9 s | +| slice | 128 | 60,1 | 0 | 4 | +3 −3 | 4 s | +| slice-light | 127 | 59,6 | 0 | 4 | +3 −4 | 4 s | +| slice-o2 (207) | 128 | 61,8 | 0 | 4 | +5 −3 | 4 s | +| slice-ntscd (181, parcial) | 113 | 62,4 | 0 | 4 | +2 −1 | 5 s | +| slice-ptafs (155, parcial) | 90 | 58,1 | 0 | 4 | +1 −3 | 5 s | + +- **TRUE errado 0 em todos os braços** (R15 control: 5). As correções de veredito se + confirmam em escala. +- **Sementes: +23 −0** contra o control, o melhor resultado da linha TACAS. Alternância: + +20 −0. As 5 perdas eca-* dela frente ao seeds têm causa achada e corrigida (ver o + diagnóstico acima); a remedição fica para a R23. +- **Slicing:** as variantes não mudam o quadro (±3). Nenhuma supera o slice simples com + margem, e nenhum knob é promovido por enquanto. Os 4 ERROR de ECA continuam: o cache do + 2d eliminou o refatiamento, mas o passo do slice ainda levava 105 s (regex sobre o IR, + ~45 s fora de qualquer orçamento) e as 3 compilações do AFL++ somavam até 0,75T. + Correções: varredura sem regex e um orçamento único para as compilações. + `Problem102_label34` com `--slice`: ERROR → UNKNOWN em 307 s. + +**Cover-Branches, 120 tarefas:** + +| braço | cobertura média | melhor / pior que o control | +|---|---|---| +| control | 44,7% | — | +| seeds | 46,1% | 31 / 13 | +| **alternate** | **50,3%** (119) | **43 / 5** | + +- **A alternância é o melhor braço em Cover-Branches** (+5,6 p.p.), o que se explica pelas + várias fases do KLEE, cada uma alimentada pelo corpus do fuzzer. O control da R19 (44,7%) + ficou abaixo do da R15 (47,7%) na mesma amostra. A carga da máquina foi maior (11 + contêineres e falta de memória no fim), e isso pesa em Cover-Branches, que usa o + orçamento inteiro. + +## R21 — checagem de `%s` e correção do classificador, SV-COMP (2026-09-29) + +- `install_r21`, control, contra a R17 control. + - **MemSafety:** o CWE193 cpy bad foi de TRUE errado para **FALSE correto**. Os 6 + `error` das tarefas alloca viraram `unknown` (classificador corrigido). + - **Falso positivo novo:** `CWE121…dest_char_declare_cpy_01_good` foi de TRUE correto + para FALSE-DEREF errado. O `ldv_strcpy` do SV-COMP copia `strlen` bytes sem o + terminador, e o terminador do buffer da versão good é um byte **não inicializado**: + para o gabarito do SV-COMP ele é zero; numa execução nativa ou no KLEE (que preenche + `alloca` com um padrão diferente de zero) não é. + - **MemCleanup:** os 2 `error` viraram `unknown`. +- **Decisão:** a checagem de `%s` fica atrás de `MAP2CHECK_CHECK_CSTRINGS=1`, desligada + por padrão, até ser medida numa amostra maior do Juliet (1 acerto × 1 erro em 50 não + basta; pelos pesos do SV-COMP compensaria, mas não com essa amostra). +- **Incidente de harness (descritor 3):** o laço do harness lê o manifest pelo fd 3, e os + filhos o herdavam, inclusive o programa analisado via chamadas externas do KLEE. O offset + andou sob o laço: o shard 0 da R24 parou em 29 de 71, e o shard 0 do seeds da R19 recebeu + linhas do shard 1. Os filhos agora rodam com o fd 3 fechado. + +## INV-1 — `--add-invariants`: crab-llvm antigo × Clam (2026-09-30) + +**Pergunta:** o `--add-invariants` do crab-llvm "funcionava", e o do Clam "não é a mesma +coisa"? + +**O que se descobriu sobre o motor antigo** (release v7.3.1 do SV-COMP 2020, que roda em +`python:2.7-slim` com o clang do LLVM 6 embutido): +- Houve **duas configurações**. + - Até 18/10/2018: `--crab-track=arr --crab-add-invariants=after-load`. Os invariantes + saíam como `verifier.assume`, o NonDetPass os mapeava para `map2check_crab_assume`, e + eles chegavam ao KLEE como `klee_assume`. + - A partir da v7.3 (SV-COMP 2019 e 2020): `--crab-track=num + --crab-add-invariants=block-entry --crab-promote-assume`. O `promote` emite + `llvm.assume`, que o NonDetPass não mapeia e que o KLEE ignora (testado no KLEE 2.1 do + release e no 3.1, com e sem `--optimize`). **Os invariantes das versões de competição + não chegavam a lugar nenhum.** + +**Geração, 90 programas** (40 de alcançabilidade da amostra Cover-Error e 50 de MemSafety), +timeout de 60 s: + +| config | rodou | com invariante | total | +|---|---|---|---| +| OLD-A (antigo, até 2018) | 76 | 14 | 155 | +| OLD-B (antigo, v7.3; `llvm.assume`, inerte) | 35 | 33 | 224 698 | +| NEW-cur (Clam, `num` + `block-entry`) | 79 | 68 | 72 452 | +| NEW-A (Clam, `mem` + `after-load`) | 70 | 19 | 702 | + +- A configuração que "funcionava" insere **poucos** invariantes, depois de leituras de + memória. A atual do Clam insere **muitos**, na entrada de cada bloco. O perfil + `memory` do Clam reproduz a ordem de grandeza da antiga. + +**Efeito na análise, sonda num laço** (`n ≤ 1000`, versões segura e com bug em `n == 777`, +symex, 60 s): + +| braço | seguro | com bug | +|---|---|---| +| sem `--add-invariants` | UNKNOWN (HaltTimer) | UNKNOWN | +| Clam padrão (18 invariantes) | UNKNOWN | UNKNOWN | +| Clam `memory` (0 invariantes) | **TRUE** | **FAILED** | +| Clam `none` (pipeline do Clam, 0 invariantes) | **TRUE** | **FAILED** | +| **sem Clam, `MAP2CHECK_PREOPT=ssa`** | **TRUE** | **FAILED** | + +- **O ganho vem do pré-processamento, não dos invariantes.** O Clam compila com + `-disable-O0-optnone` e deixa o módulo em SSA (`mem2reg`, `simplifycfg`). O Map2Check + compila em `-O0` com `optnone`, cada variável local vira um objeto de memória no KLEE, e + o laço não fecha no orçamento. +- Os 18 invariantes do perfil padrão não bastaram: o KLEE completou mais caminhos com eles + (261 contra 184 sem), mas também parou no HaltTimer. +- **Hipótese a medir em escala (R25):** `MAP2CHECK_PREOPT=ssa` (sem Clam) é um ganho + geral, e os invariantes só se pagam somados ao SSA, se se pagarem. +- Implementado nesta frente (`feat/tacas-invariants`): + - `MAP2CHECK_CLAM_PROFILE=default|memory|none`; + - log com a contagem de invariantes inseridos; + - recuo para a compilação normal quando o Clam falha (antes, o pipeline ficava sem + bitcode); + - `MAP2CHECK_PREOPT=ssa`. + +## R20, R22, R23, R24 — primeiros resultados (2026-09-30, madrugada) + +Todos contra o braço equivalente da R19, nas tarefas em comum (linhas filtradas por shard). + +| rodada | mudança medida | tarefas | cobertas (nova × R19) | +/− | TRUE errado | +|---|---|---|---|---|---| +| **R24 control** (completa) | replay dos vetores do KLEE, híbrido **sem** sementes | 213 | **146 × 128** | **+20 −2** | 0 | +| R24 seeds (parcial) | replay + sementes | 59 | 47 × 46 | +1 −0 | 0 | +| R20 seeds (parcial) | ranking `+cov` (3c) | 178 | 128 × 128 | +2 −2 | 0 | +| R23 seeds (parcial) | build final (cache do AFL++, orçamento, fd 3) | 177 | 132 × 128 | +5 −1 | 0 | + +- **O replay dos vetores do KLEE traz o híbrido simples para perto do braço com sementes** + (146 contra 151 da R19 seeds). As mudanças concentram-se em `pals_*`, eca-*, XCSP (`aim-*`, + `CostasArray`, `AllInterval`) e `fuzzle`, justamente as tarefas em que o seeds ganhava + com o dry run do AFL++. O mecanismo diagnosticado se confirma. +- **3c v1 (ranking):** neutro nesta amostra (+2 −2). O ranking só pesa quando a fila passa + de 64 entradas. +- **Cover-Branches, R22** (corpus do AFL++ na suíte, `MAP2CHECK_FUZZER_SUITE=1`): + - control, 99 tarefas: **49,2% × 44,8%**, 33 melhores e 2 piores; TestCov VALIDATED + 97/99; + - seeds, 22 tarefas: 48,5% × 44,8%, 4 melhores e 3 piores. + +## R21 CASTLE e dois incidentes (2026-09-30, madrugada) + +- **CASTLE com `install_r21`** (checagem de `%s` ainda **ligada** nesse build): TP 54, TN 44, + FN 12, UNKNOWN 5, **FP 4** (R14: TP 53, TN 44, FN 14, FP 1). Os 4 FP (787-1, 787-2, + 787-4, 822-3) são todos um `printf("%s")` de memória que o runtime não rastreia: buffer + preenchido por `scanf` e `argv[0]`. É uma confirmação independente de que + `MAP2CHECK_CHECK_CSTRINGS` deve continuar **desligado** (como está no branch da PR); os + FN caíram de 14 para 12. +- **Incidente do escalonador** (corrige uma conclusão anterior): os escalonadores leem os + jobs com `IFS=$'\t' read`, e o bash junta tabs consecutivos. Com a coluna de flags vazia, + o conteúdo da coluna de ambiente escorregava para a de flags. Com isso: + - o braço `ssa` da R25 passou `MAP2CHECK_PREOPT=ssa` ao Map2Check como **nome de + arquivo** (71/71 ERROR). Relançado com `-e`; + - **a primeira R22 control (120 ERROR) teve a mesma causa, e não falta de memória**, + como registrado antes. O relançamento dela usou `-e` e é válido; + - os outros braços têm flags não vazias ou nenhuma variável, e não foram afetados. + +### R20 e R23 seeds, completas (2026-09-30, 01h) + +| rodada | o que muda | cobertas (213) | vs R19 seeds (151) | vs R19 control (128) | TRUE errado | +|---|---|---|---|---|---| +| R20 seeds | + ranking `+cov` (3c v1) | 150 | +2 −3 | +22 | 0 | +| **R23 seeds** | build final (cache do AFL++, fd 3, hash, orçamento) | **154** | **+5 −2** | **+26** | 0 | + +- **3c v1 é neutro** também na amostra completa: fica disponível, sem ganho medido. +- **O build final com sementes é o melhor resultado de Cover-Error da linha: 154/213 + (72,3%)**, contra 111 da v15 na mesma amostra. +- As perdas recorrentes (`Problem10_label12`, `Problem13_label54`) aparecem também no + R20. São tarefas eca-* no limite do orçamento. + +## Madrugada de 2026-09-30 — R22, R23, R24 e R25 completas + +**Cover-Error, 213 tarefas** (referência: R19 control, 128): + +| braço | cobertas | % | vs R19 control | TRUE errado | tempo mediano | +|---|---|---|---|---|---| +| R24 control (replay dos vetores do KLEE) | 146 | 68,5 | +20 −2 | 0 | 4 s | +| R23 seeds (build final) | 154 | 72,3 | +26 −0 | 0 | 4 s | +| **R24 seeds (build final + replay)** | **155** | **72,8** | **+27 −0** | 0 | 5 s | +| R23 alternate (build final) | 153 | 71,8 | +26 −1 | 0 | 12 s | + +- R23 alternate × R19 alternate: +7 −2. A correção das perdas eca-* funcionou. + R23 alternate × R23 seeds: +4 −5, um empate. +- **v15 → build final na mesma amostra: 111 → 155 cobertas, TRUE errado 27 → 0.** + +**Cover-Branches, 120 tarefas** (R19 control 44,7%): + +| braço | cobertura média | melhor / pior | +|---|---|---| +| R19 seeds | 46,1% | 31 / 13 | +| **R19 alternate** | **50,6%** | 44 / 5 | +| R22 control + corpus do AFL++ | 49,7% | 40 / 3 | +| R22 seeds + corpus do AFL++ | 49,4% | 36 / 8 | + +**R25 (`--add-invariants` e SSA), shard 0 de Cover-Error (71 tarefas) e MemSafety (50):** + +| braço | Cover-Error cobertas | ERROR | MemSafety (corretas / wrong-true / wrong-false) | +|---|---|---|---| +| off | 51 | 0 | 28 / 2 / 2 | +| ssa | 50 (+2 −3) | 0 | — | +| clam-none | 50 (+1 −2) | 2 | 25 / 1 / 4 | +| clam-default | 49 (+1 −3) | 4 | 27 / 1 / 4 | +| clam-memory | 44 (+2 −9) | 7 | 25 / 2 / 4 | + +- **No híbrido, nem o SSA nem os invariantes ajudam.** O ganho que a sonda viu era do KLEE + sozinho; no híbrido, o AFL++ e o replay dos vetores já decidem essas tarefas. Os braços + com Clam **pioram**: mais FALSE errados em MemSafety (4 contra 2), e ERROR por o Clam + estourar o orçamento, já corrigido com um limite de 0,2T. +- **Decisão:** `--add-invariants` continua opcional e desligado por padrão; o SSA não é + promovido. +- **Incidente:** a mudança de versão no `CMakeLists.txt` fez o cache do `build_inv` ser + regenerado, com o prefixo voltando para `release/` e o `ENABLE_CLAM` para OFF. O + `release/` foi sobrescrito de novo e restaurado a partir do `install_v15` (idêntico, + conferido com `diff`). As rodadas usaram installs congelados antes disso. + +## R26 completa (2026-09-30) e primeiros lotes da campanha da 9.0 + +**R26, SV-COMP (120 s):** a alternância **não perde nenhum TRUE correto**. + +| | control (fixo) | seeds | alternate | +|---|---|---|---| +| MemSafety (50): correct-true / correct-false | 10 / 19 | 10 / 20 | **10 / 20** | +| MemSafety: wrong-true / wrong-false | 2 / 3 | 1 / 3 | **1 / 3** | +| MemCleanup (10): corretos | 6 | 6 | 6 | +| NoOverflows (20): corretos | 2 | 2 | 2 | + +As sementes e a alternância corrigem o TRUE errado do `CWE122…rand_18`. O seeds teve 1 +ERROR (`tricky_address2`). + +**CASTLE:** R26 e a campanha da 9.0 dão TP 54, TN 44, FN 14, FP 1, **igual à v15**; os 4 +TIMEOUT da v15 viraram UNKNOWN. + +**Campanha da 9.0, parcial** (`install_v9` = `3476ff769`; condições da v15: 4 GB, 300 s): + +| corpus | pareado com a v15 | v15 | 9.0 | +|---|---|---|---| +| Cover-Error (q400) | 532 de 1087 | 288 cobertas, **57 TRUE errados** | **394 cobertas (+112 −6), 0 TRUE errado**; mediana 59 → 19 s | +| Juliet, grupos a e b | 2 271 | TP 340, FN 118, FP 20, TN 1074, ERROR 114 | **TP 776**, FN 90, FP 20, TN 1058, ERROR 0 | + +- Juliet: 294 UNKNOWN e 102 ERROR da v15 viraram TP; 16 TN viraram UNKNOWN. diff --git a/docs/superpowers/plans/2026-09-28-tacasv3a-smart-seeds-plumbing.md b/docs/superpowers/plans/2026-09-28-tacasv3a-smart-seeds-plumbing.md new file mode 100644 index 000000000..f3b801e2d --- /dev/null +++ b/docs/superpowers/plans/2026-09-28-tacasv3a-smart-seeds-plumbing.md @@ -0,0 +1,145 @@ +# tacasv3a — Smart seeds plumbing: Implementation Plan + +> **For agentic workers:** REQUIRED SUB-SKILL: Use superpowers:subagent-driven-development (recommended) or superpowers:executing-plans to implement this plan task-by-task. Steps use checkbox (`- [ ]`) syntax for tracking. + +**Goal:** make `--seed-exchange` actually move seeds between AFL++ and KLEE, across the hybrid's three phases. + +**Architecture:** +- **Seed store.** A persistent directory `/.seeds/` next to the scratch directory, with `afl/`, `ktest/` and `replay/` subdirectories. +- **KLEE → AFL++.** KLEE vectors go to `afl/`, and the AFL++ phase uses `afl/` as its `-i`. +- **AFL++ → KLEE.** The AFL++ queue is replayed through the witness binary inside `replay/`, and the typed nondet log becomes one `.ktest` per entry in `ktest/`. KLEE then runs with `--seed-dir`. +- **Budget.** 0.2 / 0.6 / 0.2 when the exchange is on. +- **Cleanup.** The store is removed after the last phase unless `--debug`. +- **Where the code lives.** Pure selection logic goes into `modules/frontend/utils/seed_store.hpp`; the rest goes in `Caller` and `map2check.cpp`. + +**Tech Stack:** C++17, GTest, bash integration tests, Docker dev image `map2check-dev:aflpp`. Use build dir `build_aflpp` (prefix pinned to `/workspace/build_aflpp/install`) and `build_aflpp_ut` (ENABLE_TEST). Rebuild `build_aflpp` only after R15 has finished, because it is using that install. + +**Spec:** `docs/superpowers/specs/2026-09-28-tacasv3a-smart-seeds-plumbing-design.md` + +## Global Constraints + +- **Store path:** `/.seeds`, absolute, with subdirectories `afl/`, `ktest/` and `replay/`. It exists only with `--seed-exchange`. +- **Queue replay:** at most 64 entries, in queue id order, each with a 2 s cap, run inside `replay/`. Empty or duplicate vectors are skipped. +- **KLEE seeding flags:** `--seed-dir=/ktest --allow-seed-extension --allow-seed-truncation --seed-time=s`, added only when `ktest/` has a file. +- **Budget with the exchange:** KLEE `min(0.6T, remaining−5)`. Without the exchange nothing changes (0.8T). +- **Log lines:** `Seeded KLEE with N vectors from AFL++` and `Seeded the fuzzer corpus with M vectors from KLEE`. +- **Default behaviour is unchanged** without `--seed-exchange`. +- Every mini-round is logged in `docs/reports/tacas-experiment-log.md`. + +## Review Focus + +- **A crash found by AFL++ must survive the queue replays.** Replays run in `replay/`, never in the phase directory. Pinned by integration test (2). +- **A run without `--debug` leaves no `*.seeds/` directory**, including when a phase errors out. Pinned by (3). +- **A queue entry whose replay hangs** is capped at 2 s. The `timeout` is covered by the code path; no dedicated test. +- **KLEE given seeds whose object sizes differ from its own** must not abort. The extension and truncation flags cover this, and it is exercised by (1). + +--- + +### Task 1: `seed_store.hpp` (pure) + unit tests + +**Files:** +- Create: `modules/frontend/utils/seed_store.hpp` and `tests/unit/frontend/SeedStoreTest.cpp`. +- Modify: `tests/unit/frontend/CMakeLists.txt`. + +**Produces:** +- `std::string Map2Check::seedStorePath(const std::string& cwd, const std::string& programHash)` returns `cwd + "/" + programHash + ".seeds"`. +- `std::vector Map2Check::selectQueueEntries(std::vector names, size_t cap)` keeps only names starting with `id:`, sorts them lexicographically (which is id order, because AFL++ zero-pads), and truncates to `cap`. +- `bool Map2Check::isNewVector(const std::vector& bytes, std::set>* seen)` returns false for an empty vector or one already in `seen`; otherwise it inserts the vector and returns true. + +- [ ] **Step 1:** Write the tests below in `SeedStoreTest.cpp`, and register it in CMake the same way as `SlicerTest` (`add_executable(SeedStoreTest SeedStoreTest.cpp)` + `map2check_test(SeedStoreTest)`). + +```cpp +#include + +#include +#include +#include + +#include "../../../modules/frontend/utils/seed_store.hpp" + +// Next to the scratch directory, not inside it: every hybrid phase recreates +// the scratch directory, and a store inside it never reached the next phase. +TEST(SeedStorePath, SitsBesideTheScratchDirectory) { + EXPECT_EQ(Map2Check::seedStorePath("/work", "abc.map2check"), + "/work/abc.map2check.seeds"); +} + +TEST(SelectQueueEntries, KeepsOnlyQueueEntriesInIdOrderUpToTheCap) { + const std::vector names = { + "id:000002,src:000000,time:9", ".state", "README.txt", + "id:000000,time:0,execs:0,orig:seed", "id:000001,src:000000,time:5"}; + const std::vector chosen = + Map2Check::selectQueueEntries(names, 2); + ASSERT_EQ(chosen.size(), 2u); + EXPECT_EQ(chosen[0], "id:000000,time:0,execs:0,orig:seed"); + EXPECT_EQ(chosen[1], "id:000001,src:000000,time:5"); +} + +TEST(IsNewVector, RejectsEmptyAndDuplicateVectors) { + std::set> seen; + EXPECT_FALSE(Map2Check::isNewVector({}, &seen)); + EXPECT_TRUE(Map2Check::isNewVector({1, 2}, &seen)); + EXPECT_FALSE(Map2Check::isNewVector({1, 2}, &seen)); + EXPECT_TRUE(Map2Check::isNewVector({1, 3}, &seen)); +} +``` + +- [ ] **Step 2:** Run `ninja SeedStoreTest` in `build_aflpp_ut`. Expected: FAIL, header not found. +- [ ] **Step 3:** Implement the header: `#include `, namespace `Map2Check`, the three inline functions exactly as specified, and a doc comment on each. +- [ ] **Step 4:** Run the test binary. Expected: `[ PASSED ] 3 tests.`, and ctest 100%. +- [ ] **Step 5: Commit** `feat(tacasv3a): pure seed-store helpers`. + +### Task 2: Store, KLEE → AFL++, budget and cleanup + +**Files:** `modules/frontend/caller.hpp`, `modules/frontend/caller.cpp`, `modules/frontend/map2check.cpp`, `tests/integration/test_testcomp_regressions.sh` (section 11). + +**Produces:** +- The member `std::string seedStore;` (absolute), set in the `Caller` constructor from `seedStorePath(currentPath, programHash)`. +- The accessor `const std::string& seedStorePath() const`. + +- [ ] **Step 1: Failing tests.** In section 11 of the integration script: + - Replace the `n_off` check with: after the run without the flag, `ls -d "$WORK/seed"/*.seeds 2>/dev/null | wc -l` must be 0. + - Replace the `n_on` count with: after the `--seed-exchange --debug` run, count files in `"$WORK"/seed/*.seeds/afl/` whose names start with `klee-`. It must be > 0, and the log must contain `Seeded the fuzzer corpus with`. + - Add a run of the same program with `--seed-exchange` **without** `--debug`. Afterwards `ls -d "$WORK/seed"/*.seeds` must be empty (`ok "no seed store is left behind without --debug"`). + + Run the suite. Expected: the `*.seeds` checks FAIL, because the store does not exist yet. +- [ ] **Step 2: Implement.** + - Set `seedStore` in the constructor, right after `currentPath` is set. + - `exportKleeVectorsAsSeeds` writes to `seedStore + "/afl"` (`create_directories`). + - In the AFL++ branch, `inputDir` is `seedStore + "/afl"` when `seedExchange`, otherwise `"afl-in"`. The queue copy-back writes to `seedStore + "/afl/afl-" + name`. + - KLEE budget: `const double kleeShare = this->seedExchange ? 0.6 : 0.8;` replaces the literal `0.8`. + - Remove `exportFuzzerVectorAsKtest` and its `--seed-file` use. Task 3 replaces it. + - In `map2check.cpp`, keep the store path from the last `map2check_execution`: a file-scope `std::string lastSeedStore` assigned from `caller->seedStorePath()`. After the hybrid phase sequence in `main`, when `args.seedExchange && !args.debugMode`, call `std::filesystem::remove_all(lastSeedStore, ec)`. + - Remove `Caller::seedDirectory` if nothing else uses it. +- [ ] **Step 3:** Rebuild (after R15) and run the suite plus ctest. Expected: section 11 passes, and everything else is unchanged. +- [ ] **Step 4: Commit** `feat(tacasv3a): a seed store that survives the hybrid's phases`. + +### Task 3: AFL++ → KLEE by replay, and KLEE `--seed-dir` + +**Files:** `modules/frontend/caller.hpp`, `modules/frontend/caller.cpp`, `tests/integration/test_testcomp_regressions.sh`. + +**Produces:** `unsigned Caller::exportFuzzerCorpusAsKtests();` (private). It returns the number of `.ktest` files written. + +- [ ] **Step 1: Failing tests.** Add section 26, "seeds reach KLEE", and section 27, "a crash survives the replays": + - **26:** `seed.c` from section 11, run with `--seed-exchange --debug`. The log must contain `Seeded KLEE with N vectors from AFL++` with N > 0 (grep the number), and the KLEE command line (debug) must contain `--seed-dir=`. + - **27:** the program `int x = nondet(); if (x > 1000 && x < 1100) reach_error();` (AFL++ finds it quickly thanks to CmpLog/interesting values), run with `--seed-exchange --target-function --target-function-name reach_error --timeout 30`. It must report `VERIFICATION FAILED`. + + Run them. Expected: 26 FAILS (no such line); 27 passes (a regression guard; ledger it). +- [ ] **Step 2: Implement** `exportFuzzerCorpusAsKtests()`, called at the end of the AFL++ branch when `seedExchange && !isWitnessFileCreated()`: + - List `afl-out/default/queue`, then `selectQueueEntries(names, 64)`. + - For each entry: + - clear `replay/` (`remove_all` + `create_directories`); + - run `cd && timeout -k 1 2 /-witness-fuzzed.out < '' > /dev/null 2>&1`; + - read `readNonDetLogAsObjects(/klee_log.csv)`; + - skip it if the objects are empty or if `ktestToFuzzerBytes(objects)` is not new according to `isNewVector`; + - otherwise `writeKtestFile(/ktest/afl-.ktest, objects)`. + - Log `Seeded KLEE with N vectors from AFL++` when N > 0. +- [ ] **Step 3: KLEE flags.** In the KLEE branch, when `seedExchange` and `/ktest` holds any regular file, append ` --seed-dir=/ktest --allow-seed-extension --allow-seed-truncation --seed-time=s` where `seedFlag` used to go (both command variants). +- [ ] **Step 4:** Rebuild and run the suite plus ctest. Expected: 26 and 27 pass, and everything else is unchanged. +- [ ] **Step 5: Commit** `feat(tacasv3a): the fuzzer corpus reaches KLEE as typed seeds`. + +### Task 4: Mini-rounds + +- [ ] **R16, Test-Comp:** the R15 manifests (`r15-ce.tsv`, `r15-cb.tsv`), 300 s, `EXTRA_FLAGS=--seed-exchange` (GENERATOR hybrid). Compare against the R15 control arm (same tasks, same code without the exchange). Report coverage, N and M per task (grep the `Seeded` lines from raw logs, or run a sample with `--debug`), and the median time. +- [ ] **R17, SV-COMP:** MemSafety and NoOverflows from the R14 manifests, plus a ReachSafety sample (`build_corpus.py` has no reachsafety property; use `--property cover-error`'s task list with `--target-function` via `run_testcomp_evaluation.sh`'s verdict column, or skip ReachSafety and note it). 120 s, with and without `--seed-exchange`. Report correct and wrong answers per arm. +- [ ] **Log R16–R17** with comparisons, and commit. diff --git a/docs/superpowers/specs/2026-09-28-tacasv3a-smart-seeds-plumbing-design.md b/docs/superpowers/specs/2026-09-28-tacasv3a-smart-seeds-plumbing-design.md new file mode 100644 index 000000000..7ef0a0c66 --- /dev/null +++ b/docs/superpowers/specs/2026-09-28-tacasv3a-smart-seeds-plumbing-design.md @@ -0,0 +1,137 @@ +# tacasv3a — Smart seeds, parte 1: o encanamento da troca AFL++ ↔ KLEE + +**Data:** 2026-09-28 +**Branch:** `feat/tacas-smart-seeds` (a partir de `develop`, que já tem a tacasv2) +**Baseline:** tacasv2 com `--seed-exchange` desligado (o híbrido default) +**Status:** rascunho — aguardando revisão +**Linha:** `decisions/tacas-afl-slicing-roadmap.md` (ai-memory); Fase 3.3 do +`docs/migration-schedule.md`. Registro de rodadas: `docs/reports/tacas-experiment-log.md`. + +--- + +## 1. Objetivo + +Fazer a troca de sementes entre os motores **acontecer de verdade** e medir o efeito. A +v15 mediu "sem ganho" com o `--seed-exchange`, mas, como a seção 2 mostra, as sementes +praticamente nunca chegavam ao outro motor. Esta etapa conserta o encanamento; o laço +alternado com detecção de estagnação (3b) e a priorização das sementes (3c) vêm depois, +cada uma com spec e medição próprios. + +**Métrica de sucesso** (decidida com o usuário): Test-Comp — tarefas cobertas no +Cover-Error e cobertura média no Cover-Branches — **e** vereditos de propriedades do +SV-COMP (MemSafety, NoOverflows, ReachSafety), sempre contra a tacasv2 sem a troca, no +mesmo corpus e no mesmo build. + +--- + +## 2. Diagnóstico do `--seed-exchange` atual + +| # | Defeito | Onde | +|---|---|---| +| 1 | As sementes não atravessam fases: cada fase cria um `Caller` que apaga o diretório de trabalho, e `seeds/` mora dentro dele | `Caller::Caller` (`rm -rf `), `Caller::seedDirectory` | +| 2 | Fuzzer → KLEE lê o `klee_log.csv` do diretório **atual**, que acabou de ser recriado vazio; e mandaria um vetor só | `exportFuzzerVectorAsKtest` | +| 3 | O corpus do AFL++ nunca chega ao KLEE, embora o KLEE aceite um diretório de sementes | idem | +| 4 | A terceira fase (KLEE → AFL++) quase não roda: o KLEE usa até 0,8× o orçamento e sobram segundos | `map2check.cpp` (fase 3) e orçamentos em `executeAnalysis` | + +--- + +## 3. Design + +### 3.1 Armazém de sementes persistente + +- Diretório `/.seeds/`, **ao lado** do diretório de trabalho (não dentro + dele), criado na primeira fase e reaproveitado pelas seguintes: + - `afl/` — entradas para o `-i` do AFL++ (vetores do KLEE convertidos em bytes, mais o + corpus que o próprio AFL++ descobriu); + - `ktest/` — sementes para o `--seed-dir` do KLEE; + - `replay/` — diretório isolado onde as entradas do AFL++ são reexecutadas. +- Removido pelo `main` depois da última fase, salvo em `--debug`. +- Só existe com `--seed-exchange`. Sem a flag, nada muda em relação à tacasv2. + +### 3.2 Fuzzer → KLEE: conversão por replay + +Ao fim da fase AFL++ (sem violação encontrada): + +1. Para cada entrada de `afl-out/default/queue/` (em ordem de id, até **64**): + - roda o binário de witness **dentro de `replay/`**, com a entrada no stdin e teto de + 2 s. Em `replay/` os arquivos que o runtime grava (`map2check_property`, + `klee_log.csv`, …) não tocam o diretório da fase — um replay não pode sobrescrever + uma violação já registrada; + - lê o `replay/klee_log.csv` com `readNonDetLogAsObjects` e grava + `ktest/afl-.ktest` com `writeKtestFile`; apaga o log antes da próxima entrada; + - descarta vetores vazios e duplicados (mesmos bytes). +2. Registra `Seeded KLEE with N vectors from AFL++`. + +Na fase KLEE, com `ktest/` não vazio: +`--seed-dir=/ktest --allow-seed-extension --allow-seed-truncation --seed-time=<¼ do orçamento do KLEE>`. +O `--seed-time` impede que reproduzir sementes consuma a fase inteira. + +### 3.3 KLEE → fuzzer + +- `exportKleeVectorsAsSeeds` passa a gravar em `/afl/` (hoje grava em `seeds/`, + que é apagado). A fase AFL++ usa `/afl/` como `-i`. +- A cópia do corpus do AFL++ de volta ao armazém (hoje em `seeds/`) passa a gravar em + `/afl/`. + +### 3.4 Orçamento com a troca ligada + +- AFL++ **0,2**, KLEE **0,6**, AFL++ **0,2** do orçamento (hoje 0,2 / até 0,8 / o que sobrar). +- Sem `--seed-exchange`: inalterado (0,2 / 0,8), para a tacasv2 continuar medindo o mesmo. + +### 3.5 O que fica igual + +- O default continua **sem** troca. Promover a troca a default é decisão para depois da + medição. +- Nenhuma mudança nos motores, na instrumentação ou no slicing. + +--- + +## 4. Referência comparada + +| Aspecto | FuSeBMC v4 | tacasv3a | Por quê | +|---|---|---|---| +| Direção | fuzzer ↔ BMC, alternado | AFL++ → KLEE → AFL++ | O laço alternado é o 3b | +| Formato | seeds do fuzzer usados pelo BMC via "smart seeds" | replay no binário de witness para obter o vetor tipado | O KLEE precisa de um objeto por leitura nondet; o runtime já registra os tipos | +| Priorização | por cobertura | ordem de id, teto 64 | Ranking é o 3c | + +--- + +## 5. Testes + +Integração (`test_testcomp_regressions.sh`, seção de seed exchange): + +1. **As sementes atravessam fases.** Programa em que o AFL++ acha caminhos e o KLEE + resolve uma guarda (a mesma `seed.c` da seção 11): com `--seed-exchange --debug`, o log + tem `Seeded KLEE with N vectors from AFL++` com N > 0 **e** + `Seeded the fuzzer corpus with M vectors from KLEE` com M > 0, e o armazém `.seeds/` + existe ao lado do diretório de trabalho. +2. **O replay não sobrescreve uma violação.** Programa em que o próprio AFL++ acha o bug: + com `--seed-exchange`, o veredito continua FAILED. +3. **Sem `--debug`, nada fica para trás.** Depois do run, não existe `*.seeds/` no diretório. +4. **Sem a flag, nada muda.** Nenhum `*.seeds/` e nenhuma linha `Seeded` (atualiza a + seção 11, que hoje olha `seeds/` dentro do diretório de trabalho). + +Unitário: a lógica pura — seleção das entradas da fila (ordem, teto, deduplicação por +bytes) e o nome do armazém — em funções testáveis sem os motores. + +--- + +## 6. Avaliação (mini-rodadas, registradas no log) + +- **Test-Comp:** o manifesto da R15 (Cover-Error 213, Cover-Branches 120), 300 s, braço + `--seed-exchange` contra o controle da R15 (mesmo build, sem a troca). +- **SV-COMP:** amostras de MemSafety e NoOverflows da R14 (e uma de ReachSafety, com o + mesmo `build_corpus.py`), com e sem `--seed-exchange`, 120 s. +- Métricas: tarefas cobertas e cobertura de ramos; corretos, **wrong-true/wrong-false**; + N e M (sementes trocadas por tarefa) para confirmar que a troca aconteceu. + +--- + +## 7. Riscos + +| Risco | Mitigação | +|---|---| +| Replay de 64 entradas custa tempo | Teto de 2 s por entrada; binário já compilado; medir o custo por tarefa | +| Semente do AFL++ com vetor que não corresponde aos objetos do KLEE (tamanho/ordem) | `--allow-seed-extension/--allow-seed-truncation`; o vetor vem do mesmo runtime que o KLEE usa | +| KLEE gasta a fase reproduzindo sementes | `--seed-time` = ¼ do orçamento do KLEE | +| Mudar o orçamento (0,2/0,6/0,2) muda o efeito junto com a troca | Só com `--seed-exchange`; a medição compara contra o controle 0,2/0,8, e o efeito é o do pacote | diff --git a/docs/superpowers/specs/2026-09-29-tacas-2d-slicing-optimizations-design.md b/docs/superpowers/specs/2026-09-29-tacas-2d-slicing-optimizations-design.md new file mode 100644 index 000000000..67fa73dbe --- /dev/null +++ b/docs/superpowers/specs/2026-09-29-tacas-2d-slicing-optimizations-design.md @@ -0,0 +1,103 @@ +# tacas 2d — otimizações do slicing (design) + +**Data:** 2026-09-29 · **Branch:** `feat/tacas-2d-slicing` (a partir de `feat/tacas-smart-seeds`) +**Aprovação:** o usuário delegou as decisões ("você tem permissão para fazer as decisões +que quiser") e pediu as abordagens recomendadas no brainstorming de 2026-09-29. + +## Objetivo + +Hoje o `--slice` só empata com o controle: 126 × 129 cobertas na R15 Cover-Error. Além +disso, ele tem 4 ERROR próprios (ECA). O objetivo é que ele passe a ganhar, sem nenhum +TRUE errado. + +## Evidência que orienta o desenho + +- **Os 4 ERROR de ECA** (`Problem08_label51`, `Problem102_label34`, `Problem102_label02`, + `Problem103_label44`) seguem o mesmo roteiro: + - o `sbt-slicer` estoura seu limite (0,2T = 60 s) na fase 1; + - a fase 2 recria o `Caller` e **tenta fatiar de novo**, perdendo mais 60 s; + - o processo passa do orçamento e o harness o mata aos 330 s, sem suíte. +- **Cada fase refatia do zero.** Numa tarefa em que o slicer funciona, isso custa o tempo + do slicer uma vez por fase (2× no híbrido, 3× com `--seed-exchange`). +- **O dg deixa blocos vazios e funções mortas no `.bc` fatiado.** Nenhuma limpeza roda + depois da fatia. + +## Desenho + +### 1. Fatiar uma vez por execução (cache do slice) + +- **Onde fica:** um diretório `/.slice/` ao lado do scratch, no mesmo + esquema do store de sementes, porque o scratch é recriado a cada fase. +- **Chave:** um hash (FNV-1a 64 bits, em hex) do **conteúdo do `.bc` de entrada**, somado + ao rótulo dos critérios, à função de entrada e às flags extras do slicer. Chavear pelo + conteúdo, e não pelo número da fase, garante que só se reaproveita a fatia de uma + entrada idêntica. +- **O que se guarda:** + - `.bc`: a fatia pronta, depois da limpeza (item 2); + - `.failed`: marca que o slicer falhou ou estourou o tempo. Com ela, as fases + seguintes vão direto para o programa inteiro, sem gastar o slicer de novo. +- **Consulta:** acontece em `Caller::runSlicer`. + - Um acerto copia a fatia e registra "reusing the slice from an earlier phase". + - Uma falha registrada devolve `false` com o aviso de sempre, acrescido de "(cached)". +- **Ciclo de vida:** o mesmo do store. + - O diretório é apagado no início da execução (fase ≤ 1). + - O guarda de escopo de `main` o remove no fim, exceto com `--debug`. + - O guarda passa a cuidar dos dois diretórios, o de sementes e o de slice. + - Só existe com `--slice`. + +### 2. Limpeza depois da fatia (experimental) + +- **Knob de ambiente:** `MAP2CHECK_SLICE_CLEANUP`, com os valores: + - `none` (padrão até a medição); + - `light`: `opt -passes='function(simplifycfg,dce),globaldce'`; + - `o2`: `opt -O2`. +- **Onde roda:** dentro de `runSlicer`, depois de uma fatia bem-sucedida e antes de ela + entrar no cache. +- **Se o `opt` falhar,** a fatia fica sem limpeza e a execução avisa. +- **Risco do `o2`:** ele explora comportamento indefinido e pode apagar laços sem efeito + colateral. Isso muda a alcançabilidade. Por isso é só um braço de experimento, e o + gate de TRUE errado = 0 decide. +- **Depois da medição,** o vencedor vira o padrão (commit separado). + +### 3. Parâmetros do dg (experimental) + +- **Knob de ambiente:** `MAP2CHECK_SLICER_FLAGS`, anexado sem alteração à linha do + `sbt-slicer`. Os braços medidos são `--cda=ntscd` e `--pta=fs`. +- **Entra na chave do cache.** +- **Depois da medição,** o vencedor vira o padrão (commit separado). + +### Fora do escopo + +- **Cutoff-diverging consertado:** risco alto (é a causa do "Broken module"). Só entra + se 1–3 não fecharem a diferença. +- **Cache dos demais artefatos** (binário do AFL++, `.bc` do KLEE): compilar e instrumentar + custa segundos. Fica para o 3b, se as rodadas extras mostrarem esse custo. + +## Testes + +- **Unitários** (`SlicerTest.cpp`), sobre `sliceCacheKey`: + - é determinística; + - muda com o conteúdo, com o rótulo, com a entrada e com as flags. +- **Integração, seção nova:** + - o programa VLA da seção 20, rodado no híbrido com `--slice`, mostra o aviso de falha + do slicer uma vez por "slicer run" (debug) e depois "(cached)"; + - um programa fatiável roda o `sbt-slicer` uma vez só e as fases seguintes registram + "reusing the slice". +- **Suíte existente:** 40/40, e ctest. + +## Medição: rodada R19, amostra `r15-ce.tsv`, 300 s + +A mesma rodada R19 mede também o 3b; ver o spec do 3b. + +| braço | build | flags / env | +|---|---|---| +| controle | final | — | +| slice | final | `--slice` | +| slice-light | final | `--slice`, `MAP2CHECK_SLICE_CLEANUP=light` | +| slice-o2 | final | `--slice`, `MAP2CHECK_SLICE_CLEANUP=o2` | +| slice-ntscd | final | `--slice`, `MAP2CHECK_SLICER_FLAGS=--cda=ntscd` | +| slice-ptafs | final | `--slice`, `MAP2CHECK_SLICER_FLAGS=--pta=fs` | + +- **Gate:** TRUE errado = 0 em todo braço promovido. +- **Critério de promoção:** mais cobertas que o `slice` puro, com pares discordantes a + favor. diff --git a/docs/superpowers/specs/2026-09-29-tacas-3b-engine-alternation-design.md b/docs/superpowers/specs/2026-09-29-tacas-3b-engine-alternation-design.md new file mode 100644 index 000000000..bfaae49e2 --- /dev/null +++ b/docs/superpowers/specs/2026-09-29-tacas-3b-engine-alternation-design.md @@ -0,0 +1,150 @@ +# tacas 3b — alternância de engines com detecção de estagnação (design) + +**Data:** 2026-09-29 +**Branch:** `feat/tacas-3b-alternation`, a partir de `feat/tacas-2d-slicing` +**Aprovação:** o usuário delegou as decisões e pediu a abordagem recomendada no +brainstorming de 2026-09-29, a opção A: sinais nativos de estagnação com polling. + +## Objetivo + +Hoje o híbrido com `--seed-exchange` reparte o orçamento de forma fixa: +- AFL++ com 0,2T; +- KLEE com 0,6T; +- AFL++ com 0,2T. + +Isso tem dois custos: +- uma engine estagnada segura o orçamento até o fim da sua cota; +- uma engine que ainda progride é cortada no meio. + +O 3b troca de engine **quando a atual estagna**, em rodadas, até: +- achar a violação; +- provar a propriedade; +- acabar o tempo. + +## Desenho + +### Laço de rodadas (em `main`) + +A flag nova é `--alternate-engines`. Ela implica `--seed-exchange` e só vale no híbrido. +O laço alterna AFL++ e KLEE, começando pelo AFL++, com `args.phase = 1, 2, 3, …`: + +``` +janela(engine, rodada r) = min(restante, base(engine) * 2^(r-1)) + base(AFL++) = 0,1T base(KLEE) = 0,3T +para cada fase: + roda a engine com teto = janela e parada por estagnação (abaixo) + pára o laço se: violação | provedSafe | restante < max(10 s, 0,05T) +``` + +**Por que as janelas dobram:** a mesma engine volta com mais tempo quando a alternância +não resolveu. Uma engine que estagna cedo devolve o tempo que sobrou na hora. + +**Quem alimenta o KLEE:** toda fase AFL++ seguida de uma fase KLEE alimenta o KLEE +(`feedsKleePhase`). O corte é que, se o que resta não comporta outra fase, ela não +alimenta. + +**O que o KLEE recebe de semente:** +- o corpus do AFL++, como hoje; +- os `.ktest` da rodada KLEE anterior. Assim o KLEE reconstrói depressa a fronteira + que já tinha alcançado, em vez de redescobri-la. + +**O que o AFL++ recebe:** o `store/afl` já acumula a fila do AFL++ e os vetores do KLEE, +então nada muda. + +**Seleção das entradas da fila (`selectQueueEntries`):** passa a **pular as sementes com +que o fuzzer começou** (entradas `,orig:`): são vetores do KLEE ou de rodadas anteriores, +que o KLEE já tem. O `store/ktest` é limpo a cada exportação, porque os `.ktest` da rodada +KLEE anterior (`kleeprev/`) carregam o que ela já explorou. (A primeira versão deste spec +previa um `store/exported.txt`; o efeito é o mesmo com menos estado.) + +**Sem limite na troca KLEE → AFL++:** todos os vetores do KLEE vão para o fuzzer. +Completados com zeros depois do fim, alguns caminhos parciais do KLEE chegam ao erro no +dry run do AFL++, e é assim que o híbrido fixo cobre tarefas eca-* que o próprio KLEE deixa +UNKNOWN. Uma primeira versão limitava a exportação aos 64 vetores mais recentes (e o corpus +a 256). Isso custou 5 tarefas eca-* na R19 e foi removido. A calibração ficou barata depois +que o gerador do AFL++ passou a devolver zeros no fim da entrada. + +**Binários do AFL++ compilados uma vez por execução** (cache `.build/`, chaveado +pelo conteúdo dos módulos): em eca-* cada fase do fuzzer gastava ~24 s recompilando. + +**Paciência do AFL++ também dobra por rodada:** com o corte fixo de 15 s, os turnos do +fuzzer em eca-* acabavam em ~17 s, onde o híbrido fixo dava 60 s. + +### Estagnação + +- **AFL++:** `AFL_EXIT_ON_TIME=S`. O próprio fuzzer sai com 0 quando passa S segundos sem + cobertura nova. O `timeout` externo continua sendo o teto da janela. +- **KLEE:** o frontend lança o KLEE em uma thread (`system`, como hoje, com o PID do + `timeout` gravado em `klee.pid`) e faz polling do `klee-out-0/run.stats` a cada 2 s, + lendo `CoveredInstructions` da última linha pela API do SQLite, em modo somente leitura. + - Se o valor fica S segundos sem subir, o frontend manda SIGINT ao `timeout`, que o + repassa ao KLEE. + - O KLEE para de forma limpa: grava os testes dos estados que já terminaram. + - A fase é marcada como **incompleta** (`gotTimeout`). A execução nunca vira TRUE + por isso. +- **Valor de S:** `max(10 s, 0,05T)`, que dá 15 s em T = 300, para o AFL++. Para o KLEE, + S dobra a cada rodada dele: a cobertura de instruções para de subir bem antes de o KLEE + terminar os caminhos que formam uma prova, e um corte fixo nunca o deixaria chegar lá. +- **Sem SQLite:** o SQLite é uma dependência opcional, via `find_package(SQLite3)`. Sem + ele, a estagnação do KLEE fica desligada e vale só o teto da janela. O CI, que não + instala `libsqlite3-dev`, continua compilando. + +### Correção necessária: numeração da suíte + +`TestSuiteWriter` numera os casos a partir de 1 em cada fase (`testcase-1.xml`, …). Com +mais de uma fase KLEE em Cover-Branches, **uma rodada sobrescreveria a anterior**. O +contador passa a começar depois do maior `testcase-N.xml` que já existir no diretório. + +### Revisão (2026-09-29), incorporada + +- **Orçamento:** cada fase mede o próprio tempo de preparação (compilar, instrumentar, + linkar), que nenhuma janela conta. Uma fase só começa se sobrar `S + preparação`, e a + janela desconta a preparação. O AFL++ guarda 5 s de reserva, como o KLEE. +- **SIGINT:** vai direto ao PID do KLEE, filho do `timeout`. Mandado ao `timeout`, ele + repassava ao filho e ao grupo, o KLEE recebia dois sinais e perdia o despejo dos estados + vivos. +- **Suíte de Cover-Branches:** o limite de 50 casos vale para a suíte, não para cada fase, + e vetores repetidos entre fases são pulados. A suíte começa vazia a cada execução, o que + evita somar casos de uma execução anterior no mesmo diretório. +- **Flag:** sem `--timeout`, ou com `--nondet-generator`, `--alternate-engines` avisa e + não se aplica. + +## Fora do escopo + +- **Transformar o corpus do AFL++ em casos de teste de Cover-Branches.** Hoje a suíte de + CB sai só dos `.ktest` do KLEE. É um bom candidato, porque o replay tipado já existe, + mas é uma mudança de outra natureza e fica para depois. +- **Priorização das sementes (3c).** + +## Testes + +- **Unitários:** + - `SeedStoreTest`: a seleção pula nomes já exportados; + - `alternationWindow(engine, rodada, T, restante)`: janelas dobram e respeitam o + restante; + - `stagnationSeconds(T)`; + - `TestSuiteWriter`: o contador continua a partir de um diretório existente. +- **Integração, seções novas:** + - **Várias fases numa execução só:** um programa em que o AFL++ estagna (guarda de + igualdade de 32 bits que o CmpLog não resolve), rodado com `--alternate-engines`, + registra mais de uma fase e termina dentro do orçamento, sem TRUE. + - **Numeração da suíte:** um diretório com `testcase-1.xml` recebe o próximo caso como + `testcase-2.xml`. + - **Estagnação do KLEE:** um programa com laço infinito de estados, a 60 s, mostra o + aviso "KLEE stagnated" antes do teto e o veredito não é TRUE. + +## Medição (R19, a mesma rodada do 2d) + +Braços a comparar, todos com o build final: + +| braço | flags | +|---|---| +| controle | — | +| seeds | `--seed-exchange` | +| alternate | `--alternate-engines` | + +- **Amostras:** Cover-Error em `r15-ce.tsv`; Cover-Branches em `r15-cb.tsv` (seeds e + alternate). +- **Gate:** TRUE errado = 0. +- **Critério de promoção:** mais tarefas cobertas que seeds em Cover-Error e cobertura + média de CB não pior. diff --git a/docs/superpowers/specs/2026-09-29-tacas-3c-seed-ranking-design.md b/docs/superpowers/specs/2026-09-29-tacas-3c-seed-ranking-design.md new file mode 100644 index 000000000..f7741590b --- /dev/null +++ b/docs/superpowers/specs/2026-09-29-tacas-3c-seed-ranking-design.md @@ -0,0 +1,34 @@ +# tacas 3c — priorização de sementes, v1 (design) + +**Data:** 2026-09-29 +**Branch:** `feat/tacas-3c-seed-ranking`, a partir de `feat/tacas-memtrack-intrinsics` +**Aprovação:** decisões delegadas pelo usuário em 2026-09-29. + +## Problema + +O KLEE recebe no máximo 64 entradas da fila do AFL++ (`kMaxSeedsFromFuzzer`), escolhidas +pelas mais antigas por id. Quando a fila passa de 64, o que era novo no fim do fuzzing fica +de fora, e esse é justamente o caso dos programas maiores. + +## v1 (esta branch) + +- O AFL++ 4.40c marca com `,+cov` as entradas que alcançaram **arestas novas**. As demais só + mudaram as contagens de execução de arestas já vistas. Medido: 2 de 18 entradas numa fila + de 20 s. Não existe `.state/redundant_edges` nesta versão. +- `selectQueueEntries` põe as `+cov` primeiro, em ordem de id, depois as outras, também em + ordem de id, e então corta no limite. +- Teste unitário: `SelectQueueEntries.PutsNewCoverageFirst`. + +## Próximos passos (v2, fora desta branch) + +- **Distância ao alvo** (Cover-Error): priorizar sementes cujo replay passa por blocos mais + próximos de `reach_error` no CFG/SDG. O dg do slicing já tem o grafo. Exige um traço de + blocos no replay, que o `TrackBasicBlockPass` pode fornecer. +- **KLEE → AFL++:** hoje seguem os 64 `.ktest` mais recentes. O KLEE não marca quais estados + cobriram código novo; `--only-output-states-covering-new` mudaria a suíte de CB e não + entra. + +## Medição + +É preciso uma rodada `seeds` e `alternate` com este build contra a R19 (os mesmos braços +sem ranking). Só tem efeito em tarefas cuja fila passa de 64 entradas. diff --git a/modules/backend/library/lib/AnalysisModeMemcleanup.c b/modules/backend/library/lib/AnalysisModeMemcleanup.c index d66439869..3c506b206 100644 --- a/modules/backend/library/lib/AnalysisModeMemcleanup.c +++ b/modules/backend/library/lib/AnalysisModeMemcleanup.c @@ -156,6 +156,7 @@ void analysis_generate_aux_witness_files() { // TODO: FIX THIS, not working for static array #include void map2check_load(void *ptr, int size) {} +void map2check_check_cstring(const char *string) {} void map2check_free_resolved_address(void *ptr, unsigned line, const char *function_name, diff --git a/modules/backend/library/lib/AnalysisModeMemtrack.c b/modules/backend/library/lib/AnalysisModeMemtrack.c index 87e79ad1f..a06f363c3 100644 --- a/modules/backend/library/lib/AnalysisModeMemtrack.c +++ b/modules/backend/library/lib/AnalysisModeMemtrack.c @@ -153,6 +153,18 @@ void analysis_generate_aux_witness_files() { // TODO: FIX THIS, not working for static array #include +/* Every byte a %s or puts will read, up to the terminator: each must lie in + * a live allocation. Stops at the first invalid byte (ERROR_DEREF is set and + * the caller's map2check_check_deref reports it), before reading it. */ +void map2check_check_cstring(const char *string) { + if (string == NULL) return; + for (unsigned long i = 0;; ++i) { + map2check_load((void *)(string + i), 1); + if (ERROR_DEREF) return; + if (string[i] == '\0') return; + } +} + void map2check_load(void *ptr, int size) { if (!is_valid_heap_address(&heap_log, ptr, size)) { if (!is_valid_allocation_address(&allocation_log, ptr, size)) { diff --git a/modules/backend/library/lib/NonDetGeneratorAFL.c b/modules/backend/library/lib/NonDetGeneratorAFL.c index 01cefa075..4eb4bc7cc 100644 --- a/modules/backend/library/lib/NonDetGeneratorAFL.c +++ b/modules/backend/library/lib/NonDetGeneratorAFL.c @@ -52,13 +52,17 @@ size_t map2check_afl_size; * drags afl-fuzz's stability down. */ static size_t map2check_afl_index = 0; +/* Past the end of the test case every read is zero. It used to start over + * from the first byte, so `while (__VERIFIER_nondet_int())` fed by the + * placeholder seed "A" never ended: afl-fuzz's dry run timed out on it and the + * fuzzer aborted before its first execution. Zero ends such a loop, and it is + * what the witness replay logs, so the suite built from that log stays exact. + * (It also read data[0] of an empty test case.) */ uint8_t get_next_input_from_afl() { if (map2check_afl_index < map2check_afl_size) { return map2check_afl_data[map2check_afl_index++]; } - - map2check_afl_index = 0; - return map2check_afl_data[map2check_afl_index]; + return 0; } /* Fills `out` with `size` bytes from the AFL buffer, in target order. diff --git a/modules/backend/library/lib/NonDetGeneratorKlee.c b/modules/backend/library/lib/NonDetGeneratorKlee.c index 74bb6b721..be9c215b3 100644 --- a/modules/backend/library/lib/NonDetGeneratorKlee.c +++ b/modules/backend/library/lib/NonDetGeneratorKlee.c @@ -23,7 +23,15 @@ void nondet_generate_aux_witness_files() { extern void klee_assume(int); -void nondet_assume(int expr) { klee_assume(expr); } +/* A failed assumption ends the path silently. klee_assume(0) on a path where + * the condition is already false is a KLEE error ("invalid klee_assume call + * (provably false)", a user.err), and the frontend must read every KLEE error + * as a dropped path -- which made every program with an assume_abort_if_not + * unprovable. klee_silent_exit leaves no test and no error. */ +extern void klee_silent_exit(int status); +void nondet_assume(int expr) { + if (!expr) klee_silent_exit(0); +} extern void klee_make_symbolic(void *addr, size_t nbytes, const char *name); diff --git a/modules/backend/library/lib/WitnessGeneration.c b/modules/backend/library/lib/WitnessGeneration.c index a4de44c20..330f3876b 100644 --- a/modules/backend/library/lib/WitnessGeneration.c +++ b/modules/backend/library/lib/WitnessGeneration.c @@ -6,6 +6,7 @@ * SPDX-License-Identifier: (GPL-2.0) **/ +#include #include "../header/WitnessGeneration.h" #include "../header/AnalysisMode.h" #include "../header/NonDetGenerator.h" @@ -19,7 +20,10 @@ void generate_aux_files(MAP2CHECK_CONTAINER *trackbb_log, Bool violation) { * so without the guard a state that took a different branch clobbers the * violating one's log -- which is exactly what produced a test case with the * right first input and a wrong second one. */ - if (violation) { + /* The seed exchange replays the fuzzer's NON-violating queue entries to + * learn their typed vectors, so it asks for the log explicitly. Only that + * replay sets the variable; KLEE's forked states never do. */ + if (violation || getenv("MAP2CHECK_SEED_REPLAY") != NULL) { nondet_generate_aux_witness_files(); } } diff --git a/modules/backend/pass/MemoryTrackPass.cpp b/modules/backend/pass/MemoryTrackPass.cpp index a35477a80..475c930a3 100644 --- a/modules/backend/pass/MemoryTrackPass.cpp +++ b/modules/backend/pass/MemoryTrackPass.cpp @@ -10,8 +10,12 @@ #include "MemoryTrackPass.hpp" +#include +#include #include +#include +#include #include #include #include @@ -209,8 +213,10 @@ void MemoryTrackPass::instrumentMemset() { IRBuilder<> builder(BBIteratorToInst(j)); Value *function_llvm = builder.CreateGlobalStringPtr(function_name); - // Value *args[] = {varPointerCast, size}; - Value *args[] = {pointer, size}; + // map2check_load takes an i64 size; the intrinsic's may be i32. + Value *sizeCast = CastInst::CreateIntegerCast( + size, Type::getInt64Ty(*this->Ctx), false, bitcast, BBIteratorToInst(j)); + Value *args[] = {varPointerCast, sizeCast}; builder.CreateCall(map2check_load, args); Value *args2[] = {this->line_value, function_llvm}; @@ -255,6 +261,106 @@ void MemoryTrackPass::instrumentMemcpy() { builder.CreateCall(map2check_check_deref, args3); } +namespace { +/** Behind MAP2CHECK_CHECK_CSTRINGS=1 until measured on more of Juliet. The + * check fixes a wrong TRUE (CWE193 "cpy" bad: the buffer is full, the read + * always overruns it) and makes a wrong FALSE on the matching good tasks, whose + * terminator is a byte never initialized -- which SV-COMP counts as a + * terminator and a native or KLEE run does not (R21: one of each in 50). */ +bool cstringChecksEnabled() { + const char *knob = std::getenv("MAP2CHECK_CHECK_CSTRINGS"); + return knob != nullptr && std::string(knob) == "1"; +} + +/** The argument positions a constant printf format reads as strings: each + * %s without a precision (a %.Ns may legitimately point at an unterminated + * buffer). `first` is the position of the first variadic argument. Returns + * nothing for a format it cannot follow (%n$ positional arguments). */ +std::vector stringArgumentsOf(llvm::StringRef format, + unsigned first) { + std::vector positions; + unsigned argument = first; + for (size_t i = 0; i < format.size(); ++i) { + if (format[i] != '%') continue; + ++i; + if (i < format.size() && format[i] == '%') continue; + // flags + while (i < format.size() && llvm::StringRef("-+ #0'").contains(format[i])) + ++i; + // width + if (i < format.size() && format[i] == '*') { + ++argument; + ++i; + } + while (i < format.size() && isdigit(static_cast(format[i]))) + ++i; + if (i < format.size() && format[i] == '$') return {}; + // precision + bool precision = false; + if (i < format.size() && format[i] == '.') { + precision = true; + ++i; + if (i < format.size() && format[i] == '*') { + ++argument; + ++i; + } + while (i < format.size() && + isdigit(static_cast(format[i]))) + ++i; + } + // length modifiers + bool wide = false; + while (i < format.size() && llvm::StringRef("hlLqjzt").contains(format[i])) { + if (format[i] == 'l') wide = true; + ++i; + } + if (i >= format.size()) break; + if (format[i] == 's' && !precision && !wide) positions.push_back(argument); + ++argument; + } + return positions; +} +} // namespace + +/* KLEE's uClibc declares printf without defining it, so KLEE runs it as a + * native external call: whatever it reads is read outside every check. An + * unterminated buffer printed with %s -- Juliet's CWE121 CWE193 "cpy" tasks -- + * came back TRUE. The strings the call will read are checked here, before it: + * the format's %s arguments when the format is a constant, the first argument + * of puts/fputs. */ +void MemoryTrackPass::instrumentCStringArguments() { + CallInst *callInst = dyn_cast(&*this->currentInstruction); + llvm::StringRef name = this->calleeFunction->getName(); + + std::vector strings; + if (name == "puts" || name == "fputs") { + strings.push_back(0); + } else { + const unsigned formatIndex = + name == "printf" ? 0 : (name == "snprintf" ? 2 : 1); + if (callInst->arg_size() <= formatIndex) return; + llvm::StringRef format; + if (!llvm::getConstantStringInfo(callInst->getArgOperand(formatIndex), + format)) { + return; + } + strings = stringArgumentsOf(format, formatIndex + 1); + } + if (strings.empty()) return; + + IRBuilder<> builder(&*this->currentInstruction); + Value *function_llvm = + builder.CreateGlobalStringPtr(this->currentFunction->getName()); + for (unsigned position : strings) { + if (position >= callInst->arg_size()) continue; + Value *argument = callInst->getArgOperand(position); + if (!argument->getType()->isPointerTy()) continue; + builder.CreateCall(map2check_check_cstring, {argument}); + } + Value *args[] = {this->line_value, function_llvm}; + builder.CreateCall(map2check_check_deref, args); +} + void MemoryTrackPass::instrumentAlloca() { CallInst *callInst = dyn_cast(&*this->currentInstruction); auto j = this->currentInstruction; @@ -502,16 +608,22 @@ void MemoryTrackPass::switchCallInstruction() { this->instrumentFree(); } else if (this->calleeFunction->getName() == "posix_memalign") { this->instrumentPosixMemAllign(); - } else if (this->calleeFunction->getName() == "memset") { - this->instrumentMemset(); - } else if (this->calleeFunction->getName() == "llvm.memset.p0i8.i64") { - this->instrumentMemset(); - } else if (this->calleeFunction->getName() == "llvm.memset.p0i8.i32") { + } else if (llvm::isa(&*this->currentInstruction) || + calleeName == "memset") { + // By the intrinsic's kind, not its name. The names carried the pointer + // types -- llvm.memset.p0i8.i64 -- and with opaque pointers LLVM 16 names + // them llvm.memset.p0.i64: matched by name, no memset, memcpy or memmove + // clang emitted was checked at all (memset(p, 0, 16) on 8 malloc'd bytes + // came back UNKNOWN, found only by KLEE's own bounds check). this->instrumentMemset(); - } else if (this->calleeFunction->getName() == "llvm.memcpy.p0i8.p0i8.i64") { - this->instrumentMemcpy(); - } else if (this->calleeFunction->getName() == "llvm.memcpy.p0i8.p0i8.i32") { + } else if (llvm::isa(&*this->currentInstruction) || + calleeName == "memcpy" || calleeName == "memmove") { this->instrumentMemcpy(); + } else if ((calleeName == "printf" || calleeName == "fprintf" || + calleeName == "sprintf" || calleeName == "snprintf" || + calleeName == "puts" || calleeName == "fputs") && + cstringChecksEnabled()) { + this->instrumentCStringArguments(); } else if (this->calleeFunction->getName() == "malloc") { this->instrumentMalloc(); } else if (this->calleeFunction->getName() == "valloc") { @@ -782,6 +894,10 @@ void MemoryTrackPass::prepareMap2CheckInstructions() { Type::getInt64Ty(*this->Ctx), PointerType::get(*this->Ctx, 0), Type::getInt64Ty(*this->Ctx), PointerType::get(*this->Ctx, 0)); + this->map2check_check_cstring = F.getParent()->getOrInsertFunction( + "map2check_check_cstring", Type::getVoidTy(*this->Ctx), + PointerType::get(*this->Ctx, 0)); + this->map2check_check_deref = F.getParent()->getOrInsertFunction( "map2check_check_deref", Type::getVoidTy(*this->Ctx), Type::getInt64Ty(*this->Ctx), PointerType::get(*this->Ctx, 0)); diff --git a/modules/backend/pass/MemoryTrackPass.hpp b/modules/backend/pass/MemoryTrackPass.hpp index 2d404a9d2..b80148a21 100644 --- a/modules/backend/pass/MemoryTrackPass.hpp +++ b/modules/backend/pass/MemoryTrackPass.hpp @@ -49,6 +49,9 @@ struct MemoryTrackPass : public llvm::PassInfoMixin { void instrumentRealloc(); void instrumentMemset(); void instrumentMemcpy(); + /** Checks, before a printf-family call or puts/fputs, every string the call + * will read to its terminator (see the definition). */ + void instrumentCStringArguments(); void instrumentPosixMemAllign(); void instrumentFree(); void instrumentInit(); @@ -92,6 +95,7 @@ struct MemoryTrackPass : public llvm::PassInfoMixin { FunctionCallee map2check_non_static_alloca; FunctionCallee map2check_posix; FunctionCallee map2check_load; + FunctionCallee map2check_check_cstring; FunctionCallee map2check_check_deref; FunctionCallee map2check_function; FunctionCallee map2check_free_resolved_address; diff --git a/modules/backend/pass/NonDetPass.cpp b/modules/backend/pass/NonDetPass.cpp index 08dc2b6d0..4e8e397ea 100644 --- a/modules/backend/pass/NonDetPass.cpp +++ b/modules/backend/pass/NonDetPass.cpp @@ -100,6 +100,58 @@ bool rewriteAssumeToPrune(Function &F) { return true; } +/** Rewrites the program's own calls to abort() into path pruning. Returns how + * many it rewrote. + * + * In SV-COMP, abort() is not an error -- reach_error is the only one -- it is + * how a program discards a path, and the benchmarks write that assumption + * inline as well as through assume_abort_if_not: + * + * i2 = init(); + * if(!(i2)) {abort();} + * + * KLEE runs with --exit-on-error-type=Abort, so the first path violating such + * an assumption ended the whole search, with exit status 0, and the run + * answered TRUE for a program whose bug lay further on. Measured: every wrong + * TRUE of the tacasv2 control arm in the R15 Cover-Error sample (the + * seq-mthreaded/pals_* family and float-benchs/sin_interpolated_index-1). + * + * This runs on the user's module before the runtime is linked, so every abort + * here is the program's; the runtime's own abort (the one that signals a + * recorded violation) is never touched. A violation is still reported the same + * way: TargetPass instruments reach_error itself, so a `{reach_error(); + * abort();}` records the violation before the rewritten abort is reached. */ +unsigned rewriteAbortCallsToPrune(Function &F) { + std::vector aborts; + for (BasicBlock &block : F) { + for (Instruction &instruction : block) { + if (CallInst *call = dyn_cast(&instruction)) { + Function *callee = call->getCalledFunction(); + if (callee != nullptr && callee->getName() == "abort" && + call->arg_size() == 0) { + aborts.push_back(call); + } + } + } + } + if (aborts.empty()) return 0; + + LLVMContext &ctx = F.getContext(); + llvm::Type *int32 = llvm::Type::getInt32Ty(ctx); + llvm::FunctionCallee assume = F.getParent()->getOrInsertFunction( + "map2check_assume", llvm::Type::getVoidTy(ctx), int32); + for (CallInst *call : aborts) { + IRBuilder<> builder(call); + llvm::CallInst *pruned = + builder.CreateCall(assume, {llvm::ConstantInt::get(int32, 0)}); + pruned->setDebugLoc(call->getDebugLoc()); + call->eraseFromParent(); + } + llvm::errs() << "[map2check] rewrote " << aborts.size() << " abort() call(s)" + << " in " << F.getName() << " to prune the path\n"; + return aborts.size(); +} + } // namespace PreservedAnalyses NonDetPass::run(Function &F, @@ -110,6 +162,8 @@ PreservedAnalyses NonDetPass::run(Function &F, return PreservedAnalyses::none(); } + rewriteAbortCallsToPrune(F); + this->nonDetFunctions = make_unique(&F, &F.getContext()); bool initializedFunctionName = false; for (Function::iterator bb = F.begin(), e = F.end(); bb != e; ++bb) { diff --git a/modules/frontend/CMakeLists.txt b/modules/frontend/CMakeLists.txt index 19778b60e..edc9e75d1 100644 --- a/modules/frontend/CMakeLists.txt +++ b/modules/frontend/CMakeLists.txt @@ -38,4 +38,19 @@ target_include_directories(map2check PRIVATE "${CMAKE_CURRENT_BINARY_DIR}") #set_target_properties(map2check PROPERTIES COMPILE_FLAGS ${CPP_FLAGS}) #-lrt -ldl -ltinfo -lpthread -lz -lm target_link_libraries(map2check ${Boost_LIBRARIES}) + +# --alternate-engines watches KLEE's progress in its SQLite stats database +# (tacas 3b). Optional: without SQLite -- the CI images do not install it -- +# KLEE runs to its window and only the fuzzer stops on stagnation. +find_package(Threads REQUIRED) +target_link_libraries(map2check Threads::Threads) +find_package(SQLite3) +if(SQLite3_FOUND) + target_compile_definitions(Caller PRIVATE MAP2CHECK_HAVE_SQLITE) + target_include_directories(Caller PRIVATE ${SQLite3_INCLUDE_DIRS}) + target_link_libraries(map2check ${SQLite3_LIBRARIES} ${CMAKE_DL_LIBS}) + message(STATUS "SQLite3 found: KLEE stagnation detection enabled") +else() + message(STATUS "SQLite3 not found: KLEE stagnation detection disabled") +endif() install (TARGETS map2check DESTINATION .) diff --git a/modules/frontend/caller.cpp b/modules/frontend/caller.cpp index 2c557fb1f..4d2cde8d1 100644 --- a/modules/frontend/caller.cpp +++ b/modules/frontend/caller.cpp @@ -22,15 +22,28 @@ #include #include #include +#include +#include #include #include #include +#include #include #include +#include +#include + +#ifdef MAP2CHECK_HAVE_SQLITE +#include +#endif + #include "test_suite/ktest_reader.hpp" +#include "test_suite/test_suite.hpp" #include "utils/gen_crypto_hash.hpp" +#include "utils/alternation.hpp" #include "utils/log.hpp" +#include "utils/seed_store.hpp" #include "utils/slicer.hpp" #include "utils/tools.hpp" // namespace fs = boost::filesystem; @@ -63,7 +76,10 @@ Caller::Caller(std::string bc_program_path, Map2CheckMode mode, this->nonDetGenerator = generator; GenHash hash; hash.setFilePath(bc_program_path); - hash.generate_sha1_hash_for_file(); + if (hash.generate_sha1_hash_for_file() != 0) { + throw std::runtime_error("cannot read the input program " + + bc_program_path); + } this->programHash = hash.getOutputSha1HashFile() + ".map2check"; // The scratch directory is named after the SHA-1 of the input bitcode, so it @@ -84,6 +100,9 @@ Caller::Caller(std::string bc_program_path, Map2CheckMode mode, Map2Check::Log::Debug("Changing current dir"); currentPath = std::filesystem::current_path().string(); + seedStore = Map2Check::seedStorePath(currentPath, programHash); + sliceCache = Map2Check::sliceCachePath(currentPath, programHash); + buildCache = currentPath + "/" + programHash + ".build"; std::filesystem::current_path(currentPath + "/" + programHash); Map2Check::Log::Debug("Current path: " + std::filesystem::current_path().string()); @@ -103,6 +122,14 @@ std::chrono::steady_clock::time_point processStart() { } } // namespace +unsigned Caller::remainingOf(unsigned timeout) { + const auto elapsed = std::chrono::duration_cast( + std::chrono::steady_clock::now() - processStart()) + .count(); + const long long left = static_cast(timeout) - elapsed; + return left < 1 ? 1u : static_cast(left); +} + unsigned Caller::remainingSeconds() const { const auto elapsed = std::chrono::duration_cast( std::chrono::steady_clock::now() - processStart()) @@ -115,6 +142,20 @@ unsigned Caller::remainingSeconds() const { return left < 1 ? 1u : static_cast(left); } +bool Caller::ssaPreoptimization() const { + // Reachability and assert only. The memory modes track locals through the + // allocas mem2reg removes (a pointer kept in a local, promoted, made a + // legitimate free() look invalid: FALSE-FREE on safe programs), the overflow + // mode lost detections, and simplifycfg turns branches into selects, which + // is fewer paths and fewer Cover-Branches test cases. + if (map2checkMode != Map2CheckMode::REACHABILITY_MODE && + map2checkMode != Map2CheckMode::ASSERT_MODE) { + return false; + } + const char *knob = std::getenv("MAP2CHECK_PREOPT"); + return knob != nullptr && std::string(knob) == "ssa"; +} + std::string Caller::preOptimizationFlags() { std::ostringstream flags; flags.str(""); @@ -129,18 +170,222 @@ std::string Caller::postOptimizationFlags() { return flags.str(); } +namespace { +/** KLEE's covered-instruction count, from the last row of the SQLite stats + * database it rewrites every second; -1 when it cannot be read (not created + * yet, busy, or a build without SQLite). */ +long long kleeCoveredInstructions(const std::string &statsPath) { +#ifdef MAP2CHECK_HAVE_SQLITE + sqlite3 *db = nullptr; + long long covered = -1; + if (sqlite3_open_v2(statsPath.c_str(), &db, SQLITE_OPEN_READONLY, nullptr) == + SQLITE_OK) { + sqlite3_busy_timeout(db, 200); + sqlite3_stmt *statement = nullptr; + if (sqlite3_prepare_v2(db, + "SELECT CoveredInstructions FROM stats ORDER BY " + "rowid DESC LIMIT 1", + -1, &statement, nullptr) == SQLITE_OK && + sqlite3_step(statement) == SQLITE_ROW) { + covered = sqlite3_column_int64(statement, 0); + } + sqlite3_finalize(statement); + } + sqlite3_close(db); + return covered; +#else + (void)statsPath; + return -1; +#endif +} +} // namespace + +int Caller::runKleeWatched(const std::string &command) { + this->stoppedOnStagnation = false; +#ifndef MAP2CHECK_HAVE_SQLITE + return system(command.c_str()); +#else + if (this->stagnationLimit == 0) return system(command.c_str()); + + // The shell's pid becomes the pid of `timeout` through exec, and `timeout` + // forwards a SIGINT to KLEE -- whose handler halts the search cleanly and + // writes the tests of the states it finished. + std::error_code error; + std::filesystem::remove("klee.pid", error); + const std::string wrapped = "echo $$ > klee.pid; exec " + command; + std::atomic done{false}; + int result = 0; + std::thread runner([&wrapped, &done, &result] { + result = system(wrapped.c_str()); + done = true; + }); + + Map2Check::CoverageWatch watch(this->stagnationLimit); + const auto started = std::chrono::steady_clock::now(); + const std::string stats = std::string(Map2Check::kleeOutputDir) + "/run.stats"; + while (!done) { + for (int tick = 0; tick < 4 && !done; ++tick) { + std::this_thread::sleep_for(std::chrono::milliseconds(500)); + } + if (done) break; + const double now = std::chrono::duration( + std::chrono::steady_clock::now() - started) + .count(); + if (!watch.stagnated(kleeCoveredInstructions(stats), now)) continue; + + // To KLEE itself, the child of `timeout`: signalled, `timeout` forwards + // to the child AND its process group, KLEE gets two SIGINTs, and the + // second one exits before the halt dump of the live states is written. + pid_t pid = 0; + std::ifstream("klee.pid") >> pid; + pid_t klee = 0; + if (pid > 0) { + std::ifstream children("/proc/" + std::to_string(pid) + "/task/" + + std::to_string(pid) + "/children"); + children >> klee; + } + if (klee > 0) { + kill(klee, SIGINT); + } else if (pid > 0) { + kill(pid, SIGINT); + } + this->stoppedOnStagnation = true; + Map2Check::Log::Warning("KLEE stagnated: no new coverage for " + + std::to_string(this->stagnationLimit) + + " s -- stopping it"); + break; + } + runner.join(); + return result; +#endif +} + +bool Caller::replayKleeVectorsForViolation() { + // KLEE's partial paths -- the states it dumped at a halt -- stop where the + // search stopped. Run natively, completed with zeros past their end (the + // AFL++ generator's rule), some of them go on to the error: that is how the + // fixed hybrid covered eca-* tasks KLEE left UNKNOWN, by accident, in its + // last fuzzer phase's dry run. Done on purpose here, right after KLEE, and + // without needing --seed-exchange. + std::error_code error; + std::string witness; + for (const auto &entry : + std::filesystem::directory_iterator(buildCache, error)) { + const std::string candidate = + entry.path().string() + "/" + programHash + "-witness-fuzzed.out"; + if (std::filesystem::exists(candidate, error)) witness = candidate; + } + if (witness.empty()) return false; + + std::vector tests; + for (const auto &entry : std::filesystem::directory_iterator( + Map2Check::kleeOutputDir, error)) { + if (entry.path().extension() == ".ktest") { + tests.push_back(entry.path().string()); + } + } + std::sort(tests.begin(), tests.end()); + + const std::string replay = + std::filesystem::absolute("vector-replay", error).string(); + const auto started = std::chrono::steady_clock::now(); + const double allowedSeconds = std::min( + 0.1 * static_cast(this->timeout), + static_cast(this->remainingSeconds()) - 5.0); + if (allowedSeconds < 1.0) return false; + const auto allowed = std::chrono::duration(allowedSeconds); + std::set> seen; + unsigned replayed = 0; + for (const std::string &test : tests) { + if (std::chrono::steady_clock::now() - started >= allowed) break; + const std::vector bytes = + Map2Check::ktestToFuzzerBytes(Map2Check::readKtestFile(test)); + if (!seen.insert(bytes).second) continue; + std::filesystem::remove_all(replay, error); + std::filesystem::create_directories(replay, error); + { + std::ofstream input(replay + "/input", std::ios::binary); + input.write(reinterpret_cast(bytes.data()), + static_cast(bytes.size())); + } + std::ostringstream command; + command << "cd '" << replay << "' && timeout -k 1 2 '" << witness + << "' < input > /dev/null 2>&1"; + system(command.str().c_str()); + ++replayed; + if (!std::filesystem::exists(replay + "/map2check_checked_error", error)) { + continue; + } + // A violation: its files (property, nondet log, trace) become this + // phase's, as a confirmed fuzzer crash's do. + for (const auto &entry : + std::filesystem::directory_iterator(replay, error)) { + if (!entry.is_regular_file(error)) continue; + if (entry.path().filename() == "input") continue; + std::filesystem::copy_file( + entry.path(), entry.path().filename(), + std::filesystem::copy_options::overwrite_existing, error); + } + std::filesystem::remove_all(replay, error); + Map2Check::Log::Info("A KLEE vector completed with zeros reaches the " + "violation (" + std::to_string(replayed) + + " replayed)"); + return true; + } + std::filesystem::remove_all(replay, error); + return false; +} + +void Caller::keepKleeTestsAsSeeds() { + // The latest tests, not the first: KLEE numbers them as states finish, and + // the later ones are the deeper paths the next turn should start from. + std::error_code error; + const std::string kept = seedStore + "/kleeprev"; + std::filesystem::remove_all(kept, error); + std::vector tests; + for (const auto &entry : std::filesystem::directory_iterator( + Map2Check::kleeOutputDir, error)) { + if (entry.path().extension() == ".ktest") { + tests.push_back(entry.path().string()); + } + } + if (tests.empty()) return; + std::sort(tests.begin(), tests.end()); + if (tests.size() > kMaxSeedsFromFuzzer) { + tests.erase(tests.begin(), tests.end() - kMaxSeedsFromFuzzer); + } + std::filesystem::create_directories(kept, error); + for (const std::string &test : tests) { + std::filesystem::copy_file( + test, kept + "/" + std::filesystem::path(test).filename().string(), + std::filesystem::copy_options::overwrite_existing, error); + } +} + unsigned Caller::exportKleeVectorsAsSeeds() { std::error_code error; - std::filesystem::create_directories(Caller::seedDirectory, error); + const std::string aflSeeds = seedStore + "/afl"; + std::filesystem::create_directories(aflSeeds, error); - std::vector> ignored; - unsigned written = 0; - unsigned index = 0; + std::vector tests; for (const auto &entry : std::filesystem::directory_iterator( Map2Check::kleeOutputDir, error)) { - if (entry.path().extension() != ".ktest") continue; + if (entry.path().extension() == ".ktest") { + tests.push_back(entry.path().string()); + } + } + // All of them, not a sample: completed with zeros past their end, some of + // KLEE's partial paths reach the error when the fuzzer runs them -- the + // dry run records them as crashes (sig 06), and that is how the fixed + // hybrid covered eca-* tasks KLEE itself left UNKNOWN. A cap of the 64 + // latest dropped exactly those (R19: 5 eca-* losses of --alternate-engines). + // Calibrating thousands is cheap now that a nondet loop ends on zeros. + std::sort(tests.begin(), tests.end()); + unsigned written = 0; + unsigned index = 0; + for (const std::string &test : tests) { std::vector objects = - Map2Check::readKtestFile(entry.path().string()); + Map2Check::readKtestFile(test); if (objects.empty()) continue; std::vector bytes = Map2Check::ktestToFuzzerBytes(objects); @@ -149,7 +394,7 @@ unsigned Caller::exportKleeVectorsAsSeeds() { // Named by index rather than by content hash: AFL++ renames what it // keeps to its own hash anyway, so a second one here buys nothing. std::ostringstream name; - name << Caller::seedDirectory << "/klee-" << index++; + name << aflSeeds << "/klee-" << index++; std::ofstream out(name.str(), std::ios::binary); if (!out.is_open()) continue; out.write(reinterpret_cast(bytes.data()), @@ -163,24 +408,207 @@ unsigned Caller::exportKleeVectorsAsSeeds() { return written; } -std::string Caller::exportFuzzerVectorAsKtest() { - std::vector objects = - Map2Check::readNonDetLogAsObjects(Map2Check::kleeLogCSV); - if (objects.empty()) return ""; +unsigned Caller::exportFuzzerCorpusAsKtests() { + // Each queue entry is replayed through the witness binary, whose runtime + // logs every nondet read with its type (klee_log.csv) -- which is what a + // .ktest needs and what the fuzzer's raw bytes lack. The replay runs in the + // store's replay/, not here: the witness writes map2check_property and + // friends into its working directory, and a replay must never overwrite a + // violation this phase already recorded. + std::error_code error; + const std::string queue = "afl-out/default/queue"; + const std::string replay = seedStore + "/replay"; + const std::string ktests = seedStore + "/ktest"; + const std::string witness = + std::filesystem::absolute(programHash + "-witness-fuzzed.out", error) + .string(); + if (!std::filesystem::exists(witness, error)) return 0; + + std::vector names; + for (const auto &entry : + std::filesystem::directory_iterator(queue, error)) { + if (entry.is_regular_file(error)) { + names.push_back(entry.path().filename().string()); + } + } + // This round's discoveries replace the last round's: KLEE already ran on + // those, and its own tests from that turn (kleeprev/) carry them forward. + std::filesystem::remove_all(ktests, error); + std::filesystem::create_directories(ktests, error); + + // Bounded as a whole, not only per entry: the replays come out of the KLEE + // phase's budget, so they stop at 5% of the run's budget (at least 2 s). + const auto started = std::chrono::steady_clock::now(); + const auto allowed = std::chrono::duration( + std::max(2.0, 0.05 * static_cast(this->timeout))); + std::set> seen; + unsigned written = 0; + for (const std::string &name : + Map2Check::selectQueueEntries(names, kMaxSeedsFromFuzzer)) { + if (std::chrono::steady_clock::now() - started >= allowed) break; + std::filesystem::remove_all(replay, error); + std::filesystem::create_directories(replay, error); + const std::string input = + std::filesystem::absolute(queue + "/" + name, error).string(); + std::ostringstream command; + command << "cd '" << replay << "' && MAP2CHECK_SEED_REPLAY=1 timeout -k 1 2 '" << witness + << "' < '" << input << "' > /dev/null 2>&1"; + system(command.str().c_str()); + + const std::vector objects = + Map2Check::readNonDetLogAsObjects(replay + "/" + + Map2Check::kleeLogCSV); + if (objects.empty()) continue; + if (!Map2Check::isNewVector(Map2Check::ktestToFuzzerBytes(objects), + &seen)) { + continue; + } + if (Map2Check::writeKtestFile( + ktests + "/afl-" + std::to_string(written) + ".ktest", objects)) { + ++written; + } + } + std::filesystem::remove_all(replay, error); + if (written > 0) { + Map2Check::Log::Info("Seeded KLEE with " + std::to_string(written) + + " vectors from AFL++"); + } + return written; +} + +namespace { +/** MAP2CHECK_SLICER_FLAGS / MAP2CHECK_SLICE_CLEANUP: experiment knobs (tacas + * 2d spec), read from the environment so a campaign arm can set them without + * a CLI option nobody else should use. */ +std::string environmentKnob(const char *name) { + const char *value = std::getenv(name); + return value == nullptr ? std::string() : std::string(value); +} +} // namespace +std::vector> Caller::fuzzerCorpusVectors( + size_t cap) { + std::vector> vectors; std::error_code error; - std::filesystem::create_directories(Caller::seedDirectory, error); - const std::string path = - std::string(Caller::seedDirectory) + "/from-fuzzer.ktest"; - if (!Map2Check::writeKtestFile(path, objects)) return ""; - Map2Check::Log::Info("Seeding KLEE with the fuzzer's vector (" + - std::to_string(objects.size()) + " inputs)"); - return path; + const std::string queue = "afl-out/default/queue"; + const std::string replay = + std::filesystem::absolute("suite-replay", error).string(); + const std::string witness = + std::filesystem::absolute(programHash + "-witness-fuzzed.out", error) + .string(); + if (!std::filesystem::exists(witness, error)) return vectors; + + std::vector names; + for (const auto &entry : std::filesystem::directory_iterator(queue, error)) { + if (entry.is_regular_file(error)) { + names.push_back(entry.path().filename().string()); + } + } + const auto started = std::chrono::steady_clock::now(); + const auto allowed = std::chrono::duration( + std::max(2.0, 0.05 * static_cast(this->timeout))); + std::set> seen; + for (const std::string &name : Map2Check::selectQueueEntries(names, cap)) { + if (std::chrono::steady_clock::now() - started >= allowed) break; + std::filesystem::remove_all(replay, error); + std::filesystem::create_directories(replay, error); + const std::string input = + std::filesystem::absolute(queue + "/" + name, error).string(); + std::ostringstream command; + command << "cd '" << replay + << "' && MAP2CHECK_SEED_REPLAY=1 timeout -k 1 2 '" << witness + << "' < '" << input << "' > /dev/null 2>&1"; + system(command.str().c_str()); + std::vector values = + Map2Check::readNonDetLog(replay + "/" + Map2Check::kleeLogCSV); + if (values.empty() || !seen.insert(values).second) continue; + vectors.push_back(values); + } + std::filesystem::remove_all(replay, error); + return vectors; } bool Caller::runSlicer(const std::string &input, const std::string &output, std::vector primary, bool addRuntimeNames, const std::string &entry, const std::string &label) { + // Sliced once per run, not once per phase: see Map2Check::sliceCachePath. + std::error_code error; + std::string key; + { + std::ifstream in(input, std::ios::binary); + if (in.is_open()) { + std::stringstream content; + content << in.rdbuf(); + key = Map2Check::sliceCacheKey( + content.str(), label, entry, + environmentKnob("MAP2CHECK_SLICER_FLAGS") + "|" + + environmentKnob("MAP2CHECK_SLICE_CLEANUP")); + } + } + const std::string cached = sliceCache + "/" + key + ".bc"; + const std::string failed = sliceCache + "/" + key + ".failed"; + if (!key.empty() && std::filesystem::exists(failed, error)) { + Map2Check::Log::Warning( + "sbt-slicer produced no usable output (cached from an earlier phase) " + "-- analysing the unsliced program"); + return false; + } + if (!key.empty() && std::filesystem::exists(cached, error) && + std::filesystem::copy_file( + cached, output, std::filesystem::copy_options::overwrite_existing, + error)) { + Map2Check::Log::Info("Slice of " + label + + ": reusing the slice from an earlier phase"); + return true; + } + + const bool sliced = + runSlicerUncached(input, output, primary, addRuntimeNames, entry, label); + if (sliced) cleanUpSlice(output); + if (!key.empty() && std::filesystem::exists(Map2Check::slicerBinary())) { + std::filesystem::create_directories(sliceCache, error); + if (sliced) { + std::filesystem::copy_file( + output, cached, std::filesystem::copy_options::overwrite_existing, + error); + } else { + std::ofstream(failed) << label << "\n"; + } + } + return sliced; +} + +void Caller::cleanUpSlice(const std::string &slice) { + const std::string passes = Map2Check::sliceCleanupPasses( + environmentKnob("MAP2CHECK_SLICE_CLEANUP")); + if (passes.empty()) return; + const std::string cleaned = slice + ".clean.bc"; + std::ostringstream command; + // Bounded like the slicer: a pass pipeline over a large module is not + // free, and it runs outside any engine's window. + const unsigned cleanupBudget = static_cast(std::max( + 2.0, std::min(0.05 * this->timeout, + static_cast(remainingSeconds()) - 5.0))); + command << "timeout -k " << Map2Check::killGracePeriod << " " + << cleanupBudget << " " << Map2Check::optBinary << " " << passes + << " " << slice << " -o " << cleaned << " >> slicer.output 2>&1"; + Map2Check::Log::Debug(command.str()); + std::error_code error; + if (system(command.str().c_str()) == 0 && + std::filesystem::exists(cleaned, error) && + std::filesystem::file_size(cleaned, error) > 0) { + std::filesystem::rename(cleaned, slice, error); + if (!error) return; + } + Map2Check::Log::Warning("could not clean up the slice (" + passes + + ") -- keeping it as sliced"); +} + +bool Caller::runSlicerUncached(const std::string &input, + const std::string &output, + std::vector primary, + bool addRuntimeNames, const std::string &entry, + const std::string &label) { const std::string slicer = Map2Check::slicerBinary(); if (!std::filesystem::exists(slicer)) { // Announced, not silently skipped. A slicer that is asked for and absent @@ -247,7 +675,8 @@ bool Caller::runSlicer(const std::string &input, const std::string &output, << static_cast(sliceBudget) << " " << slicer << " -c " << Map2Check::slicingCriteria(primary, programNondets) << " --entry=" << entry - << " -cutoff-diverging=false --statistics -o " << output << " " + << " -cutoff-diverging=false --statistics " + << environmentKnob("MAP2CHECK_SLICER_FLAGS") << " -o " << output << " " << input << " > slicer.output 2>&1"; Map2Check::Log::Debug(command.str()); const int result = system(command.str().c_str()); @@ -351,6 +780,11 @@ bool Caller::sliceInstrumented() { return !error; } +void Caller::restoreWorkingDirectory() { + std::error_code error; + std::filesystem::current_path(currentPath, error); +} + void Caller::cleanGarbage() { std::filesystem::current_path(currentPath); std::ostringstream removeCommand; @@ -373,6 +807,39 @@ void Caller::applyNonDetGenerator() { } case (NonDetGenerator::AFLPlusPlus): { Map2Check::Log::Info("Instrumenting with AFL++"); + // Built once per run: every fuzzer phase recompiles the same modules, + // and on the eca-* programs the three builds take ~24 s -- per phase, + // which under --alternate-engines was most of each fuzzer turn. Keyed by + // the two modules' content, like the slice cache. + const std::vector aflBinaries = { + programHash + "-fuzzed.out", programHash + "-witness-fuzzed.out", + programHash + "-cmplog.out"}; + std::string buildKey; + { + std::ifstream result(programHash + "-result.bc", std::ios::binary); + std::ifstream witness(programHash + "-witness-result.bc", + std::ios::binary); + std::stringstream content; + content << result.rdbuf() << "|" << witness.rdbuf(); + buildKey = Map2Check::sliceCacheKey(content.str(), "afl++", "", ""); + } + const std::string builtDir = buildCache + "/" + buildKey; + { + std::error_code cacheErr; + if (std::filesystem::exists(builtDir + "/" + aflBinaries[0], + cacheErr)) { + for (const std::string &binary : aflBinaries) { + if (std::filesystem::exists(builtDir + "/" + binary, cacheErr)) { + std::filesystem::copy_file( + builtDir + "/" + binary, binary, + std::filesystem::copy_options::overwrite_existing, cacheErr); + } + } + Map2Check::Log::Info( + "AFL++ binaries: reusing the build of an earlier phase"); + break; + } + } std::ostringstream command; command.str(""); @@ -393,21 +860,32 @@ void Caller::applyNonDetGenerator() { 1.0, std::min(0.25 * this->timeout, std::max(1.0, static_cast(remainingSeconds()) - 5.0))); - const std::string bound = "timeout -k " + - std::to_string(Map2Check::killGracePeriod) + - " " + std::to_string(static_cast(compileBudget)) + " "; + // One budget for the three builds, not one each: sequential, each + // bounded by 0.25T, they could take 0.75T -- on eca-* that ran the + // process past its deadline with no verdict (R19). Each build gets what + // is left of the shared deadline. + const auto buildDeadline = + std::chrono::steady_clock::now() + + std::chrono::duration(compileBudget); + auto bound = [&buildDeadline]() { + const double left = std::chrono::duration( + buildDeadline - std::chrono::steady_clock::now()) + .count(); + return "timeout -k " + std::to_string(Map2Check::killGracePeriod) + + " " + std::to_string(std::max(1, static_cast(left))) + " "; + }; command - << bound << Map2Check::aflClangFastBinary() + << bound() << Map2Check::aflClangFastBinary() << " -g " << Caller::postOptimizationFlags() << " -o " + programHash + "-fuzzed.out" - << " " + programHash + "-result.bc"; + << " " + programHash + "-result.bc" << " > afl-build.log 2>&1"; - system(command.str().c_str()); + const int built = system(command.str().c_str()); std::ostringstream commandWitness; commandWitness.str(""); - commandWitness << bound << Map2Check::aflClangFastBinary() + commandWitness << bound() << Map2Check::aflClangFastBinary() << " -g " << " -o " + programHash + "-witness-fuzzed.out" << " " + programHash + "-witness-result.bc"; @@ -422,21 +900,54 @@ void Caller::applyNonDetGenerator() { // tacasv1 comparison would pit an unarmed AFL++ against an armed // LibFuzzer. Optional: if it does not build, the fuzzer runs without. std::ostringstream commandCmplog; - commandCmplog << "AFL_LLVM_CMPLOG=1 " << bound + commandCmplog << "AFL_LLVM_CMPLOG=1 " << bound() << Map2Check::aflClangFastBinary() << " -g " << Caller::postOptimizationFlags() << " -o " + programHash + "-cmplog.out" << " " + programHash + "-result.bc"; system(commandCmplog.str().c_str()); + { + std::error_code cacheErr; + if (std::filesystem::exists(aflBinaries[0], cacheErr)) { + std::filesystem::create_directories(builtDir, cacheErr); + for (const std::string &binary : aflBinaries) { + if (std::filesystem::exists(binary, cacheErr)) { + std::filesystem::copy_file( + binary, builtDir + "/" + binary, + std::filesystem::copy_options::overwrite_existing, cacheErr); + } + } + } + } + // Announced rather than discovered later as a silent no-op -- the same - // failure mode the sliced arm spent a whole campaign in. + // failure mode the sliced arm spent a whole campaign in. And for what it + // is: a link error (an undefined reach_error) used to be reported as a + // build that ran out of time. std::error_code fuzzErr; if (!std::filesystem::exists(programHash + "-fuzzed.out", fuzzErr)) { + std::string why; + if (built == 31744) { // timeout's 124 + why = "did not build within " + + std::to_string(static_cast(compileBudget)) + "s"; + } else { + std::ifstream buildLog("afl-build.log"); + // The first complaint names the cause (an undefined reference); + // the last is only clang's "linker command failed". + std::string line, firstError; + while (firstError.empty() && std::getline(buildLog, line)) { + if (line.find("error") != std::string::npos || + line.find("undefined reference") != std::string::npos) { + firstError = line; + } + } + why = "failed to build (status " + std::to_string(built) + ")" + + (firstError.empty() ? "" : ": " + firstError); + } Map2Check::Log::Warning( - "the AFL++ binary did not build within " + - std::to_string(static_cast(compileBudget)) + - "s -- skipping the fuzzer phase and leaving the budget to KLEE"); + "the AFL++ binary " + why + + " -- skipping the fuzzer phase and leaving the budget to KLEE"); } else if (!std::filesystem::exists(programHash + "-cmplog.out", fuzzErr)) { Map2Check::Log::Warning( @@ -721,9 +1232,14 @@ void Caller::executeAnalysis(std::string solvername) { // holding the budget to its last second is what turned a decided run // into an ERROR. constexpr double kPostEngineReserve = 5.0; + // With the exchange on, the fuzzer gets a real third phase: 0.2 / 0.6 / + // 0.2. Without it the hybrid keeps the 0.2 / 0.8 it was measured with. + // Alternating (--alternate-engines), main hands each phase its window. + const double kleeShare = this->seedExchange ? 0.6 : 0.8; + const double kleeCap = + this->engineWindow > 0 ? this->engineWindow : kleeShare * this->timeout; const double kleeBudget = std::max( - 1.0, std::min(0.8 * this->timeout, - this->remainingSeconds() - kPostEngineReserve)); + 1.0, std::min(kleeCap, this->remainingSeconds() - kPostEngineReserve)); kleeCommand << "timeout -k " << Map2Check::killGracePeriod << " " << static_cast(kleeBudget) << " "; kleeCommand << Map2Check::kleeBinary; @@ -777,10 +1293,44 @@ void Caller::executeAnalysis(std::string solvername) { // from nothing a path the fuzzer already walked -- which under a fixed // budget is not merely faster, it is depth the run would not otherwise // have reached. + // KLEE starts from the fuzzer's corpus when there is one, replaying + // each seed and exploring around it instead of rediscovering from + // nothing the paths the fuzzer already walked. --seed-time caps the + // replay at a quarter of the phase, so seeding cannot eat the search. std::string seedFlag; if (this->seedExchange) { - const std::string seed = exportFuzzerVectorAsKtest(); - if (!seed.empty()) seedFlag = " --seed-file=" + seed; + std::error_code seedError; + bool haveSeeds = false; + for (const auto &entry : std::filesystem::directory_iterator( + seedStore + "/ktest", seedError)) { + if (entry.is_regular_file(seedError)) { + haveSeeds = true; + break; + } + } + // KLEE's own tests from its previous turn, when the engines alternate: + // replaying them rebuilds the frontier it had reached instead of + // rediscovering it. + bool haveOwnSeeds = false; + for (const auto &entry : std::filesystem::directory_iterator( + seedStore + "/kleeprev", seedError)) { + if (entry.is_regular_file(seedError)) { + haveOwnSeeds = true; + break; + } + } + if (haveSeeds || haveOwnSeeds) { + seedFlag = std::string(haveSeeds ? " --seed-dir='" + seedStore + + "/ktest'" + : "") + + (haveOwnSeeds ? " --seed-dir='" + seedStore + "/kleeprev'" + : "") + + " --allow-seed-extension --allow-seed-truncation" + " --seed-time=" + + std::to_string(std::max( + 1u, static_cast(kleeBudget / 4))) + + "s"; + } } // Depth-first for Cover-Branches, and the reason is about what survives @@ -842,8 +1392,16 @@ void Caller::executeAnalysis(std::string solvername) { } Map2Check::Log::Debug(kleeCommand.str()); - int result = system(kleeCommand.str().c_str()); + const auto engineStarted = std::chrono::steady_clock::now(); + int result = runKleeWatched(kleeCommand.str()); + if (this->engineSeconds != nullptr) { + *this->engineSeconds = std::chrono::duration( + std::chrono::steady_clock::now() - + engineStarted) + .count(); + } if (this->seedExchange) { + if (this->stagnationLimit > 0) keepKleeTestsAsSeeds(); // Written after KLEE rather than before the next phase, because the // .ktest files are in the scratch directory that cleanGarbage() will // remove -- and because a later alternation, or a resumed run, should @@ -851,17 +1409,28 @@ void Caller::executeAnalysis(std::string solvername) { exportKleeVectorsAsSeeds(); } Map2Check::Log::Warning("Exited klee with " + std::to_string(result)); + // KLEE found nothing: its vectors, run on natively. Not for + // Cover-Branches, whose goal is no violation. + if (map2checkMode != Map2CheckMode::COVER_BRANCHES_MODE && + !isWitnessFileCreated() && + !Map2Check::hasViolatingKtest(Map2Check::kleeOutputDir)) { + replayKleeVectorsForViolation(); + } if (result == 31744) // Timeout gotTimeout = true; - // KLEE stopping on its own --max-time exits 0, like a run that explored - // every path, but it proves nothing. Treated as the timeout it is: a + // Stopped by us for want of progress: states were left, nothing proved. + if (this->stoppedOnStagnation) gotTimeout = true; + // KLEE exits 0 when its queue empties, like a run that explored every + // path -- also after its timer, a concretized input or states it killed + // itself. None of those proves anything. Treated as the timeout it is: a // violation already recorded is kept, anything else is UNKNOWN -- never // the TRUE a short path's NONE in the property file would otherwise make - // it (a reachable null dereference came back TRUE). - if (Map2Check::kleeHaltedOnTimer(Map2Check::kleeOutputDir)) { - Map2Check::Log::Warning( - "KLEE halted on its timer with states left -- not a complete " - "exploration"); + // it (a reachable null dereference, a float bug, came back TRUE). + const std::string dropped = + Map2Check::kleeDroppedPaths(Map2Check::kleeOutputDir); + if (!dropped.empty()) { + Map2Check::Log::Warning("KLEE " + dropped + + " -- not a complete exploration"); gotTimeout = true; } @@ -887,9 +1456,16 @@ void Caller::executeAnalysis(std::string solvername) { command.str(""); // Against what is LEFT, not against the nominal budget -- see // Caller::remainingSeconds. + // Alternating, the last window can be everything left: keep the same + // reserve KLEE keeps for replaying crashes and writing the suite. const double fuzzerBudget = - std::min(0.2 * this->timeout, - static_cast(this->remainingSeconds())); + this->engineWindow > 0 + ? std::max(1.0, + std::min(this->engineWindow, + static_cast(this->remainingSeconds()) - + 5.0)) + : std::min(0.2 * this->timeout, + static_cast(this->remainingSeconds())); // afl-fuzz needs a non-empty -i dir and a -o dir that does not already // exist (the hybrid may run the fuzzer phase twice). // @@ -900,7 +1476,7 @@ void Caller::executeAnalysis(std::string solvername) { // without one (the previous fuzzer could start from nothing). std::error_code seedErr; const std::string inputDir = - this->seedExchange ? std::string(Caller::seedDirectory) : "afl-in"; + this->seedExchange ? seedStore + "/afl" : std::string("afl-in"); std::filesystem::create_directories(inputDir, seedErr); if (std::filesystem::is_empty(inputDir, seedErr)) { std::ofstream seed(inputDir + "/seed"); @@ -925,6 +1501,11 @@ void Caller::executeAnalysis(std::string solvername) { << " AFL_I_DONT_CARE_ABOUT_MISSING_CRASHES=1" << " AFL_CRASHING_SEEDS_AS_NEW_CRASH=1" << " AFL_BENCH_UNTIL_CRASH=1 "; + // Alternating: the fuzzer hands the rest of its window back as soon as + // it stops finding coverage, and exits 0 doing so -- not a timeout. + if (this->stagnationLimit > 0) { + command << "AFL_EXIT_ON_TIME=" << this->stagnationLimit << " "; + } // Bounded by `timeout` alone, as the previous fuzzer was. Not also by // afl-fuzz -V: that one compares wall-clock (gettimeofday) readings, // and a clock stepped backwards -- measured at over a second under @@ -937,13 +1518,20 @@ void Caller::executeAnalysis(std::string solvername) { const bool hasCmplog = std::filesystem::exists(programHash + "-cmplog.out", cmplogErr); command << Map2Check::aflFuzzBinary() - << " -i " << inputDir + << " -i '" << inputDir << "'" << " -o afl-out"; if (hasCmplog) command << " -c ./" << programHash << "-cmplog.out"; command << " -- ./" << programHash << "-fuzzed.out" << " > fuzzer.output 2>&1"; + const auto engineStarted = std::chrono::steady_clock::now(); int result = system(command.str().c_str()); + if (this->engineSeconds != nullptr) { + *this->engineSeconds = std::chrono::duration( + std::chrono::steady_clock::now() - + engineStarted) + .count(); + } Map2Check::Log::Warning("Exited fuzzer with " + std::to_string(result)); if (result == 31744) // Timeout gotTimeout = true; @@ -982,13 +1570,8 @@ void Caller::executeAnalysis(std::string solvername) { // afl-fuzz never writes back into -i, so under --seed-exchange its // discoveries are copied into seeds/ -- the previous fuzzer grew that // directory in place. Inputs tagged ",orig:" are the seeds it started - // from, already there. - // - // Caveat, inherited unchanged from v15: seeds/ lives in the scratch - // directory, which the next phase's Caller wipes on construction, so - // this corpus does not yet reach the following KLEE or fuzzer phase. - // Making it survive changes what the hybrid measures, and belongs to - // the smart-seeds work, not to the engine swap. + // from, already there. The store is beside the scratch directory, so + // the next fuzzer phase starts from this corpus plus KLEE's vectors. if (this->seedExchange) { std::error_code queueErr; for (const auto &entry : std::filesystem::directory_iterator( @@ -998,10 +1581,16 @@ void Caller::executeAnalysis(std::string solvername) { if (name.find(",orig:") != std::string::npos) continue; std::filesystem::copy_file( entry.path(), - std::string(Caller::seedDirectory) + "/afl-" + name, + seedStore + "/afl/afl-" + name, std::filesystem::copy_options::skip_existing, queueErr); } } + // The fuzzer's corpus for the KLEE phase, unless this phase already + // decided the property. + if (this->seedExchange && this->feedsKleePhase && + !isWitnessFileCreated()) { + exportFuzzerCorpusAsKtests(); + } Map2Check::Log::Debug("Finished fuzzer"); if (isWitnessFileCreated()) { @@ -1093,12 +1682,41 @@ void Caller::compileCFile(bool is_llvm_bc) { << " -Wno-everything " << " -Winteger-overflow " << " -c -emit-llvm -g" - << " " << Caller::preOptimizationFlags() << " -o " << compiledFile + << " " << Caller::preOptimizationFlags() + << (ssaPreoptimization() ? " -Xclang -disable-O0-optnone" : "") + << " -o " << compiledFile << " " << programHash << "-preprocessed.c " << " > " << programHash << "-clang.out 2>&1"; system(command.str().c_str()); + // MAP2CHECK_PREOPT=ssa: the module in SSA form, as Clam's preprocessing + // leaves it. At -O0 clang marks every function optnone and every local + // lives in memory; KLEE then pays a memory object and a solver array per + // variable. A first probe of --add-invariants found that compiling through + // Clam with NO invariant inserted decided a loop program the plain + // pipeline left UNKNOWN (both the safe and the buggy variant) -- the gain + // was the preprocessing, not the invariants. mem2reg only promotes locals + // whose address is never taken; simplifycfg keeps common code unsunk, as + // Clam does. Neither reorders a call, so the nondet order is unchanged. + if (ssaPreoptimization()) { + std::ostringstream ssa; + ssa << Map2Check::optBinary + << " -passes='function(mem2reg,simplifycfg)'" + << " --simplifycfg-sink-common=false " << compiledFile << " -o " + << compiledFile << ".ssa.bc >> " << programHash << "-clang.out 2>&1"; + std::error_code ssaError; + if (system(ssa.str().c_str()) == 0 && + std::filesystem::exists(compiledFile + ".ssa.bc", ssaError)) { + std::filesystem::rename(compiledFile + ".ssa.bc", compiledFile, + ssaError); + } else { + Map2Check::Log::Warning( + "could not bring the module into SSA form -- analysing it as " + "compiled"); + } + } + this->pathprogram = compiledFile; } else { std::string compiledFile = programHash + "-compiled.bc"; @@ -1210,15 +1828,69 @@ void Caller::compileWithClam() { // map2check_crab_assume, which the runtime forwards to klee_assume -- so // nothing downstream needs to change. // See docs/reports/2026-08-16-crabllvm-review.md. - command << Map2Check::clamBinary() << " -o " << compiledFile << " -m 64 -g" + // MAP2CHECK_CLAM_PROFILE=memory: the configuration --add-invariants had + // until 2018-10-19, when it last reached KLEE -- memory contents tracked + // (crab-llvm's --crab-track=arr, Clam's mem) and an invariant after every + // load. From v7.3 on it ran --crab-promote-assume, which emits llvm.assume, + // which NonDetPass does not map and both KLEE 2.1 and 3.1 ignore: the + // invariants of the SV-COMP 2019/2020 builds reached nothing. Measured side + // by side against the default (num, block-entry) before choosing. + // MAP2CHECK_CLAM_PROFILE=none: Clam's pipeline without inserting anything, + // to tell the effect of compiling through Clam from that of the invariants + // (a first probe found the two pulling in opposite directions). + const char *profileEnv = std::getenv("MAP2CHECK_CLAM_PROFILE"); + const std::string profile = profileEnv != nullptr ? profileEnv : "default"; + const bool memoryProfile = profile == "memory"; + const bool noInvariants = profile == "none"; + // Bounded like the slicer: on the eca-* and product-lines programs Clam's + // analysis ran past the whole budget and the run was killed with no verdict + // (R25: 4-7 ERROR per arm). Past the bound, the fallback below compiles the + // program without invariants. + const unsigned clamBudget = static_cast(std::max( + 1.0, std::min(0.2 * this->timeout, + static_cast(remainingSeconds()) - 5.0))); + command << "timeout -k " << Map2Check::killGracePeriod << " " << clamBudget + << " " << Map2Check::clamBinary() << " -o " << compiledFile + << " -m 64 -g" << " --crab-inter" - << " --crab-track=num" - << " --crab-opt=add-invariants" - << " --crab-opt-invariants-loc=block-entry" - << " " << programHash << "-preprocessed.c "; + << (memoryProfile ? " --crab-track=mem" : " --crab-track=num") + << (noInvariants ? " --crab-opt=none" : " --crab-opt=add-invariants") + << (noInvariants ? "" + : memoryProfile ? " --crab-opt-invariants-loc=after-load" + : " --crab-opt-invariants-loc=block-entry") + << " " << programHash << "-preprocessed.c > clam.output 2>&1"; Map2Check::Log::Debug(command.str()); - system(command.str().c_str()); + const int clamResult = system(command.str().c_str()); + + std::error_code error; + if (clamResult != 0 || !std::filesystem::exists(compiledFile, error) || + std::filesystem::file_size(compiledFile, error) == 0) { + // Not the silence of the old path (issue #54): said, and the run goes on + // with the program as it is. + Map2Check::Log::Warning( + "Clam failed (status " + std::to_string(clamResult) + + ") -- analysing the program without invariants"); + compileCFile(false); + return; + } + + // How many invariants went in: the measure of what --add-invariants does. + std::ostringstream disassemble; + disassemble << Map2Check::optBinary << " -S " << compiledFile + << " -o clam-invariants.ll > /dev/null 2>&1"; + unsigned invariants = 0; + if (system(disassemble.str().c_str()) == 0) { + std::ifstream ir("clam-invariants.ll"); + std::string line; + while (std::getline(ir, line)) { + if (line.find("call void @verifier.assume") != std::string::npos) { + ++invariants; + } + } + } + Map2Check::Log::Info("Clam inserted " + std::to_string(invariants) + + " invariant(s) (" + profile + " profile)"); this->pathprogram = compiledFile; } diff --git a/modules/frontend/caller.hpp b/modules/frontend/caller.hpp index eba63101d..49a2530f0 100644 --- a/modules/frontend/caller.hpp +++ b/modules/frontend/caller.hpp @@ -93,9 +93,14 @@ class Caller { * Sizing each phase against what is LEFT keeps the sum inside the budget * however many phases there turn out to be. */ unsigned remainingSeconds() const; + /** remainingSeconds for a budget of `timeout`, without a Caller: what main + * sizes the alternating phases with. */ + static unsigned remainingOf(unsigned timeout); /** @brief Function to compile original C file removing external memory * operations calls */ void compileCFile(bool is_llvm_bc); + /** MAP2CHECK_PREOPT=ssa: compile into SSA form (see compileCFile). */ + bool ssaPreoptimization() const; /** Compiles the input through Clam so the emitted bitcode carries * verifier.assume(invariant) calls. Requires Clam dev16 installed; callers @@ -119,6 +124,11 @@ class Caller { /** Remove generated files for verification */ void cleanGarbage(); + /** Back to the directory map2check was started in, without deleting the + * scratch directory: under --debug the scratch is kept, but the next hybrid + * phase must still start from the same place (the seed store is computed + * from it). */ + void restoreWorkingDirectory(); /** Slice the program with respect to the target before analysing it. * @@ -156,22 +166,26 @@ class Caller { * is a separate decision that has to be earned by its own measurement. */ bool seedExchange = false; - /** Directory the two engines use to hand each other input vectors. - * - * A directory of files rather than a value passed from one phase to the - * next, meant to survive between phases, runs and alternations -- which is - * what time-slicing will need. AFL++ starts from it and its discoveries are - * copied back in after each fuzzer phase (afl-fuzz never writes into its -i - * dir); the KLEE phase drops its own path vectors in. - * - * NOT yet true across phases (same as v15): it sits inside the scratch - * directory, which each phase's Caller recreates empty. Fixing that is part - * of the smart-seeds work (tacasv2/v3), since it changes what the hybrid - * measures. - * - * Relative, because both engines run with the scratch directory as their - * working directory. */ - static constexpr const char* seedDirectory = "seeds"; + /** The seed store, beside the scratch directory: /.seeds with + * afl/ (fuzzer inputs), ktest/ (KLEE seeds) and replay/ (where queue entries + * are replayed). Beside, not inside: every hybrid phase recreates the scratch + * directory, and a store inside it never reached the next phase. Used only + * under --seed-exchange. */ + std::string seedStore; + /** Set by main on the hybrid's first phase: the fuzzer corpus is converted + * into KLEE seeds only when a KLEE phase follows. After the last phase the + * replays would be pure cost against a spent budget. */ + bool feedsKleePhase = false; + const std::string& seedStorePath() const { return seedStore; } + + /** Slices kept across the phases of one run (/.slice); see + * Map2Check::sliceCachePath. Removed by main with the seed store. */ + std::string sliceCache; + const std::string& sliceCachePath() const { return sliceCache; } + /** AFL++ binaries kept across the phases of one run (/.build), + * keyed by the content of the modules they are built from. */ + std::string buildCache; + const std::string& buildCachePath() const { return buildCache; } /** Writes KLEE's per-path vectors into the seed corpus. * @@ -180,12 +194,34 @@ class Caller { * fuzzer down the same path. Returns how many seeds were written. */ unsigned exportKleeVectorsAsSeeds(); - /** Writes what the fuzzer consumed as a .ktest KLEE can start from. - * - * The nondet log is the only record of a fuzzer run carrying both value and - * type, which is what a .ktest needs. Returns the path, or empty. */ - std::string exportFuzzerVectorAsKtest(); - + /** Set by main under --alternate-engines (tacas 3b): the most this phase's + * engine may run, in seconds, instead of its fixed share of the budget (0: + * the fixed shares). */ + double engineWindow = 0; + /** Seconds without new coverage after which the engine is stopped (0: never). + * AFL++ gets it as AFL_EXIT_ON_TIME; KLEE is watched through run.stats. */ + unsigned stagnationLimit = 0; + /** Whether this phase's KLEE was stopped for stagnating: incomplete. */ + bool stoppedOnStagnation = false; + /** Where to report how long this phase's engine ran (main sizes the next + * alternating phase with it); null: not reported. */ + double* engineSeconds = nullptr; + + /** At most this many fuzzer queue entries are converted into KLEE seeds. */ + static constexpr size_t kMaxSeedsFromFuzzer = 64; + + /** Converts the AFL++ queue into typed .ktest seeds for the KLEE phase, by + * replaying each entry through the witness binary inside the seed store's + * replay/ directory. Returns how many seeds were written. */ + unsigned exportFuzzerCorpusAsKtests(); + + /** The fuzzer's corpus as test-case vectors (Cover-Branches): at most `cap` + * queue entries, ranked as for KLEE, each replayed through the witness + * binary for the values it actually reads, duplicates dropped. Bounded like + * the KLEE export (5% of the budget). Empty when no fuzzer ran. */ + std::vector> fuzzerCorpusVectors(size_t cap); + + /** Instrument and execute nondeterministic generator */ void applyNonDetGenerator(); @@ -216,6 +252,25 @@ class Caller { bool runSlicer(const std::string& input, const std::string& output, std::vector primary, bool addRuntimeNames, const std::string& entry, const std::string& label); + /** runSlicer without the slice cache: what actually calls sbt-slicer. */ + bool runSlicerUncached(const std::string& input, const std::string& output, + std::vector primary, + bool addRuntimeNames, const std::string& entry, + const std::string& label); + /** Applies MAP2CHECK_SLICE_CLEANUP to a fresh slice, in place; on failure + * the slice is kept as the slicer wrote it. */ + void cleanUpSlice(const std::string& slice); + /** Runs the KLEE command, stopping it (SIGINT) once it stagnates for + * stagnationLimit seconds; plain system() when the limit is 0 or the build + * has no SQLite to read KLEE's stats with. Returns system()'s status. */ + int runKleeWatched(const std::string& command); + /** Runs KLEE's vectors natively through the fuzzer's witness binary (from + * the build cache), each completed with zeros past its end; true when one + * reached a violation, whose files are then in the scratch directory. */ + bool replayKleeVectorsForViolation(); + /** Keeps KLEE's latest tests (at most kMaxSeedsFromFuzzer) in the seed + * store's kleeprev/, to seed its next turn. */ + void keepKleeTestsAsSeeds(); }; } // namespace Map2Check diff --git a/modules/frontend/map2check.cpp b/modules/frontend/map2check.cpp index 00bb36320..25ca47dde 100644 --- a/modules/frontend/map2check.cpp +++ b/modules/frontend/map2check.cpp @@ -16,6 +16,7 @@ #include "map2check.hpp" #include +#include #include #include #include @@ -32,6 +33,7 @@ #include "test_suite/ktest_reader.hpp" #include "test_suite/test_suite.hpp" #include "utils/gen_crypto_hash.hpp" +#include "utils/alternation.hpp" #include "utils/log.hpp" #include "utils/sha256.hpp" #include "witness/witness_include.hpp" @@ -150,7 +152,8 @@ void emitTestSuite(const std::string &outputDir, const std::string &programFile, const std::string &entryFunction, const std::string &architecture, const std::string &specification, bool foundViolation, - bool coverBranches, Map2Check::Map2CheckMode mode) { + bool coverBranches, Map2Check::Map2CheckMode mode, + const std::vector> &fuzzerVectors) { Map2Check::TestSuiteMetadata metadata; metadata.producer = std::string("Map2Check ") + Map2CheckVersion; metadata.specification = specification; @@ -176,19 +179,45 @@ void emitTestSuite(const std::string &outputDir, const std::string &programFile, // coversError is false throughout: these vectors are paths, not violations. // The violating one, when there is one, is still in klee_log.csv and still // goes out under Cover-Error. + // + // The cap is on the SUITE, not on this phase: with the engines alternating, + // every KLEE phase adds cases, and later phases replay the vectors earlier + // ones already wrote (seeds) -- those are skipped. if (coverBranches) { + // The fuzzer's share first, at most half the suite, so KLEE's paths still + // find room: its corpus is ranked by new edges, the cases a coverage + // metric rewards by construction (on by default; MAP2CHECK_FUZZER_SUITE=0). + size_t fromFuzzer = 0; + for (const std::vector &inputs : fuzzerVectors) { + if (writer.caseCount() >= kMaxBranchTestCases / 2) break; + if (writer.hasTestCase(inputs)) continue; + if (!writer.writeTestCase(inputs, false)) { + Map2Check::Log::Warning("could not write test case to " + outputDir); + return; + } + ++fromFuzzer; + } + if (!fuzzerVectors.empty()) { + Map2Check::Log::Info("Test suite: " + std::to_string(fromFuzzer) + + " test cases from the fuzzer's corpus"); + } + constexpr size_t kMaxKtestsRead = 5000; std::vector> vectors = - Map2Check::readKtestVectors(Map2Check::kleeOutputDir, - kMaxBranchTestCases); + Map2Check::readKtestVectors(Map2Check::kleeOutputDir, kMaxKtestsRead); + size_t written = 0; for (const std::vector &inputs : vectors) { + if (writer.caseCount() >= kMaxBranchTestCases) break; + if (writer.hasTestCase(inputs)) continue; if (!writer.writeTestCase(inputs, false)) { Map2Check::Log::Warning("could not write test case to " + outputDir); return; } + ++written; } Map2Check::Log::Info("Test suite written to " + outputDir + " (" + - std::to_string(vectors.size()) + - " test cases from KLEE paths)"); + std::to_string(written) + + " test cases from KLEE paths, " + + std::to_string(writer.caseCount()) + " in the suite)"); return; } @@ -405,6 +434,16 @@ struct map2check_args { bool generateTestSuite = false; bool coverBranches = false; bool seedExchange = false; + // 1..3 on the hybrid path (fuzzer, KLEE, fuzzer), 0 for a single engine. + int phase = 0; + // --alternate-engines (tacas 3b): the engines take turns, each phase bounded + // by its window and stopped when it stagnates. 0 keeps the fixed shares. + bool alternateEngines = false; + double engineWindow = 0; + unsigned stagnationLimit = 0; + // Whether this phase's fuzzer corpus is converted into seeds for a KLEE + // phase that follows; -1: the fixed hybrid's rule (the first phase only). + int feedsKlee = -1; bool sliceProgram = false; std::string testSuiteDir = "test-suite"; std::string propertyFile; @@ -414,6 +453,78 @@ struct map2check_args { }; bool foundViolation = false; +// Set when a phase proved the property (TRUE). Like a violation, a proof is +// the run's answer: no later phase may run and print a verdict after it. +bool provedSafe = false; +// The seed store of the last phase, removed by main once every phase ran. +static std::string lastSeedStore; +// The slice cache of the last phase, removed by main with the seed store. +static std::string lastSliceCache; +// The AFL++ build cache of the last phase, removed by main likewise. +static std::string lastBuildCache; +// How long the last phase's engine ran; the rest of the phase is setup +// (compile, instrument, link) that no engine window accounts for. +static double lastEngineSeconds = 0; + +int map2check_execution(map2check_args args); + +/** The hybrid under --alternate-engines (tacas 3b spec): the fuzzer and KLEE + * take turns, fuzzer first, until a violation, a proof, or too little time + * for another phase. Each phase is bounded by its window -- doubled every + * round of that engine -- and ends earlier when its engine stagnates, handing + * the rest back. The fixed 0.2/0.6/0.2 split held an engine that had stopped + * progressing to the end of its share, and cut one that still was. */ +int alternateEngines(map2check_args args) { + const double budget = args.timeout; + const unsigned quiet = Map2Check::stagnationSeconds(budget); + unsigned rounds[2] = {0, 0}; + // The setup each engine's phase needed last time (compile, instrument, + // link -- time no window covers): a phase starts only if what is left + // covers its setup plus a stagnation period of engine time, and its window + // leaves the setup out. Per engine and latest, not the maximum: the first + // fuzzer phase builds the AFL++ binaries, the later ones reuse them. + double setup[2] = {0, 0}; + for (int phase = 1;; ++phase) { + const bool klee = (phase % 2 == 0); + const int self = klee ? 1 : 0; + const double left = Map2Check::Caller::remainingOf(args.timeout); + if (phase > 1 && left < quiet + setup[self]) break; + const Map2Check::Engine engine = + klee ? Map2Check::Engine::Klee : Map2Check::Engine::Fuzzer; + const unsigned round = ++rounds[self]; + args.generator = klee ? Map2Check::NonDetGenerator::Klee + : Map2Check::NonDetGenerator::AFLPlusPlus; + args.phase = phase; + args.engineWindow = Map2Check::alternationWindow( + engine, round, budget, std::max(1.0, left - setup[self])); + // Both engines' patience grows with their rounds. KLEE: coverage stops + // rising well before it finishes the paths of a proof. The fuzzer: on the + // eca-* state machines it finds new paths in bursts, and a fixed 15 s cut + // ended its turns at ~17 s where the fixed split gave it 60. + args.stagnationLimit = Map2Check::stagnationSeconds(budget, round); + // Replaying the corpus for a KLEE phase that will not get to run is + // pure cost. + args.feedsKlee = (!klee && left - setup[self] - args.engineWindow >= + quiet + setup[1]) + ? 1 + : 0; + Map2Check::Log::Info("Alternation phase " + std::to_string(phase) + ": " + + (klee ? "KLEE" : "AFL++") + ", window " + + std::to_string(static_cast( + args.engineWindow)) + " s"); + const auto started = std::chrono::steady_clock::now(); + lastEngineSeconds = 0; + const int result = map2check_execution(args); + if (result != SUCCESS) return result; + const double took = std::chrono::duration( + std::chrono::steady_clock::now() - started) + .count(); + setup[self] = std::max(0.0, took - lastEngineSeconds); + if (foundViolation || provedSafe) break; + } + return SUCCESS; +} + int map2check_execution(map2check_args args) { Map2Check::Log::Info("Started Map2Check"); // TODO(rafa.sa.xp@gmail.com): Check current mode @@ -479,6 +590,44 @@ int map2check_execution(map2check_args args) { generator); caller->c_program_fullpath = args.inputFile; caller->seedExchange = args.seedExchange; + // The store is named after the program's content, so one left by an earlier + // run (kept by --debug, or leaked by a kill) would feed that run's seeds into + // this one: every run starts from an empty store. + if (args.seedExchange && args.phase <= 1) { + std::error_code storeError; + std::filesystem::remove_all(caller->seedStorePath(), storeError); + } + // The slice cache likewise: a slice left by an earlier run is keyed by + // content and would be correct, but a ".failed" mark from a run with a + // shorter budget would refuse this one a slice it could afford. + if (args.sliceProgram && args.phase <= 1) { + std::error_code cacheError; + std::filesystem::remove_all(caller->sliceCachePath(), cacheError); + } + if (args.phase <= 1) { + std::error_code cacheError; + std::filesystem::remove_all(caller->buildCachePath(), cacheError); + } + // A run starts from an empty suite. Its phases then add to it (see + // TestSuiteWriter), and a suite left in this directory by an earlier run -- + // possibly of another program -- must not be added to. + if (args.generateTestSuite && args.phase <= 1) { + std::string suiteDir = args.testSuiteDir; + if (!fs::path(suiteDir).is_absolute()) { + suiteDir = caller->getOriginalPath() + "/" + suiteDir; + } + Map2Check::TestSuiteWriter::removeTestCases(suiteDir); + } + // Recorded now, not at the end: an exception in this phase must not leak + // the store or the slice cache past the cleanup in main. + lastSeedStore = caller->seedStorePath(); + lastSliceCache = caller->sliceCachePath(); + lastBuildCache = caller->buildCachePath(); + caller->engineSeconds = &lastEngineSeconds; + caller->feedsKleePhase = + args.feedsKlee >= 0 ? (args.feedsKlee == 1) : (args.phase == 1); + caller->engineWindow = args.engineWindow; + caller->stagnationLimit = args.stagnationLimit; caller->sliceProgram = args.sliceProgram; caller->setTimeout(args.timeout); caller->entryFunction = args.entryFunction; @@ -665,6 +814,7 @@ int map2check_execution(map2check_args args) { } else { Map2Check::Log::Info(""); Map2Check::Log::Info("VERIFICATION SUCCEEDED"); + provedSafe = true; if (args.generateWitness) generate_witness(args.inputFile, propertyViolated, args.spectTrue); } @@ -707,11 +857,23 @@ int map2check_execution(map2check_args args) { if (!fs::path(outputDir).is_absolute()) { outputDir = caller->getOriginalPath() + "/" + outputDir; } + // Cover-Branches used only KLEE's paths: the fuzzer's corpus, the inputs + // that reached new edges, was thrown away with the scratch directory. + // On by default since 9.0 (R22: 49.7% against 44.7% on the fixed hybrid; + // R26: 53.5% with the alternation); MAP2CHECK_FUZZER_SUITE=0 turns it off. + std::vector> fuzzerVectors; + const char *fuzzerSuite = std::getenv("MAP2CHECK_FUZZER_SUITE"); + if (args.coverBranches && + !(fuzzerSuite != nullptr && std::string(fuzzerSuite) == "0") && + generator == Map2Check::NonDetGenerator::AFLPlusPlus) { + fuzzerVectors = caller->fuzzerCorpusVectors(kMaxBranchTestCases); + } emitTestSuite(outputDir, caller->c_program_fullpath, args.entryFunction, args.architecture, resolveSpecification(args.propertyFile, caller->getOriginalPath(), args.mode), - foundViolation, args.coverBranches, args.mode); + foundViolation, args.coverBranches, args.mode, + fuzzerVectors); } // (6) Clean map2check execution (folders and temp files) @@ -720,9 +882,12 @@ int map2check_execution(map2check_args args) { // nondet log -- and deleting it unconditionally makes the pipeline // impossible to inspect after the fact. Debug runs are already opting into // verbosity and disk use. + lastSeedStore = caller->seedStorePath(); + lastSliceCache = caller->sliceCachePath(); if (args.debugMode) { Map2Check::Log::Info("Debug mode: keeping temp files in " + caller->getScratchDir()); + caller->restoreWorkingDirectory(); } else { Map2Check::Log::Debug("Removing temp files"); caller->cleanGarbage(); @@ -776,9 +941,17 @@ z3 (Z3 is default), btor (Boolector), and yices2 (Yices))") "the assertions (--check-asserts) or the runtime checks (--memtrack, " "--memcleanup-property, --check-overflow) before analysing it; needs " "sbt-slicer") + ("alternate-engines", + "\tthe default hybrid (needs --timeout): the fuzzer and KLEE take " + "turns, each stopped once it stops finding coverage, with windows " + "that double every round, handing each other seeds") + ("fixed-hybrid", + "\tthe 8.x hybrid instead: the fuzzer for 0.2 of the budget, then " + "KLEE (with --seed-exchange: 0.2 / 0.6 / 0.2 and a last fuzzer phase)") ("seed-exchange", "\tlet the two engines hand each other input vectors through a shared " - "seed corpus (hybrid runs; off by default)") + "seed corpus (implied by the default hybrid; with --fixed-hybrid, off " + "unless given)") ("cover-branches", "\temit one test case per path KLEE explored, from its .ktest output, " "instead of the single violating vector (Test-Comp Cover-Branches)") @@ -894,6 +1067,33 @@ z3 (Z3 is default), btor (Boolector), and yices2 (Yices))") if (vm.count("seed-exchange")) { args.seedExchange = true; } + // The hybrid is the alternation by default since 9.0: measured on the + // 213-task Cover-Error sample it ties the seed-exchange hybrid (157 each, + // against 128 for the 8.x fixed hybrid) and leads Cover-Branches (53.5% + // against 46.5%, R26). --fixed-hybrid keeps the 8.x schedule. + const bool hybrid = !vm.count("nondet-generator"); + const bool budgeted = + vm.count("timeout") && vm["timeout"].as() > 0; + if (vm.count("fixed-hybrid")) { + if (vm.count("alternate-engines")) { + Map2Check::Log::Warning( + "--fixed-hybrid and --alternate-engines both given -- using the " + "fixed hybrid"); + } + } else if (hybrid && budgeted) { + args.alternateEngines = true; + args.seedExchange = true; + } else if (vm.count("alternate-engines")) { + // Windows and stagnation are fractions of the budget, and turns only + // exist on the hybrid path: without either, say so instead of running + // something else under the flag's name. + Map2Check::Log::Warning( + !budgeted ? "--alternate-engines needs --timeout: its windows are " + "fractions of the budget -- running the fixed hybrid " + "instead" + : "--alternate-engines applies to the hybrid only -- " + "ignored with --nondet-generator"); + } if (vm.count("cover-branches")) { args.coverBranches = true; // The mode has to change too, not just the emitter. Without this the run @@ -974,14 +1174,39 @@ z3 (Z3 is default), btor (Boolector), and yices2 (Yices))") // std::cout << pathfile << std::endl; fs::path absolute_path = fs::absolute(pathfile); args.inputFile = absolute_path.string(); + // The store outlives the phases, not the run: removed on every way out + // of this block (returns and exceptions alike), unless --debug keeps it. + struct SeedStoreCleanup { + const map2check_args &args; + ~SeedStoreCleanup() { + if (args.seedExchange && !args.debugMode && !lastSeedStore.empty()) { + std::error_code storeError; + std::filesystem::remove_all(lastSeedStore, storeError); + } + if (args.sliceProgram && !args.debugMode && !lastSliceCache.empty()) { + std::error_code cacheError; + std::filesystem::remove_all(lastSliceCache, cacheError); + } + if (!args.debugMode && !lastBuildCache.empty()) { + std::error_code cacheError; + std::filesystem::remove_all(lastBuildCache, cacheError); + } + } + } seedStoreCleanup{args}; + if (args.generator == Map2Check::NonDetGenerator::None && + args.alternateEngines) { + return alternateEngines(args); + } if(args.generator == Map2Check::NonDetGenerator::None) { args.generator = Map2Check::NonDetGenerator::AFLPlusPlus; + args.phase = 1; int result = map2check_execution(args); if (result != SUCCESS) { return result; } if (!foundViolation) { args.generator = Map2Check::NonDetGenerator::Klee; + args.phase = 2; result = map2check_execution(args); if (result != SUCCESS) { return result; @@ -1000,8 +1225,9 @@ z3 (Z3 is default), btor (Boolector), and yices2 (Yices))") // Behind the flag: the hybrid was measured at 45% covered over 372 // tasks in its current shape, and that number should keep meaning what // it means until this one is measured beside it. - if (args.seedExchange && !foundViolation) { + if (args.seedExchange && !foundViolation && !provedSafe) { args.generator = Map2Check::NonDetGenerator::AFLPlusPlus; + args.phase = 3; result = map2check_execution(args); if (result != SUCCESS) { return result; diff --git a/modules/frontend/test_suite/ktest_reader.cpp b/modules/frontend/test_suite/ktest_reader.cpp index 9bbf55703..e9c80c233 100644 --- a/modules/frontend/test_suite/ktest_reader.cpp +++ b/modules/frontend/test_suite/ktest_reader.cpp @@ -318,6 +318,59 @@ bool kleeHaltedOnTimer(const std::string& kleeOutDir) { return false; } +std::string kleeDroppedPaths(const std::string& kleeOutDir) { + if (kleeHaltedOnTimer(kleeOutDir)) return "halted on its timer"; + + const std::filesystem::path dir(kleeOutDir); + std::string line; + std::ifstream warnings((dir / "warnings.txt").string()); + while (std::getline(warnings, line)) { + if (line.find("silently concretizing") != std::string::npos) { + return "concretized a symbolic value"; + } + // Near --max-memory KLEE stops forking and follows one side of each + // branch at random, or kills states outright; either way it can still + // empty its queue and exit 0. + if (line.find("skipping fork") != std::string::npos || + line.find("over memory cap") != std::string::npos) { + return "hit its memory cap"; + } + } + + // KLEE that died (a solver crash, an LLVM assertion, the OOM killer) writes + // none of the marks below and no "done" lines -- while the paths it did + // finish may have written NONE to the property file. + bool finished = false; + std::ifstream info((dir / "info").string()); + while (std::getline(info, line)) { + if (line.find("KLEE: done: completed paths") != std::string::npos) { + finished = true; + break; + } + } + if (!finished) return "did not finish its run"; + + // A state KLEE killed leaves a test with the reason: ..err for + // an error (a model limit, a memory error, an abort that halted the search), + // .early for an early termination (memory cap, depth, ...). Not + // "partially completed paths" in info: that counts the paths an assumption + // pruned too, and read that way no program with an assume_abort_if_not + // could ever be proved. + std::error_code error; + for (const auto& entry : std::filesystem::directory_iterator(dir, error)) { + const std::string name = entry.path().filename().string(); + auto endsWith = [&name](const std::string& suffix) { + return name.size() > suffix.size() && + name.compare(name.size() - suffix.size(), suffix.size(), + suffix) == 0; + }; + if (endsWith(".err") || endsWith(".early")) { + return "terminated states early (" + name + ")"; + } + } + return ""; +} + std::vector> readKtestVectors( const std::string& kleeOutDir, size_t limit) { std::vector> vectors; @@ -402,14 +455,17 @@ std::vector readNonDetLogAsObjects(const std::string& csvPath) { if (fields.size() < 7) continue; const std::string& value = fields[5]; + // KLEE matches a seed's objects to its inputs by POSITION: a read this + // cannot express (pchar, loff_t, sector_t, or a malformed row) ends the + // seed here. Skipping it shifted every later value onto the wrong input. int type = 0; try { type = std::stoi(fields[6]); } catch (const std::exception&) { - continue; + break; } const NonDetTypeInfo info = nonDetTypeInfo(type); - if (info.name == nullptr) continue; + if (info.name == nullptr) break; KtestObject object; object.name = info.name; diff --git a/modules/frontend/test_suite/ktest_reader.hpp b/modules/frontend/test_suite/ktest_reader.hpp index f9d18febb..f6ee77099 100644 --- a/modules/frontend/test_suite/ktest_reader.hpp +++ b/modules/frontend/test_suite/ktest_reader.hpp @@ -87,6 +87,23 @@ bool hasViolatingKtest(const std::string& kleeOutDir); * NONE to the property file made a reachable null dereference read as TRUE. */ bool kleeHaltedOnTimer(const std::string& kleeOutDir); +/** Why KLEE's exploration was not exhaustive, or empty if it was. + * + * KLEE exits 0 whenever its state queue empties, and that is a proof only if + * no path was dropped on the way. Three ways to drop them, all exit 0: + * - the HaltTimer (see kleeHaltedOnTimer); + * - a symbolic input concretized ("silently concretizing" in warnings.txt): + * a nondet double pinned to 0 left one path and answered TRUE + * (float-benchs/sin_interpolated_index-1); + * - states KLEE killed with its own errors or early exits (a *.err or + * *.early test): a VLA of symbolic size did that in + * loops/insertion_sort-1-2, also answered TRUE. + * Also: KLEE hitting its memory cap ("skipping fork", "over memory cap"), and + * a KLEE that never finished (no "done: completed paths" in info -- a crash). + * A path pruned by an assumption is none of these: it ends in + * klee_silent_exit and leaves no file. */ +std::string kleeDroppedPaths(const std::string& kleeOutDir); + /** Every input vector KLEE recorded under `kleeOutDir`, one per .ktest. * * Ordered by file name, which is KLEE's own path numbering: stable across diff --git a/modules/frontend/test_suite/test_suite.cpp b/modules/frontend/test_suite/test_suite.cpp index 488031a99..188ee753b 100644 --- a/modules/frontend/test_suite/test_suite.cpp +++ b/modules/frontend/test_suite/test_suite.cpp @@ -8,6 +8,7 @@ #include "test_suite.hpp" +#include #include #include #include @@ -95,7 +96,75 @@ std::vector readNonDetLog(const std::string& csvPath) { } TestSuiteWriter::TestSuiteWriter(std::string directory) - : directory(std::move(directory)), counter(0) {} + : directory(std::move(directory)), counter(0) { + // After the cases already there: with the engines alternating, more than one + // phase writes into the same suite, and counting from 1 again overwrote the + // earlier phase's cases (tacas 3b spec). + std::error_code ec; + for (const auto& entry : + std::filesystem::directory_iterator(this->directory, ec)) { + const std::string name = entry.path().filename().string(); + static const std::string kPrefix = "testcase-"; + static const std::string kSuffix = ".xml"; + if (name.size() <= kPrefix.size() + kSuffix.size() || + name.compare(0, kPrefix.size(), kPrefix) != 0 || + name.compare(name.size() - kSuffix.size(), kSuffix.size(), kSuffix) != + 0) { + continue; + } + const std::string digits = name.substr( + kPrefix.size(), name.size() - kPrefix.size() - kSuffix.size()); + if (digits.empty() || digits.size() > 9 || + digits.find_first_not_of("0123456789") != std::string::npos) { + continue; + } + this->counter = std::max( + this->counter, static_cast(std::stoul(digits))); + // Its inputs, as written (escaped), so a later phase can skip a vector + // the suite already has. + std::ifstream in(entry.path()); + std::stringstream text; + text << in.rdbuf(); + const std::string xml = text.str(); + std::vector inputs; + static const std::string kOpen = "", kClose = ""; + for (size_t at = xml.find(kOpen); at != std::string::npos; + at = xml.find(kOpen, at)) { + const size_t end = xml.find(kClose, at + kOpen.size()); + if (end == std::string::npos) break; + inputs.push_back(xml.substr(at + kOpen.size(), end - at - kOpen.size())); + at = end + kClose.size(); + } + this->cases.insert(inputs); + } +} + +namespace { +std::vector escapedInputs(const std::vector& raw) { + std::vector escaped; + escaped.reserve(raw.size()); + for (const std::string& value : raw) escaped.push_back(escapeXml(value)); + return escaped; +} +} // namespace + +bool TestSuiteWriter::hasTestCase( + const std::vector& inputs) const { + return this->cases.count(escapedInputs(inputs)) > 0; +} + +void TestSuiteWriter::removeTestCases(const std::string& directory) { + std::error_code ec; + std::vector doomed; + for (const auto& entry : std::filesystem::directory_iterator(directory, ec)) { + const std::string name = entry.path().filename().string(); + if (name.rfind("testcase-", 0) == 0 && name.size() > 13 && + name.compare(name.size() - 4, 4, ".xml") == 0) { + doomed.push_back(entry.path()); + } + } + for (const auto& path : doomed) std::filesystem::remove(path, ec); +} bool TestSuiteWriter::writeMetadata(const TestSuiteMetadata& metadata) { std::error_code ec; @@ -147,6 +216,7 @@ bool TestSuiteWriter::writeTestCase(const std::vector& inputs, out << " " << escapeXml(value) << "\n"; } out << "\n"; + this->cases.insert(escapedInputs(inputs)); out.close(); return out.good(); } diff --git a/modules/frontend/test_suite/test_suite.hpp b/modules/frontend/test_suite/test_suite.hpp index c00007242..8adec3570 100644 --- a/modules/frontend/test_suite/test_suite.hpp +++ b/modules/frontend/test_suite/test_suite.hpp @@ -29,6 +29,7 @@ #ifndef MODULES_FRONTEND_TEST_SUITE_TEST_SUITE_HPP_ #define MODULES_FRONTEND_TEST_SUITE_TEST_SUITE_HPP_ +#include #include #include @@ -65,12 +66,24 @@ class TestSuiteWriter { /** Writes metadata.xml. False if the file could not be written. */ bool writeMetadata(const TestSuiteMetadata& metadata); - /** Writes testcase-.xml, numbering from 1 in call order. */ + /** Writes testcase-.xml, numbering after the cases already in the + * directory (an earlier phase of the same run may have written some). */ bool writeTestCase(const std::vector& inputs, bool coversError); + /** How many test cases the directory holds, written earlier or by this. */ + size_t caseCount() const { return cases.size(); } + /** Whether a test case with exactly these inputs is already there. */ + bool hasTestCase(const std::vector& inputs) const; + + /** Removes every testcase-.xml from `directory` -- run once, at the start + * of a run, so a suite never mixes cases from an earlier run. */ + static void removeTestCases(const std::string& directory); + private: std::string directory; unsigned counter; + /** The inputs of every case in the directory, XML-escaped as written. */ + std::set> cases; }; } // namespace Map2Check diff --git a/modules/frontend/utils/alternation.hpp b/modules/frontend/utils/alternation.hpp new file mode 100644 index 000000000..e9a41663b --- /dev/null +++ b/modules/frontend/utils/alternation.hpp @@ -0,0 +1,75 @@ +/** + * Copyright (C) 2014 - 2026 Map2Check tool + * This file is part of the Map2Check tool, and is made available under + * the terms of the GNU General Public License version 2. + * + * SPDX-License-Identifier: (GPL-2.0) + **/ + +#ifndef MODULES_FRONTEND_UTILS_ALTERNATION_HPP_ +#define MODULES_FRONTEND_UTILS_ALTERNATION_HPP_ + +#include +#include + +namespace Map2Check { + +/** The two engines --alternate-engines takes turns with (tacas 3b spec). */ +enum class Engine { Fuzzer, Klee }; + +/** The most a phase of `engine` may take in its `round`-th turn (1-based): + * 0.1T for the fuzzer and 0.3T for KLEE, doubled every round, never more than + * what is left. The doubling is what lets an engine the alternation did not + * help come back with more time; an engine that stagnates earlier hands the + * rest back at once. */ +inline double alternationWindow(Engine engine, unsigned round, double budget, + double remaining) { + const double base = (engine == Engine::Fuzzer ? 0.1 : 0.3) * budget; + const double window = base * std::pow(2.0, round > 0 ? round - 1 : 0); + return std::min(window, remaining); +} + +/** How long an engine may go without new coverage before it is stagnant: + * 5% of the budget, at least 10 s (15 s at the Test-Comp 300 s). Also the + * least a phase must have left to be worth starting. */ +inline unsigned stagnationSeconds(double budget) { + return static_cast(std::max(10.0, 0.05 * budget)); +} + +/** KLEE's stagnation period in its `round`-th turn: doubled every round, like + * its window. Instruction coverage stops rising well before KLEE finishes the + * paths that make a proof, and a fixed cut would never let it get there. */ +inline unsigned stagnationSeconds(double budget, unsigned round) { + return stagnationSeconds(budget) * + (1u << std::min(round > 0 ? round - 1 : 0, 8u)); +} + +/** Decides from successive coverage samples whether an engine stagnated: no + * increase for `quietSeconds` since the last one. A sample of -1 means the + * reading failed (KLEE's stats database busy or not written yet) and is no + * evidence either way; the clock starts at the first real sample. */ +class CoverageWatch { + public: + explicit CoverageWatch(double quietSeconds) : quiet(quietSeconds) {} + + bool stagnated(long long covered, double now) { + if (covered < 0) return false; + if (!seen || covered > last) { + seen = true; + last = covered; + since = now; + return false; + } + return now - since >= quiet; + } + + private: + double quiet; + bool seen = false; + long long last = 0; + double since = 0; +}; + +} // namespace Map2Check + +#endif // MODULES_FRONTEND_UTILS_ALTERNATION_HPP_ diff --git a/modules/frontend/utils/gen_crypto_hash.cpp b/modules/frontend/utils/gen_crypto_hash.cpp index 1a26c5d1f..b1683c97d 100644 --- a/modules/frontend/utils/gen_crypto_hash.cpp +++ b/modules/frontend/utils/gen_crypto_hash.cpp @@ -38,6 +38,9 @@ int GenHash::generate_sha1_hash_for_file() { std::stringstream ss; std::ifstream file(this->filepath.c_str(), std::ios::binary | std::ios::ate); std::streamsize size = file.tellg(); + // An unreadable file reads as size -1, which std::vector rejected with a + // bare "cannot create std::vector larger than max_size()". + if (!file.is_open() || size < 0) return -1; file.seekg(0, std::ios::beg); std::vector buffer(size); diff --git a/modules/frontend/utils/seed_store.hpp b/modules/frontend/utils/seed_store.hpp new file mode 100644 index 000000000..23efb5219 --- /dev/null +++ b/modules/frontend/utils/seed_store.hpp @@ -0,0 +1,66 @@ +/** + * Copyright (C) 2014 - 2026 Map2Check tool + * This file is part of the Map2Check tool, and is made available under + * the terms of the GNU General Public License version 2. + * + * SPDX-License-Identifier: (GPL-2.0) + **/ + +#ifndef MODULES_FRONTEND_UTILS_SEED_STORE_HPP_ +#define MODULES_FRONTEND_UTILS_SEED_STORE_HPP_ + +#include +#include +#include +#include +#include + +namespace Map2Check { + +/** Where the engines leave seeds for each other under --seed-exchange. + * + * BESIDE the scratch directory, not inside it: every phase of the hybrid + * builds a new Caller, which recreates the scratch directory empty, and a + * store inside it never reached the next phase (tacasv3a spec, defect 1). */ +inline std::string seedStorePath(const std::string& cwd, + const std::string& programHash) { + return cwd + "/" + programHash + ".seeds"; +} + +/** The AFL++ queue entries to hand to KLEE: only real entries ("id:..."), + * those that reached new edges ("+cov") first, each group in queue order -- + * AFL++ zero-pads the id, so lexicographic order is id order, oldest + * (simplest) first -- and at most `cap` of them, so replaying them cannot eat + * the phase (tacas 3c). Not the seeds the fuzzer started from (",orig:"): + * those are KLEE's own vectors or an earlier round's entries, which KLEE + * already has. */ +inline std::vector selectQueueEntries( + std::vector names, size_t cap) { + names.erase(std::remove_if(names.begin(), names.end(), + [](const std::string& name) { + return name.rfind("id:", 0) != 0 || + name.find(",orig:") != std::string::npos; + }), + names.end()); + std::sort(names.begin(), names.end()); + // Ranked: the entries that reached new edges ("+cov" in AFL++'s name) before + // the ones that only changed hit counts, id order kept inside each group. + std::stable_partition(names.begin(), names.end(), [](const std::string& name) { + return name.find(",+cov") != std::string::npos; + }); + if (names.size() > cap) names.resize(cap); + return names; +} + +/** Whether a converted vector is worth a seed: not empty, and not one already + * written -- many queue entries differ only in bytes the program never reads, + * and they replay to the same typed vector. */ +inline bool isNewVector(const std::vector& bytes, + std::set>* seen) { + if (bytes.empty()) return false; + return seen->insert(bytes).second; +} + +} // namespace Map2Check + +#endif // MODULES_FRONTEND_UTILS_SEED_STORE_HPP_ diff --git a/modules/frontend/utils/slicer.hpp b/modules/frontend/utils/slicer.hpp index 2fe1880a8..323c5cdbe 100644 --- a/modules/frontend/utils/slicer.hpp +++ b/modules/frontend/utils/slicer.hpp @@ -10,6 +10,7 @@ #define MODULES_FRONTEND_UTILS_SLICER_HPP_ #include +#include #include #include #include @@ -47,37 +48,43 @@ inline const std::vector& nondetFunctionNames() { return names; } -/** Every __VERIFIER_nondet_* symbol in a module's textual IR (`opt -S`), - * in order of first appearance. The fixed list above cannot know every name a - * benchmark declares (int128, uint128, ...), and a name missing from the - * criteria silently brings the shifted suite back. */ -inline std::vector nondetNamesInIR(const std::string& ir) { - static const std::regex symbol(R"(@(__VERIFIER_nondet_[A-Za-z0-9_]+))"); +/** Every symbol `@...` in a module's textual IR, without the '@', in + * order of first appearance. A plain scan, not std::regex: on the eca-* modules + * (megabytes of IR) the regexes took ~45 s, outside every budget, and pushed + * the run past its deadline with no verdict (R19, 4 ERROR of the slice arm). */ +inline std::vector symbolsWithPrefixInIR(const std::string& ir, + const std::string& prefix) { + auto isNameChar = [](char c) { + return std::isalnum(static_cast(c)) || c == '_'; + }; std::vector names; - for (std::sregex_iterator it(ir.begin(), ir.end(), symbol), end; it != end; - ++it) { - const std::string name = (*it)[1]; - if (std::find(names.begin(), names.end(), name) == names.end()) { + const std::string needle = "@" + prefix; + for (size_t at = ir.find(needle); at != std::string::npos; + at = ir.find(needle, at + 1)) { + size_t end = at + 1; + while (end < ir.size() && isNameChar(ir[end])) ++end; + const std::string name = ir.substr(at + 1, end - at - 1); + if (name.size() > prefix.size() && + std::find(names.begin(), names.end(), name) == names.end()) { names.push_back(name); } } return names; } +/** Every __VERIFIER_nondet_* symbol in a module's textual IR (`opt -S`), + * in order of first appearance. The fixed list above cannot know every name a + * benchmark declares (int128, uint128, ...), and a name missing from the + * criteria silently brings the shifted suite back. */ +inline std::vector nondetNamesInIR(const std::string& ir) { + return symbolsWithPrefixInIR(ir, "__VERIFIER_nondet_"); +} + /** Every map2check_* runtime symbol in a module's textual IR, in order of * first appearance. Used as the slicing criteria for the memory properties: * the property is decided by these calls, so none of them may be removed. */ inline std::vector runtimeNamesInIR(const std::string& ir) { - static const std::regex symbol(R"(@(map2check_[A-Za-z0-9_]+))"); - std::vector names; - for (std::sregex_iterator it(ir.begin(), ir.end(), symbol), end; it != end; - ++it) { - const std::string name = (*it)[1]; - if (std::find(names.begin(), names.end(), name) == names.end()) { - names.push_back(name); - } - } - return names; + return symbolsWithPrefixInIR(ir, "map2check_"); } /** Every function a module DECLARES without defining (`declare ... @f(`), in @@ -87,24 +94,38 @@ inline std::vector runtimeNamesInIR(const std::string& ir) { * the runtime checks depends on such a call, so without it as a criterion the * slicer drops the call and the bug with it (CASTLE-787-2: a wrong TRUE). */ inline std::vector externalNamesInIR(const std::string& ir) { - static const std::regex declaration( - R"((?:^|\n)declare [^\n]*?@([A-Za-z0-9_.$]+)\()"); + auto isNameChar = [](char c) { + return std::isalnum(static_cast(c)) || c == '_' || + c == '.' || c == '$'; + }; std::vector names; - for (std::sregex_iterator it(ir.begin(), ir.end(), declaration), end; - it != end; ++it) { - const std::string name = (*it)[1]; - // Intrinsics are not calls into code the slicer could keep -- except the - // memory ones: clang lowers memcpy/memset/memmove (and struct copies) to - // them, and an overflowing copy into a buffer nothing reads again feeds no - // criterion, so it has to be one (the strcpy case again). - if (name.rfind("llvm.", 0) == 0 && name.rfind("llvm.memcpy.", 0) != 0 && - name.rfind("llvm.memmove.", 0) != 0 && - name.rfind("llvm.memset.", 0) != 0) { - continue; - } - if (std::find(names.begin(), names.end(), name) == names.end()) { - names.push_back(name); + size_t line = 0; + while (line < ir.size()) { + size_t next = ir.find('\n', line); + if (next == std::string::npos) next = ir.size(); + if (ir.compare(line, 8, "declare ") == 0) { + const size_t at = ir.find('@', line); + if (at != std::string::npos && at < next) { + size_t end = at + 1; + while (end < next && isNameChar(ir[end])) ++end; + if (end < next && ir[end] == '(') { + const std::string name = ir.substr(at + 1, end - at - 1); + // Intrinsics are not calls into code the slicer could keep -- except + // the memory ones: clang lowers memcpy/memset/memmove (and struct + // copies) to them, and an overflowing copy into a buffer nothing + // reads again feeds no criterion, so it has to be one. + const bool intrinsic = name.rfind("llvm.", 0) == 0 && + name.rfind("llvm.memcpy.", 0) != 0 && + name.rfind("llvm.memmove.", 0) != 0 && + name.rfind("llvm.memset.", 0) != 0; + if (!intrinsic && + std::find(names.begin(), names.end(), name) == names.end()) { + names.push_back(name); + } + } + } } + line = next + 1; } return names; } @@ -224,6 +245,56 @@ inline std::string describeSlice(const std::string& criterion, return text.str(); } +/** Where the slice of each phase is kept for the next ones: /.slice, + * beside the scratch directory for the reason the seed store is (every phase + * recreates the scratch). Holds .bc for a slice, .failed for a slicer + * that failed or timed out -- which the next phase must not pay for again: on + * eca-* the slicer spent 0.2T in phase 1 AND in phase 2, and the run was + * killed past its budget with no suite (R15, 4 ERROR). */ +inline std::string sliceCachePath(const std::string& cwd, + const std::string& programHash) { + return cwd + "/" + programHash + ".slice"; +} + +/** The cache key: FNV-1a (64-bit, hex) over the input bitcode's CONTENT and + * every setting that shapes the slice, so a slice is reused only for the very + * same question. Fields are separated by a byte no name contains. */ +inline std::string sliceCacheKey(const std::string& inputContent, + const std::string& criteriaLabel, + const std::string& entry, + const std::string& slicerFlags) { + uint64_t hash = 14695981039346656037ull; + auto mix = [&hash](const std::string& field) { + for (unsigned char c : field) { + hash ^= c; + hash *= 1099511628211ull; + } + hash ^= 0xff; + hash *= 1099511628211ull; + }; + mix(inputContent); + mix(criteriaLabel); + mix(entry); + mix(slicerFlags); + static const char* digits = "0123456789abcdef"; + std::string key(16, '0'); + for (int i = 15; i >= 0; --i) { + key[i] = digits[hash & 0xf]; + hash >>= 4; + } + return key; +} + +/** The opt arguments for MAP2CHECK_SLICE_CLEANUP (an experiment knob): the dg + * slicer leaves empty blocks and dead functions behind. "light" folds them + * away; "o2" is the full pipeline, which may exploit undefined behaviour and + * is measured, not trusted. Anything else means no cleanup. */ +inline std::string sliceCleanupPasses(const std::string& knob) { + if (knob == "light") return "-passes='function(simplifycfg,dce),globaldce'"; + if (knob == "o2") return "-O2"; + return ""; +} + } // namespace Map2Check #endif // MODULES_FRONTEND_UTILS_SLICER_HPP_ diff --git a/tests/integration/test_testcomp_regressions.sh b/tests/integration/test_testcomp_regressions.sh index 867841422..83a353351 100755 --- a/tests/integration/test_testcomp_regressions.sh +++ b/tests/integration/test_testcomp_regressions.sh @@ -428,36 +428,44 @@ int main(void) { } EOF -# Off by default: the hybrid's measured behaviour must not change until the -# exchange has earned its place beside it. +# The 8.x fixed hybrid keeps its behaviour: no exchange unless asked. (Since +# 9.0 the default hybrid is the alternation, which exchanges seeds.) ( cd "$WORK/seed" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 250 "$MAP2CHECK" \ - --target-function --target-function-name reach_error \ + --fixed-hybrid --target-function --target-function-name reach_error \ --debug --timeout 60 seed.c ) > "$WORK/seed/off.log" 2>&1 -scratch_off=$(find "$WORK/seed" -maxdepth 1 -name '*.map2check' -print -quit) -n_off=$(ls "$scratch_off/seeds" 2>/dev/null | wc -l) +# The seed store lives BESIDE the scratch directory (.seeds): every +# hybrid phase recreates the scratch directory, and a store inside it never +# reached the next phase (tacasv3a). +n_off=$(ls -d "$WORK/seed"/*.seeds 2>/dev/null | wc -l) if [ "$n_off" -eq 0 ]; then - ok "no seed corpus without --seed-exchange" + ok "no seed store with --fixed-hybrid and without --seed-exchange" else - fail "default behaviour" "$n_off seeds written without asking" + fail "default behaviour" "a seed store was created without asking" fi rm -rf "$WORK/seed"/*.map2check ( cd "$WORK/seed" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 300 "$MAP2CHECK" \ --target-function --target-function-name reach_error --seed-exchange \ --debug --timeout 60 seed.c ) > "$WORK/seed/on.log" 2>&1 -scratch_on=$(find "$WORK/seed" -maxdepth 1 -name '*.map2check' -print -quit) +store=$(ls -d "$WORK/seed"/*.seeds 2>/dev/null | head -1) # Only the fuzzer's own discoveries count: the Caller writes a placeholder -# seed into seeds/ itself, so a plain file count would pass with no copy-back. -n_on=$(ls "$scratch_on/seeds" 2>/dev/null | grep -c '^afl-') +# seed itself, so a plain file count would pass with no copy-back. +n_on=$(ls "$store/afl" 2>/dev/null | grep -c '^afl-') +if [ -n "$store" ] && [ "$n_on" -gt 0 ]; then + ok "the fuzzer discoveries reach the seed store beside the scratch ($n_on files)" +else + fail "seed store" "no store beside the scratch directory, or no fuzzer discoveries in it" +fi -# afl-fuzz never writes into its -i dir; the Caller copies its queue back in -# after the fuzzer phase, so the corpus survives the fuzzer process. (It does -# not yet survive into the next phase: each Caller recreates the scratch -# directory -- inherited from v15, left to the smart-seeds work.) -if [ "$n_on" -gt 0 ]; then - ok "the fuzzer discoveries are copied into seeds/ with --seed-exchange ($n_on files)" +# Without --debug the store is removed after the last phase. +rm -rf "$WORK/seed"/*.map2check "$WORK/seed"/*.seeds +( cd "$WORK/seed" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 300 "$MAP2CHECK" \ + --target-function --target-function-name reach_error --seed-exchange \ + --timeout 60 seed.c ) > "$WORK/seed/on-clean.log" 2>&1 +if [ "$(ls -d "$WORK/seed"/*.seeds 2>/dev/null | wc -l)" -eq 0 ]; then + ok "no seed store is left behind without --debug" else - fail "seed corpus" "nothing kept -- the corpus is still in-memory only" + fail "seed store cleanup" "a *.seeds directory survived a run without --debug" fi # KLEE -> fuzzer: its per-path vectors become seed files. Sound only because @@ -875,6 +883,442 @@ else ok "slicing does not invent an overflow" fi +# --- 26. the fuzzer's corpus reaches KLEE as typed seeds --------------------- +# Each queue entry is replayed through the witness binary (inside the store's +# replay/, so nothing it writes touches the phase), and the typed nondet log +# becomes a .ktest; KLEE starts from the whole set with --seed-dir. The old +# channel read a log from a scratch directory that no longer existed and sent +# at most one vector. +# An unreachable guard (44522 is not a square), so no phase can end the hybrid +# early: the fuzzer phase always hands its corpus over and KLEE always runs +# with it -- the test cannot pass without exercising the channel. +mkdir -p "$WORK/seed2" +cat > "$WORK/seed2/square.c" <<'EOF' +extern void __assert_fail(const char *, const char *, unsigned int, + const char *) __attribute__((__noreturn__)); +void reach_error(void) { __assert_fail("0", "square.c", 3, "reach_error"); } +extern int __VERIFIER_nondet_int(void); +int main(void) { + int a = __VERIFIER_nondet_int(); + int b = __VERIFIER_nondet_int(); + if (a > 100 && a < 300 && b > 0) { + if (a * a == 44522) { reach_error(); } + } + return 0; +} +EOF +( cd "$WORK/seed2" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 300 "$MAP2CHECK" \ + --target-function --target-function-name reach_error --seed-exchange \ + --debug --timeout 60 square.c ) > "$WORK/seed2/run.log" 2>&1 +n_seeds=$(grep -aoE "Seeded KLEE with [0-9]+ vectors from AFL\+\+" "$WORK/seed2/run.log" \ + | grep -oE "[0-9]+" | head -1) +if [ "${n_seeds:-0}" -gt 0 ] && grep -q -- "--seed-dir=" "$WORK/seed2/run.log"; then + ok "the fuzzer corpus reaches KLEE ($n_seeds seeds via --seed-dir)" +else + fail "fuzzer -> KLEE" "KLEE ran without seeds from the fuzzer" +fi +# The program is safe and KLEE proves it: that proof is the run's answer. The +# third (fuzzer) phase is for runs nothing has decided yet; running it after a +# proof printed UNKNOWN last, and every harness reads the last verdict. +last_verdict=$(grep -aoE "VERIFICATION (FAILED|SUCCEEDED|UNKNOWN)" "$WORK/seed2/run.log" | tail -1) +if [ "$last_verdict" = "VERIFICATION SUCCEEDED" ]; then + ok "a proof from the KLEE phase stays the final verdict under --seed-exchange" +else + fail "exchange verdict" "KLEE proved the program safe but the run ended with [$last_verdict]" +fi + +# --- 27. replaying the corpus must not erase a violation the fuzzer found ---- +mkdir -p "$WORK/seed3" +cat > "$WORK/seed3/easy.c" <<'EOF' +extern void __assert_fail(const char *, const char *, unsigned int, + const char *) __attribute__((__noreturn__)); +void reach_error(void) { __assert_fail("0", "easy.c", 3, "reach_error"); } +extern int __VERIFIER_nondet_int(void); +int main(void) { + int x = __VERIFIER_nondet_int(); + if (x > 1000 && x < 1100) { reach_error(); } + return 0; +} +EOF +( cd "$WORK/seed3" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --target-function --target-function-name reach_error --seed-exchange \ + --timeout 30 easy.c ) > "$WORK/seed3/run.log" 2>&1 +if grep -q "VERIFICATION FAILED" "$WORK/seed3/run.log"; then + ok "a violation found by the fuzzer survives the seed replays" +else + fail "seed replay" "the violation was lost with --seed-exchange" +fi + +# --- 28. the seed store starts clean, and the last phase replays nothing ---- +# The store's name is derived from the program's content, so a store left by +# an earlier run -- a --debug run keeps it on purpose, a killed one leaks it -- +# would feed its seeds into the next run of the same program: it is wiped at +# the start of a run. And the fuzzer's corpus is converted for KLEE only when a +# KLEE phase follows; after the last phase the replays would be pure cost. +mkdir -p "$WORK/seed4" +cat > "$WORK/seed4/safe.c" <<'EOF' +extern void __assert_fail(const char *, const char *, unsigned int, + const char *) __attribute__((__noreturn__)); +void reach_error(void) { __assert_fail("0", "safe.c", 3, "reach_error"); } +extern int __VERIFIER_nondet_int(void); +int main(void) { + int a = __VERIFIER_nondet_int(); + int b = __VERIFIER_nondet_int(); + if (a > 100 && b > a) { b = b - a; } + if (a != a) { reach_error(); } + return b; +} +EOF +( cd "$WORK/seed4" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 300 "$MAP2CHECK" \ + --target-function --target-function-name reach_error --seed-exchange \ + --debug --timeout 60 safe.c ) > "$WORK/seed4/first.log" 2>&1 +store4=$(ls -d "$WORK/seed4"/*.seeds 2>/dev/null | head -1) +[ -n "$store4" ] && mkdir -p "$store4/ktest" && echo stale > "$store4/ktest/stale-from-an-old-run.ktest" +rm -rf "$WORK/seed4"/*.map2check +( cd "$WORK/seed4" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 300 "$MAP2CHECK" \ + --target-function --target-function-name reach_error --seed-exchange \ + --debug --timeout 60 safe.c ) > "$WORK/seed4/run.log" 2>&1 +replays=$(grep -c "Seeded KLEE with" "$WORK/seed4/run.log") +if [ -n "$store4" ] && [ ! -e "$store4/ktest/stale-from-an-old-run.ktest" ] && \ + [ "$replays" -le 1 ] && ! grep -q "VERIFICATION FAILED" "$WORK/seed4/run.log"; then + ok "the seed store starts clean and only the first fuzzer phase feeds KLEE" +else + fail "seed store lifecycle" "stale seed kept, $replays conversions, or a safe program reported FALSE" +fi + +# --- 29. an inline "if (!c) abort();" is an assumption, not the end of search -- +# In SV-COMP abort() is not an error: it discards the path. The benchmarks use +# it inline (seq-mthreaded/pals_*: `if(!(i2)) {abort();}`), and KLEE runs with +# --exit-on-error-type=Abort, so the first path violating that assumption ended +# the WHOLE search with exit 0 -- and the run answered TRUE for a program with a +# reachable bug. Measured: every wrong TRUE of the tacasv2 control arm in R15. +mkdir -p "$WORK/abort" +cat > "$WORK/abort/inline.c" <<'EOF' +extern void __assert_fail(const char *, const char *, unsigned int, + const char *) __attribute__((__noreturn__)); +void reach_error(void) { __assert_fail("0", "inline.c", 3, "reach_error"); } +extern void abort(void); +extern int __VERIFIER_nondet_int(void); +int main(void) { + int x = __VERIFIER_nondet_int(); + if (!(x > 0)) { abort(); } + int y = __VERIFIER_nondet_int(); + if (y == x + 1) { ERROR: { reach_error(); abort(); } } + return 0; +} +EOF +( cd "$WORK/abort" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --target-function --target-function-name reach_error --nondet-generator symex \ + --timeout 45 inline.c ) > "$WORK/abort/inline.log" 2>&1 +if grep -q "VERIFICATION FAILED" "$WORK/abort/inline.log"; then + ok "an inline abort() assumption prunes the path and the bug behind it is found" +else + fail "inline abort" "the bug after an inline abort() assumption was not found: $(grep -aoE 'VERIFICATION [A-Z]+' "$WORK/abort/inline.log" | tail -1)" +fi + +# The same shape with no reachable bug must not turn into a violation. +cat > "$WORK/abort/safe.c" <<'EOF' +extern void __assert_fail(const char *, const char *, unsigned int, + const char *) __attribute__((__noreturn__)); +void reach_error(void) { __assert_fail("0", "safe.c", 3, "reach_error"); } +extern void abort(void); +extern int __VERIFIER_nondet_int(void); +int main(void) { + int x = __VERIFIER_nondet_int(); + if (!(x > 0)) { abort(); } + if (x < 0) { ERROR: { reach_error(); abort(); } } + return 0; +} +EOF +( cd "$WORK/abort" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --target-function --target-function-name reach_error --nondet-generator symex \ + --timeout 45 safe.c ) > "$WORK/abort/safe.log" 2>&1 +# And it is still provable: the pruned path is not a dropped one. Reading +# KLEE's "partially completed paths" as dropped paths turned this into UNKNOWN. +if grep -q "VERIFICATION SUCCEEDED" "$WORK/abort/safe.log"; then + ok "an inline abort() assumption does not invent a violation, and is provable" +else + fail "inline abort soundness" "a safe program with an inline abort() assumption: $(grep -aoE 'VERIFICATION [A-Z]+' "$WORK/abort/safe.log" | tail -1), expected SUCCEEDED" +fi + +# --- 30. KLEE finishing after dropping paths is not a proof ----------------- +# KLEE exits 0 whenever its queue empties -- also after pinning a symbolic +# double to 0 ("silently concretizing (reason: floating point)"): one path, +# explored "completely", and float-benchs/sin_interpolated_index-1 came back +# TRUE with a reachable bug. +mkdir -p "$WORK/dropped" +cat > "$WORK/dropped/float.c" <<'EOF2' +extern void __assert_fail(const char *, const char *, unsigned int, + const char *) __attribute__((__noreturn__)); +void reach_error(void) { __assert_fail("0", "float.c", 3, "reach_error"); } +extern double __VERIFIER_nondet_double(void); +int main(void) { + double x = __VERIFIER_nondet_double(); + if (x > 179.5 && x < 180.5) { reach_error(); } + return 0; +} +EOF2 +( cd "$WORK/dropped" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --target-function --target-function-name reach_error --nondet-generator symex \ + --timeout 45 float.c ) > "$WORK/dropped/float.log" 2>&1 +if grep -q "VERIFICATION SUCCEEDED" "$WORK/dropped/float.log"; then + fail "concretized verdict" "TRUE after KLEE concretized the symbolic double" +else + ok "a KLEE run that concretized an input is not reported TRUE" +fi + +# --- 31. the hybrid slices once per run, not once per phase ----------------- +# Every phase recreates the scratch directory, and each used to run sbt-slicer +# again. On eca-* the slicer timed out (0.2T) in phase 1 AND phase 2, the run +# overran its budget and was killed with no suite (R15, 4 ERROR). A slice, or a +# slicer failure, is now kept for the later phases of the same run. +mkdir -p "$WORK/slicecache" +cat > "$WORK/slicecache/safe.c" <<'EOF2' +extern void __assert_fail(const char *, const char *, unsigned int, + const char *) __attribute__((__noreturn__)); +void reach_error(void) { __assert_fail("0", "safe.c", 3, "reach_error"); } +extern int __VERIFIER_nondet_int(void); +int main(void) { + int x = __VERIFIER_nondet_int(); + int y = x > 0 ? x : -x; + if (y < 0 && x > 0) { reach_error(); } + return 0; +} +EOF2 +( cd "$WORK/slicecache" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --debug --slice --target-function --target-function-name reach_error \ + --timeout 30 safe.c ) > "$WORK/slicecache/safe.log" 2>&1 +slicer_runs=$(grep -c "sbt-slicer -c" "$WORK/slicecache/safe.log") +if [ "$slicer_runs" -eq 1 ] && grep -q "reusing the slice from an earlier phase" "$WORK/slicecache/safe.log"; then + ok "a slice is computed once and reused by the later phases" +else + fail "slice cache" "sbt-slicer ran $slicer_runs time(s); reuse logged: $(grep -c 'reusing the slice' "$WORK/slicecache/safe.log")" +fi + +# A slicer failure is remembered too: the VLA makes sbt-slicer fail, and the +# later phases must not pay for it again. +cat > "$WORK/slicecache/vla.c" <<'EOF2' +extern int __VERIFIER_nondet_int(void); +int main(void) { + int n = __VERIFIER_nondet_int(); + if (n > 0 && n < 10) { + int a[n]; + a[0] = 1; + return a[0]; + } + return 0; +} +EOF2 +( cd "$WORK/slicecache" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --debug --memtrack --slice --timeout 30 vla.c ) > "$WORK/slicecache/vla.log" 2>&1 +slicer_runs=$(grep -c "sbt-slicer -c" "$WORK/slicecache/vla.log") +if [ "$slicer_runs" -eq 1 ] && grep -q "no usable output (cached" "$WORK/slicecache/vla.log"; then + ok "a slicer failure is remembered by the later phases" +else + fail "slice failure cache" "sbt-slicer ran $slicer_runs time(s); cached failure logged: $(grep -c 'no usable output (cached' "$WORK/slicecache/vla.log")" +fi + +# --- 32. the fuzzer's input runs out as zeros, not as a replay of itself ----- +# Past the end of the test case the AFL++ generator used to start over from +# its first byte, so `while (__VERIFIER_nondet_int())` fed by the placeholder +# seed "A" never ended: afl-fuzz's dry run timed out on it and the fuzzer +# aborted before its first execution -- on the loop idiom sv-benchmarks is +# full of. Reads past the end now return zero. +mkdir -p "$WORK/aflloop" +cat > "$WORK/aflloop/loop.c" <<'EOF2' +extern void __assert_fail(const char *, const char *, unsigned int, + const char *) __attribute__((__noreturn__)); +void reach_error(void) { __assert_fail("0", "loop.c", 3, "reach_error"); } +extern int __VERIFIER_nondet_int(void); +int main(void) { + while (__VERIFIER_nondet_int()) { + if (__VERIFIER_nondet_int() == 7) { reach_error(); } + } + return 0; +} +EOF2 +( cd "$WORK/aflloop" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --target-function --target-function-name reach_error --nondet-generator afl \ + --timeout 45 loop.c ) > "$WORK/aflloop/loop.log" 2>&1 +if grep -q "VERIFICATION FAILED" "$WORK/aflloop/loop.log"; then + ok "a nondet-driven loop does not hang the fuzzer's dry run" +else + fail "fuzzer on a nondet loop" "expected FAILED, got: $(grep -aoE 'VERIFICATION [A-Z]+' "$WORK/aflloop/loop.log" | tail -1)" +fi + +# --- 33. --alternate-engines takes turns and stops a stagnant KLEE ---------- +# The fixed 0.2/0.6/0.2 split held an engine that had stopped progressing to +# the end of its share. Alternating, each phase ends when its engine stagnates +# and the other gets the time; KLEE stopped that way was left with states, so +# the run is never TRUE, and the whole run stays inside its budget. +mkdir -p "$WORK/alternate" +cat > "$WORK/alternate/grow.c" <<'EOF2' +extern void __assert_fail(const char *, const char *, unsigned int, + const char *) __attribute__((__noreturn__)); +void reach_error(void) { __assert_fail("0", "grow.c", 3, "reach_error"); } +extern int __VERIFIER_nondet_int(void); +int main(void) { + int s = 0; + while (__VERIFIER_nondet_int()) { + if (__VERIFIER_nondet_int() > 0) s += 1; else s += 2; + if (s < 0) { reach_error(); } + } + return 0; +} +EOF2 +t0=$(date +%s) +( cd "$WORK/alternate" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --alternate-engines --target-function --target-function-name reach_error \ + --timeout 60 grow.c ) > "$WORK/alternate/grow.log" 2>&1 +t1=$(date +%s) +phases=$(grep -c "Alternation phase" "$WORK/alternate/grow.log") +if [ "$phases" -ge 3 ] && grep -q "KLEE stagnated" "$WORK/alternate/grow.log" && \ + ! grep -q "VERIFICATION SUCCEEDED" "$WORK/alternate/grow.log" && \ + [ $((t1 - t0)) -le 75 ]; then + ok "the engines alternate, a stagnant KLEE is stopped, no TRUE ($phases phases, $((t1 - t0)) s)" +else + fail "alternation" "phases=$phases stagnated=$(grep -c 'KLEE stagnated' "$WORK/alternate/grow.log") elapsed=$((t1 - t0))s verdict=$(grep -aoE 'VERIFICATION [A-Z]+' "$WORK/alternate/grow.log" | tail -1)" +fi + +# --- 34. memset/memcpy/memmove are checked under LLVM 16's opaque pointers -- +# MemoryTrackPass matched the intrinsics by name, and the names carried the +# pointer types (llvm.memset.p0i8.i64) that LLVM 16 no longer writes +# (llvm.memset.p0.i64): no memory intrinsic clang emitted was checked. +mkdir -p "$WORK/intrinsics" +cat > "$WORK/intrinsics/over.c" <<'EOF2' +#include +#include +int main(void) { + char *p = malloc(8); + if (!p) return 0; + memset(p, 0, 16); + free(p); + return 0; +} +EOF2 +cat > "$WORK/intrinsics/safe.c" <<'EOF2' +#include +#include +struct S { int a[10]; char name[16]; }; +int main(void) { + char s[] = "hello, world"; + struct S x = {{1, 2, 3}, "abc"}, y; + y = x; + char *p = malloc(sizeof s); + if (!p) return 0; + memcpy(p, s, sizeof s); + memmove(p + 1, p, 4); + memset(y.name, 'z', sizeof y.name); + free(p); + return y.a[0] + s[0]; +} +EOF2 +( cd "$WORK/intrinsics" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --memtrack --nondet-generator symex --timeout 45 over.c ) > "$WORK/intrinsics/over.log" 2>&1 +( cd "$WORK/intrinsics" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --memtrack --nondet-generator symex --timeout 45 safe.c ) > "$WORK/intrinsics/safe.log" 2>&1 +if grep -q "FALSE-DEREF" "$WORK/intrinsics/over.log"; then + ok "a memset past the end of a heap block is a FALSE-DEREF" +else + fail "memset intrinsic" "expected FALSE-DEREF, got: $(grep -aoE 'VERIFICATION [A-Z]+' "$WORK/intrinsics/over.log" | tail -1)" +fi +if grep -q "VERIFICATION SUCCEEDED" "$WORK/intrinsics/safe.log"; then + ok "in-bounds memcpy/memmove/memset and struct copies stay TRUE" +else + fail "intrinsics soundness" "safe program: $(grep -aoE 'VERIFICATION [A-Z]+|FALSE[-_A-Z]*' "$WORK/intrinsics/safe.log" | tr '\n' ' ')" +fi + +# --- 35. a fuzzer binary that fails to link says so --------------------------- +# Every missing AFL++ binary was reported as one that "did not build within +# Ns", the budget's fault -- including a link error that no budget would fix. +mkdir -p "$WORK/afllink" +cat > "$WORK/afllink/decl.c" <<'EOF2' +extern void reach_error(void); +extern int __VERIFIER_nondet_int(void); +int main(void) { if (__VERIFIER_nondet_int() == 3) reach_error(); return 0; } +EOF2 +( cd "$WORK/afllink" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 100 "$MAP2CHECK" \ + --nondet-generator afl --target-function --target-function-name reach_error \ + --timeout 30 decl.c ) > "$WORK/afllink/decl.log" 2>&1 +if grep -q "AFL++ binary failed to build.*undefined reference" "$WORK/afllink/decl.log"; then + ok "a fuzzer link error is reported as one, with its cause" +else + fail "fuzzer link error" "$(grep -a 'AFL++ binary' "$WORK/afllink/decl.log" | head -1)" +fi + +# --- 36. MAP2CHECK_CHECK_CSTRINGS=1: a %s that reads past its buffer is a FALSE-DEREF +# KLEE's uClibc declares printf without defining it, so KLEE runs it as a +# native external call: the read of an unterminated string happened outside +# every check, and Juliet's CWE121 CWE193 "cpy" tasks came back TRUE. The +# strings a %s (or puts) will read are checked before the call. +mkdir -p "$WORK/cstring" +cat > "$WORK/cstring/unterminated.c" <<'EOF2' +#include +#include +int main(void) { + char buf[10]; + char src[11] = "AAAAAAAAAA"; + memcpy(buf, src, strlen(src)); + printf("%s\n", buf); + return 0; +} +EOF2 +cat > "$WORK/cstring/fine.c" <<'EOF2' +#include +#include +#include +int main(void) { + char buf[16] = "hello"; + char *heap = malloc(8); + if (!heap) return 0; + strcpy(heap, "abc"); + printf("%s %s %d %.3s %5s\n", buf, "literal", 42, heap, heap); + puts(buf); + free(heap); + return 0; +} +EOF2 +( cd "$WORK/cstring" && MAP2CHECK_CHECK_CSTRINGS=1 MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --memtrack --nondet-generator symex --timeout 45 unterminated.c ) > "$WORK/cstring/unterminated.log" 2>&1 +( cd "$WORK/cstring" && MAP2CHECK_CHECK_CSTRINGS=1 MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --memtrack --nondet-generator symex --timeout 45 fine.c ) > "$WORK/cstring/fine.log" 2>&1 +if grep -q "FALSE-DEREF" "$WORK/cstring/unterminated.log"; then + ok "printing an unterminated buffer with %s is a FALSE-DEREF" +else + fail "%s past the buffer" "expected FALSE-DEREF, got: $(grep -aoE 'VERIFICATION [A-Z]+' "$WORK/cstring/unterminated.log" | tail -1)" +fi +if grep -q "VERIFICATION SUCCEEDED" "$WORK/cstring/fine.log"; then + ok "terminated strings, literals, %.Ns and puts stay TRUE" +else + fail "%s soundness" "fine program: $(grep -aoE 'VERIFICATION [A-Z]+|FALSE[-_A-Z]*' "$WORK/cstring/fine.log" | tr '\n' ' ')" +fi + +# --- 37. MAP2CHECK_FUZZER_SUITE=1: the fuzzer's corpus joins a Cover-Branches suite +# The suite came only from KLEE's paths; the fuzzer's queue -- the inputs that +# reached new edges -- was thrown away with the scratch directory. +mkdir -p "$WORK/fuzzersuite" +cat > "$WORK/fuzzersuite/br.c" <<'EOF2' +extern int __VERIFIER_nondet_int(void); +int main(void) { + int a = __VERIFIER_nondet_int(), b = __VERIFIER_nondet_int(); + int r = 0; + if (a > 100) r += 1; else r -= 1; + if (b == 4242) r += 2; + return r; +} +EOF2 +( cd "$WORK/fuzzersuite" && MAP2CHECK_FUZZER_SUITE=1 MAP2CHECK_PATH="$MAP2CHECK_DIR" \ + timeout -k 10 200 "$MAP2CHECK" --cover-branches --generate-test-suite \ + --timeout 40 br.c ) > "$WORK/fuzzersuite/br.log" 2>&1 +fuzzed=$(grep -aoE "[0-9]+ test cases from the fuzzer's corpus" "$WORK/fuzzersuite/br.log" | grep -oE '^[0-9]+') +dups=$( + for f in "$WORK"/fuzzersuite/test-suite/testcase-*.xml; do grep -o '[^<]*' "$f" | tr '\n' ' '; echo; done | sort | uniq -d | wc -l) +if [ "${fuzzed:-0}" -ge 1 ] && [ "$dups" -eq 0 ]; then + ok "the fuzzer's corpus contributes test cases, without duplicates ($fuzzed)" +else + fail "fuzzer suite" "fuzzer cases=${fuzzed:-0}, duplicate cases=$dups" +fi + echo " ---" echo " Results: $PASSED passed, $FAILED failed" [ "$FAILED" -eq 0 ] || exit 1 diff --git a/tests/integration/test_verdict_classifier.sh b/tests/integration/test_verdict_classifier.sh index 6c03c4c73..904e1d5d3 100644 --- a/tests/integration/test_verdict_classifier.sh +++ b/tests/integration/test_verdict_classifier.sh @@ -60,6 +60,22 @@ VERIFICATION UNKNOWN' check "KLEE crash is ERROR, not TIMEOUT" \ ERROR "$HYBRID_CRASH" 0 13 60 +# The fuzzer's crash replayed through the program under test: the program +# segfaults (a nondet-sized alloca), which is what a crash replay is for. Not +# a tool failure -- the tool went on to KLEE and answered. +AFL_REPLAY_CRASH='Executing AFL++ with map2check +Exited fuzzer with 0 +timeout: the monitored command dumped core +Segmentation fault +Note: Could not replicate error +VERIFICATION UNKNOWN +Started Map2Check +Executing Klee with map2check +Exited klee with 0 +VERIFICATION UNKNOWN' +check "a crash replayed from the fuzzer is not ERROR" \ + UNKNOWN "$AFL_REPLAY_CRASH" 0 13 60 + # A definitive verdict still wins even when a phase died along the way. check "verdict survives a crash in the other phase" \ FALSE-OVERFLOW "$HYBRID_CRASH diff --git a/tests/lib/verdict_classifier.sh b/tests/lib/verdict_classifier.sh index 2eaba2b83..2040d0b08 100644 --- a/tests/lib/verdict_classifier.sh +++ b/tests/lib/verdict_classifier.sh @@ -72,7 +72,15 @@ classify_map2check_verdict() { if echo "$output" | grep -E "undefined reference to" | grep -qv "KLEE: WARNING"; then echo "ERROR"; return fi - if echo "$output" | grep -qE "Segmentation fault|dumped core|Aborted \(core dumped\)"; then + # A crash counts where the TOOL crashed. After "Exited fuzzer with" and + # before the next phase, the process that dumps core is the program under + # test, replayed on the fuzzer's crash to confirm it -- that is the program + # crashing, as it should (array-memsafety/*-alloca: a nondet-sized alloca). + if echo "$output" | awk ' + /Exited fuzzer with/ { replay = 1 } + /Started Map2Check/ { replay = 0 } + /Segmentation fault|dumped core|Aborted \(core dumped\)/ { if (!replay) found = 1 } + END { exit !found }'; then echo "ERROR"; return fi diff --git a/tests/memsafety/run_memsafety_evaluation.sh b/tests/memsafety/run_memsafety_evaluation.sh index 59808767a..11676a542 100755 --- a/tests/memsafety/run_memsafety_evaluation.sh +++ b/tests/memsafety/run_memsafety_evaluation.sh @@ -103,7 +103,7 @@ while IFS=$'\t' read -r category program data_model expected subproperty <&3; do # shellcheck disable=SC2086 # the flag strings are word lists on purpose ( cd "$work" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 $((BUDGET + 30)) \ "$MAP2CHECK" $MODE_FLAGS $EXTRA_FLAGS --architecture "$arch" \ - --timeout "$BUDGET" "$name" ) > "$work/map2check.log" 2>&1 "$work/map2check.log" 2>&1 "$work/map2check.log" 2>&1 "$work/map2check.log" 2>&1 "$work/testcov.log" 2>&1 "$work/testcov.log" 2>&1 + +#include "../../../modules/frontend/utils/alternation.hpp" + +using Map2Check::Engine; + +TEST(AlternationWindow, StartsAtTheBaseShareOfTheBudget) { + EXPECT_DOUBLE_EQ(Map2Check::alternationWindow(Engine::Fuzzer, 1, 300, 300), + 30); + EXPECT_DOUBLE_EQ(Map2Check::alternationWindow(Engine::Klee, 1, 300, 270), 90); +} + +TEST(AlternationWindow, DoublesEveryRound) { + EXPECT_DOUBLE_EQ(Map2Check::alternationWindow(Engine::Fuzzer, 2, 300, 300), + 60); + EXPECT_DOUBLE_EQ(Map2Check::alternationWindow(Engine::Klee, 3, 300, 1000), + 360); +} + +TEST(AlternationWindow, NeverExceedsWhatIsLeft) { + EXPECT_DOUBLE_EQ(Map2Check::alternationWindow(Engine::Klee, 2, 300, 40), 40); +} + +TEST(StagnationSeconds, IsFivePercentButAtLeastTen) { + EXPECT_EQ(Map2Check::stagnationSeconds(300), 15u); + EXPECT_EQ(Map2Check::stagnationSeconds(60), 10u); +} + +TEST(CoverageWatch, StagnatesOnlyAfterTheQuietPeriod) { + Map2Check::CoverageWatch watch(10); + EXPECT_FALSE(watch.stagnated(100, 0)); + EXPECT_FALSE(watch.stagnated(100, 9)); + EXPECT_FALSE(watch.stagnated(120, 9.5)); // progress resets the clock + EXPECT_FALSE(watch.stagnated(120, 19)); + EXPECT_TRUE(watch.stagnated(120, 19.5)); +} + +TEST(CoverageWatch, AnUnreadableSampleIsNotEvidence) { + Map2Check::CoverageWatch watch(10); + EXPECT_FALSE(watch.stagnated(-1, 0)); + EXPECT_FALSE(watch.stagnated(-1, 50)); // never read: no verdict on progress + EXPECT_FALSE(watch.stagnated(5, 51)); + EXPECT_FALSE(watch.stagnated(-1, 60)); + EXPECT_TRUE(watch.stagnated(5, 61.5)); +} + +TEST(StagnationSeconds, KleesPatienceDoublesWithItsRounds) { + EXPECT_EQ(Map2Check::stagnationSeconds(300, 1), 15u); + EXPECT_EQ(Map2Check::stagnationSeconds(300, 2), 30u); + EXPECT_EQ(Map2Check::stagnationSeconds(300, 3), 60u); +} diff --git a/tests/unit/frontend/CMakeLists.txt b/tests/unit/frontend/CMakeLists.txt index 35d6a0390..3c734e637 100644 --- a/tests/unit/frontend/CMakeLists.txt +++ b/tests/unit/frontend/CMakeLists.txt @@ -20,3 +20,13 @@ add_executable(SlicerTest SlicerTest.cpp ) map2check_test(SlicerTest) + +add_executable(SeedStoreTest + SeedStoreTest.cpp +) +map2check_test(SeedStoreTest) + +add_executable(AlternationTest + AlternationTest.cpp +) +map2check_test(AlternationTest) diff --git a/tests/unit/frontend/KtestReaderTest.cpp b/tests/unit/frontend/KtestReaderTest.cpp index e9c07f76f..afc7bac46 100644 --- a/tests/unit/frontend/KtestReaderTest.cpp +++ b/tests/unit/frontend/KtestReaderTest.cpp @@ -307,3 +307,103 @@ TEST(KleeHaltedOnTimer, AFinishedRunIsNotHalted) { EXPECT_FALSE(Map2Check::kleeHaltedOnTimer("/nonexistent/klee-last")); fs::remove_all(d); } + +// KLEE also exits 0 after dropping paths without running out of them: a +// symbolic double concretized to 0 (float-benchs/sin_interpolated_index-1: one +// path, answered TRUE), or states killed by its own errors (a VLA of symbolic +// size in loops/insertion_sort-1-2: "partially completed paths = 2", TRUE). +TEST(KleeDroppedPaths, ConcretizingAnInputDropsPaths) { + fs::path d = freshDir("concretized"); + std::ofstream(d / "warnings.txt") + << "KLEE: WARNING ONCE: silently concretizing (reason: floating point) " + "expression (ReadLSB w64 0 non_det_double) to value 0 (x.c:155)\n"; + std::ofstream(d / "info") << "KLEE: done: partially completed paths = 0\n"; + EXPECT_FALSE(Map2Check::kleeDroppedPaths(d.string()).empty()); + fs::remove_all(d); +} + +TEST(KleeDroppedPaths, AStateKilledByAnErrorDropsPaths) { + fs::path d = freshDir("killed"); + std::ofstream(d / "test000001.ktest") << ""; + std::ofstream(d / "test000001.model.err") << "Error: concretized symbolic size\n"; + EXPECT_FALSE(Map2Check::kleeDroppedPaths(d.string()).empty()); + fs::remove_all(d); +} + +TEST(KleeDroppedPaths, AStateTerminatedEarlyDropsPaths) { + fs::path d = freshDir("early"); + std::ofstream(d / "test000002.early") << "Memory limit exceeded\n"; + EXPECT_FALSE(Map2Check::kleeDroppedPaths(d.string()).empty()); + fs::remove_all(d); +} + +// KLEE that died -- a solver crash, an LLVM assertion, the OOM killer -- +// writes no HaltTimer, no .err and no "done" lines, and may leave NONE in the +// property file from the paths it did finish. +TEST(KleeDroppedPaths, ARunThatNeverFinishedDropsPaths) { + fs::path d = freshDir("crashed"); + std::ofstream(d / "info") << "KLEE: output directory is \"x\"\n"; + std::ofstream(d / "test000001.ktest") << ""; + EXPECT_FALSE(Map2Check::kleeDroppedPaths(d.string()).empty()); + fs::remove_all(d); +} + +// Near --max-memory KLEE stops forking and follows one side of each branch +// at random; it logs that once and can still exit 0. +TEST(KleeDroppedPaths, SkippingForksDropsPaths) { + fs::path d = freshDir("skipfork"); + std::ofstream(d / "warnings.txt") + << "KLEE: WARNING ONCE: skipping fork (memory cap exceeded)\n"; + std::ofstream(d / "info") << "KLEE: done: completed paths = 3\n"; + EXPECT_FALSE(Map2Check::kleeDroppedPaths(d.string()).empty()); + fs::remove_all(d); +} + +// A path pruned by an assumption is not a dropped path, and KLEE counts it +// among the "partially completed" all the same (klee_silent_exit and a failed +// klee_assume alike). Reading that counter made every program with an +// assume_abort_if_not unprovable: TRUE became UNKNOWN. +TEST(KleeDroppedPaths, AnAssumptionPrunedPathDropsNothing) { + fs::path d = freshDir("pruned"); + std::ofstream(d / "info") << "KLEE: done: completed paths = 1\n" + "KLEE: done: partially completed paths = 1\n"; + std::ofstream(d / "test000001.ktest") << ""; + EXPECT_TRUE(Map2Check::kleeDroppedPaths(d.string()).empty()); + fs::remove_all(d); +} + +TEST(KleeDroppedPaths, TheHaltTimerDropsPaths) { + fs::path d = freshDir("halted"); + std::ofstream(d / "messages.txt") << "KLEE: HaltTimer invoked\n"; + EXPECT_FALSE(Map2Check::kleeDroppedPaths(d.string()).empty()); + fs::remove_all(d); +} + +TEST(KleeDroppedPaths, AnExhaustedRunDropsNothing) { + fs::path d = freshDir("exhausted"); + std::ofstream(d / "warnings.txt") + << "KLEE: WARNING ONCE: calling external: close(12)\n"; + std::ofstream(d / "info") << "KLEE: done: completed paths = 7\n" + "KLEE: done: partially completed paths = 0\n"; + std::ofstream(d / "messages.txt") << "KLEE: output directory is \"x\"\n"; + EXPECT_TRUE(Map2Check::kleeDroppedPaths(d.string()).empty()); + fs::remove_all(d); +} + +// --- the nondet log as seeds ------------------------------------------------- + +// KLEE matches a seed's objects to its symbolic inputs by POSITION. A read the +// converter cannot express (a pchar, a loff_t) must end the seed there: skipping +// it shifted every later object onto the wrong input. +TEST(ReadNonDetLogAsObjects, StopsAtTheFirstUnsupportedRead) { + fs::path d = freshDir("nondetlog"); + std::ofstream(d / "klee_log.csv") + << "1;0;main;0;x;7;0\n" // int 7 + << "2;0;main;0;s;0;9\n" // pchar: unsupported + << "3;0;main;0;y;9;0\n"; // int 9, must not be taken + const auto objects = + Map2Check::readNonDetLogAsObjects((d / "klee_log.csv").string()); + ASSERT_EQ(objects.size(), 1u); + EXPECT_EQ(objects[0].name, "non_det_int"); + fs::remove_all(d); +} diff --git a/tests/unit/frontend/SeedStoreTest.cpp b/tests/unit/frontend/SeedStoreTest.cpp new file mode 100644 index 000000000..d7b40dbf3 --- /dev/null +++ b/tests/unit/frontend/SeedStoreTest.cpp @@ -0,0 +1,67 @@ +/** + * Copyright (C) 2014 - 2026 Map2Check tool + * This file is part of the Map2Check tool, and is made available under + * the terms of the GNU General Public License version 2. + * + * SPDX-License-Identifier: (GPL-2.0) + **/ + +#include + +#include +#include +#include + +#include "../../../modules/frontend/utils/seed_store.hpp" + +// Next to the scratch directory, not inside it: every hybrid phase recreates +// the scratch directory, and a store inside it never reached the next phase. +TEST(SeedStorePath, SitsBesideTheScratchDirectory) { + EXPECT_EQ(Map2Check::seedStorePath("/work", "abc.map2check"), + "/work/abc.map2check.seeds"); +} + +TEST(SelectQueueEntries, KeepsOnlyQueueEntriesInIdOrderUpToTheCap) { + const std::vector names = { + "id:000002,src:000000,time:9", ".state", "README.txt", + "id:000000,time:0,execs:0,orig:seed", "id:000001,src:000000,time:5"}; + const std::vector chosen = + Map2Check::selectQueueEntries(names, 2); + ASSERT_EQ(chosen.size(), 2u); + // The ",orig:" seed is not the fuzzer's discovery (see the test below). + EXPECT_EQ(chosen[0], "id:000001,src:000000,time:5"); + EXPECT_EQ(chosen[1], "id:000002,src:000000,time:9"); +} + +TEST(IsNewVector, RejectsEmptyAndDuplicateVectors) { + std::set> seen; + EXPECT_FALSE(Map2Check::isNewVector({}, &seen)); + EXPECT_TRUE(Map2Check::isNewVector({1, 2}, &seen)); + EXPECT_FALSE(Map2Check::isNewVector({1, 2}, &seen)); + EXPECT_TRUE(Map2Check::isNewVector({1, 3}, &seen)); +} + +// The fuzzer's own seeds come back in its queue tagged ",orig:" -- the KLEE +// vectors, the previous rounds' entries -- and KLEE already has those. Only +// what this round discovered is worth replaying (tacas 3b). +TEST(SelectQueueEntries, SkipsTheSeedsTheFuzzerStartedFrom) { + const auto picked = Map2Check::selectQueueEntries( + {"id:000000,time:0,execs:0,orig:klee-0", "id:000001,src:000000,op:havoc"}, + 8); + ASSERT_EQ(picked.size(), 1u); + EXPECT_EQ(picked[0], "id:000001,src:000000,op:havoc"); +} + +// Ranked (tacas 3c): the entries that reached new edges ("+cov") first, then +// the ones that only changed hit counts, each in id order -- so when the queue +// outgrows the cap, the seeds KLEE gets are the ones that went somewhere new. +TEST(SelectQueueEntries, PutsNewCoverageFirst) { + const auto picked = Map2Check::selectQueueEntries( + {"id:000001,src:000000,op:havoc", "id:000002,src:000001,op:havoc,+cov", + "id:000003,src:000000,op:havoc", "id:000004,src:000002,op:havoc,+cov"}, + 3); + ASSERT_EQ(picked.size(), 3u); + EXPECT_EQ(picked[0], "id:000002,src:000001,op:havoc,+cov"); + EXPECT_EQ(picked[1], "id:000004,src:000002,op:havoc,+cov"); + EXPECT_EQ(picked[2], "id:000001,src:000000,op:havoc"); +} diff --git a/tests/unit/frontend/SlicerTest.cpp b/tests/unit/frontend/SlicerTest.cpp index 12e9babe6..769b2c64e 100644 --- a/tests/unit/frontend/SlicerTest.cpp +++ b/tests/unit/frontend/SlicerTest.cpp @@ -199,3 +199,46 @@ TEST(InstrumentedSliceCriteria, CollectsRuntimeThenExternalNames) { EXPECT_EQ(criteria[0], "map2check_check_deref"); EXPECT_EQ(criteria[1], "strcpy"); } + +// --- the slice cache (tacas 2d) ---------------------------------------------- + +// Every hybrid phase recreates the scratch directory and used to slice again: +// on eca-* the slicer timed out in phase 1 AND phase 2, and the run blew its +// budget. The cache reuses a slice only for the very same input and settings. +TEST(SliceCacheKey, IsDeterministic) { + EXPECT_EQ(Map2Check::sliceCacheKey("BC", "reach_error", "main", ""), + Map2Check::sliceCacheKey("BC", "reach_error", "main", "")); +} + +TEST(SliceCacheKey, ChangesWithEveryInput) { + const std::string base = + Map2Check::sliceCacheKey("BC", "reach_error", "main", ""); + EXPECT_NE(base, Map2Check::sliceCacheKey("BD", "reach_error", "main", "")); + EXPECT_NE(base, Map2Check::sliceCacheKey("BC", "reach_errors", "main", "")); + EXPECT_NE(base, Map2Check::sliceCacheKey("BC", "reach_error", "mai", "")); + EXPECT_NE(base, + Map2Check::sliceCacheKey("BC", "reach_error", "main", "--pta=fs")); + // Field boundaries count: moving a character between fields is another key. + EXPECT_NE(Map2Check::sliceCacheKey("B", "Creach_error", "main", ""), base); +} + +TEST(SliceCacheKey, IsAFileName) { + const std::string key = + Map2Check::sliceCacheKey("BC", "reach_error", "main", "--cda=ntscd"); + EXPECT_EQ(key.size(), 16u); + EXPECT_EQ(key.find_first_not_of("0123456789abcdef"), std::string::npos); +} + +TEST(SliceCachePath, SitsBesideTheScratchDirectory) { + EXPECT_EQ(Map2Check::sliceCachePath("/w", "abc.map2check"), + "/w/abc.map2check.slice"); +} + +TEST(SliceCleanupPasses, MapsTheKnob) { + EXPECT_EQ(Map2Check::sliceCleanupPasses(""), ""); + EXPECT_EQ(Map2Check::sliceCleanupPasses("none"), ""); + EXPECT_EQ(Map2Check::sliceCleanupPasses("light"), + "-passes='function(simplifycfg,dce),globaldce'"); + EXPECT_EQ(Map2Check::sliceCleanupPasses("o2"), "-O2"); + EXPECT_EQ(Map2Check::sliceCleanupPasses("bogus"), ""); +} diff --git a/tests/unit/frontend/TestSuiteTest.cpp b/tests/unit/frontend/TestSuiteTest.cpp index e8dafdec5..9db106bd4 100644 --- a/tests/unit/frontend/TestSuiteTest.cpp +++ b/tests/unit/frontend/TestSuiteTest.cpp @@ -262,3 +262,48 @@ TEST(IsoUtcNow, MatchesTheFormatTheFormatExpects) { EXPECT_EQ(now[16], ':'); EXPECT_EQ(now[19], 'Z'); } + +// Engines alternate (tacas 3b): more than one phase writes test cases into the +// same suite. A writer counting from 1 again overwrote the earlier phase's. +TEST(TestSuiteWriter, NumbersAfterTheCasesAlreadyThere) { + fs::path d = freshDir("tc_continue"); + { + Map2Check::TestSuiteWriter first(d.string()); + ASSERT_TRUE(first.writeTestCase({"1"}, false)); + ASSERT_TRUE(first.writeTestCase({"2"}, false)); + } + Map2Check::TestSuiteWriter second(d.string()); + ASSERT_TRUE(second.writeTestCase({"3"}, false)); + EXPECT_NE(slurp(d / "testcase-1.xml").find("1"), + std::string::npos); + EXPECT_NE(slurp(d / "testcase-3.xml").find("3"), + std::string::npos); +} + +// Under alternation every KLEE phase adds Cover-Branches cases: the cap and +// the duplicates are counted across phases, not per phase. +TEST(TestSuiteWriter, KnowsTheCasesAnEarlierWriterLeft) { + fs::path d = freshDir("tc_known"); + { + Map2Check::TestSuiteWriter first(d.string()); + ASSERT_TRUE(first.writeTestCase({"1", "a