Event-Flow Graphs for Efficient
Path-Sensitive Analyses

I. Introduction

Accurate path-sensitive analyses require that: (a) execution effects along each path in a control-flow graph (CFG) are analyzed in isolation, i.e., without merging effects from different paths, and (b) effects along infeasible paths are excluded. The specific challenges for efficient and accurate path-sensitive analyses are thus: (a) exponential growth of the number of paths with the number of non-nested branch nodes in the CFG [1], [2], and (b) checking path feasibility requires checking satisfiability of branch conditions along the path, a process that also can incur exponential computation [3], [4], [5], [6], [7], [8].

Intuitively, our novel approach to efficient path-sensitive analysis works by considering equivalence classes of paths as follows: Two paths are considered equivalent if they have the same event trace. Each event trace is a sequence of events on a CFG path representing sufficient information for checking whether a given software property holds on that path. Since all paths in an equivalence class have the same event trace, it is sufficient to check just one path per group/class. In theory, there is an opportunity to circumvent exponential computational growth if the number of equivalence classes remains small even as the number of CFG paths grows exponentially. Although it may seem counterintuitive to just compute the event trace for each class without explicitly examining each CFG path, in this paper, we present an innovative linear-time algorithm that computes all event traces without examining each CFG path, thereby circumventing the exponential computational load.

We define a derivative of CFG, called the Event-Flow Graph (EFG), and prove that there is a one-to-one and onto mapping, where each path in the EFG corresponds to a group/class of equivalent paths in the CFG. The EFG retains the events and relevant branch nodes from the CFG, and the EFG is a minimal graph for computing all the event traces, i.e., each path in the EFG produces a unique event trace. We provide a linear-time algorithm to compute the EFG. Another benefit of introducing EFG is that it can minimize computation for checking path feasibility. In our empirical evaluation of the Linux kernel (v3.12) (Section V-C), we found that only the relevant branch nodes for forming equivalence classes were also sufficient for checking feasibility.

To assess the benefits of using EFGs in a practical scenario, we conducted an empirical evaluation of the Linux kernel (v3.12). The EFGs are defined with respect to events relevant for verifying the spin safe-synchronization property that requires that a lock of a spin object is followed by an unlock of the same object on all feasible execution paths. Our results show that the number of paths and the number of branch nodes are drastically reduced in going from a CFG to its EFG. The results from our controlled experiment show that EFGs are human comprehensible and compact compared to their corresponding CFGs and that is apparent in the reduction of the manual verification time and the effort in checking feasibility. The controlled experiment resulted on reporting a new bug [9] that has been accepted by the Linux community. All the CFGs and their corresponding EFGs from our empirical evaluation are available in [10]. In Section VI, we present an example using the Linux kernel to illustrate the use of EFG in an intra- and inter-procedural path-sensitive analysis.

II. A Motivating Example

Figure 1 shows the CFG of function hwrng_attr_current_store from the Linux kernel (v3.12). The nodes ⊤ and ⊥ respectively denote the unique entry and exit nodes added to the CFG. Also, T and F respectively denote the true and false branches from a branch node. This example concerns event traces that are needed to check the safe-synchronization property that requires that a lock of a synchronization object must be followed by an unlock of the same locked object over all feasible CFG paths. The example contains two event nodes highlighted in gray: mutex_lock_interruptible (&rng_mutex) (e₁) and mutex_unlock (&rng_mutex) (e₂).

In the CFG, the branch nodes c₂, c₃, c₄, and c₅ are considered irrelevant branch nodes; a branch node is irrelevant if all paths branching from it lead to the same event or terminal node. The branch node c₁ is a relevant branch node. For a given path P in a CFG, the sub-trace of the execution trace of P, consisting of only the relevant branch and event nodes, is called the event trace of P. That means, the paths branching from the false branch of c₁ have the same event trace (⊤e₁c₁e₂⊥). Paths with identical event traces are considered equivalent and grouped into one equivalence class. The event trace of the path branching from the true branch of c₁ is ⊤e₁c₁⊥, and it is by itself in another equivalence class.

Each equivalence class is represented by a unique event trace of the paths in that class. Once those equivalence classes are computed, it is sufficient to analyze only the event traces for all equivalence classes to check the safe-synchronization property. For example, the CFG in Figure 1 results in two event traces: 1) the trace ⊤e₁c₁e₂⊥, and 2) the trace ⊤e₁c₁⊥. It is then sufficient to analyze only these two traces to cover all the paths in the CFG.

To summarize the important points:

1. All CFG paths with the same event trace are grouped into one equivalence class. In this example, all the CFG paths are grouped into two equivalence classes.
2. Analyzing event traces is equivalent to analyzing all CFG paths.
3. A branch node is irrelevant if all the paths branching from it either lead to the same event or terminal node (a broader notion of irrelevant branch nodes is defined later). Four out of five branch nodes are irrelevant in this example.

III. Path-Sensitive Analysis with Event Traces

Definition 1: A Control Flow Graph (CFG) of a program is defined as G = (V, E, ⊤, ⊥), where G is a directed graph with a set of nodes V representing the program statements and a set of edges E representing the control-flow between statements. ⊤ and ⊥ denote the respective unique entry and exit nodes of the graph.

A. Execution Traces

After labeling each node of the CFG with a unique identifier, we define the execution trace of a CFG path as the regular expression of the node labels along that path. Let us illustrate this definition using the CFG first shown in Figure 1 and redrawn in Figure 2(a). The highlighted nodes are the event nodes. Code statements are replaced with nodes labeled x₁ through x₁₅. Figure 2(b) shows a CFG path; its execution trace is: ⊤x₁x₂e₁c₁x₃x₄c₂c₃c₄x₉c₅x₁₀x₁₁x₁₂x₁₃e₂x₁₅⊥. Figure 2(c) shows a CFG path with a loop; its execution trace is: ⊤x₁x₂e₁c₁x₃x₄(c₂c₃x₆)⁺c₂c₃c₄x₇x₈e₂x₁₅⊥, where (n_i..n_k)⁺ represents the loop between the nodes n_i to n_k that is executed one or more times.

B. Event Traces

Event traces are defined with respect to ℰ; the set of events of interest associated with the analyzed property. We will use the verification of the safe-synchronization property as a running example in illustrating all definitions. The safe-synchronization property requires that for every object p: the locking event e₁(p) is followed by the unlocking event e₂(p) on all feasible execution paths. Thus, the set ℰ_p of events, for verifying that property for object p, consists of: the locking and unlocking events defined on p, and the data-flow events in which the locked object p is either aliased or escapes to another function as a parameter, a return value, or a global variable. Such data-flow events can be determined using a taint analysis technique [11]. Once the events of interest are determined, one can write a path-sensitive verification algorithm that traverses the CFGs and checks that, for each synchronization object (p), a lock event e₁(p) is always succeeded by an unlock event e₂(p) on all execution paths. In case of a violating path which has a lock event not followed by unlock event, path feasibility needs to be conducted.

Definition 2: A property P is a 2-event property if for every object p, an event e₁(p) must be succeeded by another event e₂(p) on all feasible execution paths.

Note that event-based analyses can be performed to verify properties that can be modeled as 2-event properties like safe-synchronization and memory leak. A number of vulnerabilities listed by the MITRE Corporation [12] can be addressed using event-based analyses.

Definition 3: A CFG node is an event node if it corresponds to an event of the set of events (ℰ) associated with a given property to be analyzed.

Definition 4: Successors of a node u in a directed graph G, denoted by suc(u), consist of the set of nodes v ≠ u such that ∃ an edge (u, v).

Definition 5: Successors of a subgraph S in a directed graph G, denoted by suc(S), consist of the set of nodes v ∉ S such that v = suc(u) for u ∈ S.

Definition 6: For a branch node c, a branch edge is an out-coming edge of c.

Definition 7: A branch node c is an irrelevant branch node if the following conditions are satisfied:

• c is a non-event node.
• There exists a subgraph S containing c and all branch edges of c.
• S has no event nodes.
• S has a unique successor, i.e., |suc(S)| = 1.

Figure 3 shows an example of irrelevant branch node c.

Definition 8: An event trace of a path in CFG is a sub-expression of the execution trace consisting only of the relevant branch nodes, event nodes and the ⊤ and ⊥ nodes.

For example, the event trace for paths P₁ and P₂ depicted in Figure 2(b, c) would be: ⊤e₁c₁e₂⊥.

Definition 9: The Event-Flow Graph (EFG) G_EFG of a CFG G with respect to ℰ is the node-induced subgraph of G consisting of the event nodes, the relevant branch nodes, and the entry (⊤) and exit (⊥) nodes.

Relevancy of Branch Nodes. The notion of relevancy is defined with respect to equivalence classes of CFG paths. There could be correlation between relevant branch nodes and the remaining branch nodes or non-event nodes. In that case, the path feasibility check would need to take into account other nodes correlated to relevant branch nodes. In our empirical evaluation of the Linux kernel (Section V-C), we did not find such correlation. Thus, only the relevant branch nodes for forming equivalence classes were also sufficient for checking feasibility.

C. Equivalence Classes of CFG Paths

In this section, we will show that verifying a property P on all CFG paths is equivalent to verifying P for all event traces. Initially, let us define an equivalence relation on the CFG paths:

Definition 10: Given a CFG G and an event set ℰ which is a subset of nodes in G, we define a relation ℛ_ℰ on paths in G as follows: two CFG paths are related iff they have the same event trace.

Note that ℛ_ℰ is an equivalence relation because it is reflexive, symmetric, and transitive.

Theorem 1:^* Given a CFG G, a set ℰ of events, and the equivalence relation ℛ_ℰ, there is a one-to-one and onto mapping between the equivalence classes of ℛ_ℰ and the paths of the EFG G_EFG where each EFG path produces the event trace corresponding to an equivalence class.

^* Theorems’ & corollaries’ proofs can be found in appendix A.

Theorem 2: Given a 2-event property P, its verification on all CFG paths can be done using the event traces.

Corollary 1: Given a 2-event property P, its verification on all paths of a CFG G can be done with the corresponding EFG G_EFG.

The proof directly follows from the above two theorems.

Remark 1: Given a CFG and the set ℰ, the corresponding EFG is unique. This is because the nodes of EFG are uniquely defined as they are exactly the event nodes and relevant branch nodes. The edges in the EFG are also uniquely defined because they are induced by the edges in the CFG.

D. EFGs for Optimal Path-Sensitive Analyses

Given a 2-event property, its path-sensitive analysis can be done using EFGs instead of CFGs as follows:

For every object p:

1. Determine all the events of interest (i.e., the set ℰ_p), including the events e₁ and e₂ defined on p and the data-flow events for p.
2. If the object p is passed to other functions either as a parameter or as a return value, then consider all such functions to be relevant functions.
3. Construct EFGs with respect to ℰ_p for relevant functions.
4. Perform the path-sensitive analysis using the EFGs instead of the CFGs.
5. In case of a path that has e₁(p) not followed by e₂(p), path feasibility check is needed. Using EFGs, the path feasibility is conducted by checking the satisfiability of the conditions (relevant branch nodes), where the correlation between conditions can be computed via constant propagation [13] or global value numbering [14] as in [15].

EFGs can be used to perform inter-procedural path-sensitive analysis. In Section VI, we illustrate a case study on inter-procedural verification using EFGs. To conclude, EFG is the minimal graph that produces all event traces for an accurate and efficient path sensitive analysis given a 2-event property P and its associated set of events ℰ. For the EFG to be useful in practice, the next section presents an efficient algorithm to construct the EFG from a given CFG.

IV. Computing Event Traces of a CFG

In this section, we first present an algorithm to compact a given CFG into a T-irreducible graph. This compaction algorithm will be used later in computing the EFG. Then, we present an algorithm that efficiently computes the equivalences classes of CFG paths in linear-time based on Tarjan’s algorithm to compute strongly-connected components of a directed graph [16].

A. Algorithm I: T-irreducible Graph

Definition 11: A Colored Directed Graph (CDG) is defined as G = (V, E, C, ⊤, ⊥), where (V, E) is a finite directed graph with a set of nodes V and a set of edges E. ⊤ and ⊥ respectively represent the unique entry and exit nodes of the graph. C ⊆ V is the set of colored nodes.

For the purpose of this algorithm, a CFG is modeled as a CDG by treating the event nodes as colored nodes.

T₁: Elimination of Non-branching and Non-colored Nodes

Let G = (V, E, C, ⊤, ⊥) be a CDG and n be a non-colored node (n ∉ C) with a single successor m. The T₁ transformation is the consumption of node n by m. Induced edges are introduced so that the predecessors of node n become predecessors of node m. (Figure 4(a))

The T₁ transformation eliminates every node from CFG that is neither a branch node nor an event node. These nodes are removed because they are irrelevant to the analysis because they are not included in the resultant event traces.

T₂: Elimination of Self-Loop Edges

Let G = (V, E, C, ⊤, ⊥) be a CDG and let n be a non-colored node (n ∉ C) that has a self-loop edge (n, n). The T₂ transformation removes that edge. (Figure 4(b))

The intuition behind T₂ transformation is: in a loop block that contains no event nodes, execution of the loop is immaterial. Therefore, T₂ removes the self-loop edges.

T₃: Elimination of Irrelevant Branch Nodes

Let G = (V, E, C, ⊤, ⊥) be a CDG and let n be a non-colored node (n ∉ C) that has two or more edges, all pointing to the same successor m of n. Then the T₃ transformation is the consumption of node n by m and the predecessors of node n become predecessors of node m. (Figure 4(c))

The intuition behind the T₃ transformation is as follows: Imagine the case where a branch node n has only non-colored nodes on its branches, and all those branches ultimately merge at node m. If the non-colored nodes on those branches are eliminated by the T₁ transformation, all branches will point to node m. At this point, the branching at n is irrelevant so the branch node n can be eliminated.

Definition 12: Let T = {T₁, T₂, T₃} be the set of basic transformations described above. A CDG G is T-irreducible if it cannot be further reduced by applying transformations in T.

Algorithm I uses the transformations T₁, T₂, and T₃ to construct a T-irreducible graph as follows:

• Start with a CFG G_CFG = (V_GCFG, E_GCFG, ⊤, ⊥) and transform it into a CDG G_CDG = (V_GCFG, E_GCFG, C, ⊤, ⊥). The set C of colored nodes is the set of event nodes defined by the set ℰ associated with the analyzed property. i.e., CFG is modeled as a CDG by treating the event nodes as colored nodes.
• Transform G_CDG into a T-irreducible graph by applying the transformations in T.

B. Algorithm II: Transform CFG to EFG

We will present a linear-time algorithm that produces the minimal number of equivalence classes by transforming a CFG G into G_EFG, the corresponding event-flow graph (EFG). Intuitively, one might think that the problem of computing all event traces would require individual examination of each path in a CFG, but Algorithm II shows this not to be true. As observed in our empirical evaluation of the Linux kernel, while the number of CFG paths may grow exponentially, the number of event traces does not. In such scenarios, Algorithm II is very efficient because it requires a computational load proportional to the number of event traces rather than to the number of CFG paths.

We claim that the graph produced by Algorithm II is indeed the event-flow graph (EFG) that we have defined earlier and shown to be the minimal graph that produces all the event traces needed for an accurate and efficient path-sensitive analysis. First, we will present CFG to EFG transformation algorithm and later provide a proof that the produced graph is actually the EFG. We will use the following additional definition to further describe Algorithm II.

Definition 13: G_CG is the condensation graph of a directed graph G if each strongly-connected component (SCC) of G contracts to a single node in G_CG and the edges of G_CG are induced by edges in G. Thus, G_CG is a directed acyclic graph (DAG).

Given a CFG G_CFG and the set ℰ of events as computed in step (1) in Section III-D. Now, let us fully describe algorithm II that transforms the CFG G_CFG to its EFG G_EFG:

(1) T-Irreducible Graph Construction: Start with a CFG G_CFG and transform it into a T-irreducible graph G_T-irr by applying Algorithm I.

(2) Non-Colored Condensation Graph Construction: Compute the subgraph G_I of G_T-irr induced by its non-colored nodes. Then, construct the non-colored condensation graph G_NCCG of G_I.

(3) Colored Condensation Graph: Construct a new CDG G_CCG by adding the colored nodes in G_T-irr to G_NCCG. If an edge exists between an SCC and a colored node n in G_T-irr then introduce an edge in G_CCG between the contracted node for that SCC and the colored node n.

(4) Condensed EFG Construction: Transform G_CCG into a T-irreducible graph G_cEFG by applying Algorithm I.

(5) EFG Construction: Transform G_cEFG into G_EFG by expanding each remaining contracted SCC in G_cEFG back to the original SCC as in G_T-irr.

Remark 2: The resultant graph G_cEFG after step (4) is the condensed EFG. In addition, we claim that the resultant graph G_EFG after step (5) is the EFG.

Figures 5(a-f) illustrate the successive graphs constructed by Algorithm II, starting with the CFG (graph a) and ending with the EFG (graph f).

C. Algorithm II Complexity

The algorithmic complexity of constructing the T-irreducible graph (Steps 1 and 4) is O(|V| + |E|) where |V| and |E| are the respective numbers of nodes and edges in the CFG. For detecting the SCCs in step (2), we use an algorithm by Tarjan [16] to compute strongly-connected components of a directed graph. The run-time of this algorithm is also O(|V| + |E|), yielding a linear run-time complexity of O(|V| + |E|) for Algorithm II.

D. Algorithm I versus Algorithm II

The EFG constructed by Algorithm II achieves an important compaction of the CFG that is not possible in Algorithm I. Recall that the graph G_T-irr produced by Algorithm I may contain irrelevant branch nodes. For example, consider two branch nodes A and B with suc(A) = {B, E} and suc(B) = {A, E}, where E is an event node. The branch nodes A and B are irrelevant and should be eliminated. The subgraph consisting of the two branch nodes A and B has a unique successor E and thus, they will be eliminated in the condensed EFG G_cEFG. Note that in the above scenario even though there can be more that two branch nodes that are successors of each other, as long as they have the same event node as the successor, all such branch nodes are irrelevant and will be eliminated by Algorithm II. Thus, by including steps (2-5), Algorithm II can achieve compaction beyond that of Algorithm I.

Note that there can be a strongly-connected component (SCC) of branch nodes with two or more successors and, if so, those branch nodes must be retained. An example of such a scenario is shown in Figure 6 depicting the EFG of function cancel_bulk_urbs from the Linux kernel (v3.12). In the EFG, the SCC consisting of the branch nodes c₁ and c₂ is retained as it has two successors: the terminal node ⊥ and the event node e₁.

E. EFG: Correctness Proof

In Algorithm II, it is not enough to claim that the resultant graph G_EFG after step (5) is the EFG. We will now prove that Algorithm II produces the EFG correctly. This amounts to proving that Algorithm II removes all irrelevant branch nodes.

Theorem 3: Let G be a colored T-irreducible and acyclic graph. Then for any subgraph S containing non-colored nodes of G: |suc(S)| ≥ 2.

Corollary 2: Let G be a CFG and G_cEFG be the condensed EFG. Then, for any subgraph S containing non-colored nodes of G_cEFG, |suc(S)| ≥ 2.

Corollary 3: The graph produced by Algorithm II does not contain any irrelevant branch nodes.

V. An Empirical Evaluation

We present an empirical evaluation to show the applicability and advantages of using event-flow graphs (EFG) rather than control-flow graphs (CFG) to perform path-sensitive analyses. Specifically, we evaluate the following:

• The reduction in nodes and edges in going from CFGs to EFGs.
• The reduction in branch nodes, since only the relevant branch nodes are retained in the EFGs.
• The reduction in the effort to check feasibility of paths.

A. Experimental Setup

We use the Linux kernel (v3.12) for our empirical evaluation. We consider the spin safe-synchronization property for defining the events of interest (ℰ) for our analysis. We have used EnSoft’s C-Atlas [17] platform to compute ℰ, the CFGs, and EFGs. The C-Atlas first compiles the Linux kernel (v3.12) and pre-computes a database of relationships (i.e., call, control-flow, data-flow, etc.) between various program artifacts. This process took 34 minutes. Then, we query the C-Atlas database to find all the spin synchronization objects 𝒫. This query identifies all the variables passed as parameters to the spin locking (spin_lock, spin_trylock) and unlocking (spin_unlock) functions.

We followed the steps (1-3) in Section III-D and wrote a Java program -based on a taint analysis technique [11]- using the C-Atlas APIs to determine the set ℰ_p for every object p ∈ 𝒫, by identifying the events e₁ and e₂ that are defined on p in addition to the relevant data-flow events for p, including those in which p are passed as parameters or return values to other functions. Based on these events, we determine all the Linux kernel functions, referred to as relevant functions, needing to be analyzed for every object p. Afterward, we wrote a Java program using the C-Atlas APIs to construct the EFG for each relevant function from its corresponding CFG based on the set ℰ_p.

In the Linux kernel (v3.12), there are 531 spin objects and in total 3,894 relevant functions for the analysis of all objects. The conversion from CFGs to EFGs using Algorithm II took 9 seconds for all relevant functions. All experiments were carried out on a Windows 8, Intel Core i7 2.40Ghz, 8GB RAM laptop computer.

Table I summarizes for the Linux kernel (v3.12) the number of artifacts: LOC - lines of code, Srce Files - source files, Functions - functions, Rlvnt. Func. - relevant functions, Spin Objs. - spin lock objects, and Events - events of interest to the spin safe-synchronization property.

B. Experiment I: Reductions from CFG to EFG

We present the reduction in nodes and edges in going from CFGs to EFGs. Recall that the EFG consists of the event and relevant branch nodes and that the reduction is due to the removal of non-event nodes and irrelevant branch nodes.

Table II shows the distribution of nodes, edges, and branch nodes for both the CFGs and EFGs for all the relevant functions (F_Relevant). In assessing graphs with a large number of nodes, we find only 15 EFGs compared to 1,058 CFGs that have (> 30) nodes, i.e., a reduction of ∼99%. In assessing graphs with a large number of edges, we find only 76 EFGs compared to 1,309 CFGs that have (> 30) edges, i.e., a reduction of ∼94%. In assessing graphs with a large number of branch nodes, we find only 107 EFGs compared to 597 CFGs that have (> 10) branch nodes, i.e., a reduction of ∼90%. In assessing straightforward cases for checking feasibility of paths, we find 559 CFGs compared to 1,458 EFGs with no branch nodes, i.e., a 161% increase.

The reductions from CFGs to EFGs are particularly important for complex CFGs, and especially for CFGs with a large number of branch nodes. Table III lists the reductions for the ten functions in F_Relevant with the largest number branch nodes^†. The P(%) columns denote the reduction percentages for nodes, edges, and branch nodes. For example, for function xs_udp_data_ready the reductions from CFG to EFG are: from 1,101 to 8 nodes, from 1,513 to 11 edges, and from 317 to 4 branch nodes.

^† A complete comparison of all relevant functions for the spin safe-synchronization property in the Linux kernel (v3.12) is available at [10].

Spin objects: 1: rpc_xprt.transport_lock, 2: sock.sk_lock.slock.

C. Experiment II: Manual Verification

For this experiment, we randomly selected 400 locking events from the Linux kernel (v3.12) and asked two analysts^‡ to manually verify the spin safe-synchronization property for those events. The analysts were asked to report: 1) the analysis time for each event, 2) the conditions (branch nodes) that were used to decide on a path feasibility in case of a path that has a locking event e₁(p) is not followed by an unlocking event e₂(p) (i.e., violating path), and 3) “buggy” or “safe” verdict for each locking event where buggy means that the violating path is feasible.

^‡ Two PhD students with ∼ 9 years of experience in programming.

We conducted the experiment in two rounds, where in each round we asked the analysts to verify 200 events. In the first round R1: the first analyst A1 to use only CFGs where the other analyst A2 to use EFGs. In the second round R2: A1 to use EFGs and A2 to use CFGs. The analysts were given the following information:

• The function f_i and the line number for the locking event e_j(p) that needs to be verified.
• The set of all relevant functions for the analysis of the locking event e_j(p).
• The nodes that correspond to the events in ℰ_p are highlighted in the corresponding CFGs and EFGs. All the branch nodes are diamond-shaped.

In case of a path feasibility check, the analyst calculates the Boolean combination, i.e., AND(∧), OR(∨), NOT(¬), of conditions which must be true for the path to be executed. Then, he checks the satisfiability of that combination. For the sake of simplicity, the analyst can infer the correlation between conditions only from the information within the graphs assigned to him.

Table IV shows the analysis times for each analyst in each round along with the number of safe and buggy events. Also, it shows the number of times path feasibility (Feas.) is conducted. Both analysts came up with identical verdicts for safe and buggy and reported exactly the same set of conditions/branch nodes used for checking feasibility. A1 in R2 and A2 in R1 reported that EFGs were enough to perform the verification and the relevant branch nodes were sufficient for checking feasibility. The number of feasibility checks varies when using CFGs and EFGs. This occurs if multiple paths in the CFG, that are checked for feasibility, happen to be equivalent, hence they are represented by one path (event trace) in the corresponding EFG.

Moreover, both analysts reported a new bug [9] that has been accepted by the Linux community and it turned out to be spanning multiple kernel versions.

VI. An EFG Application Study

This study presents a real-world example from the Linux kernel (v3.12) to illustrate the applicability and advantages of using EFGs in an inter-procedural path-sensitive verification. It illustrates the verification of the safe-synchronization property for the read-semaphore synchronization object (cpufreq_rwsem), by verifying that every locking event (down_read, down_read_trylock) is always succeeded by an unlocking event (up_read) on every feasible execution path. The study involves three functions: cpufreq_bp_resume (f₁), cpufreq_cpu_get (f₂), and cpufreq_cpu_put (f₃). Figure 7 captures the relevant functions for the analysis, and it shows that f₁ first calls f₂ and then calls f₃. The first advantage of using EFGs to perform the analysis is that EFGs are simpler and more compact than their CFG counterparts. The CFG statistics are given in Table V and the EFGs are shown in Figure 7.

In f₂, there exist four paths corresponding to the four equivalence classes (i.e., unique event traces) of paths in the CFG. Three of those equivalence classes contain e₁ that needs to be verified. In the Linux kernel, function (down_read_trylock) returns 1 if the lock occurs, otherwise 0. In this example the e₁ event evaluates to true if the lock does not occur; otherwise, it evaluates to false. That means that, of the three equivalence classes containing e₁, the equivalence class that contains the true branch is infeasible when the lock occurs. Hence, the paths that contain this branch do not require verification. Now, for the other two equivalence classes that contain the false branch of e₁, those paths must have an unlocking event (up_read). In f₂, the paths that contain the true branch of the branch node c₃ contains unlocking event e₂. That means that event e₁ is verified on those paths. However, on the path that contains the false branch of c₃ (path A), there is no unlocking event. Looking at the EFG of f₂ alone, one can conclude that this path A contributes to a violation with respect to the tested property. However, the path A locking event e₁ is verified with unlocking event e₃ in function f₃ via function f₁. Here is how this is accomplished:

In f₁, the path that corresponds to the false branch of c₃ (path A) is inflated into two paths: path B that goes via the true branch of c₁, and path C that goes via the false branch of c₁. One can conclude that path B contributes to a bug since no unlocking event occurs and the function returns. However, path B turns out to be infeasible if path A in f₂ is taken. This is true because: (1) path A is the path taken via the false branch of c₃; that means c₃ evaluates to false, (2) c₁ = c₃ and the variable policy is returned from f₂ to f₁. Hence, c₁ must evaluate to false if path A is taken. This means that path B is infeasible when path A is taken. In other words, path B has no verification need. That leaves path C that is feasible and should have an unlocking event.

In f₁, path C calls f₃. In f₃, path C is inflated into paths D and E that traverses the true and false branches of c₄, respectively. Using reasoning like that for path B, one can conclude that path D contributes to a bug. However, path D is infeasible when path A is taken. This is true because path A is the path taken via the false branch of c₃; that means that it also goes via the false branch of c₂. Hence, c₂ evaluates to false in other words, (cpufreq_disabled()) must return false, so c₄ evaluates to false if path A is taken. This means that path D is infeasible when path A is taken. In other words, path D needs no verification. That leaves us with one path, E, that is feasible and has an unlocking event. We can finally conclude that there is no violation for the safe-synchronization property and that e₁ in function f₂ is verified by e₂ in f₂ (intra-procedural) and by e₃ in f₃ via f₁ (inter-procedural).

This case study shows that: 1) EFGs can be used to perform both intra- and inter-procedural path-sensitive analyses efficiently and accurately. Also, 2) the branch nodes contained in the EFG are the relevant branch nodes for the events and, in determining the feasibility of paths. In this case study, the number of branch nodes are reduced to 5 compared to 14 branch nodes in the corresponding CFGs.

VII. Related Work

Event-flow graphs are inspired by the work done by Neginhal et al. [18]. They developed the C-Vision tool that introduced the notion of event view. C-Vision reductions are based on user-input to determine irrelevant nodes/edges to be removed. There is no algorithmic notion to compute the compact CFG. However, this paper provides a linear-time algorithm to compute the event-flow graph with regard to the given events of interest to the property being analyzed. EFGs enable efficient path-sensitive analyses, and can complement existing analysis techniques that have been researched for path-sensitive analyses.

Many model-checking techniques [19] were developed to verify whether a program’s model meets a given property specified in temporal logic. These techniques emphasize precision and accuracy while sacrificing scalability. Many of these techniques explore all paths and result in state space explosion problem [20], [21], [22], [8], [23].

Our approach deals with the problematic exponential number of paths by forming equivalence classes of CFG paths, and analyzing one path from each equivalence class. Our empirical evaluation on the Linux kernel shows that EFGs achieve significant reductions in terms of nodes, edges, and branch nodes, especially for complex CFGs with large numbers of paths and branch nodes. Thus, performing efficient model-checking analyses using EFGs instead of CFGs can be quite beneficial.

Another line of research focuses on identifying and eliminating infeasible paths before analysis is performed. [24] claimed that 9-40% of the paths in many programs can be statically identified as infeasible paths. Goldberg et al. [25] have applied theorem-proving and Ngo and Tan [3] have proposed a heuristic approach to identify infeasible paths. Vojdani et al. [4] applies the concept of global invariants to deal with the exponentially-large number of paths eliminating infeasible paths. Holley and Rosen [26] have introduced qualified data-flow analysis to distinguish infeasible paths from the remaining paths. Other researchers have used symbolic evaluation to detect infeasible paths [5], [6], [7], [8].

Detecting infeasible paths is expensive as it relies on checking the satisfiability of conditions along a path. EFGs can minimize computation for checking path feasibility. As shown in our empirical evaluation of the Linux kernel (Section V-C), the relevant branch nodes for forming equivalence classes were also sufficient for checking feasibility.

Another challenge posed by precise path-sensitive analysis is the separation of execution effects/impact along different paths. Many heuristics schemes are aimed at achieving partial path-sensitive solutions that selectivity join or separate the effects of using different paths using logical disjunctions [1], [27], [28], [29], [30], [21], [8]. Other approaches [4], [31], [23], [32], [1], [33] determine the relevancy of a branch node through analyzing each individual execution path branching from a branch node. This process requires computation proportional to the number of execution paths.

The Binary Decision Diagram (BDD) [34] has been used in different contexts of program analysis as a way to reduce the explosion of state space [6], [35], [36]. The Binary Decision Tree (BDT) to BDD reduction has been also used for path-sensitive analysis [37], [38]. EFGs can be used in place of BDT to BDD reduction. While EFGs constitute a general technique for simplifying boolean formulas, EFGs have some advantages over BDDs for path-sensitive analysis. The BDT to BDD transformation is similar to those presented in the discussion of Algorithm I (Section IV-A). Unlike BDT to BDD reduction, the EFG transformation achieves further reduction and does not require the input CFG to be acyclic. The EFG transformation deals with cyclic graphs by incorporating a linear-time algorithm by Tarjan [16] to compute strongly-connected components of a directed graph.

CFG pruning techniques have been proposed in [39], [15] to overcome the computational complexity of exploring all paths. EFGs can complement their techniques as the EFG transformation achieves further reduction in the graph size. Other pruning techniques have been introduced by Choi et al. [40] and Ramalingam [41] to optimize data-flow graphs. While there is some commonality, those techniques are not well-suited for path-sensitive analyses; the equivalence relation -defined by [40], [41]- is defined with regard to data-flow analysis problems. This equivalence relation is different from the one defined by EFG. Path-sensitive analysis requires preserving the unique event traces and that will not be achieved by the cited techniques.

VIII. Conclusion

Efficient and accurate path-sensitive analyses pose challenges of: (a) analyzing the exponentially-increasing number of paths in a CFG, and (b) checking feasibility of paths in a CFG. This paper presents a technique that uses equivalence classes of CFG paths to address these challenges. We introduce the notion of event-flow graph (EFG) and present a linear-time algorithm to compute equivalence classes by compacting a CFG into an EFG. Each path in the EFG represents an equivalence class of paths in the CFG. We show that it is enough to perform path-sensitive analyses only on the equivalence classes produced by an EFG rather than on all the individual paths in the CFG.

Our empirical evaluation on the Linux kernel (v3.12) shows that using EFGs can significantly improve efficiency of path-sensitive analyses. Moreover, our controlled experiment results show that EFGs are human comprehensible and compact compared to their corresponding CFGs as they impose fewer paths to verify and fewer branch nodes for feasibility checking. We illustrated an application of EFGs to perform intra- and inter-procedural path-sensitive analyses.

For future work, we are currently developing a verification framework for verifying the safe-synchronization property and analyzing memory leaks in the Linux kernel. The framework leverages the EFG-based path-sensitive analyses to enable developing a sound verification framework that can scale well to large systems such as the Linux kernel.

Appendix

Theorems’ and Corollaries’ Proofs

Theorem 1 Proof. The equivalence relation ℛ_ℰ partitions the CFG paths into equivalence classes such that all paths in an equivalence class have the same event trace, and the CFG paths that are in different equivalence classes have different event traces.

Since G_EFG is the node-induced subgraph of the given CFG G consisting of the event and the relevant branch nodes, it follows that given an EFG path S, it will produce an unique event trace T and conversely given an event trace T there will be a unique EFG path S for which the event trace is T. Thus, there is a one-to-one and onto mapping between the equivalence classes of ℛ_ℰ and the paths of the EFG G_EFG.

Theorem 2 Proof. If property P holds for an object p on all CFG paths then it clearly holds for all corresponding event traces. Therefore, the case we must argue is the one in which property P is violated for object p on a CFG path S. Let T be the event trace for path S. Path S may pass through many branch nodes. We will argue that only the relevant branch nodes on that path are important in determining the existence of a feasible path with trace T. We will argue that there exists a feasible CFG path with trace T if and only if there exists a path S′ with trace T that is feasible with respect to the relevant branch nodes on S.

If every path with trace T is infeasible with respect to the relevant branch nodes, then all paths equivalent to S are also infeasible, because the addition of irrelevant branch nodes cannot turn an infeasible path into a feasible one. On the other hand, suppose there exists a path S′ with trace T that is feasible with respect to the relevant branch nodes. By the definition of irrelevant branch nodes, an equivalence class has paths going through all possible branches at an irrelevant branch node, so if the path S′ is not feasible due to having some irrelevant branch nodes we can choose feasible branches at those nodes to construct a new CFG path that is feasible and equivalent to S′. Thus, if there exists a path S′ with trace T that is feasible with respect to the relevant branch nodes on S, then there always exists a feasible CFG path with trace T.

Thus, if property P is violated on path S, then we have the following: (a) if S is feasible with respect to the relevant branch nodes on S, then there is a feasible path in the equivalence class of S, and the violation of P is a true positive; (b) if S is not feasible with respect to the relevant branch nodes on S, then all paths equivalent to S are also not feasible.

Definition 14: The boundary of a subgraph S in a directed graph G, denoted by boundary(S), is the set of nodes u ∈ S such that suc(u) ∈ suc(S).

Theorem 3 Proof. If a non-colored node u ∈ G has only one successor then it is eliminated by transformation T₁. Thus, since G is T-irreducible, |suc(u)| ≥ 2 for all non-colored nodes u ∈ G. Also, by assumption, G is an acyclic graph. Using these two facts, we will show that every subgraph S has a node with at least two successors outside S and thus |suc(S)| ≥ 2.

Let P_{v0 → vn} : (v₀, v₁), (v₁, v₂), ⋯ , (v_n−1, v_n)) be a maximal path in subgraph S. Since v_n is the terminal node of this maximal path P, its successor cannot be another node in S not on the path P. Also, the successor of v_n cannot be another node on the path P because G_c is an acyclic graph, so v_n must be a boundary node and all its successors must be outside the subgraph S. Since v_n is a non-colored node, |suc(v_n)| ≥ 2. Since v_n, a node in S, has at least two successors outside of S, we have |suc(S)| ≥ 2. This completes the proof.

Corollary 2 Proof. Note that the condensed EFG G_cEFG is the graph resulting from step (4) of the EFG construction algorithm. By construction, the condensed graph G_cEFG is a colored T-irreducible graph. Also, by construction G_cEFG is an acyclic graph. By applying the above theorem to G_cEFG we get the proof of the corollary.

Corollary 3 Proof. By construction, the graph G_T-irr resulting after step (1) of Algorithm II, consists of only event nodes, relevant branch nodes, and the irrelevant branch nodes retained by Algorithm I. We will now argue that all the irrelevant branch nodes will be eliminated when G_cEFG is constructed in step (4) of Algorithm II. According to the definition of irrelevant branch nodes (Definition 7), a node c is irrelevant if there is a subgraph S that contains c, all its branch edges, S has no event nodes, and |suc(S)| = 1. It follows from this definition and from the corollary 2 that G_cEFG does not contain any irrelevant branch nodes. Thus, the final graph produced by Algorithm II also does not contain any irrelevant branch nodes, because it consists of the nodes in G_cEFG and all the event nodes.

Acknowledgment

This research was supported by DARPA under agreement number FA8750-12-2-0126.