diff options
Diffstat (limited to 'src/ocaml_backend.ml')
| -rw-r--r-- | src/ocaml_backend.ml | 45 |
1 files changed, 34 insertions, 11 deletions
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index 384d8109..f103f818 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -3,6 +3,9 @@ open Ast_util open PPrint open Type_check +(* Option to turn tracing features on or off *) +let opt_trace_ocaml = ref false + type ctx = { register_inits : tannot exp list; externs : id Bindings.t; @@ -240,7 +243,10 @@ 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 _ -> parens (string ("trace \"Read: " ^ string_of_id id ^ "\";") ^^ space ^^ bang ^^ zencode ctx id) + | Register _ -> + if !opt_trace_ocaml + then parens (string ("trace \"Read: " ^ string_of_id id ^ "\";") ^^ space ^^ bang ^^ zencode ctx id) + else bang ^^ zencode ctx id | Local (Mutable, _) -> bang ^^ zencode ctx id end | E_list exps -> enclose lbracket rbracket (separate_map (semi ^^ space) (ocaml_exp ctx) exps) @@ -254,8 +260,12 @@ and ocaml_assignment ctx (LEXP_aux (lexp_aux, _) as lexp) exp = | Register typ -> let var = gensym () in let traced_exp = - parens (separate space [string "let"; var; equals; ocaml_atomic_exp ctx exp; string "in"; - string "trace_write" ^^ space ^^ string_lit (string_of_id id) ^^ space ^^ parens (ocaml_string_typ (Rewriter.simple_typ typ) var) ^^ semi; var]) + 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; ocaml_atomic_exp ctx exp; string "in"; + string "trace_write" ^^ space ^^ string_lit (string_of_id id) ^^ space ^^ str_typ ^^ semi; var]) + else ocaml_atomic_exp ctx exp in separate space [zencode ctx id; string ":="; traced_exp] | _ -> separate space [zencode ctx id; string ":="; ocaml_exp ctx exp] @@ -331,22 +341,36 @@ let ocaml_funcls ctx = in (arg_sym, string_of_arg, ret_sym, string_of_ret) in + let sail_call id arg_sym pat_sym ret_sym = + if !opt_trace_ocaml + then separate space [string "sail_trace_call"; string_lit (string_of_id id); parens (arg_sym ^^ space ^^ pat_sym); ret_sym] + else separate space [string "sail_call"] + in + let ocaml_funcl call string_of_arg string_of_ret = + if !opt_trace_ocaml + then (call ^^ twice hardline ^^ string_of_arg ^^ twice hardline ^^ string_of_ret) + else call + in function | [] -> failwith "Ocaml: empty function" | [FCL_aux (FCL_Funcl (id, pat, exp),_)] -> let Typ_aux (Typ_fn (typ1, typ2, _), _) = Bindings.find id ctx.val_specs in let pat_sym = gensym () in - let annot_pat = parens (separate space [parens (ocaml_pat ctx pat ^^ space ^^ colon ^^ space ^^ ocaml_typ ctx typ1); string "as"; pat_sym]) in + let annot_pat = + let pat = parens (ocaml_pat ctx pat ^^ space ^^ colon ^^ space ^^ ocaml_typ ctx typ1) in + if !opt_trace_ocaml + then parens (separate space [pat; string "as"; pat_sym]) + else pat + in let call_header = function_header () in let arg_sym, string_of_arg, ret_sym, string_of_ret = trace_info typ1 typ2 in let call = separate space [call_header; zencode ctx id; annot_pat; colon; ocaml_typ ctx typ2; equals; - string "sail_trace_call"; string_lit (string_of_id id); parens (arg_sym ^^ space ^^ pat_sym); ret_sym; - string "(fun r ->"] + sail_call id arg_sym pat_sym ret_sym; string "(fun r ->"] ^//^ ocaml_exp ctx exp ^^ rparen in - call ^^ twice hardline ^^ string_of_arg ^^ twice hardline ^^ string_of_ret + ocaml_funcl call string_of_arg string_of_ret | funcls -> let id = funcls_id funcls in let Typ_aux (Typ_fn (typ1, typ2, _), _) = Bindings.find id ctx.val_specs in @@ -355,12 +379,11 @@ let ocaml_funcls ctx = let arg_sym, string_of_arg, ret_sym, string_of_ret = trace_info typ1 typ2 in let call = separate space [call_header; zencode ctx id; parens (pat_sym ^^ space ^^ colon ^^ space ^^ ocaml_typ ctx typ1); equals; - string "sail_trace_call"; string_lit (string_of_id id); parens (arg_sym ^^ space ^^ pat_sym); ret_sym; - string "(fun r ->"] + sail_call id arg_sym pat_sym ret_sym; string "(fun r ->"] ^//^ (separate space [string "match"; pat_sym; string "with"] ^^ hardline ^^ ocaml_funcl_matches ctx funcls) ^^ rparen in - call ^^ twice hardline ^^ string_of_arg ^^ twice hardline ^^ string_of_ret + ocaml_funcl call string_of_arg string_of_ret let ocaml_fundef ctx (FD_aux (FD_function (_, _, _, funcls), _)) = ocaml_funcls ctx funcls @@ -391,7 +414,6 @@ let rec ocaml_enum ctx = function (* We generate a string_of_X ocaml function for each type X, to be used for debugging purposes *) - let ocaml_def_end = string ";;" ^^ twice hardline let ocaml_string_of_enum ctx id ids = @@ -491,6 +513,7 @@ let ocaml_main spec = 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 "initialize_registers ();" ^/^ string "Printexc.record_backtrace true;" ^/^ string "zmain ()") |