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..430b287759 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt @@ -18,10 +18,12 @@ 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 @@ -54,9 +56,16 @@ 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. + private val z3ResultCache = mutableMapOf, Z3Result>() + @Inject private lateinit var config: EMConfig + @Inject + private lateinit var statistics: Statistics + @PostConstruct private fun postConstruct() { if (config.generateSqlDataWithDSE) { @@ -86,18 +95,66 @@ 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 + + if (collectStats) { + statistics.reportDseQuerySeen(sqlQuery.hashCode()) + } + + val cacheKey = Pair(sqlQuery, numberOfRows) + val cached = z3ResultCache[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'") + if (collectStats) statistics.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 + if (collectStats) { + statistics.reportDseSmtlibGenTime(smtlibGenMs, smtlibBytes) + } + val fileName = storeToTmpFile(smtLib) - val z3Response = executor.solveFromFile(fileName) - return toSqlActionList(schemaDto, z3Response) + val z3Start = System.currentTimeMillis() + val z3Result = executor.solveFromFile(fileName) + val z3TimeMs = System.currentTimeMillis() - z3Start + + return when (z3Result.status) { + Z3Result.Status.SAT -> { + if (collectStats) statistics.reportDseSat(z3TimeMs) + z3ResultCache[cacheKey] = z3Result + toSqlActionList(schemaDto, z3Result.model) + } + Z3Result.Status.UNSAT -> { + if (collectStats) statistics.reportDseUnsat(z3TimeMs) + z3ResultCache[cacheKey] = z3Result + emptyList() + } + Z3Result.Status.ERROR -> { + LoggingUtil.getInfoLogger().warn("DSE: Z3 error for query '$sqlQuery': ${z3Result.errorMessage}") + if (collectStats) statistics.reportDseError(z3TimeMs) + // Errors are not cached — they may be transient Docker failures + emptyList() + } + } } /** @@ -125,35 +182,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 +278,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 +293,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 +383,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 +404,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`.|