From a9a07e3b672711f74bde27bd72b518631e3a29b4 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 19 May 2019 11:24:03 +0200 Subject: If-conversion optimization for Cminor Add an experimental pass that converts some if/then/else statements into "select" built-ins, which in turn can be compiled down to branchless instruction sequences if the target architecture supports them. The statements that are converted are of the form if (cond) { x = a1; } else { x = a2; } if (cond) { x = a1; } if (cond) { /*skip*/; } else { x = a2; } where a1, a2 are "safe" expressions, containing no operations that can fail at run-time, such as memory loads or integer divisions. To support the optimization, I added a type inference and type checking pass for Cminor, in backend/Cminortyping.v. The inferred type information is used to determine the type at which the "select" built-in operates, and to prove semantic preservation. --- driver/Compiler.v | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) (limited to 'driver') diff --git a/driver/Compiler.v b/driver/Compiler.v index 75247f71..48404b46 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -33,6 +33,7 @@ Require SimplExpr. Require SimplLocals. Require Cshmgen. Require Cminorgen. +Require Ifconv. Require Selection. Require RTLgen. Require Tailcall. @@ -54,6 +55,7 @@ Require SimplExprproof. Require SimplLocalsproof. Require Cshmgenproof. Require Cminorgenproof. +Require Ifconvproof. Require Selectionproof. Require RTLgenproof. Require Tailcallproof. @@ -149,6 +151,7 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := Definition transf_cminor_program (p: Cminor.program) : res Asm.program := OK p @@ print print_Cminor + @@@ time "If-conversion" Ifconv.transf_program @@@ time "Instruction selection" Selection.sel_program @@@ time "RTL generation" RTLgen.transl_program @@@ transf_rtl_program. @@ -233,6 +236,7 @@ Definition CompCert's_passes := ::: mkpass SimplLocalsproof.match_prog ::: mkpass Cshmgenproof.match_prog ::: mkpass Cminorgenproof.match_prog + ::: mkpass Ifconvproof.match_prog ::: mkpass Selectionproof.match_prog ::: mkpass RTLgenproof.match_prog ::: mkpass (match_if Compopts.optim_tailcalls Tailcallproof.match_prog) @@ -275,7 +279,8 @@ Proof. 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 (Ifconv.transf_program p4) as [p41|e] eqn:P41; simpl in T; try discriminate. + destruct (Selection.sel_program p41) 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 *. @@ -297,6 +302,7 @@ Proof. 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 p41; split. apply Ifconvproof.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. @@ -364,7 +370,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 p21)). + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p22)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -374,6 +380,8 @@ Ltac DestructM := eapply Cshmgenproof.transl_program_correct; eassumption. eapply compose_forward_simulations. eapply Cminorgenproof.transl_program_correct; eassumption. + eapply compose_forward_simulations. + eapply Ifconvproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply Selectionproof.transf_program_correct; eassumption. eapply compose_forward_simulations. -- cgit