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 eb12789a79..b92704e159 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,7 @@ package org.evomaster.core.solver import org.evomaster.client.java.controller.api.dto.database.schema.TableDto +import org.evomaster.core.utils.StringUtils.convertToAscii import org.evomaster.dbconstraint.ast.* import org.evomaster.solver.smtlib.AssertSMTNode import org.evomaster.solver.smtlib.EmptySMTNode @@ -31,7 +32,7 @@ class SMTConditionVisitor( * @return The SMT-LIB column reference string. */ private fun getColumnReference(tableName: String, columnName: String): String { - return "(${columnName.uppercase()} ${tableName.lowercase()}$rowIndex)" + return "(${convertToAscii(columnName).uppercase()} ${convertToAscii(tableName).lowercase()}$rowIndex)" } /** 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 f2cbbc287e..13fdb06665 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt @@ -20,6 +20,7 @@ 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.* +import org.evomaster.core.utils.StringUtils.convertToAscii import org.evomaster.solver.Z3DockerExecutor import org.evomaster.solver.smtlib.SMTLib import org.evomaster.solver.smtlib.value.* @@ -152,18 +153,24 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { // 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)) { + // 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) + } + val dbColumnName = dbColumn?.name ?: smtColumn + + var gene: Gene = IntegerGene(dbColumnName, 0) + when (val columnValue = columns.getField(smtColumn)) { is StringValue -> { - gene = if (hasColumnType(schemaDto, table, columnName, "BOOLEAN")) { - BooleanGene(columnName, toBoolean(columnValue.value)) + gene = if (hasColumnType(schemaDto, table, dbColumnName, "BOOLEAN")) { + BooleanGene(dbColumnName, toBoolean(columnValue.value)) } else { - StringGene(columnName, columnValue.value) + StringGene(dbColumnName, columnValue.value) } } is LongValue -> { - gene = if (hasColumnType(schemaDto, table, columnName, "TIMESTAMP")) { + gene = if (hasColumnType(schemaDto, table, dbColumnName, "TIMESTAMP")) { val epochSeconds = columnValue.value.toLong() val localDateTime = LocalDateTime.ofInstant( Instant.ofEpochSecond(epochSeconds), ZoneOffset.UTC @@ -171,18 +178,17 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { val formatted = localDateTime.format( DateTimeFormatter.ofPattern("yyyy-MM-dd HH:mm:ss") ) - ImmutableDataHolderGene(columnName, formatted, inQuotes = true) + ImmutableDataHolderGene(dbColumnName, formatted, inQuotes = true) } else { - IntegerGene(columnName, columnValue.value.toInt()) + IntegerGene(dbColumnName, columnValue.value.toInt()) } } is RealValue -> { - gene = DoubleGene(columnName, columnValue.value) + gene = DoubleGene(dbColumnName, columnValue.value) } } - val currentColumn = table.columns.firstOrNull(){ it.name.equals(columnName, ignoreCase = true) } - if (currentColumn != null && currentColumn.primaryKey) { - gene = SqlPrimaryKeyGene(columnName, table.id, gene, actionId) + if (dbColumn != null && dbColumn.primaryKey) { + gene = SqlPrimaryKeyGene(dbColumnName, table.id, gene, actionId) } gene.markAllAsInitialized() genes.add(gene) 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 a963e53dec..7795220e0b 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt @@ -15,11 +15,11 @@ import org.evomaster.core.utils.StringUtils import org.evomaster.dbconstraint.ConstraintDatabaseType import org.evomaster.dbconstraint.ast.SqlCondition import net.sf.jsqlparser.JSQLParserException +import org.evomaster.core.utils.StringUtils.convertToAscii import org.evomaster.dbconstraint.parser.SqlConditionParserException import org.evomaster.dbconstraint.parser.jsql.JSqlConditionParser import org.evomaster.solver.smtlib.* import org.evomaster.solver.smtlib.assertion.* -import java.util.* /** * Generates SMT-LIB constraints from SQL queries and schema definitions. @@ -58,7 +58,8 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I */ private fun appendTableDefinitions(smt: SMTLib) { for (table in schema.tables) { - val dataTypeName = "${StringUtils.capitalization(table.id.name)}Row" + val smtTableName = convertToAscii(table.id.name) + val dataTypeName = "${StringUtils.capitalization(smtTableName)}Row" // Declare datatype for the table smt.addNode( @@ -67,7 +68,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I // Declare constants for each row for (i in 1..numberOfRows) { - smt.addNode(DeclareConstSMTNode("${table.id.name.lowercase()}$i", dataTypeName)) + smt.addNode(DeclareConstSMTNode("${smtTableName.lowercase()}$i", dataTypeName)) } } } @@ -91,10 +92,10 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I * @param table The table for which unique constraints are added. */ private fun appendUniqueConstraints(smt: SMTLib, table: TableDto) { - val tableName = table.id.name.lowercase() + val smtTableName = convertToAscii(table.id.name).lowercase() for (column in table.columns) { if (column.unique) { - val nodes = assertForDistinctField(column.name, tableName) + val nodes = assertForDistinctField(convertToAscii(column.name), smtTableName) smt.addNodes(nodes) } } @@ -131,7 +132,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I * @return The corresponding SMT node. */ private fun parseCheckExpression(table: TableDto, condition: SqlCondition, index: Int): SMTNode { - val visitor = SMTConditionVisitor(table.id.name.lowercase(), emptyMap(), schema.tables, index) + val visitor = SMTConditionVisitor(convertToAscii(table.id.name).lowercase(), emptyMap(), schema.tables, index) return condition.accept(visitor, null) as SMTNode } @@ -167,21 +168,21 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I private fun appendBooleanConstraints(smt: SMTLib) { for (table in schema.tables) { - val tableName = table.id.name.lowercase() + val smtTableName = convertToAscii(table.id.name).lowercase() for (column in table.columns) { if (column.type.equals("BOOLEAN", ignoreCase = true)) { - val columnName = column.name.uppercase() + val columnName = convertToAscii(column.name).uppercase() for (i in 1..numberOfRows) { smt.addNode( AssertSMTNode( OrAssertion( listOf( - EqualsAssertion(listOf("($columnName $tableName$i)", "\"true\"")), - EqualsAssertion(listOf("($columnName $tableName$i)", "\"True\"")), - EqualsAssertion(listOf("($columnName $tableName$i)", "\"TRUE\"")), - EqualsAssertion(listOf("($columnName $tableName$i)", "\"false\"")), - EqualsAssertion(listOf("($columnName $tableName$i)", "\"False\"")), - EqualsAssertion(listOf("($columnName $tableName$i)", "\"FALSE\"")) + EqualsAssertion(listOf("($columnName $smtTableName$i)", "\"true\"")), + EqualsAssertion(listOf("($columnName $smtTableName$i)", "\"True\"")), + EqualsAssertion(listOf("($columnName $smtTableName$i)", "\"TRUE\"")), + EqualsAssertion(listOf("($columnName $smtTableName$i)", "\"false\"")), + EqualsAssertion(listOf("($columnName $smtTableName$i)", "\"False\"")), + EqualsAssertion(listOf("($columnName $smtTableName$i)", "\"FALSE\"")) ) ) ) @@ -194,10 +195,10 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I private fun appendTimestampConstraints(smt: SMTLib) { for (table in schema.tables) { - val tableName = table.id.name.lowercase() + val smtTableName = convertToAscii(table.id.name).lowercase() for (column in table.columns) { if (column.type.equals("TIMESTAMP", ignoreCase = true)) { - val columnName = column.name.uppercase() + val columnName = convertToAscii(column.name).uppercase() val lowerBound = 0 // Example for Unix epoch start val upperBound = 32503680000 // Example for year 3000 in seconds @@ -205,7 +206,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I smt.addNode( AssertSMTNode( GreaterThanOrEqualsAssertion( - "($columnName $tableName$i)", + "($columnName $smtTableName$i)", lowerBound.toString() ) ) @@ -213,7 +214,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I smt.addNode( AssertSMTNode( LessThanOrEqualsAssertion( - "($columnName $tableName$i)", + "($columnName $smtTableName$i)", upperBound.toString() ) ) @@ -232,11 +233,11 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I * @param table The table for which primary key constraints are added. */ private fun appendPrimaryKeyConstraints(smt: SMTLib, table: TableDto) { - val tableName = table.id.name.lowercase() + val smtTableName = convertToAscii(table.id.name).lowercase() val primaryKeys = table.columns.filter { it.primaryKey } for (primaryKey in primaryKeys) { - val nodes = assertForDistinctField(primaryKey.name, tableName) + val nodes = assertForDistinctField(convertToAscii(primaryKey.name), smtTableName) smt.addNodes(nodes) } } @@ -274,16 +275,16 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I * @param table The table for which foreign key constraints are added. */ private fun appendForeignKeyConstraints(smt: SMTLib, table: TableDto) { - val sourceTableName = table.id.name.lowercase() + val sourceTableName = convertToAscii(table.id.name).lowercase() for (foreignKey in table.foreignKeys) { val referencedTable = findReferencedTable(foreignKey) - val referencedTableName = referencedTable.id.name.lowercase() - val referencedColumnSelector = findReferencedPKSelector(table, referencedTable, foreignKey) + val referencedTableName = convertToAscii(referencedTable.id.name).lowercase() + val referencedColumnSelector = convertToAscii(findReferencedPKSelector(table, referencedTable, foreignKey)) for (sourceColumn in foreignKey.sourceColumns) { val nodes = assertForEqualsAny( - sourceColumn, sourceTableName, + convertToAscii(sourceColumn), sourceTableName, referencedColumnSelector, referencedTableName ) smt.addNodes(nodes) @@ -434,7 +435,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I * @return The corresponding SMT node. */ private fun parseQueryCondition(tableAliases: Map, defaultTableName: String, condition: SqlCondition, index: Int): SMTNode { - val visitor = SMTConditionVisitor(defaultTableName, tableAliases, schema.tables, index) + val visitor = SMTConditionVisitor(convertToAscii(defaultTableName), tableAliases, schema.tables, index) return condition.accept(visitor, null) as SMTNode } @@ -519,9 +520,10 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I // Only add GetValueSMTNode for the mentioned tables for (table in schema.tables) { val tableNameLower = table.id.name.lowercase() + val smtColumnName = convertToAscii(tableNameLower) if (tablesMentioned.contains(tableNameLower)) { for (i in 1..numberOfRows) { - smt.addNode(GetValueSMTNode("$tableNameLower$i")) + smt.addNode(GetValueSMTNode("$smtColumnName$i")) } } } @@ -537,22 +539,27 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I return table.columns.map { c -> val smtType = TYPE_MAP[c.type.uppercase()] ?: throw RuntimeException("Unsupported column type: ${c.type}") - DeclareConstSMTNode(c.name, smtType) + DeclareConstSMTNode(convertToAscii(c.name), smtType) } } companion object { + // Maps database 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", diff --git a/core/src/main/kotlin/org/evomaster/core/utils/StringUtils.kt b/core/src/main/kotlin/org/evomaster/core/utils/StringUtils.kt index 426d1a8737..7cccbac206 100644 --- a/core/src/main/kotlin/org/evomaster/core/utils/StringUtils.kt +++ b/core/src/main/kotlin/org/evomaster/core/utils/StringUtils.kt @@ -1,7 +1,5 @@ package org.evomaster.core.utils -import java.util.* - object StringUtils { /** @@ -82,4 +80,23 @@ object StringUtils { } return lines } + + /** + * Replaces non-ASCII characters in a name to make it a valid SMT-LIB identifier. + * SMT-LIB unquoted symbols are restricted to ASCII, so characters like Æ, Ø, Å must be transliterated. + * + * This is needed because our test suite includes Norwegian APIs whose database schemas + * contain column and table names with Norwegian characters (Æ, Ø, Å). + * + * Characters that do not decompose under NFD (Ø, Æ) are replaced explicitly. + * Characters that decompose under NFD (Å→A, and other accented letters like é, ü, ñ) + * are handled by normalizing to NFD form and stripping the remaining non-ASCII combining marks. + */ + fun convertToAscii(name: String): String { + val replaced = name + .replace('Ø', 'O').replace('ø', 'o') + .replace("Æ", "AE").replace("æ", "ae") + return java.text.Normalizer.normalize(replaced, java.text.Normalizer.Form.NFD) + .replace(Regex("[^\\x00-\\x7F]"), "") + } }