From aa34a81833efcf1dfe2a9f61a10f39499b7cc7e7 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 18 Feb 2026 18:49:56 +0000 Subject: [PATCH 1/4] Save Context History --- ...java => ErrorInstanceVarInRefinement.java} | 2 +- ...va => ErrorInstanceVarInRefinementIf.java} | 2 +- .../liquidjava/api/CommandLineLauncher.java | 3 + .../liquidjava/processor/context/Context.java | 87 +++++++++++-------- .../processor/context/ContextHistory.java | 74 ++++++++++++++++ .../RefinementTypeChecker.java | 11 ++- .../refinement_checker/TypeChecker.java | 6 +- .../general_checkers/OperationsChecker.java | 2 +- .../liquidjava/rj_language/Predicate.java | 2 +- .../liquidjava/smt/TranslatorContextToZ3.java | 4 +- .../java/liquidjava/smt/TranslatorToZ3.java | 4 +- 11 files changed, 149 insertions(+), 48 deletions(-) rename liquidjava-example/src/main/java/testSuite/{ErrorSpecificVarInRefinement.java => ErrorInstanceVarInRefinement.java} (85%) rename liquidjava-example/src/main/java/testSuite/{ErrorSpecificVarInRefinementIf.java => ErrorInstanceVarInRefinementIf.java} (87%) create mode 100644 liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSpecificVarInRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorInstanceVarInRefinement.java similarity index 85% rename from liquidjava-example/src/main/java/testSuite/ErrorSpecificVarInRefinement.java rename to liquidjava-example/src/main/java/testSuite/ErrorInstanceVarInRefinement.java index ccb34136..5edd96d8 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorSpecificVarInRefinement.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorInstanceVarInRefinement.java @@ -4,7 +4,7 @@ import liquidjava.specification.Refinement; @SuppressWarnings("unused") -public class ErrorSpecificVarInRefinement { +public class ErrorInstanceVarInRefinement { public static void main(String[] args) { @Refinement("_ < 10") int a = 6; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSpecificVarInRefinementIf.java b/liquidjava-example/src/main/java/testSuite/ErrorInstanceVarInRefinementIf.java similarity index 87% rename from liquidjava-example/src/main/java/testSuite/ErrorSpecificVarInRefinementIf.java rename to liquidjava-example/src/main/java/testSuite/ErrorInstanceVarInRefinementIf.java index c00f5b90..f0a973fd 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorSpecificVarInRefinementIf.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorInstanceVarInRefinementIf.java @@ -4,7 +4,7 @@ import liquidjava.specification.Refinement; @SuppressWarnings("unused") -public class ErrorSpecificVarInRefinementIf { +public class ErrorInstanceVarInRefinementIf { public static void main(String[] args) { @Refinement("_ < 10") int a = 6; diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java index b664ced6..e473562c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java +++ b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java @@ -8,6 +8,7 @@ import liquidjava.diagnostics.errors.CustomError; import liquidjava.diagnostics.warnings.CustomWarning; import liquidjava.processor.RefinementProcessor; +import liquidjava.processor.context.ContextHistory; import spoon.Launcher; import spoon.compiler.Environment; import spoon.processing.ProcessingManager; @@ -18,6 +19,7 @@ public class CommandLineLauncher { private static final Diagnostics diagnostics = Diagnostics.getInstance(); + private static final ContextHistory contextHistory = ContextHistory.getInstance(); public static void main(String[] args) { if (args.length == 0) { @@ -46,6 +48,7 @@ public static void launch(String... paths) { System.out.println("Running LiquidJava on: " + Arrays.toString(paths).replaceAll("[\\[\\]]", "")); diagnostics.clear(); + contextHistory.clearHistory(); Launcher launcher = new Launcher(); for (String path : paths) { if (!new File(path).exists()) { 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 ca4d68e8..5743a3b3 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java @@ -8,27 +8,26 @@ public class Context { private Stack> ctxVars; private List ctxFunctions; - private List ctxSpecificVars; - + private List ctxInstanceVars; private final List ctxGlobalVars; private List ghosts; - private Map> classStates; - private List alias; + private Map> states; + private List aliases; - public int counter; + private int counter; private static Context instance; private Context() { ctxVars = new Stack<>(); ctxVars.add(new ArrayList<>()); ctxFunctions = new ArrayList<>(); - ctxSpecificVars = new ArrayList<>(); + ctxInstanceVars = new ArrayList<>(); ctxGlobalVars = new ArrayList<>(); - alias = new ArrayList<>(); + aliases = new ArrayList<>(); ghosts = new ArrayList<>(); - classStates = new HashMap<>(); + states = new HashMap<>(); counter = 0; } @@ -41,15 +40,15 @@ public static Context getInstance() { public void reinitializeContext() { ctxVars = new Stack<>(); ctxVars.add(new ArrayList<>()); // global vars - ctxSpecificVars = new ArrayList<>(); + ctxInstanceVars = new ArrayList<>(); } public void reinitializeAllContext() { reinitializeContext(); ctxFunctions = new ArrayList<>(); - alias = new ArrayList<>(); + aliases = new ArrayList<>(); ghosts = new ArrayList<>(); - classStates = new HashMap<>(); + states = new HashMap<>(); counter = 0; } @@ -80,7 +79,7 @@ public Map> getContext() { ret.put(var.getName(), var.getType()); } } - for (RefinedVariable var : ctxSpecificVars) + for (RefinedVariable var : ctxInstanceVars) ret.put(var.getName(), var.getType()); for (RefinedVariable var : ctxGlobalVars) ret.put(var.getName(), var.getType()); @@ -94,6 +93,10 @@ public void addGlobalVariableToContext(String simpleName, String location, CtTyp ctxGlobalVars.add(vi); } + public List getCtxGlobalVars() { + return ctxGlobalVars; + } + // ---------------------- Add variables and instances ---------------------- public void addVarToContext(RefinedVariable var) { ctxVars.peek().add(var); @@ -114,8 +117,8 @@ public RefinedVariable addInstanceToContext(String simpleName, CtTypeReference getAllVariablesWithSupertypes() { if (!rv.getSuperTypes().isEmpty()) lvi.add(rv); } - for (RefinedVariable rv : ctxSpecificVars) { + for (RefinedVariable rv : ctxInstanceVars) { if (!rv.getSuperTypes().isEmpty()) lvi.add(rv); } @@ -204,7 +207,7 @@ public void addRefinementInstanceToVariable(String name, String instanceName) { ((Variable) vi1).addInstance((VariableInstance) vi2); ((VariableInstance) vi2).setParent((Variable) vi1); - addSpecificVariable(vi2); + addInstanceVariable(vi2); } public Optional getLastVariableInstance(String name) { @@ -214,14 +217,30 @@ public Optional getLastVariableInstance(String name) { return ((Variable) rv).getLastInstance(); } - public void addSpecificVariable(RefinedVariable vi) { - if (!ctxSpecificVars.contains(vi)) { - ctxSpecificVars.add(vi); + public void addInstanceVariable(RefinedVariable vi) { + if (!ctxInstanceVars.contains(vi)) { + ctxInstanceVars.add(vi); CtTypeReference type = vi.getType(); vi.addSuperTypes(type.getSuperclass(), type.getSuperInterfaces()); } } + public Variable getVariableFromInstance(VariableInstance vi) { + return vi.getParent().orElse(null); + } + + public List getCtxVars() { + List lvi = new ArrayList<>(); + for (List l : ctxVars) { + lvi.addAll(l); + } + return lvi; + } + + public List getCtxInstanceVars() { + return ctxInstanceVars; + } + // ---------------------- Variables - if information storing ---------------------- public void variablesSetBeforeIf() { for (RefinedVariable vi : getAllVariables()) @@ -290,6 +309,10 @@ public List getAllMethodsWithNameSize(String name, int size) { return l; } + public List getCtxFunctions() { + return ctxFunctions; + } + // ---------------------- Ghost Predicates ---------------------- public void addGhostFunction(GhostFunction gh) { ghosts.add(gh); @@ -300,35 +323,35 @@ public List getGhosts() { } public void addGhostClass(String klass) { - if (!classStates.containsKey(klass)) - classStates.put(klass, new ArrayList<>()); + if (!states.containsKey(klass)) + states.put(klass, new ArrayList<>()); } public void addToGhostClass(String klass, GhostState gs) { - List l = classStates.get(klass); + List l = states.get(klass); if (!l.contains(gs)) l.add(gs); } public List getGhostState(String s) { - return classStates.get(s); + return states.get(s); } - public List getGhostState() { + public List getGhostStates() { List lgs = new ArrayList<>(); - for (List l : classStates.values()) + for (List l : states.values()) lgs.addAll(l); return lgs; } // ---------------------- Alias ---------------------- public void addAlias(AliasWrapper aw) { - if (!alias.contains(aw)) - alias.add(aw); + if (!aliases.contains(aw)) + aliases.add(aw); } - public List getAlias() { - return alias; + public List getAliases() { + return aliases; } @Override @@ -354,8 +377,4 @@ public String toString() { sb.append(f.toString()); return sb.toString(); } - - public Variable getVariableFromInstance(VariableInstance vi) { - return vi.getParent().orElse(null); - } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java new file mode 100644 index 00000000..70b5c4d1 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java @@ -0,0 +1,74 @@ +package liquidjava.processor.context; + +import java.util.HashMap; +import java.util.HashSet; +import java.util.Map; +import java.util.Set; + +import spoon.reflect.cu.SourcePosition; +import spoon.reflect.declaration.CtElement; + +public class ContextHistory { + private static ContextHistory instance; + + private Map> vars; // scope -> variables in scope + 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<>(); + aliases = new HashSet<>(); + } + + public static ContextHistory getInstance() { + if (instance == null) + instance = new ContextHistory(); + return instance; + } + + public void clearHistory() { + vars.clear(); + instanceVars.clear(); + globalVars.clear(); + ghosts.clear(); + aliases.clear(); + } + + public void saveContext(CtElement element, Context context) { + SourcePosition pos = element.getPosition(); + if (pos == null || pos.getFile() == null) + return; + + 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 Map> getVars() { + return vars; + } + + public Set getInstanceVars() { + return instanceVars; + } + + public Set getGlobalVars() { + return globalVars; + } + + public Set getGhosts() { + return ghosts; + } + + public Set getAliases() { + return aliases; + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index d4d6f89e..d3d95bbd 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -54,6 +54,7 @@ public class RefinementTypeChecker extends TypeChecker { OperationsChecker otc; MethodsFunctionsChecker mfc; Diagnostics diagnostics = Diagnostics.getInstance(); + ContextHistory contextHistory = ContextHistory.getInstance(); public RefinementTypeChecker(Context context, Factory factory) { super(context, factory); @@ -95,14 +96,15 @@ public void visitCtAnnotationType(CtAnnotationType ann } @Override - public void visitCtConstructor(CtConstructor c) { + public void visitCtConstructor(CtConstructor constructor) { context.enterContext(); - mfc.loadFunctionInfo(c); + mfc.loadFunctionInfo(constructor); try { - super.visitCtConstructor(c); + super.visitCtConstructor(constructor); } catch (LJError e) { diagnostics.add(e); } + contextHistory.saveContext(constructor, context); context.exitContext(); } @@ -116,6 +118,7 @@ public void visitCtMethod(CtMethod method) { } catch (LJError e) { diagnostics.add(e); } + contextHistory.saveContext(method, context); context.exitContext(); } @@ -334,6 +337,7 @@ public void visitCtIf(CtIf ifElement) { context.enterContext(); visitCtBlock(ifElement.getThenStatement()); context.variablesSetThenIf(); + contextHistory.saveContext(ifElement.getThenStatement(), context); context.exitContext(); // VISIT ELSE @@ -345,6 +349,7 @@ public void visitCtIf(CtIf ifElement) { context.enterContext(); visitCtBlock(ifElement.getElseStatement()); context.variablesSetElseIf(); + contextHistory.saveContext(ifElement.getElseStatement(), context); context.exitContext(); } // end diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java index 31c019bc..17e666df 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 @@ -303,17 +303,17 @@ public void checkSMT(Predicate expectedType, CtElement element) throws LJError { } public void checkSMT(Predicate expectedType, CtElement element, String customMessage) throws LJError { - vcChecker.processSubtyping(expectedType, context.getGhostState(), element, factory, customMessage); + vcChecker.processSubtyping(expectedType, context.getGhostStates(), element, factory, customMessage); element.putMetadata(Keys.REFINEMENT, expectedType); } public void checkStateSMT(Predicate prevState, Predicate expectedState, CtElement target, String moreInfo) throws LJError { - vcChecker.processSubtyping(prevState, expectedState, context.getGhostState(), target, factory); + vcChecker.processSubtyping(prevState, expectedState, context.getGhostStates(), target, factory); } public boolean checksStateSMT(Predicate prevState, Predicate expectedState, SourcePosition p) throws LJError { - return vcChecker.canProcessSubtyping(prevState, expectedState, context.getGhostState(), p, factory); + return vcChecker.canProcessSubtyping(prevState, expectedState, context.getGhostStates(), p, factory); } public void throwRefinementError(SourcePosition position, Predicate expectedType, Predicate foundType, diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java index 779d68a9..de64ceb1 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java @@ -197,7 +197,7 @@ private Predicate getOperationRefinements(CtBinaryOperator operator, CtVariab Predicate newElemRef = elemRef.substituteVariable(Keys.WILDCARD, newName); RefinedVariable newVi = rtc.getContext().addVarToContext(newName, elemVar.getType(), newElemRef, elemVar); - rtc.getContext().addSpecificVariable(newVi); + rtc.getContext().addInstanceVariable(newVi); returnName = newName; } 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 eecfaa10..4f0f2fbf 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -101,7 +101,7 @@ public Predicate changeAliasToRefinement(Context context, Factory f) throws LJEr Expression ref = getExpression(); Map alias = new HashMap<>(); - for (AliasWrapper aw : context.getAlias()) { + for (AliasWrapper aw : context.getAliases()) { alias.put(aw.getName(), aw.createAliasDTO()); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java index 08749a07..d14ffd0a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java @@ -51,8 +51,8 @@ private static Expr getExpr(Context z3, String name, CtTypeReference type) }; } - static void addAlias(List alias, Map aliasTranslation) { - for (AliasWrapper a : alias) { + static void addAliases(List aliases, Map aliasTranslation) { + for (AliasWrapper a : aliases) { aliasTranslation.put(a.getName(), a); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java index b207552f..77e37e26 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java @@ -36,9 +36,9 @@ public class TranslatorToZ3 implements AutoCloseable { public TranslatorToZ3(liquidjava.processor.context.Context c) { TranslatorContextToZ3.translateVariables(z3, c.getContext(), varTranslation); TranslatorContextToZ3.storeVariablesSubtypes(z3, c.getAllVariablesWithSupertypes(), varSuperTypes); - TranslatorContextToZ3.addAlias(c.getAlias(), aliasTranslation); + TranslatorContextToZ3.addAliases(c.getAliases(), aliasTranslation); TranslatorContextToZ3.addGhostFunctions(z3, c.getGhosts(), funcTranslation); - TranslatorContextToZ3.addGhostStates(z3, c.getGhostState(), funcTranslation); + TranslatorContextToZ3.addGhostStates(z3, c.getGhostStates(), funcTranslation); } @SuppressWarnings("unchecked") From 803d1a5404f66ca51e1ce28af5226eae2f1f42f8 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 19 Feb 2026 14:27:29 +0000 Subject: [PATCH 2/4] 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 a067afc48569b58a4d36447f13fb5be4d4405845 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 19 Feb 2026 15:48:25 +0000 Subject: [PATCH 3/4] 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 8dddf47fb3f4f2d987bf410f0a5592ea8b0900bf Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 23 Feb 2026 13:47:04 +0000 Subject: [PATCH 4/4] Rename Variables --- .../liquidjava/processor/context/Context.java | 16 ++++++++-------- .../processor/context/ContextHistory.java | 14 +++++++------- 2 files changed, 15 insertions(+), 15 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 5743a3b3..23176dfd 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java @@ -12,7 +12,7 @@ public class Context { private final List ctxGlobalVars; private List ghosts; - private Map> states; + private Map> classStates; private List aliases; private int counter; @@ -27,7 +27,7 @@ private Context() { aliases = new ArrayList<>(); ghosts = new ArrayList<>(); - states = new HashMap<>(); + classStates = new HashMap<>(); counter = 0; } @@ -48,7 +48,7 @@ public void reinitializeAllContext() { ctxFunctions = new ArrayList<>(); aliases = new ArrayList<>(); ghosts = new ArrayList<>(); - states = new HashMap<>(); + classStates = new HashMap<>(); counter = 0; } @@ -323,23 +323,23 @@ public List getGhosts() { } public void addGhostClass(String klass) { - if (!states.containsKey(klass)) - states.put(klass, new ArrayList<>()); + if (!classStates.containsKey(klass)) + classStates.put(klass, new ArrayList<>()); } public void addToGhostClass(String klass, GhostState gs) { - List l = states.get(klass); + List l = classStates.get(klass); if (!l.contains(gs)) l.add(gs); } public List getGhostState(String s) { - return states.get(s); + return classStates.get(s); } public List getGhostStates() { List lgs = new ArrayList<>(); - for (List l : states.values()) + for (List l : classStates.values()) lgs.addAll(l); return lgs; } 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..0e4db162 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java @@ -12,14 +12,14 @@ public class ContextHistory { private static ContextHistory instance; - private Map>> vars; // file -> (scope -> variables in scope) + private Map>> fileScopeVars; // file -> (scope -> variables in scope) private Set instanceVars; private Set globalVars; private Set ghosts; private Set aliases; private ContextHistory() { - vars = new HashMap<>(); + fileScopeVars = new HashMap<>(); instanceVars = new HashSet<>(); globalVars = new HashSet<>(); ghosts = new HashSet<>(); @@ -33,7 +33,7 @@ public static ContextHistory getInstance() { } public void clearHistory() { - vars.clear(); + fileScopeVars.clear(); instanceVars.clear(); globalVars.clear(); ghosts.clear(); @@ -48,8 +48,8 @@ public void saveContext(CtElement element, Context context) { // add variables in scope for this position String file = pos.getFile().getAbsolutePath(); 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 instanceVars.addAll(context.getCtxInstanceVars()); @@ -69,8 +69,8 @@ public String getScopePosition(CtElement element) { pos.getEndColumn()); } - public Map>> getVars() { - return vars; + public Map>> getFileScopeVars() { + return fileScopeVars; } public Set getInstanceVars() {