https://forge.ispras.ru/https://forge.ispras.ru/favicon.ico?16490126692012-04-05T10:01:46ZOpen-Source ProjectsLinux Kernel Safety RuleDB - Feature #2706: 101: All obtained blk requests should be put after allhttps://forge.ispras.ru/issues/2706?journal_id=89282012-04-05T10:01:46ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>Status</strong> changed from <i>Open</i> to <i>Resolved</i></li><li><strong>Published in build</strong> set to <i>935d93f</i></li></ul><p>Implemented in commit 935d93f of the master branch. The bug fixed in commit 39a1d13 of linux-stable branch is found both with BLAST and CPAchecker.</p> Linux Kernel Safety RuleDB - Feature #2706: 101: All obtained blk requests should be put after allhttps://forge.ispras.ru/issues/2706?journal_id=89292012-04-05T10:05:56ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>Status</strong> changed from <i>Resolved</i> to <i>Open</i></li></ul><p>It just finds one concrete bug, so the rule isn't fully implemented.</p> Linux Kernel Safety RuleDB - Feature #2706: 101: All obtained blk requests should be put after allhttps://forge.ispras.ru/issues/2706?journal_id=89542012-04-05T13:00:45ZEvgeny Novikovnovikov@ispras.ru
<ul></ul><p>Evgeny Novikov wrote:</p>
<blockquote>
<p>The bug fixed in commit 39a1d13 of linux-stable branch is found both with BLAST and CPAchecker.</p>
</blockquote>
<p>BTW, it requires a special hack to make CPAchecker work:<br /><pre>
// HACK for CPAchecker that allows to avoid CIL parsing errors.
around: define(test_bit(nr, addr))
{
0
}
</pre><br />because of<br /><pre>
struct net_device {
...
char name[IFNAMSIZ];
...
static inline char const *netdev_name(struct net_device const *dev)
{
...
return ( char const *) & ( * dev ) . name;
}
</pre><br />leads to such amazing code after CIL:<br /><pre>
__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);
}
}
}
</pre></p> Linux Kernel Safety RuleDB - Feature #2706: 101: All obtained blk requests should be put after allhttps://forge.ispras.ru/issues/2706?journal_id=89552012-04-05T13:01:42ZEvgeny Novikovnovikov@ispras.ru
<ul></ul><p><em>test_bit</em> workaround helps to fix similar issue as described.</p> Linux Kernel Safety RuleDB - Feature #2706: 101: All obtained blk requests should be put after allhttps://forge.ispras.ru/issues/2706?journal_id=89562012-04-05T13:07:58ZEvgeny Novikovnovikov@ispras.ru
<ul></ul><p>Produced by CIL code isn't a valid C code. So it isn't surprising that it breaks CPAchecker frontend.</p> Linux Kernel Safety RuleDB - Feature #2706: 101: All obtained blk requests should be put after allhttps://forge.ispras.ru/issues/2706?journal_id=90342012-04-11T14:21:45ZEvgeny Novikovnovikov@ispras.ru
<ul></ul><p>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.</p> Linux Kernel Safety RuleDB - Feature #2706: 101: All obtained blk requests should be put after allhttps://forge.ispras.ru/issues/2706?journal_id=92652012-04-25T06:33:14ZAlexey Khoroshilovkhoroshilov@ispras.ru
<ul><li><strong>Subject</strong> changed from <i>All obtained blk requests shold be put after all</i> to <i>101: All obtained blk requests shold be put after all</i></li></ul> Linux Kernel Safety RuleDB - Feature #2706: 101: All obtained blk requests should be put after allhttps://forge.ispras.ru/issues/2706?journal_id=96052012-05-12T13:07:22ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>Priority</strong> changed from <i>High</i> to <i>Normal</i></li></ul><p>Reduce priority until we'll decide that it's high actually.</p> Linux Kernel Safety RuleDB - Feature #2706: 101: All obtained blk requests should be put after allhttps://forge.ispras.ru/issues/2706?journal_id=118512012-07-12T14:24:09ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>Subject</strong> changed from <i>101: All obtained blk requests shold be put after all</i> to <i>101: All obtained blk requests should be put after all</i></li><li><strong>Assignee</strong> changed from <i>Evgeny Novikov</i> to <i>Marina Makienko</i></li></ul><p>Indeed this rule is rather promising: it isn't so general as malloc-free, but used in a lot of drivers. That's why it's a good task for Marina. As usual careful investigation, rule and model completion, and thorough testing are required.</p> Linux Kernel Safety RuleDB - Feature #2706: 101: All obtained blk requests should be put after allhttps://forge.ispras.ru/issues/2706?journal_id=121772012-07-23T12:25:17ZMarina Makienkomakienko@ispras.ru
<ul><li><strong>Status</strong> changed from <i>Open</i> to <i>Resolved</i></li><li><strong>% Done</strong> changed from <i>0</i> to <i>100</i></li></ul> Linux Kernel Safety RuleDB - Feature #2706: 101: All obtained blk requests should be put after allhttps://forge.ispras.ru/issues/2706?journal_id=126092012-08-10T13:25:23ZMarina Makienkomakienko@ispras.ru
<ul></ul><p>__blk_put_request() was added in this model.</p>
<p>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.</p>
<p>Also the model should check function call in operation "req->end_io = ...", where req = blk_get_request() or blk_make_request().</p> Linux Kernel Safety RuleDB - Feature #2706: 101: All obtained blk requests should be put after allhttps://forge.ispras.ru/issues/2706?journal_id=126472012-08-16T09:37:09ZMarina Makienkomakienko@ispras.ru
<ul><li><strong>Description</strong> updated (<a title="View differences" href="/journals/12647/diff?detail_id=13893">diff</a>)</li></ul> Linux Kernel Safety RuleDB - Feature #2706: 101: All obtained blk requests should be put after allhttps://forge.ispras.ru/issues/2706?journal_id=126482012-08-16T09:43:29ZMarina Makienkomakienko@ispras.ru
<ul><li><strong>Description</strong> updated (<a title="View differences" href="/journals/12648/diff?detail_id=13894">diff</a>)</li></ul> Linux Kernel Safety RuleDB - Feature #2706: 101: All obtained blk requests should be put after allhttps://forge.ispras.ru/issues/2706?journal_id=147832013-01-19T20:12:19ZAlexey Khoroshilovkhoroshilov@ispras.ru
<ul><li><strong>Status</strong> changed from <i>Resolved</i> to <i>Open</i></li></ul><p>blk_get_request() and blk_make_request() return error code in different ways.<br />blk_get_request() returns NULL, blk_make_request() returns ERR_PTR.<br />Model should support it.</p> Linux Kernel Safety RuleDB - Feature #2706: 101: All obtained blk requests should be put after allhttps://forge.ispras.ru/issues/2706?journal_id=147842013-01-19T20:14:28ZAlexey Khoroshilovkhoroshilov@ispras.ru
<ul></ul><p>Another issue:<br /><pre>
/*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;
</pre></p>
<p>Why res is not updated in this branch?</p> Linux Kernel Safety RuleDB - Feature #2706: 101: All obtained blk requests should be put after allhttps://forge.ispras.ru/issues/2706?journal_id=149492013-01-31T08:29:42ZMarina Makienkomakienko@ispras.ru
<ul></ul><p>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:<br /><pre>
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;
}
</pre></p>
<p>So, if the mask is __GFP_WAIT, function will try to get request again and again.<br />But if the mask has another value, the model checks blk_get_request() return value.</p> Linux Kernel Safety RuleDB - Feature #2706: 101: All obtained blk requests should be put after allhttps://forge.ispras.ru/issues/2706?journal_id=160972013-05-06T08:41:06ZEvgeny Novikovnovikov@ispras.ru
<ul></ul><p>Now 5 of 6 false positives are due to the model successfully obtains a request with __<em>GFP_WAIT</em> 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().</p>
Moreover the model can return a failure without obtaining a request even when functions are called with __<em>GFP_WAIT</em> since a request queue may die (as it said <a href="http://lxr.free-electrons.com/source/block/blk-core.c#L1080" class="external">here</a>). Even without verification we can <a href="http://lxr.free-electrons.com/ident?i=blk_get_request" class="external">see</a> that there is a number of bugs:
<ol>
<li><a href="http://lxr.free-electrons.com/source/drivers/block/paride/pd.c#L724" class="external">Possible NULL pointer dereference</a></li>
<li><a href="http://lxr.free-electrons.com/source/drivers/ide/ide-park.c#L34" class="external">Possible NULL pointer dereference</a></li>
<li><a href="http://lxr.free-electrons.com/source/drivers/scsi/scsi_error.c#L1637" class="external">Possible NULL pointer dereference</a></li>
<li><a href="http://lxr.free-electrons.com/source/drivers/target/target_core_pscsi.c#L1050" class="external">Excessive check of blk_get_request() return value</a></li>
<li>...</li>
</ol>
<p>Developers have ignored patches <a href="https://lkml.org/lkml/2012/8/9/631" class="external">sent</a> by Marina because of:<br /><cite>drivers/ide is obsolete and scheduled for removal</cite><br />although Sergei answered:<br /><cite>It's being maintained for bug fixes still, AFAIK</cite><br />but there are also similar errors in non IDE drivers, e.g. see items 1 and 3 above.</p> Linux Kernel Safety RuleDB - Feature #2706: 101: All obtained blk requests should be put after allhttps://forge.ispras.ru/issues/2706?journal_id=186192014-02-12T10:16:04ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>Status</strong> changed from <i>Open</i> to <i>Resolved</i></li></ul><p>All noted issues with the given specification were eventually fixed in <a class="changeset" title="Merge branch 'fix101' * fix101: Removed useless commented lines and include of verifier/rcv.h ..." href="https://forge.ispras.ru/projects/ldv-rules/repository/122/revisions/09b2874079a469b3563ee613de64c064037daacd">09b28740</a> mainly by Alexey. So, now there is just one false positive that it is related with lacks of BLAST.</p> Linux Kernel Safety RuleDB - Feature #2706: 101: All obtained blk requests should be put after allhttps://forge.ispras.ru/issues/2706?journal_id=186202014-02-12T10:16:13ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>Assignee</strong> deleted (<del><i>Marina Makienko</i></del>)</li></ul> Linux Kernel Safety RuleDB - Feature #2706: 101: All obtained blk requests should be put after allhttps://forge.ispras.ru/issues/2706?journal_id=209162014-10-20T08:53:58ZVadim Mutilinmutilin@ispras.ru
<ul><li><strong>Description</strong> updated (<a title="View differences" href="/journals/20916/diff?detail_id=23212">diff</a>)</li></ul> Linux Kernel Safety RuleDB - Feature #2706: 101: All obtained blk requests should be put after allhttps://forge.ispras.ru/issues/2706?journal_id=248382015-12-10T16:42:35ZVitaly Mordanmordan@ispras.ru
<ul></ul><p>Does not work on Linux kernel 4.4-rc1.</p>
<p>Error message:</p>
<p>/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':<br />/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)</p> Linux Kernel Safety RuleDB - Feature #2706: 101: All obtained blk requests should be put after allhttps://forge.ispras.ru/issues/2706?journal_id=248612015-12-24T09:30:56ZVitaly Mordanmordan@ispras.ru
<ul></ul><p>Fixed for 4.4-rc1 according to <a class="external" href="https://bugzilla.redhat.com/show_bug.cgi?id=1285348">https://bugzilla.redhat.com/show_bug.cgi?id=1285348</a>.<br />Currently added in branch fix-101-4.4.</p> Linux Kernel Safety RuleDB - Feature #2706: 101: All obtained blk requests should be put after allhttps://forge.ispras.ru/issues/2706?journal_id=248682015-12-26T23:50:15ZAlexey Khoroshilovkhoroshilov@ispras.ru
<ul></ul><p>There is a bug in the current model:<br />struct request *ldv_blk_get_request(gfp_t mask) should return ERRPTR instead of NULL.</p> Linux Kernel Safety RuleDB - Feature #2706: 101: All obtained blk requests should be put after allhttps://forge.ispras.ru/issues/2706?journal_id=299912017-03-16T09:51:25ZVitaly Mordanmordan@ispras.ru
<ul><li><strong>Description</strong> updated (<a title="View differences" href="/journals/29991/diff?detail_id=33941">diff</a>)</li></ul>