https://forge.ispras.ru/https://forge.ispras.ru/favicon.ico?16490126692019-03-07T12:19:30ZOpen-Source ProjectsDeductive Verification Tools for Linux Kernel - Feature #9519: Frama-C CIL is too inefficienthttps://forge.ispras.ru/issues/9519?journal_id=357112019-03-07T12:19:30ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>Blocks</strong> <i><a class="issue tracker-1 status-5 priority-4 priority-default closed parent" href="/issues/6629">Bug #6629</a>: Used CIL is outdated</i> added</li></ul> Deductive Verification Tools for Linux Kernel - Feature #9519: Frama-C CIL is too inefficienthttps://forge.ispras.ru/issues/9519?journal_id=357132019-03-07T19:39:37ZMikhail Mandrykinmandrykin@ispras.ru
<ul></ul><p>The major difference between outputs of CIL 1.5 and Frama-C is the presence of unused static functions. In Frama-C they are treated as exported roots and thus always kept. Moreover, the option to allow their removal (when not transitively referenced from other roots) is not exposed as command-line parameter and only accessible to plugins. In CIL, they can be removed by default and can be kept using option <code>--keepunused</code>. With this option CIL output becomes much closer to that of Frama-C. I added two command-line options <code>-keep/remove-unused-inline-functions</code> and <code>-keep/remove-unused-static-functions</code> to our branch of Frama-c 18.0 to be able to control the behavior. Notably, with <code>-remove-unused-static-functions</code> the output is about 8 times smaller and CPAchecker runtime is about ~30s (with ~500M of RAM)</p> Deductive Verification Tools for Linux Kernel - Feature #9519: Frama-C CIL is too inefficienthttps://forge.ispras.ru/issues/9519?journal_id=357182019-03-12T08:02:31ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>File</strong> <a href="/attachments/6310">CPAchecker files.zip</a> <a class="icon-only icon-download" title="Download" href="/attachments/download/6310/CPAchecker%20files.zip">CPAchecker files.zip</a> added</li></ul><p>Thank you, these options work perfectly! You can close the given issue since I can't do that.</p>
What's interesting is that my CPAchecker (trunk:27946) consumed ~55 seconds of CPU time and ~1 GB of RAM even when I specified two options (I attached the new verification task). How did you obtain less values? My suggestions:
<ul>
<li>You used another version or/and configuration for CPAchecker.</li>
<li>You used other options for Frama-C, e.g. invoke a slicer.</li>
<li>You incorrectly measured consumed computational resources.</li>
</ul> Deductive Verification Tools for Linux Kernel - Feature #9519: Frama-C CIL is too inefficienthttps://forge.ispras.ru/issues/9519?journal_id=357192019-03-12T12:42:28ZMikhail Mandrykinmandrykin@ispras.ru
<ul><li><strong>File</strong> <a href="/attachments/6311">cil.i</a> <a class="icon-only icon-download" title="Download" href="/attachments/download/6311/cil.i">cil.i</a> added</li><li><strong>File</strong> <a href="/attachments/6312">cil.i</a> <a class="icon-only icon-download" title="Download" href="/attachments/download/6312/cil.i">cil.i</a> added</li></ul><p>Indeed, I used a modified version of CPAchecker based on rather old trunk:25704 and measured resources with /bin/time (not with BenchExec). With slicer on my configuration Frama-C takes 7seconds and ~300M RAM and CPAchecker takes 18s and ~300M RAM. I attached the output file after slicing. Also on the latest attached file on my configuration CPAchecker takes ~80s and ~800M RAM and it seems the unused static inline functions are not removed from it. I also attached the output file I get with the new options</p> Deductive Verification Tools for Linux Kernel - Feature #9519: Frama-C CIL is too inefficienthttps://forge.ispras.ru/issues/9519?journal_id=357202019-03-12T12:43:31ZMikhail Mandrykinmandrykin@ispras.ru
<ul><li><strong>Status</strong> changed from <i>New</i> to <i>Resolved</i></li></ul> Deductive Verification Tools for Linux Kernel - Feature #9519: Frama-C CIL is too inefficienthttps://forge.ispras.ru/issues/9519?journal_id=357312019-03-13T05:04:19ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>File</strong> <a href="/attachments/6313">CPAchecker files.zip</a> <a class="icon-only icon-download" title="Download" href="/attachments/download/6313/CPAchecker%20files.zip">CPAchecker files.zip</a> added</li></ul><p>Sorry, yesterday I attached incorrect file that does correspond to the previous one (with the same file the same CPAchecker could not consume too different computational resources of course). Here is the valid one.</p> Deductive Verification Tools for Linux Kernel - Feature #9519: Frama-C CIL is too inefficienthttps://forge.ispras.ru/issues/9519?journal_id=357732019-03-14T06:15:41ZEvgeny Novikovnovikov@ispras.ru
<ul></ul>I found a strange case when Frama-C CIL outputs such source code that is still much more complex for CPAchecker as it was with old CIL (CPAchecker needs more than 2x CPU time and . Please, investigate attached files. CIL commands were:
<ul>
<li>Old CIL (output file was fixed a bit as usual):<br /><pre>
cilly.asm.exe "--printCilAsIs" "--domakeCFG" "--decil" "--noInsertImplicitCasts" "--useLogicalOperators" "--ignore-merge-conflicts" "--no-convert-direct-calls" "--no-convert-field-offsets" "--no-split-structs" "--rmUnusedInlines" "--out" "cil.i" ".tmp_safe.abs-paths.trimmed.i" "irq.bk.abs-paths.trimmed.i" "atomic.abs-paths.trimmed.i" "dd.abs-paths.trimmed.i" "spi.abs-paths.trimmed.i" "err.abs-paths.trimmed.i" "panic.abs-paths.trimmed.i" "common.abs-paths.trimmed.i" "slab.abs-paths.trimmed.i" "memory.abs-paths.trimmed.i" "gcc.abs-paths.trimmed.i" "nondet.abs-paths.trimmed.i" "reference memory.abs-paths.trimmed.i" "environment_model.abs-paths.trimmed.i" "bug kind funcs.trimmed.i"
</pre></li>
<li>Frama-C CIL:<br /><pre>
toplevel.opt "-no-autoload-plugins" "-no-findlib" "-c11" "-kernel-warn-key" "CERT:MSC:38=active" "-keep-logical-operators" "-remove-unused-inline-functions" "-remove-unused-static-functions" "-print" "-print-lines" "-no-print-annot" "-ocode" "cil.i" ".tmp_safe.abs-paths.trimmed.i" "irq.bk.abs-paths.trimmed.i" "atomic.abs-paths.trimmed.i" "dd.abs-paths.trimmed.i" "spi.abs-paths.trimmed.i" "err.abs-paths.trimmed.i" "panic.abs-paths.trimmed.i" "common.abs-paths.trimmed.i" "slab.abs-paths.trimmed.i" "memory.abs-paths.trimmed.i" "gcc.abs-paths.trimmed.i" "nondet.abs-paths.trimmed.i" "reference memory.abs-paths.trimmed.i" "environment_model.abs-paths.trimmed.i" "bug kind funcs.trimmed.i"
</pre><br />Perhaps there is some bug in CPAchecker. Now I use the latest version from trunk.</li>
</ul> Deductive Verification Tools for Linux Kernel - Feature #9519: Frama-C CIL is too inefficienthttps://forge.ispras.ru/issues/9519?journal_id=357742019-03-14T06:16:28ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>File</strong> <a href="/attachments/6315">old CIL input.tar.gz</a> <a class="icon-only icon-download" title="Download" href="/attachments/download/6315/old%20CIL%20input.tar.gz">old CIL input.tar.gz</a> added</li><li><strong>File</strong> <a href="/attachments/6316">new CIL input.tar.gz</a> <a class="icon-only icon-download" title="Download" href="/attachments/download/6316/new%20CIL%20input.tar.gz">new CIL input.tar.gz</a> added</li><li><strong>File</strong> <a href="/attachments/6317">CPAchecker files - old CIL (safe).zip</a> <a class="icon-only icon-download" title="Download" href="/attachments/download/6317/CPAchecker%20files%20-%20old%20CIL%20(safe).zip">CPAchecker files - old CIL (safe).zip</a> added</li><li><strong>File</strong> <a href="/attachments/6318">CPAchecker files - new CIL (timeout).zip</a> <a class="icon-only icon-download" title="Download" href="/attachments/download/6318/CPAchecker%20files%20-%20new%20CIL%20(timeout).zip">CPAchecker files - new CIL (timeout).zip</a> added</li></ul><p>I forgot to attach files.</p> Deductive Verification Tools for Linux Kernel - Feature #9519: Frama-C CIL is too inefficienthttps://forge.ispras.ru/issues/9519?journal_id=358182019-03-17T08:33:34ZEvgeny Novikovnovikov@ispras.ru
<ul></ul><p>Recent improvements did not help much for the last example. Frama-C (CIL) still produces more complex code sometimes. It is not trivial to understand, what causes this, but it would be great.</p> Deductive Verification Tools for Linux Kernel - Feature #9519: Frama-C CIL is too inefficienthttps://forge.ispras.ru/issues/9519?journal_id=358662019-03-25T11:56:46ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>Related to</strong> <i><a class="issue tracker-4 status-1 priority-4 priority-default" href="/issues/9563">Feature #9563</a>: Investigate less efficient code generation</i> added</li></ul> Deductive Verification Tools for Linux Kernel - Feature #9519: Frama-C CIL is too inefficienthttps://forge.ispras.ru/issues/9519?journal_id=358682019-03-25T11:57:46ZEvgeny Novikovnovikov@ispras.ru
<ul><li><strong>Status</strong> changed from <i>Resolved</i> to <i>Closed</i></li></ul><p>Mikhail made a great optimization already. The remaining ones should be investigated separately, e.g. <a class="issue tracker-4 status-1 priority-4 priority-default" title="Feature: Investigate less efficient code generation (New)" href="https://forge.ispras.ru/issues/9563">#9563</a>.</p>