Abstract Interpretation of Binary Code with
Memory Accesses using Polyhedra

arXiv:1711.07257v1 [cs.PL] 20 Nov 2017

Clément Ballabriga and Julien Forget and Giuseppe Lipari
University of Lille, CNRS, Centrale Lille, UMR 9189 – CRIStAL
{name.surname}@univ-lille1.fr

Abstract. In this paper1 we propose a novel methodology for static
analysis of binary code using abstract interpretation. We use an abstract
domain based on polyhedra and two mapping functions that associate
polyhedra variables with registers and memory.
We demonstrate our methodology to the problem of computing upper
bounds to loop iterations in the code. This problem is particularly important in the domain of Worst-Case Execution Time (WCET) analysis
of safety-critical real-time code. However, our approach is general and it
can applied to other static analysis problems.

1

Introduction

In real-time systems it is important to compute upper bounds to the execution
times of every function, and check that they complete before their deadlines
under all possible conditions. Worst-Case Execution Time (WCET) analysis
consists in computing (an upper bound to) the longest path in the code. WCET
analysis is usually performed on the binary code, because it needs information
on the low-level instructions executed by the hardware processor in order to
compute the execution time.
In this paper, we propose a static analysis of binary code based on abstract
interpretation using polyhedra. Our motivation is the need to enhance existing
WCET analysis by improving the computation of upper bounds on the number
of iterations in loops, and by detecting unfeasible paths.
Most analyses by abstract interpretation proposed in the literature are performed on source code. However, there are several important advantages in performing static analysis of binary code: 1) we analyze the code that actually runs
on the machine, hence no need for additional assumptions on how the compiler
works; 2) by gaining access to the memory layout, we can precisely identify
problems with pointers (alias, buffer overflows, etc.) that are not easily identified when working only on source code; 3) We can perform the analysis even
without access to the source code.
1

An earlier version of this paper has been submitted to TACAS 2018
(http://www.etaps.org/index.php/2018/tacas) for peer-review. Compared to the
submitted paper, this version contains more up-to-date benchmarks in Section 6.

To the best of our knowledge, no other work has tackled the problem of static
analysis of binary code using abstract interpretation with polyhedra. The main
reason is probably the difficulty in representing the state of the program.
In fact, binary code lacks important structural information: the type of variables, their structure and relations, their scope and lifetime, etc. More specifically, in most of the existing abstract interpretation papers in the literature,
the abstract state of a program is represented by constraints on the program
variables. The underlying assumption is that variables are well identified and in
a relatively small number. In the binary code, the notion of program variable is
lost, so we can only analyse processor registers and memory locations. Unfortunately, a representation of the abstract state that includes all registers and all
possible memory locations is too large to be managed easily in the analysis.
Contributions of this paper. A key observation is that the number of memory
locations that are effectively used in the binary code approximately corresponds
to the number of program variables in the source code (at least, it is of the
same order of magnitude). Based on this observation, in this paper we propose
to identify the subset of registers and memory locations to be represented in the
abstract state as the analysis progresses.
To this end, we propose an abstract domain consisting of 1) a polyhedron, to
represent the linear constraints on the polyhedra variables; 2) a register mapping that maps register names to polyhedra variables; 3) a memory mapping
that maps addresses and their values to the respective polyhedra variables. The
abstract state is constructed and modified as the analysis progresses: in particular, new variables and constraints may be added to the polyhedra as new
memory locations are discovered in the code, and the two mappings are modified
accordingly. We must check that our abstract representation remains consistent
at all stages, for example when joining the states from two different paths in the
code. To do this, we carefully consider aliasing (or equivalence) between variables. We formally prove that the operations that manipulate the abstract state
are semantically consistent with the abstract interpretation framework.
We present the application of this method to the problem of computing upper
bounds to loop iterations. Finally, we evaluate the performance of our method
on benchmarks and we compare with existing static analysis tools to evaluate
the precision of our approach.

2

Related works

Many papers on static analysis are based on abstract interpretation. Approaches
vary widely depending on the abstract domain, the type of target programs
(source or binary code, language, application type, etc.), and the analysis goal
(i.e. the kind of information we want to discover). Here we attempt to summarise
the papers that are the most closely related to our research.
Abstract interpretation using polyhedra has been first described in [1]. It has
been used extensively in the context of compilers. For instance, the PAGAI [2]

analyzer processes LLVM Intermediate Representation (IR) using various abstract domains (including polyhedra) to detect several properties (such as loop
invariants). Compared to our approach, LLVM IR is closer to the source code,
as it contains information on variables and their types.
An important problem when dealing with binary code analysis is to figure
out the set of interesting data locations used by the program. This is related
to pointer analysis (the so-called aliasing problem), and has been extensively
studied [3,4]. While the majority of pointer analyses have been proposed in the
context of compiler optimizations, a certain number of ideas can be borrowed
and applied to binary code analysis.
An example of binary code analysis by abstract interpretation is described
in [5] and later improved in [6]. Compared to our approach, this method uses
a different abstract domain (interval analysis with congruence, and affine relations [7]). Furthermore, the set of abstract memory locations are computed
by a preprocessing analysis using IDA Pro [8]: in contrast, we determine them
dynamically during the analysis.
In this paper, our approach is applied to static loop bound estimation, in the
context of WCET analysis, so we compare our results with other loop bound
estimation tools. The oRange tool [9] is based on an abstract interpretation
method defined in [10]. It provides a very fast estimation of loop bounds, but
it is restricted to C source code. SWEET [11] features a loop bound estimator,
which works on an intermediary representation (ALF format). The approach is
based on slicing and abstract interpretation and it generally provides very tight
loop bounds even in complex cases, but the running time of the analysis appears
to depend on the loop bounds, and in our experience for large loop bounds the
analysis did not terminate.
Compared to these existing works, our approach combines the polyhedral
domain with binary code analysis, taking into account memory accesses; our
method is sound and always terminates.

3

Abstract domain

Abstract interpretation [12] is a static program analysis that provides a sound
approximation of the semantics of the analyzed program. Instead of computing
exact concrete program states (e.g. data valuation), abstract interpretation computes approximate abstract program states (e.g. inequalities on data valuation).
The set of abstract states is called the abstract domain. Our analysis is based on
the polyhedral abstract domain, to which we add information to track relations
between polyhedra variables and registers or memory locations.
3.1

Polyhedra

A polyhedron P denotes a set of points in a Z vector space bounded by linear
constraints (equalities or inequalities). More formally, let Cn be the set of linear
constraints in Zn . Then h{c1 , c2 , ..., cm }i (with ci ∈ Cn for 1 ≤ i ≤ m) denotes

the polyhedron consisting of all the vectors in ZN that satisfy constraints c1 , c2 ,
. . . cm . In our work, we only consider non-strict inequalities and equalities.
Like any other abstract domain, the polyhedral domain is equipped with
operations that form a lattice [13]. We present these operations below, along with
some other classic polyhedra operations [13] that we will use in the following.
Let p, p′ be two polyhedra:
– We denote p ⊆ p′ iff ∀s ∈ p, s ∈ p′ . This is the partial order of the lattice;
– We denote p′′ = p ∪ p′ the smallest polyhedron such that p ⊆ p′′ and p′ ⊆ p′′ .
This operation is the convex hull. It is the least upper bound of the lattice;
– We denote p′′ = p ∩ p′ the intersection of p and p′ (i.e. the union of the
constraints of p and p′ ). It is the greatest lower bound of the lattice;
– The bottom state ⊥ of the lattice is the empty polyhedron (the set of constraints has no solution2 ) and the top state ⊤ is the polyhedron containing
all points (the set of constraints is empty);
– We let vars(p) denote the set of variables appearing in the constraints of p;
– Let |S| denote the cardinality of set S. We let proj(p, x1 . . . xk ) denote the
projection of polyhedron p on space x1 . . . xk , with k < |vars(p)| (this effectively removes other variables from the polyhedron constraints);
– We denote max(p, x) the greatest value of x satisfying the constraints of p.
3.2

Registers and memory

In polyhedral analysis of source code, variables of the polyhedra are related
to variables of the source code. In our case, polyhedra variables are related to
registers and memory locations. An abstract state is defined as a triple (p, m, ∗),
where p is a polyhedron, m is a register mapping and ∗ is an address mapping.
In the rest of the paper, the term variable refers to polyhedron variables.
Let us first consider registers. Let r be a register, v be a variable of vars(p)
and m be a register mapping. Then we have m(r) = v iff v represents the value
of r in p. We denote varsR (p) the image of mapping m. We denote m[r : v] the
mapping m′ such that m′ (r) = v and for every register r′ 6= r, m′ (r′ ) = m(r′ ).
In other words, m[r : v] denotes a single mapping substitution.
Let us now consider memory locations. We want to keep track in our abstract state of the fact that, say variable x0 represents a memory address, and
the value at this address is represented by variable x1 . To to this, we introduce
two more subsets varsA (p) and varsC (p) of vars(p). Variables in varsA (p) define memory addresses, while variables in varsC (p) define memory values. The
subsets varsR (p), varsA (p) and varsC (p) are disjoint, so we can distinguish between variables corresponding to memory values, memory addresses, registers or
other. ∗ is a partial bijection (some addresses may have no corresponding values)
from varsA (p) to varsC (p), such that ∗(x1 ) = x2 iff x2 represents the value at
the memory address represented by x1 . The substitution ∗[x1 : x2 ] is defined
similarly to m[r : v].
2

Checking emptiness of a polyhedron over Z is a complex operation. Therefore, in
practice we approximate it by checking emptiness over the rationals.

3.3

Aliasing

In a general sense, aliasing occurs in a program when a data location can be
accessed through several symbolic names. In our context, we define an aliasing
relation between two variables x1 and x2 of a polyhedron p as follows:
– Must alias or equivalent : the constraint x1 = x2 is true for every point in p.
This is also denoted x1 ≡ x2 . This holds iff h{x1 = x2 }i) ⊆ p;
– May alias or overlapping: the constraint x1 = x2 is true for at least one point
in p. This holds iff h{x1 = x2 }i) ∩ p 6= ∅;
– Cannot alias or independent : the constraint x1 = x2 is false for every point
in p. This holds iff h{x1 = x2 }i) ∩ p = ∅.
The aliasing relation between a register r and a variable x is defined by the
aliasing relation between m(r) and x. Similarly, the aliasing relation between
two registers r1 , r2 is defined by the aliasing relation between m(r1 ) and m(r2 ).
As we will see in the following sections, while progressing in the analysis, it
may happen that our algorithm generates equivalent variables to represent the
same memory location. The presence of aliasing complicates the analysis, so we
make sure that each memory location is represented by one single variable.
Definition 1. Let s = (p, m, ∗) be an abstract state. We say that s is a consistent state iff:
∀distinct x1 , x2 ∈ varsA (p), x1 6≡ x2
In a consistent state, each data location is defined by a single variable. Indeed,
each register is defined by a single variable because mapping m is a function. The
same is true for values contained in memory locations because ∗ is a function
and because the state is consistent.
To preserve the consistency of abstract states, if at some point in the analysis we detect equivalent address variables, we merge the variables and their
constraints. Let x1 , x2 be two distinct variables of varsA (p) such that x1 ≡ x2 .
We merge x1 and x2 as follows:
M erge((p, m, ∗), x1 , x2 ) = (p1 ∪ p2 , m, ∗′ )
p1 = p where ∗(x2 ) is replaced by v2
p2 = p where ∗(x1 ) is replaced by v1 , x2 by x1 , and ∗(x2 ) by ∗(x1 )
∗′ = ∗[x2 : v3 ]
v1 = newF V (), v2 = newF V (), v3 = newF V ()
Let us describe the operation in detail. We first transform p into two different
polyhedra p1 and p2 . Polyhedron p1 is the same as p, except that we eliminate
the constraints on ∗(x2 ): this is done by replacing ∗(x2 ) with a new variable v2
in all constraints. Polyhedron p2 is the same as p, except that: 1) we remove the
constraints on ∗(x1 ); 2) we rename x2 as x1 and ∗(x2 ) as ∗(x1 ) in all constraints.
The polyhedron resulting from the merge is the convex-hull of p1 and p2 . Also,
x2 is not needed anymore, so we can change its ∗ mapping to a new variable v3 .

Equivalent address variables are merged whenever adding a new constraint,
using the following unification function:
(
M erge((p, m, ∗), x1 , x2 ) if ∃x1 , x2 ∈ varsA (p), x1 ≡ x2
U nif y(p, m, ∗) =
(p, m, ∗)
otherwise.

4

Computing abstract states

A program is represented by a graph G =< I, E >. The set of nodes I is the set
of instructions of the program. A directed edge (b1 , b2 ) ∈ E (where E ⊆ I × I),
represents a valid succession of two basic instructions in the program execution.
We say that a node bi ∈ I is a predecessor of bj , and denote bi → bj , iff
(bi , bj ) ∈ E. We say that bi dominates bj , and denote bi ≫ bj , iff all paths from
the entry node to bj go through bi . We say that node h is a loop header if it has
at least one predecessor bi such that h ≫ bi . We denote lh the loop associated
to header h. An edge (bi , h) such that h ≫ bi is called a back-edge of loop lh ;
any other edge entering the loop header h is an entry-edge.
We now describe our model of the processor architecture. We assume that
all data locations have the same size and that memory accesses are aligned to
the word size. We also assume that function calls are inlined. We consider a
simplified instruction set made up of the following instructions3 . Let r1 , r2 , r3
be registers and c be an integer constant:
– OP r1 r2 r3: stores the result of operation OP (r2 , r3 ) in register r1 , where
OP denotes an arbitrary binary arithmetic or logic operation;
– BOP r1 r2: branches to the address contained in r1 if condition OP (r2 ) is
true, where OP denotes an arbitrary unary logic operation;
– LOADI r1 c: loads constant c in register r1 ;
– LOAD r1 r2: loads the value contained in the address designated by r2 in
register r1 ;
– STORE r1 r2: stores the value of register r2 at the address designated by r1 .
The abstract interpretation of a program consists in computing an abstract
state for each edge of the program. For each node of the program, the analyses
computes the state of the output edge(s) based on the state of the input edge(s).
The state for the entry edge of the program is (⊤, ∅, ∅). The operations involved
in the computation of abstract states are:
– U pdate: this is a monotonic function. It takes an instruction, the abstract
state before the instruction, and returns the abstract state after it;
– Join: when an instruction has several input edges (due to branching) and is
not a loop header, its input state is computed by the Join operation;
– ∇: when an instruction is a loop header, its input state is computed by the
widening operation ∇.
3

Though this instruction set is very small, the principles of our analysis can be easily
extended to support a richer set of instructions.

These operations are applied repeatedly on G until a fixpoint is reached.
Since the polyhedral domain admits infinite ascending chains, specific mechanisms are used to enforce the convergence to a fixpoint: this is ensured by the
widening operation. A widening operation for the polyhedral domain has first
been proposed in [14], and further improved in [15,16]. In our work, we use the
widening operator of [15].
Finally, function newF V () returns a new fresh variable that has never been
used at any other point during the analysis. It is very important that the variable
is fresh globally (for the whole analysis) and not only locally (for the current
state), so as to avoid using the same variable in two different states for representing unrelated constraints.
Figure 1 reports an example that will be used in the rest of the section to
illustrate the operations on the abstract states.

1:
2:
3:
4:
5:

6:
7:
8:
9:

LOADI R1 4
LOADI R2 5
LOADI R3 1000
LOADI R4 9
STORE R3 R1

EQ R5 R1 R2
BNZ R4 R5
STORE R3 R2
LOAD R6 R3

# R5←R1==R2
# Branch to 9 if R56=0

Edge
(L6, L7)

P olyhedron
Registers
M emory
p1 = h{x1 = 4, x2 = 5, x3 = 1000,
m1 = {R1 : x1 , ∗1 = {x5 : x6 }
x4 = 9, x5 = x3 , x6 = x1 ,
R2 : x2 , R3 : x3 ,
x7 = (x1 − x2 )i}
R4 : x4 , R5 : x7 }
e = (L8, L9)
p1 ∩ h{x7 = 0, x8 = x2 }i
m1
∗1 [x5 : x8 ]
e′ = (L7, L9)
p1
m1
∗1
join(e, e′ ) p3 = (p1 ∩ h{x7 = 0, x6 = x2 }i) ∪ p1 =
m1
∗2 = {x5 : x6 }
h{x1 = 4, . . . , x1 ≤ x6 ≤ x2 }i
(L9, exit)
p3 ∩ h{x10 = x6 }i
m1 [R6 : x10 ]
∗2
Fig. 1. Example of analysis

4.1

Binary operation

We distinguish two possible cases. In the first case, the relation r1 = OP (r2 , r3 )
is linear and the U pdate function can be defined as follows:
U pdate(OP r1 r2 r3 , (p, m, ∗)) = (p′ , m′ , ∗)
p′ = p ∩ h{xi = OP (m(r2 ), m(r3 ))}i
m′ = m[r1 : xi ]

xi = newF V ()

For instance, in Figure 1 Line 6 introduces the constraint x7 = (x1 − x2 ) (the
equality test expressed as a linear constraint) and m1 (R5 ) = x7 .

If no linear relation can be determined, we assume that r1 can contain any
value after the update. In that case, the U pdate function is defined as follows:
U pdate′ (OP r1 r2 r3 , (p, m, ∗)) = (p, m′ , ∗)
m′ = m[r1 : newF V ()]
4.2

Branching

Branching instructions have two out-edges, to which different abstract states
can be associated. We use filtering to represent the impact of the condition
on the abstract state. It is applied only if the branching condition is a linear
constraint, otherwise the branching condition is ignored. Let taken denote the
edge corresponding to the case where the branch condition is true, and not taken
denote the other edge. The abstract states for these edges are computed as:
U pdatetaken (BOP r1 r2 , (p, m, ∗) = (p′ , m, ∗)
p′ = p ∩ h{BOP (m(r2 ))}i
U pdatenot taken (BOP r1 r2 , (p, m, ∗) = (p′ , m, ∗)
p′ = p ∩ h{¬BOP (m(r2 ))}i
For instance, in Figure 1 we add the constraint x7 = 0 on edge (L7, L8) (appearing also on edge (L8, L9)). The constraint x7 6= 0 cannot be expressed as a
linear constraint, so it is not added on edge (L7, L9).
4.3

Load

The impact of the immediate load instruction is straightforward:
U pdate(LOADI r1 c, (p, m, ∗)) = (p′ , m′ , ∗)
p′ = p ∩ h{xi = c}i m′ = m[r1 : xi ] xi = newF V ()
Let us now consider the non-immediate load instruction. If the input state
contains a memory address variable that is equivalent to the load address, then in
the output state the value of the destination register is the value of the memory
value mapped to this address:
U pdate(LOAD r1 r2 , (p, m, ∗)) = (p′ , m′ , ∗)
p′ = p ∩ h{xi = ∗(a)}i m′ = m[r1 : xi ]
a ≡ r2
xi = newF V ()
Otherwise, the destination register value is undefined:
U pdate(LOAD r1 r2 , (p, m)) = (p, m′ )
m′ = m[r1 : newF V ()]
For instance, in Figure 1 Line 9 we have x5 ≡ r3 and ∗(x5 ) = x6 , so we
introduce the constraint x10 = x6 and m′ [R6 = x10 ].

4.4

Store

Again, we need to consider the impact of aliases. First, we will define two helper
functions. The Create operation is used to create a new memory mapping. It
takes as parameters the register containing the address (rd ), the register holding
the value to store at this address (ra ), and the current abstract state.
Create(rd , ra , (p, m, ∗)) = (p′ , m, ∗′ )
p′ = p ∩ h{xi = m(rd ), xj = m(ra )}i
∗′ = ∗[xi : xj ] xi = newF V () xj = newF V ()
For instance, in Figure 1 Line 5 creates a new memory mapping: it introduces
the constraints x5 = x3 , x6 = x1 and ∗1 (x5 ) = x6 .
The Replace operation is used to handle the replacement of the value of
an already mapped memory address, overwriting the previous value. It takes
as parameters the variable representing the memory address (a), the register
holding the new value (ra ), and the current abstract state.
Replace(a, ra , (p, m, ∗)) = (p′ , m, ∗′ )
p′ = p ∩ h{xi = m(ra )}i
∗′ = ∗[a : xi ]

xi = newF V ()

For instance, in Figure 1 Line 8 replaces a previous mapping: it introduces the
constraint x8 = x2 and maps x5 to x8 (instead of x6 previously).
Finally, the new abstract state is computed as follows (note that there is at
most one address variable a such that a ≡ r1 ):
(
Replace(a, r2 , s′ ) if a ≡ r1
U pdate(ST ORE r1 r2 , (p, m, ∗)) =
Create(r1 , r2 , s′ ) otherwise
s′ =

4.5

Join

(Replace(a, r2 , (p, m, ∗)), (p, m, ∗))

{a∈A|a overlaps r1 )

Join and widening

The procedure for joining two abstract states is detailed in Algorithm 1. Polyhedra are joined using the classic polyhedra convex hull (line 11). Concerning
register and memory mappings, we first unify equivalent variables (lines 5 and 9),
so that the same variable is used to represent the same register or memory location in both input states. Then, if a memory location or register is bound in
one input state and unbound in the other, it is associated with a fresh variable
in the output state (lines 13 and 16), meaning that we consider that there are
no constraints concerning it. The widening operation is defined exactly in the
same way, except that ∇ is used in place of ∪.
This join operation is illustrated in in Figure 1 for join(e, e′ ). Here s1 corresponds to the state of e and s2 to the state of e′ . At the unification step, x5 in s1
is equivalent to x5 in s2 , so we substitute x6 for x8 in ∗2 and in the polyhedron

Algorithm 1 Computing (p, m, ∗) = Join((p1 , m1 , ∗1 ), (p2 , m2 , ∗2 ))
1:
2:
3:
4:
5:
6:
7:
8:
9:
10:
11:
12:
13:
14:
15:
16:
17:

p1,2 ← p1 ∩ p2 ;
(p′1 , m′1 , ∗′1 ) ← (p1 , m1 , ∗1 )
for each (x1 , x2 ) ∈ varsA (p1) × varsA (p2) do
if x1 is equivalent to x2 then
Replace x1 by x2 and ∗(x1 ) by ∗(x2 ) in p′1 , m′1 , and ∗′1
end if
end for
for Each r ∈ Dom(m′1 ) ∩ Dom(m2 ) do
Replace m′1 (r) by m2 (r) in p′1 , m′1 , and ∗′1
end for
p ← p′1 ∪ p2
for each r ∈ Dom(m′1 ) do
m(r) ← (m′1 (r) = m2 (r)) ? m′1 (r) : newF V ()
end for
for each a ∈ Dom(∗′1 ) do
∗(a) ← (∗′1 (a) = ∗2 (a)) ? ∗′1 (a) : newF V ()
end for

constraints, so we obtain p′1 = (p1 ∩ h{x7 = 0, x6 = x2 }i). Then, the convex hull
regroups the constraints of p′1 and p2 on x6 so we obtain x1 ≤ x6 ≤ x2 . The
convex hull also lifts the constraints on x7 and x8 .
4.6

Soundness

The general principle of the proof of soundness of an abstract interpretation
framework is based on a soundness relation σ, which relates the concrete semantics c of a program p to its abstract semantics a. The abstraction is sound (with
respect to σ) iff σ(c, a) holds for any program p [12].
In our case, the abstract semantics is defined by the abstract states assigned
to the edges of a program. We define the concrete state of a program as the valuation of registers and memory locations. Note that, due to branching instructions,
we may have several possible valuations for the same edge. Formally, a concrete
state is a set of pairs (mc , ∗c ). A register valuation mc maps registers to their
value, while a memory valuation ∗c maps memory addresses to their value. Valuations are partial because some registers or addresses may be mapped to no
value (i.e. undefined). The soundness relation is stated in the following theorem.
Theorem 1. For any program b, for any edge e of b, let C be the concrete state
of e and let (p, m, ∗) be the abstract state of e (at some point of the analysis).
Then, all valuations (mc , ∗c ) of C satisfy the constraints of p. This is denoted
σ(C, (p, m, ∗)).
Proof. We proceed by induction on the structure of the analysis (i.e. on the
definition of the update, join and widening operations). The base of the induction
is straightforward: the initial abstract state has no constraints so any concrete
state is valid.

Now, we need to prove that, for each operation U pdate, ∇, Join, assuming
that σ holds for the input state(s) of these operations, it also holds for their
output state(s).
Binary operation, Branching, LOADI: Let us first consider binary operations.
In the concrete semantics, we have:
U pdatec (OP r1 r2 r3 , C) =

[

(mc [r1 : OP (mc (r2 ), mc (r3 ))], ∗c )

(mc ,∗c )∈C

In the abstract semantics, if OP does not define a linear relation, then no
constraints are added, so σ directly holds thanks to the induction hypothesis. Otherwise, the only new constraint is xi = OP (r2 , r3 ), with m(r1 ) = xi .
Considering the induction hypothesis and the fact that for all pairs (m′c , ∗′c ) of
the output state, m′c (r1 ) = OP (m′c (r2 ), m′c (r3 )), the new constraint holds. The
Branching and LOADI cases are proved with similar reasoning.
LOAD: In the concrete semantics, we have:
U pdatec ((LOAD r1 r2 , C) =

[

(mc [r1 : ∗c (mc (r2 ))], ∗c )

(mc ,∗c )∈C

The case where no address variable is equivalent to r2 is trivial because it
introduces no new constraints. Otherwise, we have xi = ∗(a), with m[r1 : xi ].
Since a is equivalent to r2 , the property holds.
STORE: In the concrete semantics, we have:
U pdatec (ST ORE r1 r2 , C) =

[

(mc , ∗c [(mc (r1 )) : mc (r2 )])

(mc ,∗c )∈C

Let us first assume that there are no polyhedron variables overlapping r1 . In the
create case, the new constraints are xi = m(r1 ), xj = m(r2 ), with ∗[xi : xj ], so
σ holds. In the replace case, the new constraint is xi = m(r2 ), with ∗[a : xi ]
and a equivalent to r1 , so σ holds. Finally, if some variable a overlaps r1 , we
perform a Join operation between p and p plus the same constraints as for the
replace case. a overlaps r1 means that either a 6= r1 , in which case we add no
constraints (p′ = p), or a = r1 , in which case we add the same constraints as for
the replace. The soundness of the Join operation used here is proved below.
Join and ∇: Concerning the Join operation, in the concrete semantics we have:
Joinc (C1 , C2 ) = C1 ∪ C2
Let (p1 , m1 , ∗1 ) and (p2 , m2 , ∗2 ) be the abstract states corresponding to C1 and
C2 . In the abstract semantics, we join polyhedra by computing their convex hull.

By definition of the convex hull, and by the induction hypothesis, all the valuations of C1 ∪C2 satisfy the constraints of p1 ∪p2 . Concerning register and memory
mappings, the unification of equivalent variables (lines 5 and 9 of Algorithm 1)
does not change constraints. The introduction of fresh variables, when a register
or memory location is unbound in one of the input states (lines 13 and 16),
effectively relaxes the constraints on it, so the soundness holds. Soundness of
operation ∇ holds, from a similar reasoning.
⊓
⊔
4.7

Optimization

The complexity of our method depends on the number of variables and the
number of constraints created as the analysis progresses. The number of variables
introduced can be easily upper-bounded. For every instruction in the code, we
introduce at most 5 variables: two new variables for STORE and 3 new variables
for the Merge. This may seem a lot, however several optimizations are possible.
The most relevant is the elimination of unused variables from the polyhedra
as the analysis progresses: any variable that is not in m(.) or in ∗(.) can be
safely removed from the polyhedra by performing a projection on the remaining
(used) variables. For example, the Merge operation unifies two existing variables,
thus it is easy to see that after a Merge the number of useful variables in the
polyhedron is actually reduced by one. The elimination of unused variables is
implemented in the current version of our tool.
Several other optimizations are possible. An important one is to do the analysis at the level of functions: when the function ends, we can safely remove all
variables that refer to the local context of the function. Also, by introducing
techniques from data structure analysis, we can significantly reduce the number of variables that are necessary to investigate the properties of simple data
structures like arrays. We plan to implement such optimizations as future work.

5

Loop bounds

In this section, we show how to apply our abstract interpretation to the problem
of loop bounds estimation. We are interested in two types of bounds for each
loop. The max bound specifies the maximum number of times the loop body will
be executed, for each complete execution of the loop. The total bound specifies
the total number of times the loop body will be executed in the whole program.
The distinction makes sense only in the case of nested loops.
Example 1 Consider the following code snippet:
int k = 0;
for ( int i = 0; i < 10; i ++)
for ( int j = 0; j < i; j ++)
k ++;

In this example,
the max bound of the inner loop is 9, while its total bound is 45
P
(that is, n=1..9 n). The max and total bound of the outer loop are equal to 10.

The general idea of our loop bound estimation is to count loop iterations
using “virtual” registers. Before starting the analysis, for each loop lh we create
two virtual registers rmlh (for the max bound) and rtlh (for the total bound).
The constraints on these registers are updated during the abstract interpretation
of the program.
To analyse max bounds, special updates are applied on loop entries and on
loop back-edges (in addition to the updates defined previously in Section 4).
When interpreting an entry edge of loop lh , we assign value 0 to the corresponding max bound virtual register:
U pdateEntryM ax((p, m, d), lh ) = U pdate(LOADI rmlh 0, (p, m, d))
When interpreting a back-edge of loop lh , we increment the max bound
virtual register (to simplify the presentation, we abusively directly add a constant
value instead of a register content):
U pdateIterM ax(p, m, d, lh ) = U pdate(ADD rmlh rmlh 1, (p, m, d))
Let (pf , mf , df ) be the final abstract state, i.e. the state obtained as output
of the exit node of the program. Once the analysis is complete, the max bound
of a loop lh is computed as max(pf , m[rmlh ]).
The analysis of total bounds presented here only considers triangular loops.
A triangular loop (see Example 1 for instance) consists of an inner loop li nested
inside an outer loop lo , where the index of the inner loop depends on the index
of the outer loop. The objective of the analysis is to try to establish a linear
relation between them.
First, we define two auxiliary functions. The function Relation(p, x1 , x2 ) tries
to find a linear relation between variables x1 and x2 in p:

Relation(p, x1 , x2 ) =

(

(A, B, C)
undef ined

if A.x1 + B.x2 ≤ C in proj(p, x1 , x2 )
otherwise

The function T otal(A, B, C, M ) computes a sum based on coefficients A, B,
C (provided they are not undefined) and on a bound M :
T otal(A, B, C, M ) =

M−1
X
i=0


 
C − Bi
max 0,
A

Let us now detail the analysis. At the program entry, each total bound virtual
register is set to 0. The U pdateIterT otal function is applied on the back-edge
of the inner loop. It updates the total bound virtual register:
U pdateIterT otal((p, m, d), li ) = U pdate(ADD rtli rtli 1, p, m, d)

The U pdateExitT otal function is applied on the exit-edge of the inner loop.
It bounds the value of rtli :
U pdateExitT otal((p, m, d), li , lo ) = (p′ , m, d)
p′ = p ∩ h{m[rtli ] ≤ t}i
(A, B, C) = Relation(p, m[rmli ], m[rmlo ])
M = max(p, m[rmlo ])

t = T otal(A, B, C, M )

Let us consider Example 1. In the input state (p, m, ∗) of the back-edge of li
the constraint rmlo = rmli holds, so Relation(p, rmli , rmlo ]) = (1, −1, 0). Since
P10−1
n = 45. Hence, we add
max(p, rmlo ) = 10, we get T otal(1, −1, 0, 10) = n=1
constraint rtli ≤ 45 to p.
Note that the virtual register rtli is not actually used to compute the total
loop bound. It can however be used to analyse code executed after the nested
loops. For instance, in Example 1, we obtain the constraint k ≤ 45, should k
appear somewhere later in the program.

6

Experimental results

Our methodology is implemented in a prototype called ABCPoly, as a plugin of
OTAWA (version 2.0), an open source WCET computation tool [17]. ABCPoly
relies on OTAWA for CFG construction and manipulation, and on PPL [13] for
polyhedra operations. The analyses have been executed on a PC with an Intel
core i5 3470 at 3.2 Ghz, with 8 Gb of RAM. Every benchmark has been compiled
with ARM crosstool-NG 1.20.0 (gcc version 4.9.1) with -O1 optimization level.
First, we report the results of our experiments on the Mälardalen benchmarks [18] in Table 1. We exclude benchmarks that are not supported by OTAWA,
mainly due to floating point operations or indirect branching (e.g. switch). We
compare ABCPoly with SWEET [19], Pagai [2] and oRange [9]. For each benchmark, we report: the number of lines of code (in the C source), the total number
of loops, the number of loops that are correctly bounded by each tool, and the
computation time. We do not report the computation time for SWEET because
we only had access to it through an online applet. For oRange, computation time
is below the measurement resolution (10ms), except for edn, where it reaches
50ms.
The execution time of ABCPoly is typically higher than that of Pagai because
we introduce more variables and constraints. We believe we can reduce the gap
with additional optimization of the method and of the code, however ABCPoly
will probably remain more costly because it works at a lower level of abstraction.
Concerning loop bounds there are two benchmarks for which ABCPoly did
not find any loop bound: for bench edn, ABCPoly is unable to prove that there is
no array out-of-bound accesses which could potentially overwrite the loop index.
For janne complex, the difficulty is that it contains complex loop index updates
inside a if-then-else. Furthermore, note that Pagai does not compute total
loop bounds.

Bench
crc
fibcall
janne complex
expint
matmult
fdct
jfdctint
fir
edn
ns

Loops Correctly Bounded
Time (ms)
LoC Loops ABCPoly SWEET Pagai oRange ABCPoly Pagai
16
1
1
1
1
1
150
40
22
1
1
1
1
1
230
50
26
2
1
2
1
1
870
140
56
3
3
2
3
3
850
9140
84
5
5
5
5
5
3640
1380
149
2
2
2
2
2
12450 2150
165
3
3
3
3
3
10920 1960
189
2
2
2
2
1
11630
390
198 12
12
12
9
12
25190 15660
414
4
4
4
4
4
1700
380
Table 1. Benchmark results

We further illustrate the differences between tool capabilities on the two
examples of Figure 2. For both examples, ABCPoly provides the correct max
and total loop bounds. For the example foo1, oRange fails to compute the max
and total bounds of the inner loop, because it does not notice that i-x<10. For
foo2, Pagai does not find the max loop bound (the loop is considered unbounded),
because it does not infer that *ptr=&bound when executing instruction *ptr=15.

foo1 ( int x ) {
int i = 0 , j = 0 , k = 0;
for ( i = x ; i < ( x + 10); i ++)
for ( j = 0; j < ( i - x ); j ++);
}

foo2 () {
int i , bound = 10;
int * ptr = & bound ;
ptr ++; ptr - -; * ptr = 15; k = 0;
for ( i = 0; i < bound ; i ++);
}

Fig. 2. Loop examples

7

Conclusion

In this paper we propose a novel technique for performing abstract interpretation
of binary code using polyhedra. Our method consists in adding new variables to
the polyhedra as the analysis progresses, and maintaining a correspondence with
registers and memory addresses. Thanks to the relational properties of polyhedra, our technique naturally provides information on pointer aliasing when
compared to other techniques based on non-relational domains. While the complexity of our method is currently still relatively high, we believe that there is
room for improvement: we are planning to apply some well-known techniques
from static analysis to reduce the number of variables to analyse.

References
1. Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables
of a program. In: Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on
Principles of programming languages, ACM (1978) 84–96
2. Henry, J., Monniaux, D., Moy, M.: Pagai: A path sensitive static analyser. Electronic Notes in Theoretical Computer Science 289 (2012) 15–25
3. Hind, M.: Pointer analysis: Haven’t we solved this problem yet? In: Proceedings of
the 2001 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software
Tools and Engineering. PASTE ’01, New York, NY, USA, ACM (2001) 54–61
4. Hardekopf, B., Lin, C.: The ant and the grasshopper: fast and accurate pointer
analysis for millions of lines of code. ACM SIGPLAN Notices 42(6) (2007) 290–299
5. Balakrishnan, G., Reps, T.: Analyzing memory accesses in x86 executables. In:
Compiler Construction, Springer (2004) 2732–2733
6. Reps, T., Balakrishnan, G.: Improved memory-access analysis for x86 executables.
In: Compiler Construction, Springer (2008) 16–35
7. Müller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra.
ACM SIGPLAN Notices 39(1) (2004) 330–341
8. Eagle, C.: The IDA pro book: the unofficial guide to the world’s most popular
disassembler. No Starch Press (2011)
9. Bonenfant, A., de Michiel, M., Sainrat, P.: orange: A tool for static loop bound
analysis. In: Workshop on Resource Analysis, University of Hertfordshire, Hatfield,
UK. (2008)
10. Ammarguellat, Z., Harrison, III, W.L.: Automatic recognition of induction variables and recurrence relations by abstract interpretation. In: Proceedings of the
ACM SIGPLAN 1990 Conference on Programming Language Design and Implementation. PLDI ’90, New York, NY, USA, ACM (1990) 283–295
11. Ermedahl, A., Sandberg, C., Gustafsson, J., Bygde, S., Lisper, B.: Loop Bound
Analysis based on a Combination of Program Slicing, Abstract Interpretation,
and Invariant Analysis. In Rochange, C., ed.: 7th International Workshop on
Worst-Case Execution Time Analysis (WCET’07). Volume 6 of OpenAccess Series
in Informatics (OASIcs)., Dagstuhl, Germany, Schloss Dagstuhl–Leibniz-Zentrum
fuer Informatik (2007)
12. Cousot, P., Cousot, R.: Abstract interpretation frameworks. Journal of Logic and
Computation 2(4) (1992) 511–547
13. Bagnara, R., Hill, P.M., Zaffanella, E.: The parma polyhedra library: Toward a
complete set of numerical abstractions for the analysis and verification of hardware
and software systems. Science of Computer Programming 72(1) (2008) 3–21
14. Halbwachs, N., Proy, Y., Roumanoff, P.: Verification of real-time systems using
linear relation analysis. Formal Methods in System Design 11(2) (August 1997)
157–185
15. Bagnara, R., Hill, P.M., Ricci, E., Zaffanella, E.: Precise widening operators for
convex polyhedra. In: Proceedings of the 10th International Conference on Static
Analysis. SAS’03, Berlin, Heidelberg, Springer-Verlag (2003) 337–354
16. Simon, A., King, A. In: Widening Polyhedra with Landmarks. Springer Berlin
Heidelberg, Berlin, Heidelberg (2006) 166–182
17. Ballabriga, C., Cassé, H., Rochange, C., Sainrat, P.: Otawa: An open toolbox for
adaptive wcet analysis. In: Software Technologies for Embedded and Ubiquitous
Systems. Volume 6399 of Lecture Notes in Computer Science. Springer Berlin
Heidelberg (2010) 35–46

18. Gustafsson, J., Betts, A., Ermedahl, A., Lisper, B.: The mälardalen wcet benchmarks: Past, present and future. In: OASIcs-OpenAccess Series in Informatics.
Volume 15., Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2010)
19. Lisper, B.: Sweet–a tool for wcet flow analysis. In: International Symposium On
Leveraging Applications of Formal Methods, Verification and Validation, Springer
(2014) 482–485

