Practical Test Case Reduction for SMT Solvers

Abstract

Automatische Testwerkzeuge erzeugen potenziell große SMT-Testfälle, die Fehler auslösen. Aktuelle Reduzierer sind bei der Reduzierung dieser Testfälle unwirksam, da sie die Semantik der Sprache nicht berücksichtigen, während sie diese reduzieren. Wir entwickelten ein neuartiges Framework für eine effektive und effiziente Programmreduzierung, das speziell für fehlerinduzierende Testfälle im SMT-LIB v2-Format angepasst wurde, um das Testen und Debuggen von SMT-Solvern zu erleichtern. Unser Rahmenwerk unterstützt domänenspezifische Reduzierungsregeln, die die Semantik des Programms nicht verändern sollten. Unsere Evaluierungsergebnisse demonstrieren die Praxistauglichkeit von SMT-Reducer. Im Vergleich zum generischen C/C++ Reduzierer, der auch SMTLIBv2 Programme reduzieren kann, reduziert SMT-Reduser SMT-LIB Programme deutlich schneller.

Automatic testing tools generate potentially large SMT test cases that trigger bugs. Current reducers are ineffective in reducing these test cases since they do not consider the semantics of the language while reducing it. We developed a novel framework for effective and efficient program reduction customized for failure-inducing test cases in SMTLIB v2 format to ease testing and debugging of SMT solvers. Our framework supports domain-specific reduction rules that should not change the semantics of the program. Our evaluation results on SMT programs triggering bugs in SMT solvers demonstrate SMT-Reducer’s practicality for shorter reduction time compared to the state-of-the-art C-Reduce for C/C++.