# Faster SAT Solving for Software with Repeated Structures
(with Case Studies on Software Test Suite Minimization)

Jianfeng Chen<EMAIL_ADDRESS>Xipeng Shen<EMAIL_ADDRESS>Tim Menzies
<EMAIL_ADDRESS>Department of Computer Science, NC State University, NC

###### Abstract

Theorem provers has been used extensively in software engineering for software
testing or verification. However, software is now so large and complex that
additional architecture is needed to guide theorem provers as they try to
generate test suites. The Snap test suite generator (introduced in this paper)
combines the Z3 theorem prover with the following tactic: cluster some
candidate tests, then search for valid tests by proposing small mutations to
the cluster centroids. This technique effectively removes repeated structures
in the tests since many repeated structures can be replaced with one centroid.
In practice, Snap is remarkably effective. For 27 real-world programs with up
to half a million variables, Snap found test suites which were 10 to 750
smaller times than those found by the prior state-of-the-art. Also, Snap ran
orders of magnitude faster and (unlike prior work) generated 100% valid tests.

###### keywords:

SAT solvers , Test suite generation , Mutation

††journal: Journal of Systems and Software

##  1 Introduction

Many software problems can be transformed into “SAT”; i.e. a propositional
satisfiability problem [1, 2, 3, 4, 5, 6, 7]. For example, Fig. 1 shows the
different branches of program being translated into a propositional
formula111A propositional formula is constructed from simple propositions,
such as ”five is greater than three” or propositional variables such as P and
Q, using connectives or logical operators such as not, AND, OR, or IMPLIES;
for example: (P AND NOT Q) IMPLIES (P OR Q).. Test cases can be automatically
generated by theorem provers that solve for the constraints in those formula.
After decades of research, such theorem provers can process impressively
complex formula. As Micheal Lowry said at a panel at ASE’15:

> “It used to be that reduction to SAT proved a problem’s intractability. But
> with the new SAT solvers, that reduction now demonstrates practicality.”

However, in practice, there is a problem. General SAT solvers, such as the Z3
[8], MathSAT [9], vZ [10] et al., are challenged by the complexity of real-
world software models. For example, the largest benchmark for SAT Competition
2017 [11] had 58,000 variables – which is far smaller than (e.g.) the 300,000
variable problems seen in the recent SE testing literature [12].

We diagnosis the problem with SAT solvers as follows: they are looking too
closely at specific details. Recent work, presented in §2.2 suggests that
modern software systems contain many repeated structures. If so, we would
expect test suite generators to waste time generating many very similar
solutions. This is indeed the case. For example, in one sample of 10 million
tests generated from the blasted_case47 (a problem described later in this
paper), the QuickSampler tool from ICSE’18 [12], only found 26,000 unique
valid solutions. That is, 99% of the tests QuickSampler was repeating other
tests.

This paper asks if structural replication can be used to design better solvers
for SE tasks. Our case study will be test suite minimization. The Snap test
suite generator (introduced in this paper) combines Z3 with the following
tactic:

> Cluster candidate tests, then search for valid tests by via small mutations
> to the cluster centroids.

This technique effectively removes repeated structures in the tests since many
repeated structures can be replaced with one centroid. In practice, Snap is
remarkably effective. For 27 real-world programs with up to half a million
variables, Snap found test suites which were 10 to 750 smaller times than
those found by the prior state-of-the-art. Also, Snap ran orders of magnitude
faster and (unlike prior work) generated 100% valid tests. Note that:

  * •

This document will use the terms “tests”, “test cases”, or “SAT solutions”
interchangeably since we address the software testing task as a (transformed)
SAT task.

  * •

An open-source version of Snap (and all SE models used in this paper) is
freely available on-line222 http://github.com/ai-se/SatSpaceExpo.

    1 int mid(int x, int y, int z) {
    2  if (x < y) {
    3    if (y < z) return y;
    4    else if (x < z) return z;
    5    else return x;
    6  } else if (x < z) return x;
    7  else if (y < z) return z;
    8  else return y; }

The code above has the six branches shown below. Each branch is a logical
constraint $C_{1}\vee C_{2}\vee C_{3}\ldots\vee C_{6}$. A valid test selects
x, y, z such that it satisfies these constraints.

    path 1: [C1: x < y < z] L2->L3
    path 2: [C2: x < z < y] L2->L3->L4
    path 3: [C3: z < x < y] L2->L3->L4->L5
    path 4: [C4: y < x < z] L2->L6
    path 5: [C5: y < z < x] L2->L6->L7
    path 6: [C6: z < y < x] L2->L6->L7->L8

Note: 1) as x, y and z are integers, we could use (say) 7 bits to representing
them; 2) the arithmetic conditions, ie. the SMT form(Satisfiability Modulo
Theories) [13] can be translated into norm formulas via SMT conversion tools
[14]. By convention, the disjunction $\vee C_{i}$ is transformed into the
conjunction normal form (CNF) $C_{1}^{\prime}\wedge C_{2}^{\prime}\ldots$. A
valid assignment to the CNF, i.e. the assignment that fulfills all clauses, is
corresponding to a test case, covering some branch of code. Figure 1: A script
of C programming can be translated into CNF (conjunctive normal form).

##  2 Background

###  2.1 Why Explore Test Suite Minimization?

When changing software, it is useful to test if the new work damages old
functionality. For this reason, testing and re-testing code is widely applied
in both open-source projects and closed-source projects [15, 16, 17].

When developers extend a code base, test suites let them check that their new
work does not harm old functionality. Such tests mean that developers can find
and fix more faults, sooner. Hence, better tests enable faster code
modification [15, 16, 18].

By minimizing the number of tests executed, we also minimize the developer
efforts required to specify the expected behavior associated with each test
execution [19]. If testing for (e.g.) core dumps, then specifying off-nominal
behavior is trivial (just look for a core dump file). But in many other cases,
specifying what should (and should not) be seen when a test executes is a
time-consuming task requiring a deep understanding of the purpose and context
of the software.

Smaller tests suites are also cheaper to run. The industrial experience is
that excessive testing can be onerously expensive, especially when run after
each modification to software [19]. Such high-frequency testing can grow to
80% of the software maintenance effort [19, 20]. Many current organizations
spend tens of millions of dollars each year (or more) on cloud-based
facilities to run large tests suites [19]. The fewer the tests those
organizations have to run, the cheaper their testing.

Smaller test suites are faster to execute. If minimal and effective test
suites can be generated, within a fixed time limit, more faults can be found
and fixed [19]. Faster test execution means that software teams can certify a
new release, quicker. This is important for organizations using continuous
integration since faster test suites mean they can make more releases each day
– which means that clients can sooner receive new (or fixed) features [21].

Generating test suites can be difficult. Good test suite generators must
struggle to achieve several goals:

  1. 1.

Terminate quickly;

  2. 2.

Scale to large programs;

  3. 3.

Return small test suites that contain valid tests;

  4. 4.

Cover most program branches;

  5. 5.

Minimize test suite redundancy.

In practice, the test suite generation problem is a complex problem that
requires extra machinery to guide the theorem provers. For example, Snap’s
extra machinery knows how to avoid repeated structures. As as result Snap runs
very fast, and generates such small test suites.

###  2.2 Repeated Structures in Software

This section presents evidence of structural repetition in software.
Historically, this evidence lead to the design of Snap.

A repeated observation is that apparently complex software can be controlled
by just a few key variables. Just to say the obvious, controlling a system
containing a few keys is just a simple matter of finding the keys then
changing each of the key’s settings. More specifically, when applied to test
case generation, test suites get smaller if they only use the key variables.

One way to see how many keys are in a software system is to ask how many
“prototypes” (minimum number of exemplars) are required to model that system.
If the keys are few, a few examples are enough to model a system; e.g.
software with 8 binary keys only needs $2^{8}=256$ examples. There are many
different ways to find those exemplars [22] but in a result that endorses
keys, the number of required exemplars is often very small, even for seemingly
complex systems. For example, we have successfully modelled security
violations in 28,750 Mozilla functions with 271 exemplars and 6000 commits
from Github using 300 exemplars [23]. And even in the deep learning world,
there are very recent results [24] with “less than one”-short learning
suggesting that it is possible and useful to synthesize a small number of
artificial exemplars by aggregating across multiple examples.

Table 1: Snap and its related work for solving theorem proving constraints via sampling. Reference | Year |  Citation | Sampling methodology |  Case study size (max$|$variables$|$) |  Verifying samples |  Distribution/ diversity reported
---|---|---|---|---|---|---
[25] | 1999 |  105 | Binary Decision Diagram |  $\approx$1.3K |  [scale=0.12](0,0) circle (1); [fill=black] (0,0) – (90:1) arc (90:90-0*3.6:1) – cycle; |  [scale=0.12](0,0) circle (1); [fill=black] (0,0) – (90:1) arc (90:90-0*3.6:1) – cycle;
[26] | 2003 |  50 | Interval-propagation-based |  200 |  [scale=0.12](0,0) circle (1); [fill=black] (0,0) – (90:1) arc (90:90-0*3.6:1) – cycle; |  [scale=0.12](0,0) circle (1); [fill=black] (0,0) – (90:1) arc (90:90-0*3.6:1) – cycle;
[27] | 2004 |  54 | Binary Decision Diagram |  $<1$K |  [scale=0.12](0,0) circle (1); [fill=black] (0,0) – (90:1) arc (90:90-0*3.6:1) – cycle; |  [scale=0.12](0,0) circle (1); [fill=black] (0,0) – (90:1) arc (90:90-0*3.6:1) – cycle;
[28] | 2004 |  141 | Random Walk + WalkSat | No experiment conducted
[29] | 2011 |  88 | Sampling via determinism |  6k |  [scale=0.12](0,0) circle (1); [fill=black] (0,0) – (90:1) arc (90:90-0*3.6:1) – cycle; |  [scale=0.12](0,0) circle (1); [fill=black] (0,0) – (90:1) arc (90:90-0*3.6:1) – cycle;
[30] | 2012 |  25 |  MaxSat \+ Search Tree | Experiment details not reported
[31] | 2014 |  29 | Hashing based |  400K |  [scale=0.12](0,0) circle (1); [fill=black] (0,0) – (90:1) arc (90:90-0*3.6:1) – cycle; |  [scale=0.12](0,0) circle (1); [fill=black] (0,0) – (90:1) arc (90:90-50*3.6:1) – cycle;
[32] | 2015 |  28 | Hashing based (paralleling) |  400K |  [scale=0.12](0,0) circle (1); [fill=black] (0,0) – (90:1) arc (90:90-0*3.6:1) – cycle; |  [scale=0.12](0,0) circle (1); [fill=black] (0,0) – (90:1) arc (90:90-50*3.6:1) – cycle;
[33] | 2016 |  29 | Universal hashing |  400K |  [scale=0.12](0,0) circle (1); [fill=black] (0,0) – (90:1) arc (90:90-0*3.6:1) – cycle; |  [scale=0.12](0,0) circle (1); [fill=black] (0,0) – (90:1) arc (90:90-50*3.6:1) – cycle;
[12] | 2018 |  5 | Z3 + Eq. 1 flipping |  400K |  [scale=0.12](0,0) circle (1); [fill=black] (0,0) – (90:1) arc (90:90-0*3.6:1) – cycle; |  [scale=0.12](0,0) circle (1); [fill=black] (0,0) – (90:1) arc (90:90-50*3.6:1) – cycle;
Snap | 2020 |  this paper | Z3 + Eq. 1 \+ local sampling |  400K |  [scale=0.12](0,0) circle (1); [fill=black] (0,0) – (90:1) arc (90:90-100*3.6:1) – cycle; |  [scale=0.12](0,0) circle (1); [fill=black] (0,0) – (90:1) arc (90:90-100*3.6:1) – cycle;
[scale=0.12](0,0) circle (1); [fill=black] (0,0) – (90:1) arc (90:90-0*3.6:1)
– cycle; / [scale=0.12](0,0) circle (1); [fill=black] (0,0) – (90:1) arc
(90:90-100*3.6:1) – cycle; : the absence / presence of corresponding item
[scale=0.12](0,0) circle (1); [fill=black] (0,0) – (90:1) arc (90:90-50*3.6:1)
– cycle; : only partial case studies (the small case studies) were reported

The presence of keys illustrate why a few variables can be enough to model
software (e.g. in the tiny test suites generated later in this article). For
example, effective defect prediction or effort estimation is possible using
less than half a dozen variables [34, 35]. Additionally, configuring complex
systems is often remarkably simple and effective and can be achieved using
very small decision trees that only require a few variables [36]. Further, by
generating tests only for the main branches in the code, even applications
that process large cloud databases can be tested via just a few dozen inputs
[37]. As to what causes the keys, we see two possibilities: naturalness and
power laws.

Naturalness: Hindle and Devanbu wrote at ICSE’12 that “Programming languages,
in theory, are complex, flexible and powerful, but the programs that real
people actually write are mostly simple and rather repetitive, and thus they
have … statistical properties that can be captured in … models and leveraged
for SE tasks.” [38] To say that another way, computer programs are written
using a programming language and “language” is a technology that humans have
been using for millennia to enable succinct communication. Repeated structures
simplify communication since they let the observer learn expected properties
of a “typical” systems. This means, in turn, they can recognize when some part
of a system is anomalous (because it lacks the usually repeated structures)
[39]. Consequently, when we write things in a language (human or programming)
then the frequency counts of those things usually correspond to Zipf’s law;
i.e. our words and our code repeats a small number of things very often and a
large number of other things very rarely [40].

Power-laws: Code is written by people. The social interactions between people
mean that those humans focus their work on tiny parts of the code (see Lin and
Whitehead at MSR’15 [41]). To see this, consider a large system with modules
A,B,C,D…. Developer1 may only understand a small part of the code; e.g module
A. If Developer2 asks for help, then Developer1 will teach more about A than
B,C,D. When this cycle is repeated for Developer3, Developer4, etc then we
will observe these programmers know more and more about only a small part of
the code. Hence it is hardly surprising that 20% of the code contains 80% of
the errors since developers mostly work in small corners of a code base.
Again, just to state the obvious, power laws explain keys; i.e. keys are
created when core effects are localized to a few regions in the code.

In summary, for many reasons, it should be expected that software often
contains numerous repeated structures. Hence, it makes sense to adjust (e.g.)
SAT solver technology to exploit that repetition.

###  2.3  Theorem Prover For Large Problems

This section discusses prior work on SAT solving for software engineering
applications. From this review, we will argue that the QuickSampler tool from
ICSE’18 [12] is an appropriate comparison algorithm for our Snap study.

As shown in Table 1, much prior research has explored scaling theorem proving
for software engineering. One way to tame the theorem proving problem is to
simplify or decompose the CNF formulas. A recent example in this arena was
GreenTire, proposed by Jia et al. [42]. GreenTire supports constraint reuse
based on the logical implication relation among constraints. One advantage of
this approach is its efficiency guarantees. Similar to the analytical methods
in linear programming, they are always applied to a specific class of problem.
However, even with the improved theorem prover, such methods may be difficult
to be adopted in large models. GreenTire was tested in 7 case studies. Each
case study was corresponding to a small code script with ten lines of code,
e.g. the BinTree in [43]. For the larger models, such as those explored in
this paper, the following methods might do better.

Another approach, which we will call sampling, is to combine theorem provers
Z3 with stochastic sampling heuristics. For example, given random selections
for $b,c$, Eq. 1 might be used to generate a new test suite, without calling a
theorem prover. Theorem proving might then be applied to some (small) subset
of the newly generated tests, just to assess how well the heuristics are
working.

The earliest sampling tools were based on binary decision diagrams (BDDs)
[44]. Yuan et al. [25, 27] build a BDD from the input constraint model and
then weighted the branches of the vertices in the tree such that a stochastic
walk from root to the leaf was able to generate samples with the desired
distribution. In other work, Iyer proposed a technique named RACE which has
been applied in multiple industrial solutions [26]. RACE (a) builds a high-
level model to represent the constraints; then (b) implements a branch-and-
bound algorithm for sampling diverse solutions. The advantage of RACE is its
implementation simplicity. However, RACE, as well as the BDD-based approached
introduced above, return highly biased samples, that is, highly non-uniform
samples. For testing, this is not recommended since it means small parts of
the code get explored at a much higher frequency than others.

Using a SAT solver WalkSat [45], Wei et al. [28] proposed SampleSAT. SampleSAT
combines random walk steps with greedy steps from WalkSat– a method that works
well for small models. However, due to the greedy nature of WalkSat, the
performance of SampleSAT is highly skewed as the size of the constraint model
increases.

For seeking diverse samples, some use universal hashing [46] which offers
strong guarantees of uniformity. Meel et al. [33] list key ingredients of
integration of universal hashing and SAT solvers; e.g. guarantee uniform
solutions to a constraint model. These hashing algorithms can be applied to
the extreme large models (with near 0.5M variables). More recently, several
improved hashing-based techniques have been purposed to balance the
scalability of the algorithm as well as diversity (i.e. uniform distribution)
requirements. For example, Chakraborty et al. proposed an algorithm named
UniGen [31], following by the Unigen2 [32]. UniGen provides strong theoretical
guarantees on the uniformity of generated solutions and has applied to
constraint models with hundreds of thousands of variables. However, UniGen
suffered from a large computation resource requirement. Later work explored a
parallel version of this approach. Unigen2 achieved near linear speedup on the
number of CPU cores.

To the best of our knowledge, the state-of-the-art technique for generating
test cases using theorem provers is QuickSampler [12] which run faster than
prior work [30, 32] for larger programs (and found test suites with more valid
tests [12]). QuickSampler used the heuristic that “valid tests can be built by
combining other valid tests’; e.g. a new test can be built from valid tests
$a,b,c$ using $\oplus$ (“exclusive or”):

$d=c\oplus(a\oplus b)$ (1)

This heuristic is useful since “exclusive or” is faster than, say, running a
theorem prover. QuickSampler was evaluated on large real-world case studies,
some of which have more than 400K variables. At ICSE’18, it was shown that
QuickSampler outperforms aforementioned Unigen2 as well as another similar
technique named SearchTreeSampler [30]. QuickSampler starts from a set of
valid solutions generated by Z3. Next, it computes the differences between the
solutions using Eq. 1. New test cases generated in this manner are not
guaranteed to be valid. QuickSampler defines three terms, we use later in this
paper:

  * •

A test suite is a set of valid tests.

  * •

A test is valid if it uses input settings that satisfy the CNF.

  * •

One test suite is more diverse than another if it uses more variable within
the CNF disjunctions. Diverse test suites are preferred since they cover more
parts of the code.

According to Dutra et al.’s experiments, the percent of valid tests found by
QuickSampler can be higher than 70%. The percent of valid tests found by Snap,
on the other hand, is 100%. Further, as shown below, Snap builds those tests
with enough diversity much faster than QuickSampler.

##  3 About Snap

The Snap algorithm is shown in Fig. 2. In summary, Snap cluster some candidate
tests, then search for valid tests by proposing small mutations to the cluster
centroids. Mutations are generated via the deltas described below (and deltas
are applied according to their frequency of occurrence). This technique
effectively removes repeated structures in the tests since many repeated
structures are replaced with one centroid. Another way Snap exploits repeated
structures is that the algorithm tend to mutate across the repeated
structures; i.e. the higher frequency deltas.

As to the details, within Snap, each test is a set of zeros or ones (false,
true) assigned to all the variables in a CNF formula. As shown in initial
samples (steps 1a,1b), instead of computing some deltas between many tests,
Snap restrains mutation to the deltas between a few valid tests (generated
from Z3). Snap builds a pool of 10,000 deltas from $N=100$ valid tests (which
mean calling a theorem prover only $N=100$ times). Snap uses this pool as a
set of candidate “mutators” for existing tests (and by “mutator”, we mean an
operation that converts an existing test into a new one).

After that, in delta preparation (steps 2a,2b), Snap applies Eq. 1. Step 2b
sorts the deltas on occurrence frequency. This sort is used in step 3b.

0) Set up (a) Let $N=100$; i.e. initial sample size; (b) Let $k=5$; i.e.
number of clusters; (c) Let suite$=\emptyset$; i.e. the output test suite; (d)
Let samples$=\emptyset$; i.e. a temporary work space. 1) Initial samples
generation: (a) Add $N$ solutions (from Z3) to samples (b) Put all samples
into $\mathit{suite}$ (since they are valid) 2) Delta preparation: (a) Find
delta $\delta=(a\oplus b)$ for all $a,b\in\mathit{samples}$. (b) Weight each
delta by how often it repeats 3) Sampling (a) Find $k$ centroids in samples
using $k$-means; (b) For each centroid $c$, repeat $N$ times: i.
stochastically pick deltas $\delta_{i}$, $\delta_{j}$ at prob. equal to their
weight. ii. compute a new candidate using $c\oplus(\delta_{i}\vee\delta_{j})$
iii. verify new candidate using Z3; iv. if invalid, repair using Z3 (see
§3.1). Add to sample; v. add the repaired candidate to suite; 4) Loop or
terminate: (a) If improving (see §3.2), go to step 2. Else return suite.

Figure 2: Snap

In sample (steps 3a,3b), Snaps samples around the average values seen in a few
randomly selected valid tests. Here, ”averaging” is inferred by using the
median values seen in $k$ clusters. Note that, in step 3b, we use deltas that
are more likely to be valid (i.e. we use the deltas that occur more
frequently).

Step 3b.iii is where we verify the new candidate using Z3. Snap explores far
fewer candidates than QuickSampler (10 to 750 times less, see §5.2). Since we
are exploring less, we can take the time to verify them all. Hence, 100% of
Snap’s tests are valid (and the same is not true for QuickSampler– see Fig.
6).

Note that in 3b.iv, we only add our new tests to the clusters if it fails
verification (taking care to first repair it). We do this since test cases
that pass verification do not add new information. But when an instance fails
verification and is repaired, that offers new settings.

###  3.1 Implementing “Repair”

Snap’s repair function deletes “dubious” parts of a test case, then uses Z3 to
fill in the the gaps. In this way, when we repair a test, most bits are set
and Z3 only has to search a small space.

To find the “dubious” section, we reflect on how step 3b.ii operates. Recall
that the new test uses $\delta=a\oplus b$ and $a,b$ are valid tests taken from
samples. Since $a,b$ were valid, then the “dubious” parts of the test is
anything that was not seen in both $a$ and $b$. Hence, we preserve the bits in
$c\oplus\delta$ bits (where the corresponding $\delta$ bit was 1), while
removing all other bits (where $\delta$ bit was 0). For example:

  * •

To mutating $c=$(1,0,0,1,1,0,0,0) use $\delta=$(1,0,1,0, 1,0,1,0).

  * •

If $c\oplus\delta=$(0,0,1,1,0,0,1,0) is invalid, then Snap deletes the
“dubious” sections as follows.

  * •

Snap preserves any “1” bits that were seen in $\delta$.

  * •

Snap deletes the others; e.g. bits 2, 4, 6, 8 (0,~~0~~ ,1,~~1~~ ,0,~~0~~ ,
1,~~0~~).

  * •

Z3 is then called to figure out the missing bits of $(0?1?0?1?)$.

###  3.2 Implementing “Termination”

To implement Snap’s termination criteria (step 4a), we need a working measure
of diversity. Recall from the introduction that one test suite is more diverse
than another if it uses more of the variable settings with disjunctions inside
the CNF. Diverse test suites are better since they cover more parts of the
code.

To measure diversity, we used Feldt et al. [47]’s normalized compression
distance (NCD). A test suite with high NCD implies higher code coverage during
the testing333Aside: we note that we did not adopt the diversity metric
(distribution of samples displayed as a histogram) from [32, 12] since
computing that metric is very time-consuming. For the case studies of this
paper, that calculation required days of CPU. Later in this paper, we show
that our use of this diversity measure is not a threat to validity for this
study. . NCD uses gzip to the estimate Kolmogorov complexity [48] of the
tests. If $C(x)$ is the length of compression of $x$ and $C(X)$ is the
compression length of binary string set $X$’s concatenation, then:

$\text{NCD}(X)=\frac{C(X)-\min_{x\in X}\\{C(x)\\}}{\max_{x\in
X}\\{C(X\backslash\\{x\\})\\}}$ (2)

To understand how the NCD is revealing the diversity of a test suite, consider
the following test suite where each row in the matrix represents one test
case:

$\hbox{\pagecolor{red!35}T1}=\begin{bmatrix}0&0&0&0&0&\\\ 0&0&0&1&1&\\\
0&0&0&1&0&\end{bmatrix}$

Here, NCD${}_{1}=0.142$. Now, assuming that we have obtained the following
test suite after several iterations

$\hbox{\pagecolor{orange!25}T2}=\begin{bmatrix}0&0&0&0&0&\\\ 0&0&0&1&1&\\\
0&0&0&1&0&\\\ 1&0&0&0&0&\hbox{\pagecolor{green!20}$+$}\\\
0&1&0&1&1&\hbox{\pagecolor{green!20}$+$}\\\ \end{bmatrix}$

then NCD2 is now 0.272. Note that (a) $+$ marks the new test cases obtained
since T1; and (b) NCD2 is larger since the new cases cover various options in
first two bits.

On the other hand, if we further consider the following test suite:

$\hbox{\pagecolor{yellow!10}T3}=\begin{bmatrix}0&0&0&0&0&\\\ 0&0&0&1&1&\\\
0&0&0&1&0&\\\ 0&0&0&0&1&\hbox{\pagecolor{green!20}$+$}\\\ 1&0&0&0&0&\\\
0&1&0&1&1&\\\ 0&1&0&1&0&\hbox{\pagecolor{green!20}$+$}\end{bmatrix}$

then NCD3 = 0.305. Here, due to two new test cases (marked as $+$), we do see
NCD improvements in T3, as compared to T2. Such scale of improvements,
however, is not significant: from T1to T2, we got
$\mathit{\frac{0.272-0.142}{0.142}=}91\%$ NCD improvements, while in the T3,
we got $\mathit{\frac{0.305-0.272}{0.272}=}12.1\%$ increases. This is because
the new cases in T3 does not explore the diversity of new bits, such as the
third bit. 444In this example, we examine the diversity via single bit.
However, the NCD also examines the bits-group, such as the combinations of bit
pair $(x,y)$, or bit tuple $(x,y,z)$ etc.

Another point to note is that NCD is presenting the diversity of a string-
block (i.e. every substring matters). One substring $x$ where $C(x)\to 0$ does
not imply NCD$\to 1$. This is because the $x$ itself can attribute a lot to
NCD of the whole string-block. Take the aforementioned T1 as an example: among
all three cases $x_{1}$, $x_{2}$ and $x_{3}$, $C(x_{1})\to 1$, NCD$(x_{1}\cup
x_{2}\cup x_{3})\ll 1$.

###  3.3 Other Engineering Choices

Snap takes great care in how it calls a theorem prover. Theorem provers are
much slower for generating new tests than repairing invalid tests than for
verifying that a test is valid (since there are more options for generation
than for repairing than for verification). Hence, Snap needs to verify more
than it repairs (and also do repairs more than generating new tests). More
specifically:

  * •

The call to Z3 in step 1a is a generating call. This can be slowest since this
must navigate all the constraints of our CNF. Therefore, we only do this
$N=100$ times.

  * •

The call to Z3 in step 3b.iii is a verification call and is much faster since
all the variables are set.

  * •

The call to Z3 in step 3b.iv repair call, is slower than step 3b.iii since our
repair method adds open choices to a test.

Note that we only need to repair the small minority of new tests that fail
verification. Later in this paper, we can use Fig. 6 to show that repairs are
only needed on 30% (median) of all tests.

As to hyperparameters, Snap uses these control parameters:

  * •

$X=5\%$;

  * •

$T=10$ minutes;

  * •

$N=100$ samples;

  * •

$k=5$ clusters.

In future work, it could be insightful to vary these values. Another area that
might bear further investigation is the clustering method used in step 3a. For
this paper, we tried different clustering methods. Clustering ran so fast that
we were not motivated to explore alternate algorithms. Also, we found that the
details of the clustering were less important than pruning away most of the
items within each cluster (so that we only mutate the centroid).

##  4 Experimental Set-up

###  4.1 Code

To explore the research questions shown in the introduction, the Snap system
shown in Fig. 2 was implemented in C++ using Z3 v4.8.4 (the latest release
when the experiment was conducted). A $k$-means cluster was added using the
free edition of ALGLIB [49], a numerical analysis and data processing library
delivered for free under GPL or Personal/Academic license. QuickSampler does
not integrate the samples verification into the workflow. Hence, in the
experiment, we adjusted the workflow of QuickSampler so that all samples are
verified before termination, which is the same as Snap as in §3.2. Also, the
outputs of QuickSampler were the assignments of independent support. The
independent support is a subset of variables which completely determines all
the assignments to a formula [12]. In practice, engineers need the complete
test case input; consequently, for valid samples, we extended the QuickSampler
to get full assignments of all variables from independent support’s assignment
via propagation.

Table 2: Case studies used in this paper. Sorted by number of variables. Medium sized-problems are highlighted with  blue rows while the large ones are in  orange rows. Three items (marked with *) are not included in some further reports (see text). See §4.2 for details. Size | Case studies | Vars | Clauses
---|---|---|---
| blasted_case47 | 118 | 328
| blasted_case110 | 287 | 1263
| s820a_7_4 | 616 | 1703
| s820a_15_7 | 685 | 1987
| s1238a_3_2 | 685 | 1850
Small | s1196a_3_2 | 689 | 1805
| s832a_15_7 | 693 | 2017
| blasted_case_1_b12_2* | 827 | 2725
| blasted_squaring16* | 1627 | 5835
| blasted_squaring7* | 1628 | 5837
| 70.sk_3_40 | 4669 | 15864
| ProcessBean.sk_8_64 | 4767 | 14458
| 56.sk_6_38 | 4836 | 17828
| 35.sk_3_52 | 4894 | 10547
| 80.sk_2_48 | 4963 | 17060
| 7.sk_4_50 | 6674 | 24816
| doublyLinkedList.sk_8_37 | 6889 | 26918
| 19.sk_3_48 | 6984 | 23867
| 29.sk_3_45 | 8857 | 31557
Medium | isolateRightmost.sk_7_481 | 10024 | 35275
| 17.sk_3_45 | 10081 | 27056
| 81.sk_5_51 | 10764 | 38006
| LoginService2.sk_23_36 | 11510 | 41411
| sort.sk_8_52 | 12124 | 49611
| parity.sk_11_11 | 13115 | 47506
| 77.sk_3_44 | 14524 | 27573
Large | 20.sk_1_51 | 15465 | 60994
| enqueueSeqSK.sk_10_42 | 16465 | 58515
| karatsuba.sk_7_41 | 19593 | 82417
| tutorial3.sk_4_31 | 486193 | 2598178

###  4.2 Case Studies

Table 2 lists the case studies used in this work. We can see that the number
of variables ranges from hundreds to more than 486K. The large examples have
more than 50K clauses, which is very huge. For exposition purposes, we divided
the case studies into three groups: the small case studies with vars $<6K$;
the medium case studies with $6K<$ vars $<12K$ and the large case studies with
vars $>12K$.

For the following reasons, our case studies are the same as those used in the
QuickSampler paper:

  * •

We wanted to compare our method to QuickSampler;

  * •

Their case studies were online available;

  * •

Their studies are used in many papers [31, 32, 33, 12].

These case studies are representative of scenarios engineers met in software
testing or circuit testing in embedded system design. They include bit-blasted
versions of SMTLib case studies, ISCAS89 circuits augmented with parity
conditions on randomly chosen subsets of outputs and next-state variables,
problems arising from automated program synthesis and constraints arising in
bounded theorem proving. For more introduction of the case studies, please see
[32, 12].

For pragmatic reasons, certain case studies were omitted from our study. For
example, we do not report on diagStencilClean.sk_41_36 in the experiment since
the purpose of this paper is to sample a set of valid solutions to meet the
diversity requirement; while there are only 13 valid solutions from this
model. The QuickSampler spent 20 minutes (on average) to search for one
solution.

Also, we do report on the case studies marked with a star(*) in Table 2. Based
on the experiment, we found that even though the QuickSampler generates tens
of millions of samples for these examples, all samples were the assignment to
the independent support (defined in §4.1). The omission of these case studies
is not a critical issue. Solving or sampling these examples is not difficult;
since they are all very small, as compared to other larger case studies.

###  4.3 Experimental Rig

We compared Snap to the state-of-the-art QuickSampler, technique. To ensure a
repeatability, we update the Z3 solver in QuickSampler to the latest version.

To reduce the observation error and test the performance robustness, we
repeated all experiment 30 times with 30 different random seeds. To simulate
real practice, such random seeds were used in Z3 solver (for initial solution
generation), ALGLIB (for the $k$-means) and other components. Due to space
limitation, we cannot report results for all 30 repeats. Instead, we report
the medium or the IQR (75-25th variations) results.

All experiments were conducted on Xeon-E5@2GHz machines with 4GB memory,
running CentOS. We only used one core per machine.

Figure 3: RQ1 results: Time to terminated (seconds), The y-axis is in log
scale. The Snap sampling time for s1238_a_3_2 and parity.sk_11_11 is not
reported since their achieved NCD were much worse than QuickSampler’s (see
Fig. 7). Fig. 4 illustrates the corresponding speedups. Figure 4: RQ1 results:
sorted $\mathit{speedup}$ (time(QuickSampler) / time(Snap)). If over $10^{0}$,
then Snap terminates earlier.

##  5 Results

The rest of this paper use the machinery defined above to answer the four
research questions posed in the introduction.

###  5.1  RQ1: How Much Faster is the Snap Tactic?

Fig. 3 shows the execution time required for Snap and QuickSampler. The y-axis
of this plot is a log-scale and shows time in seconds. These results are shown
in the same order as Table 2. That is, from left to right, these case studies
grow from around 300 to around 3,000,000 clauses.

For the smaller case studies, shown on the left, Snap is sometimes slower than
QuickSampler. Moving left to right, from smaller to larger case studies, it
can be seen that Snap often terminates much faster than QuickSampler. On the
very right-hand side of Fig. 3, there are some results where it seems Snap is
not particularly fastest. This is due to the log-scale applied to the y-axis.
Even in these cases, Snap is terminating in less than an hour while other
approaches need more than two hours.

Fig. 4 is a summary of Fig. 3 that divides the execution time for both
systems. From this figure it can be seen:

Conclusion #1:  Snap terminated 10 to 3000 times faster than QuickSampler
(median to max).

There are some exceptions to this conclusion, where QuickSampler was faster
than Snap (see the right-hand-side of Fig. 4). Those cases are usually for
small models (17,000 clauses or less). For medium to larger models, with
20,000 to 2.5 million clauses, Snap is often orders of magnitude faster.

Table 3: RQ2 results: number of unique valid cases in test suite. Sorted by last column. Same color scheme as Table 2.  | $\mathbf{S_{S}}$ | $\mathbf{S_{Q}}$ | $\mathbf{S_{Q}}/$
---|---|---|---
Case studies | Snap | QuickSampler | $\mathbf{S_{S}}$
blasted_case47 | 2899 | 71 | 0.02
isolateRightmost | 15480 | 7510 | 0.49
LoginService2 | 404 | 210 | 0.52
19.sk_3_48 | 204 | 200 | 0.98
70.sk_3_40 | 3050 | 4270 | 1.40
s820a_15_7 | 29065 | 70099 | 2.41
29.sk_3_45 | 225 | 660 | 2.93
s820a_7_4 | 37463 | 124457 | 3.32
s832a_15_7 | 27540 | 96764 | 3.51
s1196a_3_2 | 225 | 1890 | 8.40
enqueueSeqSK | 338 | 2495 | 7.38
blasted_case110 | 274 | 2386 | 8.71
tutorial3.sk_4_31 | 336 | 2953 | 8.79
81.sk_5_51 | 227 | 2814 | 12.40
sort.sk_8_52 | 812 | 10184 | 12.54
karatsuba.sk_7_41 | 139 | 4210 | 30.29
20.sk_1_51 | 239 | 10039 | 42.00
doublyLinkedList | 278 | 12042 | 43.32
17.sk_3_45 | 228 | 12780 | 56.05
ProcessBean | 1193 | 75392 | 63.20
7.sk_4_50 | 258 | 18090 | 70.12
56.sk_6_38 | 1827 | 149031 | 81.57
80.sk_2_48 | 653 | 54440 | 83.37
77.sk_3_44 | 245 | 33858 | 138.20
35.sk_3_52 | 258 | 193920 | 751.63
Figure 5:  Identical deltas seen in 100*100 pair of valid solution deltas for
all case studies. Same color scheme as Table 2.

###  5.2 RQ2: Does the Snap tactic find fewer test cases?

Table 3 compares the number of tests from QuickSampler and Snap. As shown by
the last column in that table:  Conclusion #2:  Test cases from Snap were 10
to 750 times smaller than from QuickSampler (median to max). Hence we say that
using Snap is easier than other methods, where “easier” is defined as per our
Introduction. That is, when test suites are 10 to 750 times smaller, then they
are faster to run, consumes less cloud-compute resources, and means developers
have to spend less time processing failed tests.

###  5.3 RQ3: How “good” are the tests found via the Snap tactic?

Generating small tests sets, and doing so very quickly, is not interesting
unless those test suites are also “good”. This section applies two definitions
of “good” to the Snap output:

  * •

Credibility: Recalling Fig. 1, test suites need to satisfy the CNF clauses
generated from source code. As defined in the introduction, we say that the
“more credible” a test suite, the larger the percentage of valid tests.

  * •

Diversity: A CNF clause is conjunction of disjunctions. Diversity measures how
many of disjunctions are explored by the tests. This is important since a high
diversity means that most code branches are covered.

####  5.3.1 Credibility

Regarding credibility, we note that Snap only prints valid tests. That is,
100% of Snap’s tests are valid.

The same cannot be said for QuickSampler. That algorithm ran so quickly since
it assumed that tests generated using Eq. 1 did not need verification. To
check that assumption, for each case study, we randomly generated 100 valid
solutions, $S=\\{s_{1},s_{2},\ldots s_{100}\\}$ using Z3. Next, we selected
three $\\{a,b,c\\}\in Ss$ and built a new test case using Eq. 1; i.e.
$\mathit{new}=c\oplus(a\oplus b)$.

Fig. 5 lists the number of identical deltas seen in $100^{2}$ of those deltas.
We rarely found large sets of unique deltas; i.e. among the 100 valid
solutions given by Z3, many $\delta$s were shared within pairwise solutions.
This is important since if otherwise, the Eq. 1 heuristic would be dubious.

The percentage of these deltas that proved to be valid in step3b.iii of
Algorithm 1 are shown in Fig. 6. Dutra et al.’s estimate was that the
percentage of valid tests generated by Eq. 1 was usually 70% or more. As shown
by the median values of Fig. 6, this was indeed the case. However, we also see
that in the lower third of those results, the percent of valid tests generated
by Eq. 1 is very low: 25% to 50% (median to max).

This result make us cautious about using QuickSampler since, when the Eq. 1
heuristics fails, it seems to be inefficient.

By way of comparisons, it is relevant to remark here that Snap verifies every
test case it generates. This is practical for Snap, but impractical for
QuickSampler since these two systems typically process $10^{2}$ to $10^{8}$
test cases, respectively. In any case, another reason to recommend Snap is
that this tool delivers tests suites where 100% of all tests are valid.

In summary, in terms of credibility, Snap’s tests are 100% “good” while other
methods may find fewer “good” tests.

Figure 6: RQ3 results for “credibility”: percentage of valid mutations found
it step3b.iii (computed separately for each case study).

####  5.3.2 Diversity

Regarding diversity, Fig. 7 shows test diversity of our two systems (expressed
as NCD ratios). Results less than one indicate that Snap’s test suites are
less diverse than QuickSampler. In the median case, the ratio is one; i.e. in
terms of central tendency, there is no difference between the two algorithms.
A bootstrap test at 95% confidence (to test for statistically significant
results), and a Cohen’s effect size test (to rule out trivially small
differences) showed that in $\frac{25}{27}=93\%$ cases, there is no
significant difference (of non-trivial size).

Figure 7: RQ3 results for “diversity”: Normalized compression distance (NCD)
when QuickSampler and Snap terminated on the same case studies. Median results
over 30 runs (and small black lines show the 75th-25th variations). Same color
scheme as Table 2.

That said, in there two cases with a statistical significant difference that
are markedly less than Snap (see s1238a_3_2 and parity.sk_11_11) (Fig. 7). In
terms of scoring different algorithms, it could be argued that these examples
might mean that QuickSampler is the preferred algorithm but only (a) if
numerous invalid tests are not an issue; (b) if testing resources are fast and
cheap (so saving time and money on cloud-compute test facilities is not
worthwhile); and (c) if developer time is cheap (so the time required to
specify expected test output, or processing large numbers of failed tests, is
not an issue).

Hence we recommend Snap since,  Conclusion #3:  Usually, Snap’s tests are far
more credible and very nearly as diverse as those from QuickSampler.

##  6 Threats to Validity

###  6.1 Baseline Bias

One threat to the validity of this work is the baseline bias. Indeed, there
are many other sampling techniques, or solvers, that Snap might be compared
to. However, our goal here was to compare Snap to a recent state-of-the-art
result from ICSE’18. In further work, we will compare Snap to other methods.

###  6.2 Internal Bias

A second threat to validity is internal bias that raises from the stochastic
nature of sampling techniques. Snap requires many random operations. To
mitigate the threats, we repeated the experiments for 30 times.

###  6.3 Hyperparameter Bias

Another threat is hyperparameter bias. The hyperparameter is the set of
configurations for the algorithm. The hyperparameter used in these experiments
were shown in §3.3. Learning how to automatically adjust these settings would
be a useful direction for future work.

How long would it take to learn better parameters? As shown in Fig. 4, it can
take $10^{5}$ (approx) seconds to complete one run of our test generation
systems. Standard advice for hyperparameter optimization with (say) a genetic
algorithm is to mutate a population of 100 candidates over 100 generations
[50]. Allowing for 20 repeats (for statistical validity), then the runtimes
for hyperparameter optimization experiments could require:

$10^{5}*100*100*20/3600/168/52\approx 650\;\mathit{years}$

This is clearly an upper bound. If we applied experimental hyperparameter
optimizers that tried less than 50 configurations (selected via Bayesian
parameter optimization [51, 52]), then that runtimes could be three years of
CPU:

$10^{5}*50*20/3600/168/52\approx 3\;\mathit{years}$

Yet another method, that might be more promising, is incremental transfer
learning where optimizers transfer lessons learned between hyperparameter
optimizations running in parallel [53]. In this approach, we might not need to
wait $10^{5}$ seconds before we can find better parameters.

In summary, it would be an exciting and challenging task to perform
hyperparameter optimization in this domain.

###  6.4 Construct Validity

There are cases where the above test scheme would be incomplete. All the above
assumes that the the constraints of the program can be expressed in terms of
the literals seen within the conditionals that define each branch of a
program. This may not always be true. For example, consider constraints
between fields of buried deep within a nested data structure being passed
around the program. To address constraints of that type, we would need access
to (e.g.) invariants that many be defined within those structs, but which are
invisible to the tests in the path conditionals. Strongly typed languages like
Haskell or OCaml which can reason about nested types might be of some
assistance here. This would be a promising area for future work.

###  6.5 External Validity

Apart for issues of nested type constraints, this section lists two other
areas that would require an extension to the current Snap framework.
Specifically, Snap is not designed for testing non-deterministic or
nonfunctional requirements.

Functional requirements define systems functions; e.g. ”update credit card
record”. On the other hand, a non-functional requirements specify how the
system should do it. For example, nonfunctional requirements related to
software “ilities” such as usability, maintainability, scalability, etc. When
designing tests for nonfunctional requirements, it may be required to access
variables that are not defined in the conditionals that define program
branches; (e.g. is the user happy with the interaction?). Snap does not do
that since it draws its tests only from the variables in the branch tests.

As to testing non-deterministic systems, a deterministic function is one where
the output is fully determined by their inputs; i.e. if the function is called
$N$ times with the same inputs then in a deterministic environment, we would
expect the same output. On the other hand, a non-deterministic function is one
where identical inputs can lead to different outputs. When designing tests for
non-deterministic systems, it would be useful to make multiple tests fall down
each program branch since that better samples the space of possible non-
deterministic behaviours within that branch. Snap may not be the best tool for
non-deterministic systems since, often, it only produces one test for each of
the branches it visits.

In future work, it would be insightful to consider how Snap might be extended
for non-functional and/or non-deterministic systems.

Figure 8: The authors of the QuickSampler paper [12], say this figure shows
that different test generation algorithms QuickSampler[12],
SearchTreeSampler[30], UniGen2[32] and one uniformed random generator achieve
similar solution diversity (assuming unlimited CPU).

Figure 9: Diversity distributions (from Shannon entropy). Both QuickSampler
and Snap were terminated at the same time – Blasted cases=1min, s820a cases =
5mins, LoginService2=10mins. $Y$-axis shows valid solutions (those with same
Shannon Entropy were clustered together) $Y$-axis shows occurrences in
results.

###  6.6 Algorithm Bias

Our results used a termination criteria based on NCD, which is different from
some prior work. So is NCD a fair diversity comparison metric?.

To explore this, we need some way to compare the results of text case
generation algorithms, given the same CPU allocation, i.e. getting rid of NCD.
Fig. 8 shows one way to make that comparison ( this figure comes from the
QuickSampler paper):

  * •

Three different test case generation algorithms [12, 30, 32] (and a uniform
random generator) are executed.

  * •

Each algorithm was given 10 hours of CPU.

  * •

Fig. 8 counts the repeated solutions within each run. That figure shows that
(e.g.) 25,000 solutions are found 15 times (approximately) within all four
methods.

The authors of the QuickSampler paper used Fig. 8 to argue that, assuming a
large CPU allocation, then at the end of the run, all these algorithms achieve
similar solution diversity. Aside: just to defend QuickSampler here– merely
because the same solutions are found in Fig. 8 by different methods does not
mean that there is no benefit to QuickSampler. As discussed in [12],
QuickSampler wins over the other algorithms of Fig. 8 since (a) it scales to
larger problems and (b) it produces test suites with more valid tests, faster
than previous methods.

To illustrate Snap’s diversity in a similar manner to Fig. 8, we have the
following observations:

  * •

Recalling the Table 3 results: Snap found far fewer test cases than other
algorithms. Hence, we cannot use the $y$-axis of Fig. 8 to compare our method
to previous methods.

  * •

We need another non-NCD measure of diversity that does not favor either
QuickSampler or Snap. For that purpose, we used Shannon Entropy [54], i.e.

$H(p)=-p\log_{2}^{p}-(1-p)\log_{2}^{(1-p)}$

where $p$ is the probability of one(1)s in the solution.

In combination, our comparison proceeds as follows. QuickSampler and Snap were
run on each case study, terminating after the same number of minutes. Since
our goal was to see “what is lost by Snap”, we terminated in times similar to
the termination times seen in the RQ1 study. Specifically, those termination
times were assigned to the case studies, basing on their number of clauses,
from the set {1,5,10} minutes. As shown above in the RQ2 study, the number of
solutions generated by Snap and QuickSampler are not in the same scale.
Accordingly, we only recorded the unique solutions found in this study. At
termination, we collected all unique valid test cases when the execution
terminated at the given time and compared the diversities among them.

As seen in Fig. 9, we output the distribution of entropies, expressed as the
percentage of tests that have that entropy (and not as Fig. 8’s absolute
number of test  with that entropy).

Fig. 9 shows the distributions of the diversity of Snap and QuickSampler
results seen in blasted_case47, blasted_case10, s820a_7_4, s820a_15_7 and
LoginService2.sk_23_36. These data sets were selected for presentation here
since, in the QuickSampler paper, they were singled out for special analysis
(according to that paper, these algorithm yield a large and countable range of
diverse results). In that figure, we see that

  * •

Among all these test cases, Snap and QuickSampler yielded solutions within
same entropy range.

  * •

In fact, usually we see a very narrow range of entropy on the x-axis: In 4/5
cases, the range was less than 3%. This means that these case studies yield
solutions with similar entropy.

In summary, from Fig. 9, we say that if solutions were generated by
QuickSampler with a particular entropy, then it is likely that the Snap was
generating that kind of solutions as well. Hence, we do not see a threat to
validity introduced by how Snap selects its termination criteria.

###  6.7 Evaluation Bias

This paper has evaluated the Snap test case generator using the five goals
described in the introduction: i.e. runtime, scalability, redundancy,
credibility and minimality. But as the following examples show, these are not
the only criteria for assessing test suites. For future work it could be
useful and insightful to apply other evaluation criteria.

Firstly, Yu et al. [19] discuss the information needs for test case
prioritization. They argue that in modern complex cloud-based test
environment, it can be advantageous not to run all tests all the time. Rather,
there are engineering benefits to first running the tests that are most likely
to fail. His results show that different kinds of systems need different kinds
of prioritization schemes, but not all projects collect the kinds of data
needed for different prioritization schemes. Hence it is an open issue if
tools like Snap and QuickSampler can contribute to test case prioritization.

Secondly, once tests are run, then faults have to be localized and fixed.
Spectrum-based Reasoning (SR) is a research hot-spot on this. Given a system
of $M$ components, a test suite $T$ as well as the obtained errors after
executing $T$ on the system, SR approaches utilize similarity-like coefficient
to find a correlation between component and the errors location. Perez et al.
[55] warn that though high-coverage test suites can detect errors in the
system, it is not guaranteed that inspecting tests will yield a
straightforward explanation, i.e. root cause, for the error. It will be of
insightful to test how effective are QuickSampler or Snap in localizing faults
in real-world executions.

Thirdly, Ostrand et al. [56] argues that the value of quality assurance
methods is that they focus the analysis on what parts of the code base deserve
most attention. By this criteria, we should assess test suites by how well
they find the most bugs in the fewest lines of code.

Fourthly, a common way to assess test suite generators is via the uniformity
of the generated tests [57]. Theorem provers report their solutions in some
implementation-specific order. Hence, it is possible that after running a
theorem prover for some finite time, then the solutions found in that time may
only come from a small “corner” of the space of possible solution [31]. When
test for uniformity for a theorem prover sampling the space of $N$ possible
tests, then the frequency of occurrence of some test $T_{i}$ should be
approximately $1/N$.

We argue that issues of uniformity are less important than branch coverage
(which is measured above as diversity, see §6.6). To make that argument, we
draw a parallel from the field of data mining. Consider a rule learner that is
building a rule from the set of all possible literals in a data sets. In
theory, this space of literals is very large (all attributes combined with all
their ranges combined any any number of logical operators and combined to any
length of rule). Nevertheless, a repeated result is that such learners can
terminate very quickly [58] since, rather that searching all literals, these
learners need only explore the small set of literals commonly seen in the
data.

We draw this parallel since the success of Snap is consistent with the
conjecture that the programs we explore are using just a small subset of the
space of all settings. In that situation, uniformity is less of an issue than
diversity since the latter reports how well the tests match the “shape” of the
data.

We note that other researchers endorse our position here that effective
testing need only explore a small portion of the total state space. Miryung
Kim and colleagues [59] were testing scripts that processed up to $10^{10}$
rows of data. In theory, the test suite required here is very large indeed
(the cross-produce of all the possible values in $10^{10}$ rows). However, a
static analysis showed that those scripts could be approximated by less than 3
dozens pathways. Hence in that application, less than three dozen tests were
enough to test those scripts. Note the parallels of the Kim et al. results to
the Snap work and the data mining example offered above:

  * •

Kim et al. did not cover all possible data combinations.

  * •

Rather, they constrained their tests to just cover the standard “shape” of the
code they were testing.

Accordingly, when seeking the smallest number of tests that cover the
branches, it may be a secondary concern whether or not those test cases “bunch
up” and do not cover the cross product of all possible solutions.

##  7 Related Work

In essence, the algorithms of this paper are samplers that explore some subset
of seemingly large and complex problems. Sampling is not only useful for
finding test suites in theorem proving. It also has applications for other SE
problems such as requirement engineering, resource planning optimization, etc
[60, 61, 62, 63]. A repeated problem with all these applications was the time
required to initialize the reasoning. In that initialization step, some large
number of samples had to be collected. In practice, that step took a
significant percentage of the total runtime of those systems. We conjecture
that Snap can solve that initialization problem. Using the techniques of this
paper, it might be time now to repeat all the above work. This time, however,
instead of wasting much time on a tedious generation process, we could use
something like Snap to quick start the reasoning.

As to other related work, like Snap, the DODGE system of Agrawal et al. [64]
made an assumption that given a set of solutions to some SE problem, there is
much redundancy and repetition within those different solutions. A tool for
software analytics, DODGE needed just a few dozen evaluations to explore
billions of configuration options for (a) choice of learner, for (b) choice of
pre-processor, and for (c) control parameters for the learner and pre-
processor. DODGE executed by:

  1. 1.

Assign random weights to configuration options.

  2. 2.

Randomly pick options, favoring those with most weight;

  3. 3.

Configuring and executing data pre-processors and learners using those
options;

  4. 4.

Dividing output scores into regions of size $\epsilon=0.2$;

  5. 5.

When some new configuration has scores with $\epsilon$ of prior configurations
then…

  6. 6.

…reduce the weight of those configuration options;

  7. 7.

Go Step2

Note that after Step5, then the choices made in subsequent Step1s will avoid
options that arrive within $\epsilon$ of other observed scores. Experiments
with DODGE found that best learner performance plateau after just a few dozen
repeats of Steps12345. To explain this result, Argrawal et al. [64] note that
for a range of software analytics tasks, the outputs of a learner divide into
only a handful of equivalent regions. For example, when an software analytics
task is repeated 10 times, each time with 90% of the data, then the observed
performance scores (e.g. recall, false alarm) can vary by 5 percent, or more.
Assuming normality, then scores less than $\epsilon=1.96*2*0.05=0.196$ are
statistically indistinguishable. Hence, for learners evaluated on (say) $N=2$
scores, those scores effectively divide into just
$C=\left(\frac{1}{\epsilon=0.196}\right)^{N=2}=26$ different regions. Hence,
it is hardly surprising that a few dozen repeats of Step1,2,3,4,5 were enough
to explore a seemingly very large space of options.

It has not escaped our notice that some analogy of the DODGE result could
explain the curious success of the QuickSampler heuristic. Consider: one way
to summarize Eq. 1. is that the space around existing valid test cases
contains many other valid test cases– which is an analogous idea to Argrawal’s
$\epsilon$ regions. That said, we would be hard pressed to defend that
analogy. Argrawal’s $\epsilon$ regions are a statistical concept based on
continuous variables while Eq. 1 is defined over discrete values.

Also, there are many other ways in which DODGE is fundamentally different to
Snap. DODGE was a support tool for inductive data mining applications while
Snap is most accurately described as a support tool for a deductive system
(Z3). Further, DODGE assumes very little structure in its inputs (just tables
of data with no more than a few dozen attributes) while Snap’s inputs are far
larger and far more structured (recall from Table 2 that Snap processes CNF
formula with up to hundreds of thousands of variables). Lastly, recalling
Step6 (listed above), DODGE incrementally re-weights the space from which new
options are generated. Snap, on the other hand, treats the option generator as
a black box algorithm since it does not reach inside Z3 to alter the order in
which it generates solutions.

##  8 Conclusion

Exploring propositional formula is a core computational process with many
areas of application. Here, we explore the use of such formula for test suite
generation. SAT solvers are a promising technology for finding settings that
satisfy propositional formula. The current generation of SAT solvers is
challenged by the size of the formula seen in the recent SE testing
literature.

Using the criteria listed in the introduction (runtime, scalability,
redundancy, credibility and minimality), we recommend the following “Snap
tactic” to tame the computational complexity of SAT solving for test suite
generation:

> Cluster candidate tests, then search for valid tests by via small mutations
> to the cluster centroids.

When this tactic was applied to 27 real-world test case studies, test suite
generation can ran 10 to 3000 times faster (median to max) than a prior
report. While that prior work found tests that were 70% valid, our Snap tool
generated 100% valid tests.

Another important result was the size of the test set generated in this
manner. There is an economic imperative to run fewer tests when companies have
to pay money to run each test, and when developers have to spend time studying
the failed test. In that context, it is interesting to note that Snap’s tests
are 10 to 750 times smaller (median to max) than those from prior work. We
conjecture that:

  * •

Snap’s success is due to widespread repeated structures in software. Without
such repeated structures, we are at a loss to explain our results.

  * •

Given the presence of such repeated structures, the Snap tactic might be
useful for many other SE tasks.

## Acknowledgements

This work was partially funded by an NSF award #1703487.

## References

  * Arito et al. [2012] F. Arito, F. Chicano, E. Alba,  On the application of SAT solvers to the test suite minimization problem,  in: SSBSE, Springer, 2012, pp. 45–59.
  * Baldoni et al. [2018] R. Baldoni, E. Coppa, D. C. D’elia, C. Demetrescu, I. Finocchi,  A survey of symbolic execution techniques,  ACM Computing Surveys (CSUR) 51 (2018) 50.
  * Christakis et al. [2016] M. Christakis, P. Müller, V. Wüstholz,  Guiding dynamic symbolic execution toward unverified program executions,  in: Proceedings of the 38th International Conference on Software Engineering, ACM, 2016, pp. 144–155.
  * Nie and Leung [2011] C. Nie, H. Leung,  A survey of combinatorial testing,  ACM Computing Surveys (CSUR) 43 (2011) 11.
  * Yamada et al. [2015] A. Yamada, T. Kitamura, C. Artho, E.-H. Choi, Y. Oiwa, A. Biere,  Optimization of combinatorial testing by incremental SAT solving,  in: 2015 IEEE 8th International Conference on Software Testing, Verification and Validation (ICST), IEEE, 2015, pp. 1–10.
  * Janota et al. [2008] M. Janota, V. Kuzina, A. Wasowski,  Model construction with external constraints: An interactive journey from semantics to syntax,  in: MoDELS, Springer, 2008, pp. 431–445.
  * Mendonca et al. [2009] M. Mendonca, A. Wasowski, K. Czarnecki,  Sat-based analysis of feature models is easy,  in: Proceedings of the 13th International Software Product Line Conference, Carnegie Mellon University, 2009, pp. 231–240.
  * De Moura and Bjørner [2008] L. De Moura, N. Bjørner,  Z3: An efficient smt solver,  in: International conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer, 2008, pp. 337–340.
  * Bruttomesso et al. [2008] R. Bruttomesso, A. Cimatti, A. Franzén, A. Griggio, R. Sebastiani,  The mathsat 4 smt solver,  in: International Conference on Computer Aided Verification, Springer, 2008, pp. 299–303.
  * Bjørner et al. [2015] N. Bjørner, A.-D. Phan, L. Fleckenstein,  $\nu$Z-an optimizing smt solver,  in: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer, 2015, pp. 194–199.
  * Heule et al. [2017] M. Heule, M. Järvisalo, T. Balyo,  Sat competition,  SAT (2017).
  * Dutra et al. [2018] R. Dutra, K. Laeufer, J. Bachrach, K. Sen,  Efficient sampling of SAT solutions for testing,  in: 2018 IEEE/ACM 40th International Conference on Software Engineering (ICSE), IEEE, 2018, pp. 549–559.
  * Barrett and Tinelli [2018] C. Barrett, C. Tinelli,  Satisfiability modulo theories,  in: Handbook of Model Checking, Springer, 2018, pp. 305–343.
  * Finke [2015] M. Finke,  Equisatisfiable SAT encodings of arithmetical operations,  Online] http://www. martin-finke. de/documents/Masterarbeit_bitblast_ Finke. pdf (2015).
  * Fazlalizadeh et al. [2009] Y. Fazlalizadeh, A. Khalilian, M. A. Azgomi, S. Parsa,  Prioritizing test cases for resource constraint environments using historical test case performance data,  in: 2009 2nd IEEE International Conference on Computer Science and Information Technology, IEEE, 2009, pp. 190–195.
  * Lu et al. [2016] Y. Lu, Y. Lou, S. Cheng, L. Zhang, D. Hao, Y. Zhou, L. Zhang,  How does regression test prioritization perform in real-world software evolution?,  in: 2016 IEEE/ACM 38th International Conference on Software Engineering (ICSE), 2016, pp. 535–546.
  * Mahajan et al. [2015] S. Mahajan, S. D. Joshi, V. Khanaa,  Component-based software system test case prioritization with genetic algorithm decoding technique using java platform,  in: 2015 International Conference on Computing Communication Control and Automation, 2015, pp. 847–851.
  * Haidry and Miller [2013] S. Haidry, T. Miller,  Using dependency structures for prioritization of functional test suites,  IEEE Transactions on Software Engineering 39 (2013) 258–275.
  * Yu et al. [2019] Z. Yu, F. Fahid, T. Menzies, G. Rothermel, K. Patrick, S. Cherian,  Terminator: better automated UI test case prioritization,  in: Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2019, pp. 883–894.
  * Chittimalli and Harrold [2007] P. K. Chittimalli, M. J. Harrold,  Re-computing coverage information to assist regression testing,  in: 2007 IEEE International Conference on Software Maintenance, 2007, pp. 164–173.
  * Parnin et al. [2017] C. Parnin, E. Helms, C. Atlee, H. Boughton, M. Ghattas, A. Glover, J. Holman, J. Micco, B. Murphy, T. Savor, et al.,  The top 10 adages in continuous deployment,  IEEE Software 34 (2017) 86–95.
  * Olvera-Lopez et al. [2010] J. A. Olvera-Lopez, J. A. Carrasco-Ochoa, J. F. Martinez-Trinidad, J. Kittler,  A review of instance selection methods,  ARTIFICIAL INTELLIGENCE REVIEW 34 (2010) 133 – 143. URL: http://epubs.surrey.ac.uk/111090/. doi:10.1007/s10462-010-9165-y.
  * Yu et al. [2019] Z. Yu, C. Theisen, L. Williams, T. Menzies,  Improving vulnerability inspection efficiency using active learning,  IEEE Transactions on Software Engineering (2019).
  * Sucholutsky and Schonlau [2020] I. Sucholutsky, M. Schonlau, ’less than one’-shot learning: Learning n classes from m¡n samples, 2020. arXiv:2009.08449.
  * Yuan et al. [1999] J. Yuan, K. Shultz, C. Pixley, H. Miller, A. Aziz,  Modeling design constraints and biasing in simulation using bdds,  in: Proceedings of the 1999 IEEE/ACM international conference on Computer-aided design, IEEE Press, 1999, pp. 584–590.
  * Iyer [2003] M. A. Iyer,  RAVE: a word-level atpg-based constraints solver system for smart random simulation,  in: International Test Conference, 2003. Proceedings. ITC 2003., volume 1, 2003, pp. 299–308.
  * Yuan et al. [2004] J. Yuan, A. Aziz, C. Pixley, K. Albin,  Simplifying boolean constraint solving for random simulation-vector generation,  IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 23 (2004) 412–420.
  * Wei et al. [2004] W. Wei, J. Erenrich, B. Selman,  Towards efficient sampling: Exploiting random walk strategies,  in: AAAI, volume 4, 2004, pp. 670–676.
  * Gogate and Dechter [2011] V. Gogate, R. Dechter,  Samplesearch: Importance sampling in presence of determinism,  Artificial Intelligence 175 (2011) 694–729.
  * Ermon et al. [2012] S. Ermon, C. P. Gomes, B. Selman,  Uniform solution sampling using a constraint solver as an oracle,  arXiv preprint arXiv:1210.4861 (2012).
  * Chakraborty et al. [2014] S. Chakraborty, K. S. Meel, M. Y. Vardi,  Balancing scalability and uniformity in SAT witness generator,  in: Proceedings of the 51st Annual Design Automation Conference, ACM, 2014, pp. 1–6.
  * Chakraborty et al. [2015] S. Chakraborty, D. J. Fremont, K. S. Meel, S. A. Seshia, M. Y. Vardi,  On parallel scalable uniform SAT witness generation,  in: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer, 2015, pp. 304–319.
  * Meel et al. [2016] K. S. Meel, M. Y. Vardi, S. Chakraborty, D. J. Fremont, S. A. Seshia, D. Fried, A. Ivrii, S. Malik,  Constrained sampling and counting: Universal hashing meets SAT solving,  in: Workshops at the thirtieth AAAI conference on artificial intelligence, 2016.
  * Menzies et al. [2006] T. Menzies, J. Greenwald, A. Frank,  Data mining static code attributes to learn defect predictors,  IEEE transactions on software engineering 33 (2006) 2–13.
  * Chen et al. [2005] Z. Chen, T. Menzies, D. Port, D. Boehm,  Finding the right data for software cost modeling,  IEEE Software 22 (2005) 38–46. doi:10.1109/MS.2005.151.
  * Nair et al. [2020] V. Nair, Z. Yu, T. Menzies, N. Siegmund, S. Apel,  Finding faster configurations using flash,  IEEE Transactions on Software Engineering 46 (2020) 794–811. doi:10.1109/TSE.2018.2870895.
  * Zhang et al. [????] Q. Zhang, J. Wang, M. A. Gulzar, R. Padhye, M. Kim,  Bigfuzz: Efficient fuzz testing for data analytics using framework abstraction,  in: ASE’20, ????
  * Hindle et al. [2012] A. Hindle, E. T. Barr, Z. Su, M. Gabel, P. Devanbu,  On the naturalness of software,  in: 2012 34th International Conference on Software Engineering (ICSE), IEEE, 2012, pp. 837–847.
  * Ray et al. [2016] B. Ray, V. Hellendoorn, S. Godhane, Z. Tu, A. Bacchelli, P. Devanbu,  On the” naturalness” of buggy code,  in: 2016 IEEE/ACM 38th International Conference on Software Engineering (ICSE), IEEE, 2016, pp. 428–439.
  * Zhang [2008] H. Zhang,  Exploring regularity in source code: Software science and zipf’s law,  in: 2008 15th Working Conference on Reverse Engineering, IEEE, 2008, pp. 101–110.
  * Lin and Whitehead [2015] Z. Lin, J. Whitehead,  Why power laws? an explanation from fine-grained code changes,  in: 2015 IEEE/ACM 12th Working Conference on Mining Software Repositories, IEEE, 2015, pp. 68–75.
  * Jia et al. [2015] X. Jia, C. Ghezzi, S. Ying,  Enhancing reuse of constraint solutions to improve symbolic execution,  in: Proceedings of the 2015 International Symposium on Software Testing and Analysis, ACM, 2015, pp. 177–187.
  * Visser et al. [2006] W. Visser, C. S. Pasareanu, R. Pelánek,  Test input generation for java containers using state matching,  in: Proceedings of the 2006 international symposium on Software testing and analysis, ACM, 2006, pp. 37–48.
  * Akers [1978] S. B. Akers,  Binary decision diagrams,  IEEE Trans. Computers (1978) 509–516.
  * Selman et al. [1993] B. Selman, H. A. Kautz, B. Cohen, et al.,  Local search strategies for satisfiability testing.,  Cliques, coloring, and satisfiability 26 (1993) 521–532.
  * Mansour et al. [1993] Y. Mansour, N. Nisan, P. Tiwari,  The computational complexity of universal hashing,  Theoretical Computer Science 107 (1993) 121–133.
  * Feldt et al. [2016] R. Feldt, S. Poulding, D. Clark, S. Yoo,  Test set diameter: Quantifying the diversity of sets of test cases,  in: 2016 IEEE International Conference on Software Testing, Verification and Validation (ICST), IEEE, 2016, pp. 223–233.
  * Li and Vitányi [2013] M. Li, P. Vitányi, An introduction to Kolmogorov complexity and its applications, Springer Science & Business Media, 2013\.
  * Bochkanov and Bystritsky [2013] S. Bochkanov, V. Bystritsky,  Alglib,  Available from: www. alglib. net 59 (2013).
  * Goldberg and Holland [1988] D. E. Goldberg, J. H. Holland,  Genetic algorithms and machine learning (1988).
  * Golovin et al. [2017] D. Golovin, B. Solnik, S. Moitra, G. Kochanski, J. Karro, D. Sculley,  Google vizier: A service for black-box optimization,  in: Proceedings of the 23rd ACM SIGKDD international conference on knowledge discovery and data mining, 2017, pp. 1487–1495.
  * Nair et al. [2018] V. Nair, Z. Yu, T. Menzies, N. Siegmund, S. Apel,  Finding faster configurations using flash,  IEEE TSE (2018).
  * Krishna et al. [2020] R. Krishna, V. Nair, P. Jamshidi, T. Menzies,  Whence to learn? Transferring knowledge in configurable systems using BEETLE,  IEEE Transactions on Software Engineering (2020) 1–1.
  * Shannon [1948] C. E. Shannon,  A mathematical theory of communication,  Bell system technical journal 27 (1948) 379–423.
  * Perez et al. [2017] A. Perez, R. Abreu, A. van Deursen,  A test-suite diagnosability metric for spectrum-based fault localization approaches,  in: 2017 IEEE/ACM 39th International Conference on Software Engineering (ICSE), IEEE Computer Society, Los Alamitos, CA, USA, 2017, pp. 654–664. doi:10.1109/ICSE.2017.66.
  * Ostrand et al. [2004] T. J. Ostrand, E. J. Weyuker, R. M. Bell,  Where the bugs are,  in: Proceedings of the 2004 ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA’04, 2004, pp. 86–96. doi:10.1145/1007512.1007524.
  * Deng et al. [2009] S. Deng, Z. Kong, J. Bian, Y. Zhao,  Self-adjusting constrained random stimulus generation using splitting evenness evaluation and xor constraints,  in: 2009 Asia and South Pacific Design Automation Conference, IEEE, 2009, pp. 769–774.
  * Hand and Adams [2014] D. J. Hand, N. M. Adams,  Data mining,  Wiley StatsRef: Statistics Reference Online (2014) 1–7.
  * Gulzar et al. [2019] M. A. Gulzar, S. Mardani, M. Musuvathi, M. Kim,  White-box testing of big data analytics with complex user-defined functions,  in: FSE’19, 2019, pp. 290–301.
  * Chen et al. [2018a] J. Chen, V. Nair, R. Krishna, T. Menzies,  “Sampling” as a baseline optimizer for search-based software engineering,  IEEE Transactions on Software Engineering (2018a).
  * Chen et al. [2018b] J. Chen, V. Nair, T. Menzies,  Beyond evolutionary algorithms for search-based software engineering,  Information and Software Technology 95 (2018b) 281–294.
  * Menzies and Richardson [2005] T. Menzies, J. Richardson,  XOMO: Understanding development options for autonomy,  in: COCOMO forum, volume 2005, 2005\.
  * Chen and Menzies [2018] J. Chen, T. Menzies,  RIOT: A stochastic-based method for workflow scheduling in the cloud,  in: 2018 IEEE 11th International Conference on Cloud Computing (CLOUD), IEEE, 2018, pp. 318–325.
  * Agrawal et al. [2019] A. Agrawal, W. Fu, D. Chen, X. Shen, T. Menzies,  How to ”DODGE” complex software analytics,  IEEE Transactions on Software Engineering (2019) 1–1.