# An Approach for Detecting Feasible Paths Based on Minimal SSA Representation and Symbolic Execution
## 4 Detection Methodology
### Avoid Duplicated Feasible Paths
The SMT solver works in such a way that when a first-order logic formula is specified, the solver determines if satisfiability is met. Formula f is considered satisfiable if a value that leads to f being true exists. The solver is given inputs regarding the expression and the set of applicable constraints. The solver then attempts to identify a solution applicable under the specified constraints. The reason behind using Z3 was that it has been established as a high-performance technique for theorem proof [41]. Additionally, this solver is available for free under the Microsoft Research License Agreement (MSR-LA). Furthermore, it has Application Programming Interfaces (API) s for several languages, which make this tool compatible with several platforms. Once the path generation produces the condition of each path, it transforms them to the Z3 context based on their guidelines [36], and the results are sent to the Z3 solver to check satisfiability of those path constraints. Figure 8 shows the results of our proposed work on the example program in Figure 1.

The first column in the result table in Figure 8 shows the file name. The second column shows the number of instructions produced by the minimal SSA algorithm. The third column provides the number of branches analyzed, and the detected feasible paths (new paths) are shown on the fourth column. The last column presents the time (in seconds) required to generate all of the paths, excluding the Z3 solver time. Figure 8 shows that the first path was checked, and the results indicated that it was satisfiable (sat) under their given inputs. The second and third paths were not checked by Z3 solver since they have the same weight as the first path, which was detected as feasible. The fourth path was not satisfied (unsat) by the Z3 solver on the basis of the given inputs. Therefore, it was considered an infeasible path and was not executed at all under the given inputs. ## 5 Experimental Results and Evaluation

The proposed approach was implemented in PHP, and the implementation followed the architecture in Figure 4 and the approach presented in the previous sections. The

Figure 8: The satisfiability results of the program in Figure 1 using Z3 solver. objective of the experimental evaluation was to answer the following questions: (1) Is the proposed approach able to detect the feasible paths and avoid the detection of duplicated paths amongst the test programs (Section 5.3)? (2) Does the minimal SSA form reduce the time required to generate the paths compared with other studies that used the SSA form (Section 5.4)? (3) Is the proposed approach able to process a large set of PHP applications (Section 5.5)? ### The Dataset

The proposed approach focuses on PHP as the most popular web technology for building a web application. To our knowledge, no study has been conducted to detect feasible paths on the basis of PHP. Therefore, we used the same test programs written in C language that were used in related studies [42; 43; 44; 45; 46; 47; 48; 49; 50; 51]. These programs were rewritten in PHP. Table 2 presents the characteristics of the test programs, including the number of lines of codes, LoC, the number of branches of each program, B (can be either selection or loop statements, such as IF, IF ELSE, WHILE, FOR and DO), Description, the number of feasible paths (non-duplicated paths), F, and their reference(s), Refs. The programming language used to write these programs does not affect the results of the programs because target paths are based on the control flow graph; thus, the program does not have a specific statement related to one programming language [43]. This task is a common practice in testing experiments undertaken by several studies that rewrote these programs in MATLAB [44; 48]. Others rewrote them in Java [52; 53; 54].