Open-Source Projects: Issueshttps://forge.ispras.ru/https://forge.ispras.ru/favicon.ico?16490126692017-01-25T16:22:02ZOpen-Source Projects
Redmine Klever - Feature #7912 (Closed): Use "Python 3" in PyCharm settings instead of "Python 3.4" for p...https://forge.ispras.ru/issues/79122017-01-25T16:22:02ZVladimir Gratinskiygratinskiy@ispras.ru
<p>Some users may use Ubuntu 16.04 with default Python 3.5 there. It is not very handy to deal with a lot of changed PyCharm files in repository every time.</p> Linux Driver Verification - Feature #6040 (Closed): Building ARM-aspectatorhttps://forge.ispras.ru/issues/60402015-06-05T16:31:51ZVladimir Gratinskiygratinskiy@ispras.ru
<p>This instruction is for installing cross-compiling tools for using LDV for verification of ARM drivers. It was tested for Ubuntu 12.04 with the latest versions of binutils, gawk and glibc at 8 May 2013. But anyway it doesn't garantee 100% successfull installation on Ubuntu 12.04 and 100% unsuccessfull installation on other systems. You can try newer versions of binutils, gawk and glibc if you want. You should know that building 'cif' is not so fast as you might expect.</p>
<p>If you are still here, let's start. Let assume that {MY_WORKING_DIR} is your working directory (full path).</p>
<pre>
$ export MY_DIR={MY_WORKING_DIR}
$ sudo apt-get install texinfo
</pre>
<p>download binutils-2.23.tar.gz (<a class="external" href="http://ftp.gnu.org/gnu/binutils/">http://ftp.gnu.org/gnu/binutils/</a>)<br />extract it to {MY_WORKING_DIR}/binutils-2.23/</p>
<pre>
$ export PREFIX=$MY_DIR/cross TARGET=arm-unknown-linux-gnueabi
$ mkdir build-binutils && cd build-binutils
$ ../binutils-2.23/configure --target=$TARGET --prefix=$PREFIX --disable-nls
$ make all
$ make install
$ cd .. && export PATH=$PATH:$PREFIX/bin
$ git clone git://forge.ispras.ru/cif.git --recursive
$ git checkout 7d912b08e173310c59
$ git submodule update --recursive
$ cd cif
$ cp Makefile1_cross Makefile
</pre>
<p>Next command will finish with error</p>
<pre>
$ prefix=$MY_DIR/cross/ make install
</pre>
<pre>
$ cd aspectator-build
$ make all-gcc
</pre>
<p>Next two commands will finish with error</p>
<pre>
$ make install all-gcc
$ make -k all-target-libgcc
</pre>
<pre>
$ make -i install-target-libgcc
$ make install-gcc
</pre>
<p>If next command will finish with <strong>as: unrecognized option '-meabi=5'</strong> then everything is going fine. Otherwise this instruction can't help you.</p>
<pre>
$ ../aspectator-bin/bin/arm-unknown-linux-gnueabi-gcc -xc /dev/null
</pre>
<pre>
$ cp -r ../aspectator-bin/* ../../cross/
$ cd ../../
</pre>
<p>Download gawk-4.0.2.tar.xz (<a class="external" href="http://mirrors.ustc.edu.cn/gnu/gawk/">http://mirrors.ustc.edu.cn/gnu/gawk/</a>) and extract it to {MY_WORKING_DIR}/gawk-4.0.2</p>
<pre>
$ cd gawk-4.0.2
$ ./configure --target=$TARGET --prefix=$PREFIX
$ make all
$ make install
$ cd ..
$ git clone git://git.kernel.org/pub/scm/linux/kernel/git/stable/linux-stable.git
$ cd linux-stable
$ git checkout v3.7.3
$ make ARCH=arm headers_check
$ make ARCH=arm INSTALL_HDR_PATH=$MY_DIR/cross/arm-unknown-linux-gnueabi/ headers_install
$ cd ..
</pre>
<p>Download glibc-2.17.tar.bz2 (<a class="external" href="http://mirrors.ustc.edu.cn/gnu/libc/">http://mirrors.ustc.edu.cn/gnu/libc/</a>) and extract it to {MY_WORKING_DIR}/glibc-2.17</p>
<pre>
$ mkdir build-glibc && cd build-glibc
$ ../glibc-2.17/configure --with-binutils=$MY_DIR/cross/arm-unknown-linux-gnueabi/bin --prefix=$PREFIX --disable-nls libc_cv_forced_unwind=yes libc_cv_ctors_header=yes libc_cv_c_cleanup=yes --without-fp --host=$TARGET --with-headers=$MY_DIR/cross/arm-unknown-linux-gnueabi/include
$ make
$ make install
$ cd ../cif
$ cp Makefile2_cross Makefile
$ make clean
$ prefix=$PREFIX make install
$ cd ..
$ rm -rf $PREFIX/bin/aspectator
$ ln -s $PREFIX/bin/aspectator-bin/bin/arm-unknown-linux-gnueabi-gcc $PREFIX/bin/aspectator
</pre>
<p>Now you can run LDV with next options:</p>
<pre>
PATH=$PATH:{MY_WORKING_DIR}/cross/bin LDV_ASPECTATOR={MY_WORKING_DIR}/cross/bin/aspectator CONFIG_OPT=allmodconfig,arm,arm-unknown-linux-gnueabi-
</pre> Linux Kernel Safety RuleDB - Feature #4536 (Rejected): Commit testerhttps://forge.ispras.ru/issues/45362013-10-09T13:05:22ZVladimir Gratinskiygratinskiy@ispras.ru
<p>Commit tester allows you to check commits in linux repository with known bugs. You need only to create configuration file with tasks for ldv and information about kernels. Each task have module name, rule model name, commit, entry point, ideal verdict, your comment and other data for ldv system. Ldv system check every selected module and after it Commit Tester generate html report with table where you can find results of module verifying and summary information. For more info run (you need to have 'bin' of ldv install directory in your PATH):</p>
<p><em>commit-test.pl --help</em></p>
<p>To install it run:</p>
<p><em>prefix=<LDV_INSTALL_DIR> make install-testing</em></p>
<p>where <LDV_INSTALL_DIR> is directory with installed ldv tools.</p> Linux Kernel Safety RuleDB - Feature #3866 (New): 149: double use of init_completion()https://forge.ispras.ru/issues/38662013-01-18T14:44:30ZVladimir Gratinskiygratinskiy@ispras.ru
<p>Repeating use of init_completion() would be able to create possible race condition.<br />To avoid it we can reinit completion using INIT_COMPLETION(). Commit 41682e03d4f on torvalds fix this problem.<br /><pre>
http://git.kernel.org/?p=linux/kernel/git/torvalds/linux.git;a=commitdiff;h=41682e03d4f
</pre><br />In some cases (for example, if the critical section is used) double use of init_complition() don't lead to error.</p> Linux Kernel Safety RuleDB - Feature #3865 (Open): 148: completion must be initialized before eve...https://forge.ispras.ru/issues/38652013-01-18T14:29:45ZVladimir Gratinskiygratinskiy@ispras.ru
<p>Before each use of completion the corresponding initialization has to be carried out.<br /><em>Either static:</em><br /> <code>DECLARE_COMPLETION()</code><br /><em>or dynamic:</em><br /> <code>init_completion()</code></p> Linux Kernel Safety RuleDB - Feature #3608 (Open): 145: Usage of clock functionshttps://forge.ispras.ru/issues/36082012-10-23T09:58:01ZVladimir Gratinskiygratinskiy@ispras.ru
<p>It is necessary to use functions from clk.h correctly. This rule checks usage of functions clk_get, clk_prepare, clk_enable, clk_disable, clk_unprepare, clk_put.</p>
<pre><code>- functions must be in the correct order<br />- function clk_put mustn't get null pointer</code></pre> Linux Kernel Safety RuleDB - Feature #3399 (Open): 143: Usage of semaphoreshttps://forge.ispras.ru/issues/33992012-09-04T13:09:35ZVladimir Gratinskiygratinskiy@ispras.ru
<p>It is necessary to use semaphore correctly. This rule checks usage of the functions: up_read, down_read, up_write, down_write, down_read_trylock, down_write_trylock, downgrade_write, down_read_nested, down_write_nested.</p>
<ul>
<li> - multiple write locks are not permitted<br /> - multiple write unlocks are not permitted</li>
<li> - read lock is not permitted after write lock</li>
<li> - write lock is not permitted after read lock</li>
<li> - read and write locks must be free at the end</li>
</ul>
<p>Commit 82163edcdf on torvalds fix the last one.</p>
<p><strong>Links</strong><br />Sample bugfixes <a href="https://git.kernel.org/cgit/linux/kernel/git/stable/linux-stable.git/commit/?id=506218e" class="external">506218e</a>, <a href="https://git.kernel.org/cgit/linux/kernel/git/stable/linux-stable.git/commit/?id=de79143" class="external">de79143</a></p> Linux Driver Verification - Bug #3349 (Open): There is no initialization of ldv_mutex_TEMPLATE https://forge.ispras.ru/issues/33492012-08-20T13:10:16ZVladimir Gratinskiygratinskiy@ispras.ru
<p>In some drivers (for example drivers/infiniband/core/ib_core.ko) of linux 3.5 I've found this bug in rerouter. I wrote test drivers, and tried to make similar situation, but the bug's result wasn't repeated.</p>
<p>{<br /> ldv_mutex_TEMPLATE = 1;<br /> return ;<br />}<br />entry_point
{<br /> LDV_IN_INTERRUPT = 1;<br /> ldv_initialize_FOREACH()
{<br /> return ;<br /> }<br />...<br />}</p> Linux Driver Verification - Bug #3344 (Open): Apostrophe in commentshttps://forge.ispras.ru/issues/33442012-08-15T09:32:34ZVladimir Gratinskiygratinskiy@ispras.ru
<p>If I use apostrophe the text after it isn't showed.<br />Example:</p>
<blockquote>
<p>/* LDV_COMMENT_RETURN Return function's argument */</p>
</blockquote>
<p>In visualisation this comment shows:</p>
<blockquote>
<p>... Return function</p>
</blockquote> Linux Kernel Safety RuleDB - Feature #3340 (Open): 142: Usage of mod_timer()https://forge.ispras.ru/issues/33402012-08-14T09:23:13ZVladimir Gratinskiygratinskiy@ispras.ru
<p>It's necessary to use absolute time instead of relative for mode_timer().<br />The old implementation used a relative timeout thus the hardware watchdog was never triggered.<br />Commit f9e4715 show how to use it:</p>
<blockquote>
<p>-#define next_ping_period(cks) msecs_to_jiffies(cks - 4)<br />+#define next_ping_period(cks) (jiffies + msecs_to_jiffies(cks - 4))</p>
</blockquote> C Instrumentation Framework - Bug #3323 (Closed): Internal compiler error in Aspectatorhttps://forge.ispras.ru/issues/33232012-08-03T08:08:38ZVladimir Gratinskiygratinskiy@ispras.ru
<p>I tried to run my rule model (119_1a), and on drivers media/video/saa7134/saa7134-alsa.ko media/video/saa7134/saa7134-dvb.ko aspectator failed on the 3d stage:</p>
<blockquote>
<p>compiler-core: internal compiler error: Killed (program cc1)</p>
</blockquote>
<p>From log on the other computer:</p>
<blockquote>
<p>drivers/media///dvb/bt8xx/dvb-bt8xx.c:975:1: internal compiler error: Segmentation fault<br />Please submit a full bug report,<br />with preprocessed source if appropriate.<br />See <<a class="external" href="http://bugzilla.redhat.com/bugzilla">http://bugzilla.redhat.com/bugzilla</a>> for instructions.<br />The bug is not reproducible, so it is likely a hardware or OS problem.<br />make[ 4]: <b>* [drivers/media///dvb/bt8xx/dvb-bt8xx.o] Error 1<br />make[ 3]: <strong></b> [drivers/media///dvb/bt8xx] Error 2<br />make[ 2]: <b></strong> [drivers/media///dvb] Error 2<br />make[ 1]: *</b> [_module_drivers/media//] Error 2<br />Compile error.</p>
</blockquote>
<p>In the attached file there is a very big log :)</p> Linux Kernel Safety RuleDB - Feature #3317 (Resolved): 010: Usage of a GFP_ATOMIC flag in functio...https://forge.ispras.ru/issues/33172012-08-01T15:08:40ZVladimir Gratinskiygratinskiy@ispras.ru
<p>When calling memory allocation function from the context of interrupt it's required to ensure a non-preemptible execution of the function; but in the case of GFP_KERNEL flag, function execution can be preempted, because a greater number of operations to find and allocate memory blocks is executed.</p>
<p>Verification: If some function is positioned as one that "is executed in a context of interrupt" then it's required to ensure checking for a necessary usage of the GFP_ATOMIC flag in the memory allocation functions for kernel modules.</p>
<p>Example:<br />void* ptr = kmalloc(size, GFP_ATOMIC);</p> Linux Driver Verification - Bug #3205 (New): Driver that cannot be built is "verified" by ldv-toolshttps://forge.ispras.ru/issues/32052012-07-13T11:56:10ZVladimir Gratinskiygratinskiy@ispras.ru
<p>Driver archive in attachment. Log is so:<br /><pre>
ldv-core: NORMAL: Calling drv-env-gen...
ldv-core: WARNING: BCE failed, see '/home/vladimir/Documents/work/hello/test/work/current--X--hello.tar.bz2--X--defaultlinux-2.6.34--X--39_1/linux-2.6.34/ldv_tempdir/bce_err.log'.
ldv-core: NORMAL: Calling Domain Speicific C-Verifier
dscv: NORMAL: Nothing will be run (no mains!). Printing final report...
</pre></p>