Skip to content

TODO.md

Latest commit

 

History

History
227 lines (194 loc) · 12.8 KB

TODO.md

File metadata and controls

227 lines (194 loc) · 12.8 KB
Raw

TODO

Estado em 2026-10-28 (2.0.0-rc.1). O plano do runtime drop-in (docs/superpowers/plans/2026-10-26-runtime-drop-in-map2check.md) está concluído: o ABI C é o do runtime C do Map2Check develop, o pacote leva os 21 .bc e dois gates diferenciais passaram contra o develop 0bca42eb89d116178e6b52f52acaf73f7c305088 (gate de 2026-10-27 e gate de 2026-10-28). Falta só a release (tag v2.0.0-rc.1, PR e GitHub release), que o mantenedor faz sob pedido explícito (veja docs/release.md). Sugestões de adoção pelo Map2Check: docs/cutover/handoff-map2check.md.

Tudo abaixo é o relatório de paridade de antes do plano, mantido como histórico: as tarefas que descrevem a API núcleo 1.x (map2check_set_mode, map2check_map_*, JSON, libfuzzer) deixaram de ser ABI C na 2.0.0 (veja o CHANGELOG.md) e só valem para as funções Rust de map2check::ffi. O que segue aberto de fato: desempenho como benchmark periódico no CI, e a promoção do runtime Rust a padrão no Map2Check, decisão do mantenedor de lá.

TODO — paridade da implementação Rust

Comparação feita entre master (05b232a02a69d2a14114df9b34172e56f6365a7c) e feature/rust (417441b081c46815b42371a14af0ee5daccc08a4), antes deste relatório. O escopo é a paridade da biblioteca neste repositório; a integração com os passes e o frontend do projeto Map2Check não foi validada aqui.

Os módulos centrais de assert, overflow, memória, rastreamento de blocos, nondeterminismo e JSON já existem em Rust. As tarefas abaixo registram lacunas de ABI, comportamento e validação encontradas na comparação. As atividades adicionais abaixo foram extraídas de docs/plano_map2check_library_rust.md e não repetem as tarefas já listadas.

Prioridade alta — compatibilidade e correção

  • Alinhar a ABI C com a biblioteca Rust. Exportar ou justificar a remoção dos pontos de entrada existentes em master, incluindo get_next_step, map2check_map_non_static_alloca, map2check_map_funct_address e map2check_check_free_resolved_address. Alinhar também as assinaturas de map2check_save_nondet_log_*: em C elas recebem tipo e ponteiro para o valor e retornam um registro; em Rust recebem o valor diretamente e retornam void. Documentar explicitamente qualquer mudança intencional de contrato e regenerar/verificar include/map2check.h a partir da ABI efetiva. Referências: ffi.rs e as declarações C em master:include/nondet/nondetlog.h, master:include/caller/caller_lib_result.h e master:include/memtrack/container_memtracklog.h.

  • Implementar a semântica das opções de segurança de memória. map2check_set_memcleanup() e map2check_set_null_is_valid() são stubs vazios, e map2check_check_load() sempre passa is_null_valid: false. Armazenar essas opções no estado da análise e aplicá-las nos checks; preservar também o comportamento de map2check_check_mem_endprog() para os modos com e sem verificação de cleanup. Referências: ffi.rs, memory.rs e master:src/analysismode/analysis_memory.c.

  • Corrigir a validação de endereços após free. is_invalid_address() aceita um endereço se encontrar qualquer registro histórico não liberado. Como o registro de free é acrescentado sem remover o da alocação, um acesso posterior pode continuar sendo tratado como válido. Fazer a decisão considerar o evento mais recente aplicável à alocação e cobrir uso após liberação, realocação e limites de faixa com testes. Referências: memtrack/mod.rs e ffi.rs.

  • Restaurar ou substituir explicitamente a API de geração LibFuzzer. A implementação Rust exporta __VERIFIER_nondet_*, enquanto a biblioteca C ativa expõe map2check_gen_data_fuzzer_* e map2check_fuzzer_assume. Implementar os símbolos ainda consumidos ou migrar/documentar os consumidores para a nova API; verificar a tabela de símbolos e executar um programa C linkado contra a biblioteca Rust. Referências: libfuzzer.rs e master:include/nondet/nondet_gen_libfuzzer.h.

  • Manter o formato JSON compatível com o consumidor existente. Os nomes dos containers divergem (container_trackbb_log, container_nondet_log, container_memtrack_log em C; Container_BasicBlockLog, Container_NonDetLog, Container_AllocationLog em Rust). Também divergem os campos dos registros: C usa var_mem_address e mem_address_points_to, Rust usa var_addr e points_to; o registro C nondet usa type numérico e value escalar, Rust serializa value como enum marcado. Rust ainda emite function_name no nível do resultado, ausente no JSON C. Definir o schema suportado e cobri-lo com snapshots/testes de compatibilidade. A formatação compacta versus indentada, isoladamente, não altera o significado JSON. Referências: output/mod.rs, memtrack/mod.rs e nondet/mod.rs.

Prioridade média — estado e integração

  • Resetar o estado entre análises e iterações de fuzzing. map2check_init() chama OnceLock::get_or_init() e, portanto, não limpa contadores nem containers em chamadas subsequentes. Aplicar o reset do estado nos limites de ciclo de vida apropriados e testar duas inicializações e duas iterações LibFuzzer consecutivas, garantindo resultados independentes. Referências: ffi.rs, state.rs e libfuzzer.rs.

  • Validar os fluxos de build e testes C/KLEE/LibFuzzer. A feature klee está implementada (Task 2.7, docs/klee-feasibility.md); o Dockerfile tolera falhas ao emitir/linkar bitcode (|| true), e os scripts de integração ainda pressupõem o layout C em build/. Decidir e registrar se KLEE terá suporte Rust ou uma contingência C; em ambos os casos, fazer os builds falharem quando o artefato esperado estiver ausente e adicionar testes de link/execução C ao CI. Referências: Cargo.toml, Dockerfile, CI.yml, run_klee_test.sh e run_libfuzzer_test.sh.

  • Adicionar testes diferenciais contra a implementação C. Comparar, para programas de referência, ABI/símbolos, veredito, propriedade, linha e schema JSON entre master e Rust. Classificar divergências intencionais e executar os casos no CI; os testes unitários existentes não demonstram essa paridade ponta a ponta.

Outras atividades do plano

Prioridade alta — robustez e cobertura do contrato

  • Impedir que falhas atravessem a fronteira FFI sem tratamento. Definir o comportamento de panic por perfil de compilação e proteger exports extern "C" contra unwinding quando o perfil permitir recuperação; no perfil panic = "abort", documentar que não há recuperação. Adicionar um harness C que exercite exports antes da inicialização e entradas válidas de borda, e executar verificações com ASan/UBSan. Não passar ponteiros inválidos arbitrários: eles podem causar comportamento indefinido antes de qualquer validação Rust.

  • Completar ou descontinuar explicitamente os símbolos nondet restantes. Decidir o contrato para __VERIFIER_nondet_pointer, __VERIFIER_assume, __VERIFIER_assert, __VERIFIER_error, map2check_fuzzer_assume e os geradores pchar, loff_t e sector_t; implementar os que têm consumidores e registrar a remoção dos demais. Verificar as assinaturas/representações C e incluir testes de link e execução.

  • Cobrir a API C com programas de integração. Compilar, linkar e executar test/codeAPI_by_caller_test.c, test/codefuzz_by_caller_test.c e test/codeklee_by_caller_test.c contra a biblioteca gerada; manter esses casos como testes de CI, além dos testes unitários Rust.

Prioridade média — build, KLEE, desempenho e documentação

  • Corrigir e tornar estritos os builds de release e CI. Corrigir os caminhos/estágios do Dockerfile para os diretórios Rust e testes atuais; alinhar a versão Rust entre Dockerfile, rust-toolchain.toml e README; validar que geração do header, lint, formato, auditoria de dependências e cobertura executem no CI; remover artefatos de build legados que não sejam mais usados. Falhas na geração ou no link de bitcode não devem ser mascaradas por || true.

  • Executar o gate de viabilidade de KLEE e registrar a decisão. Feito na Task 2.7 (#20), decisão go em docs/klee-feasibility.md. Desde a 2.0.0 (Task 2.10) a rota legada (feature klee, scripts/build-klee-runtime.sh, tests/klee_paths.sh) saiu: o núcleo é a feature dropin de klee/Cargo.toml (rustc 1.72.1, bitcode LLVM 16, scripts/build-runtime-bc.sh), testado sob KLEE 3.1 por scripts/runtime-ir/test-klee-generator.sh.

  • Medir e controlar a regressão de desempenho. Criar benchmarks reproduzíveis contra a biblioteca C, usando programas de referência e corpus fixo para LibFuzzer; registrar medições e perfis quando o overhead exceder 10%. Adicionar execução periódica no CI e definir a regressão máxima aceitável como 10% na mediana.

  • Documentar desvios, compatibilidade e release. Manter uma matriz de símbolos/assinaturas com os desvios deliberados (docs/api-deltas.md), classificar diferenças semânticas com casos reproduzíveis (docs/semantic-deltas.md), atualizar o changelog e publicar o header C e guia de integração junto à versão liberada.

Dependente do repositório externo hbgit/Map2Check

Recomeçado em 2026-10-26: o trabalho do PR #76 saiu do develop do Map2Check (force push a0f8b9cd → fbbcb929). O novo plano é docs/superpowers/plans/2026-10-26-runtime-drop-in-map2check.md: a biblioteca exporta o ABI do runtime C do develop. Os itens abaixo são do plano anterior e valem só como histórico.

  • Adicionar uma camada de compatibilidade para os passes atuais. Em map2check-library, implementar uma feature isolada que exporte os nomes e assinaturas usados pelos passes de Map2Check@develop, delegando à API núcleo; incluir a matriz completa de símbolos e resolver/documentar a colisão de assinatura de map2check_check_deref. Excluir explicitamente símbolos wasm se permanecerem fora do escopo. A parte do SD-17 sobre list_log.csv foi fechada na Task 2.5: map2check_check_free/map2check_map_free recebem o endereço da variável-ponteiro, a linha FREE nomeia a variável certa e um free inválido mantém a linha que o develop acrescenta antes de checar (golden FALSE-FREE pelo caminho map2check_free; o antigo virou FALSE-FREE-RESOLVED).

  • Compatibilizar o canal de resultado legado. Feito na Task 2.4 (#19): rust/src/output/legacy_files.rs e golden tests em tests/legacy_golden/. Pendências em SD-17. Texto original: Além do JSON, implementar a escrita dos arquivos-sentinela map2check_property_* nos nomes e formatos aceitos pelo parser atual do Map2Check. Adicionar golden tests para arquivos e JSON e validar propriedade, linha e função contra saídas da biblioteca C embutida.

  • Integrar Rust ao CMake do Map2Check sob uma opção opt-in. No repositório hbgit/Map2Check, adicionar MAP2CHECK_RUST_RUNTIME inicialmente desligada, compilar/linkar libmap2check.a nos fluxos nativos e aplicar a decisão de KLEE registrada acima. Impedir link simultâneo de runtimes com símbolos duplicados e testar a opção com uma regressão pequena.

  • Migrar consumidores e aposentar a compatibilidade somente após paridade. Após um ciclo de regressão sem diferenças não adjudicadas, migrar os passes para a API núcleo e o frontend para o JSON; então remover a camada compatível e o runtime C embutido apenas quando não houver símbolos ou consumidores órfãos. Manter a opção de retorno ao runtime antigo durante a transição.

  • Aplicar critérios de prontidão antes de promover a integração. Exigir cobertura dos símbolos necessários, regressões sem divergências não adjudicadas, overhead dentro do limite acordado, fluxos None/LibFuzzer e a decisão KLEE verificados, além da documentação e release versionada. Adiar a promoção para default se qualquer gate estiver pendente.