Resumo Técnico: SEAL – Execução Simbólica com Lógica de Separação

Declaração do Problema

A verificação de programas que manipulam estruturas de dados ligadas não limitadas continua sendo um desafio significativo na análise estática. Embora muitas ferramentas dependam de verificação de modelo limitado ou heurísticas especializadas, essas abordagens frequentemente lutam com a complexidade de raciocinar sobre comprimentos de listas arbitrários e formas de memória complexas. Além disso, os analisadores existentes baseados em lógica de separação (SL) frequentemente acoplam a análise com solvers dedicados e não modulares, limitando sua extensibilidade e capacidade de integração com outras teorias lógicas.

Metodologia

O SEAL é um analisador estático projetado para a verificação de programas que manipulam estruturas de dados ligadas não limitadas. Ele emprega interpretação abstrata direta (forward) sobre fórmulas de lógica de separação (SL). A metodologia central distingue-se através de uma arquitetura modular que desacopla claramente o motor de análise do motor de raciocínio lógico.

Componentes Principais

1. Domínio Abstrato (Heaps Simbólicos):

   • O SEAL representa estados de memória abstratos como heaps simbólicos, que são fórmulas de SL da forma $\exists x_1, \dots, x_m. \phi_1 * \dots * \phi_n$.
   • Fórmulas atômicas ($\phi_i$) incluem:
     • Fórmulas puras: Descrevendo igualdades (ou desigualdades) de ponteiros ou restrições em valores não-ponteiro.
     • Átomos de apontamento (points-to): Descrevendo células únicas de heap.
     • Predicados indutivos: Descrevendo sequências não limitadas de ponteiros (ex: listas).
     • Memória livre: Um predicado especial que representa explicitamente a memória liberada que permanece alcançável.
   • O domínio rastreia valores inteiros precisos dentro de um intervalo configurável (padrão $[-5, 5]$). Os estados nos locais do programa são representados como disjunções (conjuntos) de heaps simbólicos.

2. Abstração e Alargamento (Widening):

   • Para lidar com loops e espaços de estados infinitos, o SEAL realiza o alargamento generalizando as formas de memória. Isso envolve encontrar predicados espaciais compatíveis (apontamento ou predicados de lista) e uni-los em um único predicado de lista, desde que a localização de ligação não seja alvo de ponteiros externos ou variáveis do programa.
   • O sistema rastreia comprimentos mínimos de lista até um limite fixo para garantir garantias de aciclicidade durante a abstração.
   • Adivinhação de Predicados (Predicate Guessing): Atualmente, o SEAL adivinha o predicado indutivo esperado para estruturas C antes da análise com base na contagem de campos (ex: um campo autorreferencial $\to$ SLL; dois $\to$ DLL). Esta heurística pode levar a classificações incorretas (ex: uma estrutura pretendida como uma lista aninhada sendo classificada como uma lista duplamente ligada).

3. O Solver ASTRAL:

   • Ao contrário da maioria das ferramentas baseadas em SL que usam heurísticas dedicadas para satisfatibilidade e implicação, o SEAL depende do ASTRAL, um solver de lógica de separação de propósito geral.
   • O ASTRAL traduz fórmulas de SL em teorias SMT (especificamente bitvectors e arrays) usando um limite de desdobramento de predicado (unfolding).
   • As fórmulas traduzidas são passadas para o solver SMT BITWUZLA.
   • O ASTRAL suporta predicados indutivos definidos pelo usuário, permitindo que o SEAL defina seus próprios predicados sem suporte nativo do solver para eles.

4. Mecânica de Análise:

   • Pontos Fixos de Loop (Loop Fixpoints): Um ponto fixo é alcançado quando a implicação entre o estado da iteração atual do loop ($S$) e o estado da iteração anterior ($T$) é válida. Isso é aproximado verificando se para cada heap em $S$, existe um heap em $T$ que o implica.
   • Análise Interprocedural: Chamadas de função são otimizadas usando sumários (pares de pré-condição/pós-condição).
   • Simplificação: O sistema aplica simplificações sintáticas, como redução de classes de equivalência e remoção de variáveis fora de escopo.

Contribuições Principais

• Arquitetura Modular: Ao separar o motor de interpretação abstrata do motor de raciocínio lógico via ASTRAL, o SEAL alcança um design destinado a ser mais fácil de estender e combinar com o raciocínio em outras teorias.
• Solving de Propósito Geral: A integração com o ASTRAL permite que o SEAL aproveite solvers SMT para implicação e satisfatibilidade de SL, evitando a necessidade de solvers customizados e dedicados para cada variante específica de lógica.
• Verificação de Listas Não Limitadas: A ferramenta é capaz de verificar programas com listas ligadas não limitadas, uma categoria onde muitas ferramentas concorrentes falham.

Resultados Experimentais

O SEAL participou da categoria MemSafety-LinkedLists da competição SV-COMP.

• Desempenho Geral: No conjunto completo de 134 programas, o SEAL verificou 55 como "True" (correto) e encontrou 4 "False" (bugs), com 75 relatando nenhum resultado.
• Subconjunto de Listas Não Limitadas: No subconjunto de 69 programas que exigem raciocínio sobre estruturas de dados não limitadas, o SEAL verificou 14 programas como corretos e encontrou 2 bugs.
• Comparação:
  • O SEAL superou o 2LS (que verificou apenas 3 programas não limitados).
  • O SEAL verificou menos programas que o PREDATORHP (46) e o CPACHECKER (40), ambos que utilizam grafos de memória simbólica (SMGs).
  • O SEAL foi um dos apenas quatro analisadores capazes de verificar programas com listas não limitadas nesta categoria.

Significância e Alegações

O artigo posiciona o SEAL como um protótipo promissor com foco específico em extensibilidade em vez de dominância imediata de desempenho bruto.

• Potencial Futuro: Os autores afirmam que o design modular do SEAL e sua dependência do ASTRAL fornecem uma base sólida para suportar estruturas de dados complexas que não podem ser facilmente representadas por SMGs, como skip-lists e árvores.
• Limitações: Como um protótipo inicial, o SEAL atualmente suporta apenas um subconjunto de C (aritmética de ponteiros limitada, rastreamento de inteiros específico) e depende de adivinhação heurística de predicados, o que pode levar a falsos positivos ou incapacidade de relatar violações quando a informação de inteiros está ausente.
• Roteiro (Roadmap): Os autores pretendem melhorar a seleção de predicados durante a análise, sintetizar predicados indutivos a partir de exemplos e, potencialmente, incorporar o SEAL como um domínio abstrato dentro do framework Frama-C EVA para lidar com valores não-ponteiro mais complexos.

Em resumo, o SEAL demonstra que uma abordagem baseada em SMT de propósito geral para o solving de lógica de separação é uma alternativa viável e extensível aos heurísticos especializados, oferecendo um caminho para verificar estruturas de dados complexas e não limitadas em competições futuras.