ikos static analyzer

[frederic-mahe]

IKOS (Inference Kernel for Open Static Analyzers) is a static analyzer for C/C++ based on the theory of Abstract Interpretation.

I've managed to compile and install ikos, but I've got an error message when launching the analysis of swarm's code:

Analyze swarm? [Y/n] Y
[*] Running ikos swarm.bc -o swarm.db
[*] Running ikos preprocessor
[*] Running ikos analyzer
[*] Translating LLVM bitcode to AR
ikos-analyzer: /tmp/ikos-MWk4U3/swarm.pp.bc: error: unexpected llvm::BitCastInst
ikos: error: a run-time error occurred

That error has been reported by another user and marked as a bug by ikos' developers. I'll keep that issue open for a while, until I can test a new version of ikos.

[frederic-mahe]

New attempt today (compiling with a development version of gcc by the way). It seems ikos's error has been fixed.

The error report is long, with several hundred false positives (ikos is designed for C, not C++), and some interesting findings:

db.cc: In function 'db_fprintseq(_IO_FILE*, int, int)':
db.cc:682:19: unreachable: code is dead
      long rest = len;
                  ^
db.cc: In function 'db_fprintseq(_IO_FILE*, int, int)':
db.cc:685:38: unreachable: code is dead
          fprintf(fp, "%.*s\n", (int)(MIN(rest,width)), buf+i);
                                     ^
db.cc: In function 'db_fprintseq(_IO_FILE*, int, int)':
db.cc:685:39: unreachable: code is dead
          fprintf(fp, "%.*s\n", (int)(MIN(rest,width)), buf+i);
                                      ^
db.cc: In function 'db_fprintseq(_IO_FILE*, int, int)':
db.cc:685:39: unreachable: code is dead
          fprintf(fp, "%.*s\n", (int)(MIN(rest,width)), buf+i);
                                      ^
db.cc: In function 'db_fprintseq(_IO_FILE*, int, int)':
db.cc:686:19: unreachable: code is dead
          rest -= width;
                  ^
threads.h: In function 'ThreadRunner::~ThreadRunner()':
threads.h:115:13: unreachable: code is dead
        if (pthread_join(tip->pthread, NULL))
            ^

Is that code really dead? that could be a false positive too.

[torognes]

I have looked briefly on the example above and cannot understand that that indicated code should be dead. It is the code that prints to a fasta file. The code that is supposed to be dead is the part of the code that runs when width is non-zero, i.e. when printing wrapped sequences. Maybe it always ran with width equal to zero? Maybe swarm should be compiled without optimizations (no -O3), if that has not already been done. I'll look deeper into this later.

[frederic-mahe]

Maybe swarm should be compiled without optimizations (no -O3), if that has not already been done. I'll look deeper into this later.

ikos works on the source code directly and makes its own compilation, so the level of optimization should not be relevant here. Regarding the code declared as dead, ikos can be wrong (see https://github.com/NASA-SW-VnV/ikos/issues/80), so we should probably not spend to much time on that.

Testing ikos was fun, and we should revisit it in the future, especially if C++ code support keeps improving. In the meantime, I will close that issue.