Path Feasibility Detection Using Symbolic Execution And Data Mining

Static analysis is the analysis that makes verification of properties of computerprograms without actually executing them. Based on control flow and data flow analysis,it can be used in the area of code optimization and bug finding. Static analysis is the basisof many software engineering methods and tools.A common assumption made in static analysis is that every program path isexecutable. But it is actually too conservative in many cases. Report on NAG FortranLibrary by D.Hedley shows that almost12.5%of all program paths are infreasible. That is,for all valid inputs, there are12.5%of the program paths never being executed. Theexistence of infeasible program paths has become an obstacle in applying static analysis tosoftware engineering activities.Without the knowledge of the infeasible path problem, data flow information canonly be treated in a rather conservative way, which makes further works much harder andmore inefficient. In path-oriented test case generation, many futile efforts is put intoinfeasible paths, and in bug finding, the existence of infeasible path leads to a lot of falsepositives.A hybrid approach, combining symbolic execution and data mining techniques isproposed in this paper for detecting infeasible path. Traditional symbolic executionalgorithm is modified to be more efficient so that it is more suitable for the problem ofpath feasibility. Meanwhile, Association Rules Mining is used to compensate the lack ofaccuracy in the modified symbolic execution algorithm. The balance of efficiency andaccuracy can be adjusted to programs of different scales and different kinds beforerunning.The algorithm is implemented using JavaPathFinder (a software model checker),Weka (a data mining toolkit) and DiSL (a bytecode instrumentation tool). A typical java program is used to demonstrate the feasibility of the algorithm.