Hacktoberfest 2026: die Issues, die Maintainer für den Oktober markiert haben – offen und einsteigerfreundlich. Hacktoberfest-Issues durchsuchen

Support bitwise and shift compound assignments without internal null errors

Offen
  • Stimmt etwas nicht?
#360 0 Kommentare 0 Reaktionen 0 zugewiesene Personen Auf GitHub ansehen

Maintainer antworten meist innerhalb von 1 Tag

Dieses Issue hat noch niemand übernommen.

Bewertung

Schwierigkeit
4/5
Geschätzter Aufwand
3-5 Tage
Anfängerfreundlichkeit
66/100
Issue-Typ
Bug
Klarheit
Klar beschrieben
Aktivitätsstatus
Aktiv
Tech-Stack
java
Bereich
compilers

Rechercherichtung

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.

Vom Indexierungsmodell aus dem Issue-Text verfasst.

Beschreibung

bug

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.

Vorherrschende Sprache
Java
Sterne
67
Forks
36
Ø Merge
2 T. 3 Std.
Gemergte PRs (30 T.)
29

Entwicklungsumgebung

Erste Schritte

  1. Lesen Sie das ganze Issue und danach den Beitragsleitfaden des Projekts.
  2. Schreiben Sie ins Issue, dass Sie es übernehmen — das erspart doppelte Arbeit.
  3. Forken Sie das Repository und arbeiten Sie in einem Branch.
  4. Öffnen Sie einen Pull Request, der die Issue-Nummer nennt.

Mehr aus liquid-java/liquidjava

Alle Issues in liquid-java/liquidjava

Ähnliche Issues

Weitere Issues zu Java

Neue Issues direkt in Ihr Postfach

Eine kurze Übersicht über anfängerfreundliche GitHub-Issues.