Shaheen/klee runner for pr

.gitignore

@@ -12,4 +12,5 @@ src/.mypy_cache/
 /src/.coverage
 /src/coverage.xml
 /src/htmlcov/
-/src/.dmypy.json
+/src/.dmypy.json
+/src/klee/lextab.py

Dockerfile

@@ -1,38 +1,39 @@
-FROM python:3.9-slim 
+FROM python:3.9-slim-buster
 WORKDIR /app
-COPY requirements.txt /app/ 
+COPY requirements.txt /app/
 COPY ./examples /app/examples/
-RUN pip install --trusted-host pypi.python.org -r requirements.txt 
+RUN pip install --trusted-host pypi.python.org -r requirements.txt
 RUN mkdir -p /usr/share/man/man1 && apt-get update && apt-get install -y build-essential wget software-properties-common openjdk-11-jdk-headless
-RUN wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key | apt-key add - 
+RUN wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key | apt-key add -
 RUN apt-get update
 
 # Get KLEE dependencies (LLVM 6.0) [http://klee.github.io/build-llvm60/]
 RUN apt-get install -y curl libcap-dev git unzip doxygen libsqlite3-dev libgoogle-perftools-dev libtcmalloc-minimal4 cmake libncurses5-dev
 RUN pip install tabulate
 RUN apt-get install -y clang-6.0 llvm-6.0 llvm-6.0-dev llvm-6.0-tools zsh vim tmux
 RUN apt-get install -y g++-multilib
-# Install z3 
-RUN git clone https://github.com/Z3Prover/z3/ 
-RUN cd /app/z3 && git pull && git reset --hard 2d1684bc2d2621c0d6b02b81168624388648049a 
-RUN cd /app/z3 && python scripts/mk_make.py 
+RUN apt-get install -y libgmp3-dev
+# Install z3
+RUN git clone https://github.com/Z3Prover/z3/
+RUN cd /app/z3 && git pull && git reset --hard 2d1684bc2d2621c0d6b02b81168624388648049a
+RUN cd /app/z3 && python scripts/mk_make.py
 RUN cd /app/z3/build && make && make install
 RUN pip install z3-solver
 
 # Install lit
 RUN pip install lit
 
-# Build uClibc and the POSIX environment model 
+# Build uClibc and the POSIX environment model
 RUN git clone https://github.com/klee/klee-uclibc.git
 RUN ln -s /usr/bin/llvm-config-6.0 /usr/bin/llvm-config
-RUN alias llvm-config=llvm-config-6.0 
+RUN alias llvm-config=llvm-config-6.0
 RUN CC=/usr/bin/clang-6.0 /app/klee-uclibc/configure --make-llvm-lib
 RUN cd /app/klee-uclibc && make -j2
 
 # Get KLEE
 RUN mkdir /app/build
 RUN git clone https://github.com/klee/klee.git
-RUN apt-get install zlib1g-dev
+RUN apt-get install -y zlib1g-dev
 RUN cd /app/build && cmake -DENABLE_SOLVER_STP=OFF -DENABLE_POSIX_RUNTIME=ON -DENABLE_KLEE_UCLIBC=ON -DKLEE_UCLIBC_PATH=/app/klee-uclibc -DENABLE_UNIT_TESTS=OFF -DLLVMCC=/usr/bin/clang-6.0 -ENABLE_ZLIB=OFF -DLLVMCXX=/usr/bin/clang++-6.0 /app/klee
 RUN cd /app/build && make
 
@@ -45,29 +46,29 @@ RUN pip install wllvm
 RUN curl -OL https://github.com/google/googletest/archive/release-1.7.0.zip
 RUN unzip /app/release-1.7.0.zip
 
-# C Parser written in python 
+# C Parser written in python
 RUN pip install pycparser
 RUN git clone https://github.com/eliben/pycparser
 
 ENV PATH "$PATH:/app/build/bin/"
 
-# AFL (Dependency for Kelinci) 
+# AFL (Dependency for Kelinci)
 RUN git clone https://github.com/google/AFL
 
 # Kelinci: https://github.com/isstac/kelinci
 RUN git clone https://github.com/isstac/kelinci
 
-# JQF + Zest 
+# JQF + Zest
 RUN git clone https://github.com/rohanpadhye/jqf
 
-# JPF (Symbolic Java Path Finder): https://github.com/SymbolicPathFinder/jpf-symbc 
-# Refer to https://github.com/SymbolicPathFinder/jpf-symbc/wiki/Documentation 
+# JPF (Symbolic Java Path Finder): https://github.com/SymbolicPathFinder/jpf-symbc
+# Refer to https://github.com/SymbolicPathFinder/jpf-symbc/wiki/Documentation
 RUN git clone https://github.com/javapathfinder/jpf-core
 RUN git clone https://github.com/SymbolicPathFinder/jpf-symbc
-RUN mkdir jpf && mv jpf-core jpf && mv jpf-symbc jpf 
+RUN mkdir jpf && mv jpf-core jpf && mv jpf-symbc jpf
 COPY site.properties /app/jpf/
 
-# PRISM: https://www.prismmodelchecker.org/manual/InstallingPRISM/Instructions#binaries 
+# PRISM: https://www.prismmodelchecker.org/manual/InstallingPRISM/Instructions#binaries
 COPY /dependencies/prism-4.5-linux64.tar.gz /app/
 RUN gunzip prism-4.5-linux64.tar.gz && tar xf prism-4.5-linux64.tar && cd prism-4.5-linux64 && ./install.sh
 

src/experiments/function_calls/data/apc_data.csv

@@ -0,0 +1,3 @@
+,graph_name,apc,apc_time
+0,partition_cfg._Z4swapPiS_,"(1.00000000000000, 1.00000000000000)",0.022338151931762695
+1,partition_cfg._Z9partitionPiii,"('1.1673**n', '1.1477*1.1673**n')",0.3525121212005615

src/experiments/function_calls/data/fcapc_data.csv

@@ -0,0 +1,3 @@
+,graph_name,fcapc,fcapc_time
+0,partition_cfg._Z4swapPiS_,"(1, 1)",0.13048791885375977
+1,partition_cfg._Z9partitionPiii,"(0.723606797748011*1.12783848556**n, 0.886651779312**n*(0.167526046921159 - 0.042537371471034*I) + 0.886651779312**n*(0.167526046921159 + 0.042537371471034*I) + 0.886651779312**n*(-0.0293294458752485 - 0.0661060769196468*I) + 0.886651779312**n*(-0.0293294458752485 + 0.0661060769196468*I) - 0.999999999956541*1.0**n + 0.82202443150234*1.12783848556**n + 1.12783848556**n*(-0.0492088168771647 - 0.0436310850432438*I) + 1.12783848556**n*(-0.0492088168771647 + 0.0436310850432438*I))",1.160919189453125

src/experiments/function_calls/data/final_data.csv

@@ -0,0 +1,3 @@
+,graph_name,apc,rapc,fcapc,getrgfapc,apc_time,rapc_time,fcapc_time,getrgfapc_time,longest for getrgf,longest time,case,gamma
+0,partition_cfg._Z4swapPiS_,"(1.00000000000000, 1.00000000000000)",na,"(1, 1)",1.0**(n + 1),0.022338151931762692,na,0.13048791885375974,0.1591334342956543,gammaTime,0.107,1.0,-T0 + x**3
+1,partition_cfg._Z9partitionPiii,"('1.1673**n', '1.1477*1.1673**n')",na,"(0.723606797748011*1.12783848556**n, 0.886651779312**n*(0.167526046921159 - 0.042537371471034*I) + 0.886651779312**n*(0.167526046921159 + 0.042537371471034*I) + 0.886651779312**n*(-0.0293294458752485 - 0.0661060769196468*I) + 0.886651779312**n*(-0.0293294458752485 + 0.0661060769196468*I) - 0.999999999956541*1.0**n + 0.82202443150234*1.12783848556**n + 1.12783848556**n*(-0.0492088168771647 - 0.0436310850432438*I) + 1.12783848556**n*(-0.0492088168771647 + 0.0436310850432438*I))",0.723606797749937*1.12783848556168**n,0.3525121212005615,na,1.160919189453125,0.42708683013916016,gammaTime,0.203,1.0,-(T0*(x**8 + x**4 - 1) + x**6)/(x**8 + x**4 - 1)

src/experiments/function_calls/data/getrgfapc_data.csv

@@ -0,0 +1,3 @@
+,graph_name,getrgfapc,getrgfapc_time,longest for getrgf,longest time,case,gamma
+0,partition_cfg._Z4swapPiS_,1.0**(n + 1),0.1591334342956543,gammaTime,0.107,1.0,-T0 + x**3
+1,partition_cfg._Z9partitionPiii,0.723606797749937*1.12783848556168**n,0.42708683013916016,gammaTime,0.203,1.0,-(T0*(x**8 + x**4 - 1) + x**6)/(x**8 + x**4 - 1)