Resumen Técnico: Satisfacibilidad Modulo Arrays Constantes Extensionales

Enunciado del Problema

El razonamiento sobre estructuras de datos de tipo array, particularmente en combinación con enteros de máquina, es un requisito fundamental para la verificación de hardware y software. La teoría estándar de Satisfacibilidad Modulo Teorías (SMT) de arrays extensionales, definida en SMT-LIB y axiomatizada por McCarthy, proporciona los operadores select (lectura) y store (escritura) junto con un axioma de extensionalidad. Aunque es suficiente para muchas tareas de verificación, esta teoría carece de concisión al modelar arrays inicializados con un valor predeterminado (por ejemplo, memoria inicializada a cero).

En la teoría estándar, dicha inicialización debe expresarse mediante expresiones store anidadas profundamente que escriben el valor predeterminado en cada índice relevante. Esto conduce a imprecisiones en el modelado (los índices solo pueden sobrescribirse explícitamente) y a ineficiencias graves en los procedimientos de resolución debido a la profundidad de las cadenas de store.

Extender la teoría con arrays constantes—arrays que almacenan un único elemento en cada índice—ofrece una solución concisa. Sin embargo, los procedimientos de decisión existentes para arrays constantes extensionales están restringidos a dominios de índices infinitos. Para dominios de índices finitos, los solucionadores SMT existentes solo soportan fragmentos no extensionales o, en el caso de algunos solucionadores, producen respuestas incorrectas al razonar sobre extensionalidad en arrays constantes con índices finitos. El desafío central radica en determinar si dos secuencias de operaciones store sobre diferentes arrays constantes con dominios finitos pueden hacerse iguales mediante actualizaciones suficientes de los índices, un problema que no surge en el caso infinito.

Metodología

Los autores presentan un procedimiento de decisión novedoso para la teoría de arrays constantes extensionales ($T_{\langle A \rangle}$) que soporta dominios de índices arbitrarios, incluidos los finitos. El procedimiento se formaliza como un cálculo abstracto, CAEXT, que generaliza y extiende el procedimiento de Lemas bajo Demanda (LOD) para arrays extensionales (DPA) presentado en trabajos anteriores.

El Cálculo CAEXT

El cálculo opera sobre configuraciones $\langle A, I, \pi \rangle$, donde $A$ es un conjunto de literales planos, $I$ es una interpretación en la teoría vacía ($T_E$) y $\pi$ es un mapa de pasos de propagación. El procedimiento evita la introducción de lecturas virtuales para todos los índices (lo cual es inviable para dominios infinitos y computacionalmente costoso para dominios finitos grandes) propagando valores predeterminados y rastreando índices actualizados.

Los componentes clave del cálculo incluyen:

1. Cálculo Base (AEXT): Generaliza el procedimiento LOD a órdenes de índices y elementos arbitrarios, desacoplandolo de combinaciones de teorías específicas. Propaga información de lectura basada en los axiomas de lectura-sobre-escritura de McCarthy (row-eq, row-ne) y el axioma de extensionalidad (ext).
2. Extensión a Arrays Constantes:
   • Propagación de Valores Predeterminados: En lugar de generar lecturas para cada índice, el cálculo propaga el valor predeterminado $v$ de un array constante $\langle v \rangle$ a otros arrays. Mantiene un conjunto de índices actualizados $I(a, \langle v \rangle)$, que representan los índices donde el array $a$ difiere del valor predeterminado $\langle v \rangle$ a lo largo de la ruta de propagación.
   • Detección de Conflictos (CongC): Cuando dos valores predeterminados diferentes $v$ y $w$ se propagan al mismo array $a$, el cálculo verifica si el conjunto de índices actualizados $I(a, \langle v \rangle) \cup I(a, \langle w \rangle)$ cubre todo el dominio de índices. Si el dominio es finito y los índices actualizados no cubren todos los índices posibles, surge un conflicto a menos que $v \approx w$.
   • Codificación DistinctN: Para manejar eficientemente la fórmula cuantificada $\exists i : \sigma. \bigwedge_{k \in I} i \neq k$ (verificar si existe un índice no actualizado), la implementación codifica esto como una restricción especializada distinctN. Esto verifica si el conjunto de índices actualizados contiene al menos $n$ valores distintos, donde $n$ es el tamaño del dominio de índices.

Implementación

El procedimiento de decisión está implementado en el solucionador SMT de vanguardia Bitwuzla. Se integra perfectamente con la arquitectura LOD existente de Bitwuzla, donde el solucionador de vectores de bits proporciona la interpretación $I$. La implementación incluye optimizaciones como la expansión perezosa de las restricciones distinctN y la búsqueda en anchura para las rutas de propagación, con el fin de minimizar la sobrecarga de memoria.

Contribuciones Clave

1. Generalización de LOD: Los autores generalizan el procedimiento LOD para arrays extensionales con vectores de bits de tamaño fijo a órdenes de índices y elementos arbitrarios.
2. Cálculo Abstracto AEXT: Presentan AEXT como un cálculo abstracto desacoplado para la teoría extensional de arrays, independiente del paradigma de resolución LOD.
3. Extensión a Arrays Constantes (CAEXT): Extienden AEXT para manejar arrays constantes extensionales, demostrando corrección refutacional (si se reporta unsat, la entrada es insatisfacible) y corrección de satisfacibilidad (si se alcanza una configuración saturada sin unsat, la entrada es satisfacible).
4. Implementación y Evaluación: El procedimiento se implementa en Bitwuzla y se evalúa en diversos conjuntos de pruebas, demostrando mejoras significativas en el rendimiento sobre la versión base de Bitwuzla y otros solucionadores líderes (Z3, cvc5, MathSAT5).

Resultados

La evaluación se realizó en cinco conjuntos de pruebas: smtlib (lógicas cuantificadas), mbqi (subconsultas de instanciación de cuantificadores basada en modelos), k-ind (verificación incremental de modelos de hardware), hevm (máquina virtual de Ethereum) y crafted (pruebas sintéticas diseñadas específicamente para probar la extensionalidad de arrays constantes finitos).

• Rendimiento: Bitwuzla con el nuevo procedimiento (Bitwuzla⟨A⟩) superó significativamente a todos los demás solucionadores. En el conjunto smtlib, el número de pruebas resueltas aumentó en un factor de 5 en comparación con la versión base de Bitwuzla (3.545 frente a 717). En el conjunto mbqi, Bitwuzla⟨A⟩ resolvió las 4.147 consultas, mientras que la versión base resolvió solo 4.
• Corrección: En el conjunto crafted⟨A⟩, que codifica igualdades sobre arrays constantes finitos con diferentes valores predeterminados, Bitwuzla⟨A⟩ fue el único solucionador que proporcionó respuestas correctas para todas las instancias. Z3 y MathSAT5 aceptaron las entradas pero reportaron respuestas incorrectas para un número significativo de pruebas. cvc5 y la versión base de Bitwuzla rechazaron las entradas por completo debido a la falta de soporte.
• Verificación de Corrección: Los autores verificaron los modelos producidos por los solucionadores en el conjunto crafted⟨A⟩. Solo Bitwuzla⟨A⟩ produjo modelos consistentes con sus propias afirmaciones de satisfacibilidad. Z3 y MathSAT5 produjeron modelos que, al afirmarse de nuevo en las fórmulas originales, condujeron a contradicciones.

Significado

El artículo afirma que el procedimiento de decisión propuesto expande significativamente las capacidades de resolución de Bitwuzla, permitiéndole manejar problemas que involucran arrays constantes extensionales con dominios de índices finitos que anteriormente eran irresolubles o se manejaban incorrectamente por otras herramientas.

El trabajo aborda una brecha crítica en la resolución SMT: aunque los arrays constantes son un patrón de modelado estándar para la inicialización de memoria, los solucionadores existentes carecen de soporte para ellos en dominios finitos o proporcionan resultados no sound. Al proporcionar un procedimiento de decisión sound y completo para la teoría completa de arrays constantes extensionales (tanto finitos como infinitos), este trabajo permite una verificación más precisa y eficiente en aplicaciones como la verificación de modelos de hardware y la verificación de contratos inteligentes (específicamente para la Máquina Virtual de Ethereum). Los autores señalan que, aunque su evaluación se centró en dominios finitos, el procedimiento es agnóstico a la arquitectura del solucionador subyacente y soporta completamente el caso de dominio infinito.