1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
|
@ find_drv_name @
identifier drv;
identifier mutex;
@@
pthread_mutex_protects_3(&drv->mutex, ...);
@ find_hint @
type T;
T *drv;
identifier mutex, item_1, item_2, item_3;
@@
pthread_mutex_protects_3(&drv->mutex, drv->item_1, drv->item_2, drv->item_3);
@ add_instrumentation_vars @
type find_hint.T;
identifier find_hint.mutex, find_hint.item_1, find_hint.item_2, find_hint.item_3;
type T1, T2;
fresh identifier instr_item_1 = "__instr_" ## item_1;
fresh identifier instr_item_2 = "__instr_" ## item_2;
fresh identifier instr_item_3 = "__instr_" ## item_3;
@@
T {
...
+ int instr_item_1;
T1 item_1;
...
+ int instr_item_2;
T2 item_2;
...
+ int instr_item_3;
T2 item_3;
...
};
@ add_counter depends on add_instrumentation_vars @
type find_hint.T;
identifier find_hint.mutex, find_hint.item_1, find_hint.item_2, find_hint.item_3;
identifier find_drv_name.drv;
fresh identifier fn_instr = "__instr_" ## mutex;
@@
#include <string.h>
+
+T;
+static void fn_instr(T *drv)
+{
+}
+
@ find_pthread_fn depends on find_hint @
identifier fn, ret;
expression thread, attr, val;
@@
ret = pthread_create(thread, attr, fn, val);
@ check_fn_access @
identifier find_pthread_fn.fn;
type find_hint.T;
T *drv;
//identifier find_drv_name.drv;
identifier add_counter.fn_instr;
identifier find_hint.mutex;
identifier find_hint.item_1;
identifier find_hint.item_2;
identifier find_hint.item_3;
@@
fn (...)
{
<+...
(
drv->item_1
|
drv->item_2
|
drv->item_3
)
...+>
+
+ /* top level routine accesses drv */
+ fn_instr(drv);
+
}
@ check_helpers depends on find_pthread_fn @
identifier helper;
identifier find_pthread_fn.fn;
identifier find_hint.mutex;
type find_hint.T;
T *drv;
@@
fn (...)
{
<+... when != pthread_mutex_lock(&drv->mutex);
+ /* going to check this routine */
helper(...);
...+>
}
@ helper_accessing_with_lock exists @
identifier check_helpers.helper;
type find_hint.T;
T *drv;
identifier find_hint.mutex;
identifier find_hint.item_1;
identifier find_hint.item_2;
identifier find_hint.item_3;
position p1, p2;
identifier add_counter.fn_instr;
@@
helper(...)
{
...
pthread_mutex_lock@p1(&drv->mutex);
<+...
(
drv->item_1
|
drv->item_2
|
drv->item_3
)
...+>
pthread_mutex_unlock@p2(&drv->mutex);
+ /* routine had a lock */
+ fn_instr(drv);
}
@ helper_accessing_without_lock exists @
identifier check_helpers.helper;
type find_hint.T;
T *drv;
identifier find_hint.mutex;
identifier find_hint.item_1;
identifier find_hint.item_2;
identifier find_hint.item_3;
identifier add_counter.fn_instr;
@@
helper(...)
{
<+... when != pthread_mutex_lock(&drv->mutex);
(
drv->item_1
|
drv->item_2
|
drv->item_3
)
...+>
+ /* was missing lock */
+ fn_instr(drv);
}
|
