A Direct Symbolic Execution of SQL Code for Testing of Data-Oriented Applications

TL;DR

This paper introduces a direct symbolic execution method for SQL code within applications, enabling automatic test data generation that includes valid database content, improving testing of data-oriented software.

Contribution

It presents a novel symbolic execution approach for database manipulation code integrated with traditional program analysis, using relational constraints and SMT solvers.

Findings

The approach generates meaningful test data including valid database content.

The method is scalable and more efficient with Z3 solver compared to Alloy.

Experimental results demonstrate effective test data generation in reasonable time.

Abstract

Symbolic execution is a technique which enables automatically generating test inputs (and outputs) exercising a set of execution paths within a program to be tested. If the paths cover a sufficient part of the code under test, the test data offer a representative view of the program's actual behaviour, which notably enables detecting errors and correcting faults. Relational databases are ubiquitous in software, but symbolic execution of pieces of code that manipulate them remains a non-trivial problem, particularly because of the complex structure of such databases and the complex behaviour of SQL statements. In this work, we define a direct symbolic execution for database manipulation code and integrate it with a more traditional symbolic execution of normal program code. The database tables are represented by relational symbols and the SQL statements by relational constraints over these symbols and the symbols representing the normal variables of the program. An algorithm based on these principles is presented for the symbolic execution of Java methods that implement business use cases by reading and writing in a relational database, the latter subject to data integrity constraints. The algorithm is integrated in a test generation tool and experimented over sample code. The target language for the constraints produced by the tool is the SMT-Lib standard and the used solver is Microsoft Z3. The results show that the proposed approach enables generating meaningful test data, including valid database content, in reasonable time. In particular, the Z3 solver is shown to be more scalable than the Alloy solver, used in our previous work, for solving relational constraints.