Feat wasm verification

[GuilhermeBn198]

Summary

Pipeline WASM end-to-end validado: o Map2Check agora verifica binários .wasm diretamente via map2check --wasm, reaproveitando todo o pipeline LLVM 16 + KLEE existente. 15 casos da Juliet Test Suite (CWE-121/122/124/126/127) foram validados com 15/15 FALSE. Infraestrutura de CI completa com jobs de build, testes unitários, análise estática, sanitizers e novo job E2E com KLEE real em container Docker.

Motivation

O pipeline WASM estava implementado mas não validado empiricamente. Os resultados eram inconsistentes entre execuções locais e CI devido a 4 problemas críticos de infraestrutura:

1. WABT 1.0.27 do apt vs 1.0.41 do Dockerfile.dev: wasm-rt.h do apt não tem wasm_rt_funcref_table_t nem bool is64 — WasmRuntimeStubs.c quebrava
2. Build estático não acha Z3.so: CMAKE_FIND_LIBRARY_SUFFIXES=".a" impedia o build com KLEE em ambientes com Z3/STP apenas como bibliotecas compartilhadas
3. Install rules incompletas: ninja install não copiava klee-uclibc.bca nem compiler-rt, causando crash do KLEE no E2E
4. Timeout insuficiente: 110s produzia UNKNOWN em todos os casos Juliet; 290s permite exploração suficiente para encontrar as violações

Type of change

• New feature (non-breaking change which adds functionality)
• Bug fix (non-breaking change which fixes an issue)
• This change requires a documentation update

How Has This Been Tested?

• CI GitHub Actions: jobs build-and-test, static-analysis, sanitizer-tests passando (build limpo com clang-16, sem warnings novos)
• CI job e2e-wasm: build em container Docker com KLEE real, executa test_wasm_pipeline.sh (3/3) + test_wasm_entrypoint.sh (3/3)
• Juliet WASM benchmarks: 15 casos (CWE-121/122/124/126/127) executados com map2check --wasm --memtrack --timeout 290, 15/15 FALSE
• Unit tests: 7/7 passando (ctest --output-on-failure)

Para reproduzir localmente:

docker run --rm -v $(pwd):/workspace -w /workspace -u root ghcr.io/hbgit/map2check-dev:latest bash -c '
  wget -q "https://github.com/WebAssembly/wabt/releases/download/1.0.41/wabt-1.0.41-linux-x64.tar.gz" -O /tmp/w.tgz
  tar xzf /tmp/w.tgz -C /opt && ln -sf /opt/wabt-1.0.41/bin/wasm2c /usr/local/bin/wasm2c
  wget -q "https://github.com/WebAssembly/wasi-sdk/releases/download/wasi-sdk-33/wasi-sdk-33.0-x86_64-linux.tar.gz" -O /tmp/s.tgz
  tar xzf /tmp/s.tgz -C /opt
  mkdir -p build && cd build
  cmake .. -G Ninja -DLLVM_DIR=/usr/lib/llvm-16/lib/cmake/llvm -DMAP2CHECK_DYNAMIC_LINK=ON
  ninja && ninja install
  mkdir -p ../install/lib/klee && ln -sf /opt/klee/lib/klee/runtime ../install/lib/klee/runtime
  ln -sf /usr/lib/llvm-16/lib/clang ../install/lib/clang
  MAP2CHECK_PATH=$PWD/../install WASI_SDK_PATH=/opt/wasi-sdk-33.0-x86_64-linux bash ../tests/integration/test_wasm_pipeline.sh
  MAP2CHECK_PATH=$PWD/../install WASI_SDK_PATH=/opt/wasi-sdk-33.0-x86_64-linux bash ../tests/integration/test_wasm_entrypoint.sh
'

Changes

Pipeline WASM (modules/frontend/, modules/backend/)

• wasm_lifter.{hpp,cpp} — orquestra .wasm → wasm2c → clang-16 → LLVM IR
• map2check.cpp — flag --wasm com detecção automática de entrypoint e fallback de include paths (/opt/wabt-1.0.41/include → /opt/wabt/include → /usr/include)
• caller.{hpp,cpp} — generateWasmWrapperStatic() cria main() → w2c_*_start; linka WasmRuntimeStubs.bc quando --wasm ativo
• WasmRuntimeStubs.c — substitui mmap/munmap do WABT por calloc/free compatíveis com KLEE; redireciona wasm_rt_trap → map2check_error
• MemoryTrackPass.{hpp,cpp} — modo --wasm-mode: intercepta w2c_*_dlmalloc/dlfree, registra offsets no AllocationLog, injeta map2check_wasm_check_access em loads/stores (bounds checking por alocação)
• Map2CheckLibrary.cpp — suporte a --entry-function configurável
  Build System (CMakeLists.txt, modules/backend/library/lib/CMakeLists.txt)
• MAP2CHECK_DYNAMIC_LINK=ON — desabilita busca por .a e permite find_library encontrar .so (Z3/STP no Dockerfile.dev só existem como shared)
• WasmRuntimeStubs restaurado como target ALL quando wasm-rt.h é encontrado
• Version string: v8.0.0 (LLVM 16, C++17, New PM)
  CI (.github/workflows/ci.yml)
• Novo job e2e-wasm: build em container Docker com KLEE real, executa ambos os scripts de integração WASM, timeout de 45min
• Substituição de apt install wabt (1.0.27) por WABT 1.0.41 via GitHub releases nos 3 jobs (build-and-test, static-analysis, sanitizer-tests)
• Ambos docker run no job E2E executam como root (-u root) para acesso de escrita em /opt/ e /workspace/

Testes (tests/integration/)

• test_wasm_pipeline.sh — 3 cenários: heap overflow, heap seguro, flag CLI
• test_wasm_entrypoint.sh — 3 cenários: entrypoint _start, módulos com caracteres hex-encoded, módulos com imports WASI
• Regex corrigida para aceitar entrypoints _0x5Fstart (hex-encoded)
  Benchmarks Juliet WASM (test-comp2026/simulation/)
• compile_juliet_wasm.sh — 15 casos (CWE-121/122/124/126/127)
• wasm_results.csv — 15/15 FALSE com timeout 290s (tempos de 135-179s)

Documentação

• README.md — instruções de build com Dockerfile.dev e MAP2CHECK_DYNAMIC_LINK
• docs/migration/1.7-wasm-pipeline.md — status atualizados das sub-etapas 1.7.1-1.7.7
• .opencode/skills/map2check-sbseg2026/ — backlog, consolidated data e figure inventory atualizados com dados reais

Checklist

• My code follows the style guidelines of this project
• I have performed a self-review of my own code
• I have made corresponding changes to the documentation (README, SKILL.md, chapters, migration docs)
• My changes generate no new warnings (build limpo com clang-16 em todos os 4 jobs do CI)
• I have added tests that prove my feature works (test_wasm_{pipeline,entrypoint}.sh)
• New and existing unit tests pass locally with my changes (7/7)
• Any dependent changes have been merged and published in downstream modules