1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
|
# -*- 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 = ['Inputs']
# 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')
serverExecutable = os.path.join( binaryDir, 'DafnyServer.exe')
if not os.path.exists(dafnyExecutable):
lit_config.fatal('Could not find Dafny.exe at {}'.format(dafnyExecutable))
if not os.path.exists(serverExecutable):
lit_config.warning('Could not find DafnyServer.exe at {}'.format(serverExecutable))
else:
config.suffixes.append('.transcript')
dafnyExecutable = quotePath(dafnyExecutable)
if os.name == 'posix':
dafnyExecutable = 'mono ' + dafnyExecutable
serverExecutable = 'mono ' + serverExecutable
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 -countVerificationErrors:0'
# 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) )
config.substitutions.append( ('%server', serverExecutable) )
# 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'
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') )
|
