diff --git a/core/pom.xml b/core/pom.xml index 833531fc7e..93912d71d3 100644 --- a/core/pom.xml +++ b/core/pom.xml @@ -46,6 +46,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 651d797745..48e94683b2 100644 --- a/core/src/main/kotlin/org/evomaster/core/EMConfig.kt +++ b/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. " + 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 b91b4846c5..4375472f7f 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 @@ -104,6 +104,13 @@ class Statistics : SearchListener { private val sqlZ3SeenQueryHashes = mutableSetOf() 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)}")) } 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 9f1960e10a..d5c672271f 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt @@ -5,6 +5,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 @@ -12,6 +13,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 @@ -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 + ): 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( + "SQL-Z3: extractGeneValue() fallback to raw string for unhandled gene type " + + "${inner.javaClass.name} (outer: ${gene.javaClass.name}, name: ${gene.name})" + ) + inner.getValueAsRawString() + } + } + } } diff --git a/docs/options.md b/docs/options.md index f51c573d3f..0d5ab6dde6 100644 --- a/docs/options.md +++ b/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`.|