blob: 7ea7f7caa2ef925e202e4f69baa9f1d7acd67d83 [file] [log] [blame]
@ 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);
}