From fcaa941b140bad10b3af753d82e9ba6e172582df Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 18 Feb 2026 18:49:56 +0000 Subject: [PATCH 01/12] Save Context History --- .../processor/context/ContextHistory.java | 35 +++++-------------- 1 file changed, 9 insertions(+), 26 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java index 0e4db162..70b5c4d1 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java @@ -7,19 +7,18 @@ import spoon.reflect.cu.SourcePosition; import spoon.reflect.declaration.CtElement; -import spoon.reflect.declaration.CtExecutable; public class ContextHistory { private static ContextHistory instance; - - private Map>> fileScopeVars; // file -> (scope -> variables in scope) + + private Map> vars; // scope -> variables in scope private Set instanceVars; private Set globalVars; private Set ghosts; private Set aliases; private ContextHistory() { - fileScopeVars = new HashMap<>(); + vars = new HashMap<>(); instanceVars = new HashSet<>(); globalVars = new HashSet<>(); ghosts = new HashSet<>(); @@ -33,7 +32,7 @@ public static ContextHistory getInstance() { } public void clearHistory() { - fileScopeVars.clear(); + vars.clear(); instanceVars.clear(); globalVars.clear(); ghosts.clear(); @@ -44,33 +43,17 @@ public void saveContext(CtElement element, Context context) { SourcePosition pos = element.getPosition(); if (pos == null || pos.getFile() == null) return; - - // add variables in scope for this position - String file = pos.getFile().getAbsolutePath(); - String scope = getScopePosition(element); - fileScopeVars.putIfAbsent(file, new HashMap<>()); - fileScopeVars.get(file).put(scope, new HashSet<>(context.getCtxVars())); - - // add other elements in context + + String scope = String.format("%s:%d:%d", pos.getFile().getName(), pos.getLine(), pos.getColumn()); + vars.put(scope, new HashSet<>(context.getCtxVars())); instanceVars.addAll(context.getCtxInstanceVars()); globalVars.addAll(context.getCtxGlobalVars()); ghosts.addAll(context.getGhostStates()); aliases.addAll(context.getAliases()); } - public String getScopePosition(CtElement element) { - SourcePosition pos = element.getPosition(); - SourcePosition innerPosition = pos; - if (element instanceof CtExecutable executable) { - if (executable.getBody() != null) - innerPosition = executable.getBody().getPosition(); - } - return String.format("%d:%d-%d:%d", innerPosition.getLine(), innerPosition.getColumn() + 1, pos.getEndLine(), - pos.getEndColumn()); - } - - public Map>> getFileScopeVars() { - return fileScopeVars; + public Map> getVars() { + return vars; } public Set getInstanceVars() { From a532c05a17806af02a41b8a421a9aaa414691414 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 19 Feb 2026 14:27:29 +0000 Subject: [PATCH 02/12] Save Context Vars by File and Scope --- .../processor/context/ContextHistory.java | 22 +++++++++++++++---- 1 file changed, 18 insertions(+), 4 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java index 70b5c4d1..df54651d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java @@ -7,11 +7,13 @@ import spoon.reflect.cu.SourcePosition; import spoon.reflect.declaration.CtElement; +import spoon.reflect.declaration.CtExecutable; +import spoon.reflect.declaration.CtMethod; public class ContextHistory { private static ContextHistory instance; - private Map> vars; // scope -> variables in scope + private Map>> vars; // file -> (scope -> variables in scope) private Set instanceVars; private Set globalVars; private Set ghosts; @@ -43,16 +45,28 @@ public void saveContext(CtElement element, Context context) { SourcePosition pos = element.getPosition(); if (pos == null || pos.getFile() == null) return; + + // add variables in scope for this position + String file = pos.getFile().getAbsolutePath(); + String scope = getScopePosition(element); + System.out.println("Saving context for " + file + " in scope " + scope); + vars.putIfAbsent(file, new HashMap<>()); + vars.get(file).put(scope, new HashSet<>(context.getCtxVars())); - String scope = String.format("%s:%d:%d", pos.getFile().getName(), pos.getLine(), pos.getColumn()); - vars.put(scope, new HashSet<>(context.getCtxVars())); + // add other elements in context instanceVars.addAll(context.getCtxInstanceVars()); globalVars.addAll(context.getCtxGlobalVars()); ghosts.addAll(context.getGhostStates()); aliases.addAll(context.getAliases()); } - public Map> getVars() { + public String getScopePosition(CtElement element) { + SourcePosition pos = element.getPosition(); + SourcePosition innerPosition = element instanceof CtExecutable ? ((CtExecutable) element).getBody().getPosition() : pos; + return String.format("%d:%d-%d:%d", innerPosition.getLine(), innerPosition.getColumn() + 1, pos.getEndLine(), pos.getEndColumn()); + } + + public Map>> getVars() { return vars; } From 07a4c631ae5d7340d7a47ecd2413a7ca985d4fc9 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 19 Feb 2026 15:48:25 +0000 Subject: [PATCH 03/12] Fix NPE --- .../processor/context/ContextHistory.java | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java index df54651d..b3670130 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java @@ -8,11 +8,10 @@ import spoon.reflect.cu.SourcePosition; import spoon.reflect.declaration.CtElement; import spoon.reflect.declaration.CtExecutable; -import spoon.reflect.declaration.CtMethod; public class ContextHistory { private static ContextHistory instance; - + private Map>> vars; // file -> (scope -> variables in scope) private Set instanceVars; private Set globalVars; @@ -49,10 +48,9 @@ public void saveContext(CtElement element, Context context) { // add variables in scope for this position String file = pos.getFile().getAbsolutePath(); String scope = getScopePosition(element); - System.out.println("Saving context for " + file + " in scope " + scope); vars.putIfAbsent(file, new HashMap<>()); vars.get(file).put(scope, new HashSet<>(context.getCtxVars())); - + // add other elements in context instanceVars.addAll(context.getCtxInstanceVars()); globalVars.addAll(context.getCtxGlobalVars()); @@ -62,8 +60,13 @@ public void saveContext(CtElement element, Context context) { public String getScopePosition(CtElement element) { SourcePosition pos = element.getPosition(); - SourcePosition innerPosition = element instanceof CtExecutable ? ((CtExecutable) element).getBody().getPosition() : pos; - return String.format("%d:%d-%d:%d", innerPosition.getLine(), innerPosition.getColumn() + 1, pos.getEndLine(), pos.getEndColumn()); + SourcePosition innerPosition = pos; + if (element instanceof CtExecutable executable) { + if (executable.getBody() != null) + innerPosition = executable.getBody().getPosition(); + } + return String.format("%d:%d-%d:%d", innerPosition.getLine(), innerPosition.getColumn() + 1, pos.getEndLine(), + pos.getEndColumn()); } public Map>> getVars() { From dd127c687615fcebd7d63c141e90644018bf4ece Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 20 Feb 2026 19:08:53 +0000 Subject: [PATCH 04/12] Save Ghosts By File --- .../processor/context/ContextHistory.java | 36 +++++++++++++------ .../ExternalRefinementTypeChecker.java | 6 ++-- .../refinement_checker/TypeChecker.java | 4 +++ 3 files changed, 34 insertions(+), 12 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java index b3670130..b16f3ef2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java @@ -13,16 +13,18 @@ public class ContextHistory { private static ContextHistory instance; private Map>> vars; // file -> (scope -> variables in scope) + private Map> ghosts; // file -> ghosts + + // globals + private Set aliases; private Set instanceVars; private Set globalVars; - private Set ghosts; - private Set aliases; private ContextHistory() { vars = new HashMap<>(); instanceVars = new HashSet<>(); globalVars = new HashSet<>(); - ghosts = new HashSet<>(); + ghosts = new HashMap<>(); aliases = new HashSet<>(); } @@ -41,23 +43,37 @@ public void clearHistory() { } public void saveContext(CtElement element, Context context) { - SourcePosition pos = element.getPosition(); - if (pos == null || pos.getFile() == null) + String file = getFile(element); + if (file == null) return; - // add variables in scope for this position - String file = pos.getFile().getAbsolutePath(); + // add variables in scope String scope = getScopePosition(element); vars.putIfAbsent(file, new HashMap<>()); vars.get(file).put(scope, new HashSet<>(context.getCtxVars())); - // add other elements in context + // add other elements in context (except ghosts) instanceVars.addAll(context.getCtxInstanceVars()); globalVars.addAll(context.getCtxGlobalVars()); - ghosts.addAll(context.getGhostStates()); aliases.addAll(context.getAliases()); } + public void saveGhost(CtElement element, GhostState ghost) { + String file = getFile(element); + if (file == null) + return; + ghosts.putIfAbsent(file, new HashSet<>()); + ghosts.get(file).add(ghost); + } + + private String getFile(CtElement element) { + SourcePosition pos = element.getPosition(); + if (pos == null || pos.getFile() == null) + return null; + + return pos.getFile().getAbsolutePath(); + } + public String getScopePosition(CtElement element) { SourcePosition pos = element.getPosition(); SourcePosition innerPosition = pos; @@ -81,7 +97,7 @@ public Set getGlobalVars() { return globalVars; } - public Set getGhosts() { + public Map> getGhosts() { return ghosts; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java index 154e94d0..aea227bf 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java @@ -8,6 +8,7 @@ import liquidjava.diagnostics.warnings.ExternalClassNotFoundWarning; import liquidjava.diagnostics.warnings.ExternalMethodNotFoundWarning; import liquidjava.processor.context.Context; +import liquidjava.processor.context.ContextHistory; import liquidjava.processor.context.GhostFunction; import liquidjava.processor.facade.GhostDTO; import liquidjava.processor.refinement_checker.general_checkers.MethodsFunctionsChecker; @@ -27,8 +28,9 @@ import spoon.reflect.reference.CtTypeReference; public class ExternalRefinementTypeChecker extends TypeChecker { - String prefix; - Diagnostics diagnostics = Diagnostics.getInstance(); + private String prefix; + private final Diagnostics diagnostics = Diagnostics.getInstance(); + private final ContextHistory contextHistory = ContextHistory.getInstance(); public ExternalRefinementTypeChecker(Context context, Factory factory) { super(context, factory); 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 ac2abb2d..17baf88a 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 @@ -9,6 +9,7 @@ import liquidjava.diagnostics.errors.*; import liquidjava.processor.context.AliasWrapper; import liquidjava.processor.context.Context; +import liquidjava.processor.context.ContextHistory; import liquidjava.processor.context.GhostFunction; import liquidjava.processor.context.GhostState; import liquidjava.processor.context.RefinedVariable; @@ -40,6 +41,7 @@ public abstract class TypeChecker extends CtScanner { protected final Context context; protected final Factory factory; protected final VCChecker vcChecker; + private final ContextHistory contextHistory = ContextHistory.getInstance(); public TypeChecker(Context context, Factory factory) { this.context = context; @@ -158,6 +160,7 @@ private void createStateSet(CtNewArray e, int set, CtElement element) th gs.setRefinement(Predicate.createEquals(ip, Predicate.createLit(Integer.toString(order), Types.INT))); // open(THIS) -> state1(THIS) == 1 context.addToGhostClass(g.getParentClassName(), gs); + contextHistory.saveGhost(element, gs); } order++; } @@ -183,6 +186,7 @@ private void createStateGhost(String string, CtAnnotation CtTypeReference r = factory.Type().createReference(gd.returnType()); GhostState gs = new GhostState(gd.name(), param, r, qn); context.addToGhostClass(sn, gs); + contextHistory.saveGhost(element, gs); } protected String getQualifiedClassName(CtElement element) { From eff70674c1f6600ea2081349adf2be789755f429 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 24 Feb 2026 13:27:04 +0000 Subject: [PATCH 05/12] Use Annotation Position & Mark Parameters This is needed to suggest parameters in method and parameter refinements --- .../main/java/liquidjava/diagnostics/LJDiagnostic.java | 2 +- .../liquidjava/processor/context/ContextHistory.java | 9 +++------ .../liquidjava/processor/context/RefinedVariable.java | 10 ++++++++++ .../general_checkers/MethodsFunctionsChecker.java | 1 + .../src/main/java/liquidjava/utils/Utils.java | 10 ++++++++++ 5 files changed, 25 insertions(+), 7 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java index 1c548648..d1a743dc 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java @@ -129,7 +129,7 @@ public String getSnippet() { // line number padding + pipe + column offset String indent = " ".repeat(padding) + Colors.GREY + PIPE + Colors.RESET - + " ".repeat(visualColStart - 1); + + " ".repeat(visualColStart - 1); String markers = accentColor + "^".repeat(Math.max(1, visualColEnd - visualColStart + 1)); sb.append(indent).append(markers); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java index b16f3ef2..597c647e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java @@ -5,6 +5,7 @@ import java.util.Map; import java.util.Set; +import liquidjava.utils.Utils; import spoon.reflect.cu.SourcePosition; import spoon.reflect.declaration.CtElement; import spoon.reflect.declaration.CtExecutable; @@ -76,12 +77,8 @@ private String getFile(CtElement element) { public String getScopePosition(CtElement element) { SourcePosition pos = element.getPosition(); - SourcePosition innerPosition = pos; - if (element instanceof CtExecutable executable) { - if (executable.getBody() != null) - innerPosition = executable.getBody().getPosition(); - } - return String.format("%d:%d-%d:%d", innerPosition.getLine(), innerPosition.getColumn() + 1, pos.getEndLine(), + SourcePosition annPosition = Utils.getFirstAnnotationPosition(element); + return String.format("%d:%d-%d:%d", annPosition.getLine(), annPosition.getColumn() + 1, pos.getEndLine(), pos.getEndColumn()); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java index 534f8cfa..9f57bb6e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java @@ -9,10 +9,12 @@ public abstract class RefinedVariable extends Refined { private final List> supertypes; private PlacementInCode placementInCode; + private boolean isParameter; public RefinedVariable(String name, CtTypeReference type, Predicate c) { super(name, type, c); supertypes = new ArrayList<>(); + isParameter = false; } public abstract Predicate getMainRefinement(); @@ -65,4 +67,12 @@ public boolean equals(Object obj) { return supertypes.equals(other.supertypes); } } + + public void setIsParameter(boolean b) { + isParameter = b; + } + + public boolean isParameter() { + return isParameter; + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java index af16bf92..1f1decda 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java @@ -154,6 +154,7 @@ private Predicate handleFunctionRefinements(RefinedFunction f, CtElement method, c = oc.get().substituteVariable(Keys.WILDCARD, paramName); param.putMetadata(Keys.REFINEMENT, c); RefinedVariable v = rtc.getContext().addVarToContext(param.getSimpleName(), param.getType(), c, param); + v.setIsParameter(true); rtc.getMessageFromAnnotation(param).ifPresent(v::setMessage); if (v instanceof Variable) f.addArgRefinements((Variable) v); diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index 1e99e3f0..069e007f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -44,6 +44,16 @@ public static SourcePosition getAnnotationPosition(CtElement element, String ref .map(CtElement::getPosition).orElse(element.getPosition()); } + public static SourcePosition getFirstAnnotationPosition(CtElement element) { + CtElement target = element.getParent() != null ? element.getParent() : element; + return target.getAnnotations().stream().filter(Utils::isLiquidJavaAnnotation).map(CtElement::getPosition) + .min((p1, p2) -> { + if (p1.getLine() != p2.getLine()) + return Integer.compare(p1.getLine(), p2.getLine()); + return Integer.compare(p1.getColumn(), p2.getColumn()); + }).orElse(target.getPosition()); + } + private static boolean isLiquidJavaAnnotation(CtAnnotation annotation) { return annotation.getAnnotationType().getQualifiedName().startsWith("liquidjava.specification"); } From 8ee09ea0a4ea570fa2a41158cb3ad1fe1cf33d04 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 24 Feb 2026 14:30:29 +0000 Subject: [PATCH 06/12] Fix --- .../processor/context/ContextHistory.java | 4 +++- .../src/main/java/liquidjava/utils/Utils.java | 13 ++++++------- 2 files changed, 9 insertions(+), 8 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java index 597c647e..a28781e2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java @@ -9,6 +9,7 @@ import spoon.reflect.cu.SourcePosition; import spoon.reflect.declaration.CtElement; import spoon.reflect.declaration.CtExecutable; +import spoon.reflect.declaration.CtParameter; public class ContextHistory { private static ContextHistory instance; @@ -76,8 +77,9 @@ private String getFile(CtElement element) { } public String getScopePosition(CtElement element) { + CtElement startElement = element instanceof CtParameter ? element.getParent() : element; + SourcePosition annPosition = Utils.getFirstAnnotationPosition(startElement); SourcePosition pos = element.getPosition(); - SourcePosition annPosition = Utils.getFirstAnnotationPosition(element); return String.format("%d:%d-%d:%d", annPosition.getLine(), annPosition.getColumn() + 1, pos.getEndLine(), pos.getEndColumn()); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index 069e007f..e0b46507 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -45,13 +45,12 @@ public static SourcePosition getAnnotationPosition(CtElement element, String ref } public static SourcePosition getFirstAnnotationPosition(CtElement element) { - CtElement target = element.getParent() != null ? element.getParent() : element; - return target.getAnnotations().stream().filter(Utils::isLiquidJavaAnnotation).map(CtElement::getPosition) - .min((p1, p2) -> { - if (p1.getLine() != p2.getLine()) - return Integer.compare(p1.getLine(), p2.getLine()); - return Integer.compare(p1.getColumn(), p2.getColumn()); - }).orElse(target.getPosition()); + return element.getAnnotations().stream().filter(Utils::isLiquidJavaAnnotation).map(CtElement::getPosition) + .min((p1, p2) -> { + if (p1.getLine() != p2.getLine()) + return Integer.compare(p1.getLine(), p2.getLine()); + return Integer.compare(p1.getColumn(), p2.getColumn()); + }).orElse(element.getPosition()); } private static boolean isLiquidJavaAnnotation(CtAnnotation annotation) { From e74d105ce08c6b66ef953805390eab7abcce218f Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 26 Feb 2026 11:07:11 +0000 Subject: [PATCH 07/12] Rename `fileScopeVars` --- .../processor/context/ContextHistory.java | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java index a28781e2..f969ebe3 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java @@ -14,7 +14,7 @@ public class ContextHistory { private static ContextHistory instance; - private Map>> vars; // file -> (scope -> variables in scope) + private Map>> fileScopeVars; // file -> (scope -> variables in scope) private Map> ghosts; // file -> ghosts // globals @@ -23,7 +23,7 @@ public class ContextHistory { private Set globalVars; private ContextHistory() { - vars = new HashMap<>(); + fileScopeVars = new HashMap<>(); instanceVars = new HashSet<>(); globalVars = new HashSet<>(); ghosts = new HashMap<>(); @@ -37,7 +37,7 @@ public static ContextHistory getInstance() { } public void clearHistory() { - vars.clear(); + fileScopeVars.clear(); instanceVars.clear(); globalVars.clear(); ghosts.clear(); @@ -51,8 +51,8 @@ public void saveContext(CtElement element, Context context) { // add variables in scope String scope = getScopePosition(element); - vars.putIfAbsent(file, new HashMap<>()); - vars.get(file).put(scope, new HashSet<>(context.getCtxVars())); + fileScopeVars.putIfAbsent(file, new HashMap<>()); + fileScopeVars.get(file).put(scope, new HashSet<>(context.getCtxVars())); // add other elements in context (except ghosts) instanceVars.addAll(context.getCtxInstanceVars()); @@ -84,8 +84,8 @@ public String getScopePosition(CtElement element) { pos.getEndColumn()); } - public Map>> getVars() { - return vars; + public Map>> getFileScopeVars() { + return fileScopeVars; } public Set getInstanceVars() { From 642ba0e9dddf36cbb0c2a33efb55661471560fc6 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 28 Feb 2026 16:18:59 +0000 Subject: [PATCH 08/12] Store Refined Variable Annotation Position This is needed to use the annotation position to be able to suggested the variable we are refining in the autocomplete --- .../liquidjava/processor/context/Context.java | 14 +++++++------- .../processor/context/ContextHistory.java | 1 - .../processor/context/RefinedVariable.java | 17 +++++++++++++++-- 3 files changed, 22 insertions(+), 10 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java index 23176dfd..9ffed9c0 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java @@ -105,31 +105,31 @@ public void addVarToContext(RefinedVariable var) { } public RefinedVariable addVarToContext(String simpleName, CtTypeReference type, Predicate c, - CtElement placementInCode) { + CtElement element) { RefinedVariable vi = new Variable(simpleName, type, c); - vi.addPlacementInCode(PlacementInCode.createPlacement(placementInCode)); + vi.addPlacementInCode(element); vi.addSuperTypes(type.getSuperclass(), type.getSuperInterfaces()); addVarToContext(vi); return vi; } public RefinedVariable addInstanceToContext(String simpleName, CtTypeReference type, Predicate c, - CtElement placementInCode) { + CtElement element) { RefinedVariable vi = new VariableInstance(simpleName, type, c); - vi.addPlacementInCode(PlacementInCode.createPlacement(placementInCode)); + vi.addPlacementInCode(element); if (!ctxInstanceVars.contains(vi)) addInstanceVariable(vi); return vi; } public void addRefinementToVariableInContext(String name, CtTypeReference type, Predicate et, - CtElement placementInCode) { + CtElement element) { if (hasVariable(name)) { RefinedVariable vi = getVariableByName(name); vi.setRefinement(et); - vi.addPlacementInCode(PlacementInCode.createPlacement(placementInCode)); + vi.addPlacementInCode(element); } else { - addVarToContext(name, type, et, placementInCode); + addVarToContext(name, type, et, element); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java index f969ebe3..9adf7ea3 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java @@ -8,7 +8,6 @@ import liquidjava.utils.Utils; import spoon.reflect.cu.SourcePosition; import spoon.reflect.declaration.CtElement; -import spoon.reflect.declaration.CtExecutable; import spoon.reflect.declaration.CtParameter; public class ContextHistory { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java index 9f57bb6e..1bf06797 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java @@ -4,12 +4,16 @@ import java.util.List; import java.util.Set; import liquidjava.rj_language.Predicate; +import liquidjava.utils.Utils; +import spoon.reflect.cu.SourcePosition; +import spoon.reflect.declaration.CtElement; import spoon.reflect.reference.CtTypeReference; public abstract class RefinedVariable extends Refined { private final List> supertypes; private PlacementInCode placementInCode; private boolean isParameter; + private SourcePosition annPosition; public RefinedVariable(String name, CtTypeReference type, Predicate c) { super(name, type, c); @@ -36,14 +40,23 @@ public void addSuperTypes(CtTypeReference ts, Set> sts) { supertypes.add(ct); } - public void addPlacementInCode(PlacementInCode s) { - placementInCode = s; + public void addPlacementInCode(CtElement element) { + placementInCode = PlacementInCode.createPlacement(element); + annPosition = Utils.getFirstAnnotationPosition(element); + } + + public void addPlacementInCode(PlacementInCode placement) { + placementInCode = placement; } public PlacementInCode getPlacementInCode() { return placementInCode; } + public SourcePosition getAnnPosition() { + return annPosition; + } + @Override public int hashCode() { final int prime = 31; From 0f6d3548e00c5c7f9d2ec9fafa1ef6a54c7ff226 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 28 Feb 2026 18:50:10 +0000 Subject: [PATCH 09/12] Formatting --- .../src/main/java/liquidjava/processor/context/Context.java | 3 +-- .../java/liquidjava/processor/context/RefinedVariable.java | 2 +- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java index 9ffed9c0..c6e6fd46 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java @@ -104,8 +104,7 @@ public void addVarToContext(RefinedVariable var) { var.addSuperTypes(type.getSuperclass(), type.getSuperInterfaces()); } - public RefinedVariable addVarToContext(String simpleName, CtTypeReference type, Predicate c, - CtElement element) { + public RefinedVariable addVarToContext(String simpleName, CtTypeReference type, Predicate c, CtElement element) { RefinedVariable vi = new Variable(simpleName, type, c); vi.addPlacementInCode(element); vi.addSuperTypes(type.getSuperclass(), type.getSuperInterfaces()); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java index 1bf06797..117b8717 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java @@ -56,7 +56,7 @@ public PlacementInCode getPlacementInCode() { public SourcePosition getAnnPosition() { return annPosition; } - + @Override public int hashCode() { final int prime = 31; From eb535e7548908c10ec5d5a47b0f30a088bcdb027 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 28 Feb 2026 18:52:07 +0000 Subject: [PATCH 10/12] Renaming --- .../java/liquidjava/processor/context/ContextHistory.java | 2 +- .../java/liquidjava/processor/context/RefinedVariable.java | 2 +- .../liquidjava/processor/refinement_checker/TypeChecker.java | 2 +- .../src/main/java/liquidjava/rj_language/Predicate.java | 2 +- liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java | 4 ++-- 5 files changed, 6 insertions(+), 6 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java index 9adf7ea3..2ea6444b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java @@ -77,7 +77,7 @@ private String getFile(CtElement element) { public String getScopePosition(CtElement element) { CtElement startElement = element instanceof CtParameter ? element.getParent() : element; - SourcePosition annPosition = Utils.getFirstAnnotationPosition(startElement); + SourcePosition annPosition = Utils.getFirstLJAnnotationPosition(startElement); SourcePosition pos = element.getPosition(); return String.format("%d:%d-%d:%d", annPosition.getLine(), annPosition.getColumn() + 1, pos.getEndLine(), pos.getEndColumn()); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java index 117b8717..7a04abde 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java @@ -42,7 +42,7 @@ public void addSuperTypes(CtTypeReference ts, Set> sts) { public void addPlacementInCode(CtElement element) { placementInCode = PlacementInCode.createPlacement(element); - annPosition = Utils.getFirstAnnotationPosition(element); + annPosition = Utils.getFirstLJAnnotationPosition(element); } public void addPlacementInCode(PlacementInCode placement) { 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 17baf88a..776c402b 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 @@ -256,7 +256,7 @@ protected void handleAlias(String ref, CtElement element) throws LJError { } } catch (LJError e) { // add location info to error - SourcePosition pos = Utils.getAnnotationPosition(element, ref); + SourcePosition pos = Utils.getLJAnnotationPosition(element, ref); e.setPosition(pos); throw e; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java index cb3b0077..f6931b52 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -88,7 +88,7 @@ protected Expression parse(String ref, CtElement element) throws LJError { return RefinementsParser.createAST(ref, prefix); } catch (LJError e) { // add location info to error - SourcePosition pos = Utils.getAnnotationPosition(element, ref); + SourcePosition pos = Utils.getLJAnnotationPosition(element, ref); e.setPosition(pos); throw e; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index e0b46507..3119151f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -38,13 +38,13 @@ public static String qualifyName(String prefix, String name) { return String.format("%s.%s", prefix, name); } - public static SourcePosition getAnnotationPosition(CtElement element, String refinement) { + public static SourcePosition getLJAnnotationPosition(CtElement element, String refinement) { return element.getAnnotations().stream() .filter(a -> isLiquidJavaAnnotation(a) && hasRefinementValue(a, "\"" + refinement + "\"")).findFirst() .map(CtElement::getPosition).orElse(element.getPosition()); } - public static SourcePosition getFirstAnnotationPosition(CtElement element) { + public static SourcePosition getFirstLJAnnotationPosition(CtElement element) { return element.getAnnotations().stream().filter(Utils::isLiquidJavaAnnotation).map(CtElement::getPosition) .min((p1, p2) -> { if (p1.getLine() != p2.getLine()) From ea38850ba939632d4ddb7ddc6a52a4d4fc53611a Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 5 Mar 2026 13:18:17 +0000 Subject: [PATCH 11/12] Fix Merge --- .../liquidjava/processor/refinement_checker/TypeChecker.java | 2 +- .../refinement_checker/object_checkers/AuxStateHandler.java | 2 +- 2 files changed, 2 insertions(+), 2 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 461385bf..296e4334 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 @@ -83,7 +83,7 @@ public Optional getRefinementFromAnnotation(CtElement element) throws if (ref.isPresent()) { Predicate p = new Predicate(ref.get(), element); if (!p.getExpression().isBooleanExpression()) { - SourcePosition position = Utils.getAnnotationPosition(element, ref.get()); + SourcePosition position = Utils.getLJAnnotationPosition(element, ref.get()); throw new InvalidRefinementError(position, "Refinement predicate must be a boolean expression", ref.get()); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index 61e2592c..cb70c2e9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java @@ -209,7 +209,7 @@ private static Predicate createStatePredicate(String value, String targetClass, boolean isTo, String prefix) throws LJError { Predicate p = new Predicate(value, e, prefix); if (!p.getExpression().isBooleanExpression()) { - SourcePosition position = Utils.getAnnotationPosition(e, value); + SourcePosition position = Utils.getLJAnnotationPosition(e, value); throw new InvalidRefinementError(position, "State refinement transition must be a boolean expression", value); } From dd62da865c70ba722e603798006d2e70bb163ee4 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 5 Mar 2026 13:59:13 +0000 Subject: [PATCH 12/12] Release Needed to release this new version to release the extension. --- liquidjava-verifier/pom.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/liquidjava-verifier/pom.xml b/liquidjava-verifier/pom.xml index 07abf74f..caaa0692 100644 --- a/liquidjava-verifier/pom.xml +++ b/liquidjava-verifier/pom.xml @@ -11,7 +11,7 @@ io.github.liquid-java liquidjava-verifier - 0.0.14 + 0.0.15 liquidjava-verifier LiquidJava Verifier https://github.com/liquid-java/liquidjava