Crash on example program loop.c

[yiyuaner]

After building ikos, I run it on the given example program loop.c: ikos loop.c

#include <stdio.h>
int a[10];

int main(int argc, char *argv[]) {
  size_t i = 0;
  for (;i < 10; i++) {
    a[i] = i;
  }
  a[i] = i;
  printf("%i", a[i]);
}

The program crashed and I got the following stack trace:

[*] Compiling loop.c
[*] Running ikos preprocessor
[*] Running ikos analyzer
[!] ikos was compiled in debug mode, the analysis might be slow
[*] Translating LLVM bitcode to AR
ikos-analyzer: /home/guoyiyuan/AbsInt/llvm4.1/llvm-4.0.1.src/include/llvm/Support/Casting.h:236: typename llvm::cast_retty<X, Y*>::ret_type llvm::cast(Y*) [with X = llvm::PossiblyExactOperator; Y = const llvm::Instruction; typename llvm::cast_retty<X, Y*>::ret_type = const llvm::PossiblyExactOperator*]: Assertion `isa<X>(Val) && "cast<Ty>() argument of incompatible type!"' failed.
#0 0x000000000135c4b0 llvm::sys::PrintStackTrace(llvm::raw_ostream&) /home/guoyiyuan/AbsInt/llvm4.1/llvm-4.0.1.src/lib/Support/Unix/Signals.inc:402:0
#1 0x000000000135c86e PrintStackTraceSignalHandler(void*) /home/guoyiyuan/AbsInt/llvm4.1/llvm-4.0.1.src/lib/Support/Unix/Signals.inc:466:0
#2 0x000000000135aa8e llvm::sys::RunSignalHandlers() /home/guoyiyuan/AbsInt/llvm4.1/llvm-4.0.1.src/lib/Support/Signals.cpp:44:0
#3 0x000000000135be1f SignalHandler(int) /home/guoyiyuan/AbsInt/llvm4.1/llvm-4.0.1.src/lib/Support/Unix/Signals.inc:256:0
#4 0x00007f3b6129a6d0 __restore_rt (/usr/lib64/libpthread.so.0+0xf6d0)
#5 0x00007f3b604bf277 __GI_raise /usr/src/debug/glibc-2.17-c758a686/signal/../nptl/sysdeps/unix/sysv/linux/raise.c:56:0
#6 0x00007f3b604c0968 __GI_abort /usr/src/debug/glibc-2.17-c758a686/stdlib/abort.c:92:0
#7 0x00007f3b604b8096 __assert_fail_base /usr/src/debug/glibc-2.17-c758a686/assert/assert.c:92:0
#8 0x00007f3b604b8142 (/usr/lib64/libc.so.6+0x2f142)
#9 0x00000000011d5383 llvm::cast_retty<llvm::PossiblyExactOperator, llvm::Instruction const*>::ret_type llvm::cast<llvm::PossiblyExactOperator, llvm::Instruction const>(llvm::Instruction const*) /home/guoyiyuan/AbsInt/llvm4.1/llvm-4.0.1.src/include/llvm/Support/Casting.h:236:0
#10 0x00000000011d25b8 llvm::Instruction::isExact() const /home/guoyiyuan/AbsInt/llvm4.1/llvm-4.0.1.src/lib/IR/Instruction.cpp:126:0
#11 0x0000000000d813c4 ikos::frontend::import::FunctionImporter::translate_binary_operator(ikos::frontend::import::BasicBlockTranslation*, llvm::BinaryOperator*) /home/guoyiyuan/AbsInt/ikos/frontend/llvm/src/import/function.cpp:1120:0
#12 0x0000000000d7e98c ikos::frontend::import::FunctionImporter::translate_instruction(ikos::frontend::import::BasicBlockTranslation*, llvm::Instruction*) /home/guoyiyuan/AbsInt/ikos/frontend/llvm/src/import/function.cpp:375:0
#13 0x0000000000d7e116 ikos::frontend::import::FunctionImporter::translate_basic_block(llvm::BasicBlock*) /home/guoyiyuan/AbsInt/ikos/frontend/llvm/src/import/function.cpp:222:0
#14 0x0000000000d7de27 ikos::frontend::import::FunctionImporter::translate_basic_blocks() /home/guoyiyuan/AbsInt/ikos/frontend/llvm/src/import/function.cpp:192:0
#15 0x0000000000d7dd08 ikos::frontend::import::FunctionImporter::translate_control_flow_graph() /home/guoyiyuan/AbsInt/ikos/frontend/llvm/src/import/function.cpp:166:0
#16 0x0000000000d7d2f6 ikos::frontend::import::FunctionImporter::translate_body() /home/guoyiyuan/AbsInt/ikos/frontend/llvm/src/import/function.cpp:78:0
#17 0x0000000000d6fa67 ikos::frontend::import::BundleImporter::translate_function_body(llvm::Function*) /home/guoyiyuan/AbsInt/ikos/frontend/llvm/src/import/bundle.cpp:353:0
#18 0x0000000000d50350 ikos::frontend::import::Importer::import(llvm::Module&, ikos::ar::Flags<ikos::frontend::import::Importer::ImportOption>) /home/guoyiyuan/AbsInt/ikos/frontend/llvm/src/import/importer.cpp:125:0
#19 0x0000000000a4f279 main /home/guoyiyuan/AbsInt/ikos/analyzer/src/ikos_analyzer.cpp:761:0
#20 0x00007f3b604ab445 __libc_start_main /usr/src/debug/glibc-2.17-c758a686/csu/../csu/libc-start.c:308:0
#21 0x0000000000a4e0c5 _start (/home/guoyiyuan/AbsInt/ikos_install/bin/ikos-analyzer+0xa4e0c5)
Stack dump:
0.  Program arguments: /home/guoyiyuan/AbsInt/ikos_install/bin/ikos-analyzer -a=sound,shc,nullity,pcmp,dfa,dca,fca,prover,dbz,boa,sio -d=interval -entry-points=main -globals-init=skip-big-arrays -prec=mem -proc=inter -display-checks=no -display-inv=no -color=auto -log=info /tmp/ikos-Em5Qeh/loop.pp.bc -o output.db 
ikos: error: exited with signal 6

Also make check fails too:

The following tests FAILED:
     36 - analysis-buffer-overflow (Failed)
     37 - analysis-division-by-zero (Failed)
     38 - analysis-memory (Failed)
     40 - analysis-assert-prover (Failed)
     41 - analysis-uninitialized-variable (Failed)
     42 - analysis-unaligned-pointer (Failed)
     43 - analysis-signed-int-overflow (Failed)
     44 - analysis-unsigned-int-overflow (Failed)
     45 - analysis-shift-count (Failed)
     46 - analysis-pointer-overflow (Failed)
     47 - analysis-pointer-compare (Failed)
Errors while running CTest

I'm using llvm 4.0.1. llvm 4.0.1 is built using cmake:

cmake3 -G "Unix Makefiles" -DLLVM_ENABLE_RTTI=on -DCMAKE_INSTALL_PREFIX=/path/AbsInt/llvm4.1/install ../llvm-4.0.1.src/

And ikos is built by:

cmake3 ../ikos/ -DCMAKE_INSTALL_PREFIX=../ikos_install -DCMAKE_BUILD_TYPE=Debug -DLLVM_CONFIG_EXECUTABLE=/path/AbsInt/llvm4.1/install/bin/llvm-config

Hope for your help, thanks!

[ghost]

Hi,

The issue seems to come from your LLVM. What is your OS ?

[yiyuaner]

Hi,

The issue seems to come from your LLVM. What is your OS ?

I'm using centos 7:

LSB Version:    :core-4.1-amd64:core-4.1-noarch:cxx-4.1-amd64:cxx-4.1-noarch:desktop-4.1-amd64:desktop-4.1-noarch:languages-4.1-amd64:languages-4.1-noarch:printing-4.1-amd64:printing-4.1-noarch
Distributor ID: CentOS
Description:    CentOS Linux release 7.5.1804 (Core) 
Release:    7.5.1804
Codename:   Core

[yiyuaner]

@zadlg I install boost library from source (Because boost from my system is too old) and I set env variable BOOST_ROOT to installation directory of boost before running cmake for ikos. Not sure if this is relevant.

[arthaud]

Hello @yiyuaner,

I have never seen this error before, but I think it might come from LLVM, as @zadlg mentioned.

ikos needs runtime type information (RTTI) and exception handling (EH), so you should consider compiling LLVM with -DLLVM_ENABLE_RTTI=ON -DLLVM_ENABLE_EH=ON

By the way, we have installation instruction for CentOS 7.5, see doc/INSTALL_CENTOS_7.5.md It uses the bootstrap script to compile all the dependencies (boost, llvm, etc..) automatically with the right set of flags. You can consider trying this too.

[yiyuaner]

Hello @yiyuaner,

I have never seen this error before, but I think it might come from LLVM, as @zadlg mentioned.

ikos needs runtime type information (RTTI) and exception handling (EH), so you should consider compiling LLVM with -DLLVM_ENABLE_RTTI=ON -DLLVM_ENABLE_EH=ON

By the way, we have installation instruction for CentOS 7.5, see doc/INSTALL_CENTOS_7.5.md It uses the bootstrap script to compile all the dependencies (boost, llvm, etc..) automatically with the right set of flags. You can consider trying this too.

Ok, I can install successfully now. Thanks.