SMT solver fault positioning method based on search

Abstract

The invention belongs to the field of software testing, and particularly relates to an SMT solver fault positioning method based on search. Firstly, a genetic algorithm is used for searching a variation rule list to perform variation on a test program to obtain a group of variation test programs which do not trigger faults; then, ranking the suspicious files by comparing the execution paths of the test programs which trigger the faults with the execution paths of the variation test programs which do not trigger the faults by using a frequency spectrum-based method, so as to obtain a file ranking list; according to the method, the fault of the SMT solver can be positioned and analyzed, so that a developer can be helped to quickly find the fault reason of the SMT solver, the debugging work is facilitated, and the quality of the solver is improved.

Description

technical field [0001] The invention belongs to the field of software testing, and relates to a technology for locating an SMT solver, in particular to a search-based SMT solver fault location method. Background technique [0002] SMT (The Satisfiability Modulo Theories) solver is a tool for verifying whether first-order logic formulas can be satisfied. It has been widely used in the fields of formal methods, programming languages, software engineering, and computer security. However, as a software, SMT solvers inevitably have bugs, such as the solver incorrectly reporting satisfiable programs as unsatisfiable, which makes it difficult for other tools that rely on SMT solvers to output reliable results. According to statistics, the median time for developers to fix a Z3 fault is 22 hours, of which about 2,000 faults cannot be fixed within two days; the median time for developers to fix a CVC5 fault is 6.3 days, of which about 800 A fault cannot be fixed within two days. Th...

AI Technical Summary

Problems solved by technology

Although the existing invention patents have proposed some fault location methods, these methods still have problems such as difficulty in adapting to the fault location problem of the SMT solver

For example, a spectrum-based software fault location method (patent number: CN201910205209.4) obtains the program spectrum information of each statement by executing the test case, and then selects several existing fault location sub-technologies to calculate the program spectrum of each statement The information generates multiple sentence suspicious value rankings, and finally generates a comprehensive suspicious value ranking through FA algorithm calculation; but the SMT solver is a large software system, making it very complicated and time-consuming to perform static or dynamic analysis on it

Compiler defect location method based on reinforcement learning (patent number: CN202010880640.1) uses structural variation and reinforcement learning to generate a successfully compiled mutated program, thereby locating the compiler by comparing the difference in the execution path of the mutated program and the fault trigger program Fault; but the language used by the SMT solver is a declarative grammar, and there is no structure such as control flow

Images