Crash: "Sorts Int and Bool are incompatible" when a JDK method's result is passed to a parameter refined in an external spec
メンテナーはふだん 2 日以内に返信
まだ誰も着手していません。
評価
- 難易度
- 4/5
- 見積もり時間
- 3〜5日
- 初心者へのやさしさ
- 52/100
- issue の種類
- バグ
- 明瞭さ
- おおむね明確
- 活発さ
- 活発
- 技術スタック
- java
- 領域
- compilers, testing-qa
調査の方向性
Start by reproducing the crash with the provided SocketRefinements.java and Client.java example, then compare it with the in-source refinement case that reports a normal refinement error. Trace how results from unspecified JDK methods and externally refined parameters are translated into verifier sorts. Done means the example reports a refinement error or verifies, without the internal sort error; the literal-port case should continue to verify.
索引モデルが issue の本文から書いたものです。
説明
Impact: passing an int returned by an unspecified JDK method to a parameter refined in an external spec crashes the verifier with an internal sort error. The expected outcome is a refinement error, or an accept. This is the everyday way to connect a socket in tests and tools: new Socket(host, server.getLocalPort()).
Minimal reproducer (an external spec and a client, in one directory)
// SocketRefinements.java
@ExternalRefinementsFor("java.net.Socket")
public interface SocketRefinements {
void Socket(InetAddress address, @Refinement("_ >= 0 && _ <= 65535") int port);
}
// Client.java
public class Client {
public static void main(String[] args) throws Exception {
ServerSocket server = new ServerSocket(0);
Socket s = new Socket(InetAddress.getLoopbackAddress(), server.getLocalPort());
server.close();
}
}
Expected: a refinement error, because server.getLocalPort() can't be proved in range. The same shape in-source gives one: port³ == port¹ is not a subtype of port³ >= 0 && port³ <= 65535.
Actual (main @ f7f366c, and 1a506fe):
Error: Sorts Int and Bool are incompatible
With a literal port (8080) the program verifies.
Real-world scenario. I found this while scoring java.net.Socket specs on JVM-checked probes. Every probe that connects to a local test server (new ServerSocket(0), then new Socket(loopback, server.getLocalPort())) crashes the verifier. That happens both with co-specification's generated spec and with the specs-v2 Socket spec, which refines ports the same way (Port(int x) { x >= 0 && x <= 65535 }).
- 主要言語
- Java
- スター
- 71
- フォーク
- 37
- 平均マージ
- 1日 19時間
- マージ済み PR（30日）
- 57
環境構築
- Dockerfile・Docker Compose ファイルなし
- プルリクエストのテンプレートあり
- コントリビューションガイドを読む
はじめの一歩
- issue を最後まで読み、次にプロジェクトのコントリビューションガイドを読みます。
- 着手することを issue にコメントします — 二人が同じ作業をするのを防げます。
- リポジトリをフォークし、ブランチを切って変更します。
- issue 番号を参照したプルリクエストを送ります。
liquid-java/liquidjava のほかの issue
-
難易度 2/5 1〜3時間 初心者へのやさしさ 72/100
liquid-java/liquidjava#443 ·
メンテナーはふだん 2 日以内に返信
-
bug real-world-finding
難易度 2/5 1〜3時間 初心者へのやさしさ 82/100
liquid-java/liquidjava#395 ·
メンテナーはふだん 2 日以内に返信
-
enhancement
難易度 2/5 1〜3時間 初心者へのやさしさ 65/100
liquid-java/liquidjava#373 ·
メンテナーはふだん 2 日以内に返信
-
External specs: a @StateSet declared later in the file is not found by an interface earlier in itオープン
難易度 4/5 3〜5日 初心者へのやさしさ 58/100
liquid-java/liquidjava#452 ·
メンテナーはふだん 2 日以内に返信
-
難易度 4/5 1〜2日 初心者へのやさしさ 58/100
liquid-java/liquidjava#450 ·
メンテナーはふだん 2 日以内に返信
liquid-java/liquidjava の issue をすべて見る
似ている issue
-
[Bug] 资源包列表 与 模组/数据包/世界 列表排列顺序不一致対応中かも @fishdry1000 が 3 日前に担当しました。 オープンbug
難易度 2/5 1〜3時間 初心者へのやさしさ 62/100
メンテナーはふだん 1 日以内に返信
-
難易度 2/5 1〜3時間 初心者へのやさしさ 82/100
AtlasOfLivingAustralia/species-lists#882 ·
メンテナーはふだん 1 日以内に返信
-
Type/Bug
難易度 2/5 1〜3時間 初心者へのやさしさ 62/100
ballerina-platform/ballerina-library#9458 ·
メンテナーはふだん 1 日以内に返信
-
難易度 2/5 1〜3時間 初心者へのやさしさ 68/100
winder/Universal-G-Code-Sender#3242 ·
メンテナーはふだん 1 日以内に返信
-
難易度 2/5 1〜3時間 初心者へのやさしさ 68/100
PCL-Community/PCL-CE#3767 ·
メンテナーはふだん 1 日以内に返信