Project

General

Profile

Actions

Feature #9519

closed

Frama-C CIL is too inefficient

Added by Evgeny Novikov over 5 years ago. Updated over 5 years 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 2 (1 open1 closed)

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

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

Actions
Actions

Also available in: Atom PDF