diff --git a/src/bin/sail.ml b/src/bin/sail.ml index 4e025eb35..8dca5aa08 100644 --- a/src/bin/sail.ml +++ b/src/bin/sail.ml @@ -530,8 +530,8 @@ let run_sail_format (config : Yojson.Basic.t option) = close_out out_chan | None -> () end; - let ((out_chan, _, _, _) as file_info) = Util.open_output_with_check_unformatted None f in - output_string out_chan formatted; + let file_info = Util.open_output_with_check f in + output_string file_info.channel formatted; Util.close_output_with_check file_info ) ) diff --git a/src/lib/rewrites.ml b/src/lib/rewrites.ml index 3a08a0038..ea2922cf5 100644 --- a/src/lib/rewrites.ml +++ b/src/lib/rewrites.ml @@ -4670,9 +4670,9 @@ let rewrite_step n total (ctx, ast, effect_info, env) (name, rewriter) = match !opt_ddump_rewrite_ast with | Some (f, i) -> let filename = f ^ "_rewrite_" ^ string_of_int i ^ "_" ^ name ^ ".sail" in - let ((ot, _, _, _) as ext_ot) = Util.open_output_with_check_unformatted None filename in - Pretty_print_sail.output_ast ot (strip_ast ast); - Util.close_output_with_check ext_ot; + let out = Util.open_output_with_check filename in + Pretty_print_sail.output_ast out.channel (strip_ast ast); + Util.close_output_with_check out; opt_ddump_rewrite_ast := Some (f, i + 1) | _ -> () end; diff --git a/src/lib/util.ml b/src/lib/util.ml index 30915c75f..f2bc78eab 100644 --- a/src/lib/util.ml +++ b/src/lib/util.ml @@ -540,21 +540,23 @@ let progress prefix msg n total = ) else () -let open_output_with_check opt_dir file_name = - let temp_file_name, o = Filename.open_temp_file "ll_temp" "" in - let o' = Format.formatter_of_out_channel o in - (o', (o, temp_file_name, opt_dir, file_name)) +type checked_output = { channel : out_channel; temp_file_name : string; directory : string option; file_name : string } -let open_output_with_check_unformatted opt_dir file_name = - let temp_file_name, o = Filename.open_temp_file "ll_temp" "" in - (o, temp_file_name, opt_dir, file_name) +let open_output_with_check_formatted ?directory file_name = + let temp_file_name, channel = Filename.open_temp_file "ll_temp" "" in + let fmt = Format.formatter_of_out_channel channel in + (fmt, { channel; temp_file_name; directory; file_name }) + +let open_output_with_check ?directory file_name = + let temp_file_name, channel = Filename.open_temp_file "ll_temp" "" in + { channel; temp_file_name; directory; file_name } let always_replace_files = ref true -let close_output_with_check (o, temp_file_name, opt_dir, file_name) = - let _ = close_out o in +let close_output_with_check { channel; temp_file_name; directory; file_name } = + let _ = close_out channel in let file_name = - match opt_dir with + match directory with | None -> file_name | Some dir -> if Sys.file_exists dir then () else Unix.mkdir dir 0o775; diff --git a/src/lib/util.mli b/src/lib/util.mli index efd72613e..49287966a 100644 --- a/src/lib/util.mli +++ b/src/lib/util.mli @@ -318,11 +318,25 @@ val progress : string -> string -> int -> int -> unit the output file is only updated, if its content really changes. *) val always_replace_files : bool ref -val open_output_with_check : - string option -> string -> Format.formatter * (out_channel * string * string option * string) - -val open_output_with_check_unformatted : string option -> string -> out_channel * string * string option * string - -val close_output_with_check : out_channel * string * string option * string -> unit +type checked_output = { channel : out_channel; temp_file_name : string; directory : string option; file_name : string } + +(** [open_output_with_check file_name] will open a file for output, + but will only actually create or update said file if the contents + are different to the existing contents of said file when the + output is closed. This means it works well for compiler artifacts + that are referenced by tools like Make. The 'check' that the file + actually needs updating happens in the [close_output_with_check] + function, so it is especially important that any call to this is + matched with that function otherwise no actual output will happen. + + Takes an optional directory argument, which will cause the file to + be created in a subdirectory of the current directory. The + subdirectory will be created (by the [close_output_with_check] + function) if it doesn't exist. *) +val open_output_with_check : ?directory:string -> string -> checked_output + +val open_output_with_check_formatted : ?directory:string -> string -> Format.formatter * checked_output + +val close_output_with_check : checked_output -> unit val to_upper_camel_case : string -> string diff --git a/src/sail_coq_backend/sail_plugin_coq.ml b/src/sail_coq_backend/sail_plugin_coq.ml index 805f7b2a0..41988d7be 100644 --- a/src/sail_coq_backend/sail_plugin_coq.ml +++ b/src/sail_coq_backend/sail_plugin_coq.ml @@ -204,24 +204,24 @@ let output_coq opt_dir filename alt_modules alt_modules2 libs ctx env effect_inf | [] -> base_imports_default | _ -> Str.split (Str.regexp "[ \t]+") (String.concat " " alt_modules) in - let ((ot, _, _, _) as ext_ot) = Util.open_output_with_check_unformatted opt_dir (types_module ^ ".v") in - let ((o, _, _, _) as ext_o) = Util.open_output_with_check_unformatted opt_dir (filename ^ ".v") in - let oi, ext_oi = + let types_file_info = Util.open_output_with_check ?directory:opt_dir (types_module ^ ".v") in + let file_info = Util.open_output_with_check ?directory:opt_dir (filename ^ ".v") in + let isla_channel_opt, isla_file_info_opt = match !opt_coq_isla with | None -> (None, None) | Some fname -> - let ((o, _, _, _) as ext_o) = Util.open_output_with_check_unformatted opt_dir (fname ^ ".v") in - (Some o, Some ext_o) + let file_info = Util.open_output_with_check ?directory:opt_dir (fname ^ ".v") in + (Some file_info.channel, Some file_info) in - (Pretty_print_coq.pp_ast_coq library_style (ot, base_imports) - (o, base_imports @ (types_module :: libs) @ alt_modules2) - types_module oi ctx effect_info env ast concurrency_monad_params generated_line + (Pretty_print_coq.pp_ast_coq library_style (types_file_info.channel, base_imports) + (file_info.channel, base_imports @ (types_module :: libs) @ alt_modules2) + types_module isla_channel_opt ctx effect_info env ast concurrency_monad_params generated_line ) (alt_modules2 <> []); (* suppress MR and M defns if alt_modules2 present*) - Util.close_output_with_check ext_ot; - Util.close_output_with_check ext_o; - Option.iter (fun ext -> Util.close_output_with_check ext) ext_oi + Util.close_output_with_check types_file_info; + Util.close_output_with_check file_info; + Option.iter (fun f -> Util.close_output_with_check f) isla_file_info_opt let output libs files = List.iter diff --git a/src/sail_doc_backend/sail_plugin_doc.ml b/src/sail_doc_backend/sail_plugin_doc.ml index 8d3e9ce18..e9c77cb2f 100644 --- a/src/sail_doc_backend/sail_plugin_doc.ml +++ b/src/sail_doc_backend/sail_plugin_doc.ml @@ -161,7 +161,7 @@ let html_target files out_dir_opt { ast; _ } = (fun file_info -> let output_file = Filename.concat out_dir (file_info.prefix ^ ".html") in create_directories (Filename.dirname output_file); - let ((out_chan, _, _, _) as handle) = Util.open_output_with_check_unformatted None output_file in + let handle = Util.open_output_with_check output_file in let file_links = Html_source.hyperlinks_for_file ~filename:file_info.filename ast in let file_links = Array.map @@ -184,7 +184,7 @@ let html_target files out_dir_opt { ast; _ } = try Option.map Util.read_whole_file !opt_html_css with Sys_error msg -> raise (Reporting.err_general Parse_ast.Unknown msg) in - output_html ?css ~file_info ~hyperlinks:file_links out_chan; + output_html ?css ~file_info ~hyperlinks:file_links handle.channel; Util.close_output_with_check handle ) !files diff --git a/src/sail_lem_backend/sail_plugin_lem.ml b/src/sail_lem_backend/sail_plugin_lem.ml index 8e2043233..2fe2d41ef 100644 --- a/src/sail_lem_backend/sail_plugin_lem.ml +++ b/src/sail_lem_backend/sail_plugin_lem.ml @@ -149,10 +149,10 @@ let lem_rewrites = ("attach_effects", []); ] -let write_doc dir filename doc = - let ((chan, _, _, _) as o) = Util.open_output_with_check_unformatted dir filename in - Pretty_print_common.print chan doc; - Util.close_output_with_check o +let write_doc directory filename doc = + let file_info = Util.open_output_with_check ?directory filename in + Pretty_print_common.print file_info.channel doc; + Util.close_output_with_check file_info let lem_target out_file { ctx; ast; effect_info; env = type_env; _ } = let out_filename = match out_file with Some f -> f | None -> "out" in diff --git a/src/sail_sv_backend/sail_plugin_sv.ml b/src/sail_sv_backend/sail_plugin_sv.ml index 89e9a2278..1407bb0c5 100644 --- a/src/sail_sv_backend/sail_plugin_sv.ml +++ b/src/sail_sv_backend/sail_plugin_sv.ml @@ -660,20 +660,18 @@ let verilog_target out_opt { ast; effect_info; env; default_sail_dir; _ } = let sv_output = Pretty_print_sail.Document.to_string doc in (* make_genlib_file (Filename.concat (Filename.dirname out) (sprintf "sail_genlib_%s.sv" (Filename.basename out))); *) - let ((out_chan, _, _, _) as file_info) = Util.open_output_with_check_unformatted !opt_output_dir (out ^ ".sv") in - output_string out_chan sv_output; + let file_info = Util.open_output_with_check ?directory:!opt_output_dir (out ^ ".sv") in + output_string file_info.channel sv_output; Util.close_output_with_check file_info; begin match !opt_verilate with | Verilator_compile | Verilator_run -> - let ((out_chan, _, _, _) as file_info) = - Util.open_output_with_check_unformatted !opt_output_dir ("sim_" ^ out ^ ".cpp") - in + let file_info = Util.open_output_with_check ?directory:!opt_output_dir ("sim_" ^ out ^ ".cpp") in List.iter (fun line -> - output_string out_chan line; - output_char out_chan '\n' + output_string file_info.channel line; + output_char file_info.channel '\n' ) (verilator_cpp_wrapper "sail_toplevel"); Util.close_output_with_check file_info;