Skip to content

Code Refactoring #109

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

Merged
rcosta358 merged 4 commits into from
Nov 10, 2025
Merged

Code Refactoring #109

Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
8f2142f
Code Refactoring
rcosta358 Nov 9, 2025
194f7dd
Minor Fix
rcosta358 Nov 9, 2025
07ca3f0
Fix NullPointerException in `OperationsChecker`
rcosta358 Nov 9, 2025
5472ca7
Requested Changes
rcosta358 Nov 10, 2025
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
15 changes: 1 addition & 14 deletions liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorHandler.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
import java.util.Formatter;
import java.util.HashMap;
import java.util.Locale;

import liquidjava.processor.VCImplication;
import liquidjava.processor.context.PlacementInCode;
import liquidjava.rj_language.Predicate;
Expand All @@ -11,20 +12,6 @@

public class ErrorHandler {

/**
* Prints the error message
*
* @param <T>
* @param var
* @param s
* @param expectedType
* @param cSMT
*/
public static <T> void printError(CtElement var, Predicate expectedType, Predicate cSMT,
HashMap<String, PlacementInCode> map, ErrorEmitter ee) {
printError(var, null, expectedType, cSMT, map, ee);
}

public static <T> void printError(CtElement var, String moreInfo, Predicate expectedType, Predicate cSMT,
HashMap<String, PlacementInCode> map, ErrorEmitter ee) {
String resumeMessage = "Type expected:" + expectedType.toString(); // + "; " +"Refinement found:" +
Expand Down
24 changes: 24 additions & 0 deletions liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostics.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,12 @@
import liquidjava.diagnostics.warnings.LJWarning;
import liquidjava.processor.context.PlacementInCode;

/**
* Singleton class to store diagnostics information (errors, warnings, translation map) during the verification process
*
* @see LJError
* @see LJWarning
*/
public class LJDiagnostics {
private static LJDiagnostics instance;

Expand All @@ -26,6 +32,24 @@ public static LJDiagnostics getInstance() {
return instance;
}

public static LJDiagnostics add(LJError error) {
LJDiagnostics instance = getInstance();
instance.addError(error);
return instance;
}

public static LJDiagnostics add(LJWarning warning) {
LJDiagnostics instance = getInstance();
instance.addWarning(warning);
return instance;
}

public static LJDiagnostics add(HashMap<String, PlacementInCode> map) {
LJDiagnostics instance = getInstance();
instance.setTranslationMap(map);
return instance;
}

public void addError(LJError error) {
this.errors.add(error);
}
Expand Down
2 changes: 1 addition & 1 deletion liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ public class RefinementError extends LJError {
private ValDerivationNode found;

public RefinementError(CtElement element, Predicate expected, ValDerivationNode found) {
super("Refinement Error", "Predicate refinement violation", element);
super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue(), expected), element);
this.expected = expected;
this.found = found;
}
Expand Down
2 changes: 1 addition & 1 deletion liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ public class StateConflictError extends LJError {
private String className;

public StateConflictError(CtElement element, Predicate predicate, String className) {
super("State Conflict Error", "Found multiple disjoint states from a StateSet in refinement", element);
super("State Conflict Error", "Found multiple disjoint states in state transition", element);
Copy link
Copy Markdown
Collaborator

@CatarinaGamboa CatarinaGamboa Nov 10, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We could even improve this message to something like "Found multiple disjoint states in state transition - State transition can only go to one state of each state set"

this.predicate = predicate;
this.className = className;
}
Expand Down
70 changes: 36 additions & 34 deletions ...verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,9 @@
import liquidjava.rj_language.BuiltinFunctionPredicate;
import liquidjava.rj_language.Predicate;
import liquidjava.rj_language.parsing.ParsingException;
import liquidjava.utils.Utils;
import liquidjava.utils.constants.Formats;
import liquidjava.utils.constants.Keys;
import liquidjava.utils.constants.Types;

import org.apache.commons.lang3.NotImplementedException;
import spoon.reflect.code.CtArrayRead;
Expand Down Expand Up @@ -172,22 +174,22 @@ public <T> void visitCtNewArray(CtNewArray<T> newArray) {
} catch (ParsingException e) {
return; // error already in ErrorEmitter
}
String name = String.format(freshFormat, context.getCounter());
if (c.getVariableNames().contains(WILD_VAR)) {
c = c.substituteVariable(WILD_VAR, name);
String name = String.format(Formats.RET, context.getCounter());
Copy link
Copy Markdown
Collaborator

@CatarinaGamboa CatarinaGamboa Nov 10, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

why are we changing from fresh to return?

Copy link
Copy Markdown
Collaborator Author

@rcosta358 rcosta358 Nov 10, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good eye! 😅

if (c.getVariableNames().contains(Keys.WILDCARD)) {
c = c.substituteVariable(Keys.WILDCARD, name);
} else {
c = Predicate.createEquals(Predicate.createVar(name), c);
}
context.addVarToContext(name, factory.Type().INTEGER_PRIMITIVE, c, exp);
Predicate ep;
try {
ep = Predicate.createEquals(
BuiltinFunctionPredicate.builtin_length(WILD_VAR, newArray, getErrorEmitter()),
BuiltinFunctionPredicate.builtin_length(Keys.WILDCARD, newArray, getErrorEmitter()),
Predicate.createVar(name));
} catch (ParsingException e) {
return; // error already in ErrorEmitter
}
newArray.putMetadata(REFINE_KEY, ep);
newArray.putMetadata(Keys.REFINEMENT, ep);
}
}

Expand All @@ -201,9 +203,9 @@ public <T> void visitCtThisAccess(CtThisAccess<T> thisAccess) {
CtClass<?> c = thisAccess.getParent(CtClass.class);
String s = c.getSimpleName();
if (thisAccess.getParent() instanceof CtReturn) {
String thisName = String.format(thisFormat, s);
thisAccess.putMetadata(REFINE_KEY,
Predicate.createEquals(Predicate.createVar(WILD_VAR), Predicate.createVar(thisName)));
String thisName = String.format(Formats.THIS, s);
thisAccess.putMetadata(Keys.REFINEMENT,
Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(thisName)));
}
}

Expand All @@ -227,7 +229,7 @@ public <T, A extends T> void visitCtAssignment(CtAssignment<T, A> assignment) {
CtFieldWrite<?> fw = ((CtFieldWrite<?>) ex);
CtFieldReference<?> cr = fw.getVariable();
CtField<?> f = fw.getVariable().getDeclaration();
String updatedVarName = String.format(thisFormat, cr.getSimpleName());
String updatedVarName = String.format(Formats.THIS, cr.getSimpleName());
checkAssignment(updatedVarName, cr.getType(), ex, assignment.getAssignment(), assignment, f);

// corresponding ghost function update
Expand All @@ -249,9 +251,9 @@ public <T> void visitCtArrayRead(CtArrayRead<T> arrayRead) {
}

super.visitCtArrayRead(arrayRead);
String name = String.format(instanceFormat, "arrayAccess", context.getCounter());
String name = String.format(Formats.INSTANCE, "arrayAccess", context.getCounter());
context.addVarToContext(name, arrayRead.getType(), new Predicate(), arrayRead);
arrayRead.putMetadata(REFINE_KEY, Predicate.createVar(name));
arrayRead.putMetadata(Keys.REFINEMENT, Predicate.createVar(name));
// TODO predicate for now is always TRUE
}

Expand All @@ -261,15 +263,15 @@ public <T> void visitCtLiteral(CtLiteral<T> lit) {
return;
}

List<String> types = Arrays.asList(implementedTypes);
List<String> types = Arrays.asList(Types.IMPLEMENTED);
String type = lit.getType().getQualifiedName();
if (types.contains(type)) {
lit.putMetadata(REFINE_KEY, Predicate.createEquals(Predicate.createVar(WILD_VAR),
lit.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD),
Predicate.createLit(lit.getValue().toString(), type)));

} else if (lit.getType().getQualifiedName().equals("java.lang.String")) {
// Only taking care of strings inside refinements
} else if (type.equals(Utils.NULL_TYPE)) {
} else if (type.equals(Types.NULL)) {
// Skip null literals
} else {
throw new NotImplementedException(
Expand All @@ -293,10 +295,10 @@ public <T> void visitCtField(CtField<T> f) {
// context.addVarToContext(f.getSimpleName(), f.getType(),
// c.map( i -> i.substituteVariable(WILD_VAR, f.getSimpleName()).orElse(new
// Predicate()) );
String nname = String.format(thisFormat, f.getSimpleName());
String nname = String.format(Formats.THIS, f.getSimpleName());
Predicate ret = new Predicate();
if (c.isPresent()) {
ret = c.get().substituteVariable(WILD_VAR, nname).substituteVariable(f.getSimpleName(), nname);
ret = c.get().substituteVariable(Keys.WILDCARD, nname).substituteVariable(f.getSimpleName(), nname);
}
RefinedVariable v = context.addVarToContext(nname, f.getType(), ret, f);
if (v instanceof Variable) {
Expand All @@ -315,27 +317,27 @@ public <T> void visitCtFieldRead(CtFieldRead<T> fieldRead) {
RefinedVariable rv = context.getVariableByName(fieldName);
if (rv instanceof Variable && ((Variable) rv).getLocation().isPresent()
&& ((Variable) rv).getLocation().get().equals(fieldRead.getTarget().toString())) {
fieldRead.putMetadata(REFINE_KEY, context.getVariableRefinements(fieldName));
fieldRead.putMetadata(Keys.REFINEMENT, context.getVariableRefinements(fieldName));
} else {
fieldRead.putMetadata(REFINE_KEY,
Predicate.createEquals(Predicate.createVar(WILD_VAR), Predicate.createVar(fieldName)));
fieldRead.putMetadata(Keys.REFINEMENT,
Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(fieldName)));
}

} else if (context.hasVariable(String.format(thisFormat, fieldName))) {
String thisName = String.format(thisFormat, fieldName);
fieldRead.putMetadata(REFINE_KEY,
Predicate.createEquals(Predicate.createVar(WILD_VAR), Predicate.createVar(thisName)));
} else if (context.hasVariable(String.format(Formats.THIS, fieldName))) {
String thisName = String.format(Formats.THIS, fieldName);
fieldRead.putMetadata(Keys.REFINEMENT,
Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(thisName)));

} else if (fieldRead.getVariable().getSimpleName().equals("length")) {
String targetName = fieldRead.getTarget().toString();
try {
fieldRead.putMetadata(REFINE_KEY, Predicate.createEquals(Predicate.createVar(WILD_VAR),
fieldRead.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD),
BuiltinFunctionPredicate.builtin_length(targetName, fieldRead, getErrorEmitter())));
} catch (ParsingException e) {
return; // error already in ErrorEmitter
}
} else {
fieldRead.putMetadata(REFINE_KEY, new Predicate());
fieldRead.putMetadata(Keys.REFINEMENT, new Predicate());
// TODO DO WE WANT THIS OR TO SHOW ERROR MESSAGE
}

Expand Down Expand Up @@ -417,8 +419,8 @@ public void visitCtIf(CtIf ifElement) {
} catch (ParsingException e) {
return; // error already in ErrorEmitter
}
String freshVarName = String.format(freshFormat, context.getCounter());
expRefs = expRefs.substituteVariable(WILD_VAR, freshVarName);
String freshVarName = String.format(Formats.FRESH, context.getCounter());
expRefs = expRefs.substituteVariable(Keys.WILDCARD, freshVarName);
Predicate lastExpRefs = substituteAllVariablesForLastInstance(expRefs);
expRefs = Predicate.createConjunction(expRefs, lastExpRefs);

Expand Down Expand Up @@ -470,11 +472,11 @@ public <T> void visitCtArrayWrite(CtArrayWrite<T> arrayWrite) {
BuiltinFunctionPredicate fp;
try {
fp = BuiltinFunctionPredicate.builtin_addToIndex(arrayWrite.getTarget().toString(), index.toString(),
WILD_VAR, arrayWrite, getErrorEmitter());
Keys.WILDCARD, arrayWrite, getErrorEmitter());
} catch (ParsingException e) {
return; // error already in ErrorEmitter
}
arrayWrite.putMetadata(REFINE_KEY, fp);
arrayWrite.putMetadata(Keys.REFINEMENT, fp);
}

@Override
Expand All @@ -487,7 +489,7 @@ public <T> void visitCtConditional(CtConditional<T> conditional) {
Predicate cond = getRefinement(conditional.getCondition());
Predicate c = Predicate.createITE(cond, getRefinement(conditional.getThenExpression()),
getRefinement(conditional.getElseExpression()));
conditional.putMetadata(REFINE_KEY, c);
conditional.putMetadata(Keys.REFINEMENT, c);
}

@Override
Expand Down Expand Up @@ -582,12 +584,12 @@ private Predicate substituteAllVariablesForLastInstance(Predicate c) {
* Cannot be null
*/
private <T> void getPutVariableMetadada(CtElement elem, String name) {
Predicate cref = Predicate.createEquals(Predicate.createVar(WILD_VAR), Predicate.createVar(name));
Predicate cref = Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(name));
Optional<VariableInstance> ovi = context.getLastVariableInstance(name);
if (ovi.isPresent()) {
cref = Predicate.createEquals(Predicate.createVar(WILD_VAR), Predicate.createVar(ovi.get().getName()));
cref = Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(ovi.get().getName()));
}

elem.putMetadata(REFINE_KEY, cref);
elem.putMetadata(Keys.REFINEMENT, cref);
}
}
44 changes: 17 additions & 27 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 @@ -17,7 +17,9 @@
import liquidjava.rj_language.Predicate;
import liquidjava.rj_language.parsing.ParsingException;
import liquidjava.rj_language.parsing.RefinementsParser;
import liquidjava.utils.Utils;
import liquidjava.utils.constants.Formats;
import liquidjava.utils.constants.Keys;
import liquidjava.utils.constants.Types;
import spoon.reflect.code.CtExpression;
import spoon.reflect.code.CtLiteral;
import spoon.reflect.code.CtNewArray;
Expand All @@ -31,16 +33,6 @@
import spoon.reflect.visitor.CtScanner;

public abstract class TypeChecker extends CtScanner {
public final String REFINE_KEY = "refinement";
public final String TARGET_KEY = "target";
// public final String STATE_KEY = "state";
public final String THIS = "this";
public final String WILD_VAR = "_";
public final String freshFormat = "#fresh_%d";
public final String instanceFormat = "#%s_%d";
public final String thisFormat = "this#%s";
public String[] implementedTypes = { "boolean", "int", "short", "long", "float", "double" }; // TODO add
// types e.g., "int[]"

Context context;
Factory factory;
Expand All @@ -63,7 +55,7 @@ public Factory getFactory() {
}

public Predicate getRefinement(CtElement elem) {
Predicate c = (Predicate) elem.getMetadata(REFINE_KEY);
Predicate c = (Predicate) elem.getMetadata(Keys.REFINEMENT);
return c == null ? new Predicate() : c;
}

Expand Down Expand Up @@ -142,7 +134,7 @@ private void createStateSet(CtNewArray<String> e, int set, CtElement element) {
context.addGhostClass(g.getParentClassName());

List<CtExpression<?>> ls = e.getElements();
Predicate ip = Predicate.createInvocation(g.getName(), Predicate.createVar(THIS));
Predicate ip = Predicate.createInvocation(g.getName(), Predicate.createVar(Keys.WILDCARD));
int order = 0;
for (CtExpression<?> ce : ls) {
if (ce instanceof CtLiteral<?>) {
Expand All @@ -154,7 +146,7 @@ private void createStateSet(CtNewArray<String> e, int set, CtElement element) {
gs.setGhostParent(g);
gs.setRefinement(
/* new OperationPredicate(new InvocationPredicate(f, THIS), "<-->", */
Predicate.createEquals(ip, Predicate.createLit(Integer.toString(order), Utils.INT))); // open(THIS)
Predicate.createEquals(ip, Predicate.createLit(Integer.toString(order), Types.INT))); // open(THIS)
// ->
// state1(THIS)
// == 1
Expand Down Expand Up @@ -258,7 +250,7 @@ protected void handleAlias(String value, CtElement element) {
errorEmitter);
return;
}
AliasWrapper aw = new AliasWrapper(a, factory, WILD_VAR, context, klass, path);
AliasWrapper aw = new AliasWrapper(a, factory, Keys.WILDCARD, context, klass, path);
context.addAlias(aw);
}
} catch (ParsingException e) {
Expand Down Expand Up @@ -295,12 +287,12 @@ else if (expectedType.isPresent())
else
cEt = new Predicate();

cEt = cEt.substituteVariable(WILD_VAR, simpleName);
Predicate cet = cEt.substituteVariable(WILD_VAR, simpleName);
cEt = cEt.substituteVariable(Keys.WILDCARD, simpleName);
Predicate cet = cEt.substituteVariable(Keys.WILDCARD, simpleName);

String newName = String.format(instanceFormat, simpleName, context.getCounter());
Predicate correctNewRefinement = refinementFound.substituteVariable(WILD_VAR, newName);
correctNewRefinement = correctNewRefinement.substituteVariable(THIS, newName);
String newName = String.format(Formats.INSTANCE, simpleName, context.getCounter());
Predicate correctNewRefinement = refinementFound.substituteVariable(Keys.WILDCARD, newName);
correctNewRefinement = correctNewRefinement.substituteVariable(Keys.THIS, newName);
cEt = cEt.substituteVariable(simpleName, newName);

// Substitute variable in verification
Expand All @@ -314,18 +306,16 @@ else if (expectedType.isPresent())
}

public void checkSMT(Predicate expectedType, CtElement element) {
vcChecker.processSubtyping(expectedType, context.getGhostState(), WILD_VAR, THIS, element, factory);
element.putMetadata(REFINE_KEY, expectedType);
vcChecker.processSubtyping(expectedType, context.getGhostState(), element, factory);
element.putMetadata(Keys.REFINEMENT, expectedType);
}

public void checkStateSMT(Predicate prevState, Predicate expectedState, CtElement target, String string) {
vcChecker.processSubtyping(prevState, expectedState, context.getGhostState(), WILD_VAR, THIS, target, string,
factory);
public void checkStateSMT(Predicate prevState, Predicate expectedState, CtElement target, String moreInfo) {
vcChecker.processSubtyping(prevState, expectedState, context.getGhostState(), target, moreInfo, factory);
}

public boolean checksStateSMT(Predicate prevState, Predicate expectedState, SourcePosition p) {
return vcChecker.canProcessSubtyping(prevState, expectedState, context.getGhostState(), WILD_VAR, THIS, p,
factory);
return vcChecker.canProcessSubtyping(prevState, expectedState, context.getGhostState(), p, factory);
}

public void createError(CtElement element, Predicate expectedType, Predicate foundType, String customeMessage) {
Expand Down
Loading