diff --git a/.gitignore b/.gitignore index f7671a5f39..22b50914a2 100644 --- a/.gitignore +++ b/.gitignore @@ -13,6 +13,7 @@ # virtual machine crash logs, see http://www.java.com/en/download/help/error_hotspot.xml hs_err_pid* +*.DS_Store /.idea/ .idea/ *.iml @@ -123,6 +124,7 @@ Migrations/ /e2e-tests/spring-rest-mysql-column-types/target/ /e2e-tests/spring-rest-postgres-column-types/target/ /e2e-tests/spring-rest-h2-column-types/target/ +/e2e-tests/spring-rest-h2-z3solver/target/ /test-old-libraries/target/ /e2e-tests/spring-web/target/ /e2e-tests/spring-rest-mongo/target/ @@ -166,6 +168,7 @@ Migrations/ /e2e-tests/spring-rest-bb/maven/target/ /target/ /wfc/target/ + /e2e-tests/emb-json/target/ /process_data/ /e2e-tests/spring-rest-multidb/target/ diff --git a/client-java/sql-dto/src/main/java/org/evomaster/client/java/controller/api/dto/database/execution/SqlExecutionsDto.java b/client-java/sql-dto/src/main/java/org/evomaster/client/java/controller/api/dto/database/execution/SqlExecutionsDto.java index 50cb7aaffb..c64b8904e9 100644 --- a/client-java/sql-dto/src/main/java/org/evomaster/client/java/controller/api/dto/database/execution/SqlExecutionsDto.java +++ b/client-java/sql-dto/src/main/java/org/evomaster/client/java/controller/api/dto/database/execution/SqlExecutionsDto.java @@ -54,9 +54,9 @@ public class SqlExecutionsDto { * Every time there is a WHERE clause which "failed" (ie, resulted in false), * we keep track of which tables/columns where involved in determining the * result of the WHERE. - * * If there is no WHERE, but still no data was returned, we consider it * as a failed WHERE + * The key is the table name and the value is the set of columns involved in the WHERE */ public Map> failedWhere = new HashMap<>(); diff --git a/core/src/main/kotlin/org/evomaster/core/BaseModule.kt b/core/src/main/kotlin/org/evomaster/core/BaseModule.kt index 7921106b87..be237f4c9f 100644 --- a/core/src/main/kotlin/org/evomaster/core/BaseModule.kt +++ b/core/src/main/kotlin/org/evomaster/core/BaseModule.kt @@ -14,8 +14,7 @@ import org.evomaster.core.search.service.mutator.MutationWeightControl import org.evomaster.core.search.service.mutator.genemutation.ArchiveGeneMutator import org.evomaster.core.search.tracer.ArchiveMutationTrackService import org.evomaster.core.search.tracer.TrackService - - +import org.evomaster.core.solver.SMTLibZ3DbConstraintSolver /** @@ -87,6 +86,9 @@ class BaseModule(val args: Array, val noTests: Boolean = false) : Abstra bind(ExecutionInfoReporter::class.java) .asEagerSingleton() + bind(SMTLibZ3DbConstraintSolver::class.java) + .asEagerSingleton() + //no longer needed if TestSuiteWriter is moved out? // if(noTests){ // bind(TestCaseWriter::class.java) diff --git a/core/src/main/kotlin/org/evomaster/core/Main.kt b/core/src/main/kotlin/org/evomaster/core/Main.kt index 3214c0b290..b692cc6c0e 100644 --- a/core/src/main/kotlin/org/evomaster/core/Main.kt +++ b/core/src/main/kotlin/org/evomaster/core/Main.kt @@ -12,8 +12,6 @@ import org.evomaster.core.AnsiColor.Companion.inRed import org.evomaster.core.AnsiColor.Companion.inYellow import org.evomaster.core.config.ConfigProblemException import org.evomaster.core.logging.LoggingUtil -import org.evomaster.core.output.OutputFormat -import org.evomaster.core.output.Termination import org.evomaster.core.output.TestSuiteSplitter import org.evomaster.core.output.clustering.SplitResult import org.evomaster.core.output.service.TestSuiteWriter 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 7e399ea40c..971375b788 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 @@ -22,6 +22,7 @@ import org.evomaster.core.search.gene.sql.SqlPrimaryKeyGene import org.evomaster.core.search.impact.impactinfocollection.ImpactsOfIndividual import org.evomaster.core.search.service.mutator.MutatedGeneSpecification import org.evomaster.core.search.service.mutator.StructureMutator +import org.evomaster.core.solver.SMTLibZ3DbConstraintSolver import org.evomaster.core.sql.SqlAction import org.evomaster.core.sql.SqlActionUtils import org.evomaster.core.sql.SqlInsertBuilder @@ -46,6 +47,9 @@ abstract class ApiWsStructureMutator : StructureMutator() { @Inject protected lateinit var harvestResponseHandler: HarvestActualHttpWsResponseHandler + @Inject + protected lateinit var z3Solver: SMTLibZ3DbConstraintSolver + override fun addAndHarvestExternalServiceActions( individual: EvaluatedIndividual<*>, /** @@ -268,7 +272,8 @@ abstract class ApiWsStructureMutator : StructureMutator() { val oldSqlActions = mutableListOf().plus(ind.seeInitializingActions()) - val addedSqlInsertions = handleFailedWhereSQL(ind, fw, mutatedGenes, sampler) + val failedWhereQueries = evaluatedIndividual.fitness.getViewOfAggregatedFailedWhereQueries() + val addedSqlInsertions = handleFailedWhereSQL(ind, fw, failedWhereQueries, mutatedGenes, sampler) ind.repairInitializationActions(randomness) // update impact based on added genes @@ -289,6 +294,10 @@ abstract class ApiWsStructureMutator : StructureMutator() { * Map of FAILED WHERE clauses. from table name key to column name values */ fw: Map>, + /** + * List queries with FAILED WHERE clauses + */ + failedWhereQueries: List, mutatedGenes: MutatedGeneSpecification?, sampler: ApiWsSampler ): MutableList>? { @@ -297,7 +306,7 @@ abstract class ApiWsStructureMutator : StructureMutator() { } if (config.generateSqlDataWithDSE) { - return handleDSE(sampler, fw) + return handleDSE(ind, sampler, failedWhereQueries) } return mutableListOf() @@ -385,9 +394,18 @@ abstract class ApiWsStructureMutator : StructureMutator() { return addedSqlInsertions } - private fun handleDSE(sampler: ApiWsSampler, fw: Map>): MutableList> { - /* TODO: DSE should be plugged in here */ - return mutableListOf() + private fun handleDSE(ind: T, sampler: ApiWsSampler, failedWhereQueries: List): MutableList> { + val schemaDto = sampler.sqlInsertBuilder?.schemaDto + ?: throw IllegalStateException("No DB schema is available") + + val newActions = mutableListOf>() + for (query in failedWhereQueries) { + val newActionsForQuery = z3Solver.solve(schemaDto, query) + newActions.addAll(mutableListOf(newActionsForQuery)) + ind.addInitializingDbActions(actions = newActionsForQuery) + } + + return newActions } private fun handleFailedFind( diff --git a/core/src/main/kotlin/org/evomaster/core/search/FitnessValue.kt b/core/src/main/kotlin/org/evomaster/core/search/FitnessValue.kt index ee737c8876..2d9fc0aacc 100644 --- a/core/src/main/kotlin/org/evomaster/core/search/FitnessValue.kt +++ b/core/src/main/kotlin/org/evomaster/core/search/FitnessValue.kt @@ -79,13 +79,19 @@ class FitnessValue( /** * When SUT does SQL commands using WHERE, keep track of when those "fails" (ie evaluate - * to false), in particular the tables and columns in them involved + * to false), in particular, the tables and columns in them involved */ private val aggregatedFailedWhere: MutableMap> = mutableMapOf() + /** + * When SUT does SQL commands using WHERE, keep track of when those "fails" (ie evaluate + * to false), in particular, the sql query involved + */ + private val aggregatedFailedWhereQueries: MutableList = mutableListOf() + /** * When SUT does MONGO commands using FIND, keep track of when those "fails" (ie evaluate - * to false), in particular the collection and fields in them involved + * to false), in particular, the collection and fields in them involved */ private val aggregatedFailedFind: MutableList = mutableListOf() @@ -140,6 +146,11 @@ class FitnessValue( databaseExecutions.values, {x -> x.failedWhere} )) + + aggregatedFailedWhereQueries.clear() + aggregatedFailedWhereQueries.addAll( + databaseExecutions.values.flatMap { a -> a.executionInfo }.map{ b -> b.sqlCommand } + ) } fun aggregateMongoDatabaseData(){ aggregatedFailedFind.clear() @@ -166,6 +177,8 @@ class FitnessValue( fun getViewOfAggregatedFailedWhere() = aggregatedFailedWhere + fun getViewOfAggregatedFailedWhereQueries() = aggregatedFailedWhereQueries + fun getViewOfAggregatedFailedFind() = aggregatedFailedFind fun doesCover(target: Int): Boolean { diff --git a/core/src/main/kotlin/org/evomaster/core/solver/DbConstraintSolver.kt b/core/src/main/kotlin/org/evomaster/core/solver/DbConstraintSolver.kt index 20ed170d42..2a3b2a9897 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/DbConstraintSolver.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/DbConstraintSolver.kt @@ -1,5 +1,6 @@ package org.evomaster.core.solver +import org.evomaster.client.java.controller.api.dto.database.schema.DbInfoDto import org.evomaster.core.sql.SqlAction /** @@ -10,7 +11,10 @@ interface DbConstraintSolver : AutoCloseable { /** * Solves the given constraints and returns the Db Gene to insert in the database + * @param schemaDto the schema of the database + * @param sqlQuery the query to solve + * @param numberOfRows the number of rows to insert in the db per table * @return a list of SQLAction with the inserts in the db for the given constraints */ - fun solve(sqlQuery: String): List + fun solve(schemaDto: DbInfoDto, sqlQuery: String, numberOfRows: Int = 1): List } 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 62aecc50ae..21517c100e 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SMTConditionVisitor.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SMTConditionVisitor.kt @@ -91,9 +91,13 @@ class SMTConditionVisitor( return when { operand.contains(".") -> { // Handle column references with aliases val parts = operand.split(".") - val tableName = tableAliases[parts[0]] ?: defaultTableName - val columnName = parts[parts.lastIndex] - getColumnReference(tableName, columnName) + if (tableAliases.containsKey(parts[0])) { + val tableName = tableAliases[parts[0]] ?: defaultTableName + val columnName = parts[parts.lastIndex] + getColumnReference(tableName, columnName) + } else { + operand + } } isAColumn(operand) -> { // Handle direct column references getColumnReference(defaultTableName, operand) 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 c0ad5b1bf1..f2a37eb99e 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt @@ -1,17 +1,21 @@ 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 +import org.apache.commons.io.FileUtils import org.evomaster.client.java.controller.api.dto.database.schema.ColumnDto import org.evomaster.client.java.controller.api.dto.database.schema.DatabaseType import org.evomaster.client.java.controller.api.dto.database.schema.DbInfoDto import org.evomaster.client.java.controller.api.dto.database.schema.TableDto +import org.evomaster.core.EMConfig import org.evomaster.core.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.sql.SqlPrimaryKeyGene import org.evomaster.core.search.gene.string.StringGene import org.evomaster.core.sql.SqlAction import org.evomaster.core.sql.schema.Column @@ -21,11 +25,16 @@ import org.evomaster.core.sql.schema.Table import org.evomaster.solver.Z3DockerExecutor import org.evomaster.solver.smtlib.SMTLib import org.evomaster.solver.smtlib.value.* +import java.io.File import java.io.IOException import java.nio.charset.StandardCharsets import java.nio.file.Files import java.nio.file.Paths import java.util.* +import javax.annotation.PostConstruct +import javax.annotation.PreDestroy +import kotlin.io.path.createDirectories +import kotlin.io.path.exists /** * An SMT solver implementation using Z3 in a Docker container. @@ -33,20 +42,39 @@ import java.util.* * then executes Z3 to get values and returns the necessary list of SqlActions * to satisfy the query. */ -class SMTLibZ3DbConstraintSolver( - private val schemaDto: DbInfoDto, // Database schema - private val resourcesFolder: String, // Folder for temporary resources - numberOfRows: Int = 2 // Number of rows to generate -) : DbConstraintSolver { +class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { - private val generator: SmtLibGenerator = SmtLibGenerator(schemaDto, numberOfRows) - private val executor: Z3DockerExecutor = Z3DockerExecutor(resourcesFolder) + // Create a temporary directory for tests + var resourcesFolder = Files.createTempDirectory("tmp").toString() + + private lateinit var executor: Z3DockerExecutor + private var idCounter: Long = 0L + + @Inject + private lateinit var config: EMConfig + + @PostConstruct + private fun postConstruct() { + if (config.generateSqlDataWithDSE) { + initializeExecutor() + } + } + + fun initializeExecutor() { + executor = Z3DockerExecutor(resourcesFolder) + } /** * Closes the Z3 Docker executor and cleans up temporary files. */ + @PreDestroy override fun close() { executor.close() + try { + FileUtils.cleanDirectory(File(resourcesFolder)) + } catch (e: IOException) { + throw RuntimeException("Error cleaning up resources folder", e) + } } /** @@ -56,13 +84,16 @@ class SMTLibZ3DbConstraintSolver( * @param sqlQuery The SQL query to solve. * @return A list of SQL actions that can be executed to satisfy the query. */ - override fun solve(sqlQuery: String): List { - val queryStatement = parseStatement(sqlQuery) // Parse SQL query - val smtLib = this.generator.generateSMT(queryStatement) // Generate SMTLib problem - val fileName = storeToTmpFile(smtLib) // Store SMTLib to a temporary file - val z3Response = executor.solveFromFile(fileName) // Solve using Z3 + 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 generator = SmtLibGenerator(schemaDto, numberOfRows) + val queryStatement = parseStatement(sqlQuery) + val smtLib = generator.generateSMT(queryStatement) + val fileName = storeToTmpFile(smtLib) + val z3Response = executor.solveFromFile(fileName) - return toSqlActionList(z3Response) // Convert Z3 response to SQL actions + return toSqlActionList(schemaDto, z3Response) } /** @@ -73,9 +104,9 @@ class SMTLibZ3DbConstraintSolver( */ private fun parseStatement(sqlQuery: String): Statement { return try { - CCJSqlParserUtil.parse(sqlQuery) // Parse query using JSQLParser + CCJSqlParserUtil.parse(sqlQuery) } catch (e: JSQLParserException) { - throw RuntimeException(e) // Rethrow exception if parsing fails + throw RuntimeException(e) } } @@ -85,15 +116,15 @@ class SMTLibZ3DbConstraintSolver( * @param z3Response The response from Z3. * @return A list of SQL actions. */ - private fun toSqlActionList(z3Response: Optional>): List { + private fun toSqlActionList(schemaDto: DbInfoDto, z3Response: Optional>): List { if (!z3Response.isPresent) { - return emptyList() // Return an empty list if no response + return emptyList() } val actions = mutableListOf() for (row in z3Response.get()) { - val tableName = getTableName(row.key) // Extract table name from the key + val tableName = getTableName(row.key) val columns = row.value as StructValue // Find table from schema and create SQL actions @@ -102,33 +133,37 @@ class SMTLibZ3DbConstraintSolver( // Create the list of genes with the values val genes = mutableListOf() for (columnName in columns.fields) { + var gene: Gene = IntegerGene(columnName, 0) when (val columnValue = columns.getField(columnName)) { is StringValue -> { - if (isBoolean(table, columnName)) { - val gene = BooleanGene(columnName, toBoolean(columnValue.value)) - genes.add(gene) + gene = if (isBoolean(schemaDto, table, columnName)) { + BooleanGene(columnName, toBoolean(columnValue.value)) } else { - val gene = StringGene(columnName, columnValue.value) - genes.add(gene) + StringGene(columnName, columnValue.value) } } is LongValue -> { - if (isTimestamp(table, columnName)) { - val gene = LongGene(columnName, columnValue.value.toLong()) - genes.add(gene) + gene = if (isTimestamp(table, columnName)) { + LongGene(columnName, columnValue.value.toLong()) } else { - val gene = IntegerGene(columnName, columnValue.value.toInt()) - genes.add(gene) + IntegerGene(columnName, columnValue.value.toInt()) } } is RealValue -> { - val gene = DoubleGene(columnName, columnValue.value) - genes.add(gene) + gene = DoubleGene(columnName, columnValue.value) } } + val currentColumn = table.columns.firstOrNull(){ it.name == columnName} + if (currentColumn != null && currentColumn.primaryKey) { + gene = SqlPrimaryKeyGene(columnName, tableName, gene, idCounter) + idCounter++ + } + gene.markAllAsInitialized() + genes.add(gene) } - val sqlAction = SqlAction(table, table.columns, -1, genes.toList()) + val sqlAction = SqlAction(table, table.columns, idCounter, genes.toList()) + idCounter++ actions.add(sqlAction) } @@ -139,7 +174,7 @@ class SMTLibZ3DbConstraintSolver( return value.equals("True", ignoreCase = true) } - private fun isBoolean(table: Table, columnName: String?): Boolean { + private fun isBoolean(schemaDto: DbInfoDto, table: Table, columnName: String?): Boolean { val col = schemaDto.tables.first { it.name == table.name }.columns.first { it.name == columnName } return col.type == "BOOLEAN" } @@ -171,7 +206,7 @@ class SMTLibZ3DbConstraintSolver( ?: throw RuntimeException("Table not found: $tableName") return Table( tableDto.name, - findColumns(tableDto), // Convert columns from DTO + findColumns(schema, tableDto), // Convert columns from DTO findForeignKeys(tableDto) // TODO: Implement this method ) } @@ -182,7 +217,7 @@ class SMTLibZ3DbConstraintSolver( * @param tableDto The table DTO containing column definitions. * @return A set of Column objects. */ - private fun findColumns(tableDto: TableDto): Set { + private fun findColumns(schemaDto: DbInfoDto, tableDto: TableDto): Set { return tableDto.columns.map { columnDto -> toColumnFromDto(columnDto, schemaDto.databaseType) }.toSet() @@ -271,20 +306,41 @@ class SMTLibZ3DbConstraintSolver( } /** - * Stores the SMTLib problem to a file in the resources folder. + * Stores the SMTLib problem to a file in the resources' folder. * * @param smtLib The SMTLib problem. * @return The filename of the stored SMTLib problem. */ private fun storeToTmpFile(smtLib: SMTLib): String { - val fileName = "smt2_${System.currentTimeMillis()}.smt2" - val filePath = this.resourcesFolder + fileName + val directoryPath = leadingBarResourcesFolder() + val fileNameBase = "smt2_${System.currentTimeMillis()}" + val fileExtension = ".smt2" try { - Files.write(Paths.get(filePath), smtLib.toString().toByteArray(StandardCharsets.UTF_8)) + // 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 } catch (e: IOException) { - throw RuntimeException("Error writing SMTLib to file", e) + throw RuntimeException("Failed to write SMTLib to file: ${e.message}") } - return fileName } + + private fun leadingBarResourcesFolder() = if (resourcesFolder.endsWith("/")) resourcesFolder else "$resourcesFolder/" } 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 9ada18e561..08efcf59ec 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt @@ -497,7 +497,8 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I private fun getConstructors(table: TableDto): List { return table.columns.map { c -> val smtType = TYPE_MAP[c.type.uppercase(Locale.getDefault())] - DeclareConstSMTNode(c.name, smtType!!) + ?: throw RuntimeException("Unsupported column type: ${c.type}") + DeclareConstSMTNode(c.name, smtType) } } @@ -509,6 +510,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I "TIMESTAMP" to "Int", "FLOAT" to "Real", "DOUBLE" to "Real", + "DECIMAL" to "Real", "CHARACTER VARYING" to "String", "CHAR" to "String", "CHARACTER LARGE OBJECT" to "String", diff --git a/core/src/main/kotlin/org/evomaster/core/sql/SqlInsertBuilder.kt b/core/src/main/kotlin/org/evomaster/core/sql/SqlInsertBuilder.kt index 8cf1a5e098..61c606dcff 100644 --- a/core/src/main/kotlin/org/evomaster/core/sql/SqlInsertBuilder.kt +++ b/core/src/main/kotlin/org/evomaster/core/sql/SqlInsertBuilder.kt @@ -17,7 +17,8 @@ import org.evomaster.core.logging.LoggingUtil class SqlInsertBuilder( - schemaDto: DbInfoDto, + public val schemaDto: DbInfoDto, + private val dbExecutor: DatabaseExecutor? = null ) { 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 3a77c7b05c..ebc8b0b0dc 100644 --- a/core/src/test/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolverTest.kt +++ b/core/src/test/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolverTest.kt @@ -1,25 +1,21 @@ package org.evomaster.core.solver import net.sf.jsqlparser.JSQLParserException -import org.apache.commons.io.FileUtils +import org.evomaster.client.java.controller.api.dto.database.schema.DbInfoDto import org.evomaster.client.java.sql.DbInfoExtractor import org.evomaster.client.java.sql.SqlScriptRunner import org.evomaster.core.search.gene.Gene import org.evomaster.core.search.gene.numeric.IntegerGene +import org.evomaster.core.search.gene.sql.SqlPrimaryKeyGene import org.evomaster.core.search.gene.string.StringGene import org.evomaster.solver.smtlib.* import org.junit.jupiter.api.AfterAll import org.junit.jupiter.api.Assertions.* import org.junit.jupiter.api.BeforeAll import org.junit.jupiter.api.Test -import java.io.File -import java.io.IOException -import java.nio.file.Files -import java.nio.file.Paths import java.sql.Connection import java.sql.DriverManager import java.sql.SQLException -import java.time.Instant class SMTLibZ3DbConstraintSolverTest { @@ -27,18 +23,16 @@ class SMTLibZ3DbConstraintSolverTest { companion object { private lateinit var solver: SMTLibZ3DbConstraintSolver private lateinit var connection: Connection - private lateinit var resourcesFolder: String + private lateinit var schemaDto: DbInfoDto @JvmStatic @BeforeAll fun setup() { connection = DriverManager.getConnection("jdbc:h2:mem:constraint_test", "sa", "") SqlScriptRunner.execCommand(connection, "CREATE TABLE users(id bigint generated by default as identity primary key, name varchar(255), age int, points int);\n") - val schemaDto = DbInfoExtractor.extract(connection) - - resourcesFolder = tmpResourcesFolder() - createFolder(resourcesFolder) - solver = SMTLibZ3DbConstraintSolver(schemaDto, resourcesFolder) + schemaDto = DbInfoExtractor.extract(connection) + solver = SMTLibZ3DbConstraintSolver() + solver.initializeExecutor() } @JvmStatic @@ -49,29 +43,6 @@ class SMTLibZ3DbConstraintSolverTest { if (this::solver.isInitialized) { solver.close() } - removeFolder(resourcesFolder) - } - - private fun tmpResourcesFolder(): String { - val instant = Instant.now().epochSecond.toString() - val tmpFolderPath = "tmp-solver$instant/" - return System.getProperty("user.dir") + "/src/test/resources/" + tmpFolderPath - } - - private fun createFolder(folderPath: String) { - try { - Files.createDirectories(Paths.get(folderPath)) - } catch (e: IOException) { - throw RuntimeException("Error creating tmp folder '$folderPath'. ", e) - } - } - - private fun removeFolder(folderPath: String) { - try { - FileUtils.deleteDirectory(File(folderPath)) - } catch (e: IOException) { - throw RuntimeException("Error deleting tmp folder '$folderPath'. ", e) - } } } @@ -83,7 +54,7 @@ class SMTLibZ3DbConstraintSolverTest { @Throws(JSQLParserException::class) fun selectFromUsers() { - val newActions = solver.solve("SELECT * FROM Users;") + val newActions = solver.solve(schemaDto, "SELECT * FROM Users;", 2) assertEquals(2, newActions.size) @@ -94,8 +65,9 @@ class SMTLibZ3DbConstraintSolverTest { for (gene in genesInsert1) { when (gene.name) { "ID" -> { - assertTrue(gene is IntegerGene) - assertEquals(0, (gene as IntegerGene).value) + assertTrue(gene is SqlPrimaryKeyGene) + val child = gene.getViewOfChildren().first() + assertEquals(0, (child as IntegerGene).value) } "NAME" -> { assertTrue(gene is StringGene) @@ -122,8 +94,9 @@ class SMTLibZ3DbConstraintSolverTest { for (gene in genesInsert2) { when (gene.name) { "ID" -> { - assertTrue(gene is IntegerGene) - assertEquals(1, (gene as IntegerGene).value) + assertTrue(gene is SqlPrimaryKeyGene) + val child = gene.getViewOfChildren().first() + assertEquals(1, (child as IntegerGene).value) } "NAME" -> { assertTrue(gene is StringGene) diff --git a/e2e-tests/pom.xml b/e2e-tests/pom.xml index b3968d43df..ebe6b88456 100644 --- a/e2e-tests/pom.xml +++ b/e2e-tests/pom.xml @@ -26,6 +26,7 @@ spring-rest-postgres-column-types spring-rest-mysql-column-types spring-rest-h2-column-types + spring-rest-h2-z3solver spring-web spring-rest-mongo spring-rest-bb diff --git a/e2e-tests/spring-rest-h2-z3solver/pom.xml b/e2e-tests/spring-rest-h2-z3solver/pom.xml new file mode 100644 index 0000000000..fce0920b9b --- /dev/null +++ b/e2e-tests/spring-rest-h2-z3solver/pom.xml @@ -0,0 +1,192 @@ + +4.0.0 + + + org.evomaster + evomaster-e2e-tests + 3.4.1-SNAPSHOT + + +evomaster-e2e-tests-spring-rest-h2-z3solver +jar + + + + + + + javax.validation + validation-api + 2.0.1.Final + + + + + javax.ws.rs + javax.ws.rs-api + + + org.evomaster + evomaster-e2e-tests-utils + test-jar + + + org.evomaster + evomaster-client-java-controller + + + org.evomaster + evomaster-core + test + + + org.evomaster + evomaster-client-java-instrumentation + test-jar + + + + org.springframework.boot + spring-boot-starter-web + + + org.springframework.boot + spring-boot-starter-data-jpa + + + org.springframework.boot + spring-boot-starter-security + + + com.h2database + h2 + + + org.locationtech.jts + jts-core + 1.19.0 + + + + com.google.code.gson + gson + + + + io.springfox + springfox-swagger2 + + + io.swagger + * + + + + + io.springfox + springfox-spring-web + + + io.swagger + swagger-parser + + + + + org.jetbrains.kotlin + kotlin-stdlib + + + + io.rest-assured + rest-assured + + + org.hamcrest + hamcrest-all + + + org.junit.jupiter + junit-jupiter-engine + + + org.junit.platform + junit-platform-launcher + + + org.junit.jupiter + junit-jupiter-params + + + + + javax.xml.bind + jaxb-api + + + org.glassfish.jaxb + jaxb-runtime + + + + + edu.stanford.nlp + stanford-corenlp + ${nlp.version} + test + + + edu.stanford.nlp + stanford-corenlp + ${nlp.version} + models + test + + + + + com.github.tomakehurst + wiremock-jre8-standalone + test + + + com.alibaba + dns-cache-manipulator + + + org.apache.httpcomponents + httpclient + + + com.squareup.okhttp3 + okhttp + + + + + + + + kotlin-maven-plugin + org.jetbrains.kotlin + + + org.apache.maven.plugins + maven-compiler-plugin + + + + + + + skipE2E_V2 + + true + + + + + \ No newline at end of file diff --git a/e2e-tests/spring-rest-h2-z3solver/src/main/java/com/foo/spring/rest/h2/z3solver/SwaggerConfiguration.java b/e2e-tests/spring-rest-h2-z3solver/src/main/java/com/foo/spring/rest/h2/z3solver/SwaggerConfiguration.java new file mode 100644 index 0000000000..6fe131411d --- /dev/null +++ b/e2e-tests/spring-rest-h2-z3solver/src/main/java/com/foo/spring/rest/h2/z3solver/SwaggerConfiguration.java @@ -0,0 +1,32 @@ +package com.foo.spring.rest.h2.z3solver; + +import org.springframework.context.annotation.Bean; +import org.springframework.security.core.Authentication; +import org.springframework.web.context.request.WebRequest; +import springfox.documentation.builders.ApiInfoBuilder; +import springfox.documentation.service.ApiInfo; +import springfox.documentation.spi.DocumentationType; +import springfox.documentation.spring.web.plugins.Docket; + +import static springfox.documentation.builders.PathSelectors.regex; + +public class SwaggerConfiguration { + + @Bean + public Docket docketApi() { + return new Docket(DocumentationType.SWAGGER_2) + .apiInfo(apiInfo()) + .select() + .paths(regex("/api/.*")) + .build() + .ignoredParameterTypes(WebRequest.class, Authentication.class); + } + + private ApiInfo apiInfo() { + return new ApiInfoBuilder() + .title("API") + .description("Some description") + .version("1.0") + .build(); + } +} diff --git a/e2e-tests/spring-rest-h2-z3solver/src/main/java/com/foo/spring/rest/h2/z3solver/Z3SolverApplication.java b/e2e-tests/spring-rest-h2-z3solver/src/main/java/com/foo/spring/rest/h2/z3solver/Z3SolverApplication.java new file mode 100644 index 0000000000..32ec1c016c --- /dev/null +++ b/e2e-tests/spring-rest-h2-z3solver/src/main/java/com/foo/spring/rest/h2/z3solver/Z3SolverApplication.java @@ -0,0 +1,16 @@ +package com.foo.spring.rest.h2.z3solver; + +import org.springframework.boot.SpringApplication; +import org.springframework.boot.autoconfigure.SpringBootApplication; +import org.springframework.boot.autoconfigure.security.servlet.SecurityAutoConfiguration; +import springfox.documentation.swagger2.annotations.EnableSwagger2; + +@EnableSwagger2 +@SpringBootApplication(exclude = SecurityAutoConfiguration.class) +public class Z3SolverApplication extends SwaggerConfiguration { + + public static void main(String[] args) { + SpringApplication.run(Z3SolverApplication.class, args); + } + +} diff --git a/e2e-tests/spring-rest-h2-z3solver/src/main/java/com/foo/spring/rest/h2/z3solver/Z3SolverTypesRest.java b/e2e-tests/spring-rest-h2-z3solver/src/main/java/com/foo/spring/rest/h2/z3solver/Z3SolverTypesRest.java new file mode 100644 index 0000000000..beb89f8216 --- /dev/null +++ b/e2e-tests/spring-rest-h2-z3solver/src/main/java/com/foo/spring/rest/h2/z3solver/Z3SolverTypesRest.java @@ -0,0 +1,79 @@ +package com.foo.spring.rest.h2.z3solver; + +import org.springframework.beans.factory.annotation.Autowired; +import org.springframework.http.ResponseEntity; +import org.springframework.web.bind.annotation.GetMapping; +import org.springframework.web.bind.annotation.PathVariable; +import org.springframework.web.bind.annotation.RequestMapping; +import org.springframework.web.bind.annotation.RestController; + +import javax.persistence.EntityManager; +import javax.persistence.Query; +import java.util.List; + +/** + * Created by agusaldasoro on 04-Oct-24. + */ +@RestController +@RequestMapping(path = "/api/h2/z3solver/") +public class Z3SolverTypesRest { + + @Autowired + private EntityManager em; + +// // TODO: Fix this. This fails to load, as when the WHERE clause is empty, it fails to calculate the failedWhere +// @GetMapping("/products") +// public ResponseEntity getEmptyWhere() { +// Query query = em.createNativeQuery( +// "select (1) from products"); +// List data = query.getResultList(); +// +// if (data.isEmpty()) { +// return ResponseEntity.status(400).build(); +// } else { +// return ResponseEntity.status(200).build(); +// } +// } + + @GetMapping("/products-1") + public ResponseEntity getId1() { + Query query = em.createNativeQuery( + "select (1) from products where id = 1"); + List data = query.getResultList(); + + if (data.isEmpty()) { + return ResponseEntity.status(400).build(); + } else { + return ResponseEntity.status(200).build(); + } + } + +// @GetMapping("/products-2/{id}") +// public ResponseEntity getIdNamePrice(@PathVariable("id") Long id) { +// try { +// Query query = em.createNativeQuery("SELECT * FROM products WHERE id = $id" + id); +// List data = query.getResultList(); +// +// if (data.isEmpty()) { +// return ResponseEntity.status(400).build(); +// } else { +// return ResponseEntity.status(200).build(); +// } +// } catch (Exception e) { +// return ResponseEntity.status(400).build(); +// } +// } + + @GetMapping("/products-3") + public ResponseEntity getProductsWithName() { + Query query = em.createNativeQuery("SELECT (1) FROM products WHERE id = 2 AND name = 'Agus' AND price = 10.0"); + List data = query.getResultList(); + + if (data.isEmpty()) { + return ResponseEntity.status(400).build(); + } else { + return ResponseEntity.status(200).build(); + } + } +} + diff --git a/e2e-tests/spring-rest-h2-z3solver/src/test/java/com/foo/spring/rest/h2/z3solver/SpringController.java b/e2e-tests/spring-rest-h2-z3solver/src/test/java/com/foo/spring/rest/h2/z3solver/SpringController.java new file mode 100644 index 0000000000..f2059c2a51 --- /dev/null +++ b/e2e-tests/spring-rest-h2-z3solver/src/test/java/com/foo/spring/rest/h2/z3solver/SpringController.java @@ -0,0 +1,83 @@ +package com.foo.spring.rest.h2.z3solver; + +import org.evomaster.client.java.controller.EmbeddedSutController; +import org.evomaster.client.java.controller.api.dto.SutInfoDto; +import org.evomaster.client.java.controller.api.dto.auth.AuthenticationDto; +import org.evomaster.client.java.controller.problem.ProblemInfo; +import org.evomaster.client.java.controller.problem.RestProblem; +import org.evomaster.client.java.sql.DbSpecification; +import org.springframework.boot.SpringApplication; +import org.springframework.context.ConfigurableApplicationContext; + +import java.util.List; +import java.util.Map; +import java.util.Objects; + +public abstract class SpringController extends EmbeddedSutController { + + protected ConfigurableApplicationContext ctx; + protected final Class applicationClass; + + protected SpringController(Class applicationClass) { + this.applicationClass = applicationClass; + super.setControllerPort(0); + } + + @Override + public String startSut() { + + ctx = SpringApplication.run(applicationClass, "--server.port=0"); + + return "http://localhost:" + getSutPort(); + } + + protected int getSutPort() { + return (Integer) ((Map) Objects.requireNonNull(ctx.getEnvironment() + .getPropertySources().get("server.ports")).getSource()) + .get("local.server.port"); + } + + @Override + public boolean isSutRunning() { + return ctx != null && ctx.isRunning(); + } + + @Override + public void stopSut() { + ctx.stop(); + ctx.close(); + } + + @Override + public String getPackagePrefixesToCover() { + return "com.foo."; + } + + @Override + public void resetStateOfSUT() { + // nothing to do + } + + @Override + public ProblemInfo getProblemInfo() { + return new RestProblem( + "http://localhost:" + getSutPort() + "/v2/api-docs", + null + ); + } + + @Override + public List getInfoForAuthentication() { + return null; + } + + @Override + public List getDbSpecifications() { + return null; + } + + @Override + public SutInfoDto.OutputFormat getPreferredOutputFormat() { + return SutInfoDto.OutputFormat.JAVA_JUNIT_5; + } +} diff --git a/e2e-tests/spring-rest-h2-z3solver/src/test/java/com/foo/spring/rest/h2/z3solver/Z3SolverController.java b/e2e-tests/spring-rest-h2-z3solver/src/test/java/com/foo/spring/rest/h2/z3solver/Z3SolverController.java new file mode 100644 index 0000000000..949c4d9bbb --- /dev/null +++ b/e2e-tests/spring-rest-h2-z3solver/src/test/java/com/foo/spring/rest/h2/z3solver/Z3SolverController.java @@ -0,0 +1,105 @@ +package com.foo.spring.rest.h2.z3solver; + +import kotlin.random.Random; +import org.evomaster.client.java.controller.InstrumentedSutStarter; +import org.evomaster.client.java.controller.api.dto.database.schema.DatabaseType; +import org.evomaster.client.java.sql.DbSpecification; +import org.hibernate.dialect.H2Dialect; +import org.springframework.boot.SpringApplication; +import org.springframework.jdbc.core.JdbcTemplate; + +import java.sql.Connection; +import java.sql.PreparedStatement; +import java.sql.SQLException; +import java.util.Collections; +import java.util.List; +import java.util.Objects; + +public class Z3SolverController extends SpringController { + + private static final String CREATE_TABLES_SQL = "CREATE TABLE products (\n" + + " id INTEGER NOT NULL,\n" + + " name VARCHAR(255) NOT NULL,\n" + + " price DECIMAL(10,2) NOT NULL,\n" + + " PRIMARY KEY (id)\n" + + ");"; + + public Z3SolverController() { + this(Z3SolverApplication.class); + } + + public static void main(String[] args) { + Z3SolverController controller = new Z3SolverController(); + controller.setControllerPort(40100); + InstrumentedSutStarter starter = new InstrumentedSutStarter(controller); + starter.start(); + } + + static { + /* + * To avoid issues with non-determinism checks (in particular in the handling of taint-analysis), + * we must disable the cache in H2 + */ + System.setProperty("h2.objectCache", "false"); + } + + protected Connection sqlConnection; + + protected Z3SolverController(Class applicationClass) { + super(applicationClass); + } + + @Override + public String startSut() { + + // lot of a problem if using same H2 instance. see: + // https://github.com/h2database/h2database/issues/227 + int rand = Random.Default.nextInt(); + + ctx = SpringApplication.run(applicationClass, "--server.port=0", + "--spring.datasource.url=jdbc:h2:mem:testdb_" + rand + ";DB_CLOSE_DELAY=-1;", + "--spring.jpa.database-platform=" + H2Dialect.class.getName(), + "--spring.datasource.username=sa", + "--spring.datasource.password", + "--spring.jpa.properties.hibernate.show_sql=true"); + + if (sqlConnection != null) { + try { + sqlConnection.close(); + } catch (SQLException e) { + e.printStackTrace(); + } + } + JdbcTemplate jdbc = ctx.getBean(JdbcTemplate.class); + + try { + sqlConnection = Objects.requireNonNull(jdbc.getDataSource()).getConnection(); + } catch (SQLException e) { + throw new RuntimeException(e); + } + + // execute create table + try { + createTables(); + } catch (SQLException e) { + throw new RuntimeException(e); + } + + return "http://localhost:" + getSutPort(); + } + + private void createTables() throws SQLException { + PreparedStatement stmt = sqlConnection.prepareStatement(CREATE_TABLES_SQL); + stmt.execute(); + } + + @Override + public void stopSut() { + super.stopSut(); + } + + @Override + public List getDbSpecifications() { + return Collections.singletonList(new DbSpecification(DatabaseType.H2, sqlConnection)); + } +} diff --git a/e2e-tests/spring-rest-h2-z3solver/src/test/java/org/evomaster/e2etests/spring/h2/z3solver/SpringTestBase.java b/e2e-tests/spring-rest-h2-z3solver/src/test/java/org/evomaster/e2etests/spring/h2/z3solver/SpringTestBase.java new file mode 100644 index 0000000000..315f93450c --- /dev/null +++ b/e2e-tests/spring-rest-h2-z3solver/src/test/java/org/evomaster/e2etests/spring/h2/z3solver/SpringTestBase.java @@ -0,0 +1,12 @@ +package org.evomaster.e2etests.spring.h2.z3solver; + +import org.evomaster.client.java.controller.EmbeddedSutController; +import org.evomaster.e2etests.utils.RestTestBase; + +public class SpringTestBase extends RestTestBase { + + protected static void initClass(EmbeddedSutController controller) throws Exception { + + RestTestBase.initClass(controller); + } +} \ No newline at end of file diff --git a/e2e-tests/spring-rest-h2-z3solver/src/test/java/org/evomaster/e2etests/spring/h2/z3solver/Z3SolverEMTest.java b/e2e-tests/spring-rest-h2-z3solver/src/test/java/org/evomaster/e2etests/spring/h2/z3solver/Z3SolverEMTest.java new file mode 100644 index 0000000000..0e264a326c --- /dev/null +++ b/e2e-tests/spring-rest-h2-z3solver/src/test/java/org/evomaster/e2etests/spring/h2/z3solver/Z3SolverEMTest.java @@ -0,0 +1,54 @@ +package org.evomaster.e2etests.spring.h2.z3solver; + +import com.foo.spring.rest.h2.z3solver.Z3SolverController; +import org.evomaster.core.problem.rest.HttpVerb; +import org.evomaster.core.problem.rest.RestIndividual; +import org.evomaster.core.search.Solution; +import org.junit.jupiter.api.BeforeAll; +import org.junit.jupiter.api.Test; + +import static org.junit.jupiter.api.Assertions.assertFalse; + +public class Z3SolverEMTest extends SpringTestBase { + + @BeforeAll + public static void initClass() throws Exception { + + SpringTestBase.initClass(new Z3SolverController()); + } + + @Test + public void testRunEM() throws Throwable { + + runTestHandlingFlakyAndCompilation( + "Z3SolverEM", + "com.foo.spring.rest.h2.z3solver.Z3SolverEvoMaster", + 50, + (args) -> { + args.add("--heuristicsForSQL"); + args.add("true"); + args.add("--generateSqlDataWithSearch"); + args.add("false"); + args.add("--generateSqlDataWithDSE"); + args.add("true"); + + Solution solution = initAndRun(args); + + assertFalse(solution.getIndividuals().isEmpty()); + + // TODO: Add support for queries with empty WHERE in the select + // assertHasAtLeastOne(solution, HttpVerb.GET, 400, "/api/h2/z3solver/products", null); + // assertHasAtLeastOne(solution, HttpVerb.GET, 200, "/api/h2/z3solver/products", null); + + assertHasAtLeastOne(solution, HttpVerb.GET, 400, "/api/h2/z3solver/products-1", null); + assertHasAtLeastOne(solution, HttpVerb.GET, 200, "/api/h2/z3solver/products-1", null); + + // TODO: This is currently not supported + // assertHasAtLeastOne(solution, HttpVerb.GET, 400, "/api/h2/z3solver/products-2/{id}", null); + // assertHasAtLeastOne(solution, HttpVerb.GET, 200, "/api/h2/z3solver/products-2/{id}", null); + + assertHasAtLeastOne(solution, HttpVerb.GET, 400, "/api/h2/z3solver/products-3", null); + assertHasAtLeastOne(solution, HttpVerb.GET, 200, "/api/h2/z3solver/products-3", null); + }); + } +} diff --git a/solver/src/main/java/org/evomaster/solver/Z3DockerExecutor.java b/solver/src/main/java/org/evomaster/solver/Z3DockerExecutor.java index 04904622a5..eeb196eb93 100644 --- a/solver/src/main/java/org/evomaster/solver/Z3DockerExecutor.java +++ b/solver/src/main/java/org/evomaster/solver/Z3DockerExecutor.java @@ -62,7 +62,7 @@ public Optional> solveFromFile(String fileName) { // 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"); + throw new RuntimeException("Error executing Z3 solver: \n" + result.getStdout() + "\n" + result.getStderr()); } String stdout = result.getStdout(); @@ -84,6 +84,8 @@ public Optional> solveFromFile(String fileName) { */ @Override public void close() { - z3Prover.stop(); + if (z3Prover != null) { + z3Prover.stop(); + } } }