Escape non-ASCII characters in SMT-LIB string literals

core-extra/solver/src/main/java/org/evomaster/solver/smtlib/SMTResultParser.java

@@ -170,6 +170,24 @@ private static List<String> structTokens(String text, int start) {
         return null;
     }
 
+    private static final Pattern UNICODE_ESCAPE = Pattern.compile("\\\\u\\{([0-9a-fA-F]{1,6})\\}");
+
+    /**
+     * Undoes the escapes of an SMT-LIB string literal: a double quote written as two, and a character
+     * written as \\u{X}, with X its code point in hex. Z3 writes every character outside printable
+     * ASCII that way, so without decoding, a value such as "ORDIN\\u{c6}R" was used as is.
+     */
+    static String unescapeString(String text) {
+        String unquoted = text.replace("\"\"", "\"");
+        Matcher m = UNICODE_ESCAPE.matcher(unquoted);
+        StringBuilder sb = new StringBuilder();
+        while (m.find()) {
+            m.appendReplacement(sb, Matcher.quoteReplacement(new String(Character.toChars(Integer.parseInt(m.group(1), 16)))));
+        }
+        m.appendTail(sb);
+        return sb.toString();
+    }
+
     /**
      * Parses a value string into an appropriate SMTLibValue object.
      *
@@ -186,8 +204,8 @@ private static SMTLibValue parseValue(String value) {
             value = value.substring(0, value.length() - 1).trim(); // Remove parentheses
         }
         if (value.startsWith("\"") && value.endsWith("\"")) {
-            // If it is a string: remove the quotes and undo the SMT-LIB escape of " as ""
-            return new StringValue(value.substring(1, value.length() - 1).replace("\"\"", "\""));
+            // If it is a string: remove the quotes and undo the SMT-LIB escapes
+            return new StringValue(unescapeString(value.substring(1, value.length() - 1)));
         }
         try {
             if (value.matches("- \\d+")) {

core-extra/solver/src/test/java/org/evomaster/solver/smtlib/SMTResultParserTest.java

@@ -244,4 +244,14 @@ public void testParseComposedTypeWithEscapedQuoteInString() {
         StructValue t1 = (StructValue) result.get("t__1");
         assertEquals("say \"hi\" O'Brien", ((StringValue) t1.getField("TXT")).getValue());
     }
+
+    @Test
+    public void testParseComposedTypeWithUnicodeEscapes() {
+        // Z3 writes every character outside printable ASCII as a unicode escape
+        String response = "sat\n((t__1 (id-txt 0 \"ORDIN\\u{c6}R E\\u{d8}S \\u{1f600} a\\u{5c}b\")))";
+        Z3Solution result = SMTResultParser.parseZ3Response(response);
+
+        StructValue t1 = (StructValue) result.get("t__1");
+        assertEquals("ORDIN\u00c6R E\u00d8S \ud83d\ude00 a\\b", ((StringValue) t1.getField("TXT")).getValue());
+    }
 }

core/src/main/kotlin/org/evomaster/core/database/sql/solver/SMTConditionVisitor.kt

@@ -301,13 +301,26 @@ class SMTConditionVisitor(
      * is kept. A double quote is written as "", the SMT-LIB escape; left as is, it would end the
      * literal early and Z3 would reject the whole formula. A value wrapped in double quotes, as in
      * '"x"', is still read as x.
+     *
+     * A character outside printable ASCII is written as the SMT-LIB escape \u{X}, with X its code
+     * point in hex. Z3 reads a string literal byte by byte, so written as is, the UTF-8 encoding of
+     * 'ORDINÆR' became a different, longer string, and a row satisfying it broke the very CHECK it
+     * came from. A backslash is escaped too, since followed by "u{" it would start an escape.
      */
     private fun stringLiteral(literal: SqlStringLiteralValue): String {
         var value = literal.stringValue
         if (value.length >= 2 && value.startsWith("\"") && value.endsWith("\"")) {
             value = value.substring(1, value.length - 1)
         }
-        return "\"${value.replace("\"", "\"\"")}\""
+        val escaped = StringBuilder()
+        value.codePoints().forEach { cp ->
+            when {
+                cp == '"'.code -> escaped.append("\"\"")
+                cp == '\\'.code || cp < 0x20 || cp > 0x7E -> escaped.append("\\u{").append(Integer.toHexString(cp)).append('}')
+                else -> escaped.appendCodePoint(cp)
+            }
+        }
+        return "\"$escaped\""
     }
 
     private fun asLiteral(expression: SqlCondition?): String {

core/src/test/kotlin/org/evomaster/core/database/sql/solver/StringLiteralTranslationTest.kt

@@ -48,4 +48,11 @@ class StringLiteralTranslationTest {
         assertTrue(smt.contains("\"O'Brien\"")) { "expected the apostrophe to be kept in:\n$smt" }
         assertTrue(smt.contains("\"say \"\"hi\"\"\"")) { "expected the escaped literal in:\n$smt" }
     }
+
+    @Test
+    fun `a character outside printable ASCII is written as a unicode escape`() {
+        val smt = generate("SELECT ID FROM ACCOUNT WHERE NAME = 'ORDINÆR \\ 😀'")
+
+        assertTrue(smt.contains("\"ORDIN\\u{c6}R \\u{5c} \\u{1f600}\"")) { "expected the escaped literal in:\n$smt" }
+    }
 }

core/src/test/kotlin/org/evomaster/core/database/sql/solver/service/NonAsciiLiteralSolvingTest.kt

@@ -0,0 +1,86 @@
+package org.evomaster.core.database.sql.solver.service
+
+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.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.params.ParameterizedTest
+import org.junit.jupiter.params.provider.ValueSource
+import java.sql.Connection
+import java.sql.DriverManager
+
+/**
+ * A string literal with characters outside ASCII must reach the database unchanged.
+ *
+ * Z3 reads a string literal byte by byte and writes non-ASCII characters back as unicode escapes.
+ * Written as raw UTF-8 and read back without decoding, 'ORDINÆR' came back as "ORDIN\u{c3}\u{86}R":
+ * a row generated to satisfy an enumeration CHECK broke that same CHECK, and the database rejected
+ * its INSERT. Enumerations with such values are common, e.g. in a Norwegian or Spanish schema.
+ */
+class NonAsciiLiteralSolvingTest {
+
+    companion object {
+        private lateinit var solver: SMTLibZ3DbConstraintSolver
+        private lateinit var connection: Connection
+        private lateinit var schemaDto: DbInfoDto
+
+        @JvmStatic
+        @BeforeAll
+        fun setup() {
+            connection = DriverManager.getConnection("jdbc:h2:mem:non_ascii_literal_test", "sa", "")
+            SqlScriptRunner.execCommand(
+                connection,
+                "CREATE TABLE sak(id bigint primary key, kategori varchar(20), " +
+                    "CHECK (kategori IN ('ORDINÆR', 'EØS')));\n"
+            )
+            schemaDto = DbInfoExtractor.extract(connection)
+            /*
+                H2 2.x reports the constraint with unicode-escaped literals, IN(U&'ORDIN\00c6R', ...),
+                which the CHECK parser does not read. PostgreSQL and H2 1.4 report the characters as
+                they are, so the constraint is given in that form. H2 still enforces the real one on
+                insertion.
+             */
+            schemaDto.tables.single().tableCheckExpressions.single().sqlCheckExpression =
+                "(kategori IN ('ORDINÆR', 'EØS'))"
+            solver = SMTLibZ3DbConstraintSolver()
+            solver.initializeExecutor()
+        }
+
+        @JvmStatic
+        @AfterAll
+        fun tearDown() {
+            connection.close()
+            if (this::solver.isInitialized) {
+                solver.close()
+            }
+        }
+    }
+
+    @BeforeEach
+    fun clean() {
+        SqlScriptRunner.execCommand(connection, "DELETE FROM sak;\n")
+    }
+
+    @ParameterizedTest
+    @ValueSource(strings = [
+        // the value only comes from the CHECK
+        "SELECT * FROM sak WHERE id = 1",
+        // the value comes from the query too
+        "SELECT * FROM sak WHERE kategori = 'EØS'"
+    ])
+    fun generatedRowsSatisfyTheCheckAndTheQuery(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(listOf(true), results.executionResults, "The generated row should satisfy the CHECK")
+
+        val result = SqlScriptRunner.execCommand(connection, query)
+        assertFalse(result.isEmpty(), "Inserted rows should satisfy the original query")
+    }
+}