From a92a6573ea2d7cf88c1c7ac8dcc79a241aea0df7 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Mon, 4 Feb 2019 20:06:49 +0000 Subject: Test lem output by running end-to-end tests using ocaml via lem --- test/c/cfold_reg.sail | 2 +- test/c/eq_struct.sail | 2 +- test/c/lbuild/_tags | 3 ++ test/c/lbuild/myocamlbuild.ml | 77 +++++++++++++++++++++++++++++++++++++++++++ test/c/poly_pair.sail | 2 +- test/c/run_tests.py | 26 +++++++++++++++ 6 files changed, 109 insertions(+), 3 deletions(-) create mode 100644 test/c/lbuild/_tags create mode 100644 test/c/lbuild/myocamlbuild.ml (limited to 'test') diff --git a/test/c/cfold_reg.sail b/test/c/cfold_reg.sail index a5090e91..53066bf5 100644 --- a/test/c/cfold_reg.sail +++ b/test/c/cfold_reg.sail @@ -2,7 +2,7 @@ default Order dec $include -val "eq_string" : (string, string) -> bool +val eq_string = { lem: "eq", _: "eq_string" } : (string, string) -> bool overload operator == = {eq_string} diff --git a/test/c/eq_struct.sail b/test/c/eq_struct.sail index b4258569..9da12aae 100644 --- a/test/c/eq_struct.sail +++ b/test/c/eq_struct.sail @@ -3,7 +3,7 @@ default Order dec $include $include -val eq = "eq_anything" : forall ('a : Type). ('a, 'a) -> bool +val eq = { lem: "eq", _: "eq_anything" } : forall ('a : Type). ('a, 'a) -> bool overload operator == = {eq} diff --git a/test/c/lbuild/_tags b/test/c/lbuild/_tags new file mode 100644 index 00000000..ced67350 --- /dev/null +++ b/test/c/lbuild/_tags @@ -0,0 +1,3 @@ +true: debug +<*.m{l,li}>: package(lem), package(linksem), package(zarith) +: package(lem), package(linksem), package(zarith) diff --git a/test/c/lbuild/myocamlbuild.ml b/test/c/lbuild/myocamlbuild.ml new file mode 100644 index 00000000..cc65b03a --- /dev/null +++ b/test/c/lbuild/myocamlbuild.ml @@ -0,0 +1,77 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + +open Ocamlbuild_plugin ;; +open Command ;; +open Pathname ;; +open Outcome ;; + +(* paths relative to _build *) +let lem = "lem" ;; + +(* All -wl ignores should be removed if you want to see the pattern compilation, exhaustive, and unused var warnings *) +let lem_opts = [A "-lib"; P ".."; + A "-wl_pat_comp"; P "ign"; + A "-wl_pat_exh"; P "ign"; + A "-wl_pat_fail"; P "ign"; + A "-wl_unused_vars"; P "ign"; + ] ;; + +dispatch begin function +| After_rules -> + rule "lem -> ml" + ~prod: "%.ml" + ~dep: "%.lem" + (fun env builder -> Seq [ + Cmd (S ([ P lem] @ lem_opts @ [ A "-ocaml"; P (env "%.lem") ])); + ]); + +| _ -> () +end ;; diff --git a/test/c/poly_pair.sail b/test/c/poly_pair.sail index c4989829..7c86062d 100644 --- a/test/c/poly_pair.sail +++ b/test/c/poly_pair.sail @@ -2,7 +2,7 @@ default Order dec val print = "print_endline" : string -> unit -val "eq_int" : (int, int) -> bool +val eq_int = { lem: "eq", _: "eq_int" } : (int, int) -> bool union test('a : Type, 'b : Type) = { Ctor1 : ('a, 'b), diff --git a/test/c/run_tests.py b/test/c/run_tests.py index 4f221636..4927e281 100755 --- a/test/c/run_tests.py +++ b/test/c/run_tests.py @@ -64,6 +64,30 @@ def test_ocaml(name): results.collect(tests) return results.finish() +def test_lem(name): + banner('Testing {}'.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: + step('sail -lem {}'.format(filename)) + step('mkdir -p _lbuild_{}'.format(basename)) + step('cp {}*.lem _lbuild_{}'.format(basename, basename)) + step('cp lbuild/* _lbuild_{}'.format(basename)) + step('cp ../../src/gen_lib/*.lem _lbuild_{}'.format(basename)) + os.chdir('_lbuild_{}'.format(basename)) + step('echo "let _ = {}.main ()" > main.ml'.format(basename.capitalize())) + step('ocamlbuild -use-ocamlfind main.native'.format(basename, basename)) + step('./main.native 1> {}.lresult'.format(basename)) + step('diff ../{}.expect {}.lresult'.format(basename, basename)) + print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END) + sys.exit() + results.collect(tests) + return results.finish() + xml = '\n' xml += test_c('unoptimized C', '', '', True) @@ -76,6 +100,8 @@ xml += test_interpreter('interpreter') xml += test_ocaml('OCaml') +#xml += test_lem('lem') + xml += '\n' output = open('tests.xml', 'w') -- cgit v1.2.3