Biblioteca de suporte à ferramenta Map2Check, reescrita em Rust (rewrite completo do C original). Provê rastreamento dinâmico e verificação de propriedades de segurança para os programas que o Map2Check instrumenta:
- Rastreamento de blocos básicos (
bbtrack) - Rastreamento de endereços de memória e operações de gerenciamento de memória (
memtrack) - Log dos valores não-determinísticos (
nondet), gerados pelos módulos de gerador do Map2Check (AFL++, KLEE) - Verificação de propriedades de segurança: overflow aritmético, memória inválida, assert definido pelo usuário (
analysismode) - ABI C via FFI (
ffi.rs): desde a 2.0.0 (D6), exatamente o ABI C do runtime do Map2Check (develop) que os módulos núcleo definem, mais os pontos de entrada__m2c_rt_*para os quais os módulos IR gerados (scripts/runtime-ir/gen_ll.py) encaminham o resto do ABI (scripts/check-export-set.sh)
A interface com o Map2Check são os 21 módulos .bc do runtime drop-in (scripts/build-runtime-bc.sh), que substituem os do runtime C em ${MAP2CHECK_PATH}/lib sem mudança no frontend nem nos passes. A versão 2.0.0-rc.1 foi validada contra o develop 0bca42eb89d116178e6b52f52acaf73f7c305088 por dois gates diferenciais (docs/cutover/gate-2026-10-27.md e docs/cutover/gate-2026-10-28.md). A API núcleo 1.x (map2check_set_mode, map2check_map_*, print_all_containers_as_json...) deixou de ser ABI C e não é a interface com o Map2Check: ela segue como funções Rust de map2check::ffi, usadas pelos testes. Instalação: docs/integration-guide.md; sugestões para o mantenedor do Map2Check: docs/cutover/handoff-map2check.md.
O projeto exige Rust 1.82.0, conforme definido em rust-toolchain.toml (edição 2021). O rustup seleciona automaticamente esse toolchain ao executar os comandos na raiz do projeto.
Ferramentas necessárias:
rustupecargo- Componentes Rust
clippyerustfmt - Docker, para o build da imagem
cargo-tarpaulin,cargo-audit,cargo-denyecbindgenpara cobertura, auditoria e desenvolvimento
rustup component add clippy rustfmt
cargo install cargo-tarpaulin cargo-audit cargo-deny cbindgenAs features configuradas no Cargo.toml são:
wasm: os pontos de entrada__m2c_rt_wasm_*do runtime wasm2c (modo--wasmdo Map2Check).
A feature libfuzzer saiu na 2.0.0, com a API núcleo 1.x (veja o CHANGELOG.md).
Execute os comandos a seguir na raiz do projeto:
# Compilar a biblioteca em modo release
cargo build --release
# Checar lint e possíveis erros
cargo clippy
# Verificar e formatar o código
cargo fmt
# Rodar todos os testes com todas as features ativadas
cargo test --all-featuresO artefato principal é gerado em target/release/libmap2check.a.
A cobertura é medida com cargo-tarpaulin (engine LLVM), excluindo rust/src/ffi*.rs, e o build falha abaixo de 80%. O CI e o Dockerfile usam o mesmo script:
scripts/coverage.sh # gate padrão de 80%
COVERAGE_FAIL_UNDER=0 scripts/coverage.sh # só gera o relatório, sem gateOs relatórios ficam em coverage/lcov.info e coverage/tarpaulin-report.html. No CI, eles são publicados como o artefato coverage.
O arquivo include/map2check.h é gerado automaticamente durante a compilação. O script build.rs executa o cbindgen usando cbindgen.toml e grava o resultado na pasta include/. Portanto, não é necessário gerar o header manualmente.
O Dockerfile na raiz usa um build multi-stage para compilar a biblioteca, executar os testes e gerar a cobertura:
docker build -t hbgit/map2check-library .cargo audit
cargo deny checkFluxo: develop é a branch padrão do repositório. Branches de trabalho <tipo>/issue-<N>-<slug> (tipo ∈ feat, fix, docs, test, build, ci, chore) abrem PR para develop; releases sobem de develop para main por PR. develop e main exigem o check build_and_test (workflow "CI Map2Check Rust") e commits assinados; main exige também 1 review. A configuração está em scripts/branch-protection.sh:
scripts/branch-protection.sh check develop # compara com o GitHub (exit 0/1)
scripts/branch-protection.sh apply main # requer permissão de adminSe o job build_and_test for renomeado, atualize CI_CHECK no script na mesma mudança; caso contrário, todo PR fica bloqueado esperando um check que nunca chega.
Como o check também é exigido em main, um PR para main cujo head não passe no CI fica bloqueado. Hoje o CI de main está vermelho, então PRs só de documentação vindos de develop podem ficar presos; o admin pode fazer bypass (enforce_admins=false). apply trata o script como fonte da verdade: regras adicionadas pela interface do GitHub e ausentes do payload são removidas.
rust/src/
├── lib.rs # Raiz da crate; re-exports
├── error.rs # Map2CheckError (thiserror)
├── state.rs # AnalysisState + OnceLock<Arc<Mutex<...>>>
├── ffi.rs # ÚNICO módulo com unsafe — extern "C" ABI
├── caller/mod.rs # ViolatedProperty, AnalysisResult, step counter
├── nondet/
│ ├── mod.rs # NonDetValue (enum), NonDetEntry
│ └── c_log.rs # log nondet do runtime C (NonDetLog.c, klee_log.csv)
├── memtrack/mod.rs # MemTrackEntry, VCC checks de memória
├── bbtrack/mod.rs # BasicBlockEntry, busca por linha
├── analysismode/
│ ├── mod.rs # VccChecker trait, VccContext, VccOutcome
│ ├── assert.rs # AssertChecker
│ ├── overflow.rs # AddI32, SubI32, MulI32 ... (checked_* arithmetic)
│ └── memory.rs # LoadChecker, FreeChecker, DerefChecker, MemCleanupChecker
└── output/mod.rs # to_json(), print_json() via serde_json
Map2Check Tool (LLVM Pass / Instrumentação)
│
│ extern "C" ABI (ffi.rs)
▼
┌─────────────────────────────────────────────┐
│ libmap2check.a │
│ │
│ caller ─┐ │
│ nondet ├──► AnalysisState │
│ memtrack│ OnceLock<Arc<Mutex<...>>> │
│ bbtrack ┘ │
│ │
│ analysismode ──► VccChecker trait │
│ output ──► serde_json │
└─────────────────────────────────────────────┘
| Padrão C | Equivalente Rust |
|---|---|
TAILQ globais sem lock |
OnceLock<Arc<Mutex<AnalysisState>>> |
union Data (type-punning) |
NonDetValue enum com dados; f32::from_bits() |
Buffer fixo char[512] sem bounds |
serde_json::to_string() — tamanho dinâmico |
search_in_container_by_address retorna ponteiro não-inicializado |
find_by_address retorna Option<&MemTrackEntry> |
Aritmética INT_MAX/INT_MIN manual |
i32::checked_add(), checked_sub() etc. |
lib/json-maker.c + ftoa.c |
serde_json + #[derive(Serialize)] |
Política de unsafe: somente ffi.rs (com wasm.rs e sys.rs, as chamadas da libc dos arquivos de resultado, do ambiente e do stderr) contém blocos unsafe. Todos os outros módulos têm #![deny(unsafe_code)]. Cada bloco unsafe possui um comentário // SAFETY:.
Sem modo de análise selecionado, map2check_success() emite no stdout um objeto map2check_log (numa execução do Map2Check, com modo, o resultado vai para os arquivos de propriedade, como no runtime C) com o veredito (result: "TRUE"/"FALSE"), a propriedade violada e os containers Container_TrackBBLog, Container_NonDetLog e, só em violações de memória, Container_AllocationLog. O formato exato, com exemplos verificados contra o serializador, está em docs/integration-guide.md.
docs/api-deltas.md: matriz de símbolos e assinaturas da API C (núcleo e passes do Map2Check) em relação ao C legado.docs/semantic-deltas.md: diferenças de comportamento, cada uma com caso reproduzível e teste.docs/integration-guide.md: como instalar os 21.bcno lugar dos do runtime C, o commit validado do Map2Check, como reproduzir o gate, como linkarlibmap2check.ae o formato do relatório JSON.docs/release.mdeCHANGELOG.md: processo de release e histórico de versões.
tests/compat_docs.rs falha em três casos: quando um export do header não está na matriz (ou está com a declaração errada), quando um SD-NN aponta para um teste que não existe e quando os exemplos JSON do guia divergem da saída real. Toda mudança na ABI C ou no relatório JSON atualiza esses documentos no mesmo PR.
Para montar o pacote de release localmente:
scripts/package-release.sh # dist/map2check-library-<versão>-<alvo>.tar.gz + SHA256SUMS (inclui os 21 .bc)