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

IKOS

Build Status License Release

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

Introduction

IKOS started as a C++ library designed to facilitate the development of sound static analyzers based on Abstract Interpretation. Specialization of a static analyzer for an application or family of applications is critical for achieving both precision and scalability. Developing such an analyzer is arduous and requires significant expertise in Abstract Interpretation.

IKOS provides a generic and efficient implementation of state-of-the-art Abstract Interpretation data structures and algorithms, such as control-flow graphs, fixpoint iterators, numerical abstract domains, etc. IKOS is independent of a particular programming language.

IKOS also provides a C and C++ static analyzer based on LLVM. It implements scalable analyses for detecting and proving the absence of runtime errors in C and C++ programs.

License

IKOS has been released under the NASA Open Source Agreement version 1.3, see LICENSE.pdf

Contact

[email protected]

Release notes

See RELEASE_NOTES.md

Troubleshooting

See TROUBLESHOOTING.md

Installation

Dependencies

To build and run the analyzer, you will need the following dependencies:

  • A C++ compiler that supports C++14 (gcc >= 4.9.2 or clang >= 3.4)
  • CMake >= 3.4.3
  • GMP >= 4.3.1
  • Boost >= 1.55
  • Python 2 >= 2.7.3 or Python 3 >= 3.3
  • SQLite >= 3.6.20
  • TBB >= 2
  • LLVM and Clang 9.0.x
  • (Optional) APRON >= 0.9.10
  • (Optional) Pygments

Most of them can be installed using your package manager.

Installation instructions for Arch Linux, CentOS, Debian, Fedora, Mac OS X, Red Hat, Ubuntu and Windows are available in the doc/install directory. These instructions assume you have sudo or root access. If you don't, please follow the instructions in doc/install/ROOTLESS.md.

Note: If you build LLVM from source, you need to enable run-time type information (RTTI).

Once you have all the required dependencies, move to the next section.

Build and Install

Now that you have all the dependencies on your system, you can build and install IKOS.

As you open the IKOS distribution, you shall see the following directory structure:

.
├── CMakeLists.txt
├── LICENSE.pdf
├── README.md
├── RELEASE_NOTES.md
├── TROUBLESHOOTING.md
├── analyzer
├── ar
├── cmake
├── core
├── doc
├── frontend
├── script
└── test

IKOS uses the CMake build system. You will need to specify an installation directory that will contain all the binaries, libraries and headers after installation. If you do not specify this directory, CMake will install everything under install in the root directory of the distribution. In the following steps, we will install IKOS under /path/to/ikos-install-directory.

Here are the steps to build and install IKOS:

$ mkdir build
$ cd build
$ cmake -DCMAKE_INSTALL_PREFIX=/path/to/ikos-install-directory ..
$ make
$ make install

Then, add IKOS in your PATH (consider adding this in your .bashrc):

$ PATH="/path/to/ikos-install-directory/bin:$PATH"

Tests

To build and run the tests, simply type:

$ make check

How to run IKOS

Suppose we want to analyze the following C program in a file, called loop.c:

 1: #include <stdio.h>
 2: int a[10];
 3: int main(int argc, char *argv[]) {
 4:     size_t i = 0;
 5:     for (;i < 10; i++) {
 6:         a[i] = i;
 7:     }
 8:     a[i] = i;
 9:     printf("%i", a[i]);
10: }

To analyze this program with IKOS, simply run:

$ ikos loop.c

You shall see the following output. IKOS reports two occurrences of buffer overflow at line 8 and 9.

[*] Compiling loop.c
[*] Running ikos preprocessor
[*] Running ikos analyzer
[*] Translating LLVM bitcode to AR
[*] Running liveness analysis
[*] Running widening hint analysis
[*] Running interprocedural value analysis
[*] Analyzing entry point 'main'
[*] Checking properties for entry point 'main'

# Time stats:
clang        : 0.037 sec
ikos-analyzer: 0.023 sec
ikos-pp      : 0.007 sec

# Summary:
Total number of checks                : 7
Total number of unreachable checks    : 0
Total number of safe checks           : 5
Total number of definite unsafe checks: 2
Total number of warnings              : 0

The program is definitely UNSAFE

# Results
loop.c: In function 'main':
loop.c:8:10: error: buffer overflow, trying to access index 10 of global variable 'a' of 10 elements
    a[i] = i;
         ^
loop.c: In function 'main':
loop.c:9:18: error: buffer overflow, trying to access index 10 of global variable 'a' of 10 elements
    printf("%i", a[i]);
                 ^

The ikos command takes a source file (.c, .cpp) or a LLVM bitcode file (.bc) as input, analyzes it to find runtime errors (also called undefined behaviors), creates a result database output.db in the current working directory and prints a report.

In the report, each line has one of the following status:

  • safe: the statement is proven safe;
  • error: the statement always results into an error (or is unreachable);
  • unreachable: the statement is never executed;
  • warning may mean three things:
    1. the statement results into an error for some executions, or
    2. the static analyzer did not have enough information to conclude (check dependent on an external input, for instance), or
    3. the static analyzer was not powerful enough to prove the absence of errors;

By default, ikos shows warnings and errors directly in your terminal, like a compiler would do.

If the analysis report is too big, you shall use:

  • ikos-report output.db to examine the report in your terminal
  • ikos-view output.db to examine the report in a web interface

Further information:

Contributors

See CONTRIBUTORS.md

Publications

  • Sung Kook Kim, Arnaud J. Venet, Aditya V. Thakur. Deterministic Parallel Fixpoint Computation. In Principles of Programming Languages (POPL 2020), New Orleans, Louisiana (PDF).

  • Guillaume Brat, Jorge Navas, Nija Shi and Arnaud Venet. IKOS: a Framework for Static Analysis based on Abstract Interpretation. In Proceedings of the International Conference on Software Engineering and Formal Methods (SEFM 2014), Grenoble, France (PDF).

  • Arnaud Venet. The Gauge Domain: Scalable Analysis of Linear Inequality Invariants. In Proceedings of Computer Aided Verification (CAV 2012), Berkeley, California, USA 2012. Lecture Notes in Computer Science, pages 139-154, volume 7358, Springer 2012 (PDF).

Coding Standards

See doc/CODING_STANDARDS.md

Overview of the source code

See doc/OVERVIEW.md

Owner
NASA - Software V&V
NASA - Software Verification and Validation
NASA - Software V&V
Comments
  • Questions about the algorithm of the analysis

    Questions about the algorithm of the analysis

    Code: #include <stdio.h>

    int a = 100; int size = 16; char array1[16];

    int fun(int x) { int y=0; if (x < size) { y = array1[x]; } return y; }

    int main() { fun(a); return 0; }

    I tried to stop the liveness analysis by ikos --no-liveness test.c But still got the warning unreachable: code is dead y = array1[x]; ^ I want to see if ikos can give the buffer overflow warning if I can stop the liveness analysis.

    Please tell me how I can get the buffer overflow warning from this c code from ikos.

  • ikos-analyzer stuck and/or running out of memory

    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.

  • ikos-scan fails: error: unknown argument: '-faddrsig'

    ikos-scan fails: error: unknown argument: '-faddrsig'

    ikos fails on a very simple C++ make project:

    $ ikos-scan make 
    ikos-scan-c++ -O2 -c tsne.cpp
    error: unknown argument: '-faddrsig'
    *** Error code 1
    

    FreeBSD 11.2 amd64

    -faddrsig doesn't appear in the Makefile.

  • Crashed on my codebase

    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.

  • Header files not found

    Header files not found

    When I try running the example loop.c code in the Readme,

    #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]);
    }
    

    I receive the following error:

    $ ikos loop.c
    [*] Compiling loop.c
    loop.c:1:10: fatal error: 'stdio.h' file not found
    #include <stdio.h>
             ^~~~~~~~~
    1 error generated.
    ikos: error while compiling loop.c, abort.
    

    Is there any argument in ikos that we can attach header files (if this is the problem)? Thanks.

  • Detect dynamic uninitialized variables with debug info optional

    Detect dynamic uninitialized variables with debug info optional

    1. Fix a problem in the tracking of the values of dynamically-allocated memory so that use of uninitialized dynamically-allocated memory is detected.

    2. Allow analysis of programs without debug information. This is important for the case where the LLVM comes from a binary lifter where no debug information may be available. Without debug information the name of the function with a problem is reported but file and line number information is not available.

  • Failed to get it working

    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:

    1. The first error message is from brew install.
    2. 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/[email protected]/bin/clang++ CC=/usr/local/opt/[email protected]/bin/clang cmake .. -DLLVM_CONFIG_EXECUTABLE="$(brew --prefix)/opt/[email protected]/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/[email protected]/bin/clang
    -- Check for working C compiler: /usr/local/opt/[email protected]/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/[email protected]/bin/clang++
    -- Check for working CXX compiler: /usr/local/opt/[email protected]/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>;
    ...
    
  • Problem with narrowing strategy for nonmonotonic transformation function

    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.

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

    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)

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

    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? :-)

  • Remove mention of AUR helpers

    Remove mention of AUR helpers

    AUR helpers are fully unsupported by the Arch Linux development team. Besides my statement as a Trusted User, see the following links:

    https://bbs.archlinux.org/viewtopic.php?pid=828310#p828310 https://wiki.archlinux.org/index.php/AUR_helpers https://bugs.archlinux.org/task/56602#comment164090

    Besides these considerations, the AUR itself has in 2015 adopted git, making these helpers for simple tasks such as these (one package and one dependency) obsolete. Users can easily keep track of updates by enabling email notifications on the AUR website.

  • Add tracing of invariants, triples optional

    Add tracing of invariants, triples optional

    1. Adds option to trace the invariant during analysis.

    The ikos python script option is "--trace-ar-stmts". The ikos-analyzer option is "-trace-ar-stmts".

    1. According to the LLVM reference manual, the target triple is optional. So no longer fail is it is not present.
  • Type checker error translating LLVM bitcode to AR

    Type checker error translating LLVM bitcode to AR

    I attempted to analyze Blender with IKOS. It fails during the "Translating LLVM bitcode to AR" step with the following errors:

    /home/dev/01-data/02-software/ikos-install/bin/ikos -a=nullity blender.bc
    [*] Running ikos preprocessor
    [*] Running ikos analyzer
    [*] Translating LLVM bitcode to AR
    error: left operand of statement '%15 folt %19' is not a floating point
    error: left operand of statement '%15 fuge %19' is not a floating point
    error: result of statement '<4 x si32> %21 = sext %20' is not a signed integer
    error: result of statement '<4 x float> %52 = sitofp %51' is not a floating point
    [...]
    ikos-analyzer: /tmp/ikos-aa2ksdqm/blender.pp.bc: error: type checker
    ikos: error: a run-time error occurred
    

    Please let me know if you need any additional information.

  • Consider migrating from Travis to another CI system such as GitHub Actions

    Consider migrating from Travis to another CI system such as GitHub Actions

    This repo still has a .travis.yml and a Travis CI status badge (showing an error) in the README, but since Travis stopped supporting open-source projects a while ago, the last time a build ran on this repo was about a year ago: https://travis-ci.org/github/NASA-SW-VnV/ikos

    Please consider migrating to GitHub Actions (docs) (since it's provided by GitHub and is free for open-source projects, so it's easy to set up) or another CI system of your choice, as currently, no CI is running on PRs for this project.

    FWIW, I'm not affiliated with either Travis or GitHub.

  • Generating a .egg file

    Generating a .egg file

    To be compatible with easy_install, it would be nice to have the build process generate the final .egg file (and not just the egg-info directory). Otherwise, I'm having to zip the contents of the directory into a .egg file before installing.

  • error while preprocessing llvm bitcode

    error while preprocessing llvm bitcode

    running yes | ikos-scan -q make -j4 -e --file=Makefile CFLAGS='-g -O0' on bwa results in the following error, even with using advice from #4:

    Analyze bwa? [Y/n] We only lower a select if the flag is Boolean.
    *** stack smashing detected ***: terminated
    Stack dump:
    0.	Program arguments: /opt/ikos/bin/ikos-pp -opt=basic -entry-points=main bwa.bc -o /tmp/ikos-C8a7r8/bwa.pp.bc 
    1.	Running pass 'Function Pass Manager' on module 'bwa.bc'.
    2.	Running pass 'Lower select instructions to branches' on function '@ksw_u8'
    /opt/ikos/bin/ikos-pp(+0xb02b0f)[0x55b00714eb0f]
    /opt/ikos/bin/ikos-pp(+0xb00f20)[0x55b00714cf20]
    /opt/ikos/bin/ikos-pp(+0xb03051)[0x55b00714f051]
    /lib/x86_64-linux-gnu/libpthread.so.0(+0x153c0)[0x7f67655073c0]
    /lib/x86_64-linux-gnu/libc.so.6(gsignal+0xcb)[0x7f6764ff818b]
    /lib/x86_64-linux-gnu/libc.so.6(abort+0x12b)[0x7f6764fd7859]
    /lib/x86_64-linux-gnu/libc.so.6(+0x903ee)[0x7f67650423ee]
    /lib/x86_64-linux-gnu/libc.so.6(__fortify_fail+0x2a)[0x7f67650e4b4a]
    /lib/x86_64-linux-gnu/libc.so.6(+0x132b16)[0x7f67650e4b16]
    /opt/ikos/bin/ikos-pp(+0xf44e6)[0x55b0067404e6]
    /opt/ikos/bin/ikos-pp(+0x647136)[0x55b006c93136]
    /opt/ikos/bin/ikos-pp(+0x6473e3)[0x55b006c933e3]
    /opt/ikos/bin/ikos-pp(+0x647890)[0x55b006c93890]
    /opt/ikos/bin/ikos-pp(+0xa73bf)[0x55b0066f33bf]
    /lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3)[0x7f6764fd90b3]
    /opt/ikos/bin/ikos-pp(+0xeebfe)[0x55b00673abfe]
    ikos: error while preprocessing llvm bitcode, abort.
    
  • Uninitialized Function Pointer Results In Safe

    Uninitialized Function Pointer Results In Safe

    Hello,

    I'm messing around with IKOS a bit and had an interesting result with this test case:

    void unsafe() {
        char buffer[10];
        buffer[10] = 0;
    }
    
    void safe() {
    }
    
    int main() {
        void(*func_ptr)();
        func_ptr();
        return 0;
    }
    

    It invokes an uninitialized function pointer, which is unsafe because (of course) it's usually going to jump to unmapped or non executable memory and crash, but also because it could in principle invoke unsafe().

    ./install/bin/ikos my_test_cases/test10.c
    [*] Compiling my_test_cases/test10.c
    my_test_cases/test10.c:3:5: warning: array index 10 is past the end of the array (which contains 10 elements) [-Warray-bounds]
        buffer[10] = 0;
        ^      ~~
    my_test_cases/test10.c:2:5: note: array 'buffer' declared here
        char buffer[10];
        ^
    my_test_cases/test10.c:11:5: warning: variable 'func_ptr' is uninitialized when used here [-Wuninitialized]
        func_ptr();
        ^~~~~~~~
    my_test_cases/test10.c:10:22: note: initialize the variable 'func_ptr' to silence this warning
        void(*func_ptr)();
                         ^
                          = 0
    2 warnings generated.
    [*] Running ikos preprocessor
    [*] Running ikos analyzer
    [*] Translating LLVM bitcode to AR
    [*] Running liveness analysis
    [*] Running widening hint analysis
    [*] Running interprocedural value analysis
    [*] Analyzing entry point 'main'
    [*] Checking properties for entry point 'main'
    
    # Time stats:
    clang        : 0.041 sec
    ikos-analyzer: 0.005 sec
    ikos-pp      : 0.003 sec
    
    # Summary:
    Total number of checks                : 0
    Total number of unreachable checks    : 0
    Total number of safe checks           : 0
    Total number of definite unsafe checks: 0
    Total number of warnings              : 0
    
    The program is SAFE
    
    # Results
    No entries.
    

    There are some warnings from Clang, but none from IKOS. I also noticed it didn't actually run any checks. I'm not sure if this has something to do with uninitialized values not being modeled the way I'd expect, or maybe how IKOS handles control flow and indirection, or maybe this is just violating other IKOS assumptions.

Qt-oriented static code analyzer based on the Clang framework

WARNING: master is the development branch. Please use the v1.10 branch. clazy v1.11 clazy is a compiler plugin which allows clang to understand Qt sem

Jun 22, 2022
A static analyzer for Java, C, C++, and Objective-C
A static analyzer for Java, C, C++, and Objective-C

Infer Infer is a static analysis tool for Java, C++, Objective-C, and C. Infer is written in OCaml. Installation Read our Getting Started page for det

Jun 17, 2022
Static code checker for C++

cpplint - static code checker for C++ Cpplint is a command-line tool to check C/C++ files for style issues following Google's C++ style guide. Cpplint

Jun 21, 2022
Pharos Static Binary Analysis Framework

Automated static analysis tools for binary programs

Jun 22, 2022
CITL's static analysis engine for native code artifacts

citl-static-analyzer Fast binary hardening analysis tooling. Building on Linux The build process varies by Linux distribution, owing to differences be

Feb 14, 2022
ELF static analysis and injection framework that parse, manipulate and camouflage ELF files.

elfspirit elfspirit is a useful program that parse, manipulate and camouflage ELF files. It provides a variety of functions, including adding or delet

Jun 15, 2022
A static analysis tool that helps security researchers scan a list of Windows kernel drivers for common vulnerability patterns in drivers (CVE makers!)
A static analysis tool that helps security researchers scan a list of Windows kernel drivers for common vulnerability patterns in drivers (CVE makers!)

Driver Analyzer A static analysis tool that helps security researchers scan a list of Windows kernel drivers for common vulnerability patterns in driv

Jun 13, 2022
Static analysis of C/C++ code

Cppcheck GitHub Actions Linux Build Status Windows Build Status OSS-Fuzz Coverity Scan Build Status License About the name The original name of this p

Jun 22, 2022
Static analyzer for C/C++ based on the theory of Abstract Interpretation.

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

Jun 13, 2022
Legacy stepper motor analyzer - A DYI minimalist hardware stepper motor analyzer with graphical touch screen.
Legacy stepper motor analyzer - A DYI minimalist hardware stepper motor analyzer with graphical touch screen.

Simple Stepper Motor Analyzer NOTE: This is the legacy STM32 based design which was replaced by the single board, Raspberry Pi Pico design at https://

Mar 21, 2022
✔️The smallest header-only GUI library(4 KLOC) for all platforms
✔️The smallest header-only GUI library(4 KLOC) for all platforms

Welcome to GUI-lite The smallest header-only GUI library (4 KLOC) for all platforms. 中文 Lightweight ✂️ Small: 4,000+ lines of C++ code, zero dependenc

Jun 17, 2022
A LLVM-based static analyzer to produce PyTorch operator dependency graph.

What is this? This is a clone of the deprecated LLVM-based static analyzer from the PyTorch repo, which can be used to produce the PyTorch operator de

Dec 15, 2021
Qt-oriented static code analyzer based on the Clang framework

WARNING: master is the development branch. Please use the v1.10 branch. clazy v1.11 clazy is a compiler plugin which allows clang to understand Qt sem

Jun 22, 2022
A static analyzer for Java, C, C++, and Objective-C
A static analyzer for Java, C, C++, and Objective-C

Infer Infer is a static analysis tool for Java, C++, Objective-C, and C. Infer is written in OCaml. Installation Read our Getting Started page for det

Jun 17, 2022
Yggdrasil Decision Forests (YDF) is a collection of state-of-the-art algorithms for the training, serving and interpretation of Decision Forest models.
Yggdrasil Decision Forests (YDF) is a collection of state-of-the-art algorithms for the training, serving and interpretation of Decision Forest models.

Yggdrasil Decision Forests (YDF) is a collection of state-of-the-art algorithms for the training, serving and interpretation of Decision Forest models. The library is developed in C++ and available in C++, CLI (command-line-interface, i.e. shell commands) and in TensorFlow under the name TensorFlow Decision Forests (TF-DF).

Jun 16, 2022
Based on the spatial resection theory, the algorithm solves the camera position by solving the homography matrix.
Based on the spatial resection theory, the algorithm solves the camera position by solving the homography matrix.

Based on the spatial resection theory, the algorithm solves the camera position by solving the homography matrix.

Nov 13, 2021
Source code for pbrt, the renderer described in the third edition of "Physically Based Rendering: From Theory To Implementation", by Matt Pharr, Wenzel Jakob, and Greg Humphreys.

pbrt, Version 3 This repository holds the source code to the version of pbrt that is described in the third edition of Physically Based Rendering: Fro

Jun 22, 2022
Repository for material related to the Programming Languages Virtual Meetup coverage of the Category Theory for Programmers book.

CTfP-2021 This is the material (code and presentation slide decks) that correspond to the Programming Languages Virtual Meetup course that is covering

Jun 19, 2022
A command line tool for numerically computing Out-of-time-ordered correlations for N=4 supersymmetric Yang-Mills theory and Beta deformed N=4 SYM.

A command line tool to compute OTOC for N=4 supersymmetric Yang–Mills theory This is a command line tool to numerically compute Out-of-time-ordered co

Oct 16, 2021
BSAL(Bluetooth Stack Abstract Layer)软件包是由 RT-Thread 针对不同 蓝牙协议栈接口实现的,目前支持的 协议栈有:nimble,realtek 等协议栈
BSAL(Bluetooth Stack Abstract Layer)软件包是由 RT-Thread 针对不同 蓝牙协议栈接口实现的,目前支持的 协议栈有:nimble,realtek 等协议栈

BSAL (Bluetooth Stack Abstract Layer)软件包是由 RT-Thread 针对不同 蓝牙协议栈接口实现的,目前支持的 协议栈有:nimble,realtek 等协议栈。

May 25, 2022