From 80a1d94e55192c0c5293bb2e28110269647aee6c Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 27 Oct 2026 13:18:55 +0000 Subject: [PATCH 1/3] Reuse solver results across verification runs A long-lived process such as the language server verifies the whole program again after every save, asking the solver mostly the same queries each time. Their results are now kept, identified by everything the translation to Z3 reads: the expression node by node, the types and supertypes of its variables (renamed in order of appearance), the enums, ghosts and ghost states of the context, and the solver configuration. Unknown results are never kept, and a counterexample is only reused when the variables have the same names. The system property liquidjava.caches turns the cache off, or makes it recompute every result it finds and fail on a difference, which the tests do. Co-Authored-By: Claude Opus 5.5 --- liquidjava-verifier/pom.xml | 632 +++++++++--------- .../refinement_checker/TypeChecker.java | 4 +- .../refinement_checker/VCChecker.java | 21 +- .../opt/VCConstraintSimplification.java | 2 +- .../main/java/liquidjava/smt/QueryCache.java | 230 +++++++ .../java/liquidjava/smt/SMTEvaluator.java | 123 ++-- .../java/liquidjava/smt/TranslatorToZ3.java | 2 +- .../main/java/liquidjava/utils/CacheMode.java | 28 + .../api/tests/TestSpecificationCaches.java | 100 +++ 9 files changed, 774 insertions(+), 368 deletions(-) create mode 100644 liquidjava-verifier/src/main/java/liquidjava/smt/QueryCache.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/utils/CacheMode.java create mode 100644 liquidjava-verifier/src/test/java/liquidjava/api/tests/TestSpecificationCaches.java diff --git a/liquidjava-verifier/pom.xml b/liquidjava-verifier/pom.xml index 9c16fa958..2e90736dc 100644 --- a/liquidjava-verifier/pom.xml +++ b/liquidjava-verifier/pom.xml @@ -1,94 +1,98 @@ - - 4.0.0 - - io.github.liquid-java - liquidjava-verifier - 0.0.36 - liquidjava-verifier - LiquidJava Verifier - https://github.com/liquid-java/liquidjava - jar - - - - MIT License - https://opensource.org/licenses/MIT - repo - - - - - - CatarinaGamboa - Catarina Gamboa - CatarinaGamboa@users.noreply.github.com - https://github.com/CatarinaGamboa - - - alcides - Alcides Fonseca - alcides@users.noreply.github.com - https://github.com/alcides - - - pcanelas - Paulo Canelas - pcanelas@users.noreply.github.com - https://github.com/pcanelas - - - rcosta358 - Ricardo Costa - rcosta358@users.noreply.github.com - https://github.com/rcosta358 - - - - - scm:git:git://github.com/liquid-java/liquidjava.git - scm:git:ssh://github.com:liquid-java/liquidjava.git - https://github.com/liquid-java/liquidjava/tree/main - - - - ${jar.finalName} - - - net.revelc.code.formatter - formatter-maven-plugin - 2.16.0 - - - validate - validate - - format - - - - - 20 - 20 - 20 - - - - org.apache.maven.plugins - maven-compiler-plugin - ${pVersion.compiler} - - 20 - 20 - - + + 4.0.0 + + io.github.liquid-java + liquidjava-verifier + 0.0.36 + liquidjava-verifier + LiquidJava Verifier + https://github.com/liquid-java/liquidjava + jar + + + + MIT License + https://opensource.org/licenses/MIT + repo + + + + + + CatarinaGamboa + Catarina Gamboa + CatarinaGamboa@users.noreply.github.com + https://github.com/CatarinaGamboa + + + alcides + Alcides Fonseca + alcides@users.noreply.github.com + https://github.com/alcides + + + pcanelas + Paulo Canelas + pcanelas@users.noreply.github.com + https://github.com/pcanelas + + + rcosta358 + Ricardo Costa + rcosta358@users.noreply.github.com + https://github.com/rcosta358 + + + + + scm:git:git://github.com/liquid-java/liquidjava.git + scm:git:ssh://github.com:liquid-java/liquidjava.git + https://github.com/liquid-java/liquidjava/tree/main + + + + ${jar.finalName} + + + net.revelc.code.formatter + formatter-maven-plugin + 2.16.0 + + + validate + validate + + format + + + + + 20 + 20 + 20 + + + + org.apache.maven.plugins + maven-compiler-plugin + ${pVersion.compiler} + + 20 + 20 + + org.apache.maven.plugins maven-surefire-plugin 3.2.1 - + true + + + check + @@ -120,188 +124,188 @@ org.antlr - antlr4-maven-plugin - 4.7.1 - - - - antlr4 - - - - - - org.apache.maven.plugins - maven-shade-plugin - 3.2.4 - - - package - - shade - - - - - liquidjava.api.CommandLineLauncher - - - - - *:* - - META-INF/*.SF - META-INF/*.DSA - META-INF/*.RSA - - - - - - - - - - - org.apache.maven.plugins - maven-source-plugin - 3.3.0 - - - attach-sources - - jar-no-fork - - - - - - - - org.apache.maven.plugins - maven-javadoc-plugin - 3.6.0 - - - attach-javadocs - - jar - - - - - none - 20 - - - - - - org.apache.maven.plugins - maven-gpg-plugin - 3.1.0 - - ${gpg.skip} - - - - sign-artifacts - verify - - sign - - - - - - - - org.apache.maven.plugins - maven-deploy-plugin - 3.1.2 - - true - - - - - - org.sonatype.central - central-publishing-maven-plugin - 0.9.0 - true - - central - ${maven.deploy.skip} - true - published + antlr4-maven-plugin + 4.7.1 + + + + antlr4 + + + + + + org.apache.maven.plugins + maven-shade-plugin + 3.2.4 + + + package + + shade + + + + + liquidjava.api.CommandLineLauncher + + + + + *:* + + META-INF/*.SF + META-INF/*.DSA + META-INF/*.RSA + + + + + + + + + + + org.apache.maven.plugins + maven-source-plugin + 3.3.0 + + + attach-sources + + jar-no-fork + + + + + + + + org.apache.maven.plugins + maven-javadoc-plugin + 3.6.0 + + + attach-javadocs + + jar + + + + + none + 20 + + + + + + org.apache.maven.plugins + maven-gpg-plugin + 3.1.0 + + ${gpg.skip} + + + + sign-artifacts + verify + + sign + + + + + + + + org.apache.maven.plugins + maven-deploy-plugin + 3.1.2 + + true + + + + + + org.sonatype.central + central-publishing-maven-plugin + 0.9.0 + true + + central + ${maven.deploy.skip} + true + published 3600 - - - - - - - - central - https://central.sonatype.com/api/v1/publisher - - - - - UTF-8 - 20 - 20 - 20 - - 5.10.0 - 1.3.0 + + + + + + + + central + https://central.sonatype.com/api/v1/publisher + + + + + UTF-8 + 20 + 20 + 20 + + 5.10.0 + 1.3.0 1.12.0 - 11.5.0 - 4.8.17 - - 3.8.0 - 3.1.2 - - ${project.artifactId}-${project.version} - true - true - - - - - - central - Central Repository - https://repo.maven.apache.org/maven2 - default - - false - - - - + 11.5.0 + 4.8.17 + + 3.8.0 + 3.1.2 + + ${project.artifactId}-${project.version} + true + true + + + + + + central + Central Repository + https://repo.maven.apache.org/maven2 + default + + false + + + + org.apache.commons commons-text ${version.commons-text} - - - org.junit.platform - junit-platform-launcher - test - - - org.junit.jupiter - junit-jupiter-engine - test - - - org.junit.vintage - junit-vintage-engine - test - + + + org.junit.platform + junit-platform-launcher + test + + + org.junit.jupiter + junit-jupiter-engine + test + + + org.junit.vintage + junit-vintage-engine + test + org.junit.jupiter junit-jupiter-params @@ -324,56 +328,56 @@ logback-classic 1.4.12 - - org.mdkt.compiler - InMemoryJavaCompiler - ${version.memcompiler} - - - - fr.inria.gforge.spoon - spoon-core - ${version.spoon} - - - tools.aqua - z3-turnkey - ${version.z3} - - - - io.github.liquid-java - liquidjava-api - 0.0.7 - - - - org.antlr - antlr4-runtime - 4.7.1 - - - - com.google.code.gson - gson - 2.10.1 - - - - info.picocli - picocli - 4.7.7 - - - - - - org.junit - junit-bom - 5.10.0 - pom - import - - - - + + org.mdkt.compiler + InMemoryJavaCompiler + ${version.memcompiler} + + + + fr.inria.gforge.spoon + spoon-core + ${version.spoon} + + + tools.aqua + z3-turnkey + ${version.z3} + + + + io.github.liquid-java + liquidjava-api + 0.0.7 + + + + org.antlr + antlr4-runtime + 4.7.1 + + + + com.google.code.gson + gson + 2.10.1 + + + + info.picocli + picocli + 4.7.7 + + + + + + org.junit + junit-bom + 5.10.0 + pom + import + + + + diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java index 5cf795f90..804e94233 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java @@ -415,7 +415,9 @@ public boolean checkStateSMT(Predicate prevState, Predicate expectedState, Sourc public boolean checkStateSMT(Predicate prevState, Predicate expectedState, SourcePosition p, boolean silent) throws LJError { - return verifyStateSMT(prevState, expectedState, p, silent).isOk(); + return vcChecker + .verifySMTSubtypeStates(prevState, expectedState, context.getGhostStates(), p, factory, silent, false) + .isOk(); } /** Checks that {@code prevState} implies {@code expectedState}, with a counterexample when it does not */ diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java index 0c2f4b9d8..819e4b6a2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java @@ -71,7 +71,7 @@ public void processSubtyping(Predicate expectedType, List list, CtEl DebugLog.smtStart(impl, expected); SMTResult result; try { - result = dischargeToSMT(expected, premises, annotationValuePos, true); + result = dischargeToSMT(expected, premises, annotationValuePos, true, true); } catch (SMTUnknownError error) { error.setDeclarationPosition(declarationPosition); DebugLog.smtError(error.getMessage()); @@ -123,13 +123,13 @@ public void processSubtyping(Predicate type, Predicate expectedType, List states, SourcePosition position, Factory factory, boolean silent) throws LJError { + return verifySMTSubtypeStates(type, expectedType, states, position, factory, silent, true); + } + + /** + * @param needsCounterexample + * whether the caller uses the counterexample when the verification fails + */ + public SMTResult verifySMTSubtypeStates(Predicate type, Predicate expectedType, List 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..ece70ce08 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/QueryCache.java @@ -0,0 +1,230 @@ +package liquidjava.smt; + +import java.util.ArrayList; +import java.util.Collections; +import java.util.LinkedHashMap; +import java.util.List; +import java.util.Map; +import java.util.Optional; +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 liquidjava.utils.CacheMode; +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, the enums and the ghosts and ghost states of the context, and the solver + * configuration. Variables are renamed in order of appearance, so that a query whose variables were numbered + * differently by an earlier edit is still found. 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. + */ +final class QueryCache { + + /** Changes when the way queries are solved changes */ + private static final String SOLVER = "simple solver with rlimit " + TranslatorToZ3.SIMPLE_SOLVER_RLIMIT + + ", then default solver"; + + 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) { + } + + /** {@code counterexample} is null when the query holds; it names the variables in {@code names} */ + private record Result(Counterexample counterexample, List names) { + } + + private QueryCache() { + } + + static Key key(Expression expression, Context context) { + Map> types = context.getContext(); + List occurrences = new ArrayList<>(); + expression.getVariableNames(occurrences); + List names = occurrences.stream().distinct().filter(types::containsKey).toList(); + + StringBuilder text = new StringBuilder(SOLVER).append('\n'); + text.append(expression.accept(new Canonical(names))).append('\n'); + for (int i = 0; i < names.size(); i++) { + String name = names.get(i); + text.append('@').append(i).append(": ").append(describe(types.get(name))); + for (RefinedVariable variable : context.getAllVariablesWithSupertypes()) + if (variable.getName().equals(name)) + text.append(" <: ").append(variable.getSuperTypes().stream().map(QueryCache::describe) + .collect(Collectors.joining(", "))); + text.append('\n'); + } + // every enum of the context, as their constants can be named in the query + for (CtTypeReference type : types.values()) + if (type.isEnum()) + text.append("enum ").append(describe(type)).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) { + if (CacheMode.current() == CacheMode.OFF) + return Optional.empty(); + Result result = RESULTS.get(key.text()); + if (result == null) + return Optional.empty(); + if (result.counterexample() == null) + return Optional.of(SMTResult.ok()); + if (result.names().equals(key.names())) + return Optional.of(SMTResult.error(result.counterexample())); + return needsCounterexample ? Optional.empty() : Optional.of(SMTResult.error(new Counterexample(List.of()))); + } + + static void put(Key key, SMTResult result) { + if (CacheMode.current() != CacheMode.OFF) + RESULTS.put(key.text(), new Result(result.getCounterexample(), key.names())); + } + + /** Fails if {@code recomputed} differs from the result kept for {@code key} */ + static void checkSame(Key key, SMTResult cached, SMTResult recomputed) { + CacheMode.checkSame("solver query", cached.isOk(), recomputed.isOk()); + if (cached.isError() && !cached.getCounterexample().isEmpty()) + CacheMode.checkSame("solver query", cached.getCounterexample(), recomputed.getCounterexample()); + } + + /** What the translator reads from a type: its name, 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..b7db048d9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java @@ -1,17 +1,19 @@ 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 +33,95 @@ 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) { + if (cached.get().isOk()) + DebugLog.smtUnsat(); + else + DebugLog.smtSat(cached.get().getCounterexample()); + } + 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(); + } + + // 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(); + } + return SMTResult.ok(); + } + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java index ed497c1a2..792e533e1 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java @@ -41,7 +41,7 @@ public class TranslatorToZ3 implements AutoCloseable { * Deterministic work budget of the simple solver. Queries it decides use at most about a thousand units; ones it * cannot decide can take millions, and minutes, before it gives up */ - private static final int SIMPLE_SOLVER_RLIMIT = 100_000; + static final int SIMPLE_SOLVER_RLIMIT = 100_000; private final com.microsoft.z3.Context z3 = new com.microsoft.z3.Context(); private final Map> varTranslation = new HashMap<>(); 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..c7d49b03a --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/CacheMode.java @@ -0,0 +1,28 @@ +package liquidjava.utils; + +import java.util.Locale; + +/** + * How the caches that reuse solver results across verification runs behave, set with the system property + * {@value #PROPERTY}: {@code on} (the default), {@code off}, or {@code check}, which recomputes every result found in a + * cache and fails if it differs, to test that the caches never change what the verifier reports + */ +public enum CacheMode { + ON, OFF, CHECK; + + public static final String PROPERTY = "liquidjava.caches"; + + public static CacheMode current() { + return valueOf(System.getProperty(PROPERTY, "on").toUpperCase(Locale.ROOT)); + } + + /** + * Fails when a cached result differs from the recomputed one. An {@link AssertionError}, so that code that recovers + * from exceptions cannot hide it + */ + public static void checkSame(String cache, Object cached, Object recomputed) { + if (!cached.equals(recomputed)) + throw new AssertionError( + String.format("The %s cache returned %s but recomputing gives %s", cache, cached, recomputed)); + } +} diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestSpecificationCaches.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestSpecificationCaches.java new file mode 100644 index 000000000..55e1660a7 --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestSpecificationCaches.java @@ -0,0 +1,100 @@ +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.StateConflictError; +import liquidjava.utils.CacheMode; + +/** + * The cache that keeps solver results across verification runs must never change what the verifier reports, in + * particular after a specification is edited between runs, as in the language server + */ +class TestSpecificationCaches { + + private static final String DOOR = """ + import liquidjava.specification.StateRefinement; + import liquidjava.specification.StateSet; + + @StateSet({"created", "open", "closed"}) + public class Door { + + @StateRefinement(to = "created(this)") + public Door() {} + + @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) { + Door d = new Door(); + d.read(); + } + } + """; + + @TempDir + Path dir; + + @Test + void editedTransitionIsNotTakenFromTheCache() throws IOException { + verifyCached(door("open", "open(this)")); + List edited = verifyCached(door("closed", "closed(this)")); + assertEquals(verifyUncached(), edited); + } + + @Test + void stateRefinementThatCanNeverHoldIsReportedAfterAnEdit() throws IOException { + verifyCached(door("open", "open(this)")); + List edited = verifyCached(door("open", "open(this) && closed(this)")); + assertEquals(verifyUncached(), edited); + assertTrue(Diagnostics.getInstance().getErrors().stream().anyMatch(e -> e instanceof StateConflictError), + "the conflicting state refinement must be reported"); + } + + private String door(String opened, String closable) { + return String.format(DOOR, opened, closable); + } + + /** Verifies {@code source} with the caches in use, and returns what the verifier reported */ + private List verifyCached(String source) throws IOException { + Files.writeString(dir.resolve("Door.java"), source); + return verify(CacheMode.ON); + } + + private List verifyUncached() { + return verify(CacheMode.OFF); + } + + private List verify(CacheMode mode) { + 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(); + } +} From 2d6d5cabd43eaf8e3b80c7b4d4a5a80157acb5a5 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 27 Oct 2026 13:38:09 +0000 Subject: [PATCH 2/3] Test that the solver cache follows edits to everything a query depends on Co-Authored-By: Claude Opus 5.5 --- .../liquidjava/api/tests/TestQueryCache.java | 155 ++++++++++++++++++ .../api/tests/TestSpecificationCaches.java | 100 ----------- .../java/liquidjava/smt/QueryCacheTest.java | 72 ++++++++ 3 files changed, 227 insertions(+), 100 deletions(-) create mode 100644 liquidjava-verifier/src/test/java/liquidjava/api/tests/TestQueryCache.java delete mode 100644 liquidjava-verifier/src/test/java/liquidjava/api/tests/TestSpecificationCaches.java create mode 100644 liquidjava-verifier/src/test/java/liquidjava/smt/QueryCacheTest.java 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..5bb3eb325 --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestQueryCache.java @@ -0,0 +1,155 @@ +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.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(); + } + } + """; + + @TempDir + Path dir; + + @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 { + assertSameAsUncachedAfterEdit(String.format(BOX, "int"), String.format(BOX, "long")); + } + + /** 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); + List cached = verify(after, CacheMode.ON); + List uncached = verify(after, CacheMode.OFF); + assertEquals(uncached, cached); + assertNotEquals(reportedBefore, uncached, "the edit must change what the verifier reports"); + } + + 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/api/tests/TestSpecificationCaches.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestSpecificationCaches.java deleted file mode 100644 index 55e1660a7..000000000 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestSpecificationCaches.java +++ /dev/null @@ -1,100 +0,0 @@ -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.StateConflictError; -import liquidjava.utils.CacheMode; - -/** - * The cache that keeps solver results across verification runs must never change what the verifier reports, in - * particular after a specification is edited between runs, as in the language server - */ -class TestSpecificationCaches { - - private static final String DOOR = """ - import liquidjava.specification.StateRefinement; - import liquidjava.specification.StateSet; - - @StateSet({"created", "open", "closed"}) - public class Door { - - @StateRefinement(to = "created(this)") - public Door() {} - - @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) { - Door d = new Door(); - d.read(); - } - } - """; - - @TempDir - Path dir; - - @Test - void editedTransitionIsNotTakenFromTheCache() throws IOException { - verifyCached(door("open", "open(this)")); - List edited = verifyCached(door("closed", "closed(this)")); - assertEquals(verifyUncached(), edited); - } - - @Test - void stateRefinementThatCanNeverHoldIsReportedAfterAnEdit() throws IOException { - verifyCached(door("open", "open(this)")); - List edited = verifyCached(door("open", "open(this) && closed(this)")); - assertEquals(verifyUncached(), edited); - assertTrue(Diagnostics.getInstance().getErrors().stream().anyMatch(e -> e instanceof StateConflictError), - "the conflicting state refinement must be reported"); - } - - private String door(String opened, String closable) { - return String.format(DOOR, opened, closable); - } - - /** Verifies {@code source} with the caches in use, and returns what the verifier reported */ - private List verifyCached(String source) throws IOException { - Files.writeString(dir.resolve("Door.java"), source); - return verify(CacheMode.ON); - } - - private List verifyUncached() { - return verify(CacheMode.OFF); - } - - private List verify(CacheMode mode) { - 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); + } +} From 9e686311e8e56d4e4449b6f6050bf3b0d8837c28 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 27 Oct 2026 16:10:39 +0000 Subject: [PATCH 3/3] Never rename enum constants in solver cache keys, and simplify the cache Enum constants reach the translator as names it binds to fixed values, so the cache must keep them: renaming them like variables gave m == Mode.Photo and m == Mode.Video the same key. Found by the check mode; tested by enumConstantsAreValuesNotVariables. Also, from review: drop the solver description from the key (results only live in memory, so the solver cannot change under them), leave the cache mode to SMTEvaluator, store the SMTResult itself, report the key on a mismatch, rename the property to liquidjava.cache, keep pom.xml's line endings, test the ghost type with double (long is not a ghost type), and check that each edited program reaches the solver. Co-Authored-By: Claude Opus 5.5 --- liquidjava-verifier/pom.xml | 632 +++++++++--------- .../refinement_checker/TypeChecker.java | 12 +- .../main/java/liquidjava/smt/QueryCache.java | 105 +-- .../java/liquidjava/smt/SMTEvaluator.java | 35 +- .../liquidjava/smt/TranslatorContextToZ3.java | 7 +- .../java/liquidjava/smt/TranslatorToZ3.java | 2 +- .../main/java/liquidjava/utils/CacheMode.java | 18 +- .../liquidjava/api/tests/TestQueryCache.java | 38 +- 8 files changed, 447 insertions(+), 402 deletions(-) diff --git a/liquidjava-verifier/pom.xml b/liquidjava-verifier/pom.xml index 2e90736dc..84891bc2b 100644 --- a/liquidjava-verifier/pom.xml +++ b/liquidjava-verifier/pom.xml @@ -1,97 +1,97 @@ - - 4.0.0 - - io.github.liquid-java - liquidjava-verifier - 0.0.36 - liquidjava-verifier - LiquidJava Verifier - https://github.com/liquid-java/liquidjava - jar - - - - MIT License - https://opensource.org/licenses/MIT - repo - - - - - - CatarinaGamboa - Catarina Gamboa - CatarinaGamboa@users.noreply.github.com - https://github.com/CatarinaGamboa - - - alcides - Alcides Fonseca - alcides@users.noreply.github.com - https://github.com/alcides - - - pcanelas - Paulo Canelas - pcanelas@users.noreply.github.com - https://github.com/pcanelas - - - rcosta358 - Ricardo Costa - rcosta358@users.noreply.github.com - https://github.com/rcosta358 - - - - - scm:git:git://github.com/liquid-java/liquidjava.git - scm:git:ssh://github.com:liquid-java/liquidjava.git - https://github.com/liquid-java/liquidjava/tree/main - - - - ${jar.finalName} - - - net.revelc.code.formatter - formatter-maven-plugin - 2.16.0 - - - validate - validate - - format - - - - - 20 - 20 - 20 - - - - org.apache.maven.plugins - maven-compiler-plugin - ${pVersion.compiler} - - 20 - 20 - - + + 4.0.0 + + io.github.liquid-java + liquidjava-verifier + 0.0.36 + liquidjava-verifier + LiquidJava Verifier + https://github.com/liquid-java/liquidjava + jar + + + + MIT License + https://opensource.org/licenses/MIT + repo + + + + + + CatarinaGamboa + Catarina Gamboa + CatarinaGamboa@users.noreply.github.com + https://github.com/CatarinaGamboa + + + alcides + Alcides Fonseca + alcides@users.noreply.github.com + https://github.com/alcides + + + pcanelas + Paulo Canelas + pcanelas@users.noreply.github.com + https://github.com/pcanelas + + + rcosta358 + Ricardo Costa + rcosta358@users.noreply.github.com + https://github.com/rcosta358 + + + + + scm:git:git://github.com/liquid-java/liquidjava.git + scm:git:ssh://github.com:liquid-java/liquidjava.git + https://github.com/liquid-java/liquidjava/tree/main + + + + ${jar.finalName} + + + net.revelc.code.formatter + formatter-maven-plugin + 2.16.0 + + + validate + validate + + format + + + + + 20 + 20 + 20 + + + + org.apache.maven.plugins + maven-compiler-plugin + ${pVersion.compiler} + + 20 + 20 + + org.apache.maven.plugins maven-surefire-plugin 3.2.1 - + true - - check + + check @@ -124,188 +124,188 @@ org.antlr - antlr4-maven-plugin - 4.7.1 - - - - antlr4 - - - - - - org.apache.maven.plugins - maven-shade-plugin - 3.2.4 - - - package - - shade - - - - - liquidjava.api.CommandLineLauncher - - - - - *:* - - META-INF/*.SF - META-INF/*.DSA - META-INF/*.RSA - - - - - - - - - - - org.apache.maven.plugins - maven-source-plugin - 3.3.0 - - - attach-sources - - jar-no-fork - - - - - - - - org.apache.maven.plugins - maven-javadoc-plugin - 3.6.0 - - - attach-javadocs - - jar - - - - - none - 20 - - - - - - org.apache.maven.plugins - maven-gpg-plugin - 3.1.0 - - ${gpg.skip} - - - - sign-artifacts - verify - - sign - - - - - - - - org.apache.maven.plugins - maven-deploy-plugin - 3.1.2 - - true - - - - - - org.sonatype.central - central-publishing-maven-plugin - 0.9.0 - true - - central - ${maven.deploy.skip} - true - published + antlr4-maven-plugin + 4.7.1 + + + + antlr4 + + + + + + org.apache.maven.plugins + maven-shade-plugin + 3.2.4 + + + package + + shade + + + + + liquidjava.api.CommandLineLauncher + + + + + *:* + + META-INF/*.SF + META-INF/*.DSA + META-INF/*.RSA + + + + + + + + + + + org.apache.maven.plugins + maven-source-plugin + 3.3.0 + + + attach-sources + + jar-no-fork + + + + + + + + org.apache.maven.plugins + maven-javadoc-plugin + 3.6.0 + + + attach-javadocs + + jar + + + + + none + 20 + + + + + + org.apache.maven.plugins + maven-gpg-plugin + 3.1.0 + + ${gpg.skip} + + + + sign-artifacts + verify + + sign + + + + + + + + org.apache.maven.plugins + maven-deploy-plugin + 3.1.2 + + true + + + + + + org.sonatype.central + central-publishing-maven-plugin + 0.9.0 + true + + central + ${maven.deploy.skip} + true + published 3600 - - - - - - - - central - https://central.sonatype.com/api/v1/publisher - - - - - UTF-8 - 20 - 20 - 20 - - 5.10.0 - 1.3.0 + + + + + + + + central + https://central.sonatype.com/api/v1/publisher + + + + + UTF-8 + 20 + 20 + 20 + + 5.10.0 + 1.3.0 1.12.0 - 11.5.0 - 4.8.17 - - 3.8.0 - 3.1.2 - - ${project.artifactId}-${project.version} - true - true - - - - - - central - Central Repository - https://repo.maven.apache.org/maven2 - default - - false - - - - + 11.5.0 + 4.8.17 + + 3.8.0 + 3.1.2 + + ${project.artifactId}-${project.version} + true + true + + + + + + central + Central Repository + https://repo.maven.apache.org/maven2 + default + + false + + + + org.apache.commons commons-text ${version.commons-text} - - - org.junit.platform - junit-platform-launcher - test - - - org.junit.jupiter - junit-jupiter-engine - test - - - org.junit.vintage - junit-vintage-engine - test - + + + org.junit.platform + junit-platform-launcher + test + + + org.junit.jupiter + junit-jupiter-engine + test + + + org.junit.vintage + junit-vintage-engine + test + org.junit.jupiter junit-jupiter-params @@ -328,56 +328,56 @@ logback-classic 1.4.12 - - org.mdkt.compiler - InMemoryJavaCompiler - ${version.memcompiler} - - - - fr.inria.gforge.spoon - spoon-core - ${version.spoon} - - - tools.aqua - z3-turnkey - ${version.z3} - - - - io.github.liquid-java - liquidjava-api - 0.0.7 - - - - org.antlr - antlr4-runtime - 4.7.1 - - - - com.google.code.gson - gson - 2.10.1 - - - - info.picocli - picocli - 4.7.7 - - - - - - org.junit - junit-bom - 5.10.0 - pom - import - - - - + + org.mdkt.compiler + InMemoryJavaCompiler + ${version.memcompiler} + + + + fr.inria.gforge.spoon + spoon-core + ${version.spoon} + + + tools.aqua + z3-turnkey + ${version.z3} + + + + io.github.liquid-java + liquidjava-api + 0.0.7 + + + + org.antlr + antlr4-runtime + 4.7.1 + + + + com.google.code.gson + gson + 2.10.1 + + + + info.picocli + picocli + 4.7.7 + + + + + + org.junit + junit-bom + 5.10.0 + pom + import + + + + diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java index 804e94233..fb9efd2ec 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java @@ -415,15 +415,19 @@ public boolean checkStateSMT(Predicate prevState, Predicate expectedState, Sourc public boolean checkStateSMT(Predicate prevState, Predicate expectedState, SourcePosition p, boolean silent) throws LJError { - return vcChecker - .verifySMTSubtypeStates(prevState, expectedState, context.getGhostStates(), p, factory, silent, false) - .isOk(); + return verifyStateSMT(prevState, expectedState, p, silent, false).isOk(); } /** Checks that {@code prevState} implies {@code expectedState}, with a counterexample when it does not */ public SMTResult verifyStateSMT(Predicate prevState, Predicate expectedState, SourcePosition p, boolean silent) throws LJError { - return vcChecker.verifySMTSubtypeStates(prevState, expectedState, context.getGhostStates(), p, factory, silent); + return verifyStateSMT(prevState, expectedState, p, silent, true); + } + + private SMTResult verifyStateSMT(Predicate prevState, Predicate expectedState, SourcePosition p, boolean silent, + boolean needsCounterexample) throws LJError { + return vcChecker.verifySMTSubtypeStates(prevState, expectedState, context.getGhostStates(), p, factory, silent, + needsCounterexample); } public void throwRefinementError(SourcePosition position, SourcePosition declarationPosition, diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/QueryCache.java b/liquidjava-verifier/src/main/java/liquidjava/smt/QueryCache.java index ece70ce08..46a35476b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/QueryCache.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/QueryCache.java @@ -1,11 +1,14 @@ 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; @@ -26,7 +29,6 @@ import liquidjava.rj_language.ast.UnaryExpression; import liquidjava.rj_language.ast.Var; import liquidjava.rj_language.visitors.ExpressionVisitor; -import liquidjava.utils.CacheMode; import spoon.reflect.declaration.CtEnum; import spoon.reflect.reference.CtTypeReference; @@ -35,27 +37,23 @@ * 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, the enums and the ghosts and ghost states of the context, and the solver - * configuration. Variables are renamed in order of appearance, so that a query whose variables were numbered - * differently by an earlier edit is still found. 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. + * 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 { - /** Changes when the way queries are solved changes */ - private static final String SOLVER = "simple solver with rlimit " + TranslatorToZ3.SIMPLE_SOLVER_RLIMIT - + ", then default solver"; - 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; - } - }); + 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 @@ -66,8 +64,8 @@ protected boolean removeEldestEntry(Map.Entry eldest) { record Key(String text, List names) { } - /** {@code counterexample} is null when the query holds; it names the variables in {@code names} */ - private record Result(Counterexample counterexample, List names) { + /** A result, whose counterexample names the variables in {@code names} */ + private record Entry(SMTResult result, List names) { } private QueryCache() { @@ -77,23 +75,25 @@ static Key key(Expression expression, Context context) { Map> types = context.getContext(); List occurrences = new ArrayList<>(); expression.getVariableNames(occurrences); - List names = occurrences.stream().distinct().filter(types::containsKey).toList(); - - StringBuilder text = new StringBuilder(SOLVER).append('\n'); - text.append(expression.accept(new Canonical(names))).append('\n'); + 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))); - for (RefinedVariable variable : context.getAllVariablesWithSupertypes()) - if (variable.getName().equals(name)) - text.append(" <: ").append(variable.getSuperTypes().stream().map(QueryCache::describe) - .collect(Collectors.joining(", "))); + 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 - for (CtTypeReference type : types.values()) - if (type.isEnum()) - text.append("enum ").append(describe(type)).append('\n'); + 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()) @@ -106,31 +106,46 @@ static Key key(Expression expression, Context context) { * reused when the variables have the same names */ static Optional get(Key key, boolean needsCounterexample) { - if (CacheMode.current() == CacheMode.OFF) - return Optional.empty(); - Result result = RESULTS.get(key.text()); - if (result == null) + Entry entry = RESULTS.get(key.text()); + if (entry == null) return Optional.empty(); - if (result.counterexample() == null) - return Optional.of(SMTResult.ok()); - if (result.names().equals(key.names())) - return Optional.of(SMTResult.error(result.counterexample())); + 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) { - if (CacheMode.current() != CacheMode.OFF) - RESULTS.put(key.text(), new Result(result.getCounterexample(), key.names())); + RESULTS.put(key.text(), new Entry(result, key.names())); } - /** Fails if {@code recomputed} differs from the result kept for {@code key} */ + /** + * 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) { - CacheMode.checkSame("solver query", cached.isOk(), recomputed.isOk()); - if (cached.isError() && !cached.getCounterexample().isEmpty()) - CacheMode.checkSame("solver query", cached.getCounterexample(), recomputed.getCounterexample()); + 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 name, and the constants of an enum */ + /** 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 "?"; diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java index b7db048d9..6fc196326 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java @@ -1,7 +1,6 @@ package liquidjava.smt; 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; @@ -75,12 +74,8 @@ private SMTResult check(Expression exp, Context context, boolean silent, boolean QueryCache.Key key = QueryCache.key(exp, context); Optional cached = QueryCache.get(key, needsCounterexample); if (cached.isPresent() && mode == CacheMode.ON) { - if (!silent) { - if (cached.get().isOk()) - DebugLog.smtUnsat(); - else - DebugLog.smtSat(cached.get().getCounterexample()); - } + if (!silent) + log(cached.get()); return cached.get(); } SMTResult result = solve(exp, context, silent); @@ -102,15 +97,6 @@ private SMTResult solve(Expression exp, Context context, boolean silent) throws 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) { @@ -118,10 +104,19 @@ private SMTResult solve(Expression exp, Context context, boolean silent) throws } throw error; } - if (!silent) { - DebugLog.smtUnsat(); - } - return SMTResult.ok(); + // 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/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java index 792e533e1..ed497c1a2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java @@ -41,7 +41,7 @@ public class TranslatorToZ3 implements AutoCloseable { * Deterministic work budget of the simple solver. Queries it decides use at most about a thousand units; ones it * cannot decide can take millions, and minutes, before it gives up */ - static final int SIMPLE_SOLVER_RLIMIT = 100_000; + private static final int SIMPLE_SOLVER_RLIMIT = 100_000; private final com.microsoft.z3.Context z3 = new com.microsoft.z3.Context(); private final Map> varTranslation = new HashMap<>(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/CacheMode.java b/liquidjava-verifier/src/main/java/liquidjava/utils/CacheMode.java index c7d49b03a..779e647cc 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/CacheMode.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/CacheMode.java @@ -3,26 +3,16 @@ import java.util.Locale; /** - * How the caches that reuse solver results across verification runs behave, set with the system property - * {@value #PROPERTY}: {@code on} (the default), {@code off}, or {@code check}, which recomputes every result found in a - * cache and fails if it differs, to test that the caches never change what the verifier reports + * 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.caches"; + public static final String PROPERTY = "liquidjava.cache"; public static CacheMode current() { return valueOf(System.getProperty(PROPERTY, "on").toUpperCase(Locale.ROOT)); } - - /** - * Fails when a cached result differs from the recomputed one. An {@link AssertionError}, so that code that recovers - * from exceptions cannot hide it - */ - public static void checkSame(String cache, Object cached, Object recomputed) { - if (!cached.equals(recomputed)) - throw new AssertionError( - String.format("The %s cache returned %s but recomputing gives %s", cache, cached, recomputed)); - } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestQueryCache.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestQueryCache.java index 5bb3eb325..3c5f19a20 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestQueryCache.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestQueryCache.java @@ -14,6 +14,8 @@ 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; /** @@ -96,9 +98,32 @@ public static void main(String[] args) { } """; + 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)"), @@ -124,18 +149,29 @@ void constantsOfAnEnum() throws IOException { @Test void typeOfAGhost() throws IOException { - assertSameAsUncachedAfterEdit(String.format(BOX, "int"), String.format(BOX, "long")); + // 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);