From d1b7e71bd99d7b657665d5ee052a02a3a3178b47 Mon Sep 17 00:00:00 2001 From: Agustina Aldasoro Date: Wed, 7 Oct 2026 15:01:26 +0200 Subject: [PATCH 1/2] Generate valid UUID and JSONB values UUID and JSONB columns are unconstrained SMT strings, so unless the query pinned the value Z3 picked one such as "", and the database rejected the INSERT of the whole row. A value that is not a valid UUID or JSON document is now mapped deterministically to one, which keeps the equalities imposed by keys and foreign keys. --- .../database/sql/solver/SmtLibGenerator.kt | 11 +- .../service/SMTLibZ3DbConstraintSolver.kt | 38 ++++++- .../service/UuidJsonColumnSolvingTest.kt | 102 ++++++++++++++++++ 3 files changed, 148 insertions(+), 3 deletions(-) create mode 100644 core/src/test/kotlin/org/evomaster/core/database/sql/solver/service/UuidJsonColumnSolvingTest.kt 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 cc8880de3f..8e792490b9 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,13 @@ 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 JSONB_TYPE = "JSONB" + /** * The canonical string values a BOOLEAN column may take (BOOLEAN is encoded as an SMT String). * These are generation constraints, so Z3 is forced to pick one of them; only the two canonical @@ -143,8 +150,8 @@ 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, + 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 2159ba2799..edd2294dba 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 @@ -107,6 +110,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. The canonical one is * taken from the generator rather than repeated, so the two cannot drift apart; consolidating @@ -383,7 +391,7 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { gene = 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 -> { @@ -505,6 +513,34 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { return typeMatches(col.type, expectedType) } + /** + * Makes the value Z3 assigned to a UUID or JSONB column one the database accepts. + * + * Both 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.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..3cdfcab296 --- /dev/null +++ b/core/src/test/kotlin/org/evomaster/core/database/sql/solver/service/UuidJsonColumnSolvingTest.kt @@ -0,0 +1,102 @@ +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 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" + ) + 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;\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" + ]) + 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") + } +} From 71820c69d9ef95a8331519dc3131bc14c478ae79 Mon Sep 17 00:00:00 2001 From: Agustina Aldasoro Date: Thu, 8 Oct 2026 19:44:40 +0200 Subject: [PATCH 2/2] Map JSON columns like JSONB --- .../core/database/sql/solver/SmtLibGenerator.kt | 2 ++ .../sql/solver/service/SMTLibZ3DbConstraintSolver.kt | 7 ++++--- .../sql/solver/service/UuidJsonColumnSolvingTest.kt | 11 +++++++---- 3 files changed, 13 insertions(+), 7 deletions(-) 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 6149d1e26a..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 @@ -87,6 +87,7 @@ class SmtLibGenerator( * 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" /** @@ -158,6 +159,7 @@ class SmtLibGenerator( BOOLEAN_TYPE to SMT_STRING, "BOOL" 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 ee93deb13c..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 @@ -599,9 +599,9 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { } /** - * Makes the value Z3 assigned to a UUID or JSONB column one the database accepts. + * Makes the value Z3 assigned to a UUID, JSON or JSONB column one the database accepts. * - * Both are encoded as SMT Strings with no constraint on their form, so unless the query pins the + * 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 @@ -613,7 +613,8 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { 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.JSONB_TYPE) && !isJson(value) -> + (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 } 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 index 3cdfcab296..d4c0e78a66 100644 --- 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 @@ -19,7 +19,7 @@ import java.sql.Connection import java.sql.DriverManager /** - * UUID and JSONB columns are encoded as SMT Strings with no constraint on their form. Unless the query + * 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. */ @@ -45,7 +45,8 @@ class UuidJsonColumnSolvingTest { "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 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) @@ -68,7 +69,7 @@ class UuidJsonColumnSolvingTest { @BeforeEach fun clean() { - SqlScriptRunner.execCommand(connection, "DELETE FROM child; DELETE FROM parent; DELETE FROM ev;\n") + SqlScriptRunner.execCommand(connection, "DELETE FROM child; DELETE FROM parent; DELETE FROM ev; DELETE FROM jdoc;\n") } @ParameterizedTest @@ -78,7 +79,9 @@ class UuidJsonColumnSolvingTest { // 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" + "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)