A Modular Framework for Stack-Heap and Value Abstractions (Extended Version)

Resumo Técnico: Um Framework Modular para Abstrações de Pilha-Heap e Valores

Declaração do Problema
A análise estática de programas avançada requer um raciocínio preciso sobre a semântica de memória, particularmente a interação entre alocações de pilha (estáticas) e heap (dinâmicas), e como estas afetam os valores do programa. Em linguagens como C e C++, o gerenciamento manual de memória introduz riscos como estouros de buffer (buffer overflows), erros de uso após liberação (use-after-free) e exceções de ponteiro nulo. Por outro lado, linguagens como Java e Python utilizam coleta de lixo automática, mas os comportamentos de memória subjacentes ainda variam significativamente.

Um desafio crítico na análise estática é que a análise de memória (rastreamento de ponteiros, aliases, e estruturas) e a análise de valores (rastreamento de propriedades numéricas, constantes e intervalos) têm se desenvolvido ortogonalmente ao longo do tempo. Embora a combinação destas análises seja conhecida como essencial para resultados significativos, as abordagens existentes frequentemente carecem de generalidade. Algumas ferramentas pré-processam programas para substituir acessos ao heap por variáveis simbólicas, enquanto outras dependem de extensões manuais ou especificações de estruturas de dados específicas. Há uma falta de frameworks verdadeiramente genéricos e totalmente automáticos que possam suportar diversos modelos de memória (de C a linguagens orientadas a objetos) e permitir que os domínios de valor e memória sejam escolhidos e combinados independentemente, sem a necessidade de anotações fornecidas pelo usuário.

Metodologia
Os autores propõem um framework genérico e paramétrico baseado na teoria da Interpretação Abstrata. A inovação central é uma abstração de estado dividida que separa formalmente o estado do programa em dois componentes modulares: um componente de valor ($\nu$) e um componente de memória ($\mu$).

1. Linguagem Formal ($\mu$LL): O framework é definido sobre $\mu$LL, uma linguagem imperativa pequena que estende $\mu$JS com ponteiros explícitos, operações de endereço-de, desreferência, acesso a campos e alocação de heap. Esta linguagem serve como um modelo para comportamentos de memória do tipo C++.
2. Construção de Estado Dividido: Os autores definem uma transformação de estado concreto-para-dividido que é um Isomorfismo de Galois. Diferente de trabalhos anteriores que estabeleceram uma Conexão de Galois (o que pode introduzir imprecisão), esta abordagem garante um mapeamento bijetivo entre o estado concreto (mapas de pilha e heap) e o estado dividido.
   • O Componente de Valor ($\nu$) armazena valores primitivos e valores de campos.
   • O Componente de Memória ($\mu$) armazena endereços de memória e relações de ponteiros.
   • Objetos são "explodidos" em mapeamentos de campos planos, onde cada campo é armazenado no componente de valor ou de memória, dependendo do seu tipo (primitivo vs. endereço).
3. Interação Modular: O framework define uma interface leve através da qual o domínio de valor ($V^\sharp$) e o domínio de memória ($M^\sharp$) cooperam:
   • Identificadores de Memória (MemID): Nomes abstratos representando localizações de memória concretas.
   • Substituições: Quando o domínio de memória reorganiza localizações (por exemplo, fundindo ou dividindo nós), ele comunica estas mudanças ao domínio de valor via substituições, garantindo consistência.
   • Operações: O framework especifica um conjunto de operações requeridas para cada domínio (ex: assign, assume, pointsTo, access, fresh) que lidam com o fluxo de informação. O domínio de valor lida com aritmética e lógica booleana, enquanto o domínio de memória lida com a estrutura de ponteiros e alocação.
4. Corretude (Soundness): A corretude da análise combinada é garantida pela corretidão dos domínios individuais e pela correção de sua interação via mecanismo de substituição. O framework prova que, se os domínios individuais satisfizerem condições locais específicas (C1–C2 e M1–M6), a semântica abstrata combinada é correta em relação às semânticas concretas.

Principais Contribuições
O artigo apresenta quatro principais contribuições técnicas:

• Semântica Operacional Formal: Uma semântica para $\mu$LL que modela tanto a pilha quanto o heap, suportando alocação dinâmica, aliasing de ponteiros e estruturas de dados complexas.
• Abstração de Estado Dividido: Uma reformulação do estado concreto como um Isomorfismo de Galois que separa a informação de valor e endereço sem perda de precisão. Isso permite que as análises de valor e memória operem em subcomponentes distintos e bem definidos do estado.
• Framework Abstrato Paramétrico: Uma arquitetura modular onde os domínios de valor e memória interagem através de uma interface leve e um mecanismo de substituição. Este design suporta uma ampla gama de modelos de memória (incluindo a manipulação diversa de C) e permite que qualquer domínio de valor compatível seja pareado com qualquer domínio de memória compatível.
• Instanciações Concretas: Os autores demonstram a aplicabilidade do framework instanciando-o com domínios numéricos não-relacionais (ex: Intervalos, Sinal, Propagação de Constantes) para valores e uma análise de points-to do tipo Andersen para memória.

Resultos e Avaliação
O artigo não apresenta benchmarks de larga escala, mas fornece uma validação teórica e exemplos ilustrativos:

• Demonstração de Modularidade: Um programa de exemplo envolvendo alocação de heap e atualizações condicionais mostra que a troca do domínio de valor (ex: de Propagação de Constantes para Intervalos ou para Conjuntos de Constantes) altera a precisão dos resultados enquanto deixa o domínio de memória e a lógica central do framework inalterados.
• Rastreamento de Interação: Os autores rastreiam a execução de um programa rico em ponteiros (baseado em um benchmark do SV-COMP) para demonstrar como o domínio de memória rastreia aliases de ponteiros (ex: tail e x apontando para a mesma estrutura) enquanto o domínio de valor rastreia os dados armazenados nessas localizações.
• Comportamento de Convergência: Em um exemplo combinado envolvendo um contador e campos de heap, os autores mostram como o domínio de memória atinge um ponto fixo (fixpoint) independentemente do comportamento de convergência do domínio de valor (ex: o domínio de intervalos exigindo alargamento/widening enquanto o domínio de sinal não exige), destacando a natureza independente, porém cooperativa, do estado dividido.

Significância
O artigo reivindica significância ao fornecer uma base flexível para a construção de análises estáticas que sejam adaptáveis a diferentes linguagens de programação e requisitos de análise. Ao desacoplar o raciocínio de memória e de valor, o framework:

• Aumenta a Reutilização: Domínios abstratos existentes podem ser integrados ao framework com adaptações mínimas a uma interface comum.
• Melhora a Precisão: Permite o rastreamento de informações de valor em localizações de memória (ex: o valor de um campo em um objeto de heap) de uma forma que não é possível em produtos cartesianos simples ou análises isoladas.
• Garante a Corretude Composicional: O framework garante que, se os componentes individuais forem corretos, a combinação também será correta por construção, eliminando a necessidade de re-provar a correção para cada nova combinação de domínios.

Os autores posicionam este trabalho como uma extensão de frameworks anteriores (especificamente Ferrara [19,18] e Negrini [34]), melhorando-os ao suportar referências arbitrárias, acessos dinâmicos a campos e ao impor um Isomorfismo de Galois para eliminar a perda de precisão durante a transformação do estado dividido. O trabalho futuro envolve a integração deste framework na plataforma de análise estática LiSA para suportar linguagens como C, C++ e Rust, além de LLVM-IR.