Feature #1306
openImplement -fdepth option in the more intellectual way
Added by Evgeny Novikov about 13 years ago. Updated almost 13 years ago.
0%
Description
As was mentioned in #1236 issue this should be done because in particular we don't want or even we cannot restrict our model functions to have "ldv_" prefix.
Updated by Pavel Shved about 13 years ago
- Category set to BLAST
- Assignee set to Pavel Shved
- Priority changed from Normal to High
I'd assign it a higher priority. If we really want it, we should get it done before we make too many models.
Besides, this feature alone has some "scientific" value, which could advance our project's visibility.
Updated by Alexey Khoroshilov about 13 years ago
It should help to fix this false positive:
ldv-git(-fdepth 7):68_1:drivers/mtd/nand/alauda.ko:linux-2.6.39-rc7
where usb_free_urb() is cut off by -fdepth logic that works incorrectly without ldv_ prefix.
Updated by Pavel Shved almost 13 years ago
- Due date set to 08/18/2011
- Status changed from New to Open
Okay, so the current idea is to implement the following functionality:
Only traverse to a function if the stack depth less than N, or this function, directly or indirectly, contains one of the labels specified, which should include, but not be limited to the error label.
I will start implementing it today.
Updated by Alexey Khoroshilov almost 13 years ago
How will it work with recursive functions containing the label?
Updated by Pavel Shved almost 13 years ago
Recursive calls are ignored in BLAST regardless of call stack depth constraints.
Or, do I miss something?
Updated by Pavel Shved almost 13 years ago
Your example does not finish on my machine due to insufficient resources. Do you have more of these?
Meanwhile, I realized that it's not the best solution possible. The thing is that we want to actually "mark" certain functions as "important", and this marking includes but is not limited by error labels.
Using labels for marking is not the best option. The thing is that we should insert a goto to a function body for the label to be spotted by backends of various C transforming tools. We could mark it with an impossible if operator, like this:
void ldv_spin_lock(void)
{
if (0) LABEL: goto LABEL;
/* actual code */
}
However, this if operator will be seen in the error trace.
We could place the goto after the return statement, so that it will definitely be not shown in the trace. However, BLAST asks CIL to remove such unreachable code (and, I suppose, other C transformation tools, such as Aspectator, may discard such gotos as well), and can't find the label entirely.
A more natural way to "mark" functions is to use GCC function attributes. They are non-portable, however, but our toolchain, and the primary domain, linux device drivers, supports and uses them.
So, tomorrow, I'll retool my fixes to function attributes. Embedding them into models will be straightforward.
Updated by Pavel Shved almost 13 years ago
Hm. When I got to aspectator-powered models, it stopped working, because Aspectator does not preserve these attributes, and the files generated do contain neither ldv_model nor ldv_model_inline. I guess, C backend just can't print attributes unrecognized by GCC, which the attributes I added are.
So, if we want to use the attributes, we should teach our GCC to preserve them as if they're its native ones. Not that hard, I guess... but are there any other solutions?
Updated by Evgeny Novikov almost 13 years ago
Yes... Unfortunately at the moment C backend doesn't touch GCC attributes at all. And I also guess that their support can be added rather simply (especially in case of some specific kind of attributes, like for functions).
Updated by Alexey Khoroshilov almost 13 years ago
- Priority changed from Normal to High