summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/mono/assert2.sail22
-rw-r--r--test/mono/atomsplit.sail30
-rw-r--r--test/mono/castreq.sail40
-rw-r--r--test/mono/control_deps.sail68
-rw-r--r--test/mono/exint.sail57
-rw-r--r--test/mono/feature.sail49
-rwxr-xr-xtest/mono/test.sh6
-rw-r--r--test/mono/tests10
-rw-r--r--test/mono/times8.sail42
-rw-r--r--test/mono/times8div8.sail66
10 files changed, 368 insertions, 22 deletions
diff --git a/test/mono/assert2.sail b/test/mono/assert2.sail
index 67e18f76..edf92710 100644
--- a/test/mono/assert2.sail
+++ b/test/mono/assert2.sail
@@ -1,3 +1,17 @@
+$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 mult_int = {ocaml: "mult", lem: "integerMult"} : (int, int) -> int
+overload operator * = {mult_range, mult_int, mult_real}
+val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
+overload operator < = {lt_atom, lt_int}
+
+/* Should find a set constraint below the let */
+
val f : forall 'n. atom('n) -> unit effect {escape}
function f(n) = {
@@ -7,3 +21,11 @@ function f(n) = {
()
}
}
+
+
+val run : unit -> unit effect {escape}
+
+function run () = {
+ f(8);
+ f(16);
+} \ No newline at end of file
diff --git a/test/mono/atomsplit.sail b/test/mono/atomsplit.sail
new file mode 100644
index 00000000..6e5d3e3b
--- /dev/null
+++ b/test/mono/atomsplit.sail
@@ -0,0 +1,30 @@
+$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 mult_int = {ocaml: "mult", lem: "integerMult"} : (int, int) -> int
+overload operator * = {mult_range, mult_int, mult_real}
+val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
+overload operator < = {lt_atom, lt_int}
+
+/* Test splitting required because there's a size calculation in the function */
+
+val foo : forall 'n. atom('n) -> unit effect {escape}
+
+function foo(n) = {
+ assert(constraint('n in {2,4}));
+ let 'm = 8 * n in
+ let x : bits('m) = replicate_bits(0b0,m) in
+ let y : bits('n) = replicate_bits(0b0,n) in
+ ()
+}
+
+val run : unit -> unit effect {escape}
+
+function run () = {
+ foo(2);
+ foo(4);
+} \ No newline at end of file
diff --git a/test/mono/castreq.sail b/test/mono/castreq.sail
index 3c03c452..5b155aa9 100644
--- a/test/mono/castreq.sail
+++ b/test/mono/castreq.sail
@@ -1,3 +1,25 @@
+$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 mult_int = {ocaml: "mult", lem: "integerMult"} : (int, int) -> int
+overload operator * = {mult_range, mult_int, mult_real}
+val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
+overload operator < = {lt_atom, lt_int}
+val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
+val extzv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure
+function extzv(v) = extz_vec(sizeof('m),v)
+val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append"} : forall ('n : Int) ('m : Int).
+ (bits('n), bits('m)) -> bits('n + 'm)
+overload append = {bitvector_concat}
+val bitvector_cast = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
+val bitvector_length = "length" : forall 'n. bits('n) -> atom('n)
+overload length = {bitvector_length}
+
+/* Test generation of casts across case splits (e.g., going from bits('m) to bits(32)) */
val foo : forall 'm 'n, 'm in {8,16} & 'n in {32,64}. bits('m) -> bits('n) effect pure
@@ -41,6 +63,7 @@ function assign(x) = {
r
}
+/* Adding casts for top-level pattern matches is not yet supported
val foo2 : forall 'm 'n, 'm in {8,16} & 'n in {32,64}. (atom('n), bits('m)) -> bits('n) effect pure
@@ -58,4 +81,19 @@ function bar2(8,x) =
and bar2(16,x) =
use(x)
-
+*/
+
+val run : unit -> unit effect {escape,undef}
+
+function run () = {
+ bar(0x12);
+ bar(0x3456);
+ assert((ret(0x34) : bits(32)) == 0x00340034);
+ assert((ret(0x34) : bits(64)) == 0x0034003400340034);
+ assert((ret(0x3456) : bits(32)) == 0x34563456);
+ assert((ret(0x3456) : bits(64)) == 0x3456345634563456);
+ assert((assign(0x12) : bits(32)) == 0x00120012);
+ assert((assign(0x1234) : bits(32)) == 0x12341234);
+ assert((assign(0x12) : bits(64)) == 0x0012001200120012);
+ assert((assign(0x1234) : bits(64)) == 0x1234123412341234);
+} \ No newline at end of file
diff --git a/test/mono/control_deps.sail b/test/mono/control_deps.sail
index eaefd129..b94ffe2f 100644
--- a/test/mono/control_deps.sail
+++ b/test/mono/control_deps.sail
@@ -1,44 +1,76 @@
-(* Test monomorphisation control dependencies *)
-
+$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 mult_int = {ocaml: "mult", lem: "integerMult"} : (int, int) -> int
+overload operator * = {mult_range, mult_int, mult_real}
+val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
+overload operator < = {lt_atom, lt_int}
+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 bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append"} : forall ('n : Int) ('m : Int).
+ (bits('n), bits('m)) -> bits('n + 'm)
+overload append = {bitvector_concat}
+val bitvector_cast = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
+val bitvector_length = "length" : forall 'n. bits('n) -> atom('n)
+overload length = {bitvector_length}
+
+/* Test monomorphisation control dependencies */
-val (bool,bool) -> unit effect pure f
+val f : (bool,bool) -> unit
function f(nosplit,split) = {
if nosplit then {
- let (exist 'x, true. [:'x:]) 'x = if split then 16 else 32 in
- let (bit['x]) v = extz(0b0) in
+ let 'x : {'x, true. atom('x)} = if split then 16 else 32 in
+ let v : bits('x) = extz(0b0) in
()
} else ()
}
-val (bool,bool) -> unit effect pure g
+val g : (bool,bool) -> unit
function g(split,nosplit) = {
- (exist 'x, true. [:'x:]) x := 16;
- (exist 'y, true. [:'y:]) y := 16;
+ x : {'x, true. atom('x)} = 16;
+ y : {'y, true. atom('y)} = 16;
if split then
- x := 32
+ x = 32
else
();
if nosplit then
- y := 32
+ y = 32
else
();
- let (exist 'z, true. [:'z:]) 'z = x in
- let (bit['z]) v = extz(0b0) in
+ let 'z : {'z, true. atom('z)} = x in
+ let v : bits('z)= extz(0b0) in
()
}
-typedef exception = unit
+type exception = unit
-val bool -> unit effect {escape} h
+val h : bool -> unit effect {escape}
-(* Note: we don't really need to split on b, but it's awkward to avoid.
- The important bit is not to overreact to the exception. *)
+/* Note: we don't really need to split on b, but it's awkward to avoid.
+ The important bit is not to overreact to the exception. */
+/* While the case splitting currently works, it doesn't yet generate a fake size
+ for 'x or remove the dead code that needs one
function h(b) = {
- let (exist 'x, true. [:'x:]) 'x =
+ let 'x : {'x, true. atom('x)} =
if b then 16 else throw () in
- let (bit['x]) v = extz(0b0) in
+ let v : bits('x) = extz(0b0) in
()
}
+*/
+
+val run : unit -> unit /*effect {escape}*/
+
+function run () = {
+ f(false,false);
+ f(false,true);
+ g(false,false);
+ g(false,true);
+/* h(true);*/
+} \ No newline at end of file
diff --git a/test/mono/exint.sail b/test/mono/exint.sail
new file mode 100644
index 00000000..65589fb8
--- /dev/null
+++ b/test/mono/exint.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 mult_int = {ocaml: "mult", lem: "integerMult"} : (int, int) -> int
+overload operator * = {mult_range, mult_int, mult_real}
+val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
+overload operator < = {lt_atom, lt_int}
+val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
+val extzv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure
+function extzv(v) = extz_vec(sizeof('m),v)
+val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append"} : forall ('n : Int) ('m : Int).
+ (bits('n), bits('m)) -> bits('n + 'm)
+overload append = {bitvector_concat}
+val bitvector_cast = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
+val bitvector_length = "length" : forall 'n. bits('n) -> atom('n)
+overload length = {bitvector_length}
+val cast ex_int : int -> {'n, true. atom('n)}
+function ex_int 'n = n
+
+
+/* Decode -> int -> existential test */
+
+val needssize : forall 'n, 'n >= 0. atom('n) -> unit effect pure
+
+function needssize(n) = {
+ let x : bits('n) = replicate_bits(0b0,n) in
+ ()
+}
+
+val test : bits(2) -> unit effect {undef,escape}
+
+function test(x) = {
+ n : int = undefined;
+ match x {
+ 0b00 => n = 1,
+ 0b01 => n = 2,
+ 0b10 => n = 4,
+ 0b11 => ()
+ };
+ let 'n2 = ex_int(n) in {
+ assert(constraint('n2 >= 0));
+ needssize(n2)
+ }
+}
+
+val run : unit -> unit effect {undef,escape}
+
+function run () = {
+ test(0b00);
+ test(0b01);
+ test(0b10);
+ test(0b11);
+} \ No newline at end of file
diff --git a/test/mono/feature.sail b/test/mono/feature.sail
new file mode 100644
index 00000000..c7e13e11
--- /dev/null
+++ b/test/mono/feature.sail
@@ -0,0 +1,49 @@
+$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 mult_int = {ocaml: "mult", lem: "integerMult"} : (int, int) -> int
+overload operator * = {mult_range, mult_int, mult_real}
+val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
+overload operator < = {lt_atom, lt_int}
+val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
+val extzv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure
+function extzv(v) = extz_vec(sizeof('m),v)
+val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append"} : forall ('n : Int) ('m : Int).
+ (bits('n), bits('m)) -> bits('n + 'm)
+overload append = {bitvector_concat}
+val bitvector_cast = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
+val bitvector_length = "length" : forall 'n. bits('n) -> atom('n)
+overload length = {bitvector_length}
+
+/* Inlining feature test functions, as in aarch64 */
+
+val HaveSomeFeature : unit -> bool
+
+function HaveSomeFeature () = return(true)
+
+val foo : bits(1) -> unit effect {escape, undef}
+
+function foo(x) = {
+ let i : int =
+ match x {
+ 0b0 => 8,
+ 0b1 => if HaveSomeFeature() then 16 else undefined
+ }
+ in
+ let 'n = i in {
+ assert(constraint('n >= 0));
+ let y : bits('n) = replicate_bits(0b0, n) in
+ ()
+ }
+}
+
+val run : unit -> unit effect {escape, undef}
+
+function run () = {
+ foo(0b0);
+ foo(0b1);
+} \ No newline at end of file
diff --git a/test/mono/test.sh b/test/mono/test.sh
index 7af2e93e..5bf72828 100755
--- a/test/mono/test.sh
+++ b/test/mono/test.sh
@@ -27,10 +27,10 @@ while read -u 3 TEST ARGS; do
echo "$TEST lem - ocaml" | tee -a -- "$LOG"
rm -f -- "$OUTDIR"/*
- "$SAILDIR/sail" -lem -lem_mwords "$DIR/$TEST".sail -o "$OUTDIR/testout" $ARGS $@ &>> "$LOG" && \
- "$LEMDIR/bin/lem" -ocaml -lib "$SAILDIR/src/lem_interp" "$SAILDIR/src/gen_lib/sail_values.lem" "$SAILDIR/src/gen_lib/sail_operators.lem" "$SAILDIR/src/gen_lib/sail_operators_mwords.lem" "$SAILDIR/src/lem_interp/sail_instr_kinds.lem" "$SAILDIR/src/gen_lib/prompt.lem" "$SAILDIR/src/gen_lib/state_monad.lem" "$SAILDIR/src/gen_lib/state.lem" "$SAILDIR/src/gen_lib/prompt_monad.lem" testout_types.lem testout.lem -outdir "$OUTDIR" &>> "$LOG" && \
+ "$SAILDIR/sail" -lem -lem_mwords -lem_lib Test_extra "$DIR/$TEST".sail -o "$OUTDIR/testout" $ARGS $@ &>> "$LOG" && \
+ "$LEMDIR/bin/lem" -ocaml -lib "$SAILDIR/src/lem_interp" "$SAILDIR/src/gen_lib/sail_values.lem" "$SAILDIR/src/gen_lib/sail_operators.lem" "$SAILDIR/src/gen_lib/sail_operators_mwords.lem" "$SAILDIR/src/lem_interp/sail_instr_kinds.lem" "$SAILDIR/src/gen_lib/prompt.lem" "$SAILDIR/src/gen_lib/state_monad.lem" "$SAILDIR/src/gen_lib/state.lem" "$SAILDIR/src/gen_lib/prompt_monad.lem" "$DIR/test_extra.lem" testout_types.lem testout.lem -outdir "$OUTDIR" &>> "$LOG" && \
cp -- "$DIR"/test.ml "$OUTDIR" && \
- ocamlfind ocamlc -linkpkg -package zarith -package lem sail_values.ml sail_operators.ml sail_operators_mwords.ml sail_instr_kinds.ml prompt_monad.ml prompt.ml state_monad.ml state.ml testout_types.ml testout.ml test.ml -o test &>> "$LOG" && \
+ ocamlfind ocamlc -linkpkg -package zarith -package lem sail_values.ml sail_operators.ml sail_operators_mwords.ml sail_instr_kinds.ml prompt_monad.ml prompt.ml state_monad.ml state.ml test_extra.ml testout_types.ml testout.ml test.ml -o test &>> "$LOG" && \
./test |& tee -a -- "$LOG" || \
(echo "Failed:"; echo; tail -- "$LOG"; echo; echo)
fi
diff --git a/test/mono/tests b/test/mono/tests
index 8f2c346d..f5d5306b 100644
--- a/test/mono/tests
+++ b/test/mono/tests
@@ -8,3 +8,13 @@ vector -auto_mono
union-exist -auto_mono
set -auto_mono
assert -auto_mono
+assert2 -auto_mono
+atomsplit -auto_mono
+castreq -auto_mono -undefined_gen
+control_deps -auto_mono
+exint -auto_mono -undefined_gen
+feature -auto_mono -undefined_gen -no_effects
+feature -auto_mono -undefined_gen
+times8div8 -auto_mono -undefined_gen
+times8 -auto_mono
+times8 -auto_mono -dmono_continue -dall_split_errors
diff --git a/test/mono/times8.sail b/test/mono/times8.sail
new file mode 100644
index 00000000..56b1d209
--- /dev/null
+++ b/test/mono/times8.sail
@@ -0,0 +1,42 @@
+$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 mult_int = {ocaml: "mult", lem: "integerMult"} : (int, int) -> int
+overload operator * = {mult_range, mult_int, mult_real}
+val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
+overload operator < = {lt_atom, lt_int}
+val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
+val extzv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure
+function extzv(v) = extz_vec(sizeof('m),v)
+val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append"} : forall ('n : Int) ('m : Int).
+ (bits('n), bits('m)) -> bits('n + 'm)
+overload append = {bitvector_concat}
+val bitvector_cast = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
+val bitvector_length = "length" : forall 'n. bits('n) -> atom('n)
+overload length = {bitvector_length}
+val cast ex_int : int -> {'n, true. atom('n)}
+function ex_int 'n = n
+
+/* Another byte/bit size conversion */
+
+val bar : forall 'n. atom('n) -> bits(8 * 'n) effect pure
+
+function bar (n) = replicate_bits(0x12,n)
+
+val foo : forall 'size, 8 * 'size >= 0. atom('size) -> bits(8 * 'size) effect {escape}
+
+function foo(size) = {
+ assert('size == 1 | 'size == 2, "size");
+ return bar('size)
+}
+
+val run : unit -> unit effect {escape}
+
+function run () = {
+ assert(foo(1) == 0x12);
+ assert(foo(2) == 0x1212);
+} \ No newline at end of file
diff --git a/test/mono/times8div8.sail b/test/mono/times8div8.sail
new file mode 100644
index 00000000..240bbfc6
--- /dev/null
+++ b/test/mono/times8div8.sail
@@ -0,0 +1,66 @@
+$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 mult_int = {ocaml: "mult", lem: "integerMult"} : (int, int) -> int
+overload operator * = {mult_range, mult_int, mult_real}
+val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
+overload operator < = {lt_atom, lt_int}
+val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
+val extzv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure
+function extzv(v) = extz_vec(sizeof('m),v)
+val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append"} : forall ('n : Int) ('m : Int).
+ (bits('n), bits('m)) -> bits('n + 'm)
+overload append = {bitvector_concat}
+val bitvector_cast = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
+val bitvector_length = "length" : forall 'n. bits('n) -> atom('n)
+overload length = {bitvector_length}
+val cast ex_int : int -> {'n, true. atom('n)}
+function ex_int 'n = n
+val quotient = {ocaml: "quotient", lem: "integerDiv", c: "div_int"} : (int, int) -> int
+overload operator / = {quotient}
+
+/* Byte/bits size conversions are a pain */
+
+val accept : forall 'n. (atom('n), bits(8 * 'n)) -> unit
+
+function accept (_,_) = ()
+
+val f : forall 'n. atom('n) -> unit effect {escape,undef}
+
+function f(n) = {
+ assert(constraint('n in {8,16}));
+ x : bits('n) = undefined;
+ let 'm : {'o, true. atom('o)} = ex_int(n / 8) in {
+ assert(constraint(8 * 'm = 'n));
+ x = replicate_bits(0b00000000,'m);
+ accept(m,x);
+ accept(m,replicate_bits(0b00000000,'m));
+ }
+}
+
+val accept2 : forall 'n. bits('n) -> unit
+
+function accept2 (_) = ()
+
+val g : forall 'm 'n. (atom('m), atom('n), bits('n)) -> unit effect {escape}
+
+function g(m,n,v) = {
+ assert(constraint('m >= 0 & 'n >= 0));
+ let 'o : {'p, true. atom('p)} = ex_int(m / n) in {
+ assert(constraint('o * 'n = 'm));
+ accept2(replicate_bits(v,o))
+ }
+}
+
+val run : unit -> unit effect {escape, undef}
+
+function run () = {
+ f(8);
+ f(16);
+ g(16,8,0x12);
+ g(32,32,0x12345678);
+}
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-15 16:12:43 +0000