Enable mono builtins test, tweak test output

3 files changed, 21 insertions, 32 deletions

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/pass/builtins
index 3abb0198..3abb0198 100644
--- a/test/mono/not-yet/builtins
+++ b/test/mono/pass/builtins
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