SMT solver is an important tool in the field of software engineering,which is often used to verify the satisfiability of logic formulas.However,due to the complexity of its implementation,the solver may contain serious errors.Fuzz testing is one of the effective methods to detect vulnerabilities in SMT solvers,but the existing fuzz testing tools for SMT solvers have the following shortcomings: 1)Since the test cases of the SMT solver are oriented to a variety of different theoretical logics,the existing fuzzing tools need to set corresponding grammar rules for each different theoretical logic,resulting in insufficient generality and scalability.2)Existing fuzzing tools need to provide complex specific rules and syntax specifications,which consume a lot of manpower and time resources.The use of deep neural network to automatically learn different types of grammar rules can effectively solve the above problems.So far,this paper is the first time to apply cyclic neural network to fuzz testing of SMT solver.The main research work is as follows:(1)Aiming at the problem that the lexical analyzer of natural language processing can not perform a complete lexical analysis of the test cases based on SMT-LIB language.Combined with the official documents of SMT-LIB language,this paper designs and implements a lexical analyzer for effective word segmentation of this type of test cases.At the same time,improvements are also made to the lexical analyzer to generate starting point recognition,special left bracket marks and other operations required for subsequent neural networks.(2)Aiming at the lack of scalability and versatility of the existing fuzzing tools for SMT solvers,and the time-consuming and labor-intensive problems of providing complex grammar specifications,this paper presents a method of using deep neural network to learn the syntax rules of regression test cases based on different theoretical logic at the same time,so as to improve the versatility of test cases.Based on this method,the prototype tool Deep SMT is implemented and applied to the fuzz test of the SMT solver.A large number of targeted test cases are automatically generated to test the difference of the SMT solver.(3)Aiming at the problem that Deep SMT cannot capture long-distance input dependencies due to the limitations of the cyclic neural network structure,resulting in insufficient pass rate of generated test cases,in this paper,several improved schemes are proposed,such as bi-directional gated cyclic neural network based on attention mechanism,neural network model training method based on Teacher-Foring mechanism and token segmentation of data set.Based on this method,the prototype system tool NNSMT is implemented and applied to the fuzz testing of the mainstream SMT solver,which greatly improves the pass rate of the test case.The method in this paper can deal with SMT test cases with different theoretical logic at the same time,which is simple and time-saving,universal and scalable.At the same time,experiments show that the average pass rates of SMT test programs generated by Deep SMT and NNSMT are more than 65% and 85% respectively,the code coverage of SMT solver is significantly higher than that of the original program,and the efficiency of generating test cases is also higher than the existing methods.In the preliminary study,three serious errors of Z3 solver are found,which reflects the effectiveness of the scheme designed in this paper. |