diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/ocaml/hello_world/expect | 2 | ||||
| -rw-r--r-- | test/ocaml/hello_world/hello_world.sail | 19 | ||||
| -rw-r--r-- | test/ocaml/prelude.sail | 138 | ||||
| -rwxr-xr-x | test/ocaml/run_tests.sh | 69 | ||||
| -rw-r--r-- | test/ocaml/sail_lib.ml | 169 | ||||
| -rw-r--r-- | test/ocaml/string_equality/expect | 1 | ||||
| -rw-r--r-- | test/ocaml/string_equality/string_equality.sail | 10 | ||||
| -rwxr-xr-x | test/typecheck/run_tests.sh | 42 |
8 files changed, 429 insertions, 21 deletions
diff --git a/test/ocaml/hello_world/expect b/test/ocaml/hello_world/expect new file mode 100644 index 00000000..3df47a31 --- /dev/null +++ b/test/ocaml/hello_world/expect @@ -0,0 +1,2 @@ +Hello, Sail! +Hello, World! diff --git a/test/ocaml/hello_world/hello_world.sail b/test/ocaml/hello_world/hello_world.sail new file mode 100644 index 00000000..d96429f2 --- /dev/null +++ b/test/ocaml/hello_world/hello_world.sail @@ -0,0 +1,19 @@ + +val unit -> string effect pure hello_world + +function hello_world () = { + return "Hello, World!"; + "Unreachable" +} + +val unit -> unit effect {wreg, rreg} main + +register string REG + +function main () = { + REG := "Hello, Sail!"; + print(REG); + REG := hello_world (); + print(REG); + return () +} diff --git a/test/ocaml/prelude.sail b/test/ocaml/prelude.sail new file mode 100644 index 00000000..2526d109 --- /dev/null +++ b/test/ocaml/prelude.sail @@ -0,0 +1,138 @@ + +default Order dec + +val extern (int, int) -> bool effect pure eq_int = "eq_int" +val extern forall 'n. (bit['n], bit['n]) -> bool effect pure eq_vec = "eq_list" +val extern (string, string) -> bool effect pure eq_string = "eq_string" +val (real, real) -> bool effect pure eq_real + +val extern forall Type 'a. ('a, 'a) -> bool effect pure eq_anything = "(fun (x, y) -> x == y)" + +overload (deinfix ==) [eq_int; eq_vec; eq_string; eq_real; eq_anything] + +val extern forall Type 'a, Num 'n. vector<'n - 1, 'n, dec, 'a> -> [:'n:] effect pure length = "length" + +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" + +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" + +val extern forall Num 'n, Num 'm, Num 'o. + (bit['n], [:'m:], [:'o:], bit['m - ('o - 1)]) -> bit['n] + effect pure vector_update_subrange = "update_subrange" + +val forall Num 'n, Type 'a. ('a, vector<'n - 1, 'n, dec, 'a>) -> vector<'n, 'n + 1, dec, 'a> effect pure vcons + +val extern forall Num 'n, Num 'm, Type 'a. (vector<'n - 1, 'n, dec, 'a>, vector<'m - 1, 'm, dec, 'a>) -> vector<('n + 'm) - 1, 'n + 'm, dec, 'a> effect pure append = "append" + +val extern bool -> bool effect pure not_bool = "not" +val extern forall 'n. bit['n] -> bit['n] effect pure not_vec = "not_vec" + +overload ~ [not_bool; not_vec] + +val forall Type 'a. ('a, 'a) -> bool effect pure neq_anything + +function neq_anything (x, y) = not_bool (x == y) + +overload (deinfix !=) [neq_anything] + +val extern (bool, bool) -> bool effect pure and_bool = "and_bool" +val extern forall 'n. (bit['n], bit['n]) -> bit['n] effect pure and_vec = "and_vec" + +overload (deinfix &) [and_bool; and_vec] + +val extern (bool, bool) -> bool effect pure or_bool = "or_bool" +val extern forall 'n. (bit['n], bit['n]) -> bit['n] effect pure or_vec = "or_vec" + +overload (deinfix |) [or_bool; or_vec] + +val extern forall 'n. bit['n] -> [|0:2**'n - 1|] effect pure UInt = "uint" + +val extern forall 'n. bit['n] -> [|- 2**('n - 1):2**('n - 1) - 1|] effect pure SInt = "sint" + +val extern string -> unit effect pure print = "print_endline" +val extern (string, string) -> string effect pure concat_str = "concat_string" +val int -> string effect pure DecStr +val int -> string effect pure HexStr + +val forall 'n. (bit['n], bit['n]) -> bit['n] effect pure xor_vec +val (int, int) -> int effect pure int_exp + +overload (deinfix ^) [xor_vec; int_exp] + +val extern forall 'n, 'm, 'o, 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range = "add" +val extern (int, int) -> int effect pure add_int = "add" +val extern forall 'n. (bit['n], bit['n]) -> bit['n] effect pure add_vec = "add_vec" +val forall 'n. (bit['n], int) -> bit['n] effect pure add_vec_int + +overload (deinfix +) [add_range; add_int; add_vec; add_vec_int] + +val extern forall 'n, 'm, 'o, 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range = "sub" +val extern (int, int) -> int effect pure sub_int = "sub" +val forall 'n. (bit['n], bit['n]) -> bit['n] effect pure sub_vec +val forall 'n. (bit['n], int) -> bit ['n] effect pure sub_vec_int + +val forall 'n. [|'n:'m|] -> [|-'m:-'n|] effect pure negate_range +val int -> int effect pure negate_int + +overload (deinfix -) [sub_range; sub_int; sub_vec; sub_vec_int] +overload negate [negate_range; negate_int] + +val extern forall 'n, 'm, 'o, 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n * 'o : 'm * 'p|] effect pure mult_range = "mult" +val extern (int, int) -> int effect pure mult_int = "mult" + +overload (deinfix * ) [mult_range; mult_int] + +val (int, int) -> bool effect pure gteq_int +val (real, real) -> bool effect pure gteq_real + +overload (deinfix >=) [gteq_int; gteq_real] + +val (int, int) -> bool effect pure lteq_int +val (real, real) -> bool effect pure lteq_real + +overload (deinfix <=) [lteq_int; lteq_real] + +val (int, int) -> bool effect pure gt_int +val (real, real) -> bool effect pure gt_real + +overload (deinfix >) [gt_int; gt_real] + +val (int, int) -> bool effect pure lt_int +val (real, real) -> bool effect pure lt_real + +overload (deinfix <) [lt_int; lt_real] + +val real -> int effect pure RoundDown +val real -> int effect pure RoundUp + +val extern (int, int) -> int effect pure quotient = "quotient" + +overload (deinfix quot) [quotient] + +val extern (int, int) -> int effect pure modulus = "modulus" + +overload (deinfix mod) [modulus] + +val extern (int, int) -> int effect pure shl_int +val extern (int, int) -> int effect pure shr_int + +val (nat, nat) -> nat effect pure min_nat +val (int, int) -> int effect pure min_int +val (nat, nat) -> nat effect pure max_nat +val (int, int) -> int effect pure max_int + +overload min [min_nat; min_int] +overload max [max_nat; max_int] + +val extern forall 'n, 'm. ([:'m:], [:'n:], bit['m], bit['m], bit[8 * 'n]) -> unit effect {wmem} __WriteRAM = "write_ram" +val extern forall 'n, 'm. ([:'m:], [:'n:], bit['m], bit['m]) -> bit[8 * 'n] effect {rmem} __ReadRAM = "read_ram" + +val extern forall 'n, 'm. (bit['n], [:'m:]) -> bit['n * 'm] effect pure replicate_bits + +val extern nat -> exist 'n, 'n >= 0. [:'n:] effect pure ex_nat = "identity" +val extern int -> exist 'n. [:'n:] effect pure ex_int = "identity" +val extern forall 'n, 'm. [|'n:'m|] -> exist 'o, 'n <= 'o & 'o <= 'm. [:'o:] effect pure ex_range = "identity" + diff --git a/test/ocaml/run_tests.sh b/test/ocaml/run_tests.sh new file mode 100755 index 00000000..d01535b6 --- /dev/null +++ b/test/ocaml/run_tests.sh @@ -0,0 +1,69 @@ +#!/usr/bin/env bash +set -e + +DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" +SAILDIR="$DIR/../.." + +RED='\033[0;31m' +GREEN='\033[0;32m' +YELLOW='\033[0;33m' +NC='\033[0m' + +rm -f $DIR/tests.xml + +pass=0 +fail=0 +XML="" + +function green { + (( pass += 1 )) + printf "$1: ${GREEN}$2${NC}\n" + XML+=" <testcase name=\"$1\"/>\n" +} + +function yellow { + (( fail += 1 )) + printf "$1: ${YELLOW}$2${NC}\n" + XML+=" <testcase name=\"$1\">\n <error message=\"$2\">$2</error>\n </testcase>\n" +} + +function red { + (( fail += 1 )) + printf "$1: ${RED}$2${NC}\n" + XML+=" <testcase name=\"$1\">\n <error message=\"$2\">$2</error>\n </testcase>\n" +} + +function finish_suite { + printf "$1: Passed ${pass} out of $(( pass + fail ))\n" + XML=" <testsuite name=\"$1\" tests=\"$(( pass + fail ))\" failures=\"${fail}\" timestamp=\"$(date)\">\n$XML </testsuite>\n" + printf "$XML" >> $DIR/tests.xml + XML="" + pass=0 + fail=0 +} + +SAILLIBDIR="$DIR" + +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`; + then + ./out > result; + if diff expect result; + then + green "built $i" "ok" + else + yellow "bad output $i" "fail" + fi; + rm out; + rm result; + rm -r _sbuild + else + red "building $i" "fail" + fi +done + +printf "</testsuites>\n" >> $DIR/tests.xml diff --git a/test/ocaml/sail_lib.ml b/test/ocaml/sail_lib.ml new file mode 100644 index 00000000..e287eadb --- /dev/null +++ b/test/ocaml/sail_lib.ml @@ -0,0 +1,169 @@ +open Big_int + +type 'a return = { return : 'b . 'a -> 'b } + +let with_return (type t) (f : _ -> t) = + let module M = + struct exception Return of t end + in + let return = { return = (fun x -> raise (M.Return x)); } in + try f return with M.Return x -> x + +type bit = B0 | B1 + +let and_bit = function + | B1, B1 -> B1 + | _, _ -> B0 + +let or_bit = function + | B0, B0 -> B0 + | _, _ -> B1 + +let and_vec (xs, ys) = + assert (List.length xs = List.length ys); + List.map2 (fun x y -> and_bit (x, y)) xs ys + +let and_bool (b1, b2) = b1 && b2 + +let or_vec (xs, ys) = + assert (List.length xs = List.length ys); + List.map2 (fun x y -> or_bit (x, y)) xs ys + +let or_bool (b1, b2) = b1 || b2 + +let undefined_bit () = + if Random.bool () then B0 else B1 + +let undefined_bool () = Random.bool () + +let rec undefined_vector (start_index, len, item) = + if eq_big_int len zero_big_int + then [] + else item :: undefined_vector (start_index, sub_big_int len unit_big_int, item) + +let undefined_string () = "" + +let undefined_unit () = () + +let undefined_int () = + big_int_of_int (Random.int 0xFFFF) + +let internal_pick list = + List.nth list (Random.int (List.length list)) + +let eq_int (n, m) = eq_big_int n m + +let eq_string (str1, str2) = String.compare str1 str2 = 0 + +let concat_string (str1, str2) = str1 ^ str2 + +let rec drop n xs = + match n, xs with + | 0, xs -> xs + | n, [] -> [] + | n, (x :: xs) -> drop (n -1) xs + +let rec take n xs = + match n, xs with + | 0, xs -> [] + | n, (x :: xs) -> x :: take (n - 1) xs + | n, [] -> [] + +let subrange (list, n, m) = + let n = int_of_big_int n in + let m = int_of_big_int m in + List.rev (take (n - (m - 1)) (drop m (List.rev list))) + +let eq_list (xs, ys) = List.for_all2 (fun x y -> x == y) xs ys + +let access (xs, n) = List.nth (List.rev xs) (int_of_big_int n) + +let append (xs, ys) = xs @ ys + +let update (xs, n, x) = + let n = int_of_big_int n in + take n xs @ [x] @ drop (n + 1) xs + +let update_subrange (xs, n, m, ys) = + let n = int_of_big_int n in + let m = int_of_big_int m in + assert false + +let length xs = big_int_of_int (List.length xs) + +let big_int_of_bit = function + | B0 -> zero_big_int + | B1 -> unit_big_int + +let uint xs = + let uint_bit x (n, pos) = + add_big_int n (mult_big_int (power_int_positive_int 2 pos) (big_int_of_bit x)), pos + 1 + in + fst (List.fold_right uint_bit xs (zero_big_int, 0)) + +let sint = function + | [] -> zero_big_int + | [msb] -> minus_big_int (big_int_of_bit msb) + | msb :: xs -> + let msb_pos = List.length xs in + let complement = + minus_big_int (mult_big_int (power_int_positive_int 2 msb_pos) (big_int_of_bit msb)) + in + add_big_int complement (uint xs) + +let add (x, y) = add_big_int x y +let sub (x, y) = sub_big_int x y +let mult (x, y) = mult_big_int x y +let quotient (x, y) = fst (quomod_big_int x y) +let modulus (x, y) = snd (quomod_big_int x y) + +let add_bit_with_carry (x, y, carry) = + match x, y, carry with + | B0, B0, B0 -> B0, B0 + | B0, B1, B0 -> B1, B0 + | B1, B0, B0 -> B1, B0 + | B1, B1, B0 -> B0, B1 + | B0, B0, B1 -> B1, B0 + | B0, B1, B1 -> B0, B1 + | B1, B0, B1 -> B0, B1 + | B1, B1, B1 -> B1, B1 + +let not_bit = function + | B0 -> B1 + | B1 -> B0 + +let not_vec xs = List.map not_bit xs + +let add_vec_carry (xs, ys) = + assert (List.length xs = List.length ys); + let (carry, result) = + List.fold_right2 (fun x y (c, result) -> let (z, c) = add_bit_with_carry (x, y, c) in (c, z :: result)) xs ys (B0, []) + in + carry, result + +let add_vec (xs, ys) = snd (add_vec_carry (xs, ys)) + +let rec replicate_bits (bits, n) = + if eq_big_int n zero_big_int + then [] + else bits @ replicate_bits (bits, sub_big_int n unit_big_int) + +let identity x = x + +let get_slice_int (n, m, o) = assert false + +let hex_slice (str, n, m) = assert false + +let putchar n = print_endline (string_of_big_int n) + +let write_ram (addr_size, data_size, hex_ram, addr, data) = + assert false + +let read_ram (addr_size, data_size, hex_ram, addr) = + assert false + +(* FIXME: Casts can't be externed *) +let zcast_unit_vec x = [x] + +let shl_int (n, m) = assert false +let shr_int (n, m) = assert false diff --git a/test/ocaml/string_equality/expect b/test/ocaml/string_equality/expect new file mode 100644 index 00000000..27ba77dd --- /dev/null +++ b/test/ocaml/string_equality/expect @@ -0,0 +1 @@ +true diff --git a/test/ocaml/string_equality/string_equality.sail b/test/ocaml/string_equality/string_equality.sail new file mode 100644 index 00000000..68629862 --- /dev/null +++ b/test/ocaml/string_equality/string_equality.sail @@ -0,0 +1,10 @@ + +val unit -> unit effect pure main + +function main () = { + if ("test" == "test") then { + print("true") + } else { + print("false") + } +} diff --git a/test/typecheck/run_tests.sh b/test/typecheck/run_tests.sh index 24f20d1f..eaa268a6 100755 --- a/test/typecheck/run_tests.sh +++ b/test/typecheck/run_tests.sh @@ -21,8 +21,8 @@ MIPS="$SAILDIR/mips_new_tc" cat $SAILDIR/lib/prelude.sail $SAILDIR/lib/prelude_wrappers.sail $MIPS/mips_prelude.sail > $DIR/pass/mips_prelude.sail cat $SAILDIR/lib/prelude.sail $SAILDIR/lib/prelude_wrappers.sail $MIPS/mips_prelude.sail $MIPS/mips_tlb.sail > $DIR/pass/mips_tlb.sail cat $SAILDIR/lib/prelude.sail $SAILDIR/lib/prelude_wrappers.sail $MIPS/mips_prelude.sail $MIPS/mips_tlb.sail $MIPS/mips_wrappers.sail > $DIR/pass/mips_wrappers.sail -cat $SAILDIR/lib/prelude.sail $SAILDIR/lib/prelude_wrappers.sail $MIPS/mips_prelude.sail $MIPS/mips_tlb.sail $MIPS/mips_wrappers.sail $MIPS/mips_insts.sail $MIPS/mips_epilogue.sail > $DIR/pass/mips_insts.sail -cat $SAILDIR/lib/prelude.sail $SAILDIR/lib/prelude_wrappers.sail $MIPS/mips_prelude.sail $MIPS/mips_tlb_stub.sail $MIPS/mips_wrappers.sail $MIPS/mips_insts.sail $MIPS/mips_epilogue.sail > $DIR/pass/mips_notlb.sail +cat $SAILDIR/lib/prelude.sail $SAILDIR/lib/prelude_wrappers.sail $MIPS/mips_prelude.sail $MIPS/mips_tlb.sail $MIPS/mips_wrappers.sail $MIPS/mips_ast_decl.sail $MIPS/mips_insts.sail $MIPS/mips_epilogue.sail > $DIR/pass/mips_insts.sail +cat $SAILDIR/lib/prelude.sail $SAILDIR/lib/prelude_wrappers.sail $MIPS/mips_prelude.sail $MIPS/mips_tlb_stub.sail $MIPS/mips_wrappers.sail $MIPS/mips_ast_decl.sail $MIPS/mips_insts.sail $MIPS/mips_epilogue.sail > $DIR/pass/mips_notlb.sail pass=0 fail=0 @@ -103,14 +103,14 @@ function test_lem { # MIPS requires an additional library, Mips_extras_embed. # It might be useful to allow adding options for specific test cases. # For now, include the library for all test cases, which doesn't seem to hurt. - if $SAILDIR/sail -lem -lem_lib Mips_extras_embed $DIR/$1/$i 2> /dev/null + if $SAILDIR/sail -lem -lem_lib Mips_extras_embed -lem_sequential -lem_mwords $DIR/$1/$i 2> /dev/null then green "generated lem for $1/$i" "pass" cp $MIPS/mips_extras_embed_sequential.lem $DIR/lem/ - mv $SAILDIR/${i%%.*}_embed_types.lem $DIR/lem/ + # mv $SAILDIR/${i%%.*}_embed_types.lem $DIR/lem/ mv $SAILDIR/${i%%.*}_embed_types_sequential.lem $DIR/lem/ - mv $SAILDIR/${i%%.*}_embed.lem $DIR/lem/ + # mv $SAILDIR/${i%%.*}_embed.lem $DIR/lem/ mv $SAILDIR/${i%%.*}_embed_sequential.lem $DIR/lem/ # Test sequential embedding for now # TODO: Add tests for the free monad @@ -135,26 +135,26 @@ test_lem rtpass finish_suite "Lem generation 2" -function test_ocaml { - for i in `ls $DIR/pass/`; - do - if $SAILDIR/sail -ocaml $DIR/$1/$i 2> /dev/null - then - green "generated ocaml for $1/$i" "pass" +# function test_ocaml { +# for i in `ls $DIR/pass/`; +# do +# if $SAILDIR/sail -ocaml $DIR/$1/$i 2> /dev/null +# then +# green "generated ocaml for $1/$i" "pass" - rm $SAILDIR/${i%%.*}.ml - else - red "generated ocaml for $1/$i" "fail" - fi - done -} +# rm $SAILDIR/${i%%.*}.ml +# else +# red "generated ocaml for $1/$i" "fail" +# fi +# done +# } -test_ocaml pass +# test_ocaml pass -finish_suite "Ocaml generation 1" +# finish_suite "Ocaml generation 1" -test_ocaml rtpass +# test_ocaml rtpass -finish_suite "Ocaml generation 2" +# finish_suite "Ocaml generation 2" printf "</testsuites>\n" >> $DIR/tests.xml |