Taming and Dissecting Recursions Through Interprocedural Weak Topological Ordering

The widening technique [24, 22] is introduced to ensure fixpoint termination and accelerate convergence by approximating infinite loop behavior. It involves choosing a subset of control points ${ℒ}^{\prime }\subseteq ℒ$ as widening points. For each widening point ${\mathrm{\ell }}_i\in {ℒ}^{\prime }$, we use equation ${\sigma }_{\underset{¯}{{\mathrm{\ell }}_i}}={\sigma }_{\underset{¯}{{\mathrm{\ell }}_i}}\nabla {\mathrm{\Phi }}_i({\sigma }_{\underset{¯}{{\mathrm{\ell }}_1}},{\sigma }_{\underset{¯}{{\mathrm{\ell }}_2}},\mathrm{\dots },{\sigma }_{\underset{¯}{{\mathrm{\ell }}_n}})$ instead of ${\sigma }_{\underset{¯}{{\mathrm{\ell }}_i}}={\mathrm{\Phi }}_i({\sigma }_{\underset{¯}{{\mathrm{\ell }}_1}},{\sigma }_{\underset{¯}{{\mathrm{\ell }}_2}},\mathrm{\dots },{\sigma }_{\underset{¯}{{\mathrm{\ell }}_n}})$ for fixpoint computation. In this equation, $\nabla$ is a widening operator, which is formally defined on a poset $(𝔸,⊑)$ that satisfies the following properties: (1) $\forall a,a^{\prime }\in 𝔸,a\bigsqcup a^{\prime }⊑a\nabla a^{\prime }$ and (2) for an increasing chain $a_1⊑a_2⊑\mathrm{\dots }⊑a_m$, the increasing chain $a_1^{\prime }⊑a_2^{\prime }⊑\mathrm{\dots }⊑a_m^{\prime }$ where $a_1^{\prime }=a_1$ and $a_m^{\prime }=a_{m-1}^{\prime }\nabla a_m$ eventually stabilizes. For example, the widening function on the integer interval domain $ℐ=\{[l,u]|l,u\in \mathbb{Z}\}$ is defined as: .

After the widening iteration converges to a fixpoint, a subsequent narrowing iteration, as described in [15, 24, 11, 39], aims to enhance the post solution through a downward fixpoint iteration. The narrowing operator $\mathrm{\Delta }$ satisfies the following properties: (1) $\forall a,a^{\prime }\in 𝔸,a^{\prime }⊑a⟹a\mathrm{\Delta }{a}^{\prime }⊑a$ and (2) for a decreasing chain $a_1⊒a_2⊒\mathrm{\dots }⊒a_m$, the decreasing chain $a_1^{\prime }⊒a_2^{\prime }⊒\mathrm{\dots }⊒a_m^{\prime }$ where $a_1^{\prime }=a_1$ and $a_m^{\prime }=a_{m-1}^{\prime }\mathrm{\Delta }{a}_m$ eventually stabilizes. For example, the narrowing operator on the integer interval domain $ℐ$ is defined as: $[l_0,u_0]\mathrm{\Delta }[l_1,u_1]=[\text{if }{l}_0=-\mathrm{\infty }\text{ then }{l}_1\text{ else }{l}_0,\text{if }{u}_0=+\mathrm{\infty }\text{ then }{u}_1\text{ else }{u}_0]$.

Given the explicit WTO of the control flow points, the chaotic iteration recursively computes a fixed point of the sub-components of each component in WTO every time the component reaches a fixed point [13]. WTO also provides an admissible set of widening points (the heads of WTO components) such that every loop in the program is cut by at least one widening point.

WTO is constructed based on Bourdoncle’s algorithm [32], which utilizes Tarjan’s algorithm [61] to identify all strongly connected components (SCCs) in a directed graph. The algorithm repeatedly applies Tarjan’s algorithm on the graph to break each found SCC into smaller SCCs until no further subdivision is possible. Each time an SCC is divided, smaller SCCs are ordered within the larger one in the WTO. The hierarchical structure of these components reflects the partial ordering of the WTO. Current abstract interpretation frameworks [15, 19, 18] compute WTO at the function level, applying the analysis intraprocedurally. However, the interprocedural fixpoint computation order remains implicit, as it is not guided by an interprocedural WTO structure.

Consider a path (sequence of nodes) starting from the root node in the recursion tree. We will show that the number of nodes along this path is bounded by analyzing the invocations of two specific functions: handlePartition (referred as $P$ nodes) and stabilizeCycle (reffered as $S$ nodes). These are the only types of nodes present on the path, as we have inlined all handleNode invokations for simplicity.

First, we examine the subsequence of handlePartition calls, denoted as:

We use $\mathrm{𝐹𝑃}(𝚏)$ to denote the unique function partition to which function $𝚏$ belongs. It follows that for all $i\in [1,m-1]$, $\mathrm{𝐹𝑃}({\mathrm{𝚌𝚊𝚕𝚕𝚎𝚎}}_i)=\mathrm{𝐹𝑃}({\mathrm{𝚌𝚊𝚕𝚕𝚎𝚛}}_{i+1})$. Consequently, for all , ${\mathrm{𝚌𝚊𝚕𝚕𝚎𝚛}}_j$ is reachable from ${\mathrm{𝚌𝚊𝚕𝚕𝚎𝚛}}_i$ on the call graph. We aim to prove the following sub-conclusions. Sub-conclusion 1: For all $i\le j$, $\mathrm{𝐹𝑃}({\mathrm{𝚌𝚊𝚕𝚕𝚎𝚛}}_i)\ne \mathrm{𝐹𝑃}({\mathrm{𝚌𝚊𝚕𝚕𝚎𝚎}}_j)$. Suppose this were not the case. Then, there would exists $i\le j$ such that $\mathrm{𝐹𝑃}({\mathrm{𝚌𝚊𝚕𝚕𝚎𝚛}}_i)=\mathrm{𝐹𝑃}({\mathrm{𝚌𝚊𝚕𝚕𝚎𝚎}}_j)$, implying that ${\mathrm{𝚌𝚊𝚕𝚕𝚎𝚛}}_i$ is reachable from ${\mathrm{𝚌𝚊𝚕𝚕𝚎𝚎}}_j$. Furthermore, it follows that ${\mathrm{𝚌𝚊𝚕𝚕𝚎𝚛}}_j$ would also be reachable from ${\mathrm{𝚌𝚊𝚕𝚕𝚎𝚎}}_j$, which contradicts the definition of ${𝚟}_j⟨{\mathrm{𝚌𝚊𝚕𝚕𝚎𝚛}}_j,{\mathrm{𝚌𝚊𝚕𝚕𝚎𝚎}}_j⟩$ as a non-recursive call site (according to Definition 10). Sub-conclusion 2: For all , $\mathrm{𝐹𝑃}({\mathrm{𝚌𝚊𝚕𝚕𝚎𝚛}}_i)\ne \mathrm{𝐹𝑃}({\mathrm{𝚌𝚊𝚕𝚕𝚎𝚛}}_j)$. This follows directly from Sub-conclusion 1 and $\mathrm{𝐹𝑃}({\mathrm{𝚌𝚊𝚕𝚕𝚎𝚎}}_i)=\mathrm{𝐹𝑃}({\mathrm{𝚌𝚊𝚕𝚕𝚎𝚛}}_{i+1})$. If $\mathrm{𝐹𝑃}({\mathrm{𝚌𝚊𝚕𝚕𝚎𝚛}}_i)=\mathrm{𝐹𝑃}({\mathrm{𝚌𝚊𝚕𝚕𝚎𝚛}}_j)$ for some , it would contradict Sub-conclusion 1. Sub-conclusion 3: $m\le |\mathrm{𝐹𝑃𝑎𝑟𝑠}|$, where $|\mathrm{𝐹𝑃𝑎𝑟𝑠}|$ denotes the number of function partitions in the program. If this were false, then there would exist at least one pair such that $\mathrm{𝐹𝑃}({\mathrm{𝚌𝚊𝚕𝚕𝚎𝚛}}_i)=\mathrm{𝐹𝑃}({\mathrm{𝚌𝚊𝚕𝚕𝚎𝚛}}_j)$, which would contradict Sub-conclusion 2.

Second, we examine a continuous subsequence of stabilizeCycle invocations,

For this sequence, the inequality is established, where ${\text{cycle}}_1.\text{depth}$ denotes the depth of the ${\mathrm{𝚌𝚢𝚌𝚕𝚎}}_1$. This holds because ${\mathrm{𝚌𝚢𝚌𝚕𝚎}}_{i+1}$ is a sub-IWTO component of ${\mathrm{𝚌𝚢𝚌𝚕𝚎}}_i$. Furthermore, the number of continuous $S$ subsequences is limited to length of the longest $P$ subsequence on the path, which, as previously concluded, is $|\text{FPars}|$. Consequently, the total number of $S$ nodes on the path is limited to $|\mathrm{𝐹𝑃𝑎𝑟𝑠}|\times \mathrm{𝑚𝑎𝑥𝐶𝑦𝑐𝑙𝑒𝐷𝑒𝑝𝑡ℎ}$, where maxCycleDepth is the maximum depth of all IWTO cycles.

Finally, since the path consists solely of $P$ and $S$ nodes, the length of the path is less than $|\mathrm{𝐹𝑃𝑎𝑟𝑠}|\times (\mathrm{𝑚𝑎𝑥𝑊𝑇𝑂𝑑𝑒𝑝𝑡ℎ}+1)$. $◀$

To establish this, we consider two cases. Case 1: For a $P({\mathrm{\ell }}^c⟨\mathrm{𝚌𝚊𝚕𝚕𝚎𝚛},\mathrm{𝚌𝚊𝚕𝚕𝚎𝚎}⟩)$ node, its degree is limited by the number of elements in $\mathrm{𝚌𝚊𝚕𝚕𝚎𝚎}$’s corresponding IWTO. Case 2: For a $S(\mathrm{𝚌𝚢𝚌𝚕𝚎})$ node, its child nodes represent the invoked subroutines within the double-nested loop outlined in Algorithm 2 from Lines 17 to 32. The outer loop is guaranteed to terminate within $h$ rounds [13], where $h$ represents the height of the lattice when applying the widening operation. The inner loop is bounded by the number of elements in $\mathrm{𝚌𝚢𝚌𝚕𝚎}$. Thus, the degree of an $S$ node is also finite.

In both cases, the degree of the nodes are limited, confirming that the recursion tree has finite degree. $◀$

By Lemmas 17 and 18, both the height and the breadth of the recursion tree are limited. Consequently, the recursion tree contains a finite number of nodes, which implies the termination of Algorithm 2. $◀$

We evaluate RecTopo using (1) a benchmark composed of 8312 programs from NIST [46], which includes comprehensive test cases of buffer overflow vulnerabilities, with 800 cases containing recursions, and (2) 10 popular open-source C/C++ projects across various application domains, with their statistics detailed in Table 2. These projects include paste [16] (file merger), md5sum [16] (file verifier), YAJL [4] (JSON parsing library), 8cc [7] (C compiler), libplist [8] (Property List file handler), MP4v2 [2] (MP4 file library), RIOT [3] (IoT operating system), darknet[1] (neural network framework), tmux [5] (terminal multiplexer) and Teeworlds [9] (online multiplayer game).

The experiments are conducted on an Ubuntu 22.04 server with an eight-core 2.60GHz Intel Xeon CPU and 128 GB memory. The interprocedural control and value flow graphs are built upon LLVM-IR (with LLVM version 14.0.0) using the SVF library (version 2.9). The LLVM-IR represents program functions as global variables, further modeled as address-taken variables. The call graph is built by considering the points-to information to resolve indirect calls. Program loops/recursions are captured by IWTO, which is constructed using the algorithm described in Section 4.1 (Algorithm 1). The abstract value representation is implemented using Z3 expressions [45]. We utilize the interleaved widening and narrowing strategy as described in [10] to precisely handle recursions and intraprocedural loops. We detect buffer overflows at each gep instruction by comparing the offset size and the memory size, both of which are calculated based on interval and points-to information from abstract interpretation. For the baselines IKOS, Clam and CSA, we directly use their open-source implementations and their default settings (e.g., interval analysis) for detecting buffer overflows.

For the complete NIST dataset, RecTopo consistently surpasses the baseline tools. It identifies, on average, 26.24% more buffer overflows than IKOS and Clam, while also achieving an average precision improvement of 44.19% over these tools. Its precision is also 7.59% higher than CSA. This performance underscores the robustness of RecTopo in interprocedural abstract interpretation. Moreover, the advantages of RecTopo are particularly notable in scenarios involving recursive functions, where it achieves a precision rate of 95.24% in detecting buffer overflows. In contrast, the average precision of IKOS, Clam and CSA in these test cases is only approximately 51.85%, 43.39% lower than RecTopo.

The improved recall can be attributed to RecTopo’s adoption of CSA’s robust handling of core program features, such as loop handling, and precise external API modeling [18]. Here, we focus on analyzing the precision improvements in handling recursion through two representative code scenarios shown in Figure 11. A key contributing factor is RecTopo’s construction of IWTO for recursive functions, which effectively guides the narrowing process by leveraging program path conditions. As demonstrated in Figure 11(a), the program accesses the buf buffer at ${\mathrm{\ell }}_{14}$ with an offset idx, which is obtained from the return value of the mc91(100) function call at ${\mathrm{\ell }}_{13}$. RecTopo precisely determines mc91’s return value in the range $[91,101]$. Consequently, it concludes that the buffer access at ${\mathrm{\ell }}_{14}$ is safe. In contrast, all our baseline analyses report an overflow alarm here, incorrectly indicating that the value of mc91(100) could be anywhere within $[-\mathrm{\infty },\mathrm{\infty }]$.

Another reason is that the IWTO construction approach effectively eliminates spurious recursions (widening points) arising from multiple call sites of the same function, such as the double call to adder in Figure 11(b). RecTopo accurately differentiates between these call sites, preventing misclassification of program points, ${\mathrm{\ell }}_{12},{\mathrm{\ell }}_2-{\mathrm{\ell }}_4,{\mathrm{\ell }}_{10},{\mathrm{\ell }}_{11}$, as part of a spurious recursion. This precision prevents RecTopo from widening the value of sum at the adder entry point (${\mathrm{\ell }}_2$) to $[0,\mathrm{\infty }]$. Consequently, RecTopo derives the precise value of sum at ${\mathrm{\ell }}_{14}$ as $[3,3]$, thereby eliminating a false overflow alarm.

We further analyze RecTopo’s false positives and identify two primary causes, as demonstrated in the examples in Figure 12. First, RecTopo compromises precision for efficiency in scenarios involving complex path conditions. A case in point is its failure to accurately interpret the path condition at ${\mathrm{\ell }}_2$ in Figure 12(a), resulting in an imprecise narrowing of the range of n after widening. This imprecision triggers the overflow alarm at ${\mathrm{\ell }}_{10}$. This issue primarily stems from the limitations of the abstract interpretation solver, which, although not a key contribution of RecTopo, affects its precision. Enhancing the solver’s capability for precise path condition interpretation could rectify this. Another source of precision loss is RecTopo’s inability to track relationships between variables. This limitation is illustrated in Figure 12(b), where the parameters m and n have a constraint that their sum at each call site remains constant. However, RecTopo’s interval domain representation only allows for the independent storage of their abstract states, thus failing to capture their interrelation. As a result, when the parameter m is widened to $[0,\mathrm{\infty }]$, RecTopo over-approximates idx’s range as $[0,\mathrm{\infty }]$. Adopting a relational domain to articulate the constraints between program variables could overcome this limitation.

RecTopo demonstrates superior performance across all metrics, successfully identifying 75 real bugs with a precision rate of 65.79%, representing 79.78% of all identified vulnerabilities. In contrast, IKOS and Clam achieve an average recall rate of only 30.32% among discovered bugs. The precision rates of the baseline tools average 19.28%, less than one-third of RecTopo’s precision. Notably, RecTopo achieves these significant improvements while maintaining computational efficiency comparable to CSA. The markedly lower false positive rate of RecTopo can be attributed to its sophisticated abstract interpretation framework, guided by the IWTO approach. This methodology enables precise derivation of abstract states within recursive contexts through carefully orchestrated interleaved widening and narrowing operations on recursions.

Figure 13 illustrates the patch [6] and call graph for a real-world buffer overflow identified by RecTopo in libplist [8], a portable C library to handle Property List files [53]. RecTopo and CSA initially find this bug, which is missed by Clam and IKOS. However, after the bug is patched, CSA erroneously continue to report it as a buffer overflow – resulting in false positives. By comparison, RecTopo accurately eliminates the false alarm after the bug is fixed.

The bug resides in the parse_array_node function, within a recursive calling chain as depicted in Figure 13. It is triggered at line ${\mathrm{\ell }}_{15}$, where the function UINT_TO_HOST accesses the address pointed by index1_ptr and reads an extra bplist$\to$ref_size bytes. This bug arises because bplist$\to$ref_size, the buffer access variable in the recursion, is not properly bounded, potentially allowing reads past the allocated buffer of index1_ptr, leading to a buffer overflow. When the issue is addressed by introducing a boundary check before ${\mathrm{\ell }}_{15}$, RecTopo stops reporting the problem, while CSA still signal a bug. This discrepancy is attributed to our utilization of widening and narrowing techniques within the recursive function partition, which precisely leverage path conditions to refine the abstract value of bplist$\to$ref_size, thereby providing more accurate results and effectively eliminating the false positive.

We present detailed statistics of IWTO across the ten real-world projects. Figure 14(a) illustrates the proportion of nodes residing in IWTO cycles for each program. The data reveals a substantial presence of nodes within IWTO cycles, ranging from 8.4% to 55.9%, with an average of 33.5%. Figure 14(b) depicts the aggregate depth of nodes (as defined in §2.3) across all IWTO cycles in each program. The data exhibits a near-linear growth pattern relative to program size. Given that the time complexity for cycle stabilization is linear with respect to the sum of node depths [13], this suggests that the overall time complexity for stabilizing IWTO cycles scales approximately linearly with program size. Figure 14(c) presents the number of nodes within IWTO cycles per program, while Figure 14(d) shows the maximum node depth in each program’s IWTO. The data demonstrates that while the number of nodes in cycles increases linearly with program scale, the maximum depth remains relatively stable. This relationship explains the linear growth pattern observed in the aggregate node depth measurements.

RecTopo exhibits 60.41% higher precision than RecTopo-NR. This superior precision stems from RecTopo’s ability to more precisely calculate the values of variables within recursive functions. In contrast, RecTopo-NR simplifies the process by assigning a generic top value to these variables.

This overly conservative approaches of RecTopo-NR results in broader intervals that frequently trigger false overflow alarms during buffer access. In terms of performance efficiency, RecTopo-NR leads in execution speed as it bypasses the body of recursive functions entirely.

However, the slight time advantage of RecTopo-NR does not compensate for the substantial precision gains achieved by RecTopo, reinforcing its effectiveness in balancing precision with performance.

RecTopo-GL implements a global whole-program IWTO that establishes connections between all call sites and their corresponding callee functions. The abstract interpretation within RecTopo-GL is managed by this singular IWTO, with each cycle processed with precision comparable to that of RecTopo. Despite this, RecTopo-GL demonstrates a reduction in precision by 64.27%, and it also operates 1.15$\times$ longer compared to RecTopo.

The reduced precision in RecTopo-GL can be primarily attributed to its redundant widening operations. As depicted in Figure 15(a), RecTopo achieves a significant decrease in the number of widening points, with an average reduction of 58.99% and a peak reduction of up to 81.56%. This substantial decrease in unnecessary widening throughout various program procedures directly contributes to the enhanced precision of RecTopo. Regarding scalability, the comparison of the time required to construct IWTO in RecTopo and RecTopo-GL highlights significant differences. Figure 15(b) clearly shows that constructing a whole-program IWTO in RecTopo-GL demands considerably more time – nearly 36 times longer – than the IWTO approach used in RecTopo. This comparison underscores the efficiency and practicality of the partitioned approach in handling scalability.