Generate valid UUID, JSON and JSONB values

[agusaldasoro]

Problem

UUID and JSONB columns are encoded as SMT Strings, with nothing constraining their form. Unless the query pins the value, Z3 assigns something like "" or "!0!", and the INSERT of the whole row is rejected (H2: Data conversion error converting "''" (EV: "U" UUID)).

• A table with a UUID column therefore got its rows inserted only for queries that compare that column with a literal.
• A foreign key between UUID columns failed on both rows.

The failure is silent, because SqlScriptRunner.execInsert logs a failed insertion and carries on.

JSON, the type of MySQL, H2 2.x and PostgreSQL's non-binary variant, was not in TYPE_MAP at all. Every table of the schema is declared for every query, so a single JSON column made generation fail for all queries of the schema.

Fix

SMTLibZ3DbConstraintSolver.validTextValue turns the value Z3 assigned into one the database accepts, when building the StringGene:

• UUID: a value that is not a UUID becomes UUID.nameUUIDFromBytes(value).
• JSON and JSONB: a value that is not a JSON document becomes that value as a JSON string ("" → "\"\""). Validity is checked with Jackson, rejecting trailing tokens and blank input.
• Valid values are kept, e.g. a UUID copied from the query.

The mapping is deterministic: equal strings give equal values and different strings give different ones. The equalities and distinctions the formula imposes (foreign keys, unique and primary keys) therefore still hold after the mapping.

Constraining the form inside the formula, with str.in_re and a UUID pattern, would also work. It brings in Z3's regular-expression theory, though, which makes solving noticeably more expensive, so post-processing was preferred. UUID_TYPE, JSON_TYPE and JSONB_TYPE are now constants in SmtLibGenerator, used by TYPE_MAP, which now maps JSON like JSONB.

Tests

New UuidJsonColumnSolvingTest, end to end against Z3 and H2:

• a query that leaves the UUID free: the row is inserted and returned;
• a query that pins the UUID to a literal: the literal is kept;
• a query on a table with a UUID foreign key: both rows are inserted, and the reference holds;
• a JSON column: the row is inserted and returned;
• a JSONB column (an H2 varchar reported as jsonb): the generated value is a JSON document.

On master every case fails, because the JSON column breaks generation for the whole schema. Without that column, all but the pinned-literal case fail, e.g. expected: <[true, true]> but was: <[false, false]> for the foreign key.

All tests under org.evomaster.core.database.sql.solver pass.