Data: 2026-05-17
Autor: Guilherme Bernardo
Objetivo: Documentar o estado operacional da versão atual antes da migração para Map2Check 2.0
Versão testada: v7.3.1-Flock (Wed Nov 27 20:38:14 UTC 2019)

Este relatório documenta o processo completo de build, instalação e execução de testes do Map2Check v7.3.1 em seu ambiente original (Docker com LLVM 6.0). O objetivo é estabelecer uma baseline de referência antes de iniciar a migração para a nova stack (LLVM 16, KLEE 3.2, AFL++, DG Library).

O Map2Check utiliza uma cadeia de 3 camadas Docker:

git submodule update --init --recursive

3 submodules inicializados:

• utils/base_image_map2check — Dockerfile da imagem base
• utils/benchexecrun — Dockerfile do runner de benchmarks
• utils/dev-llvm_6.0 — Dockerfile do ambiente LLVM 6.0

docker pull herberthb/base-image-map2check:v2

Imagem baixada com sucesso do Docker Hub (~3.4 GB).

docker build -t hrocha/mapdevel --no-cache -f Dockerfile .

Resultado: ✅ Sucesso. Imagem construída com Clang 6.0 pre-built.

docker run --rm \
  -v $(pwd):/home/map2check/devel_tool/mygitclone:Z \
  --user $(id -u):$(id -g) hrocha/mapdevel \
  /bin/bash -c "cd /home/map2check/devel_tool/mygitclone; ./make-release.sh"

Resultado: ✅ 50/50 targets compilados com sucesso.

Passes LLVM (shared libraries):

Binários instalados: map2check, clang, opt, llvm-link, klee, klee-replay, klee-stats, ktest-tool, ld, crabllvm/

Runtime libraries: 21 bitcode files (.bc) para instrumentação, Z3, STP, MiniSat, MetaSMT, Boolector, Lingeling, Yices.

O GoogleTest renomeou a branch padrão de master para main, e as versões recentes exigem CMake ≥ 3.16 (o container tem 3.5.1).

Arquivo: cmake/CMakeLists.txt.googletest

-  GIT_TAG           master
+  GIT_TAG           release-1.12.1

release-1.12.1 é a última versão do GoogleTest compatível com CMake < 3.13.

docker run --rm \
  -v $(pwd):/home/map2check/devel_tool/mygitclone:Z \
  --user $(id -u):$(id -g) hrocha/mapdevel \
  /bin/bash -c "cd /home/map2check/devel_tool/mygitclone; ./make-unit-test.sh"

Test project /home/map2check/devel_tool/mygitclone/build
    Start 1: HelloGTest
1/7 Test #1: HelloGTest .......................   Passed    0.00 sec
    Start 2: AllocationLogTest
2/7 Test #2: AllocationLogTest ................   Passed    0.00 sec
    Start 3: HeapLogTest
3/7 Test #3: HeapLogTest ......................   Passed    0.00 sec
    Start 4: ContainerReallocTest
4/7 Test #4: ContainerReallocTest .............   Passed    0.00 sec
    Start 5: BTreeTest
5/7 Test #5: BTreeTest ........................   Passed    0.15 sec
    Start 6: ContainerBTreeTest
6/7 Test #6: ContainerBTreeTest ...............   Passed    0.16 sec
    Start 7: MemTrackTest
7/7 Test #7: MemTrackTest .....................   Passed    0.00 sec

100% tests passed, 0 tests failed out of 7

Total Test time (real) =   0.33 sec

O BenchExec runner precisou de duas correções para funcionar em ambientes modernos:

Arquivo: utils/benchexecrun/Dockerfile

- FROM ubuntu:18.04
+ FROM ubuntu:20.04

- RUN apt-get install -y sudo \
+ RUN DEBIAN_FRONTEND=noninteractive apt-get install -y sudo \
      python3-pip \
      ...
-     python-minimal \
      libc6-dev

- RUN pip3 install benchexec
+ RUN pip3 install benchexec==3.18

- RUN test -e /usr/local/lib/python3.6/dist-packages/benchexec/tools/map2check.py ...
+ RUN PYTHON_SITE=$(python3 -c "import site; print(site.getsitepackages()[0])") && \
+     test -e ${PYTHON_SITE}/benchexec/tools/map2check.py ...

Motivos:

• BenchExec 3.16+ exige Python 3.7+ (Ubuntu 18.04 tem apenas 3.6)
• BenchExec 3.18+ tem suporte a cgroups v2 (necessário para kernels modernos)
• python-minimal foi removido no Ubuntu 20.04

O BenchExec não consegue rodar dentro de containers Docker em WSL2 porque os cgroups v2 não são delegados para dentro dos containers. Os testes de regressão foram executados diretamente com o binário map2check dentro do container de desenvolvimento.

Os testes foram executados diretamente dentro do container hrocha/mapdevel, invocando o binário map2check com timeout de 30 segundos por caso de teste:

docker run --rm \
  -v $(pwd):/home/map2check/devel_tool/mygitclone:Z \
  hrocha/mapdevel /bin/bash -c '
    cd /home/map2check/devel_tool/mygitclone/release
    timeout 30s ./map2check --timeout 25 --memtrack <arquivo.c>
  '

Os programas de teste envolvem manipulação complexa de heap dinâmica (listas encadeadas, alocações recursivas). O KLEE esgota a memória disponível antes de concluir a análise.

Adopting z3 solver...
Started Map2Check
std::bad_alloc

Causa raiz: O KLEE analisa todo o código do programa, incluindo trechos irrelevantes para a propriedade verificada. Sem slicing estático, o espaço de estados explode exponencialmente.

Solução no Map2Check 2.0: Integração com a DG Library para slicing estático — remover código morto antes da análise simbólica, reduzindo drasticamente o footprint de memória.

O programa contém um erro de memória (out of bound pointer) que o KLEE detectou, mas que o pipeline do Map2Check não propagou como falha de verificação.

Sequência observada:

1. LibFuzzer roda 8 workers, mas não encontra crash (exit code 31744)
2. KLEE identifica erros:

   KLEE: ERROR: concretized symbolic size
   KLEE: ERROR: memory error: out of bound pointer

3. Map2Check reporta incorretamente:

   VERIFICATION SUCCEEDED  ← Deveria ser FAILED

Causa raiz: Os motores (LibFuzzer e KLEE) operam em fases distintas, sem compartilhar aprendizado. Os achados do KLEE não são corretamente processados pelo frontend.

Solução no Map2Check 2.0: Implementação do Coordenador Central com Smart Seeds — orquestração bidirecional entre AFL++ e KLEE, com propagação correta de resultados.

O binário map2check está funcional com todas as opções de verificação disponíveis:

> > > 	  v7.3.1-Flock : Wed Nov 27 20:38:14 UTC 2019 	 < < <

Usage: map2check [options] file.[i|c|bc]

Options:
  --help                 show help
  --version              prints map2check version
  --debug                debug mode
  --input-file arg       specifies the files
  --smt-solver arg (=z3) specifies the smt-solver (stp, z3, btor, yices2)
  --timeout arg          timeout for map2check execution
  --target-function      searches for __VERIFIER_error is reachable
  --generate-testcase    creates c program with fail testcase (experimental)
  --memtrack             check for memory errors
  --print-counter        print counterexample
  --memcleanup-property  analyze program for memcleanup errors
  --check-overflow       analyze program for overflow failures
  --check-asserts        analyze program and verify assert failures
  --add-invariants       adding program invariants adopting Crab-LLVM
  --generate-witness     generates witness file
  --expected-result arg  specifies type of violation expected
  --btree                uses btree structure (experimental)

Os resultados deste baseline confirmam empiricamente os problemas arquiteturais descritos no pré-projeto do Map2Check 2.0:

1. Explosão de estados/memória — Testes 1-3 falham por std::bad_alloc porque o KLEE analisa código irrelevante. A integração com DG Library para slicing estático é crítica.

2. Falsos negativos por falta de orquestração — Teste 5 mostra que o KLEE detecta o erro mas o pipeline não o propaga. O Coordenador Central com feedback loop entre motores é necessário.

3. Obsolescência da infraestrutura — GoogleTest, BenchExec e Ubuntu precisaram de correções para funcionar em ambientes modernos. A migração para LLVM 16, Ubuntu 22.04, C++17 é urgente.

O baseline está estabelecido. A migração pode prosseguir com confiança de que temos uma referência quantitativa para medir o progresso.