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
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
|
# -*- Python -*-
# vim: set filetype=python:
# vim: ts=2:sts=2:sw=2:et:tw=80:
# Configuration file for the 'lit' test runner.
import os
import sys
import re
import platform
try:
import lit.util
import lit.formats
except ImportError:
pass
# name: The name of this test suite.
config.name = 'KLEE'
# testFormat: The test format to use to interpret tests.
config.test_format = lit.formats.ShTest(execute_external=False)
# suffixes: A list of file extensions to treat as test files
# Note this can be overridden by lit.local.cfg files
config.suffixes = ['.ll', '.c', '.cpp', '.kquery']
# test_source_root: The root path where tests are located.
config.test_source_root = os.path.dirname(__file__)
# test_exec_root: The root path where tests should be run.
klee_obj_root = getattr(config, 'klee_obj_root', None)
klee_src_root = getattr(config, 'klee_src_root', None)
if klee_obj_root is not None:
config.test_exec_root = os.path.join(klee_obj_root, 'test')
# Tweak the PATH to include the tool dir.
if klee_obj_root is not None:
klee_tools_dir = getattr(config, 'klee_tools_dir', None)
if not klee_tools_dir:
lit.fatal('No KLEE tools dir set!')
# Check LLVM tool directory
llvm_tools_dir = getattr(config, 'llvm_tools_dir', None)
if not llvm_tools_dir:
lit.fatal('No LLVM tool directory set!')
path = os.path.pathsep.join(
(
llvm_tools_dir,
klee_tools_dir,
config.environment['PATH']
)
)
config.environment['PATH'] = path
# Propogate some environment variable to test environment.
def addEnv(name):
if name in os.environ:
config.environment[name] = os.environ[name]
addEnv('HOME')
addEnv('PWD')
# Sanitizer environment variables
addEnv('ASAN_OPTIONS')
addEnv('ASAN_SYMBOLIZER_PATH')
addEnv('LSAN_OPTIONS')
addEnv('MSAN_OPTIONS')
addEnv('MSAN_SYMBOLIZER_PATH')
addEnv('TSAN_OPTIONS')
# llvm-gcc on Ubuntu needs to be told where to look
# for headers. If user has these in their environment
# we should propagate to test environment
addEnv('C_INCLUDE_PATH')
addEnv('CPLUS_INCLUDE_PATH')
# Check that the object root is known.
if config.test_exec_root is None:
lit.fatal('test execution root not set!')
# Add substitutions from lit.site.cfg
subs = [ 'clangxx', 'clang', 'cc', 'cxx', 'O0opt' ]
for name in subs:
value = getattr(config, name, None)
if value == None:
lit.fatal('{0} is not set'.format(name))
config.substitutions.append( ('%' + name, value))
# Add a substitution for lli.
config.substitutions.append(
('%lli', os.path.join(llvm_tools_dir, 'lli'))
)
# Add a substitution for llvm-as
config.substitutions.append(
('%llvmas', os.path.join(llvm_tools_dir, 'llvm-as'))
)
# Add a substitution for llvm-ar
config.substitutions.append(
('%llvmar', os.path.join(llvm_tools_dir, 'llvm-ar'))
)
# Add a substition for libkleeruntest
config.substitutions.append(
('%libkleeruntestdir', os.path.dirname(config.libkleeruntest))
)
config.substitutions.append(
('%libkleeruntest', config.libkleeruntest)
)
# Get KLEE and Kleaver specific parameters passed on llvm-lit cmd line
# e.g. llvm-lit --param klee_opts=--help
try:
lit.params
except AttributeError:
klee_extra_params = lit_config.params.get('klee_opts',"")
kleaver_extra_params = lit_config.params.get('kleaver_opts',"")
else:
klee_extra_params = lit.params.get('klee_opts',"")
kleaver_extra_params = lit.params.get('kleaver_opts',"")
if len(klee_extra_params) != 0:
print("Passing extra KLEE command line args: {0}".format(
klee_extra_params)
)
if len(kleaver_extra_params) != 0:
print("Passing extra Kleaver command line args: {0}".format(
kleaver_extra_params)
)
# Set absolute paths and extra cmdline args for KLEE's tools
# If a tool's name is a prefix of another, the longer name has
# to come first, e.g., klee-replay should come before klee
subs = [ ('%kleaver', 'kleaver', kleaver_extra_params),
('%klee-replay', 'klee-replay', ''),
('%klee','klee', klee_extra_params),
('%ktest-tool', 'ktest-tool', ''),
('%gen-bout', 'gen-bout', '')
]
for s,basename,extra_args in subs:
config.substitutions.append(
( s,
"{0} {1}".format(
os.path.join(klee_tools_dir, basename),
extra_args
).strip()
)
)
config.substitutions.append(
('%gentmp', os.path.join(klee_src_root, 'scripts/genTempFiles.sh'))
)
# Add feature for the LLVM version in use, so it can be tested in REQUIRES and
# XFAIL checks. We also add "not-XXX" variants, for the same reason.
known_llvm_versions = set(["3.4", "3.5", "3.6", "3.7", "3.8", "3.9"])
current_llvm_version = "%s.%s" % (config.llvm_version_major,
config.llvm_version_minor)
config.available_features.add("llvm-" + current_llvm_version)
for version in known_llvm_versions:
if version != current_llvm_version:
config.available_features.add("not-llvm-" + version)
if current_llvm_version >= version:
config.available_features.add("geq-llvm-" + version)
else:
config.available_features.add("lt-llvm-" + version)
# Solver features
if config.enable_stp:
config.available_features.add('stp')
else:
config.available_features.add('not-stp')
if config.enable_z3:
config.available_features.add('z3')
else:
config.available_features.add('not-z3')
# Zlib
config.available_features.add('zlib' if config.enable_zlib else 'not-zlib')
# POSIX runtime feature
if config.enable_posix_runtime:
config.available_features.add('posix-runtime')
# Target operating system features
supported_targets = ['linux', 'darwin']
for target in supported_targets:
if config.target_triple.find(target) != -1:
config.available_features.add(target)
else:
config.available_features.add('not-{}'.format(target))
# Sanitizer
config.available_features.add('{}asan'.format('' if config.have_asan else 'not-'))
config.available_features.add('{}ubsan'.format('' if config.have_ubsan else 'not-'))
config.available_features.add('{}msan'.format('' if config.have_msan else 'not-'))
|
