# Infeasible Path Detection Based on Code Pattern and Backward Symbolic Execution

Authors: Yang Song; Xuzhou Zhang; Yun-Zhan Gong
Journal: Mathematical Problems in Engineering
 (2020)

---

## Abstract

This paper sets out to reveal the relationship between code pattern and infeasible paths and gives advices to the selection of infeasible path detection techniques. Lots of program paths are proved to be infeasible, which leads to imprecision and low efficiency of program analysis. Detection of infeasible paths is required in many areas of software engineering including test coverage analysis, test case generation, and security vulnerability analysis. The immediate cause of path infeasibility is the contradiction of path constraints, whose distribution will affect the performance of different program analysis techniques. But there is a lack of research on the distribution of contradict constraints currently. We propose a code pattern based on the empirical study of infeasible paths; the statistical result proves the correlation of the pattern with contradict constraints. We then develop a path feasibility detection method based on backward symbolic execution. Performance of the proposed technique is evaluated from two aspects: the efficiency of detecting infeasibility paths for specific program element and the improvement of applying the technique on code coverage testing.


---

## Body

## 1. Introduction

Static program analysis analyses the program without actually executing it, which plays an important role in software engineering such as verification [1] and validation [2]. A program path is infeasible if there is no input that can execute the program along the path. Many paths in a program are proved to be infeasible [3], which cause imprecision of static analysis, such as low coverage of automated software testing. So it is necessary to detect infeasible paths.The primary cause of an infeasible path is the contradict logical formulas in path constraints. Due to the fact that the satisfiability of path constraints is undecidable, the detection of infeasible path is a significant scalability challenge. Existing techniques of infeasible path detection include matching contradict pattern [4] and checking the constraints’ satisfiability by constraints solvers [5].In recent years, intensive studies have been performed on infeasible path. Papadakis and Malevvris [6] formulated an automated symbolic execution tool that can be used for the detection of infeasible paths and generate test cases; the tool makes use of an efficient path heuristic, which is integrated with random testing, and efficiently handles the explosion of the path. Gong and Yao [5] formulated a tool for automatically identifying the branch correlations of various conditional statements by using the maximum likelihood estimation to detect infeasible paths. The achievement is important for improving the efficiency of software testing. Yano et al. [7] proposed the MOST approach, which is a search-based testing technique for the generation of a test case from Extended Finite State Machines (EFSM). MOST makes use of a multiobjective evolutionary algorithm so that the generation of test cases will be able to cover a given transition (test purpose). Wong et al. [8] suggested a method that utilizes the modified breadth first search with conflict checker, and a set of minimum Feasible Transition Paths (FTP) can be generated for each transition. They developed an EFSM executable model for algorithm modeling, algorithm verification, and performance assessment. Hermadi et al. [9] proposed and evaluated an approach for determining when further searches for testing that covers exposed target paths are no longer worthwhile. It avoids the requirement for specifying limits to the number of search generations and can help in overcoming difficulties due to unfeasible pathing in search-based generation of data in tests for paths. Ruiz and Cassé [10] presented a new strategy for discovering unfeasible pathing in binary programs. Delahaye et al. [11] present a new approach to generalised unfeasible pathing from detections of single unfeasible paths and through this method demonstrated that this unfeasible path generalisation strategy compares with that of exhaustive unfeasible path detections in that the method can accelerate generating test inputs. Marashdih et al. [12] presented an approach for identifying cross site scripting (XSS) in PHP in accordance with genetic algorithms and static analyses, as well as another strategy to remove the detected XSS vulnerability from the source code [13, 14]. But as unfeasible pathing was eliminated manually, the strategy applies only to smaller programs.In industry, the infeasible analysis is used for the programmable logic controllers (PLC); PLC are specially designed computers for automating electromechanical processes in industrial applications. There are works on formal verification of PLC [15–17]; the target PLC application such as single-task and multitask PLC programs [18] is first converted into formal model using code translation from source code to C code; then symbolic execution is performed on the C code, and after that verification is done.The performances of infeasible path detection techniques are affected by different program structure, constraints type, distribution of contradict constraints, and so on. For example, the existence of input-dependent loop makes path explosion and unpredictable path length. Assuming that there are two contradict formulas at the end of a long infeasible path, analysing the path constraints reversely can immediately detect the contradiction, while forward technique has to traverse the whole path. This intuitively derives the idea of adopting appropriate analysis technique according to the various characters of infeasible paths. But there is lack of research on the distribution of contradict constraints to the best of our knowledge.Symbolic execution is a static program analysis technique that explores program paths with symbolic values and collects execution information for further analysis. The applications of symbolic execution contain automated software testing [19], data-flow analysis [20], and worst-case execution time prediction [21]. In the application of infeasible paths detection, the path constraint collected by symbolic execution is solved by a satisfiability modulo theories (SMT) solvers. Symbolic execution can be classified into two kinds by the direction of exploration: forward symbolic execution and backward symbolic execution. Forward symbolic execution has been widely used in advanced automated testing tools [22, 23]. The application of backward symbolic execution is shown in Section 2.1.This paper presents an empirical study on the common properties of the infeasible paths in real-world software program. Motivated by the result, we characterize the control-flow and data-dependency properties and conclude a code pattern. The validity of relationship between the pattern and infeasible paths is supported by statistical evidences. The path feasibility containing specific program elements of the code pattern is detected by backward symbolic execution. The experimental result shows the improvement of utilizing reverse analysis for the code pattern.This paper contains the following contributions:(i)
We investigate the common properties of infeasible paths in real programs. These properties are presented for the first time.(ii)
Based on the investigation of infeasible paths, we propose a new code pattern and suppose its properties. The statistical results show the validity of the empirical properties.(iii)
We design an infeasible path detection technique for the proposed code pattern based on backward symbolic execution. The application of the pattern and detection technique is shown in code coverage testing. The experimental result confirms the promotion of the proposed method on the performance of covering specific program elements.The remainder of this paper is organized as follows: Section2 reformulates the path feasibility program and presents the research backgrounds. Based on the investigation, a code pattern is defined and illustrated with an example in Section 3. The architecture of the backward reverse infeasible path detection technique for the code pattern is described in Section 4. Section 5 implements experiments and presents analysis to the results. The related work about infeasible path detection and backward program analysis are introduced in Section 6. Section 7 concludes this paper and provides the direction of future work.


## 2. Background

### 2.1. Application of Reverse Analysis

Reverse program analysis explores a program in reverse direction, which starts from a specific target until reaching the program entry point, thus considering only those paths that can reach the target. Another advantage of reverse analysis is that the target statement can be utilized to raise the efficiency. The work of Yu et al. [24] utilizes an exploited string pattern on the target statement to refine analysis result reversely.These advantages can be illustrated with an example in Figure1 from [25]. Statement 9 is specified as the target; all program paths containing the target are infeasible, because the logical formulas of statement, 7 if (y > 0) and 8 if (y = = 0), are contradictory. Utilizing forward analysis may exceed the time limit to check feasibilities of 2n paths. Meanwhile, reverse analysis detects contradiction immediately. The performance gap grows significantly with the increase of infeasible path length.Figure 1
A motivating example of reverse analysis.


### 2.2. Path Feasibility Problem

A program pathp consists of a sequence of nodes n1,n2,…,nk and the edges between nodes, each node n is a statement in the program, and k is the length of p.Definition 1.
(feasible path). A pathp is said to be feasible if there exists an input x⟶ in the input domain D of the program, for which executing the program with x⟶ derives a same execution trace as p. The feasibility of p is equivalent to the satisfiability of the path constraintsCp [26].Definition 2.
(Contradict Constraint). The path constraintC is the conjunction of logical formulas φ1∧φ2∧⋯∧φk, where φi is the formula of node ni. If C is satisfiable, there exists at least one input x⟶ in D satisfying C, which is denoted as CC|=Dx⟶; otherwise C is unsatisfiable if no input in D satisfies C; we say C is contradict constraint, denoted as C|=D∅. The symbol D is omitted in the following discussion for simplicity.Definition 3.
(branch correlation). A conditional branch has correlation along a path if the output of the branch can be determined by other statements or branches along this path [27]. Take two branches bri and brj as an example; if bri and brj have branch correlation, their outputs resi and resj have two relationships, which are represented by a function symbol ⊕. If resi and resj are true or false simultaneously, represented by resi⊕resj|=0, then φi and φj have Accord-Correlation. If resi and resj are contrary whenever the formulas are assigned by any concrete values, represented by resi⊕resj|=1 , then φi and φj have contra-correlation, which is denoted as φi,φj⊥.
A former work [5] reveals that branch correlation is the sufficient condition of unsatisfiable path constraints.Definition 4.
(contradict position). Letp be an infeasible path, whose constraint is C=φ1,φ2,…,φk; if there exists φi,…,φj⊥ 1≤i<⋯<j≤k, we say that the contradict position is from i to j.
Ifk-i<i−1, analysis path constraints reversely can detect path infeasibility faster than forward analysis. But there is insufficient study on the distribution of contradict path constraints. This motivates us to investigate the character of contradict constraints before selecting program analysis techniques.


### 2.3. Character Investigation for Infeasible Path

The infeasible paths are selected from academic papers about infeasible paths detection [1, 5, 28, 29] and six open-source practical projects (WCET-benchmark (http://www.mrtc.mdh.se/projects/wcet/benchmarks.html), CoreUtil (http://www.gnu.org/software/coreutils/coreutils.html), libPNG (http://libpng.org/pub/png/libpng.html), sqlite (http://sqlite.org/), nanoxm-l (http://nanoxml.sourceforge.net/orig/), and IPEG-benchmark (http://www.ipeg.com/tag/benchmark-data/)). If the path contains function call, whose return value cannot be judged directly, the function is handled as an uninterpreted function. The return value of an uninterpreted function is considered to be arbitrarily value that satisfies path constraints. This approximation of external function call preserves strict consistency for path constraints, which is used by many analysis tools [19].The characters of infeasible paths are categorized from two aspects: control flow and data flow. Loop structure is not only a fundamental control structure but also the reason for path explosion. In constraint satisfaction problem, equation formulas are more difficult to be satisfied compared to in-equation formula [30]. So we investigate the proportion of loop structures and equality operations in infeasible paths.The results of investigation are presented in Figure2. The proportions of equality operation and loop are 76% (Figure 2(a)) and 54% (Figure 2(b)) separately. A further investigation on infeasible paths containing loop shows that 60% of their contradict constraints are related to equality operation (Figure 2(b)).Figure 2
The distribution of loops and equations in infeasible paths.
(a)(b)The investigation gives a preliminary presupposition that the existences of loop structures and equality equations are relevant to infeasible paths. An intuitive explanation is that the loop structure makes path length unpredictable, leading to a high probability of infeasible path according to a conclusion in previous study [31]; the equality equation formula makes path constraints hard to satisfy.Therefore, we define a code pattern to characterize a program containing loops and equality equations in the next section.


## 2.1. Application of Reverse Analysis

Reverse program analysis explores a program in reverse direction, which starts from a specific target until reaching the program entry point, thus considering only those paths that can reach the target. Another advantage of reverse analysis is that the target statement can be utilized to raise the efficiency. The work of Yu et al. [24] utilizes an exploited string pattern on the target statement to refine analysis result reversely.These advantages can be illustrated with an example in Figure1 from [25]. Statement 9 is specified as the target; all program paths containing the target are infeasible, because the logical formulas of statement, 7 if (y > 0) and 8 if (y = = 0), are contradictory. Utilizing forward analysis may exceed the time limit to check feasibilities of 2n paths. Meanwhile, reverse analysis detects contradiction immediately. The performance gap grows significantly with the increase of infeasible path length.Figure 1
A motivating example of reverse analysis.


## 2.2. Path Feasibility Problem

A program pathp consists of a sequence of nodes n1,n2,…,nk and the edges between nodes, each node n is a statement in the program, and k is the length of p.Definition 1.
(feasible path). A pathp is said to be feasible if there exists an input x⟶ in the input domain D of the program, for which executing the program with x⟶ derives a same execution trace as p. The feasibility of p is equivalent to the satisfiability of the path constraintsCp [26].Definition 2.
(Contradict Constraint). The path constraintC is the conjunction of logical formulas φ1∧φ2∧⋯∧φk, where φi is the formula of node ni. If C is satisfiable, there exists at least one input x⟶ in D satisfying C, which is denoted as CC|=Dx⟶; otherwise C is unsatisfiable if no input in D satisfies C; we say C is contradict constraint, denoted as C|=D∅. The symbol D is omitted in the following discussion for simplicity.Definition 3.
(branch correlation). A conditional branch has correlation along a path if the output of the branch can be determined by other statements or branches along this path [27]. Take two branches bri and brj as an example; if bri and brj have branch correlation, their outputs resi and resj have two relationships, which are represented by a function symbol ⊕. If resi and resj are true or false simultaneously, represented by resi⊕resj|=0, then φi and φj have Accord-Correlation. If resi and resj are contrary whenever the formulas are assigned by any concrete values, represented by resi⊕resj|=1 , then φi and φj have contra-correlation, which is denoted as φi,φj⊥.
A former work [5] reveals that branch correlation is the sufficient condition of unsatisfiable path constraints.Definition 4.
(contradict position). Letp be an infeasible path, whose constraint is C=φ1,φ2,…,φk; if there exists φi,…,φj⊥ 1≤i<⋯<j≤k, we say that the contradict position is from i to j.
Ifk-i<i−1, analysis path constraints reversely can detect path infeasibility faster than forward analysis. But there is insufficient study on the distribution of contradict path constraints. This motivates us to investigate the character of contradict constraints before selecting program analysis techniques.


## 2.3. Character Investigation for Infeasible Path

The infeasible paths are selected from academic papers about infeasible paths detection [1, 5, 28, 29] and six open-source practical projects (WCET-benchmark (http://www.mrtc.mdh.se/projects/wcet/benchmarks.html), CoreUtil (http://www.gnu.org/software/coreutils/coreutils.html), libPNG (http://libpng.org/pub/png/libpng.html), sqlite (http://sqlite.org/), nanoxm-l (http://nanoxml.sourceforge.net/orig/), and IPEG-benchmark (http://www.ipeg.com/tag/benchmark-data/)). If the path contains function call, whose return value cannot be judged directly, the function is handled as an uninterpreted function. The return value of an uninterpreted function is considered to be arbitrarily value that satisfies path constraints. This approximation of external function call preserves strict consistency for path constraints, which is used by many analysis tools [19].The characters of infeasible paths are categorized from two aspects: control flow and data flow. Loop structure is not only a fundamental control structure but also the reason for path explosion. In constraint satisfaction problem, equation formulas are more difficult to be satisfied compared to in-equation formula [30]. So we investigate the proportion of loop structures and equality operations in infeasible paths.The results of investigation are presented in Figure2. The proportions of equality operation and loop are 76% (Figure 2(a)) and 54% (Figure 2(b)) separately. A further investigation on infeasible paths containing loop shows that 60% of their contradict constraints are related to equality operation (Figure 2(b)).Figure 2
The distribution of loops and equations in infeasible paths.
(a)(b)The investigation gives a preliminary presupposition that the existences of loop structures and equality equations are relevant to infeasible paths. An intuitive explanation is that the loop structure makes path length unpredictable, leading to a high probability of infeasible path according to a conclusion in previous study [31]; the equality equation formula makes path constraints hard to satisfy.Therefore, we define a code pattern to characterize a program containing loops and equality equations in the next section.


## 3. Loop-Dependent Equation Pattern (LDEP)

This section firstly reviews some basic terms of control flow and data flow and then defines the code pattern and illustrates with an example.


### 3.1. Preliminary Deﬁnitions

A control flow graph (CFG) is used to represent the control structure of the program. It is a directed graph and is normally denoted asGP=N,E,ne,n0, where N is a set of nodes, E is a set of edges, and ne and n0 are respective unique entry and exit nodes to the graph. Each node n ∈ N is a statement in the program, and each edge e=ni,nj is the transfer of control between statements.The CFG is a directed cyclic graph if it contains loop structure. A loop structure is denoted asL=inL,outL, where inL and outL are the entry and exit nodes to the loop.In a CFG, a nodenj dominates a node ni, if and only if every path from ne to ni contains nj [31]. If there exist paths from ni to nj, R(n) and W(n) are the read and write operations to the memory location referenced by the variables of statement n, the node nj has data dependency with ni if formula (1) holds, and data dependency is denoted as ni↔nj.(1)Rni∩Wnj∪Wni∩Rnj∪Wni∩Wnj≠∅.Letn be an assignment statement representing assigning an expression containing y to a variable v; we say the value of y propagates to v, which is denoted as v ⟶ y. Data propagation is a transitive relation in which x ⟶ y, y ⟶ z ⇒ x ⟶ z.Based on these preliminary terms, we give the fundamental definitions for the code pattern.Definition 5.
(condition dependency). Letp be a path between two conditional statements ni and nj; if p does not contain assignment statement and Rni∩Rni≠∅ or if p contains assignment statements n1,n2,…and x∈Rni∧y∈Rnj∧x↦y, we say that ni has condition dependency with nj.
The condition dependency indicates that there exist constraints to same variables at different conditional statements, which is the necessary condition of condition correlation.Definition 6.
(dominate loop). LetDn=dn1,dn2,…,dnm be the set of nodes dominating n; if dni and dni are the entry node and exit node of the same loop structure L = {dni, dnj}, then L is the dominate j loop of n.
A noden and its dominate loop L manifest as a closed loop cycle before n in a CFG, where every path from the CFG’s entry to n contains L.Definition 7.
(exclusive node). Letn be a node in a loop L=inL,inL; if every path from inL to n contains pairs of entry node and exit node of another loop L’ or does not contain any loop, then n is the exclusive node of L.Definition 8.
(concrete equation condition). LetVn=v1,v2,… be the variable set of a conditional node n; if the logical formula of n contains an expression vi=N, where N is a constant, then corresponding statement of n is a concrete equation condition.
Take example for C language; an expression containing equality operator and a constant operand is a concrete equation condition. For instance, the constraint of a conditional statement if (v = = 3) and its true branch requires the variable v to take a constant value of 3. Popular constraints solvers optimize the calculation by replacing variable with the constant 3 [32].
Besides the explicit form of concrete equation condition, some expressions also satisfy the definition implicitly. The implicit forms of concrete equation condition are listed in Table1.Table 1
Occurrence of concrete equation condition in C language.
GrammarConstraintif(v = = N)True branch:v = Nif(v! = N)False branch:v = Nif(v)False branch: −v ≠ 0switch(v) case N:Every case:v = N


### 3.2. Loop-Dependent Equation Pattern (LDEP)

Definition 9.
(loop-dependent equation pattern,LDEP). Let L be a loop structure and a concrete equation condition nc; L is the dominate loop of nc or nc is the exclusive node of L; L and nc constitute loop-dependent equation pattern if a node ni in L has data dependency or condition dependency with nc.
We introduce this definition to strictly describe a code pattern according to the result of the investigation in Section2.3. Data dependency and condition dependency are the premises of branch correlation, which gains the possibility to infeasible paths. The fact that relevant loop cannot contain redefinition to the variables of nc is worth the whistle, for the redefinition results in relocating memory for the variable, which violates the definition of data dependency [4]. Figure 3 gives three examples of LDEP. Assuming that these loops contain data-dependent or condition-dependent node of nc, whether the program structures conform to LDEP or not is labelled with√ or ×. L4+nc and L5+nc are not LDEP because they are not dominate loops of nc.
We assume an empirical propertyR of LDEP: the constraints of concrete-equation-condition node n can lead to contra-correlation, and the contradict position is close to n.
The validity of this property will be checked statistically in the next section.Figure 3
Example of LDEP.


### 3.3. Statistical Validation for Program Containing

In this section, we use binomial testing to check the validity of the proposed property. We first investigate the appearance ofLDEP in real software project. The statistic is drawn from a widespread open-source project Coreutils-8.24 (http://www.gnu.org/software/coreutils/coreutils.html). Coreutils provides some basic tools for Unix-like system. Table 2 gives the information of Coreutils and the appearance of LDEP.Table 2
Appearance of LDEP in Coreutils.
NameFilesLOCLDEPProportionCoreutils-8.24174601642664.4/KLOCIn order to perform the testing, the propertyR to be tested is separated into two hypotheses:(i)
R1: in a program containing LDEP, the constraints of concrete-equation-condition node n can lead to contra-correlation(ii)
R2: the contradict position caused by LDEP is close to nWe do statics of infeasible paths of Coreutils. As the statistic of infeasible path is conservative, we set thatR1 holds for equal or more than 70%. R2 is an assumption on the basis of R1; the alternate hypothesis for R2 holds for equal or more than 93%.(2)H0null hypothesis:pℜ1<0.7,pℜ2<0.93,H1alternative hypothesis:pℜ1≥0.7,pℜ2≥0.93.The statisticsc is computed as , taking a = 0.05 as the level of significance; u1−a is the median of normal distribution. The statistics of sample size for R1 and R2 is shown in Table 3. The statistical result is conservative for the strategy of handling external function in Section 2.3. The cases in testing x0=170≥c0=169 and x1=163≥c1=163 give affirmative result. We conclude that R1and R2 hold at 5% level of significance.Table 3
Samples for hypothesis validation.
a = 0.05pncxℜ10.7216169170ℜ20.93170163163In summary, the proposed property of program containingLDEP in Section 2.3 holds: the constraints of concrete-equation-condition node n can lead to contra-correlation, and the contradict position is close to n.


## 3.1. Preliminary Deﬁnitions

A control flow graph (CFG) is used to represent the control structure of the program. It is a directed graph and is normally denoted asGP=N,E,ne,n0, where N is a set of nodes, E is a set of edges, and ne and n0 are respective unique entry and exit nodes to the graph. Each node n ∈ N is a statement in the program, and each edge e=ni,nj is the transfer of control between statements.The CFG is a directed cyclic graph if it contains loop structure. A loop structure is denoted asL=inL,outL, where inL and outL are the entry and exit nodes to the loop.In a CFG, a nodenj dominates a node ni, if and only if every path from ne to ni contains nj [31]. If there exist paths from ni to nj, R(n) and W(n) are the read and write operations to the memory location referenced by the variables of statement n, the node nj has data dependency with ni if formula (1) holds, and data dependency is denoted as ni↔nj.(1)Rni∩Wnj∪Wni∩Rnj∪Wni∩Wnj≠∅.Letn be an assignment statement representing assigning an expression containing y to a variable v; we say the value of y propagates to v, which is denoted as v ⟶ y. Data propagation is a transitive relation in which x ⟶ y, y ⟶ z ⇒ x ⟶ z.Based on these preliminary terms, we give the fundamental definitions for the code pattern.Definition 5.
(condition dependency). Letp be a path between two conditional statements ni and nj; if p does not contain assignment statement and Rni∩Rni≠∅ or if p contains assignment statements n1,n2,…and x∈Rni∧y∈Rnj∧x↦y, we say that ni has condition dependency with nj.
The condition dependency indicates that there exist constraints to same variables at different conditional statements, which is the necessary condition of condition correlation.Definition 6.
(dominate loop). LetDn=dn1,dn2,…,dnm be the set of nodes dominating n; if dni and dni are the entry node and exit node of the same loop structure L = {dni, dnj}, then L is the dominate j loop of n.
A noden and its dominate loop L manifest as a closed loop cycle before n in a CFG, where every path from the CFG’s entry to n contains L.Definition 7.
(exclusive node). Letn be a node in a loop L=inL,inL; if every path from inL to n contains pairs of entry node and exit node of another loop L’ or does not contain any loop, then n is the exclusive node of L.Definition 8.
(concrete equation condition). LetVn=v1,v2,… be the variable set of a conditional node n; if the logical formula of n contains an expression vi=N, where N is a constant, then corresponding statement of n is a concrete equation condition.
Take example for C language; an expression containing equality operator and a constant operand is a concrete equation condition. For instance, the constraint of a conditional statement if (v = = 3) and its true branch requires the variable v to take a constant value of 3. Popular constraints solvers optimize the calculation by replacing variable with the constant 3 [32].
Besides the explicit form of concrete equation condition, some expressions also satisfy the definition implicitly. The implicit forms of concrete equation condition are listed in Table1.Table 1
Occurrence of concrete equation condition in C language.
GrammarConstraintif(v = = N)True branch:v = Nif(v! = N)False branch:v = Nif(v)False branch: −v ≠ 0switch(v) case N:Every case:v = N


## 3.2. Loop-Dependent Equation Pattern (LDEP)

Definition 9.
(loop-dependent equation pattern,LDEP). Let L be a loop structure and a concrete equation condition nc; L is the dominate loop of nc or nc is the exclusive node of L; L and nc constitute loop-dependent equation pattern if a node ni in L has data dependency or condition dependency with nc.
We introduce this definition to strictly describe a code pattern according to the result of the investigation in Section2.3. Data dependency and condition dependency are the premises of branch correlation, which gains the possibility to infeasible paths. The fact that relevant loop cannot contain redefinition to the variables of nc is worth the whistle, for the redefinition results in relocating memory for the variable, which violates the definition of data dependency [4]. Figure 3 gives three examples of LDEP. Assuming that these loops contain data-dependent or condition-dependent node of nc, whether the program structures conform to LDEP or not is labelled with√ or ×. L4+nc and L5+nc are not LDEP because they are not dominate loops of nc.
We assume an empirical propertyR of LDEP: the constraints of concrete-equation-condition node n can lead to contra-correlation, and the contradict position is close to n.
The validity of this property will be checked statistically in the next section.Figure 3
Example of LDEP.


## 3.3. Statistical Validation for Program Containing

In this section, we use binomial testing to check the validity of the proposed property. We first investigate the appearance ofLDEP in real software project. The statistic is drawn from a widespread open-source project Coreutils-8.24 (http://www.gnu.org/software/coreutils/coreutils.html). Coreutils provides some basic tools for Unix-like system. Table 2 gives the information of Coreutils and the appearance of LDEP.Table 2
Appearance of LDEP in Coreutils.
NameFilesLOCLDEPProportionCoreutils-8.24174601642664.4/KLOCIn order to perform the testing, the propertyR to be tested is separated into two hypotheses:(i)
R1: in a program containing LDEP, the constraints of concrete-equation-condition node n can lead to contra-correlation(ii)
R2: the contradict position caused by LDEP is close to nWe do statics of infeasible paths of Coreutils. As the statistic of infeasible path is conservative, we set thatR1 holds for equal or more than 70%. R2 is an assumption on the basis of R1; the alternate hypothesis for R2 holds for equal or more than 93%.(2)H0null hypothesis:pℜ1<0.7,pℜ2<0.93,H1alternative hypothesis:pℜ1≥0.7,pℜ2≥0.93.The statisticsc is computed as , taking a = 0.05 as the level of significance; u1−a is the median of normal distribution. The statistics of sample size for R1 and R2 is shown in Table 3. The statistical result is conservative for the strategy of handling external function in Section 2.3. The cases in testing x0=170≥c0=169 and x1=163≥c1=163 give affirmative result. We conclude that R1and R2 hold at 5% level of significance.Table 3
Samples for hypothesis validation.
a = 0.05pncxℜ10.7216169170ℜ20.93170163163In summary, the proposed property of program containingLDEP in Section 2.3 holds: the constraints of concrete-equation-condition node n can lead to contra-correlation, and the contradict position is close to n.


## 4. Infeasible Path Detection Based on Backward Symbolic Execution

To make use of the properties ofLDEP, an automated coverage testing tool Hybrid-SymExe based on backward symbolic execution is proposed in this section. Compared with the general symbolic execution based coverage testing tool, Hybrid-SymExe consists of a general symbolic execution engine, a module recognizing LDEP, and a backward symbolic execution engine to search feasible path for a specific target.


### 4.1. Architecture Overview

The overview of Hybrid-SymExe’s architecture is depicted in Figure4.Figure 4
The architecture of Hybrid-SymExe.Firstly, a pretreatment is used to detect the existence ofLDEP in the program under test (PUT). PUT that does not contain LDEP is handled to a coverage testing process based on general symbolic execution. If the PUT contains LDEP, the program element of concrete equation condition is selected as the target denoted as LDEP−e according to specified coverage criteria. Automated finding of feasible path covering LDEP−e is achieved by backward symbolic execution, while other program elements are managed by the general technique.


### 4.2. Backward Symbolic Execution

The advantages of backward symbolic execution are utilizing the concrete value to optimize constraints and traversing CFG reversely to searching only in the target space. Compared to general symbolic execution, backward symbolic execution is different in that it starts execution from the target and then searches the program backward, which leads to two changes in implementation:(i)
Variables are used before definition. The backward symbolic execution searches the closest definition to symbolize the variable when meeting the variable at first time. This is similar to lazy initialization [33].(ii)
The assignment operation affects the collected constraints rather than future constraints construction. If a variablev in the collected constraints C is assigned by an expression exp in the next assignment statement, then all the occurrences of v in C are replaced by exp.The algorithm of backward symbolic execution is described by pseudocodes as shown in Algorithm1. We use the usual description in symbolic execution [34]. C and A represent conditional statement and assignment statement. C is the collection of constraints. Given a map M representing the memory, we use M′:=m+m↦v to denote the map M‘ that is the same as M except that M’(m) = v.Algorithm 1: Search feasible path for n BACKWARDSEARCH.
Require: Target n, CFG g = {N, E, ne, no}Ensure: A feasible path from ne to n path;if first thenℳ⇐ SYMBOLICINIT (inputparams);path ⇐ INITPATH()state ⇐initStateC,ℳ;end ififn is in thenReturnPathin;end iffor each pre in precessors of n doSTORESTATE();b_flag⇐ EDGEOF(pre, n);ifpre is C thenC⇐C∧SymbolicExecutionpre,b_flag;end ififpre is A then[x: symbolExpression]⇐ SYMBOLICEXECUTION(pre);ℳ;=ℳ+x↦x′;C⇐REPLACE X WITH EXPRESSIONx:=SymbolicExpression;end ifif IsCONSTRAINTSCONSISTENTC is TRUE thenBACKWARDSEARCHpre,state⇐C,ℳ,path∧n;elseRESTORE STATE();continue;end ifend forAn initial procedure firstly initializes the memory mapM, path pathn, and search state state and then starts symbolic execution from n. If current statement is C, the SymbolicExecution procedure extracts the symbolic expression of C; if current statement is A, let a variable v in the collected constraints C be assigned by an expression exp at A; then the all occurrences of v in C are replaced by exp. Each time C is updated, its satisfiability is checked by the ConstraintsConsistent procedure. The search achieves a feasible path when it reaches ne or returns null if it backtracks to the initial state.


### 4.3. Case Study

This section gives an example to explain the reverse and forward infeasible path detection work onLDEP. The example code in Figure 5 is selected from a practical project. Statement 9 is selected as the target to be covered. For simplicity, only loop structures and the statements relevant to the target condition true branch, i = = 20, are kept.Figure 5
An example code containing LDEP.The value ofi is added as different constant by the parity of i at every iteration of loop. The jump out condition of loop is related to the input variable n. This code contains typical case of LDEP because i = = 0 has data dependency and conditional dependency with statements in the loop. The loop must execute at least six iterations (i = 9, n = 20) to cover the target statement.The search tree of utilizing forward and reverse analysis to find feasible path containing the target is presented in Figure6. Lines represent constraints and operations. Value domains in the box are the values satisfying the constraints of incoming edges.Figure 6
Applying backward analysis and forward analysis on the motivating example.The left figure is the process of reverse analysis. In reverse search, the target condition truebranch,i = = 20, can be used as a precondition to optimize the constraints. Then the search forks two possible operations i = i + 3 and i = i + 1 and checks satisfiability of each constraint at statement 4. It is obvious that the available value 19 for i contradicts the predicate “i is an even number”; hence this branch of search tree is pruned. In every round of loop iteration, the reverse search detects the contradiction and discards these paths.Meanwhile, the process of using forward analysis to find feasible path is shown in the right figure. The input domains for both variables are sets of concrete values, with which both true and false branches of statement 4 are satisfiable. The search tree cannot be pruned, and also the size of value domain cannot be reduced.This case shows that utilizing reverse analysis is more efficient than forward analysis in finding feasible path for the target in the given code containingLDEP.


## 4.1. Architecture Overview

The overview of Hybrid-SymExe’s architecture is depicted in Figure4.Figure 4
The architecture of Hybrid-SymExe.Firstly, a pretreatment is used to detect the existence ofLDEP in the program under test (PUT). PUT that does not contain LDEP is handled to a coverage testing process based on general symbolic execution. If the PUT contains LDEP, the program element of concrete equation condition is selected as the target denoted as LDEP−e according to specified coverage criteria. Automated finding of feasible path covering LDEP−e is achieved by backward symbolic execution, while other program elements are managed by the general technique.


## 4.2. Backward Symbolic Execution

The advantages of backward symbolic execution are utilizing the concrete value to optimize constraints and traversing CFG reversely to searching only in the target space. Compared to general symbolic execution, backward symbolic execution is different in that it starts execution from the target and then searches the program backward, which leads to two changes in implementation:(i)
Variables are used before definition. The backward symbolic execution searches the closest definition to symbolize the variable when meeting the variable at first time. This is similar to lazy initialization [33].(ii)
The assignment operation affects the collected constraints rather than future constraints construction. If a variablev in the collected constraints C is assigned by an expression exp in the next assignment statement, then all the occurrences of v in C are replaced by exp.The algorithm of backward symbolic execution is described by pseudocodes as shown in Algorithm1. We use the usual description in symbolic execution [34]. C and A represent conditional statement and assignment statement. C is the collection of constraints. Given a map M representing the memory, we use M′:=m+m↦v to denote the map M‘ that is the same as M except that M’(m) = v.Algorithm 1: Search feasible path for n BACKWARDSEARCH.
Require: Target n, CFG g = {N, E, ne, no}Ensure: A feasible path from ne to n path;if first thenℳ⇐ SYMBOLICINIT (inputparams);path ⇐ INITPATH()state ⇐initStateC,ℳ;end ififn is in thenReturnPathin;end iffor each pre in precessors of n doSTORESTATE();b_flag⇐ EDGEOF(pre, n);ifpre is C thenC⇐C∧SymbolicExecutionpre,b_flag;end ififpre is A then[x: symbolExpression]⇐ SYMBOLICEXECUTION(pre);ℳ;=ℳ+x↦x′;C⇐REPLACE X WITH EXPRESSIONx:=SymbolicExpression;end ifif IsCONSTRAINTSCONSISTENTC is TRUE thenBACKWARDSEARCHpre,state⇐C,ℳ,path∧n;elseRESTORE STATE();continue;end ifend forAn initial procedure firstly initializes the memory mapM, path pathn, and search state state and then starts symbolic execution from n. If current statement is C, the SymbolicExecution procedure extracts the symbolic expression of C; if current statement is A, let a variable v in the collected constraints C be assigned by an expression exp at A; then the all occurrences of v in C are replaced by exp. Each time C is updated, its satisfiability is checked by the ConstraintsConsistent procedure. The search achieves a feasible path when it reaches ne or returns null if it backtracks to the initial state.


## 4.3. Case Study

This section gives an example to explain the reverse and forward infeasible path detection work onLDEP. The example code in Figure 5 is selected from a practical project. Statement 9 is selected as the target to be covered. For simplicity, only loop structures and the statements relevant to the target condition true branch, i = = 20, are kept.Figure 5
An example code containing LDEP.The value ofi is added as different constant by the parity of i at every iteration of loop. The jump out condition of loop is related to the input variable n. This code contains typical case of LDEP because i = = 0 has data dependency and conditional dependency with statements in the loop. The loop must execute at least six iterations (i = 9, n = 20) to cover the target statement.The search tree of utilizing forward and reverse analysis to find feasible path containing the target is presented in Figure6. Lines represent constraints and operations. Value domains in the box are the values satisfying the constraints of incoming edges.Figure 6
Applying backward analysis and forward analysis on the motivating example.The left figure is the process of reverse analysis. In reverse search, the target condition truebranch,i = = 20, can be used as a precondition to optimize the constraints. Then the search forks two possible operations i = i + 3 and i = i + 1 and checks satisfiability of each constraint at statement 4. It is obvious that the available value 19 for i contradicts the predicate “i is an even number”; hence this branch of search tree is pruned. In every round of loop iteration, the reverse search detects the contradiction and discards these paths.Meanwhile, the process of using forward analysis to find feasible path is shown in the right figure. The input domains for both variables are sets of concrete values, with which both true and false branches of statement 4 are satisfiable. The search tree cannot be pruned, and also the size of value domain cannot be reduced.This case shows that utilizing reverse analysis is more efficient than forward analysis in finding feasible path for the target in the given code containingLDEP.


## 5. Experimental Evaluation

In this section, we firstly report the results of a binomial testing to statistically validate the property presented in Section3.2. The second experiment compares the performance of using backward symbolic execution with using the general symbolic execution on finding feasible path for LDEP−e. The last experiment performs the improvement of introducing backward technique to automated coverage testing as an auxiliary for specific program element.


### 5.1. Comparison Experiment

The result of statistical validation verifies the property ofLDEP, which is suitable for reverse analysis. This experiment compares the performance of utilizing backward symbolic execution and general symbolic execution to find feasible path for a specific target of LDEP.The test programs are picked out from papers mentioned in Section2.3 and Coreutils. The concrete equation conditions LDEP−e are selected as the targets. We run backward symbolic execution and general symbolic execution to search feasible paths containing LDEP−e. In addition, a popular automated testing tool Pex [35] is also used as a comparison. Pex cannot be appointed to generate paths for a single program element; only whether or not it succeeded is recorded. The results are shown in Table 4.Table 4
Comparison between forward analysis and reverse analysis.
Test codeLOCSuccessTime (ms)Total paths exploredPexForwardBackwardForwardBackwardForwardBackwardSuccessFoo11NoYesTimeout729.62—273Nopel21YesYes892.2396.4112329Yesdo_decode43YesYes263.12173.078971Yeswanshu22YesYes14.516.12140Yesfenyu17NoYesTimeout54.3—39NoThe data in the table shows that general symbolic execution (forward) fails to find feasible path forLDEP−e in foo and fenyu within time limits; meanwhile backward symbolic execution (backward) finds feasible paths for all LDEP−e in tested codes. The time consumption of backward symbolic execution is lower than that of forward technique except for wanshu. The reason is that the LDEP−e in wanshu can be covered after executing the loop for 1 iteration, so the general symbolic execution can achieve feasible path faster than backward technique by saving the time of recognizing LDEP. Pex could not succeed for foo and fenyu as well.In summary, using backward symbolic execution to find feasible path forLDEP−e is better than using forward symbolic execution in most cases. There exist exceptions because the correlation of LDEP and contra-correlation are not inevitable.


### 5.2. Performance Improvement Experiment

One of the direct applications of infeasible path detection is automated coverage testing. Most coverage testing tools are based on forward analysis techniques. This section performs experiment to evaluate the improvement of applying backward symbolic execution on automated coverage testing as an auxiliary for specific target to be covered.We compare the performance of Hybrid-SymExe, Hybrid-SymExe without the backward analysis module (SymExe), and Pex on achieving full coverage of the test codes to show the improvement. The branch coverage and time assumption are shown in Table5.Table 5
Improvement of applying reverse analysis to SymExe.
Test codeBranch coverageTime consumption (ms)SymExe (%)Hybrid-SymExe (%)Pex (%)SymExeHybrid-SymExePexFoo67.710090.482000.01321.21634pel1001001001352.3877.2252do_decode100100100420.8460.7288wanshu92100100223.4289.3264fenyu83.310091.672000.0639.3287The data shows that Hybrid-SymExe receives better performance than SymExe except forwanshu. Pex is faster than Hybrid-SymExe and SymExe because Pex uses dynamic execution technique, but Pex fails to achieve full coverage for foo and fenyu.In summary, it is hard to coverLDEP−e by general symbolic execution. Using backward symbolic execution as an auxiliary for LDEP−e can improve the coverage of automated coverage testing tool. The time consumption after integrating backward symbolic execution increases for spending time on recognizing LDEP.


## 5.1. Comparison Experiment

The result of statistical validation verifies the property ofLDEP, which is suitable for reverse analysis. This experiment compares the performance of utilizing backward symbolic execution and general symbolic execution to find feasible path for a specific target of LDEP.The test programs are picked out from papers mentioned in Section2.3 and Coreutils. The concrete equation conditions LDEP−e are selected as the targets. We run backward symbolic execution and general symbolic execution to search feasible paths containing LDEP−e. In addition, a popular automated testing tool Pex [35] is also used as a comparison. Pex cannot be appointed to generate paths for a single program element; only whether or not it succeeded is recorded. The results are shown in Table 4.Table 4
Comparison between forward analysis and reverse analysis.
Test codeLOCSuccessTime (ms)Total paths exploredPexForwardBackwardForwardBackwardForwardBackwardSuccessFoo11NoYesTimeout729.62—273Nopel21YesYes892.2396.4112329Yesdo_decode43YesYes263.12173.078971Yeswanshu22YesYes14.516.12140Yesfenyu17NoYesTimeout54.3—39NoThe data in the table shows that general symbolic execution (forward) fails to find feasible path forLDEP−e in foo and fenyu within time limits; meanwhile backward symbolic execution (backward) finds feasible paths for all LDEP−e in tested codes. The time consumption of backward symbolic execution is lower than that of forward technique except for wanshu. The reason is that the LDEP−e in wanshu can be covered after executing the loop for 1 iteration, so the general symbolic execution can achieve feasible path faster than backward technique by saving the time of recognizing LDEP. Pex could not succeed for foo and fenyu as well.In summary, using backward symbolic execution to find feasible path forLDEP−e is better than using forward symbolic execution in most cases. There exist exceptions because the correlation of LDEP and contra-correlation are not inevitable.


## 5.2. Performance Improvement Experiment

One of the direct applications of infeasible path detection is automated coverage testing. Most coverage testing tools are based on forward analysis techniques. This section performs experiment to evaluate the improvement of applying backward symbolic execution on automated coverage testing as an auxiliary for specific target to be covered.We compare the performance of Hybrid-SymExe, Hybrid-SymExe without the backward analysis module (SymExe), and Pex on achieving full coverage of the test codes to show the improvement. The branch coverage and time assumption are shown in Table5.Table 5
Improvement of applying reverse analysis to SymExe.
Test codeBranch coverageTime consumption (ms)SymExe (%)Hybrid-SymExe (%)Pex (%)SymExeHybrid-SymExePexFoo67.710090.482000.01321.21634pel1001001001352.3877.2252do_decode100100100420.8460.7288wanshu92100100223.4289.3264fenyu83.310091.672000.0639.3287The data shows that Hybrid-SymExe receives better performance than SymExe except forwanshu. Pex is faster than Hybrid-SymExe and SymExe because Pex uses dynamic execution technique, but Pex fails to achieve full coverage for foo and fenyu.In summary, it is hard to coverLDEP−e by general symbolic execution. Using backward symbolic execution as an auxiliary for LDEP−e can improve the coverage of automated coverage testing tool. The time consumption after integrating backward symbolic execution increases for spending time on recognizing LDEP.


## 6. Related Work

### 6.1. Backward Analysis

Backward execution is common in data flow analysis. Reps et al. [36] showed the research on improving the efficiency of interprocedure data flow analysis by utilizing the reachability of control flow based on the IFDS data flow framework. Building on this work, ESC/Java [37] and Chandra et al. [38] integrated backward analysis to compute the weakest precondition for a target statement. The key optimization of Snugglebug is pruning search space by constructing the call graph on-demand.Similarly, Ma et al. [39] combined call graph with symbolic execution in constraint based testing. Besides, heuristic strategy is used to offer guidance to path generation. They concluded that the integration of different strategy is always better than using separate technique. This conclusion gives us inspirations of selecting different analysis techniques according to the different characters of program.


### 6.2. Infeasible Path Detection

The infeasible path detection has been applied in many software engineering fields [27, 40], in particular structural testing and coverage analysis. Detecting infeasible path can save considerable effort for automated coverage testing. The most two common approaches of infeasible path detection are dynamic analysis and static analysis. The dynamic technique uses the information of dynamic execution to predicate infeasible paths. The static technique analyses the existence of infeasible paths without executing the program.


#### 6.2.1. Dynamic Technique

Dynamic technique can be used to find solution for path-oriented test case generation problem. Bueno and Jino [41] detected infeasible path by monitoring the fitness value of execution trace. The proposed fitness function combined control flow and data flow information to improve analysis precision. The definition of LDEP also involves control and data flow information. Ngo and Tan [42] refined previous work [41] by taking empirical correlation of statement into consideration. The target path is reported as infeasible once an undesired branch is taken.A recent dynamic technique [11] utilized data dependency information to construct a generalised infeasibility automaton for matching infeasible paths in the future search.The major problem of dynamic technique is the huge consumption of computation.


#### 6.2.2. Static Technique

The immediate cause of infeasible path is the contradictory path constraints [34, 40, 43]. The constraint based testing uses symbolic execution to generate the constraints representing the path. If the constraints are found to be unsatisfiable by a constraint solver, then the path is pronounced to be infeasible. The performance of symbolic execution is subject to the ability of its underneath constraint solver and the scalability to large real-world projects.Instead of detecting one infeasible path at a time by examining path constraint, recognizing infeasible code pattern can detect a group of infeasible paths. The infeasible code pattern [4, 44] can be extracted from empirical study on the common properties of infeasible paths. Paths containing infeasible code pattern can be reported as infeasible immediately. The code pattern LDEP we proposed is different from the infeasible code pattern as LDEP reveals a potential correlation between program character and the distribution of contradict constraints. Therefore, LDEP and infeasible code pattern can work together to handle infeasible path.Another detection approach based on code pattern is branch correlation. Bodiket al. concluded in [27] that 9% to 40% of conditional statements exhibit correlation which can lead to infeasible path. Gong and Yao [5] proposed a new approach to detect branch correlation by dynamic technique, which employed maximum likelihood estimation for the probability of branch correlation based on the output values of branches. However, only part of branch correlation can be detected.


## 6.1. Backward Analysis

Backward execution is common in data flow analysis. Reps et al. [36] showed the research on improving the efficiency of interprocedure data flow analysis by utilizing the reachability of control flow based on the IFDS data flow framework. Building on this work, ESC/Java [37] and Chandra et al. [38] integrated backward analysis to compute the weakest precondition for a target statement. The key optimization of Snugglebug is pruning search space by constructing the call graph on-demand.Similarly, Ma et al. [39] combined call graph with symbolic execution in constraint based testing. Besides, heuristic strategy is used to offer guidance to path generation. They concluded that the integration of different strategy is always better than using separate technique. This conclusion gives us inspirations of selecting different analysis techniques according to the different characters of program.


## 6.2. Infeasible Path Detection

The infeasible path detection has been applied in many software engineering fields [27, 40], in particular structural testing and coverage analysis. Detecting infeasible path can save considerable effort for automated coverage testing. The most two common approaches of infeasible path detection are dynamic analysis and static analysis. The dynamic technique uses the information of dynamic execution to predicate infeasible paths. The static technique analyses the existence of infeasible paths without executing the program.


### 6.2.1. Dynamic Technique

Dynamic technique can be used to find solution for path-oriented test case generation problem. Bueno and Jino [41] detected infeasible path by monitoring the fitness value of execution trace. The proposed fitness function combined control flow and data flow information to improve analysis precision. The definition of LDEP also involves control and data flow information. Ngo and Tan [42] refined previous work [41] by taking empirical correlation of statement into consideration. The target path is reported as infeasible once an undesired branch is taken.A recent dynamic technique [11] utilized data dependency information to construct a generalised infeasibility automaton for matching infeasible paths in the future search.The major problem of dynamic technique is the huge consumption of computation.


### 6.2.2. Static Technique

The immediate cause of infeasible path is the contradictory path constraints [34, 40, 43]. The constraint based testing uses symbolic execution to generate the constraints representing the path. If the constraints are found to be unsatisfiable by a constraint solver, then the path is pronounced to be infeasible. The performance of symbolic execution is subject to the ability of its underneath constraint solver and the scalability to large real-world projects.Instead of detecting one infeasible path at a time by examining path constraint, recognizing infeasible code pattern can detect a group of infeasible paths. The infeasible code pattern [4, 44] can be extracted from empirical study on the common properties of infeasible paths. Paths containing infeasible code pattern can be reported as infeasible immediately. The code pattern LDEP we proposed is different from the infeasible code pattern as LDEP reveals a potential correlation between program character and the distribution of contradict constraints. Therefore, LDEP and infeasible code pattern can work together to handle infeasible path.Another detection approach based on code pattern is branch correlation. Bodiket al. concluded in [27] that 9% to 40% of conditional statements exhibit correlation which can lead to infeasible path. Gong and Yao [5] proposed a new approach to detect branch correlation by dynamic technique, which employed maximum likelihood estimation for the probability of branch correlation based on the output values of branches. However, only part of branch correlation can be detected.


## 6.2.1. Dynamic Technique

Dynamic technique can be used to find solution for path-oriented test case generation problem. Bueno and Jino [41] detected infeasible path by monitoring the fitness value of execution trace. The proposed fitness function combined control flow and data flow information to improve analysis precision. The definition of LDEP also involves control and data flow information. Ngo and Tan [42] refined previous work [41] by taking empirical correlation of statement into consideration. The target path is reported as infeasible once an undesired branch is taken.A recent dynamic technique [11] utilized data dependency information to construct a generalised infeasibility automaton for matching infeasible paths in the future search.The major problem of dynamic technique is the huge consumption of computation.


## 6.2.2. Static Technique

The immediate cause of infeasible path is the contradictory path constraints [34, 40, 43]. The constraint based testing uses symbolic execution to generate the constraints representing the path. If the constraints are found to be unsatisfiable by a constraint solver, then the path is pronounced to be infeasible. The performance of symbolic execution is subject to the ability of its underneath constraint solver and the scalability to large real-world projects.Instead of detecting one infeasible path at a time by examining path constraint, recognizing infeasible code pattern can detect a group of infeasible paths. The infeasible code pattern [4, 44] can be extracted from empirical study on the common properties of infeasible paths. Paths containing infeasible code pattern can be reported as infeasible immediately. The code pattern LDEP we proposed is different from the infeasible code pattern as LDEP reveals a potential correlation between program character and the distribution of contradict constraints. Therefore, LDEP and infeasible code pattern can work together to handle infeasible path.Another detection approach based on code pattern is branch correlation. Bodiket al. concluded in [27] that 9% to 40% of conditional statements exhibit correlation which can lead to infeasible path. Gong and Yao [5] proposed a new approach to detect branch correlation by dynamic technique, which employed maximum likelihood estimation for the probability of branch correlation based on the output values of branches. However, only part of branch correlation can be detected.


## 7. Conclusion

In this paper, we propose a code pattern based on empirical study of infeasible paths and exhibit its correlation with the distribution of contradict path constraints. This achievement can promote the effectiveness of infeasible path detection through utilizing backward symbolic execution for the specific program element. With the current prototype tool, a significant improvement can be seen by applying the proposed approach on coverage testing as an auxiliary.The novelty of the research results lies in the statistical validation for the empirical property of the proposed code pattern and providing the basis for employing suitable techniques according to the character of program to be analysed.Some researchers define the infeasible path as any path that is not executable under any test cases [45] and remove infeasible paths from the entire path of the control flow graph [46]. Balakrishnan et al. [47, 48] stated that developers need to distinguish these infeasible paths from the other paths of the entire control flow graph. The majority of the approaches on eliminating infeasible paths focus on C, C++, and Java programming languages. It is noteworthy that all current approaches cannot determine most of the infeasible paths effectively.In this paper, based on the investigation of infeasible paths, we explore the common properties of infeasible paths in real programs. These properties are presented for the first time. We propose a new code pattern and suppose its properties. The statistical results show the validity of the empirical properties.However, it is in a first stage of research on the distribution of contradict path constraints. We believe that this is a promising future direction of integrating different techniques to improve the efficiency of software engineering activities from different aspects [20, 49–51].



---

*Source: 4258291-2020-05-25.xml*