# -*- 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'] # 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') # Check KLEE tools directory klee_tools_dir = getattr(config, 'klee_tools_dir', None) if not klee_tools_dir: lit_config.fatal('No KLEE tools dir set!') # Check LLVM tools directory llvm_tools_dir = getattr(config, 'llvm_tools_dir', None) if not llvm_tools_dir: lit_config.fatal('No LLVM tools directory set!') # Add LLVM tools and FileCheck with not to PATH path = os.path.pathsep.join( ( os.path.join(klee_tools_dir, "testtools"), llvm_tools_dir, config.environment['PATH'] ) ) config.environment['PATH'] = path # Propagate 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_config.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_config.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 substitution for llvm-link config.substitutions.append( ('%llvmlink', os.path.join(llvm_tools_dir, 'llvm-link')) ) # Add a substition for libkleeruntest config.substitutions.append( ('%libkleeruntestdir', os.path.dirname(config.libkleeruntest)) ) config.substitutions.append( ('%libkleeruntest', config.libkleeruntest) ) # Add a substition for sqlite3 config.substitutions.append( ('%sqlite3', os.path.abspath(config.sqlite3)) ) # Get KLEE and Kleaver specific parameters passed on llvm-lit cmd line # e.g. llvm-lit --param klee_opts=--help klee_extra_params = lit_config.params.get('klee_opts',"") kleaver_extra_params = lit_config.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-exec-tree', 'klee-exec-tree', ''), ('%klee-replay', 'klee-replay', ''), ('%klee-stats', 'klee-stats', ''), ('%klee-zesti', 'klee-zesti', ''), ('%klee','klee', klee_extra_params), ('%ktest-tool', 'ktest-tool', ''), ('%ktest-randgen', 'ktest-randgen', ''), ('%ktest-gen', 'ktest-gen', '') ] 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')) ) # Prepare the full include expression, i.e. for all given paths. For example, ["path1","path2"] # becomes "-I path1 -I path2" config.substitutions.append( ('%libcxx_includes', " ".join( ["-I "+ p for p in getattr(config, 'libcxx_include_dirs', [])] )) ) # 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 = { "11.0", "11.1", "12.0", "13.0", "14.0", "15.0", "16.0", "17.0" } current_llvm_version_tuple = (int(config.llvm_version_major), int(config.llvm_version_minor)) current_llvm_version = "%s.%s" % current_llvm_version_tuple if current_llvm_version not in known_llvm_versions: lit_config.fatal("LLVM Version %s is not listed in known_llvm_versions!" % current_llvm_version) config.available_features.add("llvm-" + current_llvm_version) for version in known_llvm_versions: version_tuple = tuple(int(v) for v in version.split(".")) if version != current_llvm_version: config.available_features.add("not-llvm-" + version) if current_llvm_version_tuple >= version_tuple: 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') # Uclibc if config.enable_uclibc: config.available_features.add('uclibc') # POSIX runtime feature if config.enable_posix_runtime: config.available_features.add('posix-runtime') # libc++ runtime feature if config.enable_libcxx: config.available_features.add('libcxx') # C++ Exception Handling feature if config.enable_eh_cxx: config.available_features.add('eh-cxx') # Target operating system features supported_targets = ['linux', 'darwin', 'freebsd'] 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)) if 'WSL_DISTRO_NAME' in os.environ and 'WSL_INTEROP' not in os.environ: config.available_features.add('wsl-1') else: config.available_features.add('not-wsl-1') if 'WSL_DISTRO_NAME' in os.environ and 'WSL_INTEROP' in os.environ: config.available_features.add('wsl-2') else: config.available_features.add('not-wsl-2') # m32 support config.available_features.add('{}target-x86'.format('' if config.target_triple.find("i386") != -1 else 'not-')) config.available_features.add('{}32bit-support'.format('' if config.have_32bit_support else 'not-')) # 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-')) # SQLite config.available_features.add('{}sqlite3'.format('' if config.have_sqlite3 else 'not-'))