Add a function to perform re-writes in parallel

rewrite_defs_base_parallel j is the same as rewrite_defs_base
except it performs the re-writes in j parallel processes. Currently
only the trivial_sizeof re-write is parallelised this way with a
default of 4. This works on my machine (TM) but may fail elsewhere.
Because 2019 OCaml concurrency support is lacking, we use Unix.fork
and Marshal.to_channel to send the info from the child processes
performing the re-write back to the parent.

Also fix a missing case in pretty_print_lem

5 files changed, 64 insertions, 1 deletions

diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 822cc7b6..73c1fe8b 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -1362,6 +1362,7 @@ let doc_dec_lem (DEC_aux (reg, ((l, _) as annot))) =
        else raise (Reporting.err_unreachable l __POS__ ("can't deal with register type " ^ string_of_typ typ)) *)
   | DEC_alias(id,alspec) -> empty
   | DEC_typ_alias(typ,id,alspec) -> empty
+  | DEC_config _ -> empty
 
 let doc_spec_lem (VS_aux (valspec,annot)) =
   match valspec with
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 81fa7c29..89f64401 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -383,6 +383,64 @@ let rewrite_defs_base_progress prefix rewriters (Defs defs) =
   in
   Defs (rewrite 1 defs)
 
+let rec takedrop n xs =
+  match n, xs with
+  | 0, _ -> [], xs
+  | n, [] -> [], []
+  | n, x :: xs ->
+     let ys, xs = takedrop (n - 1) xs in
+     x :: ys, xs
+
+let rewrite_defs_base_parallel j rewriters (Defs defs) =
+  let module IntMap = Map.Make(struct type t = int let compare = compare end) in
+  let total = List.length defs in
+  let defs = ref defs in
+
+  (* We have a list of child processes in pids, and a mapping from pid
+     to result location in results. *)
+  let pids = ref [] in
+  let results = ref IntMap.empty in
+  for i = 1 to j do
+    let work = if i = 1 then total / j + total mod j else total / j in
+    let work, rest = takedrop work !defs in
+    (* Create a temporary file where the child process will return it's result *)
+    let result = Filename.temp_file "sail" ".rewrite" in
+    let pid = Unix.fork () in
+    begin
+      if pid = 0 then
+        let Defs work = rewrite_defs_base rewriters (Defs work) in
+        let out_chan = open_out result in
+        Marshal.to_channel out_chan work [Marshal.Closures];
+        close_out out_chan;
+        exit 0
+      else
+        (pids := pid :: !pids; results := IntMap.add pid result !results)
+    end;
+    defs := rest
+  done;
+  (* Make sure we haven't left any definitions behind! *)
+  assert(List.length !defs = 0);
+
+  let rewritten = ref [] in
+
+  (* Now we wait for all our child processes *)
+  while List.compare_length_with !pids 0 > 0 do
+    let child = List.hd !pids in
+    pids := List.tl !pids;
+    let _, status = Unix.waitpid [] child in
+    match status with
+    | WEXITED 0 ->
+       let result = IntMap.find child !results in
+       let in_chan = open_in result in
+       rewritten := Marshal.from_channel in_chan :: !rewritten;
+       close_in in_chan;
+       Sys.remove result
+    | _ ->
+       prerr_endline "Child process exited abnormally in parallel rewrite";
+       exit 1
+  done;
+  Defs (List.concat !rewritten)
+  
 let rewriters_base =
   {rewrite_exp = rewrite_exp;
    rewrite_pat = rewrite_pat;
diff --git a/src/rewriter.mli b/src/rewriter.mli
index 53b892d4..ec4e381c 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -70,6 +70,8 @@ val rewrite_defs : tannot defs -> tannot defs
 
 val rewrite_defs_base : tannot rewriters -> tannot defs -> tannot defs
 
+val rewrite_defs_base_parallel : int -> tannot rewriters -> tannot defs -> tannot defs
+  
 (* Same as rewrite_defs base but display a progress bar when verbosity >= 1 *)
 val rewrite_defs_base_progress : string -> tannot rewriters -> tannot defs -> tannot defs
 
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 5fb1962e..79e8792d 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -400,7 +400,7 @@ let rewrite_trivial_sizeof, rewrite_trivial_sizeof_exp =
   and rewrite_e_sizeof split_sizeof =
     { id_exp_alg with e_aux = (fun (exp, annot) -> rewrite_e_aux split_sizeof (E_aux (exp, annot))) }
   in
-  rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp (rewrite_e_sizeof true)) }, rewrite_e_aux true
+  rewrite_defs_base_parallel 4 { rewriters_base with rewrite_exp = (fun _ -> fold_exp (rewrite_e_sizeof true)) }, rewrite_e_aux true
 
 (* Rewrite sizeof expressions with type-level variables to
    term-level expressions
diff --git a/src/sail.ml b/src/sail.ml
index 8d095451..9336dfb2 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -417,6 +417,8 @@ let main() =
            close_out chan
          end
        else ());
+
+      if !opt_memo_z3 then Constraint.save_digests () else ()
     end
 
 let _ =  try