diff options
| -rw-r--r-- | .travis.yml | 28 | ||||
| -rwxr-xr-x | .travis/klee.sh | 36 | ||||
| -rw-r--r-- | Dockerfile | 1 | ||||
| -rw-r--r-- | lib/Solver/CexCachingSolver.cpp | 15 | ||||
| -rw-r--r-- | scripts/coverageServer.py | 100 |
5 files changed, 167 insertions, 13 deletions
diff --git a/.travis.yml b/.travis.yml index c971a801..1979f1ef 100644 --- a/.travis.yml +++ b/.travis.yml @@ -23,23 +23,31 @@ env: # UCLIBC: {ENABLED, DISABLED} # with Asserts enabled. + # COVERAGE set indicated that coverage data should be uplaoded to the server, only ONE job should have COVERAGE set + # FIXME: Enable when we want to test LLVM3.5 + matrix: #- LLVM_VERSION=3.5 STP_VERSION=UPSTREAM KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 #- LLVM_VERSION=3.5 STP_VERSION=UPSTREAM KLEE_UCLIBC=1 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 - - LLVM_VERSION=3.4 STP_VERSION=UPSTREAM KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 - - LLVM_VERSION=3.4 STP_VERSION=UPSTREAM KLEE_UCLIBC=1 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 - - LLVM_VERSION=2.9 STP_VERSION=UPSTREAM KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 - - LLVM_VERSION=2.9 STP_VERSION=UPSTREAM KLEE_UCLIBC=1 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 - - LLVM_VERSION=3.4 STP_VERSION=r940 KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 - - LLVM_VERSION=3.4 STP_VERSION=r940 KLEE_UCLIBC=1 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 - - LLVM_VERSION=2.9 STP_VERSION=r940 KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 - - LLVM_VERSION=2.9 STP_VERSION=r940 KLEE_UCLIBC=1 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 + - LLVM_VERSION=3.4 STP_VERSION=UPSTREAM KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=1 + - LLVM_VERSION=3.4 STP_VERSION=UPSTREAM KLEE_UCLIBC=1 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 + - LLVM_VERSION=2.9 STP_VERSION=UPSTREAM KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 + - LLVM_VERSION=2.9 STP_VERSION=UPSTREAM KLEE_UCLIBC=1 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 + - LLVM_VERSION=3.4 STP_VERSION=r940 KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 + - LLVM_VERSION=3.4 STP_VERSION=r940 KLEE_UCLIBC=1 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 + - LLVM_VERSION=2.9 STP_VERSION=r940 KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 + - LLVM_VERSION=2.9 STP_VERSION=r940 KLEE_UCLIBC=1 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 # Check at least one build with Asserts disabled. - - LLVM_VERSION=2.9 STP_VERSION=r940 KLEE_UCLIBC=1 DISABLE_ASSERTIONS=1 ENABLE_OPTIMIZED=1 + - LLVM_VERSION=2.9 STP_VERSION=r940 KLEE_UCLIBC=1 DISABLE_ASSERTIONS=1 ENABLE_OPTIMIZED=1 COVERAGE=0 # Check at least one Debug+Asserts build - - LLVM_VERSION=3.4 STP_VERSION=UPSTREAM KLEE_UCLIBC=1 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=0 + - LLVM_VERSION=3.4 STP_VERSION=UPSTREAM KLEE_UCLIBC=1 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=0 COVERAGE=0 + global: + - secure: EF/WAc4BdIRUchF3mjATN3/UwtGWtGaRgb5oIIJHjKhgZFdPsgWsXFgaOB0jaK2hfO/svj/LvlasuRIGxeePVjeaiX8ZlVpuHiX67vdYLY+0kCDRwkusRjm60/GbPU9O/Xjgb/d4aWAEkoq5OnsprVTEvU8iY2JHtAqgwR+wW9I= + - secure: Hrp1MRSxDUH2GTQg3QR/yUttY/3KmgbFb5e+zyy551dKpHjxJdsNe8bquY9oFoT7KmPQYl0HNNjEv4qWW8RK+HWHOCB55nL1KlGpOG7vAJcUEZg7ScbliGgiovMB6jIQVfeP9FhYngfc13vNZQ5PGlqzfSsHSAbvkwEogBToHVw= + - secure: DQAEQWJblXvIztN/sgH63OtFncI+Qju6wRy1zIV/iLf5KbAmLs1h3itU7EsE/+3+LgV1MVQ5QNJDBUj17A6VHRKNaQ5qnIllTAcC3o0nPDohQkQoCgDG8HZ+M4wtVfr7q2K6byEPB2UbSH+mEjSMTihJufgBBVfKyyozAfYycjg= + cache: apt before_install: ########################################################################### diff --git a/.travis/klee.sh b/.travis/klee.sh index 3106dca9..3008c7fb 100755 --- a/.travis/klee.sh +++ b/.travis/klee.sh @@ -39,6 +39,10 @@ else KLEE_UCLIBC_CONFIGURE_OPTION="" fi +COVERAGE_FLAGS="" +if [ ${COVERAGE} -eq 1 ]; then + COVERAGE_FLAGS='-fprofile-arcs -ftest-coverage' +fi ############################################################################### # KLEE ############################################################################### @@ -55,6 +59,7 @@ ${KLEE_SRC}/configure --with-llvmsrc=/usr/lib/llvm-${LLVM_VERSION}/build \ --with-llvmcxx=${KLEE_CXX} \ --with-stp="${BUILD_DIR}/stp/build" \ ${KLEE_UCLIBC_CONFIGURE_OPTION} \ + CXXFLAGS="${COVERAGE_FLAGS}" \ && make DISABLE_ASSERTIONS=${DISABLE_ASSERTIONS} \ ENABLE_OPTIMIZED=${ENABLE_OPTIMIZED} \ ENABLE_SHARED=0 @@ -94,6 +99,37 @@ set +e # We want to let all the tests run before we exit lit -v . RETURN="${RETURN}$?" +#generate and upload coverage if COVERAGE is set +if [ ${COVERAGE} -eq 1 ]; then + +#get zcov that works with gcov v4.8 + git clone https://github.com/ddunbar/zcov.git + cd zcov + sudo python setup.py install + sudo mkdir /usr/local/lib/python2.7/dist-packages/zcov-0.3.0.dev0-py2.7.egg/zcov/js + cd zcov + +#these files are not where zcov expects them to be after install so we move them + sudo cp js/sorttable.js /usr/local/lib/python2.7/dist-packages/zcov-0.3.0.dev0-py2.7.egg/zcov/js/sorttable.js + sudo cp js/sourceview.js /usr/local/lib/python2.7/dist-packages/zcov-0.3.0.dev0-py2.7.egg/zcov/js/sourceview.js + sudo cp style.css /usr/local/lib/python2.7/dist-packages/zcov-0.3.0.dev0-py2.7.egg/zcov/style.css + +#install zcov dependency + sudo apt-get install enscript + +#update gcov from v4.6 to v4.8. This is becauase gcda files are made for v4.8 and cause +#a segmentation fault in v4.6 + sudo apt-get install ggcov + sudo rm /usr/bin/gcov + sudo ln -s /usr/bin/gcov-4.8 /usr/bin/gcov + +#scan and generate coverage + zcov scan output.zcov ${BUILD_DIR} + zcov genhtml output.zcov coverage/ +#upload the coverage data, currently to a random ftp server + tar -zcvf coverage.tar.gz coverage/ + curl --form "file=@coverage.tar.gz" -u ${USER}:${PASSWORD} ${COVERAGE_SERVER} +fi ############################################################################### # Result ############################################################################### diff --git a/Dockerfile b/Dockerfile index 07f1bb48..d9fdd02d 100644 --- a/Dockerfile +++ b/Dockerfile @@ -11,6 +11,7 @@ ENV LLVM_VERSION=3.4 \ ENABLE_OPTIMIZED=1 \ KLEE_UCLIBC=1 \ KLEE_SRC=/home/klee/klee_src \ + COVERAGE=0 \ BUILD_DIR=/home/klee/klee_build RUN apt-get update && \ diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp index df7fffc5..d51c1695 100644 --- a/lib/Solver/CexCachingSolver.cpp +++ b/lib/Solver/CexCachingSolver.cpp @@ -35,6 +35,11 @@ namespace { cl::init(false)); cl::opt<bool> + CexCacheSuperSet("cex-cache-superset", + cl::desc("try substituting SAT super-set counterexample before asking the SMT solver (default=false)"), + cl::init(false)); + + cl::opt<bool> CexCacheExperimental("cex-cache-exp", cl::init(false)); } @@ -124,8 +129,10 @@ bool CexCachingSolver::searchForAssignment(KeyType &key, Assignment *&result) { if (CexCacheTryAll) { // Look for a satisfying assignment for a superset, which is trivially an // assignment for any subset. - Assignment **lookup = cache.findSuperset(key, NonNullAssignment()); - + Assignment **lookup = 0; + if (CexCacheSuperSet) + lookup = cache.findSuperset(key, NonNullAssignment()); + // Otherwise, look for a subset which is unsatisfiable, see below. if (!lookup) lookup = cache.findSubset(key, NullAssignment()); @@ -151,7 +158,9 @@ bool CexCachingSolver::searchForAssignment(KeyType &key, Assignment *&result) { // Look for a satisfying assignment for a superset, which is trivially an // assignment for any subset. - Assignment **lookup = cache.findSuperset(key, NonNullAssignment()); + Assignment **lookup = 0; + if (CexCacheSuperSet) + lookup = cache.findSuperset(key, NonNullAssignment()); // Otherwise, look for a subset which is unsatisfiable -- if the subset is // unsatisfiable then no additional constraints can produce a valid diff --git a/scripts/coverageServer.py b/scripts/coverageServer.py new file mode 100644 index 00000000..db708545 --- /dev/null +++ b/scripts/coverageServer.py @@ -0,0 +1,100 @@ +#!/usr/bin/python +from flask import * +from functools import wraps +from subprocess import call +from werkzeug import secure_filename +import json +import time +import os +import shutil +import tarfile + +##################### DESCRIPTION ################# +#This is the server to which coverage data is uploaded from travisCI. +#need to replace USER and PASSWORD with an actual username and passsword used to autheticate in /api +#Stored here, because it needs to be in version control somewhere +# +# Example of running the server +#uwsgi -s 127.0.0.1:3013 -w coverageServer:app --chmod=666 --post-buffering=81 --daemonize ./log +#where nginx is expecting uwsgi traffic at 127.0.0.1:3013 + + +#sample upload command +#curl --form "file=@coverage.tar.gz" -u USER:PASSWORD localhost:5000/api + + + + +UPLOAD_FOLDER = '.' + +#enable upload only every 5 minutes + +app = Flask(__name__) +app.config['UPLOAD_FOLDER'] = UPLOAD_FOLDER +app.config['MAX_CONTENT_LENGTH'] = 16 * 1024 * 1024 + +TIMEOUT = 0 + + +def check_auth(username, password): + return username == 'USER' and password == 'PASSWORD' + + +def authenticate(): + """Sends a 401 response that enables basic auth""" + return Response( + 'Could not verify your access level for that URL.\n' + 'You have to login with proper credentials', 401, + {'WWW-Authenticate': 'Basic realm="Login Required"'}) + + +def requires_auth(f): + @wraps(f) + def decorated(*args, **kwargs): + auth = request.authorization + if not auth or not check_auth(auth.username, auth.password): + return authenticate() + return f(*args, **kwargs) + return decorated + +@app.route("/<path:path>") +def serve_page(path): + return send_from_directory('./coverage', path) + +#check that the tar file has only one efolder named coverage +def check_tar(tar): + coverage_dir_num = 0 + for tarinfo in tar.getmembers(): + if 'coverage' in tarinfo.name and tarinfo.isdir(): + coverage_dir_num += 1 + elif not 'coverage/' in tarinfo.name: + return False + return coverage_dir_num == 1 + +@app.route("/api", methods=['POST']) +@requires_auth +def upload_coverage(): + global TIMEOUT +#only allow uploads every 5 minutes (a bit less than usuall travisCI build) + if time.time() - TIMEOUT < 300: + return "Time Out" + if request.method == 'POST': + file = request.files['file'] + if file.filename == "coverage.tar.gz": + filename = secure_filename(file.filename) + file.save(os.path.join(app.config['UPLOAD_FOLDER'], filename)) + tar = tarfile.open("./coverage.tar.gz") + if not check_tar(tar): + return "NOK" +#remove the previous coverage folder if it existis + if os.path.isdir("./coverage"): + shutil.rmtree("./coverage") + tar.extractall() + tar.close() + TIMEOUT = time.time() + return "OK" + return "NOK" + +if __name__ == "__main__": + app.debug = True + app.run(host="0.0.0.0") |