Cover Remaining RHS Expressions

Author: rcosta358

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

@@ -44,4 +44,45 @@ 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-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java

@@ -194,7 +194,7 @@ public <T, A extends T> void visitCtAssignment(CtAssignment<T, A> assignment) th
     }
 
     @Override
-    public <T, A extends T> void visitCtOperatorAssignment(CtOperatorAssignment<T, A> assignment) {
+    public <T, A extends T> void visitCtOperatorAssignment(CtOperatorAssignment<T, A> assignment) throws LJError {
         super.visitCtOperatorAssignment(assignment);
         visitAssignment(assignment);
     }

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

@@ -22,6 +22,7 @@
 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;
@@ -317,19 +318,62 @@ private Predicate getOperatorAssignmentRefinement(CtExpression<?> element) throw
             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());
         }
-        // unwrap wildcard equality: _ == expr -> expr
-        Predicate refinement = rtc.getRefinement(element);
+        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 new Predicate(binaryExpression.getSecondOperand());
+            return Optional.of(new Predicate(binaryExpression.getSecondOperand()));
         }
-        return refinement;
+        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) {