# -*- 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 = { "9.0", "10.0", "11.0", "11.1", "12.0", "13.0", "14.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-'))