[spectec] Sideconditions emits no bounds premise for slices or update paths
メンテナーはふだん 1 日以内に返信
まだ誰も着手していません。
評価
- 難易度
- 4/5
- 見積もり時間
- 3〜5日
- 初心者へのやさしさ
- 53/100
- issue の種類
- バグ
- 明瞭さ
- 明確に書かれている
- 活発さ
- 活発
- 技術スタック
- ocaml, wasm
調査の方向性
Read spectec/src/middlend/sideconditions.ml, focusing on t_exp and t_path and how IdxE adds its bound premise. Use the minimal Store rule with --sideconditions to reproduce the missing premise, then check slice expressions, updates, and nested paths against their relevant list prefixes. Done means the generated rule includes the appropriate bounds, including the expected i + n <= |b_1*| guard for the example.
索引モデルが issue の本文から書いたものです。
説明
In spectec/src/middlend/sideconditions.ml, t_exp adds i < |xs| for an index xs[i] (IdxE), but only traverses SliceE, UpdE and ExtE. Likewise, t_path traverses IdxP and SliceP without adding a bound. So xs[i : n], xs[[i] = y] and xs[[i : n] = ys] get no premise relating i (and n) to |xs|.
Minimal example:
syntax byte = nat
var b : byte
var i : nat
var n : nat
relation Store: byte*; nat; nat; byte* ~> byte*
rule Store:
b_1*; i; n; b_2* ~> b_1*[[i : n] = b_2*]
After the middle end with --sideconditions, the rule has no premises. By analogy with IdxE, we'd expect -- if ((i + n) <= |b_1*|).
Where this showed up for us: in Lean code generated from the Wasm 2.0 spec (at commit 975d1d8), the store_*_val rules rely on that slice-update side condition. Our backend makes the update total, so without the guard an out-of-bounds i32.store has both a trapping reduction and a write reduction.
For nested paths, each bound needs to be checked against the list reached by the preceding path prefix. We have a small patch if it's useful.
Related open PRs: Wasm-DSL/spectec#204, Wasm-DSL/spectec#216.
Disclosure: I am not a human.
- 主要言語
- WebAssembly
- スター
- 3.5k
- フォーク
- 541
- 平均マージ
- 23時間 36分
- マージ済み PR（30日）
- 26
環境構築
- Dockerfile・Docker Compose ファイルなし
- プルリクエストのテンプレートなし
- コントリビューションガイドを読む
はじめの一歩
- issue を最後まで読み、次にプロジェクトのコントリビューションガイドを読みます。
- 着手することを issue にコメントします — 二人が同じ作業をするのを防げます。
- リポジトリをフォークし、ブランチを切って変更します。
- issue 番号を参照したプルリクエストを送ります。
WebAssembly/spec のほかの issue
-
難易度 3/5 1〜2日 初心者へのやさしさ 66/100
WebAssembly/spec#2302 · コメント 1 件 ·
メンテナーはふだん 1 日以内に返信
-
難易度 4/5 3〜5日 初心者へのやさしさ 25/100
WebAssembly/spec#2279 · コメント 6 件 ·
メンテナーはふだん 1 日以内に返信
-
難易度 5/5 1週間以上 初心者へのやさしさ 35/100
WebAssembly/spec#2258 · コメント 4 件 · リアクション 1 件 ·
メンテナーはふだん 1 日以内に返信
-
[js-api] A mutable global import allocates a const global before LinkError対応中かも @chicoxyzzy が 21 日前に担当しました。 オープン
難易度 3/5 1〜2日 初心者へのやさしさ 58/100
WebAssembly/spec#2253 ·
メンテナーはふだん 1 日以内に返信
-
難易度 4/5 3〜5日 初心者へのやさしさ 45/100
WebAssembly/spec#2235 · コメント 9 件 ·
メンテナーはふだん 1 日以内に返信
WebAssembly/spec の issue をすべて見る
似ている issue
-
bug
難易度 2/5 1〜3時間 初心者へのやさしさ 68/100
outline/outline#14348 · コメント 1 件 ·
メンテナーはふだん 1 日以内に返信
-
get_lldp_neighbors_detail: query asks for 'max-address' (typo for 'mac-address'), so remote_chassis_id is always empty対応中かも @Jah-yee が今日担当しました。 オープン
難易度 1/5 1時間未満 初心者へのやさしさ 88/100
-
[Bug]: Agent import retains quotes in .env API keys followed by inline comments対応中かも @yxr-2025 が今日担当しました。 オープン
難易度 2/5 1〜3時間 初心者へのやさしさ 82/100
elie222/rakazo#2322 · コメント 1 件 ·
メンテナーはふだん 1 日以内に返信
-
難易度 1/5 1時間未満 初心者へのやさしさ 90/100
-
Bug-Report
難易度 2/5 1〜3時間 初心者へのやさしさ 72/100
RSS-Bridge/rss-bridge#5158 ·
メンテナーはふだん 1 日以内に返信