# An Approach for Detecting Feasible Paths Based on Minimal SSA Representation and Symbolic Execution
## 4 Detection Methodology  
This section presents our proposed approach and algorithm design, including (i) converting the source code to minimal SSA form; (ii) symbolically executing the program with a constraints extractor; (iii) avoiding repeated detection of the same feasible paths among the program paths; and (iv) solving the constraints of each new path.  
In this method, the program under test is parsed and converted to an abstract syntax tree (AST). Then, a direct translation from the AST into an SSA-based intermediate representation, which includes optimization of the SSA form to be pruned and the minimal SSA form, is conducted. The second stage starts by assigning symbolic inputs for each superglobal variable (the user input variables) and the undefined variables to represent the variables with unknown values that might affect the path conditions. The path generator algorithm will traverse each block in the SSA form. In each generation, it will flag each  
\begin{table}
\begin{tabular}{p{113.8 pt} p{113.8 pt} p{113.8 pt} p{113.8 pt}} \hline \hline
**Name** & **Technique** & **Challenges** & **Programming Language** \\ \hline \multirow{3}{*}{DART [23]} & Static source code parsing, random testing and dynamic analysis & It devolves to random testing when pointers are encountered and can only handle integer constraints. & \multirow{3}{*}{C} \\  & & Due to the use of the STP [35] solver, some paths are missed because the solver does not accurately handle all operations. & \multirow{3}{*}{C} \\  & & & \\ \multirow{3}{*}{CUTE [24]} & Concrete and symbolic execution & Failure to produce test inputs for practicable program paths. & \multirow{3}{*}{C} \\ PathCrawler [26] & Combining static analysis and dynamic analysis & A combinatorial explosion in the number of execution paths & \multirow{3}{*}{C} \\ MultiSE [6] & Merging states incrementally during symbolic execution & Treat each condition separately, which increases the chance of producing duplicated paths & \multirow{3}{*}{JavaScript} \\ KLEE [7] & [PERSON] et al. [32] algorithm and symbolic execution & Consumes a lot of time when producing feasible paths. & \multirow{3}{*}{C} \\ JpF [8] & Java virtual machine (JVM) and runtime scheduler & & \\ \multirow{3}{*}{jpf-nhandler [33]} & Automatically delegating the execution of the native method & It lacks soundness and it is not comprehensive & \multirow{3}{*}{JavaScript} \\  & Backtracking algorithm, symbolic execution, and Z3 solver & & \\ \multirow{3}{*}{SDART [12]} & Combined DART [23] with boundary values of input parameters & Some feasible paths that contain multiple conditions in the same branches are missed & \multirow{3}{*}{C} \\ \hline \hline \end{tabular}
\end{table}
Table 1: Symbolic execution studies to detect feasible paths.  
path not to be detected again and ensure that all paths were detected once. During the path generation, the conditions inside each path are extracted and stored under that path. The results of path generation and condition extraction are checked again by the introduced method (path weight method) to calculate each path's weight, and only the paths that have a unique weight are passed to the constraint solver to check their satisfiability (feasible or not) under the given inputs. Figure 4 shows the full steps of our approach to detect the feasible paths in a PHP source code.