Solvers SMT e Procedimentos de Decisão

• Explicar o que a "satisfatibilidade módulo teorias" acrescenta ao SAT booleano puro.
• Definir um procedimento de decisão e explicar que garantias ele precisa oferecer para o fragmento de fórmulas que cobre.
• Descrever, no nível da intuição, como a arquitetura DPLL(T) combina busca booleana com raciocínio específico de teorias.
• Distinguir fragmentos aritméticos decidíveis daqueles em que não se pode contar que a automação termine ou tenha sucesso.
• Diagnosticar um bug ou uma precondição faltante diretamente a partir do modelo de contraexemplo de um solver SMT.

boolean-satisfiability-and-cook-levin-connection mostrou que o SAT consegue codificar computações limitadas, mas asserções reais de programas quase nunca são puramente booleanas: elas falam de inteiros sendo comparados, arrays sendo indexados, ponteiros sendo desreferenciados e bit-vectors dando a volta em larguras fixas. Codificar tudo isso fielmente até virar variáveis proposicionais e cláusulas puras é possível em princípio, pela mesma construção no estilo tableau que a prova de Cook-Levin usa, mas muitas vezes é desperdiçador e pode esconder justamente a estrutura aritmética que um solver poderia explorar de forma muito mais direta e eficiente.

Os solvers SMT fecham essa lacuna acrescentando raciocínio específico de teorias diretamente por cima da busca booleana no estilo SAT, de modo que uma condição de verificação como "se 0 ≤ i e i < n, então este acesso ao array é seguro" possa ser entregue a um solver praticamente como está escrita, com raciocínio genuíno de aritmética e de arrays embutido, em vez de ser achatada manualmente em milhares de cláusulas booleanas puras antes. É o ponto em que a verificação automatizada começa a parecer genuinamente automática para uma grande variedade de obrigações realistas: muitas condições de verificação que seriam penosas de cumprir à mão só com as regras da lógica de Hoare viram, para um solver SMT, consultas de rotina respondidas em uma fração de segundo.

Essa automação vem com uma disciplina real e inevitável, porém, e este conceito trata tanto da fronteira do que o SMT consegue fazer quanto do que ele faz. Cada teoria de fundo que um solver suporta (aritmética linear, bit-vectors, arrays, funções não interpretadas) tem tanto fragmentos decidíveis, em que o solver tem garantia de terminar com uma resposta correta, quanto fragmentos mais ricos (muitas vezes envolvendo quantificadores ou aritmética não linear) em que essa garantia não existe. Cada uma dessas fronteiras é, no fim, mais uma instância local da mesma indecidibilidade a que esta disciplina voltou repetidamente desde testing-shows-presence-proof-shows-absence; o SMT não escapa dessa fronteira, ele só a empurra muito mais longe do que o SAT puro conseguiria sozinho.

Do SAT ao SMT

"SMT" significa satisfiability modulo theories (satisfatibilidade módulo teorias), e o nome descreve a arquitetura com precisão: a satisfatibilidade ainda é a pergunta central, mas agora módulo (em relação a, restringida por) uma teoria de fundo que dá significado a símbolos como +, <, indexação de arrays ou aritmética de bit-vectors, em vez de tratar cada átomo como uma variável booleana opaca, como o SAT puro faz. A estrutura booleana de uma fórmula (seus Es, OUs e implicações) ainda é tratada essencialmente pelo mesmo mecanismo de busca no estilo SAT já apresentado. O que é novo é que os átomos dentro dessa estrutura booleana não são mais letras proposicionais sem significado; são fatos específicos de teorias, como x + 1 < y ou a[i] = a[j], e solvers de teoria dedicados checam se uma combinação proposta desses fatos é consistente em conjunto segundo as regras reais da teoria, e não só segundo quais variáveis booleanas calharam de ser marcadas como verdadeiras ou falsas.

Procedimentos de decisão

Um procedimento de decisão, para alguma classe específica e bem definida de fórmulas, é um algoritmo com garantia de sempre terminar e sempre devolver a resposta correta de sim ou não para toda fórmula dessa classe: sem timeouts, sem "desconhecido", sem risco de rodar para sempre. A aritmética linear inteira e a aritmética linear real (fórmulas construídas com adição, comparação e multiplicação só por constantes, sem multiplicar duas variáveis entre si) têm fragmentos decidíveis bem conhecidos, com procedimentos de decisão eficientes, e é exatamente por isso que tantas condições de verificação do dia a dia (checagens de limites de arrays, aritmética simples de contadores de laço) caem dentro do território confortavelmente automatizado do SMT. A aritmética não linear geral, em que duas variáveis podem ser multiplicadas livremente, e a aritmética combinada com quantificadores irrestritos ficam do outro lado dessa fronteira: alguns fragmentos ali continuam decidíveis, mas com comportamento de pior caso muito pior, e outros são francamente indecidíveis, o que significa que nenhum procedimento de decisão para eles pode existir, ecoando exatamente o tipo de resultado de impossibilidade que Computabilidade e Complexidade já estabeleceu para o caso geral.

A ideia do DPLL(T)

A arquitetura dominante por trás dos solvers SMT modernos, comumente chamada de DPLL(T) (estendendo o algoritmo clássico DPLL para SAT com um componente de teoria T), funciona como um laço de ida e volta apertado entre as duas camadas recém-descritas. O motor SAT propõe um arranjo booleano: uma escolha de quais átomos de teoria são verdadeiros e quais são falsos, consistente só com a estrutura booleana da fórmula, ignorando por ora o significado na teoria. O solver de teoria então checa se essa combinação específica de átomos de teoria poderia de fato ser verdadeira em conjunto segundo a semântica real da teoria; se puder, a proposta do motor SAT se mantém, e, se não puder, o solver de teoria devolve um conflito (uma combinação específica e mínima de átomos que não podem coexistir), com que o motor SAT então aprende e que usa para podar não só aquela proposta, mas toda outra proposta que compartilhe a mesma combinação impossível. Esse laço de realimentação apertado é o que permite ao solver evitar a estratégia astronomicamente desperdiçadora de primeiro codificar cada fato de teoria em cláusulas booleanas puras (como uma construção no estilo tableau de Cook-Levin tecnicamente poderia) e, em vez disso, raciocinar sobre fatos de teoria diretamente, no seu nível natural de abstração, reaproveitando ainda todo o mecanismo maduro e altamente otimizado que a resolução de SAT desenvolveu para a busca puramente booleana.

Condições de verificação

Na prática, a saída de um verificador de programas (gerada diretamente por obrigações de prova da lógica de Hoare ou pelo cálculo da precondição mais fraca visto antes nesta disciplina) é um lote de fórmulas chamadas condições de verificação: afirmações como "o invariante deste laço é preservado pelo corpo" ou "este acesso ao array sempre fica dentro dos limites". O solver SMT prova cada uma verdadeira pela mesma técnica já apresentada para o SAT puro: negar a condição de verificação e mostrar que a negação é insatisfatível, o que significa que não existe estado que violaria a propriedade pretendida. Quando a negação de uma condição de verificação se mostra satisfatível, o modelo devolvido não é um beco sem saída: é uma atribuição concreta de valores a cada variável relevante que testemunha a violação, e ler esse modelo muitas vezes é o jeito mais rápido de ver exatamente qual precondição faltava, qual invariante era fraco demais ou qual caso nunca foi de fato tratado; continuando diretamente o tema, levantado primeiro em testing-shows-presence-proof-shows-absence, de que um contraexemplo concreto carrega mais valor de diagnóstico que um veredicto abstrato de "indemonstrável".

Limites de array

Considere a obrigação de prova que precisa valer logo antes de ler a[i]: 0 ≤ i ∧ i < n. Suponha que o programa, neste ponto, só tenha de fato estabelecido o fato mais fraco i ≤ n, talvez a partir de um invariante de laço com uma comparação frouxa demais. Para checar se o acesso é com certeza seguro, um solver SMT checa a negação: existe um estado que satisfaz i ≤ n mas viola 0 ≤ i ∧ i < n? Tentando i = n diretamente: isso satisfaz i ≤ n (com igualdade) e viola o i < n exigido (já que i e n são iguais, e não estritamente menores). O solver devolve i = n como atribuição que satisfaz a obrigação negada; exatamente um modelo de contraexemplo, que identifica concretamente que o caso de borda i = n é onde o conhecimento existente fica aquém. A correção a que esse contraexemplo aponta diretamente: a guarda ou o invariante do programa precisa ser fortalecido, para que se saiba que i é estritamente menor que n, e não só no máximo n, antes de o acesso ser alcançado.

Overflow de bit-vector

Considere a afirmação x + 1 > x, que vale incondicionalmente nos inteiros matemáticos para todo valor de x. A adição de máquina em representações de largura fixa não tem essa propriedade: em inteiros sem sinal de 8 bits, os valores vão de 0 a 255, e somar 1 a 255 dá a volta para 0, já que não existe um 256º valor para representar a soma real. Em x = 255, a afirmação x + 1 > x vira 0 > 255, que é falsa. Um solver SMT com teoria de bit-vectors, configurado para raciocinar sobre representações de largura fixa em vez de inteiros matemáticos ilimitados, modela esse comportamento de wraparound exatamente e relata corretamente que a afirmação é inválida, devolvendo x = 255 como contraexemplo. Um solver SMT configurado com a teoria de inteiros ilimitados, ao contrário, relataria a afirmação como válida, por não ter modelado um detalhe do nível da máquina (o wraparound de largura fixa) que a teoria escolhida simplesmente não enxerga; isso não é um bug em nenhum dos solvers, mas uma ilustração nítida de por que escolher a teoria certa para modelar a semântica real de execução de um programa importa tanto quanto confiar na resposta do solver depois que uma teoria foi escolhida.

Funções não interpretadas

Considere um símbolo de função f usado de forma abstrata, sem se comprometer com nenhuma implementação específica; a teoria de funções não interpretadas com igualdade raciocina sobre esses símbolos usando só um axioma estrutural, a congruência funcional: se a = b, então f(a) = f(b), e nada mais é presumido sobre f além disso. Dado só o fato f(a) = f(b), não decorre que a = b: saber que f produz a mesma saída para duas entradas não diz nada sobre se as próprias entradas eram iguais, já que f poderia facilmente ser uma função muitos-para-um. Dado o fato inverso, a = b, a congruência autoriza concluir f(a) = f(b), de forma direta e mecânica. Esse raciocínio limitado, mas totalmente decidível, é genuinamente útil na verificação: ele permite a uma prova tratar alguma operação de forma abstrata (como uma função não especificada, só com as propriedades que a congruência garante) sem se comprometer prematuramente com uma implementação concreta dessa operação, exatamente o nível de abstração certo quando os detalhes internos da operação são irrelevantes para a propriedade sendo checada.

• Presumir que toda consulta SMT pertence automaticamente a um fragmento decidível e fácil. Acrescentar quantificadores livremente, ou multiplicar duas variáveis entre si em uma fórmula aritmética, pode empurrar uma consulta para fora dos fragmentos que um solver tem garantia de tratar; o solver ainda pode ter sucesso na prática em muitas dessas consultas, mas "normalmente funciona" é uma garantia muito diferente de "comprovadamente sempre termina com uma resposta correta", e confundir as duas exagera o que a ferramenta de fato estabeleceu.
• Usar uma teoria de inteiros matemáticos quando o programa de fato usa aritmética de máquina de largura fixa. O exemplo de overflow de bit-vector demonstra isso de forma concreta: uma prova totalmente correta em relação à semântica de uma teoria pode ser simplesmente falsa em relação ao comportamento real da máquina, e nenhum cuidado na própria prova compensa ter modelado a semântica subjacente errada desde o início.
• Ignorar o modelo concreto que um solver SMT devolve junto com um resultado satisfatível (ou seja, com contraexemplo encontrado). Esse modelo não é uma saída incidental: é o jeito mais direto de ver por que uma condição de verificação falhou, exatamente análogo aos rastros de contraexemplo que o model checking vai devolver mais adiante nesta disciplina, e passar por cima dele para só anotar "a checagem falhou" joga fora a maior parte do valor de diagnóstico que o solver de fato forneceu.
• Acreditar que "desconhecido" significa que a propriedade é falsa. Algumas consultas a solvers, especialmente as que caem fora de um fragmento decidível, legitimamente estouram o tempo ou devolvem "desconhecido" em vez de um sim ou não definido; esse resultado não carrega nenhuma informação sobre para que lado está a resposta verdadeira, e tratá-lo como equivalente a um contraexemplo definido (ou, igualmente errado, a uma prova definida) é uma leitura equivocada e direta do que o solver de fato relatou.

Os solvers SMT estendem o SAT booleano com raciocínio ciente de teorias sobre inteiros, arrays, bit-vectors e funções não interpretadas, normalmente pelo laço de realimentação apertado da arquitetura DPLL(T) entre a busca booleana e a checagem de consistência específica de cada teoria, e é isso que faz uma grande variedade de condições de verificação realistas de programas (segurança de limites de arrays, preservação de invariantes de laço) parecer genuinamente automática, de um jeito que o SAT puro, codificado à mão, raramente consegue. Essa automação é limitada por fronteiras reais de decidibilidade específicas de cada teoria, e o exemplo de overflow de bit-vector versus inteiro mostrou de forma concreta por que escolher a teoria que de fato corresponde à semântica de execução de um programa importa tanto quanto confiar no veredicto do solver depois que essa escolha foi feita. transition-systems-and-kripke-structures continua a seguir, deslocando a atenção de condições de verificação individuais para os modelos de estados finitos que o model checking percorre de forma exaustiva, uma técnica automatizada diferente, construída sobre uma base diferente e complementar à do SAT e do SMT.