# -*- Python -*-

# Configuration file for the 'lit' test runner.

import os
import sys
import re
import platform

import lit.util
import lit.formats

lit_config.note('using Python {}'.format(sys.version))

# name: The name of this test suite.
config.name = 'Boogie'

config.test_format = lit.formats.ShTest(execute_external=False)

# suffixes: A list of file extensions to treat as test files. This is overriden
# by individual lit.local.cfg files in the test subdirectories.
config.suffixes = ['.bpl']

# excludes: A list of directories to exclude from the testsuite. The 'Inputs'
# subdirectories contain auxiliary inputs for various tests in their parent
# directories.
config.excludes = []

# test_source_root: The root path where tests are located.
config.test_source_root = os.path.dirname(os.path.abspath(__file__))

# test_exec_root: The root path where tests should be run.
config.test_exec_root = config.test_source_root

# Propagate 'HOME' through the environment.
if 'HOME' in os.environ:
    config.environment['HOME'] = os.environ['HOME']

# Propagate 'INCLUDE' through the environment.
if 'INCLUDE' in os.environ:
    config.environment['INCLUDE'] = os.environ['INCLUDE']

# Propagate 'LIB' through the environment.
if 'LIB' in os.environ:
    config.environment['LIB'] = os.environ['LIB']

# Propagate the temp directory. Windows requires this because it uses \Windows\
# if none of these are present.
if 'TMP' in os.environ:
    config.environment['TMP'] = os.environ['TMP']
if 'TEMP' in os.environ:
    config.environment['TEMP'] = os.environ['TEMP']

# Propagate PYTHON_EXECUTABLE into the environment
config.environment['PYTHON_EXECUTABLE'] = getattr(config, 'python_executable', '')

# Check that the object root is known.
if config.test_exec_root is None:
    lit_config.fatal('Could not determine execution root for tests!')

"""
   Function for quoting filepaths
   so that if they contain spaces
   lit's shell interpreter will
   treat the path as a single argument
"""
def quotePath(path):
    if ' ' in path:
        return '"{path}"'.format(path=path)
    else:
        return path

### Add Boogie specific substitutions

# Find Boogie executable and runtime
up = os.path.dirname
repositoryRoot = up(up(os.path.abspath(__file__)))
lit_config.note('Repository root is {}'.format(repositoryRoot))

configuration = lit_config.params.get('configuration', 'Debug')
framework = lit_config.params.get('framework', 'net6.0')

boogieBinary = 'Source/BoogieDriver/bin/{}/{}/BoogieDriver.dll'.format(configuration, framework)
runtime = 'dotnet'

boogieExecutable = os.path.join(repositoryRoot, boogieBinary)

if not os.path.exists(boogieExecutable):
    lit_config.fatal('Could not find Boogie executable at {}'.format(boogieExecutable))
if runtime and lit.util.which(runtime) == None:
    lit_config.fatal('Cannot find {}. Make sure it is in your PATH'.format(runtime))

boogieExecutable = runtime + ' ' + quotePath(boogieExecutable)

# We do not want absolute or relative paths in error messages, just the basename of the file
boogieExecutable += ' -useBaseNameForFileName'

# Allow user to provide extra arguments to Boogie
boogieParams = lit_config.params.get('boogie_params', '')
if len(boogieParams) > 0:
    boogieExecutable = boogieExecutable + ' ' + boogieParams

# Allow user to turn on batch mode in a way that allows skipping
# tests that don't support it.
batchMode = lit_config.params.get('batch_mode', '') == 'True'
if batchMode:
    config.available_features = ['batch_mode']
    boogieExecutable += ' -proverOpt:BATCH_MODE=true'

# Inform user what executable is being used
lit_config.note('Using Boogie: {}'.format(boogieExecutable))

config.substitutions.append(('%parallel-boogie', boogieExecutable + ' /vcsCores:2'))
config.substitutions.append(('%boogie', boogieExecutable))

# Add diff tool substitution
if os.name == 'posix':
    # use the system diff
    # Note: We need to get the absolute path because otherwise lit uses a
    #       built-in diff that does not support all flags below.
    diffExecutable = lit.util.which('diff')
else:
    # use driver around Python's difflib
    pydiff = quotePath(os.path.join(config.test_source_root, 'pydiff.py'))
    diffExecutable = sys.executable + ' ' + pydiff

diffExecutable += ' --unified=3 --strip-trailing-cr --ignore-all-space'
lit_config.note("Using diff tool: {}".format(diffExecutable))

config.substitutions.append(('%diff', diffExecutable))

# Detect the OutputCheck tool
outputCheckPath = lit.util.which('OutputCheck')
if outputCheckPath == None:
    lit_config.fatal('The OutputCheck tool is not in your PATH. Please install it.')

config.substitutions.append(('%OutputCheck', outputCheckPath + ' --dump-file-to-check'))
