From f5da5188171962d13b9f3eac04845dd19d0aa931 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 22 Apr 2020 08:08:21 +0200
Subject: automated writing Compiler.v

---
 tools/compiler_expand.ml | 87 +++++++++++++++++++++++++++++++++++++++++++-----
 1 file changed, 79 insertions(+), 8 deletions(-)

(limited to 'tools')

diff --git a/tools/compiler_expand.ml b/tools/compiler_expand.ml
index 1ef233e7..1555d75b 100644
--- a/tools/compiler_expand.ml
+++ b/tools/compiler_expand.ml
@@ -1,4 +1,5 @@
 type is_partial = TOTAL | PARTIAL;;
+type print_result = Noprint | Print of string;;
 type when_triggered = Always | Option of string;;
 
 let rtl_passes =
@@ -23,21 +24,38 @@ TOTAL, (Option "all_loads_nontrap"), None, "Allnontrap";
 PARTIAL, Always, (Some "Unused globals"), "Unusedglob"
 |];;
 
+let post_rtl_passes =
+[|
+  PARTIAL, Always, (Some "Register allocation"), "Allocation", (Print "LTL");
+  TOTAL, Always, (Some "Branch tunneling"), "Tunneling", Noprint;
+  PARTIAL, Always, (Some "CFG linearization"), "Linearize", Noprint;
+  TOTAL, Always, (Some "Label cleanup"), "CleanupLabels", Noprint;
+  PARTIAL, (Option "debug"), (Some "Debugging info for local variables"), "Debugvar", Noprint;
+  PARTIAL, Always, (Some "Mach generation"), "Stacking", (Print "Mach")
+|];;
+
+let all_passes =
+  Array.concat
+    [Array.mapi
+       (fun i (a,b,c,d) -> (a,b,c,d, Print (Printf.sprintf "RTL %d" (i+1))))
+       rtl_passes;
+     post_rtl_passes];;
+
 let totality = function TOTAL -> "total" | PARTIAL -> "partial";;
 
 let print_rtl_require oc =
-  Array.iter (fun (partial, trigger, time_label, pass_name) ->
+  Array.iter (fun (partial, trigger, time_label, pass_name, printing) ->
       Printf.fprintf oc "Require %s.\n" pass_name)
-    rtl_passes;;
+    all_passes;;
 
 let print_rtl_require_proof oc =
-  Array.iter (fun (partial, trigger, time_label, pass_name) ->
+  Array.iter (fun (partial, trigger, time_label, pass_name, printing) ->
       Printf.fprintf oc "Require %sproof.\n" pass_name)
-    rtl_passes;;
+    all_passes;;
 
 let print_rtl_transf oc =
   Array.iteri
-    (fun i (partial, trigger, time_label, pass_name) ->
+    (fun i (partial, trigger, time_label, pass_name, printing) ->
       output_string oc (match partial with
                         | TOTAL -> "   @@ "
                         | PARTIAL -> "  @@@ ");
@@ -51,17 +69,61 @@ let print_rtl_transf oc =
        | Some s ->
           Printf.fprintf oc "time \"%s\" " s);
       Printf.fprintf oc "%s.transf_program)\n" pass_name;
-      Printf.fprintf oc "   @@ print (print_RTL %d)\n" (succ i)
-    ) rtl_passes;;
+      (match printing with
+       | Noprint -> ()
+       | Print s ->
+           Printf.fprintf oc "   @@ print (print_%s)\n" s)
+    ) all_passes;;
 
 let print_rtl_mkpass oc =
-  Array.iter (fun (partial, trigger, time_label, pass_name) ->
+  Array.iter (fun (partial, trigger, time_label, pass_name, printing) ->
       output_string oc "  ::: mkpass (";
       (match trigger with
        | Always -> ()
        | Option s ->
           Printf.fprintf oc "match_if Compopts.%s " s);
       Printf.fprintf oc "%sproof.match_prog)\n" pass_name)
+    all_passes;;
+
+let print_if kind oc = function
+  | Always -> ()
+  | Option s -> Printf.fprintf oc "%s_if %s " kind s;;
+
+let numbering_base = 7
+                   
+let print_rtl_proof oc =
+  Array.iteri (fun i (partial, trigger, time_label, pass_name, printing) ->
+      let j = i+numbering_base in
+      match partial with
+      | TOTAL ->
+         Printf.fprintf oc "set (p%d := %a%s.transf_program p%d) in *.\n"
+           j (print_if "total") trigger pass_name (pred j)
+      | PARTIAL ->
+         Printf.fprintf oc "destruct (%a%s.transf_program p%d) as [p%d|e] eqn:P%d; simpl in T; try discriminate.\n"
+           (print_if "partial") trigger pass_name (pred j) j j)
+    all_passes;;
+
+let print_rtl_proof2 oc =
+  Array.iteri (fun i (partial, trigger, time_label, pass_name, printing) ->
+      let j = i+numbering_base in
+      Printf.fprintf oc "  exists p%d; split. " j;
+      (match trigger with
+       | Always -> ()
+       | Option _ ->
+          (match partial with
+           | TOTAL -> output_string oc "apply total_if_match. "
+           | PARTIAL -> output_string oc "eapply partial_if_match; eauto. "));
+      Printf.fprintf oc "apply %sproof.transf_program_match; auto.\n" pass_name)
+    all_passes;;
+
+let print_rtl_forward_simulations oc =
+  Array.iter (fun (partial, trigger, time_label, pass_name) ->
+      output_string oc "  eapply compose_forward_simulations.\n    ";
+      (match trigger with
+       | Always -> ()
+       | Option s -> output_string oc "eapply match_if_simulation. eassumption. ");
+      Printf.fprintf oc "eapply %sproof.transf_program_correct; eassumption." pass_name
+    )
     rtl_passes;;
 
 if (Array.length Sys.argv)<>3
@@ -81,6 +143,15 @@ let filename_in = Sys.argv.(1) and filename_out = Sys.argv.(2) in
            print_rtl_require_proof oc
         | "EXPAND_RTL_MKPASS" ->
            print_rtl_mkpass oc
+        | "EXPAND_RTL_PROOF" ->
+           print_rtl_proof oc
+        | "EXPAND_RTL_PROOF2" ->
+           print_rtl_proof2 oc
+        | "EXPAND_ASM_SEMANTICS" ->
+           Printf.fprintf oc "    (Asm.semantics p%d)\n"
+             ((Array.length all_passes) + 7)
+        | "EXPAND_RTL_FORWARD_SIMULATIONS" ->
+           print_rtl_forward_simulations oc
         | line -> (output_string oc line;
                    output_char oc '\n')
       done
-- 
cgit