Parallel Program Analysis via Range Splitting

Recent years have seen enormous progress in automatic software verification, driven amongst others by annual competitions like SV-COMP [13]. Software verification tools employ a bunch of different techniques for analysis, like predicate analysis, bounded model checking, k-induction, property-directed reachability, or automata-based methods. As however none of these techniques is superior over the others, today often a form of cooperative verification [24] is employed. The idea of cooperative verification is to have different sorts of analyses cooperate on the task of software verification. This principle has already been implemented in various forms [16, 19, 33, 59], in particular also as cooperations of testing and verification tools [10, 39, 41, 42]. Such cooperations most often take the form of sequential combinations, where one tool starts with the full task, stores its partial analysis result within some verification artefact, and the next tool then works on the remaining task. In contrast, parallel execution of different tools is in the majority of cases only done by portfolio approaches, simply running the different tools on the same task in parallel. One reason for using portfolios when employing parallel execution is the fact that it is unclear how to best split a program into parts on which different tools could work separately while still being able to join their partial results into one for the entire program.

With ranged symbolic execution, Siddiqui and Khurshid [86] proposed one such technique for splitting programs into parts. The idea of ranged symbolic execution is to scale symbolic execution by splitting path exploration onto several workers, thereby, in particular allowing the workers to operate in parallel. To this end, they defined so-called path ranges. A path range describes a set of program paths defined by two inputs to the program, where the path \(\pi _1\) triggered by the first input is the lower bound and the path \(\pi _2\) for the second input is the upper bound of the range. All paths in between, i.e., paths \(\pi \) such that \(\pi _1 \! \le \! \pi \! \le \! \pi _2\) (based on some ordering \(\mathord {\le }\) on paths), make up a range. A worker operating on a range performs symbolic execution on paths of the range only. In their experiments, Siddiqui and Khurshid investigated one form of splitting via path ranges, namely by randomly generating inputs, which then make up a number of ranges.

In this paper, we generalize ranged symbolic execution to arbitrary analyses. In particular, we introduce the concept of a ranged analysis to execute an arbitrary analysis on a given range and compose different ranged analyses, which can then operate on different ranges in parallel. Also, we propose a novel splitting strategy, which generates ranges along loop bounds. We implemented ranged analysis in the software verification tool CPAchecker  [21], which already provides a number of analyses, all defined as configurable program analyses (CPAs). To integrate ranged analysis in CPAchecker, we defined a new range reduction CPA, and then employed the built-in feature of analysis composition to combine it with different analyses. The thus obtained ranged analyses are then run on different ranges in parallel, using CoVeriTeam  [20] as tool for orchestration. We furthermore implemented two strategies for generating path ranges, our novel strategy employing loop bounds for defining ranges plus the original random splitting technique. A loop bound n splits program paths into ranges only entering the loop at most n times and ranges entering for more than n times¹.

Our evaluation on SV-COMP benchmarks [36] first of all confirms the results of Siddiqui and Khurshid [86] in that symbolic execution benefits from a ranged execution. Second, our results show that a loop-bound based splitting strategy brings an improvement over random splitting. Finally, we see that a composition of ranged analyses can solve analysis tasks that none of the (different) constituent analyses of a combination can solve alone.

We start by introducing some notations on programs, defining path ranges, and introducing configurable program analysis as implemented in CPAchecker.

In this section, we introduce the composition of ranged analyses as a generalization of ranged symbolic execution to arbitrary program analyses. The overall goal is to split the program paths into multiple disjoint ranges each of which is being analysed by a (different) program analysis. Therein, the task of a program analysis is to verify whether a program fulfils a given specification. Specifications are often given in the form of error locations, so that the task is proving the unreachability of error locations. The results for the verification task contain a verdict and potentially an additional witness (a justification or a concrete path violating the specification [14]). The verdict indicates whether the program fulfils the specification (verdict “true”), violates it (verdict “false”) or if the analysis did not compute a result (verdict “unknown”).

To ensure that an arbitrary program analysis operates on paths within a given range only, we employ ranged analysis. A ranged analysis is realized as a composition of an arbitrary program analysis (a CPA) and a range reduction (also given as a CPA below) ensuring path exploration to stay within the range. Then, a composition of ranged analyses is obtained by (1) splitting the program into ranges, (2) then running several ranged analyses in parallel, and (3) at the end aggregating analysis results (see Fig. 2). Splitting is described in Sec. 4. For aggregation, we simply return the verdict “false” whenever one analysis returns “false”, we return “unknown” whenever no analysis returns “false” and one analysis returns “unknown” or aborts, otherwise we return “true”. We do not support aggregation of witnesses yet (but this could be realized similar to [70]).

A crucial part of the ranged analysis is the generation of ranges, i.e., the splitting of programs into parts that can be analysed in parallel. The splitting has to either compute two paths or two test cases, both defining one range. Ranged symbolic execution [86] employs a random strategy for range generation (together with an online work-stealing concept to balance work among different workers). For the work here, we have also implemented this random strategy, selecting random paths in the execution tree to make up ranges. In addition, we propose a novel strategy based on the number of loop unrollings. Both strategies are designed to work “on-the-fly” meaning that none requires building the full execution tree upfront, they rather only compute the paths or test cases that are used to fix a range. Next, we explain both strategies in more detail, especially how they are used to generate more than two ranges.

Bounding the Number of Loop Unrollings (Lb). Given a loop bound \(i \in \mathbb {N}\), the splitting computes the left-most path in the program that contains exactly i unrollings of the loop. If the program contains nested loops, each nested loop is unrolled for i times in each iteration of the outer loop. For the computed path, we (1) build its path formula using the strongest post-condition operator [46], (2) query an SMT-solver for satisfiability and (3) in case of an answer SAT, use the evaluation of the input variables in the path formula as one test case. In case that the path formula is unsatisfiable, we iteratively remove the last statement from the path, until a satisfying path formula is found. A test case \(\tau \) determined in this way defines two ranges, namely \([\pi _{^{_\bot }},\pi _\tau ]\) and \([\pi _\tau ,\pi ^{_{\top }}]\). In case that the program is loop-free, the generation of a test case fails and we generate a single range \([\pi _{^{_\bot }}, \pi ^{_{\top }}]\). In the experiments, we used the loop bounds 3 (called Lb3) and 10 (called Lb10) with two ranges each. To compute more than two ranges, we use intervals of loop bounds.

Generating Ranges Randomly (Rdm). The second splitting strategy selects the desired number of paths randomly. At each assume edge in the program (either a loop head or an if statement), it follows either the true- or the false-branch with a probability of 50%, until it reaches a node in the CFA without successor. Again, we compute the path formula for that path and build a test case. This purely random approach is called Rdm.

To show the advantages of the composition of ranged analyses, especially the possibility of running conceptually different analyses on different ranges of a program, we realized the range reduction from Sec. 3.2 and the ranged analyses in the tool CPAchecker  [21]. The realization of the range reduction follows our formalization, i.e., it reuses elements from the value analysis, which are already implemented within CPAchecker.

Due to the composite pattern, we can build a ranged analysis as composition of range reduction and any existing program analysis within CPAchecker with nearly no effort. We can also use other (non CPA-based) off-the-shelf analyses by employing the construction depicted in Fig. 4: Instead of running the analysis in parallel with the range reduction CPA, we can build a sequential composition of the range reduction and the analysis itself. As off-the-shelf tools take programs as inputs, not ranges, we first construct a reduced program, which by construction only contains the paths within the given range. For this, we can use the existing residual program generation within CPAchecker  [19].

The composition of ranged analyses from Sec. 3 is realized using the tool CoVeriTeam  [20]. CoVeriTeam allows building parallel and sequential compositions using existing program analyses, like the ones of CPAchecker. We use CoVeriTeam for the orchestration of the composition of ranged analyses. The implementation follows the structure depicted in Fig. 2 and also contains the Aggregation component. It is configured with the program analysis \(\mathbb {A}_1, \cdots , \mathbb {A}_n\) and a splitting component. For splitting, we realized the splitters Lb3, Lb10, Rdm and Rdm9 in CPAchecker. Each splitter generates test cases in the standardized XML-based TEST-Comp test case format⁷. In case that the splitter fails (e.g. Lb3 cannot compute a test-case, if the program does not contain a loop) our implementation executes the analysis \(\mathbb {A}_1\) on the interval \([\pi _{^{_\bot }}, \pi ^{_{\top }}]\). For the evaluation, we used combinations of three existing program analyses within the ranged analysis, briefly introduced next.

Symbolic Execution. Symbolic execution [73] analyses program paths based on symbolic inputs. Here, states are pairs of a symbolic store, which describes variable values by formulae on the symbolic inputs, and a path condition, which tracks the executability of the path. Operations update the symbolic store and at branching points the path condition is extended by the symbolic evaluation of the branching condition. Furthermore, the exploration of a path is stopped when it reaches the program end or its path condition becomes unsatisfiable.

Predicate Analysis. We use CPAchecker ’s standard predicate analysis, which is configured to perform model checking and predicate abstraction with adjustable block encoding [22] such that it abstracts at loop heads only. The required set of predicates is determined by counterexample-guided abstraction refinement [35], lazy refinement [64], and interpolation [63].

Bounded Model Checking. We use iterative bounded model checking (BMC). Each iteration inspects the behaviour of the CFA unrolled up to loop bound k and increases the loop bound in case no property violation was detected. To inspect the behaviour, BMC first encodes the unrolled CFA and the property in a formula using the unified SMT-based approach for software verification [15]. Thereafter, it checks the satisfiability of the formula encoding to detect property violations.

For the evaluation, we build four different basic configurations and employed our different range splitters: Ra-2Se and Ra-3Se which employ two resp. three instances of symbolic execution in parallel, Ra-2bmc employing two instances of BMC and Ra-Se-Pred that uses symbolic execution for the range \([\pi _{^{_\bot }},\pi _\tau ]\) and predicate analysis on \([\pi _\tau ,\pi ^{_{\top }}]\) for some computed test input \(\tau \).

Siddiqui and Khurshid concentrated their evaluation on the issue of scaling, i.e., showing that a certain speed-up can be achieved by ranged execution [86]. More specifically, they showed that ranged symbolic execution can speed-up path exploration when employing ten workers operating on ranges in parallel. In contrast, our interest was not in scaling issues only, but also in the obtained verification results. We in particular wanted to find out whether a ranged analysis can obtain more results for verification tasks than analyses in isolation would achieve within the same resource limitations. Furthermore, our evaluation is different to [86] in that we limit the available CPU time, meaning that both analyses, the default analysis and the composition of ranged analyses, have the same resources and that we employ different analyses. Finally, we were interested in evaluating our novel splitting strategy, in particular in comparison to the existing random strategy. To this end, we studied the following research questions:

Numerous approaches combine different verification techniques. Selective combinations [6, 40, 45, 51, 72, 83, 92] consider certain features of a task to choose the best approach for that task. Nesting approaches [3, 4, 25, 26, 30, 32, 49, 82, 84] use one or more approaches as components in a main approach. Interleaved approaches [1, 2, 5, 10, 42, 50, 55, 58, 62, 68, 75, 78, 90, 97] alternate between different approaches that may or may not exchange information. Testification approaches [28, 29, 39, 43, 52, 74, 81] often sequentially combine a verification and a validation approach and prioritize or only report confirmed proofs and alarms. Sequential portfolio approaches [44, 61] run distinct, independent analyses in sequence while parallel portfolio approaches [91, 12, 63, 65, 66, 96] execute various, independent analyses in parallel. Parallel white-box combinations [7, 9, 37, 38, 54, 56, 59, 79] run different approaches in parallel, which exchange information for the purpose of collaboration. Next, we discuss cooperation approaches that split the search space as we do.

A common strategy for dividing the search space in sequential or interleaved combinations is to restrict the subsequent verifiers to the yet uncovered search space, e.g., not yet covered test goals [12], open proof obligations [67], or yet unexplored program paths [8, 10, 19, 31, 33, 41, 42, 47, 53, 71]. Some parallel combinations like CoDiDroid [80], distributed assertion checking [93], or the compositional tester sketched in conditional testing [12] decompose the verification statically into separate subtasks. Furthermore, some techniques split the search space to run different instances of the same analysis in parallel on different parts of the program. For example, conditional static analysis [85] characterizes paths based on their executed program branches and uses sets of program branches to describe the split. Concurrent bounded model checking techniques [69, 77] split paths based on their thread interleavings. Yan et al. [95] dynamically split the input space if the abstract interpreter returns an inconclusive result and analyses the input partitions separately with the abstract interpreter. To realize parallel test-case generation, Korat [76] considers different input ranges in distinct parallel instances. Parallel symbolic execution approaches [82, 86, 87, 8889, 94] and ranged model checking [48] split execution paths, thereby often partitioning the execution tree. The set of paths are characterized by input constraints [89], path prefixes [87, 88], or ranges [82, 86, 94, 48] and are either created statically from an initial shallow symbolic execution [87, 88, 89] or tests [82, 86, 94] or dynamically based on the already explored symbolic execution tree [27, 34, 82, 86, 98]. While we reuse the idea of splitting the program paths into ranges [82, 86, 94, 48], we generalize the idea of ranged symbolic execution [82, 86, 94] to arbitrary analyses and in particular allow to combine different analyses. Furthermore, we introduce a new static splitting strategy along loop bounds.