Counterexample: a guard stored in a boolean (boolean bad = a || b || c; if (bad) return;) is not split, so every variable of the guard is listed

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

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
52/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 by reading RefinementError.factsOf and how boolean definitions and negated facts are handled; the issue identifies linkedTerms and isKnown as relevant. Run the supplied Java reproducer and compare its counterexample with the expected timeout == -1. Done when the stored-boolean guard produces the expected minimal counterexample without unrelated guard variables or the generated name.

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

Mô tả

bug error messages

Impact: when a guard is stored in a boolean before the if, the counterexample lists values for every variable of the guard and for a generated name, instead of only the value that breaks the call. Seen on the branch of #460 (pending merge), which fixes this for an inline guard; on main the counterexample for this input has the same noise and also leaves out timeout (#453).

Minimal reproducer

import liquidjava.specification.Refinement;

public class Probe {
    static void connect(@Refinement("_ >= 0") int timeout) {}

    static void probe(int port, int retries, int timeout) {
        boolean bad = port < 0 || retries < 0 || timeout > 60000;
        if (bad) return;
        connect(timeout);
    }
}

Expected: Counterexample: timeout == -1, as with the inline guard if (port < 0 || retries < 0 || timeout > 60000) return;, which on #460's branch (712759fe) gives:

Refinement Error: !(port < 0 || retries < 0 || timeout > 60000) is not a subtype of timeout >= 0
 --> Counterexample: timeout == -1

Actual (#460's branch @ 712759fe):

Refinement Error: #fresh⁹ == (port < 0 || retries < 0 || timeout > 60000) && !#fresh⁹ is not a subtype of timeout >= 0
 7 |         boolean bad = port < 0 || retries < 0 || timeout > 60000;
 8 |         if (bad) return;
 9 |         connect(timeout);
   |         ^^^^^^^^^^^^^^^^^
10 |     }
11 | }
 --> Counterexample: timeout == -1 && port == 0 && retries == 0 && #fresh⁹ == false

main @ 0053074e prints the same Found with Counterexample: port == 0 && retries == 0 && #fresh⁹ == false.

Cause. On #460's branch, RefinementError.factsOf splits !(a || b) into !a and !b, but here found is #fresh == (a || b || c) && !#fresh. The definition is one fact that shares terms with everything, so linkedTerms pulls in port, retries and #fresh. isKnown only recognises x == v facts, so !#fresh does not hide #fresh == false. Substituting a boolean defined as x == e into !x (giving !e) before splitting would give the same facts as the inline guard. Separately, found names the local bad as #fresh⁹.

🤖 Generated with Claude Code

Ngôn ngữ chính
Java
Star
71
Fork
37
Merge trung bình
1 ngày 19 giờ
Pull request đã merge (30 ngày)
46

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.