If-conversion optimization

Extends the instruction selection pass with an if-conversion optimization:
some if/then/else statements are converted into "select" operations,
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.

A heuristic in backend/Selectionaux.ml controls when the optimization occurs,
depending on command-line flags and the complexity of the "then" and "else"
branches.

1 files changed, 64 insertions, 0 deletions

diff --git a/backend/Cminor.v b/backend/Cminor.v
index 11941da3..ca01ad50 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -591,6 +591,70 @@ Proof.
   red; intros; inv H; simpl; try omega; eapply external_call_trace_length; eauto.
 Qed.
 
+(** This semantics is determinate. *)
+
+Lemma eval_expr_determ:
+  forall ge sp e m a v, eval_expr ge sp e m a v ->
+  forall v', eval_expr ge sp e m a v' -> v' = v.
+Proof.
+  induction 1; intros v' E'; inv E'.
+- congruence.
+- congruence.
+- assert (v0 = v1) by eauto. congruence.
+- assert (v0 = v1) by eauto. assert (v3 = v2) by eauto. congruence.
+- assert (vaddr0 = vaddr) by eauto. congruence.
+Qed.
+
+Lemma eval_exprlist_determ:
+  forall ge sp e m al vl, eval_exprlist ge sp e m al vl ->
+  forall vl', eval_exprlist ge sp e m al vl' -> vl' = vl.
+Proof.
+  induction 1; intros vl' E'; inv E'.
+  - auto.
+  - f_equal; eauto using eval_expr_determ.
+Qed.
+
+Ltac Determ :=
+  try congruence;
+  match goal with
+  | [ |- match_traces _ E0 E0 /\ (_ -> _) ]  =>
+          split; [constructor|intros _; Determ]
+  | [ H: is_call_cont ?k |- _ ] =>
+          contradiction || (clear H; Determ)
+  | [ H1: eval_expr _ _ _ _ ?a ?v1, H2: eval_expr _ _ _ _ ?a ?v2 |- _ ] =>
+          assert (v1 = v2) by (eapply eval_expr_determ; eauto);
+          clear H1 H2; Determ
+  | [ H1: eval_exprlist _ _ _ _ ?a ?v1, H2: eval_exprlist _ _ _ _ ?a ?v2 |- _ ] =>
+          assert (v1 = v2) by (eapply eval_exprlist_determ; eauto);
+          clear H1 H2; Determ
+  | _ => idtac
+  end.
+
+Lemma semantics_determinate:
+  forall (p: program), determinate (semantics p).
+Proof.
+  intros. constructor; set (ge := Genv.globalenv p); simpl; intros.
+- (* determ *)
+  inv H; inv H0; Determ.
+  + subst vargs0. exploit external_call_determ. eexact H2. eexact H13.
+    intros (A & B). split; intros; auto.
+    apply B in H; destruct H; congruence.
+  + subst v0. assert (b0 = b) by (inv H2; inv H13; auto). subst b0; auto.
+  + assert (n0 = n) by (inv H2; inv H14; auto). subst n0; auto.
+  + exploit external_call_determ. eexact H1. eexact H7.
+    intros (A & B). split; intros; auto.
+    apply B in H; destruct H; congruence.
+- (* single event *)
+  red; simpl. destruct 1; simpl; try omega;
+  eapply external_call_trace_length; eauto.
+- (* initial states *)
+  inv H; inv H0. unfold ge0, ge1 in *. congruence.
+- (* nostep final state *)
+  red; intros; red; intros. inv H; inv H0.
+- (* final states *)
+  inv H; inv H0; auto.
+Qed.
+
 (** * Alternate operational semantics (big-step) *)
 
 (** We now define another semantics for Cminor without [goto] that follows