From 726a69316a0168e3ce72df74d478847394028596 Mon Sep 17 00:00:00 2001 From: Agustina Aldasoro Date: Wed, 7 Oct 2026 17:57:02 +0200 Subject: [PATCH] Escape non-ASCII characters in SMT-LIB string literals and decode them from the Z3 model --- .../solver/smtlib/SMTResultParser.java | 22 ++++- .../solver/smtlib/SMTResultParserTest.java | 10 +++ .../sql/solver/SMTConditionVisitor.kt | 15 +++- .../solver/StringLiteralTranslationTest.kt | 7 ++ .../service/NonAsciiLiteralSolvingTest.kt | 86 +++++++++++++++++++ 5 files changed, 137 insertions(+), 3 deletions(-) create mode 100644 core/src/test/kotlin/org/evomaster/core/database/sql/solver/service/NonAsciiLiteralSolvingTest.kt diff --git a/core-extra/solver/src/main/java/org/evomaster/solver/smtlib/SMTResultParser.java b/core-extra/solver/src/main/java/org/evomaster/solver/smtlib/SMTResultParser.java index 34b9d314dd..e08907a699 100644 --- a/core-extra/solver/src/main/java/org/evomaster/solver/smtlib/SMTResultParser.java +++ b/core-extra/solver/src/main/java/org/evomaster/solver/smtlib/SMTResultParser.java @@ -170,6 +170,24 @@ private static List 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+")) { diff --git a/core-extra/solver/src/test/java/org/evomaster/solver/smtlib/SMTResultParserTest.java b/core-extra/solver/src/test/java/org/evomaster/solver/smtlib/SMTResultParserTest.java index 43a6ca8fcd..a87421c8d3 100644 --- a/core-extra/solver/src/test/java/org/evomaster/solver/smtlib/SMTResultParserTest.java +++ b/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()); + } } diff --git a/core/src/main/kotlin/org/evomaster/core/database/sql/solver/SMTConditionVisitor.kt b/core/src/main/kotlin/org/evomaster/core/database/sql/solver/SMTConditionVisitor.kt index 651d5dab1a..4f71da80b5 100644 --- a/core/src/main/kotlin/org/evomaster/core/database/sql/solver/SMTConditionVisitor.kt +++ b/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 { diff --git a/core/src/test/kotlin/org/evomaster/core/database/sql/solver/StringLiteralTranslationTest.kt b/core/src/test/kotlin/org/evomaster/core/database/sql/solver/StringLiteralTranslationTest.kt index 4b6674a639..064661ed7d 100644 --- a/core/src/test/kotlin/org/evomaster/core/database/sql/solver/StringLiteralTranslationTest.kt +++ b/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" } + } } diff --git a/core/src/test/kotlin/org/evomaster/core/database/sql/solver/service/NonAsciiLiteralSolvingTest.kt b/core/src/test/kotlin/org/evomaster/core/database/sql/solver/service/NonAsciiLiteralSolvingTest.kt new file mode 100644 index 0000000000..fd9ee6c44f --- /dev/null +++ b/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") + } +}