Project

General

Profile

Feature #9519

Frama-C CIL is too inefficient

Added by Evgeny Novikov 6 months ago. Updated 5 months ago.

Status:
Closed
Priority:
Urgent
Start date:
03/07/2019
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

First experiments with Frama-C CIL clearly showed that it is not so efficient as former CIL (1.5.1 with LDV patches).

I launched CIL 1.5.1 with the following command-line options (input and output files are in attached old.tar.gz):

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_i7300_idle.abs-paths.trimmed.i" "atomic.abs-paths.trimmed.i" "io.bk.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" 

After that we have to fix the CIL output a bit. There is file cil.fixed.i in the archive. That file was provided to CPAchecker as input (see CPAchecker files - old CIL.zip).

Old CIL takes about 2 seconds of CPU time and 40 MB of RAM. CPAchecker spent just ~50 seconds of CPU time and ~1 GB of RAM.

New CIL (indeed Frama-C from our branch 18.0) was launched with the following command-line options (input and output files are in attached new.tar.gz):

toplevel.opt "-no-autoload-plugins" "-no-findlib" "-c11" "-kernel-warn-key" "CERT:MSC:38=inactive" "-keep-logical-operators" "-print" "-print-lines" "-no-print-annot" "-ocode" "cil.i" ".tmp_i7300_idle.abs-paths.trimmed.i" "atomic.abs-paths.trimmed.i" "io.bk.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" 

Its output file was passed to CPAchecker as is (CPAchecker files - new CIL.zip).

New CIL (Frama-C) consumed ~7 seconds of CPU time and ~220 MB of RAM. Also it outputs a large source file that took very much time from CPAchecker, namely, ~1.5 minutes of CPU time and ~1.5 GB of RAM.

New CIL processes source code better since I did not need any patches before/after it. The only thing I had to do is getting rid of tricky inline Assembler that is not supported by CPAchecker still.

But taking into account a disaster with computational resources consumption, at the moment there are little chances to switch to the new CIL. Can you provide any ideas, how to fix the situation. We do not suffer much from more hungry CIL since it does not influence total computational resources consumption much, but its output should be improved very considerably.
Taking all this into account


Files

old.tar.gz (751 KB) old.tar.gz Evgeny Novikov, 03/07/2019 03:01 PM
new.tar.gz (1.07 MB) new.tar.gz Evgeny Novikov, 03/07/2019 03:01 PM
CPAchecker files - old CIL.zip (40.5 KB) CPAchecker files - old CIL.zip Evgeny Novikov, 03/07/2019 03:04 PM
CPAchecker files - new CIL.zip (423 KB) CPAchecker files - new CIL.zip Evgeny Novikov, 03/07/2019 03:08 PM
CPAchecker files.zip (423 KB) CPAchecker files.zip Evgeny Novikov, 03/12/2019 11:00 AM
cil.i (182 KB) cil.i With slicing (-crude_slicer -no-summaries) Mikhail Mandrykin, 03/12/2019 03:28 PM
cil.i (293 KB) cil.i No slicing, but -remove-unused-inline-functions and -remove-unused-static-functions Mikhail Mandrykin, 03/12/2019 03:39 PM
CPAchecker files.zip (42.4 KB) CPAchecker files.zip Evgeny Novikov, 03/13/2019 08:03 AM
old CIL input.tar.gz (728 KB) old CIL input.tar.gz Evgeny Novikov, 03/14/2019 09:16 AM
new CIL input.tar.gz (614 KB) new CIL input.tar.gz Evgeny Novikov, 03/14/2019 09:16 AM
CPAchecker files - old CIL (safe).zip (36 KB) CPAchecker files - old CIL (safe).zip Evgeny Novikov, 03/14/2019 09:16 AM
CPAchecker files - new CIL (timeout).zip (35.2 KB) CPAchecker files - new CIL (timeout).zip Evgeny Novikov, 03/14/2019 09:16 AM

Related issues

Related to Deductive Verification Tools for Linux Kernel - Feature #9563: Investigate less efficient code generationNew03/25/2019

Actions
Blocks Klever - Bug #6629: Used CIL is outdatedClosed03/13/2019

Actions

History

#1

Updated by Evgeny Novikov 6 months ago

  • Blocks Bug #6629: Used CIL is outdated added
#2

Updated by Mikhail Mandrykin 6 months ago

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 --keepunused. With this option CIL output becomes much closer to that of Frama-C. I added two command-line options -keep/remove-unused-inline-functions and -keep/remove-unused-static-functions to our branch of Frama-c 18.0 to be able to control the behavior. Notably, with -remove-unused-static-functions the output is about 8 times smaller and CPAchecker runtime is about ~30s (with ~500M of RAM)

#3

Updated by Evgeny Novikov 5 months ago

Thank you, these options work perfectly! You can close the given issue since I can't do that.

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:
  • You used another version or/and configuration for CPAchecker.
  • You used other options for Frama-C, e.g. invoke a slicer.
  • You incorrectly measured consumed computational resources.
#4

Updated by Mikhail Mandrykin 5 months ago

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

#5

Updated by Mikhail Mandrykin 5 months ago

  • Status changed from New to Resolved
#6

Updated by Evgeny Novikov 5 months ago

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.

#7

Updated by Evgeny Novikov 5 months ago

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:
  • Old CIL (output file was fixed a bit as usual):
    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" 
    
  • Frama-C CIL:
    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" 
    

    Perhaps there is some bug in CPAchecker. Now I use the latest version from trunk.
#9

Updated by Evgeny Novikov 5 months ago

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.

#10

Updated by Evgeny Novikov 5 months ago

  • Related to Feature #9563: Investigate less efficient code generation added
#11

Updated by Evgeny Novikov 5 months ago

  • Status changed from Resolved to Closed

Mikhail made a great optimization already. The remaining ones should be investigated separately, e.g. #9563.

Also available in: Atom PDF