Restore experimental Z3 SQL correctness-measurement feature

core/pom.xml

@@ -46,6 +46,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

@@ -1972,6 +1972,14 @@ class EMConfig {
     @DependsOnTrueFor("generateSqlDataWithZ3")
     var collectSqlZ3Stats = false
 
+    @Experimental
+    @Cfg("Measure the correctness of Z3-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 generateSqlDataWithZ3=true.")
+    @DependsOnTrueFor("generateSqlDataWithZ3")
+    var measureSqlZ3Correctness = false
+
     @Experimental
     @Cfg("Soft timeout, in milliseconds, for each Z3 solver invocation when generating SQL data. " +
             "If a query exceeds it, Z3 returns 'unknown' for that query instead of running unbounded. " +

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

@@ -104,6 +104,13 @@ class Statistics : SearchListener {
     private val sqlZ3SeenQueryHashes = mutableSetOf<Int>()
     private var sqlZ3UniqueQueriesCount = 0
 
+    // Z3-based SQL data generation correctness distance statistics (only when measureSqlZ3Correctness=true)
+    private var sqlZ3CorrectnessCheckCount = 0
+    private var sqlZ3CorrectnessZeroDistanceCount = 0
+    private var sqlZ3CorrectnessNonZeroDistanceCount = 0
+    private val sqlZ3CorrectnessAvgDistance = IncrementalAverage()
+    private var sqlZ3CorrectnessEvalFailureCount = 0
+
     // mongo heuristic evaluation statistic
     private var mongoHeuristicEvaluationSuccessCount = 0
     private var mongoHeuristicEvaluationFailureCount = 0
@@ -301,6 +308,22 @@ class Statistics : SearchListener {
     internal fun getSqlZ3CacheHitCount() = sqlZ3CacheHitCount
     internal fun getSqlZ3CacheMissCount() = sqlZ3CacheMissCount
 
+    fun reportSqlZ3CorrectnessDistance(sqlDistance: Double, evaluationFailure: Boolean) {
+        sqlZ3CorrectnessCheckCount++
+        if (evaluationFailure) {
+            // sqlDistance is a sentinel value (e.g. Double.MAX_VALUE) in this case,
+            // and must not pollute the average of real distances
+            sqlZ3CorrectnessEvalFailureCount++
+            return
+        }
+        if (sqlDistance == 0.0) {
+            sqlZ3CorrectnessZeroDistanceCount++
+        } else {
+            sqlZ3CorrectnessNonZeroDistanceCount++
+        }
+        sqlZ3CorrectnessAvgDistance.addValue(sqlDistance)
+    }
+
     fun getMongoHeuristicsEvaluationCount(): Int = mongoHeuristicEvaluationSuccessCount + mongoHeuristicEvaluationFailureCount
 
     fun getSqlHeuristicsEvaluationCount(): Int = sqlHeuristicEvaluationSuccessCount + sqlHeuristicEvaluationFailureCount
@@ -477,6 +500,15 @@ class Statistics : SearchListener {
                 add(Pair("sqlZ3AvgSmtlibSizeBytes", "%.1f".format(sqlZ3SmtlibSizeBytes.mean)))
             }
 
+            // correctness distance stats (only emitted when measureSqlZ3Correctness=true)
+            if (config.measureSqlZ3Correctness) {
+                add(Pair("sqlZ3CorrectnessChecks",      "$sqlZ3CorrectnessCheckCount"))
+                add(Pair("sqlZ3CorrectnessZeroDistance", "$sqlZ3CorrectnessZeroDistanceCount"))
+                add(Pair("sqlZ3CorrectnessNonZero",      "$sqlZ3CorrectnessNonZeroDistanceCount"))
+                add(Pair("sqlZ3CorrectnessAvgDist",      "%.4f".format(sqlZ3CorrectnessAvgDistance.mean)))
+                add(Pair("sqlZ3CorrectnessEvalFailures", "$sqlZ3CorrectnessEvalFailureCount"))
+            }
+
             for(phase in ExecutionPhaseController.Phase.entries){
                 add(Pair("phase_${phase.name}", "${epc.getPhaseDurationInSeconds(phase)}"))
             }

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

@@ -5,13 +5,20 @@ 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
@@ -205,7 +212,33 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver {
             Z3Result.Status.SAT -> {
                 stats?.reportSqlZ3Sat(z3TimeMs)
                 z3ResultCache?.set(cacheKey, z3Result)
-                toSqlActionList(schemaDto, z3Result.solution)
+                val sqlActions = toSqlActionList(schemaDto, z3Result.solution)
+                if (::config.isInitialized && config.measureSqlZ3Correctness && queryStatement !is Insert) {
+                    /*
+                     * 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 Z3 SQL generation currently leaves unconstrained.
+                     *
+                     * Note: SqlHeuristicsCalculator is SELECT-oriented. For DELETE/UPDATE the distance
+                     * computation may fail and be reported as an evaluation failure (sqlDistanceEvaluationFailure)
+                     * rather than a real distance; such failures are counted separately and are excluded
+                     * from the average, so they do not distort the correctness metric.
+                     */
+                    val distResult = computeCorrectnessDistance(sqlQuery, schemaDto, sqlActions)
+                    if (distResult.sqlDistanceEvaluationFailure) {
+                        LoggingUtil.getInfoLogger().warn("SQL-Z3: correctness evaluation failure for query '$sqlQuery'")
+                    } else if (distResult.sqlDistance != 0.0) {
+                        LoggingUtil.getInfoLogger().warn("SQL-Z3: non-zero correctness distance (${distResult.sqlDistance}) for query '$sqlQuery'")
+                    }
+                    statisticsRef?.get()?.reportSqlZ3CorrectnessDistance(
+                        distResult.sqlDistance,
+                        distResult.sqlDistanceEvaluationFailure
+                    )
+                }
+                sqlActions
             }
             Z3Result.Status.UNSAT -> {
                 stats?.reportSqlZ3Unsat(z3TimeMs)
@@ -519,4 +552,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(
+                    "SQL-Z3: extractGeneValue() fallback to raw string for unhandled gene type " +
+                            "${inner.javaClass.name} (outer: ${gene.javaClass.name}, name: ${gene.name})"
+                )
+                inner.getValueAsRawString()
+            }
+        }
+    }
 }

docs/options.md

@@ -328,6 +328,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`.|
+|`measureSqlZ3Correctness`| __Boolean__. Measure the correctness of Z3-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 generateSqlDataWithZ3=true. *Depends on*: `generateSqlDataWithZ3=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`.|
 |`prematureStopStrategy`| __Enum__. Specify how 'improvement' is defined: either any kind of improvement even if partial (ANY), or at least one new target is fully covered (NEW). *Valid values*: `ANY, NEW`. *Default value*: `NEW`.|