Symbolic Execution Framework Of Complex Software Program Based On Machine Learning Constraint Solving

Test case generation is one of the most important research topic in software test-ing.Unlike other test case generation technologies,test case generation by symbolic execution executes programs with symbolic inputs rather than concrete inputs and maintains the path conditions during program traversing.It feeds the path conditions to the underlying constraint solver to generate test cases which trigger the corresponding program path condition.This technology has been applied to a number of testing tools,such as jCUTE,KLEE and SPF and so on.However,test case generation by symbolic execution still faces a lot of challenges when it is applied to real programs.One of the main challenges is that the underlying constraint solver can not provide effective support for complex path constraints in real programs.There are two main reasons for this problem:firstly,there are a lot of com-plex numerical calculation in real programs including nonlinear numerical calculation and the calculation of common mathematical functions.Such constraints are difficult for the existing constraint solvers;secondly,there are a large number of function calls in real programs.The existing constraint solver usually only supports constraints in the form of pure mathematical expression.In the case that users can not know the details of functions,the constraint solver is hard to solve this type of path constraint that contains a function call.In order to overcome the limitations discussed above,the main contributions of this paper are as follows:·We introduce a new symbolic execution framework,MLBSE,which is driven by machine learning based constraint solving.The main difference between MLBSE and traditional symbolic execution tools is the underlying constraint solving.To solve the complicated path conditions,MLBSE transforms the fea-sibility problem of the path conditions into an optimization problem through the dissatisfaction function,then obtains feasible solutions with RACOS.By tak-ing advantage of this machine learning based solving,MLBSE can support real programs including complex numerical calculations and function calls better.·On the basis of MLBSE,we provide 3 extensions to enhance the symbolic exe-cution function of MLBSE.MLBSE can deal with the real programs including function calls more efficiently with black-box execution mode.When MLBSE fails to solve a path condition,it reports the estimated confidence of satisfiability to guide users judge whether or not invest more resources to this path condition.In addition to this,MLBSE provides an additional strategy called ECS guided search strategy.MLBSE can invest more resources automatically for those un-solved path conditions with high estimated confidence of satisfiability.Then the effectiveness of symbolic execution can be improved without affecting the over-all efficiency..We implement MLB on the basis of a Java symbolic execution engine,Symbolic PathFinder.Intensive case studies are conducted to generate test cases for 19 real case programs.The experimental results prove that our tool outperforms the other state-of-the-art tools in terms of efficiency,quality,and stability.We also do a series experiments to discuss the extensions of MLB including black-box execution mode,estimated confidence of satisfiability and ECS guided search strategy.The experiments show that the ECS value is reasonable.And the black-box execution mode and ECS guided search strategy can further enhance the symbolic execution of MLB on real programs.