lit.site.cfg

# -*- Python -*-

# Configuration file for the 'lit' test runner.

import os
import sys
import shutil
from os import path

import lit.util
import lit.formats

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

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 = ['Inputs', 'sandbox', 'separate-compilation']

# 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"
# Use the following line to limit testing to certain compilers only. For example, "cs,java"
# config.environment['DAFNY_INTEGRATION_TESTS_ONLY_COMPILERS'] = "cs"


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

# Find Dafny.exe
up = os.path.dirname
repositoryRoot = up(up(up(up(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, 'Dafny', 'Dafny.csproj')) + ' -- '
dafnyExecutable = lit_config.params.get('executable', defaultDafnyExecutable )

testDafnyExecutableCompiler = 'dotnet run --no-build --project ' + quotePath(os.path.join(sourceDirectory, 'TestDafny', 'TestDafny.csproj')) + " -- for-each-compiler"
testDafnyExecutableResolver = 'dotnet run --no-build --project ' + quotePath(os.path.join(sourceDirectory, 'TestDafny', 'TestDafny.csproj')) + " -- for-each-resolver"

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

boogieExecutable = 'dotnet tool run boogie'

config.suffixes.append('.transcript')

dafnyArgs = [
    # We do not want absolute or relative paths in error messages, just the basename of the file
    'useBaseNameForFileName',
    'showSnippets:0',
    'env:0',

    # Try to verify 2 verification conditions at once
    'vcsCores:2',

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

    # Set a default resource limit, to catch cases where verification runs off the rails
    'rlimit:50000000',

    # Also include a time limit, because we do care about using too much time.
    'timeLimit:300',
    'allowAxioms:1',

    'deprecation:1',

    # Disallow standard libraries by default in tests,
    # to discourage the language itself from depending on them.
    'standardLibraries:0'
]
    
boogieArgs = [
    'infer:j',
    'proverOpt:O:auto_config=false',
    'proverOpt:O:type_check=true',
    'proverOpt:O:smt.case_split=3',
    'proverOpt:O:smt.qi.eager_threshold=100',
    'proverOpt:O:smt.delay_units=true',
    'proverOpt:O:smt.arith.solver=2'
]

# 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(cmd, args):
    if len(args) > 0:
        argStr = ' /'.join(args)
        return f'{cmd} /{argStr}'
    else:
        return cmd
        
dafny = addParams(buildCmd(dafnyExecutable, dafnyArgs))
boogie = buildCmd(boogieExecutable, boogieArgs)

standardArguments = addParams(' '.join(["--use-basename-for-filename", "--show-snippets:false", "--type-system-refresh", "--general-traits=datatype", "--general-newtypes"]))

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

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

config.substitutions.append( ('%resolve', dafnyExecutable + " resolve --standard-libraries:false " + standardArguments ) )
config.substitutions.append( ('%verify', dafnyExecutable + " verify --cores:2 --verification-time-limit:300 --resource-limit:50e6 --standard-libraries:false " + standardArguments) )
config.substitutions.append( ('%translate', dafnyExecutable + " translate"  ) )
config.substitutions.append( ('%trargs', "--cores:2 --verification-time-limit:300 --resource-limit:50e6 --standard-libraries:false " + standardArguments ) )
config.substitutions.append( ('%build', dafnyExecutable + " build --cores:2 --verification-time-limit:300 --resource-limit:50e6 --standard-libraries:false " + standardArguments ) )
config.substitutions.append( ('%run', dafnyExecutable + " run --cores:2 --verification-time-limit:300 --resource-limit:50e6 --standard-libraries:false " + standardArguments ) )
config.substitutions.append( ('%audit', dafnyExecutable + " audit --standard-libraries:false --use-basename-for-filename --type-system-refresh --general-traits=datatype --general-newtypes " ) )

config.substitutions.append( ('%repositoryRoot', repositoryRoot) )
config.substitutions.append( ('%binaryDir', binaryDir) )
config.substitutions.append( ('%dafny', dafny) )
config.substitutions.append( ('%boogie', boogie) )
config.substitutions.append( ('%args', standardArguments) )
config.substitutions.append( ('%testDafnyForEachCompiler', testDafnyExecutableCompiler) )
config.substitutions.append( ('%testDafnyForEachResolver', testDafnyExecutableResolver) )
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" ) )
config.substitutions.append( ('%cargo', 'cargo' ) )

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

# Sanity check: Check solver executable is available
solverRoots = os.pathsep.join(
    (path.dirname(dafnyExecutable), binaryDir, os.environ["PATH"])
)

print(solverRoots)

solverPath = \
    lit.util.which("z3-4.12.1", solverRoots) or \
    lit.util.which("cvc4", solverRoots)

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

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