select_sound

4 files changed, 103 insertions, 39 deletions

diff --git a/backend/Selection.v b/backend/Selection.v
index b9f5448c..ec4a7b38 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -283,7 +283,7 @@ Definition sel_builtin optid ef args :=
            | Some id =>
              match args with
                | a1::a2::a3::nil =>
-                 OK (Sassign id (Eop Oselect
+                 OK (Sassign id (Eop (Oselect (Ccomp0 Ceq))
                                      ((sel_expr a3):::
                                       (sel_expr a2):::
                                       (sel_expr a1):::Enil)))
diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v
index ee3c4e27..375a9cfe 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 :=
@@ -146,19 +146,77 @@ Section SOUNDNESS.
 
 Variable ge: genv.
 Variable sp: block.
-Variables m m': mem.
-Hypothesis PERM: forall b ofs k p, Mem.perm m b ofs k p -> Mem.perm m' b ofs k p.
+Variables m1 m2: mem.
+Hypothesis PERM: forall b ofs k p, Mem.perm m1 b ofs k p -> Mem.perm m2 b ofs k p.
 
 Lemma needs_of_condition_sound:
   forall cond args b args',
-  eval_condition cond args m = Some b ->
+  eval_condition cond args m1 = Some b ->
   vagree_list args args' (needs_of_condition cond) ->
-  eval_condition cond args' m' = Some b.
+  eval_condition cond args' m2 = Some b.
 Proof.
   intros. unfold needs_of_condition in H0.
   eapply default_needs_of_condition_sound; eauto.
 Qed.
 
+Let valid_pointer_inj:
+  forall b1 ofs b2 delta,
+  inject_id b1 = Some(b2, delta) ->
+  Mem.valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true ->
+  Mem.valid_pointer m2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true.
+Proof.
+  unfold inject_id; intros. inv H. rewrite Ptrofs.add_zero.
+  rewrite Mem.valid_pointer_nonempty_perm in *. eauto.
+Qed.
+
+Let weak_valid_pointer_inj:
+  forall b1 ofs b2 delta,
+  inject_id b1 = Some(b2, delta) ->
+  Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true ->
+  Mem.weak_valid_pointer m2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true.
+Proof.
+  unfold inject_id; intros. inv H. rewrite Ptrofs.add_zero.
+  rewrite Mem.weak_valid_pointer_spec in *.
+  rewrite ! Mem.valid_pointer_nonempty_perm in *.
+  destruct H0; [left|right]; eauto.
+Qed.
+
+Let weak_valid_pointer_no_overflow:
+  forall b1 ofs b2 delta,
+  inject_id b1 = Some(b2, delta) ->
+  Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true ->
+  0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned.
+Proof.
+  unfold inject_id; intros. inv H. rewrite Z.add_0_r. apply Ptrofs.unsigned_range_2.
+Qed.
+
+Let valid_different_pointers_inj:
+  forall b1 ofs1 b2 ofs2 b1' delta1 b2' delta2,
+  b1 <> b2 ->
+  Mem.valid_pointer m1 b1 (Ptrofs.unsigned ofs1) = true ->
+  Mem.valid_pointer m1 b2 (Ptrofs.unsigned ofs2) = true ->
+  inject_id b1 = Some (b1', delta1) ->
+  inject_id b2 = Some (b2', delta2) ->
+  b1' <> b2' \/
+  Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta1)) <> Ptrofs.unsigned (Ptrofs.add ofs2 (Ptrofs.repr delta2)).
+Proof.
+  unfold inject_id; intros. left; congruence.
+Qed.
+
+Lemma needs_of_condition0_sound:
+  forall cond arg1 b arg2,
+  eval_condition0 cond arg1 m1 = Some b ->
+  vagree arg1 arg2 All ->
+  eval_condition0 cond arg2 m2 = Some b.
+Proof.
+  intros until arg2.
+  intros Hcond Hagree.
+  Check eval_condition_inj.
+  Check default_needs_of_condition_sound.
+  apply eval_condition0_inj with (f := inject_id) (m1 := m1) (v1 := arg1); simpl; auto.
+  apply val_inject_lessdef. apply lessdef_vagree. assumption.
+Qed.
+
 Lemma addl_sound:
   forall v1 w1 v2 w2 x,
   vagree v1 w1 (default x) -> vagree v2 w2 (default x) ->
@@ -186,26 +244,32 @@ Proof.
     inv H. inv H0.
     trivial.
 Qed.
-
+  
 Lemma select_sound:
-  forall v0 w0 v1 w1 v2 w2 x,
-    vagree v0 w0 (default x) ->
-    vagree v1 w1 (default x) ->
-    vagree v2 w2 (default x) ->
-    vagree (eval_select v0 v1 v2) (eval_select w0 w1 w2) x.
+  forall cond v0 w0 v1 w1 v2 w2,
+    vagree v0 w0 All ->
+    vagree v1 w1 All ->
+    vagree v2 w2 All ->
+    vagree (eval_select cond v0 v1 v2 m1) (eval_select cond w0 w1 w2 m2) All.
 Proof.
-  unfold default; intros.
-  destruct x; trivial.
-  - destruct v2; simpl; trivial.
-    destruct v0; simpl; trivial.
-    destruct v1; simpl; trivial.
-    inv H. inv H0. inv H1. simpl.
-    constructor.
-  - destruct v2; simpl; trivial.
-    destruct v0; simpl; trivial.
-    destruct v1; simpl; trivial.
-    inv H. inv H0. inv H1. simpl.
-    constructor.
+  intros.
+  rewrite eval_select_to2.
+  rewrite eval_select_to2.
+  unfold eval_select2.
+  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 *.
+  - 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.
+  - simpl. constructor.
 Qed.
 
 Lemma selectl_sound:
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index e619b2f5..51d70693 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -288,6 +288,21 @@ Definition eval_select (cond : condition0) (v0 : val) (v1 : val) (vselect : val)
     | _,_,_ => Vundef
   end.
 
+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_selectl (v0 : val) (v1 : val) (vselect : val) : val :=
   match vselect with
   | Vint iselect =>
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v
index af685a5e..e791cc40 100644
--- a/mppa_k1c/ValueAOp.v
+++ b/mppa_k1c/ValueAOp.v
@@ -56,21 +56,6 @@ Definition eval_static_select (cond : condition0) (v0 v1 vselect : aval) : aval
   | _ => Vtop
   end.
 
-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 =>