Verifier crashes on a `for` loop whose body is an empty statement (`for (...) ;`)
メンテナーはふだん 2 日以内に返信
まだ誰も着手していません。
評価
調査の方向性
クラッシュは src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java の visitCtFor で発生しています。そこではラムダが約628行目で CtFor.getBody() に対して getElements を呼び出しています。同じ経路は約658行目の visitLoop も通ります。まず、そこでループ本体がどのように処理されているかを読み、次に issue にある再現コードを実行してください。この再現コードは空の ; 本体を持っています。再現コードが Correct! Passed Verification. を出力し、既存のループテストが引き続き成功すれば完了です。
索引モデルが issue の本文から書いたものです。
説明
Impact: verification stops with an internal error on any for loop whose body is an empty statement (;).
Description
for (...; ...; ...) ; has no body block: CtFor.getBody() is null, and RefinementTypeChecker.visitCtFor calls getElements on it (RefinementTypeChecker.java:628). Nothing in the loop needs a refinement, so an empty body could be checked as an empty block.
Minimal reproducer
public class Repro {
static int total(int[] counts) {
int total = 0;
for (int i = 0; i < counts.length; total += counts[i], i++)
;
return total;
}
}
Expected
Correct! Passed Verification.
Actual
Exception in thread "main" java.lang.RuntimeException:
Error while checking CtMethodImpl
on total(int[] counts) {
at Repro.java:2
with
Error while checking CtBlockImpl
on {
at Repro.java:2
with
Error while checking CtForImpl
on for (int i = 0; i < counts.length; total += counts[i], i++)
at Repro.java:4
with Cannot invoke "spoon.reflect.code.CtStatement.getElements(spoon.reflect.visitor.Filter)" because the return value of "spoon.reflect.code.CtFor.getBody()" is null
...
Caused by: java.lang.NullPointerException: Cannot invoke "spoon.reflect.code.CtStatement.getElements(spoon.reflect.visitor.Filter)" because the return value of "spoon.reflect.code.CtFor.getBody()" is null
at liquidjava.processor.refinement_checker.RefinementTypeChecker.lambda$visitCtFor$4(RefinementTypeChecker.java:628)
at liquidjava.processor.refinement_checker.RefinementTypeChecker.visitLoop(RefinementTypeChecker.java:658)
at liquidjava.processor.refinement_checker.RefinementTypeChecker.visitCtFor(RefinementTypeChecker.java:623)
Reproduced on main at ad055b49 (liquidjava-verifier 0.0.35).
Real-world file that hits it
for (int i = 0; i < updateCount.length; cnt += updateCount[i], i++) ;— tejeswarp/tungsten-replicator (file)
Context
Found while running LiquidJava on the original repository files of 53 real-world typestate and refinement bugs (the files our study exercises were simplified from). Each file is verified on its own, as a user would verify one file of a project, so the project's other classes and its dependencies are not on the classpath.
- 主要言語
- Java
- スター
- 69
- フォーク
- 36
- 平均マージ
- 2日 1時間
- マージ済み PR(30日)
- 35
環境構築
- Dockerfile・Docker Compose ファイルなし
- プルリクエストのテンプレートあり
- コントリビューションガイドを読む
はじめの一歩
- issue を最後まで読み、次にプロジェクトのコントリビューションガイドを読みます。
- 着手することを issue にコメントします — 二人が同じ作業をするのを防げます。
- リポジトリをフォークし、ブランチを切って変更します。
- issue 番号を参照したプルリクエストを送ります。
liquid-java/liquidjava のほかの issue
-
Verifier crashes on a comparison or other binary operator whose operand types cannot be resolved (classes not on the classpath)対応中かも @CatarinaGamboa が 3 日前に担当しました。 オープンbug
難易度 2/5 1〜3時間 初心者へのやさしさ 72/100
liquid-java/liquidjava#388 ·
メンテナーはふだん 2 日以内に返信
-
enhancement
難易度 2/5 1〜3時間 初心者へのやさしさ 65/100
liquid-java/liquidjava#373 ·
メンテナーはふだん 2 日以内に返信
-
Soundness: a local variable with a constant's name shadows the constant (Format.JPG read as local JPG)対応中かも @CatarinaGamboa が 3 日前に担当しました。 オープンbug
難易度 2/5 1〜3時間 初心者へのやさしさ 78/100
liquid-java/liquidjava#321 ·
メンテナーはふだん 2 日以内に返信
-
bug
難易度 4/5 3〜5日 初心者へのやさしさ 20/100
liquid-java/liquidjava#406 ·
メンテナーはふだん 2 日以内に返信
-
bug
難易度 4/5 3〜5日 初心者へのやさしさ 40/100
liquid-java/liquidjava#405 ·
メンテナーはふだん 2 日以内に返信
liquid-java/liquidjava の issue をすべて見る
似ている issue
-
bug
難易度 2/5 1〜3時間 初心者へのやさしさ 72/100
scylladb/scylla-cdc-source-connector#350 ·
メンテナーはふだん 1 日以内に返信
-
agent:working documentation enhancement go:build lane:needs-decision
難易度 2/5 1〜3時間 初心者へのやさしさ 72/100
Sanne/incus-spawn#1435 · コメント 3 件 ·
メンテナーはふだん 1 日以内に返信
-
area:shuffle bug priority:high requires-triage
難易度 2/5 1〜3時間 初心者へのやさしさ 72/100
apache/datafusion-comet#7062 ·
メンテナーはふだん 1 日以内に返信
-
wait for review
難易度 2/5 1〜3時間 初心者へのやさしさ 68/100
メンテナーはふだん 1 日以内に返信
-
enhancement good first issue up-for-grabs
難易度 2/5 1〜3時間 初心者へのやさしさ 80/100
AnikethTS/ChangeRadar#22 ·
メンテナーはふだん 1 日以内に返信