some more progress on select

4 files changed, 84 insertions, 59 deletions

diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index c3ea4baf..e619b2f5 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -283,18 +283,9 @@ Definition eval_condition0 (cond: condition0) (v1: val) (m: mem): option bool :=
   end.
 
 Definition eval_select (cond : condition0) (v0 : val) (v1 : val) (vselect : val) (m: mem) : val :=
-  match v0 with
-  | Vint i0 =>
-    match v1 with
-    | Vint i1 =>
-      match (eval_condition0 cond vselect m) with
-      | Some bval =>
-        Vint (if bval then i1 else i0)
-      | None => Vundef
-      end
-    | _ => Vundef
-    end
-  | _ => Vundef
+  match v0, v1, (eval_condition0 cond vselect m) with
+    | Vint i0, Vint i1, Some bval => Vint (if bval then i1 else i0)
+    | _,_,_ => Vundef
   end.
 
 Definition eval_selectl (v0 : val) (v1 : val) (vselect : val) : val :=
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 6d61e674..31e81093 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -283,7 +283,7 @@ Nondetfunction or (e1: expr) (e2: expr) :=
      if same_expr_pure y0 y1
      && Int.eq zero0 Int.zero
      && Int.eq zero1 Int.zero                 
-     then Eop Oselect (v0:::v1:::y0:::Enil)
+     then Eop (Oselect (Ccomp0 Cne)) (v0:::v1:::y0:::Enil)
      else Eop Oor (e1:::e2:::Enil)
   |  (Eop Oand ((Eop Oneg ((Eop (Ocmp (Ccompuimm Ceq zero0))
         (y0:::Enil)):::Enil)):::v0:::Enil)),
@@ -292,7 +292,7 @@ Nondetfunction or (e1: expr) (e2: expr) :=
      if same_expr_pure y0 y1
      && Int.eq zero0 Int.zero
      && Int.eq zero1 Int.zero                 
-     then Eop Oselect (v0:::v1:::y0:::Enil)
+     then Eop (Oselect (Ccompu0 Cne)) (v0:::v1:::y0:::Enil)
      else Eop Oor (e1:::e2:::Enil)
   | _, _ => Eop Oor (e1:::e2:::Enil)
   end.
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index 20ba74a1..4af5ccfa 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -582,22 +582,22 @@ Proof.
     inv H2. inv H5.
     replace v8 with v4 in * by congruence.
     rename v4 into vselect.
-    destruct vselect; simpl; trivial.
-    rewrite (Val.and_commut _ v5).
-    destruct v5; simpl; trivial.
-    rewrite (Val.and_commut _ v9).
-    rewrite Val.or_commut.
-    destruct v9; simpl; trivial.
-    rewrite int_eq_commut.
-    destruct (Int.eq i1 Int.zero); simpl.
-    + rewrite Int.and_zero.
-      rewrite Int.or_commut.
-      rewrite Int.or_zero.
+    destruct vselect; simpl; trivial;
+    destruct v5; simpl; trivial; destruct v9; simpl; trivial;
+    destruct (Int.eq i1 Int.zero); simpl; trivial.
+    + rewrite Int.neg_zero.
+      rewrite Int.and_commut.
       rewrite Int.and_mone.
+      rewrite Int.and_commut.
+      rewrite Int.and_zero.
+      rewrite Int.or_zero.
       reflexivity.
-    + rewrite Int.and_mone.
-      rewrite Int.neg_zero.
+    + rewrite Int.neg_zero.
+      rewrite Int.and_commut.
       rewrite Int.and_zero.
+      rewrite Int.and_commut.
+      rewrite Int.and_mone.
+      rewrite Int.or_commut.
       rewrite Int.or_zero.
       reflexivity.
   - (* select unsigned *)
@@ -620,22 +620,23 @@ Proof.
     inv H2. inv H5.
     replace v8 with v4 in * by congruence.
     rename v4 into vselect.
-    destruct vselect; simpl; trivial.
-    rewrite (Val.and_commut _ v5).
-    destruct v5; simpl; trivial.
-    rewrite (Val.and_commut _ v9).
-    rewrite Val.or_commut.
-    destruct v9; simpl; trivial.
-    rewrite int_eq_commut.
-    destruct (Int.eq i1 Int.zero); simpl.
-    + rewrite Int.and_zero.
-      rewrite Int.or_commut.
-      rewrite Int.or_zero.
+    destruct vselect; simpl; trivial;
+    destruct v5; simpl; trivial;
+    destruct v9; simpl; trivial;
+    destruct (Int.eq i1 Int.zero); simpl; trivial.
+    + rewrite Int.neg_zero.
+      rewrite Int.and_commut.
       rewrite Int.and_mone.
+      rewrite Int.and_commut.
+      rewrite Int.and_zero.
+      rewrite Int.or_zero.
       reflexivity.
-    + rewrite Int.and_mone.
-      rewrite Int.neg_zero.
+    + rewrite Int.neg_zero.
+      rewrite Int.and_commut.
       rewrite Int.and_zero.
+      rewrite Int.and_commut.
+      rewrite Int.and_mone.
+      rewrite Int.or_commut.
       rewrite Int.or_zero.
       reflexivity.
   - apply DEFAULT.
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v
index 122249a4..af685a5e 100644
--- a/mppa_k1c/ValueAOp.v
+++ b/mppa_k1c/ValueAOp.v
@@ -42,16 +42,36 @@ Definition eval_static_addressing (addr: addressing) (vl: list aval): aval :=
   | _, _ => Vbot
   end.
 
-Definition select (v0 v1 vselect : aval) : aval :=
-  match vselect with
-  | I iselect =>
-    if Int.eq Int.zero iselect
-    then binop_int (fun x0 x1 => x0) v0 v1
-    else binop_int (fun x0 x1 => x1) v0 v1
+Definition eval_static_condition0 (cond : condition0) (v : aval) : abool :=
+  match cond with
+  | Ccomp0 c => cmp_bool c v (I Int.zero)
+  | Ccompu0 c => cmpu_bool c v (I Int.zero)
+  | Ccompl0  c => cmpl_bool c v (L Int64.zero)
+  | Ccomplu0 c => cmplu_bool c v (L Int64.zero)
+  end.
+  
+Definition eval_static_select (cond : condition0) (v0 v1 vselect : aval) : aval :=
+  match eval_static_condition0 cond vselect with
+  | Just b => binop_int (fun x0 x1 => if b then x1 else x0) v0 v1
   | _ => Vtop
   end.
 
-Definition selectl (v0 v1 vselect : aval) : aval :=
+Definition eval_select2 (cond : condition0) (v0 : val) (v1 : val) (vselect : val) (m: mem) : val :=
+  match (eval_condition0 cond vselect m), v0, v1 with
+    | Some bval, Vint i0, Vint i1 => Vint (if bval then i1 else i0)
+    | _,_,_ => Vundef
+  end.
+
+Lemma eval_select_to2: forall cond v0 v1 vselect m,
+    (eval_select cond v0 v1 vselect m) =
+    (eval_select2 cond v0 v1 vselect m).
+Proof.
+  intros.
+  unfold eval_select2.
+  destruct v0; destruct v1; simpl; destruct (eval_condition0 cond vselect m); simpl; reflexivity.
+Qed.
+
+Definition eval_static_selectl (v0 v1 vselect : aval) : aval :=
   match vselect with
   | I iselect =>
     if Int.eq Int.zero iselect
@@ -60,7 +80,7 @@ Definition selectl (v0 v1 vselect : aval) : aval :=
   | _ => Vtop
   end.
 
-Definition selectf (v0 v1 vselect : aval) : aval :=
+Definition eval_static_selectf (v0 v1 vselect : aval) : aval :=
   match vselect with
   | I iselect =>
     if Int.eq Int.zero iselect
@@ -69,7 +89,7 @@ Definition selectf (v0 v1 vselect : aval) : aval :=
   | _ => Vtop
   end.
 
-Definition selectfs (v0 v1 vselect : aval) : aval :=
+Definition eval_static_selectfs (v0 v1 vselect : aval) : aval :=
   match vselect with
   | I iselect =>
     if Int.eq Int.zero iselect
@@ -202,10 +222,10 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Osingleoflong, v1::nil => singleoflong v1
   | Osingleoflongu, v1::nil => singleoflongu v1
   | Ocmp c, _ => of_optbool (eval_static_condition c vl)
-  | Oselect, v0::v1::vselect::nil => select v0 v1 vselect
-  | Oselectl, v0::v1::vselect::nil => selectl v0 v1 vselect               
-  | Oselectf, v0::v1::vselect::nil => selectf v0 v1 vselect
-  | Oselectfs, v0::v1::vselect::nil => selectfs v0 v1 vselect               
+  | (Oselect cond), v0::v1::vselect::nil => eval_static_select cond v0 v1 vselect
+  | Oselectl, v0::v1::vselect::nil => eval_static_selectl 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
   end.
 
@@ -231,6 +251,15 @@ Proof.
   destruct cond; auto with va.
 Qed.
 
+Theorem eval_static_condition0_sound:
+  forall cond varg m aarg,
+  vmatch bc varg aarg ->
+  cmatch (eval_condition0 cond varg m) (eval_static_condition0 cond aarg).
+Proof.
+  intros until aarg; intro VM.
+  destruct cond; simpl; eauto with va.
+Qed.
+
 Lemma symbol_address_sound:
   forall id ofs,
   vmatch bc (Genv.symbol_address ge id ofs) (Ptr (Gl id ofs)).
@@ -276,18 +305,22 @@ Theorem eval_static_operation_sound:
   list_forall2 (vmatch bc) vargs aargs ->
   vmatch bc vres (eval_static_operation op aargs).
 Proof.
-  unfold eval_operation, eval_static_operation; intros;
+  unfold eval_operation, eval_static_operation, eval_static_select, eval_static_selectl, eval_static_selectf, eval_static_selectfs; intros;
   destruct op; InvHyps; eauto with va.
   destruct (propagate_float_constants tt); constructor.
   destruct (propagate_float_constants tt); constructor.
   rewrite Ptrofs.add_zero_l; eauto with va.
   apply of_optbool_sound. eapply eval_static_condition_sound; eauto.
   (* select *)
-  - inv H2; simpl; try constructor.
-    + destruct (Int.eq _ _); apply binop_int_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_select_to2.
+    unfold eval_select2.
+    inv Hcond; trivial; try constructor.
+    + apply binop_int_sound; assumption.
+    + destruct a1; destruct a0; try apply vmatch_ifptr_undef.
+      apply vmatch_ifptr_i.
+    + 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.