Hacktoberfest 2026: những issue maintainer đã đánh dấu cho tháng Mười, đang mở và phù hợp người mới. Xem issue Hacktoberfest

Support bitwise and shift compound assignments without internal null errors

Đang mở
  • Có gì không ổn?
#360 0 bình luận 0 reaction 0 người được giao Xem trên GitHub

Maintainer thường phản hồi trong vòng 1 ngày

Chưa có ai nhận issue này.

Đánh giá

Độ khó
4/5
Thời gian dự kiến
3-5 ngày
Mức phù hợp với người mới
66/100
Loại issue
Lỗi
Độ rõ ràng
Đặc tả rõ ràng
Mức độ hoạt động
Sôi nổi
Công nghệ
java
Lĩnh vực
compilers

Hướng nghiên cứu

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.

Do mô hình lập chỉ mục viết ra từ nội dung của issue.

Mô tả

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.

Ngôn ngữ chính
Java
Star
67
Fork
36
Merge trung bình
2 ngày 3 giờ
Pull request đã merge (30 ngày)
29

Chuẩn bị môi trường

Bắt đầu từ đâu

  1. Đọc hết issue, rồi đọc hướng dẫn đóng góp của dự án.
  2. Bình luận trên issue rằng bạn sẽ nhận — tránh hai người làm cùng một việc.
  3. Fork repository và làm thay đổi trên một nhánh.
  4. Mở pull request có tham chiếu số hiệu của issue.

Issue khác của liquid-java/liquidjava

Tất cả issue của liquid-java/liquidjava

Issue tương tự

Thêm issue về Java

Nhận issue mới trong hộp thư của bạn

Bản tóm tắt ngắn những issue GitHub phù hợp với người mới.