# 通知設計書 49-warnProveField

## 概要

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

### 本通知の処理概要

この警告は、Nimコンパイラがオブジェクトバリアント（判別共用体）のフィールドアクセスが安全であることを静的に証明できない場合に発生する警告メッセージです。ケースオブジェクトの不正なブランチへのアクセスを検出し、潜在的なランタイムエラーを防止します。

**業務上の目的・背景**：Nimのオブジェクトバリアント（case of構文を使用したオブジェクト）では、判別子（discriminator）の値によってアクセス可能なフィールドが決まります。誤ったブランチのフィールドにアクセスすると、未定義動作やメモリ破損の原因となります。この警告により、開発者はコンパイル時に潜在的な不正アクセスを発見し、適切なケース分岐を追加することができます。

**通知の送信タイミング**：コンパイル時のエフェクト解析フェーズ（sempass2.nim）において、nkCheckedFieldExprノード（チェック付きフィールドアクセス）を解析する際に、ガード条件から該当フィールドのアクセス可能性を証明できない場合に警告が発生します。また、case文の分岐解析時（guards.nim::checkFieldAccess）でも同様のチェックが行われます。

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

**通知内容の概要**：「cannot prove that field '式' is accessible」というメッセージが表示され、アクセス可能性を証明できないフィールドを特定します。

**期待されるアクション**：開発者は、該当するフィールドアクセスの前に適切なケース分岐（if文やcase文）を追加して判別子の値を確認するか、コードの論理を見直してすべてのケースでフィールドがアクセス可能であることを保証することが期待されます。

## 通知種別

コンパイラ警告（Warning）

## 送信仕様

### 基本情報

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

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

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

## 通知テンプレート

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

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

### 本文テンプレート

```
{ファイル名}({行番号}, {列番号}) Warning: cannot prove that field '{式}' is accessible [ProveField]
```

### 添付ファイル

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

## テンプレート変数

| 変数名 | 説明 | データ取得元 | 必須 |
|--------|------|-------------|-----|
| ファイル名 | ソースファイルのパス | TLineInfo.fileIndex | Yes |
| 行番号 | 警告発生行 | n.info.line | Yes |
| 列番号 | 警告発生列 | n.info.col | Yes |
| 式 | アクセスしようとしているフィールド式 | renderTree(n[0]) | Yes |

## 送信トリガー・条件

### トリガー一覧

| トリガー種別 | トリガーイベント | 送信条件 | 説明 |
|------------|----------------|---------|------|
| コンパイル時 | フィールドアクセス解析 | doesImply != impYes | guards.nim:1189行目 |
| コンパイル時 | case文解析 | warnProveFieldが有効 | sempass2.nim:864,1332行目 |

### 送信抑止条件

| 条件 | 説明 |
|-----|------|
| `--warning[ProveField]:off` | コマンドラインオプションで警告を無効化 |
| `{.warning[ProveField]:off.}` | プラグマで警告を無効化 |
| verbosityレベル0または1 | デフォルトでは無効 |
| strictCaseObjectsが有効な場合 | エラーとして出力（警告ではない） |

## 処理フロー

### 送信フロー

```mermaid
flowchart TD
    A[nkCheckedFieldExpr検出] --> B{warnProveField有効?}
    B -->|No| C{strictCaseObjects?}
    B -->|Yes| D[checkFieldAccess呼び出し]
    C -->|Yes| D
    C -->|No| E[スキップ]
    D --> F[buildProperFieldCheck]
    F --> G{check != nil?}
    G -->|No| H[通常処理]
    G -->|Yes| I{doesImply == impYes?}
    I -->|Yes| H
    I -->|No| J{produceError?}
    J -->|Yes| K[localError発行]
    J -->|No| L[warnProveField発行]
    K --> H
    L --> H
```

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

### 参照テーブル一覧

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

### 内部データ構造

| データ構造 | 用途 | 備考 |
|-----------|------|------|
| TModel（guards） | ガード条件の集合 | 事実の含意関係を判定 |

### 更新テーブル一覧

該当なし

## エラー処理

### エラーケース一覧

| エラー種別 | 発生条件 | 対処方法 |
|----------|---------|---------|
| strictCaseObjectsエラー | strictCaseObjects有効時 | フィールドアクセス前にcase分岐を追加 |

### リトライ仕様

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

## 配信設定

### レート制限

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

### 配信時間帯

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

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

- オブジェクトバリアントの不正なフィールドアクセスは、メモリ破損やセキュリティ脆弱性につながる可能性がある
- 判別子の値によってアクセス可能なメモリ領域が異なるため、不正アクセスは予測不可能な動作を引き起こす
- この警告に注意を払うことで、より安全なコードを書くことができる

## 備考

- `strictCaseObjects`機能が有効な場合、この警告はエラーに昇格する
- verbosityレベル2以上で有効になる（NotesVerbosity配列で制御）
- オブジェクトバリアントのフィールドアクセスは、コンパイラが自動的にチェックノードを挿入する
- doesImply関数は、現在のガード条件から与えられた条件が導出できるかを判定する

---

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

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

### 推奨読解順序

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

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

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

**読解のコツ**: warnProveFieldはverbosityレベル1以下では無効になることに注意。

#### Step 2: 警告発生のエントリーポイントを理解する

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

| 順序 | ファイル | パス | 読解ポイント |
|-----|---------|------|-------------|
| 2-1 | sempass2.nim | `compiler/sempass2.nim` | 1330-1333行目でnkCheckedFieldExprの処理を確認 |
| 2-2 | sempass2.nim | `compiler/sempass2.nim` | 864行目でcase文解析時の使用を確認 |

**主要処理フロー**:
1. **1330行目**: `of nkCheckedFieldExpr:`でチェック付きフィールドアクセスを検出
2. **1332行目**: `tracked.config.hasWarn(warnProveField) or strictCaseObjects`で条件チェック
3. **1333行目**: `checkFieldAccess`関数を呼び出し

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

警告を実際に発行するguards.nimの関数を確認します。

| 順序 | ファイル | パス | 読解ポイント |
|-----|---------|------|-------------|
| 3-1 | guards.nim | `compiler/guards.nim` | checkFieldAccess関数（1182-1190行目）を確認 |

**主要処理フロー**:
1. **1182行目**: checkFieldAccess関数の定義
2. **1183行目**: `for i in 1..<n.len:`でチェック条件をループ
3. **1184行目**: `buildProperFieldCheck`でフィールドチェック条件を構築
4. **1185行目**: `m.doesImply(check) != impYes`で含意をチェック
5. **1186-1187行目**: produceErrorの場合はlocalError
6. **1188-1189行目**: そうでない場合はwarnProveField警告

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

```
sempass2.nim::track()
    │
    └─ of nkCheckedFieldExpr:（1330行目）
           │
           ├─ track(tracked, n[0])（1331行目）
           │
           └─ hasWarn(warnProveField) or strictCaseObjects?（1332行目）
                  │
                  └─ checkFieldAccess(guards, n, config, produceError)（1333行目）
                         │
                         └─ guards.nim::checkFieldAccess()
                                │
                                ├─ buildProperFieldCheck()
                                │
                                └─ doesImply(check)?
                                       │
                                       ├─ impYes: 通常処理
                                       └─ impNo/impUnknown: 警告/エラー発行
```

### データフロー図

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

obj.field（バリアントオブジェクト）
        │
        ▼
nkCheckedFieldExpr ───▶ checkFieldAccess()
                              │
                              ├─ n[0]: フィールドアクセス式
                              ├─ n[1..]: チェック条件
                              │
                              └─ doesImply(check)?
                                     │
                                     └─ impNo/impUnknown ───▶ 警告メッセージ
```

### 関連ファイル一覧

| ファイル | パス | 種別 | 役割 |
|---------|------|------|------|
| lineinfos.nim | `compiler/lineinfos.nim` | ソース | 警告種別の定義とメッセージテンプレート |
| sempass2.nim | `compiler/sempass2.nim` | ソース | エフェクト解析とcheckFieldAccess呼び出し |
| guards.nim | `compiler/guards.nim` | ソース | checkFieldAccess関数の実装 |
| msgs.nim | `compiler/msgs.nim` | ソース | メッセージ出力機能 |
