From fcaa941b140bad10b3af753d82e9ba6e172582df Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 18 Feb 2026 18:49:56 +0000 Subject: [PATCH 01/20] 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/20] 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/20] 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/20] 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/20] 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/20] 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/20] 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/20] 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/20] 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/20] 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/20] 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/20] 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 From 73b79ac4fbee9abe0ca89902d37d96b97070fdae Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 7 Mar 2026 12:53:58 +0000 Subject: [PATCH 13/20] Fix Scope Position --- .../java/liquidjava/processor/context/ContextHistory.java | 4 ++-- 1 file changed, 2 insertions(+), 2 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 2ea6444b..0aa1a9a7 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java @@ -79,8 +79,8 @@ public String getScopePosition(CtElement element) { CtElement startElement = element instanceof CtParameter ? element.getParent() : element; 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()); + return String.format("%d:%d-%d:%d", annPosition.getLine() - 1, annPosition.getColumn() - 1, + pos.getEndLine() - 1, pos.getEndColumn() - 1); } public Map>> getFileScopeVars() { From d05f418a1d98e0cd73b3b68bc2e765231c393bbb Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 6 Mar 2026 15:05:57 +0000 Subject: [PATCH 14/20] Remove Error Position --- .../liquidjava/diagnostics/ErrorPosition.java | 12 ----------- .../liquidjava/diagnostics/LJDiagnostic.java | 20 +++++++++---------- 2 files changed, 10 insertions(+), 22 deletions(-) delete mode 100644 liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorPosition.java diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorPosition.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorPosition.java deleted file mode 100644 index 3383f6bf..00000000 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorPosition.java +++ /dev/null @@ -1,12 +0,0 @@ -package liquidjava.diagnostics; - -import spoon.reflect.cu.SourcePosition; - -public record ErrorPosition(int lineStart, int colStart, int lineEnd, int colEnd) { - - public static ErrorPosition fromSpoonPosition(SourcePosition pos) { - if (pos == null || !pos.isValidPosition()) - return null; - return new ErrorPosition(pos.getLine(), pos.getColumn(), pos.getEndLine(), pos.getEndColumn()); - } -} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java index d1a743dc..affc6ae9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java @@ -13,14 +13,14 @@ public class LJDiagnostic extends RuntimeException { private final String accentColor; private final String customMessage; private String file; - private ErrorPosition position; + private SourcePosition position; private static final String PIPE = " | "; public LJDiagnostic(String title, String message, SourcePosition pos, String accentColor, String customMessage) { this.title = title; this.message = message; this.file = (pos != null && pos.getFile() != null) ? pos.getFile().getPath() : null; - this.position = ErrorPosition.fromSpoonPosition(pos); + this.position = pos; this.accentColor = accentColor; this.customMessage = customMessage; } @@ -41,14 +41,14 @@ public String getDetails() { return ""; // to be overridden by subclasses } - public ErrorPosition getPosition() { + public SourcePosition getPosition() { return position; } public void setPosition(SourcePosition pos) { if (pos == null) return; - this.position = ErrorPosition.fromSpoonPosition(pos); + this.position = pos; this.file = pos.getFile().getPath(); } @@ -82,7 +82,7 @@ public String toString() { // location if (file != null && position != null) { - sb.append("\n").append(file).append(":").append(position.lineStart()).append(Colors.RESET).append("\n"); + sb.append("\n").append(file).append(":").append(position.getLine()).append(Colors.RESET).append("\n"); } return sb.toString(); @@ -100,8 +100,8 @@ public String getSnippet() { // before and after lines for context int contextBefore = 2; int contextAfter = 2; - int startLine = Math.max(1, position.lineStart() - contextBefore); - int endLine = Math.min(lines.size(), position.lineEnd() + contextAfter); + int startLine = Math.max(1, position.getLine() - contextBefore); + int endLine = Math.min(lines.size(), position.getEndLine() + contextAfter); // calculate padding for line numbers int padding = String.valueOf(endLine).length(); @@ -115,9 +115,9 @@ public String getSnippet() { sb.append(Colors.GREY).append(lineNumStr).append(PIPE).append(line).append(Colors.RESET).append("\n"); // add error markers on the line(s) with the error - if (i >= position.lineStart() && i <= position.lineEnd()) { - int colStart = (i == position.lineStart()) ? position.colStart() : 1; - int colEnd = (i == position.lineEnd()) ? position.colEnd() : rawLine.length(); + if (i >= position.getLine() && i <= position.getEndLine()) { + int colStart = (i == position.getLine()) ? position.getColumn() : 1; + int colEnd = (i == position.getEndLine()) ? position.getEndColumn() : rawLine.length(); if (colStart > 0 && colEnd > 0) { int tabsBeforeStart = (int) rawLine.substring(0, Math.max(0, colStart - 1)).chars() From 4f0272b8ffe5dfc2765071a4c939b7464965e183 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 9 Mar 2026 11:51:25 +0000 Subject: [PATCH 15/20] Add File to GhostState --- .../processor/context/ContextHistory.java | 29 ++++--------------- .../processor/context/GhostState.java | 9 +++++- .../ExternalRefinementTypeChecker.java | 3 -- .../refinement_checker/TypeChecker.java | 6 ++-- .../src/main/java/liquidjava/utils/Utils.java | 8 +++++ 5 files changed, 24 insertions(+), 31 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 0aa1a9a7..53a78a1a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java @@ -14,9 +14,7 @@ public class ContextHistory { private static ContextHistory instance; private Map>> fileScopeVars; // file -> (scope -> variables in scope) - private Map> ghosts; // file -> ghosts - - // globals + private Set ghosts; private Set aliases; private Set instanceVars; private Set globalVars; @@ -25,7 +23,7 @@ private ContextHistory() { fileScopeVars = new HashMap<>(); instanceVars = new HashSet<>(); globalVars = new HashSet<>(); - ghosts = new HashMap<>(); + ghosts = new HashSet<>(); aliases = new HashSet<>(); } @@ -44,7 +42,7 @@ public void clearHistory() { } public void saveContext(CtElement element, Context context) { - String file = getFile(element); + String file = Utils.getFile(element); if (file == null) return; @@ -56,26 +54,11 @@ public void saveContext(CtElement element, Context 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) { + private String getScopePosition(CtElement element) { CtElement startElement = element instanceof CtParameter ? element.getParent() : element; SourcePosition annPosition = Utils.getFirstLJAnnotationPosition(startElement); SourcePosition pos = element.getPosition(); @@ -95,7 +78,7 @@ public Set getGlobalVars() { return globalVars; } - public Map> getGhosts() { + public Set getGhosts() { return ghosts; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostState.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostState.java index 121f0339..bbc51f73 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostState.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostState.java @@ -8,9 +8,12 @@ public class GhostState extends GhostFunction { private GhostFunction parent; private Predicate refinement; + private final String file; - public GhostState(String name, List> list, CtTypeReference returnType, String prefix) { + public GhostState(String name, List> list, CtTypeReference returnType, String prefix, + String file) { super(name, list, returnType, prefix); + this.file = file; } public void setGhostParent(GhostFunction parent) { @@ -28,4 +31,8 @@ public GhostFunction getParent() { public Predicate getRefinement() { return refinement; } + + public String getFile() { + return file; + } } 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 87384e44..20c6079f 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,12 +8,10 @@ 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; import liquidjava.rj_language.Predicate; -import liquidjava.rj_language.parsing.RefinementsParser; import liquidjava.utils.Utils; import spoon.reflect.code.CtLiteral; import spoon.reflect.cu.SourcePosition; @@ -31,7 +29,6 @@ public class ExternalRefinementTypeChecker extends TypeChecker { 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 296e4334..060034f3 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 @@ -154,12 +154,11 @@ private void createStateSet(CtNewArray e, int set, CtElement element) th CtLiteral s = (CtLiteral) ce; String f = s.getValue(); GhostState gs = new GhostState(f, g.getParametersTypes(), factory.Type().BOOLEAN_PRIMITIVE, - g.getPrefix()); + g.getPrefix(), Utils.getFile(element)); gs.setGhostParent(g); 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++; } @@ -192,9 +191,8 @@ private void createStateGhost(String string, CtElement element, SourcePosition p List> param = Collections.singletonList(factory.Type().createReference(qn)); CtTypeReference r = factory.Type().createReference(gd.returnType()); - GhostState gs = new GhostState(gd.name(), param, r, qn); + GhostState gs = new GhostState(gd.name(), param, r, qn, Utils.getFile(element)); context.addToGhostClass(sn, gs); - contextHistory.saveGhost(element, gs); } protected String getQualifiedClassName(CtElement element) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index 3119151f..82d37107 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -38,6 +38,14 @@ public static String qualifyName(String prefix, String name) { return String.format("%s.%s", prefix, name); } + public static String getFile(CtElement element) { + SourcePosition pos = element.getPosition(); + if (pos == null || pos.getFile() == null) + return null; + + return pos.getFile().getAbsolutePath(); + } + public static SourcePosition getLJAnnotationPosition(CtElement element, String refinement) { return element.getAnnotations().stream() .filter(a -> isLiquidJavaAnnotation(a) && hasRefinementValue(a, "\"" + refinement + "\"")).findFirst() From 1d7b0c65a2934fca5819d7c13f919c199695a772 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 9 Mar 2026 12:01:40 +0000 Subject: [PATCH 16/20] Add Variable Instance Regardless of Matching State This is because we want to show the failed variable instance in the context debugger and otherwise it is never added to the context. Not sure if this change is correct. --- .../refinement_checker/object_checkers/AuxStateHandler.java | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) 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 cb70c2e9..3bcf5732 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 @@ -482,7 +482,7 @@ private static void changeState(TypeChecker tc, VariableInstance vi, List Date: Mon, 9 Mar 2026 13:23:10 +0000 Subject: [PATCH 17/20] Minor Change --- .../refinement_checker/object_checkers/AuxStateHandler.java | 2 -- 1 file changed, 2 deletions(-) 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 3bcf5732..c01e1588 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 @@ -492,8 +492,6 @@ private static void changeState(TypeChecker tc, VariableInstance vi, List Date: Mon, 9 Mar 2026 14:15:12 +0000 Subject: [PATCH 18/20] Substitute `this` in `expectedStatesDisjunction` --- .../object_checkers/AuxStateHandler.java | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) 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 c01e1588..bd35a3ee 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 @@ -417,7 +417,7 @@ public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) throws L .changeOldMentions(vi.getName(), instanceName); if (!tc.checkStateSMT(prevState, expectState, fw.getPosition())) { // Invalid field transition - tc.throwStateRefinementError(fw.getPosition(), prevState, stateChange.getFrom(), stateChange.getMessage()); + tc.throwStateRefinementError(fw.getPosition(), prevState, expectState, stateChange.getMessage()); return; } @@ -465,6 +465,7 @@ private static void changeState(TypeChecker tc, VariableInstance vi, List Date: Mon, 9 Mar 2026 14:58:19 +0000 Subject: [PATCH 19/20] Remove Unused Imports --- .../liquidjava/processor/refinement_checker/TypeChecker.java | 2 -- .../src/main/java/liquidjava/rj_language/Predicate.java | 2 -- .../src/main/java/liquidjava/smt/TranslatorToZ3.java | 1 - 3 files changed, 5 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 060034f3..a91a4cb2 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,7 +9,6 @@ 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; @@ -41,7 +40,6 @@ 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; 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 f6931b52..c91380ee 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -6,9 +6,7 @@ import java.util.Map; import java.util.stream.Collectors; -import liquidjava.diagnostics.errors.ArgumentMismatchError; import liquidjava.diagnostics.errors.LJError; -import liquidjava.diagnostics.errors.SyntaxError; import liquidjava.processor.context.AliasWrapper; import liquidjava.processor.context.Context; import liquidjava.processor.context.GhostFunction; diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java index 96f32f66..ef50bf7c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java @@ -6,7 +6,6 @@ import com.microsoft.z3.Expr; import com.microsoft.z3.FPExpr; import com.microsoft.z3.FuncDecl; -import com.microsoft.z3.FuncInterp; import com.microsoft.z3.IntExpr; import com.microsoft.z3.IntNum; import com.microsoft.z3.RealExpr; From 6b0574c4914d772226af7a5f21edd7386b4ce509 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 9 Mar 2026 16:13:23 +0000 Subject: [PATCH 20/20] Save Scopes by File --- .../processor/context/ContextHistory.java | 39 ++++++++++--------- 1 file changed, 20 insertions(+), 19 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 53a78a1a..cdd02ddf 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java @@ -13,15 +13,15 @@ public class ContextHistory { private static ContextHistory instance; - private Map>> fileScopeVars; // file -> (scope -> variables in scope) + private Map> fileScopes; + private Set localVars; private Set ghosts; private Set aliases; - private Set instanceVars; private Set globalVars; private ContextHistory() { - fileScopeVars = new HashMap<>(); - instanceVars = new HashSet<>(); + fileScopes = new HashMap<>(); + localVars = new HashSet<>(); globalVars = new HashSet<>(); ghosts = new HashSet<>(); aliases = new HashSet<>(); @@ -34,8 +34,8 @@ public static ContextHistory getInstance() { } public void clearHistory() { - fileScopeVars.clear(); - instanceVars.clear(); + fileScopes.clear(); + localVars.clear(); globalVars.clear(); ghosts.clear(); aliases.clear(); @@ -46,13 +46,14 @@ public void saveContext(CtElement element, Context context) { if (file == null) return; - // add variables in scope + // add scope String scope = getScopePosition(element); - fileScopeVars.putIfAbsent(file, new HashMap<>()); - fileScopeVars.get(file).put(scope, new HashSet<>(context.getCtxVars())); + fileScopes.putIfAbsent(file, new HashSet<>()); + fileScopes.get(file).add(scope); - // add other elements in context (except ghosts) - instanceVars.addAll(context.getCtxInstanceVars()); + // add variables, ghosts and aliases + localVars.addAll(context.getCtxVars()); + localVars.addAll(context.getCtxInstanceVars()); globalVars.addAll(context.getCtxGlobalVars()); ghosts.addAll(context.getGhostStates()); aliases.addAll(context.getAliases()); @@ -62,16 +63,12 @@ private String getScopePosition(CtElement element) { CtElement startElement = element instanceof CtParameter ? element.getParent() : element; SourcePosition annPosition = Utils.getFirstLJAnnotationPosition(startElement); SourcePosition pos = element.getPosition(); - return String.format("%d:%d-%d:%d", annPosition.getLine() - 1, annPosition.getColumn() - 1, - pos.getEndLine() - 1, pos.getEndColumn() - 1); + return String.format("%d:%d-%d:%d", annPosition.getLine(), annPosition.getColumn(), pos.getEndLine(), + pos.getEndColumn()); } - public Map>> getFileScopeVars() { - return fileScopeVars; - } - - public Set getInstanceVars() { - return instanceVars; + public Set getLocalVars() { + return localVars; } public Set getGlobalVars() { @@ -85,4 +82,8 @@ public Set getGhosts() { public Set getAliases() { return aliases; } + + public Map> getFileScopes() { + return fileScopes; + } }