# An Approach for Detecting Feasible Paths Based on Minimal SSA Representation and Symbolic Execution
## 4 Detection Methodology
### Path Generation and Constraints Extractor  
Each block in the SSA form contains some instructions (i.e., variables, expressions, and conditions) of that block. As the SSA form contains one start block and one end block, it helps to know the start and end points of each path. The complete process of generating the paths and extracting the conditions from the minimal SSA form is presented in Algorithm 2.  
The path generator always starts from the first block as an initial block. It will first store the instructions of each block in an array of instructions and those to be used later in the constraint extractor to determine the conditions' side values. The functions inside the SSA structure are defined as a separate group of blocks. Once the generator finds a function call inside the block, it will move to the function blocks and track the instructions inside that function, and each instruction inside the function is stored in the array of instructions for that path, and the conditions inside that function are also stored in the path conditions. The last block in the function block contains the termination of that function, which will return the generator to the function call instruction.  
Each condition contains two or more children based on the condition types (i.e., if and switch). If the generator finds a condition, the generator will choose one of the children it has not yet visited, and the chosen child will be marked as visited. In this way, the generator ensures that it will not follow the same path in the next generation. Each child block will be visited once during the path, and each condition state among the path is stored in the array of conditions. At the termination of the path, a collection of conditions exist in the array of the conditions, and the path generator starts from the first block again to generate a new path.  
Since all variables from each block are stored in the array of instructions, the constraint extractor replaces the conditions of both side variables with their concrete values from the array of instructions. For example, a variable $X was defined with a value of 5, followed by a condition ($X == 5). The condition has left and right values that must be compared. First, the variable is stored in the array of instructions, and the constraint extractor searches for the condition of the left-side variable in the array of instructions and replaces the variable \"$X\" with its concrete value, which is 5. The condition's right-side variable is a concrete value and, thus, it will not be replaced because it does not exist in the array of instructions for that path. The results of the path generator and constraint extractor are a list of path  
Figure 7: Assigning a symbolic inputs for the loop condition to be executed symbolically.  
conditions and their instructions are sent to the Z3 solver to check the satisfiability of these conditions.  
```
input :SSA form output :Path conditions of the source code
```  
Paths [] \(\leftarrow\) list represent the generated paths \(\text{Cond}\) [] \(\leftarrow\) list represent the generated conditions \(\text{Instr}\) [] \(\leftarrow\) list represent the generated instructions \(\text{i}\gets 1\) FunctionPathGeneration(\(SSA\)): foreach\(B\_i\in SSA\)do if\(B\_i\)[type] is conditional blockthen ifthis conditional block Not Visited beforethen Replace condition variables with concrete values \(\text{Cond}\leftarrow\text{Store}\) the condition  Flag this condition state as visited \(\text{i}\leftarrow\text{Store}\) the next block number  PathGeneration(SSA) else  Move to next Block endif elseif\(B\_i\)[type] is Functionthen i \(\leftarrow\) Store the Function block number PathGeneration(SSA) elseif\(B\_i\)[type] is Terminatethen Paths \(\leftarrow\) Instr & Cond  i \(\gets\) 1  PathGeneration(SSA) else  Instr \(\leftarrow\) SSA[B_i][type] endif endforeach endfunction ```
**Algorithm 2**Path Generation and Constraints Extractor Algorithm.