# 通知設計書 53-warnStaticIndexCheck

## 概要

本ドキュメントは、Nimコンパイラの警告通知「warnStaticIndexCheck」（静的インデックスチェック）の設計仕様を記載する。この警告は、配列やシーケンスのインデックスアクセスにおいて、コンパイル時に境界違反を検出したり、境界内であることを証明できない場合に発生する。

### 本通知の処理概要

**業務上の目的・背景**：この警告は、配列の境界外アクセス（バッファオーバーフロー/アンダーフロー）をコンパイル時に検出することを目的としている。静的解析により、実行時エラーを未然に防ぎ、安全なコードの作成を支援する。特に並列処理（parallel文）においては、複数のスライスが重複しないことを証明する必要があり、この警告はその証明に失敗した場合にも発生する。これにより、データ競合の可能性を事前に警告できる。

**通知の送信タイミング**：コンパイル時のエフェクト解析フェーズ（sempass2.nim）および並列処理解析フェーズ（semparallel.nim）において発生する。具体的には、インデックスアクセスや配列スライスの境界チェック時に、数学的証明システム（guards.nim）を使用して検証が行われる。

**通知の受信者**：この警告はコンパイルを実行した開発者に対して、標準エラー出力またはコンパイラが設定した出力先に通知される。

**通知内容の概要**：警告メッセージは動的に生成され、「cannot prove: X <= Y」（X <= Yを証明できない）、「can prove: X > Y」（X > Yを証明できる＝境界違反）、またはスライスの重複に関するメッセージが表示される。

**期待されるアクション**：開発者はインデックスアクセスのロジックを見直し、境界チェックを追加するか、アルゴリズムを修正して安全なアクセスを保証する必要がある。並列処理の場合は、スライス範囲の重複を解消する必要がある。

## 通知種別

コンパイラ警告（Warning）

## 送信仕様

### 基本情報

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

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

標準エラー出力（stderr）に出力される。コンパイラの`--verbosity`オプションや`--warning[IndexCheck]:off`オプションにより出力を制御可能。

## 通知テンプレート

### コンパイラ出力の場合

| 項目 | 内容 |
|-----|------|
| 送信元 | Nimコンパイラ（nim c） |
| 重大度 | Warning |
| メッセージキー | IndexCheck |
| 形式 | テキスト |

### 本文テンプレート

```
{ファイルパス}({行番号}, {列番号}) Warning: {メッセージ} [IndexCheck]
```

メッセージの種類：
- `cannot prove: {a} <= {b}` - 不等式を証明できない
- `can prove: {a} > {b}` - 境界違反を証明できる
- `({x})..({y}) not disjoint from ({c})..({d})` - スライスが重複している
- `cannot prove: {x} > {d}; required for ({x})..({y}) disjoint from ({c})..({d})` - スライスの分離を証明できない

### 添付ファイル

なし

## テンプレート変数

| 変数名 | 説明 | データ取得元 | 必須 |
|--------|------|-------------|-----|
| ファイルパス | ソースファイルの絶対または相対パス | TLineInfo.fileIndex | Yes |
| 行番号 | 警告箇所の行番号 | TLineInfo.line | Yes |
| 列番号 | 警告箇所の列番号 | TLineInfo.col | Yes |
| メッセージ | 動的に生成された詳細メッセージ | 各チェック関数 | Yes |

## 送信トリガー・条件

### トリガー一覧

| トリガー種別 | トリガーイベント | 送信条件 | 説明 |
|------------|----------------|---------|------|
| コンパイル処理 | インデックス境界チェック | proveLe()がimpUnknownまたはimpNo | sempass2.nimでの配列境界検証 |
| コンパイル処理 | 並列スライス検証 | スライス範囲の分離を証明できない | semparallel.nimでのスライス重複検査 |

### 送信抑止条件

| 条件 | 説明 |
|-----|------|
| `{.warning[IndexCheck]:off.}` | プラグマによる警告抑制 |
| `--warning:IndexCheck:off` | コマンドラインオプションによる抑制 |
| verbosityレベル0 | NotesVerbosityの設定により抑制 |

## 処理フロー

### 送信フロー

```mermaid
flowchart TD
    A[インデックスアクセス/スライス解析] --> B[境界値の取得]
    B --> C[proveLe関数で証明試行]
    C --> D{証明結果?}
    D -->|impYes| E[証明成功・警告なし]
    D -->|impNo| F[境界違反を証明]
    D -->|impUnknown| G[証明不能]
    F --> H[warnStaticIndexCheck発行]
    G --> H
    H --> I[message関数呼び出し]
    I --> J[終了]
    E --> J
```

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

### 参照テーブル一覧

この警告はコンパイラ内部のデータ構造を参照するため、外部データベースは使用しない。

| データ構造 | 用途 | 備考 |
|-----------|------|------|
| TModel | 証明システムのモデル | guards.nimで定義 |
| PNode | インデックス式のAST | 境界計算に使用 |
| guards.s | 既知の制約（ガード条件）リスト | 証明に使用される事実の集合 |

### 更新テーブル一覧

なし（読み取り専用の解析処理）

## エラー処理

### エラーケース一覧

| エラー種別 | 発生条件 | 対処方法 |
|----------|---------|---------|
| 該当なし | この警告自体はエラーではない | - |

### リトライ仕様

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

## 配信設定

### レート制限

| 項目 | 内容 |
|-----|------|
| 制限 | なし（発生箇所ごとに1回出力） |

### 配信時間帯

制限なし（コンパイル実行時に即座に出力）

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

- ソースコードのパスが出力に含まれるため、ビルドログを公開する際はパス情報に注意が必要
- インデックス値が出力に含まれる可能性があるが、通常は機密情報ではない

## 備考

- この警告は`NotesVerbosity`レベル1では無効化されている（レベル2以上で有効）
- `proveLe`関数は数学的証明システム（guards.nim）を使用して不等式を検証
- 並列処理のスライス検証は、データ競合を防ぐための重要なチェック
- 証明システムは保守的に動作し、証明できない場合は警告を出す

---

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

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

### 推奨読解順序

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

警告メッセージの種類とメッセージテンプレートを理解する。

| 順序 | ファイル | パス | 読解ポイント |
|-----|---------|------|-------------|
| 1-1 | lineinfos.nim | `compiler/lineinfos.nim` | TMsgKind列挙型でwarnStaticIndexCheckの定義（72行目）とメッセージテンプレート（175行目）を確認 |

**読解のコツ**: メッセージテンプレートが`$1`となっており、動的にメッセージが生成されることを示している。

#### Step 2: エントリーポイントを理解する

警告が発生する2つの主要な場所を理解する。

| 順序 | ファイル | パス | 読解ポイント |
|-----|---------|------|-------------|
| 2-1 | sempass2.nim | `compiler/sempass2.nim` | checkLe関数とcheckBounds関数 |
| 2-2 | semparallel.nim | `compiler/semparallel.nim` | 並列処理のスライス検証 |

**主要処理フロー (sempass2.nim)**:
1. **979-990行目**: checkLe関数でproveLe()を呼び出し、結果に応じて警告を発行
2. **984-985行目**: impUnknownの場合「cannot prove: X <= Y」メッセージ
3. **989-990行目**: impNoの場合「can prove: X > Y」メッセージ
4. **992-994行目**: checkBounds関数で配列の下限・上限をチェック

**主要処理フロー (semparallel.nim)**:
1. **129-137行目**: checkLe関数で境界チェック
2. **160-180行目**: overlap関数でスライスの重複を検証
3. **167-178行目**: 重複が証明できない場合に詳細なメッセージを生成

#### Step 3: 証明システムを理解する

| 順序 | ファイル | パス | 読解ポイント |
|-----|---------|------|-------------|
| 3-1 | guards.nim | `compiler/guards.nim` | proveLe関数と証明モデル |

**主要処理フロー**:
- TModelに格納された既知の事実（ガード条件）を使用
- 数学的推論により不等式を証明または反証

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

```
sempass2.nim::trackCall (呼び出し解析)
    │
    └─ checkBounds(c, arr, idx)
           ├─ checkLe(c, lowBound, idx)
           │      └─ proveLe(guards, a, b)
           │             └─ guards.nim::proveLe
           │
           └─ checkLe(c, idx, highBound)
                  └─ proveLe(guards, a, b)
                         └─ guards.nim::proveLe

semparallel.nim::analyseParallel (並列解析)
    │
    ├─ checkBounds(c, arr, idx)
    │
    └─ overlap(m, conf, x, y, c, d)
           └─ proveLe(m, c, y)
                  └─ guards.nim::proveLe
```

### データフロー図

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

インデックスアクセス   ───▶ checkBounds/checkLe       ───▶ 警告メッセージ
arr[idx]                    │                              (stderr)
                            ├─ lowBound/highBound取得
                            ├─ proveLe()で証明試行
                            └─ message()呼び出し

並列スライス           ───▶ overlap                    ───▶ 警告メッセージ
arr[x..y]                   │                              (stderr)
                            ├─ 各スライス範囲取得
                            ├─ proveLe()で分離を検証
                            └─ message()呼び出し
```

### 関連ファイル一覧

| ファイル | パス | 種別 | 役割 |
|---------|------|------|------|
| lineinfos.nim | `compiler/lineinfos.nim` | ソース | 警告種別・メッセージ定義 |
| sempass2.nim | `compiler/sempass2.nim` | ソース | エフェクト解析・境界チェック |
| semparallel.nim | `compiler/semparallel.nim` | ソース | 並列処理のスライス検証 |
| guards.nim | `compiler/guards.nim` | ソース | 数学的証明システム |
| msgs.nim | `compiler/msgs.nim` | ソース | メッセージ出力処理 |
