CoVeriTest: Cooperative Verifier-Based Testing

Testing is a commonly used technique to measure the quality of software. Since manually creating such test suites is laborious, automatic techniques are used: e.g., model-based techniques for black-box testing and techniques based on control-flow coverage for white-box testing. Many automatic techniques have been proposed, ranging from random testing [36, 57] and fuzzing [26, 52, 53], over search-basedtesting [55] to symbolic execution [23, 24, 58] and reachability analyses [5, 12, 45, 46]. The latter are well-suited to find bugs and derive test suites that achieve high coverage, and several verification tools support test generation (e.g., [5], [61], [12]). The reachability checks for all test goals seem too expensive, but in practice, those approaches can be made pretty efficient.

Encouraged by tremendous advances in software verification [3] and a recent case study that compared model checkers with test tools w.r.t. bug finding [17], we study a new kind of combination of reachability analyses for test generation. Combinations are necessary because different analysis techniques have different strength and weaknesses. For example, consider function foo in Listing 1. Explicit state model checking [18, 33] tracks the values of variables i and s and easily detects the reachability of the statements in the outermost if branch (lines 3–6), while it has difficulties with the complex condition in the else-branch (line 8). In contrast, predicate abstraction [33, 39] can easily derive test values for the complex condition in line 8, but to handle the if branch (lines 3–6) it must spent effort on the detection of the predicates \({s=0}\), \({s=1}\), and \({i=0}\). Independently of each other, test approaches [1, 34, 47, 54] and verification approaches [9, 10, 29, 37] employ combinations to tackle such problems. However, there are no approaches yet that combine different reachability analyses for test generation.

Inspired by abstraction-driven concolic testing [32], which interleaves concolic execution and predicate abstraction, we propose , which stands for cooperative verifier-based testing. iteratively executes a given sequence of reachability analyses. In each iteration, the analyses are run in sequence and each analysis is limited by its individual, but configurable time limit. Furthermore, allows the analysis to share various types of analysis information, e.g., which paths are infeasible, have already been explored, or which abstraction level to use. To get access to a large set of reachability analyses, we implemented in the configurable software-analysis framework [15]. We used our implementation to evaluate different configurations on a large set of well-established benchmark programs and to compare with existing state-of-the-art test-generation techniques. Our experiments confirm that reachability analyses are valuable for test generation.

Contributions. In summary, we make the following contributions:

The basic idea behind testing with verifiers is to derive test cases from counterexamples [5, 61]. Thus, meeting a test goal during verification has to trigger a specification violation. First, we remind the reader of some basic notations.

Programs. Following literature [9], we represent programs by control-flow automata (CFAs). A CFA \(P=(L,\ell _0,G)\) consists of a set L of program locations (the program-counter values), an initial program location \(\ell _0\in L\), and a set of control-flow edges \(G\subseteq L\times Ops\times L\). The set Ops describes all possible operations, e.g., assume statements (resulting from conditions in if or while statements) and assignments. For the program semantics, we rely on an operational semantics, which we do not further specify.

Abstract Reachability Graph (ARG). ARGs record the work done by reachability analyses. An ARG is constructed for a program \(P=(L,\ell _0,G)\) and stores (a) the abstract state space that has been explored so far, (b) which abstract states must still be explored, and (c) what abstraction level (tracked variables, considered predicates, etc.) is used. Technically, an ARG is a five-tuple \((N, succ , root , F, \pi )\) that consists of a set N of abstract states, a special node \( root \in N\) that represents the initial states of program P, a relation \( succ \subseteq N\times G\times N\) that records already explored successor relations, a set \(F\subseteq N\) of frontier nodes, which remembers all nodes that have not been fully explored, and a precision \(\pi \) describing the abstraction level. Every ARG must ensure that a node n is either contained in F or completely explored, i.e., all abstract successors have been explored. We use ARGs for information exchange between reachability analyses.

Test Goals. In this paper, we are interested in structural coverage, e.g., branch coverage. Transferred to our notion of programs, this means that our test goals are a subset of the program’s control-flow edges. For using a verifier to generate tests, we have to encode the test goals as a specification violation. Figure 2 shows a possible encoding, which uses a protocol automaton. Whenever a test goal is executed, the automaton transits from the initial, safe state \(q_0\) to the accepting state \(q_e\), which marks a property violation. Note that reachability analyses, which we consider for test generation, can easily monitor such specifications during exploration.

Now, we have everything at hand to describe how reachability analyses generate tests. Algorithm 1 shows the test-generation process. The algorithm gets as input a program, a set of test goals, and a time limit for test generation. For cooperative test generation, we need to guide state-space explorations. To this end, we also provide an initial ARG and a condition. A condition is a concept known from conditional model checking [10] and describes which parts of the state space have already been explored by other verifiers. A verifier, e.g., a reachability analysis, can use a condition to ignore the already explored parts of the state space. Verifiers that do not understand conditions can safely ignore them.

At the beginning, Alg. 1 sets up the data structures for the test suite and the set of covered goals. To set up the specification, it follows the idea of Fig. 2. As long as not all test goals are covered, there exist abstract states that must be explored, and the time limit has not elapsed, the algorithm tries to generate new tests. Therefore, it resumes the exploration of the current ARG [5] taking into account program prog, specification \(\varphi \), and (if understood) the condition \(\psi \). If the exploration stops, then it returns an updated ARG. Exploration stops due to one of three reasons: (1) the state space is explored completely (\(F=\emptyset \)), (2) the time limit is reached, or (3) a counterexample has been found.³ In the latter case, a new test is generated. First, a counterexample trace is extracted from the ARG. The trace describes a path through the ARG that starts at the root and its last edge is a test goal (the reason for the specification violation). Next, a test is constructed from the path and added to the test suite. Basically, the path is converted into a formula and a satisfying assignment⁴ is used as the test case. For the details, we refer the reader to the work that defined the method [5]. Additionally, the covered goal (last edge on the counterexample path) is removed from the set of open test goals and added to the set of covered goals. Finally, the specification is updated to no longer consider the covered goal. When the algorithm finishes, it returns the generated test suite, the set of covered goals and the last ARG considered. The ARG is returned to enable cooperation.

The previous section described how to use a single reachability analysis to produce tests for covering a set of test goals. Due to different strengths and weaknesses, some test goals are harder to cover for one analysis than for another. To maximize the number of covered goals, different analyses should be combined. In , we rotate analyses for test generation. Thus, we avoid that analyses try to cover the same goal in parallel and we do not need to know in advance which analysis can cover which goals. Moreover, analyses that get stuck trying to cover goals that other analyses handle later, get a chance to recover. Additionally, supports cooperation among analyses. More concrete: analyses may extract and use information from ARGs constructed by previous analysis runs.

Algorithm 2 describes the workflow. It gets four inputs. Program, test goals, and time limit are already known from Alg. 1 (test generation with a single analysis). Additionally, gets a sequence of configurations, namely pairs of reachability analysis and time limit. The time limit accompanied with the analysis restricts the runtime of the respective analysis per call (see line 5). In contrast to Alg. 1, does not get an ARG or condition. To enable cooperation between analyses, constructs these two elements individually for each analysis run. During construction, it may extract and use information from results of previous analysis runs.

After initializing the test suite and the data structure to store analysis results (args), repeatedly iterates over the configurations. It starts with the first pair in the sequence and finishes iterating when its time limit exceeded or all goals are covered. In each iteration, first extracts the analysis to execute and its accompanied time limit (line 3). Then, it constructs the remaining inputs of the analysis: ARG and condition. Details regarding the construction are explained later in Alg. 3. Next, executes the current analysis with the given program, the remaining test goals, the accompanied time limit, and the constructed ARG and condition. When the analysis has finished, adds the returned tests to its test suite, removes all test goals covered by the analysis run from the set of goals, and stores the analysis result for cooperation (concatenates arg to the sequence of ARGs). If the analysis finished its exploration (arg.F=\(\emptyset \)), any remaining test goal should be unreachable and returns its test suite. Otherwise, determines how to continue in the next iteration (i.e., which configuration to consider). At the end of all iterations, returns its generated test suite.

Next, we explain how to construct the ARG and the condition input for an analysis. The ARG describes the level of abstraction and where to continue exploration while the condition describes which parts of the state space have already been explored. Both guide the exploration of an analysis, which makes them well-suited for cooperation. While there are plenty of possibilities for cooperation, we currently only support three basic options: continue exploration of the previous ARG of the analysis (reuse-arg), reuse the analysis’ abstraction level (reuse-precision), and restrict the exploration to the state space left out by the previous analysis (use-condition). The first two options only ensure that an analysis does not loose too much information due to switching. The last option, which is inspired by abstraction-driven concolic execution [32], indeed realizes cooperation between different analyses. Note that the last two options can also be combined.⁵ If all options are turned off, no information will be exchanged.

Algorithm 3 shows the cooperative initialization of ARG and condition discussed above. It gets three inputs: the program, a sequence of args needed to realize cooperation, and the number of analyses used. At the beginning, it initializes the ARG components and the condition assuming no cooperation should be done. The condition states that nothing has been explored, the abstraction level becomes the coarsest available, and the ARG root considers the start of all program executions (initial program location and arbitrary variable values). If no cooperation is configured or the ARG required for cooperation is not available (e.g., in the first round), the returned ARG and condition tell the analysis to explore the complete state space from scratch. In all other cases, the analysis will be guided by information obtained in previous iterations. Option reuse-arg looks up the last ARG of the analysis stored in args. Reuse-precision considers the same ARG as reuse-arg, but only provides the ARG’s precision \(\pi \). For use-condition, a condition is constructed from the last ARG in args. For the details of the condition construction, we refer to conditional model checking [10].

Next, we study the effectiveness of different configurations and compare with existing test-generation tools.

We systematically evaluate along the following claims:

Claim 1. For analyses that discard their own results from previous iterations (i.e., reuse-arg and reuse-precision turned off), achieves higher coverage if switches between analyses happen rarely. Evaluation Plan: We look at configurations in which analyses discard their own, previous results and compare the number of covered test goals reported by configurations that only differ in the analyses’ time limits.

Claim 2. For analyses that reuse knowledge from their own, previous execution (i.e., reuse-arg or reuse-precision turned on), achieves higher coverage if favoring more powerful analyses. Evaluation Plan: We look at configurations in which analyses reuse their own, previous knowledge and compare the number of covered test goals reported by configurations that only differ in the analyses’ time limits.

Claim 3. performs better if analyses reuse knowledge from their own, previous execution (i.e., reuse-arg or reuse-precision turned on). Evaluation Plan: From all sets of configurations that only differ in the analyses’ time limits, we select the best and compare these.

Claim 4. Interleaving multiple analyses with often achieves better results than using only one of the analyses for test generation. Evaluation Plan: We compare the number of covered goals reported by the best configuration with those numbers achieved when running only one analysis of the configuration for the total time limit.

Claim 5. Interleaving verifiers for test generation is often better than running them in parallel. Evaluation Plan: We compare the number of covered goals reported by the best configuration with the number achieved when running all analyses of the configuration in parallel.

Claim 6. complements existing test-generation tools. Evaluation Plan: We use the same infrastructure and resources as used by the International Competition on Software Testing (Test-Comp’19)⁶ and let the best configuration construct test suites. These test suites are executed by the Test-Comp’19 validator to measure the achieved branch coverage. Then, we compare the coverage achieved by with the coverage of the best two test-generation tools from Test-Comp’19.

interleaves reachability analyses to construct tests for C programs. To enable cooperation, extracts information from ARGs constructed by previous analysis runs.

A few tools use reachability analyses for test generation. [5] considers a target predicate p and generates a test for each program location that can be reached with a state fulfilling the predicate p. For test generation, uses predicate abstraction. [44‐46] and [12] generate tests for a coverage criterion specified in the query language (FQL) [46]. Both transform the FQL specification into a set of test-goal automata and check for each automaton whether its final state can be reached. uses CBMC to answer those reachability queries and uses predicate abstraction.

Various combinations have been proposed for verification [2, 10, 11, 14, 25, 27, 29‐31, 35, 37, 40, 50, 64] and test-suite generation [1, 32, 34, 36, 38, 47, 51, 54, 56, 59, 60, 63]. We focus on combinations that interleave approaches. SYNERGY [40] and DASH [2] alternate test generation and proof construction to (dis)prove a property. Similarly, SMASH [37] combines underapproximation with overapproximation. Interleaving is also used in test generation. Hybrid concolic testing [54] interleaves random testing with symbolic execution. When random testing gets stuck, symbolic execution is started from the current state. As soon as a new goal is covered, symbolic execution hands over to random testing providing the values used to cover the goal. Similarly, Driller [60] and Badger [56] combine fuzzing with concolic execution. However, they only exchange inputs. Xu et al. [51, 63] interleave different approaches to augment test suites. The approach closest to is abstraction-driven concolic testing [32]. Abstraction-driven concolic testing interleaves concolic execution and predicate analysis. Furthermore, it uses conditions extracted from the ARGs generated by the predicate analysis to direct the concolic execution towards feasible paths. Abstraction-driven concolic testing can be seen as one particular configuration of .

Also, ARG information has been reused in different contexts. Precision reuse [19] uses the precision determined in a previous analysis run to reverify a modified program. Similarly, extreme model checking [42] adapts an ARG constructed in a previous analysis to fit to the modified program.  [12] transforms an ARG that was constructed for one test goal such that it fits to a new test goal. Lazy abstraction refinement [43] adapts an ARG to continue exploration after abstraction refinement. Configurable program certification [48, 49] constructs a certificate from an ARG, which can be used to reverify a program. Similarly, reachability tools like construct witnesses [6, 7] from ARGs. Conditional model checking [10, 14] constructs a condition from an ARG when a verifier gives up. The condition describes the remaining verification task and is used by a subsequent verifier to restrict its exploration.

Testing is a standard technique for software quality assurance. But state-of-the-art techniques still miss many bugs that involve sophisticated branching conditions [17]. It turns out that techniques performing abstract reachability analyses are well-suited for this task. They simply need to check the reachability of every branch and generate a test for each positive check. However, in practice, for every such technique there exist reachability queries on which the technique is inefficient or fails [8]. We propose to overcome these practical limitations. interleaves different reachability analyses for test generation. We experimented with various configurations of , which vary in the time limits of the analyses and the type of information exchanged between different analysis runs. works best when each analysis resumes its exploration, different analyses only share test goals, and more powerful analyses get larger time budgets. Moreover, a comparison of with (a) the reachability analyses used by and (b) state-of-the-art test-generation tools witness the benefits of the new approach.

participated in Test-Comp 2019 [4] and achieved rank 3 (out of 9) in both categories, bug finding and branch coverage.¹⁷

In future, we plan to integrate further analyses, e.g., bounded model checking or symbolic execution, into and to evaluate on real-world applications.