Improvements to register read tracing in ocaml backend

3 files changed, 19 insertions, 5 deletions

diff --git a/lib/ocaml_rts/Makefile b/lib/ocaml_rts/Makefile
index eee59dd7..3d837e25 100644
--- a/lib/ocaml_rts/Makefile
+++ b/lib/ocaml_rts/Makefile
@@ -53,7 +53,7 @@ import:
 	rsync -rv --include "*/" --include="*.ml" --include="*.mli" --exclude="*" $(BITBUCKET_ROOT)/lem/ocaml-lib/ lem
 
 main: import
-	ocamlbuild -pkg uint -pkg zarith main.native
+	ocamlbuild -pkg uint -pkg zarith main.native -use-ocamlfind
 
 clean:
 	rm -r linksem
diff --git a/lib/ocaml_rts/sail_lib.ml b/lib/ocaml_rts/sail_lib.ml
index 249d61fc..c550b2ce 100644
--- a/lib/ocaml_rts/sail_lib.ml
+++ b/lib/ocaml_rts/sail_lib.ml
@@ -28,6 +28,9 @@ let trace str =
 let trace_write name str =
   trace ("Write: " ^ name ^ " " ^ str)
 
+let trace_read name str =
+  trace ("Read: " ^ name ^ " " ^ str)
+
 let sail_trace_call (type t) (name : string) (in_string : string) (string_of_out : t -> string) (f : _ -> t) =
   let module M =
     struct exception Return of t end
@@ -444,3 +447,7 @@ let string_of_zbool = function
 let string_of_zreal r = Num.string_of_num r
 let string_of_zstring str = "\"" ^ String.escaped str ^ "\""
 
+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)
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index feadb2d5..5a378fa6 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -64,7 +64,10 @@ let rec ocaml_string_typ (Typ_aux (typ_aux, _)) arg =
   match typ_aux with
   | Typ_id id -> ocaml_string_of id ^^ space ^^ arg
   | Typ_app (id, []) -> ocaml_string_of id ^^ space ^^ arg
-  | Typ_app (id, typs) -> string ("\"APP" ^ string_of_id id ^ "\"")
+  | Typ_app (id, [Typ_arg_aux (Typ_arg_typ typ, _)]) ->
+     let farg = gensym () in
+     separate space [string "string_of_list \", \""; parens (separate space [string "fun"; farg; string "->"; ocaml_string_typ typ farg]); arg]
+  | Typ_app (_, _) -> assert false
   | Typ_tup typs ->
      let args = List.map (fun _ -> gensym ()) typs in
      let body =
@@ -75,6 +78,7 @@ let rec ocaml_string_typ (Typ_aux (typ_aux, _)) arg =
   | Typ_fn (typ1, typ2, _) -> string "\"FN\""
   | Typ_var kid -> string "\"VAR\""
   | Typ_exist _ | Typ_wild -> assert false
+
 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"
@@ -252,9 +256,12 @@ 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 _ ->
-          if !opt_trace_ocaml
-          then parens (string ("trace \"Read: " ^ string_of_id id ^ "\";") ^^ space ^^ bang ^^ zencode ctx id)
+       | Register typ ->
+          if !opt_trace_ocaml then
+            let var = gensym () in
+            let str_typ = parens (ocaml_string_typ (Rewriter.simple_typ typ) var) in
+            parens (separate space [string "let"; var; equals; bang ^^ zencode ctx id; string "in";
+                                    string "trace_read" ^^ space ^^ string_lit (string_of_id id) ^^ space ^^ str_typ ^^ semi; var])
           else bang ^^ zencode ctx id
        | Local (Mutable, _) -> bang ^^ zencode ctx id
      end