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

Soundness: short-circuit RHS assignments are treated as executed

Đang mở
  • Có gì không ổn?
#323 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 2 ngày

@CatarinaGamboa đang làm issue này rồi.

Từ ngày 2/10/2026.

  • #324 của @CatarinaGamboa — đang mở

Đá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
68/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 at RefinementTypeChecker.visitCtBinaryOperator and reproduce the false && and true || cases from the issue. Compare current main with the conservative fix in PR #257, then verify both operators, nested writes, and branches where the RHS runs or is skipped. Done means the invalid refinement is rejected without rejecting valid executed-RHS cases.

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

Mô tả

Problem

A write in the right operand of Java && or || is applied to LiquidJava's variable context even when Java short-circuits and does not execute that operand. The verifier can then prove a refinement about a value the program never assigned.

Minimal reproducer

import liquidjava.specification.Refinement;

public class Repro {
    public static void main(String[] args) {
        int x = 0;
        boolean ignored = false && ((x = 1) == 1);
        @Refinement("_ == 1") int y = x; // should be a Refinement Error
        assert y == 1;                    // fails: y is 0
    }
}

Expected: Reject the refinement on y. Java skips the RHS of &&, so x remains 0.

Actual: Correct! Passed Verification. on main at dd02e996. Compiling and running the program with assertions enabled throws AssertionError. The analogous true || RHS path has the same conditional-execution rule.

Cause and scope

RefinementTypeChecker.visitCtBinaryOperator scans both operands before applying the binary operation refinement. A RHS assignment updates the context during that scan; the later operator check does not distinguish a definitely executed write from a conditionally executed one.

The closed PR #257 contains a reproducer and a conservative fix. The fix should be ported and reviewed against current main, including both operators, nested writes, and branches where the RHS runs or is skipped. Example tests now use // Expect: Refinement Error after #293.

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

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.