From 9fee0ee8531eb5a5e036eede4186c81cf97e3e30 Mon Sep 17 00:00:00 2001 From: Agustina Aldasoro Date: Mon, 6 Apr 2026 19:42:09 -0300 Subject: [PATCH] Remove dependency to DTO --- .../core/solver/SMTConditionVisitor.kt | 5 +- .../core/solver/SMTLibZ3DbConstraintSolver.kt | 235 +++++++----------- .../evomaster/core/solver/SmtLibGenerator.kt | 151 +++++------ .../org/evomaster/core/solver/SmtTable.kt | 19 +- .../core/solver/SmtLibGeneratorTest.kt | 6 +- 5 files changed, 192 insertions(+), 224 deletions(-) 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..28427919ff 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SMTConditionVisitor.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SMTConditionVisitor.kt @@ -1,6 +1,6 @@ package org.evomaster.core.solver -import org.evomaster.client.java.controller.api.dto.database.schema.TableDto +import org.evomaster.core.sql.schema.Table import org.evomaster.core.utils.StringUtils.convertToAscii import org.evomaster.dbconstraint.ast.* import org.evomaster.solver.smtlib.AssertSMTNode @@ -20,7 +20,7 @@ import java.util.* class SMTConditionVisitor( private val defaultTableName: String, private val tableAliases: Map, - private val tables: List, + private val tables: List, private val rowIndex: Int ) : SqlConditionVisitor { @@ -157,6 +157,7 @@ class SMTConditionVisitor( } } + /** * Maps SQL comparison operators to SMT-LIB comparators. * 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 13fdb06665..f3723af9f5 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt @@ -16,8 +16,8 @@ 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.placeholder.ImmutableDataHolderGene -import org.evomaster.core.search.gene.sql.SqlPrimaryKeyGene import org.evomaster.core.search.gene.string.StringGene +import org.evomaster.core.search.gene.sql.SqlPrimaryKeyGene import org.evomaster.core.sql.SqlAction import org.evomaster.core.sql.schema.* import org.evomaster.core.utils.StringUtils.convertToAscii @@ -38,7 +38,6 @@ import javax.annotation.PostConstruct import javax.annotation.PreDestroy import kotlin.io.path.createDirectories import kotlin.io.path.exists -import kotlin.text.equals /** * An SMT solver implementation using Z3 in a Docker container. @@ -91,13 +90,93 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { 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) + // Convert DTOs to domain objects at the boundary, before any business logic + val smtTables = Companion.buildSmtTables(schemaDto) + + val generator = SmtLibGenerator(smtTables, schemaDto.databaseType, numberOfRows) val queryStatement = parseStatement(sqlQuery) val smtLib = generator.generateSMT(queryStatement) val fileName = storeToTmpFile(smtLib) val z3Response = executor.solveFromFile(fileName) - return toSqlActionList(schemaDto, z3Response) + return toSqlActionList(smtTables, z3Response) + } + + companion object { + + /** + * Converts a [DbInfoDto] schema to a list of [SmtTable] domain objects. + * + * This is the boundary where DTOs are translated into domain objects. + * Exposed as a companion method so tests can build a [SmtLibGenerator] directly + * without going through the full solver pipeline. + */ + fun buildSmtTables(schemaDto: DbInfoDto): List { + return schemaDto.tables.map { tableDto -> + val columns = buildColumns(schemaDto.databaseType, tableDto) + val foreignKeys = buildForeignKeys(tableDto, columns) + val table = Table(TableId(tableDto.id.name), columns, foreignKeys) + val checkExpressions = tableDto.tableCheckExpressions.map { it.sqlCheckExpression } + SmtTable(table, checkExpressions) + } + } + + private fun buildColumns(databaseType: DatabaseType, tableDto: TableDto): Set { + return tableDto.columns.map { columnDto -> + toColumn(columnDto, databaseType) + }.toSet() + } + + private fun buildForeignKeys(tableDto: TableDto, columns: Set): Set { + return tableDto.foreignKeys.map { fkDto -> + val sourceColumns = fkDto.sourceColumns.mapNotNull { colName -> + columns.firstOrNull { it.name.equals(colName, ignoreCase = true) } + }.toSet() + ForeignKey(sourceColumns, TableId(fkDto.targetTable)) + }.toSet() + } + + private fun toColumn(columnDto: ColumnDto, databaseType: DatabaseType): Column { + return Column( + name = columnDto.name, + type = getColumnDataType(columnDto.type), + size = columnDto.size, + primaryKey = columnDto.primaryKey, + nullable = columnDto.nullable, + unique = columnDto.unique, + autoIncrement = columnDto.autoIncrement, + foreignKeyToAutoIncrement = columnDto.foreignKeyToAutoIncrement, + lowerBound = null, + upperBound = null, + enumValuesAsStrings = null, + similarToPatterns = null, + likePatterns = null, + databaseType = databaseType, + isUnsigned = false, + compositeType = null, + compositeTypeName = null, + isNotBlank = null, + minSize = null, + maxSize = null, + javaRegExPattern = null + ) + } + + /** + * Maps column type strings (from SQL schema) to [ColumnDataType] enum values. + */ + private fun getColumnDataType(type: String): ColumnDataType { + return when (type.uppercase()) { + "BIGINT" -> ColumnDataType.BIGINT + "INTEGER", "INT" -> ColumnDataType.INTEGER + "FLOAT" -> ColumnDataType.FLOAT + "DOUBLE" -> ColumnDataType.DOUBLE + "TIMESTAMP" -> ColumnDataType.TIMESTAMP + "CHARACTER VARYING" -> ColumnDataType.CHARACTER_VARYING + "CHAR" -> ColumnDataType.CHAR + else -> ColumnDataType.CHARACTER_VARYING // Default type + } + } } /** @@ -127,10 +206,11 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { /** * Converts Z3's response to a list of SqlActions. * + * @param smtTables The pre-built domain tables, used to look up schema metadata. * @param z3Response The response from Z3. * @return A list of SQL actions. */ - private fun toSqlActionList(schemaDto: DbInfoDto, z3Response: Optional>): List { + private fun toSqlActionList(smtTables: List, z3Response: Optional>): List { if (!z3Response.isPresent) { return emptyList() } @@ -138,11 +218,13 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { val actions = mutableListOf() for (row in z3Response.get()) { - val tableName = getTableName(row.key) + val smtTableName = getTableName(row.key) val columns = row.value as StructValue - // Find table from schema and create SQL actions - val table = findTableByName(schemaDto, tableName) + // Find the SmtTable by its SMT-safe name (which is what Z3 returns) + val smtTable = smtTables.firstOrNull { it.smtName == smtTableName } + ?: throw RuntimeException("Table not found for SMT name: $smtTableName") + val table = smtTable.table /* * The invariant requires that action.insertionId == primaryKey.uniqueId (and same for FK). @@ -153,7 +235,7 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { // 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 + // 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) @@ -163,14 +245,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 (dbColumn?.type == ColumnDataType.BOOLEAN || dbColumn?.type == ColumnDataType.BOOL) { BooleanGene(dbColumnName, toBoolean(columnValue.value)) } else { StringGene(dbColumnName, columnValue.value) } } is LongValue -> { - gene = if (hasColumnType(schemaDto, table, dbColumnName, "TIMESTAMP")) { + gene = if (dbColumn?.type == ColumnDataType.TIMESTAMP) { val epochSeconds = columnValue.value.toLong() val localDateTime = LocalDateTime.ofInstant( Instant.ofEpochSecond(epochSeconds), ZoneOffset.UTC @@ -205,26 +287,6 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { return value.equals("True", ignoreCase = true) } - private fun hasColumnType( - schemaDto: DbInfoDto, - table: Table, - columnName: String?, - expectedType: String - ): Boolean { - - if (columnName == null) return false - - val tableDto = schemaDto.tables.firstOrNull { - it.id.name.equals(table.id.name, ignoreCase = true) - } ?: return false - - val col = tableDto.columns.firstOrNull { - it.name.equals(columnName, ignoreCase = true) - } ?: return false - - return col.type.equals(expectedType, ignoreCase = true) - } - /** * Extracts the table name from the key by removing the last character (index). * @@ -235,117 +297,6 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { return key.substring(0, key.length - 1) // Remove last character } - /** - * Finds a table by its name from the schema and constructs a Table object. - * - * @param schema The database schema. - * @param tableName The name of the table to find. - * @return The Table object. - */ - private fun findTableByName(schema: DbInfoDto, tableName: String): Table { - val tableDto = schema.tables.find { it.id.name.equals(tableName, ignoreCase = true) } - ?: throw RuntimeException("Table not found: $tableName") - return Table( - TableId(tableDto.id.name) , //TODO other info, eg schema - findColumns(schema,tableDto), // Convert columns from DTO - findForeignKeys(tableDto) // TODO: Implement this method - ) - } - - /** - * Converts a list of ColumnDto to a set of Column objects. - * - * @param tableDto The table DTO containing column definitions. - * @return A set of Column objects. - */ - private fun findColumns(schemaDto: DbInfoDto, tableDto: TableDto): Set { - return tableDto.columns.map { columnDto -> - toColumnFromDto(columnDto, schemaDto.databaseType) - }.toSet() - } - - /** - * Converts ColumnDto to a Column object. - * - * @param columnDto The column DTO. - * @param databaseType The type of the database. - * @return The Column object. - */ - private fun toColumnFromDto( - columnDto: ColumnDto, - databaseType: DatabaseType - ): Column { - val name = columnDto.name - val type = getColumnDataType(columnDto.type) - val nullable: Boolean = columnDto.nullable - val primaryKey = columnDto.primaryKey - val unique = columnDto.unique - val autoIncrement = columnDto.autoIncrement - val foreignKeyToAutoIncrement = columnDto.foreignKeyToAutoIncrement - val size = columnDto.size - val lowerBound = null - val upperBound = null - val enumValuesAsStrings = null - val similarToPatterns = null - val likePatterns = null - val isUnsigned = false - val compositeType = null - val compositeTypeName = 0 - val isNotBlank = null - val minSize = null - val maxSize = null - val javaRegExPattern = null - - val column = Column( - name, - type, - size, - primaryKey, - nullable, - unique, - autoIncrement, - foreignKeyToAutoIncrement, - lowerBound, - upperBound, - enumValuesAsStrings, - similarToPatterns, - likePatterns, - databaseType, - isUnsigned, - compositeType, - compositeTypeName, - isNotBlank, - minSize, - maxSize, - javaRegExPattern - ) - return column - } - - /** - * Maps column types to ColumnDataType. - * - * @param type The column type as a string. - * @return The corresponding ColumnDataType. - */ - private fun getColumnDataType(type: String): ColumnDataType { - return when (type) { - "BIGINT" -> ColumnDataType.BIGINT - "INTEGER" -> ColumnDataType.INTEGER - "FLOAT" -> ColumnDataType.FLOAT - "DOUBLE" -> ColumnDataType.DOUBLE - "TIMESTAMP" -> ColumnDataType.TIMESTAMP - "CHARACTER VARYING" -> ColumnDataType.CHARACTER_VARYING - "CHAR" -> ColumnDataType.CHAR - else -> ColumnDataType.CHARACTER_VARYING // Default type - } - } - - // TODO: Implement this method - private fun findForeignKeys(tableDto: TableDto): Set { - return emptySet() // Placeholder - } - /** * Stores the SMTLib problem to a file in the resources' folder. * 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..cb74242f59 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt @@ -7,10 +7,9 @@ import net.sf.jsqlparser.statement.select.PlainSelect import net.sf.jsqlparser.statement.select.Select 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 -import org.evomaster.client.java.controller.api.dto.database.schema.ForeignKeyDto -import org.evomaster.client.java.controller.api.dto.database.schema.TableDto import org.evomaster.core.logging.LoggingUtil +import org.evomaster.core.sql.schema.ColumnDataType +import org.evomaster.core.sql.schema.ForeignKey import org.evomaster.dbconstraint.ConstraintDatabaseType import org.evomaster.dbconstraint.ast.SqlCondition import net.sf.jsqlparser.JSQLParserException @@ -23,16 +22,23 @@ import org.evomaster.solver.smtlib.assertion.* /** * Generates SMT-LIB constraints from SQL queries and schema definitions. * - * @param schema The database schema containing tables and constraints. + * @param smtTables The tables in the schema, pre-wrapped with SMT-safe identifiers. + * @param databaseType The database type, used to select the correct SQL dialect when parsing constraints. * @param numberOfRows The number of rows to be considered in constraints. */ -class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: Int) { +class SmtLibGenerator( + private val smtTables: List, + private val databaseType: DatabaseType, + private val numberOfRows: Int +) { - private var parser = JSqlConditionParser() + private val parser = JSqlConditionParser() - private val smtTables: List = schema.tables.map { SmtTable(it) } private val smtTableByOriginalName: Map = smtTables.associateBy { it.originalName } + /** Flat list of domain [org.evomaster.core.sql.schema.Table] objects, passed to [SMTConditionVisitor]. */ + private val tables: List = smtTables.map { it.table } + /** * Main method to generate SMT-LIB representation from SQL query. * @@ -91,7 +97,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I * @param smtTable The table for which unique constraints are added. */ private fun appendUniqueConstraints(smt: SMTLib, smtTable: SmtTable) { - for (column in smtTable.dto.columns) { + for (column in smtTable.table.columns) { if (column.unique) { val nodes = assertForDistinctField(smtTable.smtColumnName(column.name), smtTable.smtName) smt.addNodes(nodes) @@ -106,17 +112,17 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I * @param smtTable The table for which check constraints are added. */ private fun appendCheckConstraints(smt: SMTLib, smtTable: SmtTable) { - for (check in smtTable.dto.tableCheckExpressions) { + for (sqlExpression in smtTable.checkExpressions) { try { - val condition: SqlCondition = parser.parse(check.sqlCheckExpression, toDBType(schema.databaseType)) + val condition: SqlCondition = parser.parse(sqlExpression, toDBType(databaseType)) for (i in 1..numberOfRows) { val constraint: SMTNode = parseCheckExpression(smtTable, condition, i) smt.addNode(constraint) } } catch (e: SqlConditionParserException) { - LoggingUtil.getInfoLogger().warn("Could not translate CHECK constraint to SMT-LIB, skipping: ${check.sqlCheckExpression}. Reason: ${e.message}") + LoggingUtil.getInfoLogger().warn("Could not translate CHECK constraint to SMT-LIB, skipping: $sqlExpression. Reason: ${e.message}") } catch (e: JSQLParserException) { - LoggingUtil.getInfoLogger().warn("Could not translate CHECK constraint to SMT-LIB, skipping: ${check.sqlCheckExpression}. Reason: ${e.message}") + LoggingUtil.getInfoLogger().warn("Could not translate CHECK constraint to SMT-LIB, skipping: $sqlExpression. Reason: ${e.message}") } } } @@ -130,7 +136,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I * @return The corresponding SMT node. */ private fun parseCheckExpression(smtTable: SmtTable, condition: SqlCondition, index: Int): SMTNode { - val visitor = SMTConditionVisitor(smtTable.smtName, emptyMap(), schema.tables, index) + val visitor = SMTConditionVisitor(smtTable.smtName, emptyMap(), tables, index) return condition.accept(visitor, null) as SMTNode } @@ -166,8 +172,8 @@ 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)) { + for (column in smtTable.table.columns) { + if (column.type == ColumnDataType.BOOLEAN || column.type == ColumnDataType.BOOL) { val columnName = smtTable.smtColumnName(column.name).uppercase() for (i in 1..numberOfRows) { smt.addNode( @@ -192,8 +198,8 @@ 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)) { + for (column in smtTable.table.columns) { + if (column.type == ColumnDataType.TIMESTAMP) { val columnName = smtTable.smtColumnName(column.name).uppercase() val lowerBound = 0 // Example for Unix epoch start val upperBound = 32503680000 // Example for year 3000 in seconds @@ -229,9 +235,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I * @param smtTable The table for which primary key constraints are added. */ private fun appendPrimaryKeyConstraints(smt: SMTLib, smtTable: SmtTable) { - val primaryKeys = smtTable.dto.columns.filter { it.primaryKey } - - for (primaryKey in primaryKeys) { + for (primaryKey in smtTable.table.primaryKeys()) { val nodes = assertForDistinctField(smtTable.smtColumnName(primaryKey.name), smtTable.smtName) smt.addNodes(nodes) } @@ -270,15 +274,15 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I * @param smtTable The table for which foreign key constraints are added. */ private fun appendForeignKeyConstraints(smt: SMTLib, smtTable: SmtTable) { - for (foreignKey in smtTable.dto.foreignKeys) { + for (foreignKey in smtTable.table.foreignKeys) { val referencedSmtTable = findReferencedSmtTable(foreignKey) val referencedColumnSelector = referencedSmtTable.smtColumnName( - findReferencedPKSelector(smtTable.dto, referencedSmtTable.dto, foreignKey) + findReferencedPKSelector(smtTable.table, referencedSmtTable.table, foreignKey) ) for (sourceColumn in foreignKey.sourceColumns) { val nodes = assertForEqualsAny( - smtTable.smtColumnName(sourceColumn), smtTable.smtName, + smtTable.smtColumnName(sourceColumn.name), smtTable.smtName, referencedColumnSelector, referencedSmtTable.smtName ) smt.addNodes(nodes) @@ -320,30 +324,35 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I } /** - * Finds the primary key column name in the referenced table. + * Finds the primary key column name in the referenced table that is type-compatible with the source FK column. * + * @param sourceTable The source table containing the foreign key. * @param referencedTable The referenced table. * @param foreignKey The foreign key constraint. * @return The primary key column name in the referenced table. */ - private fun findReferencedPKSelector(sourceTable: TableDto, referencedTable: TableDto, foreignKey: ForeignKeyDto): String { - val referencedPrimaryKeys = referencedTable.columns.filter { it.primaryKey } - val sourceColumnName = foreignKey.sourceColumns.firstOrNull() + private fun findReferencedPKSelector( + sourceTable: org.evomaster.core.sql.schema.Table, + referencedTable: org.evomaster.core.sql.schema.Table, + foreignKey: ForeignKey + ): String { + val referencedPrimaryKeys = referencedTable.primaryKeys() + val sourceColumnName = foreignKey.sourceColumns.firstOrNull()?.name val sourceSmtType = sourceColumnName?.let { scn -> sourceTable.columns.firstOrNull { it.name.equals(scn, ignoreCase = true) } - ?.let { TYPE_MAP[it.type.uppercase()] } + ?.let { TYPE_MAP[it.type] } } if (referencedPrimaryKeys.isNotEmpty() && - (sourceSmtType == null || TYPE_MAP[referencedPrimaryKeys[0].type.uppercase()] == sourceSmtType)) { + (sourceSmtType == null || TYPE_MAP[referencedPrimaryKeys[0].type] == sourceSmtType)) { return referencedPrimaryKeys[0].name } // No PK or type mismatch: find a type-compatible column if (sourceSmtType != null) { - referencedTable.columns.firstOrNull { TYPE_MAP[it.type.uppercase()] == sourceSmtType } + referencedTable.columns.firstOrNull { TYPE_MAP[it.type] == sourceSmtType } ?.let { return it.name } } return referencedTable.columns.firstOrNull()?.name - ?: throw RuntimeException("Referenced table has no columns: ${foreignKey.targetTable}") + ?: throw RuntimeException("Referenced table has no columns: ${foreignKey.targetTableId.name}") } /** @@ -352,9 +361,9 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I * @param foreignKey The foreign key constraint. * @return The referenced [SmtTable]. */ - private fun findReferencedSmtTable(foreignKey: ForeignKeyDto): SmtTable { - return smtTableByOriginalName[foreignKey.targetTable.lowercase()] - ?: throw RuntimeException("Referenced table not found: ${foreignKey.targetTable}") + private fun findReferencedSmtTable(foreignKey: ForeignKey): SmtTable { + return smtTableByOriginalName[foreignKey.targetTableId.name.lowercase()] + ?: throw RuntimeException("Referenced table not found: ${foreignKey.targetTableId.name}") } /** @@ -374,7 +383,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I if (where != null) { try { - val condition = parser.parse(where.toString(), toDBType(schema.databaseType)) + val condition = parser.parse(where.toString(), toDBType(databaseType)) val tableFromQuery = TablesNamesFinder().getTables(sqlQuery as Statement).first() for (i in 1..numberOfRows) { val constraint = parseQueryCondition(tableAliases, tableFromQuery, condition, i) @@ -404,7 +413,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I if (onExpressions.isNotEmpty()) { val onExpression = onExpressions.elementAt(0) try { - val condition = parser.parse(onExpression.toString(), toDBType(schema.databaseType)) + val condition = parser.parse(onExpression.toString(), toDBType(databaseType)) val tableFromQuery = TablesNamesFinder().getTables(sqlQuery as Statement).first() for (i in 1..numberOfRows) { val constraint = parseQueryCondition(tableAliases, tableFromQuery, condition, i) @@ -431,7 +440,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I private fun parseQueryCondition(tableAliases: Map, defaultTableName: String, condition: SqlCondition, index: Int): SMTNode { val smtDefaultTableName = smtTableByOriginalName[defaultTableName.lowercase()]?.smtName ?: convertToAscii(defaultTableName) - val visitor = SMTConditionVisitor(smtDefaultTableName, tableAliases, schema.tables, index) + val visitor = SMTConditionVisitor(smtDefaultTableName, tableAliases, tables, index) return condition.accept(visitor, null) as SMTNode } @@ -480,7 +489,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I val tablesFinder = TablesNamesFinder() // Add tables from the FROM clause - val tables = try { + val queryTables = try { tablesFinder.getTables(sqlQuery) } catch (e: Exception) { // This is because the jsqlParser does not support visit(Execute execute) { @@ -490,7 +499,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I emptySet() } - for (tableName in tables){ + for (tableName in queryTables){ tablesMentioned.add(tableName.lowercase()) } @@ -530,8 +539,8 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I * @return A list of SMT nodes for column constructors. */ private fun getConstructors(smtTable: SmtTable): List { - return smtTable.dto.columns.map { c -> - val smtType = TYPE_MAP[c.type.uppercase()] + return smtTable.table.columns.map { c -> + val smtType = TYPE_MAP[c.type] ?: throw RuntimeException("Unsupported column type: ${c.type}") DeclareConstSMTNode(smtTable.smtColumnName(c.name), smtType) } @@ -539,37 +548,37 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I companion object { - // Maps database column types to SMT-LIB types + // Maps domain column types to SMT-LIB types 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", - "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", + ColumnDataType.BIGINT to "Int", + ColumnDataType.BIT to "Int", + ColumnDataType.INTEGER to "Int", + ColumnDataType.INT to "Int", + ColumnDataType.INT2 to "Int", + ColumnDataType.INT4 to "Int", + ColumnDataType.INT8 to "Int", + ColumnDataType.TINYINT to "Int", + ColumnDataType.SMALLINT to "Int", + ColumnDataType.NUMERIC to "Int", + ColumnDataType.SERIAL to "Int", + ColumnDataType.SMALLSERIAL to "Int", + ColumnDataType.BIGSERIAL to "Int", + ColumnDataType.TIMESTAMP to "Int", + ColumnDataType.DATE to "Int", + ColumnDataType.FLOAT to "Real", + ColumnDataType.DOUBLE to "Real", + ColumnDataType.DECIMAL to "Real", + ColumnDataType.REAL to "Real", + ColumnDataType.CHARACTER_VARYING to "String", + ColumnDataType.CHAR to "String", + ColumnDataType.VARCHAR to "String", + ColumnDataType.TEXT to "String", + ColumnDataType.CHARACTER_LARGE_OBJECT to "String", + ColumnDataType.BOOLEAN to "String", + ColumnDataType.BOOL to "String", + ColumnDataType.UUID to "String", + ColumnDataType.JSONB to "String", + ColumnDataType.BYTEA to "String", ) } } diff --git a/core/src/main/kotlin/org/evomaster/core/solver/SmtTable.kt b/core/src/main/kotlin/org/evomaster/core/solver/SmtTable.kt index 06b5e5bdc8..b5495e1efa 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SmtTable.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SmtTable.kt @@ -1,28 +1,35 @@ package org.evomaster.core.solver -import org.evomaster.client.java.controller.api.dto.database.schema.TableDto +import org.evomaster.core.sql.schema.Table import org.evomaster.core.utils.StringUtils import org.evomaster.core.utils.StringUtils.convertToAscii /** - * A view of a [TableDto] with pre-computed SMT-safe identifiers. + * A view of a [Table] with pre-computed SMT-safe identifiers. * * All table and column names are converted to ASCII once at construction time, * avoiding repeated [convertToAscii] calls throughout [SmtLibGenerator]. + * + * @param table The domain-level table object used for schema metadata. + * @param checkExpressions Raw SQL strings for CHECK constraints, preserved separately + * because [Table.tableConstraints] uses the [org.evomaster.dbconstraint.TableConstraintVisitor] + * hierarchy, while [SmtLibGenerator] parses constraints via + * [org.evomaster.dbconstraint.parser.jsql.JSqlConditionParser] into + * [org.evomaster.dbconstraint.ast.SqlCondition] objects for [SMTConditionVisitor]. */ -class SmtTable(val dto: TableDto) { +class SmtTable(val table: Table, val checkExpressions: List) { /** Original lowercase table name, used to match against SQL query table references. */ - val originalName: String = dto.id.name.lowercase() + val originalName: String = table.id.name.lowercase() /** SMT-safe lowercase identifier used in row constant declarations (e.g., "person1", "person2"). */ - val smtName: String = convertToAscii(dto.id.name).lowercase() + val smtName: String = convertToAscii(table.id.name).lowercase() /** SMT-LIB datatype name for this table's rows (e.g., "PersonRow"). */ val dataTypeName: String = "${StringUtils.capitalization(smtName)}Row" private val columnSmtNames: Map = - dto.columns.associate { col -> col.name to convertToAscii(col.name) } + table.columns.associate { col -> col.name to convertToAscii(col.name) } /** Returns the SMT-safe identifier for the given column name. */ fun smtColumnName(columnName: String): 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 742d4dd012..3e3ddeab2b 100644 --- a/core/src/test/kotlin/org/evomaster/core/solver/SmtLibGeneratorTest.kt +++ b/core/src/test/kotlin/org/evomaster/core/solver/SmtLibGeneratorTest.kt @@ -198,7 +198,7 @@ class SmtLibGeneratorTest { "ALTER TABLE products add constraint userIdKey foreign key (user_id) REFERENCES users;\n") val schemaDto = DbInfoExtractor.extract(connection) - generator = SmtLibGenerator(schemaDto, 2) + generator = SmtLibGenerator(SMTLibZ3DbConstraintSolver.buildSmtTables(schemaDto), schemaDto.databaseType, 2) } @JvmStatic @@ -445,7 +445,7 @@ class SmtLibGeneratorTest { "CREATE TABLE flags(id bigint generated by default as identity primary key, flag bit);" ) val schemaDto = DbInfoExtractor.extract(conn) - val bitGenerator = SmtLibGenerator(schemaDto, 2) + val bitGenerator = SmtLibGenerator(SMTLibZ3DbConstraintSolver.buildSmtTables(schemaDto), schemaDto.databaseType, 2) val selectStatement: Statement = CCJSqlParserUtil.parse("SELECT * FROM flags WHERE id > 0") val response: SMTLib = bitGenerator.generateSMT(selectStatement) @@ -520,7 +520,7 @@ class SmtLibGeneratorTest { "CREATE TABLE events(id bigint generated by default as identity primary key, created_at timestamp not null);" ) val schemaDto = DbInfoExtractor.extract(conn) - val timestampGenerator = SmtLibGenerator(schemaDto, 2) + val timestampGenerator = SmtLibGenerator(SMTLibZ3DbConstraintSolver.buildSmtTables(schemaDto), schemaDto.databaseType, 2) val selectStatement: Statement = CCJSqlParserUtil.parse("SELECT * FROM events WHERE id > 0") val response: SMTLib = timestampGenerator.generateSMT(selectStatement)