Revised instruction selection for the "select" operation

Instead of returning an optional expression, `SelectOp.select` now
always returns a CminorSel expression.  A separate Boolean-valued
function `SelectOp.select_supported` indicates at which types "select"
is supported.

Author: xavierleroy

aarch64/SelectOp.vp

@@ -523,16 +523,14 @@ Definition floatofsingle (e: expr) := Eop Ofloatofsingle (e ::: Enil).
 
 (** ** Selection *)
 
+Definition select_supported (ty: typ) :=
+  match ty with
+  | Tint | Tlong | Tfloat | Tsingle => true
+  | _ => false
+  end.
+
 Definition select (ty: typ) (cond: condition) (args: exprlist) (e1 e2: expr) :=
-  if match ty with
-     | Tint => true
-     | Tlong => true
-     | Tfloat => true
-     | Tsingle => true
-     | _ => false
-     end
-  then Some (Eop (Osel cond ty) (e1 ::: e2 ::: args))
-  else None.
+  Eop (Osel cond ty) (e1 ::: e2 ::: args).
 
 (** ** Recognition of addressing modes for load and store operations *)
 

aarch64/SelectOpproof.v

@@ -1000,18 +1000,16 @@ Qed.
 (** Selection *)
 
 Theorem eval_select:
-  forall le ty cond al vl a1 v1 a2 v2 a,
-  select ty cond al a1 a2 = Some a ->
+  forall le ty cond al vl a1 v1 a2 v2,
+  select_supported ty = true ->
   eval_exprlist ge sp e m le al vl ->
   eval_expr ge sp e m le a1 v1 ->
   eval_expr ge sp e m le a2 v2 ->
   exists v,
-     eval_expr ge sp e m le a v
+     eval_expr ge sp e m le (select ty cond al a1 a2) v
   /\ Val.lessdef (Val.select (eval_condition cond vl m) v1 v2 ty) v.
 Proof.
-  unfold select; intros.
-  destruct (match ty with Tint | Tlong | Tfloat | Tsingle => true | _ => false end); inv H.
-  econstructor; split; EvalOp; eauto.
+  unfold select; intros. TrivialExists.
 Qed.
 
 (** Addressing modes *)

arm/SelectOp.vp

@@ -379,15 +379,16 @@ Definition compf (c: comparison) (e1: expr) (e2: expr) :=
 Definition compfs (c: comparison) (e1: expr) (e2: expr) :=
   Eop (Ocmp (Ccompfs c)) (e1 ::: e2 ::: Enil).
 
+(** ** Selection *)
+
+Definition select_supported (ty: typ) :=
+  match ty with
+  | Tint | Tfloat | Tsingle => true
+  | _ => false
+  end.
+
 Definition select (ty: typ) (cond: condition) (args: exprlist) (e1 e2: expr) :=
-  if match ty with
-     | Tint => true
-     | Tfloat => true
-     | Tsingle => true
-     | _ => false
-     end
-  then Some (Eop (Osel cond ty) (e1 ::: e2 ::: args))
-  else None.
+  Eop (Osel cond ty) (e1 ::: e2 ::: args).
 
 (** ** Integer conversions *)
 

arm/SelectOpproof.v

@@ -729,18 +729,16 @@ Proof.
 Qed.
 
 Theorem eval_select:
-  forall le ty cond al vl a1 v1 a2 v2 a,
-  select ty cond al a1 a2 = Some a ->
+  forall le ty cond al vl a1 v1 a2 v2,
+  select_supported ty = true ->
   eval_exprlist ge sp e m le al vl ->
   eval_expr ge sp e m le a1 v1 ->
   eval_expr ge sp e m le a2 v2 ->
   exists v,
-     eval_expr ge sp e m le a v
+     eval_expr ge sp e m le (select ty cond al a1 a2) v
   /\ Val.lessdef (Val.select (eval_condition cond vl m) v1 v2 ty) v.
 Proof.
-  unfold select; intros.
-  destruct (match ty with Tint | Tfloat | Tsingle => true | _ => false end); inv H.
-  econstructor; split; eauto; EvalOp.
+  unfold select; intros. TrivialExists.
 Qed.
 
 Theorem eval_cast8signed: unary_constructor_sound cast8signed (Val.sign_ext 8).

backend/Selection.v

@@ -164,10 +164,9 @@ Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr :=
 
 Definition sel_select (ty: typ) (cnd ifso ifnot: expr) : expr :=
    let (cond, args) := condition_of_expr cnd in
-   match SelectOp.select ty cond args ifso ifnot with
-   | Some a => a
-   | None => Econdition (condexpr_of_expr cnd) ifso ifnot
-   end.
+   if SelectOp.select_supported ty
+   then SelectOp.select ty cond args ifso ifnot
+   else Econdition (condexpr_of_expr cnd) ifso ifnot.
 
 (** Conversion from Cminor expression to Cminorsel expressions *)
 
@@ -186,7 +185,7 @@ Fixpoint sel_exprlist (al: list Cminor.expr) : exprlist :=
   | a :: bl => Econs (sel_expr a) (sel_exprlist bl)
   end.
 
-Definition sel_select_opt (ty: typ) (arg1 arg2 arg3: Cminor.expr) : option expr :=
+Definition sel_select_expr (ty: typ) (arg1 arg2 arg3: Cminor.expr) : expr :=
   let (cond, args) := condition_of_expr (sel_expr arg1) in
   SelectOp.select ty cond args (sel_expr arg2) (sel_expr arg3).
 
@@ -375,12 +374,11 @@ Definition if_conversion_base
       (cond: Cminor.expr) (id: ident) (ifso ifnot:  Cminor.expr)
       (kont: stmt) : option stmt :=
   let ty := env id in
-  if is_known ki id
+  if SelectOp.select_supported ty
+  && is_known ki id
   && safe_expr ki ifso && safe_expr ki ifnot
   && if_conversion_heuristic id cond ifso ifnot ty kont
-  then option_map
-         (fun sel => Sassign id sel)
-         (sel_select_opt ty cond ifso ifnot)
+  then Some (Sassign id (sel_select_expr ty cond ifso ifnot))
   else None.
 
 Definition if_conversion

backend/Selectionproof.v

@@ -361,10 +361,10 @@ Lemma eval_sel_select:
         /\  Val.lessdef (Val.select (Some b) v2 v3 ty) v.
 Proof.
   unfold sel_select; intros.
-  specialize (eval_condition_of_expr _ _ _ _ H H2). 
+  specialize (eval_condition_of_expr _ _ _ _ H H2).
   destruct (condition_of_expr a1) as [cond args]; simpl fst; simpl snd. intros (vl & A & B).
-  destruct (select ty cond args a2 a3) as [a|] eqn:SEL.
-- exploit eval_select; eauto. rewrite B. auto.
+  destruct (select_supported ty) eqn:SUP.
+- rewrite <- B. eapply eval_select; eauto. 
 - exists (if b then v2 else v3); split.
   econstructor; eauto. eapply eval_condexpr_of_expr; eauto. destruct b; auto.
   apply Val.lessdef_normalize.
@@ -776,27 +776,29 @@ Proof.
   exists (v1' :: vl'); split; auto. constructor; eauto.
 Qed.
 
-Lemma sel_select_opt_correct:
-  forall ty cond a1 a2 a sp e m vcond v1 v2 b e' m' le,
-  sel_select_opt ty cond a1 a2 = Some a ->
+Lemma sel_select_expr_correct:
+  forall ty cond a1 a2 sp e m vcond v1 v2 b e' m' le,
+  SelectOp.select_supported ty = true ->
   Cminor.eval_expr ge sp e m cond vcond ->
   Cminor.eval_expr ge sp e m a1 v1 ->
   Cminor.eval_expr ge sp e m a2 v2 ->
   Val.bool_of_val vcond b ->
   env_lessdef e e' -> Mem.extends m m' ->
-  exists v', eval_expr tge sp e' m' le a v' /\ Val.lessdef (Val.select (Some b) v1 v2 ty) v'.
+  exists v', eval_expr tge sp e' m' le (sel_select_expr ty cond a1 a2) v'
+          /\ Val.lessdef (Val.select (Some b) v1 v2 ty) v'.
 Proof.
-  unfold sel_select_opt; intros. 
+  unfold sel_select_expr; intros. 
   destruct (condition_of_expr (sel_expr cond)) as [cnd args] eqn:C.
   exploit sel_expr_correct. eexact H0. eauto. eauto. intros (vcond' & EVC & LDC).
   exploit sel_expr_correct. eexact H1. eauto. eauto. intros (v1' & EV1 & LD1).
   exploit sel_expr_correct. eexact H2. eauto. eauto. intros (v2' & EV2 & LD2).
   assert (Val.bool_of_val vcond' b) by (inv H3; inv LDC; constructor).
   exploit eval_condition_of_expr. eexact EVC. eauto. rewrite C. intros (vargs' & EVARGS & EVCOND).
-  exploit eval_select; eauto. intros (v' & X & Y). 
+  exploit (eval_select tge sp e' m' le ty cnd args vargs' (sel_expr a1) v1' (sel_expr a2) v2'); eauto.
+  simpl in EVCOND; rewrite EVCOND. intros (v' & X & Y). 
   exists v'; split; eauto. 
   eapply Val.lessdef_trans; [|eexact Y].
-  apply Val.select_lessdef; auto.
+  apply Val.normalize_lessdef. destruct b; auto.
 Qed.
 
 Lemma sel_builtin_arg_correct:
@@ -984,17 +986,15 @@ Lemma if_conversion_base_correct:
            E0 (State tf Sskip tk sp (PTree.set id v' e') m').
 Proof.
   unfold if_conversion_base; intros. rewrite H2 in H. clear H2.
-  destruct andb eqn:C; try discriminate.
-  destruct (sel_select_opt ty cond ifso ifnot) as [a'|] eqn:SSO; simpl in H; inv H.
-  InvBooleans.
+  destruct andb eqn:C; inv H. InvBooleans.
   destruct (eval_safe_expr ge f sp e m ifso) as (v1 & EV1); auto.
   destruct (eval_safe_expr ge f sp e m ifnot) as (v2 & EV2); auto.
   assert (TY1: Val.has_type v1 ty) by (eapply wt_eval_expr; eauto).
   assert (TY2: Val.has_type v2 ty) by (eapply wt_eval_expr; eauto).
-  exploit sel_select_opt_correct; eauto. intros (v' & EV' & LD).
+  exploit (sel_select_expr_correct ty cond ifso ifnot); eauto. intros (v' & EV & LD).
   simpl in LD. rewrite Val.normalize_idem in LD by (destruct b; auto).
   exists v1, v2, v'; intuition auto.
-  constructor. eexact EV'.
+  constructor. exact EV.
 Qed.
 
 Lemma if_conversion_correct:
@@ -1176,8 +1176,7 @@ Lemma if_conversion_base_nolabel: forall (hf: helper_functions) ki env a id a1 a
   nolabel' s.
 Proof.
   unfold if_conversion_base; intros.
-  destruct andb; try discriminate.
-  destruct (sel_select_opt (env id) a a1 a2); inv H. 
+  destruct andb; inv H. 
   red; auto.
 Qed.
 

powerpc/SelectOp.vp

@@ -518,16 +518,15 @@ Definition floatofsingle (e: expr) := Eop Ofloatofsingle (e ::: Enil).
 
 (** ** Selection *)
 
+Definition select_supported (ty: typ) :=
+  match ty with
+  | Tint | Tfloat | Tsingle => true
+  | Tlong => Archi.ppc64
+  | _ => false
+  end.
+
 Definition select (ty: typ) (cond: condition) (args: exprlist) (e1 e2: expr) :=
-  if match ty with
-     | Tint => true
-     | Tfloat => true
-     | Tsingle => true
-     | Tlong => Archi.ppc64
-     | _ => false
-     end
-  then Some (Eop (Osel cond ty) (e1 ::: e2 ::: args))
-  else None.
+  Eop (Osel cond ty) (e1 ::: e2 ::: args).
 
 (** ** Recognition of addressing modes for load and store operations *)
 

powerpc/SelectOpproof.v

@@ -1000,19 +1000,16 @@ Proof.
 Qed.
 
 Theorem eval_select:
-  forall le ty cond al vl a1 v1 a2 v2 a,
-  select ty cond al a1 a2 = Some a ->
+  forall le ty cond al vl a1 v1 a2 v2,
+  select_supported ty = true ->
   eval_exprlist ge sp e m le al vl ->
   eval_expr ge sp e m le a1 v1 ->
   eval_expr ge sp e m le a2 v2 ->
   exists v,
-     eval_expr ge sp e m le a v
+     eval_expr ge sp e m le (select ty cond al a1 a2) v
   /\ Val.lessdef (Val.select (eval_condition cond vl m) v1 v2 ty) v.
 Proof.
-  unfold select; intros.
-  destruct (match ty with Tint => true | Tfloat => true | Tsingle => true | Tlong => Archi.ppc64 | _ => false end); inv H.
-  exists (Val.select (eval_condition cond vl m) v1 v2 ty); split; auto.
-  EvalOp.
+  unfold select; intros. TrivialExists.
 Qed.
 
 Theorem eval_addressing:

riscV/SelectOp.vp

@@ -444,12 +444,9 @@ Definition select_swap (cond: condition) : bool :=
   end.
 
 Definition select (ty: typ) (cond: condition) (args: exprlist) (e1 e2: expr) :=
-  if select_supported ty then
-    if select_swap cond
-    then Some (Eop (Osel (negate_condition cond) ty) (e2 ::: e1 ::: args))
-    else Some (Eop (Osel cond ty) (e1 ::: e2 ::: args))
-  else
-    None.
+  if select_swap cond
+  then Eop (Osel (negate_condition cond) ty) (e2 ::: e1 ::: args)
+  else Eop (Osel cond ty) (e1 ::: e2 ::: args).
 
 (** ** Recognition of addressing modes for load and store operations *)
 

riscV/SelectOpproof.v

@@ -866,17 +866,16 @@ Proof.
 Qed.
 
 Theorem eval_select:
-  forall le ty cond al vl a1 v1 a2 v2 a,
-  select ty cond al a1 a2 = Some a ->
+  forall le ty cond al vl a1 v1 a2 v2,
+  select_supported ty = true ->
   eval_exprlist ge sp e m le al vl ->
   eval_expr ge sp e m le a1 v1 ->
   eval_expr ge sp e m le a2 v2 ->
   exists v,
-     eval_expr ge sp e m le a v
+     eval_expr ge sp e m le (select ty cond al a1 a2) v
   /\ Val.lessdef (Val.select (eval_condition cond vl m) v1 v2 ty) v.
 Proof.
   unfold select; intros.
-  destruct (select_supported ty); try discriminate.
   destruct (select_swap cond); inv H.
 - TrivialExists. simpl. rewrite eval_negate_condition. destruct (eval_condition cond vl m) as [[]|]; simpl; auto.
 - TrivialExists.