summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/ocaml_backend.ml45
-rw-r--r--src/sail.ml61
2 files changed, 64 insertions, 42 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 ()")
diff --git a/src/sail.ml b/src/sail.ml
index 9c447f36..8a70cb70 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -56,39 +56,35 @@ let opt_libs_lem = ref ([]:string list)
let opt_libs_ocaml = ref ([]:string list)
let opt_file_arguments = ref ([]:string list)
let opt_mono_split = ref ([]:((string * int) * string) list)
+
let options = Arg.align ([
( "-o",
Arg.String (fun f -> opt_file_out := Some f),
"<prefix> select output filename prefix");
+ ( "-ocaml",
+ Arg.Tuple [Arg.Set opt_print_ocaml; Arg.Set Initial_check.opt_undefined_gen],
+ " output an OCaml translated version of the input");
+ ( "-ocaml_trace",
+ Arg.Tuple [Arg.Set opt_print_ocaml; Arg.Set Initial_check.opt_undefined_gen; Arg.Set Ocaml_backend.opt_trace_ocaml],
+ " output an OCaml translated version of the input with tracing instrumentation, implies -ocaml");
+ ( "-ocaml_lib",
+ Arg.String (fun l -> opt_libs_ocaml := l::!opt_libs_ocaml),
+ "<filename> provide additional library to open in OCaml output");
( "-lem_ast",
Arg.Set opt_print_lem_ast,
" output a Lem AST representation of the input");
( "-lem",
Arg.Set opt_print_lem,
" output a Lem translated version of the input");
- ( "-ocaml",
- Arg.Tuple [Arg.Set opt_print_ocaml; Arg.Set Initial_check.opt_undefined_gen],
- " output an OCaml translated version of the input");
( "-lem_lib",
Arg.String (fun l -> opt_libs_lem := l::!opt_libs_lem),
"<filename> provide additional library to open in Lem output");
- ( "-ocaml_lib",
- Arg.String (fun l -> opt_libs_ocaml := l::!opt_libs_ocaml),
- "<filename> provide additional library to open in OCaml output");
( "-lem_sequential",
Arg.Set Process_file.opt_lem_sequential,
" use sequential state monad for Lem output");
( "-lem_mwords",
Arg.Set Process_file.opt_lem_mwords,
" use native machine word library for Lem output");
-(*
- ( "-i",
- Arg.String (fun l -> lib := l::!lib),
- "<library_filename> treat this file as input only and generate no output for it");
-*)
- ( "-verbose",
- Arg.Set opt_print_verbose,
- " (debug) pretty-print the input to standard output");
( "-mono-split",
Arg.String (fun s ->
let l = Util.split_on_char ':' s in
@@ -96,39 +92,42 @@ let options = Arg.align ([
| [fname;line;var] -> opt_mono_split := ((fname,int_of_string line),var)::!opt_mono_split
| _ -> raise (Arg.Bad (s ^ " not of form <filename>:<line>:<variable>"))),
"<filename>:<line>:<variable> to case split for monomorphisation");
- ( "-ddump_raw_mono_ast",
- Arg.Set opt_ddump_raw_mono_ast,
- " (debug) dump the monomorphised ast before type-checking");
+ ( "-memo_z3",
+ Arg.Set opt_memo_z3,
+ " memoize calls to z3, improving performance when typechecking repeatedly");
+ ( "-undefined_gen",
+ Arg.Set Initial_check.opt_undefined_gen,
+ " generate undefined_type functions for types in the specification");
+ ( "-no_effects",
+ Arg.Set Type_check.opt_no_effects,
+ " (experimental) turn off effect checking");
( "-new_parser",
Arg.Set Process_file.opt_new_parser,
" (experimental) use new parser");
+ ( "-convert",
+ Arg.Set opt_convert,
+ " (experimental) convert sail to new syntax for use with -new_parser");
( "-just_check",
Arg.Set opt_just_check,
" (experimental) terminate immediately after typechecking");
- ( "-convert",
- Arg.Set opt_convert,
- " Convert sail to new syntax");
- ( "-memo_z3",
- Arg.Set opt_memo_z3,
- " Memoize calls to z3");
+ ( "-ddump_raw_mono_ast",
+ Arg.Set opt_ddump_raw_mono_ast,
+ " (debug) dump the monomorphised ast before type-checking");
+ ( "-verbose",
+ Arg.Set opt_print_verbose,
+ " (debug) pretty-print the input to standard output");
( "-ddump_tc_ast",
Arg.Set opt_ddump_tc_ast,
" (debug) dump the typechecked ast to stdout");
( "-ddump_rewrite_ast",
Arg.String (fun l -> opt_ddump_rewrite_ast := Some (l, 0)),
- " <prefix> (debug) dump the ast after each rewriting step to <prefix>_<i>.lem");
+ "<prefix> (debug) dump the ast after each rewriting step to <prefix>_<i>.lem");
( "-dtc_verbose",
Arg.Int (fun verbosity -> Type_check.opt_tc_debug := verbosity),
- " (debug) verbose typechecker output: 0 is silent");
+ "<verbosity> (debug) verbose typechecker output: 0 is silent");
( "-dno_cast",
Arg.Set opt_dno_cast,
" (debug) typecheck without any implicit casting");
- ( "-no_effects",
- Arg.Set Type_check.opt_no_effects,
- " turn off effect checking");
- ( "-undefined_gen",
- Arg.Set Initial_check.opt_undefined_gen,
- " generate undefined_type functions for types in the specification");
( "-v",
Arg.Set opt_print_version,
" print version");
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 13:27:18 +0000