title: Continuation based C を用いたプログラムの検証手法
author: 比嘉健太
profile: 琉球大学 大学院 理工学研究科 情報工学専攻
lang: Japanese

# ソフトウェアの実装の信頼性の向上
* ソフトウェアの信頼性を向上させたい
* 信頼性を向上させる手法には証明、モデル検査、テストなど様々な手法がある
* ソフトウェアが定められた仕様を常に満たすか確認することで信頼性を保証する
* 計算を拡張するメタ計算として検証機構を導入し、ソフトウェアの実装コードの検証を行なう

# ソフトウェアの信頼性向上手法
* assert
    * 実行プログラム上で仕様が満たされているかチェックする
    * 網羅的にテストできない
    * ユニットテストと組み合わせて使う
* 検証の計算システムで実行する(メタ計算)
    * Java Path Finder
        * JVM を切り替える
    * Valgrind
        * バイナリを動的解析
    * 大規模システムは実行できない

# ソフトウェアの信頼性向上手法
* アルゴリズムの正しさを証明する
    * Agda, Coq, Idris といった証明支援系でプログラムを記述する
    * 極めて難しい
    * 実装に対して適用できない
* ソフトウェアの仕様を記述し、その反例が無いかをチェックする
    * Spin, NuSMV といったモデルチェッカ
    * モデル検査用に特化した言語で実装を記述する必要がある

# Akasha の目的
* 実装そのものを検査する
    * 実装に入り込むバグを見付ける
* 高速かつ網羅的に検査する
* メタ計算の切り替えで様々な検証を行なう
* 高速なメタ計算が行なえる言語(CbC) を用いる

# Continuation based C (CbC)
* 当研究室で開発している言語
* Code Segment, Data Segment という単位でソフトウェアを記述する
* 関数呼び出しは末尾のみ、の制約を持ったC言語
    * スタックは持たない
    * goto で飛んで戻ってこない
    * 保持すべき状態が明示的になっている
    * メタ計算は goto の間に計算を挟むことで実現できる

# Code Segment and Data Segment
* Code Segment は入出力である Input Data Segment と Output Data Segment を持つ
* 単一 Code Segment はシンプル(purely functional)な処理のみを行なう
* Code Segment どうしを接続してソフトウェア全体を構築していく
* 依存のない Code Segment どうしは並列に実行することが可能
![csds](./images/code_segment_data_segment.svg){:width="50%"}


# Example of Code Segment in CbC
* Code Segment は `__code` を付けた関数
* 次の Code Segment への接続は `goto` で表される

```
__code addTen(struct Count c) {
    c.x = c.x+10;
    goto twice(c);
}

__code twice(struct Count c) {
    c.x = c.x*2;
    goto showValue(c);
}
```

# CbC のメタ計算
* Code Segment 間の接続はメタ計算レベルで行なわれる
* メタ計算も Code Segment と Data Segment で表現される
    * ポインタの扱いや並列実行はメタ計算レベルで行なう

![meta_csds](./images/meta_csds.svg){:width="50%"}



# CbC のメタ計算の実際
* Code Segment で使われる Data Segment は Meta Data Segment である Context に全て定義されている

```
union Data {
    struct Count {
        int x;
    } count;
    struct Port {
        int port;
    } port;
}

struct Context {
    union Data *data;  // Data Segment
    unsigned int gotoCount; // メタ計算に必要なデータ
};
```

# CbC のメタ計算の実際
* Meta Code Segment では Data Segment は union Data という形で一様
* メタ計算と通常の計算は stub と meta によって接続される
    * stub では利用する Data Segment の指定などを行なう

```
__code addTen_stub(struct Context* context) {
    goto addTen(context, &context->data[Count]->count);
}
__code addTen(struct Context* context, struct Count c) {
    c.port = c.x+10;
    goto meta(context, Twice);
}

__code twice_stub(struct Context* context) {
    goto twice(context, &countext->data[Count]->count);
}
__code twice(struct Context* countext, struct Count c) {
    c.x = c.x*2;
    goto meta(context, ShowValue);
}
```

# CbC のメタ計算の実際
* goto する時に必ず通る Meta Code Segment `meta` を作る
* デフォルトの meta
    * Code Segment の接続先名から次に実行される Code Segment を決定する
* meta を変更することで平行計算や例外処理やソフトウェア検証を行なう

```
__code meta(struct Context* context, enum Code next) {
    goto (context->code[next])(context);
}
```


# Meta Code Segment を使った検証
* `meta` を切り替えることでノーマルレベルの計算を拡張する
    * `goto` した回数を数える

```
// Meta Data Segment
struct Context {
    union Data *data;       // Data Segment
    unsigned int gotoCount; // メタ計算に必要なデータ
};

// Meta Code Segment
__code meta(struct Context* context, enum Code next) {
    countext.gotoCount++;
    goto (context->code[next])(context);
}
```

# Verification Method of Programs Using Continuation based C
* メタ計算として検証機構を導入する
* 仕様はCbCで記述する
    * 常に真になるべき式として定義
* 仕様を満たさない Input Data Segment が無いかチェックしていく
* 検証の対象として CbC で記述された赤黒木を用いる

# Red-Black Tree
* 赤黒木とは木構造のデータ構造
* 赤黒木の条件:
    * 各ノードは赤または黒の色を持つ
    * ルートと葉の色は黒である
    * 赤ノードは2つの黒ノードを子として持つ(よって赤ノードが続くことはない)
    * ルートから最下位ノードへの経路に含まれる黒ノードの数はどの最下位ノードでも一定である
* 仕様: 最も長い経路は最も短い経路の高々2倍に収まる

![rbtree](./images/rbtree.svg){:width="35%"}

# Verification Library Akasha
* 本研究で作成した検証用メタ計算ライブラリ
* どのような順番で要素が挿入されても常に仕様が満たされることを確認する
    * 全ての順列組み合わせのテストケースを実行する
* 仕様を満たさない挿入順番があればそれを表示
    * 深さ優先探索で有限個の要素の挿入順番を総当たりで列挙
    * 挿入後の木はきちんとバランスしているかチェックする
* CbC のメタ計算 Akasha では要素数13個までチェックできた
    * 13の階乗で62億通りを1,2時間ほど
* 実装にわざとバグを入れた場合にはバランスしない入力例を返した

# C Bounded Model Checker
* Carnegie Mellon University で開発されている記号実行モデルチェッカ
    * C, C++, Java に対応
* CbC は `__code` を `void` に、`goto` を `return` に変えると C Syntaxになる
    * 赤黒木のコードを機械的に置換で C に変換して検証
* 挿入順番は非決定的な入力 `nondet_int` を使う
* 関数呼び出しやループは展開される
    * 展開可能な最大数まで展開しても赤黒木の仕様を検証できず

# Conclusion
* 動作するプログラムの記述を変更せず検証を行なえた
    * テストケースの自動生成+仕様の反例表示ができた
* CBMC では検証できない範囲の検証を行なうことができた
    * 総当たりでチェックしているため扱えるサイズは小さい
        * CBMC に比べ高速
    * 記号実行しているわけではない
        * 有限の個数しか扱えない
* ポインタアクセスに由来するバグなどは見付けられない

# Future Works
* 状態の抽象化による探索の効率化
* 挿入だけでなく削除を含む赤黒木の仕様検証
* ポインタへの不正アクセス検出などの機能
* 検証用APIを CbC コンパイラに導入
* CBMC 側で検証できるよう赤黒木を書き換えて検証する

# CBMC Informations
* CBMC 5.4
* 実行オプション
    * cbmc --unwind 1
    * cbmc --depth 400 --property verifySpecification.assertion.1
* 赤黒木のCbC実装
    * 赤黒木部分のみ: 330行
    * スタックやメモリのアロケータなどを含める: 640行

# 他の言語でのメタ計算
* 計算を実現するような計算
* プログラムを生成するようなプログラム
    * TemplateHaskell in Haskell, Template in C++, Generics
    * コンパイル時メタプログラミング
* 言語が特別な API を提供する
    * method_missing, define_method in Ruby
* プログラムがその言語処理系の挙動を変える
    * reflection in Java
* CbC では関数呼び出しが存在していないのでメタ計算を挟むことが容易

# Red-Black Tree のコード例

```
__code insertCase2(struct Context* context, struct Node* current) {
    struct Node* parent;
    stack_pop(context->node_stack, &parent);

    if (parent->color == Black) {
        stack_pop(context->code_stack, &context->next);
        goto meta(context, context->next);
    }

    stack_push(context->node_stack, &parent);
    goto meta(context, InsertCase3);
}

__code insert2_stub(struct Context* context) {
    goto insertCase2(context, context->data[Tree]->tree.current);
}
```

# Akasha の検証コード例

```
__code verifySpecificationFinish(struct Context* context) {
    if (context->data[AkashaInfo]->akashaInfo.maxHeight >
        2*context->data[AkashaInfo]->akashaInfo.minHeight) {
        context->next = Exit;
        goto meta(context, ShowTrace);
    }
    goto meta(context, DuplicateIterator);
}
```

<!-- vim: set filetype=markdown.slide: -->