selectl with condition

1 files changed, 37 insertions, 13 deletions

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: