Operator Assignment Support

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

@@ -0,0 +1,88 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class CorrectOperatorAssignments {
+
+    @Refinement("_ > 0")
+    int plus(@Refinement("_ >= 0") int x) {
+        x += 1; // x is now > 0
+        return x;
+    }
+
+    @Refinement("_ > 0")
+    int plusInvocation(@Refinement("_ >= 0") int x) {
+        x += one(); // x is now > 0
+        return x;
+    }
+
+    @Refinement("_ == 1")
+    int one() {
+        return 1;
+    }
+
+    @Refinement("_ < 0")
+    int minus(@Refinement("_ <= 0") int x) {
+        x -= 1; // x is now < 0
+        return x;
+    }
+
+    @Refinement("_ >= 0")
+    int multiply(int x) {
+        x *= x; // x is now >= 0
+        return x;
+    }
+
+    @Refinement("_ <= 1")
+    int divide(@Refinement("0 <= _ && _ <= 3") int x) {
+        x /= 2; // x is now <= 1
+        return x;
+    }
+
+    @Refinement("_ == 0 || _ == 1")
+    int remainder(@Refinement("_ >= 0") int x) {
+        x %= 2; // x is now == 0 || x is now == 1
+        return x;
+    }
+
+    int remainderInvocation(@Refinement("_ >= 0") int x) {
+        @Refinement("_ == 10 || _ == 11")
+        int y = 10;
+        y += remainder(x); // x is now >= 6
+        return x;
+    }
+
+    @Refinement("_ == 9")
+    int plusUnaryInvocation() {
+        int y = 10;
+        y += -one();
+        return y;
+    }
+
+    @Refinement("_ == 11")
+    int plusConditional(@Refinement("_ >= 0") int x) {
+        int y = 10;
+        y += x >= 0 ? one() : 2;
+        return y;
+    }
+
+    @Refinement("_ == 13")
+    int plusBinaryExpression() {
+        int y = 10;
+        y += one() + 2;
+        return y;
+    }
+
+    int plusArrayRead(int[] values) {
+        int y = 10;
+        y += values[0];
+        return y;
+    }
+
+    @Refinement("_ == 11")
+    int plusCast() {
+        int y = 10;
+        y += (int) one();
+        return y;
+    }
+}

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

@@ -0,0 +1,60 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+public class ErrorOperatorAssignments {
+
+    @Refinement("_ == 1")
+    int one() {
+        return 1;
+    }
+
+    @Refinement("_ == 0 || _ == 1")
+    int remainder(@Refinement("_ >= 0") int x) {
+        x %= 2;
+        return x;
+    }
+
+    @Refinement("_ == 12")
+    int plusInvocation(@Refinement("_ >= 0") int x) {
+        int y = 10;
+        y += remainder(x);
+        return y; // Refinement Error
+    }
+
+    @Refinement("_ == 10")
+    int plusUnaryInvocation() {
+        int y = 10;
+        y += -one();
+        return y; // Refinement Error
+    }
+
+    @Refinement("_ == 12")
+    int plusConditional(@Refinement("_ >= 0") int x) {
+        int y = 10;
+        y += x >= 0 ? one() : 2;
+        return y; // Refinement Error
+    }
+
+    @Refinement("_ == 14")
+    int plusBinaryExpression() {
+        int y = 10;
+        y += one() + 2;
+        return y; // Refinement Error
+    }
+
+    @Refinement("_ == 10")
+    int plusArrayRead(int[] values) {
+        int y = 10;
+        y += values[0];
+        return y; // Refinement Error
+    }
+
+    @Refinement("_ == 12")
+    int plusCast() {
+        int y = 10;
+        y += (int) one();
+        return y; // Refinement Error
+    }
+}

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

@@ -38,6 +38,7 @@
 import spoon.reflect.code.CtLocalVariable;
 import spoon.reflect.code.CtNewArray;
 import spoon.reflect.code.CtNewClass;
+import spoon.reflect.code.CtOperatorAssignment;
 import spoon.reflect.code.CtReturn;
 import spoon.reflect.code.CtStatement;
 import spoon.reflect.code.CtThisAccess;
@@ -186,10 +187,23 @@ public <T> void visitCtThisAccess(CtThisAccess<T> thisAccess) {
         }
     }
 
-    @SuppressWarnings("unchecked")
     @Override
     public <T, A extends T> void visitCtAssignment(CtAssignment<T, A> assignment) throws LJError {
         super.visitCtAssignment(assignment);
+        visitAssignment(assignment);
+    }
+
+    @Override
+    public <T, A extends T> void visitCtOperatorAssignment(CtOperatorAssignment<T, A> assignment) throws LJError {
+        super.visitCtOperatorAssignment(assignment);
+        visitAssignment(assignment);
+    }
+
+    /**
+     * Handles simple and operator assignments after Spoon has visited their children
+     */
+    @SuppressWarnings("unchecked")
+    private <T, A extends T> void visitAssignment(CtAssignment<T, A> assignment) throws LJError {
         CtExpression<T> ex = assignment.getAssigned();
 
         if (ex instanceof CtVariableWriteImpl) {
@@ -379,7 +393,7 @@ public void visitCtIf(CtIf ifElement) {
                 thenRefs = Predicate.createConjunction(expRefs, freshIsTrue);
                 elseRefs = Predicate.createConjunction(expRefs, freshIsFalse);
             }
-            
+
             freshRV = context.addInstanceToContext(pathVarName, factory.Type().BOOLEAN_PRIMITIVE, thenRefs, exp);
         }
         vcChecker.addPathVariable(freshRV);
@@ -495,7 +509,7 @@ private void checkAssignment(String name, CtTypeReference<?> type, CtExpression<
             CtElement parentElem, CtElement varDecl) throws LJError {
         getPutVariableMetadata(ex, name);
 
-        Predicate refinementFound = getRefinement(assignment);
+        Predicate refinementFound = getAssignmentRefinement(name, assignment, parentElem);
         if (refinementFound == null) {
             RefinedVariable rv = context.getVariableByName(name);
             if (rv instanceof Variable) {
@@ -512,6 +526,17 @@ private void checkAssignment(String name, CtTypeReference<?> type, CtExpression<
         checkVariableRefinements(refinementFound, name, type, parentElem, varDecl);
     }
 
+    /**
+     * Get the refinement for operator assignments (e.g. x += 1)
+     */
+    private Predicate getAssignmentRefinement(String name, CtExpression<?> assignment, CtElement parentElem)
+            throws LJError {
+        if (parentElem instanceof CtOperatorAssignment<?, ?> operatorAssignment) {
+            return otc.getOperatorAssignmentRefinement(name, operatorAssignment);
+        }
+        return getRefinement(assignment);
+    }
+
     private Predicate getExpressionRefinements(CtExpression<?> element) throws LJError {
         if (element instanceof CtVariableRead<?>) {
             // CtVariableRead<?> elemVar = (CtVariableRead<?>) element;

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

@@ -16,16 +16,21 @@
 import liquidjava.utils.constants.Ops;
 import liquidjava.utils.constants.Types;
 import liquidjava.rj_language.Predicate;
+import liquidjava.rj_language.ast.BinaryExpression;
+import liquidjava.rj_language.ast.Expression;
+import liquidjava.rj_language.ast.GroupExpression;
 import org.apache.commons.lang3.NotImplementedException;
 import spoon.reflect.code.BinaryOperatorKind;
 import spoon.reflect.code.CtAssignment;
+import spoon.reflect.code.CtConditional;
 import spoon.reflect.code.CtBinaryOperator;
 import spoon.reflect.code.CtExpression;
 import spoon.reflect.code.CtFieldRead;
 import spoon.reflect.code.CtIf;
 import spoon.reflect.code.CtInvocation;
 import spoon.reflect.code.CtLiteral;
 import spoon.reflect.code.CtLocalVariable;
+import spoon.reflect.code.CtOperatorAssignment;
 import spoon.reflect.code.CtReturn;
 import spoon.reflect.code.CtUnaryOperator;
 import spoon.reflect.code.CtVariableRead;
@@ -94,6 +99,18 @@ public <T> void getBinaryOpRefinements(CtBinaryOperator<T> operator) throws LJEr
         // TODO ADD TYPES
     }
 
+    /**
+     * Builds the refinement for a operator assignment. Java operator assignments such as {@code x += y} are modeled as
+     * {@code x = x + y}; the returned predicate refines the assigned value as {@code _ == current(x) <op> rhs}.
+     */
+    public Predicate getOperatorAssignmentRefinement(String assignedName, CtOperatorAssignment<?, ?> assignment)
+            throws LJError {
+        Predicate left = getCurrentVariableValue(assignedName);
+        Predicate right = getOperatorAssignmentRefinement(assignment.getAssignment());
+        Predicate operation = Predicate.createOperation(left, getOperatorFromKind(assignment.getKind()), right);
+        return Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), operation);
+    }
+
     /**
      * Finds and adds refinement metadata to the unary operation
      *
@@ -280,6 +297,91 @@ private Predicate getOperationRefinementFromExternalLib(CtInvocation<?> inv) thr
         return new Predicate();
     }
 
+    /**
+     * Returns the latest symbolic value for a variable
+     */
+    private Predicate getCurrentVariableValue(String name) {
+        Optional<VariableInstance> variableInstance = rtc.getContext().getLastVariableInstance(name);
+        return Predicate.createVar(variableInstance.map(VariableInstance::getName).orElse(name));
+    }
+
+    /**
+     * Converts a operator assignment into an arithmetic predicate operand
+     */
+    private Predicate getOperatorAssignmentRefinement(CtExpression<?> element) throws LJError {
+        if (element instanceof CtVariableRead<?> variableRead) {
+            String name = variableRead.getVariable().getSimpleName();
+            if (variableRead instanceof CtFieldRead<?>)
+                name = String.format(Formats.THIS, name);
+            return getCurrentVariableValue(name);
+        } else if (element instanceof CtBinaryOperator<?> binaryOperator) {
+            Predicate left = getOperatorAssignmentRefinement(binaryOperator.getLeftHandOperand());
+            Predicate right = getOperatorAssignmentRefinement(binaryOperator.getRightHandOperand());
+            return Predicate.createOperation(left, getOperatorFromKind(binaryOperator.getKind()), right);
+        } else if (element instanceof CtConditional<?> conditional) {
+            Predicate condition = getConditionRefinement(conditional.getCondition());
+            Predicate thenExpression = getOperatorAssignmentRefinement(conditional.getThenExpression());
+            Predicate elseExpression = getOperatorAssignmentRefinement(conditional.getElseExpression());
+            return Predicate.createITE(condition, thenExpression, elseExpression);
+        } else if (element instanceof CtLiteral<?> literal) {
+            if (literal.getValue() == null)
+                throw new CustomError("Null literals are not supported", literal.getPosition());
+            return new Predicate(literal.getValue().toString(), element);
+        } else if (element instanceof CtInvocation<?>) {
+            VariableInstance invocationValue = (VariableInstance) element.getMetadata(Keys.TARGET);
+            if (invocationValue != null)
+                return Predicate.createVar(invocationValue.getName());
+        }
+        return valueFromRefinement(element, rtc.getRefinement(element));
+    }
+
+    private Predicate getConditionRefinement(CtExpression<Boolean> condition) throws LJError {
+        Predicate refinement = rtc.getRefinement(condition);
+        Optional<Predicate> value = unwrapWildcardEquality(refinement);
+        if (value.isPresent())
+            return value.get();
+        return refinement;
+    }
+
+    private Optional<Predicate> unwrapWildcardEquality(Predicate refinement) {
+        Expression expression = unwrapGroupExpression(refinement.getExpression());
+        if (expression instanceof BinaryExpression binaryExpression && Ops.EQ.equals(binaryExpression.getOperator())
+                && Keys.WILDCARD.equals(binaryExpression.getFirstOperand().toString())) {
+            return Optional.of(new Predicate(binaryExpression.getSecondOperand()));
+        }
+        return Optional.empty();
+    }
+
+    private Predicate valueFromRefinement(CtExpression<?> element, Predicate refinement) {
+        if (refinement == null)
+            return createFreshValue(element, new Predicate());
+
+        Optional<Predicate> value = unwrapWildcardEquality(refinement);
+        if (value.isPresent())
+            return value.get();
+
+        Expression expression = unwrapGroupExpression(refinement.getExpression());
+        boolean hasWildcard = refinement.getVariableNames().contains(Keys.WILDCARD);
+        if (!hasWildcard && !expression.isBooleanExpression())
+            return new Predicate(expression);
+
+        Predicate constraint = hasWildcard ? refinement : new Predicate();
+        return createFreshValue(element, constraint);
+    }
+
+    private Predicate createFreshValue(CtExpression<?> element, Predicate refinement) {
+        String newName = String.format(Formats.FRESH, rtc.getContext().getCounter());
+        Predicate freshRefinement = refinement.substituteVariable(Keys.WILDCARD, newName);
+        rtc.getContext().addVarToContext(newName, element.getType(), freshRefinement, element);
+        return Predicate.createVar(newName);
+    }
+
+    private Expression unwrapGroupExpression(Expression expression) {
+        while (expression instanceof GroupExpression groupExpression)
+            expression = groupExpression.getExpression();
+        return expression;
+    }
+
     /**
      * Retrieves the refinements for the variable write inside unary operation
      *