A investigação por trás do Visao: como o Equid se tornou o nosso analisador estático
Antes de ser um produto, o Visao foi um projeto de investigação chamado Equid. Era uma framework de análise estática independente da linguagem, criada para aproximar os verificadores académicos do código industrial real. Apresentamos o artigo por trás do nosso analisador e as ideias que passaram para o produto atual.
Hoje, o Visao é o nosso motor de análise estática. Lê o código-fonte e segue os defeitos até à causa de fundo, para lá dos padrões conhecidos. Escala para grandes bases de código em várias linguagens, em ambientes de alta fiabilidade. Mas não começou como produto. Começou como um projeto de investigação chamado Equid.
O Equid era uma framework de análise estática criada pelo nosso fundador, Maxim Menshikov, e apresentada na conferência ICCSA 2019 (Springer LNCS, vol. 11619). O nome vem, de forma livre, de "Engine for performing queries on unified intermediate representations of program and domain models", ou seja, um motor de consultas sobre representações intermédias unificadas de modelos de programa e de domínio. Este artigo conta a história dessa investigação: o que pretendia fazer, como funcionava e que ideias continuam hoje dentro do Visao.
O problema: teoria que não chega ao produto
A análise estática está dividida em dois mundos. De um lado estão as ferramentas académicas, com um conjunto exaustivo de funcionalidades (model checking, interpretação abstrata, resolução SMT). Raramente sobrevivem ao contacto com uma base de código real de 500 000 linhas. Do outro lado estão os verificadores industriais. Instalam-se em minutos, mas tratam o programa como uma caixa negra e falham a maior parte do que importa.
Em software de grande dimensão, sobretudo quando depende de hardware especializado, os bugs podem esconder-se em qualquer camada. Podem estar no núcleo do sistema operativo, na shell, na configuração de rede, no espaço do utilizador ou até no hardware. Os detetores universais incluídos de origem raramente chegam. E se a análise não se integra no fluxo de desenvolvimento real, os engenheiros deixam simplesmente de a usar. Esse abandono é a principal razão por que as ferramentas de verificação falham na prática.
O Equid partiu de pressupostos diferentes dos da maioria das ferramentas académicas. Esses pressupostos vinham do código industrial tal como ele é de facto:
O código maduro já está quase todo depurado
A corrupção de memória é rara em código já lançado. Por isso, explorar todo o espaço de estados é muitas vezes esforço perdido. Deve ficar reservado para os poucos componentes críticos que precisam mesmo dele.
A ferramenta ajuda, não substitui
Não é possível provar todos os algoritmos de forma automática. O programador ajuda a ferramenta, e os contratos passam a ser uma extensão natural da documentação, que a máquina consegue verificar.
Os contratos apanham a maioria dos bugs reais
Os contratos de funções e de acesso à memória chegam, em geral, para revelar a maioria dos defeitos observáveis. E não é preciso um doutoramento em métodos formais para os usar.
Tem de encaixar no fluxo de trabalho
A "análise noturna" em lote, a distribuição previsível da carga e a invocação simples são funcionalidades pensadas desde o início. Um analisador difícil de usar é um analisador que ninguém usa.
O pipeline, do início ao fim
O Equid processa o código por etapas, e todo o desenho é independente da linguagem. A análise é a mesma, seja qual for a linguagem de origem, e acrescentar uma linguagem custa pouco. O modelo interno era geral o bastante para se alargar a linguagens orientadas a objetos. É a mesma ambição multilinguagem que hoje define o Visao.
1. Código-fonte → árvore sintática generalizada (GST)
Em vez de se prender a uma framework de compilador, o Equid trata o Clang como um parser possível entre outros. O resultado do parser passa a uma árvore sintática generalizada (Generalized Syntax Tree). É uma representação unificada que elimina o açúcar sintático e junta as árvores sintáticas abstratas de várias linguagens numa só forma. A GST também extrai relações persistentes entre instruções e agrupa-as em Fragments (fragmentos). Isto torna quase trivial a análise de concorrência do tipo lock-set.
2. GST → códigos da máquina virtual
Uma árvore é pouco prática para a análise sensível ao fluxo. Por isso, o Equid converte-a numa representação intermédia (IR) própria: um conjunto compacto de instruções (declare, assign, branch, check, constraint, invoke). Ao contrário do LLVM IR e de outros códigos moldados pelo hardware, esta IR pode transportar variáveis globais próprias do analisador e tipos personalizados, sem variáveis fantasma nem soluções forçadas. Descreve o que uma expressão significa para o analisador, e não como um CPU a executaria.
3. Um Hypervisor controla as máquinas virtuais
No topo está um Hypervisor, que gere as máquinas virtuais (VM). As VM "executam" os códigos para dar sensibilidade ao fluxo e ao contexto. O programa em si não corre. Na análise sensível ao fluxo, o Hypervisor insere em linha resumos de funções construídos com interpolação de Craig. Na análise sensível ao contexto, desenrola o corpo das funções com blocos de entrada e saída. As VM tratam do fluxo de controlo. Todo o raciocínio real fica a cargo do solucionador.
4. O Multi Solver faz o raciocínio
Esta é a parte central do Equid. É também a razão por que o Visao segue os defeitos até à causa raiz, em vez de comparar padrões superficiais. O Multi Solver combina dois motores muito diferentes, que se reforçam um ao outro:
Solucionador SMT (CVC4)
Converte funções inteiras em cláusulas de asserção e verifica a negação do objetivo para detetar violações de contratos. O CVC4 foi escolhido pela estabilidade, pela interface nativa em C++ e pelo amplo suporte de teorias.
Interpretador abstrato
Produz uma sobre-aproximação com domínios abstratos (intervalos, poliedros). Esta reduz o espaço de estados do SMT, melhora a precisão e pode apanhar erros sozinha, quase sem impacto no tempo de análise.
O Multi Solver escolhe a interpretação mais conveniente para cada caso: raciocínio exato quando o espaço de estados é pequeno, sobre-aproximação quando um ciclo pode não ter limite. Um sistema de tipos preciso e ajustável trata o endianness, as larguras de inteiros ambíguas e as conversões baratas e caras. Assim, o modelo de memória mantém-se fiel em diferentes CPU e compiladores.
5. Semantic Storage na base de tudo
Todos os artefactos (recursos, fragmentos, expressões, códigos da VM) ficam num Semantic Storage (armazenamento semântico) assente em MongoDB. Cada um tem um ID estável e metadados chave-valor. Em projetos que cabem na RAM, a base de dados é opcional. Em projetos grandes, permite uma pilha tecnológica distribuída, carregar e descarregar recursos de forma dinâmica e ocupar muito menos memória. Nenhum outro analisador da comparação usava um armazenamento semântico separado como este. É uma parte importante da forma como o Visao trata hoje grandes bases de código.
Contratos e detetores
O Equid encontra bugs de duas formas complementares. Os contratos são escritos em ACSL, o mesmo formato de anotações do Frama-C. São convertidos diretamente em comandos da VM, o que dá uma primeira passagem muito rápida pelas funções do utilizador e da biblioteca padrão. Os detetores são, no essencial, fórmulas de lógica temporal (LTL) sobre o fluxo. Há alguns tipos:
- Visitantes da GST: verificações estruturais, como operandos duplicados.
- Manipuladores de marcação: seguem estados como "alocado" ou "handle aberto". Um detetor de fugas só verifica que tudo o que não é devolvido é libertado antes do return.
- Observadores de sequências: assinalam padrões errados, por exemplo
fclose(x)seguido deread(x).
A biblioteca padrão é anotada uma vez e pré-carregada no arranque. Um protótipo que recompilava as anotações para C carregava-as cerca de seis vezes mais depressa, porque saltava por completo o parser.
Encontra mesmo bugs?
Num subconjunto suportado dos benchmarks Toyota ITC, o Equid detetou cerca de 90% dos bugs nas categorias suportadas. Ficou, em geral, ao nível do Frama-C e claramente à frente do Clang e do cppcheck. Chegou a liderar em categorias como datalost e dataoverflow.
| Benchmark | Equid | Frama-C | Clang | cppcheck | Total |
|---|---|---|---|---|---|
| bitshift | 17 | 17 | 14 | 11 | 17 |
| bufferoverrun dyn. | 30 | 32 | 1 | 2 | 32 |
| bufferunderrun dyn. | 35 | 39 | 2 | 3 | 39 |
| datalost | 19 | 3 | — | — | 19 |
| dataoverflow | 25 | 16 | — | 9 | 25 |
| dataunderflow | 12 | 8 | — | 5 | 12 |
| littlemem_st | 11 | 11 | — | — | 11 |
| nullpointer | 15 | 16 | 13 | 12 | 17 |
| overrun_st | 47 | 54 | 2 | 21 | 54 |
| ptrsubtraction | 2 | 1 | — | — | 2 |
| underrun_st | 13 | 13 | 2 | 5 | 13 |
| uninitpointer | 10 | 16 | 11 | 5 | 16 |
| zerodivision | 16 | 16 | 13 | 8 | 16 |
Deteções no subconjunto wDefects dos benchmarks Toyota ITC. Clang 3.9, Frama-C Silicon, cppcheck 1.76. "—" significa que não houve deteções nessa categoria.
Para lá dos benchmarks: código real
Os benchmarks sintéticos só contam parte da história. O Equid também analisou uma aplicação de gestão de sistema operativo com 500 KLOC (500 mil linhas de código). Para isso, foram precisos modelos ACSL específicos do domínio e uma análise declarativa de ponteiros para lidar com chamadas indiretas. Esta análise usa aliases de funções como /feature/x/enable em vez de nomes internos obscuros. Depois de configurado, o Equid encontrou violações de contratos e fraquezas reais que nenhum outro analisador tinha detetado. Entre elas estavam membros de estruturas não inicializados, escondidos em código pouco conhecido de módulos.
Noutra experiência, usámos a capacidade de consulta do Equid num driver de kernel Linux de terceiros, com mais de 500 000 linhas. O Equid encontrou as causas de erros reais que as ferramentas de pesquisa automática não tinham detetado nesse código mal estruturado. A modelação deu trabalho, mas o resultado foram defeitos que nenhuma outra ferramenta alcançava.
Do Equid ao Visao
Um artigo científico mostra um momento no tempo. O artigo do Equid foi honesto sobre os limites da altura: as unions tinham suporte parcial, a cobertura interprocedimental estava incompleta e a linguagem de consulta ainda estava a amadurecer. Mas as apostas de arquitetura que fez foram precisamente as que vieram a contar. Passaram diretamente para o produto que hoje construímos:
Investigação Equid
Árvore sintática generalizada
→ No Visao: um só motor de análise para C, C++ e outras linguagens, em vez de uma ferramenta por linguagem.
Investigação Equid
Multi Solver (SMT + interpretação abstrata)
→ No Visao: seguir um defeito até à causa de fundo, para lá da comparação com padrões de bugs conhecidos.
Investigação Equid
Semantic Storage
→ No Visao: análise que escala para grandes bases de código sem esgotar a memória.
Investigação Equid
Contratos como documentação
→ No Visao: um caminho rápido e prático para os programadores chegarem a defeitos reais em código de alta fiabilidade.
A lição que começou com o Equid continua válida: uma boa verificação exige rigor e facilidade de uso ao mesmo tempo. Isso significa um analisador configurável, independente da linguagem e preciso, que encaixa na forma como a indústria trabalha de facto. Foi essa a ideia que transformámos no produto Visao.
Referência: M. Menshikov, "Equid - A Static Analysis Framework for Industrial Applications", em Computational Science and Its Applications (ICCSA 2019), Springer LNCS, vol. 11619, pp. 677-692. doi.org/10.1007/978-3-030-24289-3_50