Automatic Repair of Overflowing Expressions
with Abstract Interpretation
Francesco Logozzo
Microsoft Research, Redmond, WA, USA

Matthieu Martel
Université de Perpignan Via Domitia, DALI, Perpignan, France
Université Montpellier II & CNRS, LIRMM, UMR 5506, Montpellier, France

We consider the problem of synthesizing provably non-overflowing integer arithmetic expressions or
Boolean relations among integer arithmetic expressions. First we use a numerical abstract domain
to infer numerical properties among program variables. Then we check if those properties guarantee
that a given expression does not overflow. If this is not the case, we synthesize an equivalent, yet
not-overflowing expression, or we report that such an expression does not exists.
The synthesis of a non-overflowing expression depends on three, orthogonal factors: the input
expression (e.g., is it linear, polynomial, . . . ?), the output expression (e.g., are case splits allowed?),
and the underlying numerical abstract domain – the more precise the abstract domain is, the more
correct expressions can be synthesized.
We consider three common cases: (i) linear expressions with integer coefficients and intervals;
(ii) Boolean expressions of linear expressions; and (iii) linear expressions with templates. In the first
case we prove there exists a complete and polynomial algorithm to solve the problem. In the second
case, we have an incomplete yet polynomial algorithm, whereas in the third we have a complete yet
worst-case exponential algorithm.

1

Introduction

Unwarranted integer overflows are a common source of bugs even for the most experienced programmers. Programmers have the tendency of forgetting that machine integers behave differently than mathematical integers and that apparently innocuous expressions may lead to hard to debug bugs in the program. Consider for instance the statement below, where y is a negative 32-bits integer
x = -y;

(1)

One may then expect that x is always a positive value, and also that x 6= y. However, this is false.
When y is the minimum value −231 , then x = −231 = y, i.e., the result of the negation of a negative
integer is negative! This is not an artificial example. The Math.abs function in the standard Java library
implements the absolute function value function according to the common mathematical definition (if
the input is non-negative return it, otherwise return its negation). As a consequence, Math.abs may
return a negative value, very likely breaking most callers relying on the (somehow obvious) fact that the
absolute value is always non-negative.
The mismatch between the mathematical interpretation and the machine interpretation comes by the
fact that the expression evaluation may originate in an arithmetic overflow: the result of the expression
may be too large (or too small) to be exactly represented on b bits.
Most abstract interpretation-based static analysis tools like cccheck [5] or Astree [1] can detect
potential arithmetic overflows. They first analyze the program using some numerical abstract domain
A. Banerjee, O. Danvy, K.-G. Doh, J. Hatcliff (Eds):
David A. Schmidt’s 60th Birthday Festschrift
EPTCS 129, 2013, pp. 341–357, doi:10.4204/EPTCS.129.21

342

Automatic Repair of Overflowing Expressions with Abstract Interpretation

(e.g., Intervals [3], Pentagons [9], Octagons [12]) to infer ranges and relations among program variables
at each program point. Then, they use such information to prove that the evaluation of an arithmetic
expression may never result into an overflow. If they cannot prove it, they emit a warning. For instance,
in the example above cccheck warns about the possible negation of the MinValue.
In this paper, we want to push it a step further. We envision static analysis tools not only reporting
possible arithmetic overflows, but also suggesting fixes for them. The suggested fixes are verified repairs
in the sense of [8]. A verified repair is an expression which is equivalent to the original one when
interpreted over the mathematical integers Z, but which does not overflow when evaluated according to
the given programming language semantics.
In general, the repair depends on three orthogonal factors:
(i) the input expression language, I ,
(ii) the output expression language, O,
(iii) the available semantic information, S , i.e., the underlying abstract domain and the abstract state
inferred by the analyzer.
For instance, let us consider the repairing of (1) where the input and output expression language are
arithmetic expressions with only the 4 operations. The semantic information is
S = {y ∈ [−231 , −1]}.
Under these conditions, there is no way to repair the expression. Our algorithm in Sec. 4 will prove that
there is no way to fix the expression (1). Nevertheless, if we change the hypotheses, allowing the output
language O to include expression casting, then -((long) y) is a verified repair for -y under S . The
arithmetic overflow disappears as 231 is exactly representable in 64 bits1 , and the semantics coincides
with that over Z. Alternatively, we can imagine adding the conditional expression to O. Then
y == MinValue? 0 : −y
is a repair in that the expression is guaranteed to not overflow, but it is not a verified repair as the Z
interpretation and the machine one disagree.
Example 1 Let us consider the code in Fig. 1, returning a sub-array of arr made up of count
elements from index start. The careful programmer added preconditions (using CodeContracts, [4])
to protect its code against buffer overruns: the starting index and the count should be non-negative (to
avoid buffer underflows) and the subsegment to extract should be included in the original array (to avoid
buffer overflows). However, when start and count are very large, start + count may result into
an arithmetic overflow, i.e., it evaluates to a negative value. As a consequence, the third precondition
is trivially satisfied (an array length is always non-negative), but the program will probably go wrong,
because of some buffer underflow later in the execution.
Again, sound static analysis tools like cccheck will spot the possible arithmetic overflow in the example above. Our goal here is to synthesize an arithmetic expression matching the intent of the programmer (i.e., the semantics over Z). The algorithm we introduce in Sec. 5 will synthesize the expression:
start <= arr.Length - count
1 Note

that this repair may require changing the nominal type of x if it is not defined as a long.

(2)

F. Logozzo & M. Martel

343

int[] GetSubArray(int[] arr, int start, int count)
{
Contract.Requires(0 <= start);
Contract.Requires(0 <= count);
Contract.Requires(start + count <= arr.Length);
// ... rest of the code omitted ...
}
Figure 1: A parameter validation incorrect because of overflows.
which is guaranteed to be arithmetic overflows-free. The reason for that is that the abstract element
S = {start ∈ [0, 231 − 1], count ∈ [0, 231 − 1], arr.Length ∈ [0, 231 − 1]}
implies that
arr.Length − count
can never be too small to cause an arithmetic overflow.
In general, on machine arithmetics (2) is not equivalent to the third postcondition of Fig. 1. Therefore,
the repair cannot be done in a purely syntactic way, but it requires some semantic knowledge.
Example 2 Let us consider I = O to be the language of arithmetic additions. For simplicity, let us
assume to have 4 bits signed integers. As a consequence −8 and 7 are respectively the smallest and the
largest representable natural numbers. The sum
x1 + x2 + x3 + x4 + x5 + x6 + x7

(3)

with the semantic knowledge
S = {x1 ∈ [−2, 3], x2 ∈ [−1, 0], x3 ∈ [1, 2], x4 ∈ [−3, −1], x5 ∈ [−3, −2], x6 ∈ [−1, 1], x7 ∈ [2, 4]}
may overflow when adding x6 to the partial sum — assuming left-to-right evaluation order.
Our algorithm in Sec. 4 will automatically synthesize the following sum:
x3 + x7 + x4 + x5 + x2 + x6 + x1

(4)

which is a verified repair, as (3) and (4) coincide with the Z interpretation, but (4) does not overflow.
Main Results. First, we will define the problem of the automatic repairing of overflowing expressions
starting from the semantic knowledge inferred by a static analyzer (Sec. 3). Next, we will focus our
attention on the common case of linear expressions with integer coefficients. We show that when the
underlying abstract domain is Intervals (Sec. 4) then there exists a complete and polynomial algorithm to
repair possibly overflowing expressions – this result was quite surprising for us. When the input language
is widened to consider relations among those linear expressions, then the algorithm is still polynomial,
but incomplete (Sec. 5). On the other hand, when the underlying abstract domain is refined to Octagons,
we have a complete yet worst-case exponential algorithm — this result can be easily generalized to
template-based numerical domains (Sec. 6). We will conclude evaluating a prototype implementation on
a set of benchmarks (Sec. 7).

344

2

Automatic Repair of Overflowing Expressions with Abstract Interpretation

Preliminaries

Syntax. Without any loss of generality we assume a strongly typed while-language W with expressions
E. Expressions are either arithmetic expressions (e.g., 5 ∗ x + 1) or relational expressions (e.g., x + 2 <
3 ∗ y). Variables are declared to belong to some integral type Mb . Expressions are well typed, too.
An integral type can be a signed or unsigned integer of b bits. The smallest representable unsigned
value over b bits is 0 and the largest is 2b − 1. The smallest representable signed is −2b−1 and the largest
one is 2b−1 − 1. We denote by M b and M b the smallest and the largest values of Mb . When clear from
the context, we will omit the subscript b.
Semantics. A program state either denotes an error or maps variables to values, i.e.,
Σ = {err} ∪ (Vars → Z).
The only way to reach the error state err is by means of an arithmetic overflow — for the sake of
simplicity we treat division by zero as a particular case of overflow. We assume a semantic evaluation
function
eval ∈ E × Σ → Z ∪ {err}.
The function eval respects a fixed left-to-right evaluation of arithmetic expressions (like C# or Java, but
unlike C).
If an arithmetic overflow is encountered during the evaluation of e ∈ E in σ ∈ Σ then eval(e, σ ) = err.
We define the relation |=notOverflow ∈ ℘(℘(Σ) × E) as
S |=notOverflow e ⇐⇒ ∀σ ∈ S. eval(e, σ ) 6= err.
The concrete semantics of a program P associates each program point pc ∈ PP with the set of reachable states ⊆ Σ. Formally: JPK ∈ PP → ℘(Σ).
An abstract domain hA , vi over-approximates sets of states. In the abstract interpretation framework, this is formalized by a Galois connection, i.e., by two monotonic functions α, γ such that
∀S ∈ ℘(Σ). S ⊆ γ ◦ α(S) and ∀a ∈ A . α ◦ γ(a) v a.
The abstract semantics of P associates each program point with a sound approximation of the reachable
states. Formally, JPKa ∈ PP → A is such that
∀pc ∈ PP. JPK(pc) ⊆ γ(JPKa (pc)).

3

The Problem

In order to define the problem of repairing (or synthesis) of non-overflowing expressions, we should
make all the underlying assumptions explicit.
First, we assume the program P is analyzed using a sound static analyzer with an underlying abstract
domain A [3, 19].
Second, we denote the set of potential arithmetic overflows by A = {hpp, ei | pc ∈ PP}.
Third, we define O, the subset of A for which we cannot prove the absence of overflows, using the
abstract domain A :
O = {hpp, ei ∈ A | γ(JPKa (pp)) 6|=notOverflow e}.

F. Logozzo & M. Martel

345

Usually, static analyzers stop here: They simply report the assertions O as possible overflows. We
want to move it a step further.
We want to propose a verified repair for the expressions in O. In general, we cannot hope to repair arbitrary arithmetic expressions, so we focus our attention on a given set of input expressions I .
Examples of I are sums with unary coefficients U = {e | e = ∑i xi } and linear arithmetic with integer
coefficients L = {e | e = ∑i ai · xi , ai ∈ Z}. The repaired, or non-overflowing output expression belongs
to a set of expressions O.
We require that I ⊆ O ⊆ W, i.e., the output expressions are at least as expressive as the input ones,
and both of them are expressible in our programming language. We assume that the expressions in I
and O are side-effect free.
Our problem is to find for each expression e in O an equivalent expression in O which is provably
non-overflowing according to the semantic information inferred by the static analyzer at program point
pp. Formally, we want an algorithmic characterization of the set of repairs:
RhI ,O,A i = {hpp, e0 i | hpp, ei ∈ O, e ∈ I , e0 ∈ O, e ≡Z e0 , γ(JPKa (pp)) |=notOverflow e0 }
where ≡Z denotes the equivalence of expressions when they are interpreted over natural numbers and
not machine numbers. In practice, we are interested in non-trivial solutions to R, or in non-trivial underapproximations of R. An example of a trivial solution is the brute-force generation of all the possible
parsings e0 of an expression e ∈ I followed by testing e0 whether or not may overflow. This solution is
exponential in the size of e, a situation we want to avoid. An example of a trivial under-approximation
is the empty set — i.e., no expression is repaired.

4

Linear Expressions with Integer Coefficients

We begin by focusing our attention on the very common case when I = O = L, i.e., the input and
the output languages are linear expression with integer coefficients. We assume the underlying abstract
domain A to be the abstract domain Intv of intervals [3]. In this section we show that there exists a
complete and polynomial algorithm for RhL,L,Intvi – Algorithm 1.
The first step of Algorithm 1 is a pre-processing step to get rid of multiplications of an integer
constant to a variable. Given an expression e ∈ L, i.e.,
n

e = ∑ ai · xi

with ai ∈ Z and 1 ≤ i ≤ n

i=1

each term of the sum ai · xi is replaced by the corresponding sum:
ai · xi = xi + . . . + xi .
| {z }
ai times

Without loss of generality, we assume that all the ai are positive. Otherwise:
(i) if ai is zero, then it is trivial to remove xi ,
(ii) if ai is negative, then we record it by negating the interval S (xi ).
The pre-processed expression is then in the form of ∑ki=1 yi where k = ∑ni=1 ai and yi are variables appearing in e.

346

Automatic Repair of Overflowing Expressions with Abstract Interpretation

Algorithm 1 Sum Refactoring
Require: An expression e ∈ L and a map S ∈ Vars → Z × Z
Ensure: A permutation π ∈ [1, k] → [1, k] indicating in which order to add the elements yi to avoid
overflows, or fail if it does not exist.
1:
2:
3:
4:
5:
6:
7:
8:
9:
10:
11:
12:
13:
14:
15:
16:
17:
18:

Transform e into a sum such that e = ∑ki=1 yi
Create Y>0 , Y<0 and Y>
R ← Y>0 ∪Y<0
s ← [0, 0]; i ← 1; π = λ j. j
while R 6= 0/ do
if ∃ j ∈ R such that s + S (y j ) ⊆ M then
s ← s + S (y j ); R ← R \ j
π(i) ← j; i ← i + 1
else
Fail
end if
end while
for all j ∈ Y> do
s ← s + S (y j ); π(i) ← j; i ← i + 1
if s 6⊆ M then
Fail
end if
end for

After pre-processing, Algorithm 1 partitions the (indexes of the) variables appearing in the expression
into three sets: the positive variables Y>0 , the negative variables Y<0 , and the variables that can be positive,
negative, or zero Y> . Let x and x denote respectively the lower and upper bounds of an interval x. Then
we can formally define the above sets as:
Y>0 = {i | 1 ≤ i ≤ k, yi > 0},Y<0 = {i | 1 ≤ i ≤ k, yi < 0},Y> = {i | 1 ≤ i ≤ k, yi ≤ 0 ∧ yi ≥ 0}.
We use the shortcut R = Y>0 ∪Y<0 for the set of variables that do contain zero.
The main loop of Algorithm 1 constructs a permutation of terms in the input sum such that the partial
sum s is kept as far as possible from M and M. Initially, the partial interval sum s is set to [0, 0] and π is
set to the identity function. The algorithm iteratively selects an element yi with i ∈ R such that s + yi ⊆ M
(while loop of Line 5). The index i is removed from R and the value of yi is added to partial (interval)
sum s. The permutation π records which term is selected at each iteration. If, at some iteration, there
exists no term yi with i ∈ R such that s + yi ∈ M then the algorithm fails. We will see in Property 4 that,
in this case, there exists no solution. Once all the elements with indexes in R have been selected, the
algorithm selects the elements whose indexes belong to Y> in any order (for loop of Line 13). If the sum
is not included in M then the algorithm fails.
Example 3 Let us consider the Ex. 1, with b = 4. In this case M4 = [−8, 7] and an overflow arises
when the term x6 ∈ [−1, 1] is added since the partial sum evaluates to [−9, 3] 6⊆ M4 . In Algorithm 1, Y>0 =
{3, 7}, Y<0 = {4, 5} and Y> = {1, 2, 6}. One output of the algorithm is (the permutation corresponding
to) the sum: x3 + x7 + x4 + x5 + x2 + x6 + x1 .
The Fig. 2 provides a graphical intuition of the way in which the Algorithm 1 works. It starts with

F. Logozzo & M. Martel

[1,2]

347

[2,4]

[-3,-1]

[-3,-2]

[-1,0]

[-1,1]

[-2,3]

6
4
2
0
-2
-4
-6
-8

Figure 2: The graphical evolution of the partial sums of the repaired expression in Ex. 4.
the interval [0, 0], and it greedily selects variables such that the current partial sum gets closer, e.g., to
M. When any value in Y>0 causes the partial sum to go above M, then elements from Y<0 are selected.
Graphically this means that the interval is heading toward M. The algorithm continues until R0 is empty,
or it is not possible to “correct” the partial sum. An interesting yet unexpected result is the following
one, stating that the algorithm is complete, i.e., if there exists a solution to RhL,L,Intvi then our algorithm
finds it. If it fails, there is no way to repair e using S .
Property 1 (Completeness) Let JPKa (pp) = S be an abstract element belonging to Intv. If Algorithm
1 fails then there exists no permutation π ∈ [1, k] → [1, k] of the elements of the sum such that the partial
sums of ∑ni=1 yπ(i) do not overflow, i.e. there is no e’ ∈ L such that e ≡Z e’ and γ(S ) |=notOverflow e’.
Proof First, let us focus on the while loop of Line 5. We show that if Algorithm 1 fails at Line 10
then any parsing of the sum leads to an overflow. More precisely, if ∃Y 0 and Y 00 such that Y 0 ∪Y 00 = [1, k],
Y 0 ∩Y 00 = 0,
/ s = ∑i∈Y 0 yi ⊆ M and ∀i ∈ Y 00 , s + yi 6⊆ M then ∑ki=1 yi 6⊆ M.
Let Y 00 = {b1 , . . . , bm } and let us focus on the upper bound. If ∀i, 1 ≤ i ≤ m, s + ybi > M then
s + yb1
s + yb2
..
.

>
>

s + ybm

> M.

M
M
..
.

Their sum implies that
ms +

∑ yb > mM.

b∈Y 00

Using the fact that s = ∑i∈Y 0 yi and that Y 0 ∪Y 00 = [1, k], Equation (5) can be transformed as follows:
ms + ∑b∈Y 00 yb > mM
⇔

(m − 1)s + s + ∑b∈Y 00 yb > mM

⇔ (m − 1)s + ∑a∈Y 0 ya + ∑b∈Y 00 yb > mM
⇔

∑ki=1 yi > mM − (m − 1)s.

(5)

348

Automatic Repair of Overflowing Expressions with Abstract Interpretation

Now, let us assume that s ≤ M. From the previous equation it follows that
k

∑ yi > mM − (m − 1)s ≥ mM − (m − 1)M.

i=1

Therefore, ∑ki=1 yi > M, which is a contradiction. The same arguments holds for the lower bound M.
Concerning the for loop of Line 13, any element yi with i ∈ Y> makes the bounds of s grow (except
for the trivial case of adding [0, 0]). Consequently, if we cannot fix the variables in R, there is no way
we can fix the initial set of variables. The interval sum is deterministic, so the partial sum after the while
loop of Line 5 is always the same interval, no matter which parsing is inferred. In the loop of Line 13,
the width of the interval for the partial sum can only grow at each step with one of the two bounds strictly
moving toward M or M. As a consequence, if some parsing fails then all the parsings fail.
Property 2 (Complexity) For a linear expression with O(k) variables, Algorithm 1 performs O(k2 )
operations.
Proof Constants are bounded and, consequently, the preprocessing may only add a constant multiplicative factor. So the number of terms in the sums given to Algorithm 1 is asymptotic linear in the
number of variables of the source expressions. The while loop of Line 5 is executed O(k) times and the
selection of j at Line 6 is done in O(k). The for loop of Line 13 being linear in k, the global complexity
of the algorithm is O(k2 ).

5

Relations among Linear Expressions

We extend the results of the previous section when the considered expressions are comparisons of linear
arithmetic expressions with unary coefficients. We consider the set
B = {e1 ♦ e2 | e1 , e2 ∈ L, ♦ ∈ {=, 6=, <, >, ≤, ≥}}
for input and output expressions. We use the abstract domain Intv for the semantic knowledge. The
Algorithm 2 computes an under-approximation to RhB,B,Intvi in polynomial time.
We first need to define some functions used by the algorithm. The (distance from zero) function
d ∈ Z × Z → Z is such that

d([x, x]) = max |x|, |x| .
We let d(e) denote d(evalIntv (e, JPKa (pp)), where evalIntv is the most precise evaluation of e using
unbounded interval arithmetics [13].
The function
select(X) ∈ ℘(Z × Z) → (Z × Z) ∪ {fail}
selects an interval x ∈ X such that M 6∈ x and ∀y ∈ X.d(y) ≤ d(x). If such an interval does not exist, then
select(X) = fail.
Given an (abstract) environment mapping variables to intervals S ∈ Vars → (Z × Z), we assume,
without losing generality, that S is injective — the Algorithm can be easily extended otherwise.
Finally, we let φS0 ,S ∈ Vars → E denote the sign of a variable. It is defined as φS0 ,S (x) = x if
S0 (x) = S (x); φS0 ,S (x) = −1 ∗ x if S0 (x) = −S (x) and undefined otherwise.
The idea of Algorithm 2 is to move terms to the left or the right of the ♦ relation, and then check
whether they overflow. If it cannot pick any variable, then it simply fails. The input of the algorithm are
two sets of variables, A and B, appearing as sum on the left and on the right of ♦. The set M remembers

F. Logozzo & M. Martel

349

Algorithm 2 Boolean Expressions Refactoring
Require: Two sets of variables A, B, a Boolean expression b = e1 ♦e2 such that e1 = ∑a∈A a and e2 =
∑b∈B b and an interval map S0 .
Ensure: A solution to the overflowing problem, or fail if it does not exist
1:
2:
3:
4:
5:
6:
7:
8:
9:
10:
11:
12:
13:
14:
15:
16:
17:
18:
19:
20:
21:
22:

M ← 0;
/ e01 ← e1 ; e02 ← e2 ; S ← S0
while ¬Algorithm1(e01 , S ) ∨¬Algorithm1(e02 , S ) do
if d(e01 ) ≥ d(e02 ) then
α ← select(S (A \ M ))
if α = fail then
Fail
end if
y ← S −1 (α)
A ← A \ {y}; B ← B ∪ {y};
else
β ← select(S (B \ M ))
if β = fail then
Fail
end if
y ← S −1 (β )
A ← A ∪ {y}; B ← B \ {y}
end if
e01 ← ∑a∈A a; e02 → ∑b∈B b
M ← M ∪ {y}
S → S [y 7→ −S ]
end while
return ∑a∈A φS0 ,S (a)♦ ∑b∈B φS0 ,S (b)

which variables have been moved on the left or right side. On entry it is trivially the empty set. The
arithmetic expressions e01 , e02 are the current approximations for the solution, and S records the ranges
for variables. On entry, those variables are set to the input parameters.
The Algorithm 2 iterates as long as at least one of the expressions e01 or e02 overflows — we use
Algorithm 1 to check it. It first selects the expression which is further away from zero — roughly, the
expression which causes the largest overflow. Then, it selects the addendum that contributes most to
the overflow, and moves it on the other side of ♦. This is reflected by the updates to A and B. The
memoization set M remembers which terms have already been moved. This forbids the same term to
be moved twice. Finally, S is updated to remember that y is negated. The algorithm fails if select fails,
that is if no more term can be moved to the other side of the relation. Otherwise, a new expression is
returned, where variables moved to one side or another of ♦ are negated.
Example 4 Let us consider the evaluation of the Boolean expression x1 + x2 ≤ x3 + x4 + x5 with
simplified 4 bits integers and with the semantic information:
S0 = S = {x1 ∈ [−1, 1], x2 ∈ [−2, 0], x3 ∈ [1, 2], x4 ∈ [2, 3], x5 ∈ [5, 6]}.
An overflow arises in the evaluation of the right hand side of the relation since:
x3 + x4 + x5 ∈ [8, 11] 6⊆ [−8, 7].

350

Automatic Repair of Overflowing Expressions with Abstract Interpretation

Let us apply Algorithm 2. At the first step, B = {x3 , x4 , x5 }, M = 0.
/ Therefore select(S (B \ M )) =
[5, 6] since d(x5 ) = 6. The memoization set is updated to M = {x5 } and the relation is transformed into
x1 + x2 + x5 ≤ x3 + x4 . We record the fact that x5 appears in a negated context by updating the semantic
information:
S = {x1 ∈ [−1, 1], x2 ∈ [−2, 0], x3 ∈ [1, 2], x4 ∈ [2, 3], x5 ∈ [−6, −5]}.
Now, x1 + x2 + x5 ∈ [−9, −4] 6⊆ [−8, 7]. Therefore, the evaluation of the left operand may lead to an
overflow, and so the loop is entered again. The function select(S (A \ M )) selects [−2, 0], that is the
interval corresponding to x2 . The new expression is x1 + x5 ≤ x3 + x4 + x2 , with
S = {x1 ∈ [−1, 1], x2 ∈ [0, −2], x3 ∈ [1, 2], x4 ∈ [2, 3], x5 ∈ [−6, −5]}.
The algorithm stops since the expression does not overflow. The expression x1 − x5 ≤ x3 + x4 − x2 is
then returned to the caller.
Property 3 For a relation between two linear expressions with O(n) variables, Algorithm 2 performs
O(n3 ) steps.
Proof Each variable is moved at most once from one side of the relation to the other. Then the while
loop of Line 2 is repeated O(n) times. The select function is O(n) but the Algorithm 1 is O(n2 ). The
global complexity is then O(n3 ).

6

Exploiting Relational Information

We extend the results of Sect. 4 by using Oct, the abstract domain of Octagons [12] as the underlying
semantic knowledge. Intuitively, having a more precise abstract domain enables the inference of more
relations among variables and as a consequence more arithmetic expressions can be repaired. On the
other hand, it also makes the search space for the problem larger. We show that there exists an algorithm
to solve RhI ,O,Octi exactly, i.e., if an expression can be repaired, then our algorithm finds it.
With Oct, constraints are either in the form a ≤ x ≤ b (non-relational constraints) or a ≤ x ± y ≤ b
(relational constraints). In the following we will use an interval notation to denote those constraints:
S (x) = [a, b] and S (x+y) = [a, b].
Example 5 Let us consider variables x, y, z of type M4 , the sum x+y+z, and the semantic information S :
{x ∈ [−2, 2], y ∈ [−1, 3], z ∈ [−1, 4], x+y ∈ [−2, 3], y+z ∈ [−2, 4], x+z ∈ [−1, 5]}.
If we ignore the relational constraints then we cannot propose a fix for the expression. In fact, Algorithm 1 will fail because:
[−2, 2] + [−1, 3] + [−1, 4] 6⊆ [−8, 7].
We assume the application of the same preprocessing steps of the previous sections (multiplications
by constants are expanded into sums, variables are only added – subtraction is captured in S ). Furthermore, for the sake of simplicity, we also assume that all the variables are different — variables with
multiple occurrences are renamed.
Our repairing algorithm performs a depth-first visit of a weighted directed graph G. Intuitively, the
graph indicates in which order we should add variables or pairs of variables for which we have some

F. Logozzo & M. Martel

351

0
[-2,2]

[-2,3]
[-1,3]

[-2,2]

{x,y}

[-1,4]

[-1,3]

{x}

[-1,5]

[-1,4]

[-1,5]

{y} [-2,4] {z}
[-1,4]
[-1,3]

[-2,2]

{y,z}

{x,z}

[-2,2]
[-2,4]

[-1,4]

[-1,3]

[-2,3]

{x,y,z}

Figure 3: Graph describing the ways of summing x, y, z with the information of Ex. 6.
relational information in S . We do not explicitly build the graph — it is of exponential size. Instead, we
memorize only the current path corresponding to a non overflowing partial sum. The nodes correspond
to partial sums of variables. The weight (an interval) attached to an edge e indicates the value which must
be added to the partial sum when one or two variables are added. In general, there exists several paths
from a source node to a destination node depending on which constraints we use to add the variables.
For instance, in Ex. 6, we have a path corresponding to x + (y + z) and another path corresponding to
(x + y) + z whose weights are [−4, 6] and [−3, 7], respectively.
Formally, given an input set of variables X = {x1 , . . . xn } and the semantic information S , we define
the graph G = (V, E) as follows:
• V = ℘(X): the nodes of G are sets of variables,
• the entry node is 0/ and the exit node is X,

• (v1 , v2 ) ∈ E if v2 = v1 ∪ {xi } for some v1 ⊆ X and some variable xi ∈ X. In this case, W (v1 , v2 ) =
S (xi ),
• (v1 , v2 ) ∈ E if v2 = v1 ∪{xi , x j } for some v1 ⊆ X and some pair of variables xi and x j , with i 6= j.
In this case, W (v1 , v2 ) = S (xi + x j ).
Example 6 Let us consider the arithmetic expression and the semantic information of the Ex. 6. The
Figure 3 shows the corresponding graph G. With G, we can derive the non-overflowing expressions
(x+y)+z or x+(y+z). The expression y+(x+z) is not a repair – it may overflow under the knowledge
encoded by S .
−
Let v1 , . . . vk be a sequence of vertices in G. Then, →
v = (v1 , . . . vk ) is a path if v1 = 0/ and for all i
→
−
−
0
such that 1 ≤ i < k, (vi , vi+1 ) ∈ E; v y v is the path extended with vertex v0 ; dest(→
v ) = vk is the last
→
−
−
vertex in a non-empty path; succ(v) are the successors of vertex v, succ( v ) = succ(dest(→
v )), are the
k

successors of a (non-empty) path.
The function Repair, Algorithm 3, performs a depth-first search in G. The input to Repair is path
→
−
−
−
v in G. Intuitively, →
v describes a way of summing the variables in vk . The weight of W (→
v ) is the

352

Automatic Repair of Overflowing Expressions with Abstract Interpretation

Algorithm 3 Sum Refactoring with Relational Information
−
Require: A path →
v on G and an octagon S
Ensure: A path indicating how to compute the total sum without overflows, or fail if it does not exists
→
−
1: Function Repair( v )
→
− →
−
→
−
2: N ← succ( v ); r ← v
→
−
3: while N 6= 0/ ∧ dest( r ) 6= X do
4:
5:
6:
7:
8:
9:
10:
11:
12:
13:
14:

v0 ← pickOne(N )
−
if S |=notOverflow ∑v∈→
v yv0 x then
→
−r ← Repair(→
−
v y v0 )
end if
N ← N \ {v0 }
end while
−r ) = X then
if dest(→
−r
return →
else
Fail
end if

unbounded interval sum of the weights of the edges:
−
W (→
x)=

k−1

∑W


(v j , v j+1 ) .

j=1

Algorithm 3 visits G without explicitly building it. The set N is initialized to the set of successor
nodes of the current path. The algorithm iterates until N is empty (in which case the algorithm fails) or
the exit node X is reached (in which case the algorithm succeeds). In the main loop, a new node from the
unexplored successors N is picked
to return
 via the function pickOne. Heuristically, we want pickOne
−
the node v0 minimizing W (xn , x0 ) . If the new partial sum corresponding to the path →
v y v0 does not
overflow, then the exploration continues from such a path. Otherwise, the exploration continues with
another successor in N .
Example 7 Let us apply Algorithm 3 to Ex. 6. The initial value for Repair is 0,
/ i.e. the path
corresponding to the entry node. We have

N = {x}, {y}, {z}, {x,y}, {x,z}, {y,z} .
The function pickOne selects {x} since d((0,
/ {x})) = 2 is minimal. Therefore, it invokes Repair on the
path (0,
/ {x}). It choses {x, y} as successor. At the next recursive call, when it adds z to the path, it
detects an overflow since
[−2, 2] + [−1, 3] + [−1, 4] 6⊆ [−8, 7].
The algorithm backtracks and finds the path
(0,
/ {x}, {x, y, z})
whose weight is [−2, 2] + [−2, 4] ⊆ [−8, 7].
Property 4 (Completeness) Algorithm 3 is complete.

F. Logozzo & M. Martel

353

Proof Algorithm 3 performs a search into a graph G which describes all the ways of summing the
variables of the expression. Then, if a solution exists, it is included in G and the algorithm necessarily
finds it.
The Algorithm 3 can be generalized to any template-based numerical abstract domain [18]. In this
case, we have additional constraints of form
a ≤ a1 · x1 + . . . + an · xn ≤ b

(6)

where the xi , 1 ≤ i ≤ n are variables of the program and where a, b and the coefficients ai , 1 ≤ i ≤ n are
(1)
(2)
(a )
constants. The preprocessing transforms each term ai · xi into xi + xi + . . . + xi i and the graph used
by Algorithm 3 can be extended with new edges (v1 , v2 ) such that
!
v2 = v1 ∪

[

[

1≤i≤n

1≤ j≤ai

( j)

xi

for some v1 ⊆ X and for the constraint of Equation (6). In this case, the weight associated to the new
edge (v1 , v2 ) is S (x1 + . . . + an · xn ).

7

Experimental Results

We have a prototype OCAML implementation that we used to validate and to experiment with the algorithms presented in the previous sections. We use 32 bits signed integers, i.e., M32 ∈ [−231 , 231 − 1].
For the algorithms 1 and 2, we use the variables x1 , . . . , x6 with
S = {x1 ∈ [0, 229 ], x2 ∈ [−229 , 0], x3 ∈ [−229 , 229 ], x4 ∈ [1, 1], x5 ∈ [−1, −1], x6 ∈ [−1, 1]}.
There is nothing special about S , we generated it randomly.
To evaluate Algorithm 1, we consider all the expressions in the form of e = ∑6i=1 ai · xi and ai ∈
{0, 1, 2, 4} for 1 ≤ i ≤ 6. Overall, there are 3402 of such expressions. Under S , 1093 expressions do not
overflow, 2268 cannot be repaired, and 43 can be repaired.
Algorithm 1 proves it in a very little time: The overall time to analyze, suggest a repair or prove that
such repair does not exists is of 120ms. We report some of the repairs discovered by the algorithm in
Fig. 4.
In order to evaluate Algorithm 2, we consider all the inequalities in the form of ∑5i=1 ai ·xi < ∑5i=1 ai ·xi
such that:
(i) ai ∈ {0, 1, 2, 4}, for 1 ≤ i ≤ 5,
(ii) a given variable xi appears at most in one side of the equation,
(iii) each side of the equation owns at least one term with coefficient ai 6= 0.
There exist 7290 of such expressions, and only 213 are not repaired by Algorithm 2. The overall
time to explore all such expressions and to suggest a repair, if any, is of 202ms. Example of repairs are
in Figure 4.
To evaluate Algorithm 3, we add to S the relational information:
S (x1 + x3 ) = S (x1 + x2 ) = [−229 , 229 ].
With this information, we can repair some more expressions than with Algorithm 1 — with a negligible
additional cost. Such cases are in Fig. 4.
Overall, in our randomly generated tests, the Algorithms seem to perform extremely well.

354

Automatic Repair of Overflowing Expressions with Abstract Interpretation

Algorithm 1
2 · x1 + 2 · x3 + 2 · x5 + x6 −→ 2 · x5 + 2 · x1 + x6 + 2 · x3
2 · x1 + 2 · x3 + x4 + 2 · x5 −→ 2 · +x5 + x4 + 2 · x1 + 2 · x3
4 · x1 + 2 · x2 + x4 + 2 · x5 −→ 2 · +x5 + x4 + 2 · x2 + 4 · x1
4 · x1 + 2 · x2 + x4 + 4 · x5 + x6 −→ 4 · x5 + x4 + 2 · x2 + 4 · x1 + x6
4 · x1 + 2 · x2 + 2 · x4 + 4 · x5 −→ 4 · x5 + 2 · x4 + 2 · x2 + 4 · x1
2 · x1 + x2 + 2 · x3 + 2 · x4 + 4 · x5 + x6 −→ 4 · x5 + 2 · x4 + x2 + 2 · x1 + x6 + 2 · x3
Algorithm 2
x4 + x5 < 4 · x1 + 4 · x2 + 4 · x3 −→ 4 · x3 + 4 · x1 + x4 + x5 < 4 · x2
4 · x3 + 4 · x5 < 4 · x1 + 4 · x2 + 4 · x4 −→ 3 · x3 + 4 · x5 < x3 + 4 · x1 + 4 · x2 + 4 · x4
2 · x3 + 4 · x5 < 4 · x1 + 2 · x2 + 4 · x4 −→ x1 + 3 · x4 + 2 · x3 + 4 · x5 < 3 · x1 + 2 · x2
x4 < 4 · x1 + x2 + 2 · x3 + 4 · x5 −→ 2 · x3 + x2 + x4 < 4 · x5 + 4 · x1
2 · x1 + 4 · x3 + x4 < 4 · x2 + 4 · x5 −→ 3 · x3 < 2 · x1 + x4 + x3 + 4 · x2 + 4 · x5
4 · x2 + 2 · x4 + x5 < x1 + 4 · x3 −→ x3 + x1 + 4 · x2 + 2 · x4 + x5 < 3 · x3
Algorithm 3
2 · x2 + 2 · x3 + x6 −→ x6 + (x2 + x3 ) + x3 + x2
2 · x1 + 2 · x3 + x5 + x6 −→ x5 + x6 + x3 + (x1 + x3 ) + x1
2 · x1 + 2 · x2 + 2 · x3 + x4 + x5 −→ x4 + x5 + x2 + (x1 + x3 ) + x3 + x1 + x2
Figure 4: Some of the repairs produced by the implementation of our algorithms. For Algorithm 3, more
repairs are enabled because of a more refined semantic knowledge.

8

Related Work

The dynamic analysis community has been interested for a while to the problem of repairing faulty
programs, i.e. programs failing some test cases [16]. Their approaches can be abstracted as follows.
When a bug is found in a program P, a modified program P’ is generated such that P’ behaves as P on
a certain set of tests but it does not manifest the bug. The repaired program P’ is generated searching
a program in the set of program transformations/mutations of P –e.g., applying a set of templates [15,
21, 7, 17]. This approach has many drawbacks. First, it requires running the program, first to find the
bug in P and then to generate and check the candidates for P’. This may not be practical because the
test suite can be very large – in real software up to several hours. As a consequence the search for P’
is de facto impossible for a large P. Second, the whole program may not be available – this is the case
for instance when developing libraries. Third, the repair is as good as the test suite itself: e.g., how can
we be sure that an arithmetic overflow has been removed for all the possible inputs and not just for the
particular test case? Fourth, the generated repairs are often counter-intuitive, and not realistic, in that
they perturb the semantics of the original program in the “good” runs [20]. We differentiate from those
approaches because our approach is completely static, it exploits the semantic information inferred by
the static analyzer, and the repair is guaranteed to only improve the good executions, while removing
overflows (“bad” executions).
Orthogonally, a recent paper from Coker and Hafiz [2], introduces a set of refactorings to fix overflows in C programs to be applied in a IDE. However, unlike us, they do not propose any way to auto-

F. Logozzo & M. Martel

355

matically generate such fixes.
The bases for our paper are [8] and [10, 11]. In [8] we introduced the concept of verified repair,
the idea is that one can generate a program repair from the semantic information inferred by the static
analyzer, and verify that it improves the program by removing bad behaviors while increasing good
ones, up to some level of abstraction. We proposed some fixes for common bugs, including a greedy
incomplete algorithm to fix overflowing expressions. Here we improve over such an algorithm, by first
making clear the concept of input and output language, and that of the underlying semantic information
used to repair the overflowing expression. Furthermore, in the present paper we present three algorithms
for repairing expressions in common cases, and we formally study their properties (complexity and
completeness). In [10, 11] we considered the problem of generating (an approximation of) the most
precise arithmetic expression over floating-point values [14]. The problem of improving a floating-point
expression presents a slightly different challenge than the one considered here in that, in general, the
expressions cannot be entirely repaired. Because the floating-point arithmetic introduces roundoff errors,
it is in general impossible to find an equivalent expression which computes the exact result, i.e., the result
that we would obtain with real numbers. A verified repair then is an expression which is equivalent to
the original one when interpreted over the real numbers and which is more accurate than the original
expression in the sense that it returns a value closer to the mathematical result when evaluated with
floating-point numbers.

9

Conclusions

It is our firm belief that we need to bring static analysis tools to the next level, to make them more
practical. They should not limit themselves to find (or prove the absence of) bugs, but they should
actively help the programmers by providing suggestions to improve their program, by removing the bug
or by proposing better design choices.
In this paper, we considered the particular yet relevant problem of repairing integer expressions starting from the warnings and the invariants inferred by an abstract interpretation-based static analyzer. We
characterized the three elements in the problem: (i) the input language for expressions (“which expression should I repair?”); (ii) the output language for the expressions (“how am I allowed to repair an
expression?”); and (iii) the semantic information (“what do I know about the values of the expression?”).
Then we focused our attention on three common cases, the repairing of: (i) linear expressions with intervals; (ii) Boolean expressions containing linear ones with intervals; and (iii) linear expressions with
templates. We showed that in the first case, quite surprisingly, there exists a complete polynomial algorithm to solve the problem, whereas in the second we have a polynomial yet incomplete one, and in the
third we have a complete but worst-case exponential one.

References
[1] Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David
Monniaux & Xavier Rival (2003): A static analyzer for large safety-critical software. In Ron Cytron & Rajiv
Gupta, editors: PLDI, ACM, pp. 196–207. Available at http://doi.acm.org/10.1145/781131.781153.
[2] Zack Coker & Munawar Hafiz (2013): Program transformations to fix C integers. In David Notkin, Betty
H. C. Cheng & Klaus Pohl, editors: ICSE, IEEE / ACM, pp. 792–801. Available at http://dl.acm.org/
citation.cfm?id=2486892.

356

Automatic Repair of Overflowing Expressions with Abstract Interpretation

[3] Patrick Cousot & Radhia Cousot (1977): Abstract Interpretation: A Unified Lattice Model for Static Analysis
of Programs by Construction or Approximation of Fixpoints. In Robert M. Graham, Michael A. Harrison
& Ravi Sethi, editors: POPL, ACM, pp. 238–252. Available at http://doi.acm.org/10.1145/512950.
512973.
[4] Manuel Fähndrich, Michael Barnett & Francesco Logozzo (2010): Embedded contract languages. In Sung Y.
Shin, Sascha Ossowski, Michael Schumacher, Mathew J. Palakal & Chih-Cheng Hung, editors: SAC, ACM,
pp. 2103–2110. Available at http://doi.acm.org/10.1145/1774088.1774531.
[5] Manuel Fähndrich & Francesco Logozzo (2010): Static Contract Checking with Abstract Interpretation. In
Bernhard Beckert & Claude Marché, editors: FoVeOOS, Lecture Notes in Computer Science 6528, Springer,
pp. 10–30. Available at http://dx.doi.org/10.1007/978-3-642-18070-5_2.
[6] Martin Glinz, Gail C. Murphy & Mauro Pezzè, editors (2012): 34th International Conference on Software
Engineering, ICSE 2012, June 2-9, 2012, Zurich, Switzerland. IEEE. Available at http://ieeexplore.
ieee.org/xpl/mostRecentIssue.jsp?punumber=6218989.
[7] Claire Le Goues, Michael Dewey-Vogt, Stephanie Forrest & Westley Weimer (2012): A systematic study of
automated program repair: Fixing 55 out of 105 bugs for $8 each. In Glinz et al. [6], pp. 3–13. Available at
http://dx.doi.org/10.1109/ICSE.2012.6227211.
[8] Francesco Logozzo & Thomas Ball (2012): Modular and verified automatic program repair. In Gary T.
Leavens & Matthew B. Dwyer, editors: OOPSLA, ACM, pp. 133–146. Available at http://doi.acm.
org/10.1145/2384616.2384626.
[9] Francesco Logozzo & Manuel Fähndrich (2008): Pentagons: a weakly relational abstract domain for the
efficient validation of array accesses. In Roger L. Wainwright & Hisham Haddad, editors: SAC, ACM, pp.
184–188. Available at http://doi.acm.org/10.1145/1363686.1363736.
[10] Matthieu Martel (2007): Semantics-Based Transformation of Arithmetic Expressions. In Hanne Riis Nielson
& Gilberto Filé, editors: SAS, Lecture Notes in Computer Science 4634, Springer, pp. 298–314. Available
at http://dx.doi.org/10.1007/978-3-540-74061-2_19.
[11] Matthieu Martel (2009): Program transformation for numerical precision. In Germán Puebla & Germán Vidal, editors: PEPM, ACM, pp. 101–110. Available at http://doi.acm.org/10.1145/1480945.1480960.
[12] Antoine Miné (2006): The octagon abstract domain. Higher-Order and Symbolic Computation 19(1), pp.
31–100. Available at http://dx.doi.org/10.1007/s10990-006-8609-1.
[13] Ramon E. Moore, R. Baker Kearfott & Michael J. Cloud (2009): Introduction to Interval Analysis. SIAM,
doi:10.1137/1.9780898717716.
[14] Jean-Michel Muller, Nicolas Brisebarre, Florent de Dinechin, Claude-Pierre Jeannerod, Vincent Lefèvre,
Guillaume Melquiond, Nathalie Revol, Damien Stehlé & Serge Torres (2010): Handbook of Floating-Point
Arithmetic. Birkhäuser. Available at http://dx.doi.org/10.1007/978-0-8176-4705-6.
[15] Jeff H. Perkins, Sunghun Kim, Samuel Larsen, Saman P. Amarasinghe, Jonathan Bachrach, Michael Carbin,
Carlos Pacheco, Frank Sherwood, Stelios Sidiroglou, Greg Sullivan, Weng-Fai Wong, Yoav Zibin, Michael D.
Ernst & Martin C. Rinard (2009): Automatically patching errors in deployed software. In Jeanna Neefe
Matthews & Thomas E. Anderson, editors: SOSP, ACM, pp. 87–102. Available at http://doi.acm.org/
10.1145/1629575.1629585.
[16] Mauro Pezzè, Martin C. Rinard, Westley Weimer & Andreas Zeller (2011): Self-Repairing Programs
(Dagstuhl Seminar 11062). Dagstuhl Reports 1(2), pp. 16–29. Available at http://dx.doi.org/10.
4230/DagRep.1.2.16.
[17] Hesam Samimi, Max Schäfer, Shay Artzi, Todd D. Millstein, Frank Tip & Laurie J. Hendren (2012): Automated repair of HTML generation errors in PHP applications using string constraint solving. In Glinz et al.
[6], pp. 277–287. Available at http://dx.doi.org/10.1109/ICSE.2012.6227186.
[18] Sriram Sankaranarayanan, Henny B. Sipma & Zohar Manna (2005): Scalable Analysis of Linear Systems
Using Mathematical Programming. In Radhia Cousot, editor: VMCAI, Lecture Notes in Computer Science
3385, Springer, pp. 25–41. Available at http://dx.doi.org/10.1007/978-3-540-30579-8_2.

F. Logozzo & M. Martel

357

[19] David A. Schmidt (2009): Abstract Interpretation From a Denotational-semantics Perspective. Electr. Notes
Theor. Comput. Sci. 249, pp. 19–37, doi:10.1007/978-3-642-04164-8-14.
[20] Yi Wei, Yu Pei, Carlo A. Furia, Lucas Serpa Silva, Stefan Buchholz, Bertrand Meyer & Andreas Zeller
(2010): Automated fixing of programs with contracts. In Paolo Tonella & Alessandro Orso, editors: ISSTA,
ACM, pp. 61–72. Available at http://doi.acm.org/10.1145/1831708.1831716.
[21] Westley Weimer, ThanhVu Nguyen, Claire Le Goues & Stephanie Forrest (2009): Automatically finding
patches using genetic programming. In: ICSE, IEEE, pp. 364–374. Available at http://dx.doi.org/10.
1109/ICSE.2009.5070536.

