yoriyukiの日記 このページをアンテナに追加 RSSフィード

2010-10-17

[][]ホームページの公開とお蔵入りソフトウェアの再公開 ホームページの公開とお蔵入りソフトウェアの再公開 - yoriyukiの日記 を含むブックマーク

何だか眠れなかったので、Google Siteに自己紹介ページを作った。使い方が今ひとつ分かっていなくて、例えばファイルアップロードしてリンクするのどうしたらいいのだろう、みたいな感じなので変なことをしているかもしれないけど。

ついでに、今までお蔵入りしていたBrainScanSurrealアップロードした。

意見等伺えると幸い。

2006-10-05

[]BrainScan - 入力を指定する BrainScan - 入力を指定する - yoriyukiの日記 を含むブックマーク

ラフマニノフいいなあ。それはそうと、入力の内容に制限がないとbfプログラムするのは大変なので、','で入力される文字の集合を指定できるようにしました。

$ ./brainscan -R -D ',(0-9)>++++++[<-------->-],(0-9)[<+>-],(0-9)<.>.'

','の後の(...)の中が入力されるかもしれない文字の集合です。

2006-10-04

[]BrainScan再び [http://d.hatena.ne.jp/yoriyuki/20060924/p1:title=BrainScan]再び - yoriyukiの日記 を含むブックマーク

d.y.d.より

しかし bf を書いているとわりと真剣に「コード上の指定した位置で常に *(ptr+1)==0 であること」や「実行終了時にポインタが初期位置に戻っていること」辺りの性質を保証したくなるので、チェッカーがあると嬉しいかもしれない。わりと真剣に bf を書いていることが第一の間違いですが。

ということで、新しい検査式を導入してみました。

コードの中に?や_を書くことで、上の検査を行い成り立たない場合があればトレースを出力します。

例:

$ ./brainscan '>_'
Pointer is not zero.
        0: >
        1: _
$ ./brainscan '>+<?'
Possible non-zero value at 1
        0: >
        1: +
        2: <
        3: ?

2006-09-27

[]BrainScan Linux Binary [http://www15.ocn.ne.jp/~rodinia/brainscan-x86-linux.gz:title=BrainScan Linux Binary] - yoriyukiの日記 を含むブックマーク

OCamlだとコンパイルできない人も多いと思うので、BrainScanのバイナリ版も置いてみました。x86-linux用です。未テストなので、うまく動かなければ教えてください。

2006-09-24

[]BrainScan - オプションを追加しました BrainScan - オプションを追加しました - yoriyukiの日記 を含むブックマーク

state hasingのオプション付け加えて、.はデフォルトではなにも表示しないようにしました。うるさいので。state hashingすると、近似的に検査することで複雑なプログラムでも検証ができるようになります。

BrainScan - BrainF*ckプログラムを超高信頼化する - yoriyukiの日記

ハッシュにはCRCを使っていますがこれでいいのかどうか。

[][]BrainScan - BrainF*ckプログラムを超高信頼化する BrainScan - BrainF*ckプログラムを超高信頼化する - yoriyukiの日記 を含むブックマーク

BrainScanというものを作ってみました。BrainFuck*1のソースコードモデル検査器です。プログラムがとり得る全状態を探索し、異常が起きないか検査します。検査できるのは、

  • ポインタがアンダーフローしないこと
  • バッファの値が0-255を越えないかどうか(-Rまたは--rangeオプションを付けたときのみ)
  • コード中で!でマークされた位置に到達しないかどうか(したらエラーとみなす)

です。エラーを検出すると、そこまでのトレースを出力します。アルゴリズムは単純で、深さ優先探索をするだけです。バッファの状態は区間の集合として保持されています。OCamlで書かれて、コンパイルするにはfindlibとextlibが必要です。

例を見てみましょう。

$ ./brainscan '[]!'
! reached.
        0: [
        2: !

BrainF*ckプログラムはコマンドライン引数として与えます。この例だと、!にジャンプするのでエラーになります。

$ ./brainscan '+[]!'
$

この場合、プログラムは無限ループに入り!に到達しません。BrainScanはこれを理解して、エラーを出さずに終了します。

./brainscan ',[]!'
! reached.
        0: ,
        1: [
        3: !

今度は,で受け取る内容によっては!に行く可能性があります。-Dまたは-dotオプションを付けると、'.'で表示される可能性がある範囲を出力します。

$ ./brainscan -D ',[.]!'
! reached.
        0: ,
        1: [
        4: !
['\001'-'\255']

表示の順番がすこし変ですが、,で0以外の入力があったとき[]に到達することを理解していることが分かります。

$ ./brainscan -R ',>++++++[<-------->-],[<+>-],'<.>.'

Wikipediaにある足し算プログラムです。大量のエラーが表示されることが分かります。

残念ながら、すこし複雑なプログラム検査しようとするとメモリを大量に使ってしまいます。State hashを使うと検査は不正確になりますが、メモリの使用量が抑えられます。-Hまたは--hashオプションを使います。あとに1-31の数字を引数として与えます。数字が大きいほど正確に検査されます。

$ time ./brainscan -H31  ',>,>++++++[-<--------<-------->>] store 2 numbers from kb in (0) and (1); and subtract 48 from each
<<[ loop until the dividend is zero
>[->+>+<<] move the divisor in (1) to (2) and (3); setting (1) to zero
>[-<<- subtract 1 from both the dividend(0) and the divisor(2) until (2) is zero
[>]>>>[<[>>>-<<<[->>]<<] if the dividend is zero; exit the loop
>>>+ add one to the quotient in (5)
<<[-<<+>>] move the saved divisor in (3) to (2)
<<<] move ptr to {0} and repeat loop
>[-]>>>>[-<<<<<+>>>>>] move the quotient in (5) to (0)
<<<<++++++[-<++++++++>]<. add 48 and print result'

real    0m3.881s
user    0m3.371s
sys     0m0.234s

Wikipediaの割算の例です。-Hを使わないとメモリを使い尽くして終わりません。

追記:あたらしいオプションを付け加えたので、すこし書き換えました。

*1:と書かないとはてなキーワードに出ない