beginnings of a sail library test suite.

4 files changed, 166 insertions, 0 deletions

diff --git a/src/test/lib/Makefile b/src/test/lib/Makefile
new file mode 100644
index 00000000..2c4036f7
--- /dev/null
+++ b/src/test/lib/Makefile
@@ -0,0 +1,40 @@
+
+# Disable built-in make madness
+MAKEFLAGS=-r
+.SUFFIXES:
+
+TESTS=div.sail
+
+BITBUCKET_DIR:=$(realpath ../../../../)
+LEM_DIR:=$(BITBUCKET_DIR)/lem
+LEM:=$(LEM_DIR)/lem
+LEMLIB = $(LEM_DIR)/ocaml-lib
+SAIL_DIR:=$(BITBUCKET_DIR)/sail/src
+SAIL:=$(SAIL_DIR)/sail.native
+ZARITH_DIR:=$(LEM_DIR)/ocaml-lib/dependencies/zarith
+ZARITH_LIB:=$(ZARITH_DIR)/zarith.cmxa
+SAIL_VALUES:=$(SAIL_DIR)/gen_lib/sail_values.ml
+
+BUILD_DIR:=_build
+
+$(BUILD_DIR):
+	mkdir -p $@
+
+ocaml: | $(BUILD_DIR)
+	cp test_lib.sail $(SAIL_VALUES) run_test_embed.ml $(BUILD_DIR)
+	cd $(BUILD_DIR) && \
+	$(SAIL) -ocaml test_lib.sail -o test && \
+	ocamlopt -I $(ZARITH_DIR) $(ZARITH_LIB) sail_values.ml test.ml run_test_embed.ml -o test_embed.native && \
+	./test_embed.native
+
+interp: | $(BUILD_DIR)
+	cp test_lib.sail $(BUILD_DIR) && \
+	cp run_test_interp.ml $(BUILD_DIR) && \
+	cd $(BUILD_DIR) && \
+	$(SAIL) -lem_ast test_lib.sail -o test_lem_ast && \
+	$(LEM) -ocaml test_lem_ast.lem -lib $(SAIL_DIR)/lem_interp && \
+	ocamlfind ocamlopt -g -package num -I $(ZARITH_DIR)  -I $(SAIL_DIR)/_build/lem_interp -I $(LEMLIB) -linkpkg $(ZARITH_LIB) $(LEMLIB)/extract.cmxa  $(SAIL_DIR)/_build/lem_interp/extract.cmxa test_lem_ast.ml run_test_interp.ml -o test_interp.native && \
+	./test_interp.native
+
+all:
+	true
diff --git a/src/test/lib/run_test_embed.ml b/src/test/lib/run_test_embed.ml
new file mode 100644
index 00000000..f7b45316
--- /dev/null
+++ b/src/test/lib/run_test_embed.ml
@@ -0,0 +1,2 @@
+Test._run()
+  
diff --git a/src/test/lib/run_test_interp.ml b/src/test/lib/run_test_interp.ml
new file mode 100644
index 00000000..e6a7f00f
--- /dev/null
+++ b/src/test/lib/run_test_interp.ml
@@ -0,0 +1,56 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  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 Printf ;;
+open Format ;;
+open Big_int ;;
+open Interp_ast ;;
+open Interp_interface ;;
+open Interp_inter_imp ;;
+open Sail_impl_base ;;
+open Run_interp_model ;;
+
+let doit () =
+  let context = build_context Test_lem_ast.defs [] [] [] [] [] [] [] None [] in
+  translate_address context E_little_endian "run" None (address_of_integer (Nat_big_num.of_int 0));;
+
+doit () ;;
diff --git a/src/test/lib/test_lib.sail b/src/test/lib/test_lib.sail
new file mode 100644
index 00000000..bcabe2cc
--- /dev/null
+++ b/src/test/lib/test_lib.sail
@@ -0,0 +1,68 @@
+
+
+scattered typedef ast = const union
+val ast -> unit effect pure execute
+scattered function unit execute
+
+union ast member (unit) DUMMY
+function clause execute (DUMMY) = ()
+
+end ast
+end execute
+
+(*val extern string -> unit effect {wmv} printt*)
+
+function unit test_assert (name, pred) = {
+  print (name);
+  if pred then
+    print (": pass\n")
+  else
+    print(": fail\n")
+}
+
+function (bit[64]) run ((bit[64]) x) = {
+  test_assert ("not_bit0", (not (bitzero)) == bitone);
+  test_assert ("not_bit1", (not (bitone)) == bitzero);
+
+
+  test_assert ("bitwise_not", (~ (0b01) == 0b10));
+  test_assert ("bitwise_not_bit0", (~ (bitzero) == bitone));
+  test_assert ("bitwise_not_bit1", (~ (bitone) == bitzero));
+
+  test_assert ("bitwise_or", (0b0101 | 0b0011) == 0b0111);
+  test_assert ("bitwise_or_00", (bitzero | bitzero) == bitzero);
+  test_assert ("bitwise_or_01", (bitzero | bitone)  == bitone);
+  test_assert ("bitwise_or_10", (bitone  | bitzero) == bitone);
+  test_assert ("bitwise_or_11", (bitone  | bitone)  == bitone);
+
+  test_assert ("bitwise_xor", (0b0101 ^ 0b0011) == 0b0110);
+  (*
+  XXX something in here causes sail to infinite loop
+  test_assert ("bitwise_xor_00", (bitzero ^ bitzero) == bitzero);
+  test_assert ("bitwise_xor_01", (bitzero ^ bitone)  == bitone);
+  test_assert ("bitwise_xor_10", (bitone  ^ bitzero) == bitone);
+  test_assert ("bitwise_xor_11", (bitone  ^ bitone)  == bitzero);*)
+
+  test_assert ("bitwise_and", (0b0101 & 0b0011) == 0b0001);
+  test_assert ("bitwise_and_00", (bitzero & bitzero) == bitzero);
+  test_assert ("bitwise_and_01", (bitzero & bitone)  == bitzero);
+  test_assert ("bitwise_and_10", (bitone  & bitzero) == bitzero);
+  test_assert ("bitwise_and_11", (bitone  & bitone)  == bitone);
+
+  test_assert ("divpospos_exact", (21 div 7) == 3);
+  test_assert ("divposneg_exact", (21 div -7) == -3);
+  test_assert ("divnegpos_exact", (-21 div 7) == -3);
+  test_assert ("divnegneg_exact", (-21 div -7) == 3);
+
+  test_assert ("divpospos_approx", (21 div 8) == 2);
+  test_assert ("divposneg_approx", (21 div -8) == -2);
+  test_assert ("divnegpos_approx", (-21 div 8) == -2);
+  test_assert ("divnegneg_approx", (-21 div -8) == 2);
+
+  (* XXX currently crashes on shallow embedding 
+  test_assert ("div_overflow", ((bit[8])(0x80 quot_s 0xff)) == 0x80);
+  *)
+
+  return 0;
+}
+