Linux Driver Verification » BLAST

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;

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'.

1. 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...).
2. 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.
3. Make workaround 2. Kernel patch that comment or drop complex structure. Less incorrect but also not general solution.

Any ideas?

Currently it was fixed by small kernel header patch (3d case). Verified with small external drivers and small kernel driver directory.

Now this models can be included to the ldv-online and ldv-git check lists, aren't they?

It seems that the current fix works well, although it's not the ideal solution.

I'm renaming the bug and lowering the priority.

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.

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".

Increasing priority since the rule does not work at all.

Will try to fix it now.

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!

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.