Fixed ocaml backend so it correctly compiles registers passed by name.

Added a test case for this behavior

5 files changed, 50 insertions, 2 deletions

diff --git a/lib/ocaml_rts/sail_lib.ml b/lib/ocaml_rts/sail_lib.ml
index 176c1124..6876ec35 100644
--- a/lib/ocaml_rts/sail_lib.ml
+++ b/lib/ocaml_rts/sail_lib.ml
@@ -441,6 +441,8 @@ 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)
 
+let reg_deref r = !r
+
 let string_of_zbit = function
   | B0 -> "0"
   | B1 -> "1"
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 28bf624d..e8fd34b1 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -91,6 +91,7 @@ let ocaml_typ_id ctx = function
   | 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 "register") = 0 -> string "ref"
   | id -> zencode ctx id
 
 let rec ocaml_typ ctx (Typ_aux (typ_aux, _)) =
@@ -151,6 +152,11 @@ let rec ocaml_pat ctx (P_aux (pat_aux, _) as pat) =
 
 let begin_end doc = group (string "begin" ^^ nest 2 (break 1 ^^ doc) ^/^ string "end")
 
+(* Returns true if a type is a register being passed by name *)
+let is_passed_by_name = function
+  | (Typ_aux (Typ_app (tid, _), _)) -> string_of_id tid = "register"
+  | _ -> false
+
 let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) =
   match exp_aux with
   | E_app (f, [x]) when Env.is_union_constructor f (env_of exp) -> zencode_upper ctx f ^^ space ^^ ocaml_atomic_exp ctx x
@@ -259,6 +265,7 @@ and ocaml_atomic_exp ctx (E_aux (exp_aux, _) as exp) =
        match Env.lookup_id id (env_of exp) with
        | Local (Immutable, _) | Unbound -> zencode ctx id
        | Enum _ | Union _ -> zencode_upper ctx id
+       | Register _ when is_passed_by_name (typ_of exp) -> zencode ctx id
        | Register typ ->
           if !opt_trace_ocaml then
             let var = gensym () in
diff --git a/src/type_check.ml b/src/type_check.ml
index f7716bc9..87e747f9 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -2170,10 +2170,10 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
      then annot_exp_effect (E_lit lit) typ (mk_effect [BE_undef])
      else typ_error l ("Type " ^ string_of_typ typ ^ " failed undefined monomorphism restriction")
   (* This rule allows registers of type t to be passed by name with type register<t>*)
-  | E_id reg, Typ_app (id, [Typ_arg_aux (Typ_arg_typ typ, _)])
+  | E_id reg, Typ_app (id, [Typ_arg_aux (Typ_arg_typ arg_typ, _)])
     when string_of_id id = "register" && Env.is_register reg env ->
      let rtyp = Env.get_register reg env in
-     subtyp l env rtyp typ; annot_exp (E_id reg) typ (* CHECK: is this subtyp the correct way around? *)
+     subtyp l env rtyp arg_typ; annot_exp (E_id reg) typ (* CHECK: is this subtyp the correct way around? *)
   | E_id id, _ when is_union_id id env ->
      begin
        match Env.lookup_id id env with
diff --git a/test/ocaml/reg_passing/expect b/test/ocaml/reg_passing/expect
new file mode 100644
index 00000000..e64f92f2
--- /dev/null
+++ b/test/ocaml/reg_passing/expect
@@ -0,0 +1,3 @@
+R1 = 10
+R2 = 20
+R3 = 10
diff --git a/test/ocaml/reg_passing/reg_passing.sail b/test/ocaml/reg_passing/reg_passing.sail
new file mode 100644
index 00000000..94acdf7e
--- /dev/null
+++ b/test/ocaml/reg_passing/reg_passing.sail
@@ -0,0 +1,36 @@
+
+register R1 : int
+register R2 : int
+register R3 : int
+
+val cast "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
+val output = {
+    ocaml: "(fun (str, n) -> print_endline (str ^ string_of_big_int n))"
+  } : (string, int) -> unit
+
+val f : register(int) -> unit effect {rreg, wreg}
+
+function f R = {
+  R1 = R;
+}
+
+val g : unit -> unit effect {rreg, wreg}
+
+function g () = {
+  f(R1);
+  f(R2);
+}
+
+val main : unit -> unit effect {rreg, wreg}
+
+function main () = {
+  R1 = 4;
+  R2 = 5;
+  g ();
+  R3 = 10;
+  f(R3);
+  R2 = 20;
+  output("R1 = ", R1);
+  output("R2 = ", R2);
+  output("R3 = ", R3)
+}
\ No newline at end of file