# An Approach for Detecting Feasible Paths Based on Minimal SSA Representation and Symbolic Execution
## 2 Background
### Symbolic Execution  
Symbolic execution is the execution of a program with a symbolic representation of inputs instead of concrete values [22]. Concrete executors, for example, an interpreter, can only evaluate expressions consisting of concrete values. Meanwhile, symbolic executors allow the existence of symbolic values in the expressions, that is, expressions of concrete values as well as names that have not been given values. By allowing inputs supplied as symbolic values, a symbolic executor can construct a relation between inputs and outputs along any execution path.  
To understand the general concept of symbolic execution, refer to Figure 3. If the symbolic value \"A\" is inputted to parameter \"a\" while the function named \"Test\" is under execution, it may be said that the function is being symbolically executed. When the code is being executed, the two \"If\" statements do not have control over program flow because \"A\" may assume different values depending on the context. The trick is to construct a logical expression that captures the relation between the $res value and the input.  
Figure 2: Example of static single assignment (SSA) representation and \(\phi\) function. (**a**) Variable renaming. (**b**) A code corresponding to the \(\phi\) function usage and a simplified graph excerpt.  
This is a powerful program description that discloses all of the important factors in an input to the PHP example program as shown in Figure 2(a). It can be understood as a specification of path constraint and the exhibited behavior for each feasible program path. A path constraint indicates the condition for input, in this case, A, to meet so that the execution will go down a particular path. For example, in Figure 2(b), the path goes through the false branches of both if statements have a path constraint of (A \(\geq\) 0 \(\wedge\) A \(\leq\) 10), and the exhibited behavior is given by \(\mathsf{Sres}\) = 0. The path constraint has an assignment (\(\mathsf{Sres}\) = 0, X = 0) under which the constraint is evaluated as \"True\", which makes this path feasible. Meanwhile, the path constraint for the path goes through the true branches of both if statements are infeasible because it requires (X < 0 \(\wedge\) X > 10), which is unsatisfiable.  
A typical symbolic execution handles each path separately in a symbolic state [22]. It is essentially a container of a path constraint and records the program behaviors that symbolic execution propagates, such as the state towards the end of each path, during which symbolic execution identifies feasible and infeasible paths by asking a constraint solver. Constraint solvers are employed to determine the reason specific to symbolic expressions automatically. Constraint solving is a technique that determines a set of values for the variables that satisfy an expression subject to several constraints concerning the variables. In our example in Figure 2(c), four different paths can be observed, three of which are feasible. Symbolic execution finds a conflict in the first path constraint (P1), where the constraint solver returns unsatisfiable for this path because it does not represent a program behavior that can happen. If constraint solving returns a satisfying value assignment for a given constraint instead, then the path is feasible, and we can use the found values as test inputs to re-exhibit the associated program behavior.