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.

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

		@@ -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");

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!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

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