From 0524cedbb3d584bce62672436cec3248a1d67038 Mon Sep 17 00:00:00 2001 From: Agustina Aldasoro Date: Wed, 7 Oct 2026 14:55:24 +0200 Subject: [PATCH] Encode string literals compared with DATE or TIMESTAMP columns A plain string literal compared with a DATE or TIMESTAMP column, e.g. d > '2024-01-01', was written as an SMT string against an Int column, so Z3 rejected the formula and the query got no data. Such literals, in comparisons and IN lists, are now encoded as epoch seconds like typed DATE and TIMESTAMP literals. --- .../dbconstraint/parser/jsql/JSqlVisitor.java | 24 +++++--- .../sql/solver/SMTConditionVisitor.kt | 45 ++++++++++++++- .../TemporalStringLiteralTranslationTest.kt | 55 +++++++++++++++++++ .../solver/service/DateColumnSolvingTest.kt | 9 ++- 4 files changed, 121 insertions(+), 12 deletions(-) create mode 100644 core/src/test/kotlin/org/evomaster/core/database/sql/solver/TemporalStringLiteralTranslationTest.kt diff --git a/core-extra/dbconstraint/src/main/java/org/evomaster/dbconstraint/parser/jsql/JSqlVisitor.java b/core-extra/dbconstraint/src/main/java/org/evomaster/dbconstraint/parser/jsql/JSqlVisitor.java index 6f8562c68e..ce0680a4aa 100644 --- a/core-extra/dbconstraint/src/main/java/org/evomaster/dbconstraint/parser/jsql/JSqlVisitor.java +++ b/core-extra/dbconstraint/src/main/java/org/evomaster/dbconstraint/parser/jsql/JSqlVisitor.java @@ -741,13 +741,7 @@ public void visit(DateTimeLiteralExpression dateTimeLiteralExpression) { if (value.startsWith(SINGLE_QUOTE_CHAR) && value.endsWith(SINGLE_QUOTE_CHAR)) { value = value.substring(1, value.length() - 1); } - TemporalAccessor parsed = TIMESTAMP_PARSER.parse(value); - // An explicit offset is honoured; without one, treat the literal as UTC to match the - // UTC-based decoder in SMTLibZ3DbConstraintSolver (LocalDateTime.ofInstant(..., UTC)). - long epochSeconds = parsed.isSupported(ChronoField.OFFSET_SECONDS) - ? OffsetDateTime.from(parsed).toEpochSecond() - : LocalDateTime.from(parsed).toEpochSecond(ZoneOffset.UTC); - stack.push(new SqlBigIntegerLiteralValue(BigInteger.valueOf(epochSeconds))); + stack.push(new SqlBigIntegerLiteralValue(BigInteger.valueOf(toEpochSeconds(value)))); return; } if (dateTimeLiteralExpression.getType() == DateTimeLiteralExpression.DateTime.DATE) { @@ -761,6 +755,22 @@ public void visit(DateTimeLiteralExpression dateTimeLiteralExpression) { throw new RuntimeException("Extraction of condition not yet implemented"); } + /** + * Reads a date or timestamp, in any of the layouts {@link #TIMESTAMP_PARSER} accepts, as epoch + * seconds. A date on its own is read as its midnight. Public so that a plain string literal + * compared against a DATE or TIMESTAMP column can be encoded the same way as a typed literal. + * + * @throws java.time.format.DateTimeParseException if the text is not one of those layouts + */ + public static long toEpochSeconds(String value) { + TemporalAccessor parsed = TIMESTAMP_PARSER.parse(value); + // An explicit offset is honoured; without one, treat the literal as UTC to match the + // UTC-based decoder in SMTLibZ3DbConstraintSolver (LocalDateTime.ofInstant(..., UTC)). + return parsed.isSupported(ChronoField.OFFSET_SECONDS) + ? OffsetDateTime.from(parsed).toEpochSecond() + : LocalDateTime.from(parsed).toEpochSecond(ZoneOffset.UTC); + } + /** * A DATE is encoded like a TIMESTAMP, in epoch seconds, at midnight UTC. Sharing the unit lets a * DATE column be compared with a TIMESTAMP literal, and matches the decoder in 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 8233e10be1..321777a653 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 @@ -3,6 +3,7 @@ package org.evomaster.core.database.sql.solver import org.evomaster.client.java.controller.api.dto.database.schema.TableDto import org.evomaster.core.utils.StringUtils.convertToAscii import org.evomaster.dbconstraint.ast.* +import org.evomaster.dbconstraint.parser.jsql.JSqlVisitor import org.evomaster.solver.smtlib.AssertSMTNode import org.evomaster.solver.smtlib.EmptySMTNode import org.evomaster.solver.smtlib.SMTNode @@ -110,8 +111,8 @@ class SMTConditionVisitor( if (condition.leftOperand is SqlNullLiteralValue || condition.rightOperand is SqlNullLiteralValue) { return EmptySMTNode() // TODO: Change this when we add support for nullable columns in the db schema } - val left = getVariableAndLiteral(condition.leftOperand) - val right = getVariableAndLiteral(condition.rightOperand) + val left = operandAgainst(condition.leftOperand, condition.rightOperand) + val right = operandAgainst(condition.rightOperand, condition.leftOperand) return when (val comparator = getSMTComparator(condition.sqlComparisonOperator.toString())) { "=" -> AssertSMTNode(EqualsAssertion(listOf(left, right))) @@ -249,6 +250,42 @@ class SMTConditionVisitor( * It also avoids comparing a folded table name against the schema's own spelling, which is how the * scoped version would have to identify the tables in scope. */ + /** + * Translates one side of a comparison, given the other side. + * + * A DATE or TIMESTAMP column is encoded as epoch seconds (an SMT Int), and a typed literal such as + * `DATE '2024-01-01'` already arrives as one. A plain string literal, `'2024-01-01'`, does not: + * written as an SMT string, it made Z3 compare an Int with a String and reject the formula, so the + * query got no data. It is read as a date or timestamp instead; if it is neither, the + * DateTimeParseException drops the condition like any other untranslatable one. + */ + private fun operandAgainst(operand: SqlCondition, other: SqlCondition): String = + if (operand is SqlStringLiteralValue && other is SqlColumn && isTemporalColumn(other)) { + temporalLiteral(operand) + } else { + getVariableAndLiteral(operand) + } + + private fun temporalLiteral(literal: SqlStringLiteralValue): String { + val epochSeconds = JSqlVisitor.toEpochSeconds(literal.stringValue) + // SMT-LIB has no negative numerals: a date before 1970 is written as a negation + return if (epochSeconds < 0) "(- ${-epochSeconds})" else epochSeconds.toString() + } + + /** + * Whether a column reference is to a DATE or TIMESTAMP column of the schema. + */ + private fun isTemporalColumn(column: SqlColumn): Boolean { + val tableName = column.tableName?.let { tableAliases[it] ?: it } ?: defaultTableName + val type = tables + .firstOrNull { convertToAscii(it.id.name).equals(convertToAscii(tableName), ignoreCase = true) } + ?.columns?.firstOrNull { it.name.equals(column.columnName, ignoreCase = true) } + ?.type + ?: return false + return type.equals(SmtLibGenerator.DATE_TYPE, ignoreCase = true) || + type.equals(SmtLibGenerator.TIMESTAMP_TYPE, ignoreCase = true) + } + private fun isAColumn(operand: String): Boolean { return tables.any { table -> table.columns.any { column -> column.name.equals(operand, ignoreCase = true) } @@ -282,9 +319,11 @@ class SMTConditionVisitor( override fun visit(condition: SqlInCondition, parameter: Void?): SMTNode { val left = getVariableAndLiteral(condition.sqlColumn) + val temporal = isTemporalColumn(condition.sqlColumn) val conditions = condition.literalList.sqlConditionExpressions .map { - AssertSMTNode(EqualsAssertion(listOf(left, asLiteral(it)))) + val literal = if (temporal && it is SqlStringLiteralValue) temporalLiteral(it) else asLiteral(it) + AssertSMTNode(EqualsAssertion(listOf(left, literal))) } return if (conditions.size == 1) { conditions[0] diff --git a/core/src/test/kotlin/org/evomaster/core/database/sql/solver/TemporalStringLiteralTranslationTest.kt b/core/src/test/kotlin/org/evomaster/core/database/sql/solver/TemporalStringLiteralTranslationTest.kt new file mode 100644 index 0000000000..14453fe4b0 --- /dev/null +++ b/core/src/test/kotlin/org/evomaster/core/database/sql/solver/TemporalStringLiteralTranslationTest.kt @@ -0,0 +1,55 @@ +package org.evomaster.core.database.sql.solver + +import com.fasterxml.jackson.databind.DeserializationFeature +import com.fasterxml.jackson.databind.ObjectMapper +import net.sf.jsqlparser.parser.CCJSqlParserUtil +import org.evomaster.client.java.controller.api.dto.database.schema.DbInfoDto +import org.junit.jupiter.api.Assertions.assertEquals +import org.junit.jupiter.api.Assertions.assertFalse +import org.junit.jupiter.api.Assertions.assertTrue +import org.junit.jupiter.api.Test + +/** + * A plain string literal compared against a TIMESTAMP (or DATE) column is encoded as epoch seconds, + * like a typed `TIMESTAMP '...'` literal, since the column itself is an SMT Int. Written as an SMT + * string, it made Z3 reject the formula for comparing an Int with a String. + */ +class TemporalStringLiteralTranslationTest { + + private val mapper = ObjectMapper() + .configure(DeserializationFeature.FAIL_ON_UNKNOWN_PROPERTIES, false) + + private fun schema(): DbInfoDto = mapper.readValue( + javaClass.getResourceAsStream("/solver/sample-schema.json")!!.bufferedReader().readText(), + DbInfoDto::class.java + ) + + @Test + fun `a string literal against a timestamp column is encoded as epoch seconds`() { + val smt = SmtLibGenerator(schema(), 1) + .generateSMT(CCJSqlParserUtil.parse("SELECT ID FROM ACCOUNT WHERE CREATED_AT > '2024-01-01'")).toString() + + assertTrue(smt.contains("1704067200")) { "expected the epoch of 2024-01-01 in:\n$smt" } + assertFalse(smt.contains("\"2024-01-01\"")) { "the literal was written as a string:\n$smt" } + } + + @Test + fun `a date before 1970 is written as a negation`() { + val smt = SmtLibGenerator(schema(), 1) + .generateSMT(CCJSqlParserUtil.parse("SELECT ID FROM ACCOUNT WHERE CREATED_AT <> '1960-01-01'")).toString() + + assertTrue(smt.contains("(- 315619200)")) { "expected a negated numeral in:\n$smt" } + } + + @Test + fun `a string that is not a date drops only its condition`() { + val generator = SmtLibGenerator(schema(), 1) + val smt = generator.generateSMT( + CCJSqlParserUtil.parse("SELECT ID FROM ACCOUNT WHERE CREATED_AT = 'yesterday' AND LEVEL = 3") + ).toString() + + assertEquals(1, generator.skippedQueryConstraints) + assertFalse(smt.contains("\"yesterday\"")) { "the literal was written as a string:\n$smt" } + assertTrue(smt.contains("(LEVEL account__1)")) { "the other conjunct should be kept:\n$smt" } + } +} diff --git a/core/src/test/kotlin/org/evomaster/core/database/sql/solver/service/DateColumnSolvingTest.kt b/core/src/test/kotlin/org/evomaster/core/database/sql/solver/service/DateColumnSolvingTest.kt index ec505c835b..a6e1daf298 100644 --- a/core/src/test/kotlin/org/evomaster/core/database/sql/solver/service/DateColumnSolvingTest.kt +++ b/core/src/test/kotlin/org/evomaster/core/database/sql/solver/service/DateColumnSolvingTest.kt @@ -32,7 +32,7 @@ class DateColumnSolvingTest { @BeforeAll fun setup() { connection = DriverManager.getConnection("jdbc:h2:mem:date_column_test", "sa", "") - SqlScriptRunner.execCommand(connection, "CREATE TABLE ev(id bigint primary key, d date);\n") + SqlScriptRunner.execCommand(connection, "CREATE TABLE ev(id bigint primary key, d date, ts timestamp);\n") schemaDto = DbInfoExtractor.extract(connection) solver = SMTLibZ3DbConstraintSolver() solver.initializeExecutor() @@ -58,7 +58,12 @@ class DateColumnSolvingTest { "SELECT * FROM ev WHERE id = 1", "SELECT * FROM ev WHERE d = DATE '2024-03-05'", "SELECT * FROM ev WHERE d > DATE '2024-01-01'", - "SELECT * FROM ev WHERE d > TIMESTAMP '2024-01-01 10:00:00'" + "SELECT * FROM ev WHERE d > TIMESTAMP '2024-01-01 10:00:00'", + // plain string literals, as an ORM's bound parameters arrive, read as dates and timestamps + "SELECT * FROM ev WHERE d > '2024-01-01'", + "SELECT * FROM ev WHERE '2024-03-05' = d", + "SELECT * FROM ev WHERE d IN ('2024-03-05', '2024-03-06')", + "SELECT * FROM ev WHERE ts > '2024-01-01 10:00:00'" ]) fun generatedRowsAreInsertedAndSatisfyTheQuery(query: String) { val actions = solver.solve(schemaDto, query, 1)