# An Approach for Detecting Feasible Paths Based on Minimal SSA Representation and Symbolic Execution
## 4 Detection Methodology
### Avoid Duplicated Feasible Paths
By default, microtime() yields a string in the form \"msec sec,\" where sec is the number of seconds and msec gauges microseconds that have elapsed since sec, which is also stated in seconds. We set up the function at the first stage of generating the SSA form and it ends at the termination of generating the paths. ### Feasible Paths Detection

Table 3 depicts the outcomes of our approach and those of related studies. We compared the proposed approach with the most common engines and tools that are publicly available, such as KLEE [7] and SDART [12]. The KLEE engine is the most related work to ours. It uses the SSA form in the LLVM compiler with symbolic execution to detect feasible paths. We selected the latest version of KLEE 2.2, which was released on 7 December 2020. The SDART tool is based on CFT4 CUnit [34] and DART [23]. It reduces the number of test cases required to generate feasible paths compared with the previously mentioned tools [23; 34]. The second column in Table 3 shows the real number of feasible paths (non-duplicated paths) in each program (denoted as #TFP). The third and fourth columns show the KLEE results, where #FD denotes the number of feasible paths detected, and #DFD denotes the number of duplicated feasible paths detected. The fifth and sixth columns show the results of SDART, followed by the proposed approach's results in the seventh and eighth columns. Table 3 presents the results of each study on detecting feasible and duplicated paths. Each feasible path generated by each tool was checked to determine whether it is a new path or duplicated from previous detected paths. KLEE detected 45 feasible paths, 10 of which were duplicated. This result means that the number of new feasible paths detected by the KLEE engine was 35. Meanwhile, the SDART tool detected 27 feasible paths, four of which were duplicated. Notably, the four paths were found in the test programs that had more than two conditions at the same branch. The number of new feasible paths detected by SDART was 23. Our approach detected 35 feasible paths without any duplicated paths amongst the results, and all the duplicated paths were addressed and avoided before checking their feasibility. To answer the first question, we calculated the recall and duplicated path percentages for each study result by using the previously provided metrics (2) and (3). Table 4 shows the recall percentage of each study. The results of analyzing the test programs in Table 3 indicate that the proposed approach and KLEE have the same recall percentage (92.1%). The recall rate can reflect the comprehensiveness of the test results. Both approaches adopted the same structure to detect feasible paths. However, our approach reduced the number of instructions in the SSA form by using the minimal SSA form [11]. Meanwhile, KLEE detected 10 duplicated paths that were detected in the previous test generation. By contrast, our PWM successfully addressed such paths and did not proceed to check their satisfiability in the Z3 solver. SDART's recall percentage (65.7%) for detecting feasible paths was the lowest in the other studies. The test generation in SDART had an issue in covering the branches that had an infinite loop (fcB2002); it generated 45 test cases, without the ability to cover the last path that is related to the \"while\" loop. SDART missed 15 feasible paths that were not detected by the test programs. However, SDART was better than KLEE at reducing the number of duplicated paths in the test generation (duplicated path percentage), and the usage of this method shows its efficiency in avoiding duplicated paths under two conditions at the same branch. ### Paths Generation Time

To answer the second question, we compared the proposed approach with KLEE to reflect the reduction in the number of instructions analyzed by the minimal SSA form. KLEE [7] was implemented as a virtual machine for LLVM. However, the LLVM compiler uses the algorithm of [PERSON] et al. [32] to produce the SSA form.