Correctness statistics for DSE

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);
         }
     }

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");
     }
 

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());
+    }
+
 }

core/pom.xml

@@ -33,6 +33,10 @@
             <groupId>org.evomaster</groupId>
             <artifactId>evomaster-client-java-controller-api</artifactId>
         </dependency>
+        <dependency>
+            <groupId>org.evomaster</groupId>
+            <artifactId>evomaster-client-java-sql</artifactId>
+        </dependency>
         <dependency>
             <groupId>org.evomaster</groupId>
             <artifactId>evomaster-client-java-instrumentation-shared</artifactId>

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

core/src/main/kotlin/org/evomaster/core/search/service/Statistics.kt

@@ -98,6 +98,13 @@ class Statistics : SearchListener {
     private val dseSeenQueryHashes = mutableSetOf<Int>()
     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)}"))
             }

core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt

@@ -4,17 +4,25 @@ 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
 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)
@@ -226,7 +257,7 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver {
                             )
                             ImmutableDataHolderGene(dbColumnName, formatted, inQuotes = true)
                         } else {
-                            IntegerGene(dbColumnName, columnValue.value.toInt())
+                            LongGene(dbColumnName, columnValue.value.toLong())
                         }
                     }
                     is RealValue -> {
@@ -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<SqlAction>
+    ): 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<SqlAction>): 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<Any?> = 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()
+            }
+        }
+    }
 }