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 1ef5588bef..036f472b77 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 da35f30f98..fddc6aed30 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 @@ -129,8 +130,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 = comparisonOperand(condition.leftOperand, condition.rightOperand) + val right = comparisonOperand(condition.rightOperand, condition.leftOperand) return when (val comparator = getSMTComparator(condition.sqlComparisonOperator.toString())) { "=" -> AssertSMTNode(EqualsAssertion(listOf(left, right))) @@ -247,6 +248,42 @@ class SMTConditionVisitor( private fun isBooleanLiteral(operand: String): Boolean = operand.equals("true", ignoreCase = true) || operand.equals("false", ignoreCase = true) + /** + * Translates one operand of a comparison (`a op b`), given the operand it is compared with. + * + * 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 comparisonOperand(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) + } + /** * Whether any table in the schema declares a column with this name. * @@ -292,20 +329,19 @@ class SMTConditionVisitor( override fun visit(condition: SqlInCondition, parameter: Void?): SMTNode { val left = getVariableAndLiteral(condition.sqlColumn) + val temporal = isTemporalColumn(condition.sqlColumn) + val literals = condition.literalList.sqlConditionExpressions + .map { if (temporal && it is SqlStringLiteralValue) temporalLiteral(it) else asLiteral(it) } if (condition.isNegated) { // NOT IN: the column must differ from every value in the list - val conditions = condition.literalList.sqlConditionExpressions - .map { DistinctAssertion(listOf(left, asLiteral(it))) } + val conditions = literals.map { DistinctAssertion(listOf(left, it)) } return if (conditions.size == 1) { AssertSMTNode(conditions[0]) } else { AssertSMTNode(AndAssertion(conditions)) } } - val conditions = condition.literalList.sqlConditionExpressions - .map { - AssertSMTNode(EqualsAssertion(listOf(left, asLiteral(it)))) - } + val conditions = literals.map { AssertSMTNode(EqualsAssertion(listOf(left, it))) } return if (conditions.size == 1) { conditions[0] } else { 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)