Refactor checked output functions

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
       )
     )

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;

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;

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

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

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

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

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;