Análisis e inferencia de tipos

Operativo · Actualizado el 16 de agosto de 2026

El lenguaje TIP no tiene declaraciones de tipo explícitas, pero por supuesto las operaciones están pensadas para aplicarse sólo a ciertas clases de valores. Un binario tampoco las tiene, y por la misma razón. Este capítulo presenta la inferencia de tipos como sistema de restricciones resuelto por unificación, y después explica por qué esa técnica, tal cual, no basta para un binario, y qué se usa en su lugar.

19.1 Tipabilidad como aproximación

Para TIP parecen razonables las siguientes restricciones:

las operaciones aritméticas y las comparaciones se aplican sólo a enteros;
las condiciones de las estructuras de control deben ser enteros;
sólo enteros pueden ser entrada y salida de main;
sólo se pueden llamar funciones, y con el número correcto de argumentos;
el operador unario * sólo se aplica a punteros, o a null;
los accesos a campo se hacen sólo sobre registros;
y los campos accedidos están garantizadamente presentes.

Su violación produce errores en tiempo de ejecución, así que querríamos saber que se cumplen. Como es una cuestión no trivial, sabemos de inmediato que es indecidible.

Recurrimos por tanto a una aproximación conservadora: la tipabilidad (typability). Un programa es tipable si satisface una colección de restricciones de tipo derivadas sistemáticamente, típicamente a partir del AST. Las restricciones se construyen de modo que garanticen el cumplimiento de los requisitos anteriores, pero no al revés: el análisis rechazará algunos programas que de hecho nunca violarían nada.

El análisis que sigue es una variante de la técnica de Damas–Hindley–Milner, que constituye la base de los sistemas de tipos de ML, OCaml y Haskell, presentada aquí en el estilo basado en restricciones de Wand.

19.2 El lenguaje de tipos

Type -> int
      | ^Type                         (puntero a Type)
      | (Type, ..., Type) -> Type     (funcion)

Cada clase de término se caracteriza por un constructor de términos con una aridad: ^ tiene aridad 1; el constructor de función tiene aridad igual al número de parámetros más uno, por el tipo de retorno.

La gramática generaría tipos finitos, pero para funciones y estructuras de datos recursivas hacen falta tipos regulares, definidos como árboles regulares sobre los constructores anteriores. Un árbol posiblemente infinito es regular si contiene sólo finitos subárboles distintos.

Por ejemplo, la función foo(p,x) del capítulo «3», cuyo segundo parámetro puede referirse a la propia foo, necesita un tipo infinito:

(^int, (^int, (^int, (^int, ...) -> int) -> int) -> int) -> int

Para expresarlos de forma finita se añaden el operador μ y las variables de tipo:

Type    -> ... | mu TypeVar . Type | TypeVar
TypeVar -> t | u | ...

Un tipo μα.τ se considera idéntico a τ[μα.τ / α]. Con esa notación, el tipo de foo se escribe

μt.(^int, t) → int

Se permiten variables de tipo libres, implícitamente cuantificadas universalmente: representan cualquier tipo. Considérese

store(a,b) {
    *b = a;
    return 0;
}

que tiene tipo (t, ^t) → int con t libre, lo que corresponde al comportamiento polimórfico de la función. Nótese que tales variables no están necesariamente libres de restricción: el tipo de a puede ser cualquiera, pero debe casar con el de aquello a lo que apunta b. El tipo más restringido (int, ^int) → int también es válido, pero normalmente interesa la solución más general.

19.3 Restricciones de tipo

Para cada variable local, parámetro y nombre de función X se introduce una variable de tipo ⟦X⟧, y para cada ocurrencia de una expresión no identificador E una variable ⟦E⟧. Las restricciones se definen sistemáticamente:

Construcción	Restricción
`I` (literal entero)	`⟦I⟧ = int`
`E₁ op E₂`	`⟦E₁⟧ = ⟦E₂⟧ = ⟦E₁ op E₂⟧ = int`
`E₁ == E₂`	`⟦E₁⟧ = ⟦E₂⟧ ∧ ⟦E₁==E₂⟧ = int`
`input`	`⟦input⟧ = int`
`X = E`	`⟦X⟧ = ⟦E⟧`
`output E`	`⟦E⟧ = int`
`if (E) S`	`⟦E⟧ = int`
`while (E) S`	`⟦E⟧ = int`
`X(X₁,…,Xₙ){…return E;}`	`⟦X⟧ = (⟦X₁⟧,…,⟦Xₙ⟧)→⟦E⟧`
`E(E₁,…,Eₙ)`	`⟦E⟧ = (⟦E₁⟧,…,⟦Eₙ⟧)→⟦E(E₁,…,Eₙ)⟧`
`alloc E`	`⟦alloc E⟧ = ^⟦E⟧`
`&X`	`⟦&X⟧ = ^⟦X⟧`
`null`	`⟦null⟧ = ^α`, con `α` fresca
`*E`	`⟦E⟧ = ^⟦*E⟧`
`*E₁ = E₂`	`⟦E₁⟧ = ^⟦E₂⟧`

Para un programa completo se añade que los parámetros y el retorno de main sean int.

Para el programa

short() {
    var x, y, z;
    x = input;
    y = alloc x;
    *y = x;
    z = *y;
    return z;
}

se obtienen las restricciones ⟦short⟧ = ()→⟦z⟧, ⟦input⟧ = int, ⟦x⟧ = ⟦input⟧, ⟦alloc x⟧ = ^⟦x⟧, ⟦y⟧ = ⟦alloc x⟧, ⟦y⟧ = ^⟦x⟧, ⟦z⟧ = ⟦*y⟧ y ⟦y⟧ = ^⟦*y⟧, cuya solución es ⟦short⟧ = ()→int, ⟦x⟧ = int, ⟦y⟧ = ^int, ⟦z⟧ = int.

Todos los constructores satisfacen además el axioma general de igualdad de términos:

c(τ₁,…,τₙ) = c'(τ'₁,…,τ'ₙ) ⟹ τᵢ = τ'ᵢ para cada i

junto con reflexividad, simetría y transitividad. En el ejemplo, de ⟦y⟧ = ^⟦x⟧ y ⟦y⟧ = ^⟦*y⟧ se sigue ⟦x⟧ = ⟦*y⟧.

Una solución asigna un tipo a cada variable de tipo de forma que todas las igualdades se satisfagan. La afirmación de corrección del análisis es que la existencia de una solución implica que los errores de ejecución especificados no pueden ocurrir.

19.4 Unificación con union-find

Si hay soluciones, se calculan en tiempo casi lineal con un algoritmo de unificación para términos regulares. Como las restricciones también se extraen en tiempo lineal, el análisis entero es muy eficiente.

El algoritmo se basa en la estructura union-find o de conjuntos disjuntos, de 1964, que representa y manipula relaciones de equivalencia mediante un grafo dirigido de nodos con exactamente una arista al padre —que puede ser el propio nodo, en cuyo caso es raíz—. Dos nodos son equivalentes si tienen un ancestro común, y cada raíz es el representante canónico de su clase.

procedure MakeSet(x)
    x.parent := x

procedure Find(x)
    if x.parent != x then
        x.parent := Find(x.parent)     // compresion de caminos
    return x.parent

procedure Union(x, y)
    xr := Find(x) ;  yr := Find(y)
    if xr != yr then xr.parent := yr

Se asocia un nodo a cada término del sistema, incluidos los subtérminos, y para cada restricción τ₁ = τ₂ se invoca:

procedure Unify(t1, t2)
    r1 := Find(t1) ;  r2 := Find(t2)
    if r1 != r2 then
        if r1 y r2 son ambas variables de tipo then
            Union(r1, r2)
        else if r1 es variable de tipo y r2 es tipo propio then
            Union(r1, r2)
        else if r1 es tipo propio y r2 es variable de tipo then
            Union(r2, r1)
        else if r1 y r2 son tipos propios con el MISMO constructor then
            Union(r1, r2)
            for cada par de subterminos t1', t2' de r1 y r2 do
                Unify(t1', t2')
        else
            FALLO DE UNIFICACION

La unificación falla al intentar unificar dos términos con constructores distintos —dos tipos función con aridades distintas cuentan como constructores distintos—.

Dos detalles de implementación que importan. Union(x,y) es asimétrica: siempre elige como representante canónico el de su segundo argumento. Y Unify está construida de modo que el segundo argumento de Union sólo puede ser una variable de tipo si el primero también lo es. Con ello, los tipos propios tienen precedencia sobre las variables para ser representantes canónicos, y basta consultar el representante en lugar de toda la clase.

Leer la solución es entonces fácil: para cada variable o expresión, se invoca Find y se resuelve recursivamente cada subtérmino. La única complicación surge si la recursión lleva a un tipo infinito, en cuyo caso se introduce un término μ.

El solucionador procesa cada restricción una sola vez, así que aunque conceptualmente se generen primero y se resuelvan después, en una implementación conviene entrelazar ambas fases.

Aplicado al programa factorial complicado del capítulo «3», con foo(p,x) y main(), la solución asigna int a casi todo salvo:

[[p]]       = ^int
[[q]]       = ^int
[[alloc 0]] = ^int
[[&n]]      = ^int
[[x]]       = mu t. (^int, t) -> int
[[foo]]     = mu t. (^int, t) -> int
[[main]]    = () -> int

Los tipos recursivos son necesarios para foo y para el parámetro x. Como existe solución, el programa es correcto en tipos.

19.5 Registros y limitaciones

Para registros se amplía el lenguaje de tipos con un constructor de registro que lleva un campo por cada nombre de campo del programa, usando un tipo especial de «campo ausente». La consecuencia es que dos registros con conjuntos de campos distintos no unifican, lo que hace el análisis más rígido de lo deseable; los sistemas reales usan tipos de fila (row types) o subtipado.

Y ésa es precisamente la limitación central de este enfoque:

La unificación es simétrica. ⟦X⟧ = ⟦E⟧ obliga a que ambos tipos sean idénticos, no a que uno sea compatible con el otro. No hay forma de expresar «int puede usarse donde se espera long» ni «Derivada* puede usarse donde se espera Base*».
No hay subtipado. Todo el poder expresivo está en la igualdad de términos.
Un solo fallo lo tira todo. Si una sola restricción es insatisfacible, el programa entero se declara no tipable, sin información sobre qué parte era el problema.

Para un lenguaje fuente diseñado a la vez que su sistema de tipos, esas limitaciones son aceptables. Para un binario, son fatales.

19.6 Recuperación de tipos en un binario

En ingeniería inversa

Por qué la unificación pura no basta

En un binario no hay declaraciones, y la información de tipos hay que extraerla del uso. Las fuentes son abundantes pero todas parciales:

La instrucción usada. idiv implica con signo, div implica sin signo; movsx implica extensión de signo desde una anchura menor; cvtsi2sd implica que el origen es entero y el destino coma flotante; lea con escala 4 sugiere un array de elementos de 4 bytes.
El tamaño del acceso. mov al, [rbx] dice que hay un objeto de 1 byte en el desplazamiento 0.
Los prototipos conocidos. Una llamada a strlen dice que su argumento es char * y su retorno size_t. Esta es, con diferencia, la fuente más valiosa, y la que explica por qué las bases de datos de firmas de biblioteca importan tanto.
Las comparaciones. jb frente a jl distingue sin signo de con signo, igual que en el capítulo «9».
RTTI y vtables en C++, si no se han desactivado.

El problema es que estas fuentes se contradicen. El mismo registro puede usarse como int en un sitio y como puntero en otro, porque el compilador reutilizó el registro, o porque el programa hace type punning, o porque el análisis de SSA no separó bien los rangos de vida. Con unificación pura, una sola contradicción hace que el sistema no tenga solución y el análisis no devuelve nada.

Por eso los sistemas serios de recuperación de tipos abandonan la unificación en favor del subtipado:

TIE (Lee, Avgerinos y Brumley, 2011) define un retículo de tipos —con ⊤ arriba, ⊥ abajo, y los tipos concretos ordenados por subtipado— y genera restricciones de subtipo τ₁ ⊑ τ₂ en lugar de igualdades. El sistema resultante siempre tiene solución, porque en el peor caso todo colapsa a ⊤; y produce para cada variable un intervalo de tipos [cota inferior, cota superior] en lugar de un tipo único. Cuando el intervalo se estrecha a un punto, el tipo está determinado; cuando no, el analista ve lo que se sabe y lo que no.

Retypd (Noonan, Loginov y Cok, 2016) va más allá y trata el problema como uno de sistemas de empuje (pushdown systems), lo que le permite manejar simultáneamente subtipado, polimorfismo y tipos recursivos, y además inferir tipos de estructuras y sus campos en lugar de suponerlos dados. Es la base del motor de tipos de varias herramientas comerciales.

Ghidra y Hex-Rays usan enfoques híbridos: propagación de tipos por el grafo de def-use de la forma SSA, con reglas de resolución de conflictos y una fuerte dependencia de los prototipos de las funciones de biblioteca. No son sound en el sentido del capítulo «2», y no lo pretenden.

Consecuencia para el analista. El tipo que muestra un decompilador es una hipótesis, no un hecho, y suele ser la hipótesis más débil compatible con los usos observados. Cuando uno declara un tipo a mano, no está «corrigiendo» al decompilador: está añadiendo una restricción al sistema, que se propaga por las cadenas def-use y estrecha los intervalos de todo lo relacionado. De ahí el efecto en cascada que se observa al declarar bien un solo prototipo.

Formalización

Igualdad frente a subtipado, formalmente

Con unificación, el sistema de restricciones se resuelve sobre el álgebra libre de términos, y la solución —si existe— es el unificador más general. La estructura relevante es un álgebra de términos y el algoritmo es union-find.

Con subtipado, las restricciones son de la forma τ₁ ⊑ τ₂ sobre un retículo de tipos, y el problema pasa a ser el de calcular el menor punto fijo de un sistema de inecuaciones —exactamente el problema del capítulo «5»—. Eso tiene tres consecuencias:

Siempre hay solución, posiblemente trivial. No existe el fallo de unificación.
Los constructores de tipo requieren varianza: un puntero es covariante en lectura y contravariante en escritura, lo que en la práctica lleva a distinguir «tipo cargado desde» y «tipo almacenado en» para cada posición.
El coste sube: de casi lineal a, típicamente, cúbico, por la misma razón que en el capítulo «17».

La elección entre ambos no es de gusto: la unificación es adecuada cuando el programa fue escrito para ser tipable, y el subtipado cuando el tipado se está reconstruyendo a posteriori. Es la diferencia entre un compilador y un decompilador.

19.7 Lecturas

La técnica es una variante de Damas–Hindley–Milner (Hindley 1969, Milner 1978, Damas 1984), en la presentación por restricciones de Wand (1987). La estructura union-find es de Galler y Fischer (1964).

El capítulo «20» trata los sistemas de tipos desde un ángulo distinto: tipos anotados con efectos.

Sobre recuperación de tipos a partir del binario, las referencias son Lee, Avgerinos y Brumley, TIE: Principled Reverse Engineering of Types in Binary Programs (NDSS 2011), y Noonan, Loginov y Cok, Polymorphic Type Inference for Machine Code (PLDI 2016), que presenta Retypd.