| @ 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); |
| } |