Resumo Técnico: Satisfiabilidade Modulo Arrays Constantes Extensionais

Declaração do Problema

O raciocínio sobre estruturas de dados de arrays, particularmente em combinação com inteiros de máquina, é um requisito fundamental para a verificação de hardware e software. A teoria padrão de Satisfiabilidade Modulo Teorias (SMT) de arrays extensionais, conforme definida em SMT-LIB e axiomatizada por McCarthy, fornece os operadores select (leitura) e store (escrita), juntamente com um axioma de extensionalidade. Embora suficiente para muitas tarefas de verificação, esta teoria carece de concisão ao modelar arrays inicializados com um valor padrão (por exemplo, memória inicializada com zero).

Na teoria padrão, tal inicialização deve ser expressa por meio de expressões store profundamente aninhadas, escrevendo o valor padrão em cada índice relevante. Isso leva a imprecisões na modelagem (os índices só podem ser sobrescritos explicitamente) e a ineficiências severas nos procedimentos de resolução devido à profundidade das cadeias de store.

A extensão da teoria com arrays constantes — arrays que armazenam um único elemento em cada índice — oferece uma solução concisa. No entanto, os procedimentos de decisão existentes para arrays constantes extensionais restringem-se a domínios de índices infinitos. Para domínios de índices finitos, os solucionadores SMT existentes suportam apenas fragmentos não extensionais ou, no caso de alguns solucionadores, produzem respostas incorretas ao raciocinar sobre extensionalidade em arrays constantes com índices finitos. O desafio central reside em determinar se duas sequências de operações store sobre diferentes arrays constantes com domínios finitos podem ser tornadas iguais mediante a atualização suficiente dos índices, um problema que não surge no caso infinito.

Metodologia

Os autores apresentam um novo procedimento de decisão para a teoria de arrays constantes extensionais ($T_{\langle A \rangle}$) que suporta domínios de índices arbitrários, incluindo os finitos. O procedimento é formalizado como um cálculo abstrato, CAEXT, que generaliza e estende o procedimento Lemmas on Demand (LOD) para arrays extensionais (DPA) apresentado em trabalhos anteriores.

O Cálculo CAEXT

O cálculo opera sobre configurações $\langle A, I, \pi \rangle$, onde $A$ é um conjunto de literais planos, $I$ é uma interpretação na teoria vazia ($T_E$) e $\pi$ é um mapa de etapas de propagação. O procedimento evita a introdução de leituras virtuais para todos os índices (o que é inviável para domínios infinitos e computacionalmente caro para domínios finitos grandes) propagando valores padrão e rastreando índices atualizados.

Os componentes-chave do cálculo incluem:

1. Cálculo Base (AEXT): Generaliza o procedimento LOD para sorts de índices e elementos arbitrários, desacoplando-o de combinações de teorias específicas. Ele propaga informações de leitura com base nos axiomas de leitura-sobre-escrita de McCarthy (row-eq, row-ne) e no axioma de extensionalidade (ext).
2. Extensão para Arrays Constantes:
   • Propagação de Valores Padrão: Em vez de gerar leituras para cada índice, o cálculo propaga o valor padrão $v$ de um array constante $\langle v \rangle$ para outros arrays. Ele mantém um conjunto de índices atualizados $I(a, \langle v \rangle)$, representando os índices onde o array $a$ difere do valor padrão $\langle v \rangle$ ao longo do caminho de propagação.
   • Detecção de Conflitos (CongC): Quando dois valores padrão diferentes $v$ e $w$ são propagados para o mesmo array $a$, o cálculo verifica se o conjunto de índices atualizados $I(a, \langle v \rangle) \cup I(a, \langle w \rangle)$ cobre todo o domínio de índices. Se o domínio for finito e os índices atualizados não cobrirem todos os índices possíveis, um conflito surge, a menos que $v \approx w$.
   • Codificação DistinctN: Para lidar eficientemente com a fórmula quantificada $\exists i : \sigma. \bigwedge_{k \in I} i \neq k$ (verificando se existe um índice não atualizado), a implementação codifica isso como uma restrição especializada distinctN. Isso verifica se o conjunto de índices atualizados contém pelo menos $n$ valores distintos, onde $n$ é o tamanho do domínio de índices.

Implementação

O procedimento de decisão é implementado no solucionador SMT de última geração Bitwuzla. Ele integra-se perfeitamente à arquitetura LOD existente do Bitwuzla, onde o solucionador de vetores de bits fornece a interpretação $I$. A implementação inclui otimizações como expansão preguiçosa de restrições distinctN e busca em largura para caminhos de propagação, a fim de minimizar a sobrecarga de memória.

Contribuições Principais

1. Generalização do LOD: Os autores generalizam o procedimento LOD para arrays extensionais com vetores de bits de tamanho fixo para sorts de índices e elementos arbitrários.
2. Cálculo Abstrato AEXT: Eles apresentam o AEXT como um cálculo abstrato desacoplado para a teoria extensional de arrays, independente do paradigma de resolução LOD.
3. Extensão para Arrays Constantes (CAEXT): Eles estendem o AEXT para lidar com arrays constantes extensionais, provando correção refutacional (se for relatado unsat, a entrada é insatisfatível) e correção de satisfiabilidade (se uma configuração saturada for alcançada sem unsat, a entrada é satisfatível).
4. Implementação e Avaliação: O procedimento é implementado no Bitwuzla e avaliado em diversos benchmarks, demonstrando melhorias significativas de desempenho em relação ao Bitwuzla base e a outros solucionadores líderes (Z3, cvc5, MathSAT5).

Resultados

A avaliação foi conduzida em cinco conjuntos de benchmarks: smtlib (lógicas quantificadas), mbqi (subconsultas de instanciação de quantificadores baseada em modelo), k-ind (verificação incremental de modelo de hardware), hevm (máquina virtual Ethereum) e crafted (benchmarks sintéticos projetados especificamente para testar a extensionalidade de arrays constantes finitos).

• Desempenho: O Bitwuzla com o novo procedimento (Bitwuzla⟨A⟩) superou significativamente todos os outros solucionadores. No conjunto smtlib, o número de benchmarks resolvidos aumentou por um fator de 5 em comparação com o Bitwuzla base (3.545 vs. 717). No conjunto mbqi, o Bitwuzla⟨A⟩ resolveu todas as 4.147 consultas, enquanto a versão base resolveu apenas 4.
• Correção: No conjunto crafted⟨A⟩, que codifica igualdades sobre arrays constantes finitos com diferentes valores padrão, o Bitwuzla⟨A⟩ foi o único solucionador a fornecer respostas corretas para todas as instâncias. O Z3 e o MathSAT5 aceitaram as entradas, mas relataram respostas erradas para um número significativo de benchmarks. O cvc5 e o Bitwuzla base rejeitaram as entradas completamente devido à falta de suporte.
• Verificação de Correção: Os autores verificaram os modelos produzidos pelos solucionadores no conjunto crafted⟨A⟩. Apenas o Bitwuzla⟨A⟩ produziu modelos consistentes com suas próprias alegações de satisfiabilidade. O Z3 e o MathSAT5 produziram modelos que, quando assertados de volta às fórmulas originais, levaram a contradições.

Significância

O artigo afirma que o procedimento de decisão proposto expande significativamente as capacidades de resolução do Bitwuzla, permitindo-lhe lidar com problemas envolvendo arrays constantes extensionais com domínios de índices finitos que anteriormente eram insolúveis ou tratados incorretamente por outras ferramentas.

O trabalho aborda uma lacuna crítica na resolução SMT: enquanto arrays constantes são um padrão de modelagem para inicialização de memória, os solucionadores existentes ou carecem de suporte para eles em domínios finitos ou fornecem resultados não sólidos. Ao fornecer um procedimento de decisão sólido e completo para a teoria completa de arrays constantes extensionais (tanto finitos quanto infinitos), este trabalho permite uma verificação mais precisa e eficiente em aplicações como verificação de modelo de hardware e verificação de contratos inteligentes (especificamente para a Máquina Virtual Ethereum). Os autores observam que, embora sua avaliação tenha focado em domínios finitos, o procedimento é agnóstico à arquitetura subjacente do solucionador e suporta plenamente o caso de domínio infinito também.