Add ocaml run-time and updates to sail for ocaml backend

1 files changed, 68 insertions, 0 deletions

diff --git a/lib/ocaml_rts/linksem/hex_printing.ml b/lib/ocaml_rts/linksem/hex_printing.ml
new file mode 100644
index 00000000..fe2c42ca
--- /dev/null
+++ b/lib/ocaml_rts/linksem/hex_printing.ml
@@ -0,0 +1,68 @@
+(*Generated by Lem from hex_printing.lem.*)
+(** [hex_printing] is a utility module for converting natural numbers and integers
+  * into hex strings of various widths.  Split into a new module as both the
+  * validation code and the main program need this functionality.
+  *)
+
+open Lem_basic_classes
+open Lem_list
+open Lem_num
+open Lem_string
+
+open Missing_pervasives
+open Elf_types_native_uint
+
+(*val hex_string_of_big_int_no_padding : natural -> string*)
+(* declare ocaml target_rep function hex_string_of_big_int_no_padding = `Ml_bindings.hex_string_of_big_int_no_padding` *)
+let hex_string_of_big_int_no_padding:Nat_big_num.num ->string=  hex_string_of_natural
+(*val hex_string_of_big_int_no_padding' : integer -> string*)
+(*val hex_string_of_big_int_pad2 : natural -> string*)
+(*val hex_string_of_big_int_pad4 : natural -> string*)
+(*val hex_string_of_big_int_pad5 : natural -> string*)
+(*val hex_string_of_big_int_pad6 : natural -> string*)
+(*val hex_string_of_big_int_pad7 : natural -> string*)
+(*val hex_string_of_big_int_pad8 : natural -> string*)
+(*val hex_string_of_big_int_pad16 : natural -> string*)
+
+(*val hex_string_of_nat_pad2 : nat -> string*)
+
+(*val unsafe_hex_string_of_natural : nat -> natural -> string*)
+let unsafe_hex_string_of_natural pad m:string=  
+ (if pad = 2 then
+    Ml_bindings.hex_string_of_big_int_pad2 m
+  else if pad = 5 then
+    Ml_bindings.hex_string_of_big_int_pad5 m
+  else if pad = 4 then
+    Ml_bindings.hex_string_of_big_int_pad4 m
+  else if pad = 6 then
+    Ml_bindings.hex_string_of_big_int_pad6 m
+  else if pad = 7 then
+    Ml_bindings.hex_string_of_big_int_pad7 m
+  else if pad = 8 then
+    Ml_bindings.hex_string_of_big_int_pad8 m
+  else if pad = 16 then
+    Ml_bindings.hex_string_of_big_int_pad16 m
+  else
+    hex_string_of_big_int_no_padding m)
+
+(*val unsafe_hex_string_of_uc_list : list unsigned_char -> string*)
+let rec unsafe_hex_string_of_uc_list xs:string=  
+ ((match xs with
+    | []       -> ""
+    | x::y::xs ->
+      let sx = (unsafe_hex_string_of_natural( 2) (Nat_big_num.of_string (Uint32.to_string x))) in
+      let sy = (unsafe_hex_string_of_natural( 2) (Nat_big_num.of_string (Uint32.to_string y))) in
+      let sx =        
+(if String.length sx = 2 then
+          sx
+        else
+          "0" ^ sx)
+      in
+      let sy =        
+(if String.length sy = 2 then
+          sy
+        else
+          "0" ^ sy)
+      in
+        sx ^ (" " ^ (sy ^ (" " ^ unsafe_hex_string_of_uc_list xs)))
+  ))