Hacktoberfest 2026: as issues que os mantenedores marcaram para outubro, abertas e boas para iniciantes. Ver issues do Hacktoberfest

Support bitwise and shift compound assignments without internal null errors

Aberta
  • Algo errado?
#360 0 comentários 0 reações 0 responsáveis Ver no GitHub

Mantenedores costumam responder em até 1 dia

Ninguém assumiu esta issue ainda.

Avaliação

Dificuldade
4/5
Tempo estimado
3-5 dias
Facilidade para iniciantes
66/100
Tipo de issue
Bug
Clareza
Claramente especificada
Status de atividade
Ativa
Stack de tecnologia
java
Domínio
compilers

Direção de pesquisa

Start in liquidjava-verifier/.../refinement_checker/general_checkers/OperationsChecker.java: getOperatorFromKind (~L444) returns null for Spoon BITAND/BITOR/BITXOR/SL/SR/USR, and getOperatorAssignmentRefinement (~L107) passes that null into Predicate.createOperation. Trace how the already-working += and %= compound assignments flow through Ops and ExpressionToZ3Visitor.visitBinaryExpression, then add the missing operator cases plus a guard for unsupported operators before expression construction. Done = the ./liquidjava CompoundAnd.java reproducer prints Correct! Passed Verification, an incorrect refinement reports a Refinement Error instead of the null error, and the CorrectOperatorAssignments suite gains cases for all six integer and three Boolean compound operators.

Escrita pelo modelo de indexação a partir do texto da issue.

Descrição

bug

Problem

Bitwise and shift compound assignments produce an internal null error when LiquidJava needs to check a refinement involving their result. This affects all six remaining integer compound operators (&=, |=, ^=, <<=, >>=, >>>=) and Boolean &=, |=, ^=.

Integer +=, -=, *=, /=, and %= already work in the tested cases. The existing CorrectOperatorAssignments suite also covers %=.

Reproduction

Save as CompoundAnd.java and run ./liquidjava CompoundAnd.java from the repository root:

import liquidjava.specification.Refinement;

public class CompoundAnd {
    @Refinement("_ == 2")
    int test() {
        int x = 6;
        x &= 3;
        return x;
    }
}

Expected: Correct! Passed Verification. because 6 & 3 == 2.

Actual:

Error: Cannot invoke "String.hashCode()" because "<local4>" is null
5 |         int x = 6;
6 |         x &= 3;
7 |         return x;
  |         ^^^^^^^^^

Changing the return refinement to _ != 2 also produces the internal error, instead of a Refinement Error. Removing the return refinement produces Correct! Passed Verification.; accepting that unrefined example does not demonstrate support for checking the operation's result.

Boolean reproducer:

import liquidjava.specification.Refinement;

public class CompoundBooleanAnd {
    @Refinement("_ == false")
    boolean test() {
        boolean x = true;
        x &= false;
        return x;
    }
}

This produces the same null error.

Results from running examples

For each row, ran three separate Java files: a correct return refinement _ == expected, an incorrect return refinement _ != expected, and no return refinement. All files compile with javac.

Type Initial value Assignment Expected result Correct refinement Incorrect refinement No refinement
int 10 x += 2 12 Pass Refinement Error Pass
int 10 x -= 2 8 Pass Refinement Error Pass
int 10 x *= 2 20 Pass Refinement Error Pass
int 10 x /= 2 5 Pass Refinement Error Pass
int 10 x %= 3 1 Pass Refinement Error Pass
int 6 x &= 3 2 Internal null error Internal null error Pass
int 6 `x = 3` 7 Internal null error Internal null error
int 6 x ^= 3 5 Internal null error Internal null error Pass
int 6 x <<= 1 12 Internal null error Internal null error Pass
int -8 x >>= 1 -4 Internal null error Internal null error Pass
int -8 x >>>= 1 2147483644 Internal null error Internal null error Pass
boolean true x &= false false Internal null error Internal null error Pass
boolean false `x = true` true Internal null error Internal null error
boolean true x ^= true false Internal null error Internal null error Pass

Also reproduced the same null error with &= when:

  • The target itself is refined: @Refinement("_ >= 0") int x = 6; x &= 3;.
  • Its result initializes a refined local: int x = 6; x &= 3; @Refinement("_ == 2") int y = x;.
  • Its result is passed to a refined parameter: int x = 6; x &= 3; take(x);, where take requires _ == 2.

The diagnostic may therefore appear on the assignment or on a later use. The CLI prints this error but returns exit status 0 (and the Maven launcher reports build success).

String += was also probed, but is excluded from this operator matrix: String x = "a"; x += "b"; with a refined return reports Not Found Error: Variable 'b' could not be found. A plain refined return "ab" and ordinary string concatenation also fail with incompatible String sorts, so string support requires separate investigation.

Missing implementation

Source inspection explains the operator matrix:

  • OperationsChecker.getOperatorFromKind has no cases for Spoon BITAND, BITOR, BITXOR, SL, SR, or USR; it returns null. AND and OR there are the logical operators, not the kinds used by &= and |=.
  • getOperatorAssignmentRefinement passes that null operator into Predicate.createOperation, constructing a malformed BinaryExpression that fails during subsequent refinement processing.
  • Ops and ExpressionToZ3Visitor.visitBinaryExpression also lack bitwise/shift operations. Adding only the Spoon mappings would not implement the missing semantics.

Needed: integral bitwise/shift semantics, Boolean &/|/^ semantics, safe handling of unsupported operators before constructing expressions, and regression coverage for successful verification and expected refinement violations. Preserve Java's eager Boolean evaluation and integer width/shift semantics when implementing support.

Verification context

Reproduced at ce7a2b737194434a4bc8ae12f7f51276faea8151 (liquidjava-verifier 0.0.35), with a clean working tree, Temurin JDK 21.0.8 on macOS.

Built using:

./mvnw compile -pl liquidjava-verifier -am -Dmaven.compiler.useIncrementalCompilation=false

Confirmed the minimal integer reproducer with ./liquidjava; ran the matrix in separate processes using the equivalent launcher:

./mvnw -q exec:java -pl liquidjava-verifier \
  -Dexec.mainClass=liquidjava.api.CommandLineLauncher \
  -Dexec.args=/path/to/Example.java

Related: #350 (closed), which reported the same error for ordinary bitwise/shift expressions in refined arguments. This report explicitly covers compound assignments, all six integer operators, and Boolean operands; the shared mapping remains incomplete at the tested commit.

Linguagem predominante
Java
Estrelas
67
Forks
36
Merge médio
2d 3h
PRs com merge (30d)
29

Preparar o ambiente

Primeiros passos

  1. Leia a issue inteira e depois o guia de contribuição do projeto.
  2. Comente na issue dizendo que vai assumir — evita que duas pessoas façam o mesmo trabalho.
  3. Faça um fork do repositório e trabalhe em uma branch.
  4. Abra um pull request que referencie o número da issue.

Mais de liquid-java/liquidjava

Todas as issues de liquid-java/liquidjava

Issues semelhantes

Mais issues de Java

Receba novas issues na sua caixa de entrada

Um resumo curto de issues do GitHub para quem está começando.