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
|
#!/usr/bin/env python3
import os
import re
import sys
import hashlib
from shutil import which
mydir = os.path.dirname(__file__)
os.chdir(mydir)
sys.path.insert(0, os.path.realpath('..'))
from sailtest import *
sail_dir = get_sail_dir()
sail = get_sail()
test_dir = '../typecheck/pass'
skip_tests = {
'phantom_option',
'phantom_bitlist_union',
# The Lem backend needs sail_mem_read to be instantiated at a minimum
'concurrency_interface_dec',
'concurrency_interface_inc',
# Requires types that aren't currently in the library
'float_prelude',
# No possible configuration
'config_mismatch',
# Custom outcome
'outcome_int',
'outcome_impl_int',
}
skip_tests_mwords = {
'phantom_option',
'overload_plus',
'vector_append_gen',
'execute_decode_hard',
'simple_record_access',
'vector_append',
'existential_constraint_synonym',
'exist_tlb',
'negative_bits_union',
'while_MM',
'while_PM',
'zero_length_bv',
'negative_bits_list',
'patternrefinement',
'abstract_extend',
'issue984',
# Due to an incompatibility between -auto_mono and -smt_linearize
'pow_32_64',
# The Lem backend needs sail_mem_read to be instantiated at a minimum
'concurrency_interface_dec',
'concurrency_interface_inc',
'wf_register_type',
'bitfield_exponential',
'bitfield_abs',
'bitfield_mod',
# Abstract types not implemented for Lem yet
'abstract_bool',
'abstract_bool2',
'constraint_syn',
'ex_vector_infer',
'ex_list_infer',
'ex_cons_infer',
# Requires types that aren't currently in the library
'float_prelude',
# Needs smarter monomorphisation
'bits_alias_cast',
# No possible configuration
'config_mismatch',
# Custom outcome
'outcome_int',
'outcome_impl_int',
}
print('Sail is {}'.format(sail))
print('Sail dir is {}'.format(sail_dir))
def test_lem(name, opts, skip_list):
if which('cvc4') is None:
skip_tests.add('type_pow_zero')
skip_tests_mwords.add('type_pow_zero')
banner('Testing Lem {}'.format(name))
results = Results(name)
for filenames in chunks(os.listdir(test_dir), parallel()):
tests = {}
for filename in filenames:
basename = os.path.splitext(os.path.basename(filename))[0]
if basename in skip_list:
print_skip(filename)
continue
tests[filename] = os.fork()
if tests[filename] == 0:
step('\'{}\' --lem {} --strict-bitvector -o {} {}/{}'.format(sail, opts, basename, test_dir, filename))
step('lem -lib \'{}\'/src/gen_lib {}_types.lem {}.lem'.format(sail_dir, basename, basename))
step('rm {}_types.lem {}.lem'.format(basename, basename))
print_ok(filename)
sys.exit(0)
results.collect(tests)
return results.finish()
xml = '<testsuites>\n'
xml += test_lem('with bitlists', '', skip_tests)
xml += test_lem('with machine words', '-lem_mwords -auto_mono', skip_tests_mwords)
xml += '</testsuites>\n'
output = open('tests.xml', 'w')
output.write(xml)
output.close()
|
