Skip to content

Save Failing Refinements in RefinedVariable #170

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
rcosta358 wants to merge 2 commits into
base: context-history-improvements
Choose a base branch
from
Open

Save Failing Refinements in RefinedVariable #170

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
261fc57
Save Failing Refinements
rcosta358 Mar 5, 2026
d908849
Save Failing Refinements
rcosta358 Mar 5, 2026
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
9 changes: 9 additions & 0 deletions liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ public abstract class RefinedVariable extends Refined {
private PlacementInCode placementInCode;
private boolean isParameter;
private SourcePosition annPosition;
private Predicate failingRefinement;

public RefinedVariable(String name, CtTypeReference<?> type, Predicate c) {
super(name, type, c);
Expand Down Expand Up @@ -88,4 +89,12 @@ public void setIsParameter(boolean b) {
public boolean isParameter() {
return isParameter;
}

public void setFailingRefinement(Predicate failingRefinement) {
this.failingRefinement = failingRefinement;
}

public Predicate getFailingRefinement() {
return failingRefinement;
}
}
18 changes: 12 additions & 6 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 @@ -305,17 +305,23 @@ public void checkVariableRefinements(Predicate refinementFound, String simpleNam
rv.addSuperType(t);
context.addRefinementInstanceToVariable(simpleName, newName);
String customMessage = getMessageFromAnnotation(variable).orElse(mainRV != null ? mainRV.getMessage() : null);
checkSMT(cEt, usage, customMessage); // TODO CHANGE
checkSMT(cEt, usage, customMessage, mainRV); // TODO CHANGE
context.addRefinementToVariableInContext(simpleName, type, cet, usage);
}

public void checkSMT(Predicate expectedType, CtElement element) throws LJError {
checkSMT(expectedType, element, null);
public void checkSMT(Predicate expectedType, CtElement element, RefinedVariable rv) throws LJError {
checkSMT(expectedType, element, null, rv);
}

public void checkSMT(Predicate expectedType, CtElement element, String customMessage) throws LJError {
vcChecker.processSubtyping(expectedType, context.getGhostStates(), element, factory, customMessage);
element.putMetadata(Keys.REFINEMENT, expectedType);
public void checkSMT(Predicate expectedType, CtElement element, String customMessage, RefinedVariable rv)
throws LJError {
try {
vcChecker.processSubtyping(expectedType, context.getGhostStates(), element, factory, customMessage);
element.putMetadata(Keys.REFINEMENT, expectedType);
} catch (RefinementError e) {
rv.setFailingRefinement(expectedType);
throw e;
}
}

public void checkStateSMT(Predicate prevState, Predicate expectedState, CtElement target, String moreInfo)
Expand Down
6 changes: 3 additions & 3 deletions ...ava/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -200,8 +200,8 @@ public <R> void getReturnRefinements(CtReturn<R> ret) throws LJError {
Predicate cexpectedType = fi.getRefReturn().substituteVariable(Keys.WILDCARD, returnVarName)
.substituteVariable(Keys.THIS, returnVarName);

rtc.getContext().addVarToContext(returnVarName, method.getType(), cretRef, ret);
rtc.checkSMT(cexpectedType, ret, fi.getMessage());
RefinedVariable rv = rtc.getContext().addVarToContext(returnVarName, method.getType(), cretRef, ret);
rtc.checkSMT(cexpectedType, ret, fi.getMessage(), rv);
rtc.getContext().newRefinementToVariableInContext(returnVarName, cexpectedType);
}
}
Expand Down Expand Up @@ -372,7 +372,7 @@ private void checkParameters(CtElement invocation, List<CtExpression<?>> argumen
VariableInstance vi = (VariableInstance) invocation.getMetadata(Keys.TARGET);
c = c.substituteVariable(Keys.THIS, vi.getName());
}
rtc.checkSMT(c, invocation, fArg.getMessage());
rtc.checkSMT(c, invocation, fArg.getMessage(), fArg);
}
}

Expand Down
4 changes: 2 additions & 2 deletions ...rc/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -440,7 +440,7 @@ public static void updateGhostField(CtFieldWrite<?> fw, TypeChecker tc) throws L
// is a subtype of the variable's main refinement
if (rv instanceof Variable) {
Predicate superC = rv.getMainRefinement().substituteVariable(rv.getName(), vi2.getName());
tc.checkSMT(superC, fw);
tc.checkSMT(superC, fw, rv);
tc.getContext().addRefinementInstanceToVariable(parentTargetName, newInstanceName);
}
}
Expand Down Expand Up @@ -558,7 +558,7 @@ private static void addInstanceWithState(TypeChecker tc, String superName, Strin
// is a subtype of the variable's main refinement
if (rv instanceof Variable) {
Predicate superC = rv.getMainRefinement().substituteVariable(rv.getName(), vi2.getName());
tc.checkSMT(superC, invocation);
tc.checkSMT(superC, invocation, rv);
tc.getContext().addRefinementInstanceToVariable(superName, name2);
}
}
Expand Down