HAMPI: A Solver for Word Equations over Strings, Regular Expressions, and Context-Free Grammars

Many automatic testing, analysis, and verification techniques for programs can be effectively reduced to a constraint-generation phase followed by a constraint-solving phase. This separation of concerns often leads to more effective and maintainable software reliability tools. The increasing efficiency of off-the-shelf constraint solvers makes this approach even more compelling. However, there are few effective and sufficiently expressive off-the-shelf solvers for string constraints generated by analysis of string-manipulating programs, so researchers end up implementing their own ad-hoc solvers. To fulfill this need, we designed and implemented HAMPI, a solver for string constraints over bounded string variables. Users of HAMPI specify constraints using regular expressions, context-free grammars, equality between string terms, and typical string operations such as concatenation and substring extraction. HAMPI then finds a string that satisfies all the constraints or reports that the constraints are unsatisfiable. We demonstrate HAMPI's expressiveness and efficiency by applying it to program analysis and automated testing. We used HAMPI in static and dynamic analyses for finding SQL injection vulnerabilities in Web applications with hundreds of thousands of lines of code. We also used HAMPI in the context of automated bug finding in C programs using dynamic systematic testing (also known as concolic testing). We then compared HAMPI with another string solver, CFGAnalyzer, and show that HAMPI is several times faster. HAMPI'S source code, documentation, and experimental data are available at http://people.csail.mit.edu/akiezun/hampi(1).