Skip to content

Commit e690903

Browse files
rcosta358rcosta358
authored
Fix collisions between same-named fields (#327)
1 parent a50974f commit e690903

6 files changed

Lines changed: 86 additions & 19 deletions

File tree

‎liquidjava-example/src/main/java/testSuite/CorrectCombinedNestedFields.java‎

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.Refinement;
4+
5+
public class CorrectCombinedNestedFields {
6+
@Refinement("_ < 0")
7+
int port = -1;
8+
9+
private final Job job = new Job();
10+
11+
static class Marker {
12+
int value;
13+
}
14+
15+
@Refinement("_ < 0")
16+
public int getOuterPort() {
17+
return port;
18+
}
19+
20+
@Refinement("_ >= 0")
21+
public int getJobPort() {
22+
return job.port;
23+
}
24+
25+
public void send() {
26+
job.port = 5;
27+
}
28+
29+
static class Job {
30+
@Refinement("_ >= 0")
31+
int port;
32+
}
33+
}

‎liquidjava-example/src/main/java/testSuite/CorrectDistinctClassFields.java‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.Refinement;
4+
5+
public class CorrectDistinctClassFields {
6+
@Refinement("_ < 0") int port = -1;
7+
private final Job job = new Job();
8+
9+
public void send() {
10+
job.port = 5;
11+
}
12+
13+
static class Job {
14+
@Refinement("_ >= 0") int port;
15+
}
16+
}

‎liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java‎

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@
1818
import liquidjava.rj_language.Predicate;
1919
import liquidjava.rj_language.ast.Enum;
2020
import liquidjava.utils.StaticConstants;
21+
import liquidjava.utils.Utils;
2122
import liquidjava.utils.constants.Formats;
2223
import liquidjava.utils.constants.Keys;
2324
import liquidjava.utils.constants.Types;
@@ -232,7 +233,7 @@ private <T, A extends T> void visitAssignment(CtAssignment<T, A> assignment) thr
232233
} else if (ex instanceof CtFieldWrite<?> fw) {
233234
CtFieldReference<?> cr = fw.getVariable();
234235
CtField<?> f = fw.getVariable().getDeclaration();
235-
String updatedVarName = String.format(Formats.THIS, cr.getSimpleName());
236+
String updatedVarName = Utils.qualifyFieldName(cr);
236237
checkAssignment(updatedVarName, cr.getType(), ex, assignment.getAssignment(), assignment, f);
237238

238239
// corresponding ghost function update
@@ -273,7 +274,7 @@ public <T> void visitCtLiteral(CtLiteral<T> lit) {
273274
public <T> void visitCtField(CtField<T> f) {
274275
super.visitCtField(f);
275276
Optional<Predicate> c = getRefinementFromAnnotation(f);
276-
String name = String.format(Formats.THIS, f.getSimpleName());
277+
String name = Utils.qualifyFieldName(f.getReference());
277278
Predicate ret = new Predicate();
278279
if (c.isPresent()) {
279280
ret = c.get().substituteVariable(Keys.WILDCARD, name).substituteVariable(f.getSimpleName(), name);
@@ -303,8 +304,8 @@ public <T> void visitCtFieldRead(CtFieldRead<T> fieldRead) {
303304
Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(fieldName)));
304305
}
305306

306-
} else if (context.hasVariable(String.format(Formats.THIS, fieldName))) {
307-
String thisName = String.format(Formats.THIS, fieldName);
307+
} else if (context.hasVariable(Utils.qualifyFieldName(fieldRead.getVariable()))) {
308+
String thisName = Utils.qualifyFieldName(fieldRead.getVariable());
308309
fieldRead.putMetadata(Keys.REFINEMENT,
309310
Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(thisName)));
310311

‎liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java‎

Lines changed: 15 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -10,13 +10,15 @@
1010
import liquidjava.processor.context.Variable;
1111
import liquidjava.processor.context.VariableInstance;
1212
import liquidjava.processor.refinement_checker.TypeChecker;
13+
import liquidjava.utils.Utils;
1314
import liquidjava.utils.constants.Formats;
1415
import liquidjava.utils.constants.Keys;
1516
import liquidjava.utils.constants.Ops;
1617
import liquidjava.utils.constants.Types;
1718
import liquidjava.rj_language.Predicate;
1819
import liquidjava.rj_language.ast.BinaryExpression;
1920
import liquidjava.rj_language.ast.Expression;
21+
import liquidjava.rj_language.ast.UnaryExpression;
2022
import org.apache.commons.lang3.NotImplementedException;
2123
import spoon.reflect.code.BinaryOperatorKind;
2224
import spoon.reflect.code.CtAssignment;
@@ -121,12 +123,19 @@ public Predicate getOperatorAssignmentRefinement(String assignedName, CtOperator
121123
@SuppressWarnings({ "unchecked" })
122124
public <T> void getUnaryOpRefinements(CtUnaryOperator<T> operator) throws LJError {
123125
CtExpression<T> ex = (CtExpression<T>) operator.getOperand();
126+
if (operator.getKind() == UnaryOperatorKind.NEG && ex instanceof CtLiteral<?> literal
127+
&& literal.getValue() instanceof Number) {
128+
Predicate operand = Predicate.createLit(literal.getValue().toString(), ex.getType().getQualifiedName());
129+
Predicate value = new Predicate(new UnaryExpression("-", operand.getExpression()));
130+
operator.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), value));
131+
return;
132+
}
124133
String name = Formats.FRESH;
125134
Predicate all;
126135
if (ex instanceof CtVariableWrite<T> w) {
127136
name = w.getVariable().getSimpleName();
128-
if (w instanceof CtFieldWrite<?>)
129-
name = String.format(Formats.THIS, name);
137+
if (w instanceof CtFieldWrite<?> fieldWrite)
138+
name = Utils.qualifyFieldName(fieldWrite.getVariable());
130139
all = getRefinementUnaryVariableWrite(ex, operator, w, name);
131140
rtc.checkVariableRefinements(all, name, w.getType(), operator, w.getVariable().getDeclaration());
132141
return;
@@ -203,8 +212,8 @@ private Predicate getOperationRefinements(CtBinaryOperator<?> operator, CtVariab
203212

204213
if (element instanceof CtVariableRead<?> elemVar) {
205214
String elemName = elemVar.getVariable().getSimpleName();
206-
if (elemVar instanceof CtFieldRead)
207-
elemName = String.format(Formats.THIS, elemName);
215+
if (elemVar instanceof CtFieldRead<?> fieldRead)
216+
elemName = Utils.qualifyFieldName(fieldRead.getVariable());
208217
Predicate elemRef = rtc.getContext().getVariableRefinements(elemName);
209218

210219
// Not a field of this class (e.g. an enum constant or a static constant): use the value given by the
@@ -341,8 +350,8 @@ private Predicate getCurrentVariableValue(String name) {
341350
private Predicate getOperatorAssignmentRefinement(CtExpression<?> element) throws LJError {
342351
if (element instanceof CtVariableRead<?> variableRead) {
343352
String name = variableRead.getVariable().getSimpleName();
344-
if (variableRead instanceof CtFieldRead<?>)
345-
name = String.format(Formats.THIS, name);
353+
if (variableRead instanceof CtFieldRead<?> fieldRead)
354+
name = Utils.qualifyFieldName(fieldRead.getVariable());
346355
return getCurrentVariableValue(name);
347356
} else if (element instanceof CtBinaryOperator<?> binaryOperator) {
348357
Predicate left = getOperatorAssignmentRefinement(binaryOperator.getLeftHandOperand());

‎liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java‎

Lines changed: 12 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -180,13 +180,13 @@ private static ObjectState getStates(CtAnnotation<? extends Annotation> ctAnnota
180180

181181
// has from
182182
if (from != null) {
183-
state.setFrom(createStatePredicate(from, f.getTargetClass(), tc, e, false, prefix));
183+
state.setFrom(createStatePredicate(new Predicate(from, e, prefix), from, f.getTargetClass(), tc, e, false));
184184
state.setFromPosition(Utils.getLJAnnotationPosition(e, from));
185185
}
186186

187187
// has to
188188
if (to != null) {
189-
state.setTo(createStatePredicate(to, f.getTargetClass(), tc, e, true, prefix));
189+
state.setTo(createStatePredicate(new Predicate(to, e, prefix), to, f.getTargetClass(), tc, e, true));
190190
state.setToPosition(Utils.getLJAnnotationPosition(e, to));
191191
}
192192

@@ -209,10 +209,9 @@ private static ObjectState getStates(CtAnnotation<? extends Annotation> ctAnnota
209209
*
210210
* @return the created predicate
211211
*/
212-
private static Predicate createStatePredicate(String value, String targetClass, TypeChecker tc, CtElement e,
213-
boolean isTo, String prefix) throws LJError {
212+
private static Predicate createStatePredicate(Predicate p, String value, String targetClass, TypeChecker tc,
213+
CtElement e, boolean isTo) throws LJError {
214214
SourcePosition position = Utils.getLJAnnotationPosition(e, value);
215-
Predicate p = new Predicate(value, e, prefix);
216215
if (!p.getExpression().isBooleanExpression()) {
217216
throw new InvalidRefinementError(position, "State refinement transition must be a boolean expression",
218217
value);
@@ -392,7 +391,7 @@ public static void checkTargetChanges(TypeChecker tc, RefinedFunction f, CtExpre
392391
*/
393392
public static void updateGhostField(CtFieldWrite<?> fw, TypeChecker tc) throws LJError {
394393
CtField<?> field = fw.getVariable().getDeclaration();
395-
String updatedVarName = String.format(Formats.THIS, fw.getVariable().getSimpleName());
394+
String updatedVarName = Utils.qualifyFieldName(fw.getVariable());
396395
String targetClass = field.getDeclaringType().getQualifiedName();
397396

398397
// state transition annotation construction
@@ -421,8 +420,12 @@ public static void updateGhostField(CtFieldWrite<?> fw, TypeChecker tc) throws L
421420

422421
ObjectState stateChange = new ObjectState();
423422
String prefix = field.getDeclaringType().getQualifiedName();
424-
Predicate fromPredicate = createStatePredicate(stateChangeRefinementFrom, targetClass, tc, fw, false, prefix);
425-
Predicate toPredicate = createStatePredicate(stateChangeRefinementTo, targetClass, tc, fw, true, prefix);
423+
Predicate fromPredicate = createStatePredicate(new Predicate(), stateChangeRefinementFrom, targetClass, tc, fw,
424+
false);
425+
Predicate toPredicate = Predicate.createEquals(Predicate
426+
.createInvocation(Utils.qualifyName(prefix, field.getSimpleName()), Predicate.createVar(Keys.THIS)),
427+
Predicate.createVar(updatedVarName));
428+
toPredicate = createStatePredicate(toPredicate, stateChangeRefinementTo, targetClass, tc, fw, true);
426429
stateChange.setFrom(fromPredicate);
427430
stateChange.setTo(toPredicate);
428431

@@ -604,7 +607,7 @@ public static String prepareInvocationTarget(TypeChecker tc, CtElement target2,
604607
// means invocation is in a form of `t.method(args)`
605608
String name = v.getVariable().getSimpleName();
606609
if (target2 instanceof CtFieldRead<?> fieldRead && fieldRead.getTarget() instanceof CtThisAccess<?>) {
607-
String fieldName = String.format(Formats.THIS, name);
610+
String fieldName = Utils.qualifyFieldName(fieldRead.getVariable());
608611
if (tc.getContext().hasVariable(fieldName))
609612
name = fieldName;
610613
}

‎liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@
1919
import spoon.reflect.declaration.CtElement;
2020
import spoon.reflect.declaration.CtMethod;
2121
import spoon.reflect.factory.Factory;
22+
import spoon.reflect.reference.CtFieldReference;
2223
import spoon.reflect.reference.CtTypeReference;
2324
import spoon.support.reflect.cu.position.SourcePositionImpl;
2425

@@ -50,6 +51,10 @@ public static String qualifyName(String prefix, String name) {
5051
return String.format("%s.%s", prefix, name);
5152
}
5253

54+
public static String qualifyFieldName(CtFieldReference<?> field) {
55+
return "this#" + field.getDeclaringType().getQualifiedName() + "." + field.getSimpleName();
56+
}
57+
5358
public static String getFile(CtElement element) {
5459
SourcePosition pos = element.getPosition();
5560
if (pos == null || pos.getFile() == null)

0 commit comments

Comments
 (0)