Project

General

Profile

Actions

Feature #2462

closed

We should develop "rerouter" functionality inside CIF

Added by Evgeny Novikov almost 13 years ago. Updated about 10 years ago.

Status:
Closed
Priority:
Normal
Category:
-
Start date:
02/20/2012
Due date:
% Done:

0%

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 open2 closed)

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

Actions
Related to Linux Driver Verification - Bug #754: Rerouting does not work for static functionsOpenEvgeny Novikov01/31/2011

Actions
Related to C Instrumentation Framework - Feature #1235: rerouting: add option to take into account struct nameClosedEvgeny Novikov05/19/2011

Actions
Blocked by C Instrumentation Framework - Bug #927: Aspectator doesn't ensure uniqueness for auxiliary generated functions ClosedEvgeny Novikov03/11/2011

Actions
Actions #1

Updated by Alexey Khoroshilov over 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 #2

Updated by Evgeny Novikov about 12 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 #3

Updated by Evgeny Novikov about 12 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 #4

Updated by Evgeny Novikov over 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 #5

Updated by Evgeny Novikov over 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 #6

Updated by Evgeny Novikov over 11 years ago

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

Actions #7

Updated by Evgeny Novikov over 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 #8

Updated by Evgeny Novikov over 11 years ago

  • File deleted (testx.c)
Actions #9

Updated by Evgeny Novikov over 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 over 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 #11

Updated by Evgeny Novikov about 10 years ago

  • Priority changed from High to Normal
Actions #12

Updated by Alexey Khoroshilov about 10 years ago

What is a purpose to have this issue open?

Actions #13

Updated by Evgeny Novikov about 10 years ago

  • Status changed from Open to Closed

I created a new feature request #5287 for further experiments with rerouter.

Actions

Also available in: Atom PDF