Set up the same test infrastructure as in Boogie.

1 files changed, 146 insertions, 0 deletions

diff --git a/Test/lit.site.cfg b/Test/lit.site.cfg
new file mode 100644
index 00000000..c9597a4c
--- /dev/null
+++ b/Test/lit.site.cfg
@@ -0,0 +1,146 @@
+# -*- Python -*-
+
+# Configuration file for the 'lit' test runner.
+
+import os
+import sys
+import re
+import platform
+
+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 = []
+
+# 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 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')
+dafnyExecutable = os.path.join( binaryDir, 'Dafny.exe')
+
+if not os.path.exists(dafnyExecutable):
+    lit_config.fatal('Could not find Dafny.exe at {}'.format(dafnyExecutable))
+
+dafnyExecutable = quotePath(dafnyExecutable)
+
+if os.name == 'posix':
+    dafnyExecutable = 'mono ' + dafnyExecutable
+    if lit.util.which('mono') == None:
+        lit_config.fatal('Cannot find mono. Make sure it is your PATH')
+
+# Expected output does not contain logo
+dafnyExecutable += ' -nologo'
+
+# We do not want absolute or relative paths in error messages, just the basename of the file
+dafnyExecutable += ' -useBaseNameForFileName'
+
+# 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: {}\n'.format(dafnyExecutable))
+
+config.substitutions.append( ('%dafny', dafnyExecutable) )
+
+# Sanity check: Check solver executable is available
+# FIXME: Should this check be removed entirely?
+if os.name != 'nt':
+    solvers = ['z3.exe','cvc4.exe']
+    solverFound = False
+    for solver in solvers:
+        if os.path.exists( os.path.join(binaryDir, solver)):
+            solverFound = True
+
+    if not solverFound:
+        lit_config.fatal('Could not find solver in "{binaryDir}". Tried looking for {solvers}'.format(
+                           binaryDir=binaryDir,
+                           solvers=solvers
+                           )
+                        )
+else:
+    lit_config.warning('Skipping solver sanity check on Windows')
+
+# Add diff tool substitution
+commonDiffFlags=' --unified=3 --strip-trailing-cr --ignore-all-space'
+diffExecutable = None
+if os.name == 'posix':
+    diffExecutable = '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') )