Abstract Interpretation

In this essay, I will compare and contrast two different abstract domains: the Octagon abstract domain by Miné [6] and the Fast Polyhedra domain by Singh et al. [9]. In doing so, I will attempt to answer the question: “what is the abstract interpretation philosophy?”.

The Price of Precision

The Octagon and Fast Polyhedra domains exhibit two different (philosophical) reactions to the same problem: How do we manage the trade-off between precision and cost? To illustrate this trade-off, I consider two extremes.

At one extreme, we can perform an extremely imprecise but cheap analysis using the Interval domain [5] (Figure 1).

The Interval domain abstracts away much detail, making it imprecise but efficient – the complexity is linear in the number of variables [3]. The price of this efficiency is a lack of precision. In particular, the interval abstract domain is non-relational. This means that we cannot express relationships between variables x and y. In practice, this means that the program in Figure 2 cannot be analysed using the interval domain.

At the other extreme, we can use the Polyhedra abstract domain. This interprets program fragments into polyhedra, with form

\[ a_1 x_1 + a_2 x_2 + \ldots + a_n x_n \leq b \]

where \(x_i\) are variables and (for simplicity) \(a_i, b \in \mathbb{R}\). Note that the domain can also express equality constraints \(D x = e\), and that this can be encoded as \(\{ D x \leq e ; - D x \leq -e \}\).

The Polyhedra domain is relational, and significantly more expressive. For example, it can statically determine the constraint in Figure 2.

However, this precision comes at a heavy cost. The Polyhedra domain has time and space complexity exponential in the number of variables [3]. This is a severe cost, even to pay at compile time. Empirically, analysis using the Polyhedra domain frequently takes longer than four hours, or exhausts memory, making it an incredibly brittle tool in practice [9].

There are two philosophical approaches to this problem, which I shall term the “theoretical” and “empirical” approaches.

The Theoretical Approach

The theoretical approach is embodied by Miné’s [6] Octagon Domain.

Miné’s key insight is that one can find a middle-ground between the Interval and Polyhedra domains, by only allowing constraints of the form

\[ x \pm y \leq b \]

In effect, a restriction of the Polyhedra-style constraints to two variables, whose coefficients are \(-1\), \(0\), or \(+1\). Note that this is actually sufficient to perform the analysis in Figure 3, though clearly less expressive in the general case.

Having traded off expressiveness, what do the efficiency savings look like? Key to efficiency is choosing the right representation. In the Octagon domain, the representation is based on Difference-Bound Matrices (DBM). A DBM \(M\) is a square matrix that encodes “difference constraints” of the form \(x_i - x_j \leq b\) via entries \(M_{ij} = b\) (Figure 4). In essence, each variable is turned into a row/column index.

This is not sufficient for an Octagon, since we need to also represent constraints of the form \(x_i + x_j \leq b\) and \(x_i \leq b\). The key adaption happens in two steps: First, we can duplicate each variable \(x_i\) into two “forms”: \(x_i^+\) and \(x_i^-\), which we embed as a row/column index via a bijection \(\beta\)

\[ \beta(y) = \left\{\begin{array}{lr} 2i, & \text{if } y = x_i^+\\ 2i+1, & \text{if } y = x_i^- \end{array}\right. \]

Second, we translate “octagonal constraints” into constraints in the DBM. Two representative translations are listed:

\[ \begin{array}{rcl} x_i + x_j \leq b & \mapsto & x_i^{+} - x_j^{-} \leq b \; \land \; x_j^{+} - x_i^{-} \leq b\\ x_i \leq b & \mapsto & x_i^{+} - x_i^{-} \leq 2b \end{array} \]

We can thus import the machinery of DBMs to perform analysis on the Octagon domain. One key property is that, since \(\leq\) is a preorder, we can treat a DBM \(M\) as an adjacency matrix for a weighted graph \(G\). We can thus import the machinery of graphs to conduct analysis: for example, we can compute the shortest-path closure \(M^*\) in an obvious way. Additionally, we can use the Bellman-Ford algorithm to test for negative cycles (which correspond to unsatisfiable constraints \(x_i - x_i \leq -n\)).

With this view, we will find that some operations, like the union and intersection of two octagons, are best expressed as standard matrix operations on \(M\). Other operations, like inclusion tests, are expressed as graph-like operations on \(M^*\). Since the algorithms are standard, so too is the analysis, which illustrates that the Octagon domain has time complexity \(O(n^3)\) and space complexity \(O(n^2)\). By picking the right representation, we can appeal to standard algorithmic techniques.

Two points are worth further consideration. First, a theoretical (rather than empirical) flavour permeates through this paper. Take the widening operator, which is used to address the problem of non-termination in loops. Miné writes that “fixpoints are not computable” in the Octagon domain, and thus applies the widening operator eagerly, on every iteration of a loop. Of course, some fixpoints are computable. Hence, we may be less eager in our application of widening. For example, Singh et al. climb the lattice a finite (and empirically-determined) number of times \(n\) before switching to widening. Miné’s approach is more uniform, but less precise. In my opinion, this is an aesthetic choice, illustrating the theoretical flavour of the paper.

The second is: to what extent is the Octagon domain successful? I am not entirely sure. It is clear that having another point on the cost-efficiency curve is useful. What is not clear is just how useful. The problem is that expressiveness alone is not an entirely informative metric. How often do we need the Octagon/Polyhedra domain over the Interval/Octagon domain? Answers to these questions affect our measure of utility. In this course, we have seen cases where losing expressiveness does not necessarily result in lost utility (multi-shot continuations in Wasm [7]), and cases where the opposite holds (general recursion in Epigram [1]). Therefore, to justify the theoretician’s approach, we must make a fundamentally empirical argument.

The Empirical Approach

Empiricism is the core of Singh et al.’s [9] Fast Polyhedra Domain, which speeds up the Polyhedra Domain through two mechanisms.

First, they note that, empirically, most constraints relate only a small number of variables. Hence, we can partition variables by whether they share a constraint. For example, assuming variables \(\{x_1, x_2, x_3, x_4\}\), and the constraint set

\[ \{ x_1 + x_2 \leq 3, x_3 - x_4 \leq 7\} \]

we can partition the variables into two blocks: \(\{\{x_1, x_2 \}, \{x_3, x_4\}\}\).

Conceptually, partitions identify independent axes along which the polyhedra may be described. By analogy, a 2D vector varies independently along the \(x, y\) axes. Hence, the axes factor a complex polyhedron into simpler constituent polyhedra (“factors”), much like a 2D vector can be factored into its \(x\) and \(y\) components. In vector-space, factorisation allows us to add two vectors “component-wise”. Similarly, operations on polyhedra can be decomposed into operations on factors. For example, the meet operation can be performed “factor-wise”. This can lead to a speed-up, since for each factor, we may be able to ignore many variables and many constraints.

Second, they note that polyhedra can be represented two ways: as generators \(G\) or constraints \(C\). Some binary operations are cheaper when one argument is expressed using \(G\) and the other \(C\), some cheaper when both are expressed as \(C\), and some cheaper when both are expressed as \(G\). Hence, both representations are maintained via a conversion algorithm.

Building on these two key insights, Singh et al. layer numerous optimisations based on empirical evidence – like sparse matrix multiplication, checking smaller factors for inclusion first, and filtering out common constraints.

There are three questions worth addressing. First, does this approach actually work? At first glance, it certainly appears to – when evaluated on a set of benchmarks, Singh et al. see a speed-up ranging from “one to four orders of magnitude”. The doubts here are those that plague empiricism in general – to what extent do results generalise? There is no guarantee that partitions will not collapse into a singularity. To what extent does their technique over-fit to the benchmarks? Singh et al. pay little attention to describing whether they followed “good practice”, and developed their techniques behind a veil of ignorance.

Second, interestingly, the evaluation is performed on a CPU. The Octagon and Polyhedra domains rely heavily on vectors. Further, one of the advantages of factorisation is parallelisation. Efficient execution might be better achieved by matching the hardware to the compute. While some work [2] has been done in this space, it does not appear to have been widely explored.

Third, to what extent is the implementation correct? Singh et al. do not prove that their approach preserves semantics, which seems like a non-trivial property. Given the layers of complexity involved, such a proof might be significantly more complicated than a less empirical approach. This is a hidden dimension to the precision-cost trade-off: the difficulty of proving soundness.

The Philosophy of Abstract Interpretation

What, then, is the philosophy of abstract interpretation? I argue that the philosophy appears to stand on three pillars.

Find the Right Representation. Both the theoretical and empirical approaches feature a heavy emphasis on finding the right set of representations, with Singh et al. being willing to pay an exponential conversion cost to maintain the right representations.

Marry the Theoretical with the Empirical. Abstract interpretation cannot be free of theoreticians. It is important to note that even Singh et al.’s [9] empirical approach builds on a bedrock of theory – the lattice of partitions. I think building an abstract domain is like building a new, domain-specific programming language, whose purpose is to analyse an existing one. We want our operators to compose in expected ways, and our relationship with the existing language to be sound – assurances that can only be delivered by theory. But neither can it be free of empiricists, either. Just like any (real) programming language, an abstract domain needs to be built with an awareness of efficiency. Just as designers of programming languages have to incorporate empiricism into optimisation (cf. garbage collection), so too do designers of abstract domains.

Go it Alone. The last pillar is a stubborn desire to deliberately cripple oneself. Cousot [4] argues that type systems are just an instance of abstract interpretation. But while types also feature a cost/precision trade-off (cf. dependent types), this cost can be passed to the programmer. This makes analysis easier. Rather than having to develop automated techniques for generating proofs, with a type system, we can rely on the user to prove desired properties, and simply check their correctness. Is this better? Users can leverage domain-specific knowledge, which an automated technique struggles to recover. Still, it might take a user more than four hours to perform the calculations and annotate the program with them. But this cannot be our only metric – type systems give the user both more responsibility and agency. Responsibility can be annoying when automation excels, but agency is invaluable when the computer struggles behind a veil of opacity [8]. Type systems might scale better, and thus receive wider adoption.

References

1. [1] T. Altenkirch, C. McBride, and J. McKinna. Why Dependent Types Matter. Unpublished manuscript. 2005.
2. [2] F. Banterle and R. Giacobazzi. A Fast Implementation of the Octagon Abstract Domain on Graphics Hardware. In Static Analysis, pages 315–332. 2007.
3. [3] G. Brat, J. A. Navas, N. Shi, and A. Venet. IKOS: A Framework for Static Analysis Based on Abstract Interpretation. In Software Engineering and Formal Methods, pages 271–277. 2014.
4. [4] P. Cousot. Types as abstract interpretations. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 316–331. 1997. doi.org/10.1145/263699.263744
5. [5] P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 238–252. 1977. doi.org/10.1145/512950.512973
6. [6] A. Miné. The octagon abstract domain. In Proceedings Eighth Working Conference on Reverse Engineering, pages 310–319. 2001. doi.org/10.1109/WCRE.2001.957836
7. [7] L. Phipps-Costin, A. Rossberg, A. Guha, D. Leijen, D. Hillerström, K. C. Sivaramakrishnan, M. Pretnar, and S. Lindley. Continuing WebAssembly with Effect Handlers. arXiv:2308.08347. 2023. arxiv.org/abs/2308.08347
8. [8] B. Shneiderman. Designing the User Interface: Strategies for Effective Human-Computer Interaction. Addison-Wesley Longman Publishing Co., Inc. 1997.
9. [9] G. Singh, M. Püschel, and M. Vechev. Fast polyhedra abstract domain. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, pages 46–59. 2017. doi.org/10.1145/3009837.3009885