diff options
Diffstat (limited to 'test')
25 files changed, 263 insertions, 13 deletions
diff --git a/test/ocaml/lsl/expect b/test/ocaml/lsl/expect new file mode 100644 index 00000000..c72d1eb8 --- /dev/null +++ b/test/ocaml/lsl/expect @@ -0,0 +1,4 @@ +pass +pass +pass +pass diff --git a/test/ocaml/lsl/lsl.sail b/test/ocaml/lsl/lsl.sail new file mode 100644 index 00000000..fdb9dc43 --- /dev/null +++ b/test/ocaml/lsl/lsl.sail @@ -0,0 +1,31 @@ + +val forall Num 'n, 'n >= 0. [:'n:] -> bit['n] effect pure zeros + +function zeros n = replicate_bits(0b0, sizeof 'n) + +val forall Num 'n, Num 'shift, 'n >= 0. (bit['n], [:'shift:]) -> (bit['n], bit) effect pure lslc + +function lslc (vec, shift) = { + assert(constraint('shift >= 1), "shift must be positive"); + (bit['shift + 'n]) extended := vec : zeros(shift); + (bit['n]) result := extended[sizeof 'n - 1 .. 0]; + (bit) c := extended[sizeof 'n]; + return (result, c) +} + +val forall Num 'n, Num 'shift, 'n >= 0. (bit['n], [:'shift:]) -> bit['n] effect pure lsl + +function lsl (vec, shift) = + if shift == 0 + then vec + else let (result, _) = lslc(vec, shift) in result + +val unit -> unit effect pure main + +function main () = { + print(if lsl(0b0110,1) == 0b1100 then "pass" else "fail"); + print(if lsl(0b1111,2) == 0b1100 then "pass" else "fail"); + print(if lsl(0x0F,4) == 0xF0 then "pass" else "fail"); + let (result, c) = lslc(0xF000,2) in + print(if result == 0xC000 & c == bitone then "pass" else "fail") +} diff --git a/test/ocaml/pattern1/expect b/test/ocaml/pattern1/expect new file mode 100644 index 00000000..2ae28399 --- /dev/null +++ b/test/ocaml/pattern1/expect @@ -0,0 +1 @@ +pass diff --git a/test/ocaml/pattern1/pattern.sail b/test/ocaml/pattern1/pattern.sail new file mode 100644 index 00000000..a2314adc --- /dev/null +++ b/test/ocaml/pattern1/pattern.sail @@ -0,0 +1,11 @@ + +val unit -> unit effect pure main + +function main () = { + vec := 0x4F; + switch vec { + case (0b01 : (bit[2]) x : 0xF) -> + if (x == 0b00) then print("pass") else print("x is incorrect") + case _ -> print("pattern fail") + } +} diff --git a/test/ocaml/prelude.sail b/test/ocaml/prelude.sail index 2526d109..cbe1927d 100644 --- a/test/ocaml/prelude.sail +++ b/test/ocaml/prelude.sail @@ -15,6 +15,10 @@ val extern forall Type 'a, Num 'n. vector<'n - 1, 'n, dec, 'a> -> [:'n:] effect val extern forall Num 'n, Num 'm, Num 'o (* , 'm >= 'o, 'o >= 0, 'n >= 'm + 1 *). (bit['n], [:'m:], [:'o:]) -> bit['m - ('o - 1)] effect pure vector_subrange = "subrange" +(* FIXME: rewriter shouldn't assume this exists *) +val extern forall Num 'n, Num 'm, Num 'o (* , 'm >= 'o, 'o >= 0, 'n >= 'm + 1 *). + (bit['n], [:'m:], [:'o:]) -> bit['m - ('o - 1)] effect pure bitvector_subrange_dec = "subrange" + val extern forall Num 'n, Type 'a. (vector<'n - 1, 'n, dec, 'a>, int) -> 'a effect pure vector_access = "access" val extern forall Num 'n, Type 'a. (vector<'n - 1, 'n, dec, 'a>, int, 'a) -> vector<'n - 1, 'n, dec, 'a> effect pure vector_update = "update" diff --git a/test/ocaml/run_tests.sh b/test/ocaml/run_tests.sh index d01535b6..4454aa48 100755 --- a/test/ocaml/run_tests.sh +++ b/test/ocaml/run_tests.sh @@ -2,6 +2,7 @@ set -e DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" +cd $DIR SAILDIR="$DIR/../.." RED='\033[0;31m' @@ -49,7 +50,7 @@ printf "<testsuites>\n" >> $DIR/tests.xml for i in `ls -d */`; do cd $DIR/$i; - if $SAILDIR/sail -o out -ocaml ../prelude.sail `ls *.sail`; + if $SAILDIR/sail -o out -ocaml ../prelude.sail `ls *.sail` 1> /dev/null; then ./out > result; if diff expect result; @@ -66,4 +67,6 @@ do fi done +finish_suite "Ocaml testing" + printf "</testsuites>\n" >> $DIR/tests.xml diff --git a/test/ocaml/types/expect b/test/ocaml/types/expect new file mode 100644 index 00000000..747ef4c9 --- /dev/null +++ b/test/ocaml/types/expect @@ -0,0 +1,5 @@ +pass +pass +pass +pass +pass diff --git a/test/ocaml/types/types.sail b/test/ocaml/types/types.sail new file mode 100644 index 00000000..8f50e057 --- /dev/null +++ b/test/ocaml/types/types.sail @@ -0,0 +1,44 @@ + +typedef signal = enumerate {Low; High} + +typedef enum_single = enumerate {SingleConstructor} + +typedef byte = bit[8] +typedef b32 = bit[32] +typedef b64 = bit[64] + +register b64 R64 +register b32 R32 +register byte R8 + +register signal SIGNALREG + +typedef TestStruct = const struct { + bit[2] field1; + byte field2; + bool field3 +} + +register TestStruct SREG + +typedef option = const union forall Type 'a. { + None; + 'a Some +} + +register (option<byte>) OREG + +val unit -> unit effect {rreg, wreg} main + +function main () = { + R8 := 0xFF; + SIGNALREG := Low; + print(if SIGNALREG == Low then "pass" else "fail"); + SIGNALREG := High; + print(if SIGNALREG == High then "pass" else "fail"); + SREG.field1 := 0b00; + print(if SREG.field1 == 0b00 then "pass" else "faiL"); + SREG.field1 := 0b11; + print(if SREG.field1 == 0b11 then "pass" else "faiL"); + print("pass") +} diff --git a/test/run_tests.sh b/test/run_tests.sh new file mode 100755 index 00000000..380ebb18 --- /dev/null +++ b/test/run_tests.sh @@ -0,0 +1,7 @@ +#!/usr/bin/env bash +set -e + +DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" + +$DIR/typecheck/run_tests.sh +$DIR/ocaml/run_tests.sh diff --git a/test/typecheck/fail/mismatch_return.sail b/test/typecheck/fail/mismatch_return.sail new file mode 100644 index 00000000..85b8b636 --- /dev/null +++ b/test/typecheck/fail/mismatch_return.sail @@ -0,0 +1,7 @@ + +val unit -> unit effect pure test + +function int test () = +{ + () +} diff --git a/test/typecheck/fail/pure_record_arity.sail b/test/typecheck/fail/pure_record_arity.sail new file mode 100644 index 00000000..846df2c3 --- /dev/null +++ b/test/typecheck/fail/pure_record_arity.sail @@ -0,0 +1,25 @@ +default Order dec + +typedef State = const struct forall Type 'a, Nat 'n. { + vector<0, 'n, dec, 'a> N; + vector<0, 1, dec, bit> Z; +} + +register State procState + +let (State<bit,1>) myStateM = { + (State<bit,1>) r := undefined; + r.N := 0b1; + r.Z := 0b1; + r +} + +let (State<bit,1>) myState = { N = 0b1; Z = 0b1 } + +val unit -> unit effect {undef} test + +function test () = { + (State<bit,1>) myState1 := undefined; + (State<bit,1>) myState2 := { N = undefined; Z = 0b1 }; + (State<bit,1>) myState3 := { myState2 with N = 0b0 } +} diff --git a/test/typecheck/fail/vector_append_old.sail b/test/typecheck/fail/vector_append_old.sail new file mode 100644 index 00000000..fb6018b9 --- /dev/null +++ b/test/typecheck/fail/vector_append_old.sail @@ -0,0 +1,14 @@ + +val extern forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, 'l1 >= 0, 'l2 >= 0. + (vector<'n1,'l1,'o,bit>, vector<'n2,'l2,'o,bit>) -> vector<'n1,'l1 + 'l2,'o,bit> effect pure vector_append = "bitvector_concat" + +default Order inc + +val (bit[4], bit[4]) -> bit[8] effect pure test + +function bit[8] test (v1, v2) = +{ + zv := vector_append(v1, v2); + zv := v1 : v2; + zv +} diff --git a/test/typecheck/pass/exist_subrange.sail b/test/typecheck/pass/exist_subrange.sail new file mode 100644 index 00000000..de867b75 --- /dev/null +++ b/test/typecheck/pass/exist_subrange.sail @@ -0,0 +1,12 @@ +default Order dec + +val forall Num 'n, Num 'm, Num 'o (* , 'm >= 'o, 'o >= 0, 'n >= 'm + 1 *). + (bit['n], [:'m:], [:'o:]) -> bit['m - ('o - 1)] effect pure vector_subrange + +function unit test ((bit[6]) xs) = +{ + (int) len := 4; + (exist 'n. [:'n:]) len := 5; + ys := xs[len .. 0]; + () +} diff --git a/test/typecheck/pass/exist_true.sail b/test/typecheck/pass/exist_true.sail new file mode 100644 index 00000000..a30fb87b --- /dev/null +++ b/test/typecheck/pass/exist_true.sail @@ -0,0 +1,7 @@ + +function unit test () = +{ + (exist 'n. [:'n:]) x := 4; + (exist 'n, true. [:'n:]) y := 5; + () +} diff --git a/test/typecheck/pass/lexp_memory.sail b/test/typecheck/pass/lexp_memory.sail index 83313ac7..cc84130f 100644 --- a/test/typecheck/pass/lexp_memory.sail +++ b/test/typecheck/pass/lexp_memory.sail @@ -48,7 +48,10 @@ val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'or overload (deinfix ==) [eq_vec] -val cast forall Nat 'n, Nat 'l, Order 'ord. [|0:1|] -> vector<'n,'l,'ord,bit> effect pure cast_01_vec +val extern forall Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec + +val cast forall Nat 'n, Nat 'l. [|0:1|] -> vector<'n,'l,dec,bit> effect pure cast_01_vec +function forall Num 'n, Num 'l. (vector<'n,'l,dec,bit>) cast_01_vec i = to_vec_dec (sizeof 'n, sizeof 'l, i) val cast forall Nat 'n, Nat 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [|0:2**'m - 1|] effect pure unsigned val cast forall Type 'a. register<'a> -> 'a effect {rreg} reg_deref diff --git a/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail b/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail index 7808b2c0..0160dd8a 100644 --- a/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail +++ b/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail @@ -1,5 +1,10 @@ -val cast forall Nat 'n, Order 'ord. [:1:] -> vector<'n,1,'ord,bit> effect pure cast_1_vec -val cast forall Nat 'n, Order 'ord. [:0:] -> vector<'n,1,'ord,bit> effect pure cast_0_vec +val cast forall Num 'n. [:1:] -> vector<'n,1,dec,bit> effect pure cast_1_vec +val cast forall Num 'n. [:0:] -> vector<'n,1,dec,bit> effect pure cast_0_vec + +val extern forall Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec + +function forall Num 'n. (vector<'n,1,dec,bit>) cast_1_vec i = to_vec_dec (sizeof 'n, 1, i) +function forall Num 'n. (vector<'n,1,dec,bit>) cast_0_vec i = to_vec_dec (sizeof 'n, 1, i) default Order dec diff --git a/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail b/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail index 26f161e2..847bca60 100644 --- a/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail +++ b/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail @@ -1,6 +1,11 @@ -val cast forall Nat 'n, Order 'ord. [:1:] -> vector<'n,1,'ord,bit> effect pure cast_1_vec -val cast forall Nat 'n, Order 'ord. [:0:] -> vector<'n,1,'ord,bit> effect pure cast_0_vec +val cast forall Num 'n. [:1:] -> vector<'n,1,dec,bit> effect pure cast_1_vec +val cast forall Num 'n. [:0:] -> vector<'n,1,dec,bit> effect pure cast_0_vec +val extern forall Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec + +function forall Num 'n. (vector<'n,1,dec,bit>) cast_1_vec i = to_vec_dec (sizeof 'n, 1, i) +function forall Num 'n. (vector<'n,1,dec,bit>) cast_0_vec i = to_vec_dec (sizeof 'n, 1, i) + default Order dec typedef CauseReg = register bits [ 31 : 0 ] { diff --git a/test/typecheck/pass/pure_record2.sail b/test/typecheck/pass/pure_record2.sail new file mode 100644 index 00000000..a0a85313 --- /dev/null +++ b/test/typecheck/pass/pure_record2.sail @@ -0,0 +1,22 @@ +default Order dec + +typedef State = const struct forall Type 'a, Nat 'n. { + vector<0, 'n, dec, 'a> N; + vector<0, 1, dec, bit> Z; +} + +let (State<bit,1>) myStateM = { + (State<bit,1>) r := undefined; + r.N := 0b1; + r.Z := 0b1; + r +} + +let (State<bit,1>) myState = { N = 0b1; Z = 0b1 } + +val unit -> unit effect {undef} test + +function test () = { + (State<bit,1>) myState2 := { N = undefined; Z = 0b1 }; + (State<bit,1>) myState3 := { myState2 with N = 0b0 } +} diff --git a/test/typecheck/pass/pure_record3.sail b/test/typecheck/pass/pure_record3.sail new file mode 100644 index 00000000..61d74ebf --- /dev/null +++ b/test/typecheck/pass/pure_record3.sail @@ -0,0 +1,25 @@ +default Order dec + +typedef State = const struct forall Type 'a, Nat 'n. { + vector<0, 'n, dec, 'a> N; + vector<0, 1, dec, bit> Z; +} + +register State<bit,1> procState + +let (State<bit,1>) myStateM = { + (State<bit,1>) r := undefined; + r.N := 0b1; + r.Z := 0b1; + r +} + +let (State<bit,1>) myState = { N = 0b1; Z = 0b1 } + +val unit -> unit effect {undef} test + +function test () = { + (State<bit,1>) myState1 := undefined; + (State<bit,1>) myState2 := { N = undefined; Z = 0b1 }; + (State<bit,1>) myState3 := { myState2 with N = 0b0 } +} diff --git a/test/typecheck/pass/set_mark.sail b/test/typecheck/pass/set_mark.sail index 7bc7370b..af0b5ba2 100644 --- a/test/typecheck/pass/set_mark.sail +++ b/test/typecheck/pass/set_mark.sail @@ -1,5 +1,10 @@ -val cast forall Num 'n, Num 'm, Order 'ord. [:0:] -> vector<'n,'m,'ord,bit> effect pure cast_0_vec +val extern forall Num 'l, Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec + +val cast forall Num 'n, Num 'm. [:0:] -> vector<'n,'m,dec,bit> effect pure cast_0_vec +function forall Num 'n, Num 'm. (vector<'n,'m,dec,bit>) cast_0_vec i = to_vec_dec (sizeof 'n, sizeof 'm, i) + +default Order dec function forall Num 'N, 'N IN {32}. bit['N] Foo32( (bit['N]) x) = x diff --git a/test/typecheck/pass/set_mark2.sail b/test/typecheck/pass/set_mark2.sail index cabfb1af..591c17ad 100644 --- a/test/typecheck/pass/set_mark2.sail +++ b/test/typecheck/pass/set_mark2.sail @@ -1,4 +1,10 @@ -val cast forall Num 'n, Num 'm, Order 'ord. [:0:] -> vector<'n,'m,'ord,bit> effect pure cast_0_vec + +val extern forall Num 'l, Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec + +val cast forall Num 'n, Num 'm. [:0:] -> vector<'n,'m,dec,bit> effect pure cast_0_vec +function forall Num 'n, Num 'm. (vector<'n,'m,dec,bit>) cast_0_vec i = to_vec_dec (sizeof 'n, sizeof 'm, i) + +default Order dec function forall Nat 'N, 'N IN {32, 64}. bit['N] Foo32( (bit['N]) x) = x diff --git a/test/typecheck/pass/varity.sail b/test/typecheck/pass/varity.sail index d196f777..750d70eb 100644 --- a/test/typecheck/pass/varity.sail +++ b/test/typecheck/pass/varity.sail @@ -3,6 +3,10 @@ val int -> unit effect pure f1 val (int, int) -> unit effect pure f2 val (int, int, int) -> unit effect pure f3 +function f1 (i1) = () +function f2 (i1, i2) = () +function f3 (i1, i2, i3) = () + overload f [f1; f2; f3] val unit -> unit effect pure test diff --git a/test/typecheck/pass/vec_pat1.sail b/test/typecheck/pass/vec_pat1.sail index fe9b4a0a..b22f0029 100644 --- a/test/typecheck/pass/vec_pat1.sail +++ b/test/typecheck/pass/vec_pat1.sail @@ -10,7 +10,7 @@ val forall Num 'n, Num 'm, Num 'o, Num 'p. effect pure bitvector_concat overload (deinfix +) [bv_add] -overload vector_append [bitvector_concat] +overload append [bitvector_concat] val (bit[3], bit[3]) -> bit[3] effect pure test diff --git a/test/typecheck/pass/vector_append.sail b/test/typecheck/pass/vector_append.sail index 17db3fbd..df610fb1 100644 --- a/test/typecheck/pass/vector_append.sail +++ b/test/typecheck/pass/vector_append.sail @@ -1,14 +1,14 @@ val extern forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, 'l1 >= 0, 'l2 >= 0. - (vector<'n1,'l1,'o,bit>, vector<'n2,'l2,'o,bit>) -> vector<'n1,'l1 + 'l2,'o,bit> effect pure vector_append = "bitvector_concat" + (vector<'n1,'l1,'o,bit>, vector<'n2,'l2,'o,bit>) -> vector<'n1,'l1 + 'l2,'o,bit> effect pure append = "bitvector_concat" default Order inc val (bit[4], bit[4]) -> bit[8] effect pure test - + function bit[8] test (v1, v2) = { - zv := vector_append(v1, v2); + zv := append(v1, v2); zv := v1 : v2; zv } diff --git a/test/typecheck/pass/vector_synonym_cast.sail b/test/typecheck/pass/vector_synonym_cast.sail index f1de42e9..bd0acaa6 100644 --- a/test/typecheck/pass/vector_synonym_cast.sail +++ b/test/typecheck/pass/vector_synonym_cast.sail @@ -1,7 +1,7 @@ typedef vecsyn = vector<0,1,dec,bit> -val cast vector<1,1,dec,bit> -> vector<0,1,dec,bit> effect pure adjust_dec +val cast vector<1,1,dec,bit> -> vector<0,1,dec,bit> effect pure norm_dec val vector<1,1,dec,bit> -> vecsyn effect pure test |