Skip to content

Change instance variable numbers for line numbers instead of counter. Refs #132 #271

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
maartinss wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Change instance variable numbers for line numbers instead of counter. Refs #132 #271

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
changed variable name convention for TypeChecker:checkVariableRefinem… 
…ents, instead of using global counter, now we're using variable lines. If there's more than one variable with the same name on the same line we use a counter to identify each variable, to use the same variable name for different methods and for better tracking on files we also include the method name
  • Loading branch information
@maartinss
maartinss committed Jul 9, 2026
commit e311bd583b4f0a26885eae36b7cd9eb58452d8eb
31 changes: 31 additions & 0 deletions liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,9 @@

import java.util.*;
import liquidjava.rj_language.Predicate;
import liquidjava.utils.constants.Formats;
import spoon.reflect.declaration.CtElement;
import spoon.reflect.declaration.CtMethod;
import spoon.reflect.reference.CtTypeReference;

public class Context {
Expand All @@ -18,6 +20,8 @@ public class Context {
private int counter;
private static Context instance;

private Map<Integer, Map<String, Integer>> lineVariables;

private Context() {
ctxVars = new Stack<>();
ctxVars.add(new ArrayList<>());
Expand All @@ -29,6 +33,7 @@ private Context() {
ghosts = new ArrayList<>();
classStates = new HashMap<>();
counter = 0;
lineVariables = new HashMap<>();
}

public static Context getInstance() {
Expand All @@ -50,6 +55,7 @@ public void reinitializeAllContext() {
ghosts = new ArrayList<>();
classStates = new HashMap<>();
counter = 0;
lineVariables = new HashMap<>();
}

public void enterContext() {
Expand Down Expand Up @@ -363,6 +369,31 @@ public List<AliasWrapper> getAliases() {
return aliases;
}

// ---------------------- Variable Name ----------------------
public String getVariableName(String varName, CtElement element) {
boolean isValidPosition = element.getPosition().isValidPosition();
int line = isValidPosition ? element.getPosition().getLine() : getCounter();
CtMethod<?> method = element.getParent(CtMethod.class);

if (!isValidPosition) {
return String.format(Formats.INSTANCE, method != null ? method.getSimpleName() + "_" + varName : varName,
line);
}

Map<String, Integer> variables = lineVariables.getOrDefault(line, new HashMap<>());

String key = method != null ? method.getSimpleName() + varName + line : varName + line;

int count = variables.getOrDefault(varName, 0);
variables.put(key, count + 1);

return count == 0
? String.format(Formats.INSTANCE, method != null ? method.getSimpleName() + "_" + varName : varName,
line)
: String.format(Formats.INSTANCE + "_%d",
method != null ? method.getSimpleName() + "_" + varName : varName, line, count);
}

@Override
public String toString() {
StringBuilder sb = new StringBuilder();
Expand Down
3 changes: 1 addition & 2 deletions liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,6 @@
import liquidjava.smt.SMTEvaluator;
import liquidjava.smt.SMTResult;
import liquidjava.utils.Utils;
import liquidjava.utils.constants.Formats;
import liquidjava.utils.constants.Keys;
import liquidjava.utils.constants.Types;
import spoon.reflect.code.CtExpression;
Expand Down Expand Up @@ -351,7 +350,7 @@ public void checkVariableRefinements(Predicate refinementFound, String simpleNam
cEt = cEt.substituteVariable(Keys.WILDCARD, simpleName);
Predicate cet = cEt.substituteVariable(Keys.WILDCARD, simpleName);

String newName = String.format(Formats.INSTANCE, simpleName, context.getCounter());
String newName = context.getVariableName(simpleName, usage);
Predicate correctNewRefinement = refinementFound.substituteVariable(Keys.WILDCARD, newName);
correctNewRefinement = correctNewRefinement.substituteVariable(Keys.THIS, newName);
cEt = cEt.substituteVariable(simpleName, newName);
Expand Down