Skip to content

Commit b98a110

Browse files
rcosta358rcosta358
authored
Operator Assignment Support (#214)
1 parent cbfcc38 commit b98a110

4 files changed

Lines changed: 277 additions & 2 deletions

File tree

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

Lines changed: 88 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,88 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.Refinement;
4+
5+
public class CorrectOperatorAssignments {
6+
7+
@Refinement("_ > 0")
8+
int plus(@Refinement("_ >= 0") int x) {
9+
x += 1; // x is now > 0
10+
return x;
11+
}
12+
13+
@Refinement("_ > 0")
14+
int plusInvocation(@Refinement("_ >= 0") int x) {
15+
x += one(); // x is now > 0
16+
return x;
17+
}
18+
19+
@Refinement("_ == 1")
20+
int one() {
21+
return 1;
22+
}
23+
24+
@Refinement("_ < 0")
25+
int minus(@Refinement("_ <= 0") int x) {
26+
x -= 1; // x is now < 0
27+
return x;
28+
}
29+
30+
@Refinement("_ >= 0")
31+
int multiply(int x) {
32+
x *= x; // x is now >= 0
33+
return x;
34+
}
35+
36+
@Refinement("_ <= 1")
37+
int divide(@Refinement("0 <= _ && _ <= 3") int x) {
38+
x /= 2; // x is now <= 1
39+
return x;
40+
}
41+
42+
@Refinement("_ == 0 || _ == 1")
43+
int remainder(@Refinement("_ >= 0") int x) {
44+
x %= 2; // x is now == 0 || x is now == 1
45+
return x;
46+
}
47+
48+
int remainderInvocation(@Refinement("_ >= 0") int x) {
49+
@Refinement("_ == 10 || _ == 11")
50+
int y = 10;
51+
y += remainder(x); // x is now >= 6
52+
return x;
53+
}
54+
55+
@Refinement("_ == 9")
56+
int plusUnaryInvocation() {
57+
int y = 10;
58+
y += -one();
59+
return y;
60+
}
61+
62+
@Refinement("_ == 11")
63+
int plusConditional(@Refinement("_ >= 0") int x) {
64+
int y = 10;
65+
y += x >= 0 ? one() : 2;
66+
return y;
67+
}
68+
69+
@Refinement("_ == 13")
70+
int plusBinaryExpression() {
71+
int y = 10;
72+
y += one() + 2;
73+
return y;
74+
}
75+
76+
int plusArrayRead(int[] values) {
77+
int y = 10;
78+
y += values[0];
79+
return y;
80+
}
81+
82+
@Refinement("_ == 11")
83+
int plusCast() {
84+
int y = 10;
85+
y += (int) one();
86+
return y;
87+
}
88+
}

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

Lines changed: 60 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,60 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.Refinement;
4+
5+
@SuppressWarnings("unused")
6+
public class ErrorOperatorAssignments {
7+
8+
@Refinement("_ == 1")
9+
int one() {
10+
return 1;
11+
}
12+
13+
@Refinement("_ == 0 || _ == 1")
14+
int remainder(@Refinement("_ >= 0") int x) {
15+
x %= 2;
16+
return x;
17+
}
18+
19+
@Refinement("_ == 12")
20+
int plusInvocation(@Refinement("_ >= 0") int x) {
21+
int y = 10;
22+
y += remainder(x);
23+
return y; // Refinement Error
24+
}
25+
26+
@Refinement("_ == 10")
27+
int plusUnaryInvocation() {
28+
int y = 10;
29+
y += -one();
30+
return y; // Refinement Error
31+
}
32+
33+
@Refinement("_ == 12")
34+
int plusConditional(@Refinement("_ >= 0") int x) {
35+
int y = 10;
36+
y += x >= 0 ? one() : 2;
37+
return y; // Refinement Error
38+
}
39+
40+
@Refinement("_ == 14")
41+
int plusBinaryExpression() {
42+
int y = 10;
43+
y += one() + 2;
44+
return y; // Refinement Error
45+
}
46+
47+
@Refinement("_ == 10")
48+
int plusArrayRead(int[] values) {
49+
int y = 10;
50+
y += values[0];
51+
return y; // Refinement Error
52+
}
53+
54+
@Refinement("_ == 12")
55+
int plusCast() {
56+
int y = 10;
57+
y += (int) one();
58+
return y; // Refinement Error
59+
}
60+
}

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

Lines changed: 27 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,7 @@
3838
import spoon.reflect.code.CtLocalVariable;
3939
import spoon.reflect.code.CtNewArray;
4040
import spoon.reflect.code.CtNewClass;
41+
import spoon.reflect.code.CtOperatorAssignment;
4142
import spoon.reflect.code.CtReturn;
4243
import spoon.reflect.code.CtStatement;
4344
import spoon.reflect.code.CtThisAccess;
@@ -186,10 +187,23 @@ public <T> void visitCtThisAccess(CtThisAccess<T> thisAccess) {
186187
}
187188
}
188189

189-
@SuppressWarnings("unchecked")
190190
@Override
191191
public <T, A extends T> void visitCtAssignment(CtAssignment<T, A> assignment) throws LJError {
192192
super.visitCtAssignment(assignment);
193+
visitAssignment(assignment);
194+
}
195+
196+
@Override
197+
public <T, A extends T> void visitCtOperatorAssignment(CtOperatorAssignment<T, A> assignment) throws LJError {
198+
super.visitCtOperatorAssignment(assignment);
199+
visitAssignment(assignment);
200+
}
201+
202+
/**
203+
* Handles simple and operator assignments after Spoon has visited their children
204+
*/
205+
@SuppressWarnings("unchecked")
206+
private <T, A extends T> void visitAssignment(CtAssignment<T, A> assignment) throws LJError {
193207
CtExpression<T> ex = assignment.getAssigned();
194208

195209
if (ex instanceof CtVariableWriteImpl) {
@@ -495,7 +509,7 @@ private void checkAssignment(String name, CtTypeReference<?> type, CtExpression<
495509
CtElement parentElem, CtElement varDecl) throws LJError {
496510
getPutVariableMetadata(ex, name);
497511

498-
Predicate refinementFound = getRefinement(assignment);
512+
Predicate refinementFound = getAssignmentRefinement(name, assignment, parentElem);
499513
if (refinementFound == null) {
500514
RefinedVariable rv = context.getVariableByName(name);
501515
if (rv instanceof Variable) {
@@ -512,6 +526,17 @@ private void checkAssignment(String name, CtTypeReference<?> type, CtExpression<
512526
checkVariableRefinements(refinementFound, name, type, parentElem, varDecl);
513527
}
514528

529+
/**
530+
* Get the refinement for operator assignments (e.g. x += 1)
531+
*/
532+
private Predicate getAssignmentRefinement(String name, CtExpression<?> assignment, CtElement parentElem)
533+
throws LJError {
534+
if (parentElem instanceof CtOperatorAssignment<?, ?> operatorAssignment) {
535+
return otc.getOperatorAssignmentRefinement(name, operatorAssignment);
536+
}
537+
return getRefinement(assignment);
538+
}
539+
515540
private Predicate getExpressionRefinements(CtExpression<?> element) throws LJError {
516541
if (element instanceof CtVariableRead<?>) {
517542
// CtVariableRead<?> elemVar = (CtVariableRead<?>) element;

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

Lines changed: 102 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,16 +16,21 @@
1616
import liquidjava.utils.constants.Ops;
1717
import liquidjava.utils.constants.Types;
1818
import liquidjava.rj_language.Predicate;
19+
import liquidjava.rj_language.ast.BinaryExpression;
20+
import liquidjava.rj_language.ast.Expression;
21+
import liquidjava.rj_language.ast.GroupExpression;
1922
import org.apache.commons.lang3.NotImplementedException;
2023
import spoon.reflect.code.BinaryOperatorKind;
2124
import spoon.reflect.code.CtAssignment;
25+
import spoon.reflect.code.CtConditional;
2226
import spoon.reflect.code.CtBinaryOperator;
2327
import spoon.reflect.code.CtExpression;
2428
import spoon.reflect.code.CtFieldRead;
2529
import spoon.reflect.code.CtIf;
2630
import spoon.reflect.code.CtInvocation;
2731
import spoon.reflect.code.CtLiteral;
2832
import spoon.reflect.code.CtLocalVariable;
33+
import spoon.reflect.code.CtOperatorAssignment;
2934
import spoon.reflect.code.CtReturn;
3035
import spoon.reflect.code.CtUnaryOperator;
3136
import spoon.reflect.code.CtVariableRead;
@@ -94,6 +99,18 @@ public <T> void getBinaryOpRefinements(CtBinaryOperator<T> operator) throws LJEr
9499
// TODO ADD TYPES
95100
}
96101

102+
/**
103+
* Builds the refinement for a operator assignment. Java operator assignments such as {@code x += y} are modeled as
104+
* {@code x = x + y}; the returned predicate refines the assigned value as {@code _ == current(x) <op> rhs}.
105+
*/
106+
public Predicate getOperatorAssignmentRefinement(String assignedName, CtOperatorAssignment<?, ?> assignment)
107+
throws LJError {
108+
Predicate left = getCurrentVariableValue(assignedName);
109+
Predicate right = getOperatorAssignmentRefinement(assignment.getAssignment());
110+
Predicate operation = Predicate.createOperation(left, getOperatorFromKind(assignment.getKind()), right);
111+
return Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), operation);
112+
}
113+
97114
/**
98115
* Finds and adds refinement metadata to the unary operation
99116
*
@@ -280,6 +297,91 @@ private Predicate getOperationRefinementFromExternalLib(CtInvocation<?> inv) thr
280297
return new Predicate();
281298
}
282299

300+
/**
301+
* Returns the latest symbolic value for a variable
302+
*/
303+
private Predicate getCurrentVariableValue(String name) {
304+
Optional<VariableInstance> variableInstance = rtc.getContext().getLastVariableInstance(name);
305+
return Predicate.createVar(variableInstance.map(VariableInstance::getName).orElse(name));
306+
}
307+
308+
/**
309+
* Converts a operator assignment into an arithmetic predicate operand
310+
*/
311+
private Predicate getOperatorAssignmentRefinement(CtExpression<?> element) throws LJError {
312+
if (element instanceof CtVariableRead<?> variableRead) {
313+
String name = variableRead.getVariable().getSimpleName();
314+
if (variableRead instanceof CtFieldRead<?>)
315+
name = String.format(Formats.THIS, name);
316+
return getCurrentVariableValue(name);
317+
} else if (element instanceof CtBinaryOperator<?> binaryOperator) {
318+
Predicate left = getOperatorAssignmentRefinement(binaryOperator.getLeftHandOperand());
319+
Predicate right = getOperatorAssignmentRefinement(binaryOperator.getRightHandOperand());
320+
return Predicate.createOperation(left, getOperatorFromKind(binaryOperator.getKind()), right);
321+
} else if (element instanceof CtConditional<?> conditional) {
322+
Predicate condition = getConditionRefinement(conditional.getCondition());
323+
Predicate thenExpression = getOperatorAssignmentRefinement(conditional.getThenExpression());
324+
Predicate elseExpression = getOperatorAssignmentRefinement(conditional.getElseExpression());
325+
return Predicate.createITE(condition, thenExpression, elseExpression);
326+
} else if (element instanceof CtLiteral<?> literal) {
327+
if (literal.getValue() == null)
328+
throw new CustomError("Null literals are not supported", literal.getPosition());
329+
return new Predicate(literal.getValue().toString(), element);
330+
} else if (element instanceof CtInvocation<?>) {
331+
VariableInstance invocationValue = (VariableInstance) element.getMetadata(Keys.TARGET);
332+
if (invocationValue != null)
333+
return Predicate.createVar(invocationValue.getName());
334+
}
335+
return valueFromRefinement(element, rtc.getRefinement(element));
336+
}
337+
338+
private Predicate getConditionRefinement(CtExpression<Boolean> condition) throws LJError {
339+
Predicate refinement = rtc.getRefinement(condition);
340+
Optional<Predicate> value = unwrapWildcardEquality(refinement);
341+
if (value.isPresent())
342+
return value.get();
343+
return refinement;
344+
}
345+
346+
private Optional<Predicate> unwrapWildcardEquality(Predicate refinement) {
347+
Expression expression = unwrapGroupExpression(refinement.getExpression());
348+
if (expression instanceof BinaryExpression binaryExpression && Ops.EQ.equals(binaryExpression.getOperator())
349+
&& Keys.WILDCARD.equals(binaryExpression.getFirstOperand().toString())) {
350+
return Optional.of(new Predicate(binaryExpression.getSecondOperand()));
351+
}
352+
return Optional.empty();
353+
}
354+
355+
private Predicate valueFromRefinement(CtExpression<?> element, Predicate refinement) {
356+
if (refinement == null)
357+
return createFreshValue(element, new Predicate());
358+
359+
Optional<Predicate> value = unwrapWildcardEquality(refinement);
360+
if (value.isPresent())
361+
return value.get();
362+
363+
Expression expression = unwrapGroupExpression(refinement.getExpression());
364+
boolean hasWildcard = refinement.getVariableNames().contains(Keys.WILDCARD);
365+
if (!hasWildcard && !expression.isBooleanExpression())
366+
return new Predicate(expression);
367+
368+
Predicate constraint = hasWildcard ? refinement : new Predicate();
369+
return createFreshValue(element, constraint);
370+
}
371+
372+
private Predicate createFreshValue(CtExpression<?> element, Predicate refinement) {
373+
String newName = String.format(Formats.FRESH, rtc.getContext().getCounter());
374+
Predicate freshRefinement = refinement.substituteVariable(Keys.WILDCARD, newName);
375+
rtc.getContext().addVarToContext(newName, element.getType(), freshRefinement, element);
376+
return Predicate.createVar(newName);
377+
}
378+
379+
private Expression unwrapGroupExpression(Expression expression) {
380+
while (expression instanceof GroupExpression groupExpression)
381+
expression = groupExpression.getExpression();
382+
return expression;
383+
}
384+
283385
/**
284386
* Retrieves the refinements for the variable write inside unary operation
285387
*

0 commit comments

Comments
 (0)