lit.site.cfg

# -*- Python -*-

# Configuration file for the 'lit' test runner.

import os
import sys
import re
import platform
import shutil
import subprocess
from os import path

import lit.util
import lit.formats

# name: The name of this test suite.
config.name = 'Dafny 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"

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

PROPAGATE_ENV = [
    'APPDATA',
    'HOME',
    'INCLUDE',
    'LIB',

    # Fixes error on Windows: build cache is required, but could not be located:
    # GOCACHE is not defined and %LocalAppData% is not defined
    'LOCALAPPDATA',

    'NODE_PATH',

    # Fixes NuGet.targets(564,5): error : Value cannot be null. (Parameter 'path1')
    'ProgramFiles',
    'ProgramFiles(x86)',

    # Prevent dotnet from creating a folder called %SystemDrive%
    'SystemDrive',

    'TEMP',
    'TMP',
    'USERPROFILE',
]

for var in PROPAGATE_ENV:
    if var in os.environ:
        config.environment[var] = os.environ[var]

# 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 PYTHON_EXECUTABLE into the environment
config.environment['PYTHON_EXECUTABLE'] = getattr(config, 'python_executable', '')

# Silence dotnet's welcome message
config.environment['DOTNET_NOLOGO'] = "true"

# 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

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

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

newDafnyArgs = [
# We do not want absolute or relative paths in error messages, just the basename of the file
'--use-basename-for-filename',

# Try to verify 2 verification conditions at once
'--cores=2',

# Set a default time limit, to catch cases where verification time runs off the rails
'--verification-time-limit=300'
]

# Add standard parameters
def addParams(cmd):
    dafnyParams = lit_config.params.get('dafny_params','')
    if len(dafnyParams) > 0:
        return f'{cmd} {dafnyParams}'
    else:
        return cmd

# Add run specific parameters
def buildCmd(args):
    if len(args) > 0:
        argStr = ' /'.join(args)
        return f'{dafnyExecutable} /{argStr}'
    else:
        return args

standardArguments = addParams(' '.join([]))

# Pass --compile-suffix when available (since extern implementations depend on this)
dafnyHelpProcess = subprocess.run(['dafny', '/help'], capture_output=True)
if dafnyHelpProcess.stdout.find(b'/compileSuffix') != -1:
    standardTranslationArguments = ' '.join(['--compile-suffix'])
else:
    standardTranslationArguments = ''

resolveArgs = ' resolve --use-basename-for-filename ' + standardArguments
verifyArgs = ' verify --use-basename-for-filename --cores:2 --verification-time-limit:300 ' + standardArguments
buildArgs = ' build --use-basename-for-filename --cores:2 --verification-time-limit:300 ' + standardArguments + ' ' + standardTranslationArguments
runArgs = ' run --use-basename-for-filename --cores:2 --verification-time-limit:300 ' + standardArguments + ' ' + standardTranslationArguments
testArgs = ' test --use-basename-for-filename --cores:2 --verification-time-limit:300 ' + standardArguments + ' ' + standardTranslationArguments

config.substitutions.append( ('%trargs', '--use-basename-for-filename --cores:2 --verification-time-limit:300' ) )

config.substitutions.append( ('%resolve', dafnyExecutable + resolveArgs ) )
config.substitutions.append( ('%verify', dafnyExecutable + verifyArgs ) )
config.substitutions.append( ('%translate', dafnyExecutable + ' translate'  ) )
config.substitutions.append( ('%build', dafnyExecutable + buildArgs ) )
config.substitutions.append( ('%run', dafnyExecutable + runArgs ) )
config.substitutions.append( ('%test', dafnyExecutable + runArgs ) )

# config.substitutions.append( ('%repositoryRoot', repositoryRoot) )
# config.substitutions.append( ('%binaryDir', binaryDir) )
# config.substitutions.append( ('%dafny', dafny) )
# config.substitutions.append( ('%args', standardArguments) )
# config.substitutions.append( ('%testDafnyForEachCompiler', testDafnyExecutable) )
# config.substitutions.append( ('%baredafny', dafnyExecutable) )
# config.substitutions.append( ('%server', serverExecutable) )
# config.substitutions.append( ('%refmanexamples', os.path.join(repositoryRoot, 'docs', 'DafnyRef', 'examples')) )
config.substitutions.append( ('%os', os.name) )
config.substitutions.append( ('%ver', ver ) )
config.substitutions.append( ('%sed', 'sed -E' ) )
config.substitutions.append( ('%exits-with', 'python3 ' + os.path.join(repositoryRoot, 'Scripts/test-exit.py') ) )
config.substitutions.append( ('!', 'python3 ' + os.path.join(repositoryRoot, 'Scripts/test-exit.py') + " -z" ) )

if os.name == "nt":
    config.available_features = [ 'windows' ]
elif "Darwin" in ver:
    config.available_features = [ 'macosx', 'posix' ]
elif "18.04" in ver and "Ubuntu" in ver:
    config.available_features = [ 'ubuntu18', 'ubuntu', 'posix' ]
else:
    config.available_features = [ 'ubuntu', 'posix' ]


# Add diff tool substitution
commonDiffFlags=' --unified=3 --strip-trailing-cr'
diffExecutable = None
if os.name == 'posix' or os.name == 'nt':
    pydiff = quotePath( os.path.join(config.test_source_root, 'Scripts', '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  --comment=//') )

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