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
|
# -*- Python -*-
# 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 = [ 'llvmgcc', 'llvmgxx']
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')) )
# 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
subs = [ ('%kleaver', 'kleaver', kleaver_extra_params), ('%klee','klee', klee_extra_params) ]
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')) )
# LLVM < 3.0 doesn't Support %T directive
if int(config.llvm_version_major) == 2:
# This is a hack
config.substitutions.append(('%T','Output'))
# 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(["2.9", "3.4", "3.5"])
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)
# 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')
|
