Modified ocaml backend to use ocamlfind for linksem and lem

Fixed test cases for ocaml backend and interpreter

3 files changed, 74 insertions, 59 deletions

diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 591f31eb..2a6206d4 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -139,11 +139,11 @@ let ocaml_typ_id ctx = function
   | id when Id.compare id (mk_id "string") = 0 -> string "string"
   | id when Id.compare id (mk_id "list") = 0 -> string "list"
   | id when Id.compare id (mk_id "bit") = 0 -> string "bit"
-  | id when Id.compare id (mk_id "int") = 0 -> string "big_int"
-  | id when Id.compare id (mk_id "nat") = 0 -> string "big_int"
+  | id when Id.compare id (mk_id "int") = 0 -> string "Big_int.num"
+  | id when Id.compare id (mk_id "nat") = 0 -> string "Big_int.num"
   | id when Id.compare id (mk_id "bool") = 0 -> string "bool"
   | id when Id.compare id (mk_id "unit") = 0 -> string "unit"
-  | id when Id.compare id (mk_id "real") = 0 -> string "Num.num"
+  | id when Id.compare id (mk_id "real") = 0 -> string "Rational.t"
   | id when Id.compare id (mk_id "exception") = 0 -> string "exn"
   | id when Id.compare id (mk_id "register") = 0 -> string "ref"
   | id when Id.compare id (mk_id "ref") = 0 -> string "ref"
@@ -182,7 +182,7 @@ let ocaml_lit (L_aux (lit_aux, _)) =
   | L_one -> string "B1"
   | L_true -> string "true"
   | L_false -> string "false"
-  | L_num n -> parens (string "big_int_of_string" ^^ space ^^ string ("\"" ^ Big_int.to_string n ^ "\""))
+  | L_num n -> parens (string "Big_int.of_string" ^^ space ^^ string ("\"" ^ Big_int.to_string n ^ "\""))
   | L_undef -> failwith "undefined should have been re-written prior to ocaml backend"
   | L_string str -> string_lit str
   | L_real str -> parens (string "real_of_string" ^^ space ^^ dquotes (string (String.escaped str)))
@@ -284,14 +284,14 @@ let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) =
      let loop_var = separate space [string "let"; zencode ctx id; equals; string "ref"; ocaml_atomic_exp ctx exp_from; string "in"] in
      let loop_mod =
        match ord with
-       | Ord_aux (Ord_inc, _) -> string "add_big_int" ^^ space ^^ zencode ctx id ^^ space ^^ ocaml_atomic_exp ctx exp_step
-       | Ord_aux (Ord_dec, _) -> string "sub_big_int" ^^ space ^^ zencode ctx id ^^ space ^^ ocaml_atomic_exp ctx exp_step
+       | Ord_aux (Ord_inc, _) -> string "Big_int.add" ^^ space ^^ zencode ctx id ^^ space ^^ ocaml_atomic_exp ctx exp_step
+       | Ord_aux (Ord_dec, _) -> string "Big_int.sub" ^^ space ^^ zencode ctx id ^^ space ^^ ocaml_atomic_exp ctx exp_step
        | Ord_aux (Ord_var _, _) -> failwith "Cannot have variable loop order!"
      in
      let loop_compare =
        match ord with
-       | Ord_aux (Ord_inc, _) -> string "le_big_int"
-       | Ord_aux (Ord_dec, _) -> string "gt_big_int"
+       | Ord_aux (Ord_inc, _) -> string "Big_int.less"
+       | Ord_aux (Ord_dec, _) -> string "Big_int.greater"
        | Ord_aux (Ord_var _, _) -> failwith "Cannot have variable loop order!"
      in
      let loop_body =
@@ -636,34 +636,42 @@ let ocaml_defs (Defs defs) =
     else empty
   in
   (string "open Sail_lib;;" ^^ hardline)
-  ^^ (string "open Big_int" ^^ ocaml_def_end)
+  ^^ (string "module Big_int = Nat_big_num" ^^ ocaml_def_end)
   ^^ concat (List.map (ocaml_def ctx) defs)
   ^^ empty_reg_init
 
-let ocaml_main spec =
-  concat [separate space [string "open"; string (String.capitalize spec)] ^^ ocaml_def_end;
-          separate space [string "open"; string "Elf_loader"] ^^ ocaml_def_end;
-          separate space [string "let"; string "()"; equals]
-          ^//^ (string "Random.self_init ();"
-                ^/^ string "load_elf ();"
-                ^/^ string (if !opt_trace_ocaml then "Sail_lib.opt_trace := true;" else "Sail_lib.opt_trace := false;")
-                ^/^ string "zinitializze_registers ();"
-                ^/^ string "Printexc.record_backtrace true;"
-                ^/^ string "zmain ()")
-         ]
+let ocaml_main spec sail_dir =
+  let lines = ref [] in
+  let chan = open_in (sail_dir ^ "/lib/main.ml") in
+  begin
+    try
+      while true do
+        let line = input_line chan in
+        lines := line :: !lines
+      done;
+    with
+    | End_of_file -> close_in chan; lines := List.rev !lines
+  end;
+  (("open " ^ String.capitalize spec ^ ";;\n\n") :: !lines
+   @ [ "  zinitializze_registers ();";
+       "  Printexc.record_backtrace true;";
+       "  zmain ()\n";])
+  |> String.concat "\n"
 
 let ocaml_pp_defs f defs =
   ToChannel.pretty 1. 80 f (ocaml_defs defs)
 
 let ocaml_compile spec defs =
-  let sail_lib_dir =
-    try Sys.getenv "SAILLIBDIR" with
-    | Not_found -> failwith "Environment variable SAILLIBDIR needs to be set"
+  let sail_dir =
+    try Sys.getenv "SAIL_DIR" with
+    | Not_found -> failwith "Environment variable SAIL_DIR needs to be set"
   in
   if Sys.file_exists "_sbuild" then () else Unix.mkdir "_sbuild" 0o775;
   let cwd = Unix.getcwd () in
   Unix.chdir "_sbuild";
-  let _ = Unix.system ("cp -r " ^ sail_lib_dir ^ "/ocaml_rts/. .") in
+  let _ = Unix.system ("cp -r " ^ sail_dir ^ "/src/elf_loader.ml .") in
+  let _ = Unix.system ("cp -r " ^ sail_dir ^ "/src/sail_lib.ml .") in
+  let _ = Unix.system ("cp -r " ^ sail_dir ^ "/lib/_tags .") in
   let out_chan = open_out (spec ^ ".ml") in
   ocaml_pp_defs out_chan defs;
   close_out out_chan;
@@ -672,13 +680,13 @@ let ocaml_compile spec defs =
     begin
       print_endline "Generating main";
       let out_chan = open_out "main.ml" in
-      ToChannel.pretty 1. 80 out_chan (ocaml_main spec);
+      output_string out_chan (ocaml_main spec sail_dir);
       close_out out_chan;
-      let _ = Unix.system "ocamlbuild -pkg zarith -pkg uint main.native" in
+      let _ = Unix.system "ocamlbuild -use-ocamlfind main.native" in
       let _ = Unix.system ("cp main.native " ^ cwd ^ "/" ^ spec) in
       ()
     end
   else
-    let _ = Unix.system ("ocamlbuild -pkg zarith -pkg uint " ^ spec ^ ".cmo") in
+    let _ = Unix.system ("ocamlbuild -use-ocamlfind " ^ spec ^ ".cmo") in
     ();
   Unix.chdir cwd
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index 849aa16c..08b8ac1a 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -172,12 +172,14 @@ let sint = function
      in
      Big_int.add complement (uint xs)
 
-let add (x, y) = Big_int.add x y
-let sub (x, y) = Big_int.sub x y
+let add_int (x, y) = Big_int.add x y
+let sub_int (x, y) = Big_int.sub x y
 let mult (x, y) = Big_int.mul x y
 let quotient (x, y) = Big_int.div x y
 let modulus (x, y) = Big_int.modulus x y
 
+let negate x = Big_int.negate x
+
 let add_bit_with_carry (x, y, carry) =
   match x, y, carry with
   | B0, B0, B0 -> B0, B0
@@ -401,23 +403,23 @@ let set_slice (out_len, slice_len, out, n, slice) =
 
 let set_slice_int (_, _, _, _) = assert false
 
-(*
-let eq_real (x, y) = Num.eq_num x y
-let lt_real (x, y) = Num.lt_num x y
-let gt_real (x, y) = Num.gt_num x y
-let lteq_real (x, y) = Num.le_num x y
-let gteq_real (x, y) = Num.ge_num x y
+let eq_real (x, y) = Rational.equal x y
+let lt_real (x, y) = Rational.lt x y
+let gt_real (x, y) = Rational.gt x y
+let lteq_real (x, y) = Rational.leq x y
+let gteq_real (x, y) = Rational.geq x y
+let to_real x = Rational.of_int (Big_int.to_int x) (* FIXME *)
+let negate_real x = Rational.neg x
 
-let round_down x = Num.big_int_of_num (Num.floor_num x)
-let round_up x = Num.big_int_of_num (Num.ceiling_num x)
-let quotient_real (x, y) = Num.div_num x y
-let mult_real (x, y) = Num.mult_num x y
-let real_power (x, y) = Num.power_num x (Num.num_of_big_int y)
-let add_real (x, y) = Num.add_num x y
-let sub_real (x, y) = Num.sub_num x y
+let round_down x = failwith "round_down" (* Num.big_int_of_num (Num.floor_num x) *)
+let round_up x = failwith "round_up" (* Num.big_int_of_num (Num.ceiling_num x) *)
+let quotient_real (x, y) = Rational.div x y
+let mult_real (x, y) = Rational.mul x y (* Num.mult_num x y *)
+let real_power (x, y) = failwith "real_power" (* Num.power_num x (Num.num_of_big_int y) *)
+let add_real (x, y) = Rational.add x y
+let sub_real (x, y) = Rational.sub x y
 
-let abs_real x = Num.abs_num x
- *)
+let abs_real x = Rational.abs x
 
 let lt (x, y) = Big_int.less x y
 let gt (x, y) = Big_int.greater x y
@@ -430,22 +432,27 @@ let max_int (x, y) = Big_int.max x y
 let min_int (x, y) = Big_int.min x y
 let abs_int x = Big_int.abs x
 
-(*
-let undefined_real () = Num.num_of_int 0
+let string_of_int x = Big_int.to_string x
+
+let undefined_real () = Rational.of_int 0
+
+let rec pow x = function
+  | 0 -> 1
+  | n -> x * pow x (n - 1)
 
 let real_of_string str =
+  let rat_of_string sr = Rational.of_int (int_of_string str) in
   try
     let point = String.index str '.' in
-    let whole = Num.num_of_string (String.sub str 0 point) in
+    let whole = Rational.of_int (int_of_string (String.sub str 0 point)) in
     let frac_str = String.sub str (point + 1) (String.length str - (point + 1)) in
-    let frac = Num.div_num (Num.num_of_string frac_str) (Num.num_of_big_int (Big_int.pow_int_positive 10 (String.length frac_str))) in
-    Num.add_num whole frac
+    let frac = Rational.div (rat_of_string frac_str) (Rational.of_int (pow 10 (String.length frac_str))) in
+    Rational.add whole frac
   with
-  | Not_found -> Num.num_of_string str
+  | Not_found -> Rational.of_int (int_of_string str)
 
 (* Not a very good sqrt implementation *)
-let sqrt_real x = real_of_string (string_of_float (sqrt (Num.float_of_num x)))
- *)
+let sqrt_real x = failwith "sqrt_real" (* real_of_string (string_of_float (sqrt (Num.float_of_num x))) *)
 
 let print_int (str, x) =
   print_endline (str ^ Big_int.to_string x)
diff --git a/src/value.ml b/src/value.ml
index b5f7c0c7..b1f6f80b 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -250,12 +250,12 @@ let value_hex_slice = function
      mk_vector (Sail_lib.hex_slice (coerce_string v1, coerce_int v2, coerce_int v3))
   | _ -> failwith "value hex_slice"
 
-let value_add = function
-  | [v1; v2] -> V_int (Sail_lib.add (coerce_int v1, coerce_int v2))
+let value_add_int = function
+  | [v1; v2] -> V_int (Sail_lib.add_int (coerce_int v1, coerce_int v2))
   | _ -> failwith "value add"
 
-let value_sub = function
-  | [v1; v2] -> V_int (Sail_lib.sub (coerce_int v1, coerce_int v2))
+let value_sub_int = function
+  | [v1; v2] -> V_int (Sail_lib.sub_int (coerce_int v1, coerce_int v2))
   | _ -> failwith "value sub"
 
 let value_mult = function
@@ -378,7 +378,7 @@ let primops =
       ("print_endline", value_print);
       ("prerr_endline", value_print);
       ("putchar", value_putchar);
-      ("string_of_big_int", fun vs -> V_string (string_of_value (List.hd vs)));
+      ("string_of_int", fun vs -> V_string (string_of_value (List.hd vs)));
       ("string_of_bits", fun vs -> V_string (string_of_value (List.hd vs)));
       ("print_bits", value_print_bits);
       ("print_int", value_print_int);
@@ -407,8 +407,8 @@ let primops =
       ("set_slice_int", value_set_slice_int);
       ("set_slice", value_set_slice);
       ("hex_slice", value_hex_slice);
-      ("add", value_add);
-      ("sub", value_sub);
+      ("add_int", value_add_int);
+      ("sub_int", value_sub_int);
       ("mult", value_mult);
       ("quotient", value_quotient);
       ("modulus", value_modulus);