Array-Carrying Symbolic Execution for Function Contract Generation

1. O Problema

A geração automática de contratos de função (especificações que definem pré-condições, pós-condições e informações de atribuição/escrita em memória) é um problema fundamental na análise de programas, especialmente para a análise interprocedural. No entanto, a geração desses contratos para programas que manipulam arrays apresenta desafios significativos:

• Inferência de Invariantes: É difícil inferir invariantes precisos sobre segmentos contíguos de memória (arrays) que sejam válidos após a execução de loops.
• Informação de Atribuição (Assigns): Determinar exatamente quais partes de um array foram modificadas durante a execução de uma função é complexo, especialmente quando há múltiplos caminhos de execução ou loops com diferentes modos de saída.
• Limitações das Abordagens Existentes:
  • Interpretação Abstrata: Embora suporte segmentos de arrays, tem dificuldade em preservar informações disjuntivas sensíveis a caminhos (ex: diferentes modos de saída de um loop) e traduzi-las em contratos precisos.
  • Model Checking/SMT: Muitas vezes focam em provar asserções específicas em vez de gerar contratos reutilizáveis do tipo $\langle Pre, Post, Assign \rangle$.
  • Instrumentação: Requer especificação manual de variáveis fantasma e não trata nativamente segmentos contíguos.
  • LLMs (Modelos de Linguagem): Podem gerar resultados incorretos ("alucinações") e carecem de garantias de correção lógica.

2. Metodologia

Os autores propõem um novo framework de Execução Simbólica que "carrega" (propaga) invariantes e informações sobre segmentos contíguos de arrays ao longo da execução do programa.

Arquitetura do Framework:

1. Modelo de Memória Simbólica Estendido:
   • O sistema modela o acesso e modificação de arrays como operações de leitura e escrita em endereços de memória simbólicos.
   • Utiliza um mapa de memória ($M$) e um mapa de endereços ($A$) para rastrear estados simbólicos.
2. Carregamento de Invariantes e Segmentos:
   • Invariante Externo: O executor simbólico não tenta gerar invariantes do zero. Ele chama geradores externos (plugins) para obter invariantes numéricos e de array para os loops.
   • Segmentos Contíguos: O framework mantém uma estrutura de dados (Seg) que representa segmentos de arrays como triplas: $\langle \text{endereço\_base}, \text{comprimento}, \text{resumo\_conteúdo} \rangle$.
   • Resumo de Conteúdo ($C$): Pode ser um padrão indexado (ex: $arr[i] = i + 2$) ou uma abstração agregada (ex: soma, máximo).
3. Operações de Segmentos:
   • Leitura ($R$): Substitui o placeholder do índice no resumo do segmento pelo valor simbólico do índice.
   • Escrita ($W$): Pode dividir um segmento em dois (prefixo e sufixo) se a escrita ocorrer no meio do segmento, preservando os invariantes nas partes não afetadas.
   • Mesclagem (Merge): Após loops ou escritas, segmentos adjacentes com resumos de conteúdo sintaticamente equivalentes são mesclados para manter um resumo de alto nível.
4. Geração de Contratos:
   • Ao final da execução simbólica, os caminhos de execução são combinados.
   • As condições de caminho e os resumos de segmentos são projetados para gerar cláusulas ACSL (ANSI/ISO C Specification Language): requires (pré-condição), ensures (pós-condição) e assigns (memória modificada).
5. Implementação:
   • Protótipo implementado em C++ (~19.000 linhas) sobre a plataforma LLVM/Clang.
   • Integração com o Frama-C para verificação das especificações geradas.
   • Uso de plugins para análise de loops (baseados em lema de Farkas para invariantes afins e padrões de busca/redução).

3. Contribuições Principais

• Execução Simbólica Portadora de Arrays: Um framework que propaga ativamente invariantes e resumos de segmentos contíguos de arrays através das instruções do programa, permitindo a síntese de contratos gerais.
• Tratamento Refinado de Segmentos: Capacidade de lidar com a disjunção de segmentos (resultante de diferentes caminhos de execução ou modos de saída de loops) e operações de mesclagem/divisão precisas durante a execução simbólica.
• Síntese Automática de Contratos ACSL: Geração automática de contratos completos (pré, pós e assigns) para funções que manipulam arrays, sem necessidade de anotações manuais prévias.
• Validação Experimental: Implementação funcional e avaliação em benchmarks reais e sintéticos, demonstrando superioridade sobre ferramentas de estado da arte.

4. Resultados Experimentais

O framework foi avaliado em 282 programas C (incluindo suites SyGuS, OOPSLA-13, SV-Comp e bibliotecas reais como openHiTLS e X-509), comparado com a ferramenta AutoDeduct (que usa TriCera e ISP).

• Eficácia e Precisão:
  • A ferramenta proposta gerou contratos verificáveis para 68 dos 281 benchmarks.
  • A AutoDeduct conseguiu verificar completamente apenas 10 programas.
  • A grande vantagem foi a capacidade de lidar com propriedades complexas de memória e invariantes de loops que a AutoDeduct falhou em sintetizar (devido à falta de inferência de invariantes de loop robusta).
• Eficiência:
  • A ferramenta proposta foi significativamente mais rápida, com um tempo médio de 0,148 segundos por arquivo, contra 2,703 segundos da AutoDeduct (aproximadamente 17x mais rápida).
  • A eficiência deve-se ao design leve da execução simbólica, que evita a expansão de estados simbólicos através da abstração de segmentos de arrays em vez de desenrolar loops ou enumerar elementos.
• Limitações Identificadas:
  • Falhas na geração (69 casos) foram principalmente devido a limitações sintáticas do protótipo (operadores bit a bit, loops aninhados).
  • Não suporta ainda estruturas de ponteiros complexas (listas encadeadas, árvores), apenas aritmética de ponteiros simples baseada em arrays.

5. Significado e Impacto

Este trabalho representa um avanço significativo na análise estática de programas C, preenchendo uma lacuna crítica na geração automática de especificações formais para código que manipula arrays.

• Viabilidade Prática: A capacidade de gerar contratos precisos para bibliotecas criptográficas reais (como openHiTLS) demonstra que a técnica é aplicável a cenários do mundo real, onde a segurança e a correção de manipulação de memória são cruciais.
• Fundamento para Análise Interprocedural: Ao fornecer contratos precisos (incluindo informações de atribuição) para funções de baixo nível, o framework habilita análises mais profundas e precisas de programas maiores, permitindo que verificadores de software raciocinem sobre o comportamento global sem precisar analisar o código fonte de cada função individualmente.
• Alternativa Robusta a LLMs: O artigo oferece uma alternativa determinística e logicamente fundamentada às abordagens baseadas em LLMs para geração de especificações, garantindo a correção lógica através da execução simbólica e verificação formal.

Em resumo, a proposta introduz uma nova maneira de tratar arrays na execução simbólica, transformando a inferência de invariantes de arrays de um problema difícil em um processo automatizado e escalável, resultando em contratos de função mais precisos e verificáveis.