Widening, narrowing y análisis de intervalos

Operativo · Actualizado el 16 de agosto de 2026

Una limitación central del enfoque de los marcos monótonos es la exigencia de que los retículos tengan altura finita. Este capítulo describe la técnica que la supera —el widening, y su compañera el narrowing, ambas de Cousot y Cousot (1977)— y la aplica al análisis que más falta hace en ingeniería inversa: acotar los valores que puede tomar un registro.

8.1 El análisis de intervalos

Un análisis de intervalos calcula, para cada variable entera, una cota inferior y una superior de sus valores posibles. Los resultados son directamente aprovechables: comprobación de límites de arrays, detección de desbordamientos aritméticos, elección de la representación en tiempo de ejecución, y —en binarios— acotación de los destinos de un salto indirecto.

El retículo que describe un solo valor abstracto es

Interval = lift( { [l, h] : l, h ∈ N ∧ l ≤ h } )

donde N = {-∞, …, -2, -1, 0, 1, 2, …, ∞} es el conjunto de enteros extendido con extremos infinitos, y el orden se define por inclusión:

[l₁, h₁] ⊑ [l₂, h₂] ⟺ l₂ ≤ l₁ ∧ h₁ ≤ h₂

                        [-inf, +inf]
                    /        |         \
          [-inf, 0]      [-2, 2]        [0, +inf]
             / \          /   \           / \
      [-inf,-1] [-2,1] [-1,2]  ...   [1,+inf] [2,+inf]
              \    |     |    /
             [-2,0] [-1,1] [0,2]
                \    |    /
              [-1,0] [0,1] [1,2]
                  \   |   /
             [-1,-1] [0,0] [1,1] [2,2]
                     \  |  /
                       _|_

Fragmento del reticulo de intervalos. Se extiende infinitamente hacia los lados.

Este retículo no tiene altura finita: contiene, por ejemplo, la cadena infinita

[0,0] ⊑ [0,1] ⊑ [0,2] ⊑ [0,3] ⊑ [0,4] ⊑ …

Y lo mismo ocurre con el retículo de estados abstractos State = Var → Interval.

La evaluación abstracta de expresiones es la esperada:

eval(sigma, X)        = sigma(X)
eval(sigma, I)        = [I, I]
eval(sigma, input)    = [-inf, +inf]
eval(sigma, E1 op E2) = op^(eval(sigma,E1), eval(sigma,E2))

con los operadores abstractos definidos, en general, como

op^([l₁,h₁], [l₂,h₂]) = [ min_{x ∈ [l₁,h₁], y ∈ [l₂,h₂]} (x op y) , max_{x ∈ [l₁,h₁], y ∈ [l₂,h₂]} (x op y) ]

Por ejemplo +^([1,10], [-5,7]) = [1-5, 10+7] = [-4, 17].

Esta definición es elegante en matemáticas y molesta de implementar: escrita literalmente, recorrer todos los pares es lineal en la magnitud de los números, lo cual es inaceptable. Para la suma y la resta hay fórmulas cerradas evidentes; para la multiplicación hay que considerar los cuatro productos de extremos y quedarse con el mínimo y el máximo; para la división y la comparación hay que ir con cuidado con el cero y con el truncamiento.

Las reglas de restricción son las habituales de un análisis hacia adelante: JOIN(v) = ⊔_{w ∈ pred(v)} ⟦w⟧, la regla de la asignación ⟦v⟧ = JOIN(v)[X ↦ eval(JOIN(v), E)], y ⟦v⟧ = JOIN(v) para todo lo demás.

8.2 El punto fijo existe, pero no se alcanza

Hasta ahora hemos definido el resultado de un análisis como la solución mínima de sus restricciones, apoyándonos en el teorema de Kleene. Pero el teorema de Kleene exige altura finita, y el retículo de intervalos no la tiene. ¿Existe siquiera la solución mínima?

Formalización

Teorema del punto fijo de Tarski

En un retículo completo L, toda función monótona f : L → L tiene un único menor punto fijo, dado por

lfp(f) = ⊓ { x ∈ L : f(x) ⊑ x }

Demostración. Sea D = {x ∈ L : f(x) ⊑ x} y d = ⊓D. Veamos primero que d es punto fijo. Sea x ∈ D. Entonces d ⊑ x, porque d es cota inferior de D. Por monotonía, f(d) ⊑ f(x), y f(x) ⊑ x porque x ∈ D. Luego f(d) ⊑ x, es decir, f(d) también es cota inferior de D. Como d es la mayor cota inferior, f(d) ⊑ d. Aplicando monotonía otra vez, f(f(d)) ⊑ f(d), luego f(d) ∈ D, y como d es cota inferior de D, d ⊑ f(d). Por antisimetría, f(d) = d.

Para la minimalidad: si d' es otro punto fijo, entonces f(d') = d' ⊑ d', luego d' ∈ D, y como d es cota inferior, d ⊑ d'. Por antisimetría el menor punto fijo es único. ∎

Obsérvese la diferencia crucial con Kleene: el teorema de Tarski no exige altura finita, pero tampoco es constructivo. Dice que la respuesta existe; no dice cómo llegar a ella. El de Kleene es más débil en hipótesis pero da directamente un algoritmo.

Como las funciones de restricción del análisis de intervalos son monótonas, el teorema de Tarski garantiza que existe una solución más precisa bien definida. Pero no podemos calcularla con los algoritmos de los capítulos «5» y «7»: para algunos programas la sucesión de aproximantes fⁱ(⊥) no converge nunca. El caso más sencillo es un contador dentro de un bucle: [0,0] ⊑ [0,1] ⊑ [0,2] ⊑ … y el algoritmo no termina.

8.3 Widening simple

La solución consiste en renunciar deliberadamente a precisión para forzar la convergencia.

Sea f : L → L la función del algoritmo de punto fijo. La forma más simple de widening introduce una función ω : L → L tal que la sucesión

(ω ∘ f)ⁱ(⊥) para i = 0, 1, …

converge a un punto fijo mayor o igual que cada aproximante fⁱ(⊥), y por tanto representa información correcta sobre el programa. Para garantizarlo basta que ω sea monótona, extensiva —es decir, ∀x : x ⊑ ω(x)— y que su imagen ω(L) = {ω(x) : x ∈ L} tenga altura finita. Los algoritmos de punto fijo se adaptan trivialmente aplicando ω en cada iteración.

Intuitivamente, ω engrosa la información lo suficiente para asegurar la terminación. Para el análisis de intervalos se define punto a punto, en relación con un conjunto B formado por un número finito de enteros más -∞ y ∞. Típicamente B se siembra con todas las constantes enteras que aparecen en el programa, aunque caben otras heurísticas. Sobre intervalos individuales:

ω'([l, h]) = [ max{ i ∈ B : i ≤ l }, min{ i ∈ B : h ≤ i } ] y ω'(⊥) = ⊥

es decir, el intervalo que mejor encaja entre los permitidos. Y sobre el retículo completo, aplicando ω' a cada intervalo de cada estado abstracto:

ω(σ₁, …, σₙ) = (σ'₁, …, σ'ₙ) donde σ'ᵢ(X) = ω'(σᵢ(X))

El widening no sólo sirve para retículos de altura infinita: también se usa como técnica de aceleración en análisis con retículos de altura finita que convergen demasiado despacio y donde se tolera perder precisión.

8.4 Narrowing

El widening generalmente se pasa de largo, pero una técnica posterior, el narrowing (estrechamiento), puede mejorar el resultado.

Sea f_ω el resultado del análisis con widening. El narrowing consiste sencillamente en calcular f(f_ω). El razonamiento es corto y bonito: sabemos que lfp(f) ⊑ f_ω. Entonces f(f_ω) ⊑ ω(f(f_ω)) = (ω ∘ f)(f_ω) = f_ω, porque ω es extensiva y f_ω es punto fijo de ω ∘ f. Es decir, f(f_ω) es al menos tan preciso como f_ω. Además f(f(f_ω)) ⊑ f(f_ω) por monotonía, luego f(f_ω) ∈ {x : f(x) ⊑ x} y por el teorema de Tarski lfp(f) ⊑ f(f_ω): sigue siendo una aproximación segura. Y la técnica puede iterarse:

∀i : lfp(f) ⊑ fⁱ⁺¹(f_ω) ⊑ fⁱ(f_ω) ⊑ f_ω

Un ejemplo lo demuestra. Considérese:

y = 0; x = 7; x = x+1;
while (input) {
    x = 7;
    x = x+1;
    y = y+1;
}

Sin widening, el algoritmo ingenuo produce esta sucesión divergente para el punto posterior al bucle:

[x -> bottom, y -> bottom]
[x -> [8,8],  y -> [0,1]]
[x -> [8,8],  y -> [0,2]]
[x -> [8,8],  y -> [0,3]]
...

Con widening basado en B = {-∞, 0, 1, 7, ∞}, sembrado con las constantes del programa, la sucesión converge:

[x -> bottom,   y -> bottom]
[x -> [7,+inf], y -> [0,1]]
[x -> [7,+inf], y -> [0,7]]
[x -> [7,+inf], y -> [0,+inf]]

El resultado para y es lo mejor que se puede decir, pero el de x es decepcionante: sabemos que x vale exactamente 8. Unas pocas iteraciones de narrowing lo arreglan:

[x -> [8,8], y -> [0,+inf]]

que es la mejor respuesta posible para este programa. Ojo: la sucesión decreciente f_ω ⊒ f(f_ω) ⊒ f²(f_ω) ⊒ … no tiene garantizada la convergencia, así que en la práctica una heurística decide cuántas veces aplicar el narrowing.

8.5 El operador de widening

La forma simple de widening es innecesariamente agresiva: engrosar todos los intervalos de todos los estados abstractos en cada iteración no hace falta para asegurar la convergencia. El widening tradicional usa en su lugar un operador binario

∇ : L × L → L

que debe cumplir dos condiciones: ser un operador de cota superior, ∀x, y : x ⊑ x ∇ y ∧ y ⊑ x ∇ y; y que para toda sucesión creciente z₀ ⊑ z₁ ⊑ z₂ ⊑ …, la sucesión definida por y₀ = z₀ e y_i+1 = yᵢ ∇ z_i+1 converja en un número finito de pasos.

Con un operador así, el menor punto fijo se aproxima calculando

x₀ = ⊥ , x_i+1 = xᵢ ∇ f(xᵢ)

Esta sucesión converge —existe k con x_k+1 = x_k— y el resultado es una aproximación segura: lfp(f) ⊑ x_k.

procedure FixedPointWithWidening(f)
    x := bottom
    while x != f(x) do
        x := x widen f(x)
    return x

La idea del operador binario es que permite combinar la información de la iteración anterior con la de la actual —el argumento izquierdo y el derecho, respectivamente— y engrosar sólo los valores abstractos que son inestables. Un intervalo que no ha crecido durante una iteración no puede ser responsable de la divergencia, así que no hay razón para castigarlo.

Para el análisis de intervalos:

bottom widen' y = y
x widen' bottom = x

[l1,h1] widen' [l2,h2] = [l3, h3]   donde

  l3 = l1                          si l1 <= l2
     = max { i in B : i <= l2 }     en otro caso

  h3 = h1                          si h2 <= h1
     = min { i in B : h2 <= i }     en otro caso

y ∇ se define punto a punto a partir de ∇', igual que antes. Con esta forma más avanzada de widening y sin usar narrowing, el programa de ejemplo de la «sección 8.4 · Narrowing» da ya el mismo resultado que antes se obtenía combinando widening simple y narrowing.

Formalización

El widening binario es estrictamente más potente

Si se toma ∇ = ⊔, el cálculo procede exactamente igual que el algoritmo de punto fijo ordinario; y ⊔ es un operador de widening válido si L tiene altura finita. La forma simple de la «sección 8.3 · Widening simple» es también un caso particular: basta definir x ∇ y = ω(x ⊔ y).

Pero la diferencia no es sólo de conveniencia. Con la forma simple, el análisis usa efectivamente un subconjunto finito y fijo de L. La forma tradicional es fundamentalmente más potente: aunque cada programa concreto use sólo finitos elementos de L, Cousot y Cousot demostraron en 1992 que ningún subconjunto de altura finita sirve para todos los programas. El operador binario elige, en cada punto y para cada programa, un subconjunto distinto.

8.6 Dónde aplicar el widening

Se puede afinar más observando que la divergencia sólo puede aparecer en presencia de restricciones recursivas, es decir, de ciclos en el sistema de ecuaciones. Basta, por tanto, aplicar el widening en las cabeceras de bucle:

sigma''_i(X) = sigma_i(X) widen' sigma'_i(X)   si el nodo i es cabecera de bucle
             = sigma'_i(X)                      en otro caso

Como todo ciclo del CFG pasa por al menos una cabecera de bucle —en un grafo reducible, por definición—, esto basta para garantizar la convergencia, y mejora sensiblemente la precisión, porque los nodos que no son cabecera conservan sus intervalos exactos.

La generalización de esta idea a grafos arbitrarios es el orden topológico débil (weak topological ordering) de Bourdoncle, que identifica un conjunto de puntos de widening válido —el conjunto de «cabezas» de su descomposición jerárquica— y simultáneamente fija un orden de iteración eficiente. Es lo que implementan los analizadores serios.

8.7 Más allá de los intervalos

El análisis de intervalos es el ejemplo canónico de una familia amplia de dominios numéricos abstractos, ordenados por precisión y por coste:

Dominio	Qué expresa	Coste
Signos	`x > 0`	trivial
Intervalos	`a ≤ x ≤ b`	lineal
Congruencias	`x ≡ a (mod n)`	lineal
Zonas (zones)	`x - y ≤ c`	cúbico
Octógonos	`±x ±y ≤ c`	cúbico
Poliedros	`Σ aᵢxᵢ ≤ c`	exponencial en el peor caso

Los tres últimos son dominios relacionales: expresan relaciones entre variables, no propiedades de cada variable por separado. Es la diferencia entre saber que i ∈ [0, 100] y n ∈ [0, 100], y saber que i < n. El capítulo «9» vuelve sobre esto.

El dominio de congruencias merece una mención aparte porque en binarios resulta sorprendentemente útil: saber que un puntero es múltiplo de 8 o de 16 es lo que permite reconocer accesos alineados a estructuras y arrays.

8.8 Value-Set Analysis

En ingeniería inversa

El análisis de intervalos, adaptado a binarios

En un binario, el análisis de intervalos tal cual no sirve, por dos razones. Primera: los valores interesantes son direcciones, y un intervalo de direcciones que cruza dos objetos distintos no significa nada. Segunda: los accesos a arrays y estructuras tienen paso (stride), y un intervalo denso pierde justo la información que importa.

El Value-Set Analysis (VSA), de Balakrishnan y Reps, resuelve ambas cosas y es el análisis fundamental del análisis de binarios. Tiene tres ingredientes:

1. Regiones de memoria. El espacio de direcciones se particiona en regiones: una región global para los datos estáticos, una por cada marco de activación de procedimiento, y una por cada sitio de asignación dinámica. Una dirección no es un número: es una pareja (región, desplazamiento dentro de la región). Así, dos punteros a regiones distintas son automáticamente disjuntos, sin necesidad de razonar sobre sus valores numéricos.

2. Intervalos con paso (strided intervals). En lugar de [l, h] se usa s[l, h], que denota {l, l+s, l+2s, …, h}. El acceso mov eax, [rbx + rcx*4] con rcx ∈ 1[0,9] produce un desplazamiento en 4[0,36]: exactamente un array de diez enteros de cuatro bytes. Un intervalo denso [0,36] habría perdido esa estructura. La variante refinada, las congruencias de intervalos reducidas (reduced interval congruences), combina el intervalo con información modular.

3. Value-sets. El valor abstracto de una variable es una función que asigna a cada región de memoria un intervalo con paso. Es un producto de retículos indexado por regiones —exactamente el constructor de la «sección 5.4 · Cómo construir retículos»— y su altura es infinita, así que necesita widening.

Sobre VSA se construye la recuperación de variables: el análisis observa qué desplazamientos del marco de pila se acceden y con qué tamaños, y particiona el marco en variables locales. El algoritmo complementario, la identificación de estructura agregada (Aggregate Structure Identification, ASI), reconstruye a partir de ahí los campos de las estructuras y las dimensiones de los arrays. Cuando Hex-Rays le muestra struct_A *v3 con campos en los desplazamientos 0, 8 y 16, eso es lo que ha ocurrido por debajo.

Consecuencia práctica: el widening es la razón de que su decompilador a veces le diga que un índice está en [0, +∞). No es que la herramienta sea tonta; es que ha engrosado un intervalo inestable para poder terminar. Si el análisis ofreciera un botón de «aplica más narrowing aquí», el resultado mejoraría. Algunas herramientas lo ofrecen indirectamente, permitiendo al analista fijar a mano el rango de una variable: eso equivale a sembrar B con una constante nueva.

8.9 Lecturas

El capítulo «21» trata el mismo material desde el punto de vista de la interpretación abstracta, con más generalidad sobre las condiciones que debe cumplir un operador de widening.

La tabla de dominios numéricos de la «sección 8.7 · Más allá de los intervalos» sintetiza literatura dispersa: congruencias (Granger, 1989), zonas y octógonos (Miné, 2001 y 2006), poliedros (Cousot y Halbwachs, 1978).

Las referencias originales del widening y el narrowing son Cousot y Cousot (1977); el resultado de que ningún subconjunto de altura finita basta para todos los programas es de Cousot y Cousot (1992); el orden topológico débil es de Bourdoncle (1993). La «sección 8.8 · Value-Set Analysis» se apoya en Balakrishnan y Reps, Analyzing Memory Accesses in x86 Executables (2004), y en su trabajo posterior sobre ASI y sobre la herramienta CodeSurfer/x86.