「プログラムの形式検証」記事へのコメント

言うほど簡単だろうか?

[okky (2487)]

普通のCとかC++の形式検証ってあまり進んでいないのか。
どんなスパゲッティなプログラムであっても、検証可能だ（になって欲しい）

それって グラフ同型問題 [wikipedia.org] の一種じゃない??

解けなくはないだろうけれど、今判っているアルゴリズムが全部NPなのでは、よほど簡単な例以外実用にならないぐらい時間がかかる事になる。実用にならないから作ってない、ってことじゃないかと思う。

逆に、簡単なパターンに関しては、コンパイラの最適化のパターンマッチ⇒ライブラリとして持っているよりよいパターンへ置き換え、ですでに利用されている。多分、ソースを全部くっつけて、gcc-4 とかで限界まで最適化かけたうえで -S でアセンブラコードを出させた方が簡単に同じ部分が見つかりやすいかもしれない…。

--
fjの教祖様

Re:言うほど簡単だろうか?

[gm300 (14617)]

えっと、えっと。
形式検証にはいろいろあるのですが、デジタル回路の設計の世界では実用化されています。もうないと生きていけません。
論理多項式にしてその同型性を比較します。論理多項式といってもand or だけではなく一階論述式を使えます。（たしか使えるはず）
現実的に本当に同形なものを常に同形と判断できるか　というと　できない　が簡単な答えになります。加算回路の実装方式はいろいろあるのですが、ばらばらにしてしまったものと元の足し算の間の同型性の判断はまじめにやるだけ無駄　と考えられています（数年前は）。NP であることは最初から分かっていますが、検証toolを書く人、使う人、回路を設計する人がそれぞれ限界をわきまえて運用しています。同形にもかかわらず、同形と判断できなければ、しかたがないほかの方法を考えよう。自動検証をあきらめるか、いくつかの入力に対して正しい答えを出すことを確認して我慢するか、同形とはいえないとう結論にするか、ということになります。

ベーシックなand/or/notに全部還元されたところから始めて、機能を変えずに、消費電力を下げるため/早く動くようにするために微修正したのだが、機能は同じかどうか比較する。みたいなところから始まって、修正が及ぼす影響の範囲が想定内であること、高位の記述で実現できることが還元された表現の中で同じように表現できていることを調べる　あたりまではきています。Ｃっぽいくいえば、コンパイラが出力したアセンブルコードが正しいことの自動検証に使っています。ここでは「正しい」すなわち「同形」ではありません。アセンブルコードのほうにNOPが入っていたり、意味無くJMPしたり、無駄にPUSH/POPしてもＣのほうで見える変数に同じ値が入れば、それは正しいといえます。

形式検証では、等価性検証という分野と、プロパティチェック（日本語ではどういうか知らない）という分野があります。プロパティのほうは、assert で定義するみたいなある条件をプログラムなり回路なりが満たすことがあるのかないのかを調べます。もしかしたらassert の条件は非常に長い式かもしれないし、a == 0 になったらそれ以降は b == 0 にならない　みたいに不定な時間を使っているかもしれません。スタックオーバフローがないことを確認したい場合、スタックを操作する部分を探して、オーバーフローする場合から始めて原因を遡り続けるという形式の検証もあります。
http://ja.wikipedia.org/wiki/%E5%85%85%E8%B6%B3%E5%8F%AF%E8%83%BD%E6%80%A7%E5%95%8F%E9%A1%8C
http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories

Re:言うほど簡単だろうか?

[okky (2487)]

デジタル回路の設計の世界では実用化されています。

えぇ、それは知っています。すでに述べたようにコンパイラの最適化でも利用されていますからね。

問題はこうです。「Verilogなどに比べると、C, C++ は形式検証がしづらい。だからあまり応用されていない。さ、なぜでしょう？」

ちなみに、Java などでは結構使われています。JITコンパイラが「ランタイムに」最適化をかけても間に合うのはこのため。また、CやC++でも「同形判定」ではなく、『バグの元になりやすいパターン』を検出し警告を出す(lintとか)世界ではよく使われています。

でも、C, C++ の形式検証はむつかしくなります。同形判定ができなくなります。演算量がNPになる。なぜでしょう？というもの。

.

答は規格の中に「処理系の実装依存」と「未定義」があまりにも多すぎるからです。

例として。最近あった Linux のバグにこういうのがあります。

typedef struct {
    int x;
} sample_struct;
 
int   function( sample_struct *p )
{
   int y = p->x;
 
   if ( p == NULL ) {
      return ERROR;
   }
   /* 処理を続ける */
}

「if ( p == NULL ) { ... }」の部分が完全に消失した、というのがバグの原因です　(正確には y = p->x を追加したのがバグですが、if文が消失したためにエラーが返らなくなったのが破綻を招きました)。

実はC/C++の規格には「NULLポインターへのアクセスがあった場合、それ以降のプログラムの挙動は未定義である」というものがあります。で、上のコードを見てください。

   int y = p->x;

という一行がありますよね? p が non NULL なら、この式は正常に書かれている通りに動作するはずです。p が NULL ならこれ以降、何が起こっても構わない。

で、この知識を持って if 文を考え直してください。

もし、 p が non NULL ならこの if 文の中身は実行されません。
もし、 p が NULL なら、この if 文はすでにその前の行の段階で動作が未定義になっているので、何をしてもかまいませんし、何もしなくてもかまいません。

故に最適化は この if 文を丸ごと消失させたのです。kernel は通常のプログラムと違って Segmentation Fault を起こしません。故に y = p->x の行で停止することもなく、バグを引き起こした。

.

このような「未定義」動作のせいで、記述されているコードが簡単に消失する、と言うのがC/C++の文法の特徴の一つです。このため、処理系依存な部分が多くなり、同形判定は逆に難しくなる。
上記の例のコードでは、

   if ( p == NULL ) {
      return ERROR;
   }

と同形のコードは存在しますか？というチェックに対しては「存在しません」と答えなくちゃいけないわけですし、その理由も表示できないと意味が無いですよね?これは演算量がものすごく多い。

ハードウェア記述言語には、このような曖昧さがものすごく少ないんですよ。Javaも少ない。だから形式検証がやりやすいし、それに基づいた最適化もかけやすいんです。

--
fjの教祖様

Re:言うほど簡単だろうか?

[gm300 (14617)]

うーむ。
1) 厳密な同形性の判定ってそんなに大切？
  人間がソースを変えたなら何か変更したい意図があったのでは？
つまり同型性判定を行いたい場合で、diff みたいなtoolでは比較できない場合は、つねになんらかなの違いがあるのでは？

2) 未定義な部分を比較してもしかたがないのでは？
  != なのか !== なのか。

  例のような場合、オイラが欲しいのは、

1) 自動で y = p->x でp == NULL の場合が直近でチェックされていないのを見つける。
2) p == NULL になる場合があるのか、ないのか遡って調べてくれる

  ような tool.

　p == NULL の時に y = p->x はよくない。それは事実。
  だからといって文法的に許されるのに、p->x を全部禁止するのは意味がない。 (文法的に許さないというのもひとつの考え方。)
  使用状況が限定されていれば、関数localで検査する必要はない。馬鹿ばかしいが、if( p != NULL && function(p) != 5 ) .. みたいに一回だけfunctionが呼ばれている場合。

「Verilogなどに比べると、C, C++ は形式検証がしづらい。だからあまり応用されていない。さ、なぜでしょう？」に対する答えは、作業フローの差ではないかと思う。
1) Verilog の場合は、記述する人、シリコンに実装する人が異なり、記述する人がいいと思ってもその意図は伝わらない。意図ではなく、自動的な方法で検証できないといけない。
2) Cコンパイラに比べるとはるかにマイナーなツールでどんどん変形する。より多くの変形ミスの可能性がある。
3) Verilog シミュレータは遅く、実際に使われる期間は長く、ハードのバグは、ソフトよりも出荷後の修正が格段に大変だからより自動検証のデマンドがある。
0) 回路のほうがアトミックな構造が単純だから。これは説明のしかたが悪そう。どう直したらいいかよくわからない。

「あまり」なのか「ほとんど全く」なのか知りたいよん。

Re:言うほど簡単だろうか?

[okky (2487)]

1) 厳密な同形性の判定ってそんなに大切？
    人間がソースを変えたなら何か変更したい意図があったのでは？

えぇ、意図はあったんでしょう。ただし、そのコードがその意図を「正しく反映している」保証はありません。
そして、「論理的には正しくないが、文法的には正しい」状態は腐るほどあります。とくに文法のあちらこちらに「未定義」「実装依存」といった曖昧さがあると酷いことになる。
# なにしろ、Cの場合 int が何ビットなのか、すら「実装依存」ですからね。

Javaなどはこの辺が厳密です。なので、意味論的な揺らぎが少なく、結果、形式検証が高い意味をもつ。

.

1) 自動で y = p->x でp == NULL の場合が直近でチェックされていないのを見つける。
2) p == NULL になる場合があるのか、ないのか遡って調べてくれる

    ような tool.

1 であれば、最近の lint はできます。つーかgccのワーニングオプションを全部 on にすれば当然できる。
というかですね、1はできて当然です。だって最適化フェーズで「p==NULLの場合があるかどうか」をチェックできている。

   int y = p->x;
 
   if ( p == NULL ) {
      return ERROR;
   }

だと if 文は消失しますが、

   if ( p == NULL ) {
      return ERROR;
   }
 
   int y = p->x;

だと、if文は消失しません。

.

2はちょっと難しい。「pがNULLになる可能性を考慮したコードになっていない」事をチェックするのは簡単ですが(そういう文法チェッカーはある)、pがNULLに「ならない」事をチェックするとなるとシステムコールや標準ライブラリも含めた、全コードが必要になる(正確には、入力条件の厳格なルール記述と、出力の値範囲が全部できていればいいんですが)。

また、実際には「pがNULLになるかどうか」じゃなくて、一般的に「変数xが値のレンジaaa-bbb になる可能性」が本当に欲しい機能ですよね?

--
fjの教祖様

Re:言うほど簡単だろうか?

[gm300 (14617)]

>また、実際には「pがNULLになるかどうか」じゃなくて、一般的に「変数 xが値のレンジaaa-bbb になる可能性」が本当に欲しい機能ですよね？
  いや。限定的な範囲の中で、想定外のことが起きない、あるいは自分の想定と、コードとの間にずれがないことを知りたい。
　y = p->x ;
    if( p == NULL ) ..

  と書いたなら、y= の式のときに意味があるx が取れることを知りたい。意味があるyが取れてさらにp がNULL であるかをチェックできることを知りたい。残念ながらこの場合はそういったことはできない。p がNULL の時にif(p==NULL)まで行き着くことはできない。未定義なんで「できるとは限らない」のほうが正しいかも。

>2はちょっと難しい。... pがNULLに「ならない」事をチェックするとなるとシステムコールや標準ライブラリも含めた、全コードが必要になる
  ここでも反論したい。全コードを食わせて自動で答えが有限の時間のなかででればうれしい。それが、「なる」でも「ならない」でもなきく「わからない」であっても。常に、24時間待ちたいとは思わない。部分的なソースとその前提条件を入力して2分で答えを知るという方法も欲しい。答えが不満ならば、前提条件を絞ったり、ソースを足したり引いたりして答えを調整したい。上位の腐った関数のために、それ以降の動作が全部不定になってしまい検証ができないのはまずい。不定になる部分はとりあえず捨ててそれ以外の部分を検証したい。make -k みたいに。Java な人はmake 使わないっだったけ。