selectl with condition

8 files changed, 172 insertions, 68 deletions

diff --git a/backend/Selection.v b/backend/Selection.v
index 7191d5cb..971f9948 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -296,10 +296,7 @@ Definition sel_builtin optid ef args :=
            | Some id =>
              match args with
                | a1::a2::a3::nil =>
-                 OK (Sassign id (Eop Oselectl
-                                     ((sel_expr a3):::
-                                                   (sel_expr a2):::
-                                                   (sel_expr a1):::Enil)))
+                 OK (Sassign id (selectl (sel_expr a3) (sel_expr a2) (sel_expr a1)))
                | _ => Error (msg "__builtin_ternary_(u)long: arguments")
              end
          end
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index d8706239..b3478a9a 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -751,7 +751,8 @@ Definition transl_op
       do rd <- ireg_of res;
       transl_cond_op cmp rd args k
 
-  | Oselect cond, a0 :: a1 :: aS :: nil =>
+  | Oselect cond, a0 :: a1 :: aS :: nil
+  | Oselectl cond, a0 :: a1 :: aS :: nil =>
     assertion (mreg_eq a0 res);
       do r0 <- ireg_of a0;
       do r1 <- ireg_of a1;
@@ -769,7 +770,6 @@ Definition transl_op
            OK (Pcmoveu bt r0 rS r1 ::i k)
        end)
     
-  | Oselectl, a0 :: a1 :: aS :: nil
   | Oselectf, a0 :: a1 :: aS :: nil
   | Oselectfs, a0 :: a1 :: aS :: nil =>
     assertion (mreg_eq a0 res);
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index 1cb75c4c..874e40a8 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -1698,20 +1698,67 @@ Opaque Int.eq.
     * intros.
       rewrite Pregmap.gso; congruence.
 
-- (* Oselectl *)
-  econstructor; split.
-  + eapply exec_straight_one.
-    simpl; reflexivity.
+- (* Oselect *)
+  destruct cond in *; simpl in *; try congruence;
+    try monadInv EQ3;
+    try (injection EQ3; clear EQ3; intro Hrew; rewrite <- Hrew in * ; clear Hrew);
+  econstructor; split;
+  try ( eapply exec_straight_one; simpl; reflexivity ).
+  (* Cmp *)
   + split.
-    * unfold eval_selectl.
-      destruct (rs x1) eqn:eqX1; try constructor.
+    * unfold eval_select.
       destruct (rs x) eqn:eqX; try constructor.
       destruct (rs x0) eqn:eqX0; try constructor.
-      simpl.
-      rewrite int_eq_comm.
-      destruct (Int.eq i Int.zero); simpl; rewrite Pregmap.gss; constructor.
+      destruct c0 in *; simpl;
+      destruct (Val.cmp_bool _ _); simpl; try constructor;
+        destruct b; simpl; rewrite Pregmap.gss; constructor.
     * intros.
       rewrite Pregmap.gso; congruence.
+  (* Cmpu *)
+  + split.
+    * unfold eval_select.
+      destruct (rs x) eqn:eqX; try constructor.
+      destruct (rs x0) eqn:eqX0; try constructor.
+      destruct c0 in *; simpl in *; inv EQ2; simpl.
+      ** assert (Hcmpuabs := (Val_cmpu_bool_correct m Ceq (rs x1) (Vint Int.zero))).
+         destruct (Val.cmpu_bool _ _); simpl; try constructor.
+         destruct b in *; simpl in *; [ rewrite (Hcmpuabs true) | rewrite (Hcmpuabs false)]; trivial;
+         rewrite Pregmap.gss; constructor.
+      ** assert (Hcmpuabs := (Val_cmpu_bool_correct m Cne (rs x1) (Vint Int.zero))).
+         destruct (Val.cmpu_bool _ _); simpl; try constructor.
+         destruct b in *; simpl in *; [ rewrite (Hcmpuabs true) | rewrite (Hcmpuabs false)]; trivial;
+         rewrite Pregmap.gss; constructor.
+    * intros.
+      rewrite Pregmap.gso; congruence.
+
+  (* Cmpl *)
+  + split.
+    * unfold eval_select.
+      destruct (rs x) eqn:eqX; try constructor.
+      destruct (rs x0) eqn:eqX0; try constructor.
+      destruct c0 in *; simpl;
+      destruct (Val.cmpl_bool _ _); simpl; try constructor;
+        destruct b; simpl; rewrite Pregmap.gss; constructor.
+    * intros.
+      rewrite Pregmap.gso; congruence.
+      
+  (* Cmplu *)
+  + split.
+    * unfold eval_select.
+      destruct (rs x) eqn:eqX; try constructor.
+      destruct (rs x0) eqn:eqX0; try constructor.
+      destruct c0 in *; simpl in *; inv EQ2; simpl.
+      ** assert (Hcmpluabs := (Val_cmplu_bool_correct m Ceq (rs x1) (Vlong Int64.zero))).
+         destruct (Val.cmplu_bool _ _); simpl; try constructor.
+         destruct b in *; simpl in *; [ rewrite (Hcmpluabs true) | rewrite (Hcmpluabs false)]; trivial;
+         rewrite Pregmap.gss; constructor.
+      ** assert (Hcmpluabs := (Val_cmplu_bool_correct m Cne (rs x1) (Vlong Int64.zero))).
+         destruct (Val.cmplu_bool _ _); simpl; try constructor.
+         destruct b in *; simpl in *; [ rewrite (Hcmpluabs true) | rewrite (Hcmpluabs false)]; trivial;
+         rewrite Pregmap.gss; constructor.
+    * intros.
+      rewrite Pregmap.gso; congruence.
+
 - (* Oselectf *)
   econstructor; split.
   + eapply exec_straight_one.
diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v
index daf724ea..ddf730a9 100644
--- a/mppa_k1c/Machregs.v
+++ b/mppa_k1c/Machregs.v
@@ -209,7 +209,7 @@ Global Opaque
 
 Definition two_address_op (op: operation) : bool :=
   match op with
-  | Ocast32unsigned | Omadd | Omaddimm _ | Omaddl | Omaddlimm _ | Oselect _ | Oselectl | Oselectf | Oselectfs => true
+  | Ocast32unsigned | Omadd | Omaddimm _ | Omaddl | Omaddlimm _ | Oselect _ | Oselectl _ | Oselectf | Oselectfs => true
   | _ => false
   end.
 
diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v
index d385ebac..a276cda1 100644
--- a/mppa_k1c/NeedOp.v
+++ b/mppa_k1c/NeedOp.v
@@ -117,7 +117,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Ointofsingle | Ointuofsingle | Osingleofint | Osingleofintu => op1 (default nv)
   | Olongofsingle | Olonguofsingle | Osingleoflong | Osingleoflongu => op1 (default nv)
   | Ocmp c => needs_of_condition c
-  | Oselect _ | Oselectl | Oselectf | Oselectfs => op3 (default nv)
+  | Oselect _ | Oselectl _ | Oselectf | Oselectfs => op3 (default nv)
   end.
 
 Definition operation_is_redundant (op: operation) (nv: nval): bool :=
@@ -289,22 +289,46 @@ Proof.
 Qed.
 
 Lemma selectl_sound:
-  forall v0 w0 v1 w1 v2 w2 x,
+  forall cond v0 w0 v1 w1 v2 w2 x,
     vagree v0 w0 (default x) ->
     vagree v1 w1 (default x) ->
     vagree v2 w2 (default x) ->
-    vagree (eval_selectl v0 v1 v2) (eval_selectl w0 w1 w2) x.
+    vagree (eval_selectl cond v0 v1 v2 m1) (eval_selectl cond w0 w1 w2 m2) x.
 Proof.
-  unfold default; intros.
-  destruct x; trivial.
-  - destruct v2; simpl; trivial.
-    destruct v0; simpl; trivial.
-    destruct v1; simpl; trivial.
-  - destruct v2; simpl; trivial.
-    destruct v0; simpl; trivial.
-    destruct v1; simpl; trivial.
-    inv H. inv H0. inv H1. simpl.
-    constructor.
+  intros.
+  destruct x; simpl in *; trivial.
+  - rewrite eval_selectl_to2.
+    rewrite eval_selectl_to2.
+    unfold eval_selectl2.
+    assert (Hneedstrue := (needs_of_condition0_sound cond v2 true w2)).
+    assert (Hneedsfalse := (needs_of_condition0_sound cond v2 false w2)).
+    destruct (eval_condition0 cond v2 m1) in *; simpl in *; trivial.
+    destruct b.
+    + rewrite Hneedstrue; trivial.
+      inv H; trivial.
+      destruct w0; trivial.
+      inv H0; trivial.
+      destruct w1; trivial.
+    + rewrite Hneedsfalse; trivial.
+      inv H; trivial.
+      destruct w0; trivial.
+      inv H0; trivial.
+      destruct w1; trivial.
+  - rewrite eval_selectl_to2.
+    rewrite eval_selectl_to2.
+    unfold eval_selectl2.
+    assert (Hneedstrue := (needs_of_condition0_sound cond v2 true w2)).
+    assert (Hneedsfalse := (needs_of_condition0_sound cond v2 false w2)).
+    destruct (eval_condition0 cond v2 m1) in *; simpl in *; trivial.
+    destruct b.
+    + rewrite Hneedstrue; trivial.
+      inv H; trivial.
+      destruct w0; trivial.
+      inv H0; trivial.
+    + rewrite Hneedsfalse; trivial.
+      inv H; trivial.
+      destruct w0; trivial.
+      inv H0; trivial.
 Qed.
 
 Lemma selectf_sound:
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index 51d70693..045946fd 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -194,8 +194,8 @@ Inductive operation : Type :=
   | Osingleoflongu           (**r [rd = float32_of_unsigned_int(r1)] *)
 (*c Boolean tests: *)
   | Ocmp (cond: condition)   (**r [rd = 1] if condition holds, [rd = 0] otherwise. *)
-  | Oselect (cond: condition0) (**r [rd = if r3 then r2 else r1] *)
-  | Oselectl                 (**r [rd = if r3 then r2 else r1] *)
+  | Oselect (cond: condition0) (**r [rd = if cond r3 then r2 else r1] *)
+  | Oselectl (cond: condition0)(**r [rd = if cond r3 then r2 else r1] *)
   | Oselectf                 (**r [rd = if r3 then r2 else r1] *)
   | Oselectfs.               (**r [rd = if r3 then r2 else r1] *)
 
@@ -303,23 +303,27 @@ Proof.
   destruct v0; destruct v1; simpl; destruct (eval_condition0 cond vselect m); simpl; reflexivity.
 Qed.
 
-Definition eval_selectl (v0 : val) (v1 : val) (vselect : val) : val :=
-  match vselect with
-  | Vint iselect =>
-    match v0 with
-    | Vlong i0 =>
-      match v1 with
-      | Vlong i1 =>
-        Vlong (if Int.cmp Ceq Int.zero iselect
-               then i0
-               else i1)
-      | _ => Vundef
-      end
-    | _ => Vundef
-    end
-  | _ => Vundef
+Definition eval_selectl (cond: condition0) (v0 : val) (v1 : val) (vselect : val) (m: mem) : val :=
+  match v0, v1, (eval_condition0 cond vselect m) with
+    | Vlong i0, Vlong i1, Some bval => Vlong (if bval then i1 else i0)
+    | _,_,_ => Vundef
   end.
 
+Definition eval_selectl2 (cond : condition0) (v0 : val) (v1 : val) (vselect : val) (m: mem) : val :=
+  match (eval_condition0 cond vselect m), v0, v1 with
+    | Some bval, Vlong i0, Vlong i1 => Vlong (if bval then i1 else i0)
+    | _,_,_ => Vundef
+  end.
+
+Lemma eval_selectl_to2: forall cond v0 v1 vselect m,
+    (eval_selectl cond v0 v1 vselect m) =
+    (eval_selectl2 cond v0 v1 vselect m).
+Proof.
+  intros.
+  unfold eval_selectl2.
+  destruct v0; destruct v1; simpl; destruct (eval_condition0 cond vselect m); simpl; reflexivity.
+Qed.
+
 Definition eval_selectf (v0 : val) (v1 : val) (vselect : val) : val :=
   match vselect with
   | Vint iselect =>
@@ -483,7 +487,7 @@ Definition eval_operation
   | Osingleoflongu, v1::nil => Val.singleoflongu v1
   | Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m))
   | (Oselect cond), v0::v1::vselect::nil => Some (eval_select cond v0 v1 vselect m)
-  | Oselectl, v0::v1::vselect::nil => Some (eval_selectl v0 v1 vselect)
+  | (Oselectl cond), v0::v1::vselect::nil => Some (eval_selectl cond v0 v1 vselect m)
   | Oselectf, v0::v1::vselect::nil => Some (eval_selectf v0 v1 vselect)
   | Oselectfs, v0::v1::vselect::nil => Some (eval_selectfs v0 v1 vselect)
   | _, _ => None
@@ -676,7 +680,7 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Ocmp c => (type_of_condition c, Tint)
                 
   | Oselect cond => (Tint :: Tint :: (arg_type_of_condition0 cond) :: nil, Tint)
-  | Oselectl => (Tlong :: Tlong :: Tint :: nil, Tlong)
+  | Oselectl cond => (Tlong :: Tlong :: (arg_type_of_condition0 cond) :: nil, Tlong)
   | Oselectf  => (Tfloat :: Tfloat :: Tint :: nil, Tfloat)
   | Oselectfs => (Tsingle :: Tsingle :: Tint :: nil, Tsingle)
   end.
@@ -924,7 +928,15 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
       destruct (_ && _); simpl; trivial.
       destruct (Val.cmp_different_blocks _); simpl; trivial.
   (* selectl *)
-  - destruct v0; destruct v1; destruct v2; simpl in *; try discriminate; trivial.
+  - destruct v0; destruct v1; simpl in *; try discriminate; trivial.
+    destruct cond; destruct v2; simpl in *; trivial.
+    + destruct Archi.ptr64; simpl; trivial.
+      destruct (_ && _); simpl; trivial.
+      destruct (Val.cmp_different_blocks _); simpl; trivial.
+    + destruct Archi.ptr64; simpl; trivial.
+      destruct (_ && _); simpl; trivial.
+      destruct (Val.cmp_different_blocks _); simpl; trivial.
+
   (* selectf *)
   - destruct v0; destruct v1; destruct v2; simpl in *; try discriminate; trivial.
   (* selectfs *)
@@ -1092,6 +1104,9 @@ Definition op_depends_on_memory (op: operation) : bool :=
 
   | Oselect (Ccompu0 _) => negb Archi.ptr64
   | Oselect (Ccomplu0 _) => Archi.ptr64
+
+  | Oselectl (Ccompu0 _) => negb Archi.ptr64
+  | Oselectl (Ccomplu0 _) => Archi.ptr64
                                 
   | _ => false
   end.
@@ -1104,7 +1119,7 @@ Proof.
   intros until m2. destruct op; simpl; try congruence;
                      
   destruct cond; simpl; intros SF; auto; rewrite ? negb_false_iff in SF;
-  unfold eval_select, eval_condition0, Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity.
+  unfold eval_select, eval_selectl, eval_condition0, Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity.
 Qed.
 
 (** Global variables mentioned in an operation or addressing mode *)
@@ -1488,9 +1503,19 @@ Proof.
       assumption.
     * rewrite Hcond'. constructor.
   (* selectl *)
-  - inv H3; simpl; try constructor.
-    inv H4; simpl; try constructor.
-    inv H2; simpl; constructor.
+  - unfold eval_selectl.
+    inv H4; trivial.
+    inv H2; trivial.
+    inv H3; trivial;
+      try (destruct cond; simpl; trivial; fail).
+    destruct (eval_condition0 cond (Vptr _ _) m1) eqn:Hcond; trivial.
+    eassert (Hcond' : ((eval_condition0 cond (Vptr b2 (Ptrofs.add ofs1 (Ptrofs.repr delta)))) m2) = Some b).
+    * eapply eval_condition0_inj.
+      eapply Val.inject_ptr.
+      eassumption.
+      reflexivity.
+      assumption.
+    * rewrite Hcond'. constructor.
   (* selectf *)
   - inv H3; simpl; try constructor.
     inv H4; simpl; try constructor.
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 906d6791..eeb3ffae 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -62,10 +62,20 @@ Section SELECT.
 Context {hf: helper_functions}.
 
 (** Ternary operator *)
-Definition select o0 o1 oselect :=
+Definition select_base o0 o1 oselect :=
  Eop (Oselect (Ccomp0 Cne))
               (o0:::o1:::oselect:::Enil).
 				      
+Definition select o0 o1 oselect :=
+  select_base o0 o1 oselect.
+				      
+Definition selectl_base o0 o1 oselect :=
+ Eop (Oselectl (Ccomp0 Cne))
+              (o0:::o1:::oselect:::Enil).
+				      
+Definition selectl o0 o1 oselect :=
+  selectl_base o0 o1 oselect.
+				      
 (** ** Constants **)
 
 Definition addrsymbol (id: ident) (ofs: ptrofs) :=
@@ -288,7 +298,7 @@ Nondetfunction or (e1: expr) (e2: expr) :=
      if same_expr_pure y0 y1
      && Int.eq zero0 Int.zero
      && Int.eq zero1 Int.zero                 
-     then select v0 v1 y0
+     then select_base v0 v1 y0
      else Eop Oor (e1:::e2:::Enil)
   |  (Eop Oand ((Eop Oneg ((Eop (Ocmp (Ccompuimm Ceq zero0))
         (y0:::Enil)):::Enil)):::v0:::Enil)),
@@ -297,7 +307,7 @@ Nondetfunction or (e1: expr) (e2: expr) :=
      if same_expr_pure y0 y1
      && Int.eq zero0 Int.zero
      && Int.eq zero1 Int.zero                 
-     then select v0 v1 y0
+     then select_base v0 v1 y0
      else Eop Oor (e1:::e2:::Enil)
   | _, _ => Eop Oor (e1:::e2:::Enil)
   end.
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v
index e791cc40..62cfa85e 100644
--- a/mppa_k1c/ValueAOp.v
+++ b/mppa_k1c/ValueAOp.v
@@ -56,12 +56,9 @@ Definition eval_static_select (cond : condition0) (v0 v1 vselect : aval) : aval
   | _ => Vtop
   end.
 
-Definition eval_static_selectl (v0 v1 vselect : aval) : aval :=
-  match vselect with
-  | I iselect =>
-    if Int.eq Int.zero iselect
-    then binop_long (fun x0 x1 => x0) v0 v1
-    else binop_long (fun x0 x1 => x1) v0 v1
+Definition eval_static_selectl (cond : condition0) (v0 v1 vselect : aval) : aval :=
+  match eval_static_condition0 cond vselect with
+  | Just b => binop_long (fun x0 x1 => if b then x1 else x0) v0 v1
   | _ => Vtop
   end.
 
@@ -208,7 +205,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Osingleoflongu, v1::nil => singleoflongu v1
   | Ocmp c, _ => of_optbool (eval_static_condition c vl)
   | (Oselect cond), v0::v1::vselect::nil => eval_static_select cond v0 v1 vselect
-  | Oselectl, v0::v1::vselect::nil => eval_static_selectl v0 v1 vselect               
+  | (Oselectl cond), v0::v1::vselect::nil => eval_static_selectl cond v0 v1 vselect               
   | Oselectf, v0::v1::vselect::nil => eval_static_selectf v0 v1 vselect
   | Oselectfs, v0::v1::vselect::nil => eval_static_selectfs v0 v1 vselect               
   | _, _ => Vbot
@@ -307,11 +304,15 @@ Proof.
     + destruct (eval_condition0 cond a2 m); destruct a1; destruct a0; try apply vmatch_ifptr_undef.
       apply vmatch_ifptr_i.
   (* selectl *)
-  - inv H2; simpl; try constructor.
-    + destruct (Int.eq _ _); apply binop_long_sound; trivial.
-    + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor.
-    + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor.
-    + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor.
+  - assert (Hcond : (cmatch (eval_condition0 cond a2 m) (eval_static_condition0 cond b2))) by (apply eval_static_condition0_sound; assumption).
+    rewrite eval_selectl_to2.
+    unfold eval_selectl2.
+    inv Hcond; trivial; try constructor.
+    + apply binop_long_sound; assumption.
+    + destruct a1; destruct a0; try apply vmatch_ifptr_undef.
+      apply vmatch_ifptr_l.
+    + destruct (eval_condition0 cond a2 m); destruct a1; destruct a0; try apply vmatch_ifptr_undef.
+      apply vmatch_ifptr_l.
   (* selectf *)
   - inv H2; simpl; try constructor.
     + destruct (Int.eq _ _); apply binop_float_sound; trivial.