From f23b9963c8e043192ab635d21b2365705ed3a6d4 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 2 Apr 2026 16:24:16 +0100 Subject: [PATCH 1/2] Unsatisfiable Refinement Warning --- .../ErrorWarningUnsatRefinement.java | 28 +++++++++++++ .../warnings/UnsatRefinementWarning.java | 22 ++++++++++ .../refinement_checker/TypeChecker.java | 42 +++++++++++++++++++ .../java/liquidjava/smt/SMTEvaluator.java | 14 +++++++ .../test/java/liquidjava/utils/TestUtils.java | 2 +- 5 files changed, 107 insertions(+), 1 deletion(-) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorWarningUnsatRefinement.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/UnsatRefinementWarning.java diff --git a/liquidjava-example/src/main/java/testSuite/ErrorWarningUnsatRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorWarningUnsatRefinement.java new file mode 100644 index 00000000..9e8e3c86 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorWarningUnsatRefinement.java @@ -0,0 +1,28 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorWarningUnsatRefinement { + + public void example1() { + @Refinement("x == 0 && x != 0") // Unsat Refinement Warning + int x = 1; // Refinement Error + } + + public void example2() { + @Refinement("x % 2 > 1") // Unsat Refinement Warning + int x = 5; // Refinement Error + } + + public void example3() { + @Refinement("false") // Unsat Refinement Warning + int x = 0; // Refinement Error + } + + public void example(@Refinement("x > 0 && x < 0") int x) {} // Unsat Refinement Warning + + @Refinement("_ == true && _ == false") // Unsat Refinement Warning + public boolean example() { + return true; // Refinement Error + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/UnsatRefinementWarning.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/UnsatRefinementWarning.java new file mode 100644 index 00000000..6e6b8acf --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/UnsatRefinementWarning.java @@ -0,0 +1,22 @@ +package liquidjava.diagnostics.warnings; + +import spoon.reflect.cu.SourcePosition; + +/** + * Warning indicating that a refinement predicate is unsatisfiable + * + * @see LJWarning + */ +public class UnsatRefinementWarning extends LJWarning { + + private final String refinement; + + public UnsatRefinementWarning(SourcePosition position, String message, String refinement) { + super(message, position); + this.refinement = refinement; + } + + public String getRefinement() { + return refinement; + } +} 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 4cbbe5bf..1d9a8ecd 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 @@ -6,7 +6,9 @@ import java.util.Map; import java.util.Optional; +import liquidjava.diagnostics.Diagnostics; import liquidjava.diagnostics.errors.*; +import liquidjava.diagnostics.warnings.UnsatRefinementWarning; import liquidjava.processor.context.AliasWrapper; import liquidjava.processor.context.Context; import liquidjava.processor.context.GhostFunction; @@ -16,6 +18,7 @@ import liquidjava.processor.facade.GhostDTO; import liquidjava.rj_language.Predicate; import liquidjava.rj_language.parsing.RefinementsParser; +import liquidjava.smt.SMTEvaluator; import liquidjava.smt.SMTResult; import liquidjava.utils.Utils; import liquidjava.utils.constants.Formats; @@ -29,6 +32,9 @@ import spoon.reflect.declaration.CtClass; import spoon.reflect.declaration.CtElement; import spoon.reflect.declaration.CtInterface; +import spoon.reflect.declaration.CtMethod; +import spoon.reflect.declaration.CtTypedElement; +import spoon.reflect.declaration.CtVariable; import spoon.reflect.factory.Factory; import spoon.reflect.reference.CtTypeReference; import spoon.reflect.visitor.CtScanner; @@ -40,6 +46,7 @@ public abstract class TypeChecker extends CtScanner { protected final Context context; protected final Factory factory; protected final VCChecker vcChecker; + private final Diagnostics diagnostics = Diagnostics.getInstance(); public TypeChecker(Context context, Factory factory) { this.context = context; @@ -87,11 +94,46 @@ public Optional getRefinementFromAnnotation(CtElement element) throws throw new InvalidRefinementError(position, "Refinement predicate must be a boolean expression", ref.get()); } + checkRefinementSatisfiability(ref.get(), p, element); constr = Optional.of(p); } return constr; } + private void checkRefinementSatisfiability(String refinement, Predicate predicate, CtElement element) { + context.enterContext(); + try { + Predicate p = new Predicate(); + CtTypeReference annotationType = element instanceof CtTypedElement typedElement + ? typedElement.getType() : null; + if (annotationType != null && !context.hasVariable(Keys.WILDCARD)) + context.addVarToContext(Keys.WILDCARD, annotationType, p, element); + + if (element instanceof CtVariable variable && !context.hasVariable(variable.getSimpleName())) + context.addVarToContext(variable.getSimpleName(), variable.getType(), p, element); + + if (element instanceof CtMethod method && method.getType() != null && !context.hasVariable("return")) + context.addVarToContext("return", method.getType(), p, element); + + String qualifiedClassName = getQualifiedClassName(element); + if (qualifiedClassName != null && !context.hasVariable(Keys.THIS)) + context.addVarToContext(Keys.THIS, factory.Type().createReference(qualifiedClassName), p, element); + + Predicate refinementPredicate = predicate.changeStatesToRefinements(context.getGhostStates(), + new String[] { Keys.WILDCARD, Keys.THIS }); + refinementPredicate = refinementPredicate.changeAliasToRefinement(context, factory); + + if (new SMTEvaluator().isUnsatisfiable(refinementPredicate, context)) { + SourcePosition position = Utils.getLJAnnotationPosition(element, refinement); + diagnostics.add(new UnsatRefinementWarning(position, "This refinement can never be true", refinement)); + } + } catch (Exception e) { + // ignore + } finally { + context.exitContext(); + } + } + @SuppressWarnings({ "rawtypes" }) public Optional getMessageFromAnnotation(CtElement element) { for (CtAnnotation ann : element.getAnnotations()) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java index 096a9b95..8d1918e5 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java @@ -50,4 +50,18 @@ public SMTResult verifySubtype(Predicate subRef, Predicate supRef, Context conte } 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); + Solver solver = tz3.makeSolverForExpression(e); + return solver.check().equals(Status.UNSATISFIABLE); + } + } catch (Z3Exception e) { + throw new Z3Exception(e.getLocalizedMessage()); + } + } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java b/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java index 92883da0..35e1ead6 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java +++ b/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java @@ -34,7 +34,7 @@ public class TestUtils { * @param path */ public static boolean shouldPass(String path) { - return path.toLowerCase().contains("correct") || path.toLowerCase().contains("warning"); + return path.toLowerCase().contains("correct"); } /** From f9a30ff19a06d04dbc4d2aaaa6c5947b4dbccd75 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 2 Apr 2026 17:10:23 +0100 Subject: [PATCH 2/2] Cache Refinement Satisfiability Checks per Element --- .../main/java/testSuite/ErrorWarningUnsatRefinement.java | 6 +++--- .../processor/refinement_checker/TypeChecker.java | 4 +++- .../src/main/java/liquidjava/utils/constants/Keys.java | 1 + 3 files changed, 7 insertions(+), 4 deletions(-) diff --git a/liquidjava-example/src/main/java/testSuite/ErrorWarningUnsatRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorWarningUnsatRefinement.java index 9e8e3c86..98cd8092 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorWarningUnsatRefinement.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorWarningUnsatRefinement.java @@ -5,7 +5,7 @@ public class ErrorWarningUnsatRefinement { public void example1() { - @Refinement("x == 0 && x != 0") // Unsat Refinement Warning + @Refinement("x == 1 && x != 1") // Unsat Refinement Warning int x = 1; // Refinement Error } @@ -19,10 +19,10 @@ public void example3() { int x = 0; // Refinement Error } - public void example(@Refinement("x > 0 && x < 0") int x) {} // Unsat Refinement Warning + public void example4(@Refinement("x > 0 && x < 0") int x) {} // Unsat Refinement Warning @Refinement("_ == true && _ == false") // Unsat Refinement Warning - public boolean example() { + public boolean example5() { return true; // Refinement Error } } 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 1d9a8ecd..31c28d9b 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 @@ -94,7 +94,8 @@ public Optional getRefinementFromAnnotation(CtElement element) throws throw new InvalidRefinementError(position, "Refinement predicate must be a boolean expression", ref.get()); } - checkRefinementSatisfiability(ref.get(), p, element); + if (!Boolean.TRUE.equals(element.getMetadata(Keys.REFINEMENT_SAT_CHECK))) + checkRefinementSatisfiability(ref.get(), p, element); constr = Optional.of(p); } return constr; @@ -127,6 +128,7 @@ private void checkRefinementSatisfiability(String refinement, Predicate predicat SourcePosition position = Utils.getLJAnnotationPosition(element, refinement); diagnostics.add(new UnsatRefinementWarning(position, "This refinement can never be true", refinement)); } + element.putMetadata(Keys.REFINEMENT_SAT_CHECK, true); // for caching the satisfiability check result } catch (Exception e) { // ignore } finally { diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java index 93311c01..79b6efd0 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java @@ -2,6 +2,7 @@ public final class Keys { public static final String REFINEMENT = "refinement"; + public static final String REFINEMENT_SAT_CHECK = "refinement_sat_check"; public static final String TARGET = "target"; public static final String THIS = "this"; public static final String WILDCARD = "_";