Meta ha enviado más de 100,000 correcciones de bugs que fueron atrapadas por un analizador estático antes de que el código llegara a un usuario. La herramienta se llama Infer, es de código abierto y no ejecuta tu código. Lo lee, construye un modelo matemático de lo que el código podría hacer, y demuestra que ciertas cosas malas no pueden suceder. O encuentra un camino donde sí pueden.

La técnica es la interpretación abstracta. Suena académica porque lo es. Patrick Cousot y Radhia Cousot la inventaron en los años 70 como una forma de razonar sobre programas sin ejecutarlos. El equipo de Meta, liderado por Peter O’Hearn, tomó la teoría y la hizo lo suficientemente rápida para analizar millones de líneas de código móvil y de servidor en minutos. El resultado es una herramienta que encuentra desreferencias de puntero nulo, fugas de memoria, fugas de recursos y condiciones de carrera en tiempo de diff.

El problema: las pruebas dinámicas no pueden cubrir lo que no se te ocurrió ejecutar

Una unit test verifica un camino a través de tu código. Una integration test verifica unos pocos más. Pero una función con cinco condicionales y dos bucles tiene cientos de caminos, y la mayoría nunca se ejecutan en las suites de pruebas.

Las pruebas dinámicas, ejecutando el código, solo pueden encontrar bugs en los caminos que realmente ejecutas. El análisis estático encuentra bugs en caminos que nunca se te ocurrieron. Es la diferencia entre revisar tu casa en busca de intrusos caminando por las habitaciones con una linterna, y revisar demostrando que todas las puertas y ventanas están cerradas con llave.

El desafío es que demostrar cosas sobre programas reales es difícil. Los programas reales tienen bucles, recursión, asignación de heap y concurrencia. No puedes enumerar cada estado. La interpretación abstracta resuelve esto aproximando.

Qué significa realmente la interpretación abstracta

La interpretación abstracta funciona ejecutando tu programa sobre valores abstractos en lugar de concretos.

En una ejecución normal, una variable x podría contener el entero 42. En una interpretación abstracta, x podría contener el valor abstracto “positivo”. El análisis no sabe que x es 42. Sabe que x es mayor que cero. Eso es suficiente para demostrar que x / y no dividirá por cero si y también es positivo. No es suficiente para demostrar que x == 42. La interpretación abstracta intercambia precisión por computabilidad.

El conjunto de valores abstractos se llama dominio abstracto. El dominio más simple es el dominio de signos: cada variable es negativa, cero, positiva o desconocida. Dominios más complejos rastrean rangos, punteros o si una ubicación de memoria ha sido liberada. El análisis itera sobre el programa, aplicando versiones abstractas de cada operación, hasta que el estado abstracto deja de cambiar. En ese punto, ha encontrado un punto fijo, una aproximación de cada estado concreto posible en cada punto del programa.

Los bucles son la parte difícil. Un bucle podría ejecutarse cero veces, una vez o mil millones de veces. El analizador no puede desenrollarlo mil millones de veces. En su lugar, aplica un operador de ampliación que salta a una sobre-aproximación. Si una variable se incrementa en uno en cada iteración, el analizador podría ampliar su valor abstracto de “positivo” a “no negativo” y detenerse allí. Pierde el límite exacto, pero conserva la propiedad que importa para la demostración.

Cómo Infer usa la bi-abducción para analizar procedimientos de forma modular

La interpretación abstracta tradicional analiza todo un programa como un todo. Eso no escala para una app móvil con un millón de líneas de código. Infer resuelve esto con una técnica llamada bi-abducción.

La bi-abducción permite a Infer analizar una función a la vez. Cuando Infer analiza una función, descubre dos cosas: las precondiciones que deben cumplirse para que la función sea segura, y las postcondiciones que la función garantiza. Estas se infieren automáticamente, no las escribe el programador.

Aquí hay un ejemplo concreto. Supongamos que Infer ve esta función en C:

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

Infer infiere que greet requiere que p sea no nulo. Esa es la precondición. También infiere que greet no libera p ni modifica ningún estado visible. Esa es la postcondición. Cuando otra función llama a greet, Infer verifica al llamador contra la precondición inferida. Si el llamador podría pasar nulo, Infer reporta un bug.

El motor de bi-abducción funciona mediante ejecución simbólica sobre lógica de separación. La lógica de separación permite a Infer razonar sobre la propiedad del heap: qué función posee qué memoria, y si esa memoria ha sido liberada. Esto es lo que hace que Infer sea bueno encontrando desreferencias nulas y fugas de memoria en C, C++, Objective-C y Java.

Qué detecta Infer y qué se le escapa

Infer no es un linter de propósito general. Se enfoca en clases específicas de bugs que son costosas de encontrar dinámicamente y peligrosas en producción.

Desreferencias de puntero nulo. Infer rastrea si cada puntero es definitivamente nulo, definitivamente no nulo, o quizás nulo. Una desreferencia de un puntero quizás-nulo desencadena un reporte. En Java y Objective-C, esto atrapa el tipo de crash más común.

Fugas de memoria. Infer usa lógica de separación para rastrear la propiedad del heap. Si una función asigna memoria y no la libera ni la devuelve a un llamador, Infer reporta una fuga. Esto es particularmente valioso en codebases de C y C++ donde las fugas se acumulan durante semanas de uptime.

Fugas de recursos. Los descriptores de archivo, sockets y locks se rastrean de manera similar. Si una función abre un archivo y retorna sin cerrarlo en cada camino, Infer reporta la fuga.

Condiciones de carrera. El module RacerD de Infer analiza la concurrencia en Java. Rastrea qué hilos acceden a qué campos y si esos accesos están protegidos por locks. Dos hilos accediendo al mismo campo sin sincronización es una carrera.

Infer no atrapa todo. Se le escapan bugs que requieren razonar sobre precisión numérica, contenidos de cadenas o patrones de aliasing complejos. También es insound por diseño: puede omitir bugs para mantener los falsos positivos bajos. Un analizador estático que grita lobo en cada diff se desactiva. El despliegue interno de Meta mantuvo la tasa de falsos positivos de Infer por debajo del 10%, por lo que los desarrolladores realmente actúan sobre sus reportes.

Ejecutando Infer en tu propio código

Infer es de código abierto y soporta C, C++, Objective-C, Java y (experimentalmente) Rust y Swift. La forma más fácil de probarlo es en un proyecto de Java o C.

Instala Infer vía Homebrew o Docker:

# macOS
brew install infer

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

Para un proyecto de Java usando Maven:

infer run -- mvn compile

Para un proyecto de C usando Make:

infer run -- make

Infer compila tu código, construye un grafo de flujo de control y ejecuta el análisis. La salida es un conjunto de reportes de bugs con nombres de archivo, números de línea y la precondición inferida que fue violada.

Aquí hay un ejemplo mínimo en C que Infer marcará:

// 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;
}

Ejecutar infer run -- cc leak.c produce:

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

Infer también atrapa la desreferencia nula en este ejemplo:

// 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
}

Espera, en realidad Infer no reportará lo anterior. La función print_length maneja de forma segura un argumento nulo. Infer solo reporta cuando una desreferencia ocurre en un puntero posiblemente nulo sin una verificación. Aquí hay uno que sí se activará:

// 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
}

Infer rastrea el camino desde call_unsafe a través de unsafe_print y reporta que s es nulo cuando se evalúa s[0].

El trade-off: velocidad versus precisión

El diseño modular de Infer lo hace lo suficientemente rápido para ejecutarse en cada pull request en Meta. Pero la modularidad introduce aproximación. Cuando Infer analiza una función, no conoce el contexto de llamada exacto. Infiere precondiciones que son conservadoras, lo que significa que pueden ser más fuertes de lo necesario. Una precondición más fuerte significa menos bugs reportados en el sitio de llamada, pero también menos falsos positivos.

Esta es la tensión central en el análisis estático. Un analizador sound reporta cada bug, pero te ahoga en falsos positivos. Un analizador unsound como Infer mantiene a los desarrolladores contentos reportando solo bugs sobre los que está seguro. Los bugs que se le escapan son el costo de la adopción.

El motor de bi-abducción de Infer también tiene dificultades con el estado global y callbacks complejos. Si tu código de Java pasa una clase interna anónima a un executor, Infer puede perder la pista de qué hilo ejecuta qué método. RacerD maneja patrones comunes pero se pierde carreras sutiles que involucran variables de condición o campos atomics.

Cuándo adoptar análisis estático y cuándo omitirlo

Deberías considerar Infer si envías código nativo, apps móviles o código de servidor en lenguajes de la familia C o Java. Los bugs que encuentra — desreferencias nulas, fugas, carreras — son exactamente los que causan crashes en producción y vulnerabilidades de seguridad.

No deberías esperar que Infer reemplace tu suite de pruebas. El análisis estático y las pruebas dinámicas son complementarios. Las pruebas verifican que tu código hace lo que pretendes con los inputs que elegiste. El análisis estático verifica que tu código no hace lo que prohíbes con cualquier input.

Si tu codebase está en Python, Ruby o JavaScript, Infer no es la herramienta adecuada. Estos lenguajes carecen de la información de tipos estáticos que Infer usa para construir su modelo abstracto. Para lenguajes dinámicos, los type checkers como mypy o pyright atrapan una clase diferente de errores.

La conclusión

Las 100,000 correcciones de bugs de Meta no son un número de marketing. Son la salida de una herramienta que se ejecuta en cada diff, analiza código sin ejecutarlo y reporta bugs que ninguna prueba habría atrapado. La técnica subyacente, la interpretación abstracta, tiene décadas de antigüedad. El logro de ingeniería es hacerla lo suficientemente rápida y precisa como para que los desarrolladores no la desactiven.

No necesitas la infraestructura de Meta para beneficiarte. Instala Infer, apúntalo a tu sistema de build y ejecútalo en un module que te asuste. El module de gestión de memoria, la capa de concurrencia, el límite de interoperabilidad con C. Arregla las fugas y desreferencias nulas que encuentra. Luego agrégalo a CI y evita que el conteo de bugs crezca.

La interpretación abstracta no es magia. Es matemáticas aplicadas al código, con todas las aproximaciones y trade-offs que eso conlleva. Pero es matemática que encuentra bugs reales en codebases reales, y eso la hace digna de conocer.