Skip to content

Commit 6162a09

Browse files
agusaldasoroagusaldasoro
committed
PR Feedback
1 parent fb0a308 commit 6162a09

9 files changed

Lines changed: 64 additions & 67 deletions

File tree

‎core-extra/dbconstraint/src/main/java/org/evomaster/dbconstraint/parser/jsql/JSqlVisitor.java‎

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,10 @@ public class JSqlVisitor implements ExpressionVisitor {
3131
private static final String LOWER = "LOWER";
3232
private static final String UPPER = "UPPER";
3333

34+
private static final String SINGLE_QUOTE_CHAR = "'";
35+
36+
private static final String TIMESTAMP_FORMAT = "yyyy-MM-dd HH:mm:ss";
37+
3438
private final Deque<SqlCondition> stack = new ArrayDeque<>();
3539

3640
@Override
@@ -143,7 +147,7 @@ public void visit(StringValue stringValue) {
143147
String notEscapedValue = stringValue.getNotExcapedValue();
144148

145149
String notEscapedValueNoQuotes;
146-
if (notEscapedValue.startsWith("'") && notEscapedValue.endsWith("'")) {
150+
if (notEscapedValue.startsWith(SINGLE_QUOTE_CHAR) && notEscapedValue.endsWith(SINGLE_QUOTE_CHAR)) {
147151
notEscapedValueNoQuotes = notEscapedValue.substring(1, notEscapedValue.length() - 1);
148152
} else {
149153
notEscapedValueNoQuotes = notEscapedValue;
@@ -617,13 +621,13 @@ public void visit(TimeKeyExpression timeKeyExpression) {
617621
public void visit(DateTimeLiteralExpression dateTimeLiteralExpression) {
618622
if (dateTimeLiteralExpression.getType() == DateTimeLiteralExpression.DateTime.TIMESTAMP) {
619623
String value = dateTimeLiteralExpression.getValue();
620-
if (value.startsWith("'") && value.endsWith("'")) {
624+
if (value.startsWith(SINGLE_QUOTE_CHAR) && value.endsWith(SINGLE_QUOTE_CHAR)) {
621625
value = value.substring(1, value.length() - 1);
622626
}
623627
// Treat the timestamp string as UTC to match the UTC-based decoder in
624628
// SMTLibZ3DbConstraintSolver (LocalDateTime.ofInstant(..., UTC)).
625629
long epochSeconds = java.time.LocalDateTime.parse(value,
626-
DateTimeFormatter.ofPattern("yyyy-MM-dd HH:mm:ss"))
630+
DateTimeFormatter.ofPattern(TIMESTAMP_FORMAT))
627631
.toEpochSecond(ZoneOffset.UTC);
628632
stack.push(new SqlBigIntegerLiteralValue(BigInteger.valueOf(epochSeconds)));
629633
return;

‎core-extra/solver/src/main/java/org/evomaster/solver/MapBasedZ3Solution.java‎

Lines changed: 0 additions & 23 deletions
This file was deleted.

‎core-extra/solver/src/main/java/org/evomaster/solver/Z3DockerExecutor.java‎

Lines changed: 9 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,12 @@
11
package org.evomaster.solver;
22

33
import org.evomaster.solver.smtlib.SMTResultParser;
4-
import org.evomaster.solver.smtlib.value.SMTLibValue;
54
import org.testcontainers.containers.BindMode;
65
import org.testcontainers.containers.Container;
76
import org.testcontainers.containers.GenericContainer;
87
import org.testcontainers.images.builder.ImageFromDockerfile;
98

109
import java.io.IOException;
11-
import java.util.Map;
1210
import java.util.Optional;
1311

1412
/**
@@ -21,6 +19,11 @@ public class Z3DockerExecutor implements AutoCloseable {
2119
public static final String Z3_DOCKER_IMAGE = "ghcr.io/z3prover/z3:ubuntu-20.04-bare-z3-sha-ba8d8f0";
2220
// The Docker entrypoint that keeps it running indefinitely
2321
public static final String ENTRYPOINT = "while :; do sleep 1000 ; done";
22+
23+
// SMT-LIB (check-sat) response tokens returned by Z3
24+
private static final String SAT = "sat";
25+
private static final String UNSAT = "unsat";
26+
private static final String UNKNOWN = "unknown";
2427
private final String containerPath = "/smt2-resources/";
2528
private final GenericContainer<?> z3Prover;
2629

@@ -89,21 +92,20 @@ public Z3Result solveFromFile(String fileName, long timeoutMs) {
8992
}
9093

9194
String trimmed = stdout.trim();
92-
if (trimmed.startsWith("unsat")) {
95+
if (trimmed.startsWith(UNSAT)) {
9396
return Z3Result.unsat();
9497
}
9598
// "unknown" means Z3 could not decide (e.g. incomplete theory or timeout).
9699
// It must be handled explicitly: otherwise it would fall through and be parsed
97100
// as an empty model, silently masquerading as SAT.
98-
if (trimmed.startsWith("unknown")) {
101+
if (trimmed.startsWith(UNKNOWN)) {
99102
return Z3Result.unknown();
100103
}
101-
if (!trimmed.startsWith("sat")) {
104+
if (!trimmed.startsWith(SAT)) {
102105
return Z3Result.error("Unexpected Z3 output for file " + fileName + ": " + stdout);
103106
}
104107

105-
Map<String, SMTLibValue> assignments = SMTResultParser.parseZ3Response(stdout);
106-
return Z3Result.sat(new MapBasedZ3Solution(assignments));
108+
return Z3Result.sat(SMTResultParser.parseZ3Response(stdout));
107109

108110
} catch (IOException | InterruptedException e) {
109111
return Z3Result.error("I/O or interruption error running Z3 on " + fileName + ": " + e.getMessage());

‎core-extra/solver/src/main/java/org/evomaster/solver/Z3Solution.java‎

Lines changed: 20 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -7,37 +7,49 @@
77
/**
88
* Represents a satisfying solution produced by the Z3 solver: a mapping from
99
* SMT-LIB variable/constant names to the values Z3 assigned to them.
10-
*
11-
* This is intentionally an abstract type (rather than a raw {@link Map}) so that
12-
* alternative solution representations can be introduced without changing callers.
1310
*/
14-
public abstract class Z3Solution {
11+
public class Z3Solution {
12+
13+
private final Map<String, SMTLibValue> assignments;
14+
15+
public Z3Solution(Map<String, SMTLibValue> assignments) {
16+
this.assignments = assignments;
17+
}
1518

1619
/**
1720
* @return the assignments of this solution, keyed by variable/constant name.
1821
*/
19-
public abstract Map<String, SMTLibValue> getAssignments();
22+
public Map<String, SMTLibValue> getAssignments() {
23+
return assignments;
24+
}
2025

2126
/**
2227
* @param name the variable/constant name
2328
* @return the value assigned to the given name, or {@code null} if absent.
2429
*/
2530
public SMTLibValue get(String name) {
26-
return getAssignments().get(name);
31+
return assignments.get(name);
2732
}
2833

2934
/**
3035
* @param name the variable/constant name
3136
* @return whether the given name has an assigned value in this solution.
3237
*/
3338
public boolean containsKey(String name) {
34-
return getAssignments().containsKey(name);
39+
return assignments.containsKey(name);
3540
}
3641

3742
/**
3843
* @return the number of assignments in this solution.
3944
*/
4045
public int size() {
41-
return getAssignments().size();
46+
return assignments.size();
47+
}
48+
49+
/**
50+
* @return whether this solution has no assignments.
51+
*/
52+
public boolean isEmpty() {
53+
return assignments.isEmpty();
4254
}
4355
}

‎core-extra/solver/src/main/java/org/evomaster/solver/smtlib/SMTResultParser.java‎

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
package org.evomaster.solver.smtlib;
22

3+
import org.evomaster.solver.Z3Solution;
34
import org.evomaster.solver.smtlib.value.*;
45

56
import java.util.HashMap;
@@ -9,17 +10,18 @@
910

1011
/**
1112
* The SMTResultParser class is responsible for parsing responses from the Z3 solver.
12-
* It converts the raw SMT-LIB response into a map of variable names and their corresponding values.
13+
* It converts the raw SMT-LIB response into a {@link Z3Solution} of variable names and
14+
* their corresponding values.
1315
*/
1416
public class SMTResultParser {
1517

1618
/**
1719
* Parses the Z3 solver response and extracts variable values.
1820
*
1921
* @param z3Response the raw response from Z3 solver
20-
* @return a map where keys are variable names and values are SMTLibValue objects representing the parsed values
22+
* @return a {@link Z3Solution} mapping variable names to the {@link SMTLibValue} objects Z3 assigned to them
2123
*/
22-
public static Map<String, SMTLibValue> parseZ3Response(String z3Response) {
24+
public static Z3Solution parseZ3Response(String z3Response) {
2325
Map<String, SMTLibValue> results = new HashMap<>();
2426

2527
// Regular expression for matching simple value assignments, including negative numbers
@@ -91,7 +93,7 @@ else if (valueMatcher.find()) {
9193
buffer.setLength(0); // Clear the buffer after processing
9294
}
9395
}
94-
return results; // Return the map of parsed results
96+
return new Z3Solution(results); // Return the parsed assignments as a solution
9597
}
9698

9799
/**

‎core-extra/solver/src/test/java/org/evomaster/solver/smtlib/SMTResultParserTest.java‎

Lines changed: 10 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,32 +1,31 @@
11
package org.evomaster.solver.smtlib;
22

3+
import org.evomaster.solver.Z3Solution;
34
import org.evomaster.solver.smtlib.value.*;
45
import org.junit.jupiter.api.Test;
56

6-
import java.util.Map;
7-
87
import static org.junit.jupiter.api.Assertions.assertEquals;
98
import static org.junit.jupiter.api.Assertions.assertTrue;
109

1110
public class SMTResultParserTest {
1211
@Test
1312
public void testParseEmptyResponse() {
1413
String response = "";
15-
Map<String, SMTLibValue> result = SMTResultParser.parseZ3Response(response);
14+
Z3Solution result = SMTResultParser.parseZ3Response(response);
1615
assertTrue(result.isEmpty());
1716
}
1817

1918
@Test
2019
public void testParseMalformedResponse() {
2120
String response = "sat\n(id_1 2)";
22-
Map<String, SMTLibValue> result = SMTResultParser.parseZ3Response(response);
21+
Z3Solution result = SMTResultParser.parseZ3Response(response);
2322
assertTrue(result.isEmpty());
2423
}
2524

2625
@Test
2726
public void testParseSimpleIntValue() {
2827
String response = "sat\n((id_1 2))";
29-
Map<String, SMTLibValue> result = SMTResultParser.parseZ3Response(response);
28+
Z3Solution result = SMTResultParser.parseZ3Response(response);
3029
assertEquals(1, result.size());
3130
assertTrue(result.get("id_1") instanceof LongValue);
3231
assertEquals(2, ((LongValue) result.get("id_1")).getValue());
@@ -35,7 +34,7 @@ public void testParseSimpleIntValue() {
3534
@Test
3635
public void testParseSimpleStringValue() {
3736
String response = "sat\n((name_1 \"example\"))";
38-
Map<String, SMTLibValue> result = SMTResultParser.parseZ3Response(response);
37+
Z3Solution result = SMTResultParser.parseZ3Response(response);
3938
assertEquals(1, result.size());
4039
assertTrue(result.get("name_1") instanceof StringValue);
4140
assertEquals("example", ((StringValue) result.get("name_1")).getValue());
@@ -44,7 +43,7 @@ public void testParseSimpleStringValue() {
4443
@Test
4544
public void testParseSimpleRealValue() {
4645
String response = "sat\n((pi_1 3.14))";
47-
Map<String, SMTLibValue> result = SMTResultParser.parseZ3Response(response);
46+
Z3Solution result = SMTResultParser.parseZ3Response(response);
4847
assertEquals(1, result.size());
4948
assertTrue(result.get("pi_1") instanceof RealValue);
5049
assertEquals(3.14, ((RealValue) result.get("pi_1")).getValue());
@@ -55,7 +54,7 @@ public void testParseNegativeValue() {
5554
String response = "sat\n" +
5655
"((y 0))\n" +
5756
"((x (- 4)))";
58-
Map<String, SMTLibValue> result = SMTResultParser.parseZ3Response(response);
57+
Z3Solution result = SMTResultParser.parseZ3Response(response);
5958
assertEquals(2, result.size());
6059
assertTrue(result.get("y") instanceof LongValue);
6160
assertEquals(0, ((LongValue) result.get("y")).getValue());
@@ -67,7 +66,7 @@ public void testParseNegativeValue() {
6766
public void testParseComposedType() {
6867
String response = "sat\n((users1 (id-document-name-age-points 4 2 \"Alice\" 31 7)))";
6968

70-
Map<String, SMTLibValue> result = SMTResultParser.parseZ3Response(response);
69+
Z3Solution result = SMTResultParser.parseZ3Response(response);
7170

7271
assertEquals(1, result.size());
7372
assertTrue(result.get("users1") instanceof StructValue);
@@ -93,7 +92,7 @@ public void testParseMultipleEntries() {
9392
"((users1 (id-document-name-age-points 4 2 \"Alice\" 31 7)))\n" +
9493
"((users2 (id-document-name-age-points 6 3 \"Bob\" 91 7)))\n";
9594

96-
Map<String, SMTLibValue> result = SMTResultParser.parseZ3Response(response);
95+
Z3Solution result = SMTResultParser.parseZ3Response(response);
9796
assertEquals(4, result.size());
9897

9998
assertTrue(result.get("products1") instanceof StructValue);
@@ -163,7 +162,7 @@ public void testNegativeLong() {
163162
" \"true\"\n" +
164163
" 2)))\n";
165164

166-
Map<String, SMTLibValue> result = SMTResultParser.parseZ3Response(response);
165+
Z3Solution result = SMTResultParser.parseZ3Response(response);
167166
assertEquals(2, result.size());
168167

169168
assertTrue(result.get("documents_specs1") instanceof StructValue);

‎core-tests/e2e-tests/spring/spring-rest-h2-z3solver/src/test/java/org/evomaster/e2etests/spring/h2/z3solver/Z3SolverEMTest.java‎

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -27,12 +27,9 @@ public void testRunEM() throws Throwable {
2727
"com.foo.spring.rest.h2.z3solver.Z3SolverEvoMaster",
2828
50,
2929
(args) -> {
30-
args.add("--heuristicsForSQL");
31-
args.add("true");
32-
args.add("--generateSqlDataWithSearch");
33-
args.add("false");
34-
args.add("--generateSqlDataWithZ3");
35-
args.add("true");
30+
setOption(args, "heuristicsForSQL", "true");
31+
setOption(args, "generateSqlDataWithSearch", "false");
32+
setOption(args, "generateSqlDataWithZ3", "true");
3633

3734
Solution<RestIndividual> solution = initAndRun(args);
3835

‎core/src/main/kotlin/org/evomaster/core/problem/api/service/ApiWsStructureMutator.kt‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -344,17 +344,17 @@ abstract class ApiWsStructureMutator : StructureMutator() {
344344
): MutableList<List<SqlAction>>? {
345345

346346
if (config.generateSqlDataWithSearch) {
347-
return handleSearch(ind, sampler, mutatedGenes, fw)
347+
return generateSqlDataWithSearch(ind, sampler, mutatedGenes, fw)
348348
}
349349

350350
if (config.generateSqlDataWithZ3) {
351-
return handleZ3(ind, sampler, failedWhereQueries)
351+
return generateSqlDataWithZ3(ind, sampler, failedWhereQueries)
352352
}
353353

354354
return mutableListOf()
355355
}
356356

357-
private fun <T : ApiWsIndividual> handleSearch(
357+
private fun <T : ApiWsIndividual> generateSqlDataWithSearch(
358358
ind: T,
359359
sampler: ApiWsSampler<T>,
360360
mutatedGenes: MutatedGeneSpecification?,
@@ -436,7 +436,7 @@ abstract class ApiWsStructureMutator : StructureMutator() {
436436
return addedSqlInsertions
437437
}
438438

439-
private fun <T : ApiWsIndividual> handleZ3(ind: T, sampler: ApiWsSampler<T>, failedWhereQueries: List<String>): MutableList<List<SqlAction>> {
439+
private fun <T : ApiWsIndividual> generateSqlDataWithZ3(ind: T, sampler: ApiWsSampler<T>, failedWhereQueries: List<String>): MutableList<List<SqlAction>> {
440440
val schemaDto = sampler.sqlInsertBuilder?.schemaDto
441441
?: throw IllegalStateException("No DB schema is available")
442442

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

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -74,6 +74,10 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver {
7474

7575
companion object {
7676
private const val MAX_CACHE_SIZE = 500
77+
78+
// Must match the timestamp format used by JSqlVisitor (TIMESTAMP_FORMAT) so that
79+
// epoch<->string conversions round-trip consistently.
80+
private const val TIMESTAMP_FORMAT = "yyyy-MM-dd HH:mm:ss"
7781
}
7882

7983
@Inject
@@ -292,7 +296,7 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver {
292296
Instant.ofEpochSecond(epochSeconds), ZoneOffset.UTC
293297
)
294298
val formatted = localDateTime.format(
295-
DateTimeFormatter.ofPattern("yyyy-MM-dd HH:mm:ss")
299+
DateTimeFormatter.ofPattern(TIMESTAMP_FORMAT)
296300
)
297301
ImmutableDataHolderGene(dbColumnName, formatted, inQuotes = true)
298302
} else {

0 commit comments

Comments
 (0)