Mathematical Execution:
A Unified Approach for Testing Numerical Code
Zhoulai Fu

Zhendong Su

arXiv:1610.01133v1 [] 4 Oct 2016

Department of Computer Science, University of California, Davis, USA
zhoulai.fu@gmail.com
su@cs.ucdavis.edu

Abstract
This paper presents Mathematical Execution (ME), a new, unified
approach for testing numerical code. The key idea is to (1) capture
the desired testing objective via a representing function and (2) transform the automated testing problem to the minimization problem of
the representing function. The minimization problem is to be solved
via mathematical optimization. The main feature of ME is that it
directs input space exploration by only executing the representing
function, thus avoiding static or symbolic reasoning about the program semantics, which is particularly challenging for numerical
code. To illustrate this feature, we develop an ME-based algorithm
for coverage-based testing of numerical code. We also show the
potential of applying and adapting ME to other related problems,
including path reachability testing, boundary value analysis, and
satisfiability checking.
To demonstrate ME’s practical benefits, we have implemented
CoverMe, a proof-of-concept realization for branch coverage based
testing, and evaluated it on Sun’s C math library (used in, for
example, Android, Matlab, Java and JavaScript). We have compared
CoverMe with random testing and Austin, a publicly available
branch coverage based testing tool that supports numerical code
(Austin combines symbolic execution and search-based heuristics).
Our experimental results show that CoverMe achieves near-optimal
and substantially higher coverage ratios than random testing on all
tested programs, across all evaluated coverage metrics. Compared
with Austin, CoverMe improves branch coverage from 43% to 91%,
with significantly less time (6.9 vs. 6058.4 seconds on average).

1.

Introduction

Testing has been a predominant approach for improving software
quality. Manual testing is notoriously tedious [13]; automated testing
has been an active research topic, drawing on a rich body of
techniques, such as symbolic execution [12, 14, 17, 36], random
testing [1, 11, 30] and search-based strategies [9, 38, 42, 49].
Automated testing is about producing program failures [51]. Let
FOO be a program and dom(FOO) be its input domain. An automated
testing problem is to systematically find x ∈ dom(FOO) such that
FOO(x) ⇓ wrong, where FOO(x) ⇓ wrong denotes “FOO goes wrong if
executed on input x.” It is difficult to specify FOO(x) ⇓ wrong, which
is known as the test oracle problem [50, 69]. This paper assumes
that an algorithm for checking FOO(x) ⇓ wrong is given.
An important problem in testing is the testing of numerical code,
i.e., programs with floating-point arithmetic, non-linear variable
relations, or external function calls (such as logarithmic and trigonometric functions). These programs are pervasive in safety-critical
systems, but ensuring their quality remains difficult. Numerical code
presents two specific challenges for existing automated testing techniques: (1) Random testing is easy to employ and fast, but ineffective
in finding deep semantic issues and handling large input spaces; and

(2) symbolic execution and its variants can perform systematic path
exploration, but suffer from path explosion and are weak in dealing
with complex program logic involving numerical constraints.
Our Approach. This paper introduces a new, unified approach
for automatically testing numerical code. It proceeds as follows:
We derive from the program under test FOO another program FOO_R,
called representing function, which represents how far an input x ∈
dom(FOO) is from reaching the set {x | FOO(x) ⇓ wrong}. We require
that the representing function returns a non-negative value for all x,
which diminishes when x gets close to the set and vanishes when x
goes inside. Intuitively, this representing function is similar to a sort
of distance. It allows to approach the automated testing problem,
i.e., the problem of finding an element in {x | FOO(x) ⇓ wrong}, as
the problem of minimizing FOO_R. This approach can be justified
with a strong guarantee:
FOO(x) ⇓ wrong

⇔ x minimizes FOO_R,

(1)

assuming that there exists at least one x such that FOO(x) ⇓ wrong
(details in Sect. 4). Therefore, the essence of our approach is to
transform the automated testing problem to a minimization problem.
Minimization problems are well studied in the field of Mathematical
Optimization (MO) [53]. MO works by executing its objective
function only (see Sect. 2). That is to say, our approach does not need
to analyze the semantics of the tested programs. Instead, it directs
input space exploration by only executing the representing function.
We call this approach Mathematical Execution (abbreviated as ME).
Note that mathematical optimization by itself does not necessarily provide a panacea for automated testing because many MO
problems are themselves intractable. However, efficient algorithms
have been successfully applied to difficult mathematical optimization problems. A classic example is the NP-hard traveling salesman
problem, which has been nicely handled by simulated annealing [37],
a stochastic MO technique. Another example is Monte Carlo Markov
Chain [8], which has been effectively adapted to testing and verification [28, 29, 34, 63]. A major finding of this work is that using
mathematical optimization for testing numerical code is a powerful
approach. If we carefully design the representing function so that
certain conditions are respected, we can come up with mathematical
optimization problems that can be efficiently solved by off-the-shelf
MO tools.
To demonstrate the feasibility of our approach, we have applied
ME on coverage-based testing [54] of floating-point code, a fundamental problem in testing. The experimental results show that
our implemented tool, CoverMe, is highly effective. Fig. 1 gives a
small program from our benchmark suite Fdlibm [3]. The program
operates on two double input parameters. It first takes |x|’s high
word by bit twiddling, including a bitwise AND (&), a pointer reference (&) and a dereference (*) operator. The bit twiddling result is
stored in integer variable ix (Line 3), followed by four conditional
statements that examine ix (Lines 4–15). The tool CoverMe yields:

1 #define __HI(x) *(1+(int*)&x)
2 double __kernel_cos(double x, double y){
3
ix = __HI(x)&0x7fffffff; /* ix = |x|’s high word */
4
if(ix<0x3e400000) {
/* if |x| < 2**(-27) */
5
if(((int)x)==0) return ...; /* generate inexact */
6
}
7
...;
8
if(ix < 0x3FD33333)
/* if |x| < 0.3 */
9
return ...;
10
else {
11
if(ix > 0x3fe90000) { /* if |x| > 0.78125 */
12
...;
13
} else {
14
...;
15
}
16
return ...;
17
}
18 }
Figure 1: The benchmark program __kernel_cos taken from the Fdlibm [3]
library (http://www.netlib.org/fdlibm/k_cos.c).

100%
87.5%

line coverage
branch coverage

When investigating why CoverMe fails to achieve full branch
coverage, we find that one out of the eight branches in the program
cannot be reached. The condition if ((int) x) == 0 (Line 5)
always holds because it is nested within the |x| < 2−27 branch (Line
4). 1 Therefore, the 87.5% branch coverage is, in fact, optimal. We
have compared CoverMe with Austin [43], a publicly available, stateof-the-art coverage-based testing tool that can handle floating-point
code. Austin achieves 37.5% branch coverage in 1885.1 seconds,
whereas CoverMe achieves the optimal coverage in 15.4 seconds
(see Sect. 5).
Contributions. Our contributions follow:
• We introduce Mathematical Execution, a new general approach
for testing numerical code;
• We develop an effective coverage-based testing algorithm using
the ME approach;
• We demonstrate that ME is a unified approach by showing how
to apply ME to several important testing problems; and
• We implement the coverage-based testing tool CoverMe and
show its effectiveness on real-world numerical library code.
Paper Outline. Sect. 2 gives the background on mathematical
optimization. Sect. 3 illustrates ME by studying the case of branch
coverage based testing. We define the problem, demonstrate the
ME solution, and give the algorithmic details. Sect. 4 lays out the
theoretical foundation for ME and demonstrates ME with several
additional examples. Sect. 5 presents an implementation overview of
CoverMe and describes our experimental results. Sect. 6 discusses
the current limitations of ME. Finally, Sect. 7 surveys related work
and Sect. 8 concludes. For completeness, Appendix A lists the
benchmark programs in Fdlibm that CoverMe does not support and
their reasons, and Appendix B gives implementation details.
Notation. The sets of real and integer numbers are denoted by
and respectively. For two real numbers a and b, the usage
aEb means a ∗ 10b . In this presentation, we do not distinguish
a mathematical expression, such as x2 + |y|, and its implemen-

R

Z

1 Sun’s developers decided to use this redundant check to trigger the
inexact exception of floating-point as a side effect. From the program
semantics perspective, no input of __kernel_cos can trigger the false branch
of if (((int) x) == 0).

p4
p0

xn
(a)

p2

p1

p3

p5

(b)

Figure 2: (a) Local optimization with the curve of λ x.x ≤ 1 ? 0 : (x − 1)2 .
The illustrated technique uses tangents of the curve to converge quickly
to a minimum point; (b) Global optimization with the curve of λ x.x ≤
1 ? ((x + 1)2 − 4)2 : (x2 − 4)2 . The MCMC method starts from p0 , converges
to local minimum p1 , performs a Monte-Carlo move to p2 and converges to
p3 . Then it moves to p4 and finally converges to p5 .

tation, such as x*x + abs(y). Similarly, we use a lambda expression to mean either a mathematical function or its implementation. For example, an implementation λ x.x2 may refer to the
code double f (double x) {return x*x;}. We use the C-like syntax A? v1 : v2 to mean an implementation that returns v1 if A holds,
or v2 otherwise.

2.

Background

We begin with some preliminaries on mathematical optimization
following the exposition of [28]. A complete treatment of either is
beyond the scope of this paper. See [8, 53, 71] for more details.
A Mathematical Optimization (MO) problem is usually formulated as:
minimize f (x)
(2)
subject to x ∈ S
where f is called the objective function, and S the search space.In
general, mathematical optimization problems can be divided into
two categories. One focuses on how functions are shaped at local
regions and where a local minimum can be found near a given
input. This local optimization is classic, usually involving standard
techniques such as Newton’s or the steepest descent methods. Local
optimization not only provides the minimum value of a function
within a neighborhood of the given input points, but also aids global
optimization, which determines the function minimum over the
entire search space.
Local Optimization. Let f be a function defined over a Euclidean
space with distance function d. We call x∗ a local minimum point
if there exists a neighborhood of x∗ , namely {x | d(x, x∗ ) < δ } for
some δ > 0, so that all x in the neighborhood satisfy f (x) ≥ f (x∗ ).
The value f (x∗ ) is called a local minimum of f .
Local optimization problems can usually be efficiently solved if
the objective function is smooth (such as continuous or differentiable
to some degree) [56]. Fig. 2(a) shows a common local optimization
method with the objective function λ x.x ≤ 1 ? 0 : (x − 1)2 . It uses
tangents of the curve to quickly converge to a minimum point. The
smoothness of the curve makes it possible to deduce the function’s
behavior in the neighborhood of a particular point x by using
information at x only.
Global Optimization and MCMC. If f (x∗ ) ≤ f (x) for all x in
the search space, we call x∗ a global minimum point (or minimum
point for short), and f (x∗ ) the global minimum (or minimum for
short) of the function f . In this presentation, if we say “x∗ minimizes
the function f ”, we mean x∗ is a global minimum point of f .
We use the Monte Carlo Markov Chain (MCMC) sampling to
solve global optimization problems. A fundamental fact regarding

MCMC is that it follows the target distribution asymptotically.
For simplicity, we give the results [8] with the discrete-valued
probability.
Lemma 2.1. Let x be a random variable, A be an enumerable set
of the possible values of x. Let f be a target probability distribution
for x, i.e., the probability of x taking value a is f (a). Then, for an
MCMC sampling sequence x1 , . . . , xn . . . and a probability density
function P(xn = a) for each xn , we have P(xn = a) → f (a).

For example, consider the target distribution of coin tossing
with 0.5 probability for having the head. An MCMC sampling is a
sequence of random variables x1 ,. . . , xn , . . ., such that the probability
of xn being “head”, denoted by Pn , converges to 0.5.
MCMC provides multiple advantages in practice. Because
such sampling can simulate an arbitrary distribution (Lem. 2.1),
MCMC backends can sample for a target distribution in the form of
λ x. exp− f (x) where f is the function to minimize, which allows its
sampling process to attain the minimum points more frequently than
the other points. Also, MCMC has many sophisticated techniques
that integrate with classic local search techniques, such as the Basinhopping algorithm [45] mentioned above. Some variants of MCMC
can even handle high dimensional problems [60], or non-smooth
objective functions [25]. Fig. 2(b) illustrates a typical MCMC cycle.
Steps p0 → p1 , p2 → p3 , and p4 → p5 are the local optimization;
Steps p1 → p2 and p3 → p4 aim to prevent the MCMC sampling
from getting trapped in the local minima.

3.

in any LLVM-supported language
type_t FOO (double x1, double x2, ...)

pen

(.cpp)

double pen (int i, int op, double lhs, double rhs)

FOO_I:

Instrumented program (.bc)

type_t FOO_I (double x1, double x2, ...)

FOOloader
: Program
under
(.cpp)

test
in any LLVM-supported language

void LOADER (double* P)
type_t FOO (double x1, double x2, ...)

FOO_R (.cpp)
pen (.cpp)

void FOO_R (double* P)
1. double lhs, double rhs)
double pen (int i, Step
int op,

libr.so
FOO_I:: Instrumented
program
Instrumented program

(.bc)

void FOO_R (double* P)
type_t FOO_I (double x1, double x2, ...)

MCMC minimization procedure (.py)
(.cpp)

loader

basinhopping (func, sp, n_iter, callback)
void LOADER (double* P)

FOO_R

LLVM
(.cpp) pass
Linking

void FOO_R (double* P)

FOO: Program
libr.so

under test
in any LLVM-supported language

void FOO_R (double* P)
type_t FOO (double x1, double x2, ...)

Branch Coverage Based Testing

This section shows a detailed ME procedure in solving branch
coverage based testing for numerical code.
3.1

FOO:: Program
undertest
test
Program under

Problem Statement

MCMC minimization procedure (.py)
(.cpp)

pen

basinhopping (func, sp, n_iter, callback)
double pen (int i, int op, double lhs, double rhs)

LLVM pass
Instrumented program (.bc)
Linking

FOO_I:

Definition 3.1. Let FOO be the program under test with N conditional statements, labeled by l0 ,. . . ,lN−1 . Each li has a true branch
iT and a false branch iF . The problem of branch coverage based
testing aims to find a set of inputs X ⊆ dom(FOO) that covers all
2 ∗ N branches of FOO. Here, we say a branch is “covered” by X if it
is passed through by the path of executing FOO with an x ∈ X. We
scope the problem with three assumptions:
(a) The inputs of FOO are floating-point numbers.
(b) Each Boolean condition in FOO is an arithmetic comparison in
the form of a op b, where op ∈ {==, ≤, <, 6=, ≥, >}, and a and
b are floating-point variables or constants.
(c) Each branch of FOO is feasible, i.e., it is covered by dom(FOO).
Assumptions (a) and (b) are set for modeling numerical code. Assumption (c) is set to simplify our presentation. Our implementation
will partially relax these assumptions (details in Appendix B).
We introduce the concept of a saturated branch and use it to
reformulate Def. 3.1.
Definition 3.2. Let X be a set of inputs generated during the process
of testing. We say a branch is saturated by X if the branch itself and
all its descendant branches, if any, are covered by X. Here, a branch
b0 is called a descendant branch of b if there exists a segment of
control flow path from b to b0 . Given X ⊆ dom(FOO), we write
Saturate(X)

for the set of branches saturated by X.
To illustrate Def. 3.2, suppose that an input set X covers {0T , 0F , 1F } in the controlflow graph on the right, then Saturate(X) =
{0F , 1F }; 1T is not saturated because it is not
covered, and 0T is not saturated because its
descendant branch 1T is not covered.

(3)

type_t FOO_I (double x1, double x2, ...)

loader
(.cpp) under test
FOO: Program

in any
LLVM-supported
Step
2.
void
LOADER
(double
* P)

language

type_t FOO (double x1, double x2, ...)

Representing function
FOO_R :(.cpp)
pen

(.cpp)

void FOO_R (double* P)
double pen (int i, int op, double lhs, double rhs)

libr.so
FOO_I:

Instrumented program (.bc)

void FOO_R (double* P)
_
_

type t FOO I (double x1, double x2, ...)

Step 3.

MCMC
minimization procedure (.py)
loader (.cpp)

_
Generated(double
test inputs
basinhopping
sp,
void LOADER (func,
P) n iter, callback)
*

_R’s(.cpp)
LLVM
pass minimum points, which
X: A set of FOO
global
saturates (therefore
covers)
all branches of FOO: Program under test
Linking
_
void FOO R (double* P)
in any LLVM-supported language
libr.so

_t FOO (double x1,
typegoal
Figure 3: Branch coverage based
testing via ME. The
is to saturate
void FOO_R (double P)
(therefore cover) all branches of FOO, i.e.,*{0T , 0F , 1T ,pen
1F }.(.cpp)
MCMC minimization procedure (.py)

double x2, ...)

double pen (int i, int op, double lhs, d
basinhopping (func, sp, n_iter, callback)

_

FOO by
I: Instrumented
Observe that if all FOO
’s branches
are covered
an input setprogram (.bc)
LLVM
pass
_t FOO
_I (double x1, double x2, ...)
type
X, they are also saturated
by X, and vice versa.
This
observation
Linking
allows us to reformulate the branch coverage based
testing problem
loader (.cpp)
following the lemma below.
void LOADER (double* P)

Lemma 3.3. Let FOO be a program under test with _the assumptions
FOO R (.cpp)
Def. 3.1(a-c) satisfied. The goal of branch coverage based testing
void FOO_R (double* P)
can be stated as to find a small set of inputs X ⊆ dom(FOO) that
saturates all FOO’s branches.
libr.so

voidinput
FOO_R set
(double
P)
Remark 3.4. In Lem. 3.3, we expect the generated
X to* be
“small”, because otherwise we can use X = dom(MCMC
FOO) which
already
minimization procedure (.py)
saturates all branches under the assumption Def. 3.1(c).
_

basinhopping (func, sp, n iter, callback

LLVM pass
Linking

3.2

An Example

We use a simple program FOO in Fig. 3 to illustrate our approach.
The program has two conditional statements l0 and l1 , and their true
and false branches are denoted by 0T , 0F and 1T , 1F respectively.
The objective is to find an input set that saturates all branches. Our
approach proceeds in three steps:

Table 1: A scenario of how our approach saturates all branches of FOO by
repeatedly minimizing FOO_R. Column “Saturate”: Branches that have been
saturated. Column “FOO_R”: The representing function and its plot. Column
“x∗ ”: The point where FOO_R attains the minimum. Column “X”: Generated
test inputs.
# Saturate

Step 1. We inject a global variable r in FOO, and, immediately
before each control point li , we inject an assignment (Fig. 3)
r=

pen,

(4)

where pen invokes a code segment with parameters specific to li .
The idea of pen is to capture the distance of the program input from
saturating a branch that has not yet been saturated. As illustrated in
Fig. 3, this distance returns different values depending on whether
the branches at li are saturated or not.
We denote the instrumented program by FOO_I. The key in Step 1
is to design pen to meet certain conditions that allow us to approach
the problem defined in Lem. 3.3 as a mathematical optimization
problem. We will specify the conditions in the next step.
Step 2. This step constructs the representing function that we have
mentioned in Sect. 1. The representing function is the driver program
FOO_R shown in Fig. 3. It initializes r to 1, invokes FOO_I and then
returns r as the output of FOO_R. That is, FOO_R(x) for a given input
x calculates the value of r at the end of executing FOO_I(x).
Our approach requires two conditions on FOO_R:
C1. FOO_R(x) ≥ 0 for all x, and

C2. FOO_R(x) = 0 if and only if x saturates a new branch. In other
words, a branch that has not been saturated by the generated
input set X becomes saturated with X ∪ {x}, i.e., Saturate(X) 6=
Saturate(X ∪ {x}).

Imagine that we have designed pen so that FOO_R meets both C1 and
C2. Ideally, we can then saturate all branches of FOO by repeatedly
minimizing FOO_R as shown in the step below.
Step 3. In this step, we use MCMC to calculate the minimum
points of FOO_R. Other mathematical optimization techniques, e.g.,
genetic programming [40], may also be applicable, which we leave
for future investigation.
We start with an input set X = 0/ and Saturate(X) = 0.
/ We
minimize FOO_R and obtain a minimum point x∗ which necessarily
saturates a new branch by condition C2. Then we have X = {x∗ }
and we minimize FOO_R again which gives another input x∗∗ and
{x∗ , x∗∗ } saturates a branch that is not saturated by {x∗ }. We
continue this process until all branches are saturated. When the
algorithm terminates, FOO_R(x) must be strictly positive for any
input x, due to C1 and C2.
Tab. 1 illustrates a scenario of how our approach saturates all
branches of FOO. Each “#n” below corresponds to one line in the
table. We use pen0 and pen1 to denote pen injected at l0 and l1
respectively. (#1) Initially, Saturate = 0.
/ Any input saturates a new
branch. Both pen0 and pen1 set r = 0, and FOO_R = λ x.0 (Fig. 3).
Suppose x∗ = 0.7 is found as the minimum point. (#2) The branch
1F is now saturated and 1T is not. Thus, pen1 sets r = (y − 4)2 .
Minimizing FOO_R gives x∗ = −3.0, 1.0, or 2.0. We have illustrated
this MCMC procedure in Fig. 2(b). Suppose x∗ = 1.0 is found. (#3)
Both 1T and 1F , as well as 0T , are saturated by the generated inputs
{0.7, 1.0}. Thus, pen1 returns the previous r. Then, FOO_R amounts
to pen0 , returning 0 if x > 1, or (x − 1)2 + ε otherwise, where ε is a
small positive constant. Suppose x∗ = 1.1 is found as the minimum
point. (#4) All branches have been saturated. In this case, both
pen0 and pen1 return the previous r. Then, FOO_R becomes λ x.1,
understanding that FOO_R initializes r as 1. The minimum point, e.g.,

1

0/

2

{1F }

λ x.

FOO_R

x∗

X

λ x.0

0.7

{0.7}

(
((x + 1)2 − 4)2
(x2 − 4)2

x≤1
else

1.0 {0.7, 1.0}

.

3

(
0
{0T , 1T ,
λ x.
1F }
(x − 1)2 + ε

4

{0T , 1T ,
0F , 1F }

x>1
else

λ x.1

1.1

{0.7, 1.0,
1.1}

−5.2

{0.7, 1.0,
1.1, −5.2}

x∗ = −5.2, necessarily satisfies FOO_R(x∗ ) > 0, which terminates
the algorithm.
Remark 3.5. Given an input x, the value of FOO_R(x) may change
during the minimization process. In fact, FOO_R is constructed with
injected pen which returns different values at li depending on
whether the branches iT and iF have been saturated. Thus, the minimization step in our algorithm differs from existing mathematical
optimization techniques where the objective function is fixed [71].
3.3

Algorithm

We provide details corresponding to the three steps in Sect. 3.2. The
algorithm is summarized in Algo. 1.
Algorithm for Step 1. The outcome of this step is the instrumented program FOO_I. As explained in Sect. 3.2, the essence is
to inject the variable r and the assignment r = pen before each
conditional statement (Algo. 1, Lines 1-4).
To define pen, we first introduce a set of helper functions that
are sometimes known as branch distance. There are many different
forms of branch distance in the literature [38, 49]. We define ours
with respect to an arithmetic condition a op b.

R

Definition 3.6. Let a, b ∈ , op ∈ {==, ≤, <, 6=, ≥, >}, ε ∈
We define branch distance dε (op, a, b) as follows:
def

dε (==, a, b) = (a − b)2

(5)

def

2

(6)

def

2

(7)

dε (≤, a, b) = (a ≤ b) ? 0 : (a − b)

dε (<, a, b) = (a < b) ? 0 : (a − b) + ε
def

dε (6=, a, b) = (a 6= b) ? 0 : ε
def

R>0 .

(8)
def

and dε (≥, a, b) = dε (≤, b, a), dε (>, a, b) = dε (<, b, a). Usually,
the parameter ε is a small constant, so we drop the explicit reference
to ε when using the branch distance.
The intention of d(op, a, b) is to quantify how far a and b are
from attaining a op b. For example, d(==, a, b) is strictly positive

when a 6= b, becomes smaller when a and b go closer, and vanishes
when a == b. The following property holds:
d(op, a, b) ≥ 0 and d(op, a, b) = 0 ⇔ a op b.

Algorithm 1: Branch coverage based testing via ME.
Program under test
Number of starting points
LM
Local optimization used in MCMC
n_iter
Number of iterations for MCMC
Output: X
Generated input set
Input:

(9)

As an analogue, we set pen to quantify how far an input is from
saturating a new branch. We define pen following Algo. 1, Lines 1423.
Definition 3.7. For branch coverage based testing, the function pen
has four parameters, namely, the label of the conditional statement
li , and op, a and b from the arithmetic condition a op b.
(a) If neither of the two branches at li is saturated, we let pen return
0 because any input saturates a new branch (Lines 16-17).
(b) If one branch at li is saturated but the other is not, we set r to be
the distance to the unsaturated branch (Lines 18-21).
(c) If both branches at li have already been saturated, pen returns
the previous value of the global variable r (Lines 22-23).
For example, the two instances of pen at l0 and l1 are invoked as
pen(li , ≤, x, 1) and pen(l1 , ==, y, 4) respectively in Fig. 3.
Algorithm for Step 2. This step constructs the representing function FOO_R (Algo. 1, Line 5). Its input domain is the same as that
of FOO_I and FOO, and its output domain is double, so to simulate a
real-valued mathematical function which can then be processed by
the mathematical optimization backend.
FOO_R initializes r to 1. This is essential for the correctness of
the algorithm because we expect FOO_R returns a non-negative value
when all branches are saturated (Sect. 3.2, Step 2). FOO_R then calls
FOO_I(x) and records the value of r at the end of executing FOO_I(x).
This r is the returned value of FOO_R.
As mentioned in Sect. 3.2, it is important to ensure that FOO_R
meets conditions C1 and C2. The condition C1 holds true since
FOO_R returns the value of the instrumented r, which is never
assigned a negative quantity. The lemma below states FOO_R also
satisfies C2.
Lemma 3.8. Let FOO_R be the program constructed in Algo. 1,
and S the branches that have been saturated. Then, for any input
x ∈ dom(FOO), FOO_R(x) = 0 ⇔ x saturates a branch that does not
belong to S.
Proof. We first prove the ⇒ direction. Take an arbitrary x such that
FOO_R(x) = 0. Let τ = [l0 , . . . ln ] be the path in FOO passed through
by executing FOO(x). We know, from Lines 2-4 of the algorithm, that
each li is preceded by an invocation of pen in FOO_R. We write peni
for the one injected before li and divide {peni | i ∈ [1, n]} into three
groups. For the given input x, we let P1, P2 and P3 denote the groups
of peni that are defined in Def. 3.7(a), (b) and (c), respectively. Then,
we can always have a prefix path of τ = [l0 , . . . lm ], with 0 ≤ m ≤ n
such that each peni for i ∈ [m + 1, n] belongs to P3, and each peni
for i ∈ [0, m] belongs to either P1 or P2. Here, we can guarantee
the existence of such an m because, otherwise, all peni belong in
P3, and FOO_R becomes λ x.1. The latter contradicts the assumption
that FOO_R(x) = 0. Because each peni for i > m does nothing but
performs r = r, we know that FOO_R(x) equals to the exact value of
r that penm assigns. Now consider two disjunctive cases on penm .
If penm is in P1, we immediately conclude that x saturates a new
branch. Otherwise, if penm is in P2, we obtains the same from
Eq. (9). Thus, we have established the ⇒ direction of the lemma.
To prove the ⇐ direction, we use the same notation as above,
and let x be the input that saturates a new branch, and [l0 , . . . , ln ] be
the exercised path. Assume that lm where 0 ≤ m ≤ n corresponds to
the newly saturated branch. We know from the algorithm that (1)
penm updates r to 0, and (2) each peni such that i > m maintains the
value of r because their descendant branches have been saturated.
We have thus proven the ⇐ direction of the lemma.

FOO

n_start

/* Step 1
1
2
3

4

/* Step 2
5

*/

Inject global variable r in FOO
for conditional statement li in FOO do
Let the Boolean condition at li be a op b where
op ∈ {≤, <, =, >, ≥, 6=}
Insert assignment r = pen(li , op, a, b) before li
*/

Let FOO_I be the newly instrumented program, and FOO_R be:
double FOO_R(double x) {r = 1; FOO_I(x); return r;}

/* Step 3

12

Let Saturate = 0/
Let X = 0/
for k = 1 to n_start do
Randomly take a starting point x
Let x∗ = MCMC(FOO_R, x)
if FOO_R(x∗ ) = 0 then X = X ∪ {x∗ }
Update Saturate

13

return X

6
7
8
9
10
11

14
15
16
17
18
19
20
21
22
23
24
25

Function pen(li , op, a, b)
Let iT and iF be the true and the false branches at li
if iT 6∈ Saturate and iF 6∈ Saturate then
return 0
else if iT 6∈ Saturate and iF ∈ Saturate then
return d(op, a, b) /* d: Branch distance
else if iT ∈ Saturate and iF 6∈ Saturate then
return d(op, a, b) /* op: the opposite of op
else /* iT ∈ Saturate and iF ∈ Saturate
return r

27

28
29
30
31

32
33
34

*/
*/
*/

Function MCMC( f , x)
xL = LM( f , x)
/* Local minimization

26

*/

*/

for k = 1 to n_iter do
Let δ be a random perturbation generation from a
predefined distribution
Let xeL = LM( f , xL + δ )
if f (xeL ) < f (xL ) then accept = true
else
Let m be a random number generated from the
uniform distribution on [0, 1]
Let accept be the Boolean m < exp( f (xL ) − f (xeL ))
if accept then xL = xeL

return xL

Algorithm for Step 3. The main loop (Algo. 1, Lines 8-12) relies
on an existing MCMC engine. It takes an objective function and
a starting point and outputs x∗ that it regards as a minimum point.
Each iteration of the loop launches MCMC from a randomly selected
starting point (Line 9). From each starting point, MCMC computes
the minimum point x∗ (Line 10). If FOO_R(x∗ ) = 0, x∗ is added to
the set of the generated inputs X (Line 11). Lem. 3.8 ensures that
x∗ saturates a new branch in the case of FOO_R(x∗ ) = 0. Therefore,
in theory, we only need to set n_start = 2 ∗ N where N denotes the
number of conditional statements, so to saturate all 2 ∗ N branches.
In practice, however, we set n_start > 2 ∗ N because MCMC cannot
guarantee that its output is a true global minimum point.

The MCMC procedure (Algo. 1, Lines 24-34) is also known
as the Basinhopping algorithm [45]. It is an MCMC sampling
over the space of the local minimum points [46]. The random
starting point x is first updated to a local minimum point xL
(Line 25). Each iteration (Lines 26-33) is composed of the two
phases that are classic in the Metropolis-Hastings algorithm family
of MCMC [16]. In the first phase (Lines 27-28), the algorithm
proposes a sample xeL from the current sample x. The sample xeL is
obtained with a perturbation δ followed by a local minimization, i.e.,
xeL = LM( f , xL +δ ) (Line 28), where LM denotes a local minimization
in Basinhopping, and f is the objective function. The second phase
(Lines 29-33) decides whether the proposed xeL should be accepted
as the next sampling point. If f (xeL ) < f (xL ), the proposed xeL will
be sampled; otherwise, xeL may still be sampled, but only with
the probability of exp(( f (xL ) − f (xeL ))/T ), in which T (called the
annealing temperature [37]) is set to 1 in Algo. 1 for simplicity.

4.

Mathematical Execution

Predicate as function is a common concept in mathematics. As
Gödel stated in his 1931 work [22, 31],

Z

There shall correspond to each relation R (R ⊆ n ) a representing function φ (x1 , . . . , xn ) = 0 if R(x1 , . . . , xn ) and
φ (x1 , . . . , xn ) = 1 if ¬R(x1 . . . xn ).

Traditional representing function in its Boolean nature is a predicate/set indicator of two states, essentially being true or false. For
example, even(N) that decides whether an integer N is even can be
represented by the function λ x.(x mod 2 == 0).
In this section, we present Mathematical Execution (ME) by
extending the Boolean-valued representing function to a real-valued
calculus to address a spectrum of automated testing problems for
numerical code, which we unify in the category of the search
problem.
4.1

Search Problem

Definition 4.1. The search problem with regard to a set X aims to
(a) find an x ∈ X if X 6= 0,
/ and
(b) report “not found” if X = 0.
/
Usually, we have a search space U, and X is specified implicitly as a
subset of U. We denote the search problem by (X,U). In this paper,
we deal with numerical code, and thus, we assume that X is a subset
of N . We also assume that X is decidable so that we can check
whether an x ∈ U is an element of X.

R

Example 4.2. A search problem can be any computational task that
attempts to find an element from a set.

(a) As per the notation used in Sect. 1, an automated testing
problem of program FOO is a search problem (X,U) where
X = {x | FOO(x) ⇓ wrong} and U = dom(FOO).
(b) Another search problem is satisfiability checking, where X is
the set of the models of a constraint, and U is the value domain
to which the variables can be assigned.
4.2

Representing Function

Definition 4.3. A function R is said to be a representing function for
the search problem (X,U) if with any x ∈ U there is an associated
real value R(x), such that
(a) R(x) ≥ 0;
(b) every root of the representation function is a solution of the
search problem, i.e., R(x) = 0 =⇒ x ∈ X; and
(c) the roots of R include all solutions to the search problem, i.e.,
x ∈ X =⇒ R(x) = 0.

Example 4.4. Let (X,U) be a search problem.
(a) A trivial representing function is λ x.(x ∈ X)? 0 : 1.
(b) A generic representing function is the point-set distance. Imagine
that the search problem is embedded in a metric space [62] with
a distance dist : X × X → . As a standard practice, we can lift
dist to dist X defined as λ x. inf{dist(x, x0 ) | x0 ∈ X}, where inf
refers to the greatest lower bound, or infimum. Intuitively, dist X
measures the distance between a point x ∈ U and the set X. It
can be shown that dist X satisfies conditions Def. 4.3(a-c), and
therefore, is a representing function.
(c) The representing function used in branch coverage based testing
is the FOO_R constructed in Sect. 3, where X is the input that
saturates a new branch and U is the input domain. We have
proved that FOO_R is a representing function in Lem. 3.8.

R

The theorem below allows us to approach a search problem by
minimizing its representing function.
Theorem 4.5. Let R be the representing function for the search
problem (X,U), and R∗ be the global minimum of R.
(a) Deciding the emptiness of X is equivalent to checking the sign
of R∗ , i.e., X = 0/ ⇔ R∗ > 0.
(b) Assume X 6= 0.
/ Then, ∀x ∈ U, x minimizes R ⇔ x ∈ X.
Proof. Proof of (a): Suppose X 6= 0.
/ Let x0 be an element of X. We
have R∗ ≥ 0 by Def. 4.3(a). In addition, we have R∗ ≤ R(x0 ) since
R∗ is the minimum. Then we have R∗ ≤ 0 because R(x0 ) = 0 due
to Def. 4.3(c). Thus R∗ = 0. Conversely, R∗ = 0 implies that there
exists an x∗ ∈ U s.t. R(x∗ ) = 0. By Def. 4.3(b), x∗ ∈ X. Thus X 6= 0.
/
Proof of (b): Let 0R denote the set of the roots of R, and MR
be the set of the minimum points of R. It suffices to show that
0R ⊆ MR ⊆ X ⊆ 0R under the condition X 6= 0.
/ We have 0R ⊆ MR
because a root of R is necessarily a minimum point; we have MR ⊆ X
because X 6= 0/ implies R∗ = 0 by Thm. 4.5(a). Take an arbitrary
x∗ ∈ MR , R(x∗ ) = R∗ = 0 holds, and therefore x∗ ∈ X by Def. 4.3(b);
we have X ⊆ 0R from Def. 4.3(c).
Remark 4.6. An instance of Thm. 4.5(a) is shown in Tab. 1, Line 4.
There, FOO_R attains the minimum 1, which means that all branches
have been saturated (namely X = 0).
/ An instance of Thm. 4.5(b) is
shown in Eq. (1). Note that Thm. 4.5(b) does not hold if we drop the
assumption X 6= 0.
/ In fact, any R such as R(x) > 0 is a representing
function for a search problem (0,U),
/
but its minimum point, if any,
can never be an element of the empty set X.
4.3

The ME procedure

The representing function paves the way toward a generic solution
to the search problem. The key parameter in the ME procedure is
mathematical optimization.
Definition 4.7. Let U be a set, µ be a mathematical optimization
algorithm that attempts to calculate a minimum point for an objective
function defined over U. We define the Mathematical Execution
procedure as follows:
Input: A search problem (X,U)
Output: An element of X, or “not found”
M1. Construct the representing function R.
M2. Minimize R. Let x∗ be the minimum point obtained by µ.
M3. Return x∗ if x∗ ∈ X. Otherwise return “not found”.
The following corollary states that the ME procedure solves
the search problem, under the condition that the ME procedure is
equipped with an ideal mathematical optimization backend. Its proof
(omitted) follows Thm. 4.5.

double pen (int i, int op, double lhs, double rhs)

FOO_I:

FOO:

Instrumented program (.bc)

Program under test
in any LLVM-supported language

type_t FOO_I (double x1, double x2, ...)

type_t FOO (double x1, double x2, ...)

loader

pen

(.cpp)

(.cpp)

void LOADER (double* P)

double pen (int i, int op, double lhs, double
_R :(.cpp)
Representing
FOOrhs)

testtest
FOO: Program
Programunder
under

program
FOO_I: Instrumented
Instrumented
program

FOO:

(.bc)

type_t FOO_I (double x1, double x2, ...)

in any LLVM-supported language

loader
type_t FOO (double x1, double
Step 1.x2, ...)

pen

(.cpp)

Step 2.

FOO_R

(.cpp)

Instrumented program (.bc)

libr.so

void LOADER (double* P)

Step 3.

Generated test inputs
{ 3, 1}rhs)
lhs, double

FOO I: Instrumented program (.bc)
LLVM
type_pass
t FOO_I (double x1, double x2, ...)
Linking
loader (.cpp)

_t FOO_I (double
typereachability
Path
problemx1, double x2, ...)
void FOO_R (double* P)

Find x that
triggers
loader
(.cpp)
def
t = [0T , 1T ]

void FOO_R (double* P)
pen (.cpp)

_
basinhopping
_ (func, sp, n iter, callback)

double pen (int i, int op, double lhs, double rhs)
void FOO_R (double* P)

FOO_I:

language

libr.so
type_t FOO (double x1, double x2, ...)

MCMC
minimization
procedure
(.py)
double
pen (int i,
int op, double

void LOADER (double* P)

(.cpp)

function

Program under test

void FOO_R (double* P)
in any LLVM-supported

void LOADER (double* P)

MCMC minimization procedure
(.py)
_R (.cpp)
x triggers t , x minimizes FOO
FOO_R

basinhopping (func, sp, n_iter, callback)

void FOO_R (double* P)

FOO_RFigure
(.cpp)4: Path reachability testing via ME. The goal of this example is to find a test input that triggers the path [0T , 1T ] of the program FOO.
LLVM pass
libr.so
void FOO_R (double P)

Linking
Corollary
libr.so4.8. Let (X,U) be a search problem. Assume that µ
yields a true global minimum point in M2 of the ME procedure.
void FOO_R (double* P)
Then,
*

procedure
(a)MCMC
the ME minimization
procedure returns
an x∗ ∈(.py)
X if X 6= 0,
/ and
(b)basinhopping
the ME procedure
returns
“not
found”
if
X
=
0.
/
_
(func, sp, n iter, callback)
A known issue with testing is its incompleteness, i.e.,
Remark
4.9. pass
LLVM
“Testing
shows the presence of bugs, but not its absence” [24]. In the
Linking
context of Mathematical Execution, the above well-known remark
corresponds to the fact that, in practice, if the ME procedure returns
“not found” for the search problem (X,U), X may still be non-empty.
We call this phenomenon practical incompleteness.
The practical incompleteness occurs when the MO backend fails
to yield an accurate minimum point. To clarify, we use x∗ for an
exact global minimum point, and we use x∗ for the one calculated
by the MO backend µ. Then we consider four disjunctive cases:
(a)
(b)
(c)
(d)

R(x∗ ) = 0 and R(x∗ ) = 0;
R(x∗ ) > 0 and R(x∗ ) > 0;
R(x∗ ) = 0 and R(x∗ ) > 0;
R(x∗ ) > 0 and R(x∗ ) = 0.

The ME procedure remains correct for both (a) and (b). The case
(c) cannot happen because R(x∗ ) < R(x) for all x. The practical
incompleteness occurs in (d), where the ME procedure returns “not
found” but X 6= 0.
/ Sect. 6 further discusses this incompleteness.
4.4

Additional Examples

This subsection aims to show that ME is a unified approach by
applying it on several other important search problems besides
coverage-based testing. In each example, we illustrate ME with a
different representing function.
4.4.1

Path Reachability Testing

Given a path τ of program FOO, we call path reachability testing the
search problem (X,U) with
X = {x | x triggers the path τ},U = dom(FOO).

(10)

The path reachability problem has been studied as an independent
research topic [52], or more commonly, as a subproblem in other
testing problems [30, 38, 42].
Consider the program FOO in Fig. 4(left), which is the same as
that in Fig. 3. Suppose that we want to trigger the path τ = [0T , 1T ]
(we denote a path by a sequence of branches). Our approach to this
example problem is similar to the three steps explained in Sect. 3.2,

void FOO_R (double

P)

*
except that we design a different
representing function here. We
illustrate theMCMC
ME approach
in
Fig.
minimization4.procedure (.py)
_iter, callback)
(func,
sp, nr
Step 1. Webasinhopping
inject a global
variable
in FOO and the assignment

LLVM pass
r = r + d(op, a, b)
(11)
Linking
before the conditional statements, where d is the branch distance
defined in Def. 3.6. The instrumented program is shown as FOO_I in
Fig. 4. The assignment is to measure how far the input has attained
the desired path.
Step 2. The value of r is then retrieved through a driver program
FOO_R (Fig. 4), which initializes r to 0 (unlike in Sect. 3.2, where r
is initialized to 1), calls FOO_I and then returns r.
Step 3. A global minimum point of FOO_R is calculated by an
MO algorithm. As shown in the graph of FOO_R (Fig. 4), there
are three local minimum points, {−3, 1, 2}. Two of them, {−3, 1},
attain the global minimum 0 and either solves the path reachability
testing problem. Note that the representing function is discontinuous
at x = 1, but the MCMC procedure can easily find it (similar to
Fig. 2(b)).
Below we prove the correctness of the ME solution.
Corollary 4.10. An input x triggers τ iff x minimizes FOO_R.
Proof. First, it can be shown that the constructed FOO_R is a representing function for the path reachability problem, thus we can
apply Thm. 4.5. By Thm. 4.5(a), X 6= 0/ since FOO_R attains the
global minimum 0. Then we conclude from Thm. 4.5(b).
4.4.2

Boundary Value Analysis

In testing, test inputs that explore “boundary conditions” usually
have a higher payoff than those that do not [70]. The problem of
generating such inputs is expressed abstractly as boundary value
analysis [39, 54, 58], which can be seen as the search problem with
X = {x | x triggers a boundary condition},U = dom(FOO). (12)

Consider again the program FOO in Fig. 4. The boundary value
analysis is to find test inputs that trigger a boundary condition (a)
x = 1 at l0 , or (b) y = 4 at l1 . With manual reasoning, condition (a)
can only be triggered by input 1. Condition (b) can be triggered
if x = 2 or x = −2 before l1 . For each case, we reason backward
across the two branches at l0 and then merge the results. Eventually
we have {−3, 1, 2} as the test inputs to generate.

double pen (int i, int op, double lhs, double rhs)

FOO_I:

FOO:

Program under test
_
in any LLVM-supported languagetype t

Instrumented program (.bc)
FOO_I (double x1, double x2, ...)

loader
type_t FOO (double x1, double x2, ...)
pen

(.cpp)

void LOADER (double* P)

(.cpp)

_

FOO double
R :(.cpp)
Representing
double pen (int i, int op, double lhs,
rhs)

program
FOO_I: Instrumented
Instrumented
program

function

_
(.bc)void FOO R (double* P)

type_t FOO_I (double x1, double x2,libr.so
...)

loader

void FOO_R (double* P)

(.cpp)

void LOADER (double* P)

FOO_R

MCMC minimization procedure (.py)
basinhopping (func, sp, n_iter, callback)

(.cpp)

void FOO_R (double* P)

libr.so

LLVM pass
Linking

void FOO_R (double* P)

MCMC minimization procedure (.py)

Figure 5: Boundary value analysis via ME. This goal is to find a test input to
_iter, callback)
basinhopping
sp, n
trigger
a boundary(func,
condition,
namely,
(a) x = 1 at l0 or (b) y = 4 at l1 of the
program FOO in Fig. 4.

LLVM pass
Linking

Our ME solution follows: As before, we introduce a global
variable r to estimate how far a program input is from triggering a
boundary condition. We inject the assignment
r = r ∗ d(==, a, b)

(13)

before each condition a op b, where function d is the branch distance
defined in Def. 3.6. Fig. 5 illustrates FOO_I and FOO_R. Then we can
solve the boundary value analysis problem via minimizing FOO_R.
The correctness of this procedure follows:
Corollary 4.11. An input x triggers a boundary condition if and
only if x minimizes FOO_R.
Proof. It can be shown that (1) r is always assigned to a non-negative
value; (2) if r = 0 at the end of the program execution, then one
of the boundary conditions must hold; and (3) r = 0 at the end of
the program execution if at least one of the boundary conditions
holds. Thus, the constructed FOO_R satisfies the conditions for being
a representing function (Def. 4.3). We can then prove the corollary
following Thm. 4.5 (in the same way as we prove Cor. 4.10).
4.4.3

Satisfiability Checking

Consider the satisfiability problem with constraint

R

π = 2x ≤ 5 ∧ x2 ≥ 5 ∧ x ≥ 0

(14)

where x ∈ . If we write x∗ |= π to mean that π becomes a tautology
by substituting its free variable x with x∗ . Then, this satisfiability
problem can be expressed as the search problem ({x∗ | x∗ |= π}, ).
Its representing function can be defined as (Fig. 6):

R

def

R = λ x.(2x ≤ 5) ? 0 : (2x − 5)2 + (x2 ≥ 5) ? 0 : (x2 − 5)2
+ (x ≥ 0) ? 0 : x2 .

(15)

Then we can solve the satisfiability checking problem of constraint
π in Eq. (14) by minimizing its representing function R in Eq. (15).
The
√ ME procedure can easily locate the minimum points in between
5 (≈ 2.24) and log2 5 (≈ 2.32). Each of the minimum points is
necessarily a model of π following Thm. 4.5. The correctness of
such an approach follows:
Corollary 4.12. x∗ |= π ⇔ x∗ minimizes R.
Remark 4.13. The representing function in Eq. (15) is defined on
. It is to illustrate the concept and allows us to ignore issues about
floating-point inaccuracy. A more realistic representing function for
satisfiability checking has been shown in a recent work [28] where
the representing function is constructed based on the binary forms

R

Figure 6: Satisfiability checking via ME. This goal of this example is to find
a model of π defined in Eq. (14). The curve depicts its representing function
defined in Eq. (15).

of floating-point numbers to avoid floating-point arithmetic in the
first place.

5.

Evaluation

5.1

The ME-powered System CoverMe

We have implemented CoverMe, a proof-of-concept realization for
branch coverage based testing. CoverMe has a modular design and
can be adapted to other automated testing problems, such as path
reachability and boundary value analysis (Sect. 4.4). This section
presents the architecture of CoverMe (Fig. 7), in which we identify
three layers and their corresponding use cases. Implementation
details are given in Appendix B.
Client. This layer provides the program under test FOO and specifies the inputs to generate X. The search problem involved will be
(X, dom(FOO)). X is usually implicit, e.g., specified via a path to
trigger as in path reachability testing (Sect. 4.4.1), and checking
x ∈ X has to be feasible following Def. 4.1. FOO is a piece of code
in the LLVM intermediate representation [44] or in any language
that can be transformed to it (such as code in Ada, the C/C++ language family, or Julia). The current CoverMe has been tested on
C, and we require dom(FOO) ⊆ N , as the system backend outputs
floating-point test data by default (see the ME kernel layer below).

R

Researcher. This layer sets two parameters. One is the initial
value of the representing function, denoted by r0 . It is usually
either 0 or 1 from our experience. For example, r0 is set to 0 in
path reachability testing (Sect. 4.4.1), and 1 in both coverage-based
testing (Sect. 3.2) and boundary value analysis (Sect. 4.4.2). The
other parameter is the assignment to inject before each conditional
statement in FOO. In practice, the Researcher specifies this code
segment in the pen procedure and injects r = pen, as shown in
Sect. 3.
ME Kernel. This layer takes as inputs the program FOO provided
by the Client, r0 and pen set by the Researcher, and operates the
three steps described in Sect. 3.2. It (1) uses Clang [2] to inject r
and pen into FOO to construct FOO_I, (2) initializes r to r0 , invokes
FOO_I and returns r in FOO_R, and (3) minimizes FOO_R with MO.
As mentioned in Sect. 3.3, CoverMe uses Basinhopping, an off-theshelf implementation from SciPy optimization package [7] as the
MO backend. Basinhopping is then launched from different starting
points as shown in Algo. 1, Lines 8-12. These starting points are
randomly generated from the Hypothesis library [5].
5.2

Experimental Setup

This section discusses the benchmarks, the tools for comparison, the
settings and hardware, and two evaluation objectives.

FOO:

Program under test
FOO: Program under test
in any LLVM-supported
in any
language
LLVM-supported language
_t FOO
type_t FOO (double x1, type
double
x2, (double
...)
x1, double x2, ...)

Client

Researcher

Table 2: Gcov metrics and explanations

pentest
(.cpp) Specify X pen (.cpp)
Provide FOO: Program under
in any LLVM-supported
language
double pen
(int i, int double
op, double
pen (int
lhs, i,
double
int op,
rhs)double lhs, double rhs)
Metrics
Gcov message Description
Note
FOO: Program under test
type_t FOO (double x1,_double x2, ...)
FOOlanguage
I: Instrumented program
FOO_I: Instrumented
(.bc)
program (.bc)
in any LLVM-supported
Line%
Lines executed Covered source lines a.k.a. line or
pen
(.cpp)
Design
pen x1, type
_
_t FOOx2,
_I (double
Set
r0_I...)
t FOO
(double x1,
type
double
...)
x1, double x2, ...)
type_
t FOO
(double
double
x2,
over total source lines statement coverage
pen

double pen (int i, int op, double lhs, double rhs)

(.cpp)

loader

(.cpp)

loader

_I: Instrumented program (.bc)
FOOpen
voiddouble
LOADERlhs,
(double
double
(int i, int op,
double
rhs)
* P)void

ME Kernel

(.cpp)

Condition%

LOADER (double* P)

Branch%
FOO_R (.cpp)
Construct FOO_I: Instrumented
Constructprogram
(.bc)Minimize FOO_R (.cpp)
loader
void
FOO_Rx2,
(double
type_
t FOO_I (.cpp)
(double x1,
double
...) * P) void FOO_R (double* P)
type_t FOO_I (double x1, double x2, ...)

Branches
executed

Covered conditional
statements over total
conditional statements
Branches taken Covered branches over a.k.a.
at least once
total branches
branch coverage
Calls executed Covered calls over
total calls

Call%
void LOADER
P)
Figure 7: Architecture ofloader
CoverMe.
Each (double
layerlibr.so
is* associated
with typical
use
(.cpp)
libr.so
cases. FOO: program under test;
X:
inputs to generate;
pen: procedure that
_Rtest
FOO
(.cpp)
void
LOADER
(double* P)
void FOO_R (double* P) void FOO_R (double* P)
updates r; r0 : initial value of the representing
function; FOO_I: instrumented
_
void
FOO
R
(double
P)
*
program; FOO_R: representing
FOO_Rfunction.
(.cpp)
MCMC minimizationMCMC
procedure
minimization
(.py)
procedure (.py)

“Branches” and “Calls” in Col. 1, Tab. 2. Col. 2-4 give the corresponding Gcov report message, the descriptions and the general
void FOO_R (double* P)
metrics for coverage testing. (2) Efficiency: we measure the wall
libr.so
LLVM
pass
LLVM
pass
Benchmarks. We use the C math library Fdlibm 5.3 [3] as our
time reported by the standard Unix command “time”. The timeout
Linking
Linking
minimization
procedure
(.py) Oracle).
void MCMC
FOO_Rare
(double
* P)
benchmark. These programs
developed
by Sun (now
limit for the compared tools is 48 hours.
_
basinhopping
sp, n iter, operations,
callback)
They are real-world programs,
rich in(func,
floating-point
and
MCMC
minimization
procedure
(.py)
have been used in Matlab,
Java,
JavaScript
Android.
LLVM
pass sp, n_and
5.3 Quantitative Results
basinhopping
(func,
iter, callback)
Fdlibm includes 80 programs.
Linking Each has one or multiple entry
This subsection presents two sets of experimental results. The first
LLVM
passentry functions. Among them, we
functions. In total, Fdlibm
has 92
validates our approach by comparing it against random testing. The
exclude (1) 36 functions Linking
that do not have branches, (2) 11 functions
second compares CoverMe with Austin [43], an open-source tool
involving non-floating-point input parameters, and (3) 5 static C
that combines symbolic execution and search-based strategies.
functions. Our benchmark suite includes all remaining 40 functions
in Fdlibm. For completeness, we list untested functions and reasons
5.3.1 CoverMe versus Random Testing
why they are not selected in Appendix A.
We have compared CoverMe with Rand by running them on the
Compared Tools. We have considered tools publicly available
benchmarks described in Sect. 5.2. In Tab. 3, we sort all benchmark
to us, including Austin [43], Pex [68], and Klee [15] and its
programs (Col. 1) and entry functions (Col. 2) by their names, give
two variants, namely Klee-Mulitsolver [57] and Klee-FP [18]. We
the numbers of source lines, branches and invoked functions (Col. 3tried Klee-Mulitsolver [57] with Z3 [23] as the SMT backend but
5). All coverage results are given by Gcov. It can be seen that the
found that the expression language of Klee [15] did not support
programs are rich in branches. The largest number of branches is
floating-point constraints. Besides, some common operations in our
114 (ieee754_pow). Especially, some tested functions have more
benchmark programs, such as pointer reference and dereference,
branches than lines. For example, ieee754_atan2 has 44 branches,
type casting, external function calls, etc., are not supported by Z3
but only 39 lines; ceil has 30 branches, but only 29 lines.
or any other backend solvers compatible with Klee-Multisolver.
The times used by CoverMe are given by Col. 6 in Tab. 3.
Klee-FP supports symbolic reasoning on the equivalence between
Observe that the times used by CoverMe vary considerably through
floating-point values but does not support coverage testing [18]. Pex,
all entry functions, from 0.1 to 22.1 seconds, but all under half a
unfortunately, can only run for .NET programs on Windows whereas
minute. We find the numbers of lines (Col. 3) and branches (Col. 4)
Fdlibm is in C, and our testing platform is based on Unix.
are not correlated with the running times (Col. 6). CoverMe takes
To our best knowledge, Austin [43] is the only publicly available
1.1 seconds to run the function expm1 (with 42 branches and 56
tool supporting coverage testing for Fdlibm. Austin combines
lines) and 10.1 seconds to run the function floor (with 30 branches
symbolic execution and search-based heuristics, and has been
and 30 lines). It shows the potential for real-world program testing
thoroughly tested for branch coverage based testing on floating-point
since CoverMe may not be very sensitive to the number of lines or
programs [41]. For empirical comparison, we have also implemented
branches. We set the timeout limit of Rand as 600 seconds, since
a random sampling tool, which samples inputs from the function’s
Rand does not terminate by itself and 600 seconds are already larger
input domains using a standard pseudo-random number generator.
than the times spent by CoverMe by orders of magnitude.
We refer to the tool as Rand.
Col. 7-14 in Tab. 3 show the coverage results of Rand and
CoverMe. We use Gcov to compute four metrics: lines, condition,
Settings and Hardware. CoverMe supports the following combranches and calls (as defined in Tab. 2). All coverage results
mand line options while generating test inputs from floating-point
reported by Gcov have been included in Tab. 3 for completeness.
programs: (1) the number of Monte-Carlo iterations n_iter, (2) the
The columns “Line” and “Branch” refer to the commonly used
local optimization algorithm LM and (3) the number of starting points
line/statement coverage and branch coverage, respectively. The
n_start. These options correspond to the three input parameters in
average values of the coverage are shown in the last row of the
Algo. 1. We set n_iter = 5, n_start = 500, and LM=“powell” which
table. All values in Col. 8, 10, 12 and 14 are larger than or equal
refers to Powell’s local optimization algorithm [59].
to the corresponding values in Col. 7, 9, 11 and 13. It means that
For both Austin and CoverMe, we use the default settings for
CoverMe achieves higher coverage than Rand for every benchmark
running the benchmarks. All experiments were performed on a
program and every metric. For the line and condition coverages,
laptop with a 2.6 GHz Intel Core i7 and 4GB RAM running Ubuntu
CoverMe achieves full coverage for almost all benchmarks, with
14.04 virtual machine.
97.0% line coverage and 98.2% condition coverage on average,
Evaluation Objectives. There are two specific evaluation objecwhereas Rand achieves 54.2% and 61.2% for the two metrics. For
tives. (1) Coverage: We use the standard Gnu coverage tool Gcov [4]
the most important branch coverage (since it is a primary target
to analyze the coverage. Gcov generates four metrics for source
of this paper), CoverMe achieves 100% coverage for 11 out of 40
code coverage analysis, which are listed as “Lines”, “Conditions”,
benchmarks with an average of 90.8% coverage, while Rand does
void libr.so
FOO_R (double* P) basinhopping (func, sp,basinhopping
n_iter, callback)
(func, sp, n_iter, callback)

Table 3: Comparing Random testing and CoverMe. The benchmark programs are taken from Fdlibm [3]. We calculate the coverage percentage using Gcov [4].
The metrics of Gcov are explained in Tab. 2. “n/a” in the last two columns indicates that no function call exists in the program; lines with “n/a” are excluded
when calculating the mean values of the last two columns.

Program

Benchmark characteristics
Time (s)
Line (%)
Condition (%) Branche (%)
Call (%)
Entry function
#Line #Branch #Call
Rand CoverMe Rand CoverMe Rand CoverMe Rand CoverMe

e_acos.c
e_acosh.c
e_asin.c
e_atan2.c
e_atanh.c
e_cosh.c
e_exp.c
e_fmod.c
e_hypot.c
e_j0.c

ieee754_acos(double)
ieee754_acosh(double)
ieee754_asin(double)
ieee754_atan2(double, double)
ieee754_atanh(double)
ieee754_cosh(double)
ieee754_exp(double)
ieee754_frmod(double, double)
ieee754_hypot(double, double)
ieee754_j0(double)
ieee754_y0(double)
e_j1.c
ieee754_j1(double)
ieee754_y1(double)
e_log.c
ieee754_log(double)
e_log10.c
ieee754_log10(double)
e_pow.c
ieee754_pow(double, double)
e_rem_pio2.c ieee754_rem_pio2(double, double*)
e_remainder.c ieee754_remainder(double, double)
e_scalb.c
ieee754_scalb(double, double)
e_sinh.c
ieee754_sinh(double)
e_sqrt.c
ieee754_sqrt(double)
k_cos.c
kernel_cos(double, double)
s_asinh.c
asinh(double)
s_atan.c
atan(double)
s_cbrt.c
cbrt(double)
s_ceil.c
ceil(double)
s_cos.c
cos (double)
s_erf.c
erf(double)
erfc(double)
s_expm1.c
expm1(double)
s_floor.c
floor(double)
s_ilogb.c
ilogb(double)
s_log1p.c
log1p(double)
s_logb.c
logb(double)
s_modf.c
modf(double, double*)
s_nextafter.c nextafter(double, double)
s_rint.c
rint(double)
s_sin.c
sin (double)
s_tan.c
tan(double)
s_tanh.c
tanh(double)

33
15
31
39
15
20
31
70
50
29
26
26
26
39
18
139
64
27
9
19
68
15
14
28
24
29
12
38
43
56
30
12
46
8
32
36
34
12
6
16

12
10
14
44
12
16
24
60
22
18
16
16
16
22
8
114
30
22
14
20
46
8
12
26
6
30
8
20
24
42
30
12
36
6
10
44
20
8
4
12

MEAN

not achieve any 100% coverage and attains only 38.0% coverage on
average. CoverMe achieves 100% call coverage on average, whereas
Rand achieves 39.5%.
5.3.2

CoverMe versus Austin

Tab. 4 reports the testing results of Austin and CoverMe. It uses
the same set of benchmarks as Tab. 3 (Col. 1-2). We use the time
(Col. 3-4) and the branch coverage metric (Col. 5-6) to evaluate the
efficiency and the coverage. We choose branch coverage instead of
the other three metrics in Gcov since branch coverage is the major
concern in this paper. Besides, Gcov needs to have access to the
generated test inputs to report the coverage, but currently, there is
no viable way to access the test inputs generated by Austin. Unlike
Rand, the branch coverage percentage of Austin (Col. 5) is provided
by Austin itself, rather than by Gcov.
Austin also shows large performance variances over different
benchmarks, from 667.1 seconds (the program sin) to hours. As

0
2
0
0
0
3
0
0
0
2
5
2
4
0
1
0
1
1
0
2
0
0
2
0
0
0
6
2
2
0
0
0
0
0
0
0
0
6
3
0

7.8
2.3
8.0
17.4
8.1
8.2
8.4
22.1
15.6
9.0
0.7
10.2
0.7
3.4
1.1
18.8
1.1
2.2
8.5
0.6
15.6
15.4
8.4
8.5
0.4
8.8
0.4
9.0
0.1
1.1
10.1
8.3
9.9
0.3
3.5
17.5
3.0
0.3
0.3
0.7

18.2
46.7
19.4
59.0
40.0
50.0
25.8
54.3
66.0
55.2
69.2
65.4
69.2
87.7
83.3
15.8
29.7
77.8
66.7
57.9
85.3
73.3
57.1
25.0
87.5
27.6
100.0
21.1
18.6
21.4
26.7
33.3
71.7
87.5
31.2
72.2
26.5
100.0
100.0
43.8

100.0 33.3
93.3 60.0
100.0 28.6
79.5 54.6
100.0 16.7
100.0 75.0
96.8 33.3
77.1 66.7
100.0 63.6
100.0 55.6
100.0 87.5
100.0 75.0
100.0 87.5
100.0 90.9
100.0 100.0
92.7 28.1
92.2 46.7
100.0 72.7
100.0 85.7
100.0 60.0
94.1 87.0
100.0 75.0
100.0 66.7
96.4 30.8
91.7 100.0
100.0 20.0
100.0 100.0
100.0 50.0
100.0 41.7
100.0 33.3
100.0 20.0
91.7 33.3
100.0 61.1
87.5 100.0
100.0 46.7
88.9 81.8
100.0 30.0
100.0 100.0
100.0 100.0
100.0 50.0

6.9 54.2

97.0 61.2

100.0
100.0
100.0
84.1
100.0
100.0
100.0
80.0
100.0
100.0
100.0
100.0
100.0
100.0
100.0
92.7
100.0
100.0
100.0
100.0
92.7
100.0
100.0
100.0
100.0
100.0
100.0
100.0
100.0
100.0
100.0
83.3
100.0
100.0
100.0
95.5
100.0
100.0
100.0
100.0

16.7
40.0
14.3
34.1
8.8
37.5
20.8
48.3
40.9
33.3
56.3
50.0
56.3
59.1
62.5
15.8
33.3
45.5
50.0
35.0
69.6
37.5
41.7
19.2
50.0
10.0
75.0
30.0
25.0
21.4
10.0
16.7
38.9
50.0
33.3
59.1
15.0
75.0
50.0
33.3

100.0 n/a
90.0 50.0
92.9 n/a
63.6 n/a
91.7 n/a
93.8 0.0
96.7 n/a
70.0 n/a
90.9 n/a
94.4 0.0
100.0 0.0
93.8 0.0
100.0 0.0
90.9 n/a
87.5 100.0
81.6 n/a
93.3 100.0
100.0 100.0
92.9 n/a
95.0 0.0
82.6 n/a
87.5 n/a
91.7 50.0
88.5 n/a
83.3 n/a
83.3 n/a
100.0 83.3
100.0 0.0
100.0 0.0
97.6 n/a
83.3 n/a
75.0 n/a
88.9 n/a
83.3 n/a
100.0 n/a
79.6 n/a
90.0 n/a
100.0 83.3
100.0 66.7
100.0 n/a

n/a
100.0
n/a
n/a
n/a
100.0
n/a
n/a
n/a
100.0
100.0
100.0
100.0
n/a
100.0
n/a
100.0
100.0
n/a
100.0
n/a
n/a
100.0
n/a
n/a
n/a
100.0
100.0
100.0
n/a
n/a
n/a
n/a
n/a
n/a
n/a
n/a
100.0
100.0
n/a

98.2 38.0

90.8 39.6

100.0

shown in the last row of Tab. 4, Austin needs 6058.4 seconds on
average for the testing. It should be mentioned that the average time
does not include the benchmarks where Austin crashes or times out.
Compared with Austin, CoverMe is faster (Tab. 4, Col. 4) with 6.9
seconds on average (The results are also shown in Tab. 3(Col. 6)).
CoverMe achieves a much higher branch coverage (90.8%) than
Austin (42.8%). We also compare across Tab. 4 and Tab. 3. On
average, Austin provides slightly better branch coverage (42.8%)
than Rand (38.0%).
Col. 7-8 are the improvement metrics of CoverMe against Austin.
The Speedup (Col. 7) is calculated as the ratio of the time spent by
Austin and the time spent by CoverMe. The coverage improvement
(Col. 7) is calculated as the difference between the branch coverage
of CoverMe and that of Austin. We observe that CoverMe provides
3,868X speedup and 48.9% coverage improvement on average.
Remark 5.1. Our evaluation shows that CoverMe has achieved
high code coverage on most tested programs. One may wonder

Table 4: Comparison of Austin [43] and CoverMe. The benchmark programs are taken from the Fdlibm library [3].

Program
e_acos.c
e_acosh.c
e_asin.c
e_atan2.c
e_atanh.c
e_cosh.c
e_exp.c
e_fmod.c
e_hypot.c
e_j0.c

Benchmark
Entry function

ieee754_acos(double)
ieee754_acosh(double)
ieee754_asin(double)
ieee754_atan2(double, double)
ieee754_atanh(double)
ieee754_cosh(double)
ieee754_exp(double)
ieee754_frmod(double, double)
ieee754_hypot(double, double)
ieee754_j0(double)
ieee754_y0(double)
e_j1.c
ieee754_j1(double)
ieee754_y1(double)
e_log.c
ieee754_log(double)
e_log10.c
ieee754_log10(double)
e_pow.c
ieee754_pow(double, double)
e_rem_pio2.c ieee754_rem_pio2(double, double*)
e_remainder.c ieee754_remainder(double, double)
e_scalb.c
ieee754_scalb(double, double)
e_sinh.c
ieee754_sinh(double)
e_sqrt.c
iddd754_sqrt(double)
k_cos.c
kernel_cos(double, double)
s_asinh.c
asinh(double)
s_atan.c
atan(double)
s_cbrt.c
cbrt(double)
s_ceil.c
ceil(double)
s_cos.c
cos (double)
s_erf.c
erf(double)
erfc(double)
s_expm1.c
expm1(double)
s_floor.c
floor(double)
s_ilogb.c
ilogb(double)
s_log1p.c
log1p(double)
s_logb.c
logb(double)
s_modf.c
modf(double, double*)
s_nextafter.c nextafter(double, double)
s_rint.c
rint(double)
s_sin.c
sin (double)
s_tan.c
tan(double)
s_tanh.c
tanh(double)
MEAN

Time (second)
Branch coverage(%)
Improvement metrics
Austin CoverMe Austin
CoverMe Speedup Coverage (%)
6058.8
2016.4
6935.6
14456.0
4033.8
27334.5
2952.1
timeout
5456.8
6973.0
5838.3
4131.6
5701.7
5109.0
1175.5
timeout
timeout
4629.0
1989.8
5534.8
crash
1885.1
2439.1
7584.7
3583.4
7166.3
669.4
28419.8
6611.8
timeout
7620.6
3654.7
11913.7
1064.4
1795.1
7777.3
5355.8
667.1
704.2
2805.5

7.8
2.3
8.0
17.4
8.1
8.2
8.4
22.1
15.6
9.0
0.7
10.2
0.7
3.4
1.1
18.8
1.1
2.2
8.5
0.6
15.6
15.4
8.4
8.5
0.4
8.8
0.4
9.0
0.1
1.1
10.1
8.3
9.9
0.3
3.5
17.5
3.0
0.3
0.3
0.7

16.7
40.0
14.3
34.1
8.3
37.5
75.0
n/a
36.4
33.3
56.3
50.0
56.3
59.1
62.5
n/a
n/a
45.5
57.1
35.0
n/a
37.5
41.7
26.9
50.0
36.7
75.0
30.0
25.0
n/a
36.7
16.7
61.1
50.0
50.0
50.0
35.0
75.0
50.0
33.3

100.0
90.0
92.9
63.6
91.7
93.8
96.7
70.0
90.9
94.4
100.0
93.8
100.0
90.9
87.5
81.6
93.3
100.0
92.9
95.0
82.6
87.5
91.7
88.5
83.3
83.3
100.0
100.0
100.0
97.6
83.3
75.0
88.9
83.3
100.0
79.6
90.0
100.0
100.0
100.0

776.4
887.5
867.0
831.2
495.4
3327.7
349.7
n/a
350.9
776.5
8243.5
403.9
8411.0
1481.9
1061.3
n/a
n/a
2146.5
233.8
9695.9
n/a
122.6
290.8
890.6
9109.4
812.3
1601.6
3166.8
62020.9
n/a
757.8
438.7
1205.7
3131.8
507.0
445.4
1808.3
1951.4
2701.9
4075.0

83.3
50.0
78.6
29.6
83.3
56.3
21.7
n/a
54.6
61.1
43.8
43.8
43.8
31.8
25.0
n/a
n/a
54.6
35.7
60.0
n/a
50.0
50.0
61.6
33.3
46.7
25.0
70.0
75.0
n/a
46.7
58.3
27.8
33.3
50.0
29.6
55.0
25.0
50.0
66.7

6058.4

6.9

42.8

90.8

3868.0

48.9

whether the generated inputs have triggered any latent bugs. Note
that when no specifications are given, program crashes have been
frequently used as an oracle for finding bugs in integer programs.
Floating-point programs, on the other hand, can silently produce
wrong results without crashing. Thus, program crashes cannot be
used as a simple, readily available oracle as for integer programs.
Our experiments, therefore, have focused on assessing the efficiency
of ME in solving the problem defined in Def. 3.1 or Lem. 3.3, and
do not evaluate its effectiveness in finding bugs, which is orthogonal
and interesting future work.

6.

Incompleteness

The development of ME toward a general solution to the search
problem, as illustrated in this presentation, has been grounded in the
concept of representing function and mathematical optimization.
While our theory guarantees that the ME procedure solves the
search problem correctly (Cor. 4.8), the practical incompleteness
(Remark 4.9) remains a challenge in applying ME to real-world

automated testing problems. Below we discuss three sources of
practical incompleteness and how it can be mitigated.
Well-behaved Representing Functions. The well-behavedness
of the representing function is essential for the working of ME.
Well-behavedness is a common term in the MO literature to describe
that the MO backend under discussion can efficiently handle the
objective function. A common requirement, for example, is that the
objective function (or the representing function for ME) should be
smooth to some degree.
Consider again the path reachability problem in Sect. 4.4.1. If
FOO_I is instrumented as in Fig. 8(left), the corresponding FOO_R
also satisfies the conditions in Def. 4.3, but this FOO_R is discontinuous at {−3, 1, 2} (Fig. 8(right)). The representing function changes
its value disruptively at its minimum points. These minimum points
cannot be calculated by MO tools. The example also shows that
the conditions in Def. 4.3(a-c) can be insufficient for avoiding illbehaved representing functions. However, it is unclear to us whether
there exists a set of conditions that are both easy-to-verify and
sufficient for excluding ill-behaved functions.

E

inputs x such that [|FOO|] (x) ∈ , where [|FOO|] (x) denotes the path
of executing FOO with input x.

void FOO_I(double x){
r = r + (x <= 1)? 0:1;

l0 : if (x <= 1) x++;
double y = square(x);
r = r + (y == 4)? 0:1 ;

l1 : if (y == 4) ...;
}

Figure 8: An example of ill-behaved representing function for the path
reachability problem in Sect. 4.4.1. The left is the instrumented FOO_I; the
right is the graph of representing function FOO_R.

Reliance on Program Execution. We have seen that the ME
procedure generates test inputs of program FOO by minimizing, and
therefore, running, another program FOO_R. This execution-reliant
feature has both benefits and risks. It allows us to generate test inputs
of complex programs without analyzing their semantics; it also
means that ME can give different results with different compilers or
machines.
In our experiments, we realize that the feature becomes disadvantageous if inaccuracy occurs in the program execution. Consider
the satisfiability testing problem with the constraint π = x ≥ 1E-20.
Suppose we use the representing function Rπ (x) = x ≥ 1E-20 ? 0 :
(x − 1E-20)2 and implement Rπ as a double-precision floatingpoint program. We can verify that Rπ is a representing function
in the sense of Def. 4.3, but it evaluates to 0 not only when
x ≥ 1E-20, but also when 0 ≤ x < 1E-20 because the smallest
machine-representable double is in the order of 1E-324 [32]. Then
the ME procedure may return x∗ = 0 in step M2 and then returns
“not found” in step M3 because x∗ = 0 is not a model of π.
This issue described above may be mitigated using arbitraryprecision arithmetic [10]. Another option, as is demonstrated in the
XSat solver [28], is to construct the representing function based on
ULP, the unit in the last place value [32], which avoids floating-point
inaccuracy by using the binary representation of floating-points.
Efficient MO Backend. The inherent intractability of global optimization is another source of the incompleteness of ME. Even
if the representing function is well-behaved and free from computational inaccuracy, it is possible that the MO backend returns
sub-optimal or local minimum points due to weak implementation,
high-dimensional or intrinsically difficult problems, etc.. That said,
MO is still in active development, and our ME approach has the
flexibility to leverage its state-of-the-art, such as the Basinhopping
algorithm used in our experiments.

7.

Related Work

Automated Testing. Many automated testing approaches adopt
symbolic execution [12, 14, 17, 36]. They repeatedly select a target
path τ and gather the conjunction of logic conditions along the
path, denoted by Φτ (called path condition [36]). They then use
SMT solvers to calculate a model of Φτ . These approaches are both
sound and complete in the sense of FOO(x) ⇓ wrong ⇔ x |= Φτ .
Symbolic execution and its variants have seen much progress since
the breakthrough of SAT/SMT [55, 65], but still have difficulties
in handling numerical code. There are two well-known efficiency
issues. First, path explosion makes it time-consuming to select a
large number of τ and gather Φτ . Second, for numerical code, each
gathered Φτ involves numerical constraints that can quickly go
beyond the capabilities of modern SAT/SMT solvers.
A large number of search-based heuristics have been proposed
to mitigate issues from symbolic execution. They use fitness functions to capture path conditions and use numerical optimization to
minimize/maximize the fitness functions. A well-developed searchbased testing is Austin [43], which combines symbolic execution and
search-based heuristics. Austin has been compared with Cute [64],
a dynamic symbolic execution tool, and shows to be significantly
more efficient. These search-based solutions, however, as McMinn
points out in his survey paper [49], “are not standalone algorithms
in themselves, but rather strategies ready for adaption to specific
problems.”
Mathematical Optimization in Testing and Verification. In the
seminal work of Miller et al. [52], optimization methods are already
used in generating test data for numerical code. These methods are
then taken up in the 1990s by Koral [26, 38], which have found their
ways into many mature implementations [42, 66, 68]. Mathematical
optimization has also been employed in program verification [19,
61]. Liberti et al. [33, 47] have proposed to calculate the invariant
of an integer program as the mathematical optimization problem of
mixed integer nonlinear programming (MINLP) [67]. Recently, a
floating-point satisfiability solver XSat [28] has been developed.
It constructs a floating-point program Rπ from a formula π in
conjunctive normal form, and then decides the satisfiability of π by
checking the sign of the minimum of Rπ . This decision procedure
is an application of Thm. 4.5(a), and it calculates the models of
π using Thm. 4.5(b). Compared with XSat, our work lays out the
theoretical foundation for a precise, systematic approach to testing
numerical code; XSat is an instance of our proposed ME procedure
(see Example 4.2(b) and Sect. 4.4.3).

8.

Two Paradigms for Program Correctness. Constructing an axiomatic system [27, 35] is of central importance in ensuring program
correctness. Let FOO be a program. If we write [|FOO|] for the set of
FOO’s possible execution paths (a.k.a. trace semantics [48]), and
for the unsafe paths, then the correctness of FOO is to ensure

E

[|FOO|] ∩

E = 0./

(16)

The problem is known to be undecidable, and approximate solutions
have been extensively studied. One is abstract interpretation [20, 21],
which systematically constructs [|FOO|]] ⊇ [|FOO|], and prove Eq. (16)
by proving [|FOO|]] ∩ = 0.
/ 2 Another category of approximation
is automated testing. It attempts to disprove Eq. (16) by generating

E

2 The relationship between the abstract and concrete semantics is more
commonly formalized with a Galois connection [20]; we use [|FOO|]] ⊇ [|FOO|]
as a simplified case.

Conclusion

This paper introduces Mathematical Execution (ME), a new, unified
approach for testing numerical code. Our insight is to (1) use a
representing function to precisely and uniformly capture the desired
testing objective, and (2) use mathematical optimization to direct
input and program space exploration. What ME — and most importantly, the accompanying representation function — provides is an
approach that can handle a variety of automated testing problems, including coverage-based testing, path reachability testing, boundary
value analysis, and satisfiability checking. We have implemented a
branch coverage testing tool as a proof-of-concept demonstration
of ME’s potential. Evaluated on a collection of Sun’s math library
(used in Java, JavaScript, Matlab, and Android), our tool CoverMe
achieves substantially better coverage results (near-optimal coverage
on all tested programs) when compared to random testing and Austin
(a coverage-based testing tool that combines symbolic execution
and search-based strategies).

References
[1] American fuzzy lop. http://lcamtuf.coredump.cx/afl/. Accessed:
25 June, 2016.
[2] Clang: A C language family frontend for LLVM. http://clang.llvm.
org/. Accessed: 25 June 2016.
[3] Freely distributed math library, Fdlibm. http://www.netlib.org/
fdlibm/. Accessed: 25 June, 2016.
[4] GNU compiler collection tool, Gcov.
https://gcc.gnu.org/
onlinedocs/gcc/Gcov.html/. Accessed: 25 June 2016.
[5] Python testing library, hypothesis. https://github.com/DRMacIver/
hypothesis. Accessed: 25 June 2016.
[6] LLVM: Pass class reference. http://llvm.org/docs/doxygen/html/
classllvm_1_1Pass.html. Accessed: 25 June 2016.
[7] Scipy optimization package. http://docs.scipy.org/doc/scipydev/reference/optimize.html. Accessed: 25 June 2016.
[8] C. Andrieu, N. de Freitas, A. Doucet, and M. I. Jordan. An introduction
to MCMC for machine learning. Machine Learning, 50(1-2):5–43,
2003.
[9] A. Baars, M. Harman, Y. Hassoun, K. Lakhotia, P. McMinn, P. Tonella,
and T. Vos. Symbolic search-based testing. In Proceedings of the
26th IEEE/ACM International Conference on Automated Software
Engineering, ASE ’11, pages 53–62, Washington, DC, USA, 2011.
[10] D. H. Bailey. High-precision floating-point arithmetic in scientific
computation. Computing in Science and Engg., 7(3):54–61, May 2005.
[11] D. L. Bird and C. U. Munoz. Automatic generation of random selfchecking test cases. IBM Syst. J., 22(3):229–245, Sept. 1983.
[12] R. S. Boyer, B. Elspas, and K. N. Levitt. A formal system for testing
and debugging programs by symbolic execution. In Proceedings of the
International Conference on Reliable Software, pages 234–245, New
York, NY, USA, 1975.
[13] F. P. Brooks, Jr. The Mythical Man-month (Anniversary Ed.). AddisonWesley Longman Publishing Co., Inc., Boston, MA, USA, 1995.
[14] C. Cadar and K. Sen. Symbolic execution for software testing: Three
decades later. Commun. ACM, 56(2):82–90, 2013.
[15] C. Cadar, D. Dunbar, and D. Engler. Klee: Unassisted and automatic
generation of high-coverage tests for complex systems programs. In
Proceedings of the 8th USENIX Conference on Operating Systems
Design and Implementation, OSDI’08, pages 209–224, Berkeley, CA,
USA, 2008.
[16] S. Chib and E. Greenberg. Understanding the Metropolis-Hastings
algorithm. The American Statistician, 49(4):327–335, Nov. 1995.
[17] L. A. Clarke. A system to generate test data and symbolically execute
programs. IEEE Trans. Softw. Eng., 2(3):215–222, May 1976.
[18] P. Collingbourne, C. Cadar, and P. H. Kelly. Symbolic crosschecking of
floating-point and SIMD code. In Proceedings of the sixth conference
on Computer systems, pages 315–328, 2011.
[19] P. Cousot. Proving program invariance and termination by parametric
abstraction, lagrangian relaxation and semidefinite programming. In
International Workshop on Verification, Model Checking, and Abstract
Interpretation, pages 1–24. Springer, 2005.
[20] P. Cousot and R. Cousot. Abstract interpretation: A unified lattice
model for static analysis of programs by construction or approximation
of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN
Symposium on Principles of Programming Languages, POPL’77, pages
238–252, 1977.
[21] P. Cousot and R. Cousot. Systematic design of program analysis
frameworks. In Proceedings of the 6th ACM SIGACT-SIGPLAN
Symposium on Principles of Programming Languages, POPL’79, pages
269–282, New York, NY, USA, 1979.
[22] M. Davis. The undecidable: Basic papers on undecidable propositions,
unsolvable problems and computable functions. Dover Publications,
Incorporated, 2004.
[23] L. De Moura and N. Bjørner. Z3: An efficient SMT solver. In
Proceedings of the Theory and Practice of Software, 14th International
Conference on Tools and Algorithms for the Construction and Analysis

of Systems, TACAS’08/ETAPS’08, pages 337–340, Berlin, Heidelberg,
2008.
[24] E. W. Dijkstra. Notes on structured programming. Apr. 1970.
[25] J. Eckstein and D. P. Bertsekas. On the Douglas—Rachford splitting
method and the proximal point algorithm for maximal monotone
operators. Mathematical Programming, 55(1-3):293–318, 1992.
[26] R. Ferguson and B. Korel. The chaining approach for software test data
generation. ACM Trans. Softw. Eng. Methodol., 5(1):63–86, Jan. 1996.
[27] R. W. Floyd. Assigning meanings to programs. Mathematical aspects
of computer science, 19(19-32):1, 1967.
[28] Z. Fu and Z. Su. XSat: A fast floating-point satisfiability solver. In
Proceedings of the 28th International Conference on Computer Aided
Verification, CAV’16, Toronto, Ontario, Canada, 2016.
[29] Z. Fu, Z. Bai, and Z. Su. Automated backward error analysis for
numerical code. In Proceedings of the ACM SIGPLAN International
Conference on Object-Oriented Programming, Systems, Languages,
and Applications, OOPSLA’15, pages 639–654, Pittsburgh, PA, USA,
2015.
[30] P. Godefroid, N. Klarlund, and K. Sen. DART: Directed automated
random testing. In Proceedings of the ACM SIGPLAN 2005 Conference
on Programming Language Design and Implementation, Chicago, IL,
USA, pages 213–223, 2005.
[31] K. Gödel. Über formal unentscheidbare sätze der principia mathematica
und verwandter systeme i. Monatshefte für mathematik und physik, 38
(1):173–198, 1931.
[32] D. Goldberg. What every computer scientist should know about
floating-point arithmetic. ACM Computing Surveys (CSUR), 23(1):
5–48, 1991.
[33] E. Goubault, S. Le Roux, J. Leconte, L. Liberti, and F. Marinelli.
Static analysis by abstract interpretation: A mathematical programming
approach. Electronic notes in theoretical computer science, 267(1):
73–87, 2010.
[34] S. Heule, M. Sridharan, and S. Chandra. Mimic: Computing models for
opaque code. In Proceedings of the 10th Joint Meeting on Foundations
of Software Engineering, pages 710–720, 2015.
[35] C. A. R. Hoare. An axiomatic basis for computer programming.
Commun. ACM, 12(10):576–580, Oct. 1969.
[36] J. C. King. Symbolic execution and program testing. Commun. ACM,
19(7):385–394, July 1976.
[37] S. Kirkpatrick, C. D. Gelatt, and M. P. Vecchi. Optimization by
simulated annealing. SCIENCE, 220(4598):671–680, 1983.
[38] B. Korel. Automated software test data generation. IEEE Trans. Softw.
Eng., 16(8):870–879, Aug. 1990.
[39] N. Kosmatov, B. Legeard, F. Peureux, and M. Utting. Boundary coverage criteria for test generation from formal models. In Proceedings of
the 15th International Symposium on Software Reliability Engineering,
ISSRE ’04, pages 139–150, Washington, DC, USA, 2004.
[40] J. R. Koza. Genetic programming: On the programming of computers
by means of natural selection, volume 1. MIT press, 1992.
[41] K. Lakhotia, P. McMinn, and M. Harman. An empirical investigation
into branch coverage for C programs using CUTE and AUSTIN.
Journal of Systems and Software, 83(12):2379–2391, 2010.
[42] K. Lakhotia, N. Tillmann, M. Harman, and J. De Halleux. FloPSy:
Search-based floating point constraint solving for symbolic execution.
In Proceedings of the 22Nd IFIP WG 6.1 International Conference
on Testing Software and Systems, ICTSS’10, pages 142–157, Berlin,
Heidelberg, 2010.
[43] K. Lakhotia, M. Harman, and H. Gross. AUSTIN: An open source
tool for search based software testing of C programs. Information and
Software Technology, 55(1):112–125, 2013.
[44] C. Lattner and V. Adve. LLVM: A compilation framework for lifelong
program analysis & transformation. In Proceedings of the International
Symposium on Code Generation and Optimization: Feedback-directed
and Runtime Optimization, CGO ’04, pages 75–86, Washington, DC,
USA, 2004.

[45] D. Leitner, C. Chakravarty, R. Hinde, and D. Wales. Global optimization by basin-hopping and the lowest energy structures of LennardJones clusters containing up to 110 atoms. Phys. Rev. E, 56:363, 1997.

[67] M. Tawarmalani and N. V. Sahinidis. Global optimization of mixedinteger nonlinear programs: A theoretical and computational study.
Mathematical programming, 99(3):563–591, 2004.

[46] Z. Li and H. A. Scheraga. Monte Carlo minimization approach to
the multiple-minima problem in protein folding. Proceedings of the
National Academy of Sciences of the United States of America, 84(19):
6611–6615, 1987.

[68] N. Tillmann and J. De Halleux. Pex: White box test generation for
.NET. In Proceedings of the 2Nd International Conference on Tests
and Proofs, TAP’08, pages 134–153, Berlin, Heidelberg, 2008.

[47] L. Liberti, S. Le Roux, J. Leconte, and F. Marinelli. Mathematical programming based debugging. Electronic Notes in Discrete Mathematics,
36:1311–1318, 2010.
[48] L. Mauborgne and X. Rival. Trace partitioning in abstract interpretation
based static analyzers. In Programming Languages and Systems,
14th European Symposium on Programming, ESOP 2005, pages 5–
20, Edinburgh, UK, 2005.
[49] P. McMinn. Search-based software test data generation: A survey.
Softw. Test. Verif. Reliab., 14(2):105–156, June 2004.
[50] A. M. Memon, I. Banerjee, and A. Nagarajan. What test oracle should I
use for effective GUI testing? In 18th IEEE International Conference on
Automated Software Engineering, ASE 2003, pages 164–173, Montreal,
Canada, 2003.
[51] B. Meyer. Seven principles of software testing. IEEE Computer, 41(8):
99–101, 2008.
[52] W. Miller and D. L. Spooner. Automatic generation of floating-point
test data. IEEE Trans. Softw. Eng., 2(3):223–226, May 1976.
[53] M. Minoux. Mathematical programming: Theory and algorithms.
Wiley, New York, 1986.
[54] G. J. Myers. The art of software testing. pages I–XV, 1–234, 2004.
[55] R. Nieuwenhuis, A. Oliveras, and C. Tinelli. Solving SAT and
SAT modulo theories: From an abstract Davis–Putnam–Logemann–
Loveland procedure to DPLL(T). J. ACM, 53(6):937–977, 2006.
[56] J. Nocedal and S. J. Wright. Numerical optimization. Springer Science
& Business Media, 2006.
[57] H. Palikareva and C. Cadar. Multi-solver support in symbolic execution.
In Proceedings of the 25th International Conference on Computer
Aided Verification, CAV’13, pages 53–68, Berlin, Heidelberg, 2013.
[58] R. Pandita, T. Xie, N. Tillmann, and J. de Halleux. Guided test generation for coverage criteria. In 2010 IEEE International Conference on
Software Maintenance, ICSM’10, pages 1–10, 2010.
[59] W. H. Press, S. A. Teukolsky, W. T. Vetterling, and B. P. Flannery. Numerical recipes 3rd edition: The art of scientific computing. Cambridge
University Press, New York, NY, USA, 2007.
[60] H. Robbins and S. Monro. A stochastic approximation method. The
annals of mathematical statistics, pages 400–407, 1951.
[61] M. Roozbehani, A. Megretski, and E. Feron. Convex optimization
proves software correctness. In Proceedings of American Control
Conference, pages 1395–1400, 2005.
[62] W. Rudin. Principles of mathematical analysis. McGraw-Hill, New
York, 3 edition, 1976.
[63] E. Schkufza, R. Sharma, and A. Aiken. Stochastic optimization of
floating-point programs with tunable precision. In Proceedings of the
35th ACM SIGPLAN Conference on Programming Language Design
and Implementation, PLDI ’14, pages 53–64, New York, NY, USA,
2014.
[64] K. Sen, D. Marinov, and G. Agha. CUTE: A concolic unit testing
engine for C. In Proceedings of the 10th European Software Engineering Conference Held Jointly with 13th ACM SIGSOFT International
Symposium on Foundations of Software Engineering, ESEC/FSE-13,
pages 263–272, New York, NY, USA, 2005.
[65] J. P. M. Silva and K. A. Sakallah. GRASP: A new search algorithm
for satisfiability. In Proceedings of the 1996 IEEE/ACM International
Conference on Computer-aided Design, ICCAD ’96, pages 220–227,
Washington, DC, USA, 1996.
[66] M. Souza, M. Borges, M. d’Amorim, and C. S. Păsăreanu. CORAL:
Solving complex constraints for symbolic pathfinder. In NASA Formal
Methods Symposium, pages 359–374, 2011.

[69] E. J. Weyuker. On testing non-testable programs. Comput. J., 25(4):
465–470, 1982.
[70] L. J. White and E. I. Cohen. A domain strategy for computer program
testing. IEEE Trans. Softw. Eng., 6(3):247–257, May 1980.
[71] G. Zoutendijk. Mathematical programming methods. North-Holland,
Amsterdam, 1976.

A.

Untested Programs in Fdlibm

The programs from the freely distributed math library Fdlibm 5.3 [3]
are used as our benchmarks. Tab. 5 lists all untested programs and
functions, and explains the reason why they are not selected. Three
types of the functions are excluded from our evaluation. They are (1)
functions without any branch, (2) functions involving non-floatingpoint input parameters, and (3) static C functions.

B.

Implementation Details

As a proof-of-concept demonstration, we have implemented Algo. 1
in the tool CoverMe. This section presents the implementation and
technical details omitted from the main body of the paper.
B.1

Frontend of CoverMe

The frontend implements Step 1 and Step 2 of Algo. 1. CoverMe
compiles the program under test FOO to LLVM IR with Clang [2].
Then it uses an LLVM pass [6] to inject assignments in FOO. The program under test can be in any LLVM-supported language, e.g., Ada,
the C/C++ language family, or Julia. Our current implementation
accepts C code only.
Fig. 9 illustrates FOO as a function of signature type_t FOO
(type_t1 x1, type_t2 x2, ...). The return type (output) of the
function, type_t, can be any kind of types supported by C, whereas
the types of the input parameters, type_t1, type_t2, ..., are
restricted to double or double*. We have explained the signature of
pen in Def. 3.7. Note that CoverMe does not inject pen itself into
FOO, but instead injects assignments that invoke pen. We implement
pen in a separate C++ file.
The frontend also links FOO_I and FOO_R with a simple program
loader to generate a shared object file libr.so, which is the
outcome of the frontend. It stores the representing function in the
form of a shared object file (.so file).
B.2

Backend of CoverMe

The backend implements Step 3 of Algo. 1. It invokes the representing function via libr.so. The kernel of the backend is an
external MCMC engine. It uses the off-the-shelf implementation
known as Basinhopping from the Scipy Optimization package [7].
Basinhopping takes a range of input parameters. Fig. 9 shows
the important ones for our implementation basinhopping(f, sp,
n_iter, call_back), where f refers to the representing function
from libr.so, sp is a starting point as a Python Numpy array, n_iter
is the iteration number used in Algo. 1 and call_back is a clientdefined procedure. Basinhopping invokes call_back at the end of
each iteration (Algo. 1, Lines 24-34). The call_back procedure allows CoverMe to terminate if it saturates all branches. In this way,
CoverMe does not need to wait until passing all n_start iterations
(Algo. 1, Lines 8-12).

Table 5: Untested programs and functions in benchmark suite Fdlibm and the corresponding explanations.
Program

Entry function

Explanation

e_gamma_r.c
e_gamma.c
e_j0.c

ieee754_gamma_r(double)
ieee754_gamma(double)
pzero(double)
qzero(double)
pone(double)
qone(double)
ieee754_jn(int, double)
ieee754_yn(int, double)
sin_pi(double)
ieee754_lgammar_r(double, int*)
ieee754_lgamma(double)
kernel_rem_pio2(double*, double*, int, int, const int*)
kernel_sin(double, double, int)
kernel_standard(double, double, int)
kernel_tan(double, double, int)
copysign(double)
fabs(double)
finite(double)
frexp(double, int*)
isnan(double)
ldexp(double, int)
lib_versioin(double)
matherr(struct exception*)
scalbn(double, int)
signgam(double)
significand(double)
acos(double)
acosh(double)
asin(double)
atan2(double, double)
atanh(double)
cosh(double)
exp(double)
fmod(double, double)
gamma_r(double, int*)
gamma(double, int*)
hypot(double, double)
j0(double)
y0(double)
j1(double)
y1(double)
jn(double)
yn(double)
lgamma_r(double, int*)
lgamma(double)
log(double)
log10(double)
pow(double, double)
remainder(double, double)
scalb(double, double)
sinh(double)
sqrt(double)

no branch
no branch
static C function
static C function
static C function
static C function
unsupported input type
unsupported input type
static C function
unsupported input type
no branch
unsupported input type
unsupported input type
unsupported input type
unsupported input type
no branch
no branch
no branch
unsupported input type
no branch
unsupported input type
no branch
unsupported input type
unsupported input type
no branch
no branch
no branch
no branch
no branch
no branch
no branch
no branch
no branch
no branch
no branch
no branch
no branch
no branch
no branch
no branch
no branch
no branch
no branch
no branch
no branch
no branch
no branch
no branch
no branch
no branch
no branch
no branch

e_j1.c
e_jn.c
e_lgamma_r.c
e_lgamma.c
k_rem_pio2.c
k_sin.c
k_standard.c
k_tan.c
s_copysign.c
s_fabs.c
s_finite.c
s_frexp.c
s_isnan.c
s_ldexp.c
s_lib_version.c
s_matherr.c
s_scalbn.c
s_signgam.c
s_significand.c
w_acos.c
w_acosh.c
w_asin.c
w_atan2.c
w_atanh.c
w_cosh.c
w_exp.c
w_fmod.c
w_gamma_r.c
w_gamma.c
w_hypot.c
w_j0.c
w_j1.c
w_jn.c
w_lgamma_r.c
w_lgamma.c
w_log.c
w_log10.c
w_pow.c
w_remainder.c
w_scalb.c
w_sinh.c
w_sqrt.c

FOO:

Program under test
in any LLVM-supported language
type_t FOO (double x1, double x2, ...)

pen

(.cpp)

double pen (int i, int op, double lhs, double rhs)

FOO_I:

Instrumented program (.bc)

Dealing with Comparison between Non-floating-point Expressions (Relaxing Def. 3.1(b)). We have encountered situations
loader (.cpp)
where a conditional statement invokes a comparison between non
FOO:: Program
Program under
test test
FOO
under
floating-point numbers. CoverMe handles these situations by first
FOO:LOADER
Program
under
test
void
(double
P) test
FOO
: Program
under
in any
LLVM-supported
language
FOO: Program
under
test * language
FOO
: Program
in
any
LLVM-supported
languageunder test
in
any
LLVM-supported
in
any
LLVM-supported
language
promoting the non floating-point numbers to floating-point numbers
FOO: Program under
_Rtest
FOO
:
Program
under
test
FOO
(.cpp)
type_t FOO (double
x1, double
x2,
...)
in any LLVM-supported
language
indouble
any
LLVM-supported
FOO
: Program under testlanguageand then injecting pen as described in Algo. 1. For example, before a
_t (double
type__
tFOO
FOO
x1, double
x2, ...)
type
FOO
(double
x1,
x2, ...)
:
Program
under
test
type t FOO
(double
double x2, ...) language
in any LLVM-supported
language
in
anyx1,
LLVM-supported
void FOO_R (double
in any LLVM-supported language
* P)
: Program
under
test
pen
(.cpp)
_t FOO
_t FOO language
conditional statement like if (xi op yi) where xi and yi are inteFOO
: Program
under
test
typeFOO
(double
x1, LLVM-supported
double
x2,
...)
pen
(.cpp)
type
(double x1, double x2, ...)
pen
in (.cpp)
any
type_t x1,
FOO (double
double
type_FOO
t FOO
(double
x1,
double
x2,
...)
_
libr.so
type
t
FOO
(double
doublex1,
x2,
...)x2, ...)
:
Program
under
test
pen
(.cpp)
in any LLVM-supported
language
double
pen(int
(int
int
op,
double
gers, CoverMe injects r = pen (i, op, (double) x, (double)
any
LLVM-supported
language
double
pen
i, i,
int
op,
double
lhs,lhs,
double
rhs) rhs)
double
pen
(int
i,
int
op,double
double
lhs,
double
rhs)
FOO
:
Program
under
test
FOO: Programinunder
test
_t FOO (double x1, double x2, ...)
type
(.cpp)
FOO: Program
under
test pen (.cpp)
_R (double
pen (.cpp)
ininpen
any
LLVM-supported
language
FOO
y));. Note that such an approach does not allow us to handle data
* P)
anytype
LLVM-supported
language
_
_t void
_(double
_
FOO
I
:
Instrumented
program
(.bc)
in
any
LLVM-supported
language
double
pen
(int
i,
int
op,
double
lhs,
double
rhs)
pen (.cpp)
FOO
x1,
double
x2,
...)
FOO
I
:
Instrumented
program
(.bc)
FOO
I
:
Instrumented
program
(.bc)
_
pen (.cpp)
type
FOO (double
x1,
double x2, ...)
in anytLLVM-supported
language
double
pen rhs)
(int
i, int
op,double
double lhs,
double
types
thatrhs)
arerhs)
incompatible with floating-point types, e.g., conditions
_t FOOpen
double
(int
i,
int
op,
double
lhs,
double
type
(double
x1,
double
x2,
...)
double
pen
(int
i,
int
op,
lhs,
double
_
pen
(.cpp)
MCMC
minimization
procedure
(.py)
FOO
:
Program
under
test
_type
_t_I_
_(double
type t FOO (double
x1,
double
x2,
...)
type
t_tFOO
x1,
double
x2, x2,
...)
type
FOO
I(double
x1,
FOO
I (double
x1,double
double
x2, ...)
...)
_t
_t _
type
FOO
(double
double
x2,double
...) rhs)
typeint
FOO
x1, double
x2,
...)
double penpen
(int(.cpp)
i,
double
lhs,
double
rhs)
double
pen
(int
i,
int op,x1,
double
lhs,
FOO
Iop,
: (double
Instrumented
program
(.bc)
(p != Null), which CoverMe has to ignore.
_ILLVM-supported
inFOO
any
language
pen
(.cpp)
: Instrumented
program
(.bc)like if
basinhopping
(func,
sp, n_iter, callback)
pen (.cpp)
FOO
:
Program
under
test
loader
(.cpp)
_I: Instrumented
double
pen
(intFOO
i, _
int
op, double lhs,
double rhs)
loader
(.cpp)
(.cpp)
FOO(.cpp)
program
(.bc)
I: Instrumented
program
(.bc)
FOO
: Program
under
test
penloader
(.cpp)
pen
_t_tFOO
_I...)
_program
_Iint
type
x1, x1,
double
x2,x2,
...)
type
FOO(double
(double
double
...)
pen
_int
type
tpen
FOO
(double
x1,(.cpp)
double
x2,
FOO_Idouble
: Instrumented
(.bc)
double
pen
(int
i,
op,
lhs,
double
rhs)
pen
(int
i,
int
op,
double
lhs,
rhs)
in
any
LLVM-supported
language
FOO
Idouble
:double
Instrumented
program
(.bc)
double
(int
i,
lhs,
double
rhs)
Dealing
with Infeasible Branches (Relaxing Def. 3.1(c)). Infeavoid
LOADER
(double
LLVM
pass
in
any
LLVM-supported
language
void
LOADER
(double
* P)
* P)op, double
void
LOADER
(double
* P)
double
pen
(int
i,
int
op,
double
lhs,
double
rhs)
_
_
_
_
_
type tpen
FOO(int
I (double
x1,
double
x2,
...)
type
t
FOO I (double
x1, double x2, ...)
FOO
I
:
Instrumented
program
(.bc)
double
i,
int
op,
double
lhs,
double
rhs)
loader
(.cpp)
Linking
pen
(.cpp)
_(.bc)
_I_:IInstrumented
sible
branches
type
t
FOO
(double
x1,
double
x2,
...)
_
program
double
pen
(int
i,
int
op,
double
lhs,
double
rhs)are branches that cannot be covered by any input. At_
type_tFOO
FOO
(double
x1,
double
x2,
...)
_
_
_
FOO
R
(.cpp)
_
FOO
R
(.cpp)
type
x1,
double
x2,
...)
type
t FOO
I
(double
x1, double x2, ...)
loader
(.cpp)
FOO tIFOO
:FOO
Instrumented
program
(.bc)
FOO
RInstrumented
(.cpp)
__I(double
I:_:Instrumented
program
(.bc)
FOO
(.bc)
_t
_program
void
LOADER
(double
P) double lhs,
tempts
cover infeasible branches are useless and time-consuming.
double
pen
(int
i, int
doubleto
rhs)
type
I...)
(double
x1,
double
x2,
...)
* op,
_I(.cpp)
_Rdouble
_R FOO
type
(double
x1,
x2,
loader
__tI:FOO
void void
FOO
(double
P)
pen
(.cpp)
FOO
(double
P)loader (.cpp)
*
*
FOO
Instrumented
program
(.bc)
_x2,
__
_I_R(double
void
FOO
_t type
* P)
x1,
double
FOO
Ix2,
: ...)
Instrumented
void
loader
(double
P)
loader (.cpp)
type(.cpp)
FOO
(double
x1,
double
...)
_ttIFOO
_I(double
*(.cpp)
pen
loader
type
FOO
(double
x1,
double
x2,
...) program (.bc) Detecting infeasible branches is a difficult problem in general.
_double
FOO
(.cpp)
FOO
:libr.so
Program
under
doubletest
pen (int i, int FOO
op,
lhs, double program
rhs)
I_:RInstrumented
(.bc)
loader
(.cpp)
libr.so
void
loader
(double
void
loader (double* P)
_t FOO
_I (double
loader
(.cpp)
* P)double
type
x1,
x2,
...)
libr.so
loader
(.cpp)
_
_
uses a simple heuristic to detect and ignore infeasible
in pen
any
LLVM-supported
language
type
t (double
FOO
(double
x1,
x2,CoverMe
...)
void loader
(double
P)
_FOO
void
(double
P) double
*(int
i,
op,
double
lhs,
double
rhs)
loader
_tIFOO
* x1,
_
FOO
RP)_(.cpp)
(.cpp)
_Rint
loader
(.cpp)
type
FOO
(double
double x2, ...)
*__RIP)
void
RFOO
(double
P) * P)
FOO
Ivoid
: Instrumented
program
(.bc)
voiddouble
LOADER loader
(double
(double
*
*void
_R(double
branches.
When CoverMe finds a minimum that is not zero, that
FOO
(double
void
LOADER
_R (.cpp)
_void
void
loader
(double
P)
_
*P)P)
type
t FOO
(double
x1,* double
x2, ...)
*
FOO
FOO
R
(.cpp)
loader
(.cpp)
_t FOO_I (double x1, libr.so
double
x2, ...)
_R void
_Rtype
MCMC
minimization
(.py)
MCMC
minimization
procedure
(.py)(.cpp)
loader
(.cpp)
_I:loader
(.cpp)
void
FOO
(double
P)
FOO_RFOO
(.cpp)
(double
P)_procedure
FOO
Instrumented
program
*
FOO
R**loader
(.cpp)
is, FOO_R(x∗ ) > 0, CoverMe deems the unvisited branch of the
void
loader
(double
P) (.bc)
_R (.cpp)
FOO
MCMC
minimization
procedure
(.py)
pen
(.cpp)
_
_R (double
_R (double
void
FOO R (double
_iter,
voidFOO
FOO
P)
void
FOO
* P)
FOO
R(func,
(.cpp)
basinhopping
sp, nsp,
callback)
_R (double
loader
(.cpp)
basinhopping
(func,
n_iter,
callback)
** _
* P)
void
void
loader
(double
P)
void
LOADER (double
* P)
* P)
last conditional to be infeasible and adds it to Saturate, the set
void
loader
(double
void FOO_Rtype
(double
P)
__tdouble
_
_R (double
* P)
*basinhopping
_R
void
P)
FOO
I (double
x1,
x2,
...)
void
FOO
(double
P)
libr.so
*
sp,
n_
iter,
callback)
FOO
RFOO
(.cpp)
* rhs)
_FOO
pen
(int i, (func,
int
op,double
double
lhs,
double
R (.cpp)
void
LOADER (double* P) MCMC minimization procedure (.py)
LLVM
pass
LLVM
pass
_
of unvisited and deemed-to-be infeasible branches.
_
libr.so
void FOO R (double
FOO R (.cpp)
* P)
libr.so
_R (.cpp)
libr.so
FOO
libr.so
__IR: Linking
_R (.cpp)
_Rpass
LLVM
Instrumented
Linking
FOO
void
FOO
P)(.bc)
_P)
libr.so
void FOO
FOO
(double
basinhopping (func, sp, n_iter, callback)
R program
(.cpp)
(.cpp)
*(double
libr.so
Imagine that we modify l1 of the program FOO in Fig. 3 to the
void
(double
void loader
FOO_R (double
P) _R FOO
* *P)
* FOO
void FOO_R (double* P)
_
_
Linking
void
(double
P) double
voidFOO
FOO
R(double
(double
void
FOO
_t FOO
_R
_R_type
libr.so
* x1,
FOO
x2,P)
...) R (double* P)
void
P)P)
_R (double
*I *(double
void FOO
conditional statement if (y == -1). Then the branch 1T becomes
* FOO_R LLVM
_R void
pass
void
(double
P)
void FOO
(double
P)
_
*
*
loader
(double
P)
MCMC
minimization
procedure
(.py)
void
FOO
R
(double
P)
MCMC
minimization
procedure
(.py)
*
libr.so
*
libr.so
libr.so
MCMC
minimization
procedure P)
(.py)
Linking
infeasible. We rewrite this modified program below and illustrate
(.cpp)
void
FOO_R (double
libr.so
*
MCMC loader
minimization
(.py)
minimization
procedure (.py)
basinhopping
(func, sp, n_iter,procedure
callback)MCMC
libr.so
FOO_
R (double* P)
_void
_R (double
_RFOO
libr.so
basinhopping
(func,
sp,
n
iter,
callback)
MCMC
minimization
procedure
(.py)
_P)
void
P)
_
basinhopping
(func,
sp,
n
iter,
callback)
FOO
(.cpp)
*
MCMC
minimization
procedure (.py) how we deal with infeasible branches.
void
FOO
R
(double
_R*(double* P)
void LOADER (double
P)
void *
FOO
_iter,basinhopping
_iter, callback)
basinhopping
(func,
sp, nminimization
callback)
LLVM
(func,(.py)
sp, n
MCMC
procedure
void
FOO_Rpass
(double
P)
MCMC
minimization
procedure
(.py)
* npass
_R (double
_iter,
LLVM
void FOO
P)
basinhopping
(func,
sp,
callback)
FOO__RR
(.cpp)
void
FOO
(double
P)
MCMC
minimization
procedure
(.py)
basinhopping
(func,
sp,
n*_iter,
callback)l0: if (x <= 1) {x++};
LLVM
*pass
MCMC
minimization
procedure
(.py)
Linking
MCMC
minimization
procedure
(.py)
_
Linking
basinhopping
(func,
sp,
n
basinhopping
(func,
sp,
n pass
iter,
callback)_iter, callback)y = square(x);
LLVM
pass
_
LLVM
_
basinhopping
(func,
sp,
n
iter,
callback)
void
FOO
R
(double
P)
MCMC
minimization
(.py)
*
Linkingprocedure
MCMC
minimization
procedure (.py)
LLVM
pass
basinhopping
sp, LLVM
n_sp,
iter,
callback)
libr.so
pass
basinhopping
n_
iter,
callback)
Back-end:
Minimize
the (func,(func,
l1: if (y == -1) {...}
LLVM
pass
Linking
Linking
LLVM
pass
libr.so
_iter,
LLVM
pass
basinhopping
(func, sp,
n
callback)
Linking
representing
function
_iter, callback)
Linking
Linking
basinhopping
(func,
sp,
n
voidLLVM
FOO_R (double
P)
Linking
* P)
pass
_R (double
LLVM
pass
void FOO
Linking
*
where we omit the concrete implementation of square.
LLVM
passLinking
Linking
Let FOO_R denote the representing function constructed for the
MCMC
minimization procedure
procedureLLVM
(.py)
MCMC
minimization
(.py)pass
Linking
program. In the minimization process, whenever CoverMe obtains
Linking
basinhopping (func, sp, n__
iter, callback)
basinhopping (func, sp, n iter, callback)
x∗ such that FOO_R(x∗ ) > 0, CoverMe selects a branch that it regards
LLVM pass
infeasible. CoverMe selects the branch as follows: Suppose x∗
LLVM
pass
Linking
exercises a path τ whose last conditional statement is denoted by lz ,
Generated
test
inputs
Linking Generated test inputs
and, without loss of generality, suppose zT is passed through by τ,
X: A set ofX:
FOO
R’s of
global
then CoverMe regards zF as an infeasible branch.
A_set
FOO_minimum
R’s global points
minimum points
In the modified program above, if 1F has been saturated, the
representing function evaluates to (y + 1)2 or (y + 1)2 + 1, where y
Figure 9: CoverMe Implementation.
equals to the non-negative square(x). Thus, the minimum point x∗
must satisfy FOO_R(x∗ ) > 0 and its triggered path ends with branch
1F . CoverMe then regards 1T as an infeasible branch.
CoverMe then regards the infeasible branches as already satuB.3 Technical Details
rated. It means, in line 12 of Algo. 1, CoverMe updates Saturate
with saturated branches and infeasible branches (more precisely,
Sect. 3 assumes Def. 3.1(a-c) for the sake of simplification. This
branches that CoverMe regards infeasible).
section discusses how CoverMe relaxes the assumptions when hanThe presented heuristic works well in practice (See Sect. 5), but
dling real-world floating-point code. We also show how CoverMe
we do not claim that our heuristic always correctly detects infeasible
handles function calls at the end of this section.
branches.
Dealing with Pointers (Relaxing Def. 3.1(a)) We consider only
Dealing with Function Calls. By default, CoverMe injects r =
pointers to floating-point numbers. They may occur (1) in an input
peni only in the entry function to test. If the entry function invokes
parameter, (2) in a conditional statement, or (3) in the code body but
other external functions, they will not be transformed. For example,
not in the conditional statement.
in the program FOO of Fig. 3, we do not transform square(x). In
CoverMe inherently handles case (3) because it is executionthis way, CoverMe only attempts to saturate all branches for a single
based and does not need to analyze pointers and their effects.
function at a time.
CoverMe currently does not handle case (2) and simply ignores
However, CoverMe can also easily handle functions invoked by
these conditional statements by not injecting pen before them.
its entry function. As a simple example, consider:
Below we explain how CoverMe deals with case (1). A branch
coverage testing problem for a program whose inputs are pointers
void FOO(double x) {GOO(x);}
void GOO(double x) {if (sin(x) <= 0.99) ... }
to doubles, can be regarded as the same problem with a simplified program under test. For instance, finding test inputs to cover
If CoverMe aims to saturate FOO and GOO but not sin, and it sets
branches of program void FOO(double* p) {if (*p <= 1)... }
FOO as the entry function, then it instruments both FOO and GOO. Only
_
_
_
can be reduced to testing the program void FOO with no pointer
GOO has a conditional statement, and CoverMe injects an assignment
(double x) {if (x <= 1)... }. CoverMe transforms program
on r in GOO.
_
_
_
FOO to FOO with no pointer if a FOO’s input parameter is a
floating-point pointer.
Front-end: Construct
the
_t FOO_I
type
representing function

(double x1, double x2, ...)

