hbgit · GuilhermeBn198 · Sep 29, 2026 · Sep 29, 2026 · Sep 29, 2026 · Sep 29, 2026
diff --git 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 (`<hash>.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 (`<hash>.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 (`<hash>.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
@@ -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:
+`<hash>.seeds/` (seed store), `<hash>.slice/` (slice cache) and `<hash>.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
@@ -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
@@ -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
@@ -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)
+
+<p align="justify">
+Map2Check generates inputs with two engines: the <b>AFL++ 4.40c</b> fuzzer (persistent mode, PCGUARD,
+CmpLog) and the <b>KLEE 3.1</b> symbolic executor. By default, and whenever <code>--timeout</code> is
+given, the two run as an <b>alternating hybrid</b>. 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.
+</p>
+
+| 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. |
+
+<p align="justify">
+<b>Verdicts.</b> A TRUE verdict needs KLEE to have explored every path. Map2Check reports
+<code>UNKNOWN</code> instead when KLEE stopped early for any reason:
+</p>
+
+- 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.
+
+<p align="justify">
+A call to <code>abort()</code> 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.
+</p>
+
+<p align="justify">
+<b>Environment knobs.</b> These exist for experiments; the defaults are the measured choices.
+</p>
+
+| 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`. |
+
+<p align="justify">
+<b><code>--add-invariants</code></b> inserts abstract-interpretation invariants computed by
+<a href="https://github.com/seahorn/clam">Clam</a> (formerly crab-llvm). The build must be configured
+with <code>-DENABLE_CLAM=ON</code> and Clam installed at <code>$CLAM_DIR</code>; otherwise the option is
+refused with exit code 3.
+</p>
+
+<p align="justify">
+The option stays <b>optional</b> while it is under study. So far:
+</p>
+
+- 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).
+
+<p align="justify">
+Measurements of every option above are recorded in
+<a href="docs/reports/tacas-experiment-log.md">docs/reports/tacas-experiment-log.md</a>.
+</p>
+
 ___
 
 #### Verifying WebAssembly (WASM) binaries

diff --git a/docs/backlog.md 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.