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
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
|
#!/usr/bin/env python3
import os
import re
import sys
import hashlib
mydir = os.path.dirname(__file__)
os.chdir(mydir)
sys.path.insert(0, os.path.join(mydir, '..'))
from sailtest import *
sail_dir = get_sail_dir()
sail = get_sail()
targets = get_targets(['c', 'ocaml'])
print("Sail is {}".format(sail))
print("Sail dir is {}".format(sail_dir))
print("Targets: {}".format(targets))
def test_c_builtins(name, sail_opts):
banner('Testing builtins: {} Sail options: {}'.format(name, sail_opts))
results = Results(name)
for filenames in chunks(os.listdir('.'), parallel()):
tests = {}
for filename in filenames:
basename = os.path.splitext(os.path.basename(filename))[0]
tests[filename] = os.fork()
if tests[filename] == 0:
step('\'{}\' -no_warn -c {} {} 1> {}.c'.format(sail, sail_opts, filename, basename))
step('gcc {}.c \'{}\'/lib/*.c -lgmp -I \'{}\'/lib -o {}'.format(basename, sail_dir, sail_dir, basename))
step('./{}'.format(basename))
step('rm {}.c'.format(basename))
step('rm {}'.format(basename))
print('{} {}{}{}'.format(filename, color.PASS, 'ok', color.END))
sys.exit()
results.collect(tests)
return results.finish()
return collect_results(name, tests)
def test_ocaml_builtins(name, sail_opts):
banner('Testing builtins: {} Sail options: {}'.format(name, sail_opts))
results = Results(name)
for filenames in chunks(os.listdir('.'), parallel()):
tests = {}
for filename in filenames:
basename = os.path.splitext(os.path.basename(filename))[0]
tests[filename] = os.fork()
if tests[filename] == 0:
step('\'{}\' -no_warn -ocaml -ocaml_build_dir _sbuild_{} -o {} {}'.format(sail, basename, basename, filename))
step('./{}'.format(basename))
step('rm -r _sbuild_{}'.format(basename))
step('rm {}'.format(basename))
print('{} {}{}{}'.format(filename, color.PASS, 'ok', color.END))
sys.exit()
results.collect(tests)
return results.finish()
return collect_results(name, tests)
def test_lem_builtins(name):
banner('Testing builtins: {}'.format(name))
results = Results(name)
for filenames in chunks(os.listdir('.'), parallel()):
tests = {}
for filename in filenames:
basename = os.path.splitext(os.path.basename(filename))[0]
tests[filename] = os.fork()
if tests[filename] == 0:
# Generate Lem from Sail
step('\'{}\' -no_warn -lem -o {} {}'.format(sail, basename, filename))
# Create a directory to build the generated Lem and
# copy/move everything we need into it, as well as
# making a symlink to gen_lib for ocamlbuild
step('mkdir -p _lbuild_{}'.format(basename))
step('mv {}.lem _lbuild_{}'.format(basename, basename))
step('mv {}_types.lem _lbuild_{}'.format(basename, basename))
step('cp myocamlbuild.ml _lbuild_{}'.format(basename))
step('cp \'{}\'/src/gen_lib/*.lem _lbuild_{}'.format(sail_dir, basename))
os.chdir('_lbuild_{}'.format(basename))
# Use ocamlbuild to build the lem to OCaml using the
# myocamlbuild.ml rule
step('ocamlbuild -package lem {}.native'.format(basename))
step('./{}.native'.format(basename))
# Cleanup the build directory
os.chdir('..')
step('rm -r _lbuild_{}'.format(basename))
print('{} {}{}{}'.format(filename, color.PASS, 'ok', color.END))
sys.exit()
results.collect(tests)
return results.finish()
def test_coq_builtins(name):
banner('Testing builtins: {}'.format(name))
results = Results(name)
for filenames in chunks(os.listdir('.'), parallel()):
tests = {}
for filename in filenames:
basename = os.path.splitext(os.path.basename(filename))[0]
tests[filename] = os.fork()
if tests[filename] == 0:
# Generate Coq from Sail
step('\'{}\' -no_warn -coq -coq-lib-style stdpp -coq-record-update -coq-all-eq-dec -undefined_gen -o {} {}'.format(sail, basename, filename))
step('mkdir -p _coqbuild_{}'.format(basename))
step('mv {}.v _coqbuild_{}'.format(basename, basename))
step('mv {}_types.v _coqbuild_{}'.format(basename, basename))
step('cp test.v _coqbuild_{}'.format(basename))
os.chdir('_coqbuild_{}'.format(basename))
# TODO: find bbv properly
step('coqc {}_types.v'.format(basename))
step('coqc {}.v'.format(basename))
step('coqtop -require-import {}_types -require-import {} -l test.v -batch | tee /dev/stderr | grep -q OK'.format(basename,basename))
os.chdir('..')
step('rm -r _coqbuild_{}'.format(basename))
print('{} {}{}{}'.format(filename, color.PASS, 'ok', color.END))
sys.exit()
results.collect(tests)
return results.finish()
def test_isla_builtins(name):
banner('Testing builtins: {}'.format(name))
isla_dir = os.environ['ISLA_DIR']
results = Results(name)
for filenames in chunks(os.listdir('.'), parallel()):
tests = {}
for filename in filenames:
basename = os.path.splitext(os.path.basename(filename))[0]
tests[filename] = os.fork()
if tests[filename] == 0:
step('\'{}\'/isla-sail/isla-sail {} \'{}\'/lib/vector_dec.sail \'{}\'/test/property/include/config.sail -o {}'.format(isla_dir, filename, sail_dir, isla_dir, basename))
step('\'{}\'/target/release/isla-execute-function -A {}.ir -C \'{}\'/configs/plain.toml main'.format(isla_dir, basename, isla_dir))
step('rm {}.ir'.format(basename))
print('{} {}{}{}'.format(filename, color.PASS, 'ok', color.END))
sys.exit()
results.collect(tests)
return results.finish()
return collect_results(name, tests)
xml = '<testsuites>\n'
if 'c' in targets:
xml += test_c_builtins('C, No optimisations', '')
xml += test_c_builtins('C, Optimisations', '-O')
xml += test_c_builtins('C, Constant folding', '-Oconstant_fold')
if 'ocaml' in targets:
xml += test_ocaml_builtins('OCaml', '')
# Avoid this for most runs because it's really slow
if 'lem' in targets:
xml += test_lem_builtins('Lem to OCaml')
if 'coq' in targets:
xml += test_coq_builtins('Coq')
# Isla is separate, so don't run by default
# For testing symbolic operations in Isla it's useful to tweak the primop macros
# so that the symbolic versions are used even when the values are concrete.
if 'isla' in targets:
xml += test_isla_builtins('Isla')
xml += '</testsuites>\n'
output = open('tests.xml', 'w')
output.write(xml)
output.close()
|
