Treat instanceof as an unknown boolean

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

@@ -0,0 +1,28 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class CorrectInstanceof {
+
+    static int positive(@Refinement("_ > 0") int x) {
+        return x;
+    }
+
+    static String describe(Object o) {
+        if (o instanceof String) {
+            return "text";
+        }
+        return "other";
+    }
+
+    static int size(Object o, @Refinement("_ > 0") int n) {
+        boolean isText = o instanceof String;
+        if (isText && n > 1) {
+            return positive(n - 1);
+        }
+        if (!(o instanceof Integer) || n > 3) {
+            return positive(n);
+        }
+        return positive(n + 1);
+    }
+}

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

@@ -0,0 +1,17 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorInstanceof {
+
+    static int positive(@Refinement("_ > 0") int x) {
+        return x;
+    }
+
+    static int size(Object o, @Refinement("_ >= 0") int n) {
+        if (o instanceof String) {
+            return positive(n); // Expect: Refinement Error
+        }
+        return 1;
+    }
+}

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

@@ -82,8 +82,8 @@ public <T> void getBinaryOpRefinements(CtBinaryOperator<T> operator) throws LJEr
                 && ((CtAssignment<?, ?>) parent).getAssigned()instanceof CtVariableWrite<?> parentVar) {
             oper = getOperationRefinements(operator, parentVar, operator);
 
-        } else if (hasNullOperand(operator)) {
-            oper = createFreshValue(operator, new Predicate()); // null comparisons are not supported yet: unknown value
+        } else if (isUntranslatable(operator)) {
+            oper = createFreshValue(operator, new Predicate()); // null comparisons and instanceof: unknown value
         } else if (operatorFor(operator) == null) {
             oper = untranslatableOperation(operator);
         } else {
@@ -245,7 +245,7 @@ private Predicate getOperationRefinements(CtBinaryOperator<?> operator, CtVariab
             rtc.getContext().addVarToContext(elemName, elemVar.getType(), e, elemVar);
             return Predicate.createVar(returnName);
         } else if (element instanceof CtBinaryOperator<?> binop) {
-            if (hasNullOperand(binop)) // null comparisons are not supported yet: unknown boolean value
+            if (isUntranslatable(binop)) // null comparisons and instanceof: unknown boolean value
                 return createFreshValue(binop, new Predicate());
             if (operatorFor(binop) == null)
                 return untranslatableOperation(binop);
@@ -336,6 +336,11 @@ private Predicate getOperationRefinementFromExternalLib(CtInvocation<?> inv) thr
         return getUnconstrainedInvocationVariable(inv);
     }
 
+    /** Null comparisons are not supported yet, and the logic has no types to test {@code instanceof} against. */
+    private static boolean isUntranslatable(CtBinaryOperator<?> binop) {
+        return binop.getKind() == BinaryOperatorKind.INSTANCEOF || hasNullOperand(binop);
+    }
+
     private static boolean hasNullOperand(CtBinaryOperator<?> binop) {
         return isNullLiteral(binop.getLeftHandOperand()) || isNullLiteral(binop.getRightHandOperand());
     }