Code for testing builtins with Coq

Disabled by default because it's fairly resource heavy.
Currently two failures: a minor bug affecting divmod.sail, and undefined
values aren't set up for set_slice_bits.sail.

2 files changed, 47 insertions, 0 deletions

diff --git a/test/builtins/run_tests.py b/test/builtins/run_tests.py
index b20d4224..ba13d5b9 100755
--- a/test/builtins/run_tests.py
+++ b/test/builtins/run_tests.py
@@ -86,6 +86,37 @@ def test_lem_builtins(name):
         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('sail -no_warn -coq -o {} {}'.format(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 -R $SAIL_DIR/../bbv/theories bbv -R $SAIL_DIR/lib/coq Sail {}_types.v'.format(basename))
+                step('coqc -R $SAIL_DIR/../bbv/theories bbv -R $SAIL_DIR/lib/coq Sail {}.v'.format(basename))
+                step('coqtop -R "$SAIL_DIR/../bbv/theories" bbv -R "$SAIL_DIR/lib/coq" Sail -require {}_types -require {} -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()
+
 xml = '<testsuites>\n'
 
 xml += test_c_builtins('C, No optimisations', '')
@@ -96,6 +127,7 @@ xml += test_ocaml_builtins('OCaml', '')
 
 # Comment this out for most runs because it's really slow
 # xml += test_lem_builtins('Lem to OCaml')
+# xml += test_coq_builtins('Coq')
 
 xml += '</testsuites>\n'
 
diff --git a/test/builtins/test.v b/test/builtins/test.v
new file mode 100644
index 00000000..64c5bf10
--- /dev/null
+++ b/test/builtins/test.v
@@ -0,0 +1,15 @@
+Require Import Sail2_state_monad.
+Require Import Sail2_state_lifting.
+Require Import String.
+Require Import List.
+Import ListNotations.
+
+Goal True.
+let result := eval cbv in (liftState register_accessors (main tt) (init_state tt)) in
+match result with
+  | [(Value tt,_)] => idtac "OK"
+  | [(Ex (Failure ?s),_)] => idtac "Fail:" s
+  | _ => idtac "Fail"
+end.
+exact I.
+Qed.