From d03d8eca104497821954865e20505a6bdccefb12 Mon Sep 17 00:00:00 2001 From: Agustina Aldasoro Date: Sat, 27 Jun 2026 11:06:14 -0300 Subject: [PATCH 01/13] 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 02/13] 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 03/13] 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) From 699452049fb4adbd380b8fa5369b1ae0038df12d Mon Sep 17 00:00:00 2001 From: Agustina Aldasoro Date: Wed, 8 Jul 2026 16:09:34 -0300 Subject: [PATCH 04/13] PR Feedback --- .../dbconstraint/parser/jsql/JSqlVisitor.java | 5 +- .../evomaster/solver/MapBasedZ3Solution.java | 23 +++ .../evomaster/solver/Z3DockerExecutor.java | 37 ++++- .../java/org/evomaster/solver/Z3Result.java | 56 ++++++-- .../java/org/evomaster/solver/Z3Solution.java | 43 ++++++ .../solver/Z3DockerExecutorTest.java | 49 ++++--- .../solver/smtlib/SMTResultParserTest.java | 12 +- .../src/test/resources/composed_types.smt | 4 +- .../src/test/resources/hard_factoring.smt | 10 ++ .../rest/h2/z3solver/Z3SolverTypesRest.java | 2 +- .../spring/h2/z3solver/Z3SolverEMTest.java | 2 +- .../rest/service/resource/ResourceTestBase.kt | 2 +- .../kotlin/org/evomaster/core/EMConfig.kt | 34 +++-- .../api/service/ApiWsStructureMutator.kt | 6 +- .../core/search/service/Statistics.kt | 136 +++++++++--------- .../core/solver/SMTLibZ3DbConstraintSolver.kt | 56 ++++---- .../solver/SMTLibZ3DbConstraintSolverTest.kt | 6 +- .../core/solver/SmtLibGeneratorTest.kt | 6 +- docs/options.md | 7 +- 19 files changed, 332 insertions(+), 164 deletions(-) create mode 100644 core-extra/solver/src/main/java/org/evomaster/solver/MapBasedZ3Solution.java create mode 100644 core-extra/solver/src/main/java/org/evomaster/solver/Z3Solution.java create mode 100644 core-extra/solver/src/test/resources/hard_factoring.smt 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 9c51d6991e..bfc948d697 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 @@ -28,6 +28,9 @@ public class JSqlVisitor implements ExpressionVisitor { private static final String SIMILAR_ESCAPE = "similar_escape"; private static final String SIMILAR_TO_ESCAPE = "similar_to_escape"; + private static final String LOWER = "LOWER"; + private static final String UPPER = "UPPER"; + private final Deque stack = new ArrayDeque<>(); @Override @@ -50,7 +53,7 @@ public void visit(NullValue nullValue) { @Override public void visit(Function function) { String name = function.getName().toUpperCase(); - if ((name.equals("LOWER") || name.equals("UPPER")) + 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) diff --git a/core-extra/solver/src/main/java/org/evomaster/solver/MapBasedZ3Solution.java b/core-extra/solver/src/main/java/org/evomaster/solver/MapBasedZ3Solution.java new file mode 100644 index 0000000000..498c390bb6 --- /dev/null +++ b/core-extra/solver/src/main/java/org/evomaster/solver/MapBasedZ3Solution.java @@ -0,0 +1,23 @@ +package org.evomaster.solver; + +import org.evomaster.solver.smtlib.value.SMTLibValue; + +import java.util.Map; + +/** + * A {@link Z3Solution} backed by a plain map of variable/constant assignments, + * as produced by parsing Z3's textual output. + */ +public class MapBasedZ3Solution extends Z3Solution { + + private final Map assignments; + + public MapBasedZ3Solution(Map assignments) { + this.assignments = assignments; + } + + @Override + public Map getAssignments() { + return assignments; + } +} 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 f618363c43..dda3963899 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,11 +54,28 @@ 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 a {@link Z3Result} with status SAT (and the model), UNSAT, or ERROR + * @return a {@link Z3Result} with status SAT (and the solution), UNSAT, UNKNOWN, or ERROR */ public Z3Result solveFromFile(String fileName) { + return solveFromFile(fileName, 0); + } + + /** + * Executes the Z3 solver on an SMT-LIB file located in the container. + * The file must be in the directory specified by containerPath. + * + * @param fileName the name of the SMT-LIB file to read and solve + * @param timeoutMs soft per-query timeout in milliseconds. When greater than 0, it is passed + * to Z3 as {@code -t:}; if exceeded, Z3 returns {@code unknown} for the + * query (mapped to {@link Z3Result.Status#UNKNOWN}) rather than running + * unbounded. A value {@code <= 0} disables the timeout. + * @return a {@link Z3Result} with status SAT (and the solution), UNSAT, UNKNOWN, or ERROR + */ + public Z3Result solveFromFile(String fileName, long timeoutMs) { try { - Container.ExecResult result = z3Prover.execInContainer("z3", containerPath + fileName); + Container.ExecResult result = timeoutMs > 0 + ? z3Prover.execInContainer("z3", "-t:" + timeoutMs, containerPath + fileName) + : z3Prover.execInContainer("z3", containerPath + fileName); if (result.getExitCode() != 0) { return Z3Result.error("Z3 exited with code " + result.getExitCode() @@ -71,12 +88,22 @@ public Z3Result solveFromFile(String fileName) { + " stderr: " + result.getStderr()); } - if (stdout.trim().startsWith("unsat")) { + String trimmed = stdout.trim(); + if (trimmed.startsWith("unsat")) { return Z3Result.unsat(); } + // "unknown" means Z3 could not decide (e.g. incomplete theory or timeout). + // It must be handled explicitly: otherwise it would fall through and be parsed + // as an empty model, silently masquerading as SAT. + if (trimmed.startsWith("unknown")) { + return Z3Result.unknown(); + } + if (!trimmed.startsWith("sat")) { + return Z3Result.error("Unexpected Z3 output for file " + fileName + ": " + stdout); + } - Map model = SMTResultParser.parseZ3Response(stdout); - return Z3Result.sat(model); + Map assignments = SMTResultParser.parseZ3Response(stdout); + return Z3Result.sat(new MapBasedZ3Solution(assignments)); } catch (IOException | InterruptedException e) { return Z3Result.error("I/O or interruption error running Z3 on " + 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 index ca26f86cb1..ff4a05451a 100644 --- a/core-extra/solver/src/main/java/org/evomaster/solver/Z3Result.java +++ b/core-extra/solver/src/main/java/org/evomaster/solver/Z3Result.java @@ -1,45 +1,71 @@ 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). + * Distinguishes between four possible states: SAT (satisfiable with a solution), + * UNSAT (unsatisfiable), UNKNOWN (Z3 could not decide, e.g. an incomplete theory + * or a timeout), and ERROR (solver or parsing failure). */ public class Z3Result { public enum Status { - /** Z3 found a satisfying assignment. The model is available. */ + /** Z3 found a satisfying assignment. The solution is available. */ SAT, - /** The problem is unsatisfiable. No model exists. */ + /** The problem is unsatisfiable. No solution exists. */ UNSAT, + /** + * Z3 returned {@code unknown}: it could neither prove SAT nor UNSAT. + * Typical causes are an incomplete theory (e.g. non-linear arithmetic, + * quantifiers, some string/regex constraints) or a timeout. This is distinct + * from ERROR: the solver ran correctly, it just could not decide. + */ + UNKNOWN, /** A solver, I/O, or parsing error occurred. */ ERROR } - public final Status status; + private final Status status; /** Non-null only when status == SAT. */ - public final Map model; + private final Z3Solution solution; /** Non-null only when status == ERROR. */ - public final String errorMessage; + private final String errorMessage; - private Z3Result(Status status, Map model, String errorMessage) { + private Z3Result(Status status, Z3Solution solution, String errorMessage) { this.status = status; - this.model = model; + this.solution = solution; this.errorMessage = errorMessage; } - public static Z3Result sat(Map model) { - return new Z3Result(Status.SAT, model, null); + public Status getStatus() { + return status; + } + + /** + * @return the satisfying solution; non-null only when {@link #getStatus()} is SAT. + */ + public Z3Solution getSolution() { + return solution; + } + + /** + * @return the error message; non-null only when {@link #getStatus()} is ERROR. + */ + public String getErrorMessage() { + return errorMessage; + } + + public static Z3Result sat(Z3Solution solution) { + return new Z3Result(Status.SAT, solution, null); } public static Z3Result unsat() { return new Z3Result(Status.UNSAT, null, null); } + public static Z3Result unknown() { + return new Z3Result(Status.UNKNOWN, null, null); + } + public static Z3Result error(String message) { return new Z3Result(Status.ERROR, null, message); } diff --git a/core-extra/solver/src/main/java/org/evomaster/solver/Z3Solution.java b/core-extra/solver/src/main/java/org/evomaster/solver/Z3Solution.java new file mode 100644 index 0000000000..8fb4cab8dd --- /dev/null +++ b/core-extra/solver/src/main/java/org/evomaster/solver/Z3Solution.java @@ -0,0 +1,43 @@ +package org.evomaster.solver; + +import org.evomaster.solver.smtlib.value.SMTLibValue; + +import java.util.Map; + +/** + * Represents a satisfying solution produced by the Z3 solver: a mapping from + * SMT-LIB variable/constant names to the values Z3 assigned to them. + * + * This is intentionally an abstract type (rather than a raw {@link Map}) so that + * alternative solution representations can be introduced without changing callers. + */ +public abstract class Z3Solution { + + /** + * @return the assignments of this solution, keyed by variable/constant name. + */ + public abstract Map getAssignments(); + + /** + * @param name the variable/constant name + * @return the value assigned to the given name, or {@code null} if absent. + */ + public SMTLibValue get(String name) { + return getAssignments().get(name); + } + + /** + * @param name the variable/constant name + * @return whether the given name has an assigned value in this solution. + */ + public boolean containsKey(String name) { + return getAssignments().containsKey(name); + } + + /** + * @return the number of assignments in this solution. + */ + public int size() { + return getAssignments().size(); + } +} 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 2a447d688c..ecf4ba6327 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 @@ -44,11 +44,11 @@ static void tearDown() { public void satisfiabilityExample() { Z3Result result = executor.solveFromFile("example.smt"); - assertEquals(Z3Result.Status.SAT, result.status); - assertEquals(2, result.model.size()); + assertEquals(Z3Result.Status.SAT, result.getStatus()); + assertEquals(2, result.getSolution().size()); - assertEquals(new LongValue(0L), result.model.get("y")); - assertEquals(new LongValue((long) -4), result.model.get("x")); + assertEquals(new LongValue(0L), result.getSolution().get("y")); + assertEquals(new LongValue((long) -4), result.getSolution().get("x")); } /** @@ -70,7 +70,7 @@ public void dynamicFile() throws IOException { Files.deleteIfExists(copied); } - assertEquals(Z3Result.Status.SAT, result.status); + assertEquals(Z3Result.Status.SAT, result.getStatus()); } /** @@ -80,9 +80,9 @@ public void dynamicFile() throws IOException { public void uniqueUInt() { Z3Result result = executor.solveFromFile("unique_uint.smt"); - 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"); + assertEquals(Z3Result.Status.SAT, result.getStatus(), "Response should be SAT for unique_uint.smt"); + assertEquals(new LongValue(2L), result.getSolution().get("id_1"), "The value for id_1 should be 2"); + assertEquals(new LongValue(3L), result.getSolution().get("id_2"), "The value for id_2 should be 3"); } /** @@ -92,24 +92,24 @@ public void uniqueUInt() { public void composedTypes() { Z3Result result = executor.solveFromFile("composed_types.smt"); - assertEquals(Z3Result.Status.SAT, result.status, "Response should be SAT for composed_types.smt"); + assertEquals(Z3Result.Status.SAT, result.getStatus(), "Response should be SAT for composed_types.smt"); - assertTrue(result.model.containsKey("users1"), "Response should contain users1"); + assertTrue(result.getSolution().containsKey("users1"), "Response should contain users1"); Map users1Expected = new HashMap<>(); users1Expected.put("ID", new LongValue(3L)); - users1Expected.put("NAME", new StringValue("agus")); + users1Expected.put("NAME", new StringValue("Alice")); users1Expected.put("AGE", new LongValue(31L)); users1Expected.put("POINTS", new LongValue(7L)); - assertEquals(new StructValue(users1Expected), result.model.get("users1"), "The value for users1 is incorrect"); + assertEquals(new StructValue(users1Expected), result.getSolution().get("users1"), "The value for users1 is incorrect"); - assertTrue(result.model.containsKey("users2"), "Response should contain users2"); + assertTrue(result.getSolution().containsKey("users2"), "Response should contain users2"); Map users2Expected = new HashMap<>(); users2Expected.put("ID", new LongValue(3L)); - users2Expected.put("NAME", new StringValue("agus")); + users2Expected.put("NAME", new StringValue("Bob")); users2Expected.put("AGE", new LongValue(31L)); users2Expected.put("POINTS", new LongValue(7L)); - assertEquals(new StructValue(users2Expected), result.model.get("users2"), "The value for users2 is incorrect"); + assertEquals(new StructValue(users2Expected), result.getSolution().get("users2"), "The value for users2 is incorrect"); } /** @@ -118,8 +118,8 @@ public void composedTypes() { @Test public void whenSolvingInvalidFileItReturnsError() { Z3Result result = executor.solveFromFile("invalid.smt"); - assertEquals(Z3Result.Status.ERROR, result.status); - assertNotNull(result.errorMessage); + assertEquals(Z3Result.Status.ERROR, result.getStatus()); + assertNotNull(result.getErrorMessage()); } /** @@ -128,7 +128,18 @@ public void whenSolvingInvalidFileItReturnsError() { @Test public void whenSolvingEmptyFileItReturnsError() { Z3Result result = executor.solveFromFile("empty.smt"); - assertEquals(Z3Result.Status.ERROR, result.status); - assertNotNull(result.errorMessage); + assertEquals(Z3Result.Status.ERROR, result.getStatus()); + assertNotNull(result.getErrorMessage()); + } + + /** + * A hard non-linear problem solved with a small soft timeout: Z3 cannot decide + * in time and returns 'unknown', which must be reported as UNKNOWN (not SAT). + */ + @Test + public void whenTimeoutExceededItReturnsUnknown() { + Z3Result result = executor.solveFromFile("hard_factoring.smt", 1); + assertEquals(Z3Result.Status.UNKNOWN, result.getStatus()); + assertNull(result.getSolution()); } } diff --git a/core-extra/solver/src/test/java/org/evomaster/solver/smtlib/SMTResultParserTest.java b/core-extra/solver/src/test/java/org/evomaster/solver/smtlib/SMTResultParserTest.java index 27f16f12da..ccfcbeacfe 100644 --- a/core-extra/solver/src/test/java/org/evomaster/solver/smtlib/SMTResultParserTest.java +++ b/core-extra/solver/src/test/java/org/evomaster/solver/smtlib/SMTResultParserTest.java @@ -65,7 +65,7 @@ public void testParseNegativeValue() { @Test public void testParseComposedType() { - String response = "sat\n((users1 (id-document-name-age-points 4 2 \"agus\" 31 7)))"; + String response = "sat\n((users1 (id-document-name-age-points 4 2 \"Alice\" 31 7)))"; Map result = SMTResultParser.parseZ3Response(response); @@ -78,7 +78,7 @@ public void testParseComposedType() { assertTrue(users1.getField("DOCUMENT") instanceof LongValue); assertEquals(2, ((LongValue) users1.getField("DOCUMENT")).getValue()); assertTrue(users1.getField("NAME") instanceof StringValue); - assertEquals("agus", ((StringValue) users1.getField("NAME")).getValue()); + assertEquals("Alice", ((StringValue) users1.getField("NAME")).getValue()); assertTrue(users1.getField("AGE") instanceof LongValue); assertEquals(31, ((LongValue) users1.getField("AGE")).getValue()); assertTrue(users1.getField("POINTS") instanceof LongValue); @@ -90,8 +90,8 @@ public void testParseMultipleEntries() { String response = "sat\n" + "((products1 (price-min_price-stock-user_id 5 501 8 4)))\n" + "((products2 (price-min_price-stock-user_id 9 21739 8 6)))\n" + - "((users1 (id-document-name-age-points 4 2 \"agus\" 31 7)))\n" + - "((users2 (id-document-name-age-points 6 3 \"agus\" 91 7)))\n"; + "((users1 (id-document-name-age-points 4 2 \"Alice\" 31 7)))\n" + + "((users2 (id-document-name-age-points 6 3 \"Bob\" 91 7)))\n"; Map result = SMTResultParser.parseZ3Response(response); assertEquals(4, result.size()); @@ -128,7 +128,7 @@ public void testParseMultipleEntries() { assertTrue(users1.getField("DOCUMENT") instanceof LongValue); assertEquals(2, ((LongValue) users1.getField("DOCUMENT")).getValue()); assertTrue(users1.getField("NAME") instanceof StringValue); - assertEquals("agus", ((StringValue) users1.getField("NAME")).getValue()); + assertEquals("Alice", ((StringValue) users1.getField("NAME")).getValue()); assertTrue(users1.getField("AGE") instanceof LongValue); assertEquals(31, ((LongValue) users1.getField("AGE")).getValue()); assertTrue(users1.getField("POINTS") instanceof LongValue); @@ -142,7 +142,7 @@ public void testParseMultipleEntries() { assertTrue(users2.getField("DOCUMENT") instanceof LongValue); assertEquals(3, ((LongValue) users2.getField("DOCUMENT")).getValue()); assertTrue(users2.getField("NAME") instanceof StringValue); - assertEquals("agus", ((StringValue) users2.getField("NAME")).getValue()); + assertEquals("Bob", ((StringValue) users2.getField("NAME")).getValue()); assertTrue(users2.getField("AGE") instanceof LongValue); assertEquals(91, ((LongValue) users2.getField("AGE")).getValue()); assertTrue(users2.getField("POINTS") instanceof LongValue); diff --git a/core-extra/solver/src/test/resources/composed_types.smt b/core-extra/solver/src/test/resources/composed_types.smt index 1c5a060b6e..64a55963da 100644 --- a/core-extra/solver/src/test/resources/composed_types.smt +++ b/core-extra/solver/src/test/resources/composed_types.smt @@ -10,8 +10,8 @@ (declare-datatypes () ((UsersRow (id-name-age-points (ID Int) (NAME String) (AGE Int) (POINTS Int) )))) (declare-const users1 UsersRow) (declare-const users2 UsersRow) -(assert (= (NAME users1) "agus")) -(assert (= (NAME users2) "agus")) +(assert (= (NAME users1) "Alice")) +(assert (= (NAME users2) "Bob")) (assert (or (< (POINTS users1) 4) (> (POINTS users1) 6) )) (assert (or (< (POINTS users2) 4) (> (POINTS users2) 6) )) (assert (and (> (AGE users1) 18) (< (AGE users1) 100))) diff --git a/core-extra/solver/src/test/resources/hard_factoring.smt b/core-extra/solver/src/test/resources/hard_factoring.smt new file mode 100644 index 0000000000..e4dd156126 --- /dev/null +++ b/core-extra/solver/src/test/resources/hard_factoring.smt @@ -0,0 +1,10 @@ +; Factoring a large semiprime under non-linear integer arithmetic. +; 1000000016000000063 = 1000000007 * 1000000009 (both prime). +; This is hard for Z3, so with a small soft timeout it returns 'unknown' +; rather than deciding sat/unsat. +(declare-const p Int) +(declare-const q Int) +(assert (> p 1)) +(assert (> q 1)) +(assert (= (* p q) 1000000016000000063)) +(check-sat) diff --git a/core-tests/e2e-tests/spring/spring-rest-h2-z3solver/src/main/java/com/foo/spring/rest/h2/z3solver/Z3SolverTypesRest.java b/core-tests/e2e-tests/spring/spring-rest-h2-z3solver/src/main/java/com/foo/spring/rest/h2/z3solver/Z3SolverTypesRest.java index beb89f8216..dc1206347d 100644 --- a/core-tests/e2e-tests/spring/spring-rest-h2-z3solver/src/main/java/com/foo/spring/rest/h2/z3solver/Z3SolverTypesRest.java +++ b/core-tests/e2e-tests/spring/spring-rest-h2-z3solver/src/main/java/com/foo/spring/rest/h2/z3solver/Z3SolverTypesRest.java @@ -66,7 +66,7 @@ public ResponseEntity getId1() { @GetMapping("/products-3") public ResponseEntity getProductsWithName() { - Query query = em.createNativeQuery("SELECT (1) FROM products WHERE id = 2 AND name = 'Agus' AND price = 10.0"); + Query query = em.createNativeQuery("SELECT (1) FROM products WHERE id = 2 AND name = 'Alice' AND price = 10.0"); List data = query.getResultList(); if (data.isEmpty()) { diff --git a/core-tests/e2e-tests/spring/spring-rest-h2-z3solver/src/test/java/org/evomaster/e2etests/spring/h2/z3solver/Z3SolverEMTest.java b/core-tests/e2e-tests/spring/spring-rest-h2-z3solver/src/test/java/org/evomaster/e2etests/spring/h2/z3solver/Z3SolverEMTest.java index e5a56468a4..38a6b8b1d8 100644 --- a/core-tests/e2e-tests/spring/spring-rest-h2-z3solver/src/test/java/org/evomaster/e2etests/spring/h2/z3solver/Z3SolverEMTest.java +++ b/core-tests/e2e-tests/spring/spring-rest-h2-z3solver/src/test/java/org/evomaster/e2etests/spring/h2/z3solver/Z3SolverEMTest.java @@ -31,7 +31,7 @@ public void testRunEM() throws Throwable { args.add("true"); args.add("--generateSqlDataWithSearch"); args.add("false"); - args.add("--generateSqlDataWithDSE"); + args.add("--generateSqlDataWithZ3"); args.add("true"); Solution solution = initAndRun(args); diff --git a/core-tests/integration-tests/core-it/src/test/kotlin/org/evomaster/core/problem/rest/service/resource/ResourceTestBase.kt b/core-tests/integration-tests/core-it/src/test/kotlin/org/evomaster/core/problem/rest/service/resource/ResourceTestBase.kt index d787bc14cc..305e63fdba 100644 --- a/core-tests/integration-tests/core-it/src/test/kotlin/org/evomaster/core/problem/rest/service/resource/ResourceTestBase.kt +++ b/core-tests/integration-tests/core-it/src/test/kotlin/org/evomaster/core/problem/rest/service/resource/ResourceTestBase.kt @@ -67,7 +67,7 @@ abstract class ResourceTestBase : ExtractTestBaseH2(), ResourceBasedTestInterfac config.heuristicsForSQL = false config.generateSqlDataWithSearch = false - config.generateSqlDataWithDSE = false + config.generateSqlDataWithZ3 = false config.geneMutationStrategy = EMConfig.GeneMutationStrategy.ONE_OVER_N_BIASED_SQL } diff --git a/core/src/main/kotlin/org/evomaster/core/EMConfig.kt b/core/src/main/kotlin/org/evomaster/core/EMConfig.kt index 4d4aff3013..1fec23caab 100644 --- a/core/src/main/kotlin/org/evomaster/core/EMConfig.kt +++ b/core/src/main/kotlin/org/evomaster/core/EMConfig.kt @@ -752,8 +752,8 @@ class EMConfig { throw ConfigProblemException("Cannot generate SQL data if you not enable " + "collecting heuristics with 'heuristicsForSQL'") } - if (generateSqlDataWithDSE && generateSqlDataWithSearch) { - throw ConfigProblemException("Cannot generate SQL data with both DSE and search") + if (generateSqlDataWithZ3 && generateSqlDataWithSearch) { + throw ConfigProblemException("Cannot generate SQL data with both Z3 and search") } if (heuristicsForSQL && !extractSqlExecutionInfo) { @@ -1004,7 +1004,7 @@ class EMConfig { - fun shouldGenerateSqlData() = isUsingAdvancedTechniques() && (generateSqlDataWithDSE || generateSqlDataWithSearch) + fun shouldGenerateSqlData() = isUsingAdvancedTechniques() && (generateSqlDataWithZ3 || generateSqlDataWithSearch) fun shouldGenerateMongoData() = generateMongoData @@ -1955,24 +1955,32 @@ class EMConfig { var extractRedisExecutionInfo = false @Experimental - @Cfg("Enable EvoMaster to generate SQL data with direct accesses to the database. Use Dynamic Symbolic Execution") + @Cfg("Enable EvoMaster to generate SQL data with direct accesses to the database. Use the Z3 SMT solver") @DependsOnFalseFor("blackBox") - var generateSqlDataWithDSE = false + var generateSqlDataWithZ3 = false @Experimental - @Cfg("Collect detailed statistics for DSE SQL generation: SAT/UNSAT/error counts, " + + @Cfg("Collect detailed statistics for Z3-based 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 + "Only meaningful when generateSqlDataWithZ3=true.") + @DependsOnTrueFor("generateSqlDataWithZ3") + var collectSqlZ3Stats = false @Experimental - @Cfg("Measure the correctness of DSE-generated SQL inserts by computing the heuristic " + + @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 generateSqlDataWithDSE=true.") - @DependsOnTrueFor("generateSqlDataWithDSE") - var measureDseCorrectness = false + "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. " + + "A value of 0 disables the timeout. Only meaningful when generateSqlDataWithZ3=true.") + @DependsOnTrueFor("generateSqlDataWithZ3") + @Min(0.0) + var sqlZ3TimeoutMs = 5000 @Cfg("Enable EvoMaster to generate SQL data with direct accesses to the database. Use a search algorithm") @DependsOnFalseFor("blackBox") diff --git a/core/src/main/kotlin/org/evomaster/core/problem/api/service/ApiWsStructureMutator.kt b/core/src/main/kotlin/org/evomaster/core/problem/api/service/ApiWsStructureMutator.kt index e3f616e99c..b512624a9e 100644 --- a/core/src/main/kotlin/org/evomaster/core/problem/api/service/ApiWsStructureMutator.kt +++ b/core/src/main/kotlin/org/evomaster/core/problem/api/service/ApiWsStructureMutator.kt @@ -347,8 +347,8 @@ abstract class ApiWsStructureMutator : StructureMutator() { return handleSearch(ind, sampler, mutatedGenes, fw) } - if (config.generateSqlDataWithDSE) { - return handleDSE(ind, sampler, failedWhereQueries) + if (config.generateSqlDataWithZ3) { + return handleZ3(ind, sampler, failedWhereQueries) } return mutableListOf() @@ -436,7 +436,7 @@ abstract class ApiWsStructureMutator : StructureMutator() { return addedSqlInsertions } - private fun handleDSE(ind: T, sampler: ApiWsSampler, failedWhereQueries: List): MutableList> { + private fun handleZ3(ind: T, sampler: ApiWsSampler, failedWhereQueries: List): MutableList> { val schemaDto = sampler.sqlInsertBuilder?.schemaDto ?: throw IllegalStateException("No DB schema is available") 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 ca60751ce5..4c192a9435 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,24 +86,25 @@ 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 - - // 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 + // Z3-based SQL data generation statistics + private var sqlZ3TotalQueriesProcessed = 0 + private var sqlZ3SatCount = 0 + private var sqlZ3UnsatCount = 0 + private var sqlZ3UnknownCount = 0 + private var sqlZ3ErrorCount = 0 + private var sqlZ3ParseFailureCount = 0 + private var sqlZ3TimeMs = 0L + private var sqlZ3SmtlibGenTimeMs = 0L + private val sqlZ3SmtlibSizeBytes = IncrementalAverage() + 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 @@ -242,54 +243,60 @@ class Statistics : SearchListener { redisHeuristicEvaluationFailureCount++ } - fun reportDseSat(z3TimeMs: Long) { - dseTotalQueriesProcessed++ - dseSatCount++ - dseZ3TimeMs += z3TimeMs + fun reportSqlZ3Sat(z3TimeMs: Long) { + sqlZ3TotalQueriesProcessed++ + sqlZ3SatCount++ + sqlZ3TimeMs += z3TimeMs } - fun reportDseUnsat(z3TimeMs: Long) { - dseTotalQueriesProcessed++ - dseUnsatCount++ - dseZ3TimeMs += z3TimeMs + fun reportSqlZ3Unsat(z3TimeMs: Long) { + sqlZ3TotalQueriesProcessed++ + sqlZ3UnsatCount++ + sqlZ3TimeMs += z3TimeMs } - fun reportDseError(z3TimeMs: Long) { - dseTotalQueriesProcessed++ - dseErrorCount++ - dseZ3TimeMs += z3TimeMs + fun reportSqlZ3Unknown(z3TimeMs: Long) { + sqlZ3TotalQueriesProcessed++ + sqlZ3UnknownCount++ + sqlZ3TimeMs += z3TimeMs } - fun reportDseParseFailure() { - dseTotalQueriesProcessed++ - dseParseFailureCount++ + fun reportSqlZ3Error(z3TimeMs: Long) { + sqlZ3TotalQueriesProcessed++ + sqlZ3ErrorCount++ + sqlZ3TimeMs += z3TimeMs } - fun reportDseSmtlibGenTime(ms: Long, sizeBytes: Int) { - dseSmtlibGenTimeMs += ms - dseSmtlibSizeBytes.addValue(sizeBytes) + fun reportSqlZ3ParseFailure() { + sqlZ3TotalQueriesProcessed++ + sqlZ3ParseFailureCount++ } - fun reportDseQuerySeen(queryHash: Int) { - if (dseSeenQueryHashes.add(queryHash)) { - dseUniqueQueriesCount++ + fun reportSqlZ3SmtlibGenTime(ms: Long, sizeBytes: Int) { + sqlZ3SmtlibGenTimeMs += ms + sqlZ3SmtlibSizeBytes.addValue(sizeBytes) + } + + fun reportSqlZ3QuerySeen(queryHash: Int) { + if (sqlZ3SeenQueryHashes.add(queryHash)) { + sqlZ3UniqueQueriesCount++ } } - fun reportDseCorrectnessDistance(sqlDistance: Double, evaluationFailure: Boolean) { - dseCorrectnessCheckCount++ + 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 - dseCorrectnessEvalFailureCount++ + sqlZ3CorrectnessEvalFailureCount++ return } if (sqlDistance == 0.0) { - dseCorrectnessZeroDistanceCount++ + sqlZ3CorrectnessZeroDistanceCount++ } else { - dseCorrectnessNonZeroDistanceCount++ + sqlZ3CorrectnessNonZeroDistanceCount++ } - dseCorrectnessAvgDistance.addValue(sqlDistance) + sqlZ3CorrectnessAvgDistance.addValue(sqlDistance) } fun getMongoHeuristicsEvaluationCount(): Int = mongoHeuristicEvaluationSuccessCount + mongoHeuristicEvaluationFailureCount @@ -450,27 +457,28 @@ 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))) + // statistics info for Z3-based SQL data generation (only emitted when collectSqlZ3Stats=true) + if (config.collectSqlZ3Stats) { + add(Pair("sqlZ3TotalQueries", "$sqlZ3TotalQueriesProcessed")) + add(Pair("sqlZ3UniqueQueries", "$sqlZ3UniqueQueriesCount")) + add(Pair("sqlZ3DuplicateQueries", "${sqlZ3TotalQueriesProcessed - sqlZ3ParseFailureCount - sqlZ3UniqueQueriesCount}")) + add(Pair("sqlZ3Sat", "$sqlZ3SatCount")) + add(Pair("sqlZ3Unsat", "$sqlZ3UnsatCount")) + add(Pair("sqlZ3Unknown", "$sqlZ3UnknownCount")) + add(Pair("sqlZ3Errors", "$sqlZ3ErrorCount")) + add(Pair("sqlZ3ParseFailures", "$sqlZ3ParseFailureCount")) + add(Pair("sqlZ3TotalMs", "$sqlZ3TimeMs")) + add(Pair("sqlZ3SmtlibGenTotalMs", "$sqlZ3SmtlibGenTimeMs")) + add(Pair("sqlZ3AvgSmtlibSizeBytes", "%.1f".format(sqlZ3SmtlibSizeBytes.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")) + // 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){ 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 7895b93e91..af528608fe 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt @@ -33,6 +33,7 @@ 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.Z3Solution import org.evomaster.solver.smtlib.SMTLib import org.evomaster.solver.smtlib.value.* import java.io.File @@ -68,7 +69,7 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { // 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. + // Null until Z3 SQL generation is enabled in postConstruct — avoids allocating the map in runs where Z3 SQL generation is off. private var z3ResultCache: MutableMap, Z3Result>? = null companion object { @@ -98,7 +99,7 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { @PostConstruct private fun postConstruct() { - if (config.generateSqlDataWithDSE) { + if (config.generateSqlDataWithZ3) { initializeExecutor() z3ResultCache = object : LinkedHashMap, Z3Result>(16, 0.75f, true) { override fun removeEldestEntry(eldest: MutableMap.MutableEntry, Z3Result>?) = @@ -135,16 +136,16 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { * or an empty list if the problem is UNSAT, unparseable, or an error occurred. */ override fun solve(schemaDto: DbInfoDto, sqlQuery: String, numberOfRows: Int): List { - val collectStats = ::config.isInitialized && config.collectDseStats + val collectStats = ::config.isInitialized && config.collectSqlZ3Stats val stats: Statistics? = if (collectStats) statisticsRef?.get() else null - stats?.reportDseQuerySeen(sqlQuery.hashCode()) + stats?.reportSqlZ3QuerySeen(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) + Z3Result.Status.SAT -> toSqlActionList(schemaDto, cached.solution) else -> emptyList() } } @@ -152,8 +153,8 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { val queryStatement = try { parseStatement(sqlQuery) } catch (e: RuntimeException) { - LoggingUtil.getInfoLogger().warn("DSE: failed to parse SQL query as SMT-LIB: '$sqlQuery'") - stats?.reportDseParseFailure() + LoggingUtil.getInfoLogger().warn("SQL-Z3: failed to parse SQL query as SMT-LIB: '$sqlQuery'") + stats?.reportSqlZ3ParseFailure() return emptyList() } @@ -162,13 +163,14 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { val smtLib = generator.generateSMT(queryStatement) val smtlibBytes = smtLib.toString().toByteArray(StandardCharsets.UTF_8).size val smtlibGenMs = System.currentTimeMillis() - smtlibGenStart - stats?.reportDseSmtlibGenTime(smtlibGenMs, smtlibBytes) + stats?.reportSqlZ3SmtlibGenTime(smtlibGenMs, smtlibBytes) val fileName = storeToTmpFile(smtLib) val z3Start = System.currentTimeMillis() + val z3Timeout = if (::config.isInitialized) config.sqlZ3TimeoutMs.toLong() else 0L val z3Result = try { - executor.solveFromFile(fileName) + executor.solveFromFile(fileName, z3Timeout) } finally { Files.deleteIfExists(Paths.get(leadingBarResourcesFolder() + fileName)) } @@ -176,25 +178,25 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { return when (z3Result.status) { Z3Result.Status.SAT -> { - stats?.reportDseSat(z3TimeMs) + stats?.reportSqlZ3Sat(z3TimeMs) z3ResultCache?.set(cacheKey, z3Result) - val sqlActions = toSqlActionList(schemaDto, z3Result.model) - if (::config.isInitialized && config.measureDseCorrectness && queryStatement !is Insert) { + 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 DSE currently leaves unconstrained. + * or NOT NULL columns that Z3 SQL generation currently leaves unconstrained. */ val distResult = computeCorrectnessDistance(sqlQuery, schemaDto, sqlActions) if (distResult.sqlDistanceEvaluationFailure) { - LoggingUtil.getInfoLogger().warn("DSE: correctness evaluation failure for query '$sqlQuery'") + LoggingUtil.getInfoLogger().warn("SQL-Z3: 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'") + LoggingUtil.getInfoLogger().warn("SQL-Z3: non-zero correctness distance (${distResult.sqlDistance}) for query '$sqlQuery'") } - statisticsRef?.get()?.reportDseCorrectnessDistance( + statisticsRef?.get()?.reportSqlZ3CorrectnessDistance( distResult.sqlDistance, distResult.sqlDistanceEvaluationFailure ) @@ -202,13 +204,19 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { sqlActions } Z3Result.Status.UNSAT -> { - stats?.reportDseUnsat(z3TimeMs) + stats?.reportSqlZ3Unsat(z3TimeMs) z3ResultCache?.set(cacheKey, z3Result) emptyList() } + Z3Result.Status.UNKNOWN -> { + LoggingUtil.getInfoLogger().warn("SQL-Z3: Z3 returned 'unknown' (incomplete theory or timeout) for query '$sqlQuery'") + stats?.reportSqlZ3Unknown(z3TimeMs) + // Not cached: an 'unknown' may be timeout-driven and therefore transient + emptyList() + } Z3Result.Status.ERROR -> { - LoggingUtil.getInfoLogger().warn("DSE: Z3 error for query '$sqlQuery': ${z3Result.errorMessage}") - stats?.reportDseError(z3TimeMs) + LoggingUtil.getInfoLogger().warn("SQL-Z3: Z3 error for query '$sqlQuery': ${z3Result.errorMessage}") + stats?.reportSqlZ3Error(z3TimeMs) // Errors are not cached — they may be transient Docker failures emptyList() } @@ -240,15 +248,15 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { } /** - * Converts Z3's model to a list of SqlActions. + * Converts Z3's solution to a list of SqlActions. * - * @param model The satisfying assignment from Z3 (non-null, status must be SAT). + * @param solution The satisfying assignment from Z3 (non-null, status must be SAT). * @return A list of SQL actions. */ - private fun toSqlActionList(schemaDto: DbInfoDto, model: Map): List { + private fun toSqlActionList(schemaDto: DbInfoDto, solution: Z3Solution): List { val actions = mutableListOf() - for (row in model) { + for (row in solution.assignments) { val tableName = getTableName(row.key) val columns = row.value as StructValue @@ -533,7 +541,7 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { is ImmutableDataHolderGene -> inner.value else -> { LoggingUtil.getInfoLogger().warn( - "DSE: extractGeneValue() fallback to raw string for unhandled gene type " + + "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/core/src/test/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolverTest.kt b/core/src/test/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolverTest.kt index 4175bb5586..dd58f28a95 100644 --- a/core/src/test/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolverTest.kt +++ b/core/src/test/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolverTest.kt @@ -53,7 +53,7 @@ class SMTLibZ3DbConstraintSolverTest { @Test fun selectFromUsers() { - val newActions = solver.solve(schemaDto, "SELECT * FROM Users WHERE name = 'agus';", 2) + val newActions = solver.solve(schemaDto, "SELECT * FROM Users WHERE name = 'Alice';", 2) assertEquals(2, newActions.size) @@ -70,7 +70,7 @@ class SMTLibZ3DbConstraintSolverTest { } "NAME" -> { assertTrue(gene is StringGene) - assertEquals("agus", (gene as StringGene).value) + assertEquals("Alice", (gene as StringGene).value) } "AGE" -> { assertTrue(gene is LongGene) @@ -111,7 +111,7 @@ class SMTLibZ3DbConstraintSolverTest { } "NAME" -> { assertTrue(gene is StringGene) - assertEquals("agus", (gene as StringGene).value) + assertEquals("Alice", (gene as StringGene).value) } "AGE" -> { assertTrue(gene is LongGene) 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 ea53ef243e..49a15cdc70 100644 --- a/core/src/test/kotlin/org/evomaster/core/solver/SmtLibGeneratorTest.kt +++ b/core/src/test/kotlin/org/evomaster/core/solver/SmtLibGeneratorTest.kt @@ -50,12 +50,12 @@ class SmtLibGeneratorTest { ) addNode( AssertSMTNode( - EqualsAssertion(listOf("(NAME users1)", "\"agus\"")) + EqualsAssertion(listOf("(NAME users1)", "\"Alice\"")) ) ) addNode( AssertSMTNode( - EqualsAssertion(listOf("(NAME users2)", "\"agus\"")) + EqualsAssertion(listOf("(NAME users2)", "\"Alice\"")) ) ) addNode( @@ -192,7 +192,7 @@ class SmtLibGeneratorTest { "ALTER TABLE users add CHECK (points<=10);\n" + "ALTER TABLE users add CHECK (points>=0);\n" + "ALTER TABLE users add CHECK (points<4 OR points>6);\n" + - "ALTER TABLE users add CHECK (name = 'agus');\n" + + "ALTER TABLE users add CHECK (name = 'Alice');\n" + "ALTER TABLE users ADD UNIQUE (document);\n" + "CREATE TABLE products(price int not null, min_price int not null, stock int not null, user_id bigint not null);\n" + "ALTER TABLE products add constraint userIdKey foreign key (user_id) REFERENCES users;\n") diff --git a/docs/options.md b/docs/options.md index ced1373442..33c730e4a4 100644 --- a/docs/options.md +++ b/docs/options.md @@ -279,7 +279,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`.| +|`collectSqlZ3Stats`| __Boolean__. Collect detailed statistics for Z3-based SQL generation: SAT/UNSAT/error counts, query uniqueness, Z3 execution time, and SMT-LIB generation time. Only meaningful when generateSqlDataWithZ3=true. *Depends on*: `generateSqlDataWithZ3=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`.| @@ -301,7 +301,7 @@ There are 3 types of options: |`externalServiceIPSelectionStrategy`| __Enum__. Specify a method to select the first external service spoof IP address. *Valid values*: `NONE, DEFAULT, USER, RANDOM`. *Default value*: `NONE`.| |`extractRedisExecutionInfo`| __Boolean__. Enable extracting Redis execution info. *Depends on*: `blackBox=false`. *Default value*: `false`.| |`generateRedisData`| __Boolean__. Enable EvoMaster to generate Redis data with direct accesses to the database. *Depends on*: `blackBox=false`. *Default value*: `false`.| -|`generateSqlDataWithDSE`| __Boolean__. Enable EvoMaster to generate SQL data with direct accesses to the database. Use Dynamic Symbolic Execution. *Depends on*: `blackBox=false`. *Default value*: `false`.| +|`generateSqlDataWithZ3`| __Boolean__. Enable EvoMaster to generate SQL data with direct accesses to the database. Use the Z3 SMT solver. *Depends on*: `blackBox=false`. *Default value*: `false`.| |`handleFlakiness`| __Boolean__. Specify whether to detect flakiness and handle the flakiness in assertions during post handling of fuzzing. Note that flakiness is now supported only for fuzzing REST APIs. *Default value*: `false`.| |`heuristicsForRedis`| __Boolean__. Tracking of Redis commands to improve test generation. *Depends on*: `blackBox=false`. *Default value*: `false`.| |`heuristicsForSQLAdvanced`| __Boolean__. If using SQL heuristics, enable more advanced version. *Depends on*: `blackBox=false`. *Default value*: `false`.| @@ -328,7 +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`.| -|`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`.| +|`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`.| @@ -347,6 +347,7 @@ There are 3 types of options: |`seedTestCasesPath`| __String__. File path where the seeded test cases are located. *Default value*: `postman.postman_collection.json`.| |`skipAIModelUpdateWhenResponseIs5xx`| __Boolean__. Determines whether the AI response classifier skips model updates when the response indicates a server-side error with status code 5xx. *Default value*: `false`.| |`skipAIModelUpdateWhenResponseIsNot2xxOr400`| __Boolean__. Determines whether the AI response classifier skips model updates when the response is not 2xx or 400. *Default value*: `false`.| +|`sqlZ3TimeoutMs`| __Int__. 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. A value of 0 disables the timeout. Only meaningful when generateSqlDataWithZ3=true. *Constraints*: `min=0.0`. *Depends on*: `generateSqlDataWithZ3=true`. *Default value*: `5000`.| |`statusOracles`| __Boolean__. Lightweight checks on HTTP status codes, e.g., a GET should not return a 201 Created. *Default value*: `false`.| |`structureMutationProFS`| __Double__. Specify a probability of applying structure mutator during the focused search. *Constraints*: `probability 0.0-1.0`. *Default value*: `0.0`.| |`structureMutationProbStrategy`| __Enum__. Specify a strategy to handle a probability of applying structure mutator during the focused search. *Valid values*: `SPECIFIED, SPECIFIED_FS, DPC_TO_SPECIFIED_BEFORE_FS, DPC_TO_SPECIFIED_AFTER_FS, ADAPTIVE_WITH_IMPACT`. *Default value*: `SPECIFIED`.| From 4df0a88db91612e4386d237f7a4228e6d8996982 Mon Sep 17 00:00:00 2001 From: Agustina Aldasoro Date: Wed, 8 Jul 2026 16:13:34 -0300 Subject: [PATCH 05/13] Use default timpeout --- core/src/main/kotlin/org/evomaster/core/EMConfig.kt | 8 +++++++- .../evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt | 3 ++- 2 files changed, 9 insertions(+), 2 deletions(-) diff --git a/core/src/main/kotlin/org/evomaster/core/EMConfig.kt b/core/src/main/kotlin/org/evomaster/core/EMConfig.kt index 1fec23caab..326b39931d 100644 --- a/core/src/main/kotlin/org/evomaster/core/EMConfig.kt +++ b/core/src/main/kotlin/org/evomaster/core/EMConfig.kt @@ -59,6 +59,12 @@ class EMConfig { */ const val stringLengthHardLimit = 20_000 + /** + * Default soft timeout, in milliseconds, for each Z3 solver invocation + * when generating SQL data. See [sqlZ3TimeoutMs]. + */ + const val DEFAULT_SQL_Z3_TIMEOUT_MS = 5000 + private const val defaultExternalServiceIP = "127.0.0.4" //leading zeros are allowed @@ -1980,7 +1986,7 @@ class EMConfig { "A value of 0 disables the timeout. Only meaningful when generateSqlDataWithZ3=true.") @DependsOnTrueFor("generateSqlDataWithZ3") @Min(0.0) - var sqlZ3TimeoutMs = 5000 + var sqlZ3TimeoutMs = DEFAULT_SQL_Z3_TIMEOUT_MS @Cfg("Enable EvoMaster to generate SQL data with direct accesses to the database. Use a search algorithm") @DependsOnFalseFor("blackBox") 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 af528608fe..d0db66c4e7 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt @@ -168,7 +168,8 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { val fileName = storeToTmpFile(smtLib) val z3Start = System.currentTimeMillis() - val z3Timeout = if (::config.isInitialized) config.sqlZ3TimeoutMs.toLong() else 0L + val z3Timeout = if (::config.isInitialized) config.sqlZ3TimeoutMs.toLong() + else EMConfig.DEFAULT_SQL_Z3_TIMEOUT_MS.toLong() val z3Result = try { executor.solveFromFile(fileName, z3Timeout) } finally { From fb0a308e283bdc6f25f115b089b7707b63ef50fc Mon Sep 17 00:00:00 2001 From: Agustina Aldasoro Date: Thu, 9 Jul 2026 12:14:12 -0300 Subject: [PATCH 06/13] Fix stats --- .../core/search/service/Statistics.kt | 33 ++++++++++++++----- .../core/solver/SMTLibZ3DbConstraintSolver.kt | 7 ++-- .../core/search/service/StatisticsTest.kt | 29 +++++++++++++++- 3 files changed, 58 insertions(+), 11 deletions(-) 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 4c192a9435..3b4549ceb7 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 @@ -87,7 +87,11 @@ class Statistics : SearchListener { private val sqlRowsAverageCalculator = IncrementalAverage() // Z3-based SQL data generation statistics - private var sqlZ3TotalQueriesProcessed = 0 + // Invariant: sqlZ3QueriesSeenCount == sqlZ3CacheHitCount + sqlZ3CacheMissCount + // (every solve() call is either served from the memoization cache or handled as a miss). + private var sqlZ3QueriesSeenCount = 0 + private var sqlZ3CacheHitCount = 0 + private var sqlZ3CacheMissCount = 0 private var sqlZ3SatCount = 0 private var sqlZ3UnsatCount = 0 private var sqlZ3UnknownCount = 0 @@ -244,31 +248,31 @@ class Statistics : SearchListener { } fun reportSqlZ3Sat(z3TimeMs: Long) { - sqlZ3TotalQueriesProcessed++ + sqlZ3CacheMissCount++ sqlZ3SatCount++ sqlZ3TimeMs += z3TimeMs } fun reportSqlZ3Unsat(z3TimeMs: Long) { - sqlZ3TotalQueriesProcessed++ + sqlZ3CacheMissCount++ sqlZ3UnsatCount++ sqlZ3TimeMs += z3TimeMs } fun reportSqlZ3Unknown(z3TimeMs: Long) { - sqlZ3TotalQueriesProcessed++ + sqlZ3CacheMissCount++ sqlZ3UnknownCount++ sqlZ3TimeMs += z3TimeMs } fun reportSqlZ3Error(z3TimeMs: Long) { - sqlZ3TotalQueriesProcessed++ + sqlZ3CacheMissCount++ sqlZ3ErrorCount++ sqlZ3TimeMs += z3TimeMs } fun reportSqlZ3ParseFailure() { - sqlZ3TotalQueriesProcessed++ + sqlZ3CacheMissCount++ sqlZ3ParseFailureCount++ } @@ -278,11 +282,22 @@ class Statistics : SearchListener { } fun reportSqlZ3QuerySeen(queryHash: Int) { + sqlZ3QueriesSeenCount++ if (sqlZ3SeenQueryHashes.add(queryHash)) { sqlZ3UniqueQueriesCount++ } } + fun reportSqlZ3CacheHit() { + sqlZ3CacheHitCount++ + } + + // Exposed for tests: verify the memoization accounting invariant + // (seen == cacheHits + cacheMisses). + internal fun getSqlZ3QueriesSeenCount() = sqlZ3QueriesSeenCount + internal fun getSqlZ3CacheHitCount() = sqlZ3CacheHitCount + internal fun getSqlZ3CacheMissCount() = sqlZ3CacheMissCount + fun reportSqlZ3CorrectnessDistance(sqlDistance: Double, evaluationFailure: Boolean) { sqlZ3CorrectnessCheckCount++ if (evaluationFailure) { @@ -459,9 +474,11 @@ class Statistics : SearchListener { // statistics info for Z3-based SQL data generation (only emitted when collectSqlZ3Stats=true) if (config.collectSqlZ3Stats) { - add(Pair("sqlZ3TotalQueries", "$sqlZ3TotalQueriesProcessed")) + add(Pair("sqlZ3QueriesSeen", "$sqlZ3QueriesSeenCount")) add(Pair("sqlZ3UniqueQueries", "$sqlZ3UniqueQueriesCount")) - add(Pair("sqlZ3DuplicateQueries", "${sqlZ3TotalQueriesProcessed - sqlZ3ParseFailureCount - sqlZ3UniqueQueriesCount}")) + add(Pair("sqlZ3DuplicateQueries", "${sqlZ3QueriesSeenCount - sqlZ3UniqueQueriesCount}")) + add(Pair("sqlZ3CacheHits", "$sqlZ3CacheHitCount")) + add(Pair("sqlZ3CacheMisses", "$sqlZ3CacheMissCount")) add(Pair("sqlZ3Sat", "$sqlZ3SatCount")) add(Pair("sqlZ3Unsat", "$sqlZ3UnsatCount")) add(Pair("sqlZ3Unknown", "$sqlZ3UnknownCount")) 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 d0db66c4e7..876629fc86 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt @@ -139,11 +139,14 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { val collectStats = ::config.isInitialized && config.collectSqlZ3Stats val stats: Statistics? = if (collectStats) statisticsRef?.get() else null - stats?.reportSqlZ3QuerySeen(sqlQuery.hashCode()) - val cacheKey = Pair(sqlQuery, numberOfRows) + // Track "seen" against the same key the cache uses, so unique/duplicate counts + // line up with actual cache granularity. + stats?.reportSqlZ3QuerySeen(cacheKey.hashCode()) + val cached = z3ResultCache?.get(cacheKey) if (cached != null) { + stats?.reportSqlZ3CacheHit() return when (cached.status) { Z3Result.Status.SAT -> toSqlActionList(schemaDto, cached.solution) else -> emptyList() diff --git a/core/src/test/kotlin/org/evomaster/core/search/service/StatisticsTest.kt b/core/src/test/kotlin/org/evomaster/core/search/service/StatisticsTest.kt index dc4e4de040..59f21d7a2a 100644 --- a/core/src/test/kotlin/org/evomaster/core/search/service/StatisticsTest.kt +++ b/core/src/test/kotlin/org/evomaster/core/search/service/StatisticsTest.kt @@ -1,6 +1,6 @@ package org.evomaster.core.search.service -import org.junit.Test +import org.junit.jupiter.api.Test import org.junit.jupiter.api.Assertions.assertEquals class StatisticsTest { @@ -36,4 +36,31 @@ class StatisticsTest { assertEquals((5 + 7 + 11 + 13).toDouble() / 4, statistics.averageNumberOfEvaluatedRowsForSqlHeuristics()) } + @Test + fun testSqlZ3CacheAccountingInvariant() { + val statistics = Statistics() + + // Query #1: first sighting -> cache miss, solved as SAT + statistics.reportSqlZ3QuerySeen(1) + statistics.reportSqlZ3Sat(10) + + // Query #2: first sighting -> cache miss, solved as UNSAT + statistics.reportSqlZ3QuerySeen(2) + statistics.reportSqlZ3Unsat(5) + + // Query #1 seen again -> served from the memoization cache (a hit, not a miss) + statistics.reportSqlZ3QuerySeen(1) + statistics.reportSqlZ3CacheHit() + + assertEquals(3, statistics.getSqlZ3QueriesSeenCount()) + assertEquals(1, statistics.getSqlZ3CacheHitCount()) + assertEquals(2, statistics.getSqlZ3CacheMissCount()) + + // Every solve() is either a cache hit or a miss. + assertEquals( + statistics.getSqlZ3QueriesSeenCount(), + statistics.getSqlZ3CacheHitCount() + statistics.getSqlZ3CacheMissCount() + ) + } + } From 6162a09380a2c1df3a2eae2657851dfb0bef7c04 Mon Sep 17 00:00:00 2001 From: Agustina Aldasoro Date: Thu, 9 Jul 2026 13:12:28 -0300 Subject: [PATCH 07/13] PR Feedback --- .../dbconstraint/parser/jsql/JSqlVisitor.java | 10 +++++-- .../evomaster/solver/MapBasedZ3Solution.java | 23 --------------- .../evomaster/solver/Z3DockerExecutor.java | 16 ++++++----- .../java/org/evomaster/solver/Z3Solution.java | 28 +++++++++++++------ .../solver/smtlib/SMTResultParser.java | 10 ++++--- .../solver/smtlib/SMTResultParserTest.java | 21 +++++++------- .../spring/h2/z3solver/Z3SolverEMTest.java | 9 ++---- .../api/service/ApiWsStructureMutator.kt | 8 +++--- .../core/solver/SMTLibZ3DbConstraintSolver.kt | 6 +++- 9 files changed, 64 insertions(+), 67 deletions(-) delete mode 100644 core-extra/solver/src/main/java/org/evomaster/solver/MapBasedZ3Solution.java 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 bfc948d697..480b6e04aa 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 @@ -31,6 +31,10 @@ public class JSqlVisitor implements ExpressionVisitor { private static final String LOWER = "LOWER"; private static final String UPPER = "UPPER"; + private static final String SINGLE_QUOTE_CHAR = "'"; + + private static final String TIMESTAMP_FORMAT = "yyyy-MM-dd HH:mm:ss"; + private final Deque stack = new ArrayDeque<>(); @Override @@ -143,7 +147,7 @@ public void visit(StringValue stringValue) { String notEscapedValue = stringValue.getNotExcapedValue(); String notEscapedValueNoQuotes; - if (notEscapedValue.startsWith("'") && notEscapedValue.endsWith("'")) { + if (notEscapedValue.startsWith(SINGLE_QUOTE_CHAR) && notEscapedValue.endsWith(SINGLE_QUOTE_CHAR)) { notEscapedValueNoQuotes = notEscapedValue.substring(1, notEscapedValue.length() - 1); } else { notEscapedValueNoQuotes = notEscapedValue; @@ -617,13 +621,13 @@ public void visit(TimeKeyExpression timeKeyExpression) { public void visit(DateTimeLiteralExpression dateTimeLiteralExpression) { if (dateTimeLiteralExpression.getType() == DateTimeLiteralExpression.DateTime.TIMESTAMP) { String value = dateTimeLiteralExpression.getValue(); - if (value.startsWith("'") && value.endsWith("'")) { + if (value.startsWith(SINGLE_QUOTE_CHAR) && value.endsWith(SINGLE_QUOTE_CHAR)) { 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")) + DateTimeFormatter.ofPattern(TIMESTAMP_FORMAT)) .toEpochSecond(ZoneOffset.UTC); stack.push(new SqlBigIntegerLiteralValue(BigInteger.valueOf(epochSeconds))); return; diff --git a/core-extra/solver/src/main/java/org/evomaster/solver/MapBasedZ3Solution.java b/core-extra/solver/src/main/java/org/evomaster/solver/MapBasedZ3Solution.java deleted file mode 100644 index 498c390bb6..0000000000 --- a/core-extra/solver/src/main/java/org/evomaster/solver/MapBasedZ3Solution.java +++ /dev/null @@ -1,23 +0,0 @@ -package org.evomaster.solver; - -import org.evomaster.solver.smtlib.value.SMTLibValue; - -import java.util.Map; - -/** - * A {@link Z3Solution} backed by a plain map of variable/constant assignments, - * as produced by parsing Z3's textual output. - */ -public class MapBasedZ3Solution extends Z3Solution { - - private final Map assignments; - - public MapBasedZ3Solution(Map assignments) { - this.assignments = assignments; - } - - @Override - public Map getAssignments() { - return assignments; - } -} 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 dda3963899..92495bd26e 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 @@ -1,14 +1,12 @@ package org.evomaster.solver; import org.evomaster.solver.smtlib.SMTResultParser; -import org.evomaster.solver.smtlib.value.SMTLibValue; import org.testcontainers.containers.BindMode; import org.testcontainers.containers.Container; import org.testcontainers.containers.GenericContainer; import org.testcontainers.images.builder.ImageFromDockerfile; import java.io.IOException; -import java.util.Map; import java.util.Optional; /** @@ -21,6 +19,11 @@ public class Z3DockerExecutor implements AutoCloseable { public static final String Z3_DOCKER_IMAGE = "ghcr.io/z3prover/z3:ubuntu-20.04-bare-z3-sha-ba8d8f0"; // The Docker entrypoint that keeps it running indefinitely public static final String ENTRYPOINT = "while :; do sleep 1000 ; done"; + + // SMT-LIB (check-sat) response tokens returned by Z3 + private static final String SAT = "sat"; + private static final String UNSAT = "unsat"; + private static final String UNKNOWN = "unknown"; private final String containerPath = "/smt2-resources/"; private final GenericContainer z3Prover; @@ -89,21 +92,20 @@ public Z3Result solveFromFile(String fileName, long timeoutMs) { } String trimmed = stdout.trim(); - if (trimmed.startsWith("unsat")) { + if (trimmed.startsWith(UNSAT)) { return Z3Result.unsat(); } // "unknown" means Z3 could not decide (e.g. incomplete theory or timeout). // It must be handled explicitly: otherwise it would fall through and be parsed // as an empty model, silently masquerading as SAT. - if (trimmed.startsWith("unknown")) { + if (trimmed.startsWith(UNKNOWN)) { return Z3Result.unknown(); } - if (!trimmed.startsWith("sat")) { + if (!trimmed.startsWith(SAT)) { return Z3Result.error("Unexpected Z3 output for file " + fileName + ": " + stdout); } - Map assignments = SMTResultParser.parseZ3Response(stdout); - return Z3Result.sat(new MapBasedZ3Solution(assignments)); + return Z3Result.sat(SMTResultParser.parseZ3Response(stdout)); } catch (IOException | InterruptedException e) { return Z3Result.error("I/O or interruption error running Z3 on " + fileName + ": " + e.getMessage()); diff --git a/core-extra/solver/src/main/java/org/evomaster/solver/Z3Solution.java b/core-extra/solver/src/main/java/org/evomaster/solver/Z3Solution.java index 8fb4cab8dd..b0787ec4d5 100644 --- a/core-extra/solver/src/main/java/org/evomaster/solver/Z3Solution.java +++ b/core-extra/solver/src/main/java/org/evomaster/solver/Z3Solution.java @@ -7,23 +7,28 @@ /** * Represents a satisfying solution produced by the Z3 solver: a mapping from * SMT-LIB variable/constant names to the values Z3 assigned to them. - * - * This is intentionally an abstract type (rather than a raw {@link Map}) so that - * alternative solution representations can be introduced without changing callers. */ -public abstract class Z3Solution { +public class Z3Solution { + + private final Map assignments; + + public Z3Solution(Map assignments) { + this.assignments = assignments; + } /** * @return the assignments of this solution, keyed by variable/constant name. */ - public abstract Map getAssignments(); + public Map getAssignments() { + return assignments; + } /** * @param name the variable/constant name * @return the value assigned to the given name, or {@code null} if absent. */ public SMTLibValue get(String name) { - return getAssignments().get(name); + return assignments.get(name); } /** @@ -31,13 +36,20 @@ public SMTLibValue get(String name) { * @return whether the given name has an assigned value in this solution. */ public boolean containsKey(String name) { - return getAssignments().containsKey(name); + return assignments.containsKey(name); } /** * @return the number of assignments in this solution. */ public int size() { - return getAssignments().size(); + return assignments.size(); + } + + /** + * @return whether this solution has no assignments. + */ + public boolean isEmpty() { + return assignments.isEmpty(); } } diff --git a/core-extra/solver/src/main/java/org/evomaster/solver/smtlib/SMTResultParser.java b/core-extra/solver/src/main/java/org/evomaster/solver/smtlib/SMTResultParser.java index a1e7dfbbbd..37905f8861 100644 --- a/core-extra/solver/src/main/java/org/evomaster/solver/smtlib/SMTResultParser.java +++ b/core-extra/solver/src/main/java/org/evomaster/solver/smtlib/SMTResultParser.java @@ -1,5 +1,6 @@ package org.evomaster.solver.smtlib; +import org.evomaster.solver.Z3Solution; import org.evomaster.solver.smtlib.value.*; import java.util.HashMap; @@ -9,7 +10,8 @@ /** * The SMTResultParser class is responsible for parsing responses from the Z3 solver. - * It converts the raw SMT-LIB response into a map of variable names and their corresponding values. + * It converts the raw SMT-LIB response into a {@link Z3Solution} of variable names and + * their corresponding values. */ public class SMTResultParser { @@ -17,9 +19,9 @@ public class SMTResultParser { * Parses the Z3 solver response and extracts variable values. * * @param z3Response the raw response from Z3 solver - * @return a map where keys are variable names and values are SMTLibValue objects representing the parsed values + * @return a {@link Z3Solution} mapping variable names to the {@link SMTLibValue} objects Z3 assigned to them */ - public static Map parseZ3Response(String z3Response) { + public static Z3Solution parseZ3Response(String z3Response) { Map results = new HashMap<>(); // Regular expression for matching simple value assignments, including negative numbers @@ -91,7 +93,7 @@ else if (valueMatcher.find()) { buffer.setLength(0); // Clear the buffer after processing } } - return results; // Return the map of parsed results + return new Z3Solution(results); // Return the parsed assignments as a solution } /** diff --git a/core-extra/solver/src/test/java/org/evomaster/solver/smtlib/SMTResultParserTest.java b/core-extra/solver/src/test/java/org/evomaster/solver/smtlib/SMTResultParserTest.java index ccfcbeacfe..d912ea0ca1 100644 --- a/core-extra/solver/src/test/java/org/evomaster/solver/smtlib/SMTResultParserTest.java +++ b/core-extra/solver/src/test/java/org/evomaster/solver/smtlib/SMTResultParserTest.java @@ -1,10 +1,9 @@ package org.evomaster.solver.smtlib; +import org.evomaster.solver.Z3Solution; import org.evomaster.solver.smtlib.value.*; import org.junit.jupiter.api.Test; -import java.util.Map; - import static org.junit.jupiter.api.Assertions.assertEquals; import static org.junit.jupiter.api.Assertions.assertTrue; @@ -12,21 +11,21 @@ public class SMTResultParserTest { @Test public void testParseEmptyResponse() { String response = ""; - Map result = SMTResultParser.parseZ3Response(response); + Z3Solution result = SMTResultParser.parseZ3Response(response); assertTrue(result.isEmpty()); } @Test public void testParseMalformedResponse() { String response = "sat\n(id_1 2)"; - Map result = SMTResultParser.parseZ3Response(response); + Z3Solution result = SMTResultParser.parseZ3Response(response); assertTrue(result.isEmpty()); } @Test public void testParseSimpleIntValue() { String response = "sat\n((id_1 2))"; - Map result = SMTResultParser.parseZ3Response(response); + Z3Solution result = SMTResultParser.parseZ3Response(response); assertEquals(1, result.size()); assertTrue(result.get("id_1") instanceof LongValue); assertEquals(2, ((LongValue) result.get("id_1")).getValue()); @@ -35,7 +34,7 @@ public void testParseSimpleIntValue() { @Test public void testParseSimpleStringValue() { String response = "sat\n((name_1 \"example\"))"; - Map result = SMTResultParser.parseZ3Response(response); + Z3Solution result = SMTResultParser.parseZ3Response(response); assertEquals(1, result.size()); assertTrue(result.get("name_1") instanceof StringValue); assertEquals("example", ((StringValue) result.get("name_1")).getValue()); @@ -44,7 +43,7 @@ public void testParseSimpleStringValue() { @Test public void testParseSimpleRealValue() { String response = "sat\n((pi_1 3.14))"; - Map result = SMTResultParser.parseZ3Response(response); + Z3Solution result = SMTResultParser.parseZ3Response(response); assertEquals(1, result.size()); assertTrue(result.get("pi_1") instanceof RealValue); assertEquals(3.14, ((RealValue) result.get("pi_1")).getValue()); @@ -55,7 +54,7 @@ public void testParseNegativeValue() { String response = "sat\n" + "((y 0))\n" + "((x (- 4)))"; - Map result = SMTResultParser.parseZ3Response(response); + Z3Solution result = SMTResultParser.parseZ3Response(response); assertEquals(2, result.size()); assertTrue(result.get("y") instanceof LongValue); assertEquals(0, ((LongValue) result.get("y")).getValue()); @@ -67,7 +66,7 @@ public void testParseNegativeValue() { public void testParseComposedType() { String response = "sat\n((users1 (id-document-name-age-points 4 2 \"Alice\" 31 7)))"; - Map result = SMTResultParser.parseZ3Response(response); + Z3Solution result = SMTResultParser.parseZ3Response(response); assertEquals(1, result.size()); assertTrue(result.get("users1") instanceof StructValue); @@ -93,7 +92,7 @@ public void testParseMultipleEntries() { "((users1 (id-document-name-age-points 4 2 \"Alice\" 31 7)))\n" + "((users2 (id-document-name-age-points 6 3 \"Bob\" 91 7)))\n"; - Map result = SMTResultParser.parseZ3Response(response); + Z3Solution result = SMTResultParser.parseZ3Response(response); assertEquals(4, result.size()); assertTrue(result.get("products1") instanceof StructValue); @@ -163,7 +162,7 @@ public void testNegativeLong() { " \"true\"\n" + " 2)))\n"; - Map result = SMTResultParser.parseZ3Response(response); + Z3Solution result = SMTResultParser.parseZ3Response(response); assertEquals(2, result.size()); assertTrue(result.get("documents_specs1") instanceof StructValue); diff --git a/core-tests/e2e-tests/spring/spring-rest-h2-z3solver/src/test/java/org/evomaster/e2etests/spring/h2/z3solver/Z3SolverEMTest.java b/core-tests/e2e-tests/spring/spring-rest-h2-z3solver/src/test/java/org/evomaster/e2etests/spring/h2/z3solver/Z3SolverEMTest.java index 38a6b8b1d8..77f0d9803a 100644 --- a/core-tests/e2e-tests/spring/spring-rest-h2-z3solver/src/test/java/org/evomaster/e2etests/spring/h2/z3solver/Z3SolverEMTest.java +++ b/core-tests/e2e-tests/spring/spring-rest-h2-z3solver/src/test/java/org/evomaster/e2etests/spring/h2/z3solver/Z3SolverEMTest.java @@ -27,12 +27,9 @@ public void testRunEM() throws Throwable { "com.foo.spring.rest.h2.z3solver.Z3SolverEvoMaster", 50, (args) -> { - args.add("--heuristicsForSQL"); - args.add("true"); - args.add("--generateSqlDataWithSearch"); - args.add("false"); - args.add("--generateSqlDataWithZ3"); - args.add("true"); + setOption(args, "heuristicsForSQL", "true"); + setOption(args, "generateSqlDataWithSearch", "false"); + setOption(args, "generateSqlDataWithZ3", "true"); Solution solution = initAndRun(args); diff --git a/core/src/main/kotlin/org/evomaster/core/problem/api/service/ApiWsStructureMutator.kt b/core/src/main/kotlin/org/evomaster/core/problem/api/service/ApiWsStructureMutator.kt index b512624a9e..7e2a2419f2 100644 --- a/core/src/main/kotlin/org/evomaster/core/problem/api/service/ApiWsStructureMutator.kt +++ b/core/src/main/kotlin/org/evomaster/core/problem/api/service/ApiWsStructureMutator.kt @@ -344,17 +344,17 @@ abstract class ApiWsStructureMutator : StructureMutator() { ): MutableList>? { if (config.generateSqlDataWithSearch) { - return handleSearch(ind, sampler, mutatedGenes, fw) + return generateSqlDataWithSearch(ind, sampler, mutatedGenes, fw) } if (config.generateSqlDataWithZ3) { - return handleZ3(ind, sampler, failedWhereQueries) + return generateSqlDataWithZ3(ind, sampler, failedWhereQueries) } return mutableListOf() } - private fun handleSearch( + private fun generateSqlDataWithSearch( ind: T, sampler: ApiWsSampler, mutatedGenes: MutatedGeneSpecification?, @@ -436,7 +436,7 @@ abstract class ApiWsStructureMutator : StructureMutator() { return addedSqlInsertions } - private fun handleZ3(ind: T, sampler: ApiWsSampler, failedWhereQueries: List): MutableList> { + private fun generateSqlDataWithZ3(ind: T, sampler: ApiWsSampler, failedWhereQueries: List): MutableList> { val schemaDto = sampler.sqlInsertBuilder?.schemaDto ?: throw IllegalStateException("No DB schema is available") 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 876629fc86..a2e87053f2 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt @@ -74,6 +74,10 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { companion object { private const val MAX_CACHE_SIZE = 500 + + // Must match the timestamp format used by JSqlVisitor (TIMESTAMP_FORMAT) so that + // epoch<->string conversions round-trip consistently. + private const val TIMESTAMP_FORMAT = "yyyy-MM-dd HH:mm:ss" } @Inject @@ -292,7 +296,7 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { Instant.ofEpochSecond(epochSeconds), ZoneOffset.UTC ) val formatted = localDateTime.format( - DateTimeFormatter.ofPattern("yyyy-MM-dd HH:mm:ss") + DateTimeFormatter.ofPattern(TIMESTAMP_FORMAT) ) ImmutableDataHolderGene(dbColumnName, formatted, inQuotes = true) } else { From 27d47308c8a91d7aa2857df1dd7a876f8a5d99a0 Mon Sep 17 00:00:00 2001 From: Agustina Aldasoro Date: Thu, 9 Jul 2026 14:38:47 -0300 Subject: [PATCH 08/13] Add comments --- .../solver/smtlib/SMTResultParser.java | 3 ++ .../kotlin/org/evomaster/core/EMConfig.kt | 10 +++++ .../api/service/ApiWsStructureMutator.kt | 5 ++- .../core/solver/SMTLibZ3DbConstraintSolver.kt | 38 +++++++++++++++++-- .../evomaster/core/solver/SmtLibGenerator.kt | 22 ++++++++++- docs/options.md | 1 + 6 files changed, 74 insertions(+), 5 deletions(-) diff --git a/core-extra/solver/src/main/java/org/evomaster/solver/smtlib/SMTResultParser.java b/core-extra/solver/src/main/java/org/evomaster/solver/smtlib/SMTResultParser.java index 37905f8861..74e13dbe9b 100644 --- a/core-extra/solver/src/main/java/org/evomaster/solver/smtlib/SMTResultParser.java +++ b/core-extra/solver/src/main/java/org/evomaster/solver/smtlib/SMTResultParser.java @@ -45,6 +45,9 @@ public static Z3Solution parseZ3Response(String z3Response) { String[] lines = z3Response.split("\n"); for (String line : lines) { + // Defensive: Z3DockerExecutor already classifies 'unsat'/'unknown' before invoking this + // parser, so in practice only 'sat' models reach here. This guard is kept as a safety net + // in case the parser is ever called directly with an unsat response. if (line.startsWith("unsat")) { throw new RuntimeException("Unsatisfiable problem"); } diff --git a/core/src/main/kotlin/org/evomaster/core/EMConfig.kt b/core/src/main/kotlin/org/evomaster/core/EMConfig.kt index 326b39931d..48e94683b2 100644 --- a/core/src/main/kotlin/org/evomaster/core/EMConfig.kt +++ b/core/src/main/kotlin/org/evomaster/core/EMConfig.kt @@ -1988,6 +1988,16 @@ class EMConfig { @Min(0.0) var sqlZ3TimeoutMs = DEFAULT_SQL_Z3_TIMEOUT_MS + @Experimental + @Cfg("Number of rows the Z3 solver generates per table when solving a failed SQL query. " + + "The default of 1 is sufficient for the currently supported queries; generating a single " + + "row per table already forces the query to return a non-empty result. This will need to be " + + "increased once support for more complex JOINs (matching arbitrary row combinations, not just " + + "the diagonal pairing of row i with row i) is added. Only meaningful when generateSqlDataWithZ3=true.") + @DependsOnTrueFor("generateSqlDataWithZ3") + @Min(1.0) + var sqlZ3NumberOfRows = 1 + @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/problem/api/service/ApiWsStructureMutator.kt b/core/src/main/kotlin/org/evomaster/core/problem/api/service/ApiWsStructureMutator.kt index 7e2a2419f2..a46caa390d 100644 --- a/core/src/main/kotlin/org/evomaster/core/problem/api/service/ApiWsStructureMutator.kt +++ b/core/src/main/kotlin/org/evomaster/core/problem/api/service/ApiWsStructureMutator.kt @@ -442,7 +442,10 @@ abstract class ApiWsStructureMutator : StructureMutator() { val newActions = mutableListOf>() for (query in failedWhereQueries) { - val newActionsForQuery = z3Solver.solve(schemaDto, query) + // numberOfRows is kept at 1 by default, which is enough to force a non-empty result for the + // currently supported queries. It is configurable to allow experimenting with more rows once + // support for complex JOINs (arbitrary row combinations) is added. + val newActionsForQuery = z3Solver.solve(schemaDto, query, config.sqlZ3NumberOfRows) newActions.addAll(mutableListOf(newActionsForQuery)) ind.addInitializingDbActions(actions = newActionsForQuery) } 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 a2e87053f2..eb347f1bdb 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt @@ -167,7 +167,16 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { val smtlibGenStart = System.currentTimeMillis() val generator = SmtLibGenerator(schemaDto, numberOfRows) - val smtLib = generator.generateSMT(queryStatement) + // SMT-LIB generation can throw for unsupported column types or query shapes it cannot handle + // (e.g. a cast failure on an unexpected statement structure). Degrade gracefully to an empty + // result instead of letting the exception propagate into the structure mutator. + val smtLib = try { + generator.generateSMT(queryStatement) + } catch (e: RuntimeException) { + LoggingUtil.getInfoLogger().warn("SQL-Z3: failed to generate SMT-LIB for query '$sqlQuery': ${e.message}") + stats?.reportSqlZ3ParseFailure() + return emptyList() + } val smtlibBytes = smtLib.toString().toByteArray(StandardCharsets.UTF_8).size val smtlibGenMs = System.currentTimeMillis() - smtlibGenStart stats?.reportSqlZ3SmtlibGenTime(smtlibGenMs, smtlibBytes) @@ -325,6 +334,18 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { return value.equals("True", ignoreCase = true) } + /** + * Whether the given column's SQL type (as reported in [ColumnDto.type]) equals [expectedType], + * compared case-insensitively as a raw string. + * + * CAVEAT: this relies on [ColumnDto.type] containing the exact spelling passed in (currently + * "BOOLEAN" and "TIMESTAMP"). It is needed because the SMT sort alone cannot recover these types + * (BOOLEAN is encoded as an SMT String, TIMESTAMP as an SMT Int), so gene reconstruction must + * consult the original SQL type. The set of type spellings recognized here must stay consistent + * with [SmtLibGenerator.TYPE_MAP]; if a backend reports a variant spelling (e.g. "BOOL" or + * "TIMESTAMP WITHOUT TIME ZONE"), the special handling is silently skipped. Consolidating these + * type vocabularies into a single source of truth is future work. + */ private fun hasColumnType( schemaDto: DbInfoDto, table: Table, @@ -346,13 +367,17 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { } /** - * Extracts the table name from the key by removing the last character (index). + * Extracts the table name from a row-constant key by removing the trailing row index. + * + * Row constants are named "${smtName}${i}" (e.g. "users1", "users2"). The trailing digits are + * stripped so this works for any number of rows (e.g. "users10" -> "users"), not just single-digit + * indices. Note: this still assumes table names themselves do not end in a digit. * * @param key The key containing the table name and index. * @return The extracted table name. */ private fun getTableName(key: String): String { - return key.substring(0, key.length - 1) + return key.replace(Regex("\\d+$"), "") } /** @@ -445,6 +470,13 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { /** * Maps column types to ColumnDataType. * + * FUTURE WORK: this recognizes only a small subset of SQL type spellings and falls back to + * CHARACTER_VARYING for everything else. It is one of three independent type vocabularies that + * interpret [ColumnDto.type] — the others being [SmtLibGenerator.TYPE_MAP] (SQL type -> SMT sort) + * and [hasColumnType] (BOOLEAN/TIMESTAMP special-casing). These can silently disagree when a + * backend reports a variant spelling. They should be consolidated into a single source of truth + * so that generation and interpretation cannot drift; see the note on [hasColumnType]. + * * @param type The column type as a string. * @return The corresponding ColumnDataType. */ 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 0e06819be6..152a47d200 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt @@ -312,6 +312,11 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I findReferencedPKSelector(smtTable.dto, referencedSmtTable.dto, foreignKey) ) + // KNOWN LIMITATION: composite foreign keys are not fully supported. Each source column is + // matched independently against a single referenced column, rather than constraining the + // whole tuple of source columns to match a referenced tuple. This is correct for + // single-column FKs (the common case) but under-models multi-column FKs. Fully supporting + // composite FKs (as a tuple-level OR over referenced rows) is future work. for (sourceColumn in foreignKey.sourceColumns) { val nodes = assertForEqualsAny( smtTable.smtColumnName(sourceColumn), smtTable.smtName, @@ -442,10 +447,18 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I for (join in joins) { val onExpressions = join.onExpressions if (onExpressions.isNotEmpty()) { + // KNOWN LIMITATION: only the first ON expression is used; a composite ON + // (e.g. "a = b AND c = d") drops all but the first conjunct. val onExpression = onExpressions.elementAt(0) try { val condition = parser.parse(onExpression.toString(), toDBType(schema.databaseType)) val tableFromQuery = TablesNamesFinder().getTables(sqlQuery as Statement).first() + // KNOWN LIMITATION: the ON condition is translated with the SAME row index on + // both sides ("diagonal pairing"): row i of one table is matched only with row i + // of the other. This is sufficient at the default numberOfRows=1 to force a + // non-empty JOIN, but it does not model full INNER JOIN semantics: for + // numberOfRows>=2 it never explores mismatched-index pairs (e.g. users2 with + // products1). Matching arbitrary row combinations is future work. for (i in 1..numberOfRows) { val constraint = parseQueryCondition(tableAliases, tableFromQuery, condition, i) smt.addNode(constraint) @@ -591,7 +604,11 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I companion object { - // Maps database column types to SMT-LIB types + // Maps database column types to SMT-LIB types. + // FUTURE WORK: this is one of three independent type vocabularies interpreting ColumnDto.type + // (the others are SMTLibZ3DbConstraintSolver.getColumnDataType and .hasColumnType). They can + // silently disagree when a backend reports a variant spelling; consolidating them into a single + // source of truth is future work (see the note on SMTLibZ3DbConstraintSolver.hasColumnType). private val TYPE_MAP = mapOf( "BIGINT" to "Int", "BIT" to "Int", @@ -602,6 +619,9 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I "INT8" to "Int", "TINYINT" to "Int", "SMALLINT" to "Int", + // KNOWN LIMITATION: NUMERIC is mapped to Int, so any fractional part is truncated. This is + // inconsistent with DECIMAL (mapped to Real). Mapping NUMERIC to Real (to preserve decimals) + // is future work. "NUMERIC" to "Int", "SERIAL" to "Int", "SMALLSERIAL" to "Int", diff --git a/docs/options.md b/docs/options.md index 33c730e4a4..0d5ab6dde6 100644 --- a/docs/options.md +++ b/docs/options.md @@ -347,6 +347,7 @@ There are 3 types of options: |`seedTestCasesPath`| __String__. File path where the seeded test cases are located. *Default value*: `postman.postman_collection.json`.| |`skipAIModelUpdateWhenResponseIs5xx`| __Boolean__. Determines whether the AI response classifier skips model updates when the response indicates a server-side error with status code 5xx. *Default value*: `false`.| |`skipAIModelUpdateWhenResponseIsNot2xxOr400`| __Boolean__. Determines whether the AI response classifier skips model updates when the response is not 2xx or 400. *Default value*: `false`.| +|`sqlZ3NumberOfRows`| __Int__. Number of rows the Z3 solver generates per table when solving a failed SQL query. The default of 1 is sufficient for the currently supported queries; generating a single row per table already forces the query to return a non-empty result. This will need to be increased once support for more complex JOINs (matching arbitrary row combinations, not just the diagonal pairing of row i with row i) is added. Only meaningful when generateSqlDataWithZ3=true. *Constraints*: `min=1.0`. *Depends on*: `generateSqlDataWithZ3=true`. *Default value*: `1`.| |`sqlZ3TimeoutMs`| __Int__. 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. A value of 0 disables the timeout. Only meaningful when generateSqlDataWithZ3=true. *Constraints*: `min=0.0`. *Depends on*: `generateSqlDataWithZ3=true`. *Default value*: `5000`.| |`statusOracles`| __Boolean__. Lightweight checks on HTTP status codes, e.g., a GET should not return a 201 Created. *Default value*: `false`.| |`structureMutationProFS`| __Double__. Specify a probability of applying structure mutator during the focused search. *Constraints*: `probability 0.0-1.0`. *Default value*: `0.0`.| From c36024fdba549868ffe0c24d328155b521eb0f20 Mon Sep 17 00:00:00 2001 From: Agustina Aldasoro Date: Thu, 9 Jul 2026 14:52:32 -0300 Subject: [PATCH 09/13] Add comments --- .../solver/smtlib/SMTResultParser.java | 5 +++ .../solver/Z3DockerExecutorTest.java | 40 +++++++++++-------- .../core/solver/SMTLibZ3DbConstraintSolver.kt | 11 +++++ 3 files changed, 40 insertions(+), 16 deletions(-) diff --git a/core-extra/solver/src/main/java/org/evomaster/solver/smtlib/SMTResultParser.java b/core-extra/solver/src/main/java/org/evomaster/solver/smtlib/SMTResultParser.java index 74e13dbe9b..9c75e0e6ea 100644 --- a/core-extra/solver/src/main/java/org/evomaster/solver/smtlib/SMTResultParser.java +++ b/core-extra/solver/src/main/java/org/evomaster/solver/smtlib/SMTResultParser.java @@ -18,6 +18,11 @@ public class SMTResultParser { /** * Parses the Z3 solver response and extracts variable values. * + * FRAGILITY: parsing is regex- and position-based and assumes Z3's textual get-value layout + * (one struct per line, constructor name split on '-', values split on whitespace). It therefore + * assumes string values contain no spaces, hyphens, quotes or parentheses; such values would be + * mis-split. Hardening the parser (or requesting values in a more robust format) is future work. + * * @param z3Response the raw response from Z3 solver * @return a {@link Z3Solution} mapping variable names to the {@link SMTLibValue} objects Z3 assigned to them */ 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 ecf4ba6327..fc4c99933e 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 @@ -13,8 +13,6 @@ import java.nio.file.Path; import java.nio.file.Paths; import java.nio.file.StandardCopyOption; -import java.util.HashMap; -import java.util.Map; import static org.junit.jupiter.api.Assertions.*; @@ -95,21 +93,31 @@ public void composedTypes() { assertEquals(Z3Result.Status.SAT, result.getStatus(), "Response should be SAT for composed_types.smt"); assertTrue(result.getSolution().containsKey("users1"), "Response should contain users1"); - Map users1Expected = new HashMap<>(); - users1Expected.put("ID", new LongValue(3L)); - users1Expected.put("NAME", new StringValue("Alice")); - users1Expected.put("AGE", new LongValue(31L)); - users1Expected.put("POINTS", new LongValue(7L)); - - assertEquals(new StructValue(users1Expected), result.getSolution().get("users1"), "The value for users1 is incorrect"); - assertTrue(result.getSolution().containsKey("users2"), "Response should contain users2"); - Map users2Expected = new HashMap<>(); - users2Expected.put("ID", new LongValue(3L)); - users2Expected.put("NAME", new StringValue("Bob")); - users2Expected.put("AGE", new LongValue(31L)); - users2Expected.put("POINTS", new LongValue(7L)); - assertEquals(new StructValue(users2Expected), result.getSolution().get("users2"), "The value for users2 is incorrect"); + + // NOTE: assert the individual field VALUES, not StructValue equality: StructValue.equals only + // compares the set of field names, so a whole-struct assertEquals would pass regardless of the + // actual values Z3 returned. We assert the fully-constrained fields exactly (NAME, POINTS) and + // the underconstrained fields against their SMT-LIB constraints (AGE range, distinct IDs). + StructValue users1 = (StructValue) result.getSolution().get("users1"); + StructValue users2 = (StructValue) result.getSolution().get("users2"); + + // NAME and POINTS are pinned by the SMT-LIB (NAME = "Alice"/"Bob", POINTS = 7), so deterministic. + assertEquals(new StringValue("Alice"), users1.getField("NAME"), "NAME users1"); + assertEquals(new StringValue("Bob"), users2.getField("NAME"), "NAME users2"); + assertEquals(new LongValue(7L), users1.getField("POINTS"), "POINTS users1"); + assertEquals(new LongValue(7L), users2.getField("POINTS"), "POINTS users2"); + + // AGE is constrained to (30, 100): assert the constraint holds rather than a specific value. + long age1 = ((LongValue) users1.getField("AGE")).getValue(); + long age2 = ((LongValue) users2.getField("AGE")).getValue(); + assertTrue(age1 > 30 && age1 < 100, "AGE users1 out of range: " + age1); + assertTrue(age2 > 30 && age2 < 100, "AGE users2 out of range: " + age2); + + // IDs must be distinct (the 'distinct' assertion over the PK). + long id1 = ((LongValue) users1.getField("ID")).getValue(); + long id2 = ((LongValue) users2.getField("ID")).getValue(); + assertNotEquals(id1, id2, "user IDs must be distinct"); } /** 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 eb347f1bdb..2c54259e62 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt @@ -70,6 +70,12 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { // 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 Z3 SQL generation is enabled in postConstruct — avoids allocating the map in runs where Z3 SQL generation is off. + // + // THREAD-SAFETY: this is an access-ordered LinkedHashMap (LRU), whose get() mutates internal order, + // so it is NOT thread-safe. It relies on solve() being called from a single thread, which holds today + // because the MIO search loop (and thus fitness evaluation / structure mutation) is single-threaded. + // If fitness evaluation is ever parallelized, this cache must be synchronized or replaced with a + // concurrent LRU, otherwise concurrent access would corrupt it (lost entries / ConcurrentModificationException). private var z3ResultCache: MutableMap, Z3Result>? = null companion object { @@ -206,6 +212,11 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { * (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) { From 9bee48070774a6f2f7525d2e74709af797fcb36a Mon Sep 17 00:00:00 2001 From: Agustina Aldasoro Date: Thu, 9 Jul 2026 19:45:13 -0300 Subject: [PATCH 10/13] Add constants --- .../evomaster/solver/Z3DockerExecutor.java | 19 ++-- .../solver/smtlib/CheckSatResponse.java | 16 +++ .../solver/smtlib/SMTResultParser.java | 4 +- .../core/solver/SMTLibZ3DbConstraintSolver.kt | 4 +- .../evomaster/core/solver/SmtLibGenerator.kt | 97 +++++++++++-------- 5 files changed, 84 insertions(+), 56 deletions(-) create mode 100644 core-extra/solver/src/main/java/org/evomaster/solver/smtlib/CheckSatResponse.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 92495bd26e..1c5ae5397a 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 @@ -1,5 +1,6 @@ package org.evomaster.solver; +import org.evomaster.solver.smtlib.CheckSatResponse; import org.evomaster.solver.smtlib.SMTResultParser; import org.testcontainers.containers.BindMode; import org.testcontainers.containers.Container; @@ -20,10 +21,10 @@ public class Z3DockerExecutor implements AutoCloseable { // The Docker entrypoint that keeps it running indefinitely public static final String ENTRYPOINT = "while :; do sleep 1000 ; done"; - // SMT-LIB (check-sat) response tokens returned by Z3 - private static final String SAT = "sat"; - private static final String UNSAT = "unsat"; - private static final String UNKNOWN = "unknown"; + // Z3 CLI invocation + private static final String Z3_COMMAND = "z3"; + // Soft per-query timeout flag: "-t:" makes (check-sat) return 'unknown' on expiry + private static final String TIMEOUT_FLAG_PREFIX = "-t:"; private final String containerPath = "/smt2-resources/"; private final GenericContainer z3Prover; @@ -77,8 +78,8 @@ public Z3Result solveFromFile(String fileName) { public Z3Result solveFromFile(String fileName, long timeoutMs) { try { Container.ExecResult result = timeoutMs > 0 - ? z3Prover.execInContainer("z3", "-t:" + timeoutMs, containerPath + fileName) - : z3Prover.execInContainer("z3", containerPath + fileName); + ? z3Prover.execInContainer(Z3_COMMAND, TIMEOUT_FLAG_PREFIX + timeoutMs, containerPath + fileName) + : z3Prover.execInContainer(Z3_COMMAND, containerPath + fileName); if (result.getExitCode() != 0) { return Z3Result.error("Z3 exited with code " + result.getExitCode() @@ -92,16 +93,16 @@ public Z3Result solveFromFile(String fileName, long timeoutMs) { } String trimmed = stdout.trim(); - if (trimmed.startsWith(UNSAT)) { + if (trimmed.startsWith(CheckSatResponse.UNSAT)) { return Z3Result.unsat(); } // "unknown" means Z3 could not decide (e.g. incomplete theory or timeout). // It must be handled explicitly: otherwise it would fall through and be parsed // as an empty model, silently masquerading as SAT. - if (trimmed.startsWith(UNKNOWN)) { + if (trimmed.startsWith(CheckSatResponse.UNKNOWN)) { return Z3Result.unknown(); } - if (!trimmed.startsWith(SAT)) { + if (!trimmed.startsWith(CheckSatResponse.SAT)) { return Z3Result.error("Unexpected Z3 output for file " + fileName + ": " + stdout); } diff --git a/core-extra/solver/src/main/java/org/evomaster/solver/smtlib/CheckSatResponse.java b/core-extra/solver/src/main/java/org/evomaster/solver/smtlib/CheckSatResponse.java new file mode 100644 index 0000000000..2e4707903e --- /dev/null +++ b/core-extra/solver/src/main/java/org/evomaster/solver/smtlib/CheckSatResponse.java @@ -0,0 +1,16 @@ +package org.evomaster.solver.smtlib; + +/** + * The textual response tokens produced by SMT-LIB's {@code (check-sat)} command, as returned by Z3. + * Shared between {@code Z3DockerExecutor} (which classifies the raw output) and {@link SMTResultParser} + * so the tokens are defined in a single place. + */ +public final class CheckSatResponse { + + private CheckSatResponse() { + } + + public static final String SAT = "sat"; + public static final String UNSAT = "unsat"; + public static final String UNKNOWN = "unknown"; +} diff --git a/core-extra/solver/src/main/java/org/evomaster/solver/smtlib/SMTResultParser.java b/core-extra/solver/src/main/java/org/evomaster/solver/smtlib/SMTResultParser.java index 9c75e0e6ea..8afb04fa86 100644 --- a/core-extra/solver/src/main/java/org/evomaster/solver/smtlib/SMTResultParser.java +++ b/core-extra/solver/src/main/java/org/evomaster/solver/smtlib/SMTResultParser.java @@ -53,14 +53,14 @@ public static Z3Solution parseZ3Response(String z3Response) { // Defensive: Z3DockerExecutor already classifies 'unsat'/'unknown' before invoking this // parser, so in practice only 'sat' models reach here. This guard is kept as a safety net // in case the parser is ever called directly with an unsat response. - if (line.startsWith("unsat")) { + if (line.startsWith(CheckSatResponse.UNSAT)) { throw new RuntimeException("Unsatisfiable problem"); } if (line.trim().isEmpty()) { continue; // Skip empty lines } - if (line.startsWith("sat")) { + if (line.startsWith(CheckSatResponse.SAT)) { buffer.setLength(0); // Reset buffer if a new result starts continue; } 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 2c54259e62..244272de4a 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt @@ -303,14 +303,14 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { var gene: Gene = IntegerGene(dbColumnName, 0) when (val columnValue = columns.getField(smtColumn)) { is StringValue -> { - gene = if (hasColumnType(schemaDto, table, dbColumnName, "BOOLEAN")) { + gene = if (hasColumnType(schemaDto, table, dbColumnName, SmtLibGenerator.BOOLEAN_TYPE)) { BooleanGene(dbColumnName, toBoolean(columnValue.value)) } else { StringGene(dbColumnName, columnValue.value) } } is LongValue -> { - gene = if (hasColumnType(schemaDto, table, dbColumnName, "TIMESTAMP")) { + gene = if (hasColumnType(schemaDto, table, dbColumnName, SmtLibGenerator.TIMESTAMP_TYPE)) { val epochSeconds = columnValue.value.toLong() val localDateTime = LocalDateTime.ofInstant( Instant.ofEpochSecond(epochSeconds), ZoneOffset.UTC 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 152a47d200..2bae07a322 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt @@ -169,20 +169,15 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I private fun appendBooleanConstraints(smt: SMTLib) { for (smtTable in smtTables) { for (column in smtTable.dto.columns) { - if (column.type.equals("BOOLEAN", ignoreCase = true)) { + if (column.type.equals(BOOLEAN_TYPE, ignoreCase = true)) { val columnName = smtTable.smtColumnName(column.name).uppercase() for (i in 1..numberOfRows) { smt.addNode( AssertSMTNode( OrAssertion( - listOf( - EqualsAssertion(listOf("($columnName ${smtTable.smtName}$i)", "\"true\"")), - EqualsAssertion(listOf("($columnName ${smtTable.smtName}$i)", "\"True\"")), - EqualsAssertion(listOf("($columnName ${smtTable.smtName}$i)", "\"TRUE\"")), - EqualsAssertion(listOf("($columnName ${smtTable.smtName}$i)", "\"false\"")), - EqualsAssertion(listOf("($columnName ${smtTable.smtName}$i)", "\"False\"")), - EqualsAssertion(listOf("($columnName ${smtTable.smtName}$i)", "\"FALSE\"")) - ) + BOOLEAN_LITERALS.map { literal -> + EqualsAssertion(listOf("($columnName ${smtTable.smtName}$i)", "\"$literal\"")) + } ) ) ) @@ -195,17 +190,15 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I private fun appendTimestampConstraints(smt: SMTLib) { for (smtTable in smtTables) { for (column in smtTable.dto.columns) { - if (column.type.equals("TIMESTAMP", ignoreCase = true)) { + if (column.type.equals(TIMESTAMP_TYPE, ignoreCase = true)) { val columnName = smtTable.smtColumnName(column.name).uppercase() - val lowerBound = 0 // Example for Unix epoch start - val upperBound = 32503680000 // Example for year 3000 in seconds for (i in 1..numberOfRows) { smt.addNode( AssertSMTNode( GreaterThanOrEqualsAssertion( "($columnName ${smtTable.smtName}$i)", - lowerBound.toString() + TIMESTAMP_EPOCH_LOWER_BOUND.toString() ) ) ) @@ -213,7 +206,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I AssertSMTNode( LessThanOrEqualsAssertion( "($columnName ${smtTable.smtName}$i)", - upperBound.toString() + TIMESTAMP_EPOCH_UPPER_BOUND.toString() ) ) ) @@ -604,44 +597,62 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I companion object { + // Bounds for TIMESTAMP columns, encoded as epoch seconds (SMT Int). + private const val TIMESTAMP_EPOCH_LOWER_BOUND = 0L // Unix epoch start + private const val TIMESTAMP_EPOCH_UPPER_BOUND = 32503680000L // ~year 3000, in seconds + + // SMT-LIB sorts used as TYPE_MAP targets. + private const val SMT_INT = "Int" + private const val SMT_REAL = "Real" + private const val SMT_STRING = "String" + + // SQL type names that need special interpretation beyond their SMT sort: BOOLEAN is encoded as an + // SMT String and TIMESTAMP as an SMT Int, so gene reconstruction must consult the original type. + // Shared with the comparison sites in this class and referenced by SMTLibZ3DbConstraintSolver. + const val BOOLEAN_TYPE = "BOOLEAN" + const val TIMESTAMP_TYPE = "TIMESTAMP" + + // The string values a BOOLEAN column may take (BOOLEAN is encoded as an SMT String). + private val BOOLEAN_LITERALS = listOf("true", "True", "TRUE", "false", "False", "FALSE") + // Maps database column types to SMT-LIB types. // FUTURE WORK: this is one of three independent type vocabularies interpreting ColumnDto.type // (the others are SMTLibZ3DbConstraintSolver.getColumnDataType and .hasColumnType). They can // silently disagree when a backend reports a variant spelling; consolidating them into a single // source of truth is future work (see the note on SMTLibZ3DbConstraintSolver.hasColumnType). private val TYPE_MAP = mapOf( - "BIGINT" to "Int", - "BIT" to "Int", - "INTEGER" to "Int", - "INT" to "Int", - "INT2" to "Int", - "INT4" to "Int", - "INT8" to "Int", - "TINYINT" to "Int", - "SMALLINT" to "Int", + "BIGINT" to SMT_INT, + "BIT" to SMT_INT, + "INTEGER" to SMT_INT, + "INT" to SMT_INT, + "INT2" to SMT_INT, + "INT4" to SMT_INT, + "INT8" to SMT_INT, + "TINYINT" to SMT_INT, + "SMALLINT" to SMT_INT, // KNOWN LIMITATION: NUMERIC is mapped to Int, so any fractional part is truncated. This is // inconsistent with DECIMAL (mapped to Real). Mapping NUMERIC to Real (to preserve decimals) // is future work. - "NUMERIC" to "Int", - "SERIAL" to "Int", - "SMALLSERIAL" to "Int", - "BIGSERIAL" to "Int", - "TIMESTAMP" to "Int", - "DATE" to "Int", - "FLOAT" to "Real", - "DOUBLE" to "Real", - "DECIMAL" to "Real", - "REAL" to "Real", - "CHARACTER VARYING" to "String", - "CHAR" to "String", - "VARCHAR" to "String", - "TEXT" to "String", - "CHARACTER LARGE OBJECT" to "String", - "BOOLEAN" to "String", - "BOOL" to "String", - "UUID" to "String", - "JSONB" to "String", - "BYTEA" to "String", + "NUMERIC" to SMT_INT, + "SERIAL" to SMT_INT, + "SMALLSERIAL" to SMT_INT, + "BIGSERIAL" to SMT_INT, + TIMESTAMP_TYPE to SMT_INT, + "DATE" to SMT_INT, + "FLOAT" to SMT_REAL, + "DOUBLE" to SMT_REAL, + "DECIMAL" to SMT_REAL, + "REAL" to SMT_REAL, + "CHARACTER VARYING" to SMT_STRING, + "CHAR" to SMT_STRING, + "VARCHAR" to SMT_STRING, + "TEXT" to SMT_STRING, + "CHARACTER LARGE OBJECT" to SMT_STRING, + BOOLEAN_TYPE to SMT_STRING, + "BOOL" to SMT_STRING, + "UUID" to SMT_STRING, + "JSONB" to SMT_STRING, + "BYTEA" to SMT_STRING, ) } } From 3ddb68cb3a088652eb817b0739d01d1214d93ff0 Mon Sep 17 00:00:00 2001 From: Agustina Aldasoro Date: Thu, 9 Jul 2026 19:55:51 -0300 Subject: [PATCH 11/13] Add stats --- .../org/evomaster/core/search/service/Statistics.kt | 11 +++++++++++ .../core/solver/SMTLibZ3DbConstraintSolver.kt | 7 +++++++ .../org/evomaster/core/solver/SmtLibGenerator.kt | 11 +++++++++++ 3 files changed, 29 insertions(+) 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 3b4549ceb7..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 @@ -97,6 +97,7 @@ class Statistics : SearchListener { private var sqlZ3UnknownCount = 0 private var sqlZ3ErrorCount = 0 private var sqlZ3ParseFailureCount = 0 + private var sqlZ3PartialTranslationCount = 0 private var sqlZ3TimeMs = 0L private var sqlZ3SmtlibGenTimeMs = 0L private val sqlZ3SmtlibSizeBytes = IncrementalAverage() @@ -276,6 +277,15 @@ class Statistics : SearchListener { sqlZ3ParseFailureCount++ } + /** + * A query whose WHERE/JOIN condition could not be fully translated to SMT-LIB (the untranslatable + * part was dropped). Counted independently of the SAT/UNSAT outcome, since the weakened formula is + * usually still SAT: the generated data may not satisfy the original query. + */ + fun reportSqlZ3PartialTranslation() { + sqlZ3PartialTranslationCount++ + } + fun reportSqlZ3SmtlibGenTime(ms: Long, sizeBytes: Int) { sqlZ3SmtlibGenTimeMs += ms sqlZ3SmtlibSizeBytes.addValue(sizeBytes) @@ -484,6 +494,7 @@ class Statistics : SearchListener { add(Pair("sqlZ3Unknown", "$sqlZ3UnknownCount")) add(Pair("sqlZ3Errors", "$sqlZ3ErrorCount")) add(Pair("sqlZ3ParseFailures", "$sqlZ3ParseFailureCount")) + add(Pair("sqlZ3PartialTranslations", "$sqlZ3PartialTranslationCount")) add(Pair("sqlZ3TotalMs", "$sqlZ3TimeMs")) add(Pair("sqlZ3SmtlibGenTotalMs", "$sqlZ3SmtlibGenTimeMs")) add(Pair("sqlZ3AvgSmtlibSizeBytes", "%.1f".format(sqlZ3SmtlibSizeBytes.mean))) 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 244272de4a..035ffa44fc 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt @@ -187,6 +187,13 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { val smtlibGenMs = System.currentTimeMillis() - smtlibGenStart stats?.reportSqlZ3SmtlibGenTime(smtlibGenMs, smtlibBytes) + // If a WHERE/JOIN condition could not be translated, it was dropped from the SMT problem, so the + // generated data may not satisfy the original query. Record it: this failure mode is otherwise + // invisible in the stats (Z3 typically still returns SAT on the weakened formula). + if (generator.skippedQueryConstraints > 0) { + stats?.reportSqlZ3PartialTranslation() + } + val fileName = storeToTmpFile(smtLib) val z3Start = System.currentTimeMillis() 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 2bae07a322..f7fcab91ec 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt @@ -32,6 +32,15 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I private var parser = JSqlConditionParser() + /** + * Number of query constraints (WHERE conditions, JOIN ON conditions) that could not be translated + * to SMT-LIB and were skipped during [generateSMT]. When greater than 0, the generated formula is + * weaker than the original query, so Z3 may return SAT with rows that do not satisfy the dropped + * predicate. Exposed so the caller can record it in the solver statistics. + */ + var skippedQueryConstraints = 0 + private set + private val smtTables: List = schema.tables.map { SmtTable(it) } private val smtTableByOriginalName: Map = smtTables.associateBy { it.originalName } @@ -420,6 +429,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I smt.addNode(constraint) } } catch (e: RuntimeException) { + skippedQueryConstraints++ LoggingUtil.getInfoLogger().warn("Could not translate WHERE clause to SMT-LIB, skipping: ${where}. Reason: ${e.message}") } } @@ -457,6 +467,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I smt.addNode(constraint) } } catch (e: RuntimeException) { + skippedQueryConstraints++ LoggingUtil.getInfoLogger().warn("Could not translate JOIN ON clause to SMT-LIB, skipping: ${onExpression}. Reason: ${e.message}") } } From c943596c1bcd2b1471a0028785430284021b1161 Mon Sep 17 00:00:00 2001 From: Agustina Aldasoro Date: Sat, 11 Jul 2026 13:50:14 -0300 Subject: [PATCH 12/13] PR feedback --- core/pom.xml | 28 +-- .../kotlin/org/evomaster/core/EMConfig.kt | 8 - .../core/search/service/Statistics.kt | 32 --- .../core/solver/SMTConditionVisitor.kt | 3 +- .../core/solver/SMTLibZ3DbConstraintSolver.kt | 115 ++-------- .../evomaster/core/solver/SmtLibGenerator.kt | 175 ++++++++------ .../core/solver/SmtLibGeneratorTest.kt | 214 ++++++++---------- pom.xml | 9 +- 8 files changed, 231 insertions(+), 353 deletions(-) diff --git a/core/pom.xml b/core/pom.xml index cbfe976037..d0ed6b3954 100644 --- a/core/pom.xml +++ b/core/pom.xml @@ -14,6 +14,15 @@ ${skipCore} + + 5120m @@ -33,10 +42,6 @@ org.evomaster evomaster-client-java-controller-api - - org.evomaster - evomaster-client-java-sql - org.evomaster evomaster-client-java-instrumentation-shared @@ -477,21 +482,6 @@ 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 48e94683b2..651d797745 100644 --- a/core/src/main/kotlin/org/evomaster/core/EMConfig.kt +++ b/core/src/main/kotlin/org/evomaster/core/EMConfig.kt @@ -1972,14 +1972,6 @@ 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 4375472f7f..b91b4846c5 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,13 +104,6 @@ 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 @@ -308,22 +301,6 @@ 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 @@ -500,15 +477,6 @@ 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/SMTConditionVisitor.kt b/core/src/main/kotlin/org/evomaster/core/solver/SMTConditionVisitor.kt index 91364728db..61908bab94 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SMTConditionVisitor.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SMTConditionVisitor.kt @@ -38,7 +38,8 @@ class SMTConditionVisitor( * @return The SMT-LIB column reference string. */ private fun getColumnReference(tableName: String, columnName: String): String { - return "(${convertToAscii(columnName).uppercase()} ${convertToAscii(tableName).lowercase()}$rowIndex)" + val rowConstant = SmtLibGenerator.rowConstantName(convertToAscii(tableName).lowercase(), rowIndex) + return "(${convertToAscii(columnName).uppercase()} $rowConstant)" } /** 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 035ffa44fc..9f1960e10a 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt @@ -5,7 +5,6 @@ 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 @@ -13,12 +12,6 @@ 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 @@ -71,11 +64,12 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { // Schema is assumed stable within a single run, so only query + row count form the key. // Null until Z3 SQL generation is enabled in postConstruct — avoids allocating the map in runs where Z3 SQL generation is off. // - // THREAD-SAFETY: this is an access-ordered LinkedHashMap (LRU), whose get() mutates internal order, - // so it is NOT thread-safe. It relies on solve() being called from a single thread, which holds today - // because the MIO search loop (and thus fitness evaluation / structure mutation) is single-threaded. - // If fitness evaluation is ever parallelized, this cache must be synchronized or replaced with a - // concurrent LRU, otherwise concurrent access would corrupt it (lost entries / ConcurrentModificationException). + // THREAD-SAFETY: the backing map is an access-ordered LinkedHashMap (a bounded LRU, whose get() mutates + // internal order), wrapped in Collections.synchronizedMap so every operation is guarded by the map's + // intrinsic lock. This is the standard idiom for a thread-safe bounded LRU (a plain ConcurrentHashMap + // cannot do access-order eviction). Compound get-then-put in solve() is intentionally not atomic: at + // worst two threads recompute the same query concurrently, which is harmless (idempotent), and never + // corrupts the map. This makes the cache safe for the parallelized fitness evaluation that is planned. private var z3ResultCache: MutableMap, Z3Result>? = null companion object { @@ -111,10 +105,11 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { private fun postConstruct() { if (config.generateSqlDataWithZ3) { initializeExecutor() - z3ResultCache = object : LinkedHashMap, Z3Result>(16, 0.75f, true) { + val lru = object : LinkedHashMap, Z3Result>(16, 0.75f, true) { override fun removeEldestEntry(eldest: MutableMap.MutableEntry, Z3Result>?) = size > MAX_CACHE_SIZE } + z3ResultCache = Collections.synchronizedMap(lru) } } @@ -210,33 +205,7 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { Z3Result.Status.SAT -> { stats?.reportSqlZ3Sat(z3TimeMs) z3ResultCache?.set(cacheKey, z3Result) - 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 + toSqlActionList(schemaDto, z3Result.solution) } Z3Result.Status.UNSAT -> { stats?.reportSqlZ3Unsat(z3TimeMs) @@ -387,15 +356,15 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { /** * Extracts the table name from a row-constant key by removing the trailing row index. * - * Row constants are named "${smtName}${i}" (e.g. "users1", "users2"). The trailing digits are - * stripped so this works for any number of rows (e.g. "users10" -> "users"), not just single-digit - * indices. Note: this still assumes table names themselves do not end in a digit. + * Row constants are named "${smtName}${SEP}${i}" (e.g. "users__1", "users__2"; see + * [SmtLibGenerator.rowConstantName]). Splitting on the last separator recovers the table name + * unambiguously even when the table name itself ends in digits (e.g. "inventory2026__1" -> "inventory2026"). * * @param key The key containing the table name and index. * @return The extracted table name. */ private fun getTableName(key: String): String { - return key.replace(Regex("\\d+$"), "") + return key.substringBeforeLast(SmtLibGenerator.ROW_INDEX_SEPARATOR) } /** @@ -488,7 +457,7 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { /** * Maps column types to ColumnDataType. * - * FUTURE WORK: this recognizes only a small subset of SQL type spellings and falls back to + * TODO: this recognizes only a small subset of SQL type spellings and falls back to * CHARACTER_VARYING for everything else. It is one of three independent type vocabularies that * interpret [ColumnDto.type] — the others being [SmtLibGenerator.TYPE_MAP] (SQL type -> SMT sort) * and [hasColumnType] (BOOLEAN/TIMESTAMP special-casing). These can silently disagree when a @@ -550,60 +519,4 @@ 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/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt b/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt index f7fcab91ec..53f42cb17d 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt @@ -44,6 +44,92 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I private val smtTables: List = schema.tables.map { SmtTable(it) } private val smtTableByOriginalName: Map = smtTables.associateBy { it.originalName } + companion object { + + /** + * Separator inserted between a table's SMT name and its 1-based row index in a row-constant + * name (e.g. "users__1"). Using an explicit separator (rather than just appending the index) + * keeps table names that end in digits (e.g. "inventory2026") unambiguous when the name is + * parsed back into its table part in SMTLibZ3DbConstraintSolver.getTableName. + */ + const val ROW_INDEX_SEPARATOR = "__" + + /** Bounds for TIMESTAMP columns, encoded as epoch seconds (SMT Int). */ + private const val TIMESTAMP_EPOCH_LOWER_BOUND = 0L // Unix epoch start + private const val TIMESTAMP_EPOCH_UPPER_BOUND = 32503680000L // ~year 3000, in seconds + + /** SMT-LIB sorts used as TYPE_MAP targets. */ + private const val SMT_INT = "Int" + private const val SMT_REAL = "Real" + private const val SMT_STRING = "String" + + /** + * SQL type names that need special interpretation beyond their SMT sort: BOOLEAN is encoded as + * an SMT String and TIMESTAMP as an SMT Int, so gene reconstruction must consult the original + * type. Shared with the comparison sites in this class and referenced by SMTLibZ3DbConstraintSolver. + */ + const val BOOLEAN_TYPE = "BOOLEAN" + const val TIMESTAMP_TYPE = "TIMESTAMP" + + /** + * The canonical string values a BOOLEAN column may take (BOOLEAN is encoded as an SMT String). + * These are generation constraints, so Z3 is forced to pick one of them; only the two canonical + * lowercase spellings are needed, and toBoolean() reads them back case-insensitively. + */ + private val BOOLEAN_LITERALS = listOf("true", "false") + + /** + * Builds the SMT row-constant name for a table's SMT name and a 1-based row index, + * e.g. rowConstantName("users", 1) == "users__1". Must be the single source of truth for + * this naming so declarations, assertions, get-value nodes and parsing all stay in sync. + */ + fun rowConstantName(smtTableName: String, rowIndex: Int): String = + "$smtTableName$ROW_INDEX_SEPARATOR$rowIndex" + + /** + * Maps database column types to SMT-LIB types. + * + * FIXME: this is one of three independent type vocabularies interpreting ColumnDto.type + * (the others are SMTLibZ3DbConstraintSolver.getColumnDataType and .hasColumnType). They can + * silently disagree when a backend reports a variant spelling; consolidating them into a single + * source of truth is future work (see the note on SMTLibZ3DbConstraintSolver.hasColumnType). + */ + private val TYPE_MAP = mapOf( + "BIGINT" to SMT_INT, + "BIT" to SMT_INT, + "INTEGER" to SMT_INT, + "INT" to SMT_INT, + "INT2" to SMT_INT, + "INT4" to SMT_INT, + "INT8" to SMT_INT, + "TINYINT" to SMT_INT, + "SMALLINT" to SMT_INT, + // FIXME: NUMERIC is mapped to Int, so any fractional part is truncated. This is + // inconsistent with DECIMAL (mapped to Real). Mapping NUMERIC to Real (to preserve decimals) + // is future work. + "NUMERIC" to SMT_INT, + "SERIAL" to SMT_INT, + "SMALLSERIAL" to SMT_INT, + "BIGSERIAL" to SMT_INT, + TIMESTAMP_TYPE to SMT_INT, + "DATE" to SMT_INT, + "FLOAT" to SMT_REAL, + "DOUBLE" to SMT_REAL, + "DECIMAL" to SMT_REAL, + "REAL" to SMT_REAL, + "CHARACTER VARYING" to SMT_STRING, + "CHAR" to SMT_STRING, + "VARCHAR" to SMT_STRING, + "TEXT" to SMT_STRING, + "CHARACTER LARGE OBJECT" to SMT_STRING, + BOOLEAN_TYPE to SMT_STRING, + "BOOL" to SMT_STRING, + "UUID" to SMT_STRING, + "JSONB" to SMT_STRING, + "BYTEA" to SMT_STRING, + ) + } + /** * Main method to generate SMT-LIB representation from SQL query. * @@ -78,7 +164,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I // Declare constants for each row for (i in 1..numberOfRows) { - smt.addNode(DeclareConstSMTNode("${smtTable.smtName}$i", smtTable.dataTypeName)) + smt.addNode(DeclareConstSMTNode(rowConstantName(smtTable.smtName, i), smtTable.dataTypeName)) } } } @@ -185,7 +271,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I AssertSMTNode( OrAssertion( BOOLEAN_LITERALS.map { literal -> - EqualsAssertion(listOf("($columnName ${smtTable.smtName}$i)", "\"$literal\"")) + EqualsAssertion(listOf("($columnName ${rowConstantName(smtTable.smtName, i)})", "\"$literal\"")) } ) ) @@ -206,7 +292,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I smt.addNode( AssertSMTNode( GreaterThanOrEqualsAssertion( - "($columnName ${smtTable.smtName}$i)", + "($columnName ${rowConstantName(smtTable.smtName, i)})", TIMESTAMP_EPOCH_LOWER_BOUND.toString() ) ) @@ -214,7 +300,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I smt.addNode( AssertSMTNode( LessThanOrEqualsAssertion( - "($columnName ${smtTable.smtName}$i)", + "($columnName ${rowConstantName(smtTable.smtName, i)})", TIMESTAMP_EPOCH_UPPER_BOUND.toString() ) ) @@ -266,8 +352,8 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I AssertSMTNode( DistinctAssertion( listOf( - "(${pkSelector.uppercase()} $tableName$i)", - "(${pkSelector.uppercase()} $tableName$j)" + "(${pkSelector.uppercase()} ${rowConstantName(tableName, i)})", + "(${pkSelector.uppercase()} ${rowConstantName(tableName, j)})" ) ) ) @@ -291,8 +377,8 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I for (j in i + 1..numberOfRows) { val columnDistinctness = pkSelectors.map { selector -> DistinctAssertion(listOf( - "(${selector.uppercase()} $tableName$i)", - "(${selector.uppercase()} $tableName$j)" + "(${selector.uppercase()} ${rowConstantName(tableName, i)})", + "(${selector.uppercase()} ${rowConstantName(tableName, j)})" )) } nodes.add(AssertSMTNode(OrAssertion(columnDistinctness))) @@ -314,7 +400,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I findReferencedPKSelector(smtTable.dto, referencedSmtTable.dto, foreignKey) ) - // KNOWN LIMITATION: composite foreign keys are not fully supported. Each source column is + // TODO: composite foreign keys are not fully supported. Each source column is // matched independently against a single referenced column, rather than constraining the // whole tuple of source columns to match a referenced tuple. This is correct for // single-column FKs (the common case) but under-models multi-column FKs. Fully supporting @@ -348,8 +434,8 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I val conditions = (1..numberOfRows).map { j -> EqualsAssertion( listOf( - "(${sourceColumnSelector.uppercase()} $sourceTableName$i)", - "(${referencedColumnSelector.uppercase()} $referencedTableName$j)" + "(${sourceColumnSelector.uppercase()} ${rowConstantName(sourceTableName, i)})", + "(${referencedColumnSelector.uppercase()} ${rowConstantName(referencedTableName, j)})" ) ) } @@ -450,13 +536,13 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I for (join in joins) { val onExpressions = join.onExpressions if (onExpressions.isNotEmpty()) { - // KNOWN LIMITATION: only the first ON expression is used; a composite ON + // TODO: only the first ON expression is used; a composite ON // (e.g. "a = b AND c = d") drops all but the first conjunct. val onExpression = onExpressions.elementAt(0) try { val condition = parser.parse(onExpression.toString(), toDBType(schema.databaseType)) val tableFromQuery = TablesNamesFinder().getTables(sqlQuery as Statement).first() - // KNOWN LIMITATION: the ON condition is translated with the SAME row index on + // TODO: the ON condition is translated with the SAME row index on // both sides ("diagonal pairing"): row i of one table is matched only with row i // of the other. This is sufficient at the default numberOfRows=1 to force a // non-empty JOIN, but it does not model full INNER JOIN semantics: for @@ -586,7 +672,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I for (smtTable in smtTables) { if (tablesMentioned.contains(smtTable.originalName)) { for (i in 1..numberOfRows) { - smt.addNode(GetValueSMTNode("${smtTable.smtName}$i")) + smt.addNode(GetValueSMTNode(rowConstantName(smtTable.smtName, i))) } } } @@ -605,65 +691,4 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I DeclareConstSMTNode(smtTable.smtColumnName(c.name), smtType) } } - - companion object { - - // Bounds for TIMESTAMP columns, encoded as epoch seconds (SMT Int). - private const val TIMESTAMP_EPOCH_LOWER_BOUND = 0L // Unix epoch start - private const val TIMESTAMP_EPOCH_UPPER_BOUND = 32503680000L // ~year 3000, in seconds - - // SMT-LIB sorts used as TYPE_MAP targets. - private const val SMT_INT = "Int" - private const val SMT_REAL = "Real" - private const val SMT_STRING = "String" - - // SQL type names that need special interpretation beyond their SMT sort: BOOLEAN is encoded as an - // SMT String and TIMESTAMP as an SMT Int, so gene reconstruction must consult the original type. - // Shared with the comparison sites in this class and referenced by SMTLibZ3DbConstraintSolver. - const val BOOLEAN_TYPE = "BOOLEAN" - const val TIMESTAMP_TYPE = "TIMESTAMP" - - // The string values a BOOLEAN column may take (BOOLEAN is encoded as an SMT String). - private val BOOLEAN_LITERALS = listOf("true", "True", "TRUE", "false", "False", "FALSE") - - // Maps database column types to SMT-LIB types. - // FUTURE WORK: this is one of three independent type vocabularies interpreting ColumnDto.type - // (the others are SMTLibZ3DbConstraintSolver.getColumnDataType and .hasColumnType). They can - // silently disagree when a backend reports a variant spelling; consolidating them into a single - // source of truth is future work (see the note on SMTLibZ3DbConstraintSolver.hasColumnType). - private val TYPE_MAP = mapOf( - "BIGINT" to SMT_INT, - "BIT" to SMT_INT, - "INTEGER" to SMT_INT, - "INT" to SMT_INT, - "INT2" to SMT_INT, - "INT4" to SMT_INT, - "INT8" to SMT_INT, - "TINYINT" to SMT_INT, - "SMALLINT" to SMT_INT, - // KNOWN LIMITATION: NUMERIC is mapped to Int, so any fractional part is truncated. This is - // inconsistent with DECIMAL (mapped to Real). Mapping NUMERIC to Real (to preserve decimals) - // is future work. - "NUMERIC" to SMT_INT, - "SERIAL" to SMT_INT, - "SMALLSERIAL" to SMT_INT, - "BIGSERIAL" to SMT_INT, - TIMESTAMP_TYPE to SMT_INT, - "DATE" to SMT_INT, - "FLOAT" to SMT_REAL, - "DOUBLE" to SMT_REAL, - "DECIMAL" to SMT_REAL, - "REAL" to SMT_REAL, - "CHARACTER VARYING" to SMT_STRING, - "CHAR" to SMT_STRING, - "VARCHAR" to SMT_STRING, - "TEXT" to SMT_STRING, - "CHARACTER LARGE OBJECT" to SMT_STRING, - BOOLEAN_TYPE to SMT_STRING, - "BOOL" to SMT_STRING, - "UUID" to SMT_STRING, - "JSONB" to SMT_STRING, - "BYTEA" to SMT_STRING, - ) - } } 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 49a15cdc70..aa8a120622 100644 --- a/core/src/test/kotlin/org/evomaster/core/solver/SmtLibGeneratorTest.kt +++ b/core/src/test/kotlin/org/evomaster/core/solver/SmtLibGeneratorTest.kt @@ -29,8 +29,8 @@ class SmtLibGeneratorTest { ) ) ) - addNode(DeclareConstSMTNode("products1", "ProductsRow")) - addNode(DeclareConstSMTNode("products2", "ProductsRow")) + addNode(DeclareConstSMTNode("products__1", "ProductsRow")) + addNode(DeclareConstSMTNode("products__2", "ProductsRow")) addNode( DeclareDatatypeSMTNode( "UsersRow", ImmutableList.of( @@ -43,27 +43,27 @@ class SmtLibGeneratorTest { ) ) ) - addNode(DeclareConstSMTNode("users1", "UsersRow")) - addNode(DeclareConstSMTNode("users2", "UsersRow")) + addNode(DeclareConstSMTNode("users__1", "UsersRow")) + addNode(DeclareConstSMTNode("users__2", "UsersRow")) addNode( - AssertSMTNode(DistinctAssertion(listOf("(DOCUMENT users1)", "(DOCUMENT users2)"))) + AssertSMTNode(DistinctAssertion(listOf("(DOCUMENT users__1)", "(DOCUMENT users__2)"))) ) addNode( AssertSMTNode( - EqualsAssertion(listOf("(NAME users1)", "\"Alice\"")) + EqualsAssertion(listOf("(NAME users__1)", "\"Alice\"")) ) ) addNode( AssertSMTNode( - EqualsAssertion(listOf("(NAME users2)", "\"Alice\"")) + EqualsAssertion(listOf("(NAME users__2)", "\"Alice\"")) ) ) addNode( AssertSMTNode( OrAssertion( listOf( - LessThanAssertion("(POINTS users1)", "4"), - GreaterThanAssertion("(POINTS users1)", "6") + LessThanAssertion("(POINTS users__1)", "4"), + GreaterThanAssertion("(POINTS users__1)", "6") ) ) ) @@ -72,8 +72,8 @@ class SmtLibGeneratorTest { AssertSMTNode( OrAssertion( listOf( - LessThanAssertion("(POINTS users2)", "4"), - GreaterThanAssertion("(POINTS users2)", "6") + LessThanAssertion("(POINTS users__2)", "4"), + GreaterThanAssertion("(POINTS users__2)", "6") ) ) ) @@ -82,8 +82,8 @@ class SmtLibGeneratorTest { AssertSMTNode( AndAssertion( listOf( - GreaterThanAssertion("(AGE users1)", "18"), - LessThanAssertion("(AGE users1)", "100") + GreaterThanAssertion("(AGE users__1)", "18"), + LessThanAssertion("(AGE users__1)", "100") ) ) ) @@ -92,38 +92,38 @@ class SmtLibGeneratorTest { AssertSMTNode( AndAssertion( listOf( - GreaterThanAssertion("(AGE users2)", "18"), - LessThanAssertion("(AGE users2)", "100") + GreaterThanAssertion("(AGE users__2)", "18"), + LessThanAssertion("(AGE users__2)", "100") ) ) ) ) addNode( AssertSMTNode( - LessThanOrEqualsAssertion("(POINTS users1)", "10") + LessThanOrEqualsAssertion("(POINTS users__1)", "10") ) ) addNode( AssertSMTNode( - LessThanOrEqualsAssertion("(POINTS users2)", "10") + LessThanOrEqualsAssertion("(POINTS users__2)", "10") ) ) addNode( AssertSMTNode( - GreaterThanOrEqualsAssertion("(POINTS users1)", "0") + GreaterThanOrEqualsAssertion("(POINTS users__1)", "0") ) ) addNode( AssertSMTNode( - GreaterThanOrEqualsAssertion("(POINTS users2)", "0") + GreaterThanOrEqualsAssertion("(POINTS users__2)", "0") ) ) addNode( AssertSMTNode( OrAssertion( listOf( - EqualsAssertion(listOf("(USER_ID products1)", "(ID users1)")), - EqualsAssertion(listOf("(USER_ID products1)", "(ID users2)")) + EqualsAssertion(listOf("(USER_ID products__1)", "(ID users__1)")), + EqualsAssertion(listOf("(USER_ID products__1)", "(ID users__2)")) ) ) ) @@ -132,8 +132,8 @@ class SmtLibGeneratorTest { AssertSMTNode( OrAssertion( listOf( - EqualsAssertion(listOf("(USER_ID products2)", "(ID users1)")), - EqualsAssertion(listOf("(USER_ID products2)", "(ID users2)")) + EqualsAssertion(listOf("(USER_ID products__2)", "(ID users__1)")), + EqualsAssertion(listOf("(USER_ID products__2)", "(ID users__2)")) ) ) ) @@ -142,8 +142,8 @@ class SmtLibGeneratorTest { AssertSMTNode( DistinctAssertion( listOf( - "(ID users1)", - "(ID users2)" + "(ID users__1)", + "(ID users__2)" ) ) ) @@ -152,12 +152,8 @@ class SmtLibGeneratorTest { AssertSMTNode( OrAssertion( listOf( - EqualsAssertion(listOf("(LUCKY users1)", "\"true\"")), - EqualsAssertion(listOf("(LUCKY users1)", "\"True\"")), - EqualsAssertion(listOf("(LUCKY users1)", "\"TRUE\"")), - EqualsAssertion(listOf("(LUCKY users1)", "\"false\"")), - EqualsAssertion(listOf("(LUCKY users1)", "\"False\"")), - EqualsAssertion(listOf("(LUCKY users1)", "\"FALSE\"")) + EqualsAssertion(listOf("(LUCKY users__1)", "\"true\"")), + EqualsAssertion(listOf("(LUCKY users__1)", "\"false\"")) ) ) ) @@ -166,12 +162,8 @@ class SmtLibGeneratorTest { AssertSMTNode( OrAssertion( listOf( - EqualsAssertion(listOf("(LUCKY users2)", "\"true\"")), - EqualsAssertion(listOf("(LUCKY users2)", "\"True\"")), - EqualsAssertion(listOf("(LUCKY users2)", "\"TRUE\"")), - EqualsAssertion(listOf("(LUCKY users2)", "\"false\"")), - EqualsAssertion(listOf("(LUCKY users2)", "\"False\"")), - EqualsAssertion(listOf("(LUCKY users2)", "\"FALSE\"")) + EqualsAssertion(listOf("(LUCKY users__2)", "\"true\"")), + EqualsAssertion(listOf("(LUCKY users__2)", "\"false\"")) ) ) ) @@ -221,11 +213,11 @@ class SmtLibGeneratorTest { val response: SMTLib = generator.generateSMT(selectStatement) val expected = tableConstraints - expected.addNode(AssertSMTNode(DistinctAssertion(listOf("(AGE users1)", "30")))) - expected.addNode(AssertSMTNode(DistinctAssertion(listOf("(AGE users2)", "30")))) + expected.addNode(AssertSMTNode(DistinctAssertion(listOf("(AGE users__1)", "30")))) + expected.addNode(AssertSMTNode(DistinctAssertion(listOf("(AGE users__2)", "30")))) expected.addNode(CheckSatSMTNode()) - expected.addNode(GetValueSMTNode("users1")) - expected.addNode(GetValueSMTNode("users2")) + expected.addNode(GetValueSMTNode("users__1")) + expected.addNode(GetValueSMTNode("users__2")) assertEquals(expected, response) } @@ -247,8 +239,8 @@ class SmtLibGeneratorTest { AssertSMTNode( AndAssertion( listOf( - GreaterThanAssertion("(AGE users1)", "30"), - EqualsAssertion(listOf("7", "(POINTS users1)")) + GreaterThanAssertion("(AGE users__1)", "30"), + EqualsAssertion(listOf("7", "(POINTS users__1)")) ) ) ) @@ -257,8 +249,8 @@ class SmtLibGeneratorTest { AssertSMTNode( AndAssertion( listOf( - GreaterThanAssertion("(AGE users2)", "30"), - EqualsAssertion(listOf("7", "(POINTS users2)")) + GreaterThanAssertion("(AGE users__2)", "30"), + EqualsAssertion(listOf("7", "(POINTS users__2)")) ) ) ) @@ -266,8 +258,8 @@ class SmtLibGeneratorTest { val satConstraints = arrayOf( CheckSatSMTNode(), - GetValueSMTNode("users1"), - GetValueSMTNode("users2") + GetValueSMTNode("users__1"), + GetValueSMTNode("users__2") ) for (constraint in satConstraints) { @@ -293,8 +285,8 @@ class SmtLibGeneratorTest { AssertSMTNode( AndAssertion( listOf( - GreaterThanAssertion("(AGE users1)", "30"), - EqualsAssertion(listOf("(POINTS users1)", "7")) + GreaterThanAssertion("(AGE users__1)", "30"), + EqualsAssertion(listOf("(POINTS users__1)", "7")) ) ) ) @@ -303,8 +295,8 @@ class SmtLibGeneratorTest { AssertSMTNode( AndAssertion( listOf( - GreaterThanAssertion("(AGE users2)", "30"), - EqualsAssertion(listOf("(POINTS users2)", "7")) + GreaterThanAssertion("(AGE users__2)", "30"), + EqualsAssertion(listOf("(POINTS users__2)", "7")) ) ) ) @@ -312,8 +304,8 @@ class SmtLibGeneratorTest { val satConstraints = arrayOf( CheckSatSMTNode(), - GetValueSMTNode("users1"), - GetValueSMTNode("users2") + GetValueSMTNode("users__1"), + GetValueSMTNode("users__2") ) for (constraint in satConstraints) { @@ -338,12 +330,12 @@ class SmtLibGeneratorTest { // JOIN ON constraints expected.addNode( AssertSMTNode( - EqualsAssertion(listOf("(ID users1)", "(USER_ID products1)")) + EqualsAssertion(listOf("(ID users__1)", "(USER_ID products__1)")) ) ) expected.addNode( AssertSMTNode( - EqualsAssertion(listOf("(ID users2)", "(USER_ID products2)")) + EqualsAssertion(listOf("(ID users__2)", "(USER_ID products__2)")) ) ) @@ -356,14 +348,14 @@ class SmtLibGeneratorTest { listOf( AndAssertion( listOf( - GreaterThanAssertion("(AGE users1)", "30"), - EqualsAssertion(listOf("(POINTS users1)", "7")) + GreaterThanAssertion("(AGE users__1)", "30"), + EqualsAssertion(listOf("(POINTS users__1)", "7")) ) ), - GreaterThanAssertion("(MIN_PRICE products1)", "500") + GreaterThanAssertion("(MIN_PRICE products__1)", "500") ) ), - EqualsAssertion(listOf("(STOCK products1)", "8")) + EqualsAssertion(listOf("(STOCK products__1)", "8")) ) ) ) @@ -376,14 +368,14 @@ class SmtLibGeneratorTest { listOf( AndAssertion( listOf( - GreaterThanAssertion("(AGE users2)", "30"), - EqualsAssertion(listOf("(POINTS users2)", "7")) + GreaterThanAssertion("(AGE users__2)", "30"), + EqualsAssertion(listOf("(POINTS users__2)", "7")) ) ), - GreaterThanAssertion("(MIN_PRICE products2)", "500") + GreaterThanAssertion("(MIN_PRICE products__2)", "500") ) ), - EqualsAssertion(listOf("(STOCK products2)", "8")) + EqualsAssertion(listOf("(STOCK products__2)", "8")) ) ) ) @@ -391,10 +383,10 @@ class SmtLibGeneratorTest { val satConstraints = arrayOf( CheckSatSMTNode(), - GetValueSMTNode("products1"), - GetValueSMTNode("products2"), - GetValueSMTNode("users1"), - GetValueSMTNode("users2") + GetValueSMTNode("products__1"), + GetValueSMTNode("products__2"), + GetValueSMTNode("users__1"), + GetValueSMTNode("users__2") ) for (constraint in satConstraints) { @@ -417,13 +409,13 @@ class SmtLibGeneratorTest { val expected = tableConstraints // The NULL comparison is skipped; only the non-null constraint is emitted - expected.addNode(AssertSMTNode(GreaterThanAssertion("(AGE users1)", "30"))) - expected.addNode(AssertSMTNode(GreaterThanAssertion("(AGE users2)", "30"))) + expected.addNode(AssertSMTNode(GreaterThanAssertion("(AGE users__1)", "30"))) + expected.addNode(AssertSMTNode(GreaterThanAssertion("(AGE users__2)", "30"))) val satConstraints = arrayOf( CheckSatSMTNode(), - GetValueSMTNode("users1"), - GetValueSMTNode("users2") + GetValueSMTNode("users__1"), + GetValueSMTNode("users__2") ) for (constraint in satConstraints) { expected.addNode(constraint) @@ -460,21 +452,17 @@ class SmtLibGeneratorTest { ) ) ) - expected.addNode(DeclareConstSMTNode("flags1", "FlagsRow")) - expected.addNode(DeclareConstSMTNode("flags2", "FlagsRow")) + expected.addNode(DeclareConstSMTNode("flags__1", "FlagsRow")) + expected.addNode(DeclareConstSMTNode("flags__2", "FlagsRow")) // Primary key distinct constraint - expected.addNode(AssertSMTNode(DistinctAssertion(listOf("(ID flags1)", "(ID flags2)")))) + expected.addNode(AssertSMTNode(DistinctAssertion(listOf("(ID flags__1)", "(ID flags__2)")))) // Boolean value constraints (generated because H2 reports BIT as BOOLEAN) expected.addNode( AssertSMTNode( OrAssertion( listOf( - EqualsAssertion(listOf("(FLAG flags1)", "\"true\"")), - EqualsAssertion(listOf("(FLAG flags1)", "\"True\"")), - EqualsAssertion(listOf("(FLAG flags1)", "\"TRUE\"")), - EqualsAssertion(listOf("(FLAG flags1)", "\"false\"")), - EqualsAssertion(listOf("(FLAG flags1)", "\"False\"")), - EqualsAssertion(listOf("(FLAG flags1)", "\"FALSE\"")) + EqualsAssertion(listOf("(FLAG flags__1)", "\"true\"")), + EqualsAssertion(listOf("(FLAG flags__1)", "\"false\"")) ) ) ) @@ -483,22 +471,18 @@ class SmtLibGeneratorTest { AssertSMTNode( OrAssertion( listOf( - EqualsAssertion(listOf("(FLAG flags2)", "\"true\"")), - EqualsAssertion(listOf("(FLAG flags2)", "\"True\"")), - EqualsAssertion(listOf("(FLAG flags2)", "\"TRUE\"")), - EqualsAssertion(listOf("(FLAG flags2)", "\"false\"")), - EqualsAssertion(listOf("(FLAG flags2)", "\"False\"")), - EqualsAssertion(listOf("(FLAG flags2)", "\"FALSE\"")) + EqualsAssertion(listOf("(FLAG flags__2)", "\"true\"")), + EqualsAssertion(listOf("(FLAG flags__2)", "\"false\"")) ) ) ) ) // Query constraint: id > 0 - expected.addNode(AssertSMTNode(GreaterThanAssertion("(ID flags1)", "0"))) - expected.addNode(AssertSMTNode(GreaterThanAssertion("(ID flags2)", "0"))) + expected.addNode(AssertSMTNode(GreaterThanAssertion("(ID flags__1)", "0"))) + expected.addNode(AssertSMTNode(GreaterThanAssertion("(ID flags__2)", "0"))) expected.addNode(CheckSatSMTNode()) - expected.addNode(GetValueSMTNode("flags1")) - expected.addNode(GetValueSMTNode("flags2")) + expected.addNode(GetValueSMTNode("flags__1")) + expected.addNode(GetValueSMTNode("flags__2")) assertEquals(expected, response) } finally { @@ -534,21 +518,21 @@ class SmtLibGeneratorTest { ) ) ) - expected.addNode(DeclareConstSMTNode("events1", "EventsRow")) - expected.addNode(DeclareConstSMTNode("events2", "EventsRow")) + expected.addNode(DeclareConstSMTNode("events__1", "EventsRow")) + expected.addNode(DeclareConstSMTNode("events__2", "EventsRow")) // Primary key distinct constraint - expected.addNode(AssertSMTNode(DistinctAssertion(listOf("(ID events1)", "(ID events2)")))) + expected.addNode(AssertSMTNode(DistinctAssertion(listOf("(ID events__1)", "(ID events__2)")))) // Timestamp range constraints (Unix epoch start to year 3000 in seconds) - expected.addNode(AssertSMTNode(GreaterThanOrEqualsAssertion("(CREATED_AT events1)", "0"))) - expected.addNode(AssertSMTNode(LessThanOrEqualsAssertion("(CREATED_AT events1)", "32503680000"))) - expected.addNode(AssertSMTNode(GreaterThanOrEqualsAssertion("(CREATED_AT events2)", "0"))) - expected.addNode(AssertSMTNode(LessThanOrEqualsAssertion("(CREATED_AT events2)", "32503680000"))) + expected.addNode(AssertSMTNode(GreaterThanOrEqualsAssertion("(CREATED_AT events__1)", "0"))) + expected.addNode(AssertSMTNode(LessThanOrEqualsAssertion("(CREATED_AT events__1)", "32503680000"))) + expected.addNode(AssertSMTNode(GreaterThanOrEqualsAssertion("(CREATED_AT events__2)", "0"))) + expected.addNode(AssertSMTNode(LessThanOrEqualsAssertion("(CREATED_AT events__2)", "32503680000"))) // Query constraint: id > 0 - expected.addNode(AssertSMTNode(GreaterThanAssertion("(ID events1)", "0"))) - expected.addNode(AssertSMTNode(GreaterThanAssertion("(ID events2)", "0"))) + expected.addNode(AssertSMTNode(GreaterThanAssertion("(ID events__1)", "0"))) + expected.addNode(AssertSMTNode(GreaterThanAssertion("(ID events__2)", "0"))) expected.addNode(CheckSatSMTNode()) - expected.addNode(GetValueSMTNode("events1")) - expected.addNode(GetValueSMTNode("events2")) + expected.addNode(GetValueSMTNode("events__1")) + expected.addNode(GetValueSMTNode("events__2")) assertEquals(expected, response) } finally { @@ -580,16 +564,16 @@ class SmtLibGeneratorTest { ) ) ) - expected.addNode(DeclareConstSMTNode("assignments1", "AssignmentsRow")) - expected.addNode(DeclareConstSMTNode("assignments2", "AssignmentsRow")) + expected.addNode(DeclareConstSMTNode("assignments__1", "AssignmentsRow")) + expected.addNode(DeclareConstSMTNode("assignments__2", "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)")) + DistinctAssertion(listOf("(EMPLOYEE_ID assignments__1)", "(EMPLOYEE_ID assignments__2)")), + DistinctAssertion(listOf("(PROJECT_ID assignments__1)", "(PROJECT_ID assignments__2)")) )))) expected.addNode(CheckSatSMTNode()) - expected.addNode(GetValueSMTNode("assignments1")) - expected.addNode(GetValueSMTNode("assignments2")) + expected.addNode(GetValueSMTNode("assignments__1")) + expected.addNode(GetValueSMTNode("assignments__2")) assertEquals(expected, response) } finally { @@ -605,11 +589,11 @@ class SmtLibGeneratorTest { 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(AssertSMTNode(GreaterThanAssertion("(AGE users__1)", "30"))) + expected.addNode(AssertSMTNode(GreaterThanAssertion("(AGE users__2)", "30"))) expected.addNode(CheckSatSMTNode()) - expected.addNode(GetValueSMTNode("users1")) - expected.addNode(GetValueSMTNode("users2")) + expected.addNode(GetValueSMTNode("users__1")) + expected.addNode(GetValueSMTNode("users__2")) assertEquals(expected, response) } @@ -622,11 +606,11 @@ class SmtLibGeneratorTest { 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(AssertSMTNode(GreaterThanAssertion("(AGE users__1)", "30"))) + expected.addNode(AssertSMTNode(GreaterThanAssertion("(AGE users__2)", "30"))) expected.addNode(CheckSatSMTNode()) - expected.addNode(GetValueSMTNode("users1")) - expected.addNode(GetValueSMTNode("users2")) + expected.addNode(GetValueSMTNode("users__1")) + expected.addNode(GetValueSMTNode("users__2")) assertEquals(expected, response) } diff --git a/pom.xml b/pom.xml index 1a8b38aada..07e285bb70 100644 --- a/pom.xml +++ b/pom.xml @@ -212,6 +212,11 @@ --add-opens java.base/jdk.internal.access.foreign=ALL-UNNAMED --add-opens java.base/java.nio=ALL-UNNAMED --add-opens java.base/java.lang.ref=ALL-UNNAMED --add-opens java.base/sun.nio.cs=ALL-UNNAMED --add-opens java.base/java.nio.charset=ALL-UNNAMED --add-opens java.base/sun.net.www.protocol.http=ALL-UNNAMED --add-opens java.base/sun.net.www.protocol.https=ALL-UNNAMED --add-opens java.base/java.time=ALL-UNNAMED --add-opens java.base/java.io=ALL-UNNAMED --add-opens java.logging/java.util.logging=ALL-UNNAMED --add-opens java.base/java.util.concurrent.atomic=ALL-UNNAMED --add-opens java.base/java.util=ALL-UNNAMED --add-opens java.base/java.util.regex=ALL-UNNAMED --add-opens java.base/java.net=ALL-UNNAMED --add-opens java.base/java.lang=ALL-UNNAMED true UTF-8 + + 4096m 17 @@ -1065,7 +1070,7 @@ Fucking JDK 17!!! And fuck you JEP 403!!! https://bugs.openjdk.java.net/browse/JDK-8266851 --> - @{argLine} -ea -Xms1024m -Xmx4096m -Xss4m -Dfile.encoding=UTF-8 -Djdk.attach.allowAttachSelf=true -Duser.language=en -Duser.country=GB ${addOpens} + @{argLine} -ea -Xms1024m -Xmx${testHeapXmx} -Xss4m -Dfile.encoding=UTF-8 -Djdk.attach.allowAttachSelf=true -Duser.language=en -Duser.country=GB ${addOpens} alphabetical @@ -1085,7 +1090,7 @@ ${redirectTestOutputToFile} 2 false - @{argLine} -ea -Xms1024m -Xmx4096m -Djdk.attach.allowAttachSelf=true -Duser.language=en -Duser.country=GB ${addOpens} + @{argLine} -ea -Xms1024m -Xmx${testHeapXmx} -Djdk.attach.allowAttachSelf=true -Duser.language=en -Duser.country=GB ${addOpens} alphabetical From 455d28a4e9c3ae06ba0db16ad3b1fde4084d687c Mon Sep 17 00:00:00 2001 From: Agustina Aldasoro Date: Sun, 12 Jul 2026 12:47:15 -0300 Subject: [PATCH 13/13] Fix build --- docs/options.md | 1 - 1 file changed, 1 deletion(-) diff --git a/docs/options.md b/docs/options.md index 0d5ab6dde6..f51c573d3f 100644 --- a/docs/options.md +++ b/docs/options.md @@ -328,7 +328,6 @@ 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`.|