From d03d8eca104497821954865e20505a6bdccefb12 Mon Sep 17 00:00:00 2001 From: Agustina Aldasoro Date: Sat, 27 Jun 2026 11:06:14 -0300 Subject: [PATCH 1/3] Add DSE Memoization and time statistics --- .../evomaster/solver/Z3DockerExecutor.java | 30 +++-- .../java/org/evomaster/solver/Z3Result.java | 46 +++++++ .../solver/Z3DockerExecutorTest.java | 57 ++++---- .../kotlin/org/evomaster/core/EMConfig.kt | 7 + .../core/search/service/Statistics.kt | 60 +++++++++ .../core/solver/SMTLibZ3DbConstraintSolver.kt | 127 ++++++++++++++---- docs/options.md | 1 + 7 files changed, 257 insertions(+), 71 deletions(-) create mode 100644 core-extra/solver/src/main/java/org/evomaster/solver/Z3Result.java diff --git a/core-extra/solver/src/main/java/org/evomaster/solver/Z3DockerExecutor.java b/core-extra/solver/src/main/java/org/evomaster/solver/Z3DockerExecutor.java index eeb196eb93..f618363c43 100644 --- a/core-extra/solver/src/main/java/org/evomaster/solver/Z3DockerExecutor.java +++ b/core-extra/solver/src/main/java/org/evomaster/solver/Z3DockerExecutor.java @@ -54,28 +54,34 @@ public Z3DockerExecutor(String resourcesFolder) { * The file must be in the directory specified by containerPath. * * @param fileName the name of the SMT-LIB file to read and solve - * @return the result of the Z3 solver as a map of variable names to their values, if the problem is satisfiable (sat) - * or an empty Optional if the problem is unsatisfiable (unsat) + * @return a {@link Z3Result} with status SAT (and the model), UNSAT, or ERROR */ - public Optional> solveFromFile(String fileName) { + public Z3Result solveFromFile(String fileName) { try { - // Execute the Z3 solver on the specified file in the container Container.ExecResult result = z3Prover.execInContainer("z3", containerPath + fileName); + if (result.getExitCode() != 0) { - throw new RuntimeException("Error executing Z3 solver: \n" + result.getStdout() + "\n" + result.getStderr()); + return Z3Result.error("Z3 exited with code " + result.getExitCode() + + ": " + result.getStdout() + result.getStderr()); } + String stdout = result.getStdout(); + if (stdout == null || stdout.trim().isEmpty()) { + return Z3Result.error("Z3 produced no output for file: " + fileName + + " stderr: " + result.getStderr()); + } - // Check if the solver returned any output - if (stdout == null || stdout.isEmpty()) { - String stderr = result.getStderr(); - throw new RuntimeException("No result after solving file " + stderr); + if (stdout.trim().startsWith("unsat")) { + return Z3Result.unsat(); } - // Parse the solver output and return the result - return Optional.of(SMTResultParser.parseZ3Response(stdout)); + Map model = SMTResultParser.parseZ3Response(stdout); + return Z3Result.sat(model); + } catch (IOException | InterruptedException e) { - return Optional.empty(); + return Z3Result.error("I/O or interruption error running Z3 on " + fileName + ": " + e.getMessage()); + } catch (RuntimeException e) { + return Z3Result.error("Unexpected error parsing Z3 output for " + fileName + ": " + e.getMessage()); } } diff --git a/core-extra/solver/src/main/java/org/evomaster/solver/Z3Result.java b/core-extra/solver/src/main/java/org/evomaster/solver/Z3Result.java new file mode 100644 index 0000000000..ca26f86cb1 --- /dev/null +++ b/core-extra/solver/src/main/java/org/evomaster/solver/Z3Result.java @@ -0,0 +1,46 @@ +package org.evomaster.solver; + +import org.evomaster.solver.smtlib.value.SMTLibValue; + +import java.util.Map; + +/** + * Represents the outcome of a Z3 solver invocation. + * Distinguishes between three possible states: SAT (satisfiable with a model), + * UNSAT (unsatisfiable), and ERROR (solver or parsing failure). + */ +public class Z3Result { + + public enum Status { + /** Z3 found a satisfying assignment. The model is available. */ + SAT, + /** The problem is unsatisfiable. No model exists. */ + UNSAT, + /** A solver, I/O, or parsing error occurred. */ + ERROR + } + + public final Status status; + /** Non-null only when status == SAT. */ + public final Map model; + /** Non-null only when status == ERROR. */ + public final String errorMessage; + + private Z3Result(Status status, Map model, String errorMessage) { + this.status = status; + this.model = model; + this.errorMessage = errorMessage; + } + + public static Z3Result sat(Map model) { + return new Z3Result(Status.SAT, model, null); + } + + public static Z3Result unsat() { + return new Z3Result(Status.UNSAT, null, null); + } + + public static Z3Result error(String message) { + return new Z3Result(Status.ERROR, null, message); + } +} diff --git a/core-extra/solver/src/test/java/org/evomaster/solver/Z3DockerExecutorTest.java b/core-extra/solver/src/test/java/org/evomaster/solver/Z3DockerExecutorTest.java index 9cc66bfebd..2a447d688c 100644 --- a/core-extra/solver/src/test/java/org/evomaster/solver/Z3DockerExecutorTest.java +++ b/core-extra/solver/src/test/java/org/evomaster/solver/Z3DockerExecutorTest.java @@ -15,7 +15,6 @@ import java.nio.file.StandardCopyOption; import java.util.HashMap; import java.util.Map; -import java.util.Optional; import static org.junit.jupiter.api.Assertions.*; @@ -43,13 +42,13 @@ static void tearDown() { */ @Test public void satisfiabilityExample() { - Optional> response = executor.solveFromFile("example.smt"); + Z3Result result = executor.solveFromFile("example.smt"); - assertTrue(response.isPresent()); - assertEquals(2, response.get().size()); + assertEquals(Z3Result.Status.SAT, result.status); + assertEquals(2, result.model.size()); - assertEquals(new LongValue(0L), response.get().get("y")); - assertEquals(new LongValue((long) -4), response.get().get("x")); + assertEquals(new LongValue(0L), result.model.get("y")); + assertEquals(new LongValue((long) -4), result.model.get("x")); } /** @@ -64,14 +63,14 @@ public void dynamicFile() throws IOException { Files.copy(originalPath, copied, StandardCopyOption.REPLACE_EXISTING); - Optional> response; + Z3Result result; try { - response = executor.solveFromFile("example2.smt"); + result = executor.solveFromFile("example2.smt"); } finally { - Files.deleteIfExists(copied); // Ensure the file is deleted + Files.deleteIfExists(copied); } - assertTrue(response.isPresent()); + assertEquals(Z3Result.Status.SAT, result.status); } /** @@ -79,11 +78,11 @@ public void dynamicFile() throws IOException { */ @Test public void uniqueUInt() { - Optional> response = executor.solveFromFile("unique_uint.smt"); + Z3Result result = executor.solveFromFile("unique_uint.smt"); - assertTrue(response.isPresent(), "Response should be present for unique_uint.smt"); - assertEquals(new LongValue(2L), response.get().get("id_1"), "The value for id_1 should be 2"); - assertEquals(new LongValue(3L), response.get().get("id_2"), "The value for id_2 should be 3"); + assertEquals(Z3Result.Status.SAT, result.status, "Response should be SAT for unique_uint.smt"); + assertEquals(new LongValue(2L), result.model.get("id_1"), "The value for id_1 should be 2"); + assertEquals(new LongValue(3L), result.model.get("id_2"), "The value for id_2 should be 3"); } /** @@ -91,47 +90,45 @@ public void uniqueUInt() { */ @Test public void composedTypes() { - Optional> response = executor.solveFromFile("composed_types.smt"); + Z3Result result = executor.solveFromFile("composed_types.smt"); - assertTrue(response.isPresent(), "Response should be present for composed_types.smt"); + assertEquals(Z3Result.Status.SAT, result.status, "Response should be SAT for composed_types.smt"); - assertTrue(response.get().containsKey("users1"), "Response should contain users1"); + assertTrue(result.model.containsKey("users1"), "Response should contain users1"); Map users1Expected = new HashMap<>(); users1Expected.put("ID", new LongValue(3L)); users1Expected.put("NAME", new StringValue("agus")); users1Expected.put("AGE", new LongValue(31L)); users1Expected.put("POINTS", new LongValue(7L)); - assertEquals(new StructValue(users1Expected), response.get().get("users1"), "The value for users1 is incorrect"); + assertEquals(new StructValue(users1Expected), result.model.get("users1"), "The value for users1 is incorrect"); - assertTrue(response.get().containsKey("users2"), "Response should contain users2"); + assertTrue(result.model.containsKey("users2"), "Response should contain users2"); Map users2Expected = new HashMap<>(); users2Expected.put("ID", new LongValue(3L)); users2Expected.put("NAME", new StringValue("agus")); users2Expected.put("AGE", new LongValue(31L)); users2Expected.put("POINTS", new LongValue(7L)); - assertEquals(new StructValue(users2Expected), response.get().get("users2"), "The value for users2 is incorrect"); + assertEquals(new StructValue(users2Expected), result.model.get("users2"), "The value for users2 is incorrect"); } /** * Test solving with an invalid file to ensure proper error handling */ @Test - public void whenSolvingInvalidFileItFails() { - assertThrows( - RuntimeException.class, - () -> executor.solveFromFile("invalid.smt") - ); + public void whenSolvingInvalidFileItReturnsError() { + Z3Result result = executor.solveFromFile("invalid.smt"); + assertEquals(Z3Result.Status.ERROR, result.status); + assertNotNull(result.errorMessage); } /** * Test handling an empty file */ @Test - public void whenSolvingEmptyFileItFails() { - assertThrows( - RuntimeException.class, - () -> executor.solveFromFile("empty.smt") - ); + public void whenSolvingEmptyFileItReturnsError() { + Z3Result result = executor.solveFromFile("empty.smt"); + assertEquals(Z3Result.Status.ERROR, result.status); + assertNotNull(result.errorMessage); } } diff --git a/core/src/main/kotlin/org/evomaster/core/EMConfig.kt b/core/src/main/kotlin/org/evomaster/core/EMConfig.kt index e873d22342..570e374419 100644 --- a/core/src/main/kotlin/org/evomaster/core/EMConfig.kt +++ b/core/src/main/kotlin/org/evomaster/core/EMConfig.kt @@ -1920,6 +1920,13 @@ class EMConfig { @DependsOnFalseFor("blackBox") var generateSqlDataWithDSE = false + @Experimental + @Cfg("Collect detailed statistics for DSE SQL generation: SAT/UNSAT/error counts, " + + "query uniqueness, Z3 execution time, and SMT-LIB generation time. " + + "Only meaningful when generateSqlDataWithDSE=true.") + @DependsOnTrueFor("generateSqlDataWithDSE") + var collectDseStats = 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 94da2c063a..79deb19a78 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 @@ -86,6 +86,18 @@ class Statistics : SearchListener { private var sqlHeuristicEvaluationFailureCount = 0; private val sqlRowsAverageCalculator = IncrementalAverage() + // DSE (Dynamic Symbolic Execution) statistics + private var dseTotalQueriesProcessed = 0 + private var dseSatCount = 0 + private var dseUnsatCount = 0 + private var dseErrorCount = 0 + private var dseParseFailureCount = 0 + private var dseZ3TimeMs = 0L + private var dseSmtlibGenTimeMs = 0L + private val dseSmtlibSizeBytes = IncrementalAverage() + private val dseSeenQueryHashes = mutableSetOf() + private var dseUniqueQueriesCount = 0 + // mongo heuristic evaluation statistic private var mongoHeuristicEvaluationSuccessCount = 0 private var mongoHeuristicEvaluationFailureCount = 0 @@ -223,6 +235,40 @@ class Statistics : SearchListener { redisHeuristicEvaluationFailureCount++ } + fun reportDseSat(z3TimeMs: Long) { + dseTotalQueriesProcessed++ + dseSatCount++ + dseZ3TimeMs += z3TimeMs + } + + fun reportDseUnsat(z3TimeMs: Long) { + dseTotalQueriesProcessed++ + dseUnsatCount++ + dseZ3TimeMs += z3TimeMs + } + + fun reportDseError(z3TimeMs: Long) { + dseTotalQueriesProcessed++ + dseErrorCount++ + dseZ3TimeMs += z3TimeMs + } + + fun reportDseParseFailure() { + dseTotalQueriesProcessed++ + dseParseFailureCount++ + } + + fun reportDseSmtlibGenTime(ms: Long, sizeBytes: Int) { + dseSmtlibGenTimeMs += ms + dseSmtlibSizeBytes.addValue(sizeBytes) + } + + fun reportDseQuerySeen(queryHash: Int) { + if (dseSeenQueryHashes.add(queryHash)) { + dseUniqueQueriesCount++ + } + } + fun getMongoHeuristicsEvaluationCount(): Int = mongoHeuristicEvaluationSuccessCount + mongoHeuristicEvaluationFailureCount fun getSqlHeuristicsEvaluationCount(): Int = sqlHeuristicEvaluationSuccessCount + sqlHeuristicEvaluationFailureCount @@ -381,6 +427,20 @@ class Statistics : SearchListener { add(Pair("sqlHeuristicsEvaluationFailures","$sqlHeuristicEvaluationFailureCount" )) add(Pair("sqlHeuristicsEvaluationCount","${getSqlHeuristicsEvaluationCount()}")) + // statistics info for DSE (only emitted when collectDseStats=true) + if (config.collectDseStats) { + add(Pair("dseTotalQueries", "$dseTotalQueriesProcessed")) + add(Pair("dseUniqueQueries", "$dseUniqueQueriesCount")) + add(Pair("dseDuplicateQueries", "${dseTotalQueriesProcessed - dseParseFailureCount - dseUniqueQueriesCount}")) + add(Pair("dseSat", "$dseSatCount")) + add(Pair("dseUnsat", "$dseUnsatCount")) + add(Pair("dseErrors", "$dseErrorCount")) + add(Pair("dseParseFailures", "$dseParseFailureCount")) + add(Pair("dseZ3TotalMs", "$dseZ3TimeMs")) + add(Pair("dseSmtlibGenTotalMs", "$dseSmtlibGenTimeMs")) + add(Pair("dseAvgSmtlibSizeBytes", "%.1f".format(dseSmtlibSizeBytes.mean))) + } + 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 46afa64c2a..14f5fc3367 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt @@ -1,6 +1,7 @@ package org.evomaster.core.solver import com.google.inject.Inject + import net.sf.jsqlparser.JSQLParserException import net.sf.jsqlparser.parser.CCJSqlParserUtil import net.sf.jsqlparser.statement.Statement @@ -18,14 +19,17 @@ import org.evomaster.core.search.gene.numeric.IntegerGene import org.evomaster.core.search.gene.placeholder.ImmutableDataHolderGene import org.evomaster.core.search.gene.sql.SqlPrimaryKeyGene import org.evomaster.core.search.gene.string.StringGene +import org.evomaster.core.search.service.Statistics import org.evomaster.core.sql.SqlAction import org.evomaster.core.sql.schema.* import org.evomaster.core.utils.StringUtils.convertToAscii import org.evomaster.solver.Z3DockerExecutor +import org.evomaster.solver.Z3Result import org.evomaster.solver.smtlib.SMTLib import org.evomaster.solver.smtlib.value.* import java.io.File import java.io.IOException +import java.lang.ref.WeakReference import java.nio.charset.StandardCharsets import java.nio.file.Files import java.nio.file.Paths @@ -54,13 +58,42 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { private lateinit var executor: Z3DockerExecutor private var idCounter: Long = 0L + // Null until DSE is enabled in postConstruct — avoids allocating the map in runs where DSE is off. + private var z3ResultCache: MutableMap, Z3Result>? = null + + companion object { + private const val MAX_CACHE_SIZE = 500 + } + @Inject private lateinit var config: EMConfig + /* + Held WEAKLY on purpose. This solver has @PreDestroy, so each instance is + retained by Governator's predestroy-monitor thread (a GC root) for the whole + lifetime of the JVM. A strong reference to Statistics would therefore pin + Statistics -> Archive -> every individual, leaking across every injector ever + created. That is harmless in production (a single injector, process exits) but + OOMs test suites that build thousands of injectors (RestIndividualTestBase, + SamplerVerifierTest). A weak reference lets that graph be collected once the + owning injector is otherwise unreachable, while still resolving fine during an + active search (Statistics is strongly held by SearchTimeController then). + */ + private var statisticsRef: WeakReference? = null + + @Inject(optional = true) + fun setStatistics(statistics: Statistics) { + this.statisticsRef = WeakReference(statistics) + } + @PostConstruct private fun postConstruct() { if (config.generateSqlDataWithDSE) { initializeExecutor() + z3ResultCache = object : LinkedHashMap, Z3Result>(16, 0.75f, true) { + override fun removeEldestEntry(eldest: MutableMap.MutableEntry, Z3Result>?) = + size > MAX_CACHE_SIZE + } } } @@ -73,7 +106,9 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { */ @PreDestroy override fun close() { - executor.close() + if (::executor.isInitialized) { + executor.close() + } try { FileUtils.cleanDirectory(File(resourcesFolder)) } catch (e: IOException) { @@ -86,18 +121,67 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { * and returns a list of SqlActions that satisfy the query. * * @param sqlQuery The SQL query to solve. - * @return A list of SQL actions that can be executed to satisfy the query. + * @return A list of SQL actions that can be executed to satisfy the query, + * or an empty list if the problem is UNSAT, unparseable, or an error occurred. */ override fun solve(schemaDto: DbInfoDto, sqlQuery: String, numberOfRows: Int): List { - // TODO: Use memoized, if it's the same schema and query, return the same result and don't do any calculation + val collectStats = ::config.isInitialized && config.collectDseStats + val stats: Statistics? = if (collectStats) statisticsRef?.get() else null + + stats?.reportDseQuerySeen(sqlQuery.hashCode()) + + val cacheKey = Pair(sqlQuery, numberOfRows) + val cached = z3ResultCache?.get(cacheKey) + if (cached != null) { + return when (cached.status) { + Z3Result.Status.SAT -> toSqlActionList(schemaDto, cached.model) + else -> emptyList() + } + } + val queryStatement = try { + parseStatement(sqlQuery) + } catch (e: RuntimeException) { + LoggingUtil.getInfoLogger().warn("DSE: failed to parse SQL query as SMT-LIB: '$sqlQuery'") + stats?.reportDseParseFailure() + return emptyList() + } + + val smtlibGenStart = System.currentTimeMillis() val generator = SmtLibGenerator(schemaDto, numberOfRows) - val queryStatement = parseStatement(sqlQuery) val smtLib = generator.generateSMT(queryStatement) + val smtlibBytes = smtLib.toString().toByteArray(StandardCharsets.UTF_8).size + val smtlibGenMs = System.currentTimeMillis() - smtlibGenStart + stats?.reportDseSmtlibGenTime(smtlibGenMs, smtlibBytes) + val fileName = storeToTmpFile(smtLib) - val z3Response = executor.solveFromFile(fileName) - return toSqlActionList(schemaDto, z3Response) + val z3Start = System.currentTimeMillis() + val z3Result = try { + executor.solveFromFile(fileName) + } finally { + Files.deleteIfExists(Paths.get(leadingBarResourcesFolder() + fileName)) + } + val z3TimeMs = System.currentTimeMillis() - z3Start + + return when (z3Result.status) { + Z3Result.Status.SAT -> { + stats?.reportDseSat(z3TimeMs) + z3ResultCache?.set(cacheKey, z3Result) + toSqlActionList(schemaDto, z3Result.model) + } + Z3Result.Status.UNSAT -> { + stats?.reportDseUnsat(z3TimeMs) + z3ResultCache?.set(cacheKey, z3Result) + emptyList() + } + Z3Result.Status.ERROR -> { + LoggingUtil.getInfoLogger().warn("DSE: Z3 error for query '$sqlQuery': ${z3Result.errorMessage}") + stats?.reportDseError(z3TimeMs) + // Errors are not cached — they may be transient Docker failures + emptyList() + } + } } /** @@ -125,35 +209,24 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { } /** - * Converts Z3's response to a list of SqlActions. + * Converts Z3's model to a list of SqlActions. * - * @param z3Response The response from Z3. + * @param model The satisfying assignment from Z3 (non-null, status must be SAT). * @return A list of SQL actions. */ - private fun toSqlActionList(schemaDto: DbInfoDto, z3Response: Optional>): List { - if (!z3Response.isPresent) { - return emptyList() - } - + private fun toSqlActionList(schemaDto: DbInfoDto, model: Map): List { val actions = mutableListOf() - for (row in z3Response.get()) { + for (row in model) { val tableName = getTableName(row.key) val columns = row.value as StructValue - // Find table from schema and create SQL actions val table = findTableByName(schemaDto, tableName) - /* - * The invariant requires that action.insertionId == primaryKey.uniqueId (and same for FK). - * So we must use the same id for the action and all its PK/FK genes. - */ val actionId = idCounter idCounter++ - // Create the list of genes with the values val genes = mutableListOf() - // smtColumn is the Ascii version from SmtLib; resolve back to original DB column name for (smtColumn in columns.fields) { val dbColumn = table.columns.firstOrNull { convertToAscii(it.name).equals(smtColumn, ignoreCase = true) @@ -232,7 +305,7 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { * @return The extracted table name. */ private fun getTableName(key: String): String { - return key.substring(0, key.length - 1) // Remove last character + return key.substring(0, key.length - 1) } /** @@ -247,7 +320,7 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { ?: throw RuntimeException("Table not found: $tableName") return Table( TableId.fromDto(schema.databaseType, tableDto.id), - findColumns(schema,tableDto), // Convert columns from DTO + findColumns(schema, tableDto), findForeignKeys(tableDto) // TODO: Implement this method ) } @@ -337,13 +410,13 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { "TIMESTAMP" -> ColumnDataType.TIMESTAMP "CHARACTER VARYING" -> ColumnDataType.CHARACTER_VARYING "CHAR" -> ColumnDataType.CHAR - else -> ColumnDataType.CHARACTER_VARYING // Default type + else -> ColumnDataType.CHARACTER_VARYING } } // TODO: Implement this method private fun findForeignKeys(tableDto: TableDto): Set { - return emptySet() // Placeholder + return emptySet() } /** @@ -358,23 +431,19 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { val fileExtension = ".smt2" try { - // Create dir if it doesn't exist val directory = Paths.get(directoryPath) if (!directory.exists()) { directory.createDirectories() } - // Generate a unique file name var fileName = "$fileNameBase$fileExtension" var filePath = directory.resolve(fileName) if (filePath.exists()) { - // Add a random suffix to the file name if it already exists val randomSuffix = (1000..9999).random() fileName = "${fileNameBase}_$randomSuffix$fileExtension" filePath = directory.resolve(fileName) } - // Write the SMTLib content to the file Files.write(filePath, smtLib.toString().toByteArray(StandardCharsets.UTF_8)) return fileName diff --git a/docs/options.md b/docs/options.md index 0deff472c9..e65cd1466d 100644 --- a/docs/options.md +++ b/docs/options.md @@ -274,6 +274,7 @@ There are 3 types of options: |`callbackURLHostname`| __String__. HTTP callback verifier hostname. Default is set to 'localhost'. If the SUT is running inside a container (i.e., Docker), 'localhost' will refer to the container. This can be used to change the hostname. *Default value*: `localhost`.| |`cgaNeighborhoodModel`| __Enum__. Cellular GA: neighborhood model (RING, L5, C9, C13). *Valid values*: `RING, L5, C9, C13`. *Default value*: `RING`.| |`classificationRepairThreshold`| __Double__. If using THRESHOLD for AI Classification Repair, specify its value. All classifications with probability equal or above such threshold value will be accepted. *Constraints*: `probability 0.0-1.0`. *Default value*: `0.5`.| +|`collectDseStats`| __Boolean__. Collect detailed statistics for DSE SQL generation: SAT/UNSAT/error counts, query uniqueness, Z3 execution time, and SMT-LIB generation time. Only meaningful when generateSqlDataWithDSE=true. *Depends on*: `generateSqlDataWithDSE=true`. *Default value*: `false`.| |`discoveredInfoRewardedInFitness`| __Boolean__. If there is new discovered information from a test execution, reward it in the fitness function. *Default value*: `false`.| |`dockerLocalhost`| __Boolean__. Replace references to 'localhost' to point to the actual host machine. Only needed when running EvoMaster inside Docker. *Default value*: `false`.| |`dpcTargetTestSize`| __Int__. Specify a max size of a test to be targeted when either DPC_INCREASING or DPC_DECREASING is enabled. *Default value*: `1`.| From 406c40125678fb3e19ef303ca81b4a849d0cbc8b Mon Sep 17 00:00:00 2001 From: Agustina Aldasoro Date: Sat, 27 Jun 2026 11:09:13 -0300 Subject: [PATCH 2/3] Correctness statistics for DSE (#1587) --- .../heuristic/SqlHeuristicsCalculator.java | 3 +- .../dbconstraint/parser/jsql/JSqlVisitor.java | 33 +++++- .../parser/JSqlConditionParserTest.java | 51 +++++++- core/pom.xml | 19 +++ .../kotlin/org/evomaster/core/EMConfig.kt | 8 ++ .../core/search/service/Statistics.kt | 32 +++++ .../core/solver/SMTLibZ3DbConstraintSolver.kt | 68 ++++++++++- .../evomaster/core/solver/SmtLibGenerator.kt | 112 +++++++++++++----- .../core/search/gene/AbstractGeneTest.kt | 21 ++++ .../solver/SMTLibZ3DbConstraintSolverTest.kt | 14 +-- .../core/solver/SmtLibGeneratorTest.kt | 75 ++++++++++++ docs/options.md | 1 + 12 files changed, 392 insertions(+), 45 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-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..cfd4a3878d 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 @@ -474,6 +478,21 @@ org.antlr antlr4-maven-plugin + + + + org.apache.maven.plugins + maven-surefire-plugin + + @{argLine} -ea -Xms1024m -Xmx5120m -Xss4m -Dfile.encoding=UTF-8 -Djdk.attach.allowAttachSelf=true -Duser.language=en -Duser.country=GB ${addOpens} + + 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 14f5fc3367..0084a47dbe 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,10 +13,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 @@ -58,6 +66,8 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { private lateinit var executor: Z3DockerExecutor private var idCounter: Long = 0L + // Memoization cache: (sqlQuery, numberOfRows) -> Z3Result (SAT or UNSAT only; errors are not cached) + // Schema is assumed stable within a single run, so only query + row count form the key. // Null until DSE is enabled in postConstruct — avoids allocating the map in runs where DSE is off. private var z3ResultCache: MutableMap, Z3Result>? = null @@ -253,7 +263,7 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { ) ImmutableDataHolderGene(dbColumnName, formatted, inQuotes = true) } else { - IntegerGene(dbColumnName, columnValue.value.toInt()) + LongGene(dbColumnName, columnValue.value.toLong()) } } is RealValue -> { @@ -453,4 +463,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/search/gene/AbstractGeneTest.kt b/core/src/test/kotlin/org/evomaster/core/search/gene/AbstractGeneTest.kt index 31f26a040f..9546605b35 100644 --- a/core/src/test/kotlin/org/evomaster/core/search/gene/AbstractGeneTest.kt +++ b/core/src/test/kotlin/org/evomaster/core/search/gene/AbstractGeneTest.kt @@ -1,11 +1,32 @@ package org.evomaster.core.search.gene +import org.evomaster.core.search.gene.collection.EnumGene import org.evomaster.core.search.service.Randomness +import org.junit.jupiter.api.AfterAll +import org.junit.jupiter.api.AfterEach abstract class AbstractGeneTest { protected val geneClasses = GeneSamplerForTests.geneClasses + @AfterEach + fun cleanCaches() { + EnumGene.cleanCache() + } + + companion object { + /* + * After each test class finishes its (potentially 1000+) seeds, hint the JVM to run + * a full GC before the next class starts. Without this, on CI runners where algorithm + * tests run faster than usual (less GC pressure), the heap can be fragmented and full + * by the time GeneRandomizedTest starts, causing OOM even with -Xmx4096m. + */ + @JvmStatic + @AfterAll + fun compactHeapAfterClass() { + System.gc() + } + } protected fun getSample(seed: Long): List { val rand = Randomness() diff --git a/core/src/test/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolverTest.kt b/core/src/test/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolverTest.kt index 741712f505..4175bb5586 100644 --- a/core/src/test/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolverTest.kt +++ b/core/src/test/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolverTest.kt @@ -5,7 +5,7 @@ import org.evomaster.client.java.sql.DbInfoExtractor import org.evomaster.client.java.sql.SqlScriptRunner import org.evomaster.core.search.gene.BooleanGene import org.evomaster.core.search.gene.Gene -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 @@ -66,15 +66,15 @@ class SMTLibZ3DbConstraintSolverTest { "ID" -> { assertTrue(gene is SqlPrimaryKeyGene) val child = gene.getViewOfChildren().first() - assertEquals(4, (child as IntegerGene).value) + assertEquals(4L, (child as LongGene).value) } "NAME" -> { assertTrue(gene is StringGene) assertEquals("agus", (gene as StringGene).value) } "AGE" -> { - assertTrue(gene is IntegerGene) - assertEquals(5, (gene as IntegerGene).value) + assertTrue(gene is LongGene) + assertEquals(5L, (gene as LongGene).value) } "POINTS" -> { assertTrue(gene is BooleanGene) @@ -107,15 +107,15 @@ class SMTLibZ3DbConstraintSolverTest { "ID" -> { assertTrue(gene is SqlPrimaryKeyGene) val child = gene.getViewOfChildren().first() - assertEquals(2, (child as IntegerGene).value) + assertEquals(2L, (child as LongGene).value) } "NAME" -> { assertTrue(gene is StringGene) assertEquals("agus", (gene as StringGene).value) } "AGE" -> { - assertTrue(gene is IntegerGene) - assertEquals(3, (gene as IntegerGene).value) + assertTrue(gene is LongGene) + assertEquals(3L, (gene as LongGene).value) } "POINTS" -> { assertTrue(gene is BooleanGene) 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*: `""`.| From 859a1fd4bee347c67b85d54efd3d51f0b5d50cda Mon Sep 17 00:00:00 2001 From: Agustina Aldasoro Date: Sun, 28 Jun 2026 18:55:42 -0300 Subject: [PATCH 3/3] Fix merge conflict --- .../core/solver/SMTLibZ3DbConstraintSolver.kt | 23 ++++++++++++++++++- 1 file changed, 22 insertions(+), 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 0084a47dbe..7895b93e91 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt @@ -178,7 +178,28 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { Z3Result.Status.SAT -> { stats?.reportDseSat(z3TimeMs) z3ResultCache?.set(cacheKey, z3Result) - toSqlActionList(schemaDto, z3Result.model) + val sqlActions = toSqlActionList(schemaDto, z3Result.model) + if (::config.isInitialized && config.measureDseCorrectness && 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 DSE currently leaves unconstrained. + */ + 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'") + } + statisticsRef?.get()?.reportDseCorrectnessDistance( + distResult.sqlDistance, + distResult.sqlDistanceEvaluationFailure + ) + } + sqlActions } Z3Result.Status.UNSAT -> { stats?.reportDseUnsat(z3TimeMs)