Symbolic Execution Of Complex Programs Driven By Black-box Abstraction

With the rapid development of modern information society,the software has en-tered every aspect of people's lives.At the same time,in order to guarantee software quality,the importance of fully testing software becomes more and more prominent.Symbolic execution is one of the technologies widely used in the field of software au-tomation testing.The technique uses symbolic variables instead of concrete values as the execution inputs.In the process of program path analysis,path constraints gener-ated by branch statements are collected continuously,and then the underlying solver is called to solve the collected path constraints to generate test cases that trigger the corresponding code paths.However,in the face of complex real-world programs,symbolic execution still has many challenges.On the one hand,the performance of the underlying constraint solver limits the ability of handling complex path constraints.On the other hand,when a program contains complex path structures,such as function calls or loops,symbolic execution will fall into the search for an infinite number of paths.These all have greatly affected the application of symbolic execution techniques on complex programs.In order to solve the above problems,on the basis of the previous machine-learning-based symbolic execution framework,this paper designs a new symbolic execution framework system based on black-box abstraction.The framework system can not only handle simple path constraints but also encode complex code fragments such as function calls and loop structures into black-box path constraints.Then,the underlying machine-learning-based constraint solver performs sampling and verification,thereby improving the ability of the symbolic execution to test complex codes.The main contributions of this paper are as follows:· Symbolic Execution of Complex Codes with Function Calls Based on Black-box Abstraction:To improve support for complex codes,this paper proposes a black-box execution mechanism based on machine learning.Under this mecha-nism,the path of the specified function call is encoded as a black-box function constraint.When solving the path constraint including the black-box function,the symbolic execution framework performs black-box execution on the function,and the obtained return value is fed back to the underlying machine-learning-based con-straint solving module for verification learning.With the help of the black-box exe-cution mechanism,the symbolic execution framework skips the expansion analysis of the specified function call,puts the resources into the test analysis of the main program,and better supports the test coverage of the real program containing a large number of function calls.· Symbolic Execution of Complex Codes with Loops Based on Black-box Ab-straction:To further reduce the overhead of symbolic execution on complex paths such as processing loops,this paper proposes a method for equivalent black-box function replacement for complex code segments and extends the function of black-box symbolic execution based on this method.Through static analysis of complex code structures such as loop statements,complex code fragments are replaced with equivalent black-box function calls.In the later symbolic execution process,these black-box functions are designated for black-box execution,which reduces the bur-den of processing internal loop statements.· Complex Code Test Generation System Based on Black-box Abstraction:In order to evaluate the effect of symbolic execution with black-box abstraction,this paper designs a new code test generation system,MLB-BS,for Java language,and compares it with the traditional symbolic execution test tool systems through a se-ries of experiments.The experiment data shows that MLB-BS is superior to other tools in test coverage performance,especially in large-scale program systems with complex code structures.