Encode string literals compared with DATE or TIMESTAMP columns

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

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 = 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)))
@@ -259,6 +260,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) }
@@ -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 {

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

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)