On Precision of Domain Combination (1)

In static analysis based on abstract interpretation, convex abstract domains such as the interval, octagon, or polyhedra domains are often employed to capture numerical invariants. However, these convex abstractions inherently lose precision when the concrete semantics involve disjunctions of states. In many verification problems, reasoning about disjoint execution paths or mutually exclusive conditions requires abstract domains capable of representing disjunctions explicitly.

To address this limitation, several constructions have been proposed to extend the expressiveness of existing domains:

• Disjunctive completion
• Cardinal power and state partitioning
• Trace partitioning

These constructions can be understood as domain combinators that systematically build new abstract domains from existing ones.

Domain Combinators

A domain combinator (or domain constructor) is a higher-order abstraction mechanism that takes one or more abstract domains as inputs and produces a new domain with well-defined semantics. Each abstract domain $\mathbb D^\sharp$ is characterized by:

• a concrete domain $\mathbb D = (\wp(\mathbb M), \subseteq)$,
• an abstraction function $\alpha : \mathbb{D} \rightarrow \mathbb D^\sharp$ and concretization $\gamma : \mathbb D^\sharp \rightarrow \mathbb{D}$,
• and abstract operators (post, join, widening, etc.).

The advantage of defining such combinators is that they can be defined once and for all, and implemented modularly. In ML-style pseudo-code, a domain is a module implementing a given interface:

module D = (struct ... end : DOMAIN)

and a abstract domain combinator is a functor:

module C = functor (D : DOMAIN) -> (struct ... end : DOMAIN)

Example: Product and Coalescent Product Domains

Given two abstract domains $(\mathbb D_0^\sharp, \gamma_0, \bot_0)$ and $(\mathbb D_1^\sharp, \gamma_1, \bot_1)$, the product abstraction is \((\mathbb D^\sharp_\times, \gamma_\times, \bot_\times)\) where

That is, the product abstraction expresses conjunctions of elements of \(\mathbb D^\sharp_0\) and \(\mathbb D^\sharp_1\).

However, this simple product may be imprecise:

A reduction or coalescent product is often applied to improve precision by enforcing consistency between both components.

Given abstract domains \((\mathbb D_0^\sharp, \gamma_0, \bot_0)\) and \((\mathbb D_1^\sharp, \gamma_1, \bot_1)\), their coalescent product \((\mathbb D^\sharp_{\otimes}, \gamma_{\otimes}, \bot_{\otimes})\) satisfies:

Nontheless, in many cases, the product and coalescent product abstractions remain insufficient to achieve reduction. For instance, combining the interval domain and the congruence domain:

result in an empty concretization, which suggests that mere product is still producing useless elements in the abstract domain. This leads to a question: Can we design abstract domains that inherently capture disjunctive properties?

Limitations of Convex Abstractions

Convex domains such as intervals, octagons, and polyhedra represent convex sets of numerical states. This convexity implies that the abstract join $\sqcup$—an over-approximation of concrete union—can introduce spurious states.

Such imprecisions may cause verification to fail, as the analyzer may infer spurious states that do not correspond to any concrete execution. Non-convex abstractions aim to overcome this limitation. For instance:

• The congruence domain expresses sets such as $\{ n + k p \mid k \in \mathbb{Z} \}$, which are non-convex.
• The sign domain includes an element $[=0]$ representing $\{0\}$, which is not convex, and $0\not\in\gamma([\neq 0])$, so $[\neq 0]$ also describes a non convex set, even though other elements like $[+]$ or $[-]$ correspond to convex sets.

Example 1: Verification Problem with Boolean Guards

Consider the following C program:

bool b0, b1;
int x, y;  // uninitialized
b0 = (x > 0);
b1 = (x < 0);
if (b0 && b1)
    y = 0;
else
    y = 100 / x;

At the division point, the operation is safe because:

• if $b_0$ holds, then $x > 0$;
• if $b_1$ holds, then $x < 0$;
• if either guard fails, then $x = 0$ cannot occur in a concrete execution reaching the division.

However, a non-relational abstraction such as intervals may represent $x \in [-\infty, +\infty]$ at this point, thus failing to verify safety. If we annotate the program with the invariant:

bool b0, b1;
int x, y;   // uninitialized

b0 = x >= 0;
(b0 && x >= 0) || (!b0 && x < 0)

b1 = x <= 0;
(b0 && b1 && x == 0) || (b0 && !b1 && x > 0) || (!b0 && b1 && x < 0)

if (b0 && b1) {
  (b0 && b1 && x == 0)
  y = 0;
  (b0 && b1 && x == 0 && y == 0)
} else {
  (b0 && !b1 && x > 0) || (!b0 && b1 && x < 0)
  y = 100 / x;
  (b0 && !b1 && x > 0) || (!b0 && b1 && x < 0)
}

This shows the necessity of symbolic disjunctions to reason about disjoint cases.

Example 2: Relation Between Variables

Consider another example:

int x, s, y;
if (x > 0)
    s = 1;
else
    s = -1;
y = x * s;
assert(y >= 0);

Here, $s$ is always non-null, and has the same sign as $x$, implying $y \ge 0$. Convex abstractions (such as intervals) cannot establish that $s \neq 0$, while the congruence domain cannot express the correlation between $s$ and $x$, capturing the correlation “$s$ has the same sign as $x$”. If we annotate the program with the invariant:

int x;    // x in Z
int s;
int y;
if (x >= 0){
  (x >= 0)
  s = 1;
  (x >= 0 && s == 1)
} else {
  (x < 0)
  s = -1;
  (x < 0 && s == -1)
}
(x >= 0 && s == 1) || (x < 0 && s == -1)

y = x / s;
(x >= 0 && s == 1 && y >= 0) || (x < 0 && s == -1 && y > 0)

assert(y >= 0);

Thus, expressing such relations requires a non-trivial relational and possibly disjunctive numerical abstraction.

Disjunctive Completion

Motivation

As discussed previously, convex abstract domains such as intervals or polyhedra fail to represent disjunctive properties. A natural idea to address this limitation is to extend a given abstract domain so that it can represent disjunctions of its own elements. This leads to the notion of the disjunctive completion (also called the distributive completion) of an abstract domain.

Distributive Abstract Domains

Let $(\mathbb D, \sqsubseteq_{\mathbb D}, \sqcup_{\mathbb D})$ be a concrete lattice and $(\mathbb D^\sharp, \sqsubseteq_{\mathbb D^\sharp}, \sqcup_{\mathbb D^\sharp})$ an abstract domain with a concretization function $\gamma : \mathbb D^\sharp \to \wp(\mathbb D)$. An abstract domain is said to be distributive (or disjunctive) if and only if:

That is, abstract joins correspond exactly to concrete unions.

Examples.

• The flat lattice of constants extended with $\top$ and $\bot$, i.e. $(\mathbb{Z}_0, \sqsubseteq)$, is distributive.
• The lattice $\{ \bot, [<0], [=0], [>0], [\leq 0], [\geq 0], [\neq 0], \top \}$ of signs is distributive.
• The lattice of intervals is not distributive. For example, there is no single abstract interval whose concretization equals the union of $\gamma([0,10])$ and $\gamma([12,20])$.

Definition of Disjunctive Completion

Disjunctive Completion. Given an abstract domain $(\mathbb D^\sharp, \sqsubseteq^\sharp)$ with concretization function $\gamma: \mathbb D^\sharp \to \wp(\mathbb D)$, the disjunctive completion $(\mathbb D^\sharp_{\mathrm{disj}}, \sqsubseteq^\sharp_{\mathrm{disj}})$ with a concretization function $\gamma_{\mathrm{disj}}: \mathbb D^\sharp_{\mathrm{disj}} \to \wp(\mathbb D)$ is the smallest distributive abstract domain that extended from $\mathbb D^\sharp$ such that:

To build the disjunctive completion domain, we follow these steps:

• include in $\mathbb D^\sharp_{\mathrm{disj}}$ all elements of the base abstract domain $\mathbb D^\sharp$,
• for all finite subsets $S \subseteq \mathbb D^\sharp$, such that there is no $x^\sharp \in \mathbb D^\sharp$ and $\gamma(x^\sharp) = \bigsqcup_{y \in S} \gamma(y)$, add the element $\bigsqcup S$ to $\mathbb D^\sharp_{\mathrm{disj}}$ with $\gamma_{\mathrm{disj}}(\bigsqcup S) = \bigcup_{y \in S} \gamma(y)$.

Theorem. The process of adding all distinct disjunctions of abstract elements yields a sound and distributive abstract domain.

Example 1: Completion of the Sign Domain

Consider the sign domain with elements \(\{[\!-\!], [0], [\!+\!], [\!-\!0], [0\!+], [\!-\!0\!+]\}\):

representing respectively $\{x<0\}$, $\{x=0\}$, $\{x>0\}$, $\{x\le 0\}$, $\{x\ge 0\}$, and $\mathbb{Z}$.

The disjunctive completion $\mathbb D^\sharp_{\mathrm{disj}}$ adds new abstract elements corresponding to all unions of disjoint sign classes. For example:

This completion allows representing non-convex sets such as $\{x < 0\} \cup \{x > 0\}$, which corresponds to $x \neq 0$—impossible to express in the base sign domain.

Example 2: Completion of the Constant Domain

Let the concrete lattice $\mathbb D = (\mathbb{Z}, \subseteq)$ and the abstract domain $\mathbb D^\sharp = \{ [k] \mid k \in \mathbb{Z}\} \cup \{\top\}$ with $\gamma([k]) = \{k\}$.
The disjunctive completion of $\mathbb D^\sharp$ is isomorphic to the powerset lattice $\wp(\mathbb{Z})$:

This completion is exact—no loss of information—but it is often infinite and computationally intractable.

A intermediate solution is to define $k$-bounded disjunctive completion, which restricts disjunctions to at most $k$ elements:

For $k=2$, the abstraction precisely represents all binary disjunctions (pairs of constants) while approximating larger disjunctions by $\top$.

Example 3: Completion of the Interval Domain

We still consider the concrete domain $\mathbb D = (\mathbb{Z}, \subseteq)$, but now let the abstract domain $\mathbb D^\sharp$ be the standard interval domain:

Its disjunctive completion $\mathbb D^{\sharp}_\mathrm{disj}$ collects all finite unions of disjoint intervals:

This representation is expressive and efficient compared to the powerset of constants, though potentially infinite.

Expressiveness. Note that $(\mathbb D^\sharp)^n_{\mathrm{disj}} \neq (\mathbb D^{\sharp}_\mathrm{disj})^n$. The former represents disjunctions across the entire tuple, while the latter represents independent disjunctions per component.

Application to Verification (Example Revisited)

Using the disjunctive completion of $(\text{intervals})^3$, we can express the invariant in Example~2:

which is impossible in convex domains but naturally expressible here. This demonstrates the gain in precision obtained through disjunctive completion.

Static Analysis with Disjunctive Completion

We recall that for a program semantics defined by a concrete post-condition operator:

where $\mathbb S$ is the set of program states, its abstraction should satisfy $\alpha \circ \text{post} \sqsubseteq \text{post}^{\sharp} \circ \alpha$. In the disjunctive completion domain, we can define:

which applies the abstract transfer function pointwise to each disjunct.

The disjunctive completion also provides an exact join operator:

However, it does not admit a general widening operator due to the combinatorial explosion of disjuncts.

Static Analysis with Disjunctive Completion

To carry out the analysis of a basic imperative language, we define the following components.

Operations for the Computation of Post-Conditions. We require a sound over-approximation for basic program steps.

• The concrete post-condition: \[ post : \wp(\mathbb{S}) \to \wp(\mathbb{S}) \] where $\mathbb{S}$ is the set of concrete states.
• The abstract post-condition: \[ post^{\sharp} : \mathbb{D}^{\sharp} \to \mathbb{D}^{\sharp} \] should satisfy the soundness property: \[ post \circ \gamma \subseteq \gamma \circ post^{\#}. \]

For example, when the post operation is the following cases:

• For assignments: \[ post^{\sharp} = assign \] which inputs a variable, an expression, and an abstract pre-condition, and outputs an abstract post-condition.
• For conditional tests: \[ post^{\sharp} = test \] which inputs a boolean expression, an abstract pre-condition, and outputs an abstract post-condition.

Additional Operators.

• An operator join for over-approximation of concrete unions.
• A widening operator $\nabla$ for the analysis of loops.
• A conservative inclusion checking operator.

Transfer Functions for the Computation of Abstract Post-Conditions

We assume a monotone concrete post-condition operation \( post : \mathbb{D} \to \mathbb{D}, \) and an abstract operation \( post^{\sharp} : \mathbb{D}^{\sharp} \to \mathbb{D}^{\sharp} \) such that \( post \circ \gamma \subseteq \gamma \circ post^{\sharp}. \)

Convention. If \( \gamma(y^{\sharp}) = \bigsqcup \{ \gamma(z^{\sharp}) \mid z^{\sharp} \in \mathcal{E} \}, \) we write \( y^{\sharp} = \bigsqcup\mathcal{E}. \)

Disjunctive Completion. For the disjunctive completion domain, we can simply define: \( post^{\sharp}_{disj}\bigl(\left[\sqcup \mathcal{E}\right]\bigr) = \{ \sqcup \, post^{\sharp}(x^{\sharp}) \mid x^{\sharp} \in \mathcal{E} \,\}. \) Note that the result may be an element of the initial domain.

Abstract Join, Inclusion, and Widening

• Abstract join: the disjunctive completion provides an exact join (exercise).
• Inclusion check: left as exercise.
• Widening: there is no general definition or solution to the disjunct explosion problem.

Limitations

While theoretically elegant, disjunctive completion suffers from severe practical issues:

• Combinatorial explosion: if $A$ has $n$ elements, then $A^{\mathrm{disj}}$ may have up to $2^n$ elements.
• Representation cost: for numerical domains such as intervals, $A^{\mathrm{disj}}$ can describe arbitrary finite unions of numbers.
• Lack of general widening: no universal strategy exists to ensure convergence during fixpoint computation.

A common mitigation technique is $k$-limiting, which bounds the number of disjuncts allowed in any element.
When merging disjunctions beyond this limit, the join operator must heuristically decide which disjuncts to retain or merge.