Fold constant bitwise and shift operations, treat others as unknown

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

@@ -0,0 +1,31 @@
+package testSuite;
+
+import java.util.zip.ZipFile;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+public class CorrectBitwiseConstantArgument {
+    static final int READ = 1;
+    static final int DELETE = 4;
+
+    static void open(@Refinement("_ == 1 || _ == 5") int mode) {
+    }
+
+    static void flags(@Refinement("_ >= 0") int f) {
+    }
+
+    public static void main(String[] args) {
+        open(1 | 4); // literals fold to 5
+        open(READ | DELETE); // static final constants
+        open(ZipFile.OPEN_READ | ZipFile.OPEN_DELETE); // JDK constants, by reflection
+        open((READ | DELETE) & 5); // nested
+        open(20 >> 2 ^ 1 << 2); // shifts and xor: 5 ^ 4 = 1
+        int mask = 3 << 1;
+        mask |= 1; // operator assignment: the new value is unknown, nothing is claimed about it
+        boolean a = true, b = false;
+        boolean both = a & b; // non-short-circuit boolean operators are and/or/not-equal
+        boolean either = a | b;
+        boolean differ = a ^ b;
+    }
+}

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

@@ -0,0 +1,16 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+public class ErrorBitwiseConstantArgument {
+    static final int READ = 1;
+    static final int WRITE = 2;
+
+    static void open(@Refinement("_ == 1 || _ == 5") int mode) {
+    }
+
+    public static void main(String[] args) {
+        open(READ | WRITE); // Expect: Refinement Error
+    }
+}

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

@@ -0,0 +1,13 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+public class ErrorBitwiseUnknownOperand {
+    static void open(@Refinement("_ == 1 || _ == 5") int mode) {
+    }
+
+    static void m(int extra) {
+        open(1 | extra); // Expect: Refinement Error
+    }
+}

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

@@ -10,6 +10,7 @@
 import liquidjava.processor.context.Variable;
 import liquidjava.processor.context.VariableInstance;
 import liquidjava.processor.refinement_checker.TypeChecker;
+import liquidjava.utils.StaticConstants;
 import liquidjava.utils.Utils;
 import liquidjava.utils.constants.Formats;
 import liquidjava.utils.constants.Keys;
@@ -83,10 +84,12 @@ public <T> void getBinaryOpRefinements(CtBinaryOperator<T> operator) throws LJEr
 
         } else if (hasNullOperand(operator)) {
             oper = createFreshValue(operator, new Predicate()); // null comparisons are not supported yet: unknown value
+        } else if (operatorFor(operator) == null) {
+            oper = untranslatableOperation(operator);
         } else {
             Predicate varLeft = getOperationRefinements(operator, left);
             Predicate varRight = getOperationRefinements(operator, right);
-            oper = Predicate.createOperation(varLeft, getOperatorFromKind(operator.getKind()), varRight);
+            oper = Predicate.createOperation(varLeft, operatorFor(operator), varRight);
         }
         List<String> types = Arrays.asList(Types.IMPLEMENTED);
         if (type.contentEquals("boolean")) {
@@ -108,9 +111,12 @@ public <T> void getBinaryOpRefinements(CtBinaryOperator<T> operator) throws LJEr
      */
     public Predicate getOperatorAssignmentRefinement(String assignedName, CtOperatorAssignment<?, ?> assignment)
             throws LJError {
+        String op = getOperatorFromKind(assignment.getKind());
+        if (op == null) // x |= y, x <<= n, ...: no counterpart in the integer logic, so the new value is unknown
+            return new Predicate();
         Predicate left = getCurrentVariableValue(assignedName);
         Predicate right = getOperatorAssignmentRefinement(assignment.getAssignment());
-        Predicate operation = Predicate.createOperation(left, getOperatorFromKind(assignment.getKind()), right);
+        Predicate operation = Predicate.createOperation(left, op, right);
         return Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), operation);
     }
 
@@ -241,9 +247,11 @@ private Predicate getOperationRefinements(CtBinaryOperator<?> operator, CtVariab
         } else if (element instanceof CtBinaryOperator<?> binop) {
             if (hasNullOperand(binop)) // null comparisons are not supported yet: unknown boolean value
                 return createFreshValue(binop, new Predicate());
+            if (operatorFor(binop) == null)
+                return untranslatableOperation(binop);
             Predicate right = getOperationRefinements(operator, parentVar, binop.getRightHandOperand());
             Predicate left = getOperationRefinements(operator, parentVar, binop.getLeftHandOperand());
-            return Predicate.createOperation(left, getOperatorFromKind(binop.getKind()), right);
+            return Predicate.createOperation(left, operatorFor(binop), right);
         } else if (element instanceof CtUnaryOperator<?>) {
             Predicate a = (Predicate) element.getMetadata(Keys.REFINEMENT);
             a = a.substituteVariable(Keys.WILDCARD, "");
@@ -354,9 +362,11 @@ private Predicate getOperatorAssignmentRefinement(CtExpression<?> element) throw
                 name = Utils.qualifyFieldName(fieldRead.getVariable());
             return getCurrentVariableValue(name);
         } else if (element instanceof CtBinaryOperator<?> binaryOperator) {
+            if (operatorFor(binaryOperator) == null)
+                return untranslatableOperation(binaryOperator);
             Predicate left = getOperatorAssignmentRefinement(binaryOperator.getLeftHandOperand());
             Predicate right = getOperatorAssignmentRefinement(binaryOperator.getRightHandOperand());
-            return Predicate.createOperation(left, getOperatorFromKind(binaryOperator.getKind()), right);
+            return Predicate.createOperation(left, operatorFor(binaryOperator), right);
         } else if (element instanceof CtConditional<?> conditional) {
             Predicate condition = getConditionRefinement(conditional.getCondition());
             Predicate thenExpression = getOperatorAssignmentRefinement(conditional.getThenExpression());
@@ -443,6 +453,33 @@ private <T> Predicate getRefinementUnaryVariableWrite(CtExpression<T> ex, CtUnar
     // ############################### Operations Auxiliaries
     // ##########################################
 
+    /**
+     * The logic's operator for a binary operation, or {@code null} when it has none. On booleans the non-short-circuit
+     * {@code &}, {@code |} and {@code ^} are exactly and, or and not-equal; on integers the bitwise and shift operators
+     * have no counterpart in the linear integer logic.
+     */
+    private String operatorFor(CtBinaryOperator<?> op) {
+        String o = getOperatorFromKind(op.getKind());
+        if (o != null || op.getType() == null || !"boolean".equals(op.getType().unbox().getSimpleName()))
+            return o;
+        return switch (op.getKind()) {
+        case BITAND -> Ops.AND;
+        case BITOR -> Ops.OR;
+        case BITXOR -> Ops.NEQ;
+        default -> null;
+        };
+    }
+
+    /**
+     * A bitwise or shift operation on integers: a compile-time constant expression (e.g.
+     * {@code ZipFile.OPEN_READ | ZipFile.OPEN_DELETE}) is folded to its value; anything else is an unconstrained value
+     * of its type, so a refinement that depends on it is reported as not provable instead of crashing (#350).
+     */
+    private Predicate untranslatableOperation(CtBinaryOperator<?> op) {
+        Predicate literal = StaticConstants.asLiteralPredicate(StaticConstants.foldIntegral(op));
+        return literal != null ? literal : createFreshValue(op, new Predicate());
+    }
+
     /**
      * Get the String value of the operator from the enum
      *

liquidjava-verifier/src/main/java/liquidjava/utils/StaticConstants.java

@@ -7,7 +7,11 @@
 import liquidjava.rj_language.ast.LiteralChar;
 import liquidjava.rj_language.ast.LiteralString;
 import liquidjava.utils.constants.Types;
+import spoon.reflect.code.CtBinaryOperator;
+import spoon.reflect.code.CtExpression;
+import spoon.reflect.code.CtFieldRead;
 import spoon.reflect.code.CtLiteral;
+import spoon.reflect.code.CtUnaryOperator;
 import spoon.reflect.declaration.CtCompilationUnit;
 import spoon.reflect.declaration.CtElement;
 import spoon.reflect.declaration.CtField;
@@ -159,6 +163,78 @@ private static String packageName(CtType<?> type) {
         return type.getPackage().getQualifiedName();
     }
 
+    /**
+     * Evaluate an integral compile-time constant expression: integer literals, {@code static final} constants (see
+     * {@link #resolve(CtFieldReference)}) and the arithmetic, bitwise and shift operators over them, e.g.
+     * {@code ZipFile.OPEN_READ | ZipFile.OPEN_DELETE}. The result has Java's own semantics for the expression's type
+     * ({@code int} wraps and masks shift distances to 5 bits, {@code long} to 6). Returns {@code null} when any part is
+     * not a constant, or on division by zero.
+     */
+    public static Number foldIntegral(CtExpression<?> e) {
+        if (e instanceof CtLiteral<?> lit)
+            return integral(lit.getValue());
+        if (e instanceof CtFieldRead<?> fr)
+            return integral(resolve(fr.getVariable()));
+        boolean isLong = e.getType() != null && "long".equals(e.getType().unbox().getSimpleName());
+        if (e instanceof CtUnaryOperator<?> un) {
+            Number v = foldIntegral(un.getOperand());
+            if (v == null)
+                return null;
+            return switch (un.getKind()) {
+            case NEG -> isLong ? (Number) (-v.longValue()) : (Number) (-v.intValue());
+            case COMPL -> isLong ? (Number) (~v.longValue()) : (Number) (~v.intValue());
+            case POS -> v;
+            default -> null;
+            };
+        }
+        if (e instanceof CtBinaryOperator<?> bin) {
+            Number l = foldIntegral(bin.getLeftHandOperand()), r = foldIntegral(bin.getRightHandOperand());
+            if (l == null || r == null)
+                return null;
+            if (isLong) {
+                long a = l.longValue(), b = r.longValue();
+                return switch (bin.getKind()) {
+                case BITOR -> a | b;
+                case BITAND -> a & b;
+                case BITXOR -> a ^ b;
+                case SL -> a << b;
+                case SR -> a >> b;
+                case USR -> a >>> b;
+                case PLUS -> a + b;
+                case MINUS -> a - b;
+                case MUL -> a * b;
+                case DIV -> b == 0 ? null : a / b;
+                case MOD -> b == 0 ? null : a % b;
+                default -> null;
+                };
+            }
+            int a = l.intValue(), b = r.intValue();
+            return switch (bin.getKind()) {
+            case BITOR -> a | b;
+            case BITAND -> a & b;
+            case BITXOR -> a ^ b;
+            case SL -> a << b;
+            case SR -> a >> b;
+            case USR -> a >>> b;
+            case PLUS -> a + b;
+            case MINUS -> a - b;
+            case MUL -> a * b;
+            case DIV -> b == 0 ? null : a / b;
+            case MOD -> b == 0 ? null : a % b;
+            default -> null;
+            };
+        }
+        return null;
+    }
+
+    private static Number integral(Object v) {
+        if (v instanceof Integer || v instanceof Long || v instanceof Short || v instanceof Byte)
+            return (Number) v;
+        if (v instanceof Character c)
+            return (int) c;
+        return null;
+    }
+
     /** Wrap a resolved value as an RJ literal predicate, or {@code null} if its type is not modeled. */
     public static Predicate asLiteralPredicate(Object value) {
         if (value instanceof Boolean)