Bug #338
closedCIL can't preprocess__padding or __builtin_offsetof in rules 60_1 and 68_1
Added by Pavel Shved about 14 years ago. Updated almost 13 years ago.
0%
Description
They yield a lot of well-known simplemem: Temporary needed outside a function
exceptions.
Updated by Evgeny Novikov almost 14 years ago
- Category changed from Rules and Models to BLAST
- Assignee deleted (
Vadim Mutilin) - Priority changed from Normal to High
- Detected in build changed from ldv to 476a75
The related user story is S-01116.
In general the problem is in BLAST frontend (CIL).
I investigate the given problem while waiting for comments for statistics server improvements. The problem is related with changing in kernel headers as well as other such problems. This particular problem is caused by following changes in include/linux/spinlock_types.h
for example for linux-2.6.34.7
kernel:
typedef struct spinlock { union { struct raw_spinlock rlock; #ifdef CONFIG_DEBUG_LOCK_ALLOC # define LOCK_PADSIZE (offsetof(struct raw_spinlock, dep_map)) struct { u8 __padding[LOCK_PADSIZE]; struct lockdep_map dep_map; }; #endif }; } spinlock_t;
After preprocessing (note that aspectator isn't involved at all!) we have:
typedef struct spinlock { union { struct raw_spinlock rlock; struct { u8 __padding[(__builtin_offsetof(struct raw_spinlock,dep_map))]; struct lockdep_map dep_map; }; }; } spinlock_t;
When CIL encounter this construction u8 __padding[(__builtin_offsetof(struct raw_spinlock,dep_map))];
it tries to create 'temporary outside a function'.
- Fix CIL since it doesn't process correct programs (however this may be some of gcc extensions or so on). It may be very difficult (not supposed in this issue...).
- Make workaround 1. Undefine CONFIG_DEBUG_LOCK_ALLOC macro as well as for 32 rule (that works). Isn't correct and not general but the problem will be gone.
- Make workaround 2. Kernel patch that comment or drop complex structure. Less incorrect but also not general solution.
Any ideas?
Updated by Alexey Khoroshilov almost 14 years ago
In long term I would prefer the first approach (fixing CIL) and it would be good to have such kind of fixes accepted by upstream.
Updated by Evgeny Novikov almost 14 years ago
- Status changed from New to Resolved
- Assignee set to Evgeny Novikov
- Published in build set to ed1171a
Currently it was fixed by small kernel header patch (3d case). Verified with small external drivers and small kernel driver directory.
Updated by Evgeny Novikov almost 14 years ago
- Status changed from Resolved to Feedback
Now this models can be included to the ldv-online and ldv-git check lists, aren't they?
Updated by Pavel Shved almost 14 years ago
- Subject changed from Rules 60_1 and 68_1don't work with latest kernels to CIL can't preprocess__padding or __builtin_offsetof in rules 60_1 and 68_1
- Status changed from Feedback to Open
- Assignee deleted (
Evgeny Novikov) - Priority changed from High to Low
It seems that the current fix works well, although it's not the ideal solution.
I'm renaming the bug and lowering the priority.
Updated by Evgeny Novikov over 13 years ago
I believe that we'll able to use a pure ldv gcc pretty printer without any instrumentation to calculate such constants and release CIL from doing this "gcc" work.
Updated by Alexey Khoroshilov over 13 years ago
I do not know if it is the same problem, but 1006 of 1012 checks for 68 rule in my latest run fails with:
ZZZ: Exception: Failure("simplemem: temporary needed outside a function")
Updated by Pavel Shved over 13 years ago
- Priority changed from Low to Normal
Several months later, I, personally, have changed my opinion about such errors.
If we want to be a verification platform, we should prefer simplifying the C code to fixing our frontend (while the latter isn't that bad itself). An offset of a field a structure is a well-known trick of using (int) ( &((struct STRUCT*)0->FIELD) )
. This is quite a standard feature, and I hope that it doesn't make CIL fail.
By the way, reference launches of 68_1 on kernel 2.6.38.2 look okay, without a lot of creepy simplemem failures.
Updated by Alexey Khoroshilov over 13 years ago
- Priority changed from Normal to High
The rule 68_1 does not work at all in my runs of ldv-git on linux-3.0-rcX because of "simplemem: temporary needed outside a function".
Updated by Alexey Khoroshilov about 13 years ago
- Priority changed from High to Urgent
Increasing priority since the rule does not work at all.
Updated by Evgeny Novikov about 13 years ago
I saw briefly notes to this bug and after all I assume that using aspectator instead of plain mode can really help. For instance, here gcc built-in function is most likely to be calculated in aspectator using.
Updated by Pavel Shved about 13 years ago
- Due date set to 08/10/2011
- Assignee set to Pavel Shved
Will try to fix it now.
Updated by Pavel Shved about 13 years ago
- Status changed from Open to Resolved
Fixed in commit:d8a9b64. Tested on LDV-Git, and after verifying that it started to pass parsing stage, I also turned on 68_1 and 60_1 rules there by default!
Updated by Pavel Shved about 13 years ago
- Project changed from Linux Driver Verification to BLAST
- Category deleted (
BLAST)
Updated by Pavel Shved almost 13 years ago
- Status changed from Resolved to Closed
I have just taken a look at Alexey's ldv-git run, and didn't find any alarming signs in 68_1 rule processing. Rule 60 hasn't been run at all, though.
So, closing this. Reopen if the error appears again.