From 25547c7d1f6a0fb75ff1d8e7287d9305e0dbf293 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 21 Apr 2020 22:42:32 +0200 Subject: generate mkpass --- tools/compiler_expand.ml | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) (limited to 'tools') diff --git a/tools/compiler_expand.ml b/tools/compiler_expand.ml index 7ca3c755..1ef233e7 100644 --- a/tools/compiler_expand.ml +++ b/tools/compiler_expand.ml @@ -53,7 +53,17 @@ let print_rtl_transf oc = Printf.fprintf oc "%s.transf_program)\n" pass_name; Printf.fprintf oc " @@ print (print_RTL %d)\n" (succ i) ) rtl_passes;; - + +let print_rtl_mkpass oc = + Array.iter (fun (partial, trigger, time_label, pass_name) -> + 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) + rtl_passes;; + if (Array.length Sys.argv)<>3 then exit 1;; @@ -69,6 +79,8 @@ let filename_in = Sys.argv.(1) and filename_out = Sys.argv.(2) in print_rtl_require oc | "EXPAND_RTL_REQUIRE_PROOF" -> print_rtl_require_proof oc + | "EXPAND_RTL_MKPASS" -> + print_rtl_mkpass oc | line -> (output_string oc line; output_char oc '\n') done -- cgit