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」で記載しています。
SPIN,C言語,デバッグ:State Vectorと変数
「SpinIntro.pdf」の「SPIN's Basic Data Structures」を見ると状態ベクトル(State vecot)は全ての変数を保持している旨の記載があります。また、PanのCompile-Time Optionsには状態ベクトルをダンプするオプション(SDUMP)について記載があります。
コンパイルオプションを指定して状態ベクトルを出力させてみたのですが、読み方がわからず、私は読み方の情報も探せませんでした。ちょうどpanのソースはC言語なので変数の部分に着目してデバッグしてみました。
使用したソースは以下となります。
使用したソースから検証器の実行まで
ソース 2p.pml
byte a; active proctype p() { a = 170; /* 0xaa = -86 */ } byte b; active proctype q() { b = 187; /* 0xbb = -69 */ }
検証器の生成
検証器の生成時に-o2オプションを使用しています。今回使用したソースでは、-o2オプションを使用しないと変数a,bが状態ベクトルに含まれてきませんでした。これは、aとbを書き込みにのみ使用しているためと思われます。
$ spin -a -o2 2p.pml
実行結果
今回のケースではStateとVectorが同じ値になりました。(NOCOMPの効果?)
^が変数aとbの部分となります。顕著な変化があるのは以下の部分となります。
- New state 1 でStateが変化しています。0から-69になっている部分がbの部分でb = 187 によるものです。
- New state 3 でStateが変化しています。0から-86になっている部分がaの部分でa = 170 によるものです。
$ ./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,
^a^b
Pr: 1 Tr: 3
0: proc 1 exec 3, 1 to 2, b = 187 non-accepting [tau=0]
1: Down - program non-accepting [pids 1-0]
New state 1
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,
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,
^a^^^b
1: proc 1 PreSelected (tau=32)
Pr: 1 Tr: 4
1: proc 1 exec 4, 2 to 0, -end- non-accepting [tau=32]
2: Down - program non-accepting [pids 0-0]
New state 2
State: 1,0,0,0,0,0,20,0,0,-69,0,0,0,0,0,0,0,8,0,0,
Vector: 1,0,0,0,0,0,20,0,0,-69,0,0,0,0,0,0,0,8,0,0,
^a^^^b
Pr: 0 Tr: 5
2: proc 0 exec 5, 1 to 2, a = 170 non-accepting [tau=0]
3: Down - program non-accepting [pids 0-0]
New state 3
State: 1,0,0,0,0,0,20,0,-86,-69,0,0,0,0,0,0,0,16,0,0,
Vector: 1,0,0,0,0,0,20,0,-86,-69,0,0,0,0,0,0,0,16,0,0,
^^^a^^^b
Pr: 0 Tr: 6
3: proc 0 exec 6, 2 to 0, -end- non-accepting [tau=0]
4: Down - program non-accepting [pids -1-0]
New state 4
State: 0,0,0,0,0,0,10,0,-86,-69,
Vector: 0,0,0,0,0,0,10,0,-86,-69,
^^^a^^^b
4: no move [II=-1, tau=0, boq=-1]
4: Up - program
4: proc 0 reverses 6, 2 to 0
-end- [abit=0,adepth=0,tau=0,0]
3: Up - program
3: proc 0 reverses 5, 1 to 2
a = 170 [abit=0,adepth=0,tau=0,0]
2: Up - program
2: proc 1 reverses 4, 2 to 0
-end- [abit=0,adepth=0,tau=0,32]
1: Up - program
1: proc 1 reverses 3, 1 to 2
b = 187 [abit=0,adepth=0,tau=32,0]
Pr: 0 Tr: 5
0: proc 0 exec 5, 1 to 2, a = 170 non-accepting [tau=0]
1: Down - program non-accepting [pids 1-0]
New state 5
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,
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,
^a^^^b
Pr: 1 Tr: 3
1: proc 1 exec 3, 1 to 2, b = 187 non-accepting [tau=0]
2: Down - program non-accepting [pids 1-0]
New state 6
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,
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,
^^^a^^^b
2: proc 1 PreSelected (tau=32)
Pr: 1 Tr: 4
2: proc 1 exec 4, 2 to 0, -end- non-accepting [tau=32]
3: Down - program non-accepting [pids 0-0]
Old state 3
State: 1,0,0,0,0,0,20,0,-86,-69,0,0,0,0,0,0,0,16,0,0,
Vector: 1,0,0,0,0,0,20,0,-86,-69,0,0,0,0,0,0,0,16,0,0,
^^^a^^^b
3: Up - program
3: proc 1 reverses 4, 2 to 0
-end- [abit=0,adepth=0,tau=0,32]
2: Up - program
2: proc 1 reverses 3, 1 to 2
b = 187 [abit=0,adepth=0,tau=32,0]
Pr: 0 Tr: 6
1: Up - program
1: proc 0 reverses 5, 1 to 2
a = 170 [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 28 byte, depth reached 4, errors: 0
7 states, stored
1 states, matched
0 matches within stack
8 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
stackframes: 2/0
stats: fa 0, fh 0, zh 0, zn 0 - check 3 holds 2
stack stats: puts 0, probes 0, zaps 0
128.730 memory usage (Mbyte)
unreached in proctype p
(0 of 2 states)
unreached in proctype q
(0 of 2 states)
pan: elapsed time 0 seconds
State の出力部分をGDBで調べる
実際にデバッグした際はmainから調べるなどトライ&エラーしていますが、以下の説明ではその辺りは省略しています。
pan実行時のState:...部分を出力しているdumpstate関数にブレークポイントを設定することからデバッグを始めています。
$ gdb ./pan
GNU gdb (Ubuntu 8.1-0ubuntu3) 8.1.0.20180409-git
Copyright (C) 2018 Free Software Foundation, Inc.
License GPLv3+: GNU GPL version 3 or later <http://gnu.org/licenses/gpl.html>
This is free software: you are free to change and redistribute it.
There is NO WARRANTY, to the extent permitted by law. Type "show copying"
and "show warranty" for details.
This GDB was configured as "x86_64-linux-gnu".
Type "show configuration" for configuration details.
For bug reporting instructions, please see:
<http://www.gnu.org/software/gdb/bugs/>.
Find the GDB manual and other documentation resources online at:
<http://www.gnu.org/software/gdb/documentation/>.
For help, type "help".
Type "apropos word" to search for commands related to "word"...
Reading symbols from ./pan...done.
(gdb) break dumpstate <-- トライ&エラーでこの関数でState: ...の部分が出力されいることを予め調べています。
Breakpoint 1 at 0xa050: file pan.c, line 11346.
(gdb) run
Starting program: /home/makoto/blog/13/pan
0: Down - program non-accepting [pids 1-0]
New state 0
Breakpoint 1, dumpstate (wasnew=-1, v=0x55555576d1e0 <now> "\002", n=28, tag=1) at pan.c:11346
11346 printf(" State: ");
(gdb) until
11351 for (i = 0; i < vsize; i++)
(gdb)
11352 printf("%d,", ((char *)&now)[i]); <-- ここでコンマセパレートで出力されています。
(gdb)
11351 for (i = 0; i < vsize; i++)
(gdb)
11354 printf("\n Vector: ");
(gdb)
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,
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
出力されているのは、nowの値のようです。
11355 for (i = 0; i < n; i++)
(gdb) ptype now <-- nowの型を調べます。
type = struct State {
unsigned char _nr_pr;
unsigned char _nr_qs;
unsigned char _a_t;
unsigned char _cnt[2];
unsigned short _vsz;
unsigned char a; <-- 変数a
unsigned char b; <-- 変数b
unsigned char sv[1024];
}
(gdb) l 11352
11347 #if !defined(NOCOMP) && !defined(HC)
11348 for (i = 0; i < vsize; i++) printf("%d%s,",
11349 ((char *)&now)[i], Mask[i]?"*":"");
11350 #else
11351 for (i = 0; i < vsize; i++)
11352 printf("%d,", ((char *)&now)[i]); <-- NOCOMPを定義しているのでこのルートを通ります。
11353 #endif
11354 printf("\n Vector: ");
11355 for (i = 0; i < n; i++)
11356 printf("%d,", v[i]);
(gdb) continue
Continuing.
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,
Pr: 1 Tr: 3
0: proc 1 exec 3, 1 to 2, b = 187 non-accepting [tau=0]
1: Down - program non-accepting [pids 1-0]
New state 1
Breakpoint 1, dumpstate (wasnew=-1, v=0x55555576d1e0 <now> "\002", n=28, tag=2) at pan.c:11346
^^^^^^^^^^^^2回目のブレークなので、b=187が実行された後となります。
11346 printf(" State: ");
(gdb) p now
$1 = {_nr_pr = 2 '\002', _nr_qs = 0 '\000', _a_t = 0 '\000', _cnt = "\000", _vsz = 28, a = 0 '\000',
b = 187 '\273',
sv = "\000\000\000\000\000\000\000\b\000\000\000\000\000\000\001\021", '\000' <repeats 1007 times>}
-> nowの中身を見るとbは187となっています。
(gdb) until
11351 for (i = 0; i < vsize; i++)
(gdb)
11352 printf("%d,", ((char *)&now)[i]);
(gdb)
11351 for (i = 0; i < vsize; i++)
(gdb)
11354 printf("\n Vector: ");
(gdb)
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,
^^^^^^^^^^^^^^^^^^^^^^^
+0,1,2,3,4,5, 6,7,8, 9
-> 9個目がbの場所となります。詳細を調べてみます。
11355 for (i = 0; i < n; i++)
(gdb) printf "%d\n", (char)187
-69
(gdb) p (char *)(&now.b) - (char *)&now <-- nowの先頭とnow.bの差を確認する。
$9 = 9
(gdb) x/16x &now
+0 +1 +2 +3 +4 +5 +6 +7
0x55555576d1e0 <now>: 0x02 0x00 0x00 0x00 0x00 0x00 0x1c 0x00
+8 +9
0x55555576d1e8 <now+8>: 0x00 0xbb 0x00 0x00 0x00 0x00 0x00 0x00状態aとbを保持したState型の変数nowがコンマセパレートで出力されていました。
C言語:ビットフィールド
SPINのstate vector(状態ベクトル?)が気になってデバッグしているときに、pan.cでビットフィールドが使われている箇所を見つけました。
C言語の本で存在は知っていたのですが、使用したこともなく、また実際のコードで見たのは初めてでした。state vectorの理解にも必要になりそうだったので、pan.cを参考にコードを作成し動作を確認してみました。
確認に使用したコードは以下のものになります。
ソース bitfield.c
#include <stdio.h> #include <string.h> /* ビットフールドを使用した構造体 */ struct P1 { unsigned int _pid : 8; unsigned int _t : 3; unsigned int _p : 3; }; /* pan.cのソースコードを参考にダンプ用の関数を作成 */ void dumpstate(struct P1 *p) { int i; char *cp = (char *)p; for (i = 0; i < sizeof(struct P1); i++, cp++) { printf("%d,", *cp); } putchar('\n'); cp = (char *)p; for (i = 0; i < sizeof(struct P1); i++, cp++) { printf("0x%02x,", *cp); } putchar('\n'); } int main(void) { struct P1 p1; memset(&p1, 0x00, sizeof(struct P1)); dumpstate(&p1); p1._pid = 1; dumpstate(&p1); p1._t = 1; dumpstate(&p1); p1._p = 1; dumpstate(&p1); p1._pid = 0xff; dumpstate(&p1); p1._t = 3; dumpstate(&p1); p1._p = 3; dumpstate(&p1); return 0; }
コンパイルから実行まで
gdbでデバッグも行いたいので -g3 オプションを付与してコンパイルしています。
コンパイルと実行結果
$ gcc -Wall -g3 bitfield.c $ ./a.out 0,0,0,0, 0x00,0x00,0x00,0x00, 1,0,0,0, <- p1._pid = 1 の実行後 0x01,0x00,0x00,0x00, 1,1,0,0, <- p1._t = 1 の実行後 0x01,0x01,0x00,0x00, 1,9,0,0, <- p1._p = 1 の実行後 0x01,0x09,0x00,0x00, -1,9,0,0, 0xffffffff,0x09,0x00,0x00, <- p1._pid = 0xff の実行後 -1,11,0,0, 0xffffffff,0x0b,0x00,0x00, <- p1._t = 3 の実行後 -1,27,0,0, 0xffffffff,0x1b,0x00,0x00, <- p1._p = 3 の実行後
gdbでの実行
$ gdb ./a.out
GNU gdb (Ubuntu 8.1-0ubuntu3) 8.1.0.20180409-git
Copyright (C) 2018 Free Software Foundation, Inc.
License GPLv3+: GNU GPL version 3 or later <http://gnu.org/licenses/gpl.html>
This is free software: you are free to change and redistribute it.
There is NO WARRANTY, to the extent permitted by law. Type "show copying"
and "show warranty" for details.
This GDB was configured as "x86_64-linux-gnu".
Type "show configuration" for configuration details.
For bug reporting instructions, please see:
<http://www.gnu.org/software/gdb/bugs/>.
Find the GDB manual and other documentation resources online at:
<http://www.gnu.org/software/gdb/documentation/>.
For help, type "help".
Type "apropos word" to search for commands related to "word"...
Reading symbols from ./a.out...done.
(gdb) break main
Breakpoint 1 at 0x7f3: file bitfield.c, line 32.
(gdb) run
Starting program: /home/makoto/blog/12/a.out
Breakpoint 1, main () at bitfield.c:32
32 {
(gdb) n
35 memset(&p1, 0x00, sizeof(struct P1));
(gdb)
36 dumpstate(&p1);
(gdb)
0,0,0,0,
0x00,0x00,0x00,0x00,
38 p1._pid = 1;
(gdb) p sizeof(struct P1)
$1 = 4
(gdb) x/4tb &p1
0x7fffffffdc74: 00000000 00000000 00000000 00000000
(gdb) n
39 dumpstate(&p1);
(gdb) n
1,0,0,0,
0x01,0x00,0x00,0x00,
41 p1._t = 1;
(gdb) x/4tb &p1
0x7fffffffdc74: 00000001 00000000 00000000 00000000
^^^^^^^^_pid部分
(gdb) n
42 dumpstate(&p1);
(gdb) n
1,1,0,0,
0x01,0x01,0x00,0x00,
44 p1._p = 1;
(gdb) x/4tb &p1
0x7fffffffdc74: 00000001 00000001 00000000 00000000
^^^_p部分
(gdb) n
45 dumpstate(&p1);
(gdb)
1,9,0,0,
0x01,0x09,0x00,0x00,
47 p1._pid = 0xff;
(gdb) x/4tb &p1
0x7fffffffdc74: 00000001 00001001 00000000 00000000
^^^_t部分
(gdb) n
48 dumpstate(&p1);
(gdb)
-1,9,0,0,
0xffffffff,0x09,0x00,0x00,
50 p1._t = 3;
(gdb) x/4tb &p1
0x7fffffffdc74: 11111111 00001001 00000000 00000000
^^^^^^^^_pid部分
(gdb) n
51 dumpstate(&p1);
(gdb)
-1,11,0,0,
0xffffffff,0x0b,0x00,0x00,
53 p1._p = 3;
(gdb) x/4tb &p1
0x7fffffffdc74: 11111111 00001011 00000000 00000000
^^^_p部分
(gdb) n
54 dumpstate(&p1);
(gdb)
-1,27,0,0,
0xffffffff,0x1b,0x00,0x00,
56 return 0;
(gdb) x/4tb &p1
0x7fffffffdc74: 11111111 00011011 00000000 00000000
^^^_t部分
(gdb) n
57 }
構造体とメモリ
上記のようにgdbでp1を保存しているメモリをバイナリダンプで出力した結果を見ると、私の環境では以下のようになっているということですね。
+0バイト +1バイト
アドレス iiiiiiii 00tttppp
^^^^^^^^ |||---
^ : _pid 部分 8ビット
- : _p 部分 3ビット
| : _t 部分 3ビット_pと_tとメモリの位置を間違えてしまいそうです。
