summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
authorAlasdair2020-04-28 17:24:04 +0100
committerAlasdair2020-05-11 19:00:53 +0100
commit199e10df8e776e4b27f9cfd2357db6babf674ed1 (patch)
treec2fe422fd4f40a639f1cb7d164dde805c6f673a9 /test
parent54b6277d79c64d15b155fc161d927aa968afafa1 (diff)
Functorise and refactor C code generator
Currently uses the -c2 option Now generates a sail_state struct which is passed as a pointer to all generated functions. This contains all registers, letbindings, and the exception state. (Letbindings must be included as they can contain pointers to registers). This should make it possible to use sail models in a multi-threaded program by creating multiple sail_states, provided a suitable set of thread-safe memory builtins are provided. Currently the sail_state cannot be passed to the memory builtins. For foo.sail, now generate a foo.c, foo.h, and (optionally) a foo_emu.c. foo_emu.c wraps the generated library into an emulator that behaves the same as the one we previously generated. The sail_assert and sail_match_failure builtins are now in a separate file, as they must exist even when the RTS is not used. Name mangling can be controlled via the exports and exports_mangled fields of the configuration struct (currently not exposed outside of OCaml). exports allows specifying a name in C for any Sail identifier (before name mangling) and exports_mangled allows specifiying a name for a mangled Sail identifier - this is primarily useful for generic functions and data structures which have been specialised.
Diffstat (limited to 'test')
-rw-r--r--test/c/cheri_capreg.sail23
-rwxr-xr-xtest/c/run_tests.py38
2 files changed, 30 insertions, 31 deletions
diff --git a/test/c/cheri_capreg.sail b/test/c/cheri_capreg.sail
index a9480ab6..51001ec3 100644
--- a/test/c/cheri_capreg.sail
+++ b/test/c/cheri_capreg.sail
@@ -63,29 +63,6 @@ struct CapStruct = {
length : bits(64),
}
-let null_cap : CapStruct = struct {
- tag = false,
- padding = zeros(),
- otype = zeros(),
- uperms = zeros(),
- perm_reserved11_14 = zeros(),
- access_system_regs = false,
- permit_unseal = false,
- permit_ccall = false,
- permit_seal = false,
- permit_store_local_cap = false,
- permit_store_cap = false,
- permit_load_cap = false,
- permit_store = false,
- permit_load = false,
- permit_execute = false,
- global = false,
- sealed = false,
- address = zeros(),
- base = zeros(),
- length = 0xffffffffffffffff
-}
-
let default_cap : CapStruct = struct {
tag = true,
padding = zeros(),
diff --git a/test/c/run_tests.py b/test/c/run_tests.py
index c4f0e591..c4463e51 100755
--- a/test/c/run_tests.py
+++ b/test/c/run_tests.py
@@ -32,6 +32,27 @@ def test_c(name, c_opts, sail_opts, valgrind):
results.collect(tests)
return results.finish()
+def test_c2(name, c_opts, sail_opts, valgrind):
+ banner('Testing {} with C (-c2) options: {} Sail options: {} valgrind: {}'.format(name, c_opts, sail_opts, valgrind))
+ 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('sail -no_warn -c2 {} {} -o {}'.format(sail_opts, filename, basename))
+ step('gcc {} {}.c {}_emu.c {}/lib/*.c -lgmp -lz -I {}/lib -o {}'.format(c_opts, basename, basename, sail_dir, sail_dir, basename))
+ step('./{} 1> {}.result'.format(basename, basename), expected_status = 1 if basename == "exception" else 0)
+ step('diff {}.result {}.expect'.format(basename, basename))
+ if valgrind:
+ step("valgrind --leak-check=full --track-origins=yes --errors-for-leak-kinds=all --error-exitcode=2 ./{}".format(basename), expected_status = 1 if basename == "exception" else 0)
+ step('rm {}.c {} {}.result'.format(basename, basename, basename))
+ print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END)
+ sys.exit()
+ results.collect(tests)
+ return results.finish()
+
def test_interpreter(name):
banner('Testing {}'.format(name))
results = Results(name)
@@ -94,16 +115,17 @@ def test_lem(name):
xml = '<testsuites>\n'
-xml += test_c('unoptimized C', '', '', True)
-xml += test_c('optimized C', '-O2', '-O', True)
-xml += test_c('constant folding', '', '-Oconstant_fold', True)
-xml += test_c('monomorphised C', '-O2', '-O -Oconstant_fold -auto_mono', True)
-xml += test_c('specialization', '-O1', '-O -c_specialize', True)
-xml += test_c('undefined behavior sanitised', '-O2 -fsanitize=undefined', '-O', False)
+xml += test_c2('unoptimized C', '', '', True)
+#xml += test_c('unoptimized C', '', '', True)
+#xml += test_c('optimized C', '-O2', '-O', True)
+#xml += test_c('constant folding', '', '-Oconstant_fold', True)
+#xml += test_c('monomorphised C', '-O2', '-O -Oconstant_fold -auto_mono', True)
+#xml += test_c('specialization', '-O1', '-O -c_specialize', True)
+#xml += test_c('undefined behavior sanitised', '-O2 -fsanitize=undefined', '-O', False)
-xml += test_interpreter('interpreter')
+#xml += test_interpreter('interpreter')
-xml += test_ocaml('OCaml')
+#xml += test_ocaml('OCaml')
#xml += test_lem('lem')