C Instrumentation Framework

Category:

Start date:

02/20/2012

Due date:

% Done:

Estimated time:

Published in build:

0491d9a

Description

Since we're going to actively use different static verifiers, we need to implement rerouter in the verifier independent way. The most appropriate place for this is to do it in CIF.

Files

testx.c (605 Bytes) testx.c

Evgeny Novikov, 03/28/2013 12:16 PM

Related issues 4 (2 open — 2 closed)

Related to Linux Driver Verification - Bug #3349: There is no initialization of ldv_mutex_TEMPLATE

Open

08/20/2012

Related to Linux Driver Verification - Bug #754: Rerouting does not work for static functions

Open

01/31/2011

Related to C Instrumentation Framework - Feature #1235: rerouting: add option to take into account struct name

Closed

05/19/2011

Blocked by C Instrumentation Framework - Bug #927: Aspectator doesn't ensure uniqueness for auxiliary generated functions

Closed

03/11/2011

Issue # Delay: days Cancel

History
Notes
Property changes

Actions

Updated by Alexey Khoroshilov almost 12 years ago

It would be good in addition to existing "rerouting" to support advanced version where $sign defined as a combination of field name and structure type.

Actions

Updated by Evgeny Novikov over 11 years ago

Status changed from Open to Resolved
Published in build set to 0491d9a

It was merged to master in commit 0491d9a. Local small testing has been passed successfully. Let's wait for night testing results.

Actions

Updated by Evgeny Novikov over 11 years ago

Project changed from Linux Driver Verification to C Instrumentation Framework
Category deleted (15)
Status changed from Resolved to Closed

Works quite fine.

Actions

Updated by Evgeny Novikov about 11 years ago

Status changed from Closed to Open

At the moment aspect (may be in BLAST too) rerouter heuristic may miss bugs! Here are 3 cases when this is possible:

int var;
int *ref = &var;
/* Rerouter will think that argument signatures are "var" and "ref". */
assert(&var == ref);

int var;
int *ref = &var;
int **ref_to_ref = &ref;
/* Rerouter will think that argument signatures are "var" and "ref_to_ref". */
assert(&var == *ref_to_ref);

...
struct S *s...;
int *ref = &s->field;
/* Rerouter will think that argument signatures are "field" or "field_of_S" and "ref". */
assert(&s->field == ref);

Actually rerouter should calculate an argument signature just in case when a corresponding actual argument is represented as taking address of some object (a variable or a field of a variable having either structural type or pointer to structural type).

Actions

Updated by Evgeny Novikov about 11 years ago

It seems that the only way to make sound analysis for these cases is to treat other cases then taking address of some object as universal argument signature that means that every calculated argument signature may fit to the given one. For instance, if one directly pass pointer variable to mutex_lock then for all arg_sign it should be called mutex_lock_arg_sign. The same is for mutex_unlock as well as other (un)locking functions.

Actions

Updated by Evgeny Novikov about 11 years ago

File testx.c testx.c added

File with several cases that break rerouter heuristic is attached. I couldn't imagine other essential examples as there.

Actions

Updated by Evgeny Novikov about 11 years ago

File testx.c added

Evgeny Novikov wrote:

At the moment aspect (may be in BLAST too) rerouter heuristic may miss bugs! Here are 3 cases when this is possible:
[...]
[...]
[...]

One more case:

struct A
{
  int x1;
  int x2;
} var;
struct A *ref = &var;
/* Rerouter will think that argument signatures are "x2" or "x2_of_A" and "NOT_ARG_SIGN". */
assert(&var.x2 == &ref->x1 + 1);

Actions

Updated by Evgeny Novikov about 11 years ago

File deleted (~~testx.c~~)

Actions

Updated by Evgeny Novikov about 11 years ago

Evgeny Novikov wrote:

It seems that the only way to make sound analysis for these cases is to treat other cases then taking address of some object as universal argument signature that means that every calculated argument signature may fit to the given one. For instance, if one directly pass pointer variable to mutex_lock then for all arg_sign it should be called mutex_lock_arg_sign. The same is for mutex_unlock as well as other (un)locking functions.

The only note, that mutex_lock and mutex_unlock should be called nondeterministically to avoid bug missing (if we acquire all mutexes and then some of them is released without actually been acquired we will lose a bug).

Actions

#10

Updated by Evgeny Novikov about 11 years ago

It seems that sound implementation of rerouter needs rule models to be extended rather considerably. When argument signature for, say, mutex_lock can't be calculated we need to call something like ldv_all_mutex_lock that will try to lock all known mutexes nondeterministically. "All" means that we should use template foreach like for ldv_initialize and ldv_check_final_state. Since there is neither iteration through model states nor nondeterminism in model for mutex_lock we better need to develop a separate model (that was called ldv_all_mutex_lock before). Since different functions have different sematics (some returns void, some returns error codes, some decrease counters) we need to develop such the separate models for all functions that have corresponding models already.

That's why some experiments should be executed before implementation. May be these experiments will show that we do can distinguish different object not only just by their names but also by names of references to them.

Actions