Linux Driver Verification

In the drivers/net/cassini.ko driver I found an interesting missing unsafe with the plain_sorted_withcheck envmodel, but which was found by seq_inf_withcheck_stateful.

In the function cas_get_ethtool_stats the driver checks assertion

BUG_ON(i != CAS_NUM_STAT_KEYS);

where i=16, because it was icremented 16 times from zero and Lattice knows it.
But calculation of CAS_NUM_STAT_KEYS goes wrong. The macro CAS_NUM_STAT_KEYS expands to ARRAY_SIZE calculation.

#define ARRAY_SIZE(arr) (sizeof(arr) / sizeof((arr)[0]) + __must_be_array(arr))

where we __must_be_array is a build time check using BUILD_BUG_ON_ZERO.

Preprocessed expression looks like:

!!(i != (sizeof(ethtool_cassini_statnames) / sizeof((ethtool_cassini_statnames)[0]) + (sizeof(char[1 - 2 * !!(__builtin_types_compatible_p(typeof(ethtool_cassini_statnames), typeof(&ethtool_cassini_statnames[0])))]) - 1)))

For BLAST it appeares to be

32768  / 2048  +  64 -  1

where 64 - 1 comes from build time checks and is incorrect.

As a result analysis stops at BUG_ON statement in an endless loop

for (;;) ;

which is defined in kernel headers for failed checks.