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

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

Maintainer antworten meist innerhalb von 2 Tagen

Dieses Issue hat noch niemand übernommen.

Bewertung

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

Rechercherichtung

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.

Vom Indexierungsmodell aus dem Issue-Text verfasst.

Beschreibung

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

Vorherrschende Sprache
Java
Sterne
71
Forks
37
Ø Merge
1 T. 19 Std.
Gemergte PRs (30 T.)
46

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.