Hidden in the Branches

Compilers have a boring public life. Their input is text, their output is text, and the process is usually hidden behind a command line. Internally, though, they deal with much richer objects. In this post I want to advertise those that I particularly like: the shapes that compilers draw from the possible values of program variables.

Before a program runs, a compiler can still learn a great deal about what's possible in a run, which is extremely useful for optimizing the program. It may not be able to know the exact values of a variable x without running the program, but it may learn that x is always odd, that it is positive, or, in the kind of analysis that we're talking about, that it lies within some range. As more variables are considered at once, these ranges turn into lines, areas, and eventually three-dimensional shapes.

Consider a small movement rule for a game:

dx = input.x
dy = input.y
dz = input.z

if abs(dx) + abs(dy) + abs(dz) <= 1:
    position.x += dx
    position.y += dy
    position.z += dz

The rule gives each step a fixed movement budget. Moving in x uses part of the budget, so there is less left for y and z. At the line where the position is updated, the possible values of the three variables are exactly the triples accepted by the condition:

|dx| + |dy| + |dz| <= 1

That condition makes a 3-dimensional solid. More concretely an octahedron with six corners, eight triangular faces, one point on each positive and negative axis. It's pleasant to look at:

The shape is determined by linear inequalities. One face comes from dx + dy + dz <= 1, another from dx + dy - dz <= 1, another from dx - dy + dz <= 1, and so on through the possible choices of signs. The branch condition in the program has become a polyhedron.

This is the setting of polyhedral analysis. It works with program facts made from linear expressions: i < n, i + j <= len, used + free == capacity. These facts show up around counters, lengths, offsets, capacities, and budgets, because many program quantities are updated and compared by adding or subtracting.

The analysis keeps these facts as a collection of linear inequalities. That choice is what makes the shapes convex, and it is a practical choice: linear constraints are useful enough to express many relationships in programs, and simple enough to compute with as the program passes through branches and loops. Of course, the cost is that the analysis cannot draw every actual strange shape. Separate cases get covered by one larger shape, inconvenient conditions get replaced by something that is more easily expressible.

So polyhedral analysis has a literal name. It is a way for a compiler to learn facts about a program by producing and transforming polyhedra.


Compiler steganography

Here is a small binary perceptron. It has three weights and processes two observations derived from four binary inputs. When an observation is classified incorrectly, the usual perceptron update adjusts the weights: 

def fit(a, b, c, d, label):
    assert (
        a in [-1, 1]
        and b in [-1, 1]
        and c in [-1, 1]
        and d in [-1, 1]
        and label in [-1, 1]
    )

    weights = [0, 0, -8]

    observations = (
        (
            a + 3*b + 3*c + d,
            3*a + b - c - 3*d,
            3,
        ),
        (
            -a + c + 2*d,
            a + 2*b + c,
            1,
        ),
    )

    for observation in observations:
        margin = label * sum(
            weight * feature
            for weight, feature in zip(weights, observation)
        )

        if margin <= 0:
            weights = [
                weight + label * feature
                for weight, feature in zip(weights, observation)
            ]

    return tuple(weights)

Do you notice anything suspicious about this program? Is there a feeling that it tries to hide something?
Let's try to see what is the shape of weights in this example.

reveal

The convex hull of the three values in weights is exactly this polyhedron:

The gemstone-shaped convex hull of the perceptron's possible final weights

Across all values permitted by the assertions, its executions finish in seventeen extreme states. One is the bottom point. Eight form the wide middle of the gemstone, while another eight form the smaller, rotated ring around its crown.


References

A reading map for polyhedral analysis and the abstract domains behind it.


return home