# An Approach for Detecting Feasible Paths Based on Minimal SSA Representation and Symbolic Execution
## 4 Detection Methodology
### Avoid Duplicated Feasible Paths  
Duplicated paths are related to the branches that contain multiple conditions separated by logical operators (and, or, &&, and \(|\ |\ \)), as shown in Figure 1. These branches are split into multiple branches depending on the number of conditions inside them, which gives rise to the possibility of producing numerous paths under the same branches (called duplicated paths). The effects of not addressing these paths are manifested when a sensitive path flow is used to detect a threat in the source code. Duplicating the paths reflects an increase in false alarms in the results (detecting multiple threats in the code whilst all of them are related to one threat). To avoid producing duplicated paths, we introduce a path weight method (PWM) that can avoid generating duplicated paths. The developed PWM can be implemented in five steps, as follows:  
1. Assign a unique number to each normal block (non-conditional block) (NB) in the SSA form. 2. Count the sum of the NBs assigned a number in the current path and denote it as SNB, where SNB refers to the sum of all NBs in the current path. 3. Count the total number of conditional blocks in current path P (denoted as CB). 4. Count the total number of logical operators in current path P (denoted as LO). 5. Calculate the current path weight W(p) by using the following equation:  
\[\text{W(p)}=\frac{\text{SNB}}{\text{CB}-\text{LO}} \tag{1}\]The calculation of the current path weight in Equation (1) is performed by dividing the sum of all blocks' numbers (SNB) by the difference between the total number of conditional blocks (CB) and the total number of logical operators (LOs) in the current path. The difference between CBs and LOs provides the actual number of CBs without any repetition. The sum of all normal blocks (SNB) is used to give diversity to the weight for each path. Therefore, we can ensure that each path has its own weight, and the same weight is given to the duplicated paths. The PWM's steps for checking duplicated paths and avoiding them are presented in Algorithm 3. ```
input : All generated paths output : Only new feasible paths (non-duplicated)
```
GP[] \(\leftarrow\) list of all generated paths  NFP[] \(\leftarrow\) list of new paths (non-duplicated)  PW \(\leftarrow\) 0 // is the path weight whilePath\(\in\) GPdo  SNB \(\leftarrow\) Sum of all blocks unique number in Path (except conditional blocks)  CB \(\leftarrow\) Count the conditional blocks in Path  LO \(\leftarrow\) Count the logical operators in Path  PW \(\leftarrow\) (BS)/(CB+LO) ifPW(path) in NFPthen  Path \(\leftarrow\) Duplicated path else  Path result \(\leftarrow\) Check the satisfiability of the Path using Z3 solver ifPath result is feasiblethen  NFP \(\leftarrow\) PW(Path) else  skip and continue to the next path endif endif endwhile
```

**Algorithm 3**Avoid Duplicated Paths Algorithm. Figure 8 shows the results of the path weight method for the previous example code in Figure 1. If the path weight has not been detected before (new path), then our approach will proceed to the next step to check its feasibility (such as P1). If our PWM finds a path that has the same weight as that of a path that has been detected previously as a feasible path (such as P2 and P3, which have the same weight ('7') as P1), then it will not proceed to the next stage, in which its feasibility is checked, and the path will be considered a duplicated path. However, if our PWM finds a path that has the same weight as that of a path detected previously as an infeasible path (such as P4), then it will proceed to the next stage, in which its feasibility is checked, since the path was not detected as a feasible path before, and there is a chance for the SMT solver to solve these path conditions and consider it as a feasible path. ### Z3 Solver

The Z3 solver is based on the satisfiability modulo theory and was formulated by [PERSON] and [PERSON] while they were working at Microsoft Research [36].