diff --git a/core/src/main/kotlin/org/evomaster/core/database/sql/solver/SmtLibGenerator.kt b/core/src/main/kotlin/org/evomaster/core/database/sql/solver/SmtLibGenerator.kt index 6aadfd7dbf..b414816018 100644 --- a/core/src/main/kotlin/org/evomaster/core/database/sql/solver/SmtLibGenerator.kt +++ b/core/src/main/kotlin/org/evomaster/core/database/sql/solver/SmtLibGenerator.kt @@ -82,6 +82,14 @@ class SmtLibGenerator( const val BOOLEAN_TYPE = "BOOLEAN" const val TIMESTAMP_TYPE = "TIMESTAMP" + /** + * Encoded as SMT Strings with no constraint on their form, so the value Z3 assigns need not be + * a valid UUID or JSON document; SMTLibZ3DbConstraintSolver turns it into one. + */ + const val UUID_TYPE = "UUID" + const val JSON_TYPE = "JSON" + const val JSONB_TYPE = "JSONB" + /** * Spellings of [BOOLEAN_TYPE] that [TYPE_MAP] treats as the same type (PostgreSQL reports a * boolean column as "bool"). Every check for a boolean column must use this set: a column @@ -150,8 +158,9 @@ class SmtLibGenerator( "CHARACTER LARGE OBJECT" to SMT_STRING, BOOLEAN_TYPE to SMT_STRING, "BOOL" to SMT_STRING, - "UUID" to SMT_STRING, - "JSONB" to SMT_STRING, + UUID_TYPE to SMT_STRING, + JSON_TYPE to SMT_STRING, + JSONB_TYPE to SMT_STRING, "BYTEA" to SMT_STRING, ) } diff --git a/core/src/main/kotlin/org/evomaster/core/database/sql/solver/service/SMTLibZ3DbConstraintSolver.kt b/core/src/main/kotlin/org/evomaster/core/database/sql/solver/service/SMTLibZ3DbConstraintSolver.kt index da2fe34947..156e13ff3a 100644 --- a/core/src/main/kotlin/org/evomaster/core/database/sql/solver/service/SMTLibZ3DbConstraintSolver.kt +++ b/core/src/main/kotlin/org/evomaster/core/database/sql/solver/service/SMTLibZ3DbConstraintSolver.kt @@ -1,5 +1,8 @@ package org.evomaster.core.database.sql.solver.service +import com.fasterxml.jackson.core.JsonProcessingException +import com.fasterxml.jackson.databind.DeserializationFeature +import com.fasterxml.jackson.databind.ObjectMapper import com.google.inject.Inject import net.sf.jsqlparser.JSQLParserException @@ -115,6 +118,11 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { // round-trips: what is written here is read back to the same instant. private const val TIMESTAMP_FORMAT = "yyyy-MM-dd HH:mm:ss" + private val UUID_PATTERN = Regex("[0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[0-9a-fA-F]{4}-[0-9a-fA-F]{4}-[0-9a-fA-F]{12}") + + /** Rejects trailing content, so that e.g. "1 2" is not taken for the JSON document 1. */ + private val JSON_MAPPER = ObjectMapper().enable(DeserializationFeature.FAIL_ON_TRAILING_TOKENS) + /** * Spellings [SmtLibGenerator.TYPE_MAP] already treats as the same type. Taken from the * generator rather than repeated, so the domain constraint and the gene reconstruction cannot @@ -487,7 +495,7 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { if (hasColumnType(schemaDto, table, dbColumnName, SmtLibGenerator.BOOLEAN_TYPE)) { BooleanGene(dbColumnName, toBoolean(columnValue.value)) } else { - StringGene(dbColumnName, columnValue.value) + StringGene(dbColumnName, validTextValue(schemaDto, table, dbColumnName, columnValue.value)) } } is LongValue -> { @@ -590,6 +598,35 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { return typeMatches(col.type, expectedType) } + /** + * Makes the value Z3 assigned to a UUID, JSON or JSONB column one the database accepts. + * + * They are encoded as SMT Strings with no constraint on their form, so unless the query pins the + * value, Z3 picks something like "" and the INSERT of the whole row is rejected. A value that is + * already valid -- e.g. one copied from the query -- is kept. Any other is mapped + * deterministically: equal strings give equal values and different strings different ones, so + * the equalities and distinctions the formula imposes (foreign keys, unique and primary keys) + * still hold. Constraining the form inside the formula instead would need Z3's regular + * expressions, which make solving noticeably more expensive. + */ + private fun validTextValue(schemaDto: DbInfoDto, table: Table, columnName: String, value: String): String = + when { + hasColumnType(schemaDto, table, columnName, SmtLibGenerator.UUID_TYPE) && !UUID_PATTERN.matches(value) -> + UUID.nameUUIDFromBytes(value.toByteArray(StandardCharsets.UTF_8)).toString() + (hasColumnType(schemaDto, table, columnName, SmtLibGenerator.JSON_TYPE) || + hasColumnType(schemaDto, table, columnName, SmtLibGenerator.JSONB_TYPE)) && !isJson(value) -> + JSON_MAPPER.writeValueAsString(value) // the value as a JSON string + else -> value + } + + private fun isJson(value: String): Boolean = + try { + // readTree returns a MissingNode, rather than failing, on blank input + !JSON_MAPPER.readTree(value).isMissingNode + } catch (e: JsonProcessingException) { + false + } + /** * Whether a column's declared type is the expected one, accounting for spellings that * [SmtLibGenerator.TYPE_MAP] already treats as equivalent. diff --git a/core/src/test/kotlin/org/evomaster/core/database/sql/solver/service/UuidJsonColumnSolvingTest.kt b/core/src/test/kotlin/org/evomaster/core/database/sql/solver/service/UuidJsonColumnSolvingTest.kt new file mode 100644 index 0000000000..d4c0e78a66 --- /dev/null +++ b/core/src/test/kotlin/org/evomaster/core/database/sql/solver/service/UuidJsonColumnSolvingTest.kt @@ -0,0 +1,105 @@ +package org.evomaster.core.database.sql.solver.service + +import com.fasterxml.jackson.databind.DeserializationFeature +import com.fasterxml.jackson.databind.ObjectMapper +import org.evomaster.client.java.controller.api.dto.database.schema.DbInfoDto +import org.evomaster.client.java.sql.DbInfoExtractor +import org.evomaster.client.java.sql.SqlScriptRunner +import org.evomaster.core.database.sql.SqlActionTransformer +import org.evomaster.core.search.gene.string.StringGene +import org.junit.jupiter.api.AfterAll +import org.junit.jupiter.api.Assertions.assertEquals +import org.junit.jupiter.api.Assertions.assertFalse +import org.junit.jupiter.api.BeforeAll +import org.junit.jupiter.api.BeforeEach +import org.junit.jupiter.api.Test +import org.junit.jupiter.params.ParameterizedTest +import org.junit.jupiter.params.provider.ValueSource +import java.sql.Connection +import java.sql.DriverManager + +/** + * UUID, JSON and JSONB columns are encoded as SMT Strings with no constraint on their form. Unless the query + * pins the value, Z3 picks something like "", and the INSERT of the whole row used to be rejected. + * The failure was silent: SqlScriptRunner.execInsert logs a failed insertion and carries on. + */ +class UuidJsonColumnSolvingTest { + + companion object { + private lateinit var solver: SMTLibZ3DbConstraintSolver + private lateinit var connection: Connection + private lateinit var schemaDto: DbInfoDto + + /** + * JSONB is PostgreSQL's spelling, which H2 does not have, so a varchar column is reported as + * JSONB on a second extraction of the schema. It is only checked for the value generated. + */ + private lateinit var jsonbSchemaDto: DbInfoDto + + @JvmStatic + @BeforeAll + fun setup() { + connection = DriverManager.getConnection("jdbc:h2:mem:uuid_json_column_test", "sa", "") + SqlScriptRunner.execCommand( + connection, + "CREATE TABLE ev(id bigint primary key, u uuid);\n" + + "CREATE TABLE parent(id uuid primary key);\n" + + "CREATE TABLE child(id bigint primary key, parent_id uuid REFERENCES parent(id));\n" + + "CREATE TABLE doc(id bigint primary key, body varchar(255));\n" + + "CREATE TABLE jdoc(id bigint primary key, content json);\n" + ) + schemaDto = DbInfoExtractor.extract(connection) + jsonbSchemaDto = DbInfoExtractor.extract(connection) + jsonbSchemaDto.tables.single { it.id.name.equals("DOC", ignoreCase = true) } + .columns.single { it.name.equals("BODY", ignoreCase = true) } + .type = "jsonb" + solver = SMTLibZ3DbConstraintSolver() + solver.initializeExecutor() + } + + @JvmStatic + @AfterAll + fun tearDown() { + connection.close() + if (this::solver.isInitialized) { + solver.close() + } + } + } + + @BeforeEach + fun clean() { + SqlScriptRunner.execCommand(connection, "DELETE FROM child; DELETE FROM parent; DELETE FROM ev; DELETE FROM jdoc;\n") + } + + @ParameterizedTest + @ValueSource(strings = [ + // the value is free: Z3 picks a string that is not a UUID + "SELECT * FROM ev WHERE id = 1", + // the value is pinned by the query, and must be kept + "SELECT * FROM ev WHERE u = '123e4567-e89b-12d3-a456-426614174000'", + // a foreign key between UUID columns: the mapped values must still be equal + "SELECT * FROM child WHERE id = 1", + // a JSON column, which H2 has as well: the value is free + "SELECT * FROM jdoc WHERE id = 1" + ]) + fun generatedRowsAreInsertedAndSatisfyTheQuery(query: String) { + val actions = solver.solve(schemaDto, query, 1) + assertFalse(actions.isEmpty(), "Solver should return actions for a satisfiable query") + + val results = SqlScriptRunner.execInsert(connection, SqlActionTransformer.transform(actions).insertions) + assertEquals(actions.map { true }, results.executionResults, "Every generated row should be inserted") + + val result = SqlScriptRunner.execCommand(connection, query) + assertFalse(result.isEmpty(), "Inserted rows should satisfy the original query") + } + + @Test + fun jsonbValueIsAJsonDocument() { + val actions = solver.solve(jsonbSchemaDto, "SELECT * FROM doc WHERE id = 1", 1) + + val body = actions.single().seeTopGenes().first { it.name.equals("BODY", ignoreCase = true) } as StringGene + val mapper = ObjectMapper().enable(DeserializationFeature.FAIL_ON_TRAILING_TOKENS) + assertFalse(mapper.readTree(body.value).isMissingNode, "'${body.value}' is not a JSON document") + } +}