A Meta enviou mais de 100.000 correções de bugs que foram capturadas por um analyzer estático antes que o código chegasse a um usuário. A ferramenta se chama Infer, é open source e não executa seu código. Ela o lê, constrói um modelo matemático do que o código poderia fazer, e prova que certas coisas ruins não podem acontecer. Ou ela encontra um caminho onde podem.

A técnica é a interpretação abstrata. Soa acadêmica porque é. Patrick Cousot e Radhia Cousot a inventaram nos anos 1970 como uma forma de raciocinar sobre programas sem executá-los. A equipe da Meta, liderada por Peter O’Hearn, pegou a teoria e a tornou rápida o suficiente para analisar milhões de linhas de código mobile e de servidor em minutos. O resultado é uma ferramenta que encontra desreferências de ponteiro nulo, vazamentos de memória, vazamentos de recursos e race conditions no momento do diff.

O problema: testes dinâmicos não podem cobrir o que você não pensou em executar

Um teste unitário verifica um caminho através do seu código. Um integration test verifica mais alguns. Mas uma função com cinco condicionais e dois loops tem centenas de caminhos, e a maioria deles nunca é exercitada em suites de teste.

Testes dinâmicos, executando o código, só podem encontrar bugs em caminhos que você realmente executa. Análise estática encontra bugs em caminhos que você nunca pensou. É a diferença entre verificar sua casa para invasores caminhando pelos cômodos com uma lanterna, e verificar provando que todas as portas e janelas estão trancadas.

O desafio é que provar coisas sobre programas reais é difícil. Programas reais têm loops, recursão, alocação de heap e concorrência. Você não pode enumerar cada estado. A interpretação abstrata resolve isso aproximando.

O que a interpretação abstrata realmente significa

A interpretação abstrata funciona executando seu programa em valores abstratos em vez de valores concretos.

Em uma execução normal, uma variável x pode conter o inteiro 42. Em uma interpretação abstrata, x pode conter o valor abstrato “positivo”. A análise não sabe que x é 42. Ela sabe que x é maior que zero. Isso é suficiente para provar que x / y não dividirá por zero se y também for positivo. Não é suficiente para provar que x == 42. A interpretação abstrata troca precisão por computabilidade.

O conjunto de valores abstratos é chamado de domínio abstrato. O domínio mais simples é o domínio de sinais: cada variável é negativa, zero, positiva ou desconhecida. Domínios mais complexos rastreiam intervalos, ponteiros ou se um local de memória foi liberado. A análise itera sobre o programa, aplicando versões abstratas de cada operação, até que o estado abstrato pare de mudar. Nesse ponto, ela encontrou um ponto fixo, uma aproximação de cada estado concreto possível em cada ponto do programa.

Loops são a parte difícil. Um loop pode executar zero vezes, uma vez, ou um bilhão de vezes. O analyzer não pode desenrolá-lo um bilhão de vezes. Em vez disso, ele aplica um operador de widening que salta para uma superaproximação. Se uma variável incrementa em um a cada iteração, o analyzer pode ampliar seu valor abstrato de “positivo” para “não negativo” e parar ali. Ele perde o limite exato, mas mantém a propriedade que importa para a prova.

Como o Infer usa bi-abdução para analisar procedimentos de forma modular

A interpretação abstrata tradicional analisa um programa inteiro como um todo. Isso não escala para um aplicativo mobile com um milhão de linhas de código. O Infer resolve isso com uma técnica chamada bi-abdução.

A bi-abdução permite que o Infer analise uma função de cada vez. Quando o Infer analisa uma função, ele descobre duas coisas: as precondições que devem valer para que a função seja segura, e as pós-condições que a função garante. Essas são inferidas automaticamente, não escritas pelo programador.

Aqui está um exemplo concreto. Suponha que o Infer veja esta função em C:

void greet(struct Person* p) {
    printf("Hello, %s\n", p->name);
}

O Infer infere que greet requer que p seja não nulo. Essa é a precondição. Ele também infere que greet não libera p nem modifica nenhum estado visível. Essa é a pós-condição. Quando outra função chama greet, o Infer verifica o chamador contra a precondição inferida. Se o chamador puder passar nulo, o Infer reporta um bug.

O motor de bi-abdução funciona por execução simbólica sobre lógica de separação. A lógica de separação permite que o Infer raciocine sobre a propriedade do heap: qual função possui qual memória, e se essa memória foi liberada. É isso que torna o Infer bom em encontrar desreferências nulas e vazamentos de memória em C, C++, Objective-C e Java.

O que o Infer captura e o que deixa passar

O Infer não é um linter de propósito geral. Ele visa classes específicas de bugs que são caras de encontrar dinamicamente e perigosas em produção.

Desreferências de ponteiro nulo. O Infer rastreia se cada ponteiro é definitivamente nulo, definitivamente não nulo, ou talvez nulo. Uma desreferência de um ponteiro talvez-nulo dispara um relatório. Em Java e Objective-C, isso captura o tipo de crash mais comum.

Vazamentos de memória. O Infer usa lógica de separação para rastrear a propriedade do heap. Se uma função aloca memória e não a libera ou não a retorna para um chamador, o Infer reporta um vazamento. Isso é particularmente valioso em codebases C e C++ onde vazamentos se acumulam ao longo de semanas de uptime.

Vazamentos de recursos. Descritores de arquivo, sockets e locks são rastreados de forma semelhante. Se uma função abre um arquivo e retorna sem fechá-lo em cada caminho, o Infer reporta o vazamento.

race conditions. O module RacerD do Infer analisa a concorrência em Java. Ele rastreia quais threads acessam quais campos e se esses acessos são protegidos por locks. Duas threads acessando o mesmo campo sem sincronização é uma corrida.

O Infer não captura tudo. Ele deixa passar bugs que exigem raciocínio sobre precisão numérica, conteúdo de strings ou padrões de aliasing complexos. Ele também é unsound por design: ele pode deixar passar bugs para manter os falsos positivos baixos. Um analyzer estático que chora lobo a cada diff é desativado. A deployment interna da Meta manteve a taxa de falsos positivos do Infer abaixo de 10%, e é por isso que os desenvolvedores realmente agem sobre seus relatórios.

Executando o Infer em seu próprio código

O Infer é open source e suporta C, C++, Objective-C, Java e (experimentalmente) Rust e Swift. A maneira mais fácil de experimentá-lo é em um projeto Java ou C.

Instale o Infer via Homebrew ou Docker:

# macOS
brew install infer

# Or via Docker
docker run --rm -v $(pwd):/repo infer/infer infer run -- make -C /repo

Para um projeto Java usando Maven:

infer run -- mvn compile

Para um projeto C usando Make:

infer run -- make

O Infer compila seu código, constrói um grafo de fluxo de controle e executa a análise. A saída é um conjunto de relatórios de bugs com nomes de arquivo, números de linha e a precondição inferida que foi violada.

Aqui está um exemplo mínimo em C que o Infer sinalizará:

// leak.c
#include <stdlib.h>

int* allocate_but_leak(void) {
    int* p = malloc(sizeof(int));
    *p = 42;
    // forgot to return p or free it
    return NULL;
}

Executar infer run -- cc leak.c produz:

leak.c:5: error: MEMORY_LEAK
  memory dynamically allocated by call to `malloc()` at line 5 is not reachable after line 7

O Infer também captura a desreferência nula neste exemplo:

// null.c
#include <stdio.h>

void print_length(const char* s) {
    if (s != NULL) {
        printf("%zu\n", strlen(s));
    }
}

void unsafe_call(void) {
    print_length(NULL);  // Infer reports this
}

Espere, na verdade o Infer não reportará o acima. A função print_length lida com segurança com um argumento nulo. O Infer só reporta quando uma desreferência ocorre em um ponteiro possivelmente nulo sem uma verificação. Aqui está um que disparará:

// null_bad.c
#include <stdio.h>

void unsafe_print(const char* s) {
    // No null check before dereference
    printf("first char: %c\n", s[0]);
}

void call_unsafe(void) {
    unsafe_print(NULL);  // Infer reports this
}

O Infer rastreia o caminho de call_unsafe através de unsafe_print e reporta que s é nulo quando s[0] é avaliado.

O trade-off: velocidade versus precisão

O design modular do Infer o torna rápido o suficiente para ser executado em cada pull request na Meta. Mas a modularidade introduz aproximação. Quando o Infer analisa uma função, ele não conhece o contexto de chamada exato. Ele infere precondições que são conservadoras, o que significa que podem ser mais fortes do que o necessário. Uma precondição mais forte significa menos bugs reportados no site de chamada, mas também menos falsos positivos.

Essa é a tensão central na análise estática. Um analyzer sound reporta todos os bugs, mas o afoga em falsos positivos. Um analyzer unsound como o Infer mantém os desenvolvedores felizes reportando apenas bugs sobre os quais ele tem certeza. Os bugs que ele deixa passar são o custo da adoção.

O motor de bi-abdução do Infer também tem dificuldades com estado global e callbacks complexos. Se seu código Java passa uma classe interna anônima para um executor, o Infer pode perder a pista de qual thread executa qual método. O RacerD lida com padrões comuns mas perde corridas sutis envolvendo variáveis de condição ou campos atômicos.

Quando adotar análise estática e quando ignorá-la

Você deve considerar o Infer se envia código nativo, apps mobile ou código de servidor em linguagens da família C ou Java. Os bugs que ele encontra — desreferências nulas, vazamentos, corridas — são exatamente os que causam crashes em produção e vulnerabilidades de segurança.

Você não deve esperar que o Infer substitua sua test suite. Análise estática e testes dinâmicos são complementares. Testes verificam que seu código faz o que você pretende com os inputs que escolheu. Análise estática verifica que seu código não faz o que você proíbe com qualquer input.

Se sua codebase está em Python, Ruby ou JavaScript, o Infer não é a ferramenta certa. Essas linguagens carecem da informação de tipos estáticos que o Infer usa para construir seu modelo abstrato. Para linguagens dinâmicas, type checkers como mypy ou pyright capturam uma classe diferente de erros.

A conclusão

As 100.000 correções de bugs da Meta não são um número de marketing. São a saída de uma ferramenta que roda a cada diff, analisa código sem executá-lo e reporta bugs que nenhum teste teria capturado. A técnica subjacente, a interpretação abstrata, tem décadas de existência. A conquista de engenharia é torná-la rápida e precisa o suficiente para que os desenvolvedores não a desativem.

Você não precisa da infraestrutura da Meta para se beneficiar. Instale o Infer, aponte-o para seu sistema de build e execute-o em um module que o assusta. O module de gerenciamento de memória, a camada de concorrência, a fronteira de interop com C. Corrija os vazamentos e desreferências nulas que ele encontra. Depois adicione-o ao CI e impeça que a contagem de bugs cresça.

A interpretação abstrata não é mágica. É matemática aplicada ao código, com todas as aproximações e trade-offs que isso implica. Mas é matemática que encontra bugs reais em codebases reais, e isso a torna digna de ser conhecida.