Support bitwise and shift compound assignments without internal null errors

Start in liquidjava-verifier/.../refinement_checker/general_checkers/OperationsChecker.java: getOperatorFromKind (~L444) returns null for Spoon BITAND/BITOR/BITXOR/SL/SR/USR, and getOperatorAssignmentRefinement (~L107) passes that null into Predicate.createOperation. Trace how the already-working += and %= compound assignments flow through Ops and ExpressionToZ3Visitor.visitBinaryExpression, then add the missing operator cases plus a guard for unsupported operators before expression construction. Done = the ./liquidjava CompoundAnd.java reproducer prints Correct! Passed Verification, an incorrect refinement reports a Refinement Error instead of the null error, and the CorrectOperatorAssignments suite gains cases for all six integer and three Boolean compound operators.

Problem

Bitwise and shift compound assignments produce an internal null error when LiquidJava needs to check a refinement involving their result. This affects all six remaining integer compound operators (&=, |=, ^=, <<=, >>=, >>>=) and Boolean &=, |=, ^=.

Integer +=, -=, *=, /=, and %= already work in the tested cases. The existing CorrectOperatorAssignments suite also covers %=.

Reproduction

Save as CompoundAnd.java and run ./liquidjava CompoundAnd.java from the repository root:

import liquidjava.specification.Refinement;

public class CompoundAnd {
    @Refinement("_ == 2")
    int test() {
        int x = 6;
        x &= 3;
        return x;
    }
}

Expected: Correct! Passed Verification. because 6 & 3 == 2.

Actual:

Error: Cannot invoke "String.hashCode()" because "<local4>" is null
5 |         int x = 6;
6 |         x &= 3;
7 |         return x;
  |         ^^^^^^^^^

Changing the return refinement to _ != 2 also produces the internal error, instead of a Refinement Error. Removing the return refinement produces Correct! Passed Verification.; accepting that unrefined example does not demonstrate support for checking the operation's result.

Boolean reproducer:

import liquidjava.specification.Refinement;

public class CompoundBooleanAnd {
    @Refinement("_ == false")
    boolean test() {
        boolean x = true;
        x &= false;
        return x;
    }
}

This produces the same null error.

Results from running examples

For each row, ran three separate Java files: a correct return refinement _ == expected, an incorrect return refinement _ != expected, and no return refinement. All files compile with javac.

Type	Initial value	Assignment	Expected result	Correct refinement	Incorrect refinement	No refinement
int	10	x += 2	12	Pass	Refinement Error	Pass
int	10	x -= 2	8	Pass	Refinement Error	Pass
int	10	x *= 2	20	Pass	Refinement Error	Pass
int	10	x /= 2	5	Pass	Refinement Error	Pass
int	10	x %= 3	1	Pass	Refinement Error	Pass
int	6	x &= 3	2	Internal null error	Internal null error	Pass
int	6	`x	= 3`	7	Internal null error	Internal null error
int	6	x ^= 3	5	Internal null error	Internal null error	Pass
int	6	x <<= 1	12	Internal null error	Internal null error	Pass
int	-8	x >>= 1	-4	Internal null error	Internal null error	Pass
int	-8	x >>>= 1	2147483644	Internal null error	Internal null error	Pass
boolean	true	x &= false	false	Internal null error	Internal null error	Pass
boolean	false	`x	= true`	true	Internal null error	Internal null error
boolean	true	x ^= true	false	Internal null error	Internal null error	Pass

Also reproduced the same null error with &= when:

• The target itself is refined: @Refinement("_ >= 0") int x = 6; x &= 3;.
• Its result initializes a refined local: int x = 6; x &= 3; @Refinement("_ == 2") int y = x;.
• Its result is passed to a refined parameter: int x = 6; x &= 3; take(x);, where take requires _ == 2.

The diagnostic may therefore appear on the assignment or on a later use. The CLI prints this error but returns exit status 0 (and the Maven launcher reports build success).

String += was also probed, but is excluded from this operator matrix: String x = "a"; x += "b"; with a refined return reports Not Found Error: Variable 'b' could not be found. A plain refined return "ab" and ordinary string concatenation also fail with incompatible String sorts, so string support requires separate investigation.

Missing implementation

Source inspection explains the operator matrix:

• OperationsChecker.getOperatorFromKind has no cases for Spoon BITAND, BITOR, BITXOR, SL, SR, or USR; it returns null. AND and OR there are the logical operators, not the kinds used by &= and |=.
• getOperatorAssignmentRefinement passes that null operator into Predicate.createOperation, constructing a malformed BinaryExpression that fails during subsequent refinement processing.
• Ops and ExpressionToZ3Visitor.visitBinaryExpression also lack bitwise/shift operations. Adding only the Spoon mappings would not implement the missing semantics.

Needed: integral bitwise/shift semantics, Boolean &/|/^ semantics, safe handling of unsupported operators before constructing expressions, and regression coverage for successful verification and expected refinement violations. Preserve Java's eager Boolean evaluation and integer width/shift semantics when implementing support.

Verification context

Reproduced at ce7a2b737194434a4bc8ae12f7f51276faea8151 (liquidjava-verifier 0.0.35), with a clean working tree, Temurin JDK 21.0.8 on macOS.

Built using:

./mvnw compile -pl liquidjava-verifier -am -Dmaven.compiler.useIncrementalCompilation=false

Confirmed the minimal integer reproducer with ./liquidjava; ran the matrix in separate processes using the equivalent launcher:

./mvnw -q exec:java -pl liquidjava-verifier \
  -Dexec.mainClass=liquidjava.api.CommandLineLauncher \
  -Dexec.args=/path/to/Example.java

Related: #350 (closed), which reported the same error for ordinary bitwise/shift expressions in refined arguments. This report explicitly covers compound assignments, all six integer operators, and Boolean operands; the shared mapping remains incomplete at the tested commit.