Merge pull request #1479 from WebFuzzing/fix/more-types

Add support for special characters

Author: arcuri82

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
@@ -26,12 +27,18 @@ class SMTConditionVisitor(
     /**
      * Constructs a column reference string for SMT-LIB from a table name and column name.
      *
+     * Both names are converted to ASCII because SMT-LIB unquoted symbols only allow ASCII characters.
+     * Table and column names may come directly from SQL query text (e.g., a WHERE clause), which can
+     * contain non-ASCII characters if the schema uses them. The conversion must happen here because,
+     * unlike schema-derived names that are pre-converted via [SmtTable], query-derived names are
+     * parsed at runtime from raw SQL strings.
+     *
      * @param tableName The name of the table.
      * @param columnName The name of the column.
      * @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)"
     }
 
     /**

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,37 +153,42 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver {
 
             // Create the list of genes with the values
             val genes = mutableListOf<Gene>()
-            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
                             )
                             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)