From d075968e1e516ab80460afce57c9bcc15d206c19 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 29 May 2019 11:43:29 +0200 Subject: added -fdiv-i32 and -fdiv-i64 options --- driver/Clflags.ml | 3 +++ driver/Driver.ml | 12 +++++++++--- 2 files changed, 12 insertions(+), 3 deletions(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index b1afab6f..fd5f0e68 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -71,3 +71,6 @@ let option_fglobaladdrtmp = ref false let option_fglobaladdroffset = ref false let option_fxsaddr = ref true let option_coalesce_mem = ref true + +let option_div_i32 = ref "stsud" +let option_div_i64 = ref "stsud" diff --git a/driver/Driver.ml b/driver/Driver.ml index cfafcaa3..314cf31c 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -265,9 +265,13 @@ let num_input_files = ref 0 let cmdline_actions = let f_opt name ref = [Exact("-f" ^ name), Set ref; Exact("-fno-" ^ name), Unset ref] in - let f_opt_str name ref strref = + let f_opt_str name ref strref default = [Exact("-f" ^ name ^ "="), String - (fun s -> (strref := (if s == "" then "list" else s)); ref := true) + (fun s -> (strref := (if s == "" then default else s)); ref := true) + ] in + let f_str name strref default = + [Exact("-f" ^ name ^ "="), String + (fun s -> (strref := (if s == "" then default else s))) ] in [ (* Getting help *) @@ -369,13 +373,15 @@ let cmdline_actions = @ f_opt "cse" option_fcse @ f_opt "redundancy" option_fredundancy @ f_opt "postpass" option_fpostpass - @ f_opt_str "postpass" option_fpostpass option_fpostpass_sched + @ f_opt_str "postpass" option_fpostpass option_fpostpass_sched "list" @ f_opt "inline" option_finline @ f_opt "inline-functions-called-once" option_finline_functions_called_once @ f_opt "globaladdrtmp" option_fglobaladdrtmp @ f_opt "globaladdroffset" option_fglobaladdroffset @ f_opt "xsaddr" option_fxsaddr @ f_opt "coalesce-mem" option_coalesce_mem + @ f_str "div-i32" option_div_i32 "stsud" + @ f_str "div-i64" option_div_i64 "stsud" (* Code generation options *) @ f_opt "fpu" option_ffpu @ f_opt "sse" option_ffpu (* backward compatibility *) -- cgit From 78c4974c0a362cd0ab3bbd80203c0277d267afbb Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 5 Mar 2020 16:57:54 +0100 Subject: streamlined lattice code --- driver/Compiler.v | 1 + 1 file changed, 1 insertion(+) (limited to 'driver') diff --git a/driver/Compiler.v b/driver/Compiler.v index 499feff2..294aad1f 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -43,6 +43,7 @@ Require Constprop. Require CSE. Require ForwardMoves. Require CSE2. +Require CSE3. Require Deadcode. Require Unusedglob. Require Allnontrap. -- cgit From e76b8244db0c8394eb9f62a573ea0f511bd8db31 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 5 Mar 2020 21:26:01 +0100 Subject: CSE3 generate lists of killable --- driver/Compiler.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Compiler.v b/driver/Compiler.v index 294aad1f..a641587c 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -43,7 +43,7 @@ Require Constprop. Require CSE. Require ForwardMoves. Require CSE2. -Require CSE3. +Require CSE3analysis. Require Deadcode. Require Unusedglob. Require Allnontrap. -- cgit From 59413cb4018d09fb3b641a49ab062bc933d5274c Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 10 Mar 2020 19:56:30 +0100 Subject: starts compiling but still fake --- driver/Clflags.ml | 1 + driver/Compiler.v | 26 +++++++++++++++++--------- driver/Compopts.v | 3 +++ 3 files changed, 21 insertions(+), 9 deletions(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 6d6f1df4..f4022941 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -27,6 +27,7 @@ let option_ftailcalls = ref true let option_fconstprop = ref true let option_fcse = ref true let option_fcse2 = ref true +let option_fcse3 = ref true let option_fredundancy = ref true let option_fduplicate = ref false let option_finvertcond = ref true (* only active if option_fduplicate is also true *) diff --git a/driver/Compiler.v b/driver/Compiler.v index a641587c..22955160 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -43,7 +43,7 @@ Require Constprop. Require CSE. Require ForwardMoves. Require CSE2. -Require CSE3analysis. +Require CSE3. Require Deadcode. Require Unusedglob. Require Allnontrap. @@ -69,6 +69,7 @@ Require Constpropproof. Require CSEproof. Require ForwardMovesproof. Require CSE2proof. +Require CSE3proof. Require Deadcodeproof. Require Unusedglobproof. Require Allnontrapproof. @@ -145,14 +146,16 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 7) @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program) @@ print (print_RTL 8) - @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program + @@ total_if Compopts.optim_CSE3 (time "CSE3" CSE3.transf_program) @@ print (print_RTL 9) - @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) + @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program @@ print (print_RTL 10) - @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program + @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) @@ print (print_RTL 11) - @@@ time "Unused globals" Unusedglob.transform_program + @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program @@ print (print_RTL 12) + @@@ time "Unused globals" Unusedglob.transform_program + @@ print (print_RTL 13) @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program @@ -260,6 +263,7 @@ Definition CompCert's_passes := ::: mkpass (match_if Compopts.optim_constprop Renumberproof.match_prog) ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) ::: mkpass (match_if Compopts.optim_CSE2 CSE2proof.match_prog) + ::: mkpass (match_if Compopts.optim_CSE3 CSE3proof.match_prog) ::: mkpass (match_if Compopts.optim_forward_moves ForwardMovesproof.match_prog) ::: mkpass (match_if Compopts.optim_redundancy Deadcodeproof.match_prog) ::: mkpass (match_if Compopts.all_loads_nontrap Allnontrapproof.match_prog) @@ -307,8 +311,9 @@ Proof. set (p12 := total_if optim_constprop Renumber.transf_program p11) in *. destruct (partial_if optim_CSE CSE.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate. set (p13bis := total_if optim_CSE2 CSE2.transf_program p13) in *. - set (p13ter := total_if optim_forward_moves ForwardMoves.transf_program p13bis) in *. - destruct (partial_if optim_redundancy Deadcode.transf_program p13ter) as [p14|e] eqn:P14; simpl in T; try discriminate. + set (p13ter := total_if optim_CSE3 CSE3.transf_program p13bis) in *. + set (p13quater := total_if optim_forward_moves ForwardMoves.transf_program p13ter) in *. + destruct (partial_if optim_redundancy Deadcode.transf_program p13quater) as [p14|e] eqn:P14; simpl in T; try discriminate. set (p14bis := total_if all_loads_nontrap Allnontrap.transf_program p14) in *. destruct (Unusedglob.transform_program p14bis) as [p15|e] eqn:P15; simpl in T; try discriminate. destruct (Allocation.transf_program p15) as [p16|e] eqn:P16; simpl in T; try discriminate. @@ -332,7 +337,8 @@ Proof. exists p12; split. apply total_if_match. apply Renumberproof.transf_program_match. exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. exists p13bis; split. apply total_if_match. apply CSE2proof.transf_program_match. - exists p13ter; split. eapply total_if_match; eauto. apply ForwardMovesproof.transf_program_match. + exists p13ter; split. apply total_if_match. apply CSE3proof.transf_program_match. + exists p13quater; split. eapply total_if_match; eauto. apply ForwardMovesproof.transf_program_match. exists p14; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. exists p14bis; split. eapply total_if_match; eauto. apply Allnontrapproof.transf_program_match. exists p15; split. apply Unusedglobproof.transf_program_match; auto. @@ -393,7 +399,7 @@ Ltac DestructM := destruct H as (p & M & MM); clear H end. repeat DestructM. subst tp. - assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p25)). + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p26)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -423,6 +429,8 @@ Ltac DestructM := eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact CSE2proof.transf_program_correct. eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact CSE3proof.transf_program_correct. + eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact ForwardMovesproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Deadcodeproof.transf_program_correct; eassumption. diff --git a/driver/Compopts.v b/driver/Compopts.v index b4b9f30d..1f952164 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -43,6 +43,9 @@ Parameter optim_CSE: unit -> bool. (** Flag -fcse2. For DMonniaux's common subexpression elimination. *) Parameter optim_CSE2: unit -> bool. +(** Flag -fcse3. For DMonniaux's common subexpression elimination. *) +Parameter optim_CSE3: unit -> bool. + (** Flag -fredundancy. For dead code elimination. *) Parameter optim_redundancy: unit -> bool. -- cgit From d47f93b0f7ced7ae02cfeb8827886ac65e06817d Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 10 Mar 2020 21:35:25 +0100 Subject: -fcse3 command line option --- driver/Driver.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Driver.ml b/driver/Driver.ml index db71aef9..6f32fc33 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -196,6 +196,7 @@ Processing options: (=0: none, =1: limited, =2: full; default is full) -fcse Perform common subexpression elimination [on] -fcse2 Perform inter-loop common subexpression elimination [on] + -fcse3 Perform inter-loop common subexpression elimination [on] -fredundancy Perform redundancy elimination [on] -fpostpass Perform postpass scheduling (only for K1 architecture) [on] -fpostpass= Perform postpass scheduling with the specified optimization [list] @@ -265,7 +266,7 @@ let dump_mnemonics destfile = let optimization_options = [ option_ftailcalls; option_fifconversion; option_fconstprop; - option_fcse; option_fcse2; + option_fcse; option_fcse2; option_fcse3; option_fpostpass; option_fredundancy; option_finline; option_finline_functions_called_once; ] @@ -391,6 +392,7 @@ let cmdline_actions = @ f_opt "const-prop" option_fconstprop @ f_opt "cse" option_fcse @ f_opt "cse2" option_fcse2 + @ f_opt "cse3" option_fcse3 @ f_opt "redundancy" option_fredundancy @ f_opt "postpass" option_fpostpass @ f_opt "duplicate" option_fduplicate -- cgit From f1327f4d4e2fb15c6032959375cdc36ffe20167f Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 12 Mar 2020 14:11:39 +0100 Subject: typing and store stuff --- driver/Compiler.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'driver') diff --git a/driver/Compiler.v b/driver/Compiler.v index c2428d94..47fb8236 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -146,7 +146,7 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 7) @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program) @@ print (print_RTL 8) - @@ total_if Compopts.optim_CSE3 (time "CSE3" CSE3.transf_program) + @@@ partial_if Compopts.optim_CSE3 (time "CSE3" CSE3.transf_program) @@ print (print_RTL 9) @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program @@ print (print_RTL 10) @@ -311,7 +311,7 @@ Proof. set (p12 := total_if optim_constprop Renumber.transf_program p11) in *. destruct (partial_if optim_CSE CSE.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate. set (p13bis := total_if optim_CSE2 CSE2.transf_program p13) in *. - set (p13ter := total_if optim_CSE3 CSE3.transf_program p13bis) in *. + destruct (partial_if optim_CSE3 CSE3.transf_program p13bis) as [p13ter|e] eqn:P13ter; simpl in T; try discriminate. set (p13quater := total_if optim_forward_moves ForwardMoves.transf_program p13ter) in *. destruct (partial_if optim_redundancy Deadcode.transf_program p13quater) as [p14|e] eqn:P14; simpl in T; try discriminate. set (p14bis := total_if all_loads_nontrap Allnontrap.transf_program p14) in *. @@ -337,7 +337,7 @@ Proof. exists p12; split. apply total_if_match. apply Renumberproof.transf_program_match. exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. exists p13bis; split. apply total_if_match. apply CSE2proof.transf_program_match. - exists p13ter; split. apply total_if_match. apply CSE3proof.transf_program_match. + exists p13ter; split. eapply partial_if_match; eauto. apply CSE3proof.transf_program_match. exists p13quater; split. eapply total_if_match; eauto. apply ForwardMovesproof.transf_program_match. exists p14; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. exists p14bis; split. eapply total_if_match; eauto. apply Allnontrapproof.transf_program_match. -- cgit From bbe0809b3cd483ce5fc82e4f2d0a106823c54f26 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 14 Mar 2020 09:19:26 +0100 Subject: CSE3 alias analysis --- driver/Clflags.ml | 5 +++-- driver/Compopts.v | 3 +++ driver/Driver.ml | 6 ++++-- 3 files changed, 10 insertions(+), 4 deletions(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 7e3b23d8..a8594be4 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -25,9 +25,10 @@ let option_ffpu = ref true let option_ffloatconstprop = ref 2 let option_ftailcalls = ref true let option_fconstprop = ref true -let option_fcse = ref true -let option_fcse2 = ref true +let option_fcse = ref false +let option_fcse2 = ref false let option_fcse3 = ref true +let option_fcse3_alias_analysis = ref true let option_fredundancy = ref true let option_fduplicate = ref 0 let option_finvertcond = ref true diff --git a/driver/Compopts.v b/driver/Compopts.v index 1f952164..f1ab4f7b 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -46,6 +46,9 @@ Parameter optim_CSE2: unit -> bool. (** Flag -fcse3. For DMonniaux's common subexpression elimination. *) Parameter optim_CSE3: unit -> bool. +(** Flag -fcse3-alias-analysis. For DMonniaux's common subexpression elimination. *) +Parameter optim_CSE3_alias_analysis: unit -> bool. + (** Flag -fredundancy. For dead code elimination. *) Parameter optim_redundancy: unit -> bool. diff --git a/driver/Driver.ml b/driver/Driver.ml index 12b61d86..133bac0a 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -194,9 +194,10 @@ Processing options: -fconst-prop Perform global constant propagation [on] -ffloat-const-prop Control constant propagation of floats (=0: none, =1: limited, =2: full; default is full) - -fcse Perform common subexpression elimination [on] - -fcse2 Perform inter-loop common subexpression elimination [on] + -fcse Perform common subexpression elimination [off] + -fcse2 Perform inter-loop common subexpression elimination [off] -fcse3 Perform inter-loop common subexpression elimination [on] + -fcse3-alias-analysis Perform inter-loop common subexpression elimination with alias analysis [on] -fredundancy Perform redundancy elimination [on] -fpostpass Perform postpass scheduling (only for K1 architecture) [on] -fpostpass= Perform postpass scheduling with the specified optimization [list] @@ -393,6 +394,7 @@ let cmdline_actions = @ f_opt "cse" option_fcse @ f_opt "cse2" option_fcse2 @ f_opt "cse3" option_fcse3 + @ f_opt "cse3-alias-analysis" option_fcse3_alias_analysis @ f_opt "redundancy" option_fredundancy @ f_opt "postpass" option_fpostpass @ [ Exact "-fduplicate", Integer (fun n -> option_fduplicate := n) ] -- cgit From 07f2bfbd62568e2e0d983ccb33d020bf6985e874 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sun, 29 Mar 2020 18:30:01 +0200 Subject: nop insertion at entrypoint --- driver/Compiler.v | 38 +++++++++++++++++++++++--------------- 1 file changed, 23 insertions(+), 15 deletions(-) (limited to 'driver') diff --git a/driver/Compiler.v b/driver/Compiler.v index 47fb8236..cc1e7917 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -37,6 +37,7 @@ Require Selection. Require RTLgen. Require Tailcall. Require Inlining. +Require FirstNop. Require Renumber. Require Duplicate. Require Constprop. @@ -63,6 +64,7 @@ Require Selectionproof. Require RTLgenproof. Require Tailcallproof. Require Inliningproof. +Require FirstNopproof. Require Renumberproof. Require Duplicateproof. Require Constpropproof. @@ -134,28 +136,30 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 1) @@@ time "Inlining" Inlining.transf_program @@ print (print_RTL 2) - @@ time "Renumbering" Renumber.transf_program + @@ time "Inserting initial nop" FirstNop.transf_program @@ print (print_RTL 3) - @@@ time "Tail-duplicating" Duplicate.transf_program + @@ time "Renumbering" Renumber.transf_program @@ print (print_RTL 4) - @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) + @@@ time "Tail-duplicating" Duplicate.transf_program @@ print (print_RTL 5) - @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program) + @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) @@ print (print_RTL 6) - @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) + @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program) @@ print (print_RTL 7) - @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program) + @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) @@ print (print_RTL 8) - @@@ partial_if Compopts.optim_CSE3 (time "CSE3" CSE3.transf_program) + @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program) @@ print (print_RTL 9) - @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program + @@@ partial_if Compopts.optim_CSE3 (time "CSE3" CSE3.transf_program) @@ print (print_RTL 10) - @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) + @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program @@ print (print_RTL 11) - @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program + @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) @@ print (print_RTL 12) - @@@ time "Unused globals" Unusedglob.transform_program + @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program @@ print (print_RTL 13) + @@@ time "Unused globals" Unusedglob.transform_program + @@ print (print_RTL 14) @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program @@ -257,6 +261,7 @@ Definition CompCert's_passes := ::: mkpass RTLgenproof.match_prog ::: mkpass (match_if Compopts.optim_tailcalls Tailcallproof.match_prog) ::: mkpass Inliningproof.match_prog + ::: mkpass FirstNopproof.match_prog ::: mkpass Renumberproof.match_prog ::: mkpass Duplicateproof.match_prog ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog) @@ -305,8 +310,9 @@ Proof. unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T. simpl in T. set (p7 := total_if optim_tailcalls Tailcall.transf_program p6) in *. destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate. - set (p9 := Renumber.transf_program p8) in *. - destruct (Duplicate.transf_program p9) as [p10|e] eqn:P10; simpl in T; try discriminate. + set (p9 := FirstNop.transf_program p8) in *. + set (p9bis := Renumber.transf_program p9) in *. + destruct (Duplicate.transf_program p9bis) as [p10|e] eqn:P10; simpl in T; try discriminate. set (p11 := total_if optim_constprop Constprop.transf_program p10) in *. set (p12 := total_if optim_constprop Renumber.transf_program p11) in *. destruct (partial_if optim_CSE CSE.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate. @@ -331,7 +337,8 @@ Proof. exists p6; split. apply RTLgenproof.transf_program_match; auto. exists p7; split. apply total_if_match. apply Tailcallproof.transf_program_match. exists p8; split. apply Inliningproof.transf_program_match; auto. - exists p9; split. apply Renumberproof.transf_program_match; auto. + exists p9; split. apply FirstNopproof.transf_program_match; auto. + exists p9bis; split. apply Renumberproof.transf_program_match; auto. exists p10; split. apply Duplicateproof.transf_program_match; auto. exists p11; split. apply total_if_match. apply Constpropproof.transf_program_match. exists p12; split. apply total_if_match. apply Renumberproof.transf_program_match. @@ -399,7 +406,7 @@ Ltac DestructM := destruct H as (p & M & MM); clear H end. repeat DestructM. subst tp. - assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p26)). + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p27)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -417,6 +424,7 @@ Ltac DestructM := eapply match_if_simulation. eassumption. exact Tailcallproof.transf_program_correct. eapply compose_forward_simulations. eapply Inliningproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. eapply FirstNopproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply Duplicateproof.transf_program_correct; eassumption. -- cgit From d0590cab5ee32df395c129ee3edfa2dc3aaa202d Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 1 Apr 2020 13:30:30 +0200 Subject: begin adapting for LICM phase --- driver/Clflags.ml | 1 + driver/Compopts.v | 3 +++ driver/Driver.ml | 2 ++ 3 files changed, 6 insertions(+) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index ff2647a7..ae96e820 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -82,5 +82,6 @@ let option_fxsaddr = ref true let option_faddx = ref false let option_fcoalesce_mem = ref true let option_fforward_moves = ref true +let option_fmove_loop_invariants = ref false let option_all_loads_nontrap = ref false let option_inline_auto_threshold = ref 0 diff --git a/driver/Compopts.v b/driver/Compopts.v index a3181da8..e4dae87d 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -48,6 +48,9 @@ Parameter optim_CSE3: unit -> bool. (** Flag -fcse3-alias-analysis. For DMonniaux's common subexpression elimination. *) Parameter optim_CSE3_alias_analysis: unit -> bool. +(** Flag -fmove-loop-invariants. *) +Parameter optim_move_loop_invariants: unit -> bool. + (** Flag -fredundancy. For dead code elimination. *) Parameter optim_redundancy: unit -> bool. diff --git a/driver/Driver.ml b/driver/Driver.ml index b167dbd1..0f9e637c 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -199,6 +199,7 @@ Processing options: -fcse2 Perform inter-loop common subexpression elimination [off] -fcse3 Perform inter-loop common subexpression elimination [on] -fcse3-alias-analysis Perform inter-loop common subexpression elimination with alias analysis [on] + -fmove-loop-invariants Perform loop-invariant code motion [off] -fredundancy Perform redundancy elimination [on] -fpostpass Perform postpass scheduling (only for K1 architecture) [on] -fpostpass= Perform postpass scheduling with the specified optimization [list] @@ -401,6 +402,7 @@ let cmdline_actions = @ f_opt "cse2" option_fcse2 @ f_opt "cse3" option_fcse3 @ f_opt "cse3-alias-analysis" option_fcse3_alias_analysis + @ f_opt "move-loop-invariants" option_fmove_loop_invariants @ f_opt "redundancy" option_fredundancy @ f_opt "postpass" option_fpostpass @ [ Exact "-fduplicate", Integer (fun n -> option_fduplicate := n) ] -- cgit From 6379f6291eea909426f074db67837b04a1dec9ae Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 1 Apr 2020 14:24:05 +0200 Subject: attempt at compiling --- driver/Compiler.v | 36 ++++++++++++++++++++++++------------ 1 file changed, 24 insertions(+), 12 deletions(-) (limited to 'driver') diff --git a/driver/Compiler.v b/driver/Compiler.v index 5175abdb..dbf62368 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -41,6 +41,7 @@ Require FirstNop. Require Renumber. Require Duplicate. Require Constprop. +Require LICM. Require CSE. Require ForwardMoves. Require CSE2. @@ -68,6 +69,7 @@ Require FirstNopproof. Require Renumberproof. Require Duplicateproof. Require Constpropproof. +Require LICMproof. Require CSEproof. Require ForwardMovesproof. Require CSE2proof. @@ -136,7 +138,7 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 1) @@@ time "Inlining" Inlining.transf_program @@ print (print_RTL 2) - @@ time "Inserting initial nop" FirstNop.transf_program + @@ total_if Compopts.optim_move_loop_invariants (time "Inserting initial nop" FirstNop.transf_program) @@ print (print_RTL 3) @@ time "Renumbering" Renumber.transf_program @@ print (print_RTL 4) @@ -144,22 +146,26 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 5) @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) @@ print (print_RTL 6) - @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program) + @@ time "Renumbering pre LICM" Renumber.transf_program @@ print (print_RTL 7) - @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) + @@@ partial_if Compopts.optim_move_loop_invariants (time "LICM" LICM.transf_program) @@ print (print_RTL 8) - @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program) + @@ total_if Compopts.optim_move_loop_invariants (time "Renumbering pre CSE" Renumber.transf_program) @@ print (print_RTL 9) - @@@ partial_if Compopts.optim_CSE3 (time "CSE3" CSE3.transf_program) + @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) @@ print (print_RTL 10) - @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program + @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program) @@ print (print_RTL 11) - @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) + @@@ partial_if Compopts.optim_CSE3 (time "CSE3" CSE3.transf_program) @@ print (print_RTL 12) - @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program + @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program @@ print (print_RTL 13) - @@@ time "Unused globals" Unusedglob.transform_program + @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) @@ print (print_RTL 14) + @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program + @@ print (print_RTL 15) + @@@ time "Unused globals" Unusedglob.transform_program + @@ print (print_RTL 16) @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program @@ -261,10 +267,11 @@ Definition CompCert's_passes := ::: mkpass RTLgenproof.match_prog ::: mkpass (match_if Compopts.optim_tailcalls Tailcallproof.match_prog) ::: mkpass Inliningproof.match_prog - ::: mkpass FirstNopproof.match_prog + ::: mkpass (match_if Compopts.optim_move_loop_invariants FirstNopproof.match_prog) ::: mkpass Renumberproof.match_prog ::: mkpass (match_if Compopts.optim_duplicate Duplicateproof.match_prog) ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog) + ::: mkpass (match_if Compopts.optim_move_loop_invariants LICMproof.match_prog) ::: mkpass (match_if Compopts.optim_constprop Renumberproof.match_prog) ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) ::: mkpass (match_if Compopts.optim_CSE2 CSE2proof.match_prog) @@ -308,14 +315,19 @@ Proof. destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate. destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate. unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T. simpl in T. + ::: mkpass (match_if Compopts.optim_move_loop_invariants LICM.match_prog) + ::: mkpass (match_if Compopts.optim_move_loop_invariants Renumberproof.match_prog) + ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) set (p7 := total_if optim_tailcalls Tailcall.transf_program p6) in *. destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate. - set (p9 := FirstNop.transf_program p8) in *. + set (p9 := total_if Compopts.optim_move_loop_invariants FirstNop.transf_program p8) in *. set (p9bis := Renumber.transf_program p9) in *. destruct (partial_if optim_duplicate Duplicate.transf_program p9bis) as [p10|e] eqn:P10; simpl in T; try discriminate. set (p11 := total_if optim_constprop Constprop.transf_program p10) in *. set (p12 := total_if optim_constprop Renumber.transf_program p11) in *. - destruct (partial_if optim_CSE CSE.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate. + destruct (partial_if optim_move_loop_invariants LICM.transf_program p12) as [p12bis|e] eqn:P12bis; simpl in T; try discriminate. + set (p12ter :=(total_if optim_move_loop_invariant Renumber.transf_program p12bis)) in *. + destruct (partial_if optim_CSE CSE.transf_program p12ter) as [p13|e] eqn:P13; simpl in T; try discriminate. set (p13bis := total_if optim_CSE2 CSE2.transf_program p13) in *. destruct (partial_if optim_CSE3 CSE3.transf_program p13bis) as [p13ter|e] eqn:P13ter; simpl in T; try discriminate. set (p13quater := total_if optim_forward_moves ForwardMoves.transf_program p13ter) in *. -- cgit From 01f42ef55d91bbb57b47ecc2be7e691165778980 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 1 Apr 2020 15:38:06 +0200 Subject: fix Compiler.v --- driver/Compiler.v | 28 ++++++++++++++++------------ 1 file changed, 16 insertions(+), 12 deletions(-) (limited to 'driver') diff --git a/driver/Compiler.v b/driver/Compiler.v index dbf62368..89a15d93 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -271,8 +271,9 @@ Definition CompCert's_passes := ::: mkpass Renumberproof.match_prog ::: mkpass (match_if Compopts.optim_duplicate Duplicateproof.match_prog) ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog) + ::: mkpass Renumberproof.match_prog ::: mkpass (match_if Compopts.optim_move_loop_invariants LICMproof.match_prog) - ::: mkpass (match_if Compopts.optim_constprop Renumberproof.match_prog) + ::: mkpass (match_if Compopts.optim_move_loop_invariants Renumberproof.match_prog) ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) ::: mkpass (match_if Compopts.optim_CSE2 CSE2proof.match_prog) ::: mkpass (match_if Compopts.optim_CSE3 CSE3proof.match_prog) @@ -315,18 +316,15 @@ Proof. destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate. destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate. unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T. simpl in T. - ::: mkpass (match_if Compopts.optim_move_loop_invariants LICM.match_prog) - ::: mkpass (match_if Compopts.optim_move_loop_invariants Renumberproof.match_prog) - ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) set (p7 := total_if optim_tailcalls Tailcall.transf_program p6) in *. destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate. set (p9 := total_if Compopts.optim_move_loop_invariants FirstNop.transf_program p8) in *. set (p9bis := Renumber.transf_program p9) in *. destruct (partial_if optim_duplicate Duplicate.transf_program p9bis) as [p10|e] eqn:P10; simpl in T; try discriminate. set (p11 := total_if optim_constprop Constprop.transf_program p10) in *. - set (p12 := total_if optim_constprop Renumber.transf_program p11) in *. + set (p12 := Renumber.transf_program p11) in *. destruct (partial_if optim_move_loop_invariants LICM.transf_program p12) as [p12bis|e] eqn:P12bis; simpl in T; try discriminate. - set (p12ter :=(total_if optim_move_loop_invariant Renumber.transf_program p12bis)) in *. + set (p12ter :=(total_if optim_move_loop_invariants Renumber.transf_program p12bis)) in *. destruct (partial_if optim_CSE CSE.transf_program p12ter) as [p13|e] eqn:P13; simpl in T; try discriminate. set (p13bis := total_if optim_CSE2 CSE2.transf_program p13) in *. destruct (partial_if optim_CSE3 CSE3.transf_program p13bis) as [p13ter|e] eqn:P13ter; simpl in T; try discriminate. @@ -349,11 +347,13 @@ Proof. exists p6; split. apply RTLgenproof.transf_program_match; auto. exists p7; split. apply total_if_match. apply Tailcallproof.transf_program_match. exists p8; split. apply Inliningproof.transf_program_match; auto. - exists p9; split. apply FirstNopproof.transf_program_match; auto. - exists p9bis; split. apply Renumberproof.transf_program_match; auto. + exists p9; split. apply total_if_match. apply FirstNopproof.transf_program_match. + exists p9bis; split. apply Renumberproof.transf_program_match. exists p10; split. eapply partial_if_match; eauto. apply Duplicateproof.transf_program_match; auto. exists p11; split. apply total_if_match. apply Constpropproof.transf_program_match. - exists p12; split. apply total_if_match. apply Renumberproof.transf_program_match. + exists p12; split. apply Renumberproof.transf_program_match. + exists p12bis; split. eapply partial_if_match; eauto. apply LICMproof.transf_program_match. + exists p12ter; split. apply total_if_match; eauto. apply Renumberproof.transf_program_match. exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. exists p13bis; split. apply total_if_match. apply CSE2proof.transf_program_match. exists p13ter; split. eapply partial_if_match; eauto. apply CSE3proof.transf_program_match. @@ -418,7 +418,7 @@ Ltac DestructM := destruct H as (p & M & MM); clear H end. repeat DestructM. subst tp. - assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p27)). + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p29)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -436,12 +436,16 @@ Ltac DestructM := eapply match_if_simulation. eassumption. exact Tailcallproof.transf_program_correct. eapply compose_forward_simulations. eapply Inliningproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. eapply FirstNopproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact FirstNopproof.transf_program_correct. eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Duplicateproof.transf_program_correct. eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact Constpropproof.transf_program_correct. + eapply match_if_simulation. eassumption. exact Constpropproof.transf_program_correct. + eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact LICMproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Renumberproof.transf_program_correct. eapply compose_forward_simulations. -- cgit From 87d2c34910a017c13a908cfe2cf2c627e56e6cfe Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 1 Apr 2020 15:46:03 +0200 Subject: reordering passes --- driver/Compiler.v | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'driver') diff --git a/driver/Compiler.v b/driver/Compiler.v index 89a15d93..e6d39152 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -144,9 +144,9 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 4) @@@ partial_if Compopts.optim_duplicate (time "Tail-duplicating" Duplicate.transf_program) @@ print (print_RTL 5) - @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) + @@ time "Renumbering pre constprop" Renumber.transf_program @@ print (print_RTL 6) - @@ time "Renumbering pre LICM" Renumber.transf_program + @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) @@ print (print_RTL 7) @@@ partial_if Compopts.optim_move_loop_invariants (time "LICM" LICM.transf_program) @@ print (print_RTL 8) @@ -270,8 +270,8 @@ Definition CompCert's_passes := ::: mkpass (match_if Compopts.optim_move_loop_invariants FirstNopproof.match_prog) ::: mkpass Renumberproof.match_prog ::: mkpass (match_if Compopts.optim_duplicate Duplicateproof.match_prog) - ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog) ::: mkpass Renumberproof.match_prog + ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog) ::: mkpass (match_if Compopts.optim_move_loop_invariants LICMproof.match_prog) ::: mkpass (match_if Compopts.optim_move_loop_invariants Renumberproof.match_prog) ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) @@ -321,8 +321,8 @@ Proof. set (p9 := total_if Compopts.optim_move_loop_invariants FirstNop.transf_program p8) in *. set (p9bis := Renumber.transf_program p9) in *. destruct (partial_if optim_duplicate Duplicate.transf_program p9bis) as [p10|e] eqn:P10; simpl in T; try discriminate. - set (p11 := total_if optim_constprop Constprop.transf_program p10) in *. - set (p12 := Renumber.transf_program p11) in *. + set (p11 := Renumber.transf_program p10) in *. + set (p12 := total_if optim_constprop Constprop.transf_program p11) in *. destruct (partial_if optim_move_loop_invariants LICM.transf_program p12) as [p12bis|e] eqn:P12bis; simpl in T; try discriminate. set (p12ter :=(total_if optim_move_loop_invariants Renumber.transf_program p12bis)) in *. destruct (partial_if optim_CSE CSE.transf_program p12ter) as [p13|e] eqn:P13; simpl in T; try discriminate. @@ -350,8 +350,8 @@ Proof. exists p9; split. apply total_if_match. apply FirstNopproof.transf_program_match. exists p9bis; split. apply Renumberproof.transf_program_match. exists p10; split. eapply partial_if_match; eauto. apply Duplicateproof.transf_program_match; auto. - exists p11; split. apply total_if_match. apply Constpropproof.transf_program_match. - exists p12; split. apply Renumberproof.transf_program_match. + exists p11; split. apply Renumberproof.transf_program_match. + exists p12; split. apply total_if_match. apply Constpropproof.transf_program_match. exists p12bis; split. eapply partial_if_match; eauto. apply LICMproof.transf_program_match. exists p12ter; split. apply total_if_match; eauto. apply Renumberproof.transf_program_match. exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. @@ -442,8 +442,8 @@ Ltac DestructM := eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Duplicateproof.transf_program_correct. eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact Constpropproof.transf_program_correct. eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. + eapply match_if_simulation. eassumption. exact Constpropproof.transf_program_correct. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact LICMproof.transf_program_correct; eassumption. eapply compose_forward_simulations. -- cgit From 1972df30827022dcb39110cddf9032eaa3dc61b9 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 8 Apr 2020 11:35:17 +0200 Subject: begin installing profiling --- driver/Clflags.ml | 3 +++ driver/Compopts.v | 3 +++ driver/Driver.ml | 4 +++- 3 files changed, 9 insertions(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 6986fb96..87c8d9c8 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -82,3 +82,6 @@ let option_fcoalesce_mem = ref true let option_fforward_moves = ref true let option_all_loads_nontrap = ref false let option_inline_auto_threshold = ref 0 + +let option_profile_arcs = ref false + diff --git a/driver/Compopts.v b/driver/Compopts.v index 848657e5..245322ef 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -75,6 +75,9 @@ Parameter all_loads_nontrap: unit -> bool. (** Flag -fforward-moves. Forward moves after CSE. *) Parameter optim_forward_moves: unit -> bool. +(** Flag -fprofile-arcs. Add profiling logger. *) +Parameter profile_arcs : unit -> bool. + (* TODO is there a more appropriate place? *) Require Import Coqlib. Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f. diff --git a/driver/Driver.ml b/driver/Driver.ml index 388482a0..909ef0d5 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -223,6 +223,7 @@ Code generation options: (use -fno- to turn off -f) -falign-branch-targets Set alignment (in bytes) of branch targets -falign-cond-branches Set alignment (in bytes) of conditional branches -fcommon Put uninitialized globals in the common section [on]. + -fprofile-arcs Profile branches [off]. |} ^ target_help ^ toolchain_help ^ @@ -412,7 +413,8 @@ let cmdline_actions = @ f_opt "coalesce-mem" option_fcoalesce_mem @ f_opt "all-loads-nontrap" option_all_loads_nontrap @ f_opt "forward-moves" option_fforward_moves -(* Code generation options *) + (* Code generation options *) + @ f_opt "profile-arcs" option_profile_arcs @ f_opt "fpu" option_ffpu @ f_opt "sse" option_ffpu (* backward compatibility *) @ [ -- cgit From 3c30567c452f030267d0fb09465adf8d7b44a90d Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 8 Apr 2020 12:36:24 +0200 Subject: installed Profiling (not finished) --- driver/Compiler.v | 33 +++++++++++++++++++++------------ 1 file changed, 21 insertions(+), 12 deletions(-) (limited to 'driver') diff --git a/driver/Compiler.v b/driver/Compiler.v index 499feff2..dc32cd3f 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -37,6 +37,7 @@ Require Selection. Require RTLgen. Require Tailcall. Require Inlining. +Require Profiling. Require Renumber. Require Duplicate. Require Constprop. @@ -62,6 +63,7 @@ Require Selectionproof. Require RTLgenproof. Require Tailcallproof. Require Inliningproof. +Require Profilingproof. Require Renumberproof. Require Duplicateproof. Require Constpropproof. @@ -132,26 +134,28 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 1) @@@ time "Inlining" Inlining.transf_program @@ print (print_RTL 2) - @@ time "Renumbering" Renumber.transf_program + @@ total_if Compopts.profile_arcs (time "Profiling insertion" Profiling.transf_program) @@ print (print_RTL 3) - @@@ partial_if Compopts.optim_duplicate (time "Tail-duplicating" Duplicate.transf_program) + @@ time "Renumbering" Renumber.transf_program @@ print (print_RTL 4) - @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) + @@@ partial_if Compopts.optim_duplicate (time "Tail-duplicating" Duplicate.transf_program) @@ print (print_RTL 5) - @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program) + @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) @@ print (print_RTL 6) - @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) + @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program) @@ print (print_RTL 7) - @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program) + @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) @@ print (print_RTL 8) - @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program + @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program) @@ print (print_RTL 9) - @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) + @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program @@ print (print_RTL 10) - @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program + @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) @@ print (print_RTL 11) - @@@ time "Unused globals" Unusedglob.transform_program + @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program @@ print (print_RTL 12) + @@@ time "Unused globals" Unusedglob.transform_program + @@ print (print_RTL 13) @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program @@ -253,6 +257,7 @@ Definition CompCert's_passes := ::: mkpass RTLgenproof.match_prog ::: mkpass (match_if Compopts.optim_tailcalls Tailcallproof.match_prog) ::: mkpass Inliningproof.match_prog + ::: mkpass (match_if Compopts.profile_arcs Profilingproof.match_prog) ::: mkpass Renumberproof.match_prog ::: mkpass (match_if Compopts.optim_duplicate Duplicateproof.match_prog) ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog) @@ -300,7 +305,8 @@ Proof. unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T. simpl in T. set (p7 := total_if optim_tailcalls Tailcall.transf_program p6) in *. destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate. - set (p9 := Renumber.transf_program p8) in *. + set (p8bis := total_if profile_arcs Profiling.transf_program p8) in *. + set (p9 := Renumber.transf_program p8bis) in *. destruct (partial_if optim_duplicate Duplicate.transf_program p9) as [p10|e] eqn:P10; simpl in T; try discriminate. set (p11 := total_if optim_constprop Constprop.transf_program p10) in *. set (p12 := total_if optim_constprop Renumber.transf_program p11) in *. @@ -325,6 +331,7 @@ Proof. exists p6; split. apply RTLgenproof.transf_program_match; auto. exists p7; split. apply total_if_match. apply Tailcallproof.transf_program_match. exists p8; split. apply Inliningproof.transf_program_match; auto. + exists p8bis; split. apply total_if_match. apply Profilingproof.transf_program_match; auto. exists p9; split. apply Renumberproof.transf_program_match; auto. exists p10; split. eapply partial_if_match; eauto. apply Duplicateproof.transf_program_match; auto. exists p11; split. apply total_if_match. apply Constpropproof.transf_program_match. @@ -392,7 +399,7 @@ Ltac DestructM := destruct H as (p & M & MM); clear H end. repeat DestructM. subst tp. - assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p25)). + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p26)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -410,6 +417,8 @@ Ltac DestructM := eapply match_if_simulation. eassumption. exact Tailcallproof.transf_program_correct. eapply compose_forward_simulations. eapply Inliningproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact Profilingproof.transf_program_correct. eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Duplicateproof.transf_program_correct. -- cgit From 96165dbec88ab4c951d99e64e51f5c55a1244137 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 8 Apr 2020 16:28:00 +0200 Subject: fixed a bug in support libraries; reload profiling info --- driver/Clflags.ml | 1 - driver/Driver.ml | 1 + 2 files changed, 1 insertion(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 87c8d9c8..600c3371 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -84,4 +84,3 @@ let option_all_loads_nontrap = ref false let option_inline_auto_threshold = ref 0 let option_profile_arcs = ref false - diff --git a/driver/Driver.ml b/driver/Driver.ml index 909ef0d5..7fbcb025 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -328,6 +328,7 @@ let cmdline_actions = _Regexp "-O[123]$", Unit (set_all optimization_options); Exact "-Os", Set option_Osize; Exact "-Obranchless", Set option_Obranchless; + Exact "-fprofile-use=", String (fun s -> Profilingaux.load_profiling_info s); Exact "-finline-auto-threshold", Integer (fun n -> option_inline_auto_threshold := n); Exact "-fsmall-data", Integer(fun n -> option_small_data := n); Exact "-fsmall-const", Integer(fun n -> option_small_const := n); -- cgit From c3f5f3dbd088091e3fab9f357b01693932d148f8 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 8 Apr 2020 17:02:45 +0200 Subject: reloading and exploiting seems to work --- driver/Clflags.ml | 1 + driver/Compiler.v | 33 +++++++++++++++++++++------------ driver/Compopts.v | 3 +++ driver/Driver.ml | 4 +++- 4 files changed, 28 insertions(+), 13 deletions(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 600c3371..e8f7cef2 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -84,3 +84,4 @@ let option_all_loads_nontrap = ref false let option_inline_auto_threshold = ref 0 let option_profile_arcs = ref false +let option_fbranch_probabilities = ref true diff --git a/driver/Compiler.v b/driver/Compiler.v index dc32cd3f..3f0ac3e5 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -38,6 +38,7 @@ Require RTLgen. Require Tailcall. Require Inlining. Require Profiling. +Require ProfilingExploit. Require Renumber. Require Duplicate. Require Constprop. @@ -64,6 +65,7 @@ Require RTLgenproof. Require Tailcallproof. Require Inliningproof. Require Profilingproof. +Require ProfilingExploitproof. Require Renumberproof. Require Duplicateproof. Require Constpropproof. @@ -136,26 +138,28 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 2) @@ total_if Compopts.profile_arcs (time "Profiling insertion" Profiling.transf_program) @@ print (print_RTL 3) - @@ time "Renumbering" Renumber.transf_program + @@ total_if Compopts.branch_probabilities (time "Profiling use" ProfilingExploit.transf_program) @@ print (print_RTL 4) - @@@ partial_if Compopts.optim_duplicate (time "Tail-duplicating" Duplicate.transf_program) + @@ time "Renumbering" Renumber.transf_program @@ print (print_RTL 5) - @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) + @@@ partial_if Compopts.optim_duplicate (time "Tail-duplicating" Duplicate.transf_program) @@ print (print_RTL 6) - @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program) + @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) @@ print (print_RTL 7) - @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) + @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program) @@ print (print_RTL 8) - @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program) + @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) @@ print (print_RTL 9) - @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program + @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program) @@ print (print_RTL 10) - @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) + @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program @@ print (print_RTL 11) - @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program + @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) @@ print (print_RTL 12) - @@@ time "Unused globals" Unusedglob.transform_program + @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program @@ print (print_RTL 13) + @@@ time "Unused globals" Unusedglob.transform_program + @@ print (print_RTL 14) @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program @@ -258,6 +262,7 @@ Definition CompCert's_passes := ::: mkpass (match_if Compopts.optim_tailcalls Tailcallproof.match_prog) ::: mkpass Inliningproof.match_prog ::: mkpass (match_if Compopts.profile_arcs Profilingproof.match_prog) + ::: mkpass (match_if Compopts.branch_probabilities ProfilingExploitproof.match_prog) ::: mkpass Renumberproof.match_prog ::: mkpass (match_if Compopts.optim_duplicate Duplicateproof.match_prog) ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog) @@ -306,7 +311,8 @@ Proof. set (p7 := total_if optim_tailcalls Tailcall.transf_program p6) in *. destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate. set (p8bis := total_if profile_arcs Profiling.transf_program p8) in *. - set (p9 := Renumber.transf_program p8bis) in *. + set (p8ter := total_if branch_probabilities ProfilingExploit.transf_program p8bis) in *. + set (p9 := Renumber.transf_program p8ter) in *. destruct (partial_if optim_duplicate Duplicate.transf_program p9) as [p10|e] eqn:P10; simpl in T; try discriminate. set (p11 := total_if optim_constprop Constprop.transf_program p10) in *. set (p12 := total_if optim_constprop Renumber.transf_program p11) in *. @@ -332,6 +338,7 @@ Proof. exists p7; split. apply total_if_match. apply Tailcallproof.transf_program_match. exists p8; split. apply Inliningproof.transf_program_match; auto. exists p8bis; split. apply total_if_match. apply Profilingproof.transf_program_match; auto. + exists p8ter; split. apply total_if_match. apply ProfilingExploitproof.transf_program_match; auto. exists p9; split. apply Renumberproof.transf_program_match; auto. exists p10; split. eapply partial_if_match; eauto. apply Duplicateproof.transf_program_match; auto. exists p11; split. apply total_if_match. apply Constpropproof.transf_program_match. @@ -399,7 +406,7 @@ Ltac DestructM := destruct H as (p & M & MM); clear H end. repeat DestructM. subst tp. - assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p26)). + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p27)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -419,6 +426,8 @@ Ltac DestructM := eapply Inliningproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Profilingproof.transf_program_correct. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact ProfilingExploitproof.transf_program_correct. eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Duplicateproof.transf_program_correct. diff --git a/driver/Compopts.v b/driver/Compopts.v index 245322ef..98cbcc37 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -78,6 +78,9 @@ Parameter optim_forward_moves: unit -> bool. (** Flag -fprofile-arcs. Add profiling logger. *) Parameter profile_arcs : unit -> bool. +(** Flag -fbranch_probabilities. Use profiling information if available *) +Parameter branch_probabilities : unit -> bool. + (* TODO is there a more appropriate place? *) Require Import Coqlib. Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f. diff --git a/driver/Driver.ml b/driver/Driver.ml index 7fbcb025..29fbaa7c 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -222,8 +222,10 @@ Code generation options: (use -fno- to turn off -f) -falign-functions Set alignment (in bytes) of function entry points -falign-branch-targets Set alignment (in bytes) of branch targets -falign-cond-branches Set alignment (in bytes) of conditional branches - -fcommon Put uninitialized globals in the common section [on]. + -fcommon Put uninitialized globals in the common section [on] -fprofile-arcs Profile branches [off]. + -fprofile-use= filename Use profiling information in filename + -fbranch-probabilities Use profiling information (if available) for branches [on] |} ^ target_help ^ toolchain_help ^ -- cgit From 7aca3fcf600365b416865a6b6bc6ecc9852b08df Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 8 Apr 2020 17:24:09 +0200 Subject: -fbranch-probabilities --- driver/Driver.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Driver.ml b/driver/Driver.ml index 29fbaa7c..0f716168 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -417,7 +417,8 @@ let cmdline_actions = @ f_opt "all-loads-nontrap" option_all_loads_nontrap @ f_opt "forward-moves" option_fforward_moves (* Code generation options *) - @ f_opt "profile-arcs" option_profile_arcs + @ f_opt "profile-arcs" option_profile_arcs + @ f_opt "branch-probabilities" option_fbranch_probabilities @ f_opt "fpu" option_ffpu @ f_opt "sse" option_ffpu (* backward compatibility *) @ [ -- cgit From a95735290d61f50a388895ef86627becd67c4553 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sun, 19 Apr 2020 20:04:15 +0200 Subject: activate LICM --- driver/Clflags.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index ae96e820..8deb5224 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -82,6 +82,6 @@ let option_fxsaddr = ref true let option_faddx = ref false let option_fcoalesce_mem = ref true let option_fforward_moves = ref true -let option_fmove_loop_invariants = ref false +let option_fmove_loop_invariants = ref true let option_all_loads_nontrap = ref false let option_inline_auto_threshold = ref 0 -- cgit From eead578fde08a1555086ed75714bca3ca1f9b1dc Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sun, 19 Apr 2020 21:14:21 +0200 Subject: add options for controlling madd and notrap selection --- driver/Clflags.ml | 4 +++- driver/Compopts.v | 3 +++ driver/Driver.ml | 2 ++ 3 files changed, 8 insertions(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 8deb5224..8e3305ef 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -79,9 +79,11 @@ let use_standard_headers = ref Configuration.has_standard_headers let option_fglobaladdrtmp = ref false let option_fglobaladdroffset = ref false let option_fxsaddr = ref true -let option_faddx = ref false +let option_faddx = ref false +let option_fmadd = ref true let option_fcoalesce_mem = ref true let option_fforward_moves = ref true let option_fmove_loop_invariants = ref true +let option_fnontrap_loads = ref true let option_all_loads_nontrap = ref false let option_inline_auto_threshold = ref 0 diff --git a/driver/Compopts.v b/driver/Compopts.v index e4dae87d..5acd2640 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -69,6 +69,9 @@ Parameter optim_xsaddr: unit -> bool. (** FIXME TEMPORARY Flag -fcoaelesce-mem. Fuse (default true) *) Parameter optim_coalesce_mem: unit -> bool. +(* FIXME TEMPORARY Flag -faddx. Fuse (default true) *) +Parameter optim_madd: unit -> bool. + (** FIXME TEMPORARY Flag -faddx. Fuse (default false) *) Parameter optim_addx: unit -> bool. diff --git a/driver/Driver.ml b/driver/Driver.ml index 0f9e637c..6a9e9b92 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -415,6 +415,8 @@ let cmdline_actions = @ f_opt "globaladdroffset" option_fglobaladdroffset @ f_opt "xsaddr" option_fxsaddr @ f_opt "addx" option_faddx + @ f_opt "madd" option_fmadd + @ f_opt "nontrap-loads" option_fnontrap_loads @ f_opt "coalesce-mem" option_fcoalesce_mem @ f_opt "all-loads-nontrap" option_all_loads_nontrap @ f_opt "forward-moves" option_fforward_moves -- cgit From 9cc12b684ee6833971c9549aa76cc683ba931090 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 21 Apr 2020 22:08:07 +0200 Subject: begin scripting the Compiler.v file --- driver/Compiler.v | 568 ------------------------------------------------ driver/Compiler.vexpand | 533 +++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 533 insertions(+), 568 deletions(-) delete mode 100644 driver/Compiler.v create mode 100644 driver/Compiler.vexpand (limited to 'driver') diff --git a/driver/Compiler.v b/driver/Compiler.v deleted file mode 100644 index 69041ab0..00000000 --- a/driver/Compiler.v +++ /dev/null @@ -1,568 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(** The whole compiler and its proof of semantic preservation *) - -(** Libraries. *) -Require Import String. -Require Import Coqlib Errors. -Require Import AST Linking Smallstep. -(** Languages (syntax and semantics). *) -Require Ctypes Csyntax Csem Cstrategy Cexec. -Require Clight. -Require Csharpminor. -Require Cminor. -Require CminorSel. -Require RTL. -Require LTL. -Require Linear. -Require Mach. -Require Asm. -(** Translation passes. *) -Require Initializers. -Require SimplExpr. -Require SimplLocals. -Require Cshmgen. -Require Cminorgen. -Require Selection. -Require RTLgen. -Require Tailcall. -Require Inlining. -Require Profiling. -Require ProfilingExploit. -Require FirstNop. -Require Renumber. -Require Duplicate. -Require Constprop. -Require LICM. -Require CSE. -Require ForwardMoves. -Require CSE2. -Require CSE3. -Require Deadcode. -Require Unusedglob. -Require Allnontrap. -Require Allocation. -Require Tunneling. -Require Linearize. -Require CleanupLabels. -Require Debugvar. -Require Stacking. -Require Asmgen. -(** Proofs of semantic preservation. *) -Require SimplExprproof. -Require SimplLocalsproof. -Require Cshmgenproof. -Require Cminorgenproof. -Require Selectionproof. -Require RTLgenproof. -Require Tailcallproof. -Require Inliningproof. -Require Profilingproof. -Require ProfilingExploitproof. -Require FirstNopproof. -Require Renumberproof. -Require Duplicateproof. -Require Constpropproof. -Require LICMproof. -Require CSEproof. -Require ForwardMovesproof. -Require CSE2proof. -Require CSE3proof. -Require Deadcodeproof. -Require Unusedglobproof. -Require Allnontrapproof. -Require Allocproof. -Require Tunnelingproof. -Require Linearizeproof. -Require CleanupLabelsproof. -Require Debugvarproof. -Require Stackingproof. -Require Import Asmgenproof. -(** Command-line flags. *) -Require Import Compopts. - -(** Pretty-printers (defined in Caml). *) -Parameter print_Clight: Clight.program -> unit. -Parameter print_Cminor: Cminor.program -> unit. -Parameter print_RTL: Z -> RTL.program -> unit. -Parameter print_LTL: LTL.program -> unit. -Parameter print_Mach: Mach.program -> unit. - -Local Open Scope string_scope. - -(** * Composing the translation passes *) - -(** We first define useful monadic composition operators, - along with funny (but convenient) notations. *) - -Definition apply_total (A B: Type) (x: res A) (f: A -> B) : res B := - match x with Error msg => Error msg | OK x1 => OK (f x1) end. - -Definition apply_partial (A B: Type) - (x: res A) (f: A -> res B) : res B := - match x with Error msg => Error msg | OK x1 => f x1 end. - -Notation "a @@@ b" := - (apply_partial _ _ a b) (at level 50, left associativity). -Notation "a @@ b" := - (apply_total _ _ a b) (at level 50, left associativity). - -Definition print {A: Type} (printer: A -> unit) (prog: A) : A := - let unused := printer prog in prog. - -Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f. - -Definition total_if {A: Type} - (flag: unit -> bool) (f: A -> A) (prog: A) : A := - if flag tt then f prog else prog. - -Definition partial_if {A: Type} - (flag: unit -> bool) (f: A -> res A) (prog: A) : res A := - if flag tt then f prog else OK prog. - -(** We define three translation functions for whole programs: one - starting with a C program, one with a Cminor program, one with an - RTL program. The three translations produce Asm programs ready for - pretty-printing and assembling. *) - -Definition transf_rtl_program (f: RTL.program) : res Asm.program := - OK f - @@ print (print_RTL 0) - @@ total_if Compopts.optim_tailcalls (time "Tail calls" Tailcall.transf_program) - @@ print (print_RTL 1) - @@@ time "Inlining" Inlining.transf_program - @@ print (print_RTL 2) - @@ total_if Compopts.profile_arcs (time "Profiling insertion" Profiling.transf_program) - @@ print (print_RTL 3) - @@ total_if Compopts.branch_probabilities (time "Profiling use" ProfilingExploit.transf_program) - @@ print (print_RTL 4) - @@ total_if Compopts.optim_move_loop_invariants (time "Inserting initial nop" FirstNop.transf_program) - @@ print (print_RTL 5) - @@ time "Renumbering" Renumber.transf_program - @@ print (print_RTL 6) - @@@ partial_if Compopts.optim_duplicate (time "Tail-duplicating" Duplicate.transf_program) - @@ print (print_RTL 7) - @@ time "Renumbering pre constprop" Renumber.transf_program - @@ print (print_RTL 8) - @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) - @@ print (print_RTL 9) - @@@ partial_if Compopts.optim_move_loop_invariants (time "LICM" LICM.transf_program) - @@ print (print_RTL 10) - @@ total_if Compopts.optim_move_loop_invariants (time "Renumbering pre CSE" Renumber.transf_program) - @@ print (print_RTL 11) - @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) - @@ print (print_RTL 12) - @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program) - @@ print (print_RTL 13) - @@@ partial_if Compopts.optim_CSE3 (time "CSE3" CSE3.transf_program) - @@ print (print_RTL 14) - @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program - @@ print (print_RTL 15) - @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) - @@ print (print_RTL 16) - @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program - @@ print (print_RTL 17) - @@@ time "Unused globals" Unusedglob.transform_program - @@ print (print_RTL 18) - @@@ time "Register allocation" Allocation.transf_program - @@ print print_LTL - @@ time "Branch tunneling" Tunneling.tunnel_program - @@@ time "CFG linearization" Linearize.transf_program - @@ time "Label cleanup" CleanupLabels.transf_program - @@@ partial_if Compopts.debug (time "Debugging info for local variables" Debugvar.transf_program) - @@@ time "Mach generation" Stacking.transf_program - @@ print print_Mach - @@@ time "Total Mach->Asm generation" Asmgen.transf_program. - -Definition transf_cminor_program (p: Cminor.program) : res Asm.program := - OK p - @@ print print_Cminor - @@@ time "Instruction selection" Selection.sel_program - @@@ time "RTL generation" RTLgen.transl_program - @@@ transf_rtl_program. - -Definition transf_clight_program (p: Clight.program) : res Asm.program := - OK p - @@ print print_Clight - @@@ time "Simplification of locals" SimplLocals.transf_program - @@@ time "C#minor generation" Cshmgen.transl_program - @@@ time "Cminor generation" Cminorgen.transl_program - @@@ transf_cminor_program. - -Definition transf_c_program (p: Csyntax.program) : res Asm.program := - OK p - @@@ time "Clight generation" SimplExpr.transl_program - @@@ transf_clight_program. - -(** Force [Initializers] and [Cexec] to be extracted as well. *) - -Definition transl_init := Initializers.transl_init. -Definition cexec_do_step := Cexec.do_step. - -(** The following lemmas help reason over compositions of passes. *) - -Lemma print_identity: - forall (A: Type) (printer: A -> unit) (prog: A), - print printer prog = prog. -Proof. - intros; unfold print. destruct (printer prog); auto. -Qed. - -Lemma compose_print_identity: - forall (A: Type) (x: res A) (f: A -> unit), - x @@ print f = x. -Proof. - intros. destruct x; simpl. rewrite print_identity. auto. auto. -Qed. - -(** * Relational specification of compilation *) - -Definition match_if {A: Type} (flag: unit -> bool) (R: A -> A -> Prop): A -> A -> Prop := - if flag tt then R else eq. - -Lemma total_if_match: - forall (A: Type) (flag: unit -> bool) (f: A -> A) (rel: A -> A -> Prop) (prog: A), - (forall p, rel p (f p)) -> - match_if flag rel prog (total_if flag f prog). -Proof. - intros. unfold match_if, total_if. destruct (flag tt); auto. -Qed. - -Lemma partial_if_match: - forall (A: Type) (flag: unit -> bool) (f: A -> res A) (rel: A -> A -> Prop) (prog tprog: A), - (forall p tp, f p = OK tp -> rel p tp) -> - partial_if flag f prog = OK tprog -> - match_if flag rel prog tprog. -Proof. - intros. unfold match_if, partial_if in *. destruct (flag tt). auto. congruence. -Qed. - -Instance TransfIfLink {A: Type} {LA: Linker A} - (flag: unit -> bool) (transf: A -> A -> Prop) (TL: TransfLink transf) - : TransfLink (match_if flag transf). -Proof. - unfold match_if. destruct (flag tt). -- auto. -- red; intros. subst tp1 tp2. exists p; auto. -Qed. - -(** This is the list of compilation passes of CompCert in relational style. - Each pass is characterized by a [match_prog] relation between its - input code and its output code. The [mkpass] and [:::] combinators, - defined in module [Linking], ensure that the passes are composable - (the output language of a pass is the input language of the next pass) - and that they commute with linking (property [TransfLink], inferred - by the type class mechanism of Coq). *) - -Local Open Scope linking_scope. - -Definition CompCert's_passes := - mkpass SimplExprproof.match_prog - ::: mkpass SimplLocalsproof.match_prog - ::: mkpass Cshmgenproof.match_prog - ::: mkpass Cminorgenproof.match_prog - ::: mkpass Selectionproof.match_prog - ::: mkpass RTLgenproof.match_prog - ::: mkpass (match_if Compopts.optim_tailcalls Tailcallproof.match_prog) - ::: mkpass Inliningproof.match_prog - ::: mkpass (match_if Compopts.profile_arcs Profilingproof.match_prog) - ::: mkpass (match_if Compopts.branch_probabilities ProfilingExploitproof.match_prog) - ::: mkpass (match_if Compopts.optim_move_loop_invariants FirstNopproof.match_prog) - ::: mkpass Renumberproof.match_prog - ::: mkpass (match_if Compopts.optim_duplicate Duplicateproof.match_prog) - ::: mkpass Renumberproof.match_prog - ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog) - ::: mkpass (match_if Compopts.optim_move_loop_invariants LICMproof.match_prog) - ::: mkpass (match_if Compopts.optim_move_loop_invariants Renumberproof.match_prog) - ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) - ::: mkpass (match_if Compopts.optim_CSE2 CSE2proof.match_prog) - ::: mkpass (match_if Compopts.optim_CSE3 CSE3proof.match_prog) - ::: mkpass (match_if Compopts.optim_forward_moves ForwardMovesproof.match_prog) - ::: mkpass (match_if Compopts.optim_redundancy Deadcodeproof.match_prog) - ::: mkpass (match_if Compopts.all_loads_nontrap Allnontrapproof.match_prog) - ::: mkpass Unusedglobproof.match_prog - ::: mkpass Allocproof.match_prog - ::: mkpass Tunnelingproof.match_prog - ::: mkpass Linearizeproof.match_prog - ::: mkpass CleanupLabelsproof.match_prog - ::: mkpass (match_if Compopts.debug Debugvarproof.match_prog) - ::: mkpass Stackingproof.match_prog - ::: mkpass Asmgenproof.match_prog - ::: pass_nil _. - -(** Composing the [match_prog] relations above, we obtain the relation - between CompCert C sources and Asm code that characterize CompCert's - compilation. *) - -Definition match_prog: Csyntax.program -> Asm.program -> Prop := - pass_match (compose_passes CompCert's_passes). - -(** The [transf_c_program] function, when successful, produces - assembly code that is in the [match_prog] relation with the source C program. *) - -Theorem transf_c_program_match: - forall p tp, - transf_c_program p = OK tp -> - match_prog p tp. -Proof. - intros p tp T. - unfold transf_c_program, time in T. simpl in T. - destruct (SimplExpr.transl_program p) as [p1|e] eqn:P1; simpl in T; try discriminate. - unfold transf_clight_program, time in T. rewrite ! compose_print_identity in T. simpl in T. - destruct (SimplLocals.transf_program p1) as [p2|e] eqn:P2; simpl in T; try discriminate. - destruct (Cshmgen.transl_program p2) as [p3|e] eqn:P3; simpl in T; try discriminate. - destruct (Cminorgen.transl_program p3) as [p4|e] eqn:P4; simpl in T; try discriminate. - unfold transf_cminor_program, time in T. rewrite ! compose_print_identity in T. simpl in T. - destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate. - destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate. - unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T. simpl in T. - set (p7 := total_if optim_tailcalls Tailcall.transf_program p6) in *. - destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate. - set (p8bis := total_if profile_arcs Profiling.transf_program p8) in *. - set (p8ter := total_if branch_probabilities ProfilingExploit.transf_program p8bis) in *. - set (p9 := total_if Compopts.optim_move_loop_invariants FirstNop.transf_program p8ter) in *. - set (p9bis := Renumber.transf_program p9) in *. - destruct (partial_if optim_duplicate Duplicate.transf_program p9bis) as [p10|e] eqn:P10; simpl in T; try discriminate. - set (p11 := Renumber.transf_program p10) in *. - set (p12 := total_if optim_constprop Constprop.transf_program p11) in *. - destruct (partial_if optim_move_loop_invariants LICM.transf_program p12) as [p12bis|e] eqn:P12bis; simpl in T; try discriminate. - set (p12ter :=(total_if optim_move_loop_invariants Renumber.transf_program p12bis)) in *. - destruct (partial_if optim_CSE CSE.transf_program p12ter) as [p13|e] eqn:P13; simpl in T; try discriminate. - set (p13bis := total_if optim_CSE2 CSE2.transf_program p13) in *. - destruct (partial_if optim_CSE3 CSE3.transf_program p13bis) as [p13ter|e] eqn:P13ter; simpl in T; try discriminate. - set (p13quater := total_if optim_forward_moves ForwardMoves.transf_program p13ter) in *. - destruct (partial_if optim_redundancy Deadcode.transf_program p13quater) as [p14|e] eqn:P14; simpl in T; try discriminate. - set (p14bis := total_if all_loads_nontrap Allnontrap.transf_program p14) in *. - destruct (Unusedglob.transform_program p14bis) as [p15|e] eqn:P15; simpl in T; try discriminate. - destruct (Allocation.transf_program p15) as [p16|e] eqn:P16; simpl in T; try discriminate. - set (p17 := Tunneling.tunnel_program p16) in *. - destruct (Linearize.transf_program p17) as [p18|e] eqn:P18; simpl in T; try discriminate. - set (p19 := CleanupLabels.transf_program p18) in *. - destruct (partial_if debug Debugvar.transf_program p19) as [p20|e] eqn:P20; simpl in T; try discriminate. - destruct (Stacking.transf_program p20) as [p21|e] eqn:P21; simpl in T; try discriminate. - unfold match_prog; simpl. - exists p1; split. apply SimplExprproof.transf_program_match; auto. - exists p2; split. apply SimplLocalsproof.match_transf_program; auto. - exists p3; split. apply Cshmgenproof.transf_program_match; auto. - exists p4; split. apply Cminorgenproof.transf_program_match; auto. - exists p5; split. apply Selectionproof.transf_program_match; auto. - exists p6; split. apply RTLgenproof.transf_program_match; auto. - exists p7; split. apply total_if_match. apply Tailcallproof.transf_program_match. - exists p8; split. apply Inliningproof.transf_program_match; auto. - exists p8bis; split. apply total_if_match. apply Profilingproof.transf_program_match; auto. - exists p8ter; split. apply total_if_match. apply ProfilingExploitproof.transf_program_match; auto. - exists p9; split. apply total_if_match. apply FirstNopproof.transf_program_match. - exists p9bis; split. apply Renumberproof.transf_program_match. - exists p10; split. eapply partial_if_match; eauto. apply Duplicateproof.transf_program_match; auto. - exists p11; split. apply Renumberproof.transf_program_match. - exists p12; split. apply total_if_match. apply Constpropproof.transf_program_match. - exists p12bis; split. eapply partial_if_match; eauto. apply LICMproof.transf_program_match. - exists p12ter; split. apply total_if_match; eauto. apply Renumberproof.transf_program_match. - exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. - exists p13bis; split. apply total_if_match. apply CSE2proof.transf_program_match. - exists p13ter; split. eapply partial_if_match; eauto. apply CSE3proof.transf_program_match. - exists p13quater; split. eapply total_if_match; eauto. apply ForwardMovesproof.transf_program_match. - exists p14; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. - exists p14bis; split. eapply total_if_match; eauto. apply Allnontrapproof.transf_program_match. - exists p15; split. apply Unusedglobproof.transf_program_match; auto. - exists p16; split. apply Allocproof.transf_program_match; auto. - exists p17; split. apply Tunnelingproof.transf_program_match. - exists p18; split. apply Linearizeproof.transf_program_match; auto. - exists p19; split. apply CleanupLabelsproof.transf_program_match; auto. - exists p20; split. eapply partial_if_match; eauto. apply Debugvarproof.transf_program_match. - exists p21; split. apply Stackingproof.transf_program_match; auto. - exists tp; split. apply Asmgenproof.transf_program_match; auto. - reflexivity. -Qed. - -(** * Semantic preservation *) - -(** We now prove that the whole CompCert compiler (as characterized by the - [match_prog] relation) preserves semantics by constructing - the following simulations: -- Forward simulations from [Cstrategy] to [Asm] - (composition of the forward simulations for each pass). -- Backward simulations for the same languages - (derived from the forward simulation, using receptiveness of the source - language and determinacy of [Asm]). -- Backward simulation from [Csem] to [Asm] - (composition of two backward simulations). -*) - -Remark forward_simulation_identity: - forall sem, forward_simulation sem sem. -Proof. - intros. apply forward_simulation_step with (fun s1 s2 => s2 = s1); intros. -- auto. -- exists s1; auto. -- subst s2; auto. -- subst s2. exists s1'; auto. -Qed. - -Lemma match_if_simulation: - forall (A: Type) (sem: A -> semantics) (flag: unit -> bool) (transf: A -> A -> Prop) (prog tprog: A), - match_if flag transf prog tprog -> - (forall p tp, transf p tp -> forward_simulation (sem p) (sem tp)) -> - forward_simulation (sem prog) (sem tprog). -Proof. - intros. unfold match_if in *. destruct (flag tt). eauto. subst. apply forward_simulation_identity. -Qed. - -Theorem cstrategy_semantic_preservation: - forall p tp, - match_prog p tp -> - forward_simulation (Cstrategy.semantics p) (Asm.semantics tp) - /\ backward_simulation (atomic (Cstrategy.semantics p)) (Asm.semantics tp). -Proof. - intros p tp M. unfold match_prog, pass_match in M; simpl in M. -Ltac DestructM := - match goal with - [ H: exists p, _ /\ _ |- _ ] => - let p := fresh "p" in let M := fresh "M" in let MM := fresh "MM" in - destruct H as (p & M & MM); clear H - end. - repeat DestructM. subst tp. - assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p31)). - { - eapply compose_forward_simulations. - eapply SimplExprproof.transl_program_correct; eassumption. - eapply compose_forward_simulations. - eapply SimplLocalsproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply Cshmgenproof.transl_program_correct; eassumption. - eapply compose_forward_simulations. - eapply Cminorgenproof.transl_program_correct; eassumption. - eapply compose_forward_simulations. - eapply Selectionproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply RTLgenproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact Tailcallproof.transf_program_correct. - eapply compose_forward_simulations. - eapply Inliningproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact Profilingproof.transf_program_correct. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact ProfilingExploitproof.transf_program_correct. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact FirstNopproof.transf_program_correct. - eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact Duplicateproof.transf_program_correct. - eapply compose_forward_simulations. - eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. - eapply match_if_simulation. eassumption. exact Constpropproof.transf_program_correct. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact LICMproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact Renumberproof.transf_program_correct. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact CSEproof.transf_program_correct. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact CSE2proof.transf_program_correct. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact CSE3proof.transf_program_correct. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact ForwardMovesproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact Deadcodeproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact Allnontrapproof.transf_program_correct. - eapply compose_forward_simulations. - eapply Unusedglobproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply Allocproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply Tunnelingproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply Linearizeproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply CleanupLabelsproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact Debugvarproof.transf_program_correct. - eapply compose_forward_simulations. - eapply Stackingproof.transf_program_correct with (return_address_offset := Asmgenproof0.return_address_offset). - exact Asmgenproof.return_address_exists. - eassumption. - eapply Asmgenproof.transf_program_correct; eassumption. - } - split. auto. - apply forward_to_backward_simulation. - apply factor_forward_simulation. auto. eapply sd_traces. eapply Asm.semantics_determinate. - apply atomic_receptive. apply Cstrategy.semantics_strongly_receptive. - apply Asm.semantics_determinate. -Qed. - -Theorem c_semantic_preservation: - forall p tp, - match_prog p tp -> - backward_simulation (Csem.semantics p) (Asm.semantics tp). -Proof. - intros. - apply compose_backward_simulation with (atomic (Cstrategy.semantics p)). - eapply sd_traces; eapply Asm.semantics_determinate. - apply factor_backward_simulation. - apply Cstrategy.strategy_simulation. - apply Csem.semantics_single_events. - eapply ssr_well_behaved; eapply Cstrategy.semantics_strongly_receptive. - exact (proj2 (cstrategy_semantic_preservation _ _ H)). -Qed. - -(** * Correctness of the CompCert compiler *) - -(** Combining the results above, we obtain semantic preservation for two - usage scenarios of CompCert: compilation of a single monolithic program, - and separate compilation of multiple source files followed by linking. - - In the monolithic case, we have a whole C program [p] that is - compiled in one run of CompCert to a whole Asm program [tp]. - Then, [tp] preserves the semantics of [p], in the sense that there - exists a backward simulation of the dynamic semantics of [p] - by the dynamic semantics of [tp]. *) - -Theorem transf_c_program_correct: - forall p tp, - transf_c_program p = OK tp -> - backward_simulation (Csem.semantics p) (Asm.semantics tp). -Proof. - intros. apply c_semantic_preservation. apply transf_c_program_match; auto. -Qed. - -(** Here is the separate compilation case. Consider a nonempty list [c_units] - of C source files (compilation units), [C1 ,,, Cn]. Assume that every - C compilation unit [Ci] is successfully compiled by CompCert, obtaining - an Asm compilation unit [Ai]. Let [asm_unit] be the nonempty list - [A1 ... An]. Further assume that the C units [C1 ... Cn] can be linked - together to produce a whole C program [c_program]. Then, the generated - Asm units can be linked together, producing a whole Asm program - [asm_program]. Moreover, [asm_program] preserves the semantics of - [c_program], in the sense that there exists a backward simulation of - the dynamic semantics of [asm_program] by the dynamic semantics of [c_program]. -*) - -Theorem separate_transf_c_program_correct: - forall c_units asm_units c_program, - nlist_forall2 (fun cu tcu => transf_c_program cu = OK tcu) c_units asm_units -> - link_list c_units = Some c_program -> - exists asm_program, - link_list asm_units = Some asm_program - /\ backward_simulation (Csem.semantics c_program) (Asm.semantics asm_program). -Proof. - intros. - assert (nlist_forall2 match_prog c_units asm_units). - { eapply nlist_forall2_imply. eauto. simpl; intros. apply transf_c_program_match; auto. } - assert (exists asm_program, link_list asm_units = Some asm_program /\ match_prog c_program asm_program). - { eapply link_list_compose_passes; eauto. } - destruct H2 as (asm_program & P & Q). - exists asm_program; split; auto. apply c_semantic_preservation; auto. -Qed. diff --git a/driver/Compiler.vexpand b/driver/Compiler.vexpand new file mode 100644 index 00000000..4c7c963a --- /dev/null +++ b/driver/Compiler.vexpand @@ -0,0 +1,533 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** The whole compiler and its proof of semantic preservation *) + +(** Libraries. *) +Require Import String. +Require Import Coqlib Errors. +Require Import AST Linking Smallstep. +(** Languages (syntax and semantics). *) +Require Ctypes Csyntax Csem Cstrategy Cexec. +Require Clight. +Require Csharpminor. +Require Cminor. +Require CminorSel. +Require RTL. +Require LTL. +Require Linear. +Require Mach. +Require Asm. +(** Translation passes. *) +Require Initializers. +Require SimplExpr. +Require SimplLocals. +Require Cshmgen. +Require Cminorgen. +Require Selection. +Require RTLgen. +Require Tailcall. +Require Inlining. +Require Profiling. +Require ProfilingExploit. +Require FirstNop. +Require Renumber. +Require Duplicate. +Require Constprop. +Require LICM. +Require CSE. +Require ForwardMoves. +Require CSE2. +Require CSE3. +Require Deadcode. +Require Unusedglob. +Require Allnontrap. +Require Allocation. +Require Tunneling. +Require Linearize. +Require CleanupLabels. +Require Debugvar. +Require Stacking. +Require Asmgen. +(** Proofs of semantic preservation. *) +Require SimplExprproof. +Require SimplLocalsproof. +Require Cshmgenproof. +Require Cminorgenproof. +Require Selectionproof. +Require RTLgenproof. +Require Tailcallproof. +Require Inliningproof. +Require Profilingproof. +Require ProfilingExploitproof. +Require FirstNopproof. +Require Renumberproof. +Require Duplicateproof. +Require Constpropproof. +Require LICMproof. +Require CSEproof. +Require ForwardMovesproof. +Require CSE2proof. +Require CSE3proof. +Require Deadcodeproof. +Require Unusedglobproof. +Require Allnontrapproof. +Require Allocproof. +Require Tunnelingproof. +Require Linearizeproof. +Require CleanupLabelsproof. +Require Debugvarproof. +Require Stackingproof. +Require Import Asmgenproof. +(** Command-line flags. *) +Require Import Compopts. + +(** Pretty-printers (defined in Caml). *) +Parameter print_Clight: Clight.program -> unit. +Parameter print_Cminor: Cminor.program -> unit. +Parameter print_RTL: Z -> RTL.program -> unit. +Parameter print_LTL: LTL.program -> unit. +Parameter print_Mach: Mach.program -> unit. + +Local Open Scope string_scope. + +(** * Composing the translation passes *) + +(** We first define useful monadic composition operators, + along with funny (but convenient) notations. *) + +Definition apply_total (A B: Type) (x: res A) (f: A -> B) : res B := + match x with Error msg => Error msg | OK x1 => OK (f x1) end. + +Definition apply_partial (A B: Type) + (x: res A) (f: A -> res B) : res B := + match x with Error msg => Error msg | OK x1 => f x1 end. + +Notation "a @@@ b" := + (apply_partial _ _ a b) (at level 50, left associativity). +Notation "a @@ b" := + (apply_total _ _ a b) (at level 50, left associativity). + +Definition print {A: Type} (printer: A -> unit) (prog: A) : A := + let unused := printer prog in prog. + +Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f. + +Definition total_if {A: Type} + (flag: unit -> bool) (f: A -> A) (prog: A) : A := + if flag tt then f prog else prog. + +Definition partial_if {A: Type} + (flag: unit -> bool) (f: A -> res A) (prog: A) : res A := + if flag tt then f prog else OK prog. + +(** We define three translation functions for whole programs: one + starting with a C program, one with a Cminor program, one with an + RTL program. The three translations produce Asm programs ready for + pretty-printing and assembling. *) + +Definition transf_rtl_program (f: RTL.program) : res Asm.program := + OK f + @@ print (print_RTL 0) +EXPAND_TRANSF_PROGRAM + @@@ time "Register allocation" Allocation.transf_program + @@ print print_LTL + @@ time "Branch tunneling" Tunneling.tunnel_program + @@@ time "CFG linearization" Linearize.transf_program + @@ time "Label cleanup" CleanupLabels.transf_program + @@@ partial_if Compopts.debug (time "Debugging info for local variables" Debugvar.transf_program) + @@@ time "Mach generation" Stacking.transf_program + @@ print print_Mach + @@@ time "Total Mach->Asm generation" Asmgen.transf_program. + +Definition transf_cminor_program (p: Cminor.program) : res Asm.program := + OK p + @@ print print_Cminor + @@@ time "Instruction selection" Selection.sel_program + @@@ time "RTL generation" RTLgen.transl_program + @@@ transf_rtl_program. + +Definition transf_clight_program (p: Clight.program) : res Asm.program := + OK p + @@ print print_Clight + @@@ time "Simplification of locals" SimplLocals.transf_program + @@@ time "C#minor generation" Cshmgen.transl_program + @@@ time "Cminor generation" Cminorgen.transl_program + @@@ transf_cminor_program. + +Definition transf_c_program (p: Csyntax.program) : res Asm.program := + OK p + @@@ time "Clight generation" SimplExpr.transl_program + @@@ transf_clight_program. + +(** Force [Initializers] and [Cexec] to be extracted as well. *) + +Definition transl_init := Initializers.transl_init. +Definition cexec_do_step := Cexec.do_step. + +(** The following lemmas help reason over compositions of passes. *) + +Lemma print_identity: + forall (A: Type) (printer: A -> unit) (prog: A), + print printer prog = prog. +Proof. + intros; unfold print. destruct (printer prog); auto. +Qed. + +Lemma compose_print_identity: + forall (A: Type) (x: res A) (f: A -> unit), + x @@ print f = x. +Proof. + intros. destruct x; simpl. rewrite print_identity. auto. auto. +Qed. + +(** * Relational specification of compilation *) + +Definition match_if {A: Type} (flag: unit -> bool) (R: A -> A -> Prop): A -> A -> Prop := + if flag tt then R else eq. + +Lemma total_if_match: + forall (A: Type) (flag: unit -> bool) (f: A -> A) (rel: A -> A -> Prop) (prog: A), + (forall p, rel p (f p)) -> + match_if flag rel prog (total_if flag f prog). +Proof. + intros. unfold match_if, total_if. destruct (flag tt); auto. +Qed. + +Lemma partial_if_match: + forall (A: Type) (flag: unit -> bool) (f: A -> res A) (rel: A -> A -> Prop) (prog tprog: A), + (forall p tp, f p = OK tp -> rel p tp) -> + partial_if flag f prog = OK tprog -> + match_if flag rel prog tprog. +Proof. + intros. unfold match_if, partial_if in *. destruct (flag tt). auto. congruence. +Qed. + +Instance TransfIfLink {A: Type} {LA: Linker A} + (flag: unit -> bool) (transf: A -> A -> Prop) (TL: TransfLink transf) + : TransfLink (match_if flag transf). +Proof. + unfold match_if. destruct (flag tt). +- auto. +- red; intros. subst tp1 tp2. exists p; auto. +Qed. + +(** This is the list of compilation passes of CompCert in relational style. + Each pass is characterized by a [match_prog] relation between its + input code and its output code. The [mkpass] and [:::] combinators, + defined in module [Linking], ensure that the passes are composable + (the output language of a pass is the input language of the next pass) + and that they commute with linking (property [TransfLink], inferred + by the type class mechanism of Coq). *) + +Local Open Scope linking_scope. + +Definition CompCert's_passes := + mkpass SimplExprproof.match_prog + ::: mkpass SimplLocalsproof.match_prog + ::: mkpass Cshmgenproof.match_prog + ::: mkpass Cminorgenproof.match_prog + ::: mkpass Selectionproof.match_prog + ::: mkpass RTLgenproof.match_prog + ::: mkpass (match_if Compopts.optim_tailcalls Tailcallproof.match_prog) + ::: mkpass Inliningproof.match_prog + ::: mkpass (match_if Compopts.profile_arcs Profilingproof.match_prog) + ::: mkpass (match_if Compopts.branch_probabilities ProfilingExploitproof.match_prog) + ::: mkpass (match_if Compopts.optim_move_loop_invariants FirstNopproof.match_prog) + ::: mkpass Renumberproof.match_prog + ::: mkpass (match_if Compopts.optim_duplicate Duplicateproof.match_prog) + ::: mkpass Renumberproof.match_prog + ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog) + ::: mkpass (match_if Compopts.optim_move_loop_invariants LICMproof.match_prog) + ::: mkpass (match_if Compopts.optim_move_loop_invariants Renumberproof.match_prog) + ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) + ::: mkpass (match_if Compopts.optim_CSE2 CSE2proof.match_prog) + ::: mkpass (match_if Compopts.optim_CSE3 CSE3proof.match_prog) + ::: mkpass (match_if Compopts.optim_forward_moves ForwardMovesproof.match_prog) + ::: mkpass (match_if Compopts.optim_redundancy Deadcodeproof.match_prog) + ::: mkpass (match_if Compopts.all_loads_nontrap Allnontrapproof.match_prog) + ::: mkpass Unusedglobproof.match_prog + ::: mkpass Allocproof.match_prog + ::: mkpass Tunnelingproof.match_prog + ::: mkpass Linearizeproof.match_prog + ::: mkpass CleanupLabelsproof.match_prog + ::: mkpass (match_if Compopts.debug Debugvarproof.match_prog) + ::: mkpass Stackingproof.match_prog + ::: mkpass Asmgenproof.match_prog + ::: pass_nil _. + +(** Composing the [match_prog] relations above, we obtain the relation + between CompCert C sources and Asm code that characterize CompCert's + compilation. *) + +Definition match_prog: Csyntax.program -> Asm.program -> Prop := + pass_match (compose_passes CompCert's_passes). + +(** The [transf_c_program] function, when successful, produces + assembly code that is in the [match_prog] relation with the source C program. *) + +Theorem transf_c_program_match: + forall p tp, + transf_c_program p = OK tp -> + match_prog p tp. +Proof. + intros p tp T. + unfold transf_c_program, time in T. simpl in T. + destruct (SimplExpr.transl_program p) as [p1|e] eqn:P1; simpl in T; try discriminate. + unfold transf_clight_program, time in T. rewrite ! compose_print_identity in T. simpl in T. + destruct (SimplLocals.transf_program p1) as [p2|e] eqn:P2; simpl in T; try discriminate. + destruct (Cshmgen.transl_program p2) as [p3|e] eqn:P3; simpl in T; try discriminate. + destruct (Cminorgen.transl_program p3) as [p4|e] eqn:P4; simpl in T; try discriminate. + unfold transf_cminor_program, time in T. rewrite ! compose_print_identity in T. simpl in T. + destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate. + destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate. + unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T. simpl in T. + set (p7 := total_if optim_tailcalls Tailcall.transf_program p6) in *. + destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate. + set (p8bis := total_if profile_arcs Profiling.transf_program p8) in *. + set (p8ter := total_if branch_probabilities ProfilingExploit.transf_program p8bis) in *. + set (p9 := total_if Compopts.optim_move_loop_invariants FirstNop.transf_program p8ter) in *. + set (p9bis := Renumber.transf_program p9) in *. + destruct (partial_if optim_duplicate Duplicate.transf_program p9bis) as [p10|e] eqn:P10; simpl in T; try discriminate. + set (p11 := Renumber.transf_program p10) in *. + set (p12 := total_if optim_constprop Constprop.transf_program p11) in *. + destruct (partial_if optim_move_loop_invariants LICM.transf_program p12) as [p12bis|e] eqn:P12bis; simpl in T; try discriminate. + set (p12ter :=(total_if optim_move_loop_invariants Renumber.transf_program p12bis)) in *. + destruct (partial_if optim_CSE CSE.transf_program p12ter) as [p13|e] eqn:P13; simpl in T; try discriminate. + set (p13bis := total_if optim_CSE2 CSE2.transf_program p13) in *. + destruct (partial_if optim_CSE3 CSE3.transf_program p13bis) as [p13ter|e] eqn:P13ter; simpl in T; try discriminate. + set (p13quater := total_if optim_forward_moves ForwardMoves.transf_program p13ter) in *. + destruct (partial_if optim_redundancy Deadcode.transf_program p13quater) as [p14|e] eqn:P14; simpl in T; try discriminate. + set (p14bis := total_if all_loads_nontrap Allnontrap.transf_program p14) in *. + destruct (Unusedglob.transform_program p14bis) as [p15|e] eqn:P15; simpl in T; try discriminate. + destruct (Allocation.transf_program p15) as [p16|e] eqn:P16; simpl in T; try discriminate. + set (p17 := Tunneling.tunnel_program p16) in *. + destruct (Linearize.transf_program p17) as [p18|e] eqn:P18; simpl in T; try discriminate. + set (p19 := CleanupLabels.transf_program p18) in *. + destruct (partial_if debug Debugvar.transf_program p19) as [p20|e] eqn:P20; simpl in T; try discriminate. + destruct (Stacking.transf_program p20) as [p21|e] eqn:P21; simpl in T; try discriminate. + unfold match_prog; simpl. + exists p1; split. apply SimplExprproof.transf_program_match; auto. + exists p2; split. apply SimplLocalsproof.match_transf_program; auto. + exists p3; split. apply Cshmgenproof.transf_program_match; auto. + exists p4; split. apply Cminorgenproof.transf_program_match; auto. + exists p5; split. apply Selectionproof.transf_program_match; auto. + exists p6; split. apply RTLgenproof.transf_program_match; auto. + exists p7; split. apply total_if_match. apply Tailcallproof.transf_program_match. + exists p8; split. apply Inliningproof.transf_program_match; auto. + exists p8bis; split. apply total_if_match. apply Profilingproof.transf_program_match; auto. + exists p8ter; split. apply total_if_match. apply ProfilingExploitproof.transf_program_match; auto. + exists p9; split. apply total_if_match. apply FirstNopproof.transf_program_match. + exists p9bis; split. apply Renumberproof.transf_program_match. + exists p10; split. eapply partial_if_match; eauto. apply Duplicateproof.transf_program_match; auto. + exists p11; split. apply Renumberproof.transf_program_match. + exists p12; split. apply total_if_match. apply Constpropproof.transf_program_match. + exists p12bis; split. eapply partial_if_match; eauto. apply LICMproof.transf_program_match. + exists p12ter; split. apply total_if_match; eauto. apply Renumberproof.transf_program_match. + exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. + exists p13bis; split. apply total_if_match. apply CSE2proof.transf_program_match. + exists p13ter; split. eapply partial_if_match; eauto. apply CSE3proof.transf_program_match. + exists p13quater; split. eapply total_if_match; eauto. apply ForwardMovesproof.transf_program_match. + exists p14; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. + exists p14bis; split. eapply total_if_match; eauto. apply Allnontrapproof.transf_program_match. + exists p15; split. apply Unusedglobproof.transf_program_match; auto. + exists p16; split. apply Allocproof.transf_program_match; auto. + exists p17; split. apply Tunnelingproof.transf_program_match. + exists p18; split. apply Linearizeproof.transf_program_match; auto. + exists p19; split. apply CleanupLabelsproof.transf_program_match; auto. + exists p20; split. eapply partial_if_match; eauto. apply Debugvarproof.transf_program_match. + exists p21; split. apply Stackingproof.transf_program_match; auto. + exists tp; split. apply Asmgenproof.transf_program_match; auto. + reflexivity. +Qed. + +(** * Semantic preservation *) + +(** We now prove that the whole CompCert compiler (as characterized by the + [match_prog] relation) preserves semantics by constructing + the following simulations: +- Forward simulations from [Cstrategy] to [Asm] + (composition of the forward simulations for each pass). +- Backward simulations for the same languages + (derived from the forward simulation, using receptiveness of the source + language and determinacy of [Asm]). +- Backward simulation from [Csem] to [Asm] + (composition of two backward simulations). +*) + +Remark forward_simulation_identity: + forall sem, forward_simulation sem sem. +Proof. + intros. apply forward_simulation_step with (fun s1 s2 => s2 = s1); intros. +- auto. +- exists s1; auto. +- subst s2; auto. +- subst s2. exists s1'; auto. +Qed. + +Lemma match_if_simulation: + forall (A: Type) (sem: A -> semantics) (flag: unit -> bool) (transf: A -> A -> Prop) (prog tprog: A), + match_if flag transf prog tprog -> + (forall p tp, transf p tp -> forward_simulation (sem p) (sem tp)) -> + forward_simulation (sem prog) (sem tprog). +Proof. + intros. unfold match_if in *. destruct (flag tt). eauto. subst. apply forward_simulation_identity. +Qed. + +Theorem cstrategy_semantic_preservation: + forall p tp, + match_prog p tp -> + forward_simulation (Cstrategy.semantics p) (Asm.semantics tp) + /\ backward_simulation (atomic (Cstrategy.semantics p)) (Asm.semantics tp). +Proof. + intros p tp M. unfold match_prog, pass_match in M; simpl in M. +Ltac DestructM := + match goal with + [ H: exists p, _ /\ _ |- _ ] => + let p := fresh "p" in let M := fresh "M" in let MM := fresh "MM" in + destruct H as (p & M & MM); clear H + end. + repeat DestructM. subst tp. + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p31)). + { + eapply compose_forward_simulations. + eapply SimplExprproof.transl_program_correct; eassumption. + eapply compose_forward_simulations. + eapply SimplLocalsproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply Cshmgenproof.transl_program_correct; eassumption. + eapply compose_forward_simulations. + eapply Cminorgenproof.transl_program_correct; eassumption. + eapply compose_forward_simulations. + eapply Selectionproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply RTLgenproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact Tailcallproof.transf_program_correct. + eapply compose_forward_simulations. + eapply Inliningproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact Profilingproof.transf_program_correct. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact ProfilingExploitproof.transf_program_correct. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact FirstNopproof.transf_program_correct. + eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact Duplicateproof.transf_program_correct. + eapply compose_forward_simulations. + eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. + eapply match_if_simulation. eassumption. exact Constpropproof.transf_program_correct. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact LICMproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact Renumberproof.transf_program_correct. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact CSEproof.transf_program_correct. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact CSE2proof.transf_program_correct. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact CSE3proof.transf_program_correct. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact ForwardMovesproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact Deadcodeproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact Allnontrapproof.transf_program_correct. + eapply compose_forward_simulations. + eapply Unusedglobproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply Allocproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply Tunnelingproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply Linearizeproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply CleanupLabelsproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact Debugvarproof.transf_program_correct. + eapply compose_forward_simulations. + eapply Stackingproof.transf_program_correct with (return_address_offset := Asmgenproof0.return_address_offset). + exact Asmgenproof.return_address_exists. + eassumption. + eapply Asmgenproof.transf_program_correct; eassumption. + } + split. auto. + apply forward_to_backward_simulation. + apply factor_forward_simulation. auto. eapply sd_traces. eapply Asm.semantics_determinate. + apply atomic_receptive. apply Cstrategy.semantics_strongly_receptive. + apply Asm.semantics_determinate. +Qed. + +Theorem c_semantic_preservation: + forall p tp, + match_prog p tp -> + backward_simulation (Csem.semantics p) (Asm.semantics tp). +Proof. + intros. + apply compose_backward_simulation with (atomic (Cstrategy.semantics p)). + eapply sd_traces; eapply Asm.semantics_determinate. + apply factor_backward_simulation. + apply Cstrategy.strategy_simulation. + apply Csem.semantics_single_events. + eapply ssr_well_behaved; eapply Cstrategy.semantics_strongly_receptive. + exact (proj2 (cstrategy_semantic_preservation _ _ H)). +Qed. + +(** * Correctness of the CompCert compiler *) + +(** Combining the results above, we obtain semantic preservation for two + usage scenarios of CompCert: compilation of a single monolithic program, + and separate compilation of multiple source files followed by linking. + + In the monolithic case, we have a whole C program [p] that is + compiled in one run of CompCert to a whole Asm program [tp]. + Then, [tp] preserves the semantics of [p], in the sense that there + exists a backward simulation of the dynamic semantics of [p] + by the dynamic semantics of [tp]. *) + +Theorem transf_c_program_correct: + forall p tp, + transf_c_program p = OK tp -> + backward_simulation (Csem.semantics p) (Asm.semantics tp). +Proof. + intros. apply c_semantic_preservation. apply transf_c_program_match; auto. +Qed. + +(** Here is the separate compilation case. Consider a nonempty list [c_units] + of C source files (compilation units), [C1 ,,, Cn]. Assume that every + C compilation unit [Ci] is successfully compiled by CompCert, obtaining + an Asm compilation unit [Ai]. Let [asm_unit] be the nonempty list + [A1 ... An]. Further assume that the C units [C1 ... Cn] can be linked + together to produce a whole C program [c_program]. Then, the generated + Asm units can be linked together, producing a whole Asm program + [asm_program]. Moreover, [asm_program] preserves the semantics of + [c_program], in the sense that there exists a backward simulation of + the dynamic semantics of [asm_program] by the dynamic semantics of [c_program]. +*) + +Theorem separate_transf_c_program_correct: + forall c_units asm_units c_program, + nlist_forall2 (fun cu tcu => transf_c_program cu = OK tcu) c_units asm_units -> + link_list c_units = Some c_program -> + exists asm_program, + link_list asm_units = Some asm_program + /\ backward_simulation (Csem.semantics c_program) (Asm.semantics asm_program). +Proof. + intros. + assert (nlist_forall2 match_prog c_units asm_units). + { eapply nlist_forall2_imply. eauto. simpl; intros. apply transf_c_program_match; auto. } + assert (exists asm_program, link_list asm_units = Some asm_program /\ match_prog c_program asm_program). + { eapply link_list_compose_passes; eauto. } + destruct H2 as (asm_program & P & Q). + exists asm_program; split; auto. apply c_semantic_preservation; auto. +Qed. -- cgit From 1bd4d678fb719a6a52ade232eb2b36a6e621677a Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 21 Apr 2020 22:24:31 +0200 Subject: Require autogen --- driver/Compiler.vexpand | 38 ++++---------------------------------- 1 file changed, 4 insertions(+), 34 deletions(-) (limited to 'driver') diff --git a/driver/Compiler.vexpand b/driver/Compiler.vexpand index 4c7c963a..d0ba33d3 100644 --- a/driver/Compiler.vexpand +++ b/driver/Compiler.vexpand @@ -35,22 +35,7 @@ Require Cshmgen. Require Cminorgen. Require Selection. Require RTLgen. -Require Tailcall. -Require Inlining. -Require Profiling. -Require ProfilingExploit. -Require FirstNop. -Require Renumber. -Require Duplicate. -Require Constprop. -Require LICM. -Require CSE. -Require ForwardMoves. -Require CSE2. -Require CSE3. -Require Deadcode. -Require Unusedglob. -Require Allnontrap. +EXPAND_RTL_REQUIRE Require Allocation. Require Tunneling. Require Linearize. @@ -65,22 +50,7 @@ Require Cshmgenproof. Require Cminorgenproof. Require Selectionproof. Require RTLgenproof. -Require Tailcallproof. -Require Inliningproof. -Require Profilingproof. -Require ProfilingExploitproof. -Require FirstNopproof. -Require Renumberproof. -Require Duplicateproof. -Require Constpropproof. -Require LICMproof. -Require CSEproof. -Require ForwardMovesproof. -Require CSE2proof. -Require CSE3proof. -Require Deadcodeproof. -Require Unusedglobproof. -Require Allnontrapproof. +EXPAND_RTL_REQUIRE_PROOF Require Allocproof. Require Tunnelingproof. Require Linearizeproof. @@ -138,7 +108,7 @@ Definition partial_if {A: Type} Definition transf_rtl_program (f: RTL.program) : res Asm.program := OK f @@ print (print_RTL 0) -EXPAND_TRANSF_PROGRAM +EXPAND_RTL_TRANSF_PROGRAM @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program @@ -308,7 +278,7 @@ Proof. set (p13quater := total_if optim_forward_moves ForwardMoves.transf_program p13ter) in *. destruct (partial_if optim_redundancy Deadcode.transf_program p13quater) as [p14|e] eqn:P14; simpl in T; try discriminate. set (p14bis := total_if all_loads_nontrap Allnontrap.transf_program p14) in *. - destruct (Unusedglob.transform_program p14bis) as [p15|e] eqn:P15; simpl in T; try discriminate. + destruct (Unusedglob.transf_program p14bis) as [p15|e] eqn:P15; simpl in T; try discriminate. destruct (Allocation.transf_program p15) as [p16|e] eqn:P16; simpl in T; try discriminate. set (p17 := Tunneling.tunnel_program p16) in *. destruct (Linearize.transf_program p17) as [p18|e] eqn:P18; simpl in T; try discriminate. -- cgit From 25547c7d1f6a0fb75ff1d8e7287d9305e0dbf293 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 21 Apr 2020 22:42:32 +0200 Subject: generate mkpass --- driver/Compiler.vexpand | 19 +------------------ 1 file changed, 1 insertion(+), 18 deletions(-) (limited to 'driver') diff --git a/driver/Compiler.vexpand b/driver/Compiler.vexpand index d0ba33d3..c044d9ef 100644 --- a/driver/Compiler.vexpand +++ b/driver/Compiler.vexpand @@ -208,24 +208,7 @@ Definition CompCert's_passes := ::: mkpass Cminorgenproof.match_prog ::: mkpass Selectionproof.match_prog ::: mkpass RTLgenproof.match_prog - ::: mkpass (match_if Compopts.optim_tailcalls Tailcallproof.match_prog) - ::: mkpass Inliningproof.match_prog - ::: mkpass (match_if Compopts.profile_arcs Profilingproof.match_prog) - ::: mkpass (match_if Compopts.branch_probabilities ProfilingExploitproof.match_prog) - ::: mkpass (match_if Compopts.optim_move_loop_invariants FirstNopproof.match_prog) - ::: mkpass Renumberproof.match_prog - ::: mkpass (match_if Compopts.optim_duplicate Duplicateproof.match_prog) - ::: mkpass Renumberproof.match_prog - ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog) - ::: mkpass (match_if Compopts.optim_move_loop_invariants LICMproof.match_prog) - ::: mkpass (match_if Compopts.optim_move_loop_invariants Renumberproof.match_prog) - ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) - ::: mkpass (match_if Compopts.optim_CSE2 CSE2proof.match_prog) - ::: mkpass (match_if Compopts.optim_CSE3 CSE3proof.match_prog) - ::: mkpass (match_if Compopts.optim_forward_moves ForwardMovesproof.match_prog) - ::: mkpass (match_if Compopts.optim_redundancy Deadcodeproof.match_prog) - ::: mkpass (match_if Compopts.all_loads_nontrap Allnontrapproof.match_prog) - ::: mkpass Unusedglobproof.match_prog +EXPAND_RTL_MKPASS ::: mkpass Allocproof.match_prog ::: mkpass Tunnelingproof.match_prog ::: mkpass Linearizeproof.match_prog -- cgit From f5da5188171962d13b9f3eac04845dd19d0aa931 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 22 Apr 2020 08:08:21 +0200 Subject: automated writing Compiler.v --- driver/Compiler.vexpand | 119 ++++-------------------------------------------- 1 file changed, 8 insertions(+), 111 deletions(-) (limited to 'driver') diff --git a/driver/Compiler.vexpand b/driver/Compiler.vexpand index c044d9ef..17b504b7 100644 --- a/driver/Compiler.vexpand +++ b/driver/Compiler.vexpand @@ -36,12 +36,6 @@ Require Cminorgen. Require Selection. Require RTLgen. EXPAND_RTL_REQUIRE -Require Allocation. -Require Tunneling. -Require Linearize. -Require CleanupLabels. -Require Debugvar. -Require Stacking. Require Asmgen. (** Proofs of semantic preservation. *) Require SimplExprproof. @@ -51,12 +45,6 @@ Require Cminorgenproof. Require Selectionproof. Require RTLgenproof. EXPAND_RTL_REQUIRE_PROOF -Require Allocproof. -Require Tunnelingproof. -Require Linearizeproof. -Require CleanupLabelsproof. -Require Debugvarproof. -Require Stackingproof. Require Import Asmgenproof. (** Command-line flags. *) Require Import Compopts. @@ -109,16 +97,8 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := OK f @@ print (print_RTL 0) EXPAND_RTL_TRANSF_PROGRAM - @@@ time "Register allocation" Allocation.transf_program - @@ print print_LTL - @@ time "Branch tunneling" Tunneling.tunnel_program - @@@ time "CFG linearization" Linearize.transf_program - @@ time "Label cleanup" CleanupLabels.transf_program - @@@ partial_if Compopts.debug (time "Debugging info for local variables" Debugvar.transf_program) - @@@ time "Mach generation" Stacking.transf_program - @@ print print_Mach @@@ time "Total Mach->Asm generation" Asmgen.transf_program. - + Definition transf_cminor_program (p: Cminor.program) : res Asm.program := OK p @@ print print_Cminor @@ -209,12 +189,6 @@ Definition CompCert's_passes := ::: mkpass Selectionproof.match_prog ::: mkpass RTLgenproof.match_prog EXPAND_RTL_MKPASS - ::: mkpass Allocproof.match_prog - ::: mkpass Tunnelingproof.match_prog - ::: mkpass Linearizeproof.match_prog - ::: mkpass CleanupLabelsproof.match_prog - ::: mkpass (match_if Compopts.debug Debugvarproof.match_prog) - ::: mkpass Stackingproof.match_prog ::: mkpass Asmgenproof.match_prog ::: pass_nil _. @@ -244,30 +218,7 @@ Proof. destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate. destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate. unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T. simpl in T. - set (p7 := total_if optim_tailcalls Tailcall.transf_program p6) in *. - destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate. - set (p8bis := total_if profile_arcs Profiling.transf_program p8) in *. - set (p8ter := total_if branch_probabilities ProfilingExploit.transf_program p8bis) in *. - set (p9 := total_if Compopts.optim_move_loop_invariants FirstNop.transf_program p8ter) in *. - set (p9bis := Renumber.transf_program p9) in *. - destruct (partial_if optim_duplicate Duplicate.transf_program p9bis) as [p10|e] eqn:P10; simpl in T; try discriminate. - set (p11 := Renumber.transf_program p10) in *. - set (p12 := total_if optim_constprop Constprop.transf_program p11) in *. - destruct (partial_if optim_move_loop_invariants LICM.transf_program p12) as [p12bis|e] eqn:P12bis; simpl in T; try discriminate. - set (p12ter :=(total_if optim_move_loop_invariants Renumber.transf_program p12bis)) in *. - destruct (partial_if optim_CSE CSE.transf_program p12ter) as [p13|e] eqn:P13; simpl in T; try discriminate. - set (p13bis := total_if optim_CSE2 CSE2.transf_program p13) in *. - destruct (partial_if optim_CSE3 CSE3.transf_program p13bis) as [p13ter|e] eqn:P13ter; simpl in T; try discriminate. - set (p13quater := total_if optim_forward_moves ForwardMoves.transf_program p13ter) in *. - destruct (partial_if optim_redundancy Deadcode.transf_program p13quater) as [p14|e] eqn:P14; simpl in T; try discriminate. - set (p14bis := total_if all_loads_nontrap Allnontrap.transf_program p14) in *. - destruct (Unusedglob.transf_program p14bis) as [p15|e] eqn:P15; simpl in T; try discriminate. - destruct (Allocation.transf_program p15) as [p16|e] eqn:P16; simpl in T; try discriminate. - set (p17 := Tunneling.tunnel_program p16) in *. - destruct (Linearize.transf_program p17) as [p18|e] eqn:P18; simpl in T; try discriminate. - set (p19 := CleanupLabels.transf_program p18) in *. - destruct (partial_if debug Debugvar.transf_program p19) as [p20|e] eqn:P20; simpl in T; try discriminate. - destruct (Stacking.transf_program p20) as [p21|e] eqn:P21; simpl in T; try discriminate. +EXPAND_RTL_PROOF unfold match_prog; simpl. exists p1; split. apply SimplExprproof.transf_program_match; auto. exists p2; split. apply SimplLocalsproof.match_transf_program; auto. @@ -275,30 +226,7 @@ Proof. exists p4; split. apply Cminorgenproof.transf_program_match; auto. exists p5; split. apply Selectionproof.transf_program_match; auto. exists p6; split. apply RTLgenproof.transf_program_match; auto. - exists p7; split. apply total_if_match. apply Tailcallproof.transf_program_match. - exists p8; split. apply Inliningproof.transf_program_match; auto. - exists p8bis; split. apply total_if_match. apply Profilingproof.transf_program_match; auto. - exists p8ter; split. apply total_if_match. apply ProfilingExploitproof.transf_program_match; auto. - exists p9; split. apply total_if_match. apply FirstNopproof.transf_program_match. - exists p9bis; split. apply Renumberproof.transf_program_match. - exists p10; split. eapply partial_if_match; eauto. apply Duplicateproof.transf_program_match; auto. - exists p11; split. apply Renumberproof.transf_program_match. - exists p12; split. apply total_if_match. apply Constpropproof.transf_program_match. - exists p12bis; split. eapply partial_if_match; eauto. apply LICMproof.transf_program_match. - exists p12ter; split. apply total_if_match; eauto. apply Renumberproof.transf_program_match. - exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. - exists p13bis; split. apply total_if_match. apply CSE2proof.transf_program_match. - exists p13ter; split. eapply partial_if_match; eauto. apply CSE3proof.transf_program_match. - exists p13quater; split. eapply total_if_match; eauto. apply ForwardMovesproof.transf_program_match. - exists p14; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. - exists p14bis; split. eapply total_if_match; eauto. apply Allnontrapproof.transf_program_match. - exists p15; split. apply Unusedglobproof.transf_program_match; auto. - exists p16; split. apply Allocproof.transf_program_match; auto. - exists p17; split. apply Tunnelingproof.transf_program_match. - exists p18; split. apply Linearizeproof.transf_program_match; auto. - exists p19; split. apply CleanupLabelsproof.transf_program_match; auto. - exists p20; split. eapply partial_if_match; eauto. apply Debugvarproof.transf_program_match. - exists p21; split. apply Stackingproof.transf_program_match; auto. +EXPAND_RTL_PROOF2 exists tp; split. apply Asmgenproof.transf_program_match; auto. reflexivity. Qed. @@ -350,7 +278,9 @@ Ltac DestructM := destruct H as (p & M & MM); clear H end. repeat DestructM. subst tp. - assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p31)). + assert (F: forward_simulation (Cstrategy.semantics p) +EXPAND_ASM_SEMANTICS + ). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -364,42 +294,9 @@ Ltac DestructM := eapply Selectionproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply RTLgenproof.transf_program_correct; eassumption. +EXPAND_RTL_FORWARD_SIMULATIONS eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact Tailcallproof.transf_program_correct. - eapply compose_forward_simulations. - eapply Inliningproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact Profilingproof.transf_program_correct. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact ProfilingExploitproof.transf_program_correct. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact FirstNopproof.transf_program_correct. - eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact Duplicateproof.transf_program_correct. - eapply compose_forward_simulations. - eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. - eapply match_if_simulation. eassumption. exact Constpropproof.transf_program_correct. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact LICMproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact Renumberproof.transf_program_correct. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact CSEproof.transf_program_correct. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact CSE2proof.transf_program_correct. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact CSE3proof.transf_program_correct. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact ForwardMovesproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact Deadcodeproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact Allnontrapproof.transf_program_correct. - eapply compose_forward_simulations. - eapply Unusedglobproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply Allocproof.transf_program_correct; eassumption. + eapply Allocationproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply Tunnelingproof.transf_program_correct; eassumption. eapply compose_forward_simulations. -- cgit From 05a5825ee55227327ba1b09a548e3b9ba876d0cf Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 22 Apr 2020 08:53:06 +0200 Subject: use cbn in T instead of simpl in T --- driver/Compiler.vexpand | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Compiler.vexpand b/driver/Compiler.vexpand index 17b504b7..1e671464 100644 --- a/driver/Compiler.vexpand +++ b/driver/Compiler.vexpand @@ -217,7 +217,8 @@ Proof. unfold transf_cminor_program, time in T. rewrite ! compose_print_identity in T. simpl in T. destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate. destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate. - unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T. simpl in T. + unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T. + cbn in T. EXPAND_RTL_PROOF unfold match_prog; simpl. exists p1; split. apply SimplExprproof.transf_program_match; auto. -- cgit From 9718c8244b561b6f81a7a5a7dd0fb3ff1d570344 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 22 Apr 2020 09:10:15 +0200 Subject: simpl -> cbn --- driver/Compiler.v | 39 ++++++++++++++++++++------------------- 1 file changed, 20 insertions(+), 19 deletions(-) (limited to 'driver') diff --git a/driver/Compiler.v b/driver/Compiler.v index 499feff2..002c55fe 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -288,34 +288,35 @@ Theorem transf_c_program_match: match_prog p tp. Proof. intros p tp T. - unfold transf_c_program, time in T. simpl in T. - destruct (SimplExpr.transl_program p) as [p1|e] eqn:P1; simpl in T; try discriminate. - unfold transf_clight_program, time in T. rewrite ! compose_print_identity in T. simpl in T. - destruct (SimplLocals.transf_program p1) as [p2|e] eqn:P2; simpl in T; try discriminate. - destruct (Cshmgen.transl_program p2) as [p3|e] eqn:P3; simpl in T; try discriminate. - destruct (Cminorgen.transl_program p3) as [p4|e] eqn:P4; simpl in T; try discriminate. - unfold transf_cminor_program, time in T. rewrite ! compose_print_identity in T. simpl in T. - destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate. - destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate. - unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T. simpl in T. + unfold transf_c_program, time in T. cbn in T. + destruct (SimplExpr.transl_program p) as [p1|e] eqn:P1; cbn in T; try discriminate. + unfold transf_clight_program, time in T. rewrite ! compose_print_identity in T. cbn in T. + destruct (SimplLocals.transf_program p1) as [p2|e] eqn:P2; cbn in T; try discriminate. + destruct (Cshmgen.transl_program p2) as [p3|e] eqn:P3; cbn in T; try discriminate. + destruct (Cminorgen.transl_program p3) as [p4|e] eqn:P4; cbn in T; try discriminate. + unfold transf_cminor_program, time in T. rewrite ! compose_print_identity in T. cbn in T. + destruct (Selection.sel_program p4) as [p5|e] eqn:P5; cbn in T; try discriminate. + destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; cbn in T; try discriminate. + unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T. + cbn in T. set (p7 := total_if optim_tailcalls Tailcall.transf_program p6) in *. - destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate. + destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; cbn in T; try discriminate. set (p9 := Renumber.transf_program p8) in *. - destruct (partial_if optim_duplicate Duplicate.transf_program p9) as [p10|e] eqn:P10; simpl in T; try discriminate. + destruct (partial_if optim_duplicate Duplicate.transf_program p9) as [p10|e] eqn:P10; cbn in T; try discriminate. set (p11 := total_if optim_constprop Constprop.transf_program p10) in *. set (p12 := total_if optim_constprop Renumber.transf_program p11) in *. - destruct (partial_if optim_CSE CSE.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate. + destruct (partial_if optim_CSE CSE.transf_program p12) as [p13|e] eqn:P13; cbn in T; try discriminate. set (p13bis := total_if optim_CSE2 CSE2.transf_program p13) in *. set (p13ter := total_if optim_forward_moves ForwardMoves.transf_program p13bis) in *. - destruct (partial_if optim_redundancy Deadcode.transf_program p13ter) as [p14|e] eqn:P14; simpl in T; try discriminate. + destruct (partial_if optim_redundancy Deadcode.transf_program p13ter) as [p14|e] eqn:P14; cbn in T; try discriminate. set (p14bis := total_if all_loads_nontrap Allnontrap.transf_program p14) in *. - destruct (Unusedglob.transform_program p14bis) as [p15|e] eqn:P15; simpl in T; try discriminate. - destruct (Allocation.transf_program p15) as [p16|e] eqn:P16; simpl in T; try discriminate. + destruct (Unusedglob.transform_program p14bis) as [p15|e] eqn:P15; cbn in T; try discriminate. + destruct (Allocation.transf_program p15) as [p16|e] eqn:P16; cbn in T; try discriminate. set (p17 := Tunneling.tunnel_program p16) in *. - destruct (Linearize.transf_program p17) as [p18|e] eqn:P18; simpl in T; try discriminate. + destruct (Linearize.transf_program p17) as [p18|e] eqn:P18; cbn in T; try discriminate. set (p19 := CleanupLabels.transf_program p18) in *. - destruct (partial_if debug Debugvar.transf_program p19) as [p20|e] eqn:P20; simpl in T; try discriminate. - destruct (Stacking.transf_program p20) as [p21|e] eqn:P21; simpl in T; try discriminate. + destruct (partial_if debug Debugvar.transf_program p19) as [p20|e] eqn:P20; cbn in T; try discriminate. + destruct (Stacking.transf_program p20) as [p21|e] eqn:P21; cbn in T; try discriminate. unfold match_prog; simpl. exists p1; split. apply SimplExprproof.transf_program_match; auto. exists p2; split. apply SimplLocalsproof.match_transf_program; auto. -- cgit From c991b6f67778634cf1c8df5fb429a74d068c8fb8 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 22 Apr 2020 11:27:15 +0200 Subject: cbn and copyright --- driver/Compiler.vexpand | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) (limited to 'driver') diff --git a/driver/Compiler.vexpand b/driver/Compiler.vexpand index 1e671464..0f59aab7 100644 --- a/driver/Compiler.vexpand +++ b/driver/Compiler.vexpand @@ -208,15 +208,15 @@ Theorem transf_c_program_match: match_prog p tp. Proof. intros p tp T. - unfold transf_c_program, time in T. simpl in T. - destruct (SimplExpr.transl_program p) as [p1|e] eqn:P1; simpl in T; try discriminate. - unfold transf_clight_program, time in T. rewrite ! compose_print_identity in T. simpl in T. - destruct (SimplLocals.transf_program p1) as [p2|e] eqn:P2; simpl in T; try discriminate. - destruct (Cshmgen.transl_program p2) as [p3|e] eqn:P3; simpl in T; try discriminate. - destruct (Cminorgen.transl_program p3) as [p4|e] eqn:P4; simpl in T; try discriminate. - unfold transf_cminor_program, time in T. rewrite ! compose_print_identity in T. simpl in T. - destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate. - destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate. + unfold transf_c_program, time in T. cbn in T. + destruct (SimplExpr.transl_program p) as [p1|e] eqn:P1; cbn in T; try discriminate. + unfold transf_clight_program, time in T. rewrite ! compose_print_identity in T. cbn in T. + destruct (SimplLocals.transf_program p1) as [p2|e] eqn:P2; cbn in T; try discriminate. + destruct (Cshmgen.transl_program p2) as [p3|e] eqn:P3; cbn in T; try discriminate. + destruct (Cminorgen.transl_program p3) as [p4|e] eqn:P4; cbn in T; try discriminate. + unfold transf_cminor_program, time in T. rewrite ! compose_print_identity in T. cbn in T. + destruct (Selection.sel_program p4) as [p5|e] eqn:P5; cbn in T; try discriminate. + destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; cbn in T; try discriminate. unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T. cbn in T. EXPAND_RTL_PROOF -- cgit From a4e86b9131f39648e6e54f2ae5c498be0c2e5f41 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 22 Apr 2020 11:43:45 +0200 Subject: use cbn not simpl --- driver/Compiler.v | 42 +++++++++++++++++++++--------------------- 1 file changed, 21 insertions(+), 21 deletions(-) (limited to 'driver') diff --git a/driver/Compiler.v b/driver/Compiler.v index e6d39152..17cb67af 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -306,38 +306,38 @@ Theorem transf_c_program_match: match_prog p tp. Proof. intros p tp T. - unfold transf_c_program, time in T. simpl in T. - destruct (SimplExpr.transl_program p) as [p1|e] eqn:P1; simpl in T; try discriminate. - unfold transf_clight_program, time in T. rewrite ! compose_print_identity in T. simpl in T. - destruct (SimplLocals.transf_program p1) as [p2|e] eqn:P2; simpl in T; try discriminate. - destruct (Cshmgen.transl_program p2) as [p3|e] eqn:P3; simpl in T; try discriminate. - destruct (Cminorgen.transl_program p3) as [p4|e] eqn:P4; simpl in T; try discriminate. - unfold transf_cminor_program, time in T. rewrite ! compose_print_identity in T. simpl in T. - destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate. - destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate. - unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T. simpl in T. + unfold transf_c_program, time in T. cbn in T. + destruct (SimplExpr.transl_program p) as [p1|e] eqn:P1; cbn in T; try discriminate. + unfold transf_clight_program, time in T. rewrite ! compose_print_identity in T. cbn in T. + destruct (SimplLocals.transf_program p1) as [p2|e] eqn:P2; cbn in T; try discriminate. + destruct (Cshmgen.transl_program p2) as [p3|e] eqn:P3; cbn in T; try discriminate. + destruct (Cminorgen.transl_program p3) as [p4|e] eqn:P4; cbn in T; try discriminate. + unfold transf_cminor_program, time in T. rewrite ! compose_print_identity in T. cbn in T. + destruct (Selection.sel_program p4) as [p5|e] eqn:P5; cbn in T; try discriminate. + destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; cbn in T; try discriminate. + unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T. cbn in T. set (p7 := total_if optim_tailcalls Tailcall.transf_program p6) in *. - destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate. + destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; cbn in T; try discriminate. set (p9 := total_if Compopts.optim_move_loop_invariants FirstNop.transf_program p8) in *. set (p9bis := Renumber.transf_program p9) in *. - destruct (partial_if optim_duplicate Duplicate.transf_program p9bis) as [p10|e] eqn:P10; simpl in T; try discriminate. + destruct (partial_if optim_duplicate Duplicate.transf_program p9bis) as [p10|e] eqn:P10; cbn in T; try discriminate. set (p11 := Renumber.transf_program p10) in *. set (p12 := total_if optim_constprop Constprop.transf_program p11) in *. - destruct (partial_if optim_move_loop_invariants LICM.transf_program p12) as [p12bis|e] eqn:P12bis; simpl in T; try discriminate. + destruct (partial_if optim_move_loop_invariants LICM.transf_program p12) as [p12bis|e] eqn:P12bis; cbn in T; try discriminate. set (p12ter :=(total_if optim_move_loop_invariants Renumber.transf_program p12bis)) in *. - destruct (partial_if optim_CSE CSE.transf_program p12ter) as [p13|e] eqn:P13; simpl in T; try discriminate. + destruct (partial_if optim_CSE CSE.transf_program p12ter) as [p13|e] eqn:P13; cbn in T; try discriminate. set (p13bis := total_if optim_CSE2 CSE2.transf_program p13) in *. - destruct (partial_if optim_CSE3 CSE3.transf_program p13bis) as [p13ter|e] eqn:P13ter; simpl in T; try discriminate. + destruct (partial_if optim_CSE3 CSE3.transf_program p13bis) as [p13ter|e] eqn:P13ter; cbn in T; try discriminate. set (p13quater := total_if optim_forward_moves ForwardMoves.transf_program p13ter) in *. - destruct (partial_if optim_redundancy Deadcode.transf_program p13quater) as [p14|e] eqn:P14; simpl in T; try discriminate. + destruct (partial_if optim_redundancy Deadcode.transf_program p13quater) as [p14|e] eqn:P14; cbn in T; try discriminate. set (p14bis := total_if all_loads_nontrap Allnontrap.transf_program p14) in *. - destruct (Unusedglob.transform_program p14bis) as [p15|e] eqn:P15; simpl in T; try discriminate. - destruct (Allocation.transf_program p15) as [p16|e] eqn:P16; simpl in T; try discriminate. + destruct (Unusedglob.transform_program p14bis) as [p15|e] eqn:P15; cbn in T; try discriminate. + destruct (Allocation.transf_program p15) as [p16|e] eqn:P16; cbn in T; try discriminate. set (p17 := Tunneling.tunnel_program p16) in *. - destruct (Linearize.transf_program p17) as [p18|e] eqn:P18; simpl in T; try discriminate. + destruct (Linearize.transf_program p17) as [p18|e] eqn:P18; cbn in T; try discriminate. set (p19 := CleanupLabels.transf_program p18) in *. - destruct (partial_if debug Debugvar.transf_program p19) as [p20|e] eqn:P20; simpl in T; try discriminate. - destruct (Stacking.transf_program p20) as [p21|e] eqn:P21; simpl in T; try discriminate. + destruct (partial_if debug Debugvar.transf_program p19) as [p20|e] eqn:P20; cbn in T; try discriminate. + destruct (Stacking.transf_program p20) as [p21|e] eqn:P21; cbn in T; try discriminate. unfold match_prog; simpl. exists p1; split. apply SimplExprproof.transf_program_match; auto. exists p2; split. apply SimplLocalsproof.match_transf_program; auto. -- cgit From 7a30a72809448535785cd47d26d9415f6ada93e3 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 23 Apr 2020 07:25:57 +0200 Subject: make sure phases are aligned --- driver/Clflags.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 6986fb96..467d41aa 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -79,6 +79,6 @@ let option_fglobaladdroffset = ref false let option_fxsaddr = ref true let option_faddx = ref false let option_fcoalesce_mem = ref true -let option_fforward_moves = ref true +let option_fforward_moves = ref false let option_all_loads_nontrap = ref false let option_inline_auto_threshold = ref 0 -- cgit From 69447b8515c0bd123c6aa72c5545cf9beda79ec4 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 23 Apr 2020 11:43:06 +0200 Subject: fix in CSE3 move propagation --- driver/Compiler.v | 40 ++++++++++++++++++++-------------------- 1 file changed, 20 insertions(+), 20 deletions(-) (limited to 'driver') diff --git a/driver/Compiler.v b/driver/Compiler.v index 3dbd35ce..6a799bd7 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -293,35 +293,35 @@ Theorem transf_c_program_match: match_prog p tp. Proof. intros p tp T. - unfold transf_c_program, time in T. simpl in T. - destruct (SimplExpr.transl_program p) as [p1|e] eqn:P1; simpl in T; try discriminate. - unfold transf_clight_program, time in T. rewrite ! compose_print_identity in T. simpl in T. - destruct (SimplLocals.transf_program p1) as [p2|e] eqn:P2; simpl in T; try discriminate. - destruct (Cshmgen.transl_program p2) as [p3|e] eqn:P3; simpl in T; try discriminate. - destruct (Cminorgen.transl_program p3) as [p4|e] eqn:P4; simpl in T; try discriminate. - unfold transf_cminor_program, time in T. rewrite ! compose_print_identity in T. simpl in T. - destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate. - destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate. - unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T. simpl in T. + unfold transf_c_program, time in T. cbn in T. + destruct (SimplExpr.transl_program p) as [p1|e] eqn:P1; cbn in T; try discriminate. + unfold transf_clight_program, time in T. rewrite ! compose_print_identity in T. cbn in T. + destruct (SimplLocals.transf_program p1) as [p2|e] eqn:P2; cbn in T; try discriminate. + destruct (Cshmgen.transl_program p2) as [p3|e] eqn:P3; cbn in T; try discriminate. + destruct (Cminorgen.transl_program p3) as [p4|e] eqn:P4; cbn in T; try discriminate. + unfold transf_cminor_program, time in T. rewrite ! compose_print_identity in T. cbn in T. + destruct (Selection.sel_program p4) as [p5|e] eqn:P5; cbn in T; try discriminate. + destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; cbn in T; try discriminate. + unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T. cbn in T. set (p7 := total_if optim_tailcalls Tailcall.transf_program p6) in *. - destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate. + destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; cbn in T; try discriminate. set (p9 := Renumber.transf_program p8) in *. - destruct (partial_if optim_duplicate Duplicate.transf_program p9) as [p10|e] eqn:P10; simpl in T; try discriminate. + destruct (partial_if optim_duplicate Duplicate.transf_program p9) as [p10|e] eqn:P10; cbn in T; try discriminate. set (p11 := total_if optim_constprop Constprop.transf_program p10) in *. set (p12 := total_if optim_constprop Renumber.transf_program p11) in *. - destruct (partial_if optim_CSE CSE.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate. + destruct (partial_if optim_CSE CSE.transf_program p12) as [p13|e] eqn:P13; cbn in T; try discriminate. set (p13bis := total_if optim_CSE2 CSE2.transf_program p13) in *. - destruct (partial_if optim_CSE3 CSE3.transf_program p13bis) as [p13ter|e] eqn:P13ter; simpl in T; try discriminate. + destruct (partial_if optim_CSE3 CSE3.transf_program p13bis) as [p13ter|e] eqn:P13ter; cbn in T; try discriminate. set (p13quater := total_if optim_forward_moves ForwardMoves.transf_program p13ter) in *. - destruct (partial_if optim_redundancy Deadcode.transf_program p13quater) as [p14|e] eqn:P14; simpl in T; try discriminate. + destruct (partial_if optim_redundancy Deadcode.transf_program p13quater) as [p14|e] eqn:P14; cbn in T; try discriminate. set (p14bis := total_if all_loads_nontrap Allnontrap.transf_program p14) in *. - destruct (Unusedglob.transform_program p14bis) as [p15|e] eqn:P15; simpl in T; try discriminate. - destruct (Allocation.transf_program p15) as [p16|e] eqn:P16; simpl in T; try discriminate. + destruct (Unusedglob.transform_program p14bis) as [p15|e] eqn:P15; cbn in T; try discriminate. + destruct (Allocation.transf_program p15) as [p16|e] eqn:P16; cbn in T; try discriminate. set (p17 := Tunneling.tunnel_program p16) in *. - destruct (Linearize.transf_program p17) as [p18|e] eqn:P18; simpl in T; try discriminate. + destruct (Linearize.transf_program p17) as [p18|e] eqn:P18; cbn in T; try discriminate. set (p19 := CleanupLabels.transf_program p18) in *. - destruct (partial_if debug Debugvar.transf_program p19) as [p20|e] eqn:P20; simpl in T; try discriminate. - destruct (Stacking.transf_program p20) as [p21|e] eqn:P21; simpl in T; try discriminate. + destruct (partial_if debug Debugvar.transf_program p19) as [p20|e] eqn:P20; cbn in T; try discriminate. + destruct (Stacking.transf_program p20) as [p21|e] eqn:P21; cbn in T; try discriminate. unfold match_prog; simpl. exists p1; split. apply SimplExprproof.transf_program_match; auto. exists p2; split. apply SimplLocalsproof.match_transf_program; auto. -- cgit From 2316b5dc954b4047f3f48c61e7f4e34deb729efe Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 23 Apr 2020 12:29:38 +0200 Subject: make tracing output optional --- driver/Clflags.ml | 1 + driver/Driver.ml | 1 + 2 files changed, 2 insertions(+) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index ff2647a7..a5f5f7a4 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -84,3 +84,4 @@ let option_fcoalesce_mem = ref true let option_fforward_moves = ref true let option_all_loads_nontrap = ref false let option_inline_auto_threshold = ref 0 +let option_debug_compcert = ref 0 diff --git a/driver/Driver.ml b/driver/Driver.ml index b167dbd1..9b873505 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -330,6 +330,7 @@ let cmdline_actions = Exact "-Os", Set option_Osize; Exact "-Obranchless", Set option_Obranchless; Exact "-finline-auto-threshold", Integer (fun n -> option_inline_auto_threshold := n); + Exact "-debug-compcert", Integer (fun n -> option_debug_compcert := n); Exact "-fsmall-data", Integer(fun n -> option_small_data := n); Exact "-fsmall-const", Integer(fun n -> option_small_const := n); Exact "-ffloat-const-prop", Integer(fun n -> option_ffloatconstprop := n); -- cgit From 7b0d7a74ccfaf5843c41e2844e02e94e9a76bfd8 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 23 Apr 2020 14:25:31 +0200 Subject: CSE3 across calls --- driver/Clflags.ml | 3 ++- driver/Compopts.v | 5 ++++- driver/Driver.ml | 4 +++- 3 files changed, 9 insertions(+), 3 deletions(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index b9828f15..9d868de3 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -25,10 +25,11 @@ let option_ffpu = ref true let option_ffloatconstprop = ref 2 let option_ftailcalls = ref true let option_fconstprop = ref true -let option_fcse = ref false +let option_fcse = ref true let option_fcse2 = ref false let option_fcse3 = ref true let option_fcse3_alias_analysis = ref true +let option_fcse3_across_calls = ref false let option_fredundancy = ref true let option_fduplicate = ref (-1) let option_finvertcond = ref true diff --git a/driver/Compopts.v b/driver/Compopts.v index 5acd2640..fb3481e2 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -45,9 +45,12 @@ Parameter optim_CSE2: unit -> bool. (** Flag -fcse3. For DMonniaux's common subexpression elimination. *) Parameter optim_CSE3: unit -> bool. -(** Flag -fcse3-alias-analysis. For DMonniaux's common subexpression elimination. *) +(** Flag -fcse3-alias-analysis. For DMonniaux's common subexpression elimination. Perform a simple alias analysis. *) Parameter optim_CSE3_alias_analysis: unit -> bool. +(** Flag -fcse3-across-calls. For DMonniaux's common subexpression elimination. Propagate information across function calls (may increase register pressure). *) +Parameter optim_CSE3_across_calls: unit -> bool. + (** Flag -fmove-loop-invariants. *) Parameter optim_move_loop_invariants: unit -> bool. diff --git a/driver/Driver.ml b/driver/Driver.ml index 4e4bab16..ea9af62e 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -195,10 +195,11 @@ Processing options: -fconst-prop Perform global constant propagation [on] -ffloat-const-prop Control constant propagation of floats (=0: none, =1: limited, =2: full; default is full) - -fcse Perform common subexpression elimination [off] + -fcse Perform common subexpression elimination [on] -fcse2 Perform inter-loop common subexpression elimination [off] -fcse3 Perform inter-loop common subexpression elimination [on] -fcse3-alias-analysis Perform inter-loop common subexpression elimination with alias analysis [on] + -fcse3-across-calls Propagate CSE3 information across function calls [off] -fmove-loop-invariants Perform loop-invariant code motion [off] -fredundancy Perform redundancy elimination [on] -fpostpass Perform postpass scheduling (only for K1 architecture) [on] @@ -403,6 +404,7 @@ let cmdline_actions = @ f_opt "cse2" option_fcse2 @ f_opt "cse3" option_fcse3 @ f_opt "cse3-alias-analysis" option_fcse3_alias_analysis + @ f_opt "cse3-across-calls" option_fcse3_across_calls @ f_opt "move-loop-invariants" option_fmove_loop_invariants @ f_opt "redundancy" option_fredundancy @ f_opt "postpass" option_fpostpass -- cgit From f1f535cad98f3db3e586f0f7a2dbc329fc5bff6f Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 6 May 2020 20:16:08 +0200 Subject: CSE3 across merges --- driver/Clflags.ml | 1 + driver/Compopts.v | 3 +++ driver/Driver.ml | 2 ++ 3 files changed, 6 insertions(+) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 14d15ba6..d84a546d 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -30,6 +30,7 @@ let option_fcse2 = ref false let option_fcse3 = ref true let option_fcse3_alias_analysis = ref true let option_fcse3_across_calls = ref false +let option_fcse3_across_merges = ref true let option_fredundancy = ref true let option_fduplicate = ref (-1) let option_finvertcond = ref true diff --git a/driver/Compopts.v b/driver/Compopts.v index 3c5ccf36..445f5793 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -51,6 +51,9 @@ Parameter optim_CSE3_alias_analysis: unit -> bool. (** Flag -fcse3-across-calls. For DMonniaux's common subexpression elimination. Propagate information across function calls (may increase register pressure). *) Parameter optim_CSE3_across_calls: unit -> bool. +(** Flag -fcse3-across-calls. For DMonniaux's common subexpression elimination. Propagate information across control-flow merges (may increase register pressure). *) +Parameter optim_CSE3_across_merges: unit -> bool. + (** Flag -fmove-loop-invariants. *) Parameter optim_move_loop_invariants: unit -> bool. diff --git a/driver/Driver.ml b/driver/Driver.ml index b9060ca7..9d1caa9e 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -200,6 +200,7 @@ Processing options: -fcse3 Perform inter-loop common subexpression elimination [on] -fcse3-alias-analysis Perform inter-loop common subexpression elimination with alias analysis [on] -fcse3-across-calls Propagate CSE3 information across function calls [off] + -fcse3-across-merges Propagate CSE3 information across control-flow merges [on] -fmove-loop-invariants Perform loop-invariant code motion [off] -fredundancy Perform redundancy elimination [on] -fpostpass Perform postpass scheduling (only for K1 architecture) [on] @@ -413,6 +414,7 @@ let cmdline_actions = @ f_opt "cse3" option_fcse3 @ f_opt "cse3-alias-analysis" option_fcse3_alias_analysis @ f_opt "cse3-across-calls" option_fcse3_across_calls + @ f_opt "cse3-across-merges" option_fcse3_across_merges @ f_opt "move-loop-invariants" option_fmove_loop_invariants @ f_opt "redundancy" option_fredundancy @ f_opt "postpass" option_fpostpass -- cgit From 6171f6a0880acbf0d007a7715cc37984ac25d851 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 6 May 2020 22:33:02 +0200 Subject: -fcse3-glb --- driver/Clflags.ml | 1 + driver/Compopts.v | 3 +++ driver/Driver.ml | 2 ++ 3 files changed, 6 insertions(+) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index d84a546d..b0d3740e 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -31,6 +31,7 @@ let option_fcse3 = ref true let option_fcse3_alias_analysis = ref true let option_fcse3_across_calls = ref false let option_fcse3_across_merges = ref true +let option_fcse3_glb = ref true let option_fredundancy = ref true let option_fduplicate = ref (-1) let option_finvertcond = ref true diff --git a/driver/Compopts.v b/driver/Compopts.v index 445f5793..d576ede6 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -54,6 +54,9 @@ Parameter optim_CSE3_across_calls: unit -> bool. (** Flag -fcse3-across-calls. For DMonniaux's common subexpression elimination. Propagate information across control-flow merges (may increase register pressure). *) Parameter optim_CSE3_across_merges: unit -> bool. +(** Flag -fcse3-glb *) +Parameter optim_CSE3_glb: unit -> bool. + (** Flag -fmove-loop-invariants. *) Parameter optim_move_loop_invariants: unit -> bool. diff --git a/driver/Driver.ml b/driver/Driver.ml index 9d1caa9e..90afb812 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -201,6 +201,7 @@ Processing options: -fcse3-alias-analysis Perform inter-loop common subexpression elimination with alias analysis [on] -fcse3-across-calls Propagate CSE3 information across function calls [off] -fcse3-across-merges Propagate CSE3 information across control-flow merges [on] + -fcse3-glb Refine CSE3 information using greatest lower bounds [on] -fmove-loop-invariants Perform loop-invariant code motion [off] -fredundancy Perform redundancy elimination [on] -fpostpass Perform postpass scheduling (only for K1 architecture) [on] @@ -415,6 +416,7 @@ let cmdline_actions = @ f_opt "cse3-alias-analysis" option_fcse3_alias_analysis @ f_opt "cse3-across-calls" option_fcse3_across_calls @ f_opt "cse3-across-merges" option_fcse3_across_merges + @ f_opt "cse3-glb" option_fcse3_glb @ f_opt "move-loop-invariants" option_fmove_loop_invariants @ f_opt "redundancy" option_fredundancy @ f_opt "postpass" option_fpostpass -- cgit From b4a08d0815342b6238d307864f0823d0f07bb691 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 26 May 2020 22:04:20 +0200 Subject: k1c -> kvx changes --- driver/Clflags.ml | 2 +- driver/Configuration.ml | 2 +- driver/Frontend.ml | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index b0d3740e..eb21b3f8 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -15,7 +15,7 @@ let prepro_options = ref ([]: string list) let linker_options = ref ([]: string list) let assembler_options = ref ([]: string list) -let option_flongdouble = ref (Configuration.arch = "mppa_k1c") +let option_flongdouble = ref (Configuration.arch = "kvx") let option_fstruct_passing = ref false let option_fbitfields = ref false let option_fvararg_calls = ref true diff --git a/driver/Configuration.ml b/driver/Configuration.ml index 08084720..1d40214a 100644 --- a/driver/Configuration.ml +++ b/driver/Configuration.ml @@ -123,7 +123,7 @@ let get_bool_config key = let arch = match get_config_string "arch" with - | "powerpc"|"arm"|"x86"|"riscV"|"mppa_k1c"|"aarch64" as a -> a + | "powerpc"|"arm"|"x86"|"riscV"|"kvx"|"aarch64" as a -> a | v -> bad_config "arch" [v] let model = get_config_string "model" let abi = get_config_string "abi" diff --git a/driver/Frontend.ml b/driver/Frontend.ml index b9db0d23..5db0040f 100644 --- a/driver/Frontend.ml +++ b/driver/Frontend.ml @@ -116,7 +116,7 @@ let init () = | "riscV" -> if Configuration.model = "64" then Machine.rv64 else Machine.rv32 - | "mppa_k1c" -> Machine.mppa_k1c + | "kvx" -> Machine.kvx | "aarch64" -> Machine.aarch64 | _ -> assert false end; -- cgit