# 通知設計書 50-warnProveIndex

## 概要

本ドキュメントは、Nimコンパイラの警告メッセージ `warnProveIndex`（インデックス証明警告）に関する設計書です。

### 本通知の処理概要

この警告は、Nimコンパイラが配列やシーケンスへのインデックスアクセスが有効な範囲内であることを静的に証明できない場合に発生する警告メッセージです。配列の境界外アクセスを検出し、潜在的なランタイムエラーを防止します。

**業務上の目的・背景**：配列やシーケンスへの境界外アクセスは、プログラムのクラッシュやメモリ破損、セキュリティ脆弱性の原因となります。Nimコンパイラは静的境界チェック（optStaticBoundsCheck）が有効な場合、インデックスの有効性を静的に検証します。この警告により、開発者はコンパイル時に潜在的な境界外アクセスを発見し、適切な範囲チェックを追加することができます。

**通知の送信タイミング**：コンパイル時のエフェクト解析フェーズ（sempass2.nim）において、`optStaticBoundsCheck`が有効な状態で配列アクセス（mArrGet, mArrPut）が解析される際に、インデックスの有効性を証明できない場合に警告が発生します。また、warnStaticIndexCheckを通じて同様の警告が出力されることもあります。

**通知の受信者**：Nimプログラムをコンパイルする開発者がこの警告を受け取ります。コンパイラの標準出力または標準エラー出力に警告メッセージが表示されます。

**通知内容の概要**：「cannot prove index '式' is valid」というメッセージが表示され、有効性を証明できないインデックス式を特定します。

**期待されるアクション**：開発者は、該当するインデックスアクセスの前に適切な範囲チェック（if文での境界確認など）を追加するか、インデックスが常に有効範囲内であることを保証するようにコードを修正することが期待されます。

## 通知種別

コンパイラ警告（Warning）

## 送信仕様

### 基本情報

| 項目 | 内容 |
|-----|------|
| 送信方式 | 同期（コンパイル時） |
| 優先度 | 中（警告レベル） |
| リトライ | なし |

### 送信先決定ロジック

コンパイラを実行している開発者のコンソールに直接出力されます。警告の有効/無効は `--warning[ProveIndex]:on/off` オプションで制御可能です。デフォルトではverbosityレベル1では無効です。

## 通知テンプレート

### コンパイラ警告の場合

| 項目 | 内容 |
|-----|------|
| メッセージID | ProveIndex |
| 警告レベル | Warning |
| 形式 | テキスト |

### 本文テンプレート

```
{ファイル名}({行番号}, {列番号}) Warning: cannot prove index '{式}' is valid [ProveIndex]
```

### 添付ファイル

該当なし（コンパイラ警告のため添付ファイルは存在しない）

## テンプレート変数

| 変数名 | 説明 | データ取得元 | 必須 |
|--------|------|-------------|-----|
| ファイル名 | ソースファイルのパス | TLineInfo.fileIndex | Yes |
| 行番号 | 警告発生行 | TLineInfo.line | Yes |
| 列番号 | 警告発生列 | TLineInfo.col | Yes |
| 式 | 有効性を証明できないインデックス式 | $idx（インデックス値） | Yes |

## 送信トリガー・条件

### トリガー一覧

| トリガー種別 | トリガーイベント | 送信条件 | 説明 |
|------------|----------------|---------|------|
| コンパイル時 | 配列アクセス解析 | optStaticBoundsCheck有効 | sempass2.nim:1144-1146行目 |

### 送信抑止条件

| 条件 | 説明 |
|-----|------|
| `--warning[ProveIndex]:off` | コマンドラインオプションで警告を無効化 |
| `{.warning[ProveIndex]:off.}` | プラグマで警告を無効化 |
| verbosityレベル0または1 | デフォルトでは無効 |
| optStaticBoundsCheckが無効 | 静的境界チェックが無効の場合 |

## 処理フロー

### 送信フロー

```mermaid
flowchart TD
    A[配列アクセス検出] --> B{optStaticBoundsCheck有効?}
    B -->|No| C[通常処理]
    B -->|Yes| D[checkBounds呼び出し]
    D --> E[checkLe: lowBound <= idx]
    E --> F{proveLe結果}
    F -->|impYes| G[次のチェック]
    F -->|impNo/impUnknown| H[warnStaticIndexCheck発行]
    G --> I[checkLe: idx <= highBound]
    I --> J{proveLe結果}
    J -->|impYes| C
    J -->|impNo/impUnknown| H
    H --> C
```

## データベース参照・更新仕様

### 参照テーブル一覧

該当なし（コンパイラ内部処理のため外部データベース参照なし）

### 内部データ構造

| データ構造 | 用途 | 備考 |
|-----------|------|------|
| TModel（guards） | ガード条件の集合 | 数学的関係の証明に使用 |

### 更新テーブル一覧

該当なし

## エラー処理

### エラーケース一覧

| エラー種別 | 発生条件 | 対処方法 |
|----------|---------|---------|
| 該当なし（警告のみ） | - | - |

### リトライ仕様

| 項目 | 内容 |
|-----|------|
| リトライ回数 | 0（リトライなし） |
| リトライ間隔 | - |
| リトライ対象エラー | - |

## 配信設定

### レート制限

| 項目 | 内容 |
|-----|------|
| 1分あたり上限 | 制限なし |
| 1日あたり上限 | 制限なし |

### 配信時間帯

コンパイル実行時に即座に出力される（時間帯制限なし）

## セキュリティ考慮事項

- 配列の境界外アクセスは、バッファオーバーフローによるセキュリティ脆弱性の主要な原因
- 境界外読み取りは情報漏洩につながる可能性がある
- 境界外書き込みはコード実行の脆弱性につながる可能性がある
- この警告に注意を払うことで、より安全なコードを書くことができる

## 備考

- `--staticBoundsCheck:on`オプションでoptStaticBoundsCheckを有効化できる
- warnStaticIndexCheckはより詳細なメッセージを出力（「cannot prove: a <= b」など）
- verbosityレベル2以上で有効になる（NotesVerbosity配列で制御）
- proveLe関数は、ガード条件から不等式を証明する
- 現在、warnProveIndexは定義されているが直接使用されていない可能性がある（warnStaticIndexCheckで代替）

---

## コードリーディングガイド

本通知を理解するために参照すべきファイルと、推奨する読み解き順序を以下に示す。

### 推奨読解順序

#### Step 1: データ構造を理解する

まず、警告メッセージの種類を定義するデータ構造を理解することが重要です。

| 順序 | ファイル | パス | 読解ポイント |
|-----|---------|------|-------------|
| 1-1 | lineinfos.nim | `compiler/lineinfos.nim` | TMsgKind列挙型でwarnProveIndexの定義を確認（70行目） |
| 1-2 | lineinfos.nim | `compiler/lineinfos.nim` | MsgKindToStr配列で警告メッセージテンプレートを確認（172行目） |
| 1-3 | lineinfos.nim | `compiler/lineinfos.nim` | NotesVerbosityでverbosity制御を確認（267行目） |

**読解のコツ**: warnProveIndexとwarnStaticIndexCheckは関連する警告で、共にverbosityレベル1以下では無効になります。

#### Step 2: 境界チェックのエントリーポイントを理解する

sempass2.nimでの呼び出しを確認します。

| 順序 | ファイル | パス | 読解ポイント |
|-----|---------|------|-------------|
| 2-1 | sempass2.nim | `compiler/sempass2.nim` | 1144-1146行目でmArrGet, mArrPutの処理を確認 |
| 2-2 | sempass2.nim | `compiler/sempass2.nim` | 992-994行目でcheckBounds関数を確認 |
| 2-3 | sempass2.nim | `compiler/sempass2.nim` | 979-990行目でcheckLe関数を確認 |

**主要処理フロー**:
1. **1144行目**: `a.sym.magic in {mArrGet, mArrPut}`で配列アクセスを検出
2. **1145行目**: `optStaticBoundsCheck in tracked.currOptions`で静的チェックが有効かを確認
3. **1146行目**: `checkBounds(tracked, n[1], n[2])`で境界チェックを実行

#### Step 3: checkLe関数を理解する

不等式の証明と警告発行を確認します。

| 順序 | ファイル | パス | 読解ポイント |
|-----|---------|------|-------------|
| 3-1 | sempass2.nim | `compiler/sempass2.nim` | checkLe関数（979-990行目）を確認 |

**主要処理フロー**:
1. **979行目**: checkLe関数の定義
2. **980行目**: `proveLe(c.guards, a, b)`で不等式を証明
3. **981行目**: `impUnknown`の場合は「cannot prove」メッセージ
4. **984-985行目**: warnStaticIndexCheckで警告を発行
5. **988-990行目**: `impNo`の場合は「can prove: a > b」メッセージ

### プログラム呼び出し階層図

```
sempass2.nim::trackCall()
    │
    └─ mArrGet, mArrPut検出（1144行目）
           │
           └─ optStaticBoundsCheck有効?（1145行目）
                  │
                  └─ checkBounds(arr, idx)（1146行目）
                         │
                         ├─ checkLe(lowBound, idx)（993行目）
                         │      │
                         │      └─ proveLe()
                         │             │
                         │             └─ impUnknown/impNo: warnStaticIndexCheck
                         │
                         └─ checkLe(idx, highBound)（994行目）
                                │
                                └─ proveLe()
                                       │
                                       └─ impUnknown/impNo: warnStaticIndexCheck
```

### データフロー図

```
[入力]                              [処理]                         [出力]

arr[idx]
    │
    ▼
配列アクセス検出 ───▶ checkBounds(arr, idx)
                           │
                           ├─ lowBound(arr) ← arr.low
                           ├─ highBound(arr) ← arr.high
                           │
                           └─ proveLe(guards, low, idx)?
                                  │
                                  └─ impUnknown ───▶ 警告メッセージ
                                                 "cannot prove: low <= idx"
```

### 関連ファイル一覧

| ファイル | パス | 種別 | 役割 |
|---------|------|------|------|
| lineinfos.nim | `compiler/lineinfos.nim` | ソース | 警告種別の定義とメッセージテンプレート |
| sempass2.nim | `compiler/sempass2.nim` | ソース | 配列アクセス検出と境界チェック |
| guards.nim | `compiler/guards.nim` | ソース | proveLe関数（不等式証明） |
| msgs.nim | `compiler/msgs.nim` | ソース | メッセージ出力機能 |
