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-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..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
@@ -13,6 +13,10 @@
import net.sf.jsqlparser.statement.select.Select;
import org.evomaster.dbconstraint.ast.*;
+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;
@@ -45,7 +49,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 +124,10 @@ 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");
+ // 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)));
}
@Override
@@ -599,7 +612,19 @@ 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);
+ }
+ // 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;
+ }
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..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
@@ -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,51 @@ 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());
+ // 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/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..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
@@ -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,22 @@ 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++
+ return
+ }
+ if (sqlDistance == 0.0) {
+ dseCorrectnessZeroDistanceCount++
+ } else {
+ dseCorrectnessNonZeroDistanceCount++
+ }
+ dseCorrectnessAvgDistance.addValue(sqlDistance)
+ }
+
fun getMongoHeuristicsEvaluationCount(): Int = mongoHeuristicEvaluationSuccessCount + mongoHeuristicEvaluationFailureCount
fun getSqlHeuristicsEvaluationCount(): Int = sqlHeuristicEvaluationSuccessCount + sqlHeuristicEvaluationFailureCount
@@ -441,6 +464,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 430b287759..b78d7b8b3e 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
@@ -11,10 +12,17 @@ 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
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
@@ -141,7 +149,30 @@ 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.isInitialized && config.measureDseCorrectness) {
+ /*
+ * 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
+ )
+ }
+ }
+ sqlActions
}
Z3Result.Status.UNSAT -> {
if (collectStats) statistics.reportDseUnsat(z3TimeMs)
@@ -426,4 +457,60 @@ 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(schemaDto, sqlActions)
+ val calculator = SqlHeuristicsCalculator.SqlHeuristicsCalculatorBuilder()
+ .withTableColumnResolver(TableColumnResolver(schemaDto))
+ .withSourceQueryResultSet(queryResultSet)
+ .build()
+ return calculator.computeDistance(sqlQuery)
+ }
+
+ private fun toQueryResultSet(schemaDto: DbInfoDto, 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)
+ }
+ // 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
+ }
+
+ private fun extractGeneValue(gene: Gene): Any? {
+ 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 -> {
+ 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()
+ }
+ }
+ }
}
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)
+ }
}
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*: `""`.|