lit.site.cfg

# -*- Python -*-

# Configuration file for the 'lit' test runner.

import os
import sys
import re
import platform
from os import path

import lit.util
import lit.formats

# name: The name of this test suite.
config.name = 'Dafny Standard Libraries'

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 = ['.dfy']

# 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

config.environment['MSBUILDSINGLELOADCONTEXT'] = "1"

# 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']

# Prevent this issue on windows: https://github.com/dotnet/sdk/issues/8887
if 'HOMEPATH' in os.environ and 'HOMEDRIVE' in os.environ:
    config.environment['DOTNET_CLI_HOME'] = os.environ['HOMEDRIVE'] + os.environ['HOMEPATH']

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

if 'USERPROFILE' in os.environ:
    config.environment['USERPROFILE'] = os.environ['USERPROFILE']

# 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', '')

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

# Propagate 'LOCALAPPDATA' into lit's environment
# Fixes error on Windows
#   build cache is required, but could not be located:
#   GOCACHE is not defined and %LocalAppData% is not defined
if 'LOCALAPPDATA' in os.environ:
    config.environment['LOCALAPPDATA'] = os.environ['LOCALAPPDATA']

# 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 Dafny specific substitutions

# Find Dafny.exe
up = os.path.dirname
repositoryRoot = up(
                     up( os.path.abspath(__file__) )
                   )
lit_config.note('Repository root is {}'.format(repositoryRoot))

binaryDir = os.path.join(repositoryRoot, 'Binaries')
config.dafnyBinaryDir = binaryDir
sourceDirectory = os.path.join(repositoryRoot, 'Source')

defaultDafnyExecutable = 'dotnet run --no-build --project ' + quotePath(os.path.join(sourceDirectory, 'DafnyDriver', 'DafnyDriver.csproj'))
# dafnyExecutable = lit_config.params.get('executable', defaultDafnyExecutable + " --")
dafnyExecutable = 'dafny'

defaultServerExecutable = 'dotnet run --no-build --project ' + quotePath(os.path.join(sourceDirectory, 'DafnyServer', 'DafnyServer.csproj'))
# serverExecutable = lit_config.params.get('serverExecutable', defaultServerExecutable)

config.suffixes.append('.transcript')

# just the command needed to run dafny, without any additional command line options
# bareDafnyExecutable = dafnyExecutable
bareDafnyExecutable = 'dafny'

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

dafnyExecutable += ' -timeLimit:30'

# The following option adjusts the exit codes of the Dafny executable
dafnyExecutable += ' -countVerificationErrors:0'

# We do not want output such as "Compiled program written to Foo.cs"
# from the compilers, since that changes with the target language
dafnyExecutable += ' -compileVerbose:0'

# Allow user to provide extra arguments to Dafny
dafnyParams = lit_config.params.get('dafny_params','')
if len(dafnyParams) > 0:
    dafnyExecutable = dafnyExecutable + ' ' + dafnyParams

# Inform user what executable is being used
lit_config.note('Using Dafny (%dafny): {}\n'.format(dafnyExecutable))
lit_config.note('%baredafny will expand to {}\n'.format(bareDafnyExecutable))

ver = "0"
if os.name != "nt":
    ver = os.uname().version

config.substitutions.append( ('%dafny', dafnyExecutable) )
config.substitutions.append( ('%baredafny', bareDafnyExecutable) )
# config.substitutions.append( ('%server', serverExecutable) )
config.substitutions.append( ('%os', os.name) )
config.substitutions.append( ('%ver', ver ) )
if os.name == "nt":
    config.available_features = [ 'windows' ]
elif "Darwin" in ver:
    config.available_features = [ 'macosx', 'posix' ]
elif "16.04" in ver and "Ubuntu" in ver:
    config.available_features = [ 'ubuntu16', 'ubuntu', 'posix' ]
else:
    config.available_features = [ 'ubuntu', 'posix' ]

# Sanity check: Check solver executable is available
# z3Path = None

# potentialSolverRoots = [path.dirname(bareDafnyExecutable), binaryDir]
# potentialSolverExecutables = ['cvc4.exe', path.join("z3", "bin", "z3"), 'z3.exe', path.join("z3", "bin", "z3.exe")]

# for root in potentialSolverRoots:
#     for executable in potentialSolverExecutables:
#         if not z3Path:
#             potentialPath = path.join(root, executable)
#             if path.exists(potentialPath):
#                 z3Path = potentialPath

# if not z3Path:
#     lit_config.fatal('Could not find solver')
# config.substitutions.append( ('%z3', z3Path ) )

# Add diff tool substitution
commonDiffFlags=' --unified=3 --strip-trailing-cr'
diffExecutable = None
if os.name == 'posix':
    diffExecutable = lit.util.which('diff') + commonDiffFlags
elif os.name == 'nt':
    pydiff = quotePath( os.path.join(config.test_source_root, 'pydiff.py') )
    diffExecutable = sys.executable + ' ' + pydiff + commonDiffFlags
else:
    lit_config.fatal('Unsupported platform')
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') )

config.substitutions.append( ('%{dirsep}', os.sep) )