From 71f2f7875235621ce155c8c7d7326fabdbc63b35 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 17 Apr 2018 17:52:37 +0100
Subject: Enable mono builtins test, tweak test output

---
 test/mono/builtins.sail    | 49 +++++++++++++++++-----------------------------
 test/mono/not-yet/builtins |  1 -
 test/mono/pass/builtins    |  1 +
 test/mono/test.ml          |  4 +++-
 4 files changed, 22 insertions(+), 33 deletions(-)
 delete mode 100644 test/mono/not-yet/builtins
 create mode 100644 test/mono/pass/builtins

diff --git a/test/mono/builtins.sail b/test/mono/builtins.sail
index e565ab58..7fb2b822 100644
--- a/test/mono/builtins.sail
+++ b/test/mono/builtins.sail
@@ -1,55 +1,42 @@
 $include <smt.sail>
 $include <flow.sail>
+$include <vector_dec.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 neq_vec = {lem: "neq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
+function neq_vec (x, y) = not_bool(x == y)
+overload operator != = {neq_vec}
 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)
+/* A function that constant propagation won't touch */
+val launder : forall 'n. bits('n) -> bits('n) effect {escape}
+function launder(x) = {
+  assert(true);
+  x
+}
 
-val test : bool -> unit effect {escape,rreg,wreg}
+val test : bool -> unit effect {escape}
 
 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 x' : bits('n) = launder(x);
     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 }));
+    assert(x != y, "!= by propagation");
+    assert(slice(x, 0, 4) == slice(x',0,4), "propagated slice == runtime slice");
+    assert(0x3 == slice(y, 4, 4), "literal vs propagated middle slice");
+    assert(UInt(x) == (match n { 8 => 18, 16 => 4660 }), "UInt propagation vs literal");
 }
 
-val run : unit -> unit effect {escape,rreg,wreg}
+val run : unit -> unit effect {escape}
 
 function run() = {
     test(true);
diff --git a/test/mono/not-yet/builtins b/test/mono/not-yet/builtins
deleted file mode 100644
index 3abb0198..00000000
--- a/test/mono/not-yet/builtins
+++ /dev/null
@@ -1 +0,0 @@
-builtins.sail -auto_mono
\ No newline at end of file
diff --git a/test/mono/pass/builtins b/test/mono/pass/builtins
new file mode 100644
index 00000000..3abb0198
--- /dev/null
+++ b/test/mono/pass/builtins
@@ -0,0 +1 @@
+builtins.sail -auto_mono
\ No newline at end of file
diff --git a/test/mono/test.ml b/test/mono/test.ml
index 32d3b2ed..a54e3145 100644
--- a/test/mono/test.ml
+++ b/test/mono/test.ml
@@ -1,3 +1,5 @@
 match Out.run() with
 | Done _ -> exit 0
-| _ -> exit 1
+| Fail s -> prerr_endline ("Fail: " ^ s); exit 1
+| Error s -> prerr_endline ("Error: " ^ s); exit 1
+| _ -> prerr_endline "Unexpected outcome"; exit 1
-- 
cgit v1.2.3