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
|
#!/usr/bin/env python3
import os
import re
import sys
import hashlib
import argparse
mydir = os.path.dirname(__file__)
os.chdir(mydir)
sys.path.insert(0, os.path.realpath('..'))
from sailtest import *
update_expected = args.update_expected
run_skips = args.run_skips
sail_dir = get_sail_dir()
sail = get_sail()
# Self-tests refers to self contained Sail programs in test/c/ which are Sail programs
# that you can run to exercise the language and the extracted output.
# Not all self-tests are supported.
skip_selftests = {
'outcome_impl', # custom outcome types (not expected to work)
'outcome_impl_int', # custom outcome types (not expected to work)
'outcome_impl_bool', # custom outcome types (not expected to work)
'union_variant_names',
'varswap',
'real',
'poly_outcome',
'string_of_bits',
'pointer_assign',
'concurrency_interface',
'for_shadow',
'string_literal_type',
'issue429',
'pc_no_wildcard',
'type_if_bits',
'nexp_simp_euclidian',
'issue136',
'anf_as_pattern',
'real_prop',
'constructor247',
'deep_poly_nest',
'config_abstract_bool', # Register type unsupported in state.ml
'newtype',
'assign_in_funarg',
'concurrency_interface_v2',
'config_map_guard',
'let_assert',
}
print("Sail is {}".format(sail))
print("Sail dir is {}".format(sail_dir))
def test_lean(subdir: str, skip_list = None, runnable: bool = False):
"""
Run all Sail files available in the `subdir`.
If `runnable` is set to `True`, it will do `lake run`
instead of `lake build`.
"""
banner(f'Testing lean target (sub-directory: {subdir})')
results = Results(subdir)
for filenames in chunks(os.listdir(f'../{subdir}'), parallel()):
tests = {}
for filename in filenames:
basename = os.path.splitext(os.path.basename(filename))[0]
is_skip = False
if skip_list is not None and basename in skip_list:
if run_skips:
is_skip = True
else:
print_skip(filename)
continue
tests[filename] = os.fork()
if tests[filename] == 0:
os.chdir(f'../{subdir}')
step('rm -r {} || true'.format(basename))
step('mkdir -p {}'.format(basename))
# TODO: should probably be dependent on whether print should be pure or effectful.
extra_flags = [
'--splice',
'coq-print.splice',
'--strict-bitvector',
] if runnable else [ ]
if not runnable:
extra_flags.append('--lean-matchbv')
extra_flags = ' '.join(extra_flags)
step('\'{}\' {} {} --lean --lean-single-file --lean-output-dir {}'.format(sail, extra_flags, filename, basename), name=filename)
if runnable and basename.startswith('fail'):
step(f'lake exe run > expected 2> err_status',
cwd=f'{basename}/out',
name=filename,
expected_status=1,
stderr_file=f'{basename}/out/err_status')
elif runnable:
step('timeout 90s lake exe run > expected 2> err_status',
cwd=f'{basename}/out',
name=filename,
stderr_file=f'{basename}/out/err_status')
else:
# NOTE: lake --dir does not behave the same as cd $dir && lake build...
step('lake build', cwd=f'{basename}/out', name=filename)
if not runnable:
output = f"{basename}/output"
step(f'cat {basename}/out/Out/Defs.lean > {output}')
step(f'echo >> {output}; echo "XXXXXXXXX" >> {output}; echo >> {output}')
step(f'cat {basename}/out/Out.lean >> {output}')
status = step_with_status(f'diff {output} {basename}.expected.lean', name=filename)
if status != 0:
if update_expected:
print(f'Overriding file {basename}.expected.lean')
step(f'cp {output} {basename}.expected.lean')
else:
sys.exit(1)
else:
status = step_with_status(f'diff {basename}/out/expected {basename}.expect', name=filename)
if status != 0:
sys.exit(1)
step('rm -r {}'.format(basename))
if is_skip:
print(f'{basename} now passes!')
print_ok(filename)
sys.exit(0)
results.collect(tests)
return results.finish()
xml = '<testsuites>\n'
xml += test_lean('lean')
xml += test_lean('c', skip_list=skip_selftests, runnable=True)
xml += '</testsuites>\n'
output = open('tests.xml', 'w')
output.write(xml)
output.close()
|
