From cd136bb8adf12d23aef95fce74c6481261777f61 Mon Sep 17 00:00:00 2001 From: Agustina Aldasoro Date: Wed, 7 Oct 2026 14:48:11 +0200 Subject: [PATCH] Encode DATE columns like TIMESTAMP ones A DATE column was an unbounded SMT Int inserted as a bare integer, which the database rejects, so no row of a table with a DATE column was ever inserted; DATE literals were not parsed at all. DATE now shares the TIMESTAMP encoding, epoch seconds at midnight UTC: it is bounded, kept to whole days, rebuilt as yyyy-MM-dd, and DATE literals are parsed. --- .../dbconstraint/parser/jsql/JSqlVisitor.java | 23 +++++- .../database/sql/solver/SmtLibGenerator.kt | 21 +++++- .../service/SMTLibZ3DbConstraintSolver.kt | 16 +++- .../WhereClauseTranslationLimitsTest.kt | 10 +++ .../solver/service/DateColumnSolvingTest.kt | 73 +++++++++++++++++++ 5 files changed, 135 insertions(+), 8 deletions(-) create mode 100644 core/src/test/kotlin/org/evomaster/core/database/sql/solver/service/DateColumnSolvingTest.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 97c8203c12..6f8562c68e 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 cc8880de3f..14f967c804 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 @@ -82,6 +82,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 + /** * The canonical string values a BOOLEAN column may take (BOOLEAN is encoded as an SMT String). * These are generation constraints, so Z3 is forced to pick one of them; only the two canonical @@ -131,7 +138,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, @@ -330,7 +337,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) { @@ -350,6 +358,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 2159ba2799..bac02b6db3 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 @@ -106,6 +106,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" /** * Spellings [SmtLibGenerator.TYPE_MAP] already treats as the same type. The canonical one is @@ -387,13 +388,20 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { } } is LongValue -> { - gene = 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 + } + gene = 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 { @@ -478,8 +486,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") + } +}