Enforcing Termination of Interprocedural Analysis

Abstract

Interprocedural analysis by means of partial tabulation of summary functions may not terminate when the same procedure is analyzed for infinitely many abstract calling contexts or when the abstract domain has infinite strictly ascending chains. As a remedy, we present a novel local solver for general abstract equation systems, be they monotonic or not, and prove that this solver fails to terminate only when infinitely many variables are encountered. We clarify in which sense the computed results are sound. Moreover, we show that interprocedural analysis performed by this novel local solver, is guaranteed to terminate for all non-recursive programs — irrespective of whether the complete lattice is infinite or has infinite strictly ascending or descending chains.

A Experimental Evaluation

We implemented the solvers TSTP and TSMP presented in Sects. 6 and 7 within the analysis framework Goblint ¹. For that, these solvers have been extended to deal with side-effects (see [3] for a detailed discussion of this mechanism) to jointly deal with flow- and context-sensitive and flow-insensitive analyses. In order to perform a fair comparison of the new solvers with warrowing-based local solving as proposed in [2, 4], we provided a simplified version of TSMP. This simplified solver performs priority based iteration in the same way as TSMP but uses the warrowing operator instead of selecting operators according to extra flags. These three solvers were evaluated on the SPECint benchmark suite² consisting of not too small real-world C programs (1,600 to 34,000 LOC). Furthermore, the following C programs where analyzed: ent³, figlet⁴, maradns⁵, wget⁶, and some programs from the coreutils⁷ package. The analyzed program wget is the largest one with around 77,000 LOC.

The analyses which we performed are put on top of a basic analysis of pointers, strings and enums. For enum variables, sets of possibles values are maintained. The benchmark programs were analyzed with full context-sensitivity of local data while globals were treated flow-insensitively.

The experimental setting is a fully context-sensitive interval analysis of int variables. Therefore, program 482.sphinx had to be excluded from the benchmark suite since it uses procedures which recurse on int arguments. Interestingly, the warrowing solver behaves exactly the same as TSMP on all of our benchmark programs. We interpret this by the fact that for the given analysis the right-hand sides are effectively monotonic. Accordingly, Fig. 7 only reports the relative precision of TSTP compared to TSMP.

Fig. 6.

Efficiency of TSMP vs. TSTP. (Color figure online)

Figure 6 compares the solvers TSMP and TSTP in terms of space and time. For a reasonable metric for space we choose the total number of variables (i.e., occurring pairs of program points and contexts) and for time the total number of evaluations of right-hand sides of a corresponding variable. The table indicates that the solver TSMP requires only around half of the variables of the solver TSTP. Interestingly, the percentage of evaluations of right-hand sides in a run of TSMP is still around 60 to 70 % of the solver TSTP.

Fig. 7.

Precision of TSMP vs. TSTP.

In the second experiment, as depicted by Fig. 7, we compare the precision of the two solvers. For a reasonable metric we only compare the values of variables which occur in both solver runs. As a result, between 80 and 95 % of the variables receive the same value. It is remarkable that the mixed phase solver is not necessarily more precise. In many cases, an increase in precision is observed, yes — there are, however, also input programs where the two-phase solver excels.