nasa-sw-vnv / ikos Goto Github PK

Static analyzer for C/C++ based on the theory of Abstract Interpretation.

License: Other

CMake 2.07% CSS 0.08% C++ 72.20% Shell 1.55% C 1.88% TeX 1.14% Python 4.51% JavaScript 0.20% HTML 0.09% LLVM 16.09% Dockerfile 0.19%

static-analysis software-verification abstract-interpretation program-analysis

ikos's People

Contributors

Stargazers

Watchers

Forkers

aogrcs tiandiyixian elcraked rep6 gavinnishizawa joegana grip3 yiyuaner djuanbei atnnn aladw dancal heruix skg7on mmyjona longjohncoder fjsnogueira fcccode moneytech devhttps cristian357r4 4144 prog012 shaunstanislauslau daydayup40 slowmistio ezhangle rnestler gavz xiaahui nimdakey sececter lqingyu abioy hxl1990 sasqwatch vaioco pharshid codyps explife0011 olivierh59500 codezor satyendrabanjare uuhan qing666888 fuath xxm3 zhuhuibeishadiao fengjixuchui venkyjntu-git ubuntu-repo nag1bat0r zoq ryderblue vkandola alxarc agileehsan mr-sour plkms loongwalker ck624 m-meidani blockspacer yijiangtian anmavrid avleze hbourbouh cyberican transmitterdan iamwonseok jacobusthesecond 5l1v3r1 caballa allegro62 john-tornblom ezaffanella weitaomiao kmc-kk zzmjohn mfuchs1984 antonpaule alecpedigree4 amamory-verification c0de3 can-yildirim posticarus dmott-eyelock tareq97-zz secbugs cmboling nuclearsandwich richardlford guillaume66 kerwinzxc danieljpietz keremc jiankangren clayne aphelion-aerospace space-ros

ikos's Issues

ikos-analyzer stuck and/or running out of memory

When analyzing the suricata code base (~300k lines of C), the ikos-analyzer uses excessive memory and appears to get stuck in some kind of loop.

Analyze src/suricata? [Y/n]
[*] Running ikos src/suricata.bc -o src/suricata.db
[*] Running ikos preprocessor
[*] Running ikos analyzer
[*] Translating LLVM bitcode to AR
[*] Running liveness analysis
[*] Running fixpoint profile analysis
[*] Running interprocedural value analysis
[*] Analyzing entry point: main

I killed it at 30G of memory use to avoid the OOM killer kicking in and disrupting other processes on this box.

The way I set up this test:

docker run -it ubuntu:18.10 /bin/bash
apt update && apt upgrade -y && apt -y install clang-7 libpcre3 libpcre3-dbg libpcre3-dev build-essential autoconf automake libtool libpcap-dev libnet1-dev libyaml-0-2 libyaml-dev pkg-config zlib1g zlib1g-dev libcap-ng-dev libcap-ng0 make libmagic-dev libjansson-dev libboost-dev libboost-atomic1.67-dev libboost-date-time1.67-dev libboost-iostreams1.67-dev libboost-graph1.67-dev libboost-filesystem1.67-dev libboost-numpy1.67-dev libboost-python1.67-dev libboost-random1.67-dev libboost-thread1.67-dev libboost1.67-tools-dev libboost-test1.67-dev build-essential git cmake libgmp-dev libsqlite3-dev libapron-dev

git clone https://github.com/NASA-SW-VnV/ikos
cd ikos/
mkdir build
cd build/
cmake -DLLVM_CONFIG_EXECUTABLE=/usr/bin/llvm-config-7 ../
make
make install
export PATH=/ikos/install/bin/:$PATH
cd /
git clone https://github.com/OISF/suricata
cd suricata/
git clone https://github.com/OISF/libhtp
bash autogen.sh 
ikos-scan ./configure --disable-shared --disable-gccmarch-native
ikos-scan make

When running ikos with verbose output, I noticed that some functions were analyzed a lot of times. I'm not sure if that is normal.

# ikos -v src/suricata.bc &> debug.log
... killed when process uses 10G of mem ...
# cat debug.log | sort | uniq -c | sort -nr |head -n25
  11929 [.] Analyzing function: SCMapEnumValueToName
  11928 [.] Analyzing function: SCLocalTime
   5868 [.] Analyzing function: SCErrorToString
   3003 [.] Analyzing function: strlcpy
   2982 [.] Analyzing function: SCLogMessageJSON
   2982 [.] Analyzing function: SCLogMessageGetBuffer
   2982 [.] Analyzing function: CreateIsoTimeString
   2981 [.] Analyzing function: json_decref.8298
   2930 [.] Analyzing function: SCLogMatchFGFilter
   1987 [.] Analyzing function: SCLogPrintToStream
   1465 [.] Analyzing function: SCLogMatchFGFilterWL
   1465 [.] Analyzing function: SCLogMatchFGFilterBL
   1465 [.] Analyzing function: SCLogMatchFDFilter
    994 [.] Analyzing function: SCLogReopen
    994 [.] Analyzing function: SCLogPrintToSyslog
    994 [.] Analyzing function: SCLogMapLogLevelToSyslogLevel
    514 [.] Analyzing function: SCLogMessage
     45 [.] Analyzing function: ConfNodeLookupChild
     43 [.] Analyzing function: ConfNodeNew
     29 [.] Analyzing function: RunModeRegisterNewRunMode
     29 [.] Analyzing function: RunModeGetCustomMode
     14 [.] Analyzing function: ConfSetFinal
     14 [.] Analyzing function: ConfNodeFree
     14 [.] Analyzing function: ConfGetNodeOrCreate
      8 [.] Analyzing function: LiveRegisterDeviceName

Some of the functions in this list are called from a lot of locations in the code (sometimes through macros), not sure if that is relevant. Not all of them are though. E.g. SCLogReopen is just directly called from one location, but that is from SCLogMessage, which is called for a lot of locations.

Forward -I and -D flags to clang

This was requested a lot on reddit, and I think this is a good idea.

Feel free to suggest other flags.

ikos: error while preprocessing llvm bitcode, abort.

Good day,

I managed to run ikos properly and compile a test program.
running "extract-bc" works as advertised and produces a *.bc bytecode file.
then when I run:
ikos cli.bc

I get this:
[*] Running ikos preprocessor We only lower a select if the flag is Boolean. We only lower a select if the flag is Boolean. We only lower a select if the flag is Boolean. We only lower a select if the flag is Boolean. We only lower a select if the flag is Boolean. We only lower a select if the flag is Boolean. We only lower a select if the flag is Boolean. We only lower a select if the flag is Boolean. We only lower a select if the flag is Boolean. We only lower a select if the flag is Boolean. We only lower a select if the flag is Boolean. We only lower a select if the flag is Boolean. Branch condition is not 'i1' type! br <4 x i1> %1407, label %1409, label %1410 %1407 = and <4 x i1> %1406, %1405 Branch condition is not 'i1' type! br <4 x i1> %1421, label %1423, label %1424 %1421 = and <4 x i1> %1420, %1419 Branch condition is not 'i1' type! br <4 x i1> %1435, label %1437, label %1438 %1435 = and <4 x i1> %1434, %1433 Branch condition is not 'i1' type! br <4 x i1> %1449, label %1451, label %1452 %1449 = and <4 x i1> %1448, %1447 Branch condition is not 'i1' type! br <4 x i1> %1463, label %1465, label %1466 %1463 = and <4 x i1> %1462, %1461 Branch condition is not 'i1' type! br <4 x i1> %1477, label %1479, label %1480 %1477 = and <4 x i1> %1476, %1475 Branch condition is not 'i1' type! br <4 x i1> %1491, label %1493, label %1494 %1491 = and <4 x i1> %1490, %1489 Branch condition is not 'i1' type! br <4 x i1> %1505, label %1507, label %1508 %1505 = and <4 x i1> %1504, %1503 Branch condition is not 'i1' type! br <4 x i1> %1519, label %1521, label %1522 %1519 = and <4 x i1> %1518, %1517 Branch condition is not 'i1' type! br <4 x i1> %1533, label %1535, label %1536 %1533 = and <4 x i1> %1532, %1531 Branch condition is not 'i1' type! br <4 x i1> %1547, label %1549, label %1550 %1547 = and <4 x i1> %1546, %1545 Branch condition is not 'i1' type! br <4 x i1> %1561, label %1563, label %1564 %1561 = and <4 x i1> %1560, %1559 LLVM ERROR: Broken function found, compilation aborted! ikos: error while preprocessing llvm bitcode, abort.

clang version 4.0.1 (tags/RELEASE_401/final) Target: x86_64-apple-darwin17.7.0 Thread model: posix InstalledDir: /usr/local/opt/llvm@4/bin

It appears that LLVM has a broken function somewhere and other projects not Ikos related have had the same issue based on my Google results. Have any of you come across this while using Ikos and how was it solved?

warning: possible buffer overflow - std::vector with iterators

ikos produces false positives with regard to possible buffer overflows when iterating over std::vectors.

Minimal working example:

#include <vector>

int main(int argc, char * argv[])
{
    std::vector<int> v;
    v.resize(10);

    for(int * p = v.data(); p < v.data() + 10; p++)
        if(*p == 0)
            return 1;

    return 0;
}

Output:

../../../test-use-after-free.cpp: In function 'main':
../../../test-use-after-free.cpp:10:6: warning: possible buffer overflow, pointer 'p' with offset between 0 and 39 bytes points to dynamic memory allocated at '__gnu_cxx::new_allocator<int>::allocate(unsigned long long, void const*):111:27' of size 40 bytes
                if(*p == 0)
                   ^

System:

MSYS2

Version:

$ ./ikos --version
ikos 2.1

clang-4.0: error: linker command failed with exit code 1

Development Environment

Type	Configure	OS	Kernel
DigitalOcean VPS	2vCPUs / 4 GB Memory / 80 GB Disk	Debian 8	3.16.0-5-amd64

sudo apt update && sudo apt install build-essential cmake doxygen libgmp-dev libboost-all-dev libsqlite3-dev libtinfo-dev libz-dev -y
wget http://releases.llvm.org/4.0.1/clang+llvm-4.0.1-x86_64-linux-gnu-debian8.tar.xz && tar xvf clang+llvm-4.0.1-x86_64-linux-gnu-debian8.tar.xz && rm clang+llvm-4.0.1-x86_64-linux-gnu-debian8.tar.xz
wget https://github.com/NASA-SW-VnV/ikos/archive/v1.3.tar.gz && tar xvf v1.3.tar.gz && rm v1.3.tar.gz
export CC=/root/clang+llvm-4.0.1-x86_64-linux-gnu-debian8/bin/clang && export CXX=/root/clang+llvm-4.0.1-x86_64-linux-gnu-debian8/bin/clang++
cd ikos-1.3 && mkdir build && cd build
cmake .. -DLLVM_CONFIG_EXECUTABLE=/root/clang+llvm-4.0.1-x86_64-linux-gnu-debian8/bin/llvm-config
make -j2

Error Message

Linking CXX executable ikos-pp
CMakeFiles/ikos-pp.dir/src/ikos-pp/ikos_pp.cpp.o:(.data.rel.ro._ZTIN4llvm2cl15OptionValueCopyISsEE[_ZTIN4llvm2cl15OptionValueCopyISsEE]+0x10): undefined reference to `typeinfo for llvm::cl::GenericOptionValue'
CMakeFiles/ikos-pp.dir/src/ikos-pp/ikos_pp.cpp.o:(.data.rel.ro._ZTIN4llvm2cl4listISsbNS0_6parserISsEEEE[_ZTIN4llvm2cl4listISsbNS0_6parserISsEEEE]+0x18): undefined reference to `typeinfo for llvm::cl::Option'
CMakeFiles/ikos-pp.dir/src/ikos-pp/ikos_pp.cpp.o:(.data.rel.ro._ZTIN4llvm2cl3optI7PPLevelLb0ENS0_6parserIS2_EEEE[_ZTIN4llvm2cl3optI7PPLevelLb0ENS0_6parserIS2_EEEE]+0x18): undefined reference to `typeinfo for llvm::cl::Option'
CMakeFiles/ikos-pp.dir/src/ikos-pp/ikos_pp.cpp.o:(.data.rel.ro._ZTIN4llvm2cl6parserI7PPLevelEE[_ZTIN4llvm2cl6parserI7PPLevelEE]+0x10): undefined reference to `typeinfo for llvm::cl::generic_parser_base'
CMakeFiles/ikos-pp.dir/src/ikos-pp/ikos_pp.cpp.o:(.data.rel.ro._ZTIN4llvm2cl15OptionValueCopyI7PPLevelEE[_ZTIN4llvm2cl15OptionValueCopyI7PPLevelEE]+0x10): undefined reference to `typeinfo for llvm::cl::GenericOptionValue'
CMakeFiles/ikos-pp.dir/src/ikos-pp/ikos_pp.cpp.o:(.data.rel.ro._ZTIN4llvm2cl15OptionValueCopyIbEE[_ZTIN4llvm2cl15OptionValueCopyIbEE]+0x10): undefined reference to `typeinfo for llvm::cl::GenericOptionValue'
libikos-pp-lib.a(lower_cst_expr.cpp.o):(.data.rel.ro._ZTIN7ikos_pp16LowerCstExprPassE+0x10): undefined reference to `typeinfo for llvm::ModulePass'
libikos-pp-lib.a(lower_select.cpp.o):(.data.rel.ro._ZTIN7ikos_pp11LowerSelectE+0x10): undefined reference to `typeinfo for llvm::FunctionPass'
libikos-pp-lib.a(name_values.cpp.o):(.data.rel.ro._ZTIN7ikos_pp10NameValuesE+0x10): undefined reference to `typeinfo for llvm::ModulePass'
libikos-pp-lib.a(mark_internal_inline.cpp.o):(.data.rel.ro._ZTIN7ikos_pp18MarkInternalInlineE+0x10): undefined reference to `typeinfo for llvm::ModulePass'
libikos-pp-lib.a(remove_printf_calls.cpp.o):(.data.rel.ro._ZTIN7ikos_pp17RemovePrintfCallsE+0x10): undefined reference to `typeinfo for llvm::FunctionPass'
libikos-pp-lib.a(mark_no_return_functions.cpp.o):(.data.rel.ro._ZTIN7ikos_pp21MarkNoReturnFunctionsE+0x10): undefined reference to `typeinfo for llvm::ModulePass'
libikos-pp-lib.a(remove_unreachable_blocks.cpp.o):(.data.rel.ro._ZTIN7ikos_pp23RemoveUnreachableBlocksE+0x10): undefined reference to `typeinfo for llvm::FunctionPass'
clang-4.0: error: linker command failed with exit code 1 (use -v to see invocation)
frontends/llvm/CMakeFiles/ikos-pp.dir/build.make:120: recipe for target 'frontends/llvm/ikos-pp' failed
make[2]: *** [frontends/llvm/ikos-pp] Error 1
CMakeFiles/Makefile2:2581: recipe for target 'frontends/llvm/CMakeFiles/ikos-pp.dir/all' failed
make[1]: *** [frontends/llvm/CMakeFiles/ikos-pp.dir/all] Error 2
make[1]: *** Waiting for unfinished jobs....
Linking CXX shared library libadd-loop-counters.so
[ 79%] Built target add-loop-counters
Makefile:127: recipe for target 'all' failed
make: *** [all] Error 2

Thanks in advance.

Crashed on my codebase

Just tried this static analyser on my codebase ( https://github.com/ttsiodras/renderer/ ) - and sadly, got a crash:

  CXX      renderer-BVH.o
  CXX      renderer-Loader.o
  CXX      renderer-Raytracer.o
  CXXLD    renderer
  CXX      showShadowMap-showShadowMap.o
  CXX      showShadowMap-Keyboard.o
  CXXLD    showShadowMap
make[2]: Leaving directory '/home/ttsiod/Github/renderer/src'
make[1]: Leaving directory '/home/ttsiod/Github/renderer/src'
make[1]: Entering directory '/home/ttsiod/Github/renderer'
make[1]: Nothing to be done for 'all-am'.
make[1]: Leaving directory '/home/ttsiod/Github/renderer'
Analyze lib3ds-1.3.0/tools/3dsdump? [Y/n] n
Analyze src/renderer? [Y/n] Y
[*] Running ikos src/renderer.bc -o src/renderer.db
[*] Running ikos preprocessor
[*] Running ikos analyzer
[*] Translating LLVM bitcode to AR
ikos-analyzer: /tmp/ikos-j60gqc4k/renderer.pp.bc: error: unexpected null pointer in llvm::DICompositeType with DW_TAG_structure_type or DW_TAG_class_type tag
ikos: error: a run-time error occured

The code is available in my GitHub repo, so the bug is easy to reproduce.

Link error on debian 9

I tried IKOS on Debian 9 two days ago and it worked perfectly.
I tried again today, and I'm getting a linker error.
I will investigate whenever I have time.

root@f67f01e4d08f:~/ikos/build# make all check
Scanning dependencies of target ikos-ar
[  0%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/format/dot.cpp.o
[  1%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/format/namer.cpp.o
[  1%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/format/text.cpp.o
[  3%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/pass/add_loop_counters.cpp.o
[  3%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/pass/name_values.cpp.o
[  4%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/pass/pass.cpp.o
[  4%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/pass/simplify_cfg.cpp.o
[  6%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/pass/unify_exit_nodes.cpp.o
[  6%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/pass/simplify_upcast_comparison.cpp.o
[  8%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/bundle.cpp.o
[  8%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/code.cpp.o
[  9%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/context.cpp.o
[  9%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/context_impl.cpp.o
[ 11%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/data_layout.cpp.o
[ 12%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/function.cpp.o
[ 12%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/intrinsic.cpp.o
[ 14%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/statement.cpp.o
[ 14%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/type.cpp.o
[ 16%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/value.cpp.o
[ 16%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/verify/frontend.cpp.o
[ 17%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/verify/type.cpp.o
[ 17%] Linking CXX static library libikos-ar.a
[ 17%] Built target ikos-ar
Scanning dependencies of target ikos-llvm-to-ar
[ 19%] Building CXX object frontend/llvm/CMakeFiles/ikos-llvm-to-ar.dir/src/import/bundle.cpp.o
[ 19%] Building CXX object frontend/llvm/CMakeFiles/ikos-llvm-to-ar.dir/src/import/constant.cpp.o
[ 20%] Building CXX object frontend/llvm/CMakeFiles/ikos-llvm-to-ar.dir/src/import/data_layout.cpp.o
[ 20%] Building CXX object frontend/llvm/CMakeFiles/ikos-llvm-to-ar.dir/src/import/exception.cpp.o
[ 22%] Building CXX object frontend/llvm/CMakeFiles/ikos-llvm-to-ar.dir/src/import/function.cpp.o
[ 22%] Building CXX object frontend/llvm/CMakeFiles/ikos-llvm-to-ar.dir/src/import/importer.cpp.o
[ 24%] Building CXX object frontend/llvm/CMakeFiles/ikos-llvm-to-ar.dir/src/import/library_function.cpp.o
[ 25%] Building CXX object frontend/llvm/CMakeFiles/ikos-llvm-to-ar.dir/src/import/source_location.cpp.o
[ 25%] Building CXX object frontend/llvm/CMakeFiles/ikos-llvm-to-ar.dir/src/import/type.cpp.o
[ 27%] Linking CXX static library libikos-llvm-to-ar.a
[ 27%] Built target ikos-llvm-to-ar
Scanning dependencies of target ikos-pp-lib
[ 27%] Building CXX object frontend/llvm/CMakeFiles/ikos-pp-lib.dir/src/pass/initialize.cpp.o
[ 29%] Building CXX object frontend/llvm/CMakeFiles/ikos-pp-lib.dir/src/pass/lower_cst_expr.cpp.o
[ 29%] Building CXX object frontend/llvm/CMakeFiles/ikos-pp-lib.dir/src/pass/lower_select.cpp.o
[ 30%] Building CXX object frontend/llvm/CMakeFiles/ikos-pp-lib.dir/src/pass/mark_internal_inline.cpp.o
[ 30%] Building CXX object frontend/llvm/CMakeFiles/ikos-pp-lib.dir/src/pass/mark_no_return_function.cpp.o
[ 32%] Building CXX object frontend/llvm/CMakeFiles/ikos-pp-lib.dir/src/pass/name_values.cpp.o
[ 32%] Building CXX object frontend/llvm/CMakeFiles/ikos-pp-lib.dir/src/pass/remove_printf_calls.cpp.o
[ 33%] Building CXX object frontend/llvm/CMakeFiles/ikos-pp-lib.dir/src/pass/remove_unreachable_blocks.cpp.o
[ 33%] Linking CXX static library libikos-pp.a
[ 33%] Built target ikos-pp-lib
Scanning dependencies of target ikos-pp
[ 33%] Building CXX object frontend/llvm/CMakeFiles/ikos-pp.dir/src/ikos_pp.cpp.o
[ 35%] Linking CXX executable ikos-pp
/usr/bin/ld: /usr/lib/llvm-7/lib/libLLVMBitWriter.a(BitcodeWriterPass.cpp.o): SHT_GROUP section [index 24] has no SHF_GROUP sections
/usr/bin/ld: /usr/lib/llvm-7/lib/libLLVMBitWriter.a(BitcodeWriterPass.cpp.o): SHT_GROUP section [index 25] has no SHF_GROUP sections
/usr/bin/ld: /usr/lib/llvm-7/lib/libLLVMBitWriter.a(BitcodeWriterPass.cpp.o): SHT_GROUP section [index 26] has no SHF_GROUP sections
/usr/bin/ld: /usr/lib/llvm-7/lib/libLLVMBitWriter.a(BitcodeWriterPass.cpp.o): SHT_GROUP section [index 24] has no SHF_GROUP sections
/usr/bin/ld: /usr/lib/llvm-7/lib/libLLVMBitWriter.a(BitcodeWriterPass.cpp.o): SHT_GROUP section [index 25] has no SHF_GROUP sections
/usr/bin/ld: /usr/lib/llvm-7/lib/libLLVMBitWriter.a(BitcodeWriterPass.cpp.o): SHT_GROUP section [index 26] has no SHF_GROUP sections
/usr/lib/llvm-7/lib/libLLVMBitWriter.a: error adding symbols: File format not recognized
collect2: error: ld returned 1 exit status
frontend/llvm/CMakeFiles/ikos-pp.dir/build.make:134: recipe for target 'frontend/llvm/ikos-pp' failed
make[2]: *** [frontend/llvm/ikos-pp] Error 1
CMakeFiles/Makefile2:1547: recipe for target 'frontend/llvm/CMakeFiles/ikos-pp.dir/all' failed
make[1]: *** [frontend/llvm/CMakeFiles/ikos-pp.dir/all] Error 2
Makefile:138: recipe for target 'all' failed
make: *** [all] Error 2

Build error Linking CXX executable ikos-pp

Hey am getting these errors when trying to build the ikos tool

[ 48%] Built target arbos-api
[ 48%] Built target arbos
[ 48%] Built target print
[ 48%] Built target ikos-pp-lib
[ 48%] Linking CXX executable ikos-pp
/usr/bin/ld: cannot find -lLLVMAnalysis
/usr/bin/ld: cannot find -lLLVMAsmParser
/usr/bin/ld: cannot find -lLLVMBitReader
/usr/bin/ld: cannot find -lLLVMBitWriter
/usr/bin/ld: cannot find -lLLVMCodeGen
/usr/bin/ld: cannot find -lLLVMCore
/usr/bin/ld: cannot find -lLLVMInstCombine
/usr/bin/ld: cannot find -lLLVMInstrumentation
/usr/bin/ld: cannot find -lLLVMipo
/usr/bin/ld: cannot find -lLLVMIRReader
/usr/bin/ld: cannot find -lLLVMMC
/usr/bin/ld: cannot find -lLLVMObjCARCOpts
/usr/bin/ld: cannot find -lLLVMScalarOpts
/usr/bin/ld: cannot find -lLLVMSupport
/usr/bin/ld: cannot find -lLLVMTarget
/usr/bin/ld: cannot find -lLLVMTransformUtils
/usr/bin/ld: cannot find -lLLVMVectorize
collect2: error: ld returned 1 exit status
make[2]: *** [frontends/llvm/CMakeFiles/ikos-pp.dir/build.make:87: frontends/llvm/ikos-pp] Error 1
make[1]: *** [CMakeFiles/Makefile2:2823: frontends/llvm/CMakeFiles/ikos-pp.dir/all] Error 2
make: *** [Makefile:141: all] Error 2

Wanted to see if you had any suggestions for where I could look to resolve these errors. For reference I am building this on a Fedora 26 machine.

ikos-view produces line numbers that are off by one

ikos-view produces an output that is off by one line when the file starts with an empty line. Please note that this is independent of #12 as this issue occurs both with Windows (CR LF) as well as Unix (LF) line endings.

Minimal working example:


#include <vector>

int main(int argc, char * argv[])
{
    std::vector<int> v;

    v.resize(10);

    for(int * p = v.data(); p < v.data() + 10; p++)
        if(*p == 0)
            return 1;

    return 0;
}

Output:

With first line empty:

With empty line removed:

System:

MSYS2

Version:

$ ./ikos --version
ikos 2.1

Support flexible array members

IKOS fails to run on C programs that make use of flexible array members.

To reproduce:

struct line {
  int length;
  char contents[];
};

struct line l;

int main() {
  return 0;
}

I get the following output (IKOS 2.1):

# ikos test.c
[*] Compiling test.c
[*] Running ikos preprocessor
[*] Running ikos analyzer
[*] Translating LLVM bitcode to AR
ikos-analyzer: /tmp/ikos-LdnO87/test.pp.bc: error: unexpected negative count for llvm::DICompositeType with DW_TAG_array_type tag
ikos: error: a run-time error occured

As I understand it, this occurs because flexible array members are empty arrays, causing LLVM to generate a DISubrange with a count of -1 (https://llvm.org/docs/LangRef.html#disubrange). During import IKOS checks for subranges with a negative count, producing the run-time error above. This check is at https://github.com/NASA-SW-VnV/ikos/blob/v2.1/frontend/llvm/src/import/type.cpp#L1292.

compile_commands.json support

Some tools like bear can generate a compile_commands.json file which is a standard format many other tools accept. (I thought scan-build supports this as input, but cant seem to find documentation at the moment).

It would be nice to feed this as input to ikos.

Taking a long time to execute the constructor of OutputDatabase

Ikos(built by cygwin or mingw32) takes a long time to execute the OutputDatabase‘s constructor(analyzer/src/database/output.cpp : 49) on my computer. Even the program below takes 5-6s. Is this normal, are there any suggestions?

int main() {
  return 0;
}

clang                                   : 0.148 sec
ikos-analyzer                           : 5.581 sec
ikos-analyzer.check.main                : 0.000 sec
ikos-analyzer.fixpoint-profile-analysis : 0.000 sec
ikos-analyzer.liveness-analysis         : 0.000 sec
ikos-analyzer.llvm-to-ar                : 0.000 sec
ikos-analyzer.load-bc                   : 0.002 sec
ikos-analyzer.simplify-cfg              : 0.000 sec
ikos-analyzer.simplify-upcast-comparison: 0.000 sec
ikos-analyzer.type-checker              : 0.000 sec
ikos-analyzer.unify-exit-nodes          : 0.000 sec
ikos-analyzer.value-analysis            : 0.001 sec
ikos-analyzer.value.main                : 0.000 sec
ikos-analyzer.verify-bc                 : 0.000 sec
ikos-pp                                 : 0.056 sec

Non-convergence with while(1)

Hi @arthaud

I have problems getting analysis to converge on this function:

uint32_t CLKPWR_GetCLK (uint8_t ClkType)
{
    switch(ClkType)
    {
        case CLKPWR_CLKTYPE_CPU:
            return SystemCoreClock;

        case CLKPWR_CLKTYPE_PER:
            return PeripheralClock;

        case CLKPWR_CLKTYPE_EMC:
            return EMCClock;

        case CLKPWR_CLKTYPE_USB:
            return USBClock;

        default:
            while(1); //error loop
    }
}

SystemCoreClock, PeripheralClock, EMCClock and USBClock are all uint32_t-variables.

I run IKOS like this:
ikos --entry-points=CLKPWR_GetCLK whole_program.bc

It seems the problem is with the while(1);-loop, since analysis converges immediately if I replace with assert(0);.

error: unexpected ar::Type in add_bitcast()

$ cat testcase.c
#include <stdint.h>
struct a {
  signed b : 5;
  int32_t c;
  signed d
};
e;
struct a f(uint16_t, *, *);
g() {
  int32_t h;
  i(f(i, e, h));
}
struct a f(uint16_t j, *k, *l) {}
$ ikos testcase.c 2>&1 | tail -2
ikos-analyzer: …: error: unexpected ar::Type in add_bitcast()
ikos: error: a run-time error occured

add CMake support

I can't check my project on CMake even using Makefile as a generator.

Assertion failed: (ar_cst), function translate_constant, file frontend/llvm/src/import/constant.cpp, line 200

The following code: https://github.com/myfreeweb/soad/blob/ef9b4e93ad02f66825c4174de4e38fc3174ee29b/soad.c

Apparently has some kind of integer constant ikos doesn't like:

(lldb) p *cst
error: ikos-analyzer 0x02dedb51: DW_TAG_inheritance failed to resolve the base class at 0x02dedbd3 from enclosing type 0x02dedb48.
Please file a bug and attach the file at the start of this error message
(llvm::Constant) $0 = {
  llvm::User = {
    llvm::Value = {
      VTy = 0x00000008017c96c8
      UseList = 0x00000008017dfc90
      SubclassID = '\r'
      HasValueHandle = '\0'
      SubclassOptionalData = '\0'
      SubclassData = 0
      NumUserOperands = 0
      IsUsedByMD = 0
      HasName = 0
      HasHungOffUses = 0
      HasDescriptor = 0
    }
  }
}
(lldb) p *cst->VTy
(llvm::Type) $1 = {
  Context = 0x00007fffffffc7f0
  ID = IntegerTyID
  SubclassData = 32
  NumContainedTys = 0
  ContainedTys = 0x0000000000000000
}

(or maybe this is caused by other weird bugs.. running on FreeBSD 13-current with system llvm70, most programs are causing failures)

Crash on example program loop.c

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!

CMAKE_BUILD_TYPE=Release but it says 'ikos was compiled in debug mode'

[!] ikos was compiled in debug mode, the analysis might be slow

error: a run-time error occured - non-static data member arrays with initializer

ikos encounters a run-time error when non-static data member arrays have an initializer.

Minimal working example:

struct MyStruct
{
    bool isDown[3] = {};
};

int main(int argc, char * argv[])
{
    MyStruct s;

    return 0;
}

Output:

$ ./ikos /home/username/test-member-initialization.cpp -v
[*] Compiling C:/msys64/home/username/test-member-initialization.cpp
[.] Running C:/msys64/mingw64/bin/clang.exe -c -emit-llvm -Wall -U_FORTIFY_SOURCE -D_FORTIFY_SOURCE=0 -g -O0 -Xclang -disable-O0-optnone 'C:/msys64/home/username/test-member-initialization.cpp' -o 'C:/Users/username/AppData/Local/Temp/ikos-83d3zstj/test-member-initialization.bc' -isystem 'C:/msys64/home/username/ikos-2.1/install/include' -fcolor-diagnostics -std=c++14
C:/msys64/home/username/test-member-initialization.cpp:9:11: warning: unused variable 's' [-Wunused-variable]
        MyStruct s;
                 ^
1 warning generated.
[*] Running ikos preprocessor
[.] Running 'C:/msys64/home/username/ikos-2.1/install/bin/ikos-pp.exe' -opt=basic -entry-points=main 'C:/Users/username/AppData/Local/Temp/ikos-83d3zstj/test-member-initialization.bc' -o 'C:/Users/username/AppData/Local/Temp/ikos-83d3zstj/test-member-initialization.pp.bc'
[*] Running ikos analyzer
[.] Running 'C:/msys64/home/username/ikos-2.1/install/bin/ikos-analyzer.exe' -a=sound,dfa,dca,dbz,boa,sio,prover,nullity,fca,pcmp,shc -d=interval -entry-points=main -globals-init=skip-big-arrays -prec=mem -proc=inter -allow-dbg-mismatch -display-checks=no -display-inv=no -color=auto -log=debug 'C:/Users/username/AppData/Local/Temp/ikos-83d3zstj/test-member-initialization.pp.bc' -o output.db
[.] Creating output database output.db
[.] Loading LLVM bitcode
[.] Verifying integrity of LLVM bitcode
[.] Checking for debug information
[*] Translating LLVM bitcode to AR
[.] Running type verifier on AR
[.] Running simplify-cfg pass on AR
[.] Running simplify-upcast-comparison pass on AR
[.] Running unify-exit-nodes pass on AR
[*] Running liveness analysis
[.] Running liveness analysis on function @_ZN8MyStructC2Ev
[.] Running liveness analysis on function @main
[*] Running fixpoint profile analysis
[*] Running interprocedural value analysis
[.] Computing global variable static initialization
[*] Analyzing entry point: main
[.] Analyzing function: MyStruct::MyStruct()
[*] Checking properties and writing results for entry point: main
ikos: error: a run-time error occured

System:

MSYS2

Version:

$ ./ikos --version
ikos 2.1

Support llvm instructions insertelement and extractelement

The llvm instructions insertelement and extractelement are currently not supported.
They could be translated into ar::InsertElement and ar::ExtractElement, the same way we translate insertvalue and extractvalue.

To reproduce:

#include <stdio.h>

typedef struct {
  float x;
  float y;
} pos_t;

typedef struct { pos_t begin, end; } line_t;

line_t f(float y) {
  return {{0.0, y}, {2.0, 0}};
}

int main() {
  printf("%f\n", f(2.0).begin.y);
  return 0;
}

Using ikos --opt=aggressive:

$ ikos test.cpp --opt=aggressive
[*] Compiling test.cpp
[*] Running ikos preprocessor
[*] Running ikos analyzer
[!] ikos was compiled in debug mode, the analysis might be slow
[*] Translating LLVM bitcode to AR
  %.sroa.0.4.vec.insert = insertelement <2 x float> <float 0.000000e+00, float undef>, float %0, i32 1, !dbg !24
ikos-analyzer: /var/folders/9g/hvg_xszs3q79k8tvtqhm_q5s5y3dxb/T/ikos-ynzQre/test.pp.bc: error: unsupported llvm::Instruction (opcode: insertelement)
ikos: error: a run-time error occured

Support llvm instruction shufflevector

The llvm instruction shufflevector is currently not supported.
This instruction is generated when using Intel intrinsic _mm_shuffle_ps.

Short example:

#include <x86intrin.h>

extern void printv(__m128);

int main(int argc, char** argv) {
    __m128 m = _mm_set_ps(4, 3, 2, 1);
    m = _mm_shuffle_ps(m, m, 0x1B);
    printv(m);
}

$ ikos test.c
[*] Compiling test.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: /var/folders/9g/hvg_xszs3q79k8tvtqhm_q5s5y3dxb/T/ikos-iDBHbA/test.pp.bc: error: unsupported llvm::Instruction in infer_type_hint_use() (opcode: shufflevector)
ikos: error: a run-time error occurred

To support shufflevector, we could translate it into:

an ar::ShuffleVector statement;
a call to an intrinsic function ar.shufflevector.

Implementing the behavior seems pretty hard to me, and probably pointless since it probably won't help to prove properties we are interested in (e.g, buffer overflows). I'm thinking about ignoring it safely (set the result to top).

error: a run-time error occured - std::vector of char

ikos encounters a run-time error when std::vectors with a char as element type is used. This error does not occur when an unsigned char or signed char is used. Possibly related to #20 (comment) and #21 (comment) but here provided with minimal working example.

Minimal working example:

#include <vector>

int main(int argc, char * argv[])
{
    std::vector<char> v;

    return 0;
}

Output:

$ ./ikos /home/username/test-vector.cpp -v
[*] Compiling C:/msys64/home/username/test-vector.cpp
[.] Running C:/msys64/mingw64/bin/clang.exe -c -emit-llvm -Wall -U_FORTIFY_SOURCE -D_FORTIFY_SOURCE=0 -g -O0 -Xclang -disable-O0-optnone 'C:/msys64/home/username/test-vector.cpp' -o 'C:/Users/username/AppData/Local/Temp/ikos-3sw6dqmp/test-vector.bc' -isystem 'C:/msys64/home/username/ikos-2.1/install/include' -fcolor-diagnostics -std=c++14
[*] Running ikos preprocessor
[.] Running 'C:/msys64/home/username/ikos-2.1/install/bin/ikos-pp.exe' -opt=basic -entry-points=main 'C:/Users/username/AppData/Local/Temp/ikos-3sw6dqmp/test-vector.bc' -o 'C:/Users/username/AppData/Local/Temp/ikos-3sw6dqmp/test-vector.pp.bc'
[*] Running ikos analyzer
[.] Running 'C:/msys64/home/username/ikos-2.1/install/bin/ikos-analyzer.exe' -a=prover,sio,sound,fca,dfa,pcmp,shc,dca,nullity,boa,dbz -d=interval -entry-points=main -globals-init=skip-big-arrays -prec=mem -proc=inter -allow-dbg-mismatch -display-checks=no -display-inv=no -color=auto -log=debug 'C:/Users/username/AppData/Local/Temp/ikos-3sw6dqmp/test-vector.pp.bc' -o output.db
[.] Creating output database output.db
[.] Loading LLVM bitcode
[.] Verifying integrity of LLVM bitcode
[.] Checking for debug information
[*] Translating LLVM bitcode to AR
ikos-analyzer.exe: C:/Users/username/AppData/Local/Temp/ikos-3sw6dqmp/test-vector.pp.bc: error: unexpected null pointer in llvm::DICompositeType with DW_TAG_structure_type or DW_TAG_class_type tag
ikos: error: a run-time error occured

System:

MSYS2

Version:

$ ./ikos --version
ikos 2.1

Is include(HandleLLVMOptions) and include(AddLLVM) necessary?

I made some changes on llvm and built it with msvc14. When I built IKOS with mingw32-gcc, there was a problem with win-like-path to posix-like-path in HandleLLVMOptions.cmake or AddLLVM.cmake. They seem useless, can I remove them?

error: unexpected negative count for llvm::DICompositeType with DW_TAG_array_type tag

When trying out Ikos on the Suricata code base, I see the following error:

root@c08dee9a79a9:~/suricata# ikos -v src/suricata.bc 
[*] Running ikos preprocessor
[.] Running /ikos/install/bin/ikos-pp -opt=basic -entry-points=main src/suricata.bc -o /tmp/ikos-r7ALl_/suricata.pp.bc
[*] Running ikos analyzer
[.] Running /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 -allow-dbg-mismatch -display-checks=no -display-inv=no -color=auto -log=debug /tmp/ikos-r7ALl_/suricata.pp.bc -o output.db
[.] Creating output database output.db
[.] Loading LLVM bitcode
[.] Verifying integrity of LLVM bitcode
[.] Checking for debug information
[*] Translating LLVM bitcode to AR
ikos-analyzer: /tmp/ikos-r7ALl_/suricata.pp.bc: error: unexpected negative count for llvm::DICompositeType with DW_TAG_array_type tag
ikos: error: a run-time error occured

The error looks a lot like the one in #18. The suggested work around there doesn't work, since -allow-dbg-mismatch is already passed to ikos-analyzer.

This is on Ubuntu 18.10 in a docker setup.

Can not compile with llvm/clang 4.0.1

$ mingw32-make
[ 17%] Built target ikos-ar
[ 25%] Built target ikos-pp-lib
mingw32-make[2]: *** No rule to make target 'LLVMAnalysis-NOTFOUND', needed by 'frontend/llvm/ikos-pp.exe'.  Stop.
mingw32-make[1]: *** [CMakeFiles\Makefile2:1614: frontend/llvm/CMakeFiles/ikos-pp.dir/all] Error 2
mingw32-make: *** [Makefile:140: all] Error 2

Errors occur when including llvm/ToolOutputFile.h and llvm/InitializePasses.h using llvm 4.0.1.
After solving them, there are still error upon.

False positive on a pointer to integer cast generated by pointer arithmetic

ikos produces false positives with regard to null pointers and use after free when resizing a std::vector twice. This might be related to #39, but in this case the warning message prints "which might be released".

Minimal working example:

#include <vector>

int main(int argc, char * argv[])
{
	std::vector<int> v;

	v.resize(1);
	v.resize(1);
	int * p = v.data();
	*p = 0;

	return 0;
}

Output:

test-use-after-free-3.cpp: In function 'main':
test-use-after-free-3.cpp:11:5: warning: pointer 'p' might be null
        *p = 0;
           ^
test-use-after-free-3.cpp: In function 'main':
test-use-after-free-3.cpp:11:5: warning: possible use after free, pointer 'p' points to:
                                                * dynamic memory allocated at '__gnu_cxx::new_allocator<int>::allocate(unsigned long long, void const*):111:27', which might be released
                                                * dynamic memory allocated at '__gnu_cxx::new_allocator<int>::allocate(unsigned long long, void const*):111:27', which might be released
        *p = 0;
           ^

System:

MSYS2

Version:

8c9e9fb

error: a run-time error occured - std::sort

ikos encounters a run-time error when a std::vector is std::sorted.

Minimal working example:

#include <vector>
#include <algorithm>

int main(int argc, char * argv[])
{
	std::vector<int> v;

	std::sort(v.begin(), v.end());

	return 0;
}

Output:

$ ./ikos /home/username/test-sort.cpp -v
[*] Compiling C:/msys64/home/username/test-sort.cpp
[.] Running C:/msys64/mingw64/bin/clang.exe -c -emit-llvm -Wall -U_FORTIFY_SOURCE -D_FORTIFY_SOURCE=0 -g -O0 -Xclang -disable-O0-optnone 'C:/msys64/home/username/test-sort.cpp' -o 'C:/Users/username/AppData/Local/Temp/ikos-k9ml8851/test-sort.bc' -isystem 'C:/msys64/home/username/ikos-2.1/install/include' -fcolor-diagnostics -std=c++14
[*] Running ikos preprocessor
[.] Running 'C:/msys64/home/username/ikos-2.1/install/bin/ikos-pp.exe' -opt=basic -entry-points=main 'C:/Users/username/AppData/Local/Temp/ikos-k9ml8851/test-sort.bc' -o 'C:/Users/username/AppData/Local/Temp/ikos-k9ml8851/test-sort.pp.bc'
[*] Running ikos analyzer
[.] Running 'C:/msys64/home/username/ikos-2.1/install/bin/ikos-analyzer.exe' -a=pcmp,nullity,sound,dfa,dbz,fca,dca,boa,sio,prover,shc -d=interval -entry-points=main -globals-init=skip-big-arrays -prec=mem -proc=inter -allow-dbg-mismatch -display-checks=no -display-inv=no -color=auto -log=debug 'C:/Users/username/AppData/Local/Temp/ikos-k9ml8851/test-sort.pp.bc' -o output.db
[.] Creating output database output.db
[.] Loading LLVM bitcode
[.] Verifying integrity of LLVM bitcode
[.] Checking for debug information
[*] Translating LLVM bitcode to AR
ikos-analyzer.exe: C:/Users/username/AppData/Local/Temp/ikos-k9ml8851/test-sort.pp.bc: error: unsupported intrinsic function @llvm.ctlz.i64
ikos: error: a run-time error occured

System:

MSYS2

Version:

$ ./ikos --version
ikos 2.1

error: unexpected tag for union member of llvm::DICompositeType

Thanks for a very impressive tool!

I've successfully tried ikos against various small programs. I really like it!

When giving it a try against the Bitcoin Core project I encountered an error which I'm unable to resolve:

$ git clone https://github.com/bitcoin/bitcoin bitcoin-ikos
$ cd bitcoin-ikos/
$ ./autogen.sh
$ ikos-scan ./configure --disable-wallet --disable-hardening --disable-asm --disable-zmq --with-gui=no --without-miniupnpc --disable-bench --enable-debug
$ ikos-scan make
…
make[1]: Leaving directory '/root/build-bitcoin/bitcoin-ikos'
Analyze src/bitcoin-cli? [Y/n]
[*] Running ikos src/bitcoin-cli.bc -o src/bitcoin-cli.db
[*] Running ikos preprocessor
[*] Running ikos analyzer
[*] Translating LLVM bitcode to AR
ikos-analyzer: /tmp/ikos-BQBQ4G/bitcoin-cli.pp.bc: error: unexpected tag for union member of llvm::DICompositeType
ikos: error: a run-time error occured

What can I do to try to resolve it? :-)

Make failed with the following error

error: llvm::DICompositeType with DW_TAG_array_type tag, but llvm::StructType is not the last element

$ cat testcase.c
struct {
  unsigned : 7;
  unsigned a
} b[6][1] = {{{}}};
$ ikos testcase.c 2>&1 | tail -2
ikos-analyzer: …: error: llvm::DICompositeType with DW_TAG_array_type tag, but llvm::StructType is not the last element
ikos: error: a run-time error occured

Problem with narrowing strategy for nonmonotonic transformation function

int count = 10;
int main() {
  int i;
  for (i = 0; i < 10; i++) {
    count = count >> 1;
  }
  return 0;
}

it seems having problem with narrowing strategy for nonmonotonic transformation function.
like code upon, using interval domain, the analyzer can not stop.

Compile error using ninja

I am getting an error when I try to build ikos using ninja:

$ cmake -GNinja ..
[...]
$ ninja
[35/119] Linking CXX executable frontend/llvm/ikos-pp
FAILED: frontend/llvm/ikos-pp
: && /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/c++  -fPIC -fvisibility-inlines-hidden -Werror=date-time -Werror=unguarded-availability-new -std=c++11 -w -fdiagnostics-color -g -Wl,-search_paths_first -Wl,-headerpad_max_install_names -Wl,--color-diagnostics frontend/llvm/CMakeFiles/ikos-pp.dir/src/ikos_pp.cpp.o  -o frontend/llvm/ikos-pp  frontend/llvm/libikos-pp.a /Users/marthaud/Homebrew/Cellar/llvm/7.0.0_1/lib/libLLVMAnalysis.a /Users/marthaud/Homebrew/Cellar/llvm/7.0.0_1/lib/libLLVMAsmParser.a /Users/marthaud/Homebrew/Cellar/llvm/7.0.0_1/lib/libLLVMBitReader.a /Users/marthaud/Homebrew/Cellar/llvm/7.0.0_1/lib/libLLVMBitWriter.a /Users/marthaud/Homebrew/Cellar/llvm/7.0.0_1/lib/libLLVMCodeGen.a /Users/marthaud/Homebrew/Cellar/llvm/7.0.0_1/lib/libLLVMCore.a /Users/marthaud/Homebrew/Cellar/llvm/7.0.0_1/lib/libLLVMCoroutines.a /Users/marthaud/Homebrew/Cellar/llvm/7.0.0_1/lib/libLLVMInstCombine.a /Users/marthaud/Homebrew/Cellar/llvm/7.0.0_1/lib/libLLVMInstrumentation.a /Users/marthaud/Homebrew/Cellar/llvm/7.0.0_1/lib/libLLVMipo.a /Users/marthaud/Homebrew/Cellar/llvm/7.0.0_1/lib/libLLVMIRReader.a /Users/marthaud/Homebrew/Cellar/llvm/7.0.0_1/lib/libLLVMMC.a /Users/marthaud/Homebrew/Cellar/llvm/7.0.0_1/lib/libLLVMObjCARCOpts.a /Users/marthaud/Homebrew/Cellar/llvm/7.0.0_1/lib/libLLVMScalarOpts.a /Users/marthaud/Homebrew/Cellar/llvm/7.0.0_1/lib/libLLVMSupport.a /Users/marthaud/Homebrew/Cellar/llvm/7.0.0_1/lib/libLLVMTarget.a /Users/marthaud/Homebrew/Cellar/llvm/7.0.0_1/lib/libLLVMTransformUtils.a /Users/marthaud/Homebrew/Cellar/llvm/7.0.0_1/lib/libLLVMVectorize.a /Users/marthaud/Homebrew/lib/libboost_filesystem-mt.dylib /Users/marthaud/Homebrew/lib/libboost_system-mt.dylib /Users/marthaud/Homebrew/Cellar/llvm/7.0.0_1/lib/libLLVMBitWriter.a /Users/marthaud/Homebrew/Cellar/llvm/7.0.0_1/lib/libLLVMInstrumentation.a /Users/marthaud/Homebrew/Cellar/llvm/7.0.0_1/lib/libLLVMAsmParser.a /Users/marthaud/Homebrew/Cellar/llvm/7.0.0_1/lib/libLLVMLinker.a /Users/marthaud/Homebrew/Cellar/llvm/7.0.0_1/lib/libLLVMInstCombine.a /Users/marthaud/Homebrew/Cellar/llvm/7.0.0_1/lib/libLLVMAggressiveInstCombine.a /Users/marthaud/Homebrew/Cellar/llvm/7.0.0_1/lib/libLLVMTransformUtils.a /Users/marthaud/Homebrew/Cellar/llvm/7.0.0_1/lib/libLLVMAnalysis.a /Users/marthaud/Homebrew/Cellar/llvm/7.0.0_1/lib/libLLVMObject.a /Users/marthaud/Homebrew/Cellar/llvm/7.0.0_1/lib/libLLVMBitReader.a /Users/marthaud/Homebrew/Cellar/llvm/7.0.0_1/lib/libLLVMMCParser.a /Users/marthaud/Homebrew/Cellar/llvm/7.0.0_1/lib/libLLVMMC.a /Users/marthaud/Homebrew/Cellar/llvm/7.0.0_1/lib/libLLVMDebugInfoCodeView.a /Users/marthaud/Homebrew/Cellar/llvm/7.0.0_1/lib/libLLVMDebugInfoMSF.a /Users/marthaud/Homebrew/Cellar/llvm/7.0.0_1/lib/libLLVMProfileData.a /Users/marthaud/Homebrew/Cellar/llvm/7.0.0_1/lib/libLLVMCore.a /Users/marthaud/Homebrew/Cellar/llvm/7.0.0_1/lib/libLLVMBinaryFormat.a /Users/marthaud/Homebrew/Cellar/llvm/7.0.0_1/lib/libLLVMSupport.a -lz -lcurses -lm /Users/marthaud/Homebrew/Cellar/llvm/7.0.0_1/lib/libLLVMDemangle.a && :
ld: unknown option: --color-diagnostics
clang: error: linker command failed with exit code 1 (use -v to see invocation)
[44/119] Building CXX object analyzer/CMakeFiles/ikos-analyzer.dir/src/ikos_analyzer.cpp.o
ninja: build stopped: subcommand failed.

error: unsupported llvm::Instruction in infer_type_hint_use() (opcode: insertelement)

To reproduce:

$ git clone https://github.com/sipa/minisketch minisketch-ikos
$ cd minisketch-ikos/src
$ ikos-scan make
…
ikos-scan-c++ -DHAVE_CLZ -O2 -g0 -Wall -std=c++11 bench.o libminisketch.a -o bench
Analyze test-exhaust? [Y/n]
[*] Running ikos test-exhaust.bc -o test-exhaust.db
[*] Running ikos preprocessor
[*] Running ikos analyzer
[*] Translating LLVM bitcode to AR
ikos-analyzer: /tmp/ikos-xWxGFk/test-exhaust.pp.bc: error: unsupported llvm::Instruction in infer_type_hint_use() (opcode: insertelement)
ikos: error: a run-time error occured

error: llvm::DICompositeType with DW_TAG_array_type tag and llvm::StructType have a different number of elements

$ cat testcase.cpp
struct i {
  unsigned j[16];
} k[]{{}, {2}};
$ clang++ -c testcase.cpp
$ ikos testcase.cpp
[*] Compiling testcase.cpp
[*] Running ikos preprocessor
[*] Running ikos analyzer
[*] Translating LLVM bitcode to AR
ikos-analyzer: …: error: llvm::DICompositeType with DW_TAG_array_type tag and llvm::StructType have a different number of elements
ikos: error: a run-time error occured

Please consider another license

First, sorry to be a pain with license

The NASA OS license isn't considered as a free license by at least the FSF and Debian.
This prevents the inclusion of ikos into Debian & Ubuntu repositories.

Sources:
https://www.gnu.org/licenses/license-list.html#NASA
https://en.wikipedia.org/wiki/NASA_Open_Source_Agreement

document icos-scan

Looks like there's another tool that wasn't in the readme: https://www.reddit.com/r/C_Programming/comments/a5a5nc/ikos_21_an_open_source_static_analyzer_for_c_and_c/ebm1r8i/

error: unexpected dwarf encoding for llvm::DIBasicType

I got the following error when digging the problem in issue #21:

unexpected dwarf encoding for llvm::DIBasicType

I was able to reproduce it with the following example:

int f(decltype(nullptr) x) {
	return 1;
}

int main() {
	return f(nullptr);
}

error: unexpected opaque llvm::StructType

$ cat testcase.cpp
namespace a {
namespace b {
struct c;
template <typename ae, typename af, typename d, typename ag, typename ah>
void e(d, ag, ah, ae, af) {}
template <typename d> class f {
public:
  f(d);
};
} // namespace b
} // namespace a
class g {
  struct h {};
  template <typename d, typename ag> void am(d i, ag j) {
    e(i, j, h(), 0, static_cast<a::b::c *>(0));
  }
  template <typename d> void ap(d i) { am(i, 0); }

public:
  void aq() {
    int an;
    a::b::f ar(an);
    ap(ar);
  }
};
void aw() {
  g au;
  au.aq();
}
$ ikos testcase.cpp
[*] Compiling testcase.cpp
…
[*] Running ikos preprocessor
[*] Running ikos analyzer
[*] Translating LLVM bitcode to AR
ikos-analyzer: …: error: unexpected opaque llvm::StructType
ikos: error: a run-time error occured

warning: pointer might be null/possible use after free - copying between std::vectors

ikos produces false positives with regard to null pointers and use after free after copying from one std::vector to another std::vector.

Minimal working example:

#include <vector>

struct MyStruct
{
    int i;
};

int main(int argc, char * argv[])
{
    std::vector<MyStruct> v1;
    v1.resize(1);

    std::vector<MyStruct> v2;

    for(MyStruct * p = v1.data(); p < v1.data() + 1; p++)
        v2.push_back(*p);

    MyStruct s = *v2.data();

    return 0;
}

Output:

../../../test-use-after-free-2.cpp: In function 'main':
../../../test-use-after-free-2.cpp:19:15: warning: pointer '(int8_t*)(std::vector<MyStruct, std::allocator<MyStruct> >::data()(&v2))' might be null
        MyStruct s = *v2.data();
                     ^
../../../test-use-after-free-2.cpp: In function 'main':
../../../test-use-after-free-2.cpp:19:15: warning: possible use after free, pointer '(int8_t*)(std::vector<MyStruct, std::allocator<MyStruct> >::data()(&v2))' points to dynamic memory allocated at '__gnu_cxx::new_allocator<MyStruct>::allocate(unsigned long long, void const*):111:27'
        MyStruct s = *v2.data();
                     ^

System:

MSYS2

Version:

$ ./ikos --version
ikos 2.1

Misleading dead code in a generated catch block

ikos produces false positives with regard to dead code in destructors.

Minimal working example:

#include <cstdlib>

struct MyStruct
{
    MyStruct()
    {
        data = (char*)malloc(10);
    }

    ~MyStruct()
    {
        free(data);
    }

    char * data;
};

int main(int argc, char * argv[])
{
    MyStruct s;

    return 0;
}

Output:

# Results
../../../test-destructor.cpp: In function 'MyStruct::~MyStruct()':
../../../test-destructor.cpp:13:3: unreachable: code is dead
                free(data);
                ^
../../../test-destructor.cpp: In function 'MyStruct::~MyStruct()':
../../../test-destructor.cpp:13:3: unreachable: code is dead
                free(data);
                ^

System:

MSYS2

Version:

$ ./ikos --version
ikos 2.1

Problem with widening global pointers in loop

int *p;
void main() {
  int i;
  int A[4];
  p = A;
  for (i = 0; i < 10; i++) {
    p++;  
  }
}

if i do not use globals-init=none, it seems having problem while widening global pointers in loop.

Problem with ZEXT SEXT and TRUNC

extern int random();
unsigned char cnt;
void main() {
  int A[8];
  cnt = random();
  if (cnt > 0 && cnt < 8) { 
    A[cnt] = 0;
  }
}

In this case, we can't find relationships between pre-conversion and post-conversion because the implicit conversion produces temporary variables.
I used to convert a = ZEXT(b) (SEXT or TRUNC) to a = b or add a equals b relation to the relational abstraction when it is sound.
Is there any other better way or we should modify current transfer functions?

ikos-analyzer fails: error: llvm::Type and ar::Type alloc size are different

$ ikos test.cpp 
[*] Compiling test.cpp
[*] Running ikos preprocessor
[*] Running ikos analyzer
[*] Translating LLVM bitcode to AR
ikos-analyzer: /tmp/ikos-ON9hAd/test.pp.bc: error: llvm::Type and ar::Type alloc size are different
ikos: error: a run-time error occured

test.cpp is a testcase for the osg library (http://www.openscenegraph.org/).

test.cpp.txt

FreeBSD 11.2 amd64
ikos-2.1 installed from the port.
llvm-70, clang-70.

Failed to get it working

Hi,

I failed to get it working. Here is my frustrating list of what I have tried:

Failed to build on Ubuntu 18.10 x64 using Clang 7 and GCC 7.3
Failed to install on macOS Mojave using brew install
Failed to build from source on macOS Mojave using clang++-7 installed using brew
Failed to build from source on macOS Mojave using Apple clang
Failed to build from source on macOS Mojave using GCC-8

I am an expert C/C++ user, it is very rare that I fail to build any C/C++ project!

Below are 2 error messages I encountered:

The first error message is from brew install.
The second error message is from building ikos from source on macOS Mojave using clang++-7.

$ brew install nasa-sw-vnv/core/ikos
Updating Homebrew...
==> Auto-updated Homebrew!
Updated 1 tap (homebrew/core).
==> Updated Formulae
mutt

==> Tapping nasa-sw-vnv/core
Cloning into '/usr/local/Homebrew/Library/Taps/nasa-sw-vnv/homebrew-core'...
remote: Enumerating objects: 7, done.
remote: Counting objects: 100% (7/7), done.
remote: Compressing objects: 100% (7/7), done.
remote: Total 7 (delta 0), reused 5 (delta 0), pack-reused 0
Unpacking objects: 100% (7/7), done.
Tapped 2 formulae (34 files, 32.5KB).
==> Installing ikos from nasa-sw-vnv/core
==> Installing dependencies for nasa-sw-vnv/core/ikos: ppl and apron
==> Installing nasa-sw-vnv/core/ikos dependency: ppl
==> Downloading https://homebrew.bintray.com/bottles/ppl-1.2.mojave.bottle.1.tar.gz
==> Downloading from https://akamai.bintray.com/59/59aa81dbfdc59de055e528724282fb0a1f7c627fc4bbc2f6b2d026e0
######################################################################## 100.0%
==> Pouring ppl-1.2.mojave.bottle.1.tar.gz
🍺  /usr/local/Cellar/ppl/1.2: 1,882 files, 43.4MB
==> Installing nasa-sw-vnv/core/ikos dependency: apron
==> Downloading http://apron.cri.ensmp.fr/library/apron-0.9.10.tgz
######################################################################## 100.0%
==> Patching
patching file ppl/ppl_user.cc
patching file products/Makefile
==> make APRON_PREFIX=/usr/local/Cellar/apron/0.9.10 GMP_PREFIX=/usr/local/opt/gmp MPFR_PREFIX=/usr/local/o
🍺  /usr/local/Cellar/apron/0.9.10: 125 files, 8.8MB, built in 1 minute 40 seconds
==> Installing nasa-sw-vnv/core/ikos
==> Downloading https://github.com/nasa-sw-vnv/ikos/releases/download/v2.1/ikos-2.1.tar.gz
==> Downloading from https://github-production-release-asset-2e65be.s3.amazonaws.com/107311216/92e8fc00-fc91-11e8-9865-791f35ccb369?X-Amz-Algorithm=AWS4-HMAC-SHA256&X-Amz-Credential=AKIAIWNJYA
######################################################################## 100.0%
==> Downloading https://files.pythonhosted.org/packages/4e/8b/75469c270ac544265f0020aa7c4ea925c5284b23e445cf3aa8b99f662690/virtualenv-16.1.0.tar.gz
######################################################################## 100.0%
==> python -c import setuptools... --no-user-cfg install --prefix=/private/tmp/ikos--homebrew-virtualenv-20181212-90845-13xpewv/target --install-scripts=/private/tmp/ikos--homebrew-virtualenv-
Last 15 lines from /Users/kim/Library/Logs/Homebrew/ikos/01.python:
-c
import setuptools, tokenize
__file__ = 'setup.py'
exec(compile(getattr(tokenize, 'open', open)(__file__).read()
  .replace('\r\n', '\n'), __file__, 'exec'))
--no-user-cfg
install
--prefix=/private/tmp/ikos--homebrew-virtualenv-20181212-90845-13xpewv/target
--install-scripts=/private/tmp/ikos--homebrew-virtualenv-20181212-90845-13xpewv/target/bin
--single-version-externally-managed
--record=installed.txt

/System/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/distutils/dist.py:267: UserWarning: Unknown distribution option: 'python_requires'
  warnings.warn(msg)
error in virtualenv setup command: 'extras_require' must be a dictionary whose values are strings or lists of strings containing valid project/version requirement specifiers.

If reporting this issue please do so at (not Homebrew/brew or Homebrew/core):
https://github.com/nasa-sw-vnv/homebrew-core/issues

/usr/local/Homebrew/Library/Homebrew/utils/github.rb:245:in `raise_api_error': GitHub Must specify two-factor authentication OTP code.:The GitHub credentials in the macOS keychain may be invalid. (GitHub::AuthenticationFailedError)
Clear them with:
  printf "protocol=https\nhost=github.com\n" | git credential-osxkeychain erase
Or create a personal access token:
  https://github.com/settings/tokens/new?scopes=gist,public_repo&description=Homebrew
echo 'export HOMEBREW_GITHUB_API_TOKEN=your_token_here' >> ~/.bash_profile
	from /usr/local/Homebrew/Library/Homebrew/utils/github.rb:206:in `open_api'
	from /usr/local/Homebrew/Library/Homebrew/utils/github.rb:324:in `search'
	from /usr/local/Homebrew/Library/Homebrew/utils/github.rb:257:in `search_issues'
	from /usr/local/Homebrew/Library/Homebrew/utils/github.rb:270:in `issues_for_formula'
	from /usr/local/Homebrew/Library/Homebrew/exceptions.rb:372:in `fetch_issues'
	from /usr/local/Homebrew/Library/Homebrew/exceptions.rb:368:in `issues'
	from /usr/local/Homebrew/Library/Homebrew/exceptions.rb:422:in `dump'
	from /usr/local/Homebrew/Library/Homebrew/brew.rb:127:in `rescue in <main>'
	from /usr/local/Homebrew/Library/Homebrew/brew.rb:17:in `<main>'

$ CXX=/usr/local/opt/llvm@7/bin/clang++ CC=/usr/local/opt/llvm@7/bin/clang cmake .. -DLLVM_CONFIG_EXECUTABLE="$(brew --prefix)/opt/llvm@7/bin/llvm-config"
-- The C compiler identification is Clang 7.0.0
-- The CXX compiler identification is Clang 7.0.0
-- Check for working C compiler: /usr/local/opt/llvm@7/bin/clang
-- Check for working C compiler: /usr/local/opt/llvm@7/bin/clang -- works
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Detecting C compile features
-- Detecting C compile features - done
-- Check for working CXX compiler: /usr/local/opt/llvm@7/bin/clang++
-- Check for working CXX compiler: /usr/local/opt/llvm@7/bin/clang++ -- works
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- All libraries and binaries will be installed in /Users/kim/Downloads/ikos-master/install
-- Including core
-- All libraries and binaries will be installed in /Users/kim/Downloads/ikos-master/install
-- Found Boost: /usr/local/include (found version "1.68.0")
-- Found the following Boost libraries:
--   unit_test_framework
-- Found GMP: /usr/local/include  
-- Found MPFR: /usr/local/include (Required is at least version "1.0.0") 
-- Found PPL: /usr/local/Cellar/ppl/1.2/include  
-- Found APRON: /usr/local/include  
-- Performing Test CXX_SUPPORTS_CXX14
-- Performing Test CXX_SUPPORTS_CXX14 - Success
-- Performing Test CXX_SUPPORTS_FVISIBILITY_INLINES_HIDDEN
-- Performing Test CXX_SUPPORTS_FVISIBILITY_INLINES_HIDDEN - Success
-- Performing Test CXX_SUPPORTS_WALL
-- Performing Test CXX_SUPPORTS_WALL - Success
-- Performing Test CXX_SUPPORTS_WEXTRA
-- Performing Test CXX_SUPPORTS_WEXTRA - Success
-- Performing Test CXX_SUPPORTS_WEVERYTHING
-- Performing Test CXX_SUPPORTS_WEVERYTHING - Success
-- Performing Test CXX_SUPPORTS_WNO_SWITCH_ENUM
-- Performing Test CXX_SUPPORTS_WNO_SWITCH_ENUM - Success
-- Performing Test CXX_SUPPORTS_WNO_PADDED
-- Performing Test CXX_SUPPORTS_WNO_PADDED - Success
-- Performing Test CXX_SUPPORTS_WNO_CXX98_COMPAT
-- Performing Test CXX_SUPPORTS_WNO_CXX98_COMPAT - Success
-- Performing Test CXX_SUPPORTS_WNO_CXX98_COMPAT_PEDANTIC
-- Performing Test CXX_SUPPORTS_WNO_CXX98_COMPAT_PEDANTIC - Success
-- Performing Test CXX_SUPPORTS_WNO_C99_EXTENSIONS
-- Performing Test CXX_SUPPORTS_WNO_C99_EXTENSIONS - Success
-- Performing Test CXX_SUPPORTS_WNO_COVERED_SWITCH_DEFAULT
-- Performing Test CXX_SUPPORTS_WNO_COVERED_SWITCH_DEFAULT - Success
-- Performing Test CXX_SUPPORTS_WNO_EXIT_TIME_DESTRUCTORS
-- Performing Test CXX_SUPPORTS_WNO_EXIT_TIME_DESTRUCTORS - Success
-- Performing Test CXX_SUPPORTS_WNO_GLOBAL_CONSTRUCTORS
-- Performing Test CXX_SUPPORTS_WNO_GLOBAL_CONSTRUCTORS - Success
-- Performing Test CXX_SUPPORTS_WNO_WEAK_VTABLES
-- Performing Test CXX_SUPPORTS_WNO_WEAK_VTABLES - Success
-- Performing Test CXX_SUPPORTS_WNO_DISABLED_MACRO_EXPANSION
-- Performing Test CXX_SUPPORTS_WNO_DISABLED_MACRO_EXPANSION - Success
-- Found Doxygen: /usr/local/bin/doxygen (found version "1.8.14") found components:  doxygen dot 
-- Including ar
-- All libraries and binaries will be installed in /Users/kim/Downloads/ikos-master/install
-- Found Boost: /usr/local/include (found version "1.68.0")
-- Including frontend/llvm
-- All libraries and binaries will be installed in /Users/kim/Downloads/ikos-master/install
-- Found Boost: /usr/local/include (found version "1.68.0")
-- Found the following Boost libraries:
--   filesystem
--   system
-- Found LLVM: /usr/local/Cellar/llvm/7.0.0_1 (found version "7.0.0") 
-- Performing Test LLVM_NO_OLD_LIBSTDCXX
-- Performing Test LLVM_NO_OLD_LIBSTDCXX - Success
-- Performing Test C_SUPPORTS_FPIC
-- Performing Test C_SUPPORTS_FPIC - Success
-- Performing Test CXX_SUPPORTS_FPIC
-- Performing Test CXX_SUPPORTS_FPIC - Success
-- Building with -fPIC
-- Performing Test SUPPORTS_FVISIBILITY_INLINES_HIDDEN_FLAG
-- Performing Test SUPPORTS_FVISIBILITY_INLINES_HIDDEN_FLAG - Success
-- Performing Test C_SUPPORTS_WERROR_DATE_TIME
-- Performing Test C_SUPPORTS_WERROR_DATE_TIME - Success
-- Performing Test CXX_SUPPORTS_WERROR_DATE_TIME
-- Performing Test CXX_SUPPORTS_WERROR_DATE_TIME - Success
-- Performing Test C_SUPPORTS_WERROR_UNGUARDED_AVAILABILITY_NEW
-- Performing Test C_SUPPORTS_WERROR_UNGUARDED_AVAILABILITY_NEW - Success
-- Performing Test CXX_SUPPORTS_WERROR_UNGUARDED_AVAILABILITY_NEW
-- Performing Test CXX_SUPPORTS_WERROR_UNGUARDED_AVAILABILITY_NEW - Success
-- Performing Test CXX_SUPPORTS_CXX11
-- Performing Test CXX_SUPPORTS_CXX11 - Success
-- Linker detection: ld64
-- Including analyzer
-- All libraries and binaries will be installed in /Users/kim/Downloads/ikos-master/install
-- Found Boost: /usr/local/include (found version "1.68.0")
-- Found the following Boost libraries:
--   filesystem
--   system
-- Found SQLite3: /Library/Frameworks/Mono.framework/Headers  
-- Found PythonInterp: /usr/bin/python (found version "2.7.10") 
-- Building with -fPIC
-- Linker detection: ld64
-- Found Clang: /usr/local/Cellar/llvm/7.0.0_1/bin/clang (found version "7.0.0") 
-- Performing Test CXX_SUPPORTS_WNO_UNUSED_LOCAL_TYPEDEFS
-- Performing Test CXX_SUPPORTS_WNO_UNUSED_LOCAL_TYPEDEFS - Success
-- Configuring done
-- Generating done
-- Build files have been written to: /Users/kim/Downloads/ikos-master/build
Delphines-MBP:build kim$ time make -j8
Scanning dependencies of target ikos-python
Scanning dependencies of target ikos-llvm-to-ar
Scanning dependencies of target ikos-pp-lib
Scanning dependencies of target ikos-ar
[  1%] Generating python/ikos/settings/__init__.py
[  1%] Generating python/build/lib/ikos/__init__.py
[  3%] Building CXX object frontend/llvm/CMakeFiles/ikos-pp-lib.dir/src/pass/initialize.cpp.o
[  5%] Building CXX object frontend/llvm/CMakeFiles/ikos-pp-lib.dir/src/pass/lower_cst_expr.cpp.o
[  5%] Building CXX object frontend/llvm/CMakeFiles/ikos-pp-lib.dir/src/pass/mark_internal_inline.cpp.o
[  5%] Building CXX object frontend/llvm/CMakeFiles/ikos-pp-lib.dir/src/pass/lower_select.cpp.o
[  6%] Building CXX object frontend/llvm/CMakeFiles/ikos-pp-lib.dir/src/pass/mark_no_return_function.cpp.o
[  6%] Built target ikos-python
[  6%] Building CXX object frontend/llvm/CMakeFiles/ikos-pp-lib.dir/src/pass/name_values.cpp.o
[  8%] Building CXX object frontend/llvm/CMakeFiles/ikos-llvm-to-ar.dir/src/import/bundle.cpp.o
[ 10%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/format/dot.cpp.o
[ 10%] Building CXX object frontend/llvm/CMakeFiles/ikos-llvm-to-ar.dir/src/import/constant.cpp.o
[ 10%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/format/namer.cpp.o
[ 11%] Building CXX object frontend/llvm/CMakeFiles/ikos-llvm-to-ar.dir/src/import/data_layout.cpp.o
[ 13%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/format/text.cpp.o
[ 13%] Building CXX object frontend/llvm/CMakeFiles/ikos-llvm-to-ar.dir/src/import/exception.cpp.o
[ 15%] Building CXX object frontend/llvm/CMakeFiles/ikos-pp-lib.dir/src/pass/remove_printf_calls.cpp.o
[ 15%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/pass/add_loop_counters.cpp.o
[ 15%] Building CXX object frontend/llvm/CMakeFiles/ikos-pp-lib.dir/src/pass/remove_unreachable_blocks.cpp.o
[ 16%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/pass/name_values.cpp.o
[ 18%] Building CXX object frontend/llvm/CMakeFiles/ikos-llvm-to-ar.dir/src/import/function.cpp.o
[ 18%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/pass/pass.cpp.o
[ 20%] Linking CXX static library libikos-pp.a
[ 20%] Building CXX object frontend/llvm/CMakeFiles/ikos-llvm-to-ar.dir/src/import/importer.cpp.o
[ 20%] Built target ikos-pp-lib
[ 21%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/pass/simplify_cfg.cpp.o
[ 23%] Building CXX object frontend/llvm/CMakeFiles/ikos-llvm-to-ar.dir/src/import/library_function.cpp.o
Scanning dependencies of target ikos-pp
[ 23%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/pass/unify_exit_nodes.cpp.o
[ 25%] Building CXX object frontend/llvm/CMakeFiles/ikos-pp.dir/src/ikos_pp.cpp.o
[ 25%] Building CXX object frontend/llvm/CMakeFiles/ikos-llvm-to-ar.dir/src/import/source_location.cpp.o
[ 26%] Building CXX object frontend/llvm/CMakeFiles/ikos-llvm-to-ar.dir/src/import/type.cpp.o
[ 28%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/pass/simplify_upcast_comparison.cpp.o
[ 28%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/bundle.cpp.o
[ 30%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/code.cpp.o
[ 30%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/context.cpp.o
[ 31%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/context_impl.cpp.o
[ 31%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/data_layout.cpp.o
[ 33%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/function.cpp.o
[ 33%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/intrinsic.cpp.o
[ 35%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/statement.cpp.o
[ 35%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/type.cpp.o
[ 35%] Linking CXX executable ikos-pp
[ 36%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/semantic/value.cpp.o
[ 36%] Built target ikos-pp
[ 36%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/verify/frontend.cpp.o
[ 38%] Building CXX object ar/CMakeFiles/ikos-ar.dir/src/verify/type.cpp.o
[ 38%] Linking CXX static library libikos-llvm-to-ar.a
[ 38%] Built target ikos-llvm-to-ar
[ 38%] Linking CXX static library libikos-ar.a
[ 38%] Built target ikos-ar
Scanning dependencies of target ikos-import
Scanning dependencies of target ikos-analyzer
[ 40%] Building CXX object frontend/llvm/CMakeFiles/ikos-import.dir/src/ikos_import.cpp.o
[ 40%] Building CXX object analyzer/CMakeFiles/ikos-analyzer.dir/src/analysis/call_context.cpp.o
[ 41%] Building CXX object analyzer/CMakeFiles/ikos-analyzer.dir/src/ikos_analyzer.cpp.o
[ 43%] Building CXX object analyzer/CMakeFiles/ikos-analyzer.dir/src/analysis/fixpoint_profile.cpp.o
[ 43%] Building CXX object analyzer/CMakeFiles/ikos-analyzer.dir/src/analysis/hardware_addresses.cpp.o
[ 45%] Building CXX object analyzer/CMakeFiles/ikos-analyzer.dir/src/analysis/literal.cpp.o
[ 45%] Building CXX object analyzer/CMakeFiles/ikos-analyzer.dir/src/analysis/liveness.cpp.o
[ 46%] Building CXX object analyzer/CMakeFiles/ikos-analyzer.dir/src/analysis/memory_location.cpp.o
/Users/kim/Downloads/ikos-master/analyzer/src/analysis/call_context.cpp:60:16: error: no member named 'try_emplace' in 'llvm::DenseMap<std::__1::pair<ikos::analyzer::CallContext *,
      ikos::ar::CallBase *>, std::__1::unique_ptr<ikos::analyzer::CallContext, std::__1::default_delete<ikos::analyzer::CallContext> >,
      llvm::DenseMapInfo<std::__1::pair<ikos::analyzer::CallContext *, ikos::ar::CallBase *> > >'
    this->_map.try_emplace({parent, call},
    ~~~~~~~~~~ ^
1 error generated.
make[2]: *** [analyzer/CMakeFiles/ikos-analyzer.dir/src/analysis/call_context.cpp.o] Error 1
make[2]: *** Waiting for unfinished jobs....
In file included from /Users/kim/Downloads/ikos-master/analyzer/src/analysis/memory_location.cpp:47:
In file included from /Users/kim/Downloads/ikos-master/analyzer/include/ikos/analyzer/util/source_location.hpp:50:
In file included from /Users/kim/Downloads/ikos-master/frontend/llvm/include/ikos/frontend/llvm/import/source_location.hpp:50:
In file included from /usr/local/Cellar/llvm/7.0.0_1/include/llvm/IR/DebugInfoMetadata.h:26:
In file included from /usr/local/Cellar/llvm/7.0.0_1/include/llvm/BinaryFormat/Dwarf.h:28:
/usr/local/Cellar/llvm/7.0.0_1/include/llvm/Support/FormatVariadicDetails.h:66:20: error: no template named 'SameType'
  static char test(SameType<Signature_format, &U::format> *);
                   ^
In file included from /Users/kim/Downloads/ikos-master/analyzer/src/analysis/memory_location.cpp:47:
In file included from /Users/kim/Downloads/ikos-master/analyzer/include/ikos/analyzer/util/source_location.hpp:50:
In file included from /Users/kim/Downloads/ikos-master/frontend/llvm/include/ikos/frontend/llvm/import/source_location.hpp:50:
/usr/local/Cellar/llvm/7.0.0_1/include/llvm/IR/DebugInfoMetadata.h:72:9: error: unknown type name 'Metadata'
  const Metadata *MD = nullptr;
        ^
/usr/local/Cellar/llvm/7.0.0_1/include/llvm/IR/DebugInfoMetadata.h:79:33: error: unknown type name 'Metadata'
  explicit TypedDINodeRef(const Metadata *MD) : MD(MD) {
                                ^
/usr/local/Cellar/llvm/7.0.0_1/include/llvm/IR/DebugInfoMetadata.h:90:12: error: unknown type name 'Metadata'
  operator Metadata *() const { return const_cast<Metadata *>(MD); }
           ^
/usr/local/Cellar/llvm/7.0.0_1/include/llvm/IR/DebugInfoMetadata.h:98:34: error: unknown type name 'DINode'; did you mean 'MDNode'?
using DINodeRef = TypedDINodeRef<DINode>;
                                 ^
/Library/Frameworks/Mono.framework/Headers/llvm/IR/Metadata.h:126:7: note: 'MDNode' declared here
class MDNode : public Value, public FoldingSetNode {
      ^
In file included from /Users/kim/Downloads/ikos-master/analyzer/src/analysis/memory_location.cpp:47:
In file included from /Users/kim/Downloads/ikos-master/analyzer/include/ikos/analyzer/util/source_location.hpp:50:
In file included from /Users/kim/Downloads/ikos-master/frontend/llvm/include/ikos/frontend/llvm/import/source_location.hpp:50:
/usr/local/Cellar/llvm/7.0.0_1/include/llvm/IR/DebugInfoMetadata.h:99:35: error: use of undeclared identifier 'DIScope'
using DIScopeRef = TypedDINodeRef<DIScope>;
...

imprecise on simple example, missing dead code

On the following source code:

#include <stdlib.h>

int main() {
    int* p = 0;
    int a = 20;
    if (a > 30) {
        free(p);
        a = 10;
    }
    return 0;
}

IKOS reports:

[*] Compiling test.c
[*] Running ikos preprocessor
[*] Running ikos analyzer
[!] ikos was compiled in debug mode, the analysis might be slow
[*] Translating LLVM bitcode to AR
[*] Running liveness analysis
[*] Running fixpoint profile analysis
[*] Running interprocedural value analysis
[*] Analyzing entry point: main
[*] Checking properties and writing results for entry point: main

# Time stats:
clang        : 0.172 sec
ikos-analyzer: 0.063 sec
ikos-pp      : 0.052 sec

# Summary:
Total number of checks                : 3
Total number of unreachable checks    : 0
Total number of safe checks           : 3
Total number of definite unsafe checks: 0
Total number of warnings              : 0

The program is SAFE

# Results
No entries.

It should report a dead code instead.

After some investigation, the code is rewrote by llvm into:

if (20>30) {
   free(null);
}

And for some reason, IKOS does not implement the comparison between 2 constants,
see

ikos/analyzer/include/ikos/analyzer/analysis/execution_engine/numerical.hpp

Line 1450 in 31df51c

// TODO(marthaud): check if `left pred right` for MachineInt

Please respect the standard cmake BUILD_SHARED_LIBS variable

Currently you install static libraries:

lib/libikos-ar.a
lib/libikos-llvm-to-ar.a
lib/libikos-pp.a

Error on a pointer to integer cast required by Windows ABI

ikos erroneously emits a definite unsafe check when a std::vector iterator to the beginning of the vector is dereferenced.

Minimal working example:

#include <vector>

struct MyStruct
{
    int i;
};

int main(int argc, char * argv[])
{
    std::vector<MyStruct> v;
    v.resize(1);

    MyStruct s = *v.begin();

    return 0;
}

Output:

../../../test-vector-iterator.cpp: In function 'main':
../../../test-vector-iterator.cpp:14:15: error: invalid memory access
        MyStruct s = *v.begin();
                     ^

System:

MSYS2

Version:

$ ./ikos --version
ikos 2.1

Problem running tests for ikos

I was trying to run regression testsuite for ikos but all of them failed. Probably because some configurations are missing. I'm unable to find what is the right configuration/environment variable setting before running the tests.

my build configs are as follows:

SRC=~/work/ikos
BUILD=$SRC/build
cd $BUILD

export PATH=/usr/local/opt/llvm@4/bin:$PATH
cmake -GNinja ..

I'm working on macbook.

Assertion failed: ((x.bit_width() == y.bit_width()) && ("parameters have a different bit-width")), function assert_compatible

Version 2.1 breaks on FreeBSD 11.2 amd64 with llvm-70:

$  ikos loop.c
[*] 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
[*] Running liveness analysis
[*] Running fixpoint profile analysis
[*] Running interprocedural value analysis
[*] Analyzing entry point: main
[*] Checking properties and writing results for entry point: main
Assertion failed: ((x.bit_width() == y.bit_width()) && ("parameters have a different bit-width")), function assert_compatible, file /usr/ports/devel/ikos/work/ikos-2.1/core/include/ikos/core/number/compatibility.hpp, line 61.
0  ikos-analyzer 0x0000000000ab9a18 llvm::raw_null_ostream::~raw_null_ostream() + 106104
1  ikos-analyzer 0x0000000000ab7cb7 llvm::raw_null_ostream::~raw_null_ostream() + 98583
2  ikos-analyzer 0x0000000000aba022 llvm::raw_null_ostream::~raw_null_ostream() + 107650
3  libthr.so.3   0x0000000802662d66 pthread_sigmask + 1334
4  libthr.so.3   0x00000008026622d2 pthread_getspecific + 3602
Stack dump:
0.	Program arguments: /usr/local/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 -allow-dbg-mismatch -display-checks=no -display-inv=no -color=auto -log=info /tmp/ikos-X2FvAl/loop.pp.bc -o output.db 
ikos: error: exited with signal SIGIOT

Line numbers in warnings do not match source

Hi guys,

For some of the projects I am scanning, warning line numbers do not match the source code. As an example, I can get a warning for line 465 in a file with less than 250 lines of code. Or the warning will be several lines below the stuff it warns about.

Here is an example: http://www.rowdy.dk/pics/warning.png
(the code shown is a part of STM32 standard peripheral library from STMicroelectronics for an ARM Cortex-M3 CPU)

My work-flow is this:
I run clang over each .c file and finish with llvm-link to create a single file called whole_program.bc, which I then pass to IKOS.

I assume IKOS gets line numbers from the LLVM bitcode, so it sounds like a problem with the LLVM-part of the toolchain. What do you think?

I tried using the wllvm-wrapper, but it doesn't change anything.

Do you have any good ideas for how to debug this issue?

nasa-sw-vnv / ikos Goto Github PK

ikos's People

Contributors

Stargazers

Watchers

Forkers

ikos's Issues

Minimal working example:

System:

Version:

Development Environment

Error Message

Minimal working example:

Output:

System:

Version:

Minimal working example:

Output:

System:

Version:

Minimal working example:

Output:

System:

Version:

Minimal working example:

Output:

System:

Version:

Minimal working example:

Output:

System:

Version:

Minimal working example:

Output:

System:

Version:

Minimal working example:

Output:

System:

Version:

Minimal working example:

Output:

System:

Version:

Recommend Projects

Recommend Topics

Recommend Org