C言語:GDBによるデバッグ
0からnまでの整数の和を求める例を題材にデバッガ(gdb)の使用例を紹介したいと思います。バグがある状態から始めます。
main.c(バグ有り)
int sum(int n) { int acc = 0; int i; for (i = 0; i < n; i++) { acc += i; } return acc; } int main(void) { int n = 10; int wa = sum(n); return wa; }
GDB配下でのプログラム実行
gdbは起動中のプログラムにアタッチす方法も有りますが、今回はgdbの引数にプログラムを指定して起動します。
$ gdb -q main Reading symbols from main...done. (gdb) run Startping program: /home/makoto/blog/22_Cdebug/main [Inferior 1 (process 4924) exited with code 055] (gdb) p $_exitcode $1 = 45
1から10までの和なので55になってほしいのですが、45になっています。
ステップ実行していく
ひとまず関数のトップであるmainから調べていくことにします。
mainで止まるようにブレークポイントを設定します。
(gdb) break main Breakpoint 1 at 0x555555554630: file main.c, line 15. (gdb) info breakpoints Num Type Disp Enb Address What 1 breakpoint keep y 0x0000555555554630 in main at main.c:15 breakpoint already hit 1 time
main.cの15行目にブレークポイントが設定されています。再度プログラム実行します。
(gdb) run Starting program: /home/makoto/blog/22_Cdebug/main
main関数でプログラムが止まります。
Breakpoint 1, main () at main.c:15 15 int n = 10;
まだ、「int n = 10」は実行されていません。試しに変数nの値を調べてみます。
(gdb) print n $2 = 0
1文進めます。($Xの部分は気にしなくて大丈夫です。)
(gdb) next 16 int wa = sum(n);
今度はnが10で初期化されているはずです。
(gdb) print n $3 = 10
もう1文進めます。
(gdb) next 18 return wa; (gdb) print wa $4 = 45
結果が45になっています。sumが悪そうです。mainのブレークポイントを削除して、今度はsumに設定してみます。
(gdb) delete 1 (gdb) break sum Breakpoint 2 at 0x555555554601: file main.c, line 3. (gdb) info breakpoints Num Type Disp Enb Address What 2 breakpoint keep y 0x0000555555554601 in sum at main.c:3
再度最初から実行します。
(gdb) run The program being debugged has been started already. Start it from the beginning? (y or n) y Starting program: /home/makoto/blog/22_Cdebug/main Breakpoint 2, sum (n=10) at main.c:3 3 int acc = 0;
今度はsum(main.cの3行目)で止まります。1文実行してみます。
(gdb) next 6 for (i = 0; i < n; i++) (gdb) print acc $8 = 0
accが0で初期化されています。for文のなかまで進めてみます。
(gdb) next 8 acc += i;
最初のループを終え、行が戻ります。
(gdb) next 6 for (i = 0; i < n; i++)
ここで各種値を確認してみます。
(gdb) print acc $5 = 0 (gdb) print i $6 = 0
このタイミングではまだiはインクリメントされていません。継続条件も確認してみます。
(gdb) print i < n $3 = 1
成立しています。もう一文進めてみます。
(gdb) next 8 acc += i;
i++が実行されているはずです。
(gdb) print i $5 = 1
iが1なので今度はaccに1が加えられるはずです。
(gdb) next 6 for (i = 0; i < n; i++) (gdb) print acc $6 = 1
加えられています。ループを一気に進めてみます。
(gdb) until 10 return acc; (gdb) print acc $7 = 45
accが45となっていて10足りません。この時のiと各種値を見てみます。
(gdb) print i $10 = 10 (gdb) print n $11 = 10 (gdb) print i < n $12 = 0
iは10になっていますが、i < n が成立せずにループを終了していそうです。もう少し詳しく見てみます。再度実行します。
(gdb) run The program being debugged has been started already. Start it from the beginning? (y or n) y Starting program: /home/makoto/blog/22_Cdebug/main Breakpoint 2, sum (n=10) at main.c:3 3 int acc = 0;
直前のiが9の部分で止まるようにして、そこから詳しく見てみたいと思います。
(gdb) watch i == 9 Hardware watchpoint 3: i == 9
実行を進めます。
(gdb) continue Continuing. Hardware watchpoint 3: i == 9 Old value = 0 New value = 1 0x000055555555461b in sum (n=10) at main.c:6 6 for (i = 0; i < n; i++)
値を確認します。
(gdb) print i $10 = 9 (gdb) print acc $11 = 36
i++が実行された直後ですね。
(gdb) next 8 acc += i; (gdb) next 6 for (i = 0; i < n; i++) (gdb) print acc $13 = 45
36に9が加えられて45になっています。更に実行を継続してみます。
(gdb) continue Continuing. Hardware watchpoint 7: i == 9 Old value = 1 New value = 0 0x000055555555461b in sum (n=10) at main.c:6 6 for (i = 0; i < n; i++) (gdb) print i $29 = 10 (gdb) print n $30 = 10 (gdb) print i < n $31 = 0
i == 9の条件が破れたところで再度止まってくれました。各種値を確認してみると、i,nが10となりi < nの継続条件が成り立っていません。C言語からはインクリメントと継続条件のどちらが先か見えませんが、このような場合は逆アセンブルしてみると見えてきます。(私はアセンブラの理解が怪しいので誤っていたらすみません。)
(gdb) disassemble Dump of assembler code for function sum: 0x00005555555545fa <+0>: push %rbp 0x00005555555545fb <+1>: mov %rsp,%rbp 0x00005555555545fe <+4>: mov %edi,-0x14(%rbp) 0x0000555555554601 <+7>: movl $0x0,-0x8(%rbp) 0x0000555555554608 <+14>: movl $0x0,-0x4(%rbp) 0x000055555555460f <+21>: jmp 0x55555555461b <sum+33> 0x0000555555554611 <+23>: mov -0x4(%rbp),%eax 0x0000555555554614 <+26>: add %eax,-0x8(%rbp) 0x0000555555554617 <+29>: addl $0x1,-0x4(%rbp) => 0x000055555555461b <+33>: mov -0x4(%rbp),%eax 0x000055555555461e <+36>: cmp -0x14(%rbp),%eax 0x0000555555554621 <+39>: jl 0x555555554611 <sum+23> 0x0000555555554623 <+41>: mov -0x8(%rbp),%eax 0x0000555555554626 <+44>: pop %rbp 0x0000555555554627 <+45>: retq End of assembler dump.
+29でインクリメントされていて+36の部分で継続条件を判定しているようです。
rbp-0x4の場所が変数iの場所ですね。
(gdb) print *(int *)($rbp-0x4) $32 = 10
nが10の場合はaccに加えたいので、継続条件をi <= nに修正することにします。
int sum(int n) { int acc = 0; int i; for (i = 0; i <= n; i++) { acc += i; } return acc; }
コンパイルして再度実行してみます。(コンパイルば別のターミナルから実行してgdbは別ターミナルで実行したままにしています。)
(gdb) run Starting program: /home/makoto/blog/22_Cdebug/main warning: Probes-based dynamic linker interface failed. Reverting to original interface. Breakpoint 2, sum (n=10) at main.c:3 3 int acc = 0; (gdb) until 6 for (i = 0; i <= n; i++) (gdb) 8 acc += i; (gdb) 6 for (i = 0; i <= n; i++) (gdb) 10 return acc; (gdb) print acc $33 = 55
うまく行っていそうです。
C言語:型に性質をもたせる?(コンパイル時の警告まで)
[増補改訂]関数プログラミング実践入門 ──簡潔で、正しいコードを書くために (WEB+DB PRESS plus)の「1.5 型に性質をもたせる HTMLの文字列エスケープ」を読んで、C言語の場合はどんな風にできるのかと思い実装してみました。おそらくコンパイル時のチェックで警告されるところまではいくのかな、と思いつつ。
ソース以下となります。
サンプルソースとコンパイル
HTMLEscapedString.h
ヘッダファイルでは構造体HTMLEscapedStringのメンバを利用者に公開しないようにしています。
#ifndef __HTML_ESC_STRING__ #define __HTML_ESC_STRING__ typedef struct HTMLEscapedString HTMLEscapedString; const HTMLEscapedString * const escape(const char *); void putHTMLEscapedStrLn(const struct HTMLEscapedString * const); #endif
HTMLEscapedString.c
構造体HTMLEscapedStringのメンバはヘッダファイルで利用者に公開しないようにしていますが、今回のケースでは欲しいメンバがなかったので、実際のメンバもありません。メンバを持たない構造体って今まで考えたことはなかったのですが定義できるのですね。本のサンプルではescape定義時に使用する関数escapeAmpとescapeOtherを補助として定義していますが、以下ではそれらを使用せずに処理を真似て実装しています。
#include <stdlib.h> #include <stdio.h> #include "HTMLEscapedString.h" /* 型 */ struct HTMLEscapedString { }; /* メモリを確保して返すことにする。*/ static HTMLEscapedString * const createHTMLEscapedString(int size) { return malloc(size); } const HTMLEscapedString * const escape(const char *src) { /* 簡易的にサイズは固定とする。*/ HTMLEscapedString *const dst = createHTMLEscapedString(128); char *dstp = (char *)dst; while(*src) { if('&' == *src) { *(dstp++) = '&'; *(dstp++) = 'a'; *(dstp++) = 'm'; *(dstp++) = 'p'; } else if('<' == *src) { *(dstp++) = '&'; *(dstp++) = 'l'; *(dstp++) = 't'; } else if('>' == *src) { *(dstp++) = '&'; *(dstp++) = 'g'; *(dstp++) = 't'; } else if('"' == *src) { *(dstp++) = '&'; *(dstp++) = 'q'; *(dstp++) = 'u'; *(dstp++) = 'o'; *(dstp++) = 't'; } else { *(dstp++) = *src; } src++; } return dst; } void putHTMLEscapedStrLn(const struct HTMLEscapedString *str) { printf("%s\n", (char *)str); }
簡単にするためエスケープ後の文字列は適当にサイズ128で確保しています。実際にこのような作りにする場合は、変換後の文字列の領域がどれぐらい必要になるかを知るためにサイズを求める関数を別途用意するなど必要になると思います。
main.c
#include <stdio.h> #include "HTMLEscapedString.h" int main(void) { const char *src = "Amp:&,<include>,Quote:\""; const HTMLEscapedString * const dst = escape(src); printf("%s\n", src); putHTMLEscapedStrLn(dst); /* 警告が出る */ printf("%s\n", dst); return 0; }
Makefile
all : runAll runAll : main01 main02 ./main01 @echo "" LD_LIBRARY_PATH=. ./main02 # 共有ライブラリ使用版 main02 : main.o libHTMLEscapedString.so gcc -Wall main.o -L . -lHTMLEscapedString -o main02 # オブジェクトファイルリンク版 main01 : main.o HTMLEscapedString.o gcc -Wall main.o HTMLEscapedString.o -o main01 main.o : main.c HTMLEscapedString.h gcc -Wall -c main.c libHTMLEscapedString.so : HTMLEscapedString.c HTMLEscapedString.h gcc -Wall -shared -fPIC HTMLEscapedString.o -o libHTMLEscapedString.so HTMLEscapedString.o : HTMLEscapedString.c HTMLEscapedString.h gcc -Wall -c HTMLEscapedString.c clean : rm -f *.o *.so main01 main02
実行
オプジェクトファイルをリンク時に指定する方法(main01)と共有ライブラリを使用する方法で実行してみました。実行すると型が合わない旨の警告が出ています。
$ make
gcc -Wall -c main.c
main.c: In function ‘main’:
main.c:13:12: warning: format ‘%s’ expects argument of type ‘char *’, but argument 2 has type ‘const HTMLEscapedString * const {aka const struct HTMLEscapedString * const}’ [-Wformat=]
printf("%s\n", dst);
~^
gcc -Wall -c HTMLEscapedString.c
gcc -Wall main.o HTMLEscapedString.o -o main01
gcc -Wall -shared -fPIC HTMLEscapedString.o -o libHTMLEscapedString.so
gcc -Wall main.o -L . -lHTMLEscapedString -o main02
./main01
Amp:&,<include>,Quote:"
Amp:&,<include>,Quote:"
Amp:&,<include>,Quote:"
LD_LIBRARY_PATH=. ./main02
Amp:&,<include>,Quote:"
Amp:&,<include>,Quote:"
Amp:&,<include>,Quote:"
GCC:LD_PRELOADを使用したmallocの動作切替
今回もC言語の関数単体テスト系の話題です。mallocを利用する関数を試験する際にmallocのスタブを作成して単体試験を実行しようとすると単体試験のツール自体がmallocを使用していたりしてうまく動かないケースがあります。
このような場合、GDBを使用してmallocの戻り値を操作したりしていたのですが、LD_PRELOADを使用してmallocの動作を切り替えることができましたので紹介します。ネタもとは「Binary Hacks ―ハッカー秘伝のテクニック100選」のHACK#61「LD_PRELOADで既存の関数をラップする」です。
使用したのは以下のソースになります。
サンプルソースとコンパイル
malloc_stub.c
#define _GNU_SOURCE #include <dlfcn.h> #include <stdlib.h> static void *(*malloc0)(size_t size); void __attribute__((constructor)) init_malloc0(void) { malloc0 = dlsym(RTLD_NEXT, "malloc"); } void *malloc(size_t size) { if( !getenv("MALLOC_STUB") ) { /* 環境変数未定義時 */ return malloc0(size); } else { /* 環境変数定義時 */ return NULL; } }
環境変数MALLOC_STUBが定義されている場合はNULLを返すことにします。
このモジュールは共有ライブラリとしてコンパイルします。
$ gcc -shared -fPIC -o malloc_stub.so malloc_stub.c -ldl
GCC:-includeを使用したマクロ展開制御
C言語の関数単体テストを作成している際に関数形式マクロの展開を調整したいと思う部分が出てきました。使用していたコンパイラはGCCでマニュアルを見るとマクロの読み込みを制御するオプション(-include)がありましたので、使ってみました。
使用したのは以下のソースになります。
サンプルソース
macro.h
関数形式マクロが定義されているヘッダファイル
#ifndef __MACRO_H__ #define __MACRO_H__ #include <stdio.h> #define LOG(fmt, ...) printf("%s, %s, %d : " fmt, __func__, __FILE__, __LINE__, ##__VA_ARGS__) #endif
func.c
関数形式マクロを利用するモジュール
#include "macro.h" #include "func.h" int square(int x) { int ret = x * x; LOG("x = %d, x**2 = %d\n", x, ret); return ret; }
func.h
#ifndef __FUNC_H__ #define __FUNC_H__ int square(int); #endif
普通にプリプロセスを通した場合
$ gcc -E func.c
:
int square(int x)
{
int ret = x * x;
printf("%s, %s, %d : " "x = %d, x**2 = %d\n", __func__, "func.c", 7, x, ret);
return ret;
}普通にプリプロセスを通すとLOGが展開されてprintfになっていますが、
このprintf展開をfunc.c, func.hを変更せずにどうにかLOGのままにしたい。
GCCのオプションを調べると-includeが使えそうでした。
以下のようなテスト向けのヘッダファイルを用意してプリプロセスを行ってみます。
test.h
#ifdef LOG #undef LOG #endif
GCC -includeオプション使用
$ gcc -Wall -E -include macro.h -include test.h func.c
:
int square(int x)
{
int ret = x * x;
LOG("x = %d, x**2 = %d\n", x, ret);
return ret;
}LOGのまま残っています。
SPIN:状態の探索(2プロセス)(探索)
前回「Pr: 0 Tr: 6」で探索が切れているように見える部分が気になったので、デバッグしてみました。調べられた感じでは、プロセスの削除順序が関係しているようです。一応、「プロセスは生成順序と逆順で消滅する」と記載のある資料を見つけたのでこの記述の動作に該当してそうです。ただ、1次情報までは見つけられませんでした。
使用したソースから検証器の実行まで
ソース 2p.pmlを使用しています。検証器の生成とコンパイルも前回と同様となります。
デバッグ
トライ&エラーは省きますが、調べていくとdo_transitとdelprocに行き着きました。
(gdb) break do_transit
Breakpoint 1 at 0x404d: file pan.c, line 5887.
(gdb) break delproc
Breakpoint 2 at 0x93c6: file pan.c, line 10440.
(gdb) run
Starting program: /home/makoto/blog/16_delproc/pan
0: Down - program non-accepting [pids 1-0]
New state 0
State: 2,0,0,0,0,0,28,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,1,9,0,0,
Vector: 2,0,0,0,0,0,28,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,1,9,0,0,
:
(gdb) c
Continuing.
Pr: 0 Tr: 6 <-- 気になる部分
Breakpoint 2, delproc (sav=1, h=0) at pan.c:10440 <-- h=0はプロセスp
10440 { int d, i=0;
(gdb) n
10444 if (h+1 != (int) now._nr_pr)
(gdb)
10445 { return 0;
(gdb) list
10440 { int d, i=0;
10441 #ifndef NOCOMP
10442 int o_vsize = vsize;
10443 #endif
10444 if (h+1 != (int) now._nr_pr) <-- この条件が成立し
10445 { return 0; <-- delprocを抜けている。(プロセスqはまだ生きている。)
10446 }
10447 #ifdef TRIX
10448 #ifdef V_TRIX
10449 printf("%4d: delproc %d -- parent %d\n", depth, h, processes[h]->parent_pid);
(gdb) n
10530 }
(gdb)
do_transit (t=0x55555576c350, II=0) at pan.c:5910
5910 }
:
(gdb) n
new_state () at pan.c:7126
7126 { continue;
(gdb) list
7121 #ifdef INLINE
7122 #include FORWARD_MOVES
7123 P999: /* jumps here when move succeeds */
7124 #else
7125 if (!(_m = do_transit(t, II)))
7126 { continue; <-- このルートに入り次の探索に進んでいる。
7127 }
7128 #endif
7129 #ifdef BCS
7130 if (depth > BASE
デバッグ補助
上記をみるとソースにプリプロセスディレクディブが多く含まれてきます。これがあるとかなりソースが読みにくいです。実は、この結果に行き着く際にはpan.cに含まれているコメント「gcc -E -DNOREDUCE -DBITSTATE pan.c > ppan.c」を参考に以下のようにコンパイルしてデバッグしました。
$ gcc -E -DVERBOSE -DSDUMP -DNOCOMP -DNOREDUCE pan.c | indent -sob -st -bli0 | expand | sed '/^#/d' > ppan.c $ gcc -w -g3 ppan.c -o pan
SPIN:状態の探索(2プロセス)
今回は2プロセスが動作するサンプルモデルを作成して状態空間の探索を追ってみました。前回と同じように読み解けるかと思いきや、よくわからない動きを見ることとなりました。
使用したソースは以下となります。
使用したソースから検証器の実行まで
単に2プロセスが動作するできるだけ単純になるような以下のソースを用意しました。
ソース 2p.pml
byte a; active proctype p() { a = 170; /* 0xaa = -86 */ } byte b; active proctype q() { b = 187; /* 0xbb = -69 */ }
検証器の生成
$ spin -a -o2 2p.pml
検証器のコンパイル
$ gcc -w -g3 -DVERBOSE -DSDUMP -DNOCOMP -DNOREDUCE pan.c -o pan
実行結果
$ ./pan | cat -n
1 0: Down - program non-accepting [pids 1-0]
2 New state 0
3 State: 2,0,0,0,0,0,28,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,1,9,0,0,
4 Vector: 2,0,0,0,0,0,28,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,1,9,0,0,
5 Pr: 1 Tr: 3
6 0: proc 1 exec 3, 1 to 2, b = 187 non-accepting [tau=0]
7 1: Down - program non-accepting [pids 1-0]
8 New state 1
9 State: 2,0,0,0,0,0,28,0,0,-69,0,0,0,0,0,0,0,8,0,0,0,0,0,0,1,17,0,0,
10 Vector: 2,0,0,0,0,0,28,0,0,-69,0,0,0,0,0,0,0,8,0,0,0,0,0,0,1,17,0,0,
11 Pr: 1 Tr: 4
12 1: proc 1 exec 4, 2 to 0, -end- non-accepting [tau=0]
13 2: Down - program non-accepting [pids 0-0]
14 New state 2
15 State: 1,0,0,0,0,0,20,0,0,-69,0,0,0,0,0,0,0,8,0,0,
16 Vector: 1,0,0,0,0,0,20,0,0,-69,0,0,0,0,0,0,0,8,0,0,
17 Pr: 0 Tr: 5
18 2: proc 0 exec 5, 1 to 2, a = 170 non-accepting [tau=0]
19 3: Down - program non-accepting [pids 0-0]
20 New state 3
21 State: 1,0,0,0,0,0,20,0,-86,-69,0,0,0,0,0,0,0,16,0,0,
22 Vector: 1,0,0,0,0,0,20,0,-86,-69,0,0,0,0,0,0,0,16,0,0,
23 Pr: 0 Tr: 6
24 3: proc 0 exec 6, 2 to 0, -end- non-accepting [tau=0]
25 4: Down - program non-accepting [pids -1-0]
26 New state 4
27 State: 0,0,0,0,0,0,10,0,-86,-69,
28 Vector: 0,0,0,0,0,0,10,0,-86,-69,
29 4: no move [II=-1, tau=0, boq=-1]
30 4: Up - program
31 4: proc 0 reverses 6, 2 to 0
32 -end- [abit=0,adepth=0,tau=0,0]
33 3: Up - program
34 3: proc 0 reverses 5, 1 to 2
35 a = 170 [abit=0,adepth=0,tau=0,0]
36 2: Up - program
37 2: proc 1 reverses 4, 2 to 0
38 -end- [abit=0,adepth=0,tau=0,0]
39 Pr: 0 Tr: 5
40 1: proc 0 exec 5, 1 to 2, a = 170 non-accepting [tau=0]
41 2: Down - program non-accepting [pids 1-0]
42 New state 5
43 State: 2,0,0,0,0,0,28,0,-86,-69,0,0,0,0,0,0,0,16,0,0,0,0,0,0,1,17,0,0,
44 Vector: 2,0,0,0,0,0,28,0,-86,-69,0,0,0,0,0,0,0,16,0,0,0,0,0,0,1,17,0,0,
45 Pr: 1 Tr: 4
46 2: proc 1 exec 4, 2 to 0, -end- non-accepting [tau=0]
47 3: Down - program non-accepting [pids 0-0]
48 Old state 3
49 State: 1,0,0,0,0,0,20,0,-86,-69,0,0,0,0,0,0,0,16,0,0,
50 Vector: 1,0,0,0,0,0,20,0,-86,-69,0,0,0,0,0,0,0,16,0,0,
51 3: Up - program
52 3: proc 1 reverses 4, 2 to 0
53 -end- [abit=0,adepth=0,tau=0,0]
54 Pr: 0 Tr: 6
55 2: Up - program
56 2: proc 0 reverses 5, 1 to 2
57 a = 170 [abit=0,adepth=0,tau=0,0]
58 1: Up - program
59 1: proc 1 reverses 3, 1 to 2
60 b = 187 [abit=0,adepth=0,tau=0,0]
61 Pr: 0 Tr: 5
62 0: proc 0 exec 5, 1 to 2, a = 170 non-accepting [tau=0]
63 1: Down - program non-accepting [pids 1-0]
64 New state 6
65 State: 2,0,0,0,0,0,28,0,-86,0,0,0,0,0,0,0,0,16,0,0,0,0,0,0,1,9,0,0,
66 Vector: 2,0,0,0,0,0,28,0,-86,0,0,0,0,0,0,0,0,16,0,0,0,0,0,0,1,9,0,0,
67 Pr: 1 Tr: 3
68 1: proc 1 exec 3, 1 to 2, b = 187 non-accepting [tau=0]
69 2: Down - program non-accepting [pids 1-0]
70 Old state 5
71 State: 2,0,0,0,0,0,28,0,-86,-69,0,0,0,0,0,0,0,16,0,0,0,0,0,0,1,17,0,0,
72 Vector: 2,0,0,0,0,0,28,0,-86,-69,0,0,0,0,0,0,0,16,0,0,0,0,0,0,1,17,0,0,
73 2: Up - program
74 2: proc 1 reverses 3, 1 to 2
75 b = 187 [abit=0,adepth=0,tau=0,0]
76 Pr: 0 Tr: 6
77 1: Up - program
78 1: proc 0 reverses 5, 1 to 2
79 a = 170 [abit=0,adepth=0,tau=0,0]
80
81 (Spin Version 6.4.9 -- 17 December 2018)
82 + FullStack Matching
83
84 Full statespace search for:
85 never claim - (none specified)
86 assertion violations +
87 acceptance cycles - (not selected)
88 invalid end states +
89
90 State-vector 28 byte, depth reached 4, errors: 0
91 7 states, stored
92 2 states, matched
93 0 matches within stack
94 9 transitions (= stored+matched)
95 0 atomic steps
96 hash conflicts: 0 (resolved)
97 stackframes: 2/0
98
99 stats: fa 0, fh 0, zh 0, zn 0 - check 0 holds 0
100 stack stats: puts 0, probes 0, zaps 0
101 128.730 memory usage (Mbyte)
102
103 unreached in proctype p
104 (0 of 2 states)
105 unreached in proctype q
106 (0 of 2 states)
107
108 pan: elapsed time 0 seconds
結果のグラフ化
上記結果を読み解いていくと前回は出てこなかった以下のパターンが54, 76行目に出てきます。「Pr: 0 Tr: 6」の部分でいきなりスタックを巻き戻し、ぱっと見ると探索を中断しているように見えます。
51 3: Up - program
52 3: proc 1 reverses 4, 2 to 0
53 -end- [abit=0,adepth=0,tau=0,0]
54 Pr: 0 Tr: 6
55 2: Up - program
56 2: proc 0 reverses 5, 1 to 2
57 a = 170 [abit=0,adepth=0,tau=0,0] 73 2: Up - program
74 2: proc 1 reverses 3, 1 to 2
75 b = 187 [abit=0,adepth=0,tau=0,0]
76 Pr: 0 Tr: 6
77 1: Up - program
78 1: proc 0 reverses 5, 1 to 2
79 a = 170 [abit=0,adepth=0,tau=0,0]グラフ化したものが以下になります。「Pr: 0 Tr: 6」以降の部分は赤で表示させています。
ともに新規状態としても良さそうですが、なぜなんでしょうかね。
SPIN:状態探索(1プロセス,分岐あり)とグラフ化
SPINの検証器が状態空間をどのように探索しているのかが気になったので、状態ベクトルを出力させながら追ってみました。
使用したソースは以下となります。
使用したソースから検証器の実行まで
分岐を2箇所に用意した計4経路を通るような以下のソースを用意しました。
ソース branch.pml
byte a = 0; active proctype p() { if :: a = 170; /* 0xaa = -86 */ :: a = 187; /* 0xbb = -69 */ fi if :: a = 204; /* 0xcc = -52 */ :: a = 221; /* 0xdd = -35 */ fi }
検証器の生成
$ spin -a -o2 2p.pml
検証器のコンパイル
$ gcc -w -g3 -DVERBOSE -DSDUMP -DNOCOMP pan.c -o pan
実行結果
$ ./pan
0: Down - program non-accepting [pids 0-0]
New state 0
State: 1,0,0,0,0,0,20,0,0,0,0,0,0,0,0,0,0,12,0,0,
Vector: 1,0,0,0,0,0,20,0,0,0,0,0,0,0,0,0,0,12,0,0,
Pr: 0 Tr: 3
0: proc 0 exec 3, 3 to 7, a = 170 non-accepting [tau=0]
1: Down - program non-accepting [pids 0-0]
New state 1
State: 1,0,0,0,0,0,20,0,-86,0,0,0,0,0,0,0,0,28,0,0,
Vector: 1,0,0,0,0,0,20,0,-86,0,0,0,0,0,0,0,0,28,0,0,
Pr: 0 Tr: 5
1: proc 0 exec 5, 7 to 9, a = 204 non-accepting [tau=0]
2: Down - program non-accepting [pids 0-0]
New state 2
State: 1,0,0,0,0,0,20,0,-52,0,0,0,0,0,0,0,0,36,0,0,
Vector: 1,0,0,0,0,0,20,0,-52,0,0,0,0,0,0,0,0,36,0,0,
Pr: 0 Tr: 7
2: proc 0 exec 7, 9 to 0, -end- non-accepting [tau=0]
3: Down - program non-accepting [pids -1-0]
New state 3
State: 0,0,0,0,0,0,10,0,-52,0,
Vector: 0,0,0,0,0,0,10,0,-52,0,
3: no move [II=-1, tau=0, boq=-1]
3: Up - program
3: proc 0 reverses 7, 9 to 0
-end- [abit=0,adepth=0,tau=0,0]
2: Up - program
2: proc 0 reverses 5, 7 to 9
a = 204 [abit=0,adepth=0,tau=0,0]
Pr: 0 Tr: 6
1: proc 0 exec 6, 7 to 9, a = 221 non-accepting [tau=0]
2: Down - program non-accepting [pids 0-0]
New state 4
State: 1,0,0,0,0,0,20,0,-35,0,0,0,0,0,0,0,0,36,0,0,
Vector: 1,0,0,0,0,0,20,0,-35,0,0,0,0,0,0,0,0,36,0,0,
Pr: 0 Tr: 7
2: proc 0 exec 7, 9 to 0, -end- non-accepting [tau=0]
3: Down - program non-accepting [pids -1-0]
New state 5
State: 0,0,0,0,0,0,10,0,-35,0,
Vector: 0,0,0,0,0,0,10,0,-35,0,
3: no move [II=-1, tau=0, boq=-1]
3: Up - program
3: proc 0 reverses 7, 9 to 0
-end- [abit=0,adepth=0,tau=0,0]
2: Up - program
2: proc 0 reverses 6, 7 to 9
a = 221 [abit=0,adepth=0,tau=0,0]
1: Up - program
1: proc 0 reverses 3, 3 to 7
a = 170 [abit=0,adepth=0,tau=0,0]
Pr: 0 Tr: 4
0: proc 0 exec 4, 3 to 7, a = 187 non-accepting [tau=0]
1: Down - program non-accepting [pids 0-0]
New state 6
State: 1,0,0,0,0,0,20,0,-69,0,0,0,0,0,0,0,0,28,0,0,
Vector: 1,0,0,0,0,0,20,0,-69,0,0,0,0,0,0,0,0,28,0,0,
Pr: 0 Tr: 5
1: proc 0 exec 5, 7 to 9, a = 204 non-accepting [tau=0]
2: Down - program non-accepting [pids 0-0]
Old state 2
State: 1,0,0,0,0,0,20,0,-52,0,0,0,0,0,0,0,0,36,0,0,
Vector: 1,0,0,0,0,0,20,0,-52,0,0,0,0,0,0,0,0,36,0,0,
2: Up - program
2: proc 0 reverses 5, 7 to 9
a = 204 [abit=0,adepth=0,tau=0,0]
Pr: 0 Tr: 6
1: proc 0 exec 6, 7 to 9, a = 221 non-accepting [tau=0]
2: Down - program non-accepting [pids 0-0]
Old state 4
State: 1,0,0,0,0,0,20,0,-35,0,0,0,0,0,0,0,0,36,0,0,
Vector: 1,0,0,0,0,0,20,0,-35,0,0,0,0,0,0,0,0,36,0,0,
2: Up - program
2: proc 0 reverses 6, 7 to 9
a = 221 [abit=0,adepth=0,tau=0,0]
1: Up - program
1: proc 0 reverses 4, 3 to 7
a = 187 [abit=0,adepth=0,tau=0,0]
(Spin Version 6.4.9 -- 17 December 2018)
+ Partial Order Reduction
+ FullStack Matching
Full statespace search for:
never claim - (none specified)
assertion violations +
acceptance cycles - (not selected)
invalid end states +
State-vector 20 byte, depth reached 3, errors: 0
7 states, stored
2 states, matched
0 matches within stack
9 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
stackframes: 1/0
stats: fa 0, fh 0, zh 0, zn 0 - check 0 holds 0
stack stats: puts 0, probes 0, zaps 0
128.730 memory usage (Mbyte)
unreached in proctype p
(0 of 9 states)
pan: elapsed time 0 seconds
結果のグラフ化
上記の結果を見ると深さ優先探索で以下の流れて探索しています。
- 1経路目 : s1からs3まで探索して終了状態まで進み、s1まで戻っています。
- 2経路目 : s1からs5のまで探索し、s0まで戻っています。
- 3経路目 : s1からs6まで進み、遷移先s2が探索済みだったのでs6に戻っています。
- 4経路目 : s6からs4と進みますが、こちらも探索済みだったので、s0まで戻って探索終了となっています。
グラフ化したものが以下になります。
円形は状態で「State X」に対応するものを「sX」で、各状態でのaの値とプロセスの状態p(1:実行中,0:終了)を「a,p」で記載しています。四角は遷移で「Pr: A Tr: B」に対応するものを「trA,B」で記載しています。
