From fccf018feecf914c937dc4cc253a882f482943f2 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 9 Mar 2018 12:16:30 +0000
Subject: Sort mono test cases, add missing files

---
 test/mono/builtins.sail              | 57 ++++++++++++++++++++++++++++++++++++
 test/mono/not-yet/builtins           |  1 +
 test/mono/not-yet/control_deps       |  1 +
 test/mono/not-yet/feature            |  1 +
 test/mono/not-yet/fnreduce           |  1 +
 test/mono/not-yet/fnreduce_manual    |  1 +
 test/mono/not-yet/times8             |  1 +
 test/mono/not-yet/union-exist        |  1 +
 test/mono/not-yet/union-exist_manual |  1 +
 test/mono/pass/control_deps          |  1 -
 test/mono/pass/feature               |  1 -
 test/mono/pass/fnreduce              |  1 -
 test/mono/pass/fnreduce_manual       |  1 -
 test/mono/pass/times8                |  1 -
 test/mono/pass/union-exist           |  1 -
 test/mono/pass/union-exist_manual    |  1 -
 test/mono/test_extra.lem             | 17 +++++++++++
 17 files changed, 82 insertions(+), 7 deletions(-)
 create mode 100644 test/mono/builtins.sail
 create mode 100644 test/mono/not-yet/builtins
 create mode 100644 test/mono/not-yet/control_deps
 create mode 100644 test/mono/not-yet/feature
 create mode 100644 test/mono/not-yet/fnreduce
 create mode 100644 test/mono/not-yet/fnreduce_manual
 create mode 100644 test/mono/not-yet/times8
 create mode 100644 test/mono/not-yet/union-exist
 create mode 100644 test/mono/not-yet/union-exist_manual
 delete mode 100644 test/mono/pass/control_deps
 delete mode 100644 test/mono/pass/feature
 delete mode 100644 test/mono/pass/fnreduce
 delete mode 100644 test/mono/pass/fnreduce_manual
 delete mode 100644 test/mono/pass/times8
 delete mode 100644 test/mono/pass/union-exist
 delete mode 100644 test/mono/pass/union-exist_manual
 create mode 100644 test/mono/test_extra.lem

(limited to 'test')

diff --git a/test/mono/builtins.sail b/test/mono/builtins.sail
new file mode 100644
index 00000000..e565ab58
--- /dev/null
+++ b/test/mono/builtins.sail
@@ -0,0 +1,57 @@
+$include <smt.sail>
+$include <flow.sail>
+default Order dec
+type bits ('n : Int) = vector('n, dec, bit)
+val operator & = "and_bool" : (bool, bool) -> bool
+val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
+overload operator == = {eq_int, eq_vec}
+val neq_vec = {lem: "neq"} : forall 'n. (bits('n), bits('n)) -> bool
+function neq_vec (x, y) = not_bool(eq_vec(x, y))
+overload operator != = {neq_atom, neq_vec}
+val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec"} : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n.
+  (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1))
+val mult_int = {ocaml: "mult", lem: "integerMult"} : (int, int) -> int
+overload operator * = {mult_range, mult_int, mult_real}
+val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
+val extz : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure
+function extz(v) = extz_vec(sizeof('m),v)
+val "exts_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
+val exts : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure
+function exts(v) = exts_vec(sizeof('m),v)
+val UInt = {
+  ocaml: "uint",
+  lem: "uint",
+  interpreter: "uint",
+  c: "sail_uint"
+} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1)
+val bitvector_cast = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
+val slice = "slice" : forall ('n : Int) ('m : Int), 'm >= 0 & 'n >= 0.
+  (bits('m), int, atom('n)) -> bits('n)
+
+/* Test constant propagation's implementation of builtins
+   TODO: need some way to check that everything has propagated. */
+
+register r8 : bits(8)
+register r16 : bits(16)
+
+val test : bool -> unit effect {escape,rreg,wreg}
+
+function test(b) = {
+    let 'n : {'n, 'n in {8,16}. atom('n)} = if b then 8 else 16;
+    let x : bits('n) = match 'n { 8 => 0x12, 16 => 0x1234 };
+    /* Constant propagation doesn't do registers, so uses of x' will be
+       evaluated at runtime */
+    let x' : bits('n) = match 'n { 8 => {r8 = x; r8}, 16 => {r16 = x; r16} };
+    let y : bits('n) = match 'n { 8 => 0x35, 16 => 0x5637 };
+    assert(x != y);
+    assert(slice(x, 0, 4) == slice(x',0,4));
+    assert(0x3 == slice(y, 4, 4));
+    assert(UInt(x) == (match n { 8 => 18, 16 => 4660 }));
+}
+
+val run : unit -> unit effect {escape,rreg,wreg}
+
+function run() = {
+    test(true);
+    test(false);
+}
\ No newline at end of file
diff --git a/test/mono/not-yet/builtins b/test/mono/not-yet/builtins
new file mode 100644
index 00000000..3abb0198
--- /dev/null
+++ b/test/mono/not-yet/builtins
@@ -0,0 +1 @@
+builtins.sail -auto_mono
\ No newline at end of file
diff --git a/test/mono/not-yet/control_deps b/test/mono/not-yet/control_deps
new file mode 100644
index 00000000..e173c42f
--- /dev/null
+++ b/test/mono/not-yet/control_deps
@@ -0,0 +1 @@
+control_deps.sail -auto_mono
\ No newline at end of file
diff --git a/test/mono/not-yet/feature b/test/mono/not-yet/feature
new file mode 100644
index 00000000..9363dd68
--- /dev/null
+++ b/test/mono/not-yet/feature
@@ -0,0 +1 @@
+feature -auto_mono -undefined_gen
\ No newline at end of file
diff --git a/test/mono/not-yet/fnreduce b/test/mono/not-yet/fnreduce
new file mode 100644
index 00000000..4237c34a
--- /dev/null
+++ b/test/mono/not-yet/fnreduce
@@ -0,0 +1 @@
+fnreduce.sail -auto_mono
\ No newline at end of file
diff --git a/test/mono/not-yet/fnreduce_manual b/test/mono/not-yet/fnreduce_manual
new file mode 100644
index 00000000..25d8256c
--- /dev/null
+++ b/test/mono/not-yet/fnreduce_manual
@@ -0,0 +1 @@
+fnreduce.sail -mono_split fnreduce.sail:43:x
\ No newline at end of file
diff --git a/test/mono/not-yet/times8 b/test/mono/not-yet/times8
new file mode 100644
index 00000000..1315855d
--- /dev/null
+++ b/test/mono/not-yet/times8
@@ -0,0 +1 @@
+times8.sail -auto_mono
\ No newline at end of file
diff --git a/test/mono/not-yet/union-exist b/test/mono/not-yet/union-exist
new file mode 100644
index 00000000..ebb89267
--- /dev/null
+++ b/test/mono/not-yet/union-exist
@@ -0,0 +1 @@
+union-exist.sail -auto_mono
diff --git a/test/mono/not-yet/union-exist_manual b/test/mono/not-yet/union-exist_manual
new file mode 100644
index 00000000..d35c3d48
--- /dev/null
+++ b/test/mono/not-yet/union-exist_manual
@@ -0,0 +1 @@
+union-exist.sail -mono_split union-exist.sail:9:v
\ No newline at end of file
diff --git a/test/mono/pass/control_deps b/test/mono/pass/control_deps
deleted file mode 100644
index e173c42f..00000000
--- a/test/mono/pass/control_deps
+++ /dev/null
@@ -1 +0,0 @@
-control_deps.sail -auto_mono
\ No newline at end of file
diff --git a/test/mono/pass/feature b/test/mono/pass/feature
deleted file mode 100644
index 9363dd68..00000000
--- a/test/mono/pass/feature
+++ /dev/null
@@ -1 +0,0 @@
-feature -auto_mono -undefined_gen
\ No newline at end of file
diff --git a/test/mono/pass/fnreduce b/test/mono/pass/fnreduce
deleted file mode 100644
index 4237c34a..00000000
--- a/test/mono/pass/fnreduce
+++ /dev/null
@@ -1 +0,0 @@
-fnreduce.sail -auto_mono
\ No newline at end of file
diff --git a/test/mono/pass/fnreduce_manual b/test/mono/pass/fnreduce_manual
deleted file mode 100644
index 25d8256c..00000000
--- a/test/mono/pass/fnreduce_manual
+++ /dev/null
@@ -1 +0,0 @@
-fnreduce.sail -mono_split fnreduce.sail:43:x
\ No newline at end of file
diff --git a/test/mono/pass/times8 b/test/mono/pass/times8
deleted file mode 100644
index 1315855d..00000000
--- a/test/mono/pass/times8
+++ /dev/null
@@ -1 +0,0 @@
-times8.sail -auto_mono
\ No newline at end of file
diff --git a/test/mono/pass/union-exist b/test/mono/pass/union-exist
deleted file mode 100644
index ebb89267..00000000
--- a/test/mono/pass/union-exist
+++ /dev/null
@@ -1 +0,0 @@
-union-exist.sail -auto_mono
diff --git a/test/mono/pass/union-exist_manual b/test/mono/pass/union-exist_manual
deleted file mode 100644
index d35c3d48..00000000
--- a/test/mono/pass/union-exist_manual
+++ /dev/null
@@ -1 +0,0 @@
-union-exist.sail -mono_split union-exist.sail:9:v
\ No newline at end of file
diff --git a/test/mono/test_extra.lem b/test/mono/test_extra.lem
new file mode 100644
index 00000000..a567257c
--- /dev/null
+++ b/test/mono/test_extra.lem
@@ -0,0 +1,17 @@
+open import Pervasives_extra
+open import Sail_instr_kinds
+open import Sail_values
+open import Sail_operators_mwords
+open import Prompt_monad
+open import State
+
+let undefined_int () = (0:ii)
+val undefined_bitvector : forall 'a. Size 'a => integer -> mword 'a
+let undefined_bitvector len = duplicate B0 len
+
+val uint : forall 'a. Size 'a => mword 'a -> integer
+let uint = unsigned
+
+val slice : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b
+let slice v lo len =
+  subrange_vec_dec v (lo + len - 1) lo
-- 
cgit v1.2.3