diff options
| -rw-r--r-- | lib/ocaml_rts/sail_lib.ml | 4 | ||||
| -rw-r--r-- | test/ocaml/sail_lib.ml | 169 | ||||
| -rw-r--r-- | test/ocaml/vec_32_64/expect | 2 | ||||
| -rw-r--r-- | test/ocaml/vec_32_64/vec_32_64.sail | 28 | ||||
| -rw-r--r-- | test/typecheck/fail/ex_cast.sail | 12 |
5 files changed, 44 insertions, 171 deletions
diff --git a/lib/ocaml_rts/sail_lib.ml b/lib/ocaml_rts/sail_lib.ml index e3a77edf..292f187e 100644 --- a/lib/ocaml_rts/sail_lib.ml +++ b/lib/ocaml_rts/sail_lib.ml @@ -439,10 +439,10 @@ let real_of_string str = let sqrt_real x = real_of_string (string_of_float (sqrt (Num.float_of_num x))) let print_int (str, x) = - prerr_endline (str ^ string_of_big_int x) + print_endline (str ^ string_of_big_int x) let print_bits (str, xs) = - prerr_endline (str ^ string_of_bits xs) + print_endline (str ^ string_of_bits xs) let reg_deref r = !r diff --git a/test/ocaml/sail_lib.ml b/test/ocaml/sail_lib.ml deleted file mode 100644 index e287eadb..00000000 --- a/test/ocaml/sail_lib.ml +++ /dev/null @@ -1,169 +0,0 @@ -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/vec_32_64/expect b/test/ocaml/vec_32_64/expect new file mode 100644 index 00000000..4d4fce36 --- /dev/null +++ b/test/ocaml/vec_32_64/expect @@ -0,0 +1,2 @@ +xs = 0x00000000 +zeros(64) = 0x0000000000000000 diff --git a/test/ocaml/vec_32_64/vec_32_64.sail b/test/ocaml/vec_32_64/vec_32_64.sail new file mode 100644 index 00000000..eb518515 --- /dev/null +++ b/test/ocaml/vec_32_64/vec_32_64.sail @@ -0,0 +1,28 @@ +(* This example is more testing the typechecker flow typing rather +than the ocaml backend, but it does test that recursive functions work +correctly *) + +val get_size : unit -> {|32, 64|} + +function get_size () = 32 + +val only64 = { ocaml: "(fun _ -> ())" } : bits(64) -> unit + +val zeros : forall 'n. atom('n) -> vector('n - 1, 'n, dec, bit) + +function zeros n = + if (n == 1 + 0) then 0b0 else 0b0 @ zeros('n - 1) + +val main : unit -> unit + +function main () = { + let 'length = get_size (); + let xs = zeros(length); + if (length == 32) then { + () + } else { + only64(xs) + }; + print_bits("xs = ", xs); + print_bits("zeros(64) = ", zeros(64)) +}
\ No newline at end of file diff --git a/test/typecheck/fail/ex_cast.sail b/test/typecheck/fail/ex_cast.sail new file mode 100644 index 00000000..5ea22d14 --- /dev/null +++ b/test/typecheck/fail/ex_cast.sail @@ -0,0 +1,12 @@ + +default Order dec + +val cast int -> exist 'n. [:'n:] effect pure ex_int + +val [:'n:] -> bit['n] effect pure zeros + +val int -> unit effect pure test + +function test n = { + x := zeros(n) +} |