Feature #9519
closedFrama-C CIL is too inefficient
0%
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
Updated by Evgeny Novikov about 5 years ago
- Blocks Bug #6629: Used CIL is outdated added
Updated by Mikhail Mandrykin about 5 years 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)
Updated by Evgeny Novikov about 5 years ago
- File CPAchecker files.zip CPAchecker files.zip added
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.
Updated by Mikhail Mandrykin about 5 years 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
Updated by Mikhail Mandrykin about 5 years ago
- Status changed from New to Resolved
Updated by Evgeny Novikov about 5 years ago
- File CPAchecker files.zip CPAchecker files.zip added
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.
Updated by Evgeny Novikov about 5 years ago
- 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.
Updated by Evgeny Novikov about 5 years ago
- File old CIL input.tar.gz old CIL input.tar.gz added
- File new CIL input.tar.gz new CIL input.tar.gz added
- File CPAchecker files - old CIL (safe).zip CPAchecker files - old CIL (safe).zip added
- File CPAchecker files - new CIL (timeout).zip CPAchecker files - new CIL (timeout).zip added
I forgot to attach files.
Updated by Evgeny Novikov about 5 years 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.
Updated by Evgeny Novikov about 5 years ago
- Related to Feature #9563: Investigate less efficient code generation added
Updated by Evgeny Novikov about 5 years ago
- Status changed from Resolved to Closed
Mikhail made a great optimization already. The remaining ones should be investigated separately, e.g. #9563.