states,
+ SourcePosition position, Factory factory, boolean silent, boolean needsCounterexample) throws LJError {
if (!silent) {
DebugLog.smtVerifying(position);
}
@@ -185,7 +194,7 @@ public SMTResult verifySMTSubtypeStates(Predicate type, Predicate expectedType,
SMTResult result;
try {
- result = dischargeToSMT(expected, premises, position, true);
+ result = dischargeToSMT(expected, premises, position, true, needsCounterexample);
} catch (RuntimeException ex) {
if (!silent) {
DebugLog.smtError(ex.getMessage());
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCConstraintSimplification.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCConstraintSimplification.java
index 0050f6611..a7376348d 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCConstraintSimplification.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCConstraintSimplification.java
@@ -71,7 +71,7 @@ private VCImplication remove(VCImplication implication, VCImplication removed) {
*/
private boolean implies(Predicate stronger, Predicate weaker) {
try {
- SMTResult result = new SMTEvaluator().verifySubtype(stronger, weaker, Context.getInstance(), true);
+ SMTResult result = new SMTEvaluator().verifySubtype(stronger, weaker, Context.getInstance(), true, false);
return result.isOk();
} catch (Exception e) {
return false;
diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/QueryCache.java b/liquidjava-verifier/src/main/java/liquidjava/smt/QueryCache.java
new file mode 100644
index 000000000..46a35476b
--- /dev/null
+++ b/liquidjava-verifier/src/main/java/liquidjava/smt/QueryCache.java
@@ -0,0 +1,245 @@
+package liquidjava.smt;
+
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.Collections;
+import java.util.HashSet;
+import java.util.LinkedHashMap;
+import java.util.List;
+import java.util.Map;
+import java.util.Optional;
+import java.util.Set;
+import java.util.stream.Collectors;
+
+import liquidjava.processor.context.Context;
+import liquidjava.processor.context.GhostFunction;
+import liquidjava.processor.context.RefinedVariable;
+import liquidjava.rj_language.ast.AliasInvocation;
+import liquidjava.rj_language.ast.BinaryExpression;
+import liquidjava.rj_language.ast.Enum;
+import liquidjava.rj_language.ast.Expression;
+import liquidjava.rj_language.ast.FunctionInvocation;
+import liquidjava.rj_language.ast.Ite;
+import liquidjava.rj_language.ast.LiteralBoolean;
+import liquidjava.rj_language.ast.LiteralChar;
+import liquidjava.rj_language.ast.LiteralInt;
+import liquidjava.rj_language.ast.LiteralLong;
+import liquidjava.rj_language.ast.LiteralReal;
+import liquidjava.rj_language.ast.LiteralString;
+import liquidjava.rj_language.ast.UnaryExpression;
+import liquidjava.rj_language.ast.Var;
+import liquidjava.rj_language.visitors.ExpressionVisitor;
+import spoon.reflect.declaration.CtEnum;
+import spoon.reflect.reference.CtTypeReference;
+
+/**
+ * Results of solver queries, kept across verification runs. A long-lived process such as the language server verifies
+ * the whole program again after every save, and asks the solver mostly the same queries each time.
+ *
+ * A query is identified by everything {@link TranslatorToZ3} reads to build it: the expression, node by node, the type
+ * and supertypes of each of its variables, and the enums, ghosts and ghost states of the context. Variables are renamed
+ * in order of appearance, so that a query whose variables were numbered differently by an earlier edit is still found.
+ * Names that denote enum constants are values, not variables, and keep their name. A counterexample names the
+ * variables, so a cached one is only reused when the names are the same; otherwise a caller that needs one asks the
+ * solver again. Unknown results and errors are never kept. Results only live as long as the process, so the verifier
+ * and the solver cannot change under them.
+ */
+final class QueryCache {
+
+ private static final int MAX_RESULTS = 50_000;
+
+ private static final Map RESULTS = Collections.synchronizedMap(new LinkedHashMap<>(16, 0.75f, true) {
+ @Override
+ protected boolean removeEldestEntry(Map.Entry eldest) {
+ return size() > MAX_RESULTS;
+ }
+ });
+
+ /**
+ * @param text
+ * the query with its variables renamed
+ * @param names
+ * the variables of the query, in the order they were renamed
+ */
+ record Key(String text, List names) {
+ }
+
+ /** A result, whose counterexample names the variables in {@code names} */
+ private record Entry(SMTResult result, List names) {
+ }
+
+ private QueryCache() {
+ }
+
+ static Key key(Expression expression, Context context) {
+ Map> types = context.getContext();
+ List occurrences = new ArrayList<>();
+ expression.getVariableNames(occurrences);
+ Set constants = enumConstants(types.values());
+ List names = occurrences.stream().distinct().filter(n -> types.containsKey(n) && !constants.contains(n))
+ .toList();
+
+ StringBuilder text = new StringBuilder(expression.accept(new Canonical(names))).append('\n');
+ Map> supertypes = new LinkedHashMap<>();
+ for (RefinedVariable variable : context.getAllVariablesWithSupertypes())
+ if (names.contains(variable.getName()))
+ supertypes.computeIfAbsent(variable.getName(), k -> new ArrayList<>()).add(
+ variable.getSuperTypes().stream().map(QueryCache::describe).collect(Collectors.joining(", ")));
+ for (int i = 0; i < names.size(); i++) {
+ String name = names.get(i);
+ text.append('@').append(i).append(": ").append(describe(types.get(name)));
+ supertypes.getOrDefault(name, List.of()).forEach(s -> text.append(" <: ").append(s));
+ text.append('\n');
+ }
+ // every enum of the context, as their constants can be named in the query
+ types.values().stream().filter(CtTypeReference::isEnum).map(QueryCache::describe).distinct()
+ .forEach(e -> text.append("enum ").append(e).append('\n'));
+ for (GhostFunction ghost : context.getGhosts())
+ text.append("ghost ").append(describe(ghost)).append('\n');
+ for (GhostFunction state : context.getGhostStates())
+ text.append("state ").append(describe(state)).append('\n');
+ return new Key(text.toString(), names);
+ }
+
+ /**
+ * The result kept for {@code key}, or nothing if there is none or it cannot be used: a counterexample is only
+ * reused when the variables have the same names
+ */
+ static Optional get(Key key, boolean needsCounterexample) {
+ Entry entry = RESULTS.get(key.text());
+ if (entry == null)
+ return Optional.empty();
+ if (entry.result().isOk() || entry.names().equals(key.names()))
+ return Optional.of(entry.result());
+ return needsCounterexample ? Optional.empty() : Optional.of(SMTResult.error(new Counterexample(List.of())));
+ }
+
+ static void put(Key key, SMTResult result) {
+ RESULTS.put(key.text(), new Entry(result, key.names()));
+ }
+
+ /**
+ * Fails if {@code recomputed} differs from {@code cached}, with an {@link AssertionError} so that code that
+ * recovers from exceptions cannot hide it
+ */
+ static void checkSame(Key key, SMTResult cached, SMTResult recomputed) {
+ boolean same = cached.isOk() == recomputed.isOk() && (cached.isOk() || cached.getCounterexample().isEmpty()
+ || cached.getCounterexample().equals(recomputed.getCounterexample()));
+ if (!same)
+ throw new AssertionError(
+ String.format("The solver query cache returned %s but recomputing gives %s for%n%s",
+ describe(cached), describe(recomputed), key.text()));
+ }
+
+ /** The names the translator binds to the constants of the enums, which denote values rather than variables */
+ private static Set enumConstants(Collection> types) {
+ Set constants = new HashSet<>();
+ for (CtTypeReference type : types)
+ if (type.isEnum() && type.getDeclaration()instanceof CtEnum declaration)
+ declaration.getEnumValues().forEach(
+ v -> constants.add(TranslatorContextToZ3.enumConstantName(declaration, v.getSimpleName())));
+ return constants;
+ }
+
+ private static String describe(SMTResult result) {
+ return result.isOk() ? "ok" : "error with " + result.getCounterexample();
+ }
+
+ /** What the translator reads from a type: its names, and the constants of an enum */
+ private static String describe(CtTypeReference type) {
+ if (type == null)
+ return "?";
+ if (type.isEnum() && type.getDeclaration()instanceof CtEnum declaration)
+ return type.getQualifiedName() + declaration.getEnumValues().stream().map(v -> v.getSimpleName()).toList();
+ return type.getQualifiedName() + " " + type;
+ }
+
+ private static String describe(GhostFunction ghost) {
+ return ghost.getQualifiedName() + ghost.getParametersTypes().stream().map(Object::toString).toList() + " "
+ + ghost.getReturnType();
+ }
+
+ /** The expression node by node, with its variables renamed in order of appearance */
+ private static final class Canonical implements ExpressionVisitor {
+
+ private final List names;
+
+ Canonical(List names) {
+ this.names = names;
+ }
+
+ private String all(List expressions) {
+ return expressions.stream().map(e -> e.accept(this)).collect(Collectors.joining(" "));
+ }
+
+ @Override
+ public String visitAliasInvocation(AliasInvocation alias) {
+ return "(alias " + alias.getName() + " " + all(alias.getArgs()) + ")";
+ }
+
+ @Override
+ public String visitBinaryExpression(BinaryExpression exp) {
+ return "(" + exp.getOperator() + " " + exp.getFirstOperand().accept(this) + " "
+ + exp.getSecondOperand().accept(this) + ")";
+ }
+
+ @Override
+ public String visitFunctionInvocation(FunctionInvocation fun) {
+ return "(call " + fun.getName() + " " + all(fun.getArgs()) + ")";
+ }
+
+ @Override
+ public String visitIte(Ite ite) {
+ return "(ite " + ite.getCondition().accept(this) + " " + ite.getThen().accept(this) + " "
+ + ite.getElse().accept(this) + ")";
+ }
+
+ @Override
+ public String visitLiteralInt(LiteralInt lit) {
+ return "(int " + lit.getValue() + ")";
+ }
+
+ @Override
+ public String visitLiteralLong(LiteralLong lit) {
+ return "(long " + lit.getValue() + ")";
+ }
+
+ @Override
+ public String visitLiteralBoolean(LiteralBoolean lit) {
+ return "(bool " + lit.isBooleanTrue() + ")";
+ }
+
+ @Override
+ public String visitLiteralChar(LiteralChar lit) {
+ return "(char " + (int) lit.getValue() + ")";
+ }
+
+ @Override
+ public String visitLiteralReal(LiteralReal lit) {
+ return "(real " + Double.doubleToLongBits(lit.getValue()) + ")";
+ }
+
+ @Override
+ public String visitLiteralString(LiteralString lit) {
+ return "(string " + lit.toString().length() + ":" + lit + ")";
+ }
+
+ @Override
+ public String visitUnaryExpression(UnaryExpression exp) {
+ return "(" + exp.getOp() + " " + exp.getExpression().accept(this) + ")";
+ }
+
+ @Override
+ public String visitEnum(Enum en) {
+ Expression literal = en.getResolvedLiteral();
+ return "(const " + en.getTypeName() + " " + en.getConstName() + " "
+ + (literal == null ? "-" : literal.accept(this)) + ")";
+ }
+
+ @Override
+ public String visitVar(Var var) {
+ int index = names.indexOf(var.getName());
+ return index < 0 ? "(free " + var.getName().length() + ":" + var.getName() + ")" : "@" + index;
+ }
+ }
+}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java
index 30f8ac242..6fc196326 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java
@@ -1,17 +1,18 @@
package liquidjava.smt;
-import com.martiansoftware.jsap.SyntaxException;
import com.microsoft.z3.Expr;
-import com.microsoft.z3.Model;
import com.microsoft.z3.Solver;
import com.microsoft.z3.Status;
import com.microsoft.z3.Z3Exception;
+import java.util.Optional;
+
import liquidjava.diagnostics.DebugLog;
import liquidjava.diagnostics.errors.SMTUnknownError;
import liquidjava.processor.context.Context;
import liquidjava.rj_language.Predicate;
import liquidjava.rj_language.ast.Expression;
+import liquidjava.utils.CacheMode;
public class SMTEvaluator {
@@ -31,64 +32,91 @@ public SMTResult verifySubtype(Predicate subRef, Predicate supRef, Context conte
public SMTResult verifySubtype(Predicate subRef, Predicate supRef, Context context, boolean silent)
throws Exception {
+ return verifySubtype(subRef, supRef, context, silent, true);
+ }
+
+ /**
+ * @param needsCounterexample
+ * whether the caller uses the counterexample of a failing check, which a result kept from an earlier run
+ * only has when the variables have the same names
+ */
+ public SMTResult verifySubtype(Predicate subRef, Predicate supRef, Context context, boolean silent,
+ boolean needsCounterexample) throws Exception {
if (!silent) {
DebugLog.smtStart(subRef, supRef);
}
Predicate toVerify = Predicate.createConjunction(subRef, supRef.negate());
try {
- Expression exp = toVerify.getExpression();
- try (TranslatorToZ3 tz3 = new TranslatorToZ3(context)) {
- ExpressionToZ3Visitor visitor = new ExpressionToZ3Visitor(tz3);
- Expr e = exp.accept(visitor);
- Solver solver = tz3.makeSimpleSolverForExpression(e);
- Status result = solver.check();
- if (result.equals(Status.UNKNOWN)) {
- solver = tz3.makeSolverForExpression(e);
- result = solver.check();
- }
-
- // subRef is not a subtype of supRef
- if (result.equals(Status.SATISFIABLE)) {
- Model model = solver.getModel();
- Counterexample counterexample = tz3.getCounterexample(model);
- if (!silent) {
- DebugLog.smtSat(counterexample);
- }
- return SMTResult.error(counterexample);
- }
- if (result.equals(Status.UNKNOWN)) {
- SMTUnknownError error = new SMTUnknownError(solver.getReasonUnknown());
- if (!silent) {
- DebugLog.smtError(error.getMessage());
- }
- throw error;
- }
- if (!silent) {
- DebugLog.smtUnsat();
- }
- }
- } catch (SyntaxException e) {
- System.out.println("Could not parse: " + toVerify);
- e.printStackTrace();
+ return check(toVerify.getExpression(), context, silent, needsCounterexample);
} catch (Z3Exception e) {
throw new Z3Exception(e.getLocalizedMessage());
}
- return SMTResult.ok();
}
public boolean isUnsatisfiable(Predicate predicate, Context context) throws Exception {
try {
- Expression exp = predicate.getExpression();
- try (TranslatorToZ3 tz3 = new TranslatorToZ3(context)) {
- ExpressionToZ3Visitor visitor = new ExpressionToZ3Visitor(tz3);
- Expr e = exp.accept(visitor);
- Status result = tz3.makeSimpleSolverForExpression(e).check();
- if (result.equals(Status.UNKNOWN))
- result = tz3.makeSolverForExpression(e).check();
- return result.equals(Status.UNSATISFIABLE);
- }
+ return check(predicate.getExpression(), context, true, false).isOk();
+ } catch (SMTUnknownError e) {
+ return false;
} catch (Z3Exception e) {
throw new Z3Exception(e.getLocalizedMessage());
}
}
+
+ /**
+ * Whether {@code exp} is unsatisfiable, with a counterexample when it is not, reusing the result of an earlier run
+ */
+ private SMTResult check(Expression exp, Context context, boolean silent, boolean needsCounterexample)
+ throws Exception {
+ CacheMode mode = CacheMode.current();
+ if (mode == CacheMode.OFF)
+ return solve(exp, context, silent);
+ QueryCache.Key key = QueryCache.key(exp, context);
+ Optional cached = QueryCache.get(key, needsCounterexample);
+ if (cached.isPresent() && mode == CacheMode.ON) {
+ if (!silent)
+ log(cached.get());
+ return cached.get();
+ }
+ SMTResult result = solve(exp, context, silent);
+ if (cached.isPresent())
+ QueryCache.checkSame(key, cached.get(), result);
+ else
+ QueryCache.put(key, result);
+ return result;
+ }
+
+ private SMTResult solve(Expression exp, Context context, boolean silent) throws Exception {
+ try (TranslatorToZ3 tz3 = new TranslatorToZ3(context)) {
+ ExpressionToZ3Visitor visitor = new ExpressionToZ3Visitor(tz3);
+ Expr e = exp.accept(visitor);
+ Solver solver = tz3.makeSimpleSolverForExpression(e);
+ Status result = solver.check();
+ if (result.equals(Status.UNKNOWN)) {
+ solver = tz3.makeSolverForExpression(e);
+ result = solver.check();
+ }
+
+ if (result.equals(Status.UNKNOWN)) {
+ SMTUnknownError error = new SMTUnknownError(solver.getReasonUnknown());
+ if (!silent) {
+ DebugLog.smtError(error.getMessage());
+ }
+ throw error;
+ }
+ // subRef is not a subtype of supRef
+ SMTResult verified = result.equals(Status.SATISFIABLE)
+ ? SMTResult.error(tz3.getCounterexample(solver.getModel())) : SMTResult.ok();
+ if (!silent)
+ log(verified);
+ return verified;
+ }
+ }
+
+ private static void log(SMTResult result) {
+ if (result.isOk())
+ DebugLog.smtUnsat();
+ else
+ DebugLog.smtSat(result.getCounterexample());
+ }
}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java
index 235cb170e..9e58bd905 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java
@@ -49,11 +49,16 @@ private static EnumSort translateEnum(Context z3, Map> varTra
EnumSort enumSort = z3.mkEnumSort(k, enumValueNames);
Expr[] consts = enumSort.getConsts();
for (int i = 0; i < enumValueNames.length; i++)
- varTranslation.put(enumDecl.getSimpleName() + "." + enumValueNames[i], consts[i]);
+ varTranslation.put(enumConstantName(enumDecl, enumValueNames[i]), consts[i]);
return enumSort;
});
}
+ /** The name the constant {@code value} of an enum is translated from, which denotes that constant */
+ static String enumConstantName(CtEnum enumDecl, String value) {
+ return enumDecl.getSimpleName() + "." + value;
+ }
+
public static void storeVariablesSubtypes(Context z3, List variables,
Map>> varSuperTypes) {
for (RefinedVariable v : variables) {
diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/CacheMode.java b/liquidjava-verifier/src/main/java/liquidjava/utils/CacheMode.java
new file mode 100644
index 000000000..779e647cc
--- /dev/null
+++ b/liquidjava-verifier/src/main/java/liquidjava/utils/CacheMode.java
@@ -0,0 +1,18 @@
+package liquidjava.utils;
+
+import java.util.Locale;
+
+/**
+ * Whether the verifier reuses solver results from earlier verification runs, set with the system property
+ * {@value #PROPERTY}: {@code on} (the default), {@code off}, or {@code check}, which recomputes every result found in
+ * the cache and fails if it differs, to test that the cache never changes what the verifier reports
+ */
+public enum CacheMode {
+ ON, OFF, CHECK;
+
+ public static final String PROPERTY = "liquidjava.cache";
+
+ public static CacheMode current() {
+ return valueOf(System.getProperty(PROPERTY, "on").toUpperCase(Locale.ROOT));
+ }
+}
diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestQueryCache.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestQueryCache.java
new file mode 100644
index 000000000..3c5f19a20
--- /dev/null
+++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestQueryCache.java
@@ -0,0 +1,191 @@
+package liquidjava.api.tests;
+
+import static org.junit.jupiter.api.Assertions.*;
+
+import java.io.IOException;
+import java.nio.file.Files;
+import java.nio.file.Path;
+import java.util.List;
+import java.util.stream.Stream;
+
+import org.junit.jupiter.api.Test;
+import org.junit.jupiter.api.io.TempDir;
+
+import liquidjava.api.CommandLineLauncher;
+import liquidjava.diagnostics.Diagnostics;
+import liquidjava.diagnostics.LJDiagnostic;
+import liquidjava.diagnostics.errors.NotFoundError;
+import liquidjava.diagnostics.errors.SyntaxError;
+import liquidjava.utils.CacheMode;
+
+/**
+ * The cache that keeps solver results across verification runs must never change what the verifier reports. Each test
+ * verifies a program, edits one thing the solver queries depend on without changing their text, and verifies it again,
+ * as the language server does after a save: the result must be the same as without the cache, and must change.
+ */
+class TestQueryCache {
+
+ private static final String DOOR = """
+ import liquidjava.specification.StateRefinement;
+ import liquidjava.specification.StateSet;
+
+ @StateSet({"created", "open", "closed"})
+ public class Test {
+
+ @StateRefinement(to = "created(this)")
+ public Test() {}
+
+ @StateRefinement(from = "created(this)", to = "%s(this)")
+ public void open() {}
+
+ @StateRefinement(from = "open(this)")
+ public void read() {}
+
+ @StateRefinement(from = "%s", to = "closed(this)")
+ public void close() {}
+
+ public static void main(String[] args) {
+ Test d = new Test();
+ d.open();
+ d.read();
+ }
+ }
+ """;
+
+ private static final String NUMBER = """
+ import liquidjava.specification.Refinement;
+
+ public class Test {
+ public static void atLeastOne(@Refinement("v >= 1") %1$s v) {}
+
+ public static void positive(@Refinement("v > 0") %1$s v) {
+ atLeastOne(v);
+ }
+ }
+ """;
+
+ private static final String COLOR = """
+ import liquidjava.specification.Refinement;
+
+ public class Test {
+ enum Color { %s }
+
+ public static void green(@Refinement("c == Color.Green") Color c) {}
+
+ public static void notRed(@Refinement("c != Color.Red") Color c) {
+ green(c);
+ }
+ }
+ """;
+
+ private static final String BOX = """
+ import liquidjava.specification.Ghost;
+ import liquidjava.specification.StateRefinement;
+
+ @Ghost("%s size")
+ public class Test {
+
+ @StateRefinement(to = "size(this) > 0")
+ public Test() {}
+
+ @StateRefinement(from = "size(this) >= 1")
+ public void take() {}
+
+ public static void main(String[] args) {
+ Test b = new Test();
+ b.take();
+ }
+ }
+ """;
+
+ private static final String MODE = """
+ import liquidjava.specification.Refinement;
+
+ public class Test {
+ enum Mode { Photo, Video }
+
+ public static void photo(@Refinement("m == Mode.Photo") Mode m) {}
+
+ public static void main(String[] args) {
+ photo(Mode.Photo);
+ photo(Mode.Video);
+ }
+ }
+ """;
+
+ @TempDir
+ Path dir;
+
+ @Test
+ void enumConstantsAreValuesNotVariables() throws IOException {
+ // the two calls only differ in the enum constant: the second must not reuse the result of the first
+ List cached = verify(MODE, CacheMode.ON);
+ assertEquals(verify(MODE, CacheMode.OFF), cached);
+ assertEquals(1, Diagnostics.getInstance().getErrors().size(), "photo(Mode.Video) must be reported");
+ }
+
+ @Test
+ void editedTransition() throws IOException {
+ assertSameAsUncachedAfterEdit(String.format(DOOR, "open", "open(this)"),
+ String.format(DOOR, "closed", "closed(this)"));
+ }
+
+ @Test
+ void stateRefinementThatCanNeverHold() throws IOException {
+ assertSameAsUncachedAfterEdit(String.format(DOOR, "open", "open(this)"),
+ String.format(DOOR, "open", "open(this) && closed(this)"));
+ }
+
+ @Test
+ void typeOfAVariable() throws IOException {
+ // integers greater than 0 are at least 1, but long values are reals to the solver
+ assertSameAsUncachedAfterEdit(String.format(NUMBER, "int"), String.format(NUMBER, "long"));
+ }
+
+ @Test
+ void constantsOfAnEnum() throws IOException {
+ assertSameAsUncachedAfterEdit(String.format(COLOR, "Red, Green"), String.format(COLOR, "Red, Green, Blue"));
+ }
+
+ @Test
+ void typeOfAGhost() throws IOException {
+ // sizes greater than 0 are at least 1 for an int ghost, but not for a double one
+ assertSameAsUncachedAfterEdit(String.format(BOX, "int"), String.format(BOX, "double"));
+ }
+
+ /** Verifies {@code before}, then {@code after} with the cache, which must report what it reports without it */
+ private void assertSameAsUncachedAfterEdit(String before, String after) throws IOException {
+ List reportedBefore = verify(before, CacheMode.ON);
+ assertWellFormed(before);
+ List cached = verify(after, CacheMode.ON);
+ List uncached = verify(after, CacheMode.OFF);
+ assertWellFormed(after);
+ assertEquals(uncached, cached);
+ assertNotEquals(reportedBefore, uncached, "the edit must change what the verifier reports");
+ }
+
+ /** The program must reach the solver, or the test would not exercise the cache */
+ private static void assertWellFormed(String source) {
+ assertTrue(
+ Diagnostics.getInstance().getErrors().stream()
+ .noneMatch(e -> e instanceof SyntaxError || e instanceof NotFoundError),
+ () -> "not well formed:\n" + source);
+ }
+
+ private List verify(String source, CacheMode mode) throws IOException {
+ Files.writeString(dir.resolve("Test.java"), source);
+ String previous = System.getProperty(CacheMode.PROPERTY);
+ System.setProperty(CacheMode.PROPERTY, mode.name());
+ try {
+ CommandLineLauncher.launch(dir.toString());
+ } finally {
+ if (previous == null)
+ System.clearProperty(CacheMode.PROPERTY);
+ else
+ System.setProperty(CacheMode.PROPERTY, previous);
+ }
+ Diagnostics diagnostics = Diagnostics.getInstance();
+ return Stream.concat(diagnostics.getErrors().stream(), diagnostics.getWarnings().stream())
+ .map(LJDiagnostic::toString).toList();
+ }
+}
diff --git a/liquidjava-verifier/src/test/java/liquidjava/smt/QueryCacheTest.java b/liquidjava-verifier/src/test/java/liquidjava/smt/QueryCacheTest.java
new file mode 100644
index 000000000..c61d299e9
--- /dev/null
+++ b/liquidjava-verifier/src/test/java/liquidjava/smt/QueryCacheTest.java
@@ -0,0 +1,72 @@
+package liquidjava.smt;
+
+import static org.junit.jupiter.api.Assertions.*;
+
+import java.util.List;
+import java.util.Set;
+
+import org.junit.jupiter.api.AfterEach;
+import org.junit.jupiter.api.Test;
+
+import liquidjava.processor.context.Context;
+import liquidjava.processor.context.Variable;
+import liquidjava.rj_language.Predicate;
+import spoon.Launcher;
+import spoon.reflect.factory.Factory;
+import spoon.reflect.reference.CtTypeReference;
+
+class QueryCacheTest {
+
+ private final Context context = Context.getInstance();
+ private final Factory factory = new Launcher().getFactory();
+
+ @AfterEach
+ void resetContext() {
+ context.reinitializeAllContext();
+ }
+
+ @Test
+ void variablesAreRenamedInOrderOfAppearance() {
+ addVariable("a", int.class);
+ addVariable("b", int.class);
+ addVariable("c", int.class);
+ addVariable("d", int.class);
+ QueryCache.Key ab = key("a > b");
+ QueryCache.Key cd = key("c > d");
+ assertEquals(ab.text(), cd.text());
+ assertEquals(List.of("a", "b"), ab.names());
+ assertEquals(List.of("c", "d"), cd.names());
+ QueryCache.Key ba = key("b > a");
+ assertEquals(ab.text(), ba.text());
+ assertEquals(List.of("b", "a"), ba.names());
+ assertNotEquals(ab.text(), key("a > a").text());
+ }
+
+ @Test
+ void typesOfTheVariablesAreInTheKey() {
+ addVariable("a", int.class);
+ addVariable("b", long.class);
+ assertNotEquals(key("a > 0").text(), key("b > 0").text());
+ }
+
+ @Test
+ void supertypesOfTheVariablesAreInTheKey() {
+ CtTypeReference type = factory.Type().createReference(java.io.IOException.class);
+ Variable plain = new Variable("plain", type, new Predicate());
+ Variable withSupertypes = new Variable("withSupertypes", type, new Predicate());
+ withSupertypes.addSuperTypes(factory.Type().createReference(Runnable.class), Set.of());
+ context.addVarToContext(plain);
+ context.addVarToContext(withSupertypes);
+ assertNotEquals(key("plain == plain").text(), key("withSupertypes == withSupertypes").text());
+ }
+
+ private void addVariable(String name, Class type) {
+ context.addVarToContext(name, factory.Type().createReference(type), new Predicate(),
+ factory.Code().createCodeSnippetStatement(""));
+ }
+
+ private QueryCache.Key key(String predicate) {
+ return QueryCache.key(
+ new Predicate(predicate, factory.Code().createCodeSnippetStatement(""), "").getExpression(), context);
+ }
+}