JAIST Repository
https://dspace.jaist.ac.jp/

Title

Overflow and Roundoff Error Analysis via Model
Checking

Author(s)Ngoc, Do Thi Bich; Ogawa, Mizuhito

Citation

2009 Seventh IEEE International Conference on
Software Engineering and Formal Methods: 105‑114

Issue Date

2009‑11Type

Conference Paper

Text version

publisher

URL

http://hdl.handle.net/10119/9549

RightsCopyright (C) 2009 IEEE. Reprinted from 2009
Seventh IEEE International Conference on Software
Engineering and Formal Methods, 2009, 105‑114.
This material is posted here with permission of
the IEEE. Such permission of the IEEE does not in
any way imply IEEE endorsement of any of JAIST's
products or services. Internal or personal use ofthis material is permitted. However, permission
to reprint/republish this material foradvertising or promotional purposes or for
creating new collective works for resale orredistribution must be obtained from the IEEE by
writing to pubs‑permissions@ieee.org. By choosing
to view this document, you agree to allprovisions of the copyright laws protecting it.

Description

Japan Advanced Institute of Science and Technology

2009 Seventh IEEE International Conference on Software Engineering and Formal Methods

Overﬂow and Roundoff Error Analysis via Model Checking
Mizuhito Ogawa
School of Information Science
Japan Advanced Institute of Science and Technology
Ishikawa, Japanmizuhito@jaist.ac.jp

Do Thi Bich Ngoc
School of Information Science
Japan Advanced Institute of Science and Technology
Ishikawa, Japandongoc@jaist.ac.jp

Abstractvariables. AI arithmetic supplies higher precision, especiallyin linear operations (e.g., addition, subtraction). However, fornonlinear operations (e.g., multiplication, division), AI arithmetic introduces a fresh noise symbol each time. This leads
to high complexity if there are many nonlinear operations.

This paper proposes a framework for statically analyzing
overﬂow and roundoff errors of C programs. First, a newrange representation, “extended afﬁne interval”, is proposed
to estimate overﬂow and roundoff errors. Second, the overﬂow and roundoff error analysis problem is encoded asa weighted model checking problem. To avoid widening,
currently we focus on programs with bounded loops, which
typically appear in encoder/decoder reference algorithms.
Last, we implement the proposed framework as a static
analysis tool CANA. Experimental results on small programs
show that the extended afﬁne interval is much more precise
than classical interval.

This paper proposes a framework for statically analyzing
OREs for C programs with bounded loops.
First, we propose an extended afﬁne interval (EAI)by assigning a CI coefﬁcient to each noise symbol of
AI form. Compared to AI arithmetic, EAI arithmetic
does not need to introduce new noise symbols for any
operations.
Second, ORE analysis is encoded as a weighted model
checking problem [11]. We represent C programs byweighted transition systems, in which weights are designed using range representations (e.g., CI, AI, EAI).
To avoid widening, currently we focus on programswith bounded loops only, which typically appear inencoder/decoder reference algorithms.
We implement the proposed framework as a static
analysis tool CANA, to analyze OREs of ﬁxed point
algorithms. The backend engine is Weighted PDS library 1 . The input of CANA is C program with nested
loops p64  64q, without procedure calls or pointermanipulations. Experimental results on small programs
demonstrate that EAI is more precise than CI and iscomparable to AI.

Key words: program analysis, model checking, roundoff
error, overﬂow error, afﬁne interval.

1. Introduction
In computer algorithms, real numbers are often represented as ﬂoating point numbers. However, hardware typically uses ﬁxed point number representations for lower costand higher speed. Direct transformation from a reference
algorithm to a hardware algorithm with ﬁxed point numbers
often returns different computational results. This causes
serious problems, especially in digital signal processing,such as in Mpeg decoder and OpenGL libraries.
There have been several works on overﬂow and roundoff
error (ORE) analysis [2], [6], [8], [4], [5]. These works
mostly focus on analyzing roundoff errors in ﬂoating point
systems. In this work, we aim to analyze OREs of ﬁxed
point (reference) algorithms.

The rest of this paper is organized as follows. Section 2
presents ORE problem for ﬁxed point numbers. In Section 3,
we recall the basic notions of CI and AI arithmetics. Then,
we propose a new range representation, EAI, and its arithmetic. We introduce an abstract domain for ORE problems
in Section 4.
Section 5 shows how to encode ORE analysis as aweighted model checking problem. Section 6 shows CANA
implementation and its experimental results. Section 7 mentions related works, and Section 8 concludes the paper andindicates future work.

Based on abstract interpretation technique [1], OREs areanalyzed by automatically propagating the ranges of variablevalues and their roundoff errors. There are two main techniques to propagate ranges. The ﬁrst method uses classicalinterval (CI) [9] to represent possible ranges. This method is
simple but imprecise, because it does not handle correlations
between variables. The second method uses afﬁne interval(AI) [4], [13], [14], which introduces symbolic manipulations on noise symbols, to handle correlations between
978-0-7695-3870-9/09 $26.00 © 2009 IEEE
DOI 10.1109/SEFM.2009.32

1. http://www.fmi.uni-stuttgart.de/szs/tools/wpds/

105

/* CANACANA ALL sign 7 8
global x range 0 1
global n range 100 100*/
double x; int n;
int main () {int i;
double rst;
rst = x; i = 0;
while (i <= n) {rst = rst + i ;i++; }
rst = rst/10.0f ;rst = rst - x * x;
return 1;}

2. Overﬂow and roundoff error problems
2.1. Fixed point numbers and errors
Fixed point numbers are a simple and easy way to express
real numbers, using a ﬁxed number of bits. Fixed point
numbers are generally used when hardware cost, speed, orcomplexity are important issues. We recall some notations
related to ﬁxed point numbers, as follows:
Deﬁnition 1 (Fixed point number): A ﬁxed point number a on base b is represented in the form: a 
sp a1 a2 . . . aip  aip 1 . . . aip f p , where sign part spP t0, 1u
determines if a is sign or unsign, ak P r0, b  1s @k P
r1, ip f ps, ip is the width of integer part, and f p is thewidth of the fraction part.
A real number x is represented by a pair pxf , xr q where
xf is the ﬁxed point value and xr is the corresponding
roundoff error.
There are two types of ﬁxed point errors (FE): roundoff
error due to the ﬁnite fraction part, and overﬂow error due
to the ﬁnite integer part. In programs, one must strike abalance between overﬂow and roundoff errors; by scaling
down the data, the occurrence of overﬂow error is reduced,
but the relative size of the roundoff error is increased. Hence,
we need to consider the largest value of roundoff error andthe largest value of ﬁxed point number. The overﬂow androundoff error (ORE) problems are stated as follows:

Figure 1. An example of a C program
Deﬁnition 2 (FE arithmetic): Let pxf , xr q and pyf , yr q
be representations of x, y, and let  be a noise symbol
such that || ¤ bf p {2. FE arithmetic f  t`, a, b, cu isdeﬁned below.

pxf , xr q ` pyf , yr qpxf yf , xr yr q
pxf , xr q a pyf , yr qpxf  yf , xr  yr q
pxf , xr q b pyf , yr qpxf  yf ,xr  yf xf  yr xr  yr qpxf , xr q c pyf , yr qpxf  yf ,pxf xr q  pyf yr q  xf  yf q

Given a program, initial ranges of variables, and ﬁxed
point format, there are some natural questions:
1) Whether roundoff error of a result lies within thresholdbound or not?
2) Whether overﬂow error may occur? Where?
For clarity, let us illustrate the above problem by a simple
example:Example 1: Assuming that the input C program as shownin Figure 1, the inputs of the program satisfy x P r0, 1s,n  100, and real variables (x, rst) are represented by usingﬁxed point format psp  1, ip  7, f p  8q. The questions
are:1) Does roundoff error of rst lie within r0.01, 0.01s?
2) May overﬂow error occur? Where?

Because of roundoff error, the result of ﬁxed point conditional expression is sometimes different from the resultof real number conditional expression. Therefore, the ﬁxed
point program leads to incorrect results. We deﬁne the FE
comparison operations for ORE problems by comparing therange values of real number representations. For a given
real number representation pxf , xr q, the corresponding range
values are x̃  rxf  |xr |, xf|xr |s. The results of FE
comparison operations may be true, false, or unknown.
Unknown means that the result of real number expression
may differ from that of ﬁxed point expression. Formally, FE
comparison operations are deﬁned as follows:

2.2. FE operations
In ﬁxed point arithmetic, the result must be rounded or
truncated to ﬁt the result into the same number of bits as
the operands. The computation of ﬁxed point arithmetic hasroundoff error , such that || ¤ bf p {2. The roundoff
error of a result is then the sum of  and the result of
propagating the roundoff error of operands. The roundoff
error of arithmetic on ﬁxed point numbers is computed byusing FE arithmetic, as follows:

Deﬁnition 3 (FE comparison operations): Letand pyf , yr q be representations of two numbers.

pxf , xr q,$'&true if @u P x̃ @v P ỹ.u ¤ v
px , x q ¤ py , y q  'false if @u P x̃ @v P ỹ.u ¡ v%unknown otherwise
f

106

r

f

r

$true if px  y ^ x  y  0q''
&false if p@u P x̃ @v P ỹ.u vq
px , x q  p y , y q '_ p@u P x̃ @v P ỹ.u ¡ v q
'
%
f

f

r

f

f

r

Example 2: Let b = 10, sp = 1 (sign), ip = 5, and fp= 3. For an arbitrary number t, the roundoff error is tr r103 {2, 103 {2s. It is easy to see that:rr

tr  tr

unknown otherwiser103 , 103 s

where x̃, ỹ are range values of pxf , xr q, pyf , yr q respectively.
Remark 1: Other comparison operations (e.g., ¡, ! )can be deﬁned using the above operations.

CI arithmetic assumes the ﬁrst operand and the second
operand to be independent, while in fact, they represent thesame quantity tr and the result must be r0, 0s.

3.2. Afﬁne interval

3. Range representations

Afﬁne interval (AI) was introduced by Stolﬁ [13], [14]as a model for self-validated numerical analysis. It was
proposed to address the “error explosion” problem in conventional CI. Unlike CI, in AI, the quantities are represented
as afﬁne combinations (afﬁne forms) of certain primitive
variables, which stand for sources of uncertainty in the data
or approximations made during the computation.
Deﬁnition 6: An Afﬁne interval of x is a formula

To estimate ORE of arithmetic on ﬁxed point numbers,
there are two known over-approximations: classical interval [9] and afﬁne interval [13], [14]. In this section, we
describe these two methods. We then propose a new range
representation method, called “extended afﬁne interval”.

3.1. Classical intervalx:  x0x1 ε1° |x |, xwith x P rx Classical interval (CI) was introduced in the 1960s by
Moore [9] as an approach to putting bounds on rounding
errors in mathematical computations. In CI, each quantity
is represented by the set of all possible values. Formally, CI
is deﬁned as follows:

n
i

0

i

x2 ε2

0



xn εn

i

0

° |x |s. x is called thenicentral value. For each i P r1, ns, εi P r1, 1s is a noise
symbol, which stands for an independent component of thetotal uncertainty. The set of afﬁne interval forms is denoted:
by R.
In AI arithmetic, the results of linear operations (addition,
subtraction) are straightforward operations on AIs. However,
the results of nonlinear operations (multiplication, division)
are not AI forms. Hence, we need to approximate thenonlinear parts of the results by introducing new noise
symbols.

Deﬁnition 4: A classical interval of x is an interval x 
rxl , xh s with xl ¤ x ¤ xh . The set of classical intervals isdenoted by R.
The result of CI arithmetic is also a CI that binds all
possible results. In particular, CI arithmetic is evaluated asfollows:
Deﬁnition 5: CI arithmetic consists of operations t ,  ,  , u on pairs of CIs deﬁned below:
rxl , xh sr103 {2, 103 {2s  r103 {2, 103 {2sDeﬁnition 7: AI arithmetic consists of operations : 

°

°

:, 
: , u: on pairs of AIs as deﬁned below. Let x
t:, 
:
n

n

:  y0x0i1 xi εi and yi1 yi εi . AI operations are
as deﬁned below:nx: : y:  px0 y0 q
yi q ε ii1 pxin: y:  px0  y0 q
x
:
p
x

yi q ε ii 1 inn: y:  px0::xi1 xi εi q  py0
i 1 y i ε i qryl , yh s  rxl

yl , xh yh s
rxl , xh s  ryl , yh s  rxl  yh , xh  yl s
rxl , xh s  ryl , yh s  rminpxl yl , xl yh , xh yl , xh yh q,
maxpxl yl , xl yh , xh yl , xh yh qs
11
rxl , xh s  ryl , yh s  rxl , xh s  r y , u s if 0 R ryl , yh s
h
l

°
°
 x y
0 0

For x, x1 , ..., xn P R,  P , and a constant c, wedenote:x1 x2  x1 x2 , cx  xc  x  rc, cs,
c  x  rc, cs  rxs, x  c  x  rc, cs, and
n
x2

xn .
i1 xi  x1°°n
i 1 px0 yi

°

xi y0 qεi

Bεn 1

°

°
°
° |x |, x ° |x |s,: y:  x: p q, if 0 R rx x::where εn 1 P r1, 1s is a new noise symbol, and Bnnis the maximum value of p i1 xi εi qp i1 yi εi q. An easynnapproximation of B is p i1 |xi |qp i1 |yi |q

°

°

n
n
1
0
i
0
i
i
i
y:
1
where y: is computed by Chebyshev approximation [13].

CI assumes that all intervals are independent, even if theircorresponding quantities are dependent. This assumption
leads to a great loss of precision in a long computation
chain, which is called “error explosion”. The next example
illustrates such a problem.

AI is more precise than CI for linear operations, as shownin the following example.
Example 3: Let us consider base, ﬁxed point format, andnumber t as in Example 2. Hence, the roundoff error is107

t:r  0 p103 {2qε. It is easy to see that:: t:r  p0  0q p103 {2  103 {2qε  0.
t:r This result is the correct result of the subtraction ptr  tr q.

Although EAI does not introduce new noise symbols, thisdoes not mean EAI arithmetic is always less precise than AI
arithmetic. AI arithmetic only advances in cases when wereuse the results of some nonlinear parts. Let us consider
the example below:
Example 4: Let y  x  x, z  y  y and the initial boundof x be r1, 1s. The bound of z is computed based on AI
and EAI arithmetics as follows:
AI arithmetic: x:  ε1 , y:  ε1 : ε1  ε2 where ε2 is: ε2  0
introduced for multiplication. z:  ε2 p
EAI arithmetic: xp  ε1 , yp  ε1 ε1  r1, 1sε1 , zp 
p 1, 1sε1  r2, 2sε1 .
r1, 1sε1 r
The bound of z:, [0,0], lies within the bound of zp, [-2,2]. So,
AI arithmetic is more precise in this case.
However, if we compute the bound of t  x  x  x x without reusing the multiplication x  x, then both AI
arithmetic and EAI arithmetic return the same bound.
t:, pt can be computed in a similar way. We omit the detailsof these computations here due to space limitations.

In AI arithmetic, each time we perform a nonlinear operation, we introduce a new noise symbol, which is problematicfor a program with a large number of nonlinear operations.

3.3. Extended afﬁne interval
To deal with the limits of the above two methods, we
propose a new interval called extended afﬁne interval (EAI).
EAI is extended from AI by assigning for each noise symbol
one CI coefﬁcient, which allows EAI multiplication without
new noise symbols.
Deﬁnition 8: An extended afﬁne interval of x is aformulax
p  x0

°n

ņ



xk εk

k 1

with x P x0k1 xk r1, 1s, where εi P r1, 1s is anoise symbol for each i P r1, ns and xj P R for each j P
pr0, ns. The set of extended afﬁne intervals is denoted by R.

4. Abstract domain for ORE problem

The linear operations of EAI arithmetic are designed
similarly to those of AI arithmetic. For nonlinear operations,unlike AI, EAI arithmetic does not need to introduce newnoise symbols. The results of nonlinear operations are guaranteed to be EAIs by approximating nonlinear parts. For
example, let°us consider the multiplicationof two EAIs. Let°nnp  x0
x
p
x
ε
,
y

y
y
ε
i
i
i
i 1
i1 i .°Without loss of°n 0ngenerality, assume that k°yr
xk r1, 1s.
1n k 1, 1s  k1°n
p yp  px0
p
We have: x
p
x
ε
q

p
y
i
i
0
i 1
i 1 y i ε i q
°n

x
y
p
x
y
x
y
x
B
q
ε
,
where
B 
0
0
i
i
i
i
0
i 1
°n 0
°n
y
ε
.
An
easy
approximation
of
B
is
y
r
1, 1s.
ii 1 ik 1 kFormally, EAI arithmetic is deﬁned as follows:

The abstract value of a variable aims to cover all of its
possible values at one program location. For the ORE problem, the abstract value is a pair of ﬁxed point and roundoff
error ranges. We will show three kinds of abstractions basedon CI, AI, and EAI range representations.

4.1. Abstract domain

Deﬁnition 10: Let f xp and rdf be corresponding range
representations of ﬁxed point and roundoff error.
CI abstract domain Φ  tpf xp, rdf q|f xp, rdf P Ru
:  tpf xp, rdf q|f xp, rdf P R: u
AI abstract domain Φp  tpf xp, rdf q|f xp, rdf P R
pu
EAI abstract domain ΦFor a fresh symbol K (which stands for undeﬁned oruninitialized), we deﬁne ΦK  Φ Y tKu.

Deﬁnition 9: EAI arithmetic consists of operations

p, 
p p
p  tp, below. Let°n, u on pairs of EAI as°deﬁnednp  x0x
p  y0i1 xi εi and yi1 y i εi . The EAI
operations are deﬁned below:°x
p p yp  px0 y 0 q °ni1 pxi y i qεinp yp  px0  y 0 qxp
i1 pxi  y i qεip yp 
p
x
$
°n
°n
'
if
0
&x0 y°i1 px0 y i xi y 0 xi
k1 y k r1, 1sqεi°

The following example illustrates how to initial EAI
abstract values.
Example 5: Assume that we use ﬁxed point format sp 
1, ip  7, f p  8q, base b  2, x P r0, 2s, and y P r1, 3s.
Since f p  8, the initial roundoff error of x lies within
p be EAI
the range r29 , 29 s. Let px
pf , xpr q, pypf , ypr q P Φabstractions of x and y. We have:pf  r1, 1s r1, 1sεf x and xpr  r29 , 29 sεrxx
ypf  r2, 2s r1, 1sεf y and ypr  r29 , 29 sεryy r1, 1s  k1 xk r1, 1s°n0 0
i1 0 i xi y 0 y ik°1nxk r1, 1sqεi otherwise
1
p yp  xp 
p p y1p q if 0 R x0xpk1 xk r1, 1s where yp
is computed by Chebyshev approximation [13].
nk 1 k'% x y ° n px yn4.2. Abstract arithmetic
Abstract arithmetic aims to propagate both ﬁxed point
ranges and roundoff error ranges of variables.

Similar to AI arithmetic, the commutative property holds
for both addition and multiplication; the associative property
only holds for addition; and the distributive property does
not hold.

Deﬁnition 11: Replacing pxf , xr q, pyf , yr q, f, and  inthe deﬁnition of FE arithmetic (Deﬁnition 2) with108f  t`, a, b, cu, and , we obtain
CI abstract arithmetic,px:f , x:r q, py:f , y:r q, f:  t :̀ , a: , b: , c: u, and :, we obtainp let x be range ofFor example, let px
pf , xpr q, pypf , ypr q P Φ,px
pf p xpr q, and let y be the range pypf p ypr q.
p pypf , ypr q is evaluated as follows:
pf , xpr q ¤px

pxf , xr q, py f , y r q,

AI abstract arithmetic, andfabc

pf , xpr q, pypf , ypr q, p  t p̀ , p , p , p u, and p, we obtainpx
EAI abstract arithmetic,
where

#

p pypf , ypr q px
pf , xpr q ¤p  rbf p {2, bf p {2s:  pbf p {2qεr with a fresh noise symbol εrfalse if @u P x @v P y.u ¡ v'%unknown otherwise

The following example illustrates how to evaluate EAI
p.
abstract comparison ¤Example 7: Use px
pf , xpr q, and pypf , ypr q as in Example 5.
p pypf , ypr q is evaluated as follows:px
pf , xpr q ¤x
p  xpf p xpr
 r1, 1s
εf x
r29 , 29 sεrx
The range of x
p is x  r29 , 2 29 s.
pypr
yp  ypf
 r2, 2s
εf yr29 , 29 sεry
The range of yp is y  r1 29 , 3 29 s.
Since x X y  r2 29 , 3 29 s, we can conclude thatp pypf , ypr q is unknown.
pf , xpr q ¤px

p The EAI abstract
For example, let px
pf , xpr q, pypf , ypr q P Φ.
operations are evaluated as follows:p ypf , xpr p ypr q
p ypf , xpr p ypr qp
pf , xpr q a pypf , ypr q  pxpf px
p ypf ,p pypf , ypr q  pxpf pf , xpr q bpx
p ypr p xpr 
p ypf p xpr p ypr p pqxpf p ypf ,p pypf , ypr q  pxpf pxpf , xpr q c
p ypf p pq
p ypf p ypr q
p xpf pf p xpr qppxpx
pf , xpr q p̀ pypf , ypr q  pxpf

To illustrate how abstract values are evaluated, we show the

4.4. Meet operation

following example:
Example 6: Let us consider px
pf , xpr q, pypf , ypr q as in
Example 5. Then, EAI abstract addition pzpf , zpr q px
pf , xpr q p̀ pypf , ypr q is evaluated as follows:
zpf  xpf p ypf
 pr1, 1s
r1, 1sεf x q p pr2, 2s
r1, 1sεf y q
 r3, 3s
r1, 1sεf x
r1, 1sεf y
We then get the range of zpf as r1, 5s by replacing
εf x , εf y with r1, 1s.
Similarly, zpr  r29 , 29 sεrx
range of zpr is r28 , 28 s.

$'&true if @u P x @v P y.u ¤ v

At the meet of two paths in a program, we need to
combine the results that are generated from these paths. The
result of the meet must bind all input abstract values. We
ﬁrst consider how to compute the union of two ranges:
Deﬁnition 13: The unions of ranges are:
CI: rxl , x°pxl , yl q, maxpxh , yh qs.
h sYryl , yh s  rmin°
n
n
u0 v0
AI: pu0
u
ε
q
Y
:
p
v
i
i
0
i°
1
i1 vi εi q  p2n|u 0  v 0 | εn 1i1 ti εi q where εn 1 P r1, 1s is a2
new noise symbol and, for each i,r29 , 29 sεry , and the

#

ti 

Therefore the ﬁxed point value of z is bounded by r1, 5s
and the roundoff error of t is bound by r28 , 28 s.

EAI:
p u0
p u0 Y v 0 q

4.3. Abstract comparison operationsui
vi

if |ui | ¡ |vi |,otherwise.

°n
p pv 0° n i 1 u i ε i q Y
i 1 p u i Y v i q ε i .

°n

i 1 v i εi q Then, the result of meet operation is a pair of the unionof ﬁxed point ranges and the union of roundoff error ranges.
Deﬁnition 14: The meets in abstract values are:CI meet: pxf , xr q \ py f , y r q  pxf Y y f , xr Y y r q:f , x:r q \: py:f , y:r q  px:f Y: y:f , x:r Y: y:r q
AI meet: px
EAI meet: px
pf , zpr q \p pypf , ypr q  pxpf Y
p ypf , xpr Y
p ypr q:p
: , \up is extended to ΦK P tΦK , ΦK , ΦK u by K
\ P t\, \\pxf , xr q  pxf , xr q\ K pxf , xr q.

Instead of nondeterministic transitions at a conditional
branch, the conditional expression can often be evaluatedby using abstract environment. This is useful in avoiding
unnecessary execution paths. The abstract comparison operations are deﬁned by using FE comparisons as follows:
Deﬁnition 12: Replacing pxf , xr q, pyf , yr q, in the deﬁnition of x̃ in FE comparisons (Deﬁnition 3) with
pxf , xr q, py f , y r q, we obtain CI abstract comparison
operations o  t¤, u,:f , x:r q, py:f , y:r q, we obtain AI abstract comparisonpx:  t¤: , : u, andoperations opx
pf , xpr q, pypf , ypr q, we obtain EAI abstract comparisonp  t¤
p , uoperations op .

5. ORE analysis as weighted model checking
5.1. Weighted model checking
It has been suggested that the connections between program analysis and model checking are intimate [12]. That109

Deﬁnition 18: An idempotent semiring is bounded if
there are no inﬁnite descending chains wrt , where a  b
if and only if a ` b  a.

is, a program is ﬁrst encoded into a model ( transition
system) by abstraction, and the program analysis problem
then becomes model checking problem on the generated
model.
Weighted model checking computes dataﬂow (or, an update of environments) by associating a weight to each transition in the model. It was originally proposed as weighted
pushdown model checking [11]. For our purpose, it isenough to restrict the underlying pushdown system to a ﬁnite
state transition system.

5.2. Weight domain for ORE problem
For an ORE problem, we abstract a concrete environment
as an abstract environment by using range representations.
Deﬁnition 19: Let V ar be the set of all variables of the
program. An abstract environment at a program locationis the set of functions AbsEnv  tV ar Ñ ΦkK u, where: K , Φp K u. We deﬁne the zerok  |V ar| and ΦK P tΦK , Φenvironment e0 P AbsEnv by e0 pxq K for x P V ar.
Let e, e1 P AbsEnv, and environment meet operation isdeﬁned below:

Deﬁnition 15: A transition system P is a triplet

pP, Δ, s0 q in which

P is a ﬁnite set of states,
Δ  P  P is a set of transitions, ands0 P P is the initial state.
In weighted model checking, the weight domain mustsatisfy the conditions of the idempotent semiring.

e \ e1  λx.epxq \ e1 pxq
where \ P t\, \: , \up .

Deﬁnition 16: A idempotent semiring is a quintuple
where 0, 1 P D and `, b are binary
operators on D such that, for a, b, c P D,
pD, `q is a commutative monoid with the unit 0,pD, bq is a monoid with the unit 1,
b distributes over `, i.e., a b pb ` cq  pa b bq ` pa b cq
and pa ` bq b c  pa b cq ` pb b cq,` is idempotent, i.e., a ` a  a, and
0 is the zero element of b, i.e., a b 0  0 b a  0.
For program analysis, each element of a bounded idempotent semiring is regarded as follows:
0 stands for interruption of dataﬂow,
1 stands for the identity function (i.e., no state update),b is the composition of two successive dataﬂows, and` merges two dataﬂows at the meet of two transition
sequences.
pD, `, b, 0, 1q,

Weight design. The standard deﬁnition of a weight domain
has the base set of weights D  AbsEnv Ñ AbsEnv. We
then theoretically deﬁne the weight domain for D as follows:
Deﬁnition 20: The weight domain (bounded idempotent
semiring) S  pD, `, b, 0, 1q withD  AbsEnv Ñ AbsEnv,
1  λx.x,0  λx.e0 , $'&λx.w1 pxq \ w2 pxq if w1 , w2  0
w1 ` w2  w1
if w2  0'%w
if w1  0
# 2
w2  w1 if w1 , w2  0
w1 b w2 0otherwise

The weighted transition system is then deﬁned as atransition system “plus” a weight domain.
Deﬁnition 17: A weighted transition system is a triplet
W  pP, S, f q, where P  pP, Δ, s0 q is a transition system,
S  pD, `, b, 0, 1q is a bounded idempotent semiring andf : Δ Ñ D is a map that assigns a weight to each transition.
Denote Δ be a set of all sequences of transitions. Letσ  rr , . . . , r s P Δ . We deﬁne v pσ q  f pr q b . . . b
1kΔ: , \up .
where \ P t\, \However, this does not satisfy the descending chain condition (boundedness), since intervals are inﬁnitely many (thusthe abstract domain is inﬁnite). To cope with this problem,
we:restrict the models to be acyclic,ﬁx an initial abstract environment I, andgenerate weight on-the-ﬂy.

1

f prk q. If σ is a transition sequence from a state c to a state
c1 , we denote c ñσ c1 . The set of all such sequences isdenoted by pathspc, c1 q, i.e.,pathspc, c1 q  tσ | c ñσ c1 u

In the context of our ORE analysis, the intuition behindthe ﬁrst two is,a target program has bounded loops only; thus after unfolding loops, abstraction produces an acyclic transition
system, andthe result of ORE analysis depends heavily on the input
value; we will set a possible range of inputs at the
program entry in advance.

Weighted model checking ﬁnds the weight summary ofpathspc, c1 q, which is the summation `σPpathspc,c q v pσ q.
If a cycle in a weighted model exists, pathspc, c1 q becomes inﬁnite. For termination of a weighted model checking, we need an idempotent semiring must be bounded.
1110

On-the-ﬂy weight generation. We ﬁrst introduce the augmented weight domain to associate an input abstract environment to each weight. “ ” means any input.

instruction”x y z”(assignment)Deﬁnition 21: The augmented weight domain S
pD , `, b, 0 , 1 q consists of D  tpW, wq | W P
AbsEnv, w P Du, 0  p , 0q, 1  p , 1q, and“if x y then s”(Conditional instruction)

w1 ` w2 
w1 b w2 

#
#

 

0

Control instructions

pW2 , w1 b w2 q if W1  w2 pW2 q

 | P


zt uuq

main {
st1: rst = x; i = 0;
st2: while (i <= n) {st3: if (!(i<=n)){st4: break;}st5: __cil_tmp3 =(float)i;
rst += __cil_tmp3;i++;st6: rst /= 10.0f;__cil_tmp4 = x * x;
rst -= __cil_tmp4;
st7: return (1); st8: }Now we are ready to deﬁne the on-the-ﬂy weight domain
SP,I for a transition system P and I P AbsEnv. The
intuition is, starting from the initial abstract environment
I, only reachable instances of weights are computed in onthe-ﬂy manner.
Deﬁnition 22: For a transition system P and I P
AbsEnv, the weight domain SP,I  pDP,I , `, b, 0, 1q is
a sub semiring of S  with DP,I  D . DP,I is given by

1

1
σ
σ 1
pW, wq D^σ,Wσ PvΔpσqpDIc,q c^ PwP. vs0pσñ1 q c ñ c

In implementation, we will identify Dwith D  AbsEnv  AbsEnv by

t  e
e
e 
e

Table 1. Weight function of ORE analysis

otherwiseotherwise0
for w1  pW1 , w1 q, w2  pW2 , w2 q P D .

"

p



pW1 , w1 ` w2 q if W1  W2

weightWi , xo yi zi , vo vi v V ar x
whereis the corresponding
abstract arithmetic operation of
0 if xi yi false; 1 otherwise,
whereis the corresponding
abstract comparison of1

1*

Figure 2. CIL code for Example 1

 AbsEnv  D
The weight function is deﬁned as follows:
Deﬁnition 23: For an acyclic transition system P and I P
AbsEnv, the weight function fP,I : Δ Ñ DP,I is given in
Table 1.

pW, wq  pW, wpW qq
for W P AbsEnv, w P D.

As a result, we obtain the weighted transition system:

5.3. Weighted transition system for ORE problem

W  pP, SP,I , fP,I q

The inputs of our analysis are a subclass of C programs
that have bounded loops only. In preprocessing phase, C
programs are transformed into three address codes. Next,
analysis is performed on these three address codes. Basically,
the instructions of three address codes include:
Assignment: “x  y  z” with  P t , , , {u.
Conditional instruction: “if x  y then s” where s isan instruction and  P t , , ¡, ¡, , ! u. If thecondition px  y q is false, s is not visited; otherwise, s
is visited.
Control instruction: “return loc”, “goto loc”, “break”,“continue”. Control moves to the speciﬁed location, andthe values of variables do not change.
While Loop: “while x  y { body }” with  P t, , ¡, ¡, , ! u. body is repeated as long as thecondition px  y q holds. Inside body, “break” will exitfrom the loop.
In preprocessing phase, the bounded while loops are
unfolded as a sequence of conditional instructions. Thus,
the generated transition system is acyclic.

The following example describes how to create the weighted
transition system for the program in Example 1.
Example 8: We use EAI range representation type. The
three address codes and control ﬂow graph (CFG) of the C
program in Example 1 are shown in Figure 2, and in Figure
3. st1, ..., st8 are locations.
The transition system is P  pP, Δq, where P 
tst1, st2..., st8u, Δ and f is deﬁned in Table 2.
The initial abstract environment Winit at st1 is generated
from initial range values of variables (given in the topmost
comments in Example 1) as:$'&Winit pxq  pr0.5, 0.5s r0.5, 0.5sεxf , r29 , 29 sεxr q
W pnq  pr100, 100s, r0, 0sq'%Winitif v R tx, nu
init pv q  pr0, 0s, r0, 0sq

Then, the resulting weighted transition system is W
pP, SP,Winit , f q.



Since the abstraction is an over-approximation, we conclude soundness of ORE analysis.
111

true

st1

C program andinitial ranges of vars

st2

CIL library

st3

CANA system
Collect data

false
st4

st5

Range arithmetics

Stm Info

Var & Fun Info

CFG

st6
Expression library

Create PDS

Create Fun f

st7
WDomainst8

Figure 3. CFG of three address codes in Figure 2
transition(st1,st2)(st2,st3)(st3,st5)(st3,st4)(st5,st2)(st4,st6)(st6,st7)(st7,st8)

WPDS library
Roundoff andoverflow errors

weightpWinit , trsto  xinit , io  pr0, 0s, r0, 0sq,
vo  vi | v P V ar ztrst, iuuq
1
if ppii p ni q  f alseq 0 else 1
if notppii p ni q  f alseq 0 else 1
pWi , t cil tmp3o  ii ,rsto  rsti p̀ cil tmp3i ,io  ii p̀ 1,
vo  vi | v P V ar zt cil tmp3, rst, iuuq
1
pWi , t cil tmp4o  xi p xi ,rsto  rsti p 10 p xi p xi ,vo  vi | v P V ar zt cil tmp4, rstuuq
1

c

a

WPDS

Figure 4. CANA system
unbounded loops at the moment, we adopt WPDS only
for weighted ﬁnite state (and acyclic) transition systems(i.e., weighted pushdown system with empty stack).
The inputs of CANA are subclass of ANSI C programs
and initial ranges of variables. The outputs of CANA are
roundoff error ranges of variables at each point of the
program, and warning about overﬂow errors (if they occur).
CANA has six main modules (Figure 4) as follows:
1) Collect data module generates information required
for analysis, including: statement information (StmInfo), (2) variable and function information (Var andFunc Info), and (3) CFG of C program.
2) Range arithmetics module includes three types ofrange arithmetics: CI arithmetic, AI arithmetic, andEAI arithmetic.
3) Evaluate exps module evaluates the abstract values of
expressions based on types of range arithmetics.
4) Create PDS module generates transition system fromcontrol ﬂow graph of C program.
5) Create Fun f module assigns a weight to each transition.
6) WDomain module includes two operations: b and `.

bb

Table 2. Weight function for a CIL code in Example 8

Theorem 1: For a C (CIL) program with bounded loops
only, ORE analysis is sound.

6. Experiments
6.1. Implementation
We have implemented our analysis framework in a tool
C ANAlyzer (CANA). CANA uses two libraries as back-end
engines: CIL library 2 and WPDS library 3 .
CIL (C Intermediate Language) is a high-level representation along with tools that permit source-to-source
transformation of C programs. CIL is used to generate
three address codes, information about variables, and
CFG of C program.
WPDS (Weighted Pushdown System) is a library,which provides functions to the sets of forward- or
backward- reachable conﬁgurations in a weighted pushdown system. Since we exclude procedure calls and6.2. Experimental Results
We have implemented in CANA three types of range representations: CI, AI, and EAI. CANA can analyze programs
that have nested loops 64  64.
Example 9: Figure 5 shows the result of analyzing the
C program in Example 1. This shows that the roundoff
error of rst lies within r0.007295, 0.007295s. This range
satisﬁes the condition that the roundoff error of rst lie withinr0.01, 0.01s.

2. http://hal.cs.berkeley.edu/cil/
3. http://www.fmi.uni-stuttgart.de/szs/tools/wpds/

112

[x]
real err
CIAI
EAI[0,0.2]0.01909
0.04373
0.03770.03232[0.2,0.4]
0.03
0.05990.04060.0356[0.4,0.6]
0.03891
0.09172
0.06179
0.05763[0.6,0.8]
0.061588
0.148848
0.104468
0.100454

0.16
0.14
true err

error range

0.12

CI

0.1

AI

0.08

EI

0.06
0.04

Figure 5. The result of CANA for Example 10.02
0[0,0.2]

An overﬂow error may occur for variable rst, because theﬁxed point value of rst lies within r504.093750, 505.500000s
where the largest ﬁxed point number which can be represented must be less than 27  128.
In order to compare the efﬁciency of EAI arithmetic to
CI, and AI arithmetics, we analyzed source codes of three
examples: the ﬁrst example is a C program that computesa polynomial of degree 5, the second is a program that
calculates the sine function, and the last is a tiny fragment,
which frequently appears in the mpeg decoder reference
algorithm. Figure 6 shows experimental results of analyzingthese programs. Figure 6a shows results of analyzing the
program that computes P 5pxq  1x 3x2 2x3 x4 5x5 ,where the fraction part f p  8. The true err row is thewidth of roundoff error ranges which are found by testing
method; the CI, AI, and EAI rows are the approximate
widths of roundoff error ranges computed by using CI
arithmetic, AI arithmetic, and EAI arithmetic, respectively.
Our experiments show that EAI is more precise than CI andis comparable to AI. We get similar results for the programthat computes sine of x shown in Figure 6b, and the part ofmpeg decoder pM peg pexpsq in Figure 6c. All tests run inless than 2 seconds.

[0.2,0.4][0.4,0.6]
x range[0.6,0.8]

a. The analysis result of P5(x)[x]real err
CIAI
EAI[0,0.2]0.006470.02040.02035
0.01759[0.2,0.4]
0.01080.02080.02040.0176[0.4,0.6]
0.01049
0.021390.020290.01749[0.6,0.8]
0.010206
0.022198
0.019976
0.017184

0.025

error range

0.02

true err
CI

0.015

AI
EI

0.01
0.005
0
[0,0.2][0.2,0.4][0.4,0.6]
x range[0.6,0.8]

b. The analysis result of Sin(x)[exps]
real err
CI
AI
EAI[0,30]
1.36309
1.73766
1.634531.63453[30,60]1.36311.73771.63451.6345[60,90]1.36309
1.73766
1.634531.63453[90,120]
1.363086
1.737656
1.634531
1.634531

2
error range

7. Related WorkTo our limited knowledge, for ORE problem, there are
not many works on abstract interpretation-based static
analysis in literature. The works most closely related toours are papers of Goubault and Putot [4], [5] and Martel[7], [8].

true err
CI

1.5

AI

1

EI
0.5
0
[0,30][30,60]x range[60,90][90,120]c. The analysis result of pMpeg(exps)
Figure 6. The experimental results

In [4], Goubault and Putot used AI arithmetic to approximate the roundoff error of ANSI C programs. This work
focused on ﬂoating point numbers, not ﬁxed point numbers.
Goubault and Putot [5] introduced an under approximation
method of computations in real numbers by using meanvalue theorem. Similar to our method, their method also
does not introduce new noise symbols during computation.
113

However, using mean value theorem requires more computations than our method. Also, their method aims to ﬁnd theunder-approximation, instead of over-approximation.

authors would like to thank anonymous reviewers, Prof.
Hiroyuki Seki, Dr. Nao Hirokawa, Dr. Xin Li, and Ms. MaryAnn Mooradian for their valuable comments.

Martel [7], [8] introduced a method to build the roundoff
error function of noise symbols by simply computing the addition, multiplication, substraction and division of functions.
The procedure will stop whenever the degree of roundoff
error function reaches the bound n. Therefore, roundoff error
function is an nth degree function of noise symbols, while
EAI arithmetic only returns linear function of input noise
symbols.

References[1] P. Cousot and R. Cousot. Abstract interpretation: a uniﬁed
lattice model for static analysis of programs by construction orapproximation of ﬁxpoints. In Proc. Intl. Conf. POPL77, pp.
238-252, Los Angeles, 1977.
[2] L. Giraud, J. Langou, M. Rozlonk, J. v. d. Eshof, Rounding
error analysis of the classical Gram-Schmidt orthogonalization
process, Numerische Mathematik, v.101 n.1, pp.87-100, July
2005

8. Conclusion[3] D. Gopan. Numeric program analysis techniques with applications to array analysis and library summarization. PhD Thesis,
University of Wisconsin-Madison, 2007

In this paper, we analyzed the overﬂow and roundoff
errors of C programs. In conclusion, our contributions are
summarized as follows:
An extended afﬁne interval (EAI) was ﬁrst proposed
to estimate overﬂow and roundoff errors. EAI has two
main advantages over current methods. First, EAI ismore precise than CI because EAI can store information
sources of uncertainty, whereas CI cannot. Second, EAI
forms are more compact than AI forms. This is because
EAI arithmetic does not introduce new noise symbols,
while AI arithmetic does.
We proposed an ORE analysis method based onweighted model checking. The range representations(i.e., CI, AI, and EAI) are used to create the set ofweights. Next, the C program is modeled by weighted
transition system (ﬁnite transition system + weight
domain), where weight domain is generated in an onthe-ﬂy manner. Finally, the ORE problem was reduced
to checking reachability properties for the weighted
transition system.
A static analysis tool CANA for overﬂow and roundoff
error analysis of subclass C programs was implemented. Although our experiments were performed on
small examples, the result is encouraging that EAI ismore precise than CI and is comparable to AI.

[4] E. Goubault and S. Putot. Static analysis of numerical algorithms. In SAS’06, pp. 18-34, LNCS 4134, Springer-Verlag
2006.
[5] E. Goubault and S. Putot. Under-approximations of computations in real numbers based on generalized afﬁne arithmetic. In
Proc. Intl. Conf. SAS’07, pp. 137-152, LNCS 4634, SpringerVerlag 2007.
[6] C. F. Fang, T. Chen, and R. Rutenbar. Floating-point error
analysis based on afﬁne arithmetic. In Proc. 2003 International
Conf. on Acoustic, Speech and Signal Processing, pp.561-564,
2003.
[7] M. Martel. Propagation of Roundoff Errors in Finite Precision
Computations: A Semantics Approach. In 11th European Symposium on Programming, pp. 194-208, Springer-Verlag 2002.
[8] M. Martel. Semantics of roundoff error propagation in ﬁnite
precision calculations. In Higher-Order and Symbolic Computation, v19(1),pp.7-30, Springer Netherlands 2006.
[9] R. E. Moore. Interval Analysis. Prentice-Hall, 1966.
[10] G. C. Necula, S. McPeak, S. P. Rahul, W. Weimer. CIL: Intermediate Language and Tools for Analysis and Transformationof C Programs, In Proc. Intl. Conf. on Compiler Construction(CC’02), pp. 213-228, LNCS 2304, Springer-Verlag 2002.

For future work, we plan to consider the following issues:
Design a widening operator to analyze programs thathave unbounded loops,
Improve CANA to analyze C programs in practice, e.g.,
the endoder/decoder reference algorithms, andCombine our proposed technique with the simulation
technique to improve precision and efﬁciency of ORE
analysis.

[11] T. Reps, S. Schwoon, S. Jha and D. Melski. Weighted pushdown systems and their application to interprocedural dataﬂow
analysis. Science of Computer Programming 58, pp. 206-263,
No. 1-2, October 2005.
[12] D. A. Schmidt and B. Steffen. Program analysis as model
checking of abstract interpretations. In Proc. Intl. Conf.
SAS’98, pp. 351380, LNCS 1503, Springe-Verlag 1998.
[13] J. Stolﬁ. Self-Validated Numerical Methods and Applications.
Ph. D. Dissertation, Computer Science Department, Stanford
University, 1997.

Acknowledgements[14] J. Stolﬁ and L.H. de Figueiredo. An introduction to afﬁnearithmetic. TEMA Tend. Mat. Apl. Comput., No.4, Vol.3, pp.
297-312, 2003.

This research is partially supported by STARC (Semiconductor Technology Academic Research Center). The

114