Running klee on a C++ program using its Docker image

klee_cpp.sh

#!/usr/bin/env bash
set -euo pipefail

FILE=${1-main.cc}

if [ ! -f "${FILE}" ]
then	
cat << EOF > "${FILE}"
#include <klee/klee.h>
#include <assert.h>

constexpr size_t N = 2;

#include <array>
#include <numeric>
#include <cstdint>

using namespace std;

template<size_t SIZE>
class A {
  public:
    std::array<uint8_t, SIZE> x;
    A() {}
    auto sum()->decltype(std::accumulate(x.begin(), x.end(), 0)) {
        return std::accumulate(x.begin(), x.end(), 0);
    }      
};

int main(int argc, char *argv[])
{
    A<N> a;
    klee_make_symbolic(a.x.data(), N * (sizeof a.x[0]), "x");
    a.x[0] = 1;
    auto inc = [](uint8_t y)->uint8_t { return y + 1; };
    klee_assert(a.sum() != inc(0));
    return 0;
}
EOF
fi

KLEE_IMAGE="klee/klee:2.0"
docker pull "${KLEE_IMAGE}"
RUN="docker run -v $(pwd):$(pwd) --rm ${KLEE_IMAGE}"

CLANG_BIN=/tmp/llvm-60-install_O_D_A/bin
CLANGXX="${RUN} ${CLANG_BIN}/clang++"

KLEE_INCLUDE=/home/klee/klee_src/include
KLEE_BUILD=/home/klee/klee_build
KLEE_BIN="${KLEE_BUILD}/bin"

KLEE="${RUN} ${KLEE_BIN}/klee"
KTEST="${RUN} ${KLEE_BIN}/ktest-tool"

${CLANGXX} -std=c++11 -g -emit-llvm -I"${KLEE_INCLUDE}" -c "$(pwd)/${FILE}" -o "$(pwd)/${FILE%%.*}.bc"

${KLEE} "$(pwd)/${FILE%%.*}.bc"

ERROR_FILE="$(basename "$(find -L klee-last -name '*.assert.err')")"

${KTEST} "$(pwd)/klee-last/${ERROR_FILE%%.*}.ktest"