1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
|
#dist: xenial
services:
- docker
language: cpp
env:
###########################################################################
# Configurations
#
# Each line in the "env" section represents a set of environment variables
# passed to a build. Thus each line represents a different build
# configuration.
###########################################################################
# Check a subset of the matrix of:
# LLVM : {3.8, 3.9, 4.0, 5.0, 6.0, 7.0, 8.0, 9.0, 10.0}
# SOLVERS : {Z3, STP, STP:Z3, metaSMT}
# STP_VERSION : {2.3.3, master}
# METASMT_VERSION : {v4.rc1}
# METASMT_DEFAULT : {BTOR, CVC4, STP, YICES2, Z3}
# METASMT_BOOST_VERSION : {x.y.z} // e.g. 1.60.0, libboost-dev will be used if unspecified
# UCLIBC: {0, klee_uclibc_v1.0.0, klee_0_9_29} // Note ``0`` means disabled
# DISABLE_ASSERTIONS: {0, 1}
# ENABLE_OPTIMIZED: {0, 1}
# COVERAGE: {0, 1} // when set indicates that coverage data should be uploaded to the service
# USE_TCMALLOC: {0, 1}
# Define default values - they are overwritten by each matrix entry if needed
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=
# Default configuration for all Travis-CI jobs. They are overriden by each job.
- BASE_IMAGE=ubuntu:bionic-20200112
- REPOSITORY=klee
- COVERAGE=0
- DISABLE_ASSERTIONS=0
- ENABLE_OPTIMIZED=1
- ENABLE_DEBUG=1
- GTEST_VERSION=1.7.0
- KLEE_RUNTIME_BUILD="Debug+Asserts"
- LLVM_VERSION=6.0
- METASMT_VERSION=qf_abv
- MINISAT_VERSION="master"
- REQUIRES_RTTI=0
- SANITIZER_BUILD=
- SOLVERS=STP:Z3
- STP_VERSION=2.3.3
- TCMALLOC_VERSION=2.7
- UCLIBC_VERSION=klee_uclibc_v1.2
- USE_TCMALLOC=1
- USE_LIBCXX=1
- Z3_VERSION=4.8.4
jobs:
include:
# Check supported LLVM versions
- name: "LLVM 10"
env: LLVM_VERSION=10.0
- name: "LLVM 9"
env: LLVM_VERSION=9.0
- name: "LLVM 8"
env: LLVM_VERSION=8.0
- name: "LLVM 7"
env: LLVM_VERSION=7.0
- name: "LLVM 6"
env: LLVM_VERSION=6.0
- name: "LLVM 5"
env: LLVM_VERSION=5.0
- name: "LLVM 4"
env: LLVM_VERSION=4.0
- name: "LLVM 3.9"
env: LLVM_VERSION=3.9
- name: "LLVM 3.8"
env: LLVM_VERSION=3.8
# Sanitizer builds. Do unoptimized build otherwise the optimizer might remove problematic code
- name: "ASan"
env: SANITIZER_BUILD=address ENABLE_OPTIMIZED=0 USE_TCMALLOC=0
- name: "UBSan"
env: SANITIZER_BUILD=undefined ENABLE_OPTIMIZED=0 USE_TCMALLOC=0
# Use without libcxx as it is too slow to finish before travis time-out
- name: "MSan"
env: SANITIZER_BUILD=memory ENABLE_OPTIMIZED=0 USE_TCMALLOC=0 SOLVERS=STP USE_LIBCXX=0
# Test just using Z3 only
- name: "Z3 only"
env: SOLVERS=Z3
# Test just using metaSMT
- name: "metaSMT STP"
env: SOLVERS=metaSMT METASMT_DEFAULT=STP REQUIRES_RTTI=1
- name: "metaSMT Boolector"
env: SOLVERS=metaSMT METASMT_DEFAULT=BTOR REQUIRES_RTTI=1
# Test we can build against STP master
- name: "STP master"
env: SOLVERS=STP STP_VERSION=master
# Check we can build latest klee-uclibc branch
- name: "Latest klee-uclibc"
env: UCLIBC_VERSION=klee_0_9_29
# Check at least one build with Asserts disabled.
- name: "Asserts enabled"
env: SOLVERS=STP DISABLE_ASSERTIONS=1
# Check without TCMALLOC and with an optimised runtime library
- name: "No TCMalloc, optimised runtime"
env: USE_TCMALLOC=0 KLEE_RUNTIME_BUILD="Release+Debug+Asserts"
# Coverage build
- name: "Coverage"
env: ENABLE_OPTIMIZED=0 COVERAGE=1
# macOS
- name: "macOS"
os: osx
env: SOLVERS=STP UCLIBC_VERSION=0 USE_TCMALLOC=0 USE_LIBCXX=0
# Docker
- name: "Docker"
env: BUILD_DOCKER=1
# TODO: Add Doxygen build
addons:
apt:
packages:
- docker-ce
cache:
ccache: true
apt: true
directories:
- $HOME/Library/Caches/Homebrew
before_install:
- if [[ "$TRAVIS_OS_NAME" == "osx" ]]; then brew update; brew install bash ; fi
script:
# Build KLEE and run tests
- if [[ "${BUILD_DOCKER}" != "1" && "$TRAVIS_OS_NAME" == "osx" ]]; then export BASE=/tmp && export PATH="/usr/local/opt/ccache/libexec:/usr/local/bin:$PATH"; scripts/build/build.sh klee --debug --install-system-deps; export DYLD_LIBRARY_PATH=="$(cd ${BASE}/metaSMT-*-deps/stp-git-basic/lib/ && pwd)"; scripts/build/run-tests.sh /tmp/klee_build* --debug; fi
- if [[ "${BUILD_DOCKER}" != "1" && "$TRAVIS_OS_NAME" == "linux" ]]; then scripts/build/build.sh klee --docker --debug --push-docker-deps --create-final-image; fi
- if [[ "${BUILD_DOCKER}" != "1" && "$COVERAGE" == "1" && "$TRAVIS_OS_NAME" == "linux" ]]; then scripts/build/run-tests.sh --coverage --upload-coverage --run-docker --debug; fi
- if [[ "${BUILD_DOCKER}" != "1" && "$COVERAGE" == "0" && "$TRAVIS_OS_NAME" == "linux" ]]; then scripts/build/run-tests.sh --run-docker --debug; fi
- if [[ "${BUILD_DOCKER}" -eq 1 ]]; then docker build .; fi
|
