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

Abierto
  • ¿Algo no está bien?
#471 0 comentarios 0 reacciones 0 asignados Ver en GitHub

Los mantenedores suelen responder en 2 días

Nadie ha tomado este issue todavía.

Evaluación

Dificultad
4/5
Tiempo estimado
3-5 días
Aptitud para principiantes
52/100
Tipo de issue
Error
Claridad
Bien especificado
Estado de actividad
Activo
Stack tecnológico
java
Área
compilers

Línea de trabajo

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.

Escrito por el modelo de indexación a partir del texto del issue.

Descripción

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

Lenguaje dominante
Java
Estrellas
71
Forks
37
Merge medio
1 d 19 h
PR fusionados (30 d)
46

Preparar el entorno

Primeros pasos

  1. Lee el issue completo y luego la guía de contribución del proyecto.
  2. Comenta en el issue que vas a ocuparte — evita que dos personas hagan lo mismo.
  3. Haz un fork del repositorio y trabaja en una rama.
  4. Abre un pull request que haga referencia al número del issue.

Más de liquid-java/liquidjava

Todos los issues de liquid-java/liquidjava

Issues similares

Más issues de Java

Recibe los nuevos issues en tu correo

Un resumen breve de issues de GitHub para principiantes.