Fold constant bitwise and shift operations, treat others as unknown

[CatarinaGamboa]

Fixes #350.

Problem

A bitwise or shift operator in a refined argument crashed the verifier: getOperatorFromKind had no case for |, &, ^, <<, >> or >>>, so the null operator reached a string switch (Cannot invoke "String.hashCode()"). Bit flags combined with | are the standard way to pass JDK mode constants, so correct code such as new ZipFile(f, ZipFile.OPEN_READ | ZipFile.OPEN_DELETE) could not be verified.

Example

static void open(@Refinement("_ == 1 || _ == 5") int mode) {}

open(ZipFile.OPEN_READ | ZipFile.OPEN_DELETE); // was: crash; now: verifies (1 | 4 == 5)
open(READ | WRITE);                            // static final 1 | 2 == 3: Refinement Error
open(1 | extra);                               // unknown operand: Refinement Error (cannot prove)

Change

• StaticConstants.foldIntegral evaluates integral compile-time constant expressions (literals, static final constants from source or by reflection, and arithmetic, bitwise and shift operators over them) with Java's semantics for the expression's type (int vs long overflow and shift masking).
• OperationsChecker: where a binary operator has no counterpart in the logic, a constant expression is folded to a literal; anything else is a fresh, unconstrained value of its type, as null comparisons already are. A compound assignment such as x |= y leaves x unknown. The non-short-circuit &, | and ^ on booleans map to and, or and not-equal.
• Unchanged for every operator that was already supported.

Tests

• CorrectBitwiseConstantArgument: literals, static final constants, JDK constants by reflection, nested, shifts and xor, |=, boolean &/|/^.
• ErrorBitwiseConstantArgument: a folded constant that violates the refinement.
• ErrorBitwiseUnknownOperand: a non-constant operand is reported as not provable instead of crashing.

mvn test: all tests pass (369).

Found while building verification exercises from real Java bugs (a passport decoder passed OPEN_DELETE without OPEN_READ; the corrected program hit this crash).

🤖 Generated with Claude Code