Z3-based SQL data generation: memoization, explicit outcomes, statistics & fixes by agusaldasoro · Pull Request #1586 · WebFuzzing/EvoMaster

agusaldasoro · 2026-06-16T00:49:19Z

Summary

Adds memoization and explicit outcome handling to EvoMaster's Z3-based SQL data generation (generateSqlDataWithZ3), plus optional statistics/correctness instrumentation and several encoding fixes.

Memoization: caches solver results by (sqlQuery, numberOfRows) in a bounded LRU, skipping redundant Docker/Z3 executions for repeated queries. Only deterministic outcomes (SAT/UNSAT) are cached; UNKNOWN/ERROR are not (they may be transient). The cache stores the Z3Result (not the generated SqlActions), so each individual still gets fresh, independently-mutable genes.
Explicit solver outcomes: introduces Z3Result (SAT / UNSAT / UNKNOWN / ERROR) and Z3Solution, replacing Optional<Map<String, SMTLibValue>>. Z3DockerExecutor classifies Z3's stdout before parsing, so unknown/unsat are no longer misparsed as an empty SAT model.
Configurable Z3 timeout (sqlZ3TimeoutMs, default 5000ms): passes a soft -t: timeout to Z3; on expiry Z3 returns unknown (mapped to UNKNOWN) instead of running unbounded.
Configurable rows (sqlZ3NumberOfRows, default 1): number of rows generated per table.
Optional statistics (collectSqlZ3Stats): per-run counters written to statistics.csv only when enabled — query volume & cache reuse, solver outcomes, and cost (Z3 time, SMT-LIB gen time/size).
Optional correctness measurement (measureSqlZ3Correctness): after a SAT result, generated rows are re-evaluated with SqlHeuristicsCalculator to measure their distance to the original SQL predicate; mismatches are logged and recorded.
Encoding fixes:
- Composite primary keys now enforce tuple uniqueness (OR of per-column distinctness) instead of per-column distinctness, which over-constrained the encoding.
- SmtLibGenerator supports DELETE and UPDATE, not just SELECT.
- Integer columns map to LongGene instead of truncating via .toInt().
- Improved SQL parsing in JSqlVisitor (LOWER/UPPER, timestamp literals) and added SmtLibGeneratorTest coverage.
Memory fix: the solver holds Statistics via a WeakReference, so its @PreDestroy registration (a GC root through Governator's predestroy-monitor thread) no longer pins Statistics → Archive → individuals, which was OOMing test suites that build many injectors.

All new options are @Experimental and default-off (or default 1 / 5000), so default runs are unaffected.

Configuration

Flag	Default	Purpose
`generateSqlDataWithZ3`	false	Enable Z3-based SQL data generation
`sqlZ3NumberOfRows`	1	Rows generated per table
`sqlZ3TimeoutMs`	5000	Soft per-query Z3 timeout in ms (0 = off)
`collectSqlZ3Stats`	false	Emit solver statistics to CSV
`measureSqlZ3Correctness`	false	Post-verify generated rows against the SQL predicate

Statistics (`collectSqlZ3Stats`)

Query volume / cache: sqlZ3QueriesSeen, sqlZ3UniqueQueries, sqlZ3DuplicateQueries, sqlZ3CacheHits, sqlZ3CacheMisses — invariant: sqlZ3QueriesSeen = sqlZ3CacheHits + sqlZ3CacheMisses.
Outcomes: sqlZ3Sat, sqlZ3Unsat, sqlZ3Unknown, sqlZ3Errors, sqlZ3ParseFailures — sum equals sqlZ3CacheMisses.
Cost: sqlZ3TotalMs, sqlZ3SmtlibGenTotalMs, sqlZ3AvgSmtlibSizeBytes.

Correctness (`measureSqlZ3Correctness`)

sqlZ3CorrectnessChecks, sqlZ3CorrectnessZeroDistance, sqlZ3CorrectnessNonZero, sqlZ3CorrectnessAvgDist, sqlZ3CorrectnessEvalFailures.

Known limitations (documented in code as `KNOWN LIMITATION` / `FUTURE WORK`)

JOIN ON uses diagonal row pairing (row i ↔ row i) and only the first ON conjunct — sufficient at k=1, not full INNER JOIN semantics.
Composite foreign keys are matched per-column, not as a tuple.
NULL conditions (IS NULL / IS NOT NULL / = NULL) are dropped; all columns are treated as NOT NULL.
NUMERIC maps to Int (truncating decimals), inconsistent with DECIMAL → Real.
Three type-name vocabularies interpret ColumnDto.type independently and could drift on variant spellings.

jgaleotti · 2026-06-24T18:10:32Z

Is this ready for review? It seems to be failing...

agusaldasoro · 2026-06-24T18:32:27Z

Is this ready for review? It seems to be failing...

@jgaleotti The changes are ready and working, but there seems to be an out of memory issue that I can not solve in the Core and CoreIT tests

agusaldasoro · 2026-06-29T00:55:45Z

@jgaleotti Hey! It's ready for review now, thanks!

jgaleotti · 2026-07-08T16:22:20Z

    public void visit(Function function) {
-        // TODO This translation should be implemented
+        String name = function.getName().toUpperCase();
+        if ((name.equals("LOWER") || name.equals("UPPER"))


replace "LOWER" and "UPPER" with constants

jgaleotti · 2026-07-08T16:24:04Z

+/**
+ * Represents the outcome of a Z3 solver invocation.
+ * Distinguishes between three possible states: SAT (satisfiable with a model),
+ * UNSAT (unsatisfiable), and ERROR (solver or parsing failure).


what about timeout? is that an outcome?

also, can Z3 return UNKNOWN?

jgaleotti · 2026-07-08T16:26:37Z

+    /** Non-null only when status == ERROR. */
+    public final String errorMessage;
+
+    private Z3Result(Status status, Map<String, SMTLibValue> model, String errorMessage) {


create a abstract class Z3Solution and rename model to solution. (Using model can be a bit misleading nowadays due to LLMs...)

jgaleotti · 2026-07-08T16:27:13Z

+        ERROR
+    }
+
+    public final Status status;


why not getters and private fields?

jgaleotti · 2026-07-08T16:35:18Z

    private val sqlRowsAverageCalculator = IncrementalAverage()

+    // DSE (Dynamic Symbolic Execution) statistics
+    private var dseTotalQueriesProcessed = 0


To be honest, I need we need a more suitable term sonce there is no "dse/dynamic symbolic execution" involved in this work :)
What do you think of generateSqlDataWithDSE -> generateSqlDataWithZ3 ? Regarding the "dse..." it could be prefixed to "sqlZ3..." ?

jgaleotti · 2026-07-08T16:39:48Z

                }
                "NAME" -> {
                    assertTrue(gene is StringGene)
                    assertEquals("agus", (gene as StringGene).value)


"Alice" and "Bob" please :)

jgaleotti · 2026-07-08T21:08:34Z

-        if (config.generateSqlDataWithDSE) {
-            return handleDSE(ind, sampler, failedWhereQueries)
+        if (config.generateSqlDataWithZ3) {
+            return handleZ3(ind, sampler, failedWhereQueries)


generateSqlDataWithZ3(...)

jgaleotti · 2026-07-08T21:08:47Z

@@ -347,8 +347,8 @@ abstract class ApiWsStructureMutator : StructureMutator() {
            return handleSearch(ind, sampler, mutatedGenes, fw)


generateSqlDataWithSearch(...)

jgaleotti · 2026-07-08T21:15:24Z

@@ -31,7 +31,7 @@ public void testRunEM() throws Throwable {
                    args.add("true");


replace args.add with setOption(args,"generateSqlDataWithSearch","false")

jgaleotti · 2026-07-08T21:20:32Z

-        // TODO This translation should be implemented
+        if (dateTimeLiteralExpression.getType() == DateTimeLiteralExpression.DateTime.TIMESTAMP) {
+            String value = dateTimeLiteralExpression.getValue();
+            if (value.startsWith("'") && value.endsWith("'")) {


replace "'" with constant

jgaleotti · 2026-07-08T21:20:49Z

+            // Treat the timestamp string as UTC to match the UTC-based decoder in
+            // SMTLibZ3DbConstraintSolver (LocalDateTime.ofInstant(..., UTC)).
+            long epochSeconds = java.time.LocalDateTime.parse(value,
+                    DateTimeFormatter.ofPattern("yyyy-MM-dd HH:mm:ss"))


replace "yyyy-MM-dd HH:mm:ss" with constant

jgaleotti · 2026-07-08T21:21:43Z

-                String stderr = result.getStderr();
-                throw new RuntimeException("No result after solving file " + stderr);
+            String trimmed = stdout.trim();
+            if (trimmed.startsWith("unsat")) {


replace "unsat" with constant

jgaleotti · 2026-07-08T21:21:57Z

+            // "unknown" means Z3 could not decide (e.g. incomplete theory or timeout).
+            // It must be handled explicitly: otherwise it would fall through and be parsed
+            // as an empty model, silently masquerading as SAT.
+            if (trimmed.startsWith("unknown")) {


replace "unknown" with constant

jgaleotti · 2026-07-08T21:22:06Z

+            if (trimmed.startsWith("unknown")) {
+                return Z3Result.unknown();
+            }
+            if (!trimmed.startsWith("sat")) {


replace "sat" with constant

jgaleotti · 2026-07-08T21:22:55Z

+                return Z3Result.error("Unexpected Z3 output for file " + fileName + ": " + stdout);
+            }
+
+            Map<String, SMTLibValue> assignments = SMTResultParser.parseZ3Response(stdout);


The parser should create a solution instead of a assignment map

jgaleotti · 2026-07-08T21:24:07Z

+    /**
+     * @return the assignments of this solution, keyed by variable/constant name.
+     */
+    public abstract Map<String, SMTLibValue> getAssignments();


why is this abstract?

jgaleotti · 2026-07-09T20:45:53Z

+            // Defensive: Z3DockerExecutor already classifies 'unsat'/'unknown' before invoking this
+            // parser, so in practice only 'sat' models reach here. This guard is kept as a safety net
+            // in case the parser is ever called directly with an unsat response.
            if (line.startsWith("unsat")) {


replace "unsat" with constant value

jgaleotti · 2026-07-09T20:49:38Z

+                    smt.addNode(constraint)
                }
+            } catch (e: RuntimeException) {
+                LoggingUtil.getInfoLogger().warn("Could not translate WHERE clause to SMT-LIB, skipping: ${where}. Reason: ${e.message}")


is this failure considered in the sqlZ3 stats?

Good catch! It wasn't (the catch is inside generateSMT, so the predicate is silently dropped and Z3 still returns SAT).

Now fixed: it increments skippedQueryConstraints (here + the JOIN ON catch) and is reported as a new sqlZ3PartialTranslations stat column.

jgaleotti · 2026-07-09T20:51:04Z

+                     * from the average, so they do not distort the correctness metric.
+                     */
+                    val distResult = computeCorrectnessDistance(sqlQuery, schemaDto, sqlActions)
+                    if (distResult.sqlDistanceEvaluationFailure) {


is this considered in the stats?

jgaleotti · 2026-07-09T20:51:15Z

+                    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) {


is this case considered in the stats?

Yes. Both branches are recorded by the reportSqlZ3CorrectnessDistance(distResult.sqlDistance, distResult.sqlDistanceEvaluationFailure) call right below this block.

arcuri82

@agusaldasoro hi, this was a large PR, touching different aspects. please try to make smaller, more focused PRs in future :) eg, changing of surefire setting could had been done independently on a different PR

arcuri82 · 2026-07-10T09:33:46Z

+            }
+
+            // correctness distance stats (only emitted when measureSqlZ3Correctness=true)
+            if (config.measureSqlZ3Correctness) {


why 2 distinct configuration options? as we do this only for debugging, could just have 1

These correctness stats were something I added to debug the code for myself — the idea was to run them locally only (not on the cluster). They were genuinely useful: they helped me find a few bugs
by measuring how far the generated rows were from actually satisfying the predicate. But they're not needed for the time-measurement runs we do on the cluster, and they add overhead that could
interfere with the real objective there — which is exactly why they were a separate flag from collectSqlZ3Stats.

That said, to keep this PR focused I've moved the whole correctness feature to a separate branch (dse/sql-z3-correctness) so we can discuss it later. It's not needed for now, so this PR no longer
has that second option.

arcuri82 · 2026-07-10T09:35:25Z

                for (join in joins) {
                    val onExpressions = join.onExpressions
                    if (onExpressions.isNotEmpty()) {
+                        // KNOWN LIMITATION: only the first ON expression is used; a composite ON


should add a TODO in the comments here

arcuri82 · 2026-07-10T09:35:31Z

                        try {
                            val condition = parser.parse(onExpression.toString(), toDBType(schema.databaseType))
                            val tableFromQuery = TablesNamesFinder().getTables(sqlQuery as Statement).first()
+                            // KNOWN LIMITATION: the ON condition is translated with the SAME row index on


should add a TODO in the comments here

arcuri82 · 2026-07-10T09:36:12Z

@@ -539,37 +608,62 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I

    companion object {


companion objects should be top of file, and not after line 600

arcuri82 · 2026-07-10T09:36:40Z

    companion object {

-        // Maps database column types to SMT-LIB types
+        // Bounds for TIMESTAMP columns, encoded as epoch seconds (SMT Int).


use JavaDoc /** */ for fields and functions

arcuri82 · 2026-07-10T10:33:26Z

-     * Extracts the table name from the key by removing the last character (index).
+     * 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


did you choose this? if so, wouldn't better to have a separator? eg, ${smtName}__${i}

arcuri82 · 2026-07-10T10:34:38Z

    /**
     * Maps column types to ColumnDataType.
     *
+     * FUTURE WORK: this recognizes only a small subset of SQL type spellings and falls back to


put TODO. note that TODO and FIXME comments are handled specially in IDEs

arcuri82 · 2026-07-10T10:35:51Z

+            "Distance=0 means the insert satisfies the WHERE; distance>0 means it does not. " +
+            "Only meaningful when generateSqlDataWithZ3=true.")
+    @DependsOnTrueFor("generateSqlDataWithZ3")
+    var measureSqlZ3Correctness = false


no need of 2 separated options to collect statistics

arcuri82 · 2026-07-10T10:41:27Z

        </dependency>
+        <dependency>
+            <groupId>org.evomaster</groupId>
+            <artifactId>evomaster-client-java-sql</artifactId>


you should not add this kind of dependency between modules before discussing it, as it has several architectural consequences. remove it. different though if it is imported as test

arcuri82 · 2026-07-10T10:45:29Z

+                <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>


you shouldn't copy&paste configurations like this, as it ends up with code duplication, which must be avoided, as the 2 will inevitably diverge throught time. why not increasing -Xms directly on the root pom avoiding duplication? otherwise, that value itself should be in a param, which is the overriden in properties declaration in this pom file

agusaldasoro changed the title ~~Dse/memoization~~ Add DSE Metrics + Memoization Jun 16, 2026

agusaldasoro requested a review from jgaleotti June 16, 2026 01:45

agusaldasoro changed the title ~~Add DSE Metrics + Memoization~~ DSE Memoization + Statistics Jun 18, 2026

agusaldasoro marked this pull request as ready for review June 18, 2026 11:52

agusaldasoro force-pushed the dse/memoization branch from 9817750 to 55cf2de Compare June 24, 2026 19:33

agusaldasoro marked this pull request as draft June 25, 2026 00:37

agusaldasoro removed the request for review from jgaleotti June 25, 2026 00:37

Add DSE Memoization and time statistics

d03d8ec

agusaldasoro force-pushed the dse/memoization branch from 6aced03 to d03d8ec Compare June 27, 2026 14:06

Correctness statistics for DSE (#1587)

406c401

agusaldasoro changed the title ~~DSE Memoization + Statistics~~ DSE Statistics & Fixes Jun 27, 2026

agusaldasoro marked this pull request as ready for review June 27, 2026 14:18

agusaldasoro and others added 2 commits June 28, 2026 18:55

Fix merge conflict

859a1fd

Merge branch 'master' into dse/memoization

83fcdcf

agusaldasoro requested a review from jgaleotti June 29, 2026 00:55

agusaldasoro added 6 commits June 30, 2026 14:11

Merge branch 'master' into dse/memoization

a5ff0a4

Merge branch 'master' into dse/memoization

5baadf4

Merge branch 'master' into dse/memoization

180b716

Merge branch 'master' into dse/memoization

5adb691

Merge branch 'master' into dse/memoization

4b33bb6

Merge branch 'master' into dse/memoization

745d470

jgaleotti requested changes Jul 8, 2026

View reviewed changes

agusaldasoro added 2 commits July 8, 2026 16:09

PR Feedback

6994520

Use default timpeout

4df0a88

agusaldasoro requested a review from jgaleotti July 8, 2026 19:17

jgaleotti requested changes Jul 8, 2026

View reviewed changes

Fix stats

fb0a308

agusaldasoro and others added 3 commits July 9, 2026 13:12

PR Feedback

6162a09

Merge branch 'master' into dse/memoization

3d8b0ea

Add comments

27d4730

agusaldasoro changed the title ~~DSE Statistics & Fixes~~ Z3-based SQL data generation: memoization, explicit outcomes, statistics & fixes Jul 9, 2026

Add comments

c36024f

agusaldasoro requested a review from jgaleotti July 9, 2026 17:53

jgaleotti requested changes Jul 9, 2026

View reviewed changes

agusaldasoro and others added 3 commits July 9, 2026 19:32

Merge branch 'master' into dse/memoization

127bf4c

Add constants

9bee480

Add stats

3ddb68c

agusaldasoro requested a review from jgaleotti July 9, 2026 22:56

jgaleotti approved these changes Jul 9, 2026

View reviewed changes

jgaleotti requested a review from arcuri82 July 9, 2026 23:09

arcuri82 requested changes Jul 10, 2026

View reviewed changes

agusaldasoro and others added 2 commits July 11, 2026 13:50

PR feedback

c943596

Merge branch 'master' into dse/memoization

2fee4ad

agusaldasoro requested a review from arcuri82 July 11, 2026 16:53

Fix build

455d28a

		@@ -347,8 +347,8 @@ abstract class ApiWsStructureMutator : StructureMutator() {
		return handleSearch(ind, sampler, mutatedGenes, fw)

		@@ -31,7 +31,7 @@ public void testRunEM() throws Throwable {
		args.add("true");

		@@ -539,37 +608,62 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I

		companion object {

Uh oh!

Conversation

agusaldasoro commented Jun 16, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Configuration

Statistics (collectSqlZ3Stats)

Correctness (measureSqlZ3Correctness)

Known limitations (documented in code as KNOWN LIMITATION / FUTURE WORK)

Uh oh!

jgaleotti commented Jun 24, 2026

Uh oh!

agusaldasoro commented Jun 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

agusaldasoro commented Jun 29, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

arcuri82 left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

agusaldasoro Jul 11, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

agusaldasoro commented Jun 16, 2026 •

edited

Loading

Statistics (`collectSqlZ3Stats`)

Correctness (`measureSqlZ3Correctness`)

Known limitations (documented in code as `KNOWN LIMITATION` / `FUTURE WORK`)

agusaldasoro commented Jun 24, 2026 •

edited

Loading

agusaldasoro Jul 11, 2026 •

edited

Loading