summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lib/_tags2
-rw-r--r--lib/main.ml70
-rw-r--r--riscv/prelude.sail32
-rw-r--r--riscv/riscv_types.sail71
-rw-r--r--src/interpreter.ml4
-rw-r--r--src/ocaml_backend.ml3
-rw-r--r--src/sail_lib.ml21
-rw-r--r--src/value.ml10
-rw-r--r--test/ocaml/bitfield/test.isail6
-rw-r--r--test/ocaml/hello_world/test.isail6
-rw-r--r--test/ocaml/loop/test.isail4
-rw-r--r--test/ocaml/lsl/test.isail4
-rw-r--r--test/ocaml/pattern1/test.isail4
-rw-r--r--test/ocaml/reg_alias/test.isail6
-rw-r--r--test/ocaml/reg_passing/test.isail6
-rw-r--r--test/ocaml/reg_ref/test.isail6
-rw-r--r--test/ocaml/short_circuit/test.isail6
-rw-r--r--test/ocaml/string_equality/test.isail6
-rw-r--r--test/ocaml/trycatch/test.isail6
-rw-r--r--test/ocaml/types/test.isail6
-rw-r--r--test/ocaml/vec_32_64/test.isail6
-rw-r--r--test/ocaml/void/test.isail6
-rwxr-xr-xtest/riscv/run_tests.sh2
23 files changed, 258 insertions, 35 deletions
diff --git a/lib/_tags b/lib/_tags
new file mode 100644
index 00000000..b1a8186f
--- /dev/null
+++ b/lib/_tags
@@ -0,0 +1,2 @@
+<*.m{l,li}>: package(lem), package(linksem), package(zarith), package(uint)
+<main.native>: package(lem), package(linksem), package(zarith), package(uint) \ No newline at end of file
diff --git a/lib/main.ml b/lib/main.ml
new file mode 100644
index 00000000..5733425f
--- /dev/null
+++ b/lib/main.ml
@@ -0,0 +1,70 @@
+
+(**************************************************************************)
+(* Sail *)
+(* *)
+(* Copyright (c) 2013-2017 *)
+(* Kathyrn Gray *)
+(* Shaked Flur *)
+(* Stephen Kell *)
+(* Gabriel Kerneis *)
+(* Robert Norton-Wright *)
+(* Christopher Pulte *)
+(* Peter Sewell *)
+(* Alasdair Armstrong *)
+(* Brian Campbell *)
+(* Thomas Bauereiss *)
+(* Anthony Fox *)
+(* Jon French *)
+(* Dominic Mulligan *)
+(* Stephen Kell *)
+(* Mark Wassell *)
+(* *)
+(* All rights reserved. *)
+(* *)
+(* This software was developed by the University of Cambridge Computer *)
+(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *)
+(* (REMS) project, funded by EPSRC grant EP/K008528/1. *)
+(* *)
+(* Redistribution and use in source and binary forms, with or without *)
+(* modification, are permitted provided that the following conditions *)
+(* are met: *)
+(* 1. Redistributions of source code must retain the above copyright *)
+(* notice, this list of conditions and the following disclaimer. *)
+(* 2. Redistributions in binary form must reproduce the above copyright *)
+(* notice, this list of conditions and the following disclaimer in *)
+(* the documentation and/or other materials provided with the *)
+(* distribution. *)
+(* *)
+(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *)
+(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *)
+(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *)
+(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *)
+(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *)
+(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *)
+(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *)
+(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *)
+(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *)
+(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *)
+(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *)
+(* SUCH DAMAGE. *)
+(**************************************************************************)
+
+open Elf_loader;;
+
+let opt_file_arguments = ref ([] : string list)
+
+let options = Arg.align []
+
+let usage_msg = "Sail OCaml RTS options:"
+
+let () =
+ Arg.parse options (fun s -> opt_file_arguments := !opt_file_arguments @ [s]) usage_msg
+
+let () =
+ Random.self_init ();
+ begin
+ match !opt_file_arguments with
+ | f :: _ -> load_elf f
+ | _ -> ()
+ end;
+ (* ocaml_backend.ml will append from here *)
diff --git a/riscv/prelude.sail b/riscv/prelude.sail
index ff11cf7e..c8fdd467 100644
--- a/riscv/prelude.sail
+++ b/riscv/prelude.sail
@@ -142,10 +142,10 @@ val real_power = "real_power" : (real, int) -> real
overload operator ^ = {xor_vec, int_power, real_power}
-val add_range = "add" : forall 'n 'm 'o 'p.
+val add_range = "add_int" : forall 'n 'm 'o 'p.
(range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p)
-val add_int = "add" : (int, int) -> int
+val add_int = "add_int" : (int, int) -> int
val add_vec = "add_vec" : forall 'n. (bits('n), bits('n)) -> bits('n)
@@ -155,10 +155,10 @@ val add_real = "add_real" : (real, real) -> real
overload operator + = {add_range, add_int, add_vec, add_vec_int, add_real}
-val sub_range = "sub" : forall 'n 'm 'o 'p.
+val sub_range = "sub_int" : forall 'n 'm 'o 'p.
(range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o)
-val sub_int = "sub" : (int, int) -> int
+val sub_int = "sub_int" : (int, int) -> int
val "sub_vec" : forall 'n. (bits('n), bits('n)) -> bits('n)
@@ -256,13 +256,19 @@ overload min = {min_nat, min_int}
overload max = {max_nat, max_int}
val __WriteRAM = "write_ram" : forall 'n 'm.
- (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> unit
+ (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> unit effect {wmv}
+
+val __RISCV_write : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv}
+function __RISCV_write (addr, width, data) = __WriteRAM(64, width, 0x0000_0000_0000_0000, addr, data)
val __TraceMemoryWrite : forall 'n 'm.
(atom('n), bits('m), bits(8 * 'n)) -> unit
val __ReadRAM = "read_ram" : forall 'n 'm.
- (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n)
+ (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
+
+val __RISCV_read : forall 'n. (bits(64), atom('n)) -> bits(8 * 'n) effect {rmem}
+function __RISCV_read (addr, width) = __ReadRAM(64, width, 0x0000_0000_0000_0000, addr)
val __TraceMemoryRead : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit
@@ -302,9 +308,15 @@ union exception = {
Error_EBREAK,
}
+val "sign_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
+val "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
+
val EXTS : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m)
val EXTZ : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m)
+function EXTS v = sign_extend(v, sizeof('m))
+function EXTZ v = zero_extend(v, sizeof('m))
+
infix 4 <_s
infix 4 >=_s
infix 4 <_u
@@ -325,7 +337,9 @@ and bit_to_bool bitzero = false
infix 7 >>
infix 7 <<
-val operator >> : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
-val operator << : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
+val operator >> = "shift_bits_right" : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
+val operator << = "shift_bits_left" : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
+
+val vector64 : int -> bits(64)
-val vector64 : int -> bits(64) \ No newline at end of file
+function vector64 n = __raw_GetSlice_int(64, n, 0) \ No newline at end of file
diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail
index cb2ea794..8673785c 100644
--- a/riscv/riscv_types.sail
+++ b/riscv/riscv_types.sail
@@ -72,12 +72,19 @@ function wGPR (r, v) =
function check_alignment (addr : bits(64), width : atom('n)) -> forall 'n. unit =
if unsigned(addr) % width != 0 then throw(Error_misaligned_access) else ()
-val "MEMr" : forall 'n. (bits(64), atom('n)) -> bits(8 * 'n) effect {rmem}
-val "MEMr_acquire" : forall 'n. (bits(64), atom('n)) -> bits(8 * 'n) effect {rmem}
-val "MEMr_strong_acquire" : forall 'n. (bits(64), atom('n)) -> bits(8 * 'n) effect {rmem}
-val "MEMr_reserved" : forall 'n. (bits(64), atom('n)) -> bits(8 * 'n) effect {rmem}
-val "MEMr_reserved_acquire" : forall 'n. (bits(64), atom('n)) -> bits(8 * 'n) effect {rmem}
-val "MEMr_reserved_strong_acquire" : forall 'n. (bits(64), atom('n)) -> bits(8 * 'n) effect {rmem}
+val MEMr : forall 'n. (bits(64), atom('n)) -> bits(8 * 'n) effect {rmem}
+val MEMr_acquire : forall 'n. (bits(64), atom('n)) -> bits(8 * 'n) effect {rmem}
+val MEMr_strong_acquire : forall 'n. (bits(64), atom('n)) -> bits(8 * 'n) effect {rmem}
+val MEMr_reserved : forall 'n. (bits(64), atom('n)) -> bits(8 * 'n) effect {rmem}
+val MEMr_reserved_acquire : forall 'n. (bits(64), atom('n)) -> bits(8 * 'n) effect {rmem}
+val MEMr_reserved_strong_acquire : forall 'n. (bits(64), atom('n)) -> bits(8 * 'n) effect {rmem}
+
+function MEMr (addr, width) = __RISCV_read(addr, width)
+function MEMr_acquire (addr, width) = __RISCV_read(addr, width)
+function MEMr_strong_acquire (addr, width) = __RISCV_read(addr, width)
+function MEMr_reserved (addr, width) = __RISCV_read(addr, width)
+function MEMr_reserved_acquire (addr, width) = __RISCV_read(addr, width)
+function MEMr_reserved_strong_acquire (addr, width) = __RISCV_read(addr, width)
val mem_read : forall 'n. (bits(64), atom('n), bool, bool, bool) -> bits(8 * 'n) effect {rmem, escape}
@@ -96,12 +103,21 @@ function mem_read (addr, width, aq, rl, res) = {
}
}
-val "MEMea" : forall 'n. (bits(64), atom('n)) -> unit effect {eamem}
-val "MEMea_release" : forall 'n. (bits(64), atom('n)) -> unit effect {eamem}
-val "MEMea_strong_release" : forall 'n. (bits(64), atom('n)) -> unit effect {eamem}
-val "MEMea_conditional" : forall 'n. (bits(64), atom('n)) -> unit effect {eamem}
-val "MEMea_conditional_release" : forall 'n. (bits(64), atom('n)) -> unit effect {eamem}
-val "MEMea_conditional_strong_release" : forall 'n. (bits(64), atom('n)) -> unit effect {eamem}
+val MEMea : forall 'n. (bits(64), atom('n)) -> unit effect {eamem}
+val MEMea_release : forall 'n. (bits(64), atom('n)) -> unit effect {eamem}
+val MEMea_strong_release : forall 'n. (bits(64), atom('n)) -> unit effect {eamem}
+val MEMea_conditional : forall 'n. (bits(64), atom('n)) -> unit effect {eamem}
+val MEMea_conditional_release : forall 'n. (bits(64), atom('n)) -> unit effect {eamem}
+val MEMea_conditional_strong_release : forall 'n. (bits(64), atom('n)) -> unit effect {eamem}
+
+val eamem_effect = "skip" : unit -> unit effect {eamem}
+
+function MEMea _ = { eamem_effect(); () }
+function MEMea_release _ = { eamem_effect(); () }
+function MEMea_strong_release _ = { eamem_effect(); () }
+function MEMea_conditional _ = { eamem_effect(); () }
+function MEMea_conditional_release _ = { eamem_effect(); () }
+function MEMea_conditional_strong_release _ = { eamem_effect(); () }
val mem_write_ea : forall 'n. (bits(64), atom('n), bool, bool, bool) -> unit effect {eamem, escape}
@@ -120,12 +136,19 @@ function mem_write_ea (addr, width, aq, rl, con) = {
}
}
-val "MEMval" : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv}
-val "MEMval_release" : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv}
-val "MEMval_strong_release" : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv}
-val "MEMval_conditional" : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv}
-val "MEMval_conditional_release" : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv}
-val "MEMval_conditional_strong_release" : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv}
+val MEMval : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv}
+val MEMval_release : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv}
+val MEMval_strong_release : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv}
+val MEMval_conditional : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv}
+val MEMval_conditional_release : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv}
+val MEMval_conditional_strong_release : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv}
+
+function MEMval (addr, width, data) = __RISCV_write(addr, width, data)
+function MEMval_release (addr, width, data) = __RISCV_write(addr, width, data)
+function MEMval_strong_release (addr, width, data) = __RISCV_write(addr, width, data)
+function MEMval_conditional (addr, width, data) = __RISCV_write(addr, width, data)
+function MEMval_conditional_release (addr, width, data) = __RISCV_write(addr, width, data)
+function MEMval_conditional_strong_release (addr, width, data) = __RISCV_write(addr, width, data)
val mem_write_value : forall 'n. (bits(64), atom('n), bits(8 * 'n), bool, bool, bool) -> unit effect {wmv, escape}
@@ -146,12 +169,12 @@ function mem_write_value (addr, width, value, aq, rl, con) = {
val "speculate_conditional_success" : unit -> bool effect {exmem}
-val "MEM_fence_rw_rw" : unit -> unit effect {barr}
-val "MEM_fence_r_rw" : unit -> unit effect {barr}
-val "MEM_fence_r_r" : unit -> unit effect {barr}
-val "MEM_fence_rw_w" : unit -> unit effect {barr}
-val "MEM_fence_w_w" : unit -> unit effect {barr}
-val "MEM_fence_i" : unit -> unit effect {barr}
+val MEM_fence_rw_rw = "skip" : unit -> unit effect {barr}
+val MEM_fence_r_rw = "skip" : unit -> unit effect {barr}
+val MEM_fence_r_r = "skip" : unit -> unit effect {barr}
+val MEM_fence_rw_w = "skip" : unit -> unit effect {barr}
+val MEM_fence_w_w = "skip" : unit -> unit effect {barr}
+val MEM_fence_i = "skip" : unit -> unit effect {barr}
enum uop = {RISCV_LUI, RISCV_AUIPC} /* upper immediate ops */
enum bop = {RISCV_BEQ, RISCV_BNE, RISCV_BLT, RISCV_BGE, RISCV_BLTU, RISCV_BGEU} /* branch ops */
diff --git a/src/interpreter.ml b/src/interpreter.ml
index 1a8cad90..599a83bf 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -105,6 +105,10 @@ let value_of_lit (L_aux (l_aux, _)) =
|> List.map (fun c -> List.map (fun b -> V_bit b) (Sail_lib.hex_char c))
|> List.concat
|> (fun v -> V_vector v)
+ | L_bin str ->
+ Util.string_to_list str
+ |> List.map (fun c -> V_bit (Sail_lib.bin_char c))
+ |> (fun v -> V_vector v)
| _ -> failwith "Unimplemented value_of_lit" (* TODO *)
let is_value = function
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 2a6206d4..970dea83 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -195,7 +195,8 @@ let rec ocaml_pat ctx (P_aux (pat_aux, _) as pat) =
match Env.lookup_id id (pat_env_of pat) with
| Local (Immutable, _) | Unbound -> zencode ctx id
| Enum _ -> zencode_upper ctx id
- | _ -> failwith "Ocaml: Cannot pattern match on mutable variable or register"
+ | Union _ -> zencode_upper ctx id
+ | _ -> failwith ("Ocaml: Cannot pattern match on mutable variable or register:" ^ string_of_pat pat)
end
| P_lit lit -> ocaml_lit lit
| P_typ (_, pat) -> ocaml_pat ctx pat
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index 08b8ac1a..86c12aae 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -255,6 +255,11 @@ let get_slice_int (n, m, o) =
assert (Big_int.equal (Big_int.of_int (List.length slice)) n);
slice
+let bin_char = function
+ | '0' -> B0
+ | '1' -> B1
+ | _ -> failwith "Invalid binary character"
+
let hex_char = function
| '0' -> [B0; B0; B0; B0]
| '1' -> [B0; B0; B0; B1]
@@ -479,8 +484,24 @@ let rec string_of_list sep string_of = function
| [x] -> string_of x
| x::ls -> (string_of x) ^ sep ^ (string_of_list sep string_of ls)
+let skip () = ()
+
let zero_extend (vec, n) =
let m = Big_int.to_int n in
if m <= List.length vec
then take m vec
else replicate_bits ([B0], Big_int.of_int (m - List.length vec)) @ vec
+
+
+let sign_extend (vec, n) =
+ let m = Big_int.to_int n in
+ match vec with
+ | B0 :: _ as vec -> replicate_bits ([B0], Big_int.of_int (m - List.length vec)) @ vec
+ | [] -> replicate_bits ([B0], Big_int.of_int (m - List.length vec)) @ vec
+ | B1 :: _ as vec -> replicate_bits ([B1], Big_int.of_int (m - List.length vec)) @ vec
+
+(* FIXME *)
+let shift_bits_right (x, y) = x
+let shift_bits_left (x, y) = x
+
+let speculate_conditional_success () = true
diff --git a/src/value.ml b/src/value.ml
index b1f6f80b..0b50ee1f 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -328,6 +328,14 @@ let rec string_of_value = function
| V_record record ->
"{" ^ Util.string_of_list ", " (fun (field, v) -> field ^ "=" ^ string_of_value v) (StringMap.bindings record) ^ "}"
+let value_sign_extend = function
+ | [v1; v2] -> mk_vector (Sail_lib.sign_extend (coerce_bv v1, coerce_int v2))
+ | _ -> failwith "value sign_extend"
+
+let value_zero_extend = function
+ | [v1; v2] -> mk_vector (Sail_lib.zero_extend (coerce_bv v1, coerce_int v2))
+ | _ -> failwith "value zero_extend"
+
let eq_value v1 v2 = string_of_value v1 = string_of_value v2
let value_eq_anything = function
@@ -407,6 +415,8 @@ let primops =
("set_slice_int", value_set_slice_int);
("set_slice", value_set_slice);
("hex_slice", value_hex_slice);
+ ("zero_extend", value_zero_extend);
+ ("sign_extend", value_sign_extend);
("add_int", value_add_int);
("sub_int", value_sub_int);
("mult", value_mult);
diff --git a/test/ocaml/bitfield/test.isail b/test/ocaml/bitfield/test.isail
new file mode 100644
index 00000000..b3eb5d41
--- /dev/null
+++ b/test/ocaml/bitfield/test.isail
@@ -0,0 +1,6 @@
+initialize_registers()
+:run
+:output result
+main()
+:run
+:quit \ No newline at end of file
diff --git a/test/ocaml/hello_world/test.isail b/test/ocaml/hello_world/test.isail
new file mode 100644
index 00000000..b3eb5d41
--- /dev/null
+++ b/test/ocaml/hello_world/test.isail
@@ -0,0 +1,6 @@
+initialize_registers()
+:run
+:output result
+main()
+:run
+:quit \ No newline at end of file
diff --git a/test/ocaml/loop/test.isail b/test/ocaml/loop/test.isail
new file mode 100644
index 00000000..6a9595e3
--- /dev/null
+++ b/test/ocaml/loop/test.isail
@@ -0,0 +1,4 @@
+:output result
+main()
+:run
+:quit \ No newline at end of file
diff --git a/test/ocaml/lsl/test.isail b/test/ocaml/lsl/test.isail
new file mode 100644
index 00000000..6a9595e3
--- /dev/null
+++ b/test/ocaml/lsl/test.isail
@@ -0,0 +1,4 @@
+:output result
+main()
+:run
+:quit \ No newline at end of file
diff --git a/test/ocaml/pattern1/test.isail b/test/ocaml/pattern1/test.isail
new file mode 100644
index 00000000..6a9595e3
--- /dev/null
+++ b/test/ocaml/pattern1/test.isail
@@ -0,0 +1,4 @@
+:output result
+main()
+:run
+:quit \ No newline at end of file
diff --git a/test/ocaml/reg_alias/test.isail b/test/ocaml/reg_alias/test.isail
new file mode 100644
index 00000000..b3eb5d41
--- /dev/null
+++ b/test/ocaml/reg_alias/test.isail
@@ -0,0 +1,6 @@
+initialize_registers()
+:run
+:output result
+main()
+:run
+:quit \ No newline at end of file
diff --git a/test/ocaml/reg_passing/test.isail b/test/ocaml/reg_passing/test.isail
new file mode 100644
index 00000000..b3eb5d41
--- /dev/null
+++ b/test/ocaml/reg_passing/test.isail
@@ -0,0 +1,6 @@
+initialize_registers()
+:run
+:output result
+main()
+:run
+:quit \ No newline at end of file
diff --git a/test/ocaml/reg_ref/test.isail b/test/ocaml/reg_ref/test.isail
new file mode 100644
index 00000000..b3eb5d41
--- /dev/null
+++ b/test/ocaml/reg_ref/test.isail
@@ -0,0 +1,6 @@
+initialize_registers()
+:run
+:output result
+main()
+:run
+:quit \ No newline at end of file
diff --git a/test/ocaml/short_circuit/test.isail b/test/ocaml/short_circuit/test.isail
new file mode 100644
index 00000000..b3eb5d41
--- /dev/null
+++ b/test/ocaml/short_circuit/test.isail
@@ -0,0 +1,6 @@
+initialize_registers()
+:run
+:output result
+main()
+:run
+:quit \ No newline at end of file
diff --git a/test/ocaml/string_equality/test.isail b/test/ocaml/string_equality/test.isail
new file mode 100644
index 00000000..b3eb5d41
--- /dev/null
+++ b/test/ocaml/string_equality/test.isail
@@ -0,0 +1,6 @@
+initialize_registers()
+:run
+:output result
+main()
+:run
+:quit \ No newline at end of file
diff --git a/test/ocaml/trycatch/test.isail b/test/ocaml/trycatch/test.isail
new file mode 100644
index 00000000..b3eb5d41
--- /dev/null
+++ b/test/ocaml/trycatch/test.isail
@@ -0,0 +1,6 @@
+initialize_registers()
+:run
+:output result
+main()
+:run
+:quit \ No newline at end of file
diff --git a/test/ocaml/types/test.isail b/test/ocaml/types/test.isail
new file mode 100644
index 00000000..b3eb5d41
--- /dev/null
+++ b/test/ocaml/types/test.isail
@@ -0,0 +1,6 @@
+initialize_registers()
+:run
+:output result
+main()
+:run
+:quit \ No newline at end of file
diff --git a/test/ocaml/vec_32_64/test.isail b/test/ocaml/vec_32_64/test.isail
new file mode 100644
index 00000000..b3eb5d41
--- /dev/null
+++ b/test/ocaml/vec_32_64/test.isail
@@ -0,0 +1,6 @@
+initialize_registers()
+:run
+:output result
+main()
+:run
+:quit \ No newline at end of file
diff --git a/test/ocaml/void/test.isail b/test/ocaml/void/test.isail
new file mode 100644
index 00000000..b3eb5d41
--- /dev/null
+++ b/test/ocaml/void/test.isail
@@ -0,0 +1,6 @@
+initialize_registers()
+:run
+:output result
+main()
+:run
+:quit \ No newline at end of file
diff --git a/test/riscv/run_tests.sh b/test/riscv/run_tests.sh
index 9430efec..5b5f67cb 100755
--- a/test/riscv/run_tests.sh
+++ b/test/riscv/run_tests.sh
@@ -61,5 +61,5 @@ fi
finish_suite "RISCV tests"
-prinf "</testsuites>\n" >> $DIR/tests.xml
+printf "</testsuites>\n" >> $DIR/tests.xml
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 10:38:21 +0000