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

Aperta
  • Qualcosa non va?
#471 0 commenti 0 reazioni 0 assegnatari Vedi su GitHub

I maintainer di solito rispondono entro 2 giorni

Nessuno ha ancora preso questa issue.

Valutazione

Difficoltà
4/5
Tempo stimato
3-5 giorni
Idoneità per principianti
52/100
Tipo di issue
Bug
Chiarezza
Specificata chiaramente
Stato di attività
Attiva
Stack tecnologico
java
Ambito
compilers

Direzione di ricerca

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.

Scritto dal modello di indicizzazione a partire dal testo della issue.

Descrizione

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

Lingua principale
Java
Stelle
71
Fork
37
Merge medio
1g 19h
PR unite (30g)
46

Preparare l'ambiente

Come iniziare

  1. Leggi tutta la issue e poi la guida ai contributi del progetto.
  2. Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
  3. Fai un fork del repository e lavora su un branch.
  4. Apri una pull request che faccia riferimento al numero della issue.

Altre issue di liquid-java/liquidjava

Tutte le issue di liquid-java/liquidjava

Issue simili

Altre issue su Java

Ricevi le nuove issue nella tua casella

Un breve riepilogo di issue GitHub adatte ai principianti.