PR feedback

Author: agusaldasoro

core/pom.xml

@@ -14,6 +14,15 @@
 
     <properties>
         <skipTests>${skipCore}</skipTests>
+        <!--
+            core has the heaviest gene test suite (GeneRandomizedTest: 1001 seeds × ~100 gene types).
+            On CI runners where algorithm tests complete faster than usual, less GC activity
+            accumulates before gene tests run, leaving the heap more fragmented and full.
+            5120m (vs the global 4096m) provides the headroom to survive runner variability.
+            GitHub Actions ubuntu-latest has 7 GB RAM: 5 GB heap + 1 GB Maven + 1 GB OS = 7 GB.
+            Overrides the root-pom testHeapXmx to avoid duplicating the surefire/failsafe argLine.
+        -->
+        <testHeapXmx>5120m</testHeapXmx>
     </properties>
 
     <dependencies>
@@ -33,10 +42,6 @@
             <groupId>org.evomaster</groupId>
             <artifactId>evomaster-client-java-controller-api</artifactId>
         </dependency>
-        <dependency>
-            <groupId>org.evomaster</groupId>
-            <artifactId>evomaster-client-java-sql</artifactId>
-        </dependency>
         <dependency>
             <groupId>org.evomaster</groupId>
             <artifactId>evomaster-client-java-instrumentation-shared</artifactId>
@@ -477,21 +482,6 @@
                 <groupId>org.antlr</groupId>
                 <artifactId>antlr4-maven-plugin</artifactId>
             </plugin>
-
-            <!--
-                core has the heaviest gene test suite (GeneRandomizedTest: 1001 seeds × ~100 gene types).
-                On CI runners where algorithm tests complete faster than usual, less GC activity
-                accumulates before gene tests run, leaving the heap more fragmented and full.
-                5120m (vs the global 4096m) provides the headroom to survive runner variability.
-                GitHub Actions ubuntu-latest has 7 GB RAM: 5 GB heap + 1 GB Maven + 1 GB OS = 7 GB.
-            -->
-            <plugin>
-                <groupId>org.apache.maven.plugins</groupId>
-                <artifactId>maven-surefire-plugin</artifactId>
-                <configuration>
-                    <argLine>@{argLine} -ea -Xms1024m -Xmx5120m -Xss4m -Dfile.encoding=UTF-8 -Djdk.attach.allowAttachSelf=true -Duser.language=en -Duser.country=GB ${addOpens}</argLine>
-                </configuration>
-            </plugin>
         </plugins>
     </build>
 

core/src/main/kotlin/org/evomaster/core/EMConfig.kt

@@ -1972,14 +1972,6 @@ class EMConfig {
     @DependsOnTrueFor("generateSqlDataWithZ3")
     var collectSqlZ3Stats = false
 
-    @Experimental
-    @Cfg("Measure the correctness of Z3-generated SQL inserts by computing the heuristic " +
-            "distance between the original failing WHERE query and the generated INSERT data. " +
-            "Distance=0 means the insert satisfies the WHERE; distance>0 means it does not. " +
-            "Only meaningful when generateSqlDataWithZ3=true.")
-    @DependsOnTrueFor("generateSqlDataWithZ3")
-    var measureSqlZ3Correctness = false
-
     @Experimental
     @Cfg("Soft timeout, in milliseconds, for each Z3 solver invocation when generating SQL data. " +
             "If a query exceeds it, Z3 returns 'unknown' for that query instead of running unbounded. " +

core/src/main/kotlin/org/evomaster/core/search/service/Statistics.kt

@@ -104,13 +104,6 @@ class Statistics : SearchListener {
     private val sqlZ3SeenQueryHashes = mutableSetOf<Int>()
     private var sqlZ3UniqueQueriesCount = 0
 
-    // Z3-based SQL data generation correctness distance statistics (only when measureSqlZ3Correctness=true)
-    private var sqlZ3CorrectnessCheckCount = 0
-    private var sqlZ3CorrectnessZeroDistanceCount = 0
-    private var sqlZ3CorrectnessNonZeroDistanceCount = 0
-    private val sqlZ3CorrectnessAvgDistance = IncrementalAverage()
-    private var sqlZ3CorrectnessEvalFailureCount = 0
-
     // mongo heuristic evaluation statistic
     private var mongoHeuristicEvaluationSuccessCount = 0
     private var mongoHeuristicEvaluationFailureCount = 0
@@ -308,22 +301,6 @@ class Statistics : SearchListener {
     internal fun getSqlZ3CacheHitCount() = sqlZ3CacheHitCount
     internal fun getSqlZ3CacheMissCount() = sqlZ3CacheMissCount
 
-    fun reportSqlZ3CorrectnessDistance(sqlDistance: Double, evaluationFailure: Boolean) {
-        sqlZ3CorrectnessCheckCount++
-        if (evaluationFailure) {
-            // sqlDistance is a sentinel value (e.g. Double.MAX_VALUE) in this case,
-            // and must not pollute the average of real distances
-            sqlZ3CorrectnessEvalFailureCount++
-            return
-        }
-        if (sqlDistance == 0.0) {
-            sqlZ3CorrectnessZeroDistanceCount++
-        } else {
-            sqlZ3CorrectnessNonZeroDistanceCount++
-        }
-        sqlZ3CorrectnessAvgDistance.addValue(sqlDistance)
-    }
-
     fun getMongoHeuristicsEvaluationCount(): Int = mongoHeuristicEvaluationSuccessCount + mongoHeuristicEvaluationFailureCount
 
     fun getSqlHeuristicsEvaluationCount(): Int = sqlHeuristicEvaluationSuccessCount + sqlHeuristicEvaluationFailureCount
@@ -500,15 +477,6 @@ class Statistics : SearchListener {
                 add(Pair("sqlZ3AvgSmtlibSizeBytes", "%.1f".format(sqlZ3SmtlibSizeBytes.mean)))
             }
 
-            // correctness distance stats (only emitted when measureSqlZ3Correctness=true)
-            if (config.measureSqlZ3Correctness) {
-                add(Pair("sqlZ3CorrectnessChecks",      "$sqlZ3CorrectnessCheckCount"))
-                add(Pair("sqlZ3CorrectnessZeroDistance", "$sqlZ3CorrectnessZeroDistanceCount"))
-                add(Pair("sqlZ3CorrectnessNonZero",      "$sqlZ3CorrectnessNonZeroDistanceCount"))
-                add(Pair("sqlZ3CorrectnessAvgDist",      "%.4f".format(sqlZ3CorrectnessAvgDistance.mean)))
-                add(Pair("sqlZ3CorrectnessEvalFailures", "$sqlZ3CorrectnessEvalFailureCount"))
-            }
-
             for(phase in ExecutionPhaseController.Phase.entries){
                 add(Pair("phase_${phase.name}", "${epc.getPhaseDurationInSeconds(phase)}"))
             }

core/src/main/kotlin/org/evomaster/core/solver/SMTConditionVisitor.kt

@@ -38,7 +38,8 @@ class SMTConditionVisitor(
      * @return The SMT-LIB column reference string.
      */
     private fun getColumnReference(tableName: String, columnName: String): String {
-        return "(${convertToAscii(columnName).uppercase()} ${convertToAscii(tableName).lowercase()}$rowIndex)"
+        val rowConstant = SmtLibGenerator.rowConstantName(convertToAscii(tableName).lowercase(), rowIndex)
+        return "(${convertToAscii(columnName).uppercase()} $rowConstant)"
     }
 
     /**

core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt

@@ -5,20 +5,13 @@ import com.google.inject.Inject
 import net.sf.jsqlparser.JSQLParserException
 import net.sf.jsqlparser.parser.CCJSqlParserUtil
 import net.sf.jsqlparser.statement.Statement
-import net.sf.jsqlparser.statement.insert.Insert
 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.logging.LoggingUtil
-import org.evomaster.client.java.sql.DataRow
-import org.evomaster.client.java.sql.QueryResult
-import org.evomaster.client.java.sql.QueryResultSet
-import org.evomaster.client.java.sql.heuristic.SqlHeuristicsCalculator
-import org.evomaster.client.java.sql.heuristic.TableColumnResolver
-import org.evomaster.client.java.sql.internal.SqlDistanceWithMetrics
 import org.evomaster.core.search.gene.BooleanGene
 import org.evomaster.core.search.gene.Gene
 import org.evomaster.core.search.gene.numeric.DoubleGene
@@ -71,11 +64,12 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver {
     // Schema is assumed stable within a single run, so only query + row count form the key.
     // Null until Z3 SQL generation is enabled in postConstruct — avoids allocating the map in runs where Z3 SQL generation is off.
     //
-    // THREAD-SAFETY: this is an access-ordered LinkedHashMap (LRU), whose get() mutates internal order,
-    // so it is NOT thread-safe. It relies on solve() being called from a single thread, which holds today
-    // because the MIO search loop (and thus fitness evaluation / structure mutation) is single-threaded.
-    // If fitness evaluation is ever parallelized, this cache must be synchronized or replaced with a
-    // concurrent LRU, otherwise concurrent access would corrupt it (lost entries / ConcurrentModificationException).
+    // THREAD-SAFETY: the backing map is an access-ordered LinkedHashMap (a bounded LRU, whose get() mutates
+    // internal order), wrapped in Collections.synchronizedMap so every operation is guarded by the map's
+    // intrinsic lock. This is the standard idiom for a thread-safe bounded LRU (a plain ConcurrentHashMap
+    // cannot do access-order eviction). Compound get-then-put in solve() is intentionally not atomic: at
+    // worst two threads recompute the same query concurrently, which is harmless (idempotent), and never
+    // corrupts the map. This makes the cache safe for the parallelized fitness evaluation that is planned.
     private var z3ResultCache: MutableMap<Pair<String, Int>, Z3Result>? = null
 
     companion object {
@@ -111,10 +105,11 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver {
     private fun postConstruct() {
         if (config.generateSqlDataWithZ3) {
             initializeExecutor()
-            z3ResultCache = object : LinkedHashMap<Pair<String, Int>, Z3Result>(16, 0.75f, true) {
+            val lru = object : LinkedHashMap<Pair<String, Int>, Z3Result>(16, 0.75f, true) {
                 override fun removeEldestEntry(eldest: MutableMap.MutableEntry<Pair<String, Int>, Z3Result>?) =
                     size > MAX_CACHE_SIZE
             }
+            z3ResultCache = Collections.synchronizedMap(lru)
         }
     }
 
@@ -210,33 +205,7 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver {
             Z3Result.Status.SAT -> {
                 stats?.reportSqlZ3Sat(z3TimeMs)
                 z3ResultCache?.set(cacheKey, z3Result)
-                val sqlActions = toSqlActionList(schemaDto, z3Result.solution)
-                if (::config.isInitialized && config.measureSqlZ3Correctness && queryStatement !is Insert) {
-                    /*
-                     * INSERT statements have no WHERE clause, so SqlHeuristicsCalculator has no
-                     * predicate to evaluate distance against and will always report a failure.
-                     * Correctness measurement only makes sense for queries that filter rows
-                     * (SELECT, DELETE, UPDATE). In the future this could be extended to verify
-                     * that the generated rows satisfy insertion preconditions such as FK constraints
-                     * or NOT NULL columns that Z3 SQL generation currently leaves unconstrained.
-                     *
-                     * Note: SqlHeuristicsCalculator is SELECT-oriented. For DELETE/UPDATE the distance
-                     * computation may fail and be reported as an evaluation failure (sqlDistanceEvaluationFailure)
-                     * rather than a real distance; such failures are counted separately and are excluded
-                     * from the average, so they do not distort the correctness metric.
-                     */
-                    val distResult = computeCorrectnessDistance(sqlQuery, schemaDto, sqlActions)
-                    if (distResult.sqlDistanceEvaluationFailure) {
-                        LoggingUtil.getInfoLogger().warn("SQL-Z3: correctness evaluation failure for query '$sqlQuery'")
-                    } else if (distResult.sqlDistance != 0.0) {
-                        LoggingUtil.getInfoLogger().warn("SQL-Z3: non-zero correctness distance (${distResult.sqlDistance}) for query '$sqlQuery'")
-                    }
-                    statisticsRef?.get()?.reportSqlZ3CorrectnessDistance(
-                        distResult.sqlDistance,
-                        distResult.sqlDistanceEvaluationFailure
-                    )
-                }
-                sqlActions
+                toSqlActionList(schemaDto, z3Result.solution)
             }
             Z3Result.Status.UNSAT -> {
                 stats?.reportSqlZ3Unsat(z3TimeMs)
@@ -387,15 +356,15 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver {
     /**
      * Extracts the table name from a row-constant key by removing the trailing row index.
      *
-     * Row constants are named "${smtName}${i}" (e.g. "users1", "users2"). The trailing digits are
-     * stripped so this works for any number of rows (e.g. "users10" -> "users"), not just single-digit
-     * indices. Note: this still assumes table names themselves do not end in a digit.
+     * Row constants are named "${smtName}${SEP}${i}" (e.g. "users__1", "users__2"; see
+     * [SmtLibGenerator.rowConstantName]). Splitting on the last separator recovers the table name
+     * unambiguously even when the table name itself ends in digits (e.g. "inventory2026__1" -> "inventory2026").
      *
      * @param key The key containing the table name and index.
      * @return The extracted table name.
      */
     private fun getTableName(key: String): String {
-        return key.replace(Regex("\\d+$"), "")
+        return key.substringBeforeLast(SmtLibGenerator.ROW_INDEX_SEPARATOR)
     }
 
     /**
@@ -488,7 +457,7 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver {
     /**
      * Maps column types to ColumnDataType.
      *
-     * FUTURE WORK: this recognizes only a small subset of SQL type spellings and falls back to
+     * TODO: this recognizes only a small subset of SQL type spellings and falls back to
      * CHARACTER_VARYING for everything else. It is one of three independent type vocabularies that
      * interpret [ColumnDto.type] — the others being [SmtLibGenerator.TYPE_MAP] (SQL type -> SMT sort)
      * and [hasColumnType] (BOOLEAN/TIMESTAMP special-casing). These can silently disagree when a
@@ -550,60 +519,4 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver {
     }
 
     private fun leadingBarResourcesFolder() = if (resourcesFolder.endsWith("/")) resourcesFolder else "$resourcesFolder/"
-
-    private fun computeCorrectnessDistance(
-        sqlQuery: String,
-        schemaDto: DbInfoDto,
-        sqlActions: List<SqlAction>
-    ): SqlDistanceWithMetrics {
-        val queryResultSet = toQueryResultSet(schemaDto, sqlActions)
-        val calculator = SqlHeuristicsCalculator.SqlHeuristicsCalculatorBuilder()
-            .withTableColumnResolver(TableColumnResolver(schemaDto))
-            .withSourceQueryResultSet(queryResultSet)
-            .build()
-        return calculator.computeDistance(sqlQuery)
-    }
-
-    private fun toQueryResultSet(schemaDto: DbInfoDto, sqlActions: List<SqlAction>): QueryResultSet {
-        val queryResultSet = QueryResultSet()
-        val byTable = sqlActions.groupBy { it.table.id.name }
-        for ((tableName, actions) in byTable) {
-            val columnNames = actions.first().seeTopGenes().map { it.name }
-            val queryResult = QueryResult(columnNames, tableName)
-            for (action in actions) {
-                val values: List<Any?> = action.seeTopGenes().map { gene -> extractGeneValue(gene) }
-                queryResult.addRow(DataRow(tableName, columnNames, values))
-            }
-            queryResultSet.addQueryResult(queryResult)
-        }
-        // Tables not present in Z3's SAT model (e.g. the optional side of a LEFT OUTER JOIN)
-        // still need an (empty) QueryResult, otherwise SqlHeuristicsCalculator NPEs when it
-        // looks them up unconditionally while walking the FROM/JOIN clause.
-        for (table in schemaDto.tables) {
-            if (table.id.name !in byTable.keys) {
-                val columnNames = table.columns.map { it.name }
-                queryResultSet.addQueryResult(QueryResult(columnNames, table.id.name))
-            }
-        }
-        return queryResultSet
-    }
-
-    private fun extractGeneValue(gene: Gene): Any? {
-        val inner = if (gene is SqlPrimaryKeyGene) gene.gene else gene
-        return when (inner) {
-            is IntegerGene             -> inner.value
-            is LongGene                -> inner.value
-            is StringGene              -> inner.value
-            is DoubleGene              -> inner.value
-            is BooleanGene             -> inner.value
-            is ImmutableDataHolderGene -> inner.value
-            else -> {
-                LoggingUtil.getInfoLogger().warn(
-                    "SQL-Z3: extractGeneValue() fallback to raw string for unhandled gene type " +
-                            "${inner.javaClass.name} (outer: ${gene.javaClass.name}, name: ${gene.name})"
-                )
-                inner.getValueAsRawString()
-            }
-        }
-    }
 }