Generate valid UUID, JSON and JSONB values

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,
         )
     }

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.

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")
+    }
+}