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 99f91ac785..1ef5588bef 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 @@ -20,6 +20,7 @@ import java.time.format.DateTimeFormatterBuilder; import java.time.temporal.ChronoField; import java.time.temporal.TemporalAccessor; +import java.time.LocalDate; import java.time.LocalDateTime; import java.time.OffsetDateTime; import java.util.ArrayDeque; @@ -173,8 +174,8 @@ public void visit(HexValue hexValue) { @Override public void visit(DateValue dateValue) { - // TODO This translation should be implemented - throw new RuntimeException("Extraction of condition not yet implemented"); + // JDBC escape {d 'yyyy-MM-dd'}: the same encoding as DATE 'yyyy-MM-dd' + pushDate(dateValue.getValue().toLocalDate()); } @Override @@ -749,9 +750,27 @@ public void visit(DateTimeLiteralExpression dateTimeLiteralExpression) { stack.push(new SqlBigIntegerLiteralValue(BigInteger.valueOf(epochSeconds))); return; } + if (dateTimeLiteralExpression.getType() == DateTimeLiteralExpression.DateTime.DATE) { + String value = dateTimeLiteralExpression.getValue(); + if (value.startsWith(SINGLE_QUOTE_CHAR) && value.endsWith(SINGLE_QUOTE_CHAR)) { + value = value.substring(1, value.length() - 1); + } + pushDate(LocalDate.parse(value)); + return; + } throw new RuntimeException("Extraction of condition not yet implemented"); } + /** + * 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 + * SMTLibZ3DbConstraintSolver. + */ + private void pushDate(LocalDate date) { + long epochSeconds = date.atStartOfDay().toEpochSecond(ZoneOffset.UTC); + stack.push(new SqlBigIntegerLiteralValue(BigInteger.valueOf(epochSeconds))); + } + @Override public void visit(NotExpression notExpression) { // TODO This translation should be implemented diff --git a/core/src/main/kotlin/org/evomaster/core/database/sql/solver/SmtLibGenerator.kt b/core/src/main/kotlin/org/evomaster/core/database/sql/solver/SmtLibGenerator.kt index 67e2a8eabd..2c51def9d6 100644 --- a/core/src/main/kotlin/org/evomaster/core/database/sql/solver/SmtLibGenerator.kt +++ b/core/src/main/kotlin/org/evomaster/core/database/sql/solver/SmtLibGenerator.kt @@ -98,6 +98,13 @@ class SmtLibGenerator( const val BOOLEAN_TYPE = "BOOLEAN" const val TIMESTAMP_TYPE = "TIMESTAMP" + /** + * Encoded like [TIMESTAMP_TYPE], in epoch seconds (SMT Int), constrained to midnight UTC. The + * shared unit lets a DATE column be compared with a TIMESTAMP literal. + */ + const val DATE_TYPE = "DATE" + internal const val SECONDS_PER_DAY = 86400L + /** * Encoded as SMT Strings with no constraint on their form, so the value Z3 assigns need not be * a valid UUID or JSON document; SMTLibZ3DbConstraintSolver turns it into one. @@ -162,7 +169,7 @@ class SmtLibGenerator( "SMALLSERIAL" to SMT_INT, "BIGSERIAL" to SMT_INT, TIMESTAMP_TYPE to SMT_INT, - "DATE" to SMT_INT, + DATE_TYPE to SMT_INT, "FLOAT" to SMT_REAL, "DOUBLE" to SMT_REAL, "DECIMAL" to SMT_REAL, @@ -417,7 +424,8 @@ class SmtLibGenerator( private fun appendTimestampConstraints(smt: SMTLib) { for (smtTable in smtTables) { for (column in smtTable.dto.columns) { - if (column.type.equals(TIMESTAMP_TYPE, ignoreCase = true)) { + val isDate = column.type.equals(DATE_TYPE, ignoreCase = true) + if (isDate || column.type.equals(TIMESTAMP_TYPE, ignoreCase = true)) { val columnName = smtTable.smtColumnName(column.name).uppercase() for (i in 1..numberOfRows) { @@ -437,6 +445,15 @@ class SmtLibGenerator( ) ) ) + if (isDate) { + smt.addNode( + AssertSMTNode( + EqualsAssertion( + listOf("(mod ($columnName ${rowConstantName(smtTable.smtName, i)}) $SECONDS_PER_DAY)", "0") + ) + ) + ) + } } } } diff --git a/core/src/main/kotlin/org/evomaster/core/database/sql/solver/service/SMTLibZ3DbConstraintSolver.kt b/core/src/main/kotlin/org/evomaster/core/database/sql/solver/service/SMTLibZ3DbConstraintSolver.kt index 156e13ff3a..7b6b44386b 100644 --- a/core/src/main/kotlin/org/evomaster/core/database/sql/solver/service/SMTLibZ3DbConstraintSolver.kt +++ b/core/src/main/kotlin/org/evomaster/core/database/sql/solver/service/SMTLibZ3DbConstraintSolver.kt @@ -117,6 +117,7 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { // reads a superset of the layouts a database may emit, of which this is one, so the value // round-trips: what is written here is read back to the same instant. private const val TIMESTAMP_FORMAT = "yyyy-MM-dd HH:mm:ss" + private const val DATE_FORMAT = "yyyy-MM-dd" private val UUID_PATTERN = Regex("[0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[0-9a-fA-F]{4}-[0-9a-fA-F]{4}-[0-9a-fA-F]{12}") @@ -499,13 +500,20 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { } } is LongValue -> { - if (hasColumnType(schemaDto, table, dbColumnName, SmtLibGenerator.TIMESTAMP_TYPE)) { + val datePattern = when { + hasColumnType(schemaDto, table, dbColumnName, SmtLibGenerator.TIMESTAMP_TYPE) -> TIMESTAMP_FORMAT + // Without this a DATE column was inserted as a bare integer, which the + // database rejects, so no row of its table was ever inserted + hasColumnType(schemaDto, table, dbColumnName, SmtLibGenerator.DATE_TYPE) -> DATE_FORMAT + else -> null + } + if (datePattern != null) { val epochSeconds = columnValue.value.toLong() val localDateTime = LocalDateTime.ofInstant( Instant.ofEpochSecond(epochSeconds), ZoneOffset.UTC ) val formatted = localDateTime.format( - DateTimeFormatter.ofPattern(TIMESTAMP_FORMAT) + DateTimeFormatter.ofPattern(datePattern) ) ImmutableDataHolderGene(dbColumnName, formatted, inQuotes = true) } else { @@ -571,8 +579,8 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { * compared case-insensitively as a raw string. * * CAVEAT: this relies on [ColumnDto.type] containing the exact spelling passed in (currently - * "BOOLEAN" and "TIMESTAMP"). It is needed because the SMT sort alone cannot recover these types - * (BOOLEAN is encoded as an SMT String, TIMESTAMP as an SMT Int), so gene reconstruction must + * "BOOLEAN", "TIMESTAMP" and "DATE"). It is needed because the SMT sort alone cannot recover these + * types (BOOLEAN is encoded as an SMT String, TIMESTAMP and DATE as an SMT Int), so gene reconstruction must * consult the original SQL type. The set of type spellings recognized here must stay consistent * with [SmtLibGenerator.TYPE_MAP]; if a backend reports a variant spelling (e.g. "BOOL" or * "TIMESTAMP WITHOUT TIME ZONE"), the special handling is silently skipped. Consolidating these diff --git a/core/src/test/kotlin/org/evomaster/core/database/sql/solver/WhereClauseTranslationLimitsTest.kt b/core/src/test/kotlin/org/evomaster/core/database/sql/solver/WhereClauseTranslationLimitsTest.kt index 83b3457a04..41597aa288 100644 --- a/core/src/test/kotlin/org/evomaster/core/database/sql/solver/WhereClauseTranslationLimitsTest.kt +++ b/core/src/test/kotlin/org/evomaster/core/database/sql/solver/WhereClauseTranslationLimitsTest.kt @@ -62,6 +62,16 @@ class WhereClauseTranslationLimitsTest { assertEpoch("T > TIMESTAMP '2026-08-18'", 1787011200) } + /** + * A DATE literal shares the TIMESTAMP encoding, at midnight UTC, so a DATE column can be compared + * with either. It used to be rejected, dropping the whole clause. + */ + @Test + fun `date literals are encoded as the epoch of their midnight`() { + assertEpoch("D > DATE '2026-08-18'", 1787011200) + assertEpoch("D = {d '2026-08-18'}", 1787011200) + } + /** * The layouts accepted are a set, not a prefix rule. A separator carries the time of day with it, * so a date followed by a dangling `T` or space is rejected rather than silently read as midnight, 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 new file mode 100644 index 0000000000..ec505c835b --- /dev/null +++ b/core/src/test/kotlin/org/evomaster/core/database/sql/solver/service/DateColumnSolvingTest.kt @@ -0,0 +1,73 @@ +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 DATE column is encoded, like a TIMESTAMP one, as epoch seconds, and must be inserted as a date. + * + * It used to be inserted as the bare integer Z3 assigned to it, which the database rejects, so no row + * of a table with a DATE column was ever inserted, whatever the query. The failure was silent: + * SqlScriptRunner.execInsert logs a failed insertion and carries on. + */ +class DateColumnSolvingTest { + + 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:date_column_test", "sa", "") + SqlScriptRunner.execCommand(connection, "CREATE TABLE ev(id bigint primary key, d date);\n") + schemaDto = DbInfoExtractor.extract(connection) + solver = SMTLibZ3DbConstraintSolver() + solver.initializeExecutor() + } + + @JvmStatic + @AfterAll + fun tearDown() { + connection.close() + if (this::solver.isInitialized) { + solver.close() + } + } + } + + @BeforeEach + fun clean() { + SqlScriptRunner.execCommand(connection, "DELETE FROM ev;\n") + } + + @ParameterizedTest + @ValueSource(strings = [ + "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'" + ]) + fun generatedRowsAreInsertedAndSatisfyTheQuery(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 be inserted") + + val result = SqlScriptRunner.execCommand(connection, query) + assertFalse(result.isEmpty(), "Inserted rows should satisfy the original query") + } +}