Linux Driver Verification » Linux Kernel Safety RuleDB

Evgeny Novikov wrote:

The bug fixed in commit 39a1d13 of linux-stable branch is found both with BLAST and CPAchecker.

BTW, it requires a special hack to make CPAchecker work:

// HACK for CPAchecker that allows to avoid CIL parsing errors.
around: define(test_bit(nr, addr))
{
0
}

struct net_device {
  ...
  char                    name[IFNAMSIZ];
...
static inline char const *netdev_name(struct net_device const *dev)
{
  ...
  return ( char const *) & ( * dev ) . name;
}

__inline static char const   *netdev_name(struct net_device  const  *dev ).
{ 
  ...
  char ( const  (*__cil_tmp7))[16U] ;

  {
  {
#line 2232
  __cil_tmp7 = (char ( const  (*))[16U])dev;
#line 2232
  return ((char const   *)__cil_tmp7);
  }
}
}

test_bit workaround helps to fix similar issue as described.

Produced by CIL code isn't a valid C code. So it isn't surprising that it breaks CPAchecker frontend.

Unfortunately, I cannot make a simple workaround for the given issue (say, with help of aspectator, because it cannot completely remove a function definition). Just manual fix of code allows to avoid it.

__blk_put_request() was added in this model.

There was an attempt to check arguments of blk_execute_rq_nowait(): if the last argument is blk_end_sync_rq, it isn't need to call blk_put_request(). But it's a problem to test it.

Also the model should check function call in operation "req->end_io = ...", where req = blk_get_request() or blk_make_request().

Another issue:

    /*Check the last argument of blk_[make|get]_request. If it's one of this values it's isn't necessary to check res on error*/
    if (mask == __GFP_WAIT || mask == GFP_KERNEL || mask == GFP_NOIO)
        /* LDV_COMMENT_CHANGE_STATE Get blk request. */
        ldv_blk_rq = LDV_BLK_RQ_GOT;

Why res is not updated in this branch?

If the last argument of function (gfp_t gfp_mask) is __GFP_WAIT, we don't need to check function return value. The structure of function blk_get_request() is:

static struct request *get_request(struct request_queue *q, int rw_flags, struct bio *bio, gfp_t gfp_mask) {
    ...
retry:
    rq = __get_request(rl, rw_flags, bio, gfp_mask);
    ...
    if (!(gfp_mask & __GFP_WAIT) || unlikely(blk_queue_dead(q))) {
        blk_put_rl(rl);
        return NULL;
    }
    ...
    goto retry;
}

So, if the mask is __GFP_WAIT, function will try to get request again and again.
But if the mask has another value, the model checks blk_get_request() return value.

Now 5 of 6 false positives are due to the model successfully obtains a request with __GFP_WAIT flags but returns 0. It should return nonzero value in case of blk_get_request() and non pointer error value in case of blk_make_request().

1. Possible NULL pointer dereference
2. Possible NULL pointer dereference
3. Possible NULL pointer dereference
4. Excessive check of blk_get_request() return value
5. ...

Developers have ignored patches sent by Marina because of:
drivers/ide is obsolete and scheduled for removal
although Sergei answered:
It's being maintained for bug fixes still, AFAIK
but there are also similar errors in non IDE drivers, e.g. see items 1 and 3 above.

Does not work on Linux kernel 4.4-rc1.

Error message:

/home/ldvuser/ref_launch/work/current--X--kernel--X--defaultlinux-4.4-rc1.tar.xz--X--101_1a--X--cpachecker/linux-4.4-rc1.tar.xz/csd_deg_dscv/25/dscv_tempdir/rule-instrumentor/101_1a/common-model/ldv_common_model.c: In function 'ldv_blk_get_request':
/home/ldvuser/ref_launch/work/current--X--kernel--X--defaultlinux-4.4-rc1.tar.xz--X--101_1a--X--cpachecker/linux-4.4-rc1.tar.xz/csd_deg_dscv/25/dscv_tempdir/rule-instrumentor/101_1a/common-model/ldv_common_model.c:28:15: error: '__GFP_WAIT' undeclared (first use in this function)

Fixed for 4.4-rc1 according to https://bugzilla.redhat.com/show_bug.cgi?id=1285348.
Currently added in branch fix-101-4.4.

There is a bug in the current model:
struct request *ldv_blk_get_request(gfp_t mask) should return ERRPTR instead of NULL.