From d1fa41e877e9777b85bf8c9a32b6cf40afda5979 Mon Sep 17 00:00:00 2001 From: Agustina Aldasoro Date: Mon, 15 Jun 2026 22:29:48 -0300 Subject: [PATCH 1/7] Add correctness statistics for DSE --- core/pom.xml | 4 ++ .../kotlin/org/evomaster/core/EMConfig.kt | 8 +++ .../core/search/service/Statistics.kt | 28 ++++++++++ .../core/solver/SMTLibZ3DbConstraintSolver.kt | 56 ++++++++++++++++++- 4 files changed, 95 insertions(+), 1 deletion(-) diff --git a/core/pom.xml b/core/pom.xml index e07fe92519..fd45fa199f 100644 --- a/core/pom.xml +++ b/core/pom.xml @@ -33,6 +33,10 @@ org.evomaster evomaster-client-java-controller-api + + org.evomaster + evomaster-client-java-sql + org.evomaster evomaster-client-java-instrumentation-shared diff --git a/core/src/main/kotlin/org/evomaster/core/EMConfig.kt b/core/src/main/kotlin/org/evomaster/core/EMConfig.kt index 570e374419..f7956efd28 100644 --- a/core/src/main/kotlin/org/evomaster/core/EMConfig.kt +++ b/core/src/main/kotlin/org/evomaster/core/EMConfig.kt @@ -1927,6 +1927,14 @@ class EMConfig { @DependsOnTrueFor("generateSqlDataWithDSE") var collectDseStats = false + @Experimental + @Cfg("Measure the correctness of DSE-generated SQL inserts by computing the heuristic " + + "distance between the original failing WHERE query and the generated INSERT data. " + + "Distance=0 means the insert satisfies the WHERE; distance>0 means it does not. " + + "Only meaningful when generateSqlDataWithDSE=true.") + @DependsOnTrueFor("generateSqlDataWithDSE") + var measureDseCorrectness = false + @Cfg("Enable EvoMaster to generate SQL data with direct accesses to the database. Use a search algorithm") @DependsOnFalseFor("blackBox") var generateSqlDataWithSearch = true diff --git a/core/src/main/kotlin/org/evomaster/core/search/service/Statistics.kt b/core/src/main/kotlin/org/evomaster/core/search/service/Statistics.kt index 79deb19a78..1fa5a3124e 100644 --- a/core/src/main/kotlin/org/evomaster/core/search/service/Statistics.kt +++ b/core/src/main/kotlin/org/evomaster/core/search/service/Statistics.kt @@ -98,6 +98,13 @@ class Statistics : SearchListener { private val dseSeenQueryHashes = mutableSetOf() private var dseUniqueQueriesCount = 0 + // DSE correctness distance statistics (only when measureDseCorrectness=true) + private var dseCorrectnessCheckCount = 0 + private var dseCorrectnessZeroDistanceCount = 0 + private var dseCorrectnessNonZeroDistanceCount = 0 + private val dseCorrectnessAvgDistance = IncrementalAverage() + private var dseCorrectnessEvalFailureCount = 0 + // mongo heuristic evaluation statistic private var mongoHeuristicEvaluationSuccessCount = 0 private var mongoHeuristicEvaluationFailureCount = 0 @@ -269,6 +276,18 @@ class Statistics : SearchListener { } } + fun reportDseCorrectnessDistance(sqlDistance: Double, evaluationFailure: Boolean) { + dseCorrectnessCheckCount++ + if (evaluationFailure) { + dseCorrectnessEvalFailureCount++ + } else if (sqlDistance == 0.0) { + dseCorrectnessZeroDistanceCount++ + } else { + dseCorrectnessNonZeroDistanceCount++ + } + dseCorrectnessAvgDistance.addValue(sqlDistance) + } + fun getMongoHeuristicsEvaluationCount(): Int = mongoHeuristicEvaluationSuccessCount + mongoHeuristicEvaluationFailureCount fun getSqlHeuristicsEvaluationCount(): Int = sqlHeuristicEvaluationSuccessCount + sqlHeuristicEvaluationFailureCount @@ -441,6 +460,15 @@ class Statistics : SearchListener { add(Pair("dseAvgSmtlibSizeBytes", "%.1f".format(dseSmtlibSizeBytes.mean))) } + // correctness distance stats (only emitted when measureDseCorrectness=true) + if (config.measureDseCorrectness) { + add(Pair("dseCorrectnessChecks", "$dseCorrectnessCheckCount")) + add(Pair("dseCorrectnessZeroDistance", "$dseCorrectnessZeroDistanceCount")) + add(Pair("dseCorrectnessNonZero", "$dseCorrectnessNonZeroDistanceCount")) + add(Pair("dseCorrectnessAvgDist", "%.4f".format(dseCorrectnessAvgDistance.mean))) + add(Pair("dseCorrectnessEvalFailures", "$dseCorrectnessEvalFailureCount")) + } + for(phase in ExecutionPhaseController.Phase.entries){ add(Pair("phase_${phase.name}", "${epc.getPhaseDurationInSeconds(phase)}")) } diff --git a/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt b/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt index 907fb2406d..0f8e9f3626 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt @@ -11,6 +11,12 @@ import org.evomaster.client.java.controller.api.dto.database.schema.DbInfoDto import org.evomaster.client.java.controller.api.dto.database.schema.TableDto import org.evomaster.core.EMConfig import org.evomaster.core.logging.LoggingUtil +import org.evomaster.client.java.sql.DataRow +import org.evomaster.client.java.sql.QueryResult +import org.evomaster.client.java.sql.QueryResultSet +import org.evomaster.client.java.sql.heuristic.SqlHeuristicsCalculator +import org.evomaster.client.java.sql.heuristic.TableColumnResolver +import org.evomaster.client.java.sql.internal.SqlDistanceWithMetrics import org.evomaster.core.search.gene.BooleanGene import org.evomaster.core.search.gene.Gene import org.evomaster.core.search.gene.numeric.DoubleGene @@ -141,7 +147,15 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { Z3Result.Status.SAT -> { if (collectStats) statistics.reportDseSat(z3TimeMs) z3ResultCache[cacheKey] = z3Result - toSqlActionList(schemaDto, z3Result.model) + val sqlActions = toSqlActionList(schemaDto, z3Result.model) + if (config.measureDseCorrectness) { + val distResult = computeCorrectnessDistance(sqlQuery, schemaDto, sqlActions) + statistics.reportDseCorrectnessDistance( + distResult.sqlDistance, + distResult.sqlDistanceEvaluationFailure + ) + } + sqlActions } Z3Result.Status.UNSAT -> { if (collectStats) statistics.reportDseUnsat(z3TimeMs) @@ -426,4 +440,44 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { } private fun leadingBarResourcesFolder() = if (resourcesFolder.endsWith("/")) resourcesFolder else "$resourcesFolder/" + + private fun computeCorrectnessDistance( + sqlQuery: String, + schemaDto: DbInfoDto, + sqlActions: List + ): SqlDistanceWithMetrics { + val queryResultSet = toQueryResultSet(sqlActions) + val calculator = SqlHeuristicsCalculator.SqlHeuristicsCalculatorBuilder() + .withTableColumnResolver(TableColumnResolver(schemaDto)) + .withSourceQueryResultSet(queryResultSet) + .build() + return calculator.computeDistance(sqlQuery) + } + + private fun toQueryResultSet(sqlActions: List): QueryResultSet { + val queryResultSet = QueryResultSet() + val byTable = sqlActions.groupBy { it.table.id.name } + for ((tableName, actions) in byTable) { + val columnNames = actions.first().seeTopGenes().map { it.name } + val queryResult = QueryResult(columnNames, tableName) + for (action in actions) { + val values: List = action.seeTopGenes().map { gene -> extractGeneValue(gene) } + queryResult.addRow(DataRow(tableName, columnNames, values)) + } + queryResultSet.addQueryResult(queryResult) + } + return queryResultSet + } + + private fun extractGeneValue(gene: Gene): Any? { + val inner = if (gene is SqlPrimaryKeyGene) gene.gene else gene + return when (inner) { + is IntegerGene -> inner.value + is StringGene -> inner.value + is DoubleGene -> inner.value + is BooleanGene -> inner.value + is ImmutableDataHolderGene -> inner.value + else -> inner.getValueAsRawString() + } + } } From 7eccbad2f5638e37ff863d5c7077aaaee6cdb439 Mon Sep 17 00:00:00 2001 From: Agustina Aldasoro Date: Mon, 15 Jun 2026 22:47:23 -0300 Subject: [PATCH 2/7] Update docs --- docs/options.md | 1 + 1 file changed, 1 insertion(+) diff --git a/docs/options.md b/docs/options.md index e65cd1466d..42d9b5ceed 100644 --- a/docs/options.md +++ b/docs/options.md @@ -321,6 +321,7 @@ There are 3 types of options: |`maxSizeOfHandlingResource`| __Int__. Specify a maximum number of handling (remove/add) resource size at once, e.g., add 3 resource at most. *Constraints*: `min=0.0`. *Default value*: `0`.| |`maxSizeOfMutatingInitAction`| __Int__. Specify a maximum number of handling (remove/add) init actions at once, e.g., add 3 init actions at most. *Constraints*: `min=0.0`. *Default value*: `0`.| |`maxTestSizeStrategy`| __Enum__. Specify a strategy to handle a max size of a test. *Valid values*: `SPECIFIED, DPC_INCREASING, DPC_DECREASING`. *Default value*: `SPECIFIED`.| +|`measureDseCorrectness`| __Boolean__. Measure the correctness of DSE-generated SQL inserts by computing the heuristic distance between the original failing WHERE query and the generated INSERT data. Distance=0 means the insert satisfies the WHERE; distance>0 means it does not. Only meaningful when generateSqlDataWithDSE=true. *Depends on*: `generateSqlDataWithDSE=true`. *Default value*: `false`.| |`mutationTargetsSelectionStrategy`| __Enum__. Specify a strategy to select targets for evaluating mutation. *Valid values*: `FIRST_NOT_COVERED_TARGET, EXPANDED_UPDATED_NOT_COVERED_TARGET, UPDATED_NOT_COVERED_TARGET`. *Default value*: `FIRST_NOT_COVERED_TARGET`.| |`onePlusLambdaLambdaOffspringSize`| __Int__. 1+(λ,λ) GA: number of offspring (λ) per generation. *Constraints*: `min=1.0`. *Default value*: `4`.| |`overlay`| __String__. Specify an OAI Overlay file path, or a folder containing those. In this latter case, Overlay files will be searched recursively in the nested folder, matching a given list of configurable suffixes. Each Overlay will be applied to the target OpenAPI schema. If more than one Overlay file is applied, no specific ordering of transformations is enforced. *Default value*: `""`.| From a71de1699b27cfea3f7fd0fd866ff854825159fa Mon Sep 17 00:00:00 2001 From: Agustina Aldasoro Date: Tue, 16 Jun 2026 11:24:24 -0300 Subject: [PATCH 3/7] Fix stats --- .../kotlin/org/evomaster/core/search/service/Statistics.kt | 6 +++++- .../org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt | 5 +++++ 2 files changed, 10 insertions(+), 1 deletion(-) diff --git a/core/src/main/kotlin/org/evomaster/core/search/service/Statistics.kt b/core/src/main/kotlin/org/evomaster/core/search/service/Statistics.kt index 1fa5a3124e..ca60751ce5 100644 --- a/core/src/main/kotlin/org/evomaster/core/search/service/Statistics.kt +++ b/core/src/main/kotlin/org/evomaster/core/search/service/Statistics.kt @@ -279,8 +279,12 @@ class Statistics : SearchListener { fun reportDseCorrectnessDistance(sqlDistance: Double, evaluationFailure: Boolean) { dseCorrectnessCheckCount++ if (evaluationFailure) { + // sqlDistance is a sentinel value (e.g. Double.MAX_VALUE) in this case, + // and must not pollute the average of real distances dseCorrectnessEvalFailureCount++ - } else if (sqlDistance == 0.0) { + return + } + if (sqlDistance == 0.0) { dseCorrectnessZeroDistanceCount++ } else { dseCorrectnessNonZeroDistanceCount++ diff --git a/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt b/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt index 0f8e9f3626..6386f8774a 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt @@ -150,6 +150,11 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { val sqlActions = toSqlActionList(schemaDto, z3Result.model) if (config.measureDseCorrectness) { val distResult = computeCorrectnessDistance(sqlQuery, schemaDto, sqlActions) + if (distResult.sqlDistanceEvaluationFailure) { + LoggingUtil.getInfoLogger().warn("DSE: correctness evaluation failure for query '$sqlQuery'") + } else if (distResult.sqlDistance != 0.0) { + LoggingUtil.getInfoLogger().warn("DSE: non-zero correctness distance (${distResult.sqlDistance}) for query '$sqlQuery'") + } statistics.reportDseCorrectnessDistance( distResult.sqlDistance, distResult.sqlDistanceEvaluationFailure From 242b8a312efb5379d0adf0950ac0e66cb9e067d3 Mon Sep 17 00:00:00 2001 From: Agustina Aldasoro Date: Tue, 16 Jun 2026 17:12:59 -0300 Subject: [PATCH 4/7] Fix stats --- .../heuristic/SqlHeuristicsCalculator.java | 3 ++- .../core/solver/SMTLibZ3DbConstraintSolver.kt | 23 ++++++++++++++++--- 2 files changed, 22 insertions(+), 4 deletions(-) diff --git a/client-java/sql/src/main/java/org/evomaster/client/java/sql/heuristic/SqlHeuristicsCalculator.java b/client-java/sql/src/main/java/org/evomaster/client/java/sql/heuristic/SqlHeuristicsCalculator.java index 2d9a83cd00..db8e0b9584 100644 --- a/client-java/sql/src/main/java/org/evomaster/client/java/sql/heuristic/SqlHeuristicsCalculator.java +++ b/client-java/sql/src/main/java/org/evomaster/client/java/sql/heuristic/SqlHeuristicsCalculator.java @@ -124,7 +124,8 @@ public SqlDistanceWithMetrics computeDistance(String sqlCommand) { double distanceToTrue = 1.0d - t.getOfTrue(); return new SqlDistanceWithMetrics(distanceToTrue, 0, false); } catch (Exception ex) { - SimpleLogger.uniqueWarn("Failed to compute complete SQL heuristics for: " + sqlCommand); + SimpleLogger.uniqueWarn("Failed to compute complete SQL heuristics for: " + sqlCommand + + " | cause: " + ex.getClass().getName() + ": " + ex.getMessage()); return new SqlDistanceWithMetrics(Double.MAX_VALUE, 0, true); } } diff --git a/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt b/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt index 6386f8774a..938c592822 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt @@ -21,6 +21,7 @@ import org.evomaster.core.search.gene.BooleanGene import org.evomaster.core.search.gene.Gene import org.evomaster.core.search.gene.numeric.DoubleGene import org.evomaster.core.search.gene.numeric.IntegerGene +import org.evomaster.core.search.gene.numeric.LongGene import org.evomaster.core.search.gene.placeholder.ImmutableDataHolderGene import org.evomaster.core.search.gene.sql.SqlPrimaryKeyGene import org.evomaster.core.search.gene.string.StringGene @@ -451,7 +452,7 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { schemaDto: DbInfoDto, sqlActions: List ): SqlDistanceWithMetrics { - val queryResultSet = toQueryResultSet(sqlActions) + val queryResultSet = toQueryResultSet(schemaDto, sqlActions) val calculator = SqlHeuristicsCalculator.SqlHeuristicsCalculatorBuilder() .withTableColumnResolver(TableColumnResolver(schemaDto)) .withSourceQueryResultSet(queryResultSet) @@ -459,7 +460,7 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { return calculator.computeDistance(sqlQuery) } - private fun toQueryResultSet(sqlActions: List): QueryResultSet { + private fun toQueryResultSet(schemaDto: DbInfoDto, sqlActions: List): QueryResultSet { val queryResultSet = QueryResultSet() val byTable = sqlActions.groupBy { it.table.id.name } for ((tableName, actions) in byTable) { @@ -471,6 +472,15 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { } queryResultSet.addQueryResult(queryResult) } + // Tables not present in Z3's SAT model (e.g. the optional side of a LEFT OUTER JOIN) + // still need an (empty) QueryResult, otherwise SqlHeuristicsCalculator NPEs when it + // looks them up unconditionally while walking the FROM/JOIN clause. + for (table in schemaDto.tables) { + if (table.id.name !in byTable.keys) { + val columnNames = table.columns.map { it.name } + queryResultSet.addQueryResult(QueryResult(columnNames, table.id.name)) + } + } return queryResultSet } @@ -478,11 +488,18 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { val inner = if (gene is SqlPrimaryKeyGene) gene.gene else gene return when (inner) { is IntegerGene -> inner.value + is LongGene -> inner.value is StringGene -> inner.value is DoubleGene -> inner.value is BooleanGene -> inner.value is ImmutableDataHolderGene -> inner.value - else -> inner.getValueAsRawString() + else -> { + LoggingUtil.getInfoLogger().warn( + "DSE: extractGeneValue() fallback to raw string for unhandled gene type " + + "${inner.javaClass.name} (outer: ${gene.javaClass.name}, name: ${gene.name})" + ) + inner.getValueAsRawString() + } } } } From a2c23217ce2e0bd6899bc65ac2ee0a131fac0359 Mon Sep 17 00:00:00 2001 From: Agustina Aldasoro Date: Wed, 17 Jun 2026 01:27:56 -0300 Subject: [PATCH 5/7] Implement missing parse sql --- .../dbconstraint/parser/jsql/JSqlVisitor.java | 25 +++++++++-- .../parser/JSqlConditionParserTest.java | 43 ++++++++++++++++++- 2 files changed, 62 insertions(+), 6 deletions(-) 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 cebf38b411..e6f249b5da 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 @@ -13,6 +13,8 @@ import net.sf.jsqlparser.statement.select.Select; import org.evomaster.dbconstraint.ast.*; +import java.math.BigInteger; +import java.sql.Timestamp; import java.util.ArrayDeque; import java.util.ArrayList; import java.util.Deque; @@ -45,7 +47,14 @@ public void visit(NullValue nullValue) { @Override public void visit(Function function) { - // TODO This translation should be implemented + String name = function.getName().toUpperCase(); + if ((name.equals("LOWER") || name.equals("UPPER")) + && function.getParameters() != null + && function.getParameters().size() == 1) { + // Treat LOWER(col)/UPPER(col) as the column itself (case-folding is dropped as an approximation) + function.getParameters().get(0).accept(this); + return; + } throw new RuntimeException("Extraction of condition not yet implemented"); } @@ -113,8 +122,8 @@ public void visit(TimeValue timeValue) { @Override public void visit(TimestampValue timestampValue) { - // TODO This translation should be implemented - throw new RuntimeException("Extraction of condition not yet implemented"); + long epochSeconds = timestampValue.getValue().getTime() / 1000L; + stack.push(new SqlBigIntegerLiteralValue(BigInteger.valueOf(epochSeconds))); } @Override @@ -599,7 +608,15 @@ public void visit(TimeKeyExpression timeKeyExpression) { @Override public void visit(DateTimeLiteralExpression dateTimeLiteralExpression) { - // TODO This translation should be implemented + if (dateTimeLiteralExpression.getType() == DateTimeLiteralExpression.DateTime.TIMESTAMP) { + String value = dateTimeLiteralExpression.getValue(); + if (value.startsWith("'") && value.endsWith("'")) { + value = value.substring(1, value.length() - 1); + } + long epochSeconds = Timestamp.valueOf(value).getTime() / 1000L; + stack.push(new SqlBigIntegerLiteralValue(BigInteger.valueOf(epochSeconds))); + return; + } throw new RuntimeException("Extraction of condition not yet implemented"); } diff --git a/core-extra/dbconstraint/src/test/java/org/evomaster/dbconstraint/parser/JSqlConditionParserTest.java b/core-extra/dbconstraint/src/test/java/org/evomaster/dbconstraint/parser/JSqlConditionParserTest.java index bd09d25f30..824befd1ba 100644 --- a/core-extra/dbconstraint/src/test/java/org/evomaster/dbconstraint/parser/JSqlConditionParserTest.java +++ b/core-extra/dbconstraint/src/test/java/org/evomaster/dbconstraint/parser/JSqlConditionParserTest.java @@ -1,12 +1,12 @@ package org.evomaster.dbconstraint.parser; import org.evomaster.dbconstraint.ConstraintDatabaseType; -import org.evomaster.dbconstraint.ast.SqlCondition; -import org.evomaster.dbconstraint.ast.SqlInCondition; +import org.evomaster.dbconstraint.ast.*; import org.evomaster.dbconstraint.parser.jsql.JSqlConditionParser; import org.junit.jupiter.api.Test; import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertInstanceOf; import static org.junit.jupiter.api.Assertions.assertTrue; public class JSqlConditionParserTest { @@ -104,4 +104,43 @@ public void testParseCastAsCharacterLargeObject() throws SqlConditionParserExcep assertEquals(expected, actual); } + @Test + public void testParseLowerFunction() throws SqlConditionParserException { + JSqlConditionParser parser = new JSqlConditionParser(); + // LOWER(col) should be treated as col (case-folding dropped as approximation) + SqlCondition withLower = parser.parse("LOWER(commit_mgr_desc) != 'init'", ConstraintDatabaseType.H2); + SqlCondition withoutLower = parser.parse("commit_mgr_desc != 'init'", ConstraintDatabaseType.H2); + assertEquals(withoutLower, withLower); + } + + @Test + public void testParseUpperFunction() throws SqlConditionParserException { + JSqlConditionParser parser = new JSqlConditionParser(); + SqlCondition withUpper = parser.parse("UPPER(status) != 'ACTIVE'", ConstraintDatabaseType.H2); + SqlCondition withoutUpper = parser.parse("status != 'ACTIVE'", ConstraintDatabaseType.H2); + assertEquals(withoutUpper, withUpper); + } + + @Test + public void testParseIsNotNullOrLower() throws SqlConditionParserException { + // Pattern seen in tracking-system: col IS NOT NULL OR LOWER(other_col) != 'init' + JSqlConditionParser parser = new JSqlConditionParser(); + SqlCondition condition = parser.parse( + "commit_emp_desc IS NOT NULL OR LOWER(commit_mgr_desc) != 'init'", + ConstraintDatabaseType.H2); + assertInstanceOf(SqlOrCondition.class, condition); + } + + @Test + public void testParseTimestampLiteral() throws SqlConditionParserException { + // Pattern seen in tracking-system: col = TIMESTAMP 'datetime-string' + JSqlConditionParser parser = new JSqlConditionParser(); + SqlCondition condition = parser.parse( + "commit_date = TIMESTAMP '2020-11-26 10:49:41'", + ConstraintDatabaseType.H2); + assertInstanceOf(SqlComparisonCondition.class, condition); + SqlComparisonCondition cmp = (SqlComparisonCondition) condition; + assertInstanceOf(SqlBigIntegerLiteralValue.class, cmp.getRightOperand()); + } + } From d7aa5fb2240683abd46af8467b313a6530af36e5 Mon Sep 17 00:00:00 2001 From: Agustina Aldasoro Date: Wed, 17 Jun 2026 03:27:15 -0300 Subject: [PATCH 6/7] Fix some bugs --- .../dbconstraint/parser/jsql/JSqlVisitor.java | 12 +- .../parser/JSqlConditionParserTest.java | 8 ++ .../core/solver/SMTLibZ3DbConstraintSolver.kt | 29 +++-- .../evomaster/core/solver/SmtLibGenerator.kt | 112 +++++++++++++----- .../core/solver/SmtLibGeneratorTest.kt | 75 ++++++++++++ 5 files changed, 195 insertions(+), 41 deletions(-) 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 e6f249b5da..9c51d6991e 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 @@ -15,6 +15,8 @@ import java.math.BigInteger; import java.sql.Timestamp; +import java.time.ZoneOffset; +import java.time.format.DateTimeFormatter; import java.util.ArrayDeque; import java.util.ArrayList; import java.util.Deque; @@ -122,7 +124,9 @@ public void visit(TimeValue timeValue) { @Override public void visit(TimestampValue timestampValue) { - long epochSeconds = timestampValue.getValue().getTime() / 1000L; + // Treat the timestamp string as UTC so the epoch round-trips consistently with the + // UTC-based decoder in SMTLibZ3DbConstraintSolver (LocalDateTime.ofInstant(..., UTC)). + long epochSeconds = timestampValue.getValue().toLocalDateTime().toEpochSecond(ZoneOffset.UTC); stack.push(new SqlBigIntegerLiteralValue(BigInteger.valueOf(epochSeconds))); } @@ -613,7 +617,11 @@ public void visit(DateTimeLiteralExpression dateTimeLiteralExpression) { if (value.startsWith("'") && value.endsWith("'")) { value = value.substring(1, value.length() - 1); } - long epochSeconds = Timestamp.valueOf(value).getTime() / 1000L; + // Treat the timestamp string as UTC to match the UTC-based decoder in + // SMTLibZ3DbConstraintSolver (LocalDateTime.ofInstant(..., UTC)). + long epochSeconds = java.time.LocalDateTime.parse(value, + DateTimeFormatter.ofPattern("yyyy-MM-dd HH:mm:ss")) + .toEpochSecond(ZoneOffset.UTC); stack.push(new SqlBigIntegerLiteralValue(BigInteger.valueOf(epochSeconds))); return; } diff --git a/core-extra/dbconstraint/src/test/java/org/evomaster/dbconstraint/parser/JSqlConditionParserTest.java b/core-extra/dbconstraint/src/test/java/org/evomaster/dbconstraint/parser/JSqlConditionParserTest.java index 824befd1ba..2d38c5ced4 100644 --- a/core-extra/dbconstraint/src/test/java/org/evomaster/dbconstraint/parser/JSqlConditionParserTest.java +++ b/core-extra/dbconstraint/src/test/java/org/evomaster/dbconstraint/parser/JSqlConditionParserTest.java @@ -141,6 +141,14 @@ public void testParseTimestampLiteral() throws SqlConditionParserException { assertInstanceOf(SqlComparisonCondition.class, condition); SqlComparisonCondition cmp = (SqlComparisonCondition) condition; assertInstanceOf(SqlBigIntegerLiteralValue.class, cmp.getRightOperand()); + // The epoch value must be computed in UTC so that the round-trip in + // SMTLibZ3DbConstraintSolver (LocalDateTime.ofInstant(..., UTC)) preserves + // the original string representation regardless of JVM timezone. + SqlBigIntegerLiteralValue epoch = (SqlBigIntegerLiteralValue) cmp.getRightOperand(); + long expected = java.time.LocalDateTime.parse("2020-11-26 10:49:41", + java.time.format.DateTimeFormatter.ofPattern("yyyy-MM-dd HH:mm:ss")) + .toEpochSecond(java.time.ZoneOffset.UTC); + assertEquals(java.math.BigInteger.valueOf(expected), epoch.getBigInteger()); } } diff --git a/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt b/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt index 938c592822..07c170af01 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt @@ -4,6 +4,7 @@ import com.google.inject.Inject import net.sf.jsqlparser.JSQLParserException import net.sf.jsqlparser.parser.CCJSqlParserUtil import net.sf.jsqlparser.statement.Statement +import net.sf.jsqlparser.statement.insert.Insert import org.apache.commons.io.FileUtils import org.evomaster.client.java.controller.api.dto.database.schema.ColumnDto import org.evomaster.client.java.controller.api.dto.database.schema.DatabaseType @@ -150,16 +151,26 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { z3ResultCache[cacheKey] = z3Result val sqlActions = toSqlActionList(schemaDto, z3Result.model) if (config.measureDseCorrectness) { - val distResult = computeCorrectnessDistance(sqlQuery, schemaDto, sqlActions) - if (distResult.sqlDistanceEvaluationFailure) { - LoggingUtil.getInfoLogger().warn("DSE: correctness evaluation failure for query '$sqlQuery'") - } else if (distResult.sqlDistance != 0.0) { - LoggingUtil.getInfoLogger().warn("DSE: non-zero correctness distance (${distResult.sqlDistance}) for query '$sqlQuery'") + /* + * INSERT statements have no WHERE clause, so SqlHeuristicsCalculator has no + * predicate to evaluate distance against and will always report a failure. + * Correctness measurement only makes sense for queries that filter rows + * (SELECT, DELETE, UPDATE). In the future this could be extended to verify + * that the generated rows satisfy insertion preconditions such as FK constraints + * or NOT NULL columns that DSE currently leaves unconstrained. + */ + if (queryStatement !is Insert) { + val distResult = computeCorrectnessDistance(sqlQuery, schemaDto, sqlActions) + if (distResult.sqlDistanceEvaluationFailure) { + LoggingUtil.getInfoLogger().warn("DSE: correctness evaluation failure for query '$sqlQuery'") + } else if (distResult.sqlDistance != 0.0) { + LoggingUtil.getInfoLogger().warn("DSE: non-zero correctness distance (${distResult.sqlDistance}) for query '$sqlQuery'") + } + statistics.reportDseCorrectnessDistance( + distResult.sqlDistance, + distResult.sqlDistanceEvaluationFailure + ) } - statistics.reportDseCorrectnessDistance( - distResult.sqlDistance, - distResult.sqlDistanceEvaluationFailure - ) } sqlActions } diff --git a/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt b/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt index 26c76bb849..0e06819be6 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt @@ -2,9 +2,11 @@ package org.evomaster.core.solver import net.sf.jsqlparser.schema.Table import net.sf.jsqlparser.statement.Statement +import net.sf.jsqlparser.statement.delete.Delete import net.sf.jsqlparser.statement.select.FromItem import net.sf.jsqlparser.statement.select.PlainSelect import net.sf.jsqlparser.statement.select.Select +import net.sf.jsqlparser.statement.update.Update import net.sf.jsqlparser.util.TablesNamesFinder import org.evomaster.client.java.controller.api.dto.database.schema.DatabaseType import org.evomaster.client.java.controller.api.dto.database.schema.DbInfoDto @@ -231,9 +233,19 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I private fun appendPrimaryKeyConstraints(smt: SMTLib, smtTable: SmtTable) { val primaryKeys = smtTable.dto.columns.filter { it.primaryKey } - for (primaryKey in primaryKeys) { - val nodes = assertForDistinctField(smtTable.smtColumnName(primaryKey.name), smtTable.smtName) - smt.addNodes(nodes) + if (primaryKeys.size <= 1) { + // Single-column PK: the column must be individually distinct across all row pairs. + for (primaryKey in primaryKeys) { + smt.addNodes(assertForDistinctField(smtTable.smtColumnName(primaryKey.name), smtTable.smtName)) + } + } else { + // Composite PK: the *tuple* of PK columns must be distinct across all row pairs, + // meaning at least one column must differ — not necessarily all of them. + // Emitting per-column distinctness (the old behaviour) was over-constrained: it + // prevented valid rows like (emp=1, proj=2) and (emp=1, proj=3) because it forced + // every PK column to differ individually, rather than just the tuple. + val pkSelectors = primaryKeys.map { smtTable.smtColumnName(it.name) } + smt.addNodes(assertForDistinctCompositePK(pkSelectors, smtTable.smtName)) } } @@ -263,6 +275,30 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I return nodes } + /** + * Generates composite PK distinctness assertions across all row pairs. + * For each pair (i, j), asserts that at least one PK column differs between row i and row j. + * + * @param pkSelectors The list of PK column names (SMT form). + * @param tableName The SMT name of the table. + * @return A list of SMT nodes representing composite PK distinctness assertions. + */ + private fun assertForDistinctCompositePK(pkSelectors: List, tableName: String): List { + val nodes = mutableListOf() + for (i in 1..numberOfRows) { + for (j in i + 1..numberOfRows) { + val columnDistinctness = pkSelectors.map { selector -> + DistinctAssertion(listOf( + "(${selector.uppercase()} $tableName$i)", + "(${selector.uppercase()} $tableName$j)" + )) + } + nodes.add(AssertSMTNode(OrAssertion(columnDistinctness))) + } + } + return nodes + } + /** * Appends foreign key constraints for each table to the SMT-LIB. * @@ -368,21 +404,25 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I appendJoinConstraints(smt, sqlQuery, tableAliases) - if (sqlQuery is Select) { // TODO: Handle other queries - val plainSelect = sqlQuery.selectBody as PlainSelect - val where = plainSelect.where + val (where, defaultTable) = when (sqlQuery) { + is Select -> { + val plainSelect = sqlQuery.selectBody as PlainSelect + Pair(plainSelect.where, TablesNamesFinder().getTables(sqlQuery as Statement).firstOrNull()) + } + is Delete -> Pair(sqlQuery.where, sqlQuery.table.getName()) + is Update -> Pair(sqlQuery.where, sqlQuery.table.getName()) + else -> Pair(null, null) + } - if (where != null) { - try { - val condition = parser.parse(where.toString(), toDBType(schema.databaseType)) - val tableFromQuery = TablesNamesFinder().getTables(sqlQuery as Statement).first() - for (i in 1..numberOfRows) { - val constraint = parseQueryCondition(tableAliases, tableFromQuery, condition, i) - smt.addNode(constraint) - } - } catch (e: RuntimeException) { - LoggingUtil.getInfoLogger().warn("Could not translate WHERE clause to SMT-LIB, skipping: ${where}. Reason: ${e.message}") + if (where != null && defaultTable != null) { + try { + val condition = parser.parse(where.toString(), toDBType(schema.databaseType)) + for (i in 1..numberOfRows) { + val constraint = parseQueryCondition(tableAliases, defaultTable, condition, i) + smt.addNode(constraint) } + } catch (e: RuntimeException) { + LoggingUtil.getInfoLogger().warn("Could not translate WHERE clause to SMT-LIB, skipping: ${where}. Reason: ${e.message}") } } } @@ -443,23 +483,35 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I */ private fun extractTableAliases(sqlQuery: Statement): Map { val tableAliasMap = mutableMapOf() - if (sqlQuery is Select) { // TODO: Handle other queries - val plainSelect = sqlQuery.selectBody as PlainSelect - val fromItem = plainSelect.fromItem - if (fromItem != null) { - val tableName = getTableName(fromItem) - val alias = fromItem.alias?.name ?: tableName - tableAliasMap[alias] = tableName - - val joins = plainSelect.joins - if (joins != null) { - for (join in joins) { - val joinAlias = join.rightItem.alias?.name ?: join.rightItem.toString() - val joinName = getTableName(join.rightItem) - tableAliasMap[joinAlias] = joinName + when (sqlQuery) { + is Select -> { + val plainSelect = sqlQuery.selectBody as PlainSelect + val fromItem = plainSelect.fromItem + if (fromItem != null) { + val tableName = getTableName(fromItem) + val alias = fromItem.alias?.name ?: tableName + tableAliasMap[alias] = tableName + + val joins = plainSelect.joins + if (joins != null) { + for (join in joins) { + val joinAlias = join.rightItem.alias?.name ?: join.rightItem.toString() + val joinName = getTableName(join.rightItem) + tableAliasMap[joinAlias] = joinName + } } } } + is Delete -> { + val tableName = sqlQuery.table.getName() + val alias = sqlQuery.table.alias?.name ?: tableName + tableAliasMap[alias] = tableName + } + is Update -> { + val tableName = sqlQuery.table.getName() + val alias = sqlQuery.table.alias?.name ?: tableName + tableAliasMap[alias] = tableName + } } return tableAliasMap } diff --git a/core/src/test/kotlin/org/evomaster/core/solver/SmtLibGeneratorTest.kt b/core/src/test/kotlin/org/evomaster/core/solver/SmtLibGeneratorTest.kt index 742d4dd012..ea53ef243e 100644 --- a/core/src/test/kotlin/org/evomaster/core/solver/SmtLibGeneratorTest.kt +++ b/core/src/test/kotlin/org/evomaster/core/solver/SmtLibGeneratorTest.kt @@ -555,4 +555,79 @@ class SmtLibGeneratorTest { conn.close() } } + + @Test + @Throws(JSQLParserException::class) + fun compositePkEmitsDisjunctiveDistinctness() { + val conn = DriverManager.getConnection("jdbc:h2:mem:composite_pk_test", "sa", "") + try { + SqlScriptRunner.execCommand( + conn, + "CREATE TABLE assignments(employee_id int not null, project_id int not null, PRIMARY KEY (employee_id, project_id));" + ) + val schemaDto = DbInfoExtractor.extract(conn) + val compositePkGenerator = SmtLibGenerator(schemaDto, 2) + + val selectStatement: Statement = CCJSqlParserUtil.parse("SELECT * FROM assignments") + val response: SMTLib = compositePkGenerator.generateSMT(selectStatement) + + val expected = SMTLib() + expected.addNode( + DeclareDatatypeSMTNode( + "AssignmentsRow", ImmutableList.of( + DeclareConstSMTNode("EMPLOYEE_ID", "Int"), + DeclareConstSMTNode("PROJECT_ID", "Int") + ) + ) + ) + expected.addNode(DeclareConstSMTNode("assignments1", "AssignmentsRow")) + expected.addNode(DeclareConstSMTNode("assignments2", "AssignmentsRow")) + // Composite PK: at least one column must differ between row pairs — not each column individually. + expected.addNode(AssertSMTNode(OrAssertion(listOf( + DistinctAssertion(listOf("(EMPLOYEE_ID assignments1)", "(EMPLOYEE_ID assignments2)")), + DistinctAssertion(listOf("(PROJECT_ID assignments1)", "(PROJECT_ID assignments2)")) + )))) + expected.addNode(CheckSatSMTNode()) + expected.addNode(GetValueSMTNode("assignments1")) + expected.addNode(GetValueSMTNode("assignments2")) + + assertEquals(expected, response) + } finally { + conn.close() + } + } + + @Test + @Throws(JSQLParserException::class) + fun deleteFromUsersWithWhereClause() { + val deleteStatement: Statement = CCJSqlParserUtil.parse("DELETE FROM users WHERE age > 30") + + val response: SMTLib = generator.generateSMT(deleteStatement) + + val expected = tableConstraints + expected.addNode(AssertSMTNode(GreaterThanAssertion("(AGE users1)", "30"))) + expected.addNode(AssertSMTNode(GreaterThanAssertion("(AGE users2)", "30"))) + expected.addNode(CheckSatSMTNode()) + expected.addNode(GetValueSMTNode("users1")) + expected.addNode(GetValueSMTNode("users2")) + + assertEquals(expected, response) + } + + @Test + @Throws(JSQLParserException::class) + fun updateUsersWithWhereClause() { + val updateStatement: Statement = CCJSqlParserUtil.parse("UPDATE users SET points = 5 WHERE age > 30") + + val response: SMTLib = generator.generateSMT(updateStatement) + + val expected = tableConstraints + expected.addNode(AssertSMTNode(GreaterThanAssertion("(AGE users1)", "30"))) + expected.addNode(AssertSMTNode(GreaterThanAssertion("(AGE users2)", "30"))) + expected.addNode(CheckSatSMTNode()) + expected.addNode(GetValueSMTNode("users1")) + expected.addNode(GetValueSMTNode("users2")) + + assertEquals(expected, response) + } } From 150146d537ced57a8872a3a30d3b59fdce78288b Mon Sep 17 00:00:00 2001 From: Agustina Aldasoro Date: Wed, 17 Jun 2026 04:23:54 -0300 Subject: [PATCH 7/7] Fix init --- .../org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt b/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt index e94297d5f0..b78d7b8b3e 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt @@ -150,7 +150,7 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { if (collectStats) statistics.reportDseSat(z3TimeMs) z3ResultCache[cacheKey] = z3Result val sqlActions = toSqlActionList(schemaDto, z3Result.model) - if (config.measureDseCorrectness) { + if (::config.isInitialized && config.measureDseCorrectness) { /* * INSERT statements have no WHERE clause, so SqlHeuristicsCalculator has no * predicate to evaluate distance against and will always report a failure.