A Generic Information Extraction System for String Constraints

TL;DR

This paper introduces SMTQUERY, a Python-based tool for analyzing string constraint benchmarks in SMT-LIB format, aiming to improve understanding and processing of real-world string solving instances.

Contribution

The paper presents SMTQUERY, a novel analysis tool that enhances the examination of string constraint benchmarks, facilitating better solver development and benchmark management.

Findings

SMTQUERY provides detailed analysis of string benchmarks.

The tool supports efficient data extraction and visualization.

It aids in identifying patterns and challenges in string solving instances.

Abstract

String constraint solving, and the underlying theory of word equations, are highly interesting research topics both for practitioners and theoreticians working in the wide area of satisfiability modulo theories. As string constraint solving algorithms, a.k.a. string solvers, gained a more prominent role in the formal analysis of string-heavy programs, especially in connection to symbolic code execution and security protocol verification, we can witness an ever-growing number of benchmarks collecting string solving instances from real-world applications as well as an ever-growing need for more efficient and reliable solvers, especially for the aforementioned real-world instances. Thus, it seems that the string solving area (and the developers, theoreticians, and end-users active in it) could greatly benefit from a better understanding and processing of the existing string solving benchmarks. In this context, we propose SMTQUERY: an SMT-LIB benchmark analysis tool for string constraints. SMTQUERY is implemented in Python 3, and offers a collection of analysis and information extraction tools for a comprehensive data base of string benchmarks (presented in SMT-LIB format), based on an SQL-centred language called QLANG.