/dynamite

A dynamic analyzer for proving program termination and non-termination.

Primary LanguageRoff

Dynamite

Installation

  1. Install SageMath from conda (http://doc.sagemath.org/html/en/installation/conda.html)

    wget https://repo.anaconda.com/miniconda/Miniconda2-latest-Linux-x86_64.sh
    sh Miniconda2-latest-Linux-x86_64.sh
    conda config --add channels conda-forge
    conda create -n sage sage=8.8 python=2.7
    
  2. conda activate sage

  3. Install Java 8 from conda:

    conda install -c anaconda openjdk

    conda install openjdk=8.0.192

  4. pip install lark-parser

  5. pip install z3-solver

  6. JavaPathFinder

    mkdir jpf
    cd jpf/
    git clone https://github.com/javapathfinder/jpf-core
    git clone https://github.com/SymbolicPathFinder/jpf-symbc
    mkdir /root/.jpf
    echo 'jpf-core = /jpf/jpf-core' >> /root/.jpf/site.properties
    echo 'jpf-symbc = /jpf/jpf-symbc' >> /root/.jpf/site.properties
    echo 'extensions=${jpf-core},${jpf-symbc}' >> /root/.jpf/site.properties
    cp /dynamo/deps/dig/src/java/InvariantListenerVu.java ../jpf-symbc/src/main/gov/nasa/jpf/symbc/
    cd jpf-core/
    git checkout java-8
    ant
    cd ../jpf-symbc/
    ant
    
  7. ENV

    export JPF_HOME=/jpf
    export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:$JPF_HOME/jpf-symbc/lib
    
  8. LLDB

    conda install -c conda-forge lldb
    

Note

  1. Remove a conda environment: conda env remove --name myenv

  2. Search a conda package: conda search sage --channel conda-forge

  3. Install pip: sudo easy_install pip

  4. LLDB

    breakpoint set --name main
    breakpoint set --func-regex vtrace* # BreakpointCreateByRegex('vtrace*', None)
    run
    expr -i 0 -- mainQ(1, 2)
    frame variable
    
    opt = lldb.SBExpressionOptions()
    opt.SetIgnoreBreakpoints(False)
    v = target.EvaluateExpression('mainQ(1, 2)', opt)
    
    docker run --cap-add=SYS_PTRACE --security-opt seccomp=unconfined --security-opt apparmor=unconfined --name dynamo-dev -it letonchanh/dynamo-dev bash
    
    apt-get install cmake ninja-build build-essential subversion swig libedit-dev libncurses5-dev
    unset PYTHONPATH
    git clone https://github.com/llvm/llvm-project.git
    cd llvm-project
    mkdir build
    cd build
    cmake -G Ninja -DLLVM_ENABLE_PROJECTS="clang;lldb" -DPYTHON_EXECUTABLE="/tools/SageMath/local/bin/python3" -DLLDB_CAN_USE_LLDB_SERVER=True -DCMAKE_INSTALL_PREFIX=/tools/llvm -DCMAKE_BUILD_TYPE=Release ../llvm
    ninja lldb
    ninja lldb-server
    
  5. angr

Support

This work is supported by Office of Naval Research under Grant No.: N00014-17-1-2787.