Add hooks to call cgen stub file for RISC-V

2 files changed, 22 insertions, 4 deletions

diff --git a/src/sail.ml b/src/sail.ml
index 73173946..0d26df9c 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -64,6 +64,7 @@ let opt_print_ocaml = ref false
 let opt_print_c = ref false
 let opt_print_latex = ref false
 let opt_print_coq = ref false
+let opt_print_cgen = ref false
 let opt_memo_z3 = ref false
 let opt_sanity = ref false
 let opt_includes_c = ref ([]:string list)
@@ -143,6 +144,9 @@ let options = Arg.align ([
   ( "-trace",
     Arg.Tuple [Arg.Set C_backend.opt_trace; Arg.Set Ocaml_backend.opt_trace_ocaml],
     " Instrument ouput with tracing");
+  ( "-cgen",
+    Arg.Set opt_print_cgen,
+    " Generate CGEN source");
   ( "-lem",
     Arg.Set opt_print_lem,
     " output a Lem translated version of the input");
@@ -352,6 +356,9 @@ let main() =
          Util.opt_warnings := true;
          C_backend.compile_ast (C_backend.initial_ctx type_envs) (!opt_includes_c) ast_c
        else ());
+      (if !(opt_print_cgen)
+       then Cgen_backend.output type_envs ast
+       else ());
       (if !(opt_print_lem)
        then
          let mwords = !Pretty_print_lem.opt_mwords in
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index a718e6d5..620df900 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -578,8 +578,14 @@ 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 print_real (str, r) = print_string "REAL\n"
-let prerr_real (str, r) = prerr_string "REAL\n"
+let real_to_string x =
+  if Big_int.equal (Rational.den x) (Big_int.of_int 1) then
+    Big_int.to_string (Rational.num x)
+  else
+    Big_int.to_string (Rational.num x) ^ "/" ^ Big_int.to_string (Rational.den x)
+
+let print_real (str, r) = print_endline (str ^ real_to_string r)
+let prerr_real (str, r) = prerr_endline (str ^ real_to_string r)
 
 let round_down x = Rational.floor x (* Num.big_int_of_num (Num.floor_num x) *)
 let round_up x = Rational.ceiling x (* Num.big_int_of_num (Num.ceiling_num x) *)
@@ -592,6 +598,12 @@ let sub_real (x, y) = Rational.sub x y
 
 let abs_real x = Rational.abs x
 
+let sqrt x =
+  if Big_int.equal (Rational.den x) (Big_int.of_int 1) then
+    Big_int.sqrt (Rational.den x)
+  else
+    failwith "sqrt"
+
 let lt (x, y) = Big_int.less x y
 let gt (x, y) = Big_int.greater x y
 let lteq (x, y) = Big_int.less_equal x y
@@ -620,8 +632,7 @@ let real_of_string str =
   | [whole] -> Rational.of_int (int_of_string str)
   | _ -> failwith "invalid real literal"
 
-(* Not a very good sqrt implementation *)
-let sqrt_real x = failwith "sqrt_real" (* real_of_string (string_of_float (sqrt (Num.float_of_num x))) *)
+let sqrt_real x = failwith "sqrt_real"
 
 let print str = Pervasives.print_string str