From 5de29e7f7561532208c3f5f89c3e7a463fff8f56 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 12 Feb 2026 17:39:50 +0000 Subject: [PATCH 1/5] Individual Refinement Satisfiability --- .../errors/UnsatisfiableRefinementError.java | 22 +++++++++ .../refinement_checker/TypeChecker.java | 47 +++++++++++++++++++ .../src/main/java/liquidjava/utils/Utils.java | 3 +- .../liquidjava/utils/constants/Formats.java | 1 + 4 files changed, 71 insertions(+), 2 deletions(-) create mode 100644 liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/UnsatisfiableRefinementError.java diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/UnsatisfiableRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/UnsatisfiableRefinementError.java new file mode 100644 index 00000000..301ba825 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/UnsatisfiableRefinementError.java @@ -0,0 +1,22 @@ +package liquidjava.diagnostics.errors; + +import spoon.reflect.cu.SourcePosition; + +/** + * Error indicating that a refinement is intrinsically unsatisfiable (e.g., x > 0 && x < 0) + * + * @see LJError + */ +public class UnsatisfiableRefinementError extends LJError { + + private final String refinement; + + public UnsatisfiableRefinementError(SourcePosition position, String refinement) { + super("Unsatisfiable Refinement", "This predicate can never be true", position, null); + 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 31c019bc..f3236d6b 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,6 +6,8 @@ import java.util.Map; import java.util.Optional; +import javax.xml.transform.Source; + import liquidjava.diagnostics.errors.*; import liquidjava.processor.context.AliasWrapper; import liquidjava.processor.context.Context; @@ -28,6 +30,8 @@ import spoon.reflect.declaration.CtClass; import spoon.reflect.declaration.CtElement; import spoon.reflect.declaration.CtInterface; +import spoon.reflect.declaration.CtNamedElement; +import spoon.reflect.declaration.CtTypedElement; import spoon.reflect.factory.Factory; import spoon.reflect.reference.CtTypeReference; import spoon.reflect.visitor.CtScanner; @@ -85,11 +89,54 @@ public Optional getRefinementFromAnnotation(CtElement element) throws throw new InvalidRefinementError(element.getPosition(), "Refinement predicate must be a boolean expression", ref.get()); } + checkRefinementSatisfiability(p, element, ref.get()); constr = Optional.of(p); } return constr; } + private void checkRefinementSatisfiability(Predicate refinement, CtElement element, String refinementString) + throws LJError { + if (refinement.isBooleanTrue()) { + return; + } + + context.enterContext(); + try { + Predicate pred = refinement.clone(); + CtTypeReference elementType = element instanceof CtTypedElement typedElement ? typedElement.getType() + : null; + if (elementType == null) + return; + + String oldName = element instanceof CtNamedElement named ? named.getSimpleName() : Keys.WILDCARD; + String newName = String.format(Formats.REF, context.getCounter()); + + // add var to context + context.addVarToContext(newName, elementType, new Predicate(), element); + pred = pred.substituteVariable(oldName, newName); + + // if the refinement contains variables that are not in context, skip satisfiability check (e.g., old, + // length) + if (pred.getVariableNames().stream().anyMatch(name -> !context.hasVariable(name))) + return; + + // check if false is a subtype of the refinement (the refinement is unsatisfiable) + Predicate falsePred = Predicate.createLit("false", Types.BOOLEAN); + boolean isUnsatisfiable = vcChecker.smtChecks(falsePred, pred, element.getPosition()); + if (isUnsatisfiable) { + SourcePosition pos = Utils.getAnnotationPosition(element, refinementString); + throw new UnsatisfiableRefinementError(pos, refinementString); + } + } catch (UnsatisfiableRefinementError e) { + throw e; + } catch (LJError e) { + // ignore other errors + } finally { + context.exitContext(); + } + } + @SuppressWarnings({ "rawtypes" }) public Optional getMessageFromAnnotation(CtElement element) { for (CtAnnotation ann : element.getAnnotations()) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index 1cf45bc7..1e99e3f0 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -50,7 +50,6 @@ private static boolean isLiquidJavaAnnotation(CtAnnotation annotation) { private static boolean hasRefinementValue(CtAnnotation annotation, String refinement) { Map values = annotation.getValues(); - return Stream.of("value", "to", "from") - .anyMatch(key -> refinement.equals(String.valueOf(values.get(key)))); + return Stream.of("value", "to", "from").anyMatch(key -> refinement.equals(String.valueOf(values.get(key)))); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java index f3ae77f0..cca9c146 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java @@ -5,4 +5,5 @@ public final class Formats { public static final String INSTANCE = "#%s_%d"; public static final String THIS = "this#%s"; public static final String RET = "#ret_%d"; + public static final String REF = "#ref_%d"; } \ No newline at end of file From a1df13baeaac5b052e229783d010727d412f977c Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 12 Feb 2026 18:13:35 +0000 Subject: [PATCH 2/5] Cache Refinement Satisfiability Results --- .../refinement_checker/TypeChecker.java | 39 +++++++++++++++---- 1 file changed, 32 insertions(+), 7 deletions(-) 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 f3236d6b..a26a836e 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 @@ -2,12 +2,12 @@ import java.lang.annotation.Annotation; import java.util.Collections; +import java.util.HashMap; +import java.util.HashSet; import java.util.List; import java.util.Map; import java.util.Optional; -import javax.xml.transform.Source; - import liquidjava.diagnostics.errors.*; import liquidjava.processor.context.AliasWrapper; import liquidjava.processor.context.Context; @@ -43,6 +43,7 @@ public abstract class TypeChecker extends CtScanner { protected final Context context; protected final Factory factory; protected final VCChecker vcChecker; + private final Map refinementSatisfiabilityCache = new HashMap<>(); public TypeChecker(Context context, Factory factory) { this.context = context; @@ -97,10 +98,25 @@ public Optional getRefinementFromAnnotation(CtElement element) throws private void checkRefinementSatisfiability(Predicate refinement, CtElement element, String refinementString) throws LJError { + + // skip if trivially true if (refinement.isBooleanTrue()) { return; } + // normalize refinement for caching x > 0 and y > 0 hit same cache + String pattern = getRefinementPattern(refinement); + + // if we already checked this refinement pattern, use cached result + if (refinementSatisfiabilityCache.containsKey(pattern)) { + boolean isSatisfiable = refinementSatisfiabilityCache.get(pattern); + if (!isSatisfiable) { + SourcePosition pos = Utils.getAnnotationPosition(element, refinementString); + throw new UnsatisfiableRefinementError(pos, refinementString); + } + return; // skip + } + context.enterContext(); try { Predicate pred = refinement.clone(); @@ -116,14 +132,10 @@ private void checkRefinementSatisfiability(Predicate refinement, CtElement eleme context.addVarToContext(newName, elementType, new Predicate(), element); pred = pred.substituteVariable(oldName, newName); - // if the refinement contains variables that are not in context, skip satisfiability check (e.g., old, - // length) - if (pred.getVariableNames().stream().anyMatch(name -> !context.hasVariable(name))) - return; - // check if false is a subtype of the refinement (the refinement is unsatisfiable) Predicate falsePred = Predicate.createLit("false", Types.BOOLEAN); boolean isUnsatisfiable = vcChecker.smtChecks(falsePred, pred, element.getPosition()); + refinementSatisfiabilityCache.put(pattern, !isUnsatisfiable); if (isUnsatisfiable) { SourcePosition pos = Utils.getAnnotationPosition(element, refinementString); throw new UnsatisfiableRefinementError(pos, refinementString); @@ -137,6 +149,19 @@ private void checkRefinementSatisfiability(Predicate refinement, CtElement eleme } } + private String getRefinementPattern(Predicate refinement) { + Predicate pattern = refinement.clone().substituteVariable(Keys.WILDCARD, "$"); + List varNames = pattern.getVariableNames(); + HashSet uniqueVars = new HashSet<>(); + uniqueVars.addAll(varNames); + int i = 1; + for (String var : uniqueVars) { + pattern = pattern.substituteVariable(var, "x" + i); + i++; + } + return pattern.toString(); + } + @SuppressWarnings({ "rawtypes" }) public Optional getMessageFromAnnotation(CtElement element) { for (CtAnnotation ann : element.getAnnotations()) { From 53968ac931c67f272209ddd9891b2bd90503a6ac Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 14 Feb 2026 16:36:40 +0000 Subject: [PATCH 3/5] Fixes --- .../refinement_checker/TypeChecker.java | 39 ++++++++----------- 1 file changed, 16 insertions(+), 23 deletions(-) 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 a26a836e..f6f94c13 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 @@ -96,15 +96,18 @@ public Optional getRefinementFromAnnotation(CtElement element) throws return constr; } - private void checkRefinementSatisfiability(Predicate refinement, CtElement element, String refinementString) + private void checkRefinementSatisfiability(Predicate predicate, CtElement element, String refinementString) throws LJError { // skip if trivially true - if (refinement.isBooleanTrue()) { + if (predicate.isBooleanTrue()) return; - } - // normalize refinement for caching x > 0 and y > 0 hit same cache + // replace _ with variable name + String name = element instanceof CtNamedElement named ? named.getSimpleName() : Keys.WILDCARD; + Predicate refinement = predicate.clone().substituteVariable(Keys.WILDCARD, name); + + // normalize refinement so that equivalent refinements hit the same cache entry String pattern = getRefinementPattern(refinement); // if we already checked this refinement pattern, use cached result @@ -114,49 +117,39 @@ private void checkRefinementSatisfiability(Predicate refinement, CtElement eleme SourcePosition pos = Utils.getAnnotationPosition(element, refinementString); throw new UnsatisfiableRefinementError(pos, refinementString); } - return; // skip + return; // skip check } + // check if false is a subtype of the refinement (the refinement is unsatisfiable) context.enterContext(); try { - Predicate pred = refinement.clone(); - CtTypeReference elementType = element instanceof CtTypedElement typedElement ? typedElement.getType() + CtTypeReference elementType = element instanceof CtTypedElement typedElement ? typedElement.getType() : null; - if (elementType == null) - return; - - String oldName = element instanceof CtNamedElement named ? named.getSimpleName() : Keys.WILDCARD; - String newName = String.format(Formats.REF, context.getCounter()); + if (elementType != null) + context.addVarToContext(name, elementType, new Predicate(), element); - // add var to context - context.addVarToContext(newName, elementType, new Predicate(), element); - pred = pred.substituteVariable(oldName, newName); - - // check if false is a subtype of the refinement (the refinement is unsatisfiable) Predicate falsePred = Predicate.createLit("false", Types.BOOLEAN); - boolean isUnsatisfiable = vcChecker.smtChecks(falsePred, pred, element.getPosition()); + boolean isUnsatisfiable = vcChecker.smtChecks(falsePred, refinement, element.getPosition()); refinementSatisfiabilityCache.put(pattern, !isUnsatisfiable); if (isUnsatisfiable) { SourcePosition pos = Utils.getAnnotationPosition(element, refinementString); throw new UnsatisfiableRefinementError(pos, refinementString); } - } catch (UnsatisfiableRefinementError e) { - throw e; } catch (LJError e) { - // ignore other errors + // ignore errors } finally { context.exitContext(); } } private String getRefinementPattern(Predicate refinement) { - Predicate pattern = refinement.clone().substituteVariable(Keys.WILDCARD, "$"); + Predicate pattern = refinement.clone(); List varNames = pattern.getVariableNames(); HashSet uniqueVars = new HashSet<>(); uniqueVars.addAll(varNames); int i = 1; for (String var : uniqueVars) { - pattern = pattern.substituteVariable(var, "x" + i); + pattern = pattern.substituteVariable(var, "#" + i); i++; } return pattern.toString(); From f09c4013e93e7d8973c1cd9231441e47d8fcef8e Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 14 Feb 2026 16:43:37 +0000 Subject: [PATCH 4/5] Remove Unsatisfiable Refinements Caching --- .../refinement_checker/TypeChecker.java | 40 +++---------------- 1 file changed, 5 insertions(+), 35 deletions(-) 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 f6f94c13..cba97194 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 @@ -2,8 +2,6 @@ import java.lang.annotation.Annotation; import java.util.Collections; -import java.util.HashMap; -import java.util.HashSet; import java.util.List; import java.util.Map; import java.util.Optional; @@ -43,7 +41,6 @@ public abstract class TypeChecker extends CtScanner { protected final Context context; protected final Factory factory; protected final VCChecker vcChecker; - private final Map refinementSatisfiabilityCache = new HashMap<>(); public TypeChecker(Context context, Factory factory) { this.context = context; @@ -103,26 +100,13 @@ private void checkRefinementSatisfiability(Predicate predicate, CtElement elemen if (predicate.isBooleanTrue()) return; - // replace _ with variable name - String name = element instanceof CtNamedElement named ? named.getSimpleName() : Keys.WILDCARD; - Predicate refinement = predicate.clone().substituteVariable(Keys.WILDCARD, name); - - // normalize refinement so that equivalent refinements hit the same cache entry - String pattern = getRefinementPattern(refinement); - - // if we already checked this refinement pattern, use cached result - if (refinementSatisfiabilityCache.containsKey(pattern)) { - boolean isSatisfiable = refinementSatisfiabilityCache.get(pattern); - if (!isSatisfiable) { - SourcePosition pos = Utils.getAnnotationPosition(element, refinementString); - throw new UnsatisfiableRefinementError(pos, refinementString); - } - return; // skip check - } - - // check if false is a subtype of the refinement (the refinement is unsatisfiable) context.enterContext(); try { + // replace _ with variable name + String name = element instanceof CtNamedElement named ? named.getSimpleName() : Keys.WILDCARD; + Predicate refinement = predicate.clone().substituteVariable(Keys.WILDCARD, name); + + // check if false is a subtype of the refinement (the refinement is unsatisfiable) CtTypeReference elementType = element instanceof CtTypedElement typedElement ? typedElement.getType() : null; if (elementType != null) @@ -130,7 +114,6 @@ private void checkRefinementSatisfiability(Predicate predicate, CtElement elemen Predicate falsePred = Predicate.createLit("false", Types.BOOLEAN); boolean isUnsatisfiable = vcChecker.smtChecks(falsePred, refinement, element.getPosition()); - refinementSatisfiabilityCache.put(pattern, !isUnsatisfiable); if (isUnsatisfiable) { SourcePosition pos = Utils.getAnnotationPosition(element, refinementString); throw new UnsatisfiableRefinementError(pos, refinementString); @@ -142,19 +125,6 @@ private void checkRefinementSatisfiability(Predicate predicate, CtElement elemen } } - private String getRefinementPattern(Predicate refinement) { - Predicate pattern = refinement.clone(); - List varNames = pattern.getVariableNames(); - HashSet uniqueVars = new HashSet<>(); - uniqueVars.addAll(varNames); - int i = 1; - for (String var : uniqueVars) { - pattern = pattern.substituteVariable(var, "#" + i); - i++; - } - return pattern.toString(); - } - @SuppressWarnings({ "rawtypes" }) public Optional getMessageFromAnnotation(CtElement element) { for (CtAnnotation ann : element.getAnnotations()) { From 015524c7f7a75b19a4907bb07d1f853e9f0d84c2 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 14 Feb 2026 16:52:20 +0000 Subject: [PATCH 5/5] Add Tests --- .../java/testSuite/ErrorUnsatisfiableRefinement.java | 12 ++++++++++++ .../ErrorUnsatisfiableRefinementParameter.java | 9 +++++++++ .../ErrorUnsatisfiableRefinementReturn.java | 11 +++++++++++ .../errors/UnsatisfiableRefinementError.java | 2 +- .../processor/refinement_checker/TypeChecker.java | 2 ++ 5 files changed, 35 insertions(+), 1 deletion(-) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorUnsatisfiableRefinement.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorUnsatisfiableRefinementParameter.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorUnsatisfiableRefinementReturn.java diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnsatisfiableRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorUnsatisfiableRefinement.java new file mode 100644 index 00000000..9d8bda0b --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorUnsatisfiableRefinement.java @@ -0,0 +1,12 @@ +// Unsatisfiable Refinement Error +package testSuite; + +import liquidjava.specification.Refinement; + +@SuppressWarnings("unused") +public class ErrorUnsatisfiableRefinement { + void test() { + @Refinement("_ > 0 && _ < 0") + int x = 5; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnsatisfiableRefinementParameter.java b/liquidjava-example/src/main/java/testSuite/ErrorUnsatisfiableRefinementParameter.java new file mode 100644 index 00000000..b4ffed8a --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorUnsatisfiableRefinementParameter.java @@ -0,0 +1,9 @@ +// Unsatisfiable Refinement Error +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorUnsatisfiableRefinementParameter { + + void test(@Refinement("x == 0 && x == 1") int x) {} +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnsatisfiableRefinementReturn.java b/liquidjava-example/src/main/java/testSuite/ErrorUnsatisfiableRefinementReturn.java new file mode 100644 index 00000000..022f1cf9 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorUnsatisfiableRefinementReturn.java @@ -0,0 +1,11 @@ +// Unsatisfiable Refinement Error +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorUnsatisfiableRefinementReturn { + @Refinement("_ % 2 == 3") + int test() { + return 1; + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/UnsatisfiableRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/UnsatisfiableRefinementError.java index 301ba825..431a82ec 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/UnsatisfiableRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/UnsatisfiableRefinementError.java @@ -12,7 +12,7 @@ public class UnsatisfiableRefinementError extends LJError { private final String refinement; public UnsatisfiableRefinementError(SourcePosition position, String refinement) { - super("Unsatisfiable Refinement", "This predicate can never be true", position, null); + super("Unsatisfiable Refinement Error", "This predicate can never be true", position, null); this.refinement = 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 cba97194..c9329f16 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 @@ -118,6 +118,8 @@ private void checkRefinementSatisfiability(Predicate predicate, CtElement elemen SourcePosition pos = Utils.getAnnotationPosition(element, refinementString); throw new UnsatisfiableRefinementError(pos, refinementString); } + } catch (UnsatisfiableRefinementError e) { + throw e; } catch (LJError e) { // ignore errors } finally {