Feature #2462
closedWe should develop "rerouter" functionality inside CIF
0%
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
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.
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.
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.
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).
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.
Updated by Evgeny Novikov about 11 years ago
File with several cases that break rerouter heuristic is attached. I couldn't imagine other essential examples as there.
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);
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).
Updated by Evgeny Novikov almost 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.
Updated by Evgeny Novikov over 9 years ago
- Priority changed from High to Normal
Updated by Alexey Khoroshilov over 9 years ago
What is a purpose to have this issue open?
Updated by Evgeny Novikov over 9 years ago
- Status changed from Open to Closed
I created a new feature request #5287 for further experiments with rerouter.